Fix variable ordering problem by adding a 'kind' field inside variables so...

Fix variable ordering problem by adding a 'kind' field inside variables so that variables of the function type are processed before arguments types and after Gamma.

types/types.ml

@@ -1724,7 +1724,7 @@ module Print = struct
 
   let memo = DescrHash.create 63
   let counter = ref 0
-  let alloc def = { 
+  let alloc def = {
     id = (incr counter; !counter);
     def = def;
     state = `None;
@@ -1957,7 +1957,7 @@ module Print = struct
                   let res =
                     match Atoms.sample bdd with
                     |None -> false
-                    | _ -> true 
+                    | _ -> true
                   in res
               | _ -> false
               with Not_found -> true
@@ -1967,9 +1967,9 @@ module Print = struct
               if subtype tt_times seqs_descr then
                 let seq = cap tt seqs_descr in
                 let seq_times = { empty with times = seq.times } in
-                if is_empty seq || (is_empty seq_times && not finite_atoms) then 
+                if is_empty seq || (is_empty seq_times && not finite_atoms) then
                   [], tt
-                else 
+                else
                   let tt =
                     let d = diff tt seqs_descr in
                     if finite_atoms then d
@@ -2201,7 +2201,7 @@ module Print = struct
     | { state = `Named n } -> n
     | _ -> assert false
 
-  
+
   let rec do_print_slot (pri : Level.t) ppf s =
     match s.state with
       | `Named n -> U.print ppf n
@@ -2314,10 +2314,10 @@ module Print = struct
 	(List.rev (c :: accu), None)
     | r -> (List.rev accu,Some r)
 
-  and print_gname ppf = function 
+  and print_gname ppf = function
     |(cu,n,[||]) -> Format.fprintf ppf "%s%a" cu Ns.QName.print n
     |(cu,n,al) ->
-        Format.fprintf ppf "%s%a(%s)" cu Ns.QName.print n 
+        Format.fprintf ppf "%s%a(%s)" cu Ns.QName.print n
         (String.concat "," (List.map (Utils.string_of_formatter pp_type) (Array.to_list al)))
 
   and pp_type ppf t =
@@ -2814,7 +2814,7 @@ module Positive = struct
     else begin
       let subst l d =
         try ty(snd(List.find (fun (alpha,_) -> Var.equal d alpha) l))
-        with Not_found -> var d 
+        with Not_found -> var d
       in
       let new_t = (substitute_aux Var.Set.empty (decompose t) (subst l)) in
       descr (solve new_t)
@@ -2826,7 +2826,7 @@ module Positive = struct
     let subst h d =
       try Hashtbl.find h d
       with Not_found -> begin
-        let x = var (Var.fresh d) in 
+        let x = var (Var.fresh d) in
         Hashtbl.add h d x ;
         x
       end
@@ -2835,6 +2835,13 @@ module Positive = struct
     let new_t = substitute_aux delta dec (subst h) in
     descr (solve new_t)
 
+  let substitute_kind delta kind t =
+    if no_var t then t else
+      let subst kin d = var (Var.set_kind kind d) in
+      let dec = decompose t in
+      let new_t = substitute_aux delta dec (subst kind) in
+      descr (solve new_t)
+
   (* We cannot use the variance annotation of variables to simplify them,
      since variables are shared amongst types. If we have two types
      A -> A and (A,A) (produced by the algorithm) then we can still simplify the
@@ -2930,8 +2937,8 @@ module Tallying = struct
      * equivalent *)
     let semantic_compare t1 t2 =
       let c = Descr.compare t1 t2 in
-      if c = 0 then 0 else 
-      if equiv t1 t2 then 0 
+      if c = 0 then 0 else
+      if equiv t1 t2 then 0
       else c
 
     (* constraint set : map to store constraints of the form (s <= alpha <= t) *)
@@ -3592,8 +3599,11 @@ exception FoundApply of t * int * int * Tallying.CS.sl
 
 (** find two sets of type substitutions I,J such that
     s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
+
 let apply_raw delta s t =
   Tallying.NormMemoHash.clear Tallying.memo_norm;
+  let s = Positive.substitute_kind delta Var.function_kind s in
+  let t = Positive.substitute_kind delta Var.argument_kind t in
   let vgamma = Var.mk "Gamma" in
   let gamma = var vgamma in
   let cgamma = cons gamma in

types/var.ml

 
 module V = struct
-  type t = { id : Ident.U.t ; fr : int }
+  type t = { id : Ident.U.t ; fr : int ; kind : int }
+  type kind = int
+  let function_kind = 1
+  let argument_kind = 2
+
   let dump ppf t = Format.fprintf ppf "{%a(%d)}" Ident.U.print t.id t.fr
-  let compare x y = Pervasives.compare (x.id,x.fr) (y.id,y.fr)
+  let compare x y = Pervasives.compare (x.kind,x.id,x.fr) (y.kind,y.id,y.fr)
   let equal x y = (compare x y) = 0
-  let hash x = Hashtbl.hash (x.id,x.fr)
+  let hash x = Hashtbl.hash (x.id,x.fr,x.kind)
   let check _ = ()
 
+  let freshcounter = ref 0
+
   let is_fresh x = x.fr > 0
-  let fresh v = { v with fr = v.fr + 1 }
 
-  let mk id = { id = Ident.U.mk id; fr = 0 }
-  let id x = Ident.U.get_str x.id
+  let fresh v = { v with fr = (incr freshcounter;!freshcounter) }
 
+  let mk id = { id = Ident.U.mk id; fr = 0; kind = 0; }
+
+  let id x = Ident.U.get_str x.id
+  let set_kind k v = { v with kind = k }
   let pp ppf x = Format.fprintf ppf "'%a" Ident.U.print x.id
-  let pp ppf x = dump ppf x 
 end
 
 include V

types/var.mli

 
 include Custom.T
+type kind
+
 type var = t
 
+val function_kind : kind
+val argument_kind : kind
+val set_kind : kind -> t -> t
 val pp : Format.formatter -> t -> unit
 val mk : string -> t
 val id : t -> string