better comp functions

compile/compile.ml

@@ -72,12 +72,28 @@ let fresharg =
     (0,U.mk s)
 ;;
 
-let comp s1 s2 = match s1, s2 with
+let rec comp s1 s2 = match s1, s2 with
   | Identity, _ -> s2
   | _, Identity -> s1
+  (* 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 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
+      | Comp(_) as s5 when s3 != s5 -> (match comp s4 s2 with
+	  | Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
+	  | _ -> s1)
+      | _ -> s1)
+  (* Same case as above, but s1 is a List and s2 a Comp *)
+  | List(_), Comp(s3, s4) -> (match comp s3 s1 with
+      | Comp(_) as s5 when s3 != s5 -> (match comp s4 s1 with
+	  | Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
+	  | _ -> s2)
+      | _ -> s2)
+  (* Default: comp s1 s2 -> Comp(s1, s2). *)
+  (* To do? Do something else if s1 = Comp and s2 = Comp or if Sel *)
   | _, _ -> Comp(s1, s2)
 
 (* from intermediate explicitely typed language to Evaluation language (lambda) *)

runtime/value.ml

@@ -23,12 +23,28 @@ and t =
   | Concat of t * t
   | Absent
 
-let comp s1 s2 = match s1, s2 with
+let rec comp s1 s2 = match s1, s2 with
   | Identity, _ -> s2
   | _, Identity -> s1
+  (* 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 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
+      | Comp(_) as s5 when s3 != s5 -> (match comp s4 s2 with
+	  | Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
+	  | _ -> s1)
+      | _ -> s1)
+  (* Same case as above, but s1 is a List and s2 a Comp *)
+  | List(_), Comp(s3, s4) -> (match comp s3 s1 with
+      | Comp(_) as s5 when s3 != s5 -> (match comp s4 s1 with
+	  | Comp(_) as s5 when s3 != s5 -> Comp(s1, s2)
+	  | _ -> s2)
+      | _ -> s2)
+  (* Default: comp s1 s2 -> Comp(s1, s2). *)
+  (* To do? Do something else if s1 = Comp and s2 = Comp or if Sel *)
   | _, _ -> Comp(s1, s2)
 
 (*