Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
ca81a659
Commit
ca81a659
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-05-25 17:58:11 by cvscast] Display toplevel
Original author: cvscast Date: 2003-05-25 18:04:13+00:00
parent
3b7ef1a6
Changes
6
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
ca81a659
...
...
@@ -163,6 +163,7 @@ install_web:
scp webiface cduce@iris:cgi-bin/cduce
ssh cduce@iris
"chmod +s cgi-bin/cduce"
#
# Customize the following variables to match the settings
# of your local web server
...
...
@@ -180,7 +181,7 @@ install_web_local:web/files webiface
cp
web/img/
*
.
*
$(CDUCE_HTML_DIR)
/img
website
:
web/files
scp web/www/
*
.php web/cduce.css cduce@iris:public_html/
scp web/www/
*
.php web/cduce.css cduce@iris
.ens.fr
:public_html/
local_website
:
cduce
(
cd
web
;
../cduce
--quiet
site.cd
--arg
site.xml
)
...
...
driver/cduce.ml
View file @
ca81a659
...
...
@@ -31,132 +31,125 @@ let print_value ppf v =
let
dump_env
ppf
=
Format
.
fprintf
ppf
"Global types:"
;
Typer
.
dump_global_types
ppf
;
Format
.
fprintf
ppf
".@
\n
"
;
Format
.
fprintf
ppf
".@
.
"
;
Env
.
iter
(
fun
x
v
->
let
t
=
Env
.
find
x
!
typing_env
in
Format
.
fprintf
ppf
"@[|- %a : %a@ => %a@]@
\n
"
U
.
print
(
Id
.
value
x
)
print_norm
t
print_value
v
Format
.
fprintf
ppf
"@[val %a : @[%a = %a@]@]@."
U
.
print
(
Id
.
value
x
)
print_norm
t
print_value
v
)
!
eval_env
let
rec
print_exn
ppf
=
function
|
Location
(
loc
,
exn
)
->
Format
.
fprintf
ppf
"Error %a:@
\n
"
Location
.
print_loc
loc
;
Format
.
fprintf
ppf
"Error %a:@
.
"
Location
.
print_loc
loc
;
Format
.
fprintf
ppf
"%a"
Location
.
html_hilight
loc
;
print_exn
ppf
exn
|
Value
.
CDuceExn
v
->
Format
.
fprintf
ppf
"Uncaught CDuce exception: @[%a@]@
\n
"
Format
.
fprintf
ppf
"Uncaught CDuce exception: @[%a@]@
.
"
print_value
v
|
Eval
.
MultipleDeclaration
v
->
Format
.
fprintf
ppf
"Multiple declaration for global value %a@
\n
"
Format
.
fprintf
ppf
"Multiple declaration for global value %a@
.
"
U
.
print
(
Id
.
value
v
)
|
Typer
.
WrongLabel
(
t
,
l
)
->
Format
.
fprintf
ppf
"Wrong record selection: the label %a@
\n
"
Format
.
fprintf
ppf
"Wrong record selection: the label %a@
.
"
U
.
print
(
LabelPool
.
value
l
);
Format
.
fprintf
ppf
"applied to an expression of type:@
\n
%a@
\n
"
Format
.
fprintf
ppf
"applied to an expression of type:@
.
%a@
.
"
print_norm
t
|
Typer
.
ShouldHave
(
t
,
msg
)
->
Format
.
fprintf
ppf
"This expression should have type:@
\n
%a@
\n
%s@
\n
"
Format
.
fprintf
ppf
"This expression should have type:@
.
%a@
.
%s@
.
"
print_norm
t
msg
|
Typer
.
ShouldHave2
(
t1
,
msg
,
t2
)
->
Format
.
fprintf
ppf
"This expression should have type:@
\n
%a@
\n
%s %a@
\n
"
Format
.
fprintf
ppf
"This expression should have type:@
.
%a@
.
%s %a@
.
"
print_norm
t1
msg
print_norm
t2
|
Typer
.
Error
s
->
Format
.
fprintf
ppf
"%s@
\n
"
s
Format
.
fprintf
ppf
"%s@
.
"
s
|
Typer
.
Constraint
(
s
,
t
)
->
Format
.
fprintf
ppf
"This expression should have type:@
\n
%a@
\n
"
Format
.
fprintf
ppf
"This expression should have type:@
.
%a@
.
"
print_norm
t
;
Format
.
fprintf
ppf
"but its inferred type is:@
\n
%a@
\n
"
Format
.
fprintf
ppf
"but its inferred type is:@
.
%a@
.
"
print_norm
s
;
Format
.
fprintf
ppf
"which is not a subtype, as shown by the sample:@
\n
%a@
\n
"
Format
.
fprintf
ppf
"which is not a subtype, as shown by the sample:@
.
%a@
.
"
print_sample
(
Sample
.
get
(
Types
.
diff
s
t
))
|
Typer
.
NonExhaustive
t
->
Format
.
fprintf
ppf
"This pattern matching is not exhaustive@
\n
"
;
Format
.
fprintf
ppf
"Residual type:@
\n
%a@
\n
"
Format
.
fprintf
ppf
"This pattern matching is not exhaustive@
.
"
;
Format
.
fprintf
ppf
"Residual type:@
.
%a@
.
"
print_norm
t
;
Format
.
fprintf
ppf
"Sample:@
\n
%a@
\n
"
print_sample
(
Sample
.
get
t
)
Format
.
fprintf
ppf
"Sample:@
.
%a@
.
"
print_sample
(
Sample
.
get
t
)
|
Typer
.
UnboundId
x
->
Format
.
fprintf
ppf
"Unbound identifier %a@
\n
"
U
.
print
(
Id
.
value
x
)
Format
.
fprintf
ppf
"Unbound identifier %a@
.
"
U
.
print
(
Id
.
value
x
)
|
Wlexer
.
Illegal_character
c
->
Format
.
fprintf
ppf
"Illegal character (%s)@
\n
"
(
Char
.
escaped
c
)
Format
.
fprintf
ppf
"Illegal character (%s)@
.
"
(
Char
.
escaped
c
)
|
Wlexer
.
Unterminated_comment
->
Format
.
fprintf
ppf
"Comment not terminated@
\n
"
Format
.
fprintf
ppf
"Comment not terminated@
.
"
|
Wlexer
.
Unterminated_string
->
Format
.
fprintf
ppf
"String literal not terminated@
\n
"
Format
.
fprintf
ppf
"String literal not terminated@
.
"
|
Wlexer
.
Unterminated_string_in_comment
->
Format
.
fprintf
ppf
"This comment contains an unterminated string literal@
\n
"
Format
.
fprintf
ppf
"This comment contains an unterminated string literal@
.
"
|
Parser
.
Error
s
|
Stream
.
Error
s
->
Format
.
fprintf
ppf
"Parsing error: %s@
\n
"
s
Format
.
fprintf
ppf
"Parsing error: %s@
.
"
s
|
Location
.
Generic
s
->
Format
.
fprintf
ppf
"%s@
\n
"
s
Format
.
fprintf
ppf
"%s@
.
"
s
|
exn
->
(* raise exn *)
Format
.
fprintf
ppf
"%s@
\n
"
(
Printexc
.
to_string
exn
)
Format
.
fprintf
ppf
"%s@
.
"
(
Printexc
.
to_string
exn
)
let
debug
ppf
=
function
|
`Subtype
(
t1
,
t2
)
->
Format
.
fprintf
ppf
"[DEBUG:subtype]@
\n
"
;
Format
.
fprintf
ppf
"[DEBUG:subtype]@
.
"
;
let
t1
=
Types
.
descr
(
Typer
.
typ
t1
)
and
t2
=
Types
.
descr
(
Typer
.
typ
t2
)
in
Format
.
fprintf
ppf
"%a <= %a : %b@
\n
"
print_norm
t1
print_norm
t2
Format
.
fprintf
ppf
"%a <= %a : %b@
.
"
print_norm
t1
print_norm
t2
(
Types
.
subtype
t1
t2
)
|
`Sample
t
->
Format
.
fprintf
ppf
"[DEBUG:sample]@
\n
"
;
let
t
=
Types
.
descr
(
Typer
.
typ
t
)
in
Format
.
fprintf
ppf
"%a@
\n
"
print_sample
(
Sample
.
get
t
)
Format
.
fprintf
ppf
"[DEBUG:sample]@."
;
(
try
let
t
=
Types
.
descr
(
Typer
.
typ
t
)
in
Format
.
fprintf
ppf
"%a@."
print_sample
(
Sample
.
get
t
)
with
Not_found
->
Format
.
fprintf
ppf
"Empty type : no sample !@."
)
|
`Filter
(
t
,
p
)
->
Format
.
fprintf
ppf
"[DEBUG:filter]@
\n
"
;
Format
.
fprintf
ppf
"[DEBUG:filter]@
.
"
;
let
t
=
Typer
.
typ
t
and
p
=
Typer
.
pat
p
in
let
f
=
Patterns
.
filter
(
Types
.
descr
t
)
p
in
List
.
iter
(
fun
(
x
,
t
)
->
Format
.
fprintf
ppf
" %a:%a@
\n
"
U
.
print
(
Id
.
value
x
)
Format
.
fprintf
ppf
" %a:%a@
.
"
U
.
print
(
Id
.
value
x
)
print_norm
(
Types
.
descr
t
))
f
|
`Accept
p
->
Format
.
fprintf
ppf
"[DEBUG:accept]@
\n
"
;
Format
.
fprintf
ppf
"[DEBUG:accept]@
.
"
;
let
p
=
Typer
.
pat
p
in
let
t
=
Patterns
.
accept
p
in
Format
.
fprintf
ppf
" %a@
\n
"
Types
.
Print
.
print
(
Types
.
descr
t
)
Format
.
fprintf
ppf
" %a@
.
"
Types
.
Print
.
print
(
Types
.
descr
t
)
|
`Compile
(
t
,
pl
)
->
Format
.
fprintf
ppf
"[DEBUG:compile]@
\n
"
;
Format
.
fprintf
ppf
"[DEBUG:compile]@
.
"
;
let
t
=
Typer
.
typ
t
and
pl
=
List
.
map
Typer
.
pat
pl
in
Patterns
.
Compile
.
debug_compile
ppf
t
pl
let
insert_type_bindings
ppf
=
List
.
iter
(
fun
(
x
,
t
)
->
let
insert_bindings
ppf
=
List
.
iter2
(
fun
(
x
,
t
)
(
y
,
v
)
->
assert
(
x
=
y
);
typing_env
:=
Env
.
add
x
t
!
typing_env
;
if
not
!
quiet
then
Format
.
fprintf
ppf
"|- %a : %a@."
U
.
print
(
Id
.
value
x
)
print_norm
t
)
let
insert_eval_bindings
ppf
=
List
.
iter
(
fun
(
x
,
v
)
->
eval_env
:=
Env
.
add
x
v
!
eval_env
;
if
not
!
quiet
then
Format
.
fprintf
ppf
"=> %a : @[%a@]@."
U
.
print
(
Id
.
value
x
)
print_value
v
)
Format
.
fprintf
ppf
"val %a : @[%a@] = @[%a@]@."
U
.
print
(
Id
.
value
x
)
print_norm
t
print_value
v
)
let
rec
collect_funs
ppf
accu
=
function
|
{
descr
=
Ast
.
FunDecl
e
}
::
rest
->
let
(
_
,
e
)
=
Typer
.
expr
e
in
collect_funs
ppf
(
e
::
accu
)
rest
|
rest
->
insert_type_bindings
ppf
(
Typer
.
type_rec_funs
!
typing_env
accu
);
let
typs
=
Typer
.
type_rec_funs
!
typing_env
accu
in
Typer
.
report_unused_branches
()
;
insert_eval_bindings
ppf
(
Eval
.
eval_rec_funs
!
eval_env
accu
);
let
vals
=
Eval
.
eval_rec_funs
!
eval_env
accu
in
insert_bindings
ppf
typs
vals
;
rest
let
rec
collect_types
ppf
accu
=
function
...
...
@@ -177,23 +170,21 @@ let rec phrases ppf phs = match phs with
Typer
.
report_unused_branches
()
;
if
not
!
quiet
then
Location
.
dump_loc
ppf
e
.
Typed
.
exp_loc
;
if
not
!
quiet
then
Format
.
fprintf
ppf
"|- %a@."
print_norm
t
;
let
v
=
Eval
.
eval
!
eval_env
e
in
if
not
!
quiet
then
Format
.
fprintf
ppf
"
=> @[%a@]@."
print_value
v
;
Format
.
fprintf
ppf
"
- : @[%a@] = @[%a@]@."
print_norm
t
print_value
v
;
phrases
ppf
rest
|
{
descr
=
Ast
.
LetDecl
(
p
,
e
)
}
::
rest
->
let
decl
=
Typer
.
let_decl
p
e
in
insert_type_bindings
ppf
(
Typer
.
type_let_decl
!
typing_env
decl
);
let
typs
=
Typer
.
type_let_decl
!
typing_env
decl
in
Typer
.
report_unused_branches
()
;
insert_eval_bindings
ppf
(
Eval
.
eval_let_decl
!
eval_env
decl
);
let
vals
=
Eval
.
eval_let_decl
!
eval_env
decl
in
insert_bindings
ppf
typs
vals
;
phrases
ppf
rest
|
{
descr
=
Ast
.
Debug
l
}
::
rest
->
debug
ppf
l
;
phrases
ppf
rest
|
[]
->
()
|
_
->
assert
false
let
run
rule
ppf
ppf_err
input
=
try
...
...
driver/examples.ml
View file @
ca81a659
...
...
@@ -21,13 +21,12 @@ let fun f4 (A -> String; ['0'--'9'+] -> Int)
| x -> int_of x;;
f4
\"
123
\"
;;
"
;
"mutrec"
,
"(* A
ll the types submitted
at
on
ce
are mutually recursive *)
"
;
"mutrec"
,
"(* A
djacent type declar
at
i
on
s
are mutually recursive *)
type T = <t>S;;
type S = [ (Char | T)* ];;
let x : S = [ 'abc' <t>['def'] 'ghi' ];;
(* Consecutive function definitions (without any other toplevel phrase
in the middle) are grouped together *)
(* Similarly for toplevel function definitions *)
let fun f (x : Int) : Int = g x;;
let fun g (x : Int) : Int = 3;;
...
...
driver/webiface.ml
View file @
ca81a659
...
...
@@ -292,7 +292,7 @@ let main (cgi : Netcgi.std_activation) =
|
`Close
->
dialog
""
|
`Example
->
dialog
(
example
(
cgi
#
argument_value
"example"
))
);
p
"
p
(
"
<div class=
\"
box
\"
><h2>About the prototype</h2>
<p>
CDuce is under active development; some features may not work properly.
...
...
@@ -303,7 +303,9 @@ and uses several OCaml packages:
<a href='http://ocamlnet.sourceforge.net/'>OCamlnet</a>,
<a href='http://www.ocaml-programming.de/programming/pxp.html'>PXP</a>,
<a href='http://www.eleves.ens.fr/home/frisch/soft#wlex'>wlex</a>.</p>
<p><a href='mailto:Alain.Frisch@ens.fr'>Webmaster</a></p></div>"
;
<p><a href='mailto:Alain.Frisch@ens.fr'>Webmaster</a></p>
<p>Prototype version "
^
Cduce_config
.
version
^
",
built on "
^
Cduce_config
.
build_date
^
".</p></div>"
);
html_footer
p
;
cgi
#
output
#
commit_work
()
with
...
...
parser/ast.ml
View file @
ca81a659
...
...
@@ -8,7 +8,6 @@ type pprog = pmodule_item list
and
pmodule_item
=
pmodule_item'
located
and
pmodule_item'
=
|
TypeDecl
of
string
*
ppat
|
PatDecl
of
string
*
ppat
|
LetDecl
of
ppat
*
pexpr
|
FunDecl
of
pexpr
|
EvalStatement
of
pexpr
...
...
web/manual/interpreter.xml
View file @
ca81a659
...
...
@@ -46,6 +46,50 @@ scripts, which are executed successively.</li>
</box>
<box
title=
"Phrases"
link=
"phrases"
>
<p>
CDuce programs are sequences of phrases, which can
be juxtaposed or separated by
<code>
;;
</code>
. There are five kinds of
phrases:
</p>
<ul>
<li>
Types declarations
<code>
type %%T%% = %%t%%
</code>
. Adjacent types declarations are mutually
recursives, e.g.:
<sample>
<![CDATA[
type T = <a>
[ S* ]
type S =
<b>
[ T ]
]]>
</sample>
</li>
<li>
Function declarations
<code>
let fun %%f%% %%...%%
</code>
.
Adjacent function declarations are mutually recursives, e.g.:
<sample>
<![CDATA[
let fun f (x : Int) : Int = g x
let fun g (x : Int) : Int = x + 1
]]>
</sample>
</li>
<li>
Global bindings
<code>
let %%p%% = %%e%%
</code>
or
<code>
let %%p%% : %%t%% = %%e%%
</code>
.
</li>
<li>
Evaluation statements (an expression to evaluate).
</li>
<li>
Debugging statements:
<sample>
<![CDATA[
debug filter %%t%% %%p%% {{ inference for pattern matching }}
debug accept %%p%% {{ type accepted by a pattern }}
debug sample %%t%% {{ compute a sample from a type }}
debug subtype %%t%%1 %%t2%% {{ check subtyping }}
debug compile %%t%% %%p%%1 ... %%pn%% {{ compilation of pattern matching }}
]]>
</sample>
</li>
</ul>
</box>
<box
title=
"Toplevel"
link=
"toplevel"
>
<p>
...
...
@@ -55,11 +99,17 @@ behaves as an interactive toplevel.
<p>
Toplevel phrases are processed after each
<code>
;;
</code>
.
Mutually recursive declaration of types or functions
Mutually recursive declaration
s
of types or functions
must be contained in a single adjacent sequence of phrases
(without
<code>
;;
</code>
inbetween).
</p>
<p>
In order to allow persistence (option
<code>
--dump
</code>
to operate,
you must quit the toplevel with
<code>
Ctrl-D
</code>
and not
<code>
Ctrl-C
</code>
</p>
<p>
The toplevel has no line editing facilities.
You can use an external wrapper such as
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment