1 files changed, 103 insertions, 69 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 6ce14c853d..eeb9c421a1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -20,7 +20,9 @@ open Declarations
 open Environ
 open Entries
 open Typeops
-open Fast_typeops
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 
 (* Insertion of constants and parameters in environment. *)
 
@@ -85,58 +87,92 @@ let concat_seff = SideEffects.concat
 let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff
 
 let inline_side_effects env body ctx side_eff =
-  let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
+  (** First step: remove the constants that are still in the environment *)
+  let filter { eff = se; from_env = mb } =
     let cbl = match se with
-      | SEsubproof (c,cb,b) -> [c,cb,b]
-      | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
+    | SEsubproof (c, cb, b) -> [c, cb, b]
+    | SEscheme (cl,_) ->
+      List.map (fun (_, c, cb, b) -> c, cb, b) cl
+    in
     let not_exists (c,_,_) =
       try ignore(Environ.lookup_constant c env); false
       with Not_found -> true in 
     let cbl = List.filter not_exists cbl in
-    let cname c = 
-      let name = string_of_con c in
-      for i = 0 to String.length name - 1 do
-        if name.[i] == '.' || name.[i] == '#' then name.[i] <- '_' done;
-      Name (id_of_string name) in
-    let rec sub c i x = match kind_of_term x with
-      | Const (c', _) when eq_constant c c' -> mkRel i
-      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
-    let rec sub_body c u b i x = match kind_of_term x with
-      | Const (c',u') when eq_constant c c' -> 
-	Vars.subst_instance_constr u' b
-      | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
-    let fix_body (c,cb,b) (t,ctx) =
-      match cb.const_body, b with
-      | Def b, _ ->
-          let b = Mod_subst.force_constr b in
-	  let poly = cb.const_polymorphic in
-	    if not poly then
-              let b_ty = Typeops.type_of_constant_type env cb.const_type in
-              let t = sub c 1 (Vars.lift 1 t) in
-	        mkLetIn (cname c, b, b_ty, t),
-		Univ.ContextSet.union ctx
-		  (Univ.ContextSet.of_context cb.const_universes)
-	    else 
-	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
-      | OpaqueDef _, `Opaque (b,_) -> 
-	  let poly = cb.const_polymorphic in
-	    if not poly then
-              let b_ty = Typeops.type_of_constant_type env cb.const_type in
-              let t = sub c 1 (Vars.lift 1 t) in
-	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
-		Univ.ContextSet.union ctx
-		  (Univ.ContextSet.of_context cb.const_universes)
-	    else
-	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
+    (cbl, mb)
+  in
+  (* CAVEAT: we assure that most recent effects come first *)
+  let side_eff = List.map filter (uniq_seff_rev side_eff) in
+  let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
+  let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+  let side_eff = List.rev side_eff in
+  (** Most recent side-effects first in side_eff *)
+  if List.is_empty side_eff then (body, ctx, sigs)
+  else
+    (** Second step: compute the lifts and substitutions to apply *)
+    let cname c =
+      let name = Constant.to_string c in
+      let map c = if c == '.' || c == '#' then '_' else c in
+      let name = String.map map name in
+      Name (Id.of_string name)
+    in
+    let fold (subst, var, ctx, args) (c, cb, b) =
+      let (b, opaque) = match cb.const_body, b with
+      | Def b, _ -> (Mod_subst.force_constr b, false)
+      | OpaqueDef _, `Opaque (b,_) -> (b, true)
       | _ -> assert false
+      in
+      if cb.const_polymorphic then
+        (** Inline the term to emulate universe polymorphism *)
+        let data = (Univ.UContext.instance cb.const_universes, b) in
+        let subst = Cmap_env.add c (Inl data) subst in
+        (subst, var, ctx, args)
+      else
+        (** Abstract over the term at the top of the proof *)
+        let ty = Typeops.type_of_constant_type env cb.const_type in
+        let subst = Cmap_env.add c (Inr var) subst in
+        let univs = Univ.ContextSet.of_context cb.const_universes in
+        let ctx = Univ.ContextSet.union ctx univs in
+        (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
     in
-    let t, ctx = List.fold_right fix_body cbl (t,ctx) in
-    t, ctx, (mb,List.length cbl) :: sl
-  in
-  (* CAVEAT: we assure a proper order *)
-  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff_rev side_eff)
+    let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
+    (** Third step: inline the definitions *)
+    let rec subst_const i k t = match Constr.kind t with
+    | Const (c, u) ->
+      let data = try Some (Cmap_env.find c subst) with Not_found -> None in
+      begin match data with
+      | None -> t
+      | Some (Inl (inst, b)) ->
+        (** [b] is closed but may refer to other constants *)
+        subst_const i k (Vars.subst_instance_constr u b)
+      | Some (Inr n) ->
+        mkRel (k + n - i)
+      end
+    | Rel n ->
+      (** Lift free rel variables *)
+      if n <= k then t
+      else mkRel (n + len - i - 1)
+    | _ -> map_constr_with_binders ((+) 1) (fun k t -> subst_const i k t) k t
+    in
+    let map_args i (na, b, ty, opaque) =
+      (** Both the type and the body may mention other constants *)
+      let ty = subst_const (len - i - 1) 0 ty in
+      let b = subst_const (len - i - 1) 0 b in
+      (na, b, ty, opaque)
+    in
+    let args = List.mapi map_args args in
+    let body = subst_const 0 0 body in
+    let fold_arg (na, b, ty, opaque) accu =
+      if opaque then mkApp (mkLambda (na, ty, accu), [|b|])
+      else mkLetIn (na, b, ty, accu)
+    in
+    let body = List.fold_right fold_arg args body in
+    (body, ctx, sigs)
+
+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 *)
@@ -150,7 +186,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
@@ -184,13 +220,10 @@ 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 ->
-      feedback ~id:(State state_id) Feedback.Complete)
+      feedback ~id:state_id Feedback.Complete)
 
 let infer_declaration ~trust env kn dcl =
   match dcl with
@@ -214,7 +247,7 @@ let infer_declaration ~trust env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+        Future.chain ~pure:true body (fun ((body,uctx),side_eff) ->
           let body, uctx, signatures =
             inline_side_effects env body uctx side_eff in
           let valid_signatures = check_signatures trust signatures in
@@ -223,13 +256,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,
@@ -286,18 +319,17 @@ let global_vars_set_constant_type env = function
   | RegularArity t -> global_vars_set env t
   | TemplateArity (ctx,_) ->
       Context.Rel.fold_outside
-        (Context.Rel.Declaration.fold
+        (RelDecl.fold_constr
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
 let record_aux env s_ty s_bo suggested_expr =
-  let open Context.Named.Declaration in
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
       (CList.map_filter (fun decl ->
-          let id = get_id decl in
-          if List.exists (Id.equal id % get_id) in_ty then None
+          let id = NamedDecl.get_id decl in
+          if List.exists (NamedDecl.get_id %> Id.equal id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -306,26 +338,25 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
-  let open Context.Named.Declaration in
   let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
+    let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
       let n = List.length l in
-      errorlabstrm "" (Pp.(str "The following section " ++
+      user_err  (Pp.(str "The following section " ++
         str (String.plural n "variable") ++
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
   let sort evn l =
     List.filter (fun decl ->
-      let id = get_id decl in
-      List.exists (Names.Id.equal id % get_id) l)
+      let id = NamedDecl.get_id decl in
+      List.exists (NamedDecl.get_id %> Names.Id.equal id) l)
     (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
-    let context_ids = List.map get_id (named_context env) in
+    let context_ids = List.map NamedDecl.get_id (named_context env) in
     match ctx with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
@@ -453,7 +484,7 @@ let export_side_effects mb env ce =
       let { const_entry_body = body } = c in
       let _, eff = Future.force body in
       let ce = DefinitionEntry { c with
-        const_entry_body = Future.chain ~greedy:true ~pure:true body
+        const_entry_body = Future.chain ~pure:true body
           (fun (b_ctx, _) -> b_ctx, empty_seff) } in
       let not_exists (c,_,_,_) =
         try ignore(Environ.lookup_constant c env); false
@@ -508,7 +539,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 =
@@ -519,8 +554,7 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let open Context.Named.Declaration in
-       let context_ids = List.map get_id (named_context env) in
+       let context_ids = List.map NamedDecl.get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
@@ -536,7 +570,7 @@ let translate_local_def mb env id centry =
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
 let inline_entry_side_effects env ce = { ce with
-  const_entry_body = Future.chain ~greedy:true ~pure:true
+  const_entry_body = Future.chain ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
       let body, ctx',_ = inline_side_effects env body ctx side_eff in
       (body, ctx'), empty_seff);