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
d05c1abe
Commit
d05c1abe
authored
Jun 19, 2014
by
Pietro Abate
Browse files
Large refactoring of printinf functions
parent
c15314b2
Changes
18
Hide whitespace changes
Inline
Side-by-side
compile/lambda.ml
View file @
d05c1abe
...
...
@@ -99,8 +99,8 @@ module Print = struct
let
pp_aux
ppf
=
Utils
.
pp_list
(
fun
ppf
(
t1
,
t2
)
->
Format
.
fprintf
ppf
"(%a -> %a)"
Types
.
Print
.
p
rint
t1
Types
.
Print
.
p
rint
t2
Types
.
Print
.
p
p_type
t1
Types
.
Print
.
p
p_type
t2
)
ppf
in
function
...
...
compile/lambda.mli
View file @
d05c1abe
...
...
@@ -77,6 +77,6 @@ type code_item =
type
code
=
code_item
list
module
Print
:
sig
val
string_of_lambda
:
expr
->
string
val
pp_lambda
:
Format
.
formatter
->
expr
->
unit
val
string_of_lambda
:
expr
->
string
end
compile/print_auto.ml
View file @
d05c1abe
...
...
@@ -10,7 +10,7 @@ let rec_state ppf d =
let
rec
print_source
lhs
ppf
=
function
|
Catch
->
Format
.
fprintf
ppf
"v"
|
Const
c
->
Types
.
Print
.
p
rint
_const
ppf
c
|
Const
c
->
Types
.
Print
.
p
p
_const
ppf
c
|
Nil
->
Format
.
fprintf
ppf
"`nil"
|
Left
->
Format
.
fprintf
ppf
"v1"
|
Right
->
Format
.
fprintf
ppf
"v2"
...
...
@@ -55,7 +55,7 @@ let print_kind ppf actions =
Format
.
fprintf
ppf
")"
in
let
print_basic
(
t
,
ret
)
=
Format
.
fprintf
ppf
" | %a -> %a@
\n
"
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
p_type
t
(
print_ret
[]
)
ret
in
let
print_prod2
lhs
=
function
...
...
driver/cduce.ml
View file @
d05c1abe
...
...
@@ -40,7 +40,7 @@ let rec is_abstraction = function
|
_
->
false
let
print_norm
ppf
d
=
Types
.
Print
.
p
rint
ppf
((
*
Types
.
normalize
*
)
d
)
Types
.
Print
.
p
p_type
ppf
((
*
Types
.
normalize
*
)
d
)
let
print_sample
ppf
s
=
Sample
.
print
ppf
s
...
...
@@ -159,16 +159,16 @@ let rec print_exn ppf = function
U
.
print
ns2
|
Sequence
.
Error
(
Sequence
.
CopyTag
(
t
,
expect
))
->
Format
.
fprintf
ppf
"Tags in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
rint
expect
Types
.
Print
.
p
p_type
t
Types
.
Print
.
p
p_type
expect
Sample
.
print
(
Sample
.
get
(
Types
.
diff
t
expect
))
|
Sequence
.
Error
(
Sequence
.
CopyAttr
(
t
,
expect
))
->
Format
.
fprintf
ppf
"Attributes in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
rint
expect
Types
.
Print
.
p
p_type
t
Types
.
Print
.
p
p_type
expect
Sample
.
print
(
Sample
.
get
(
Types
.
diff
t
expect
))
|
Sequence
.
Error
(
Sequence
.
UnderTag
(
t
,
exn
))
->
Format
.
fprintf
ppf
"Under tag %a:@."
Types
.
Print
.
p
rint
t
;
Format
.
fprintf
ppf
"Under tag %a:@."
Types
.
Print
.
p
p_type
t
;
print_exn
ppf
exn
|
exn
->
...
...
@@ -199,7 +199,7 @@ let debug ppf tenv cenv = function
let
t
=
Typer
.
typ
tenv
t
and
p
=
Typer
.
pat
tenv
p
in
Format
.
fprintf
ppf
"[DEBUG:filter t=%a p=%a]@."
Types
.
Print
.
p
rint
(
Types
.
descr
t
)
Types
.
Print
.
p
p_type
(
Types
.
descr
t
)
Patterns
.
Print
.
print
(
Patterns
.
descr
p
);
let
f
=
Patterns
.
filter
(
Types
.
descr
t
)
p
in
IdMap
.
iteri
(
fun
x
t
->
...
...
@@ -210,7 +210,7 @@ let debug ppf tenv cenv = function
Format
.
fprintf
ppf
"[DEBUG:accept]@."
;
let
p
=
Typer
.
pat
tenv
p
in
let
t
=
Patterns
.
accept
p
in
Format
.
fprintf
ppf
" %a@."
Types
.
Print
.
p
rint
(
Types
.
descr
t
)
Format
.
fprintf
ppf
" %a@."
Types
.
Print
.
p
p_type
(
Types
.
descr
t
)
|
`Compile
(
t
,
pl
)
->
Format
.
fprintf
ppf
"[DEBUG:compile]@."
;
let
no
=
ref
(
-
1
)
in
...
...
@@ -230,7 +230,7 @@ let debug ppf tenv cenv = function
let
t
=
Typer
.
typ
tenv
t
in
(
try
let
c
=
Sample
.
single
(
Types
.
descr
t
)
in
Format
.
fprintf
ppf
"Constant:%a@."
Types
.
Print
.
p
rint
_const
c
Format
.
fprintf
ppf
"Constant:%a@."
Types
.
Print
.
p
p
_const
c
with
|
Exit
->
Format
.
fprintf
ppf
"Non constant@."
|
Not_found
->
Format
.
fprintf
ppf
"Empty@."
)
...
...
@@ -247,7 +247,7 @@ let directive ppf tenv cenv = function
dump_env
ppf
tenv
cenv
|
`Print_type
t
->
let
t
=
Typer
.
typ
tenv
t
in
Format
.
fprintf
ppf
"%a@."
Types
.
Print
.
p
rint
_noname
(
Types
.
descr
t
)
Format
.
fprintf
ppf
"%a@."
Types
.
Print
.
p
p
_noname
(
Types
.
descr
t
)
|
`Reinit_ns
->
Typer
.
set_ns_table_for_printer
tenv
|
`Help
->
...
...
driver/librarian.ml
View file @
d05c1abe
...
...
@@ -70,7 +70,7 @@ let show ppf id t v =
|
Some
id
->
Format
.
fprintf
ppf
"@[val %a : @[%a@]@."
Ident
.
print
id
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
p_type
t
|
None
->
()
...
...
runtime/eval.ml
View file @
d05c1abe
...
...
@@ -165,7 +165,7 @@ and eval_abstraction env locals slots iface body lsize sigma =
let
f
arg
=
let
v
=
eval_branches
env
(
Array
.
create
lsize
Value
.
Absent
)
body
arg
in
if
sigma
<>
Value
.
Mono
then
env
.
(
1
)
<-
arg
;
pp_lambda_env
Format
.
std_formatter
env
locals
;
(*
pp_lambda_env Format.std_formatter env locals;
*)
v
in
let
a
=
Value
.
Abstraction
(
Some
iface
,
f
,
sigma
)
in
...
...
runtime/value.ml
View file @
d05c1abe
...
...
@@ -38,11 +38,8 @@ let rec codomain = function
(* Comp for Value.sigma but simplify if possible. *)
let
rec
comp
s1
s2
=
match
s1
,
s2
with
|
Identity
,
_
->
s2
|
_
,
Identity
->
s1
|
Mono
,
_
->
s2
|
_
,
Mono
->
s1
|
Identity
,
_
|
Mono
,
_
->
s2
|
_
,
Identity
|
_
,
Mono
->
s1
|
Comp
(
s3
,
s4
)
,
List
(
_
)
->
(
match
comp
s4
s2
with
|
Comp
(
_
)
as
s5
when
s4
=
s5
->
s1
...
...
@@ -128,9 +125,7 @@ let concat v1 v2 =
let
append
v1
v2
=
concat
v1
(
Pair
(
v2
,
nil
,
Mono
))
let
raise'
v
=
raise
(
CDuceExn
v
)
let
failwith'
s
=
raise'
(
string_latin1
s
)
let
failwith'
s
=
raise
(
CDuceExn
(
string_latin1
s
))
let
rec
const
=
function
|
Types
.
Integer
i
->
Integer
i
...
...
@@ -177,8 +172,6 @@ let normalize_string_utf8 i j s q =
let
(
c
,
i
)
=
Utf8
.
next
s
i
in
Pair
(
Char
(
Chars
.
V
.
mk_int
c
)
,
String_utf8
(
i
,
j
,
s
,
q
)
,
Mono
)
(***** The dirty things **********)
type
pair
=
{
dummy
:
t
;
mutable
pair_tl
:
t
}
...
...
@@ -237,7 +230,6 @@ let eval_lazy_concat v =
Obj
.
set_field
v
1
(
Obj
.
field
nv
1
)
(******************************)
let
normalize
=
function
...
...
@@ -314,8 +306,8 @@ module Print = struct
let
pp_aux
ppf
=
Utils
.
pp_list
(
fun
ppf
(
t1
,
t2
)
->
Format
.
fprintf
ppf
"(%a -> %a)"
Types
.
Print
.
p
rint
t1
Types
.
Print
.
p
rint
t2
Types
.
Print
.
p
p_type
t1
Types
.
Print
.
p
p_type
t2
)
ppf
in
function
...
...
@@ -328,8 +320,8 @@ module Print = struct
let
pp_iface
ppf
l
=
let
f
ppf
(
t1
,
t2
)
=
Format
.
fprintf
ppf
"(%a,%a)"
Types
.
Print
.
p
rint
t1
Types
.
Print
.
p
rint
t2
Types
.
Print
.
p
p_type
t1
Types
.
Print
.
p
p_type
t2
in
Utils
.
pp_list
f
ppf
l
...
...
@@ -502,6 +494,22 @@ let dump_xml ppf v =
Format
.
fprintf
ppf
"@[<hv1>"
;
Format
.
fprintf
ppf
"<value>@,%a@,</value>@]"
aux
v
(*
let rec compare_sigma x y =
if (x == y) then 0
else
match x,y with
|Comp(sx1,sx2),Comp(sy1,xy2) ->
| List(sl1), List(sl2) ->
if List.for_all2 (fun v1 v2 ->
Types.Tallying.E.comparea v1 v2 ) sl1 sl2 = 0 then 0
else (List.length sl1) - (List.length sl2)
| Sel(t1,if1,s1), Sel(t2,if2,s2) ->
| _, _ -> Pervasives.compare x y
*)
(* XXX here I don't compare sigmas !!! *)
let
rec
compare
x
y
=
if
(
x
==
y
)
then
0
...
...
@@ -831,13 +839,10 @@ let cduce2ocaml_option f v =
|
Pair
(
x
,
y
,
sigma
)
->
Some
(
f
x
)
|
_
->
None
let
ocaml2cduce_option
f
=
function
|
Some
x
->
Pair
(
f
x
,
nil
,
Mono
)
|
None
->
nil
let
add
v1
v2
=
match
(
v1
,
v2
)
with
|
(
Integer
x
,
Integer
y
)
->
Integer
(
Intervals
.
V
.
add
x
y
)
|
(
Record
(
r1
,
sigma1
)
,
Record
(
r2
,
sigma2
))
->
Record
(
Imap
.
merge
r1
r2
,
Mono
)
(* XXX *)
...
...
@@ -863,7 +868,6 @@ let modulo v1 v2 = match (v1,v2) with
|
(
Integer
x
,
Integer
y
)
->
Integer
(
Intervals
.
V
.
modulo
x
y
)
|
_
->
assert
false
let
pair
v1
v2
=
Pair
(
v1
,
v2
,
Mono
)
let
xml
v1
v2
v3
=
Xml
(
v1
,
v2
,
v3
,
Mono
)
...
...
@@ -875,7 +879,6 @@ let mk_record labels fields =
done
;
record
!
l
(* TODO: optimize cases
- (f x = [])
- all chars copied or deleted *)
...
...
@@ -887,7 +890,6 @@ let rec transform_aux f accu = function
let
transform
f
v
=
transform_aux
f
nil
v
let
rec
xtransform_aux
f
accu
=
function
|
Pair
(
x
,
y
,
sigma
)
->
let
accu
=
match
f
x
with
...
...
runtime/value.mli
View file @
d05c1abe
...
...
@@ -30,7 +30,6 @@ val comp : sigma -> sigma -> sigma
module
ValueSet
:
Set
.
S
with
type
elt
=
t
exception
CDuceExn
of
t
val
raise'
:
t
->
'
a
(* "raise" for CDuce exceptions *)
val
failwith'
:
string
->
'
a
(* "failwith" for CDuce exceptions *)
val
tagged_tuple
:
string
->
t
list
->
t
...
...
tests/lambda/src/lambdaTests.ml
View file @
d05c1abe
...
...
@@ -24,38 +24,38 @@ let run_test_compile msg expected totest =
let
tests_poly_abstr
=
[
"Test CDuce.lambda.const_abstr failed"
,
"Abstraction(Dummy,,,,Sel(,(Int -> Int),{}))"
,
"Abstraction(Dummy,,,,Sel(,
[
(Int -> Int)
]
,{}))"
,
"fun f x : Int : Int -> 2"
;
"Test CDuce.lambda.poly.identity failed"
,
"Abstraction(Dummy,,,,Sel(,([ Char* ] | Int -> [ Char* ] | Int),Comp({},{
{ `$A =
Int }
,{ `$A = [ Char* ]
}
})))"
,
"Abstraction(Dummy,,,,Sel(,
[
([ Char* ] | Int -> [ Char* ] | Int)
]
,Comp({},{{ `$A =
Int },{ `$A = [ Char* ]
}})))"
,
"(fun f x : 'A : 'A -> x) [{A/Int},{A/String}]"
;
"Test CDuce.runtime.poly.tail failed"
,
"Abstraction(Dummy,,,,Sel(,([ (`$A & Int | Char | Atom | (Any,Any) |
"Abstraction(Dummy,,,,Sel(,
[
([ (`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow)* ] -> [ (`$A & Int |
Char |
Atom |
(Any,Any) |
<(Any) (Any)>Any |
Arrow)* ]),{}))"
,
Arrow)* ])
]
,{}))"
,
"fun tail x : ['A] : ['A] -> match x : ['A] with | (el : 'A) :: (rest : ['A]) -> rest"
;
"Test CDuce.runtime.poly.pair failed"
,
"Abstraction(Dummy,,,,Sel(,((`$A & Int | Char | Atom | (Any,Any) |
"Test CDuce.runtime.poly.pair failed"
,
"Abstraction(Dummy,,,,Sel(,
[
((`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow,`$B & Int | Char |
Atom | (Any,Any) | <(Any) (Any)>Any | Arrow) ->
`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow),{}))"
,
`$A & Int | Char | Atom | (Any,Any) | <(Any) (Any)>Any | Arrow)
]
,{}))"
,
"fun pair x : ('A * 'B) : 'A -> match x : ('A * 'B) with | (z : 'A, y : 'B) -> z"
;
"Test CDuce.runtime.poly.match_abstr failed"
,
"Apply(Match(Abstraction(Dummy,,,,Sel(,(`$A & Int | Char | Atom | (Any,Any) |
"Test CDuce.runtime.poly.match_abstr failed"
,
"Apply(Match(Abstraction(Dummy,,,,Sel(,
[
(`$A & Int | Char | Atom | (Any,Any) |
<(Any) (Any)>Any | Arrow -> `$A & Int |
Char |
Atom |
(Any,Any) |
<(Any) (Any)>Any |
Arrow),{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ { `$A =
Arrow)
]
,{})), {accept_chars=false; brs_disp=<disp>; brs_rhs=[| (2, TVar(Local(0),Comp({},{ { `$A =
Int
} }))) |]; brs_stack_pos=0}),Const(3))"
,
"(match (fun f x : 'A : 'A -> x) : ('A -> 'A) with | y : ('A -> 'A) -> y[{A/Int}]).3"
;
...
...
@@ -72,9 +72,9 @@ let tests_poly_abstr = [
*)
"Test CDuce.lambda.identity_applied failed"
,
"Apply(PolyAbstraction(Dummy,Dummy,,{accept_chars=true; brs_disp=<disp>; brs_rhs=[| (1, Var(Local(0))) |]; brs_stack_pos=0},,Sel(Env(1),(
`$A -> `$A),{
{
`$A = Int
}
})),Const(2))"
,
"Apply(PolyAbstraction(Dummy,Dummy,,{accept_chars=true; brs_disp=<disp>; brs_rhs=[| (1, Var(Local(0))) |]; brs_stack_pos=0},,Sel(Env(1),
[
(
`$A -> `$A)
]
,{
{
`$A = Int
}})),Const(2))"
,
"(fun f x : 'A : 'A -> x)[{A/Int}].2"
;
];;
...
...
@@ -461,8 +461,8 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
assert_equal
~
msg
:
"Test CDuce.runtime.poly.identity failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),{
{ `$A = Int }
,{ `$A = [ Char* ]
}
}))"
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,{{ `$A = Int },{ `$A = [ Char* ]
}}))"
(
run_test_eval
"(fun f x : 'A : 'A -> x)[{A/Int},{A/String}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.identity_applied failed"
...
...
@@ -485,32 +485,32 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
| (_ : 'A) :: (rest : ['A]) -> rest).[3; 7; 8; 5]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),{
{ `$A = Int
}
}))"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,{{ `$A = Int
}}))"
(
run_test_eval
"(((fun f x : 'A : 'A -> x)[{A/Int}])[{A/String}])[{A/Bool}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.2 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Comp({
{ `$A = `$B
}
},{
{ `$B = `$A }
}),{
{ `$A = `$B
}
})))"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,Comp(Comp({{ `$A = `$B
}},{{ `$B = `$A }}),{{ `$A = `$B
}})))"
(
run_test_eval
"(((fun f x : 'A : 'A -> x)[{A/'B}])[{B/'A}])[{A/'B}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.3 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Comp(Comp({
{ `$B = `$A
}
},{
{ `$A = `$B }
}),{
{ `$B = `$A }
}),{
{ `$A = `$B
}
})))"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,Comp(Comp(Comp({{ `$B = `$A
}},{{ `$A = `$B }}),{{ `$B = `$A }}),{{ `$A = `$B
}})))"
(
run_test_eval
"((((fun f x : 'A : 'A -> x)[{A/'B}])[{B/'A}])[{A/'B}])[{B/'A}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.4 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp({
{ `$B = Int }
},{
{ `$A =
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,Comp({{ `$B = Int }},{{ `$A =
`$B
}
})))"
}})))"
(
run_test_eval
"(((((fun f x : 'A : 'A -> x)[{A/'B}])[{A/Int}])[{B/Int}])[{B/Int}])[{B/'A}]"
);
assert_equal
~
msg
:
"Test CDuce.runtime.poly.multicomp.5 failed"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Comp({
{ `$D = `$C
}
,{ `$C = `$B }
},{
{ `$B = `$C } }),{
{ `$A = `$B } ,{ `$C = `$D
}
})))"
~
printer
:
(
fun
x
->
x
)
"Abstraction((`$A,`$A),Sel(1,
[
(`$A -> `$A)
]
,Comp(Comp({{ `$D = `$C
},{ `$C = `$B }},{{ `$B = `$C } }),{{ `$A = `$B } ,{ `$C = `$D
}})))"
(
run_test_eval
"((((fun f x : 'A : 'A -> x)[{A/'B},{C/'D}])[{B/'C}])[{B/'D}])[{D/'C},{C/'B}]"
);
);
...
...
tests/lambda/src/testlib.ml
View file @
d05c1abe
...
...
@@ -43,7 +43,7 @@ module BIN = struct
end
let
print_norm
ppf
d
=
Types
.
Print
.
p
rint
ppf
((
*
Types
.
normalize
*
)
d
)
Types
.
Print
.
p
p_type
ppf
((
*
Types
.
normalize
*
)
d
)
let
print_sample
ppf
s
=
Sample
.
print
ppf
s
...
...
@@ -114,16 +114,16 @@ let rec print_exn ppf = function
Ns
.
U
.
print
ns2
|
Sequence
.
Error
(
Sequence
.
CopyTag
(
t
,
expect
))
->
Format
.
fprintf
ppf
"Tags in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
rint
expect
Types
.
Print
.
p
p_type
t
Types
.
Print
.
p
p_type
expect
Sample
.
print
(
Sample
.
get
(
Types
.
diff
t
expect
))
|
Sequence
.
Error
(
Sequence
.
CopyAttr
(
t
,
expect
))
->
Format
.
fprintf
ppf
"Attributes in %a will be copied, but only %a are allowed.@.Counter-example:%a@."
Types
.
Print
.
p
rint
t
Types
.
Print
.
p
rint
expect
Types
.
Print
.
p
p_type
t
Types
.
Print
.
p
p_type
expect
Sample
.
print
(
Sample
.
get
(
Types
.
diff
t
expect
))
|
Sequence
.
Error
(
Sequence
.
UnderTag
(
t
,
exn
))
->
Format
.
fprintf
ppf
"Under tag %a:@."
Types
.
Print
.
p
rint
t
;
Format
.
fprintf
ppf
"Under tag %a:@."
Types
.
Print
.
p
p_type
t
;
print_exn
ppf
exn
|
exn
->
...
...
@@ -151,7 +151,7 @@ let parse_cduce ?(verbose=false) s =
with
exn
->
catch_exn
Format
.
err_formatter
exn
in
if
verbose
then
Format
.
printf
"Cduce Typed %s ====>
\n
%a
\n
%!
@."
s
Typed
.
Print
.
pp_typed
texpr
;
Format
.
printf
"Cduce Typed %s ====>
\n
%a@."
s
Typed
.
Print
.
pp_typed
texpr
;
texpr
(* Typed AST -> Typed *)
...
...
@@ -159,7 +159,7 @@ let parse_texpr ?(verbose=false) s =
let
expr
=
Parse
.
ExprParser
.
of_string_no_file
s
in
let
env
,
texpr
=
Compute
.
to_typed
expr
in
if
verbose
then
Format
.
printf
"Computed Typed %s ====>
\n
%a
\n
%!
@."
s
Typed
.
Print
.
pp_typed
texpr
;
Format
.
printf
"Computed Typed %s ====>
\n
%a@."
s
Typed
.
Print
.
pp_typed
texpr
;
texpr
(* --> Lambda *)
...
...
@@ -169,7 +169,7 @@ let parse_lexpr ?(verbose=false) texpr =
with
exn
->
catch_exn
Format
.
err_formatter
exn
in
if
verbose
then
Format
.
printf
"Lambda : %s
\n
%!
@."
(
Lambda
.
Print
.
string_of_lambda
lambdaexpr
);
Format
.
printf
"Lambda : %s@."
(
Lambda
.
Print
.
string_of_lambda
lambdaexpr
);
lambdaexpr
,
lsize
(* --> Value *)
...
...
@@ -179,27 +179,27 @@ let parse_vexpr ?(verbose=false) (lambdaexpr,lsize) =
with
exn
->
catch_exn
Format
.
err_formatter
exn
in
if
verbose
then
Format
.
printf
"Value : %s
\n
%!
@."
(
Value
.
Print
.
string_of_value
evalexpr
);
Format
.
printf
"Value : %s@."
(
Value
.
Print
.
string_of_value
evalexpr
);
evalexpr
(* Cduce program -> Lambda *)
let
parse_cduce_lexpr
?
(
verbose
=
false
)
s
=
let
parse_cduce_lexpr
?
(
quite
=
false
)
?
(
verbose
=
false
)
s
=
let
texpr
=
parse_cduce
~
verbose
s
in
parse_lexpr
~
verbose
:
true
texpr
parse_lexpr
~
verbose
:
(
not
quite
)
texpr
(* Cduce program -> Value *)
let
parse_cduce_vexpr
?
(
verbose
=
false
)
s
=
let
parse_cduce_vexpr
?
(
quite
=
false
)
?
(
verbose
=
false
)
s
=
let
texpr
=
parse_cduce
~
verbose
s
in
let
lambdaexpr
,
lsize
=
parse_lexpr
~
verbose
texpr
in
parse_vexpr
~
verbose
:
true
(
lambdaexpr
,
lsize
)
parse_vexpr
~
verbose
:
(
not
quite
)
(
lambdaexpr
,
lsize
)
(* Typed AST -> Lambda *)
let
parse_texpr_lexpr
?
(
verbose
=
false
)
s
=
let
parse_texpr_lexpr
?
(
quite
=
false
)
?
(
verbose
=
false
)
s
=
let
texpr
=
parse_texpr
~
verbose
s
in
parse_lexpr
~
verbose
:
true
texpr
parse_lexpr
~
verbose
:
(
not
quite
)
texpr
(* Typed AST -> Value *)
let
parse_texpr_vexpr
?
(
verbose
=
false
)
s
=
let
parse_texpr_vexpr
?
(
quite
=
false
)
?
(
verbose
=
false
)
s
=
let
texpr
=
parse_texpr
~
verbose
s
in
let
lambdaexpr
,
lsize
=
parse_lexpr
~
verbose
texpr
in
parse_vexpr
~
verbose
:
true
(
lambdaexpr
,
lsize
)
parse_vexpr
~
verbose
:
(
not
quite
)
(
lambdaexpr
,
lsize
)
tests/lambda/src/valueTests.ml
View file @
d05c1abe
...
...
@@ -4,45 +4,39 @@ open Testlib
(* Typed -> Lambda *)
let
run_test_compile
msg
expected
totest
_
=
let
expected
,_
=
parse_texpr_lexpr
expected
in
let
totest
,_
=
parse_cduce_lexpr
totest
in
assert_equal
~
msg
:
msg
~
printer
:
(
fun
x
->
Lambda
.
Print
.
string_of_lambda
x
)
expected
totest
let
expected
,_
=
parse_texpr_lexpr
~
quite
:
true
expected
in
let
totest
,_
=
parse_cduce_lexpr
~
quite
:
true
totest
in
assert_equal
~
msg
:
msg
~
printer
:
(
fun
x
->
x
)
(
Lambda
.
Print
.
string_of_lambda
expected
)
(
Lambda
.
Print
.
string_of_lambda
totest
)
;;
let
tests_poly_abstr
=
[
"Test CDuce.lambda.const_abstr failed"
,
"fun f
x
: Int : Int
->
2"
,
"
fun f (x : Int)
: Int
= 2
"
;
"fun f
(_
: Int
)
: Int
=
2"
,
"
let x : Int = 3 in x
: Int"
;
"Test CDuce.lambda.let"
,
"let x : Int = 3 in x : Int"
,
"let x : Int = 3 in x : Int"
;
(*
"Test CDuce.lambda.identity",
"",
"(fun f x : 'A : 'A -> x)[{A/Int}].2";
"Test CDuce.lambda.appl_identity_int"
,
"let x : Int = 3 in x : Int"
,
"(fun (x : `$A) : `$A = x) 2"
;
"Test CDuce.
runtime.misc.partial
",
"",
"fun
applier x : 'A f : ('A -> 'A) : 'A -> f.x
";
"Test CDuce.
lambda.appl_identity_tag
"
,
"
let x : Int = 3 in x : Int
"
,
"
(
fun
(x : `$A) : `$A = x) `a
"
;
"Test CDuce.lambda.apply",
"",
"(fun f x : Int : Int -> x).2";
"Test CDuce.lambda.applier",
"",
"fun applier x : Int f : (Int->Int) : Int -> f.x";
"Test CDuce.runtime.misc.applier_applied failed",
"",
"((fun applier x : Int f : (Int->Int) : Int -> f.x).2).(fun g x : Int : Int -> x)";
"Test CDuce.lambda.partial"
,
"let x : Int = 3 in x : Int"
,
"fun (`$A -> (Int -> Int)) | _ -> (fun (`$B -> `$B) y -> y)"
;
"Test CDuce.lambda.applier poly",
"",
"fun applier x : 'A f : ('A -> Int) : Int -> f.x";
*)
"Test CDuce.lambda.appl_partial"
,
"let x : Int = 3 in x : Int"
,
"(fun (`$A -> (Int -> Int)) | _ -> (fun (`$B -> `$B) y -> y)) 3"
;
];;
let
tests_compile
=
"CDuce compile tests (Typed -> Lambda )"
>:::
...
...
@@ -50,9 +44,13 @@ let tests_compile = "CDuce compile tests (Typed -> Lambda )" >:::
(* Typed -> Lambda -> Value *)
let
run_test_eval
msg
expected
totest
_
=
let
expected
=
parse_texpr_vexpr
expected
in
let
totest
=
parse_cduce_vexpr
totest
in
assert_equal
~
msg
:
msg
~
printer
:
(
fun
x
->
x
)
(
Value
.
Print
.
string_of_value
expected
)
(
Value
.
Print
.
string_of_value
totest
)
let
expected
=
parse_texpr_vexpr
~
quite
:
true
expected
in
let
totest
=
parse_cduce_vexpr
~
quite
:
true
totest
in
assert_equal
~
msg
:
msg
~
printer
:
(
fun
x
->
x
)
(
Value
.
Print
.
string_of_value
expected
)
(
Value
.
Print
.
string_of_value
totest
)
let
tests_eval
=
"CDuce evaluation tests (Typed -> Lambda -> Value )"
>:::
List
.
map
(
fun
(
m
,
e
,
f
)
->
f
>::
run_test_eval
m
e
f
)
tests_poly_abstr
...
...
tests/libtest/tallyingTest.ml
View file @
d05c1abe
...
...
@@ -8,11 +8,6 @@ let parse_typ s =
Types
.
descr
nodepat
;;
let
to_string
pp
t
=
Format
.
fprintf
Format
.
str_formatter
"%a@."
pp
t
;
Format
.
flush_str_formatter
()
;;
(* the abstract field is ignored in the comparison *)
module
ESet
=
OUnitDiff
.
SetMake
(
struct
type
t
=
(
Var
.
var
*
Types
.
t
)
...
...
@@ -21,7 +16,7 @@ module ESet = OUnitDiff.SetMake (struct
if
(
v1
,
t1
)
==
(
v2
,
t2
)
then
0
else
let
c
=
Var
.
compare
v1
v2
in
if
c
<>
0
then
c
else
Types
.
compare
(
diff
t1
a
)
(
diff
t2
a
)
let
pp_printer
ppf
(
v
,
t
)
=
Format
.
fprintf
ppf
"(%a = %
s
)"
Var
.
print
v
(
to_string
Print
.
p
rint
t
)
let
pp_printer
ppf
(
v
,
t
)
=
Format
.
fprintf
ppf
"(%a = %
a
)"
Var
.
print
v
Types
.
Print
.
p
p_type
t
let
pp_print_sep
=
OUnitDiff
.
pp_comma_separator
end
)
...
...
@@ -346,8 +341,8 @@ let test_tallying =
let
s_sigma
=
Tallying
.(
s
$$
sigma
)
in
let
t_sigma
=
Tallying
.(
t
$$
sigma
)
in
assert_equal
~
pp_diff
:
(
fun
fmt
_
->
Format
.
fprintf
fmt
"s @ sigma_i = %a
\n
"
Types
.
Print
.
p
rint
s_sigma
;
Format
.
fprintf
fmt
"t @ sigma_i = %a
\n
"
Types
.
Print
.
p
rint
t_sigma
Format
.
fprintf
fmt
"s @ sigma_i = %a
\n
"
Types
.
Print
.
p
p_type
s_sigma
;
Format
.
fprintf
fmt
"t @ sigma_i = %a
\n
"
Types
.
Print
.
p
p_type
t_sigma
)
(
Types
.
subtype
s_sigma
t_sigma
)
true
)
sigma
)
l
...
...
@@ -474,13 +469,13 @@ let test_apply =
let
t2_gamma
=
sigmacup
sl
(
Types
.
arrow
(
Types
.
cons
t
)
gamma
)
in
assert_equal
~
pp_diff
:
(
fun
fmt
_
->
Format
.
fprintf
fmt
"t1 < 0 -> 1 = %a
\n
"
Types
.
Print
.
p
rint
t1
Format
.
fprintf
fmt
"t1 < 0 -> 1 = %a
\n
"
Types
.
Print
.
p
p_type
t1
)
(
Types
.
subtype
t1
(
parse_typ
"Empty -> Any"
))
true
;
assert_equal
~
pp_diff
:
(
fun
fmt
_
->
Format
.
fprintf
fmt
"sl = %a
\n
"
Types
.
Tallying
.
CS
.
pp_sl
sl
;
Format
.
fprintf
fmt
"t1 = %a
\n
"
Types
.
Print
.
p
rint
t1
;
Format
.
fprintf
fmt
"t2 -> gamma = %a
\n
"
Types
.
Print
.
p
rint
t2_gamma
;
Format
.
fprintf
fmt
"t1 = %a
\n
"
Types
.
Print
.
p
p_type
t1
;
Format
.
fprintf
fmt
"t2 -> gamma = %a
\n
"
Types
.
Print
.
p
p_type
t2_gamma
;
)
(
Types
.
subtype
t1
t2_gamma
)
true
with
Tallying
.
Step1Fail
->
assert_equal
[]
[]
)
...
...
tests/libtest/typesTest.ml
View file @
d05c1abe
...
...
@@ -7,11 +7,6 @@ let parse_typ s =
Types
.
descr
nodepat
;;
let
to_string
pp
t
=
Format
.
fprintf
Format
.
str_formatter
"%a@."
pp
t
;
Format
.
flush_str_formatter
()
;;
let
tlv_tests
=
[
"is_var"
,
[