Add a memoization table to remember previously applied substitutions.

types/types.ml

@@ -2814,20 +2814,51 @@ module Positive = struct
     apply_subst ~subst:subst ~after:(fun y -> define x y;x) t
 
   (* Pre-condition : alpha \not\in \delta *)
+  module MemoSubst = Hashtbl.Make (struct
+      type t = descr * (Var.t * descr) list
+      let hash (t, l) =
+        List.fold_left
+          (fun acc (v,t) -> Var.hash v + 17 * Descr.hash t + 31 * acc)
+          (Descr.hash t) l
+
+      let equal (t1, l1) (t2, l2) =
+        Descr.equal t1 t2 && (try List.for_all2 (fun (v1, t1) (v2, t2) ->
+            Var.equal v1 v2 && Descr.equal t1 t2) l1 l2 with _ -> false)
+    end)
+
+  let memo_subst = MemoSubst.create 17
+  let () = at_exit (fun () ->
+      Format.eprintf "%i@\n%!" (MemoSubst.length memo_subst))
+
   let substitute t (alpha,s) =
-    let vs = ty s in
-    let subst d = if Var.equal d alpha then vs else var d in
-    apply_subst ~subst:subst t
+    let k = (t, [(alpha, s)]) in
+    try
+      MemoSubst.find memo_subst k
+    with Not_found ->
+      let r =
+        let vs = ty s in
+        let subst d = if Var.equal d alpha then vs else var d in
+        apply_subst ~subst:subst t
+      in
+      MemoSubst.add memo_subst k r; r
 
   let substitute_list t l =
-    let subst d =
-      try
-        ty
-        @@ snd
-        @@ List.find (fun (alpha,_) -> Var.equal d alpha) l
-      with Not_found -> var d
-    in
-    apply_subst ~subst:subst t
+    let k = (t,l) in
+    try
+      MemoSubst.find memo_subst k
+    with Not_found ->
+      let r =
+        let subst d =
+          try
+            ty
+            @@ snd
+            @@ List.find (fun (alpha,_) -> Var.equal d alpha) l
+          with Not_found -> var d
+        in
+        apply_subst ~subst:subst t
+      in
+      MemoSubst.add memo_subst k r; r
+
 
   let substitute_free delta t =
     let h = Hashtbl.create 17 in