API change. Tallying.tallying now returns a list of maps

compile/operators.ml

@@ -46,7 +46,7 @@ let register_cst op t v =
 let register_fun op dom codom eval =
   register_cst op
     (Types.arrow (Types.cons dom) (Types.cons codom))
-    (Value.Abstraction (Some [(dom,codom)],eval, `List([[]])))
+    (Value.Abstraction (Some [(dom,codom)],eval, `List([])))
 
 let register_fun2 op dom1 dom2 codom eval =
   let t2 = Types.arrow (Types.cons dom2) (Types.cons codom) in
@@ -55,7 +55,7 @@ let register_fun2 op dom1 dom2 codom eval =
     (Types.arrow (Types.cons dom1) (Types.cons t2))
     (Value.Abstraction (Some [(dom1,t2)],(fun v1 ->
 					    Value.Abstraction (iface2,
-							       eval v1, `List([[]]))), `List([[]])))
+							       eval v1, `List([]))), `List([])))
 let register_op op ?(expect=Types.any) typ eval =
   register_unary op 
     (fun tf _ _ -> let t = tf expect true in typ t)

runtime/load_xml.ml

@@ -48,9 +48,9 @@ let attrib att =
 
 let elem ns tag att child =
   if !keep_ns then
-    XmlNs (Atom tag, Record (attrib att, `List([[]])), child, ns, `List([[]]))
+    XmlNs (Atom tag, Record (attrib att, `List([])), child, ns, `List([]))
   else
-    Xml (Atom tag, Record (attrib att, `List([[]])), child, `List([[]]))
+    Xml (Atom tag, Record (attrib att, `List([])), child, `List([]))
 
 type stack = 
   | Element of Value.t * stack
@@ -64,7 +64,7 @@ let ns_table = ref Ns.empty_table
 
 let rec create_elt accu = function
   | String (s,st) -> create_elt (string s accu) st
-  | Element (x,st) -> create_elt (Pair (x,accu, `List([[]]))) st
+  | Element (x,st) -> create_elt (Pair (x,accu, `List([]))) st
   | Start (ns,name,att,old_table,st) -> 
       stack := Element (elem ns name att accu, st);
       ns_table := old_table
@@ -132,7 +132,7 @@ let load_html s =
     | Nethtml.Element (tag, att, child) -> 
 	let att = List.map (fun (n,v) -> (Label.mk (Ns.empty, U.mk n), U.mk v)) att in
 	Pair (elem Ns.empty_table (Atoms.V.mk (Ns.empty,U.mk tag) )
-		att (val_of_docs child), q, `List([[]]))
+		att (val_of_docs child), q, `List([]))
   and val_of_docs = function
     | [] -> nil
     | h::t -> val_of_doc (val_of_docs t) h

runtime/print_xml.ml

@@ -59,7 +59,7 @@ module H = Hashtbl.Make(Ns.Uri)
 
 let exn_print_xml = CDuceExn (Pair (
 				Atom (Atoms.V.mk_ascii "Invalid_argument"),
-				string_latin1 "print_xml", `List([[]])))
+				string_latin1 "print_xml", `List([])))
 
 let blank = U.mk " "
 let true_literal = U.mk "true"

types/builtin.ml

@@ -85,42 +85,42 @@ let exn_load_file_utf8 = lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "load_file_utf8"),
-      Value.string_latin1 "File is not a valid UTF-8 stream", `List([[]])))
+      Value.string_latin1 "File is not a valid UTF-8 stream", `List([])))
 )
 
 let exn_int_of =  lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
-      Value.string_latin1 "int_of", `List([[]])))
+      Value.string_latin1 "int_of", `List([])))
 )
 
 let exn_char_of = lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
-      Value.string_latin1 "char_of", `List([[]])))
+      Value.string_latin1 "char_of", `List([])))
 )
 
 let exn_float_of = lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
-      Value.string_latin1 "float_of", `List([[]])))
+      Value.string_latin1 "float_of", `List([])))
 )
 
 let exn_namespaces = lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
-      Value.string_latin1 "namespaces", `List([[]])))
+      Value.string_latin1 "namespaces", `List([])))
 )
 
 let exn_cdata_of = lazy (
   Value.CDuceExn (
     Value.Pair (
       Value.Atom (Atoms.V.mk_ascii "Invalid_argument"),
-      Value.string_latin1 "cdata_of", `List([[]])))
+      Value.string_latin1 "cdata_of", `List([])))
 )
 
 let eval_load_file ~utf8 e =
@@ -301,7 +301,7 @@ register_fun "split_atom"
 	 let (ns,l) = Atoms.V.value q in
 	 Value.Pair(
 	   Value.string_utf8 (Ns.Uri.value ns),
-	   Value.string_utf8 l, `List([[]]))
+	   Value.string_utf8 l, `List([]))
      | _ -> assert false);;
 
 register_fun "make_atom"

types/types.ml

@@ -2842,9 +2842,8 @@ module Tallying = struct
 
     type s = S.t
     type m = M.t
-    type e = Descr.s E.t
     type es = ES.t
-    type sigma = (Var.var * t) list
+    type sigma = Descr.s E.t
     type sl = sigma list
 
     let singleton = function
@@ -2854,10 +2853,7 @@ module Tallying = struct
     let pp_s = S.print
     let pp_m = M.print
     let pp_e = E.print
-    let pp_sl ppf ll =
-      print_lst (fun ppf l ->
-        (print_lst (fun ppf (v,t) -> Format.fprintf ppf "(%a/%a)" Var.print v Print.print t) ppf l)
-      ) ppf ll
+    let pp_sl ppf ll = print_lst E.print ppf ll
 
     let sat = S.singleton M.empty
     let unsat = S.empty
@@ -3150,28 +3146,24 @@ module Tallying = struct
   let tallying l =
     let n = List.fold_left (fun acc (s,t) ->
       let d = diff s t in
-      if is_empty d then CS.sat else
-        if no_var d then CS.unsat else
-          CS.prod acc (norm d)) CS.sat l
+      if is_empty d then CS.sat 
+      else if no_var d then CS.unsat
+      else CS.prod acc (norm d)) CS.sat l
     in
-(*    Format.printf "Norm : %a\n" CS.pp_s n;*)
     if Pervasives.(n = CS.unsat) then raise Step1Fail else
     let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
-(*    Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
     if CS.ES.is_empty m then raise Step2Fail else
     let el = CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc) m CS.ES.empty in
-(*    Format.printf "Unify : %a\n" CS.ES.print el;*)
-    List.map (CS.E.bindings) (CS.ES.elements el)
+    (* List.map (CS.E.bindings) *) (CS.ES.elements el)
 
   let apply_subst t subl =
-    List.fold_left (fun acc s ->
-      Positive.substitute acc s) t subl
+    CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) subl t
 
   let domain ll =
-    List.fold_left (fun acc l ->
-      List.fold_left (fun acc (v,_) ->
+    List.fold_left (fun acc e ->
+      CS.E.fold (fun v _ acc ->
         Var.Set.add v acc
-      ) acc l
+      ) e acc
     ) Var.Set.empty ll
 
 end
@@ -3188,8 +3180,8 @@ let apply_raw s t =
   let rec aux (i,acc1) (j,acc2) t1 t2 () =
     let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
     try
-      (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]),
-      (acc1, acc2)
+      let sl = Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))] in
+      (sl,(acc1, acc2))
     with
     |Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
     |Tallying.Step2Fail -> begin
@@ -3214,28 +3206,39 @@ let apply_raw s t =
   !result
 
 let apply_full s t =
-  let subst_lst,(s,t) = apply_raw s t in
+  let (subst_lst,(s,t)) = apply_raw s t in
+  let gamma = Var.mk "Gamma" in
+  let ss,tt,res = 
+    List.fold_left (fun (ssacc,ttacc,resacc) e ->
+      let ss = Tallying.CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) e s in
+      let tt = Tallying.CS.E.fold (fun var subst acc -> Positive.substitute acc (var,subst)) e t in
+      let res = Tallying.CS.E.find gamma e in
+      (cap ssacc (Positive.clean_type ss),
+       cap ttacc (Positive.clean_type tt),
+       cap resacc (Positive.clean_type res)
+      )
+    ) (any,any,any) subst_lst
+  in
+(*
   let ss =
-    List.fold_left (fun tacc constr_lst ->
-      cap tacc (List.fold_left (fun tacc subst ->
-        Positive.substitute tacc subst) s constr_lst)) any subst_lst
+    List.fold_left (fun tacc e ->
+      cap tacc (List.fold_left (fun tacc subst -> 
+        Positive.substitute tacc subst) s (Tallying.CS.E.bindings e))) any subst_lst
   in
   let tt =
-    List.fold_left (fun tacc constr_lst ->
+    List.fold_left (fun tacc e ->
       cap tacc (List.fold_left (fun tacc subst ->
-        Positive.substitute tacc subst) t constr_lst)) any subst_lst
+        Positive.substitute tacc subst) t (Tallying.CS.E.bindings e))) any subst_lst
   in
-  (*let arr = Arrow.get ss in
-  let res = Arrow.apply arr (tt) in *)
   let ss = Positive.clean_type ss in
   let tt = Positive.clean_type tt in
-  (*let res = Positive.clean_type res in *)
-  let res2 = List.fold_left
+  let res2 = List.fold_left (fun acc e -> cap acc (Tallying.CS.E.find gamma e)) any subst_lst in
     (fun acc l -> cap acc (snd (List.find (fun (`Var v, _) -> 0 == String.compare v.Var.id "Gamma") l))) any subst_lst
   in
   let res2 = Positive.clean_type res2 in
+    *)
   Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n%!"
-  Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res2; res2
+  Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res
 
 
 let apply s t = fst (apply_raw s t)

types/types.mli

@@ -398,14 +398,13 @@ module Tallying : sig
 
     type s = S.t
     type m =  M.t
-    type e = t E.t
     type es = ES.t
-    type sigma = (Var.var * t) list
+    type sigma = t E.t
     type sl = sigma list
 
     val pp_s  : Format.formatter -> s -> unit
     val pp_m  : Format.formatter -> m -> unit
-    val pp_e  : Format.formatter -> e -> unit
+    val pp_e  : Format.formatter -> sigma -> unit
     val pp_sl : Format.formatter -> sl -> unit
 
     val merge : m -> m -> m
@@ -419,7 +418,7 @@ module Tallying : sig
   val norm : t -> CS.s
   val merge : CS.m -> CS.s
   val solve : CS.s -> CS.es
-  val unify : CS.e -> CS.e
+  val unify : CS.sigma -> CS.sigma
   val tallying : (t * t) list -> CS.sl
   val apply_subst : t -> CS.sigma -> t
   val domain : CS.sl -> Var.Set.t
@@ -428,4 +427,4 @@ end
 
 val apply : t -> t -> Tallying.CS.sl
 val apply_full : t -> t -> t
-val apply_raw : t -> t -> Tallying.CS.sl * (t*t)
+val apply_raw : t -> t -> (Tallying.CS.sl * (t * t))