A very modest typeclass caching

src/basic/FStar.Common.fst

@@ -150,3 +150,10 @@ let max_suffix (f : 'a -> bool) (xs : list 'a) : list 'a * list 'a =
       (acc, x::xs)
   in
   xs |> List.rev |> aux [] |> (fun (xs, ys) -> List.rev ys, xs)
+
+let rec eq_list (f: 'a -> 'a -> bool) (l1 l2 : list 'a)
+  : bool
+  = match l1, l2 with
+    | [], [] -> true
+    | [], _ | _, [] -> false
+    | x1::t1, x2::t2 -> f x1 x2 && eq_list f t1 t2

src/syntax/FStar.Syntax.Util.fst

@@ -2541,3 +2541,10 @@ let is_binder_unused (b:binder) =
 
 let deduplicate_terms (l:list term) = 
   FStar.Compiler.List.deduplicate (fun x y -> eq_tm x y = Equal) l
+
+let eq_binding b1 b2 =
+    match b1, b2 with
+    | Binding_var bv1, Binding_var bv2 -> bv_eq bv1 bv2 && term_eq bv1.sort bv2.sort
+    | Binding_lid (lid1, _), Binding_lid (lid2, _) -> lid_equals lid1 lid2
+    | Binding_univ u1, Binding_univ u2 -> ident_equals u1 u2
+    | _ -> false

src/typechecker/FStar.TypeChecker.Rel.fst

@@ -5404,6 +5404,37 @@ let is_tac_implicit_resolved (env:env) (i:implicit) : bool =
 let resolve_implicits' env is_tac is_gen (implicits:Env.implicits)
   : list (implicit * implicit_checking_status) =
 
+  (* Meta argument cache: during a single run of this resolve_implicits' function
+  we keep track of all results of the "cacheable" tactics that are used for meta
+  arguments. The only cacheable tactic, for now, is tcresolve. Before trying to run
+  it, we check the cache to see if we have already solved a problem in the same environment
+  and for the same uvar type (in this case, the constraint). If so, we just take that result.
+
+  This is pretty conservative. e.g. in
+    f (1 + 1);
+    g (1 + 1)
+  we cannot reuse the solution for each +, since there is an extra unit binder when
+  we check `g ...`. But it does lead to big gains in expressions like `1 + 1 + 1 ...`. *)
+  let cacheable tac = U.is_fvar PC.tcresolve_lid tac in
+  let __meta_arg_cache : ref (list (term & env_t & typ & term)) = BU.mk_ref [] in
+  let meta_arg_cache_result (tac : term) (e : env_t) (ty : term) (res : term) : unit =
+    __meta_arg_cache := (tac, e, ty, res) :: !__meta_arg_cache
+  in
+  let meta_arg_cache_lookup (tac : term) (e : env_t) (ty : term) : option term =
+    let rec aux l : option term =
+      match l with
+      | [] -> None
+      | (tac', e', ty', res') :: l' ->
+        if U.term_eq tac tac'
+           && FStar.Common.eq_list U.eq_binding e.gamma e'.gamma
+           && U.term_eq ty ty'
+        then Some res'
+        else aux l'
+    in
+    aux !__meta_arg_cache
+  in
+  (* / cache *) 
+
   let rec until_fixpoint (acc:tagged_implicits * bool)
                          (implicits:Env.implicits) 
     : tagged_implicits =
@@ -5434,34 +5465,46 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits)
 
     | hd::tl ->
       let { imp_reason = reason; imp_tm = tm; imp_uvar = ctx_u; imp_range = r } = hd in
-      let { 
-            uvar_decoration_typ;
-            uvar_decoration_should_check 
-          } = UF.find_decoration ctx_u.ctx_uvar_head
-      in
-      if Env.debug env <| Options.Other "Rel"
-      then BU.print3 "resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n"
-             (show tm)
-             (Print.ctx_uvar_to_string ctx_u)
-             (string_of_bool is_tac);
-      if Allow_unresolved? uvar_decoration_should_check
-      then until_fixpoint (out, true) tl
-      else if unresolved ctx_u
-      then (if flex_uvar_has_meta_tac ctx_u
-            then let t = run_meta_arg_tac ctx_u in
-                 // let the unifier handle setting the variable
-                 let extra =
-                   match teq_nosmt env t tm with
-                   | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?"
-                   | Some g -> g.implicits in
-
-                 until_fixpoint (out, true) (extra @ tl)
-            else until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl)
-      else if Allow_untyped? uvar_decoration_should_check ||
-              Already_checked? uvar_decoration_should_check ||
-              is_gen
-      then until_fixpoint (out, true) tl
-      else begin
+      let { uvar_decoration_typ; uvar_decoration_should_check } = UF.find_decoration ctx_u.ctx_uvar_head in
+      if Env.debug env <| Options.Other "Rel" then
+        BU.print3 "resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n"
+             (show tm) (show ctx_u) (show is_tac);
+      begin match () with
+      | _ when Allow_unresolved? uvar_decoration_should_check ->
+        until_fixpoint (out, true) tl
+
+      | _ when unresolved ctx_u && flex_uvar_has_meta_tac ctx_u ->
+        let Some (Ctx_uvar_meta_tac meta) = ctx_u.ctx_uvar_meta in
+        let m_env : env_t = Dyn.undyn (fst meta) in
+        let tac = snd meta in
+        let typ = U.ctx_uvar_typ ctx_u in
+        let solve_with (t:term) =
+          let extra =
+            match teq_nosmt env t tm with
+            | None -> failwith "resolve_implicits: unifying with an unresolved uvar failed?"
+            | Some g -> g.implicits
+          in
+          until_fixpoint (out, true) (extra @ tl)
+        in
+        if cacheable tac then
+          match meta_arg_cache_lookup tac m_env typ with
+          | Some res -> solve_with res
+          | None ->
+            let t = run_meta_arg_tac ctx_u in
+            meta_arg_cache_result tac m_env typ t;
+            solve_with t
+        else
+          let t = run_meta_arg_tac ctx_u in
+          solve_with t
+
+      | _ when unresolved ctx_u ->
+        until_fixpoint ((hd, Implicit_unresolved)::out, changed) tl
+
+      | _ when Allow_untyped? uvar_decoration_should_check ||
+               Already_checked? uvar_decoration_should_check ||
+               is_gen ->
+        until_fixpoint (out, true) tl
+      | _ ->
         let env = {env with gamma=ctx_u.ctx_uvar_gamma} in
         (*
          * AR: Some opportunities for optimization here,

tests/Makefile

@@ -12,6 +12,7 @@ ALL_TEST_DIRS += micro-benchmarks
 ALL_TEST_DIRS += prettyprinting
 ALL_TEST_DIRS += struct
 ALL_TEST_DIRS += tactics
+ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 
 all: $(addsuffix .all, $(ALL_TEST_DIRS))

tests/typeclasses/CoallesceConstraints.fst

@@ -0,0 +1,16 @@
+module CoallesceConstraints
+
+open FStar.Class.Printable
+
+(* tcresolve runs only once here. We should really check for it... *)
+let test (x:int) =
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x ^
+  to_string x ^ to_string x ^ to_string x ^ to_string x

tests/typeclasses/Makefile

@@ -0,0 +1,15 @@
+FSTAR_HOME=../..
+
+FSTAR_FILES=$(wildcard *.fst)
+
+all: verify-all
+
+include $(FSTAR_HOME)/examples/Makefile.common
+
+verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
+
+clean:
+	$(call msg, "CLEAN")
+	$(Q)rm -f .depend
+	$(Q)rm -rf _cache
+	$(Q)rm -rf _output