1 files changed, 133 insertions, 100 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 08114abc..fd939402 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -31,7 +31,6 @@ open Environ
 open Esubst
 
 let stats = ref false
-let share = ref true
 
 (* Profiling *)
 let beta = ref 0
@@ -265,7 +264,8 @@ type 'a infos_cache = {
   i_repr : 'a infos -> 'a infos_tab -> constr -> 'a;
   i_env : env;
   i_sigma : existential -> constr option;
-  i_rels : (Context.Rel.Declaration.t * Pre_env.lazy_val) Range.t;
+  i_rels : (Constr.rel_declaration * lazy_val) Range.t;
+  i_share : bool;
 }
 
 and 'a infos = {
@@ -313,13 +313,13 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref =
 let evar_value cache ev =
   cache.i_sigma ev
 
-let create mk_cl flgs env evars =
-  let open Pre_env in
+let create ~repr ~share flgs env evars =
   let cache =
-    { i_repr = mk_cl;
+    { i_repr = repr;
       i_env = env;
       i_sigma = evars;
-      i_rels = (Environ.pre_env env).env_rel_context.env_rel_map;
+      i_rels = env.env_rel_context.env_rel_map;
+      i_share = share;
     }
   in { i_flags = flgs; i_cache = cache }
 
@@ -385,8 +385,8 @@ let mk_red f = {norm=Red;term=f}
 
 (* Could issue a warning if no is still Red, pointing out that we loose
    sharing. *)
-let update v1 no t =
-  if !share then
+let update ~share v1 no t =
+  if share then
     (v1.norm <- no;
      v1.term <- t;
      v1)
@@ -398,7 +398,7 @@ let update v1 no t =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Constant.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -482,7 +482,7 @@ let rec lft_fconstr n ft =
 let lift_fconstr k f =
   if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
-  if Int.equal k 0 then v else CArray.Fun1.map lft_fconstr k v
+  if Int.equal k 0 then v else Array.Fun1.map lft_fconstr k v
 
 let clos_rel e i =
   match expand_rel i e with
@@ -499,14 +499,16 @@ let compact_stack head stk =
         (* Be sure to create a new cell otherwise sharing would be
            lost by the update operation *)
         let h' = lft_fconstr depth head in
-        let _ = update m h'.norm h'.term in
+        (** The stack contains [Zupdate] marks only if in sharing mode *)
+        let _ = update ~share:true m h'.norm h'.term in
         strip_rec depth s
     | stk -> zshift depth stk in
   strip_rec 0 stk
 
 (* Put an update mark in the stack, only if needed *)
-let zupdate m s =
-  if !share && begin match m.norm with Red -> true | _ -> false end
+let zupdate info m s =
+  let share = info.i_cache.i_share in
+  if share && begin match m.norm with Red -> true | _ -> false end
   then
     let s' = compact_stack m s in
     let _ = m.term <- FLOCKED in
@@ -547,7 +549,7 @@ let mk_clos_vect env v = match v with
 | [|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
+| v -> Array.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
@@ -562,7 +564,7 @@ let mk_clos_deep clos_fun env t =
           term = FCast (clos_fun env a, k, clos_fun env b)}
     | App (f,v) ->
         { norm = Red;
-	  term = FApp (clos_fun env f, CArray.Fun1.map clos_fun env v) }
+          term = FApp (clos_fun env f, Array.Fun1.map clos_fun env v) }
     | Proj (p,c) ->
 	{ norm = Red;
 	  term = FProj (p, clos_fun env c) }
@@ -588,78 +590,95 @@ let mk_clos_deep clos_fun env t =
 let mk_clos2 = mk_clos_deep mk_clos
 
 (* The inverse of mk_clos_deep: move back to constr *)
-let rec to_constr constr_fun lfts v =
+let rec to_constr lfts v =
   match v.term with
     | FRel i -> mkRel (reloc_rel i lfts)
     | FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
     | FFlex (VarKey x) -> mkVar x
     | FAtom c -> exliftn lfts c
     | FCast (a,k,b) ->
-        mkCast (constr_fun lfts a, k, constr_fun lfts b)
+      mkCast (to_constr lfts a, k, to_constr lfts b)
     | FFlex (ConstKey op) -> mkConstU op
     | FInd op -> mkIndU op
     | FConstruct op -> mkConstructU op
     | FCaseT (ci,p,c,ve,env) ->
-	mkCase (ci, constr_fun lfts (mk_clos env p),
-                constr_fun lfts c,
-		Array.map (fun b -> constr_fun lfts (mk_clos env b)) ve)
-    | FFix ((op,(lna,tys,bds)),e) ->
+      if is_subs_id env && is_lift_id lfts then
+        mkCase (ci, p, to_constr lfts c, ve)
+      else
+        let subs = comp_subs lfts env in
+        mkCase (ci, subst_constr subs p,
+            to_constr lfts c,
+            Array.map (fun b -> subst_constr subs b) ve)
+    | FFix ((op,(lna,tys,bds)) as fx, e) ->
+      if is_subs_id e && is_lift_id lfts then
+        mkFix fx
+      else
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
-	let lfts' = el_liftn n lfts in
-	mkFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		         CArray.Fun1.map constr_fun lfts' fbds))
-    | FCoFix ((op,(lna,tys,bds)),e) ->
+        let subs_ty = comp_subs lfts e in
+        let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+        let tys = Array.Fun1.map subst_constr subs_ty tys in
+        let bds = Array.Fun1.map subst_constr subs_bd bds in
+        mkFix (op, (lna, tys, bds))
+    | FCoFix ((op,(lna,tys,bds)) as cfx, e) ->
+      if is_subs_id e && is_lift_id lfts then
+        mkCoFix cfx
+      else
         let n = Array.length bds in
-        let ftys = CArray.Fun1.map mk_clos e tys in
-        let fbds = CArray.Fun1.map mk_clos (subs_liftn n e) bds in
-	let lfts' = el_liftn (Array.length bds) lfts in
-	mkCoFix (op, (lna, CArray.Fun1.map constr_fun lfts ftys,
-		           CArray.Fun1.map constr_fun lfts' fbds))
+        let subs_ty = comp_subs lfts e in
+        let subs_bd = comp_subs (el_liftn n lfts) (subs_liftn n e) in
+        let tys = Array.Fun1.map subst_constr subs_ty tys in
+        let bds = Array.Fun1.map subst_constr subs_bd bds in
+        mkCoFix (op, (lna, tys, bds))
     | FApp (f,ve) ->
-	mkApp (constr_fun lfts f,
-	       CArray.Fun1.map constr_fun lfts ve)
+        mkApp (to_constr lfts f,
+               Array.Fun1.map to_constr lfts ve)
     | FProj (p,c) ->
-        mkProj (p,constr_fun lfts c)
+        mkProj (p,to_constr lfts c)
 
-    | FLambda _ ->
-        let (na,ty,bd) = destFLambda mk_clos2 v in
-	mkLambda (na, constr_fun lfts ty,
-	              constr_fun (el_lift lfts) bd)
+    | FLambda (len, tys, f, e) ->
+      if is_subs_id e && is_lift_id lfts then
+        Term.compose_lam (List.rev tys) f
+      else
+        let subs = comp_subs lfts e in
+        let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in
+        let f = subst_constr (subs_liftn len subs) f in
+        Term.compose_lam (List.rev tys) f
     | FProd (n,t,c)   ->
-	mkProd (n, constr_fun lfts t,
-	           constr_fun (el_lift lfts) c)
+        mkProd (n, to_constr lfts t,
+                   to_constr (el_lift lfts) c)
     | FLetIn (n,b,t,f,e) ->
-        let fc = mk_clos2 (subs_lift e) f in
-	mkLetIn (n, constr_fun lfts b,
-	            constr_fun lfts t,
-	            constr_fun (el_lift lfts) fc)
+      let subs = comp_subs (el_lift lfts) (subs_lift e) in
+        mkLetIn (n, to_constr lfts b,
+                    to_constr lfts t,
+                    subst_constr subs f)
     | FEvar ((ev,args),env) ->
-        mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
-    | FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
+      let subs = comp_subs lfts env in
+        mkEvar(ev,Array.map (fun a -> subst_constr subs a) args)
+    | FLIFT (k,a) -> to_constr (el_shft k lfts) a
     | FCLOS (t,env) ->
-        let fr = mk_clos2 env t in
-        let unfv = update v fr.norm fr.term in
-        to_constr constr_fun lfts unfv
+      if is_subs_id env && is_lift_id lfts then t
+      else
+        let subs = comp_subs lfts env in
+        subst_constr subs t
     | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
 
+and subst_constr subst c = match Constr.kind c with
+| Rel i ->
+  begin match expand_rel i subst with
+  | Inl (k, lazy v) -> Vars.lift k v
+  | Inr (m, _) -> mkRel m
+  end
+| _ ->
+  Constr.map_with_binders Esubst.subs_lift subst_constr subst c
+
+and comp_subs el s =
+  Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s
+
 (* This function defines the correspondance between constr and
    fconstr. When we find a closure whose substitution is the identity,
    then we directly return the constr to avoid possibly huge
    reallocation. *)
-let term_of_fconstr =
-  let rec term_of_fconstr_lift lfts v =
-    match v.term with
-      | FCLOS(t,env) when is_subs_id env && is_lift_id lfts -> t
-      | FLambda(_,tys,f,e) when is_subs_id e && is_lift_id lfts ->
-          Term.compose_lam (List.rev tys) f
-      | FFix(fx,e) when is_subs_id e && is_lift_id lfts -> mkFix fx
-      | FCoFix(cfx,e) when is_subs_id e && is_lift_id lfts -> mkCoFix cfx
-      | _ -> to_constr term_of_fconstr_lift lfts v in
-  term_of_fconstr_lift el_id
-
-
+let term_of_fconstr c = to_constr el_id c
 
 (* fstrong applies unfreeze_fun recursively on the (freeze) term and
  * yields a term.  Assumes that the unfreeze_fun never returns a
@@ -675,14 +694,15 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s ->
-        zip {norm=neutr m.norm; term=FProj(Projection.make cst true,m)} s
+    | Zproj p :: s ->
+        zip {norm=neutr m.norm; term=FProj(Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
         zip (lift_fconstr n m) s
     | Zupdate(rf)::s ->
-        zip (update rf m.norm m.term) s
+      (** The stack contains [Zupdate] marks only if in sharing mode *)
+        zip (update ~share:true rf m.norm m.term) s
 
 let fapp_stack (m,stk) = zip m stk
 
@@ -702,7 +722,8 @@ let strip_update_shift_app_red head stk =
         strip_rec (Zapp args :: rstk)
           {norm=h.norm;term=FApp(h,args)} depth s
     | Zupdate(m)::s ->
-        strip_rec rstk (update m h.norm h.term) depth s
+      (** The stack contains [Zupdate] marks only if in sharing mode *)
+        strip_rec rstk (update ~share:true m h.norm h.term) depth s
     | stk -> (depth,List.rev rstk, stk) in
   strip_rec [] head 0 stk
 
@@ -727,7 +748,8 @@ let get_nth_arg head n stk =
             List.rev (if Int.equal n 0 then rstk else (Zapp bef :: rstk)) in
           (Some (stk', args.(n)), append_stack aft s')
     | Zupdate(m)::s ->
-        strip_rec rstk (update m h.norm h.term) n s
+        (** The stack contains [Zupdate] mark only if in sharing mode *)
+        strip_rec rstk (update ~share:true m h.norm h.term) n s
     | s -> (None, List.rev rstk @ s) in
   strip_rec [] head n stk
 
@@ -736,7 +758,8 @@ let get_nth_arg head n stk =
 let rec get_args n tys f e stk =
   match stk with
       Zupdate r :: s ->
-        let _hd = update r Cstr (FLambda(n,tys,f,e)) in
+        (** The stack contains [Zupdate] mark only if in sharing mode *)
+        let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in
         get_args n tys f e s
     | Zshift k :: s ->
         get_args n tys f (subs_shft (k,e)) s
@@ -804,21 +827,26 @@ let drop_parameters depth n argstk =
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
+  let open Declarations in
   let mib = lookup_mind (fst ind) env in
-    match mib.Declarations.mind_record with
-    | Some (Some (_,projs,pbs)) when
-        mib.Declarations.mind_finite == Declarations.BiFinite ->
-	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+  (* disallow eta-exp for non-primitive records *)
+  if not (mib.mind_finite == BiFinite) then raise Not_found;
+  match Declareops.inductive_make_projections ind mib with
+  | Some projs ->
+    (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-      let pars = mib.Declarations.mind_nparams in
-      let right = fapp_stack (f, s') in
-      let (depth, args, s) = strip_update_shift_app m s in
-      (** Try to drop the params, might fail on partially applied constructors. *)
-      let argss = try_drop_parameters depth pars args in
-      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (Projection.make p true, right) }) projs in
-	argss, [Zapp hstack]
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+    let pars = mib.Declarations.mind_nparams in
+    let right = fapp_stack (f, s') in
+    let (depth, args, s) = strip_update_shift_app m s in
+    (** Try to drop the params, might fail on partially applied constructors. *)
+    let argss = try_drop_parameters depth pars args in
+    let hstack = Array.map (fun p ->
+        { norm = Red; (* right can't be a constructor though *)
+          term = FProj (Projection.make p true, right) })
+        projs
+    in
+    argss, [Zapp hstack]
+  | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
@@ -857,9 +885,7 @@ let contract_fix_vect fix =
 let unfold_projection info p =
   if red_projection info.i_flags p
   then
-    let open Declarations in
-    let pb = lookup_projection p (info_env info) in
-    Some (Zproj (pb.proj_npars, pb.proj_arg, Projection.constant p))
+    Some (Zproj (Projection.repr p))
   else None
 
 (*********************************************************************)
@@ -870,10 +896,10 @@ let unfold_projection info p =
 let rec knh info m stk =
   match m.term with
     | FLIFT(k,a) -> knh info a (zshift k stk)
-    | FCLOS(t,e) -> knht info e t (zupdate m stk)
+    | FCLOS(t,e) -> knht info e t (zupdate info m stk)
     | FLOCKED -> assert false
-    | FApp(a,b) -> knh info a (append_stack b (zupdate m stk))
-    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate m stk)
+    | FApp(a,b) -> knh info a (append_stack b (zupdate info m stk))
+    | FCaseT(ci,p,t,br,e) -> knh info t (ZcaseT(ci,p,br,e)::zupdate info m stk)
     | FFix(((ri,n),(_,_,_)),_) ->
         (match get_nth_arg m ri.(n) stk with
              (Some(pars,arg),stk') -> knh info arg (Zfix(m,pars)::stk')
@@ -882,7 +908,7 @@ let rec knh info m stk =
     | FProj (p,c) ->
       (match unfold_projection info p with
        | None -> (m, stk)
-       | Some s -> knh info c (s :: zupdate m stk))
+       | Some s -> knh info c (s :: zupdate info m stk))
 
 (* cases where knh stops *)
     | (FFlex _|FLetIn _|FConstruct _|FEvar _|
@@ -940,9 +966,9 @@ let rec knr info tab m stk =
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info tab fxe fxbd stk'
-	| (depth, args, Zproj (n, m, cst)::s) when use_match ->
-	    let rargs = drop_parameters depth n args in
-	    let rarg = project_nth_arg m rargs in
+        | (depth, args, Zproj p::s) when use_match ->
+            let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+            let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
             kni info tab rarg s
         | (_,args,s) -> (m,args@s))
      else (m,stk)
@@ -984,7 +1010,7 @@ let rec zip_term zfun m stk =
         let t = mkCase(ci, zfun (mk_clos e p), m,
 		       Array.map (fun b -> zfun (mk_clos e b)) br) in
         zip_term zfun t s
-    | Zproj(_,_,p)::s ->
+    | Zproj p::s ->
         let t = mkProj (Projection.make p true, m) in
 	zip_term zfun t s
     | Zfix(fx,par)::s ->
@@ -1000,10 +1026,11 @@ let rec zip_term zfun m stk =
    2- tries to rebuild the term. If a closure still has to be computed,
       calls itself recursively. *)
 let rec kl info tab m =
+  let share = info.i_cache.i_share in
   if is_val m then (incr prune; term_of_fconstr m)
   else
     let (nm,s) = kni info tab m [] in
-    let () = if !share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
+    let () = if share then ignore (fapp_stack (nm, s)) in (* to unlock Zupdates! *)
     zip_term (kl info tab) (norm_head info tab nm) s
 
 (* no redex: go up for atoms and already normalized terms, go down
@@ -1024,14 +1051,14 @@ and norm_head info tab m =
       | FProd(na,dom,rng) ->
           mkProd(na, kl info tab dom, kl info tab rng)
       | FCoFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkCoFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FFix((n,(na,tys,bds)),e) ->
-          let ftys = CArray.Fun1.map mk_clos e tys in
+          let ftys = Array.Fun1.map mk_clos e tys in
           let fbds =
-            CArray.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
+            Array.Fun1.map mk_clos (subs_liftn (Array.length na) e) bds in
           mkFix(n,(na, CArray.map (kl info tab) ftys, CArray.map (kl info tab) fbds))
       | FEvar((i,args),env) ->
           mkEvar(i, Array.map (fun a -> kl info tab (mk_clos env a)) args)
@@ -1052,16 +1079,22 @@ let norm_val info tab v =
 
 let inject c = mk_clos (subs_id 0) c
 
-let whd_stack infos tab m stk =
+let whd_stack infos tab m stk = match m.norm with
+| Whnf | Norm ->
+  (** No need to perform [kni] nor to unlock updates because
+      every head subterm of [m] is [Whnf] or [Norm] *)
+  knh infos m stk
+| Red | Cstr ->
   let k = kni infos tab m stk in
-  let () = if !share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
+  let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *)
   k
 
 (* cache of constants: the body is computed only when needed. *)
 type clos_infos = fconstr infos
 
 let create_clos_infos ?(evars=fun _ -> None) flgs env =
-  create (fun _ _ c -> inject c) flgs env evars
+  let share = (Environ.typing_flags env).Declarations.share_reduction in
+  create ~share ~repr:(fun _ _ c -> inject c) flgs env evars
 
 let create_tab () = KeyTable.create 17