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
0dfcb292
Commit
0dfcb292
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-02-17 21:51:52 by cvscast] Empty log message
Original author: cvscast Date: 2003-02-17 21:51:53+00:00
parent
3f87b380
Changes
3
Hide whitespace changes
Inline
Side-by-side
driver/cduce.ml
View file @
0dfcb292
open
Location
let
quiet
=
ref
false
let
typing_env
=
State
.
ref
"Cduce.typing_env"
Typer
.
Env
.
empty
let
glb_env
=
State
.
ref
"Cduce.glb_env"
Typer
.
Env
.
empty
let
eval_env
=
Eval
.
global_env
...
...
@@ -172,7 +174,8 @@ let run ppf ppf_err input =
let
insert_type_bindings
=
List
.
iter
(
fun
(
x
,
t
)
->
typing_env
:=
Typer
.
Env
.
add
x
t
!
typing_env
;
Format
.
fprintf
ppf
"|- %s : %a@
\n
@."
x
print_norm
t
)
if
not
!
quiet
then
Format
.
fprintf
ppf
"|- %s : %a@
\n
@."
x
print_norm
t
)
in
let
type_decl
decl
=
...
...
@@ -184,7 +187,8 @@ let run ppf ppf_err input =
List
.
iter
(
fun
(
x
,
v
)
->
Eval
.
enter_global
x
v
;
Format
.
fprintf
ppf
"=> %s : @[%a@]@
\n
@."
x
print_value
v
if
not
!
quiet
then
Format
.
fprintf
ppf
"=> %s : @[%a@]@
\n
@."
x
print_value
v
)
bindings
in
...
...
@@ -194,9 +198,11 @@ let run ppf ppf_err input =
let
(
fv
,
e
)
=
Typer
.
expr
!
glb_env
e
in
let
t
=
Typer
.
type_check
!
typing_env
e
Types
.
any
true
in
Location
.
dump_loc
ppf
e
.
Typed
.
exp_loc
;
Format
.
fprintf
ppf
"|- %a@
\n
@."
print_norm
t
;
if
not
!
quiet
then
Format
.
fprintf
ppf
"|- %a@
\n
@."
print_norm
t
;
let
v
=
Eval
.
eval
Eval
.
Env
.
empty
e
in
Format
.
fprintf
ppf
"=> @[%a@]@
\n
@."
print_value
v
if
not
!
quiet
then
Format
.
fprintf
ppf
"=> @[%a@]@
\n
@."
print_value
v
|
Ast
.
LetDecl
(
p
,
{
descr
=
Ast
.
Abstraction
_
})
->
()
|
Ast
.
LetDecl
(
p
,
e
)
->
let
decl
=
Typer
.
let_decl
!
glb_env
p
e
in
...
...
driver/cduce.mli
View file @
0dfcb292
val
quiet
:
bool
ref
val
typing_env
:
Typer
.
env
ref
(* Types of toplevel bindings *)
val
eval_env
:
Eval
.
env
ref
(* Values of toplevel bindings *)
val
glb_env
:
Typer
.
glb
ref
(* Global types *)
...
...
driver/run.ml
View file @
0dfcb292
...
...
@@ -2,12 +2,11 @@ let () = State.close ();;
let
dump
=
ref
None
let
src
=
ref
[]
let
quiet
=
ref
false
let
specs
=
[
"-dump"
,
Arg
.
String
(
fun
s
->
dump
:=
Some
s
)
,
" specify filename for persistency"
;
"-quiet"
,
Arg
.
Set
quiet
,
"-quiet"
,
Arg
.
Set
Cduce
.
quiet
,
"suppress normal output (typing, results)"
]
...
...
@@ -16,7 +15,7 @@ let () =
"cduce [options] [script]
\n\n
Options:"
let
ppf
=
if
!
quiet
then
Format
.
formatter_of_buffer
(
Buffer
.
create
1023
)
if
!
Cduce
.
quiet
then
Format
.
formatter_of_buffer
(
Buffer
.
create
1023
)
else
Format
.
std_formatter
let
ppf_err
=
Format
.
err_formatter
...
...
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