From 2b8ad7e04002ebe9fec5790da924673418f2fa7f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 16 Feb 2017 12:26:13 +0100
Subject: Optimizing array mapping in the kernel.

We unroll the map operation by hand in two performance-critical cases so as
not to call the generic array allocation function in OCaml, and allocate
directly on the minor heap instead. The generic array function is slow because
it needs to discriminate between float and non-float arrays. The unrolling
replaces this by a simple increment to the minor heap pointer and moves from
the stack.

The quantity of unrolling was determined by experimental measures on various Coq
developments. It looks like most of the maps are for small arrays of size lesser
or equal to 4, so this is what is implemented here. We could probably extend it
to an even bigger number, but that would result in ugly code. From what I've seen,
virtually all maps are of size less than 16, so that we could probably be almost
optimal by going up to 16 unrollings, but the code tradeoffs are not obvious. Maybe
when we have PPX?
---
 kernel/cClosure.ml  | 11 ++++++++++-
 kernel/reduction.ml | 13 ++++++++++++-
 2 files changed, 22 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fe9ec5794c..b1dd26119e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -540,7 +540,16 @@ let mk_clos e t =
     | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) ->
         {norm = Red; term = FCLOS(t,e)}
 
-let mk_clos_vect env v = CArray.Fun1.map mk_clos env v
+(** Hand-unrolling of the map function to bypass the call to the generic array
+    allocation *)
+let mk_clos_vect env v = match v with
+| [||] -> [||]
+| [|v0|] -> [|mk_clos env v0|]
+| [|v0; v1|] -> [|mk_clos env v0; mk_clos env v1|]
+| [|v0; v1; v2|] -> [|mk_clos env v0; mk_clos env v1; mk_clos env v2|]
+| [|v0; v1; v2; v3|] ->
+  [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|]
+| v -> CArray.Fun1.map mk_clos env v
 
 (* Translate the head constructor of t from constr to fconstr. This
    function is parameterized by the function to apply on the direct
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1ae89347ad..0d7f77edae 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -71,6 +71,17 @@ let rec zlapp v = function
     Zlapp v2 :: s -> zlapp (Array.append v v2) s
   | s -> Zlapp v :: s
 
+(** Hand-unrolling of the map function to bypass the call to the generic array
+    allocation. Type annotation is required to tell OCaml that the array does
+    not contain floats. *)
+let map_lift (l : lift) (v : fconstr array) = match v with
+| [||] -> assert false
+| [|c0|] -> [|(l, c0)|]
+| [|c0; c1|] -> [|(l, c0); (l, c1)|]
+| [|c0; c1; c2|] -> [|(l, c0); (l, c1); (l, c2)|]
+| [|c0; c1; c2; c3|] -> [|(l, c0); (l, c1); (l, c2); (l, c3)|]
+| v -> CArray.Fun1.map (fun l t -> (l, t)) l v
+
 let pure_stack lfts stk =
   let rec pure_rec lfts stk =
     match stk with
@@ -80,7 +91,7 @@ let pure_stack lfts stk =
               (Zupdate _,lpstk)  -> lpstk
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
-                (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
+                (l,zlapp (map_lift l a) pstk)
 	    | (Zproj (n,m,c), (l,pstk)) ->
 		(l, Zlproj (c,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
-- 
cgit v1.2.3


From ff996b19faeff112a156f5db6c9ab9f26e855145 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 Mar 2017 00:22:51 +0200
Subject: Fix hashconsing of terms in the kernel.

In one case, the hashconsed type of a judgement was not used anywhere else.

In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.
---
 kernel/cooking.ml      | 8 ++++++--
 kernel/cooking.mli     | 2 +-
 kernel/opaqueproof.ml  | 5 ++++-
 kernel/opaqueproof.mli | 5 +++--
 kernel/term_typing.ml  | 7 +++++--
 5 files changed, 19 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f5059cd750..a9f212393e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -191,15 +191,19 @@ let lift_univs cb subst =
       subst, Univ.UContext.make (inst,cstrs')
   else subst, cb.const_universes
 
-let cook_constant env { from = cb; info } =
+let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
+  let map c =
+    let c = abstract_constant_body (expmod c) hyps in
+    if hcons then hcons_constr c else c
+  in
   let body = on_body modlist (hyps, usubst, abs_ctx)
-    (fun c -> abstract_constant_body (expmod c) hyps)
+    map
     cb.const_body
   in
   let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index eb40730969..7d47eba23e 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,7 +21,7 @@ type result =
     bool * constant_universes * inline
     * Context.Named.t option
 
-val cook_constant : env -> recipe -> result
+val cook_constant : hcons:bool -> env -> recipe -> result
 val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f147ea3433..74ba73508c 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -48,7 +48,10 @@ let turn_indirect dp o (prfs,odp) = match o with
       then CErrors.anomaly (Pp.str "Indirect in a different table")
       else CErrors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
-      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
+      (** Uncomment to check dynamically that all terms turned into
+          indirections are hashconsed. *)
+(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
+(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
       let id = Int.Map.cardinal prfs in
       let prfs = Int.Map.add id (d,cu) prfs in
       let ndp =
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5139cf0512..3897d5e51e 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,8 +28,9 @@ val empty_opaquetab : opaquetab
 (** From a [proofterm] to some [opaque]. *)
 val create : proofterm -> opaque
 
-(** Turn a direct [opaque] into an indirect one, also hashconses constr.
- *  The integer is an hint of the maximum id used so far *)
+(** Turn a direct [opaque] into an indirect one. It is your responsibility to
+  hashcons the inner term beforehand. The integer is an hint of the maximum id
+  used so far *)
 val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
 
 (** From a [opaque] back to a [constr]. This might use the
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eb2c040e1..2eba1eb2a7 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -186,7 +186,8 @@ let rec unzip ctx j =
       unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
-  { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
+  (** Do not hashcons type: it is not used by the callers of this function. *)
+  { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} 
 
 let feedback_completion_typecheck =
   let open Feedback in
@@ -507,7 +508,9 @@ let translate_local_assum env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant env r)
+  let (_, dir, _) = Constant.repr3 kn in
+  let hcons = DirPath.is_empty dir in
+  build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
 let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-- 
cgit v1.2.3


From 7fbf2a541fcc36e08ce595b482c2f257f171ab3d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 27 Mar 2017 11:35:48 +0200
Subject: Adding the size of the opaquetab in its representation.

This turned out to be costly in proofs with many abstracted lemmas, as an
important part of the time was passed in the computation of the size of the
opaquetab.
---
 kernel/opaqueproof.ml | 46 ++++++++++++++++++++++++++++------------------
 1 file changed, 28 insertions(+), 18 deletions(-)

(limited to 'kernel')

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 74ba73508c..d0593c0e05 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -21,8 +21,18 @@ type proofterm = (constr * Univ.universe_context_set) Future.computation
 type opaque =
   | Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
   | Direct of cooking_info list * proofterm
-type opaquetab = (cooking_info list * proofterm) Int.Map.t * DirPath.t
-let empty_opaquetab = Int.Map.empty, DirPath.initial
+type opaquetab = {
+  opaque_val : (cooking_info list * proofterm) Int.Map.t;
+  (** Actual proof terms *)
+  opaque_len : int;
+  (** Size of the above map *)
+  opaque_dir : DirPath.t;
+}
+let empty_opaquetab = {
+  opaque_val = Int.Map.empty;
+  opaque_len = 0;
+  opaque_dir = DirPath.initial;
+}
 
 (* hooks *)
 let default_get_opaque dp _ =
@@ -42,9 +52,9 @@ let set_indirect_univ_accessor f = (get_univ := f)
 
 let create cu = Direct ([],cu)
 
-let turn_indirect dp o (prfs,odp) = match o with
+let turn_indirect dp o tab = match o with
   | Indirect (_,_,i) ->
-      if not (Int.Map.mem i prfs)
+      if not (Int.Map.mem i tab.opaque_val)
       then CErrors.anomaly (Pp.str "Indirect in a different table")
       else CErrors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
@@ -52,14 +62,15 @@ let turn_indirect dp o (prfs,odp) = match o with
           indirections are hashconsed. *)
 (* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
 (* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
-      let id = Int.Map.cardinal prfs in
-      let prfs = Int.Map.add id (d,cu) prfs in
-      let ndp =
-        if DirPath.equal dp odp then odp
-        else if DirPath.equal odp DirPath.initial then dp
+      let id = tab.opaque_len in
+      let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+      let opaque_dir =
+        if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
+        else if DirPath.equal tab.opaque_dir DirPath.initial then dp
         else CErrors.anomaly
           (Pp.str "Using the same opaque table for multiple dirpaths") in
-      Indirect ([],dp,id), (prfs, ndp)
+      let ntab = { opaque_val; opaque_dir; opaque_len = id + 1 } in
+      Indirect ([],dp,id), ntab
 
 let subst_opaque sub = function
   | Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
@@ -75,21 +86,21 @@ let discharge_direct_opaque ~cook_constr ci = function
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain ~pure:true cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque (prfs,odp) = function
+let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> ignore(Future.join cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
         ignore(Future.join fp)
 
-let uuid_opaque (prfs,odp) = function
+let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> Some (Future.uuid cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then Some (Future.uuid (snd (Int.Map.find i prfs)))
       else None
 
-let force_proof (prfs,odp) = function
+let force_proof { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
   | Indirect (l,dp,i) ->
@@ -100,7 +111,7 @@ let force_proof (prfs,odp) = function
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints (prfs,odp) = function
+let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
@@ -109,14 +120,14 @@ let force_constraints (prfs,odp) = function
         | None -> Univ.ContextSet.empty
         | Some u -> Future.force u
 
-let get_constraints (prfs,odp) = function
+let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> Some(Future.chain ~pure:true cu snd)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then Some(Future.chain ~pure:true (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof (prfs,odp) = function
+let get_proof { opaque_val = prfs; opaque_dir = odp } = function
   | Direct (_,cu) -> Future.chain ~pure:true cu fst
   | Indirect (l,dp,i) ->
       let pt =
@@ -132,8 +143,7 @@ let a_constr = Future.from_val (Term.mkRel 1)
 let a_univ = Future.from_val Univ.ContextSet.empty
 let a_discharge : cooking_info list = []
 
-let dump (otab,_) =
-  let n = Int.Map.cardinal otab in
+let dump { opaque_val = otab; opaque_len = n } =
   let opaque_table = Array.make n a_constr in
   let univ_table = Array.make n a_univ in
   let disch_table = Array.make n a_discharge in
-- 
cgit v1.2.3


From 11b4703ed83eeda9d959464f08185aedd3f7c250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 Mar 2017 22:28:18 +0200
Subject: More efficient check in validity of side-effects.

We don't need to look for the size of the whole list to find whether we can
extract a suffix from it, as we can do it in one go instead. This slowness
was observable in abstract-heavy code.
---
 kernel/term_typing.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eba1eb2a7..c171ba2bbf 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -139,6 +139,12 @@ let inline_side_effects env body ctx side_eff =
   (* CAVEAT: we assure a proper order *)
   List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
 
+let rec is_nth_suffix n l suf =
+  if Int.equal n 0 then l == suf
+  else match l with
+  | [] -> false
+  | _ :: l -> is_nth_suffix (pred n) l suf
+
 (* Given the list of signatures of side effects, checks if they match.
  * I.e. if they are ordered descendants of the current revstruct *)
 let check_signatures curmb sl =
@@ -151,7 +157,7 @@ let check_signatures curmb sl =
           match sl with
           | None -> sl, None
           | Some n ->
-              if List.length mb >= how_many && CList.skipn how_many mb == curmb
+              if is_nth_suffix how_many mb curmb
               then Some (n + how_many), Some mb
               else None, None
         with CEphemeron.InvalidKey -> None, None in
-- 
cgit v1.2.3


From 78aca729a95d5e622c251d247abf29159dfe66a4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Apr 2017 18:49:58 +0200
Subject: Documenting the fact terms are only hashconsed outside of a section.

---
 kernel/term_typing.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c171ba2bbf..e203fce9a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -514,6 +514,8 @@ let translate_local_assum env t =
     t
 
 let translate_recipe env kn r =
+  (** We only hashcons the term when outside of a section, otherwise this would
+      be useless. It is detected by the dirpath of the constant being empty. *)
   let (_, dir, _) = Constant.repr3 kn in
   let hcons = DirPath.is_empty dir in
   build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
-- 
cgit v1.2.3


From d939a024cd077c8abce709dd69eb805cab9068db Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Apr 2017 01:21:41 +0200
Subject: Inline the only use of hcons_j in Term_typing.

---
 kernel/term_typing.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index e203fce9a8..6dfa64357c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -191,10 +191,6 @@ let rec unzip ctx j =
   | `Cut (n,ty,arg) :: ctx ->
       unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
-let hcons_j j =
-  (** Do not hashcons type: it is not used by the callers of this function. *)
-  { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} 
-
 let feedback_completion_typecheck =
   let open Feedback in
   Option.iter (fun state_id ->
@@ -231,13 +227,13 @@ let infer_declaration ~trust env kn dcl =
             let body,env,ectx = skip_trusted_seff valid_signatures body env in
             let j = infer env body in
             unzip ectx j in
-          let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _ = judge_of_cast env j DEFAULTcast tyj in
           assert (eq_constr typ tyj.utj_val);
+          let c = hcons_constr j.uj_val in
           let _typ = RegularArity (Vars.subst_univs_level_constr subst typ) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, uctx) in
+          c, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
-- 
cgit v1.2.3