Merge branch 'master' into econstr

7 files changed, 78 insertions, 33 deletions

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/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..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,21 +52,25 @@ 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) ->
-      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr 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
+      (** 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 = 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)
@@ -72,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) ->
@@ -97,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
@@ -106,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 =
@@ -129,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
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/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)) ->
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eb2c040e1..6dfa64357c 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
@@ -185,9 +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 =
-  { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
-
 let feedback_completion_typecheck =
   let open Feedback in
   Option.iter (fun state_id ->
@@ -224,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,
@@ -507,7 +510,11 @@ let translate_local_assum env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant env 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)
 
 let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =