Types with variables are no longer internally represented by the same

type.

This change allows sharing only for types that do not contain variables.

types/types.ml

@@ -426,6 +426,7 @@ let var a =  {
 }
 
 let is_var t = TLV.is_single t.toplvars
+let no_var t = TLV.no_variables t.toplvars
 
 let char c = { empty with chars = BoolChars.atom (`Atm c) }
 let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
@@ -2721,9 +2722,10 @@ module Tallying = struct
   let memo_norm = DescrHash.create 17
   let norm t =
     try DescrHash.find memo_norm t
-    with Not_found ->
+    with Not_found -> begin
       let res = norm (t,DescrHash.create 17) in
       DescrHash.add memo_norm t res; res
+    end
 
   exception UnSatConstr
 

types/types.mli

@@ -110,6 +110,9 @@ val neg    : t -> t
 val empty  : t
 val any    : t
 
+val no_var : t -> bool
+val is_var : t -> bool
+
 val any_node : Node.t
 val empty_node : Node.t
 

typing/typepat.ml

@@ -129,7 +129,8 @@ let deferr s = raise (Patterns.Error s)
       (* x and y have been internalized; if they were equivalent,
 	 they would be equal *)
     else match x.desc,y.desc with
-      | IType (tx,_), IType (ty,_) when Types.equal tx ty -> link x y
+      | IType (tx,_), IType (ty,_) when (Types.no_var tx) && (Types.no_var ty) && (Types.equal tx ty) -> link x y
+      | IType (tx,_), IType (ty,_) when not(Types.no_var tx) && (Types.no_var ty) -> ()
       | IOr (x1,x2,_), IOr (y1,y2,_)
       | IAnd (x1,x2,_), IAnd (y1,y2,_)
       | IDiff (x1,x2,_), IDiff (y1,y2,_)

typing/typer.ml

@@ -395,7 +395,7 @@ module IType = struct
     let d = derecurs variance penv p in
     elim_concats ();
     check_delayed ();
-    (* internalize d; *)
+    internalize d;
     d
 
 (* API *)