Replace Sel(_,_,Id) with Id; eval_sigma now returns empty on Mono

[TESTS][LAMBDA] Update tests; improve lambda printer

compile/compile.ml

@@ -74,6 +74,11 @@ let fresharg =
     (0,U.mk s)
 ;;
 
+(*
+  Comp for Lambda.sigma but simplify if possible.
+  TODO: - Merge with the comp function in value.ml
+        - Check the domains of sigmas before optimizing
+*)
 let rec comp s1 s2 = match s1, s2 with
   | Identity, _ -> s2
   | _, Identity -> s1
@@ -223,7 +228,9 @@ and compile_abstr env a =
   if is_mono then
     Abstraction(slots, a.Typed.fun_iface, body, !(env.max_stack))
   else
-    let sigma = Sel(Env 1,a.Typed.fun_iface,lift(env.sigma)) in
+    let sigma = match env.sigma with
+      | Identity -> Identity
+      | _ -> Sel(Env 1,a.Typed.fun_iface,lift(env.sigma)) in
     PolyAbstraction(slots, a.Typed.fun_iface, body, !(env.max_stack), sigma)
 
 and compile_branches env (brs : Typed.branches) =

runtime/run_dispatch.ml

@@ -193,7 +193,7 @@ let (@@) v sigma =
 
 let rec eval_sigma env = 
   let open Value in function
-    |Mono -> assert false
+    |Mono -> []
     |Identity -> []
     |List l -> l
     |Comp(s1,s2) -> (eval_sigma env s1) @ (eval_sigma env s2)

runtime/value.ml

@@ -24,6 +24,11 @@ and t =
   | Concat of t * t
   | Absent
 
+(*
+  Comp for Value.sigma but simplify if possible.
+  TODO: - Merge with the comp function in compile.ml
+        - Check the domains of sigmas before optimizing
+*)
 let rec comp s1 s2 = match s1, s2 with
   | Identity, _ -> s2
   | _, Identity -> s1

tests/lambda/src/lambdaTests.ml

@@ -72,8 +72,8 @@ let tests_poly_abstr = [
   *)
 
   "Test CDuce.lambda.identity_applied failed",
-  "Apply(PolyAbstraction(Dummy,Dummy,,,,Sel(Env(1),(`$A -> `$A),{ { `$A = 
-Int
+  "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";
 ];;
@@ -214,16 +214,14 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
                            | x : (!(Int|Bool)) -> x).[2; 3]");
       assert_equal ~msg:"Test CDuce.runtime.misc.map failed"
 	~printer:(fun x -> x)
-    "Abstraction((`$A -> `$B,[ `$A* ] -> [ `$B* ]),Sel(1,(`$A -> `$B -> [ `$A* ] -> 
-                                                                   [ 
-                                                                   `$B* ]),Id))"
+    "Abstraction((`$A -> `$B,[ `$A* ] -> [ `$B* ]),Id)"
 	(run_test_eval "fun map f : ('A -> 'B) x : ['A] : ['B] ->
                           match x : ['A] with
                             | (el : 'A) :: [] -> f.el
                             | (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))");
       assert_equal ~msg:"Test CDuce.runtime.misc.map_even failed"
 	~printer:(fun x -> x)
-	"Abstraction(([ `$A* ],[ `$B* ]),Sel(1,([ `$A* ] -> [ `$B* ]),Id))"
+	"Abstraction(([ `$A* ],[ `$B* ]),Id)"
 	(run_test_eval "(fun map f : ('A->'B) x : ['A] : ['B] ->
                           match x : ['A] with
                             | (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))
@@ -257,7 +255,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
       assert_equal ~msg:"Test CDuce.runtime.misc.map_even_hard failed"
 	~printer:(fun x -> x)
 	"(Atom(true),(\"hey\",((3,(5,Atom(nil),Mono),Mono),(Atom(true),(Abstraction((
-`$C,`$C),Sel(1,(`$C -> `$C),Id)),(Atom(false),Atom(nil),Mono),Mono),Mono),Mono),Mono),Mono)"
+`$C,`$C),Mono),(Atom(false),Atom(nil),Mono),Mono),Mono),Mono),Mono),Mono)"
 	(run_test_eval "(fun map f : ('A->'B) x : ['A] : ['B] ->
                           match x : ['A] with
                             | (el : 'A) :: (rest : ['A]) -> ((f.el), ((map.f).rest))
@@ -456,7 +454,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
     "poly" >:: ( fun test_ctxt ->
       assert_equal ~msg:"Test CDuce.runtime.poly.identity_pure failed"
 	~printer:(fun x -> x)
-	"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Id))"
+	"Abstraction((`$A,`$A),Id)"
 	(run_test_eval "fun f x : 'A : 'A -> x");
 
       assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
@@ -475,7 +473,7 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
 
       assert_equal ~msg:"Test CDuce.runtime.poly.tail failed"
 	~printer:(fun x -> x)
-      "Abstraction(([ `$A* ],[ `$A* ]),Sel(1,([ `$A* ] -> [ `$A* ]),Id))"
+      "Abstraction(([ `$A* ],[ `$A* ]),Id)"
 	(run_test_eval "fun tail x : ['A] : ['A] -> match x : ['A] with
                      | (_ : 'A) :: (rest : ['A]) -> rest");
 

tests/lambda/src/printer.ml

@@ -238,9 +238,9 @@ and pp_lambda ppf =
   | TVar (v,sigma) -> Format.fprintf ppf "TVar(%a,%a)" pp_vloc v pp_lambda_sigma sigma
   | Apply (e1,e2) -> Format.fprintf ppf "Apply(%a,%a)" pp_lambda e1 pp_lambda e2
   | PolyAbstraction (va, l, b, i, sigma) ->
-      Format.fprintf ppf "PolyAbstraction(%a,,,,%a)" pp_vloc_array va pp_lambda_sigma sigma
+      Format.fprintf ppf "PolyAbstraction(%a,,%a,,%a)" pp_vloc_array va pp_lbranches b pp_lambda_sigma sigma
   | Abstraction (va, l, b, i) ->
-      Format.fprintf ppf "Abstraction(%a,,,,)" pp_vloc_array va
+      Format.fprintf ppf "Abstraction(%a,,%a,,)" pp_vloc_array va pp_lbranches b
   | Check(_) -> Format.fprintf ppf "Check"
   | Const(v) -> Format.fprintf ppf "Const(%a)" pp_value v
   | Pair(e1, e2) -> Format.fprintf ppf "Pair(%a, %a)" pp_lambda e1 pp_lambda e2