1 files changed, 128 insertions, 133 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c..5968fbf3 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -27,22 +27,22 @@ open Decls
 open Decl_kinds
 
 (** flag for internal message display *)
-type internal_flag = 
-  | KernelVerbose (* kernel action, a message is displayed *)
-  | KernelSilent  (* kernel action, no message is displayed *)
-  | UserVerbose   (* user action, a message is displayed *)
+type internal_flag =
+  | UserAutomaticRequest (* kernel action, a message is displayed *)
+  | InternalTacticRequest  (* kernel action, no message is displayed *)
+  | UserIndividualRequest   (* user action, a message is displayed *)
 
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
-  | Inl ctx -> Global.push_context_set ctx
+  | Inl ctx -> Global.push_context_set false ctx
   | Inr (id,(p,d,mk)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
@@ -50,20 +50,20 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty),ctx) in
+      let () = Global.push_named_assum ((id,ty,poly),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def (id,de) in
-        Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
-	(Univ.ContextSet.of_context de.const_entry_universes) in
+      let univs = Global.push_named_def (id,de) in
+      Explicit, de.const_entry_opaque,
+      de.const_entry_polymorphic, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable id impl poly ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
   add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
-  | Inr (id,_) -> 
+  | Inr (id,_) ->
     if variable_polymorphic id then None
     else Some (Inl (variable_context id))
   | Inl _ -> Some o
@@ -93,9 +93,13 @@ type constant_obj = {
   cst_hyps : Dischargedhypsmap.discharged_hyps;
   cst_kind : logical_kind;
   cst_locl : bool;
+  mutable cst_exported : Safe_typing.exported_private_constant list;
+  (* mutable: to avoid change the libobject API, since cache_function
+   * does not return an updated object *)
+  mutable cst_was_seff : bool
 }
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -116,8 +120,9 @@ let open_constant i ((sp,kn), obj) =
     match (Global.lookup_constant con).const_body with
     | (Def _ | Undef _) -> ()
     | OpaqueDef lc ->
-        match Opaqueproof.get_constraints (Global.opaque_tables ())lc with
-        | Some f when Future.is_val f -> Global.push_context_set (Future.force f)
+        match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with
+        | Some f when Future.is_val f ->
+	   Global.push_context_set false (Future.force f)
         | _ -> ()
 
 let exists_name id =
@@ -130,8 +135,17 @@ let check_exists sp =
 let cache_constant ((sp,kn), obj) =
   let id = basename sp in
   let _,dir,_ = repr_kn kn in
-  let () = check_exists sp in
-  let kn' = Global.add_constant dir id obj.cst_decl in
+  let kn' =
+    if obj.cst_was_seff then begin
+      obj.cst_was_seff <- false;  
+      if Global.exists_objlabel (Label.of_id (basename sp))
+      then constant_of_kn kn
+      else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp))
+    end else
+      let () = check_exists sp in
+      let kn', exported = Global.add_constant dir id obj.cst_decl in
+      obj.cst_exported <- exported;
+      kn' in
   assert (eq_constant kn' (constant_of_kn kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   let cst = Global.lookup_constant kn' in
@@ -156,19 +170,22 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+  ConstantEntry
+    (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
   cst_hyps = [];
   cst_kind = cst.cst_kind;
   cst_locl = cst.cst_locl;
+  cst_exported = [];
+  cst_was_seff = cst.cst_was_seff;
 }
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let inConstant : constant_obj -> obj =
-  declare_object { (default_object "CONSTANT") with
+let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -176,17 +193,41 @@ let inConstant : constant_obj -> obj =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let declare_scheme = ref (fun _ _ -> assert false)
+let set_declare_scheme f = declare_scheme := f
+
 let declare_constant_common id cst =
-  let (sp,kn) = add_leaf id (inConstant cst) in
+  let update_tables c =
+(*  Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
+    declare_constant_implicits c;
+    Heads.declare_head (EvalConstRef c);
+    Notation.declare_ref_arguments_scope (ConstRef c) in
+  let o = inConstant cst in
+  let _, kn as oname = add_leaf id o in
+  List.iter (fun (c,ce,role) ->
+      (* handling of private_constants just exported *)
+      let o = inConstant {
+        cst_decl = ConstantEntry (false, ce);
+        cst_hyps = [] ;
+        cst_kind = IsProof Theorem;
+        cst_locl = false;
+        cst_exported = [];
+        cst_was_seff = true; } in
+      let id = Label.to_id (pi3 (Constant.repr3 c)) in
+      ignore(add_leaf id o);
+      update_tables c;
+      match role with
+      | Safe_typing.Subproof -> ()
+      | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|])
+    (outConstant o).cst_exported;
+  pull_to_head oname;
   let c = Global.constant_of_delta_kn kn in
-  declare_constant_implicits c;
-  Heads.declare_head (EvalConstRef c);
-  Notation.declare_ref_arguments_scope (ConstRef c);
+  update_tables c;
   c
 
-let definition_entry ?(opaque=false) ?(inline=false) ?types 
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Declareops.no_seff) body =
-  { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
+    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
+  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_polymorphic = poly;
@@ -195,98 +236,33 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
     const_entry_feedback = None;
     const_entry_inline_code = inline}
 
-let declare_scheme = ref (fun _ _ -> assert false)
-let set_declare_scheme f = declare_scheme := f
-let declare_sideff env fix_exn se =
-  let cbl, scheme = match se with
-    | SEsubproof (c, cb, pt) -> [c, cb, pt], None
-    | SEscheme (cbl, k) ->
-        List.map (fun (_,c,cb,pt) -> c,cb,pt) cbl, Some (cbl,k) in
-  let id_of c = Names.Label.to_id (Names.Constant.label c) in
-  let pt_opaque_of cb pt =
-    match cb, pt with
-    | { const_body = Def sc }, _ -> (Mod_subst.force_constr sc, Univ.ContextSet.empty), false
-    | { const_body = OpaqueDef _ }, `Opaque(pt,univ) -> (pt, univ), true
-    | _ -> assert false
-  in
-  let ty_of cb =
-    match cb.Declarations.const_type with
-    | Declarations.RegularArity t -> Some t 
-    | Declarations.TemplateArity _ -> None in
-  let cst_of cb pt =
-    let pt, opaque = pt_opaque_of cb pt in
-    let univs, subst = 
-      if cb.const_polymorphic then
-	let univs = Univ.instantiate_univ_context cb.const_universes in
-	  univs, Vars.subst_instance_constr (Univ.UContext.instance univs)
-      else cb.const_universes, fun x -> x
-    in
-    let pt = (subst (fst pt), snd pt) in
-    let ty = Option.map subst (ty_of cb) in
-    { cst_decl = ConstantEntry (DefinitionEntry {
-        const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
-        const_entry_secctx = Some cb.Declarations.const_hyps;
-        const_entry_type = ty;
-        const_entry_opaque = opaque;
-        const_entry_inline_code = false;
-        const_entry_feedback = None;
-	const_entry_polymorphic = cb.const_polymorphic;
-	const_entry_universes = univs;
-    });
-    cst_hyps = [] ;
-    cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
-    cst_locl = true;
-  } in
-  let exists c =
-    try ignore(Environ.lookup_constant c env); true
-    with Not_found -> false in 
-  let knl =
-    CList.map_filter (fun (c,cb,pt) ->
-      if exists c then None
-      else Some (c,declare_constant_common (id_of c) (cst_of cb pt))) cbl in
-  match scheme with
-  | None -> ()
-  | Some (inds_consts,kind) ->
-      !declare_scheme kind (Array.of_list
-         (List.map (fun (c,kn) ->
-             CList.find_map (fun (x,c',_,_) ->
-               if Constant.equal c c' then Some (x,kn) else None) inds_consts)
-           knl))
-
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
-  let cd = (* We deal with side effects *)
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+  let export = (* We deal with side effects *)
     match cd with
-    | Entries.DefinitionEntry de ->
-        if export_seff ||
-           not de.const_entry_opaque ||
-           de.const_entry_polymorphic then
+    | DefinitionEntry de when
+        export_seff ||
+        not de.const_entry_opaque ||
+        de.const_entry_polymorphic ->
           let bo = de.const_entry_body in
           let _, seff = Future.force bo in
-          if Declareops.side_effects_is_empty seff then cd
-          else begin
-            let seff = Declareops.uniquize_side_effects seff in
-            Declareops.iter_side_effects
-              (declare_sideff (Global.env ()) (Future.fix_exn_of bo)) seff;
-            Entries.DefinitionEntry { de with
-              const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
-                pt, Declareops.no_seff) }
-        end
-        else cd
-    | _ -> cd
+          Safe_typing.empty_private_constants <> seff
+    | _ -> false
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (export,cd);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
+    cst_exported = [];
+    cst_was_seff = false;
   } in
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
-  let cb = 
+  let cb =
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
     declare_constant ~internal ~local id
@@ -382,12 +358,12 @@ let inInductive : inductive_obj -> obj =
 let declare_projections mind =
   let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in
     match spec.mind_record with
-    | Some (Some (_, kns, pjs)) -> 
-      Array.iteri (fun i kn -> 
+    | Some (Some (_, kns, pjs)) ->
+      Array.iteri (fun i kn ->
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
 	let kn' = declare_constant id (ProjectionEntry entry,
-				       IsDefinition StructureComponent) 
+				       IsDefinition StructureComponent)
 	in
 	  assert(eq_constant kn kn')) kns; true
     | Some None | None -> false
@@ -441,50 +417,69 @@ let assumption_message id =
 
 (** Global universe names, in a different summary *)
 
-type universe_names = 
+type universe_names =
     (Univ.universe_level Idmap.t * Id.t Univ.LMap.t)
 
-let input_universes : universe_names -> Libobject.obj =
-  let open Libobject in 
-    declare_object
+(* Discharged or not *)
+type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
+
+let cache_universes (p, l) =
+  let glob = Universes.global_universe_names () in
+  let glob', ctx =
+    List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
+		    ((Idmap.add id lev idl, Univ.LMap.add lev id lid),
+		     Univ.ContextSet.add_universe lev ctx))
+      (glob, Univ.ContextSet.empty) l
+  in
+    Global.push_context_set false ctx;
+    if p then Lib.add_section_context ctx;
+    Universes.set_global_universe_names glob'
+
+let input_universes : universe_decl -> Libobject.obj =
+  declare_object
     { (default_object "Global universe name state") with
-      cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi);
-      load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi);
-      discharge_function = (fun (_, a) -> Some a);
+      cache_function = (fun (na, pi) -> cache_universes pi);
+      load_function = (fun _ (_, pi) -> cache_universes pi);
+      discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
       classify_function = (fun a -> Keep a) }
 
-let do_universe l =
-  let glob = Universes.global_universe_names () in
-  let glob' = 
-    List.fold_left (fun (idl,lid) (l, id) ->
-      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
-	(Idmap.add id lev idl, Univ.LMap.add lev id lid))
-      glob l
+let do_universe poly l =
+  let l =
+    List.map (fun (l, id) ->
+	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
+	      (id, lev)) l
   in
-    Lib.add_anonymous_leaf (input_universes glob')
+    Lib.add_anonymous_leaf (input_universes (poly, l))
+
+type constraint_decl = polymorphic * Univ.constraints
+
+let cache_constraints (na, (p, c)) =
+  Global.add_constraints c;
+  if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
 
+let discharge_constraints (_, (p, c as a)) =
+  if p then None else Some a
 
-let input_constraints : Univ.constraints -> Libobject.obj =
-  let open Libobject in 
+let input_constraints : constraint_decl -> Libobject.obj =
+  let open Libobject in
     declare_object
     { (default_object "Global universe constraints") with
-      cache_function = (fun (na, c) -> Global.add_constraints c);
-      load_function = (fun _ (_, c) -> Global.add_constraints c);
-      discharge_function = (fun (_, a) -> Some a);
+      cache_function = cache_constraints;
+      load_function = (fun _ -> cache_constraints);
+      discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
-let do_constraint l = 
-  let u_of_id = 
+let do_constraint poly l =
+  let u_of_id =
     let names, _ = Universes.global_universe_names () in
-      fun (loc, id) -> 
+      fun (loc, id) ->
 	try Idmap.find id names
 	with Not_found ->
-	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)	    
+	  user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
     let lu = u_of_id l and ru = u_of_id r in
       Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
-    Lib.add_anonymous_leaf (input_constraints constraints)
-  
+    Lib.add_anonymous_leaf (input_constraints (poly, constraints))