Fix comp function

[TESTS][LAMBDA] add tests for comp of sigmas

compile/compile.ml

@@ -80,19 +80,18 @@ 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
-*)
+(* Comp for Lambda.sigma but simplify if possible. *)
 let rec comp s1 s2 = match s1, s2 with
   | Identity, _ -> s2
   | _, Identity -> s1
-  | _, _  when Var.Set.inter (domain s1) (codomain s2) != Var.Set.empty -> Comp(s1, s2)
-  (* If l1 subsigma of l2 or l2 subsigma of l1 then we keep the biggest *)
-  | List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
-      | None -> Comp(s1, s2)
-      | Some l -> List(l))
+
+  (* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
+  | _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
+      -> Comp(s1, s2)
+
+  | List(l1), List(l2) ->
+    if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
+
   (* If s1 is a Comp(s3, s4) and s2 a List(l), then if l has a subsigma in s3
      or in s4 we return s1, else we return Comp(s1, s2) *)
   | Comp(s3, s4), List(_) -> (match comp s3 s2 with

runtime/value.ml

@@ -36,21 +36,20 @@ let rec codomain = function
   | Comp(s1,s2) -> Var.Set.union (codomain s1) (codomain s2)
   | Sel(_,_,sigma) -> (codomain sigma)
 
-(*
-  Comp for Value.sigma but simplify if possible.
-  TODO: - Merge with the comp function in compile.ml
-        - Check the domains of sigmas before optimizing
-*)
+(* 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
-  | _, _  when Var.Set.inter (domain s1) (codomain s2) != Var.Set.empty -> Comp(s1, s2)
-  (* If l1 subsigma of l2 or l2 subsigma of l1 then we keep the biggest *)
-  | List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
-      | None -> Comp(s1, s2)
-      | Some l -> List(l))
+
+  (* If a variable in the image of s2 is in the domain of s1 we can't simplify *)
+  | _, _ when not (Var.Set.is_empty (Var.Set.inter (domain s1) (codomain s2)))
+      -> Comp(s1, s2)
+
+  | List(l1), List(l2) ->
+    if Var.Set.subset (domain s1) (domain s2) then s2 else Comp(s1, s2)
+
   (* If s1 is a Comp(s3, s4) and s2 a List(l), then if l has a subsigma in s3
      or in s4 we return s1, else we return Comp(s1, s2) *)
   | Comp(s3, s4), List(_) -> (match comp s3 s2 with

tests/lambda/src/lambdaTests.ml

@@ -486,10 +486,9 @@ 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),Comp({ { `$A = Int
- } },{ { `$A = [ Char* ]
- } })))"
-	(run_test_eval "(((fun f x : 'A : 'A -> x)[{A/Int}])[{A/String}])[{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
@@ -497,6 +496,18 @@ let tests_eval = "CDuce runtime tests (Typed -> Lambda -> Value)" >:::
  } })))"
 	(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
+ } })))"
+	(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(Comp({ { `$B = Int
+ } },{ { `$A = Int } }),{ { `$A = `$B
+ } })))"
+	(run_test_eval "(((((fun f x : 'A : 'A -> x)[{A/'B}])[{A/Int}])[{B/Int}])[{B/Int}])[{B/'A}]");
+
     );
 
   ]

types/types.ml

@@ -3245,17 +3245,6 @@ module Tallying = struct
       ) e acc
     ) Var.Set.empty ll
 
-  (* Returns Some l2 if l1 is a subsigma of l2, Some l1 if l2 is a subsigma of
-     l1, None otherwise. *)
-  let subsigma l1 l2 =
-    let rec aux l = function
-      | [] -> Some l
-      | x :: rest ->
-	(try ignore(List.find (fun y -> CS.E.compare Descr.compare x y = 0) l); aux l rest
-	 with Not_found -> None)
-    in
-    if List.length l1 > List.length l2 then aux l1 l2 else aux l2 l1
-
   let is_identity = List.for_all (CS.E.is_empty)
 
 end

types/types.mli

@@ -423,7 +423,6 @@ module Tallying : sig
   val (@@) : t -> CS.sigma -> t
   val domain : CS.sl -> Var.Set.t
   val codomain : CS.sl -> Var.Set.t
-  val subsigma : CS.sl -> CS.sl -> CS.sl option
   val is_identity : CS.sl -> bool
 
 end