Use comp functions to simplify sigmas instead of direct calls to constructors

compile/compile.ml

@@ -72,6 +72,14 @@ let fresharg =
     (0,U.mk s)
 ;;
 
+let comp s1 s2 = match s1, s2 with
+  | Identity, _ -> s2
+  | _, Identity -> s1
+  | List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
+      | None -> Comp(s1, s2)
+      | Some l -> List(l))
+  | _, _ -> Comp(s1, s2)
+
 (* from intermediate explicitely typed language to Evaluation language (lambda) *)
 (* Typed -> Lambda *)
 let rec compile env e = compile_aux env e.Typed.exp_descr
@@ -90,7 +98,7 @@ and compile_aux env = function
       in
       if Var.Set.is_empty polyvars then Var (v)
       else TVar(v,env.sigma)
-  | Typed.Subst(e,sl) -> compile { env with sigma = Comp(env.sigma,List sl) } e
+  | Typed.Subst(e,sl) -> compile { env with sigma = comp env.sigma (List sl) } e
   | Typed.ExtVar (cu,x,_) -> Var (find_ext cu x)
   | Typed.Apply (e1,e2) -> Apply (compile env e1, compile env e2)
   | Typed.Abstraction a -> compile_abstr env a

runtime/eval.ml

@@ -64,11 +64,11 @@ let tag_op_resolved = Obj.tag (Obj.repr (OpResolved ((fun _ -> assert false), []
 let tag_const = Obj.tag (Obj.repr (Const (Obj.magic 0)))
 
 let apply_sigma sigma = function
-  |Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,Value.Comp(sigma,sigma'))
-  |Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,Value.Comp(sigma,sigma'))
-  |Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.Comp(sigma,sigma'))
-  |Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.Comp(sigma,sigma'))
-  |Value.Record(m,sigma') -> Value.Record(m,Value.Comp(sigma,sigma'))
+  |Value.Pair(v1,v2,sigma') -> Value.Pair(v1,v2,Value.comp sigma sigma')
+  |Value.Abstraction(iface,f,sigma') -> Value.Abstraction(iface,f,Value.comp sigma sigma')
+  |Value.Xml(v1,v2,v3,sigma') -> Value.Xml(v1,v2,v3,Value.comp sigma sigma')
+  |Value.XmlNs(v1,v2,v3,ns,sigma') -> Value.XmlNs(v1,v2,v3,ns,Value.comp sigma sigma')
+  |Value.Record(m,sigma') -> Value.Record(m,Value.comp sigma sigma')
   |v -> v
 ;;
 

runtime/run_dispatch.ml

@@ -183,16 +183,12 @@ let rec run_disp_basic v f =  function
 let (@@) v sigma =
   let open Value in
   if sigma = Identity then v else
-    let comp = function
-      |Identity,s | s,Identity -> s
-      |s1,s2 -> Comp(s1,s2)
-    in 
     match v with
-    |Pair (v1,v2,s) -> Pair (v1,v2,comp(sigma,s))
-    |Xml (v1,v2,v3,s) -> Xml (v1,v2,v3,comp(sigma,s))
-    |XmlNs (v1,v2,v3,a,s) -> XmlNs (v1,v2,v3,a,comp(sigma,s))
-    |Record (r,s) -> Record (r,comp(sigma,s))
-    |Abstraction (iface,t,s) -> Abstraction (iface,t,comp(sigma,s))
+    |Pair (v1,v2,s) -> Pair (v1,v2,comp sigma s)
+    |Xml (v1,v2,v3,s) -> Xml (v1,v2,v3,comp sigma s)
+    |XmlNs (v1,v2,v3,a,s) -> XmlNs (v1,v2,v3,a,comp sigma s)
+    |Record (r,s) -> Record (r,comp sigma s)
+    |Abstraction (iface,t,s) -> Abstraction (iface,t,comp sigma s)
     |_ -> v
 
 let rec eval_sigma env = 

runtime/value.ml

@@ -23,6 +23,14 @@ and t =
   | Concat of t * t
   | Absent
 
+let comp s1 s2 = match s1, s2 with
+  | Identity, _ -> s2
+  | _, Identity -> s1
+  | List(l1), List(l2) -> (match Types.Tallying.subsigma l1 l2 with
+      | None -> Comp(s1, s2)
+      | Some l -> List(l))
+  | _, _ -> Comp(s1, s2)
+
 (* 
   The only representation of the empty sequence is nil.
   In particular, in String_latin1 and String_utf8, the string cannot be empty.

runtime/value.mli

@@ -24,6 +24,8 @@ and t =
   | Concat of t * t
   | Absent
 
+val comp : sigma -> sigma -> sigma
+
 module ValueSet: Set.S with type elt = t
 
 exception CDuceExn of t

tests/lambda/src/lambdaTests.ml

@@ -72,9 +72,8 @@ let tests_poly_abstr = [
   *)
 
   "Test CDuce.lambda.identity_applied failed",
-  "Apply(Abstraction(Dummy,Dummy,,,,Sel(Env(1),(`$A -> `$A),Comp(Id,{ { `$A = 
-Int
- } })),Env(1)),Const(2))",
+  "Apply(Abstraction(Dummy,Dummy,,,,Sel(Env(1),(`$A -> `$A),{ { `$A = Int
+ } }),Env(1)),Const(2))",
   "(fun f x : 'A : 'A -> x)[{A/Int}].2";
 ];;
 
@@ -236,7 +235,9 @@ Int -> Bool),(Bool -> Bool),(Any \\ (Int | Bool) -> Any \\ (Int | Bool)),Id))"
                           | x : (!Int) -> x).[4; \"hey\"; 3; 2]");
       assert_equal ~msg:"Test CDuce.runtime.misc.map_even_hard failed"
 	~printer:(fun x -> x)
-	"(Atom(true),(\"hey\",((3,(5,Atom(nil),Id),Id),(Atom(true),(Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Id)),(Atom(false),Atom(nil),Id),Id),Id),Id),Id),Id)"
+	"(Atom(true),(\"hey\",((3,(5,Atom(nil),Id),{ { `$A = Int } ,{ `$A = Bool
+ } }),(Atom(true),(Abstraction((`$C,`$C),Comp({ { `$A = Int } ,{ `$A = 
+Bool } },Sel(1,(`$C -> `$C),Id))),(Atom(false),Atom(nil),Id),Id),Id),Id),Id),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))
@@ -444,9 +445,8 @@ X1 -> X1 where X1 = (Int,Int)),Id))"
 	(run_test_eval "fun f x : 'A : 'A -> x");
       assert_equal ~msg:"Test CDuce.runtime.poly.identity failed"
 	~printer:(fun x -> x)
-	"Abstraction((`$A,`$A),Sel(1,(`$A -> `$A),Comp(Id,{ { `$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"
 	~printer:(fun x -> x) "2"

types/types.ml

@@ -3238,6 +3238,17 @@ 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
+
 end
 
 exception Found of t * int * int * Tallying.CS.sl

types/types.mli

@@ -422,6 +422,7 @@ module Tallying : sig
   val tallying : (t * t) list -> CS.sl
   val (@@) : t -> CS.sigma -> t
   val domain : CS.sl -> Var.Set.t
+  val subsigma : CS.sl -> CS.sl -> CS.sl option
 
 end