Commit c906e750 authored by Pietro Abate's avatar Pietro Abate
Browse files

Merge branch 'typing-test' of https://git.cduce.org/cduce into typing-test

Conflicts:
	tests/typed/src/main.ml
	tests/typed/src/printer.ml
	tests/typed/src/printer.mli
parents 88a2b235 82e58431
......@@ -70,6 +70,35 @@ let run_test_typer msg expected totest =
let expected = (parse_typed expected) in
let totest = (parse_expr totest) in
assert_equal ~msg:msg ~printer:(fun x -> Printer.typed_to_string x) expected totest
(*
"match" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.match.hard failed"
~printer:(fun x -> x) (load_file "tests/match/hard.ref")
(run_test "(fun ((Int -> Int) -> Int) | f ->
(match f 0 with | 0 -> 0 | _ -> 1)) (fun (Int -> Int) | x -> x+2)");
assert_equal ~msg:"Test CDuce.runtime.match.medium failed"
~printer:(fun x -> x) (load_file "tests/match/medium.ref")
(run_test "(fun (Int -> Int) | x ->
(match x with | 1 -> 3 | x -> x)) 2");
assert_equal ~msg:"Test CDuce.runtime.match.simple failed"
~printer:(fun x -> x) (load_file "tests/match/simple.ref")
(run_test "(fun (Int -> Int) | x -> (match x with | _ -> x)) 2");
);
"list" >:: ( fun test_ctxt ->
assert_equal ~msg:"Test CDuce.runtime.list.fold failed"
~printer:(fun x -> x) (load_file "tests/list/fold.ref")
(run_test "fun (Int -> [Int*] -> [Int*])
| x -> (fun ([Int*] -> [Int*])
| y -> [x] @ y)");
assert_equal ~msg:"Test CDuce.runtime.list.is_empty failed"
~printer:(fun x -> x) (load_file "tests/list/is_empty.ref")
(run_test "fun ([Int*] -> Bool) | [] -> `true | _ -> `false");
assert_equal ~msg:"Test CDuce.runtime.list.tail failed"
~printer:(fun x -> x) (load_file "tests/list/tail.ref")
(run_test "fun ([Int*] -> [Int*]) | [_ (rest::(Int*))] -> rest | [] -> []");
);
*)
(* (message, typed expr - expected, cduce expr) *)
let tests_typer_list = [
......
......@@ -62,6 +62,7 @@ and pp_typed_aux ppf e =
Format.fprintf ppf "Match(%a,%a)" pp_typed e pp_branches b
| Typed.Subst(e, s) ->
Format.fprintf ppf "Subst(%a,[%a])" pp_typed e pp_typedsigma s
| Typed.Op(s, i, l) -> Format.fprintf ppf "(%s, %d, " s i; (print_lst pp_typed ppf l); Format.fprintf ppf ")"
| _ -> assert false
and pp_abst ppf abstr =
......
val typed_to_string : Typed.texpr -> string
val print_env : Lambda.var_loc Ident.Env.t -> unit
val print_value : Value.t -> unit
val value_to_string : Value.t -> string
val lambda_to_string : Lambda.expr -> string
{typ:Int; descr=({typ:Int -> Int; descr=Abstraction(name:<none>,
iface:[(Int, Int)],
{typ: Int; descr= ({typ: Int -> Int; descr= Abstraction(name:<none>,
iface:[(
Int, Int)],
body:[typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:176; descr:Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ:Int; descr=Var(0, x)}}}], typ:Int -> Int, fv:[])}).({typ:Int; descr=Integer(2)})}
pat:{id:3; descr:[x]; accept:[id:176; descr:
Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ: Int; descr= Var(0,x)}}}], typ:
Int -> Int, fv:[])}).({typ: Int; descr= Integer(2)})}
{typ:Int -> X1 -> X1 where X1 = [ Int* ]; descr=Abstraction(name:<none>,
iface:[(Int, X1 -> X1 where X1 = [ Int* ])],
{typ: Int -> X1 -> X1 where X1 = [ Int* ]; descr= Abstraction(name:<none>,
iface:[(
Int, X1 -> X1 where X1 = [ Int* ])],
body:[typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:178; descr:Any]; fv:[(0, x)]};
body:{typ:X1 -> X1 where X1 = [ Int* ], descr:{typ:X1 -> X1 where X1 = [ Int* ]; descr=Abstraction(name:<none>,
iface:[([ Int* ], [ Int* ])],
pat:{id:3; descr:[x]; accept:[id:178; descr:
Any]; fv:[(0, x)]};
body:{typ:X1 -> X1 where X1 = [ Int* ], descr:{typ:
X1 -> X1 where X1 = [ Int* ]; descr= Abstraction(name:<none>,
iface:[(
[ Int* ], [ Int* ])],
body:[typ:[ Int* ], accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[Any; [(0, y)]; Capture(0, y)]; accept:[id:179; descr:Any]; fv:[(0, y)]};
body:{typ:[ Int* ], descr:{typ:[ Int* ]; descr=Op(@, 0, [{typ:[ Int* ]; descr=({typ:Int; descr=Var(0, x)}, {typ:[ Int* ]; descr=Atom(nil)})}; {typ:[ Int* ]; descr=Var(0, y)}])}}}], typ:X1 -> X1 where X1 = [ Int* ], fv:[(0, x)])}}}], typ:Int -> X1 -> X1 where X1 = [ Int* ], fv:[])}
pat:{id:4; descr:[y]; accept:[id:179; descr:
Any]; fv:[(0, y)]};
body:{typ:[ Int* ], descr:{typ: [ Int* ]; descr= (@, 0, {typ:
[ Int* ]; descr= ({typ: Int; descr= Var(0,x)}, {typ: [ Int* ]; descr= Atom(nil)})} ,{typ:
[ Int* ]; descr= Var(0,y)})}}}], typ:X1 -> X1 where X1 = [ Int* ], fv:[(0, x)])}}}], typ:
Int -> X1 -> X1 where X1 = [ Int* ], fv:[])}
{typ:[ Int ] -> Bool; descr=Abstraction(name:<none>,
iface:[([ Int ], Bool)],
body:[typ:[ Int ], accept:Any, branches:
{used:false; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[[ ]; []; Constr([ ])]; accept:[id:179; descr:[ ]]; fv:[]};
body:{typ:Empty, descr:{typ:Empty; descr=Atom(true)}}},
{typ: [ Int* ] -> Bool; descr= Abstraction(name:<none>,
iface:[([ Int* ],
Bool)],
body:[typ:[ Int* ], accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[Any; []; Constr(Any)]; accept:[id:180; descr:Any]; fv:[]};
body:{typ:Bool, descr:{typ:Bool; descr=Atom(false)}}}], typ:[ Int ] -> Bool, fv:[])}
pat:{id:3; descr:[
[ ]]; accept:[id:178; descr:[ ]]; fv:[]};
body:{typ:Bool, descr:{typ:
Bool; descr= Atom(true)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[
Any]; accept:[id:179; descr:Any]; fv:[]};
body:{typ:Bool, descr:{typ:
Bool; descr= Atom(false)}}}], typ:[ Int* ] -> Bool, fv:[])}
{typ:X1 -> X1 where X1 = [ Int* ]; descr=Abstraction(name:<none>,
iface:[([ Int* ], [ Int* ])],
{typ: X1 -> X1 where X1 = [ Int* ]; descr= Abstraction(name:<none>,
iface:[(
[ Int* ], [ Int* ])],
body:[typ:[ Int* ], accept:[ (Any Int*)? ], branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[[ Any Int* ]; [(0, rest)]; Times({id:5; descr:[Any; []; Constr(Any)]; accept:[id:179; descr:Any]; fv:[]}, {id:4; descr:[[ Int* ]; [(0, rest)]; Cap([Any; [(0, rest)]; Capture(0, rest)], [[ Int* ]; []; Constr([ Int* ])])]; accept:[id:178; descr:[ Int* ]]; fv:[(0, rest)]})]; accept:[id:177; descr:[ Any Int* ]]; fv:[(0, rest)]};
body:{typ:[ Int* ], descr:{typ:[ Int* ]; descr=Var(0, rest)}}},
pat:{id:3; descr:[(
Any,(rest & [ Int* ]))]; accept:[id:177; descr:[ Any Int* ]]; fv:[(0, rest)]};
body:{typ:
[ Int* ], descr:{typ: [ Int* ]; descr= Var(0,rest)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:6; descr:[[ ]; []; Constr([ ])]; accept:[id:180; descr:[ ]]; fv:[]};
body:{typ:[ Int* ], descr:{typ:[ Int* ]; descr=Atom(nil)}}}], typ:X1 -> X1 where X1 = [ Int* ], fv:[])}
pat:{id:6; descr:[
[ ]]; accept:[id:180; descr:[ ]]; fv:[]};
body:{typ:[ Int* ], descr:{typ:
[ Int* ]; descr= Atom(nil)}}}], typ:X1 -> X1 where X1 = [ Int* ], fv:[])}
{typ: Int; descr= ({typ: (Int -> Int) -> Int; descr= Abstraction(name:<none>,
iface:[(
Int -> Int, Int)],
body:[typ:Int -> Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[f]; accept:[id:177; descr:
Any]; fv:[(0, f)]};
body:{typ:Int, descr:{typ: Int; descr= Match({typ:
Int; descr= ({typ: Int -> Int; descr= Var(0,f)}).({typ: Int; descr= Integer(0)})},typ:
Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[
0]; accept:[id:178; descr:0]; fv:[]};
body:{typ:Int, descr:{typ: Int; descr= Integer(0)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:5; descr:[
Any]; accept:[id:179; descr:Any]; fv:[]};
body:{typ:Int, descr:{typ:
Int; descr= Integer(1)}}})}}}], typ:(Int -> Int) -> Int, fv:[])}).({typ:
Int -> Int; descr= Abstraction(name:<none>,
iface:[(Int, Int)],
body:[typ:
Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:6; descr:[x]; accept:[id:180; descr:
Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ: Int; descr= (+, 0, {typ:
Int; descr= Var(0,x)} ,{typ: 2; descr= Integer(2)})}}}], typ:Int -> Int, fv:[])})}
{typ:Int; descr=({typ:Int -> Int; descr=Abstraction(name:<none>,
iface:[(Int, Int)],
{typ: Int; descr= ({typ: Int -> Int; descr= Abstraction(name:<none>,
iface:[(
Int, Int)],
body:[typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:176; descr:Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ:Int; descr=Match({typ:Int; descr=Var(0, x)},typ:Int, accept:Any, branches:
pat:{id:3; descr:[x]; accept:[id:176; descr:
Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ: Int; descr= Match({typ:
Int; descr= Var(0,x)},typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[1; []; Constr(1)]; accept:[id:177; descr:1]; fv:[]};
body:{typ:Int, descr:{typ:Int; descr=Integer(3)}}},
pat:{id:4; descr:[
1]; accept:[id:177; descr:1]; fv:[]};
body:{typ:Int, descr:{typ: Int; descr= Integer(3)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:5; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:178; descr:Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ:Int; descr=Var(0, x)}}})}}}], typ:Int -> Int, fv:[])}).({typ:Int; descr=Integer(2)})}
pat:{id:5; descr:[x]; accept:[id:178; descr:
Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ: Int; descr= Var(0,x)}}})}}}], typ:
Int -> Int, fv:[])}).({typ: Int; descr= Integer(2)})}
{typ:Int; descr=({typ:Int -> Int; descr=Abstraction(name:<none>,
iface:[(Int, Int)],
{typ: Int; descr= ({typ: Int -> Int; descr= Abstraction(name:<none>,
iface:[(
Int, Int)],
body:[typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:176; descr:Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ:Int; descr=Match({typ:Int; descr=Var(0, x)},typ:Int, accept:Any, branches:
pat:{id:3; descr:[x]; accept:[id:176; descr:
Any]; fv:[(0, x)]};
body:{typ:Int, descr:{typ: Int; descr= Match({typ:
Int; descr= Var(0,x)},typ:Int, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[Any; []; Constr(Any)]; accept:[id:177; descr:Any]; fv:[]};
body:{typ:Int, descr:{typ:Int; descr=Var(0, x)}}})}}}], typ:Int -> Int, fv:[])}).({typ:Int; descr=Integer(2)})}
pat:{id:4; descr:[
Any]; accept:[id:177; descr:Any]; fv:[]};
body:{typ:Int, descr:{typ:
Int; descr= Var(0,x)}}})}}}], typ:Int -> Int, fv:[])}).({typ: Int; descr= Integer(2)})}
{typ:(Int,Int); descr=({typ:X1 -> X1 where X1 = (Int,Int); descr=({typ:X1 -> X1 -> X1 where X1 = (Int,Int); descr=Abstraction(name:<none>,
iface:[((Int,Int), X1 -> X1 where X1 = (Int,Int))],
body:[typ:(Int,Int), accept:Pair, branches:
{typ: (Int,Int); descr= ({typ: X1 -> X1 where X1 = (Int,Int); descr= ({typ:
X1 -> X1 -> X1 where X1 = (Int,Int); descr= Abstraction(name:<none>,
iface:[(
(Int,Int), X1 -> X1 where X1 = (Int,Int))],
body:[typ:(Int,Int), accept:
Pair, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Pair; [(0, x)]; Times({id:5; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:180; descr:Any]; fv:[(0, x)]}, {id:4; descr:[Any; []; Constr(Any)]; accept:[id:179; descr:Any]; fv:[]})]; accept:[id:178; descr:Pair]; fv:[(0, x)]};
body:{typ:X1 -> X1 where X1 = (Int,Int), descr:{typ:X1 -> X1 where X1 = (Int,Int); descr=Abstraction(name:<none>,
iface:[((Int,Int), (Int,Int))],
pat:{id:3; descr:[(x,
Any)]; accept:[id:178; descr:Pair]; fv:[(0, x)]};
body:{typ:X1 -> X1 where
X1 = (Int,Int), descr:{typ:
X1 -> X1 where X1 = (Int,Int); descr= Abstraction(name:<none>,
iface:[(
(Int,Int), (Int,Int))],
body:[typ:(Int,Int), accept:Pair, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:6; descr:[Pair; [(0, y)]; Times({id:7; descr:[Any; [(0, y)]; Capture(0, y)]; accept:[id:182; descr:Any]; fv:[(0, y)]}, {id:4; descr:[Any; []; Constr(Any)]; accept:[id:179; descr:Any]; fv:[]})]; accept:[id:181; descr:Pair]; fv:[(0, y)]};
body:{typ:(Int,Int), descr:{typ:(Int,Int); descr=({typ:Int; descr=Var(0, x)}, {typ:Int; descr=Var(0, y)})}}}], typ:X1 -> X1 where X1 = (Int,Int), fv:[(0, x)])}}}], typ:X1 -> X1 -> X1 where X1 = (Int,Int), fv:[])}).({typ:(Int,Int); descr=({typ:Int; descr=Integer(2)}, {typ:Int; descr=Integer(3)})})}).({typ:(Int,Int); descr=({typ:Int; descr=Integer(1)}, {typ:Int; descr=Integer(5)})})}
pat:{id:6; descr:[(y,
Any)]; accept:[id:181; descr:Pair]; fv:[(0, y)]};
body:{typ:(Int,Int), descr:{typ:
(Int,Int); descr= ({typ: Int; descr= Var(0,x)}, {typ: Int; descr= Var(0,y)})}}}], typ:
X1 -> X1 where X1 = (Int,Int), fv:[(0, x)])}}}], typ:X1 -> X1 -> X1 where
X1 = (Int,Int), fv:[])}).({typ:
(Int,Int); descr= ({typ: Int; descr= Integer(2)}, {typ: Int; descr= Integer(3)})})}).({typ:
(Int,Int); descr= ({typ: Int; descr= Integer(1)}, {typ: Int; descr= Integer(5)})})}
{typ:([ Char* ] | Int | `true | `false) -> Bool; descr=Abstraction(name:<none>,
iface:[([ Char* ] | Int | `true | `false, Bool)],
body:[typ:[ Char* ] | Int | `true | `false, accept:Any, branches:
{typ: ([ Char* ] | Int | `true | `false) -> Bool; descr= Abstraction(name:<none>,
iface:[(
[ Char* ] | Int | `true | `false, Bool)],
body:[typ:[ Char* ] | Int | `true |
`false, accept:Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[String; []; Constr(String)]; accept:[id:177; descr:String]; fv:[]};
body:{typ:Bool, descr:{typ:Bool; descr=Atom(true)}}},
pat:{id:3; descr:[
String]; accept:[id:177; descr:String]; fv:[]};
body:{typ:Bool, descr:{typ:
Bool; descr= Atom(true)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[Any; []; Constr(Any)]; accept:[id:178; descr:Any]; fv:[]};
body:{typ:Bool, descr:{typ:Bool; descr=Atom(false)}}}], typ:([ Char* ] | Int | `true | `false) -> Bool, fv:[])}
pat:{id:4; descr:[
Any]; accept:[id:178; descr:Any]; fv:[]};
body:{typ:Bool, descr:{typ:
Bool; descr= Atom(false)}}}], typ:([ Char* ] | Int | `true | `false) -> Bool, fv:[])}
{typ:X1 -> X1 where X1 = [ Char* ] | Int; descr=Abstraction(name:<none>,
iface:[([ Char* ] | Int, [ Char* ] | Int)],
body:[typ:[ Char* ] | Int, accept:Any, branches:
{typ: X1 -> X1 where X1 = [ Char* ] | Int; descr= Abstraction(name:<none>,
iface:[(
[ Char* ] | Int, [ Char* ] | Int)],
body:[typ:[ Char* ] | Int, accept:
Any, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:3; descr:[Any; [(0, x)]; Capture(0, x)]; accept:[id:176; descr:Any]; fv:[(0, x)]};
body:{typ:[ Char* ] | Int, descr:{typ:[ Char* ] | Int; descr=Match({typ:[ Char* ] | Int; descr=Var(0, x)},typ:[ Char* ] | Int, accept:[ Char* ] | Int, branches:
pat:{id:3; descr:[x]; accept:[id:176; descr:
Any]; fv:[(0, x)]};
body:{typ:[ Char* ] | Int, descr:{typ: [ Char* ] | Int; descr= Match({typ:
[ Char* ] | Int; descr= Var(0,x)},typ:[ Char* ] | Int, accept:[ Char* ] | Int, branches:
{used:true; ghost:false; br_vars_empty:[];
pat:{id:4; descr:[Int; []; Constr(Int)]; accept:[id:177; descr:Int]; fv:[]};
body:{typ:[ Char* ] | Int, descr:{typ:[ Char* ] | Int; descr=Integer(2)}}},
pat:{id:4; descr:[
Int]; accept:[id:177; descr:Int]; fv:[]};
body:{typ:[ Char* ] | Int, descr:{typ:
[ Char* ] | Int; descr= Integer(2)}}} ,
{used:true; ghost:false; br_vars_empty:[];
pat:{id:5; descr:[String; []; Constr(String)]; accept:[id:178; descr:String]; fv:[]};
body:{typ:[ Char* ] | Int, descr:{typ:[ Char* ] | Int; descr="Piece of cake"}}})}}}], typ:X1 -> X1 where X1 = [ Char* ] | Int, fv:[])}
pat:{id:5; descr:[
String]; accept:[id:178; descr:String]; fv:[]};
body:{typ:[ Char* ] | Int, descr:{typ:
[ Char* ] | Int; descr= "Piece of cake"}}})}}}], typ:X1 -> X1 where
X1 = [ Char* ] | Int, fv:[])}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment