Avoid roundtrip [fconstr] -> [constr] -> [fconstr] in the kernel

kernel/cClosure.ml

@@ -271,6 +271,46 @@ and fterm =
 
 and finvert = fconstr array
 
+let copy_fconstr (x : fconstr) : fconstr =
+  (* note: it could be worthwhile to try to copy the [fconstr] lazily.
+     doing this would probably mean that we should use a better
+  *)
+  let module SF = Hashtbl in
+  let memo = SF.create 17 in
+  let rec copy_fconstr x =
+    try SF.find memo x
+    with Not_found ->
+      let y = { mark = x.mark ; term = copy_fterm x.term } in
+      let () = SF.add memo x y in
+      y
+  and copy_fterm = function
+    | FRel _ as x -> x
+    | FAtom _ as x -> x
+    | FFlex _ as x -> x
+    | FInd _ as x -> x
+    | FConstruct _ as x -> x
+    | FApp (a, b) -> FApp (copy_fconstr a, Array.map copy_fconstr b)
+    | FProj (a, t) -> FProj (a, copy_fconstr t)
+    | FFix (f, ts) -> FFix (f, copy_usubs ts)
+    | FCoFix (f, ts) -> FCoFix (f, copy_usubs ts)
+    | FCaseT (ci, us, cs, cr, f, cbs, ts) ->
+      FCaseT (ci, us, cs, cr, copy_fconstr f, cbs, copy_usubs ts)
+    | FCaseInvert (ci, u, cs, cr, fs, f, cbs, ts) ->
+      FCaseInvert (ci, u, cs, cr, Array.map copy_fconstr fs, copy_fconstr f, cbs, copy_usubs ts)
+    | FLambda (i, l, c, ts) -> FLambda (i, l, c, copy_usubs ts)
+    | FProd (p, f, c, ts) -> FProd (p, copy_fconstr f, c, copy_usubs ts)
+    | FLetIn (b, t1, t2, c, ts) -> FLetIn (b, copy_fconstr t1, copy_fconstr t2, c, copy_usubs ts)
+    | FEvar (e, ts) -> FEvar (e, copy_usubs ts)
+    | FArray (u, p, f) -> FArray (u, Parray.map copy_fconstr p, copy_fconstr f)
+    | FLIFT (i, f) -> FLIFT (i, copy_fconstr f)
+    | FCLOS (c, ts) -> FCLOS (c, copy_usubs ts)
+    | FInt _ as x -> x
+    | FFloat _ as x -> x
+    | FIrrelevant as x -> x
+    | FLOCKED as x -> x
+  and copy_usubs x = (Esubst.subs_map copy_fconstr (fst x), snd x)
+  in copy_fconstr x
+
 let fterm_of v = v.term
 let set_ntrl v = v.mark <- Ntrl
 let is_val v = match v.mark with Ntrl -> true | Cstr | Whnf | Red -> false
@@ -339,7 +379,7 @@ let empty_stack = []
 let append_stack v s =
   if Int.equal (Array.length v) 0 then s else
   match s with
-  | Zapp l :: s -> Zapp (Array.append v l) :: s
+  | Zapp l :: s -> Zapp (Array.append v l) :: s (* <<<< this is an allocation *)
   | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] ->
     Zapp v :: s
 

kernel/cClosure.mli

@@ -90,6 +90,8 @@ type fconstr
 (** [fconstr] can be accessed by using the function [fterm_of] and by
    matching on type [fterm] *)
 
+val copy_fconstr : fconstr -> fconstr
+
 type finvert
 
 type 'a usubs = 'a subs Univ.puniverses

kernel/esubst.ml

@@ -115,7 +115,20 @@ type 'a tree =
 
 *)
 
+let or_var_map f = function
+  | Arg x -> Arg (f x)
+  | Var x -> Var x
+
+let rec tree_map f = function
+  | Leaf (s, x) -> Leaf (s, or_var_map f x)
+  | Node (s1, x, l, r, s2) -> Node (s1, or_var_map f x, tree_map f l, tree_map f r, s2)
+
 type 'a subs = Nil of shf * int | Cons of int * 'a tree * 'a subs
+
+let rec subs_map f = function
+  | Nil _ as x -> x
+  | Cons (i, t, s) -> Cons (i, tree_map f t, subs_map f s)
+
 (*
   In the naive semantics mentioned above, we have the following.
 

kernel/esubst.mli

@@ -44,6 +44,9 @@ val subs_lift: 'a subs -> 'a subs
 (** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ *)
 val subs_liftn: int -> 'a subs -> 'a subs
 
+(** map *)
+val subs_map: ('a -> 'b) -> 'a subs -> 'b subs
+
 (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
     [subs]. The result is either (Inl(lams,v)) when the variable is
     substituted by value [v] under [lams] binders (i.e. v *has* to be

kernel/reduction.ml

@@ -187,10 +187,12 @@ let whd_allnolet env t =
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
 
 (* functions of this type can be called from outside the kernel *)
-type 'a extended_conversion_function =
+type ('l,'r) extended_conversion_function_2 =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:constr evar_handler ->
-  'a -> 'a -> unit
+  'l -> 'r -> unit
+
+type 'a extended_conversion_function = ('a,'a) extended_conversion_function_2
 
 exception NotConvertible
 
@@ -853,15 +855,15 @@ and convert_list l2r infos lft1 lft2 v1 v2 cuniv = match v1, v2 with
   convert_list l2r infos lft1 lft2 v1 v2 cuniv
 | _, _ -> raise NotConvertible
 
-let clos_gen_conv trans cv_pb l2r evars env graph univs t1 t2 =
+let clos_gen_conv trans cv_pb l2r evars env graph univs l r =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_conv_infos ~univs:graph ~evars reds env in
   let infos = {
     cnv_inf = infos;
     lft_tab = create_tab ();
     rgt_tab = create_tab ();
   } in
-  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+  ccnv cv_pb l2r infos el_id el_id l r univs
 
 
 let check_eq univs u u' =
@@ -915,16 +917,24 @@ let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=defaul
   in
     if b then ()
     else
-      let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
+      let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) (inject t1) (inject t2) in
         ()
 
 let conv = gen_conv CONV
 let conv_leq = gen_conv CUMUL
 
+let gen_conv_fconstr cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=default_evar_handler) t1 t2 =
+  let univs = Environ.universes env in
+  let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) (inject t1) t2 in
+  ()
+
+let conv_fconstr = gen_conv_fconstr CONV
+let conv_leq_fconstr = gen_conv_fconstr CUMUL
+
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let graph = Environ.universes env in
   let (s, _) =
-    clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
+    clos_gen_conv reds cv_pb l2r evars env graph univs (inject t1) (inject t2)
   in s
 
 let default_conv cv_pb env t1 t2 =

kernel/reduction.mli

@@ -10,6 +10,7 @@
 
 open Constr
 open Environ
+open CClosure
 
 (***********************************************************************
   s Reduction functions *)
@@ -29,10 +30,13 @@ val nf_betaiota      : env -> constr -> constr
 exception NotConvertible
 
 type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
-type 'a extended_conversion_function =
+
+type ('l,'r) extended_conversion_function_2 =
   ?l2r:bool -> ?reds:TransparentState.t -> env ->
   ?evars:constr evar_handler ->
-  'a -> 'a -> unit
+  'l -> 'r -> unit
+
+type 'a extended_conversion_function = ('a,'a) extended_conversion_function_2
 
 type conv_pb = CONV | CUMUL
 
@@ -69,8 +73,11 @@ val checked_universes : UGraph.t universe_compare
 
 (** These two functions can only raise NotConvertible *)
 val conv : constr extended_conversion_function
+val conv_fconstr : (constr, fconstr) extended_conversion_function_2
 
 val conv_leq : types extended_conversion_function
+val conv_leq_fconstr : (types, fconstr) extended_conversion_function_2
+
 
 (** Depending on the universe state functions, this might raise
   [UniverseInconsistency] in addition to [NotConvertible] (for better error

kernel/typeops.ml

@@ -194,12 +194,18 @@ let type_of_apply env func funt argsv argstv =
       let () = assert (check_empty_stack stk) in
       match fterm_of typ with
       | FProd (_, c1, c2, e) ->
-        let arg = argsv.(i) in
         let argt = argstv.(i) in
-        let c1 = term_of_fconstr c1 in
-        begin match conv_leq env argt c1 with
-        | () -> apply_rec (i+1) (mk_clos (CClosure.usubs_cons (inject arg) e) c2)
+        (* reductions necessary to compare the type of the argument
+           to the type of [c1] should *not* be retained when checking
+           the rest of the term. To achieve this, while retaining sharing,
+           we perform the conversion check on a copy of [c1].
+         *)
+        begin match conv_leq_fconstr env argt (copy_fconstr c1) with
+        | () ->
+          let arg = argsv.(i) in
+          apply_rec (i+1) (mk_clos (CClosure.usubs_cons (inject arg) e) c2)
         | exception NotConvertible ->
+          let c1 = term_of_fconstr c1 in
           error_cant_apply_bad_type env
             (i+1,c1,argt)
             (make_judge func funt)