diff options
43 files changed, 547 insertions, 312 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7def963e7..dc5c17a75 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -79,12 +79,6 @@ type constant_body = { const_proj : projection_body option; const_inline_code : bool } -type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] - -type side_effect = - | SEsubproof of constant * constant_body * seff_env - | SEscheme of (inductive * constant * constant_body * seff_env) list * string - (** {6 Representation of mutual inductive types in the kernel } *) type recarg = diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c1..248504c1b 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -304,17 +304,7 @@ let hcons_mind mib = (** {6 Stm machinery } *) -let string_of_side_effect = function - | SEsubproof (c,_,_) -> Names.string_of_con c - | SEscheme (cl,_) -> - String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) -type side_effects = side_effect list -let no_seff = ([] : side_effects) -let iter_side_effects f l = List.iter f (List.rev l) -let fold_side_effects f a l = List.fold_left f a l -let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l)) -let union_side_effects l1 l2 = l1 @ l2 -let flatten_side_effects l = List.flatten l -let side_effects_of_list l = l -let cons_side_effects x l = x :: l -let side_effects_is_empty = List.is_empty +let string_of_side_effect { Entries.eff } = match eff with + | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")" + | Entries.SEscheme (cl,_) -> + "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")" diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ce65af975..1b8700958 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -9,6 +9,7 @@ open Declarations open Mod_subst open Univ +open Entries (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool val string_of_side_effect : side_effect -> string -type side_effects -val no_seff : side_effects -val iter_side_effects : (side_effect -> unit) -> side_effects -> unit -val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a -val uniquize_side_effects : side_effects -> side_effects -val union_side_effects : side_effects -> side_effects -> side_effects -val flatten_side_effects : side_effects list -> side_effects -val side_effects_of_list : side_effect list -> side_effects -val cons_side_effects : side_effect -> side_effects -> side_effects -val side_effects_is_empty : side_effects -> bool - (** {6 Inductive types} *) val eq_recarg : recarg -> recarg -> bool diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d35..e058519e9 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -54,11 +54,11 @@ type mutual_inductive_entry = { mind_entry_private : bool option } (** {6 Constants (Definition/Axiom) } *) -type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects -type const_entry_body = proof_output Future.computation +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation -type definition_entry = { - const_entry_body : const_entry_body; +type 'a definition_entry = { + const_entry_body : 'a const_entry_body; (* List of section variables *) const_entry_secctx : Context.section_context option; (* State id on which the completion of type checking is reported *) @@ -78,8 +78,8 @@ type projection_entry = { proj_entry_ind : mutual_inductive; proj_entry_arg : int } -type constant_entry = - | DefinitionEntry of definition_entry +type 'a constant_entry = + | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry @@ -96,3 +96,16 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option + +type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] + +type side_eff = + | SEsubproof of constant * Declarations.constant_body * seff_env + | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string + +type side_effect = { + from_env : Declarations.structure_body Ephemeron.key; + eff : side_eff; +} + +type side_effects = side_effect list diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 9f4361f40..badb15b56 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f) let create cu = Direct ([],cu) let turn_indirect dp o (prfs,odp) = match o with - | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque") + | Indirect (_,_,i) -> + if not (Int.Map.mem i prfs) + then Errors.anomaly (Pp.str "Indirect in a different table") + else Errors.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 diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ec245b064..b71cd31b5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -207,15 +207,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -let sideff_of_con env c = +type private_constant = Entries.side_effect +type private_constants = private_constant list + +type private_constant_role = Term_typing.side_effect_role = + | Subproof + | Schema of inductive * string + +let empty_private_constants = [] +let add_private x xs = x :: xs +let concat_private xs ys = xs @ ys +let mk_pure_proof = Term_typing.mk_pure_proof +let inline_private_constants_in_constr = Term_typing.handle_side_effects +let inline_private_constants_in_definition_entry = Term_typing.handle_entry_side_effects +let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) + +let constant_entry_of_private_constant = function + | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } -> + [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ] + | { Entries.eff = Entries.SEscheme (l,_) } -> + List.map (fun (_,kn,cb,eff_env) -> + kn, Term_typing.constant_entry_of_side_effect cb eff_env) l + +let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in - SEsubproof (c, cbo, get_opaque_body env.env cbo) -let sideff_of_scheme kind env cl = - SEscheme( - List.map (fun (i,c) -> - let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opaque_body env.env cbo) cl, - kind) + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) } + +let private_con_of_scheme ~kind env cl = + { Entries.from_env = Ephemeron.create env.revstruct; + Entries.eff = Entries.SEscheme( + List.map (fun (i,c) -> + let cbo = Environ.lookup_constant c env.env in + i, c, cbo, get_opaque_body env.env cbo) cl, + kind) } + +let universes_of_private eff = + let open Declarations in + List.fold_left (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc in + if cb.const_polymorphic then acc + else (Univ.ContextSet.of_context cb.const_universes) :: acc) + acc l + | Entries.SEsubproof _ -> acc) + [] eff let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -337,7 +377,7 @@ let safe_push_named (id,_,_ as d) env = let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in + let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -442,19 +482,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe -let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in - let cb = match decl with - | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe senv.env kn r in - if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb - in +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +let add_constant_aux no_section senv (kn, cb) = + let l = pi3 (Constant.repr3 kn) in let cb, otab = match cb.const_body with - | OpaqueDef lc when DirPath.is_empty dir -> + | OpaqueDef lc when no_section -> (* In coqc, opaque constants outside sections will be stored indirectly in a specific table *) let od, otab = @@ -471,7 +508,33 @@ let add_constant dir l decl senv = (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' | _ -> senv' in - kn, senv'' + senv'' + +let add_constant dir l decl senv = + let kn = make_con senv.modpath dir l in + let no_section = DirPath.is_empty dir in + let seff_to_export, decl = + match decl with + | ConstantEntry (true, ce) -> + let exports, ce = + Term_typing.validate_side_effects_for_export + senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce) + | _ -> [], decl + in + let senv = + List.fold_left (add_constant_aux no_section) senv + (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in + let senv = + let cb = + match decl with + | ConstantEntry (export_seff,ce) -> + Term_typing.translate_constant senv.revstruct senv.env kn ce + | GlobalRecipe r -> + let cb = Term_typing.translate_recipe senv.env kn r in + if no_section then Declareops.hcons_const_body cb else cb in + add_constant_aux no_section senv (kn, cb) in + (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index eac08eb83..2214cf8bb 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment (** {6 Stm machinery } *) -val sideff_of_con : safe_environment -> constant -> Declarations.side_effect -val sideff_of_scheme : - string -> safe_environment -> (inductive * constant) list -> - Declarations.side_effect +type private_constant +type private_constants + +type private_constant_role = + | Subproof + | Schema of inductive * string + +val side_effects_of_private_constants : + private_constants -> Entries.side_effects + +val empty_private_constants : private_constants +val add_private : private_constant -> private_constants -> private_constants +val concat_private : private_constants -> private_constants -> private_constants + +val private_con_of_con : safe_environment -> constant -> private_constant +val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant + +val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output +val inline_private_constants_in_constr : + Environ.env -> Constr.constr -> private_constants -> Constr.constr +val inline_private_constants_in_definition_entry : + Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + +val universes_of_private : private_constants -> Univ.universe_context_set list val is_curmod_library : safe_environment -> bool @@ -63,16 +83,23 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer + Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + (* bool: export private constants *) + | ConstantEntry of bool * private_constants Entries.constant_entry | GlobalRecipe of Cooking.recipe +type exported_private_constant = + constant * private_constants Entries.constant_entry * private_constant_role + +(** returns the main constant plus a list of auxiliary constants (empty + unless one requires the side effects to be exported) *) val add_constant : - DirPath.t -> Label.t -> global_declaration -> constant safe_transformer + DirPath.t -> Label.t -> global_declaration -> + (constant * exported_private_constant list) safe_transformer (** Adding an inductive type *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cab99077f..d75bd73fb 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x (* Insertion of constants and parameters in environment. *) -let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff +let mk_pure_proof c = (c, Univ.ContextSet.empty), [] + +let equal_eff e1 e2 = + let open Entries in + match e1, e2 with + | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } -> + Names.Constant.equal c1 c2 + | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } -> + CList.for_all2eq + (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2) + cl1 cl2 + | _ -> false + +let rec uniq_seff = function + | [] -> [] + | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs) +(* The list of side effects is in reverse order (most recent first). + * To keep the "tological" order between effects we have to uniqize from the + * tail *) +let uniq_seff l = List.rev (uniq_seff (List.rev l)) let handle_side_effects env body ctx side_eff = - let handle_sideff (t,ctx) se = + let handle_sideff (t,ctx,sl) { 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 @@ -65,7 +84,7 @@ let handle_side_effects env body ctx side_eff = 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) (fun i x -> sub_body c u b i x) i x in + | _ -> 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, _ -> @@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff = 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) + (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 | _ -> assert false in - List.fold_right fix_body cbl (t,ctx) + 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 *) - Declareops.fold_side_effects handle_sideff (body,ctx) - (Declareops.uniquize_side_effects side_eff) + List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff) + +let check_signatures curmb sl = + let is_direct_ancestor (sl, curmb) (mb, how_many) = + match curmb with + | None -> None, None + | Some curmb -> + try + let mb = Ephemeron.get mb in + match sl with + | None -> sl, None + | Some n -> + if List.length mb >= how_many && CList.skipn how_many mb == curmb + then Some (n + how_many), Some mb + else None, None + with Ephemeron.InvalidKey -> None, None in + let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in + sl + +let trust_seff sl b e = + let rec aux sl b e acc = + match sl, kind_of_term b with + | (None|Some 0), _ -> b, e, acc + | Some sl, LetIn (n,c,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc) + | Some sl, App(hd,arg) -> + begin match kind_of_term hd with + | Lambda (n,ty,bo) -> + aux (Some (sl-1)) bo + (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc) + | _ -> assert false + end + | _ -> assert false + in + aux sl b e [] + +let rec unzip ctx j = + match ctx with + | [] -> j + | `Let (n,c,ty) :: ctx -> + unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) } + | `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} @@ -105,7 +167,7 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration env kn dcl = +let infer_declaration ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -124,9 +186,14 @@ let infer_declaration env kn dcl = let tyj = infer_type env typ in let proofterm = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> - let body,ctx = handle_side_effects env body ctx side_eff in + let body, ctx, signatures = + handle_side_effects env body ctx side_eff in + let trusted_signatures = check_signatures trust signatures in let env' = push_context_set ctx env in - let j = infer env' body in + let j = + let body, env', zip_ctx = trust_seff trusted_signatures body env' in + let j = infer env' body in + unzip zip_ctx j in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,7 +210,7 @@ let infer_declaration env kn dcl = let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx = handle_side_effects env body + let body, ctx, _ = handle_side_effects env body (Univ.ContextSet.union univsctx ctx) side_eff in let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in @@ -294,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) (*s Global and local constant declaration. *) -let translate_constant env kn ce = - build_constant_declaration kn env (infer_declaration env (Some kn) ce) +let translate_constant mb env kn ce = + build_constant_declaration kn env + (infer_declaration ~trust:mb env (Some kn) ce) + +let constant_entry_of_side_effect cb u = + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, []); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = + (match cb.const_type with RegularArity t -> Some t | _ -> None); + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = cb.const_universes; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } +;; + +let turn_direct (kn,cb,u,r as orig) = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b,c) -> + let pt = Future.from_val (b,c) in + kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r + | _ -> orig +;; + +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +let validate_side_effects_for_export mb env ce = + match ce with + | ParameterEntry _ | ProjectionEntry _ -> [], ce + | DefinitionEntry c -> + 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 + (fun (b_ctx, _) -> b_ctx, []) } in + let not_exists (c,_,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = match se with + | SEsubproof (c,cb,b) -> [c,cb,b,Subproof] + | SEscheme (cl,k) -> + List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in + let cbl = List.filter not_exists cbl in + if cbl = [] then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in + let trusted = check_signatures mb signatures in + let push_seff env = function + | kn, cb, `Nothing, _ -> + Environ.add_constant kn cb env + | kn, cb, `Opaque(_, ctx), _ -> + let env = Environ.add_constant kn cb env in + Environ.push_context_set + ~strict:(not cb.const_polymorphic) ctx env in + let rec translate_seff sl seff acc env = + match sl, seff with + | _, [] -> List.rev acc, ce + | (None | Some 0), cbs :: rest -> + let env, cbs = + List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> + let ce = constant_entry_of_side_effect ocb u in + let cb = translate_constant mb env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + (env,[]) cbs in + translate_seff sl rest (cbs @ acc) env + | Some sl, cbs :: rest -> + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map (fun (kn,cb,u,r) -> + kn, cb, constant_entry_of_side_effect cb u, r) cbs in + translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env +;; let translate_local_assum env t = let j = infer env t in @@ -305,9 +457,9 @@ let translate_local_assum env t = let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant env r) -let translate_local_def env id centry = +let translate_local_def mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with @@ -332,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie let handle_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~greedy:true ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx' = handle_side_effects env body ctx side_eff in - (body, ctx'), Declareops.no_seff); + let body, ctx',_ = handle_side_effects env body ctx side_eff in + (body, ctx'), []); } let handle_side_effects env body side_eff = - fst (handle_side_effects env body Univ.ContextSet.empty side_eff) + pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 8d92bcc68..509160ccc 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,23 +12,42 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> proof_output +val mk_pure_proof : constr -> side_effects proof_output -val handle_side_effects : env -> constr -> Declareops.side_effects -> constr +val handle_side_effects : env -> constr -> side_effects -> constr (** Returns the term where side effects have been turned into let-ins or beta redexes. *) -val handle_entry_side_effects : env -> definition_entry -> definition_entry +val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry (** Same as {!handle_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : env -> constant -> constant_entry -> constant_body +val uniq_seff : side_effects -> side_effects + +val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> constant_body + +(* Checks weather the side effects in constant_entry can be trusted. + * Returns the list of effects to be exported. + * Note: It forces the Future.computation. *) +type side_effect_role = + | Subproof + | Schema of inductive * string + +type exported_side_effect = + constant * constant_body * side_effects Entries.constant_entry * side_effect_role + +val validate_side_effects_for_export : + structure_body -> env -> side_effects constant_entry -> + exported_side_effect list * side_effects constant_entry + +val constant_entry_of_side_effect : + constant_body -> seff_env -> side_effects constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,8 +56,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> - constant_entry -> Cooking.result +val infer_declaration : trust:structure_body -> env -> constant option -> + side_effects constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body diff --git a/library/declare.ml b/library/declare.ml index 0004f45a2..63e5a7224 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -35,7 +35,7 @@ type internal_flag = (** 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 @@ -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 *) @@ -131,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,20 +169,23 @@ let discharge_constant ((sp, kn), obj) = Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* 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)) +let dummy_constant_entry = + 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; @@ -177,16 +193,40 @@ 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 = + ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; @@ -196,90 +236,25 @@ 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 = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let cd = (* We deal with side effects *) + 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 diff --git a/library/declare.mli b/library/declare.mli index 7ed451c3f..fdbd23561 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -22,7 +22,7 @@ open Decl_kinds (** Declaration of local constructions (Variable/Hypothesis/Local) *) 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 @@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) -type constant_declaration = constant_entry * logical_kind +type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind (** [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns @@ -49,8 +49,8 @@ type internal_flag = (* Defaut definition entries, transparent with no secctx or proj information *) val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> - ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects -> - constr -> definition_entry + ?poly:polymorphic -> ?univs:Univ.universe_context -> + ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant @@ -60,7 +60,7 @@ val declare_definition : ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant -(** Since transparent constant's side effects are globally declared, we +(** Since transparent constants' side effects are globally declared, we * need that *) val set_declare_scheme : (string -> (inductive * constant) array -> unit) -> unit diff --git a/library/global.mli b/library/global.mli index ac231f7fd..03469bea4 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,10 +31,11 @@ val set_engagement : Declarations.engagement -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> Univ.universe_context_set +val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> + constant * Safe_typing.exported_private_constant list val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive diff --git a/library/heads.ml b/library/heads.ml index 5c153b067..73d2aa053 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -68,7 +68,10 @@ let kind_of_head env t = | None -> NotImmediatelyComputableHead) | Const (cst,_) -> (try on_subterm k l b (constant_head cst) - with Not_found -> assert false) + with Not_found -> + Errors.anomaly + Pp.(str "constant not found in kind_of_head: " ++ + str (Names.Constant.to_string cst))) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead | Sort _ | Ind _ | Prod _ -> RigidHead RigidType diff --git a/library/libobject.ml b/library/libobject.ml index 2ee57baf9..85c830ea2 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -108,6 +108,9 @@ let declare_object_full odecl = let declare_object odecl = try fst (declare_object_full odecl) with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) +let declare_object_full odecl = + try declare_object_full odecl + with e -> Errors.fatal_error (Errors.print e) (Errors.is_anomaly e) let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t) diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index c232ae31a..d6c29283f 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -6,8 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -let map_const_entry_body (f:Term.constr->Term.constr) (x:Entries.const_entry_body) - : Entries.const_entry_body = +let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) + : Safe_typing.private_constants Entries.const_entry_body = Future.chain ~pure:true x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 9e27ddf2e..c43932324 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) ignore( Declare.declare_constant name - (Entries.DefinitionEntry ce, + (DefinitionEntry ce, Decl_kinds.IsDefinition (Decl_kinds.Scheme)) ); Declare.definition_message name; @@ -447,7 +447,7 @@ let get_funs_constant mp dp = exception No_graph_found exception Found_type of int -let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list = +let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list = let env = Global.env () in let funs = List.map fst fas in let first_fun = List.hd funs in @@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr let sorts = Array.of_list sorts in List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types in - let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in + let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*) let (idxs,_),(_,ta,_ as decl) = destFix fix in let other_result = @@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt in {const with - Entries.const_entry_body = - (Future.from_val (Term_typing.mk_pure_proof princ_body)); - Entries.const_entry_type = Some scheme_type + const_entry_body = + (Future.from_val (Safe_typing.mk_pure_proof princ_body)); + const_entry_type = Some scheme_type } ) other_fun_princ_types @@ -620,7 +620,7 @@ let build_scheme fas = ignore (Declare.declare_constant princ_id - (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); + (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem)); Declare.definition_message princ_id ) fas diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index f6e5578d2..bc082f073 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -1,3 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + open Names open Term open Misctypes @@ -29,7 +37,7 @@ val compute_new_princ_type_from_rel : constr array -> sorts array -> exception No_graph_found val make_scheme : Evd.evar_map ref -> - (pconstant*glob_sort) list -> Entries.definition_entry list + (pconstant*glob_sort) list -> Safe_typing.private_constants Entries.definition_entry list val build_scheme : (Id.t*Libnames.reference*glob_sort) list -> unit val build_case_scheme : (Id.t*Libnames.reference*glob_sort) -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 35bd1c36d..aa47e2619 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,7 @@ let get_locality = function | Global -> false let save with_clean id const (locality,_,kind) hook = - let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in + let fix_exn = Future.fix_exn_of const.const_entry_body in let l,r = match locality with | Discharge when Lib.sections_are_opened () -> let k = Kindops.logical_kind_of_goal_kind kind in diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 10daf6e84..23f1da1ba 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -46,7 +46,7 @@ val const_of_id: Id.t -> Globnames.global_reference(* constantyes *) val jmeq : unit -> Term.constr val jmeq_refl : unit -> Term.constr -val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> +val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind -> unit Lemmas.declaration_hook Ephemeron.key -> unit (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and @@ -54,7 +54,7 @@ val save : bool -> Id.t -> Entries.definition_entry -> Decl_kinds.goal_kind -> *) val get_proof_clean : bool -> Names.Id.t * - (Entries.definition_entry * Decl_kinds.goal_kind) + (Safe_typing.private_constants Entries.definition_entry * Decl_kinds.goal_kind) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1107c2951..0593bbca8 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -579,7 +579,7 @@ type evar_map = { (** Metas *) metas : clbinding Metamap.t; (** Interactive proofs *) - effects : Declareops.side_effects; + effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be eventually turned into goals if not solved.*) principal_future_goal : Evar.t option; (** if [Some e], [e] must be @@ -768,7 +768,7 @@ let empty = { conv_pbs = []; last_mods = Evar.Set.empty; metas = Metamap.empty; - effects = Declareops.no_seff; + effects = Safe_typing.empty_private_constants; evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *) future_goals = []; principal_future_goal = None; @@ -1041,22 +1041,8 @@ let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) let emit_universe_side_effects eff u = - Declareops.fold_side_effects - (fun acc eff -> - match eff with - | Declarations.SEscheme (l,s) -> - List.fold_left - (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (s, ctx) -> merge_uctx true univ_rigid acc ctx - in if cb.Declarations.const_polymorphic then acc - else - merge_uctx true univ_rigid acc - (Univ.ContextSet.of_context cb.Declarations.const_universes)) - acc l - | Declarations.SEsubproof _ -> acc) - u eff + let uctxs = Safe_typing.universes_of_private eff in + List.fold_left (merge_uctx true univ_rigid) u uctxs let add_uctx_names s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l s names_rev) @@ -1399,11 +1385,11 @@ let e_eq_constr_univs evdref t u = (* Side effects *) let emit_side_effects eff evd = - { evd with effects = Declareops.union_side_effects eff evd.effects; + { evd with effects = Safe_typing.concat_private eff evd.effects; universes = emit_universe_side_effects eff evd.universes } let drop_side_effects evd = - { evd with effects = Declareops.no_seff; } + { evd with effects = Safe_typing.empty_private_constants; } let eval_side_effects evd = evd.effects diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 52d7d4212..9379b50b5 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -261,10 +261,10 @@ val dependent_evar_ident : existential_key -> evar_map -> Id.t (** {5 Side-effects} *) -val emit_side_effects : Declareops.side_effects -> evar_map -> evar_map +val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map (** Push a side-effect into the evar map. *) -val eval_side_effects : evar_map -> Declareops.side_effects +val eval_side_effects : evar_map -> Safe_typing.private_constants (** Return the effects contained in the evar map. *) val drop_side_effects : evar_map -> evar_map diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 00ef8ecaf..02dbd1fdc 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -150,10 +150,14 @@ let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in - let ce = if side_eff then Term_typing.handle_entry_side_effects env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun (pt, _) -> pt, Declareops.no_seff) } in + let ce = + if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce + else { ce with + const_entry_body = Future.chain ~pure:true ce.const_entry_body + (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in let (cb, ctx), se = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Declareops.side_effects_is_empty se); + assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = @@ -188,7 +192,7 @@ let refine_by_tactic env sigma ty tac = other goals that were already present during its invocation, so that those goals rely on effects that are not present anymore. Hopefully, this hack will work in most cases. *) - let ans = Term_typing.handle_side_effects env ans neff in + let ans = Safe_typing.inline_private_constants_in_constr env ans neff in ans, sigma (**********************************************************************) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index b1fba132d..fc521ea43 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -69,11 +69,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) val cook_proof : unit -> (Id.t * - (Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -152,7 +152,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a0ead42ef..809ed41c7 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -67,7 +67,7 @@ type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -315,13 +315,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = let open Universes in let body = c in let typ = - if not (keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff)) then + if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then nf t else t in let used_univs_body = Universes.universes_of_constr body in let used_univs_typ = Universes.universes_of_constr typ in - if keep_body_ucst_separate || not (Declareops.side_effects_is_empty eff) then + if keep_body_ucst_separate || + not (Safe_typing.empty_private_constants = eff) then let initunivs = Evd.evar_context_universe_context initial_euctx in let ctx = Evd.evar_universe_context_set initunivs universes in (* For vi2vo compilation proofs are computed now but we need to @@ -365,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = { id = pid; entries = entries; persistence = strength; universes = universes }, fun pr_ending -> Ephemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index fcb706cc8..f8615e849 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -58,7 +58,7 @@ type lemma_possible_guards = int list list type proof_universes = Evd.evar_universe_context type proof_object = { id : Names.Id.t; - entries : Entries.definition_entry list; + entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; (* constraints : Univ.constraints; *) @@ -97,7 +97,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 5a9e7f39f..927df33a0 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -336,7 +336,7 @@ val tclENV : Environ.env tactic (** {7 Put-like primitives} *) (** [tclEFFECTS eff] add the effects [eff] to the current state. *) -val tclEFFECTS : Declareops.side_effects -> unit tactic +val tclEFFECTS : Safe_typing.private_constants -> unit tactic (** [mark_as_unsafe] declares the current tactic is unsafe. *) val mark_as_unsafe : unit tactic diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c49ddfd8e..6c1832688 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -70,11 +70,12 @@ let adjust_guardness_conditions const = function try ignore(Environ.lookup_constant c e); true with Not_found -> false in if exists c e then e else Environ.add_constant c cb e in - let env = Declareops.fold_side_effects (fun env -> function + let env = List.fold_left (fun env { eff } -> + match eff with | SEsubproof (c, cb,_) -> add c cb env | SEscheme (l,_) -> List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) - env (Declareops.uniquize_side_effects eff) in + env (Safe_typing.side_effects_of_private_constants eff) in let indexes = search_guard Loc.ghost env possible_indexes fixdecls in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index e6a8cbe3a..8a6d93cf7 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in - (c, Evd.evar_universe_context sigma), Declareops.no_seff + (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind = let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) let ind_scheme_kind_from_type = declare_individual_scheme_object "_ind_nodep" @@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index f7d3ad5d0..b2603315d 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -193,7 +193,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Declareops.no_seff) + (c, ctx), Safe_typing.empty_private_constants) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind = [|main_body|]) else main_body)))))) - in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff + in (c, Evd.evar_universe_context_of ctx), + Safe_typing.concat_private eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -660,7 +661,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -670,7 +671,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -680,7 +681,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -694,7 +695,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -704,7 +705,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) (* End of rewriting schemes *) @@ -782,4 +783,4 @@ let build_congr env (eq,refl,ctx) ind = let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) - build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff) + build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 6bb84808a..3fe330730 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -25,7 +25,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val build_r2l_forward_rew_scheme : bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -37,7 +37,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Declareops.side_effects + constr Evd.in_evar_universe_context * Safe_typing.private_constants val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index bc711b81e..674c85af7 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl = assert false in let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, Declareops.no_seff + sigma, elim, Safe_typing.empty_private_constants else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1437b2462..0b920066f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac = (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in - let open Declareops in - let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in - let effs = cons_side_effects eff + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = add_private eff Entries.(snd (Future.force const.const_entry_body)) in let args = List.rev (instance_from_named_context sign) in let solve = diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 8ac273c84..7a89b9f54 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -179,12 +179,12 @@ let build_beq_scheme mode kn = let rec aux c = let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in match kind_of_term c with - | Rel x -> mkRel (x-nlist+ndx), Declareops.no_seff - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Declareops.no_seff + | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants | Cast (x,_,_) -> aux (applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> - if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Declareops.no_seff + if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants else begin try let eq, eff = @@ -193,9 +193,8 @@ let build_beq_scheme mode kn = let eqa, eff = let eqa, effs = List.split (List.map aux a) in Array.of_list eqa, - Declareops.union_side_effects - (Declareops.flatten_side_effects (List.rev effs)) - eff in + List.fold_left Safe_typing.concat_private eff (List.rev effs) + in let args = Array.append (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in @@ -238,7 +237,7 @@ let build_beq_scheme mode kn = let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in let ar = Array.make n (Lazy.force ff) in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.make n (Lazy.force ff) in @@ -256,7 +255,7 @@ let build_beq_scheme mode kn = (nb_cstr_args+ndx+1) cc in - eff := Declareops.union_side_effects eff' !eff; + eff := Safe_typing.concat_private eff' !eff; Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] @@ -288,7 +287,7 @@ let build_beq_scheme mode kn = let names = Array.make nb_ind Anonymous and types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet in - let eff = ref Declareops.no_seff in + let eff = ref Safe_typing.empty_private_constants in let u = Univ.Instance.empty in for i=0 to (nb_ind-1) do names.(i) <- Name (Id.of_string (rec_name i)); @@ -296,7 +295,7 @@ let build_beq_scheme mode kn = (mkArrow (mkFullInd ((kn,i),u) 1) (Lazy.force bb)); let c, eff' = make_one_eq i in cores.(i) <- c; - eff := Declareops.union_side_effects eff' !eff + eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in @@ -875,7 +874,7 @@ let compute_dec_tact ind lnamesparrec nparrec = Not_found -> Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.") end >>= fun (lbI,eff'') -> - let eff = (Declareops.union_side_effects eff'' (Declareops.union_side_effects eff' eff)) in + let eff = (Safe_typing.concat_private eff'' (Safe_typing.concat_private eff' eff)) in Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; intros_using fresh_first_intros; @@ -942,7 +941,7 @@ let make_eq_decidability mode mind = (compute_dec_goal (ind,u) lnamesparrec nparrec) (compute_dec_tact ind lnamesparrec nparrec) in - ([|ans|], ctx), Declareops.no_seff + ([|ans|], ctx), Safe_typing.empty_private_constants let eq_dec_scheme_kind = declare_mutual_scheme_object "_eq_dec" make_eq_decidability diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 805a29e39..e750f0ca2 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -187,7 +187,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro Evarutil.check_evars env Evd.empty !evars termtype; let ctx = Evd.universe_context !evars in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (Entries.ParameterEntry + (ParameterEntry (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in instance_hook k None global imps ?hook (ConstRef cst); id end diff --git a/toplevel/command.ml b/toplevel/command.ml index d75efeca1..433ef4dcc 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k imps in - Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r + Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r let _ = Obligations.declare_definition_ref := declare_definition @@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = if Flags.is_program_mode () then let env = Global.env () in let (c,ctx), sideff = Future.force ce.const_entry_body in - assert(Declareops.side_effects_is_empty sideff); + assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t @@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let ctx = Evd.universe_context ?names:pl evd in ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); @@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in let vars = Universes.universes_of_constr (List.hd fixdecls) in - let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in + let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let evd = Evd.from_ctx ctx in let evd = Evd.restrict_universe_context evd vars in diff --git a/toplevel/command.mli b/toplevel/command.mli index 94b4af9dd..a031677b4 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -26,17 +26,17 @@ val do_constraint : polymorphic -> (** {6 Hooks for Pcoq} *) -val set_declare_definition_hook : (definition_entry -> unit) -> unit -val get_declare_definition_hook : unit -> (definition_entry -> unit) +val set_declare_definition_hook : (Safe_typing.private_constants definition_entry -> unit) -> unit +val get_declare_definition_hook : unit -> (Safe_typing.private_constants definition_entry -> unit) (** {6 Definitions/Let} *) val interp_definition : lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> - constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits + constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Impargs.manual_implicits val declare_definition : Id.t -> definition_kind -> - definition_entry -> Impargs.manual_implicits -> + Safe_typing.private_constants definition_entry -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> @@ -170,4 +170,4 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 7d5d61fb8..b6da21e5a 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -20,8 +20,8 @@ open Cooking (* Discharging mutual inductive *) let detype_param = function - | (Name id,None,p) -> id, Entries.LocalAssum p - | (Name id,Some p,_) -> id, Entries.LocalDef p + | (Name id,None,p) -> id, LocalAssum p + | (Name id,Some p,_) -> id, LocalDef p | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") (* Replace diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 218c47b28..dde801a7f 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -29,9 +29,9 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants type 'a scheme_kind = string @@ -124,7 +124,9 @@ let define internal id c p univs = let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in let entry = { - const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Declareops.no_seff); + const_entry_body = + Future.from_val ((c,Univ.ContextSet.empty), + Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = None; const_entry_polymorphic = p; @@ -148,8 +150,8 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = | None -> add_suffix mib.mind_packets.(i).mind_typename suff in let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; - const, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme kind (Global.safe_env()) [ind,const]) eff + const, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -168,8 +170,8 @@ let define_mutual_scheme_base kind suff f mode names mind = let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in declare_scheme kind schemes; consts, - Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) (Array.to_list schemes)) eff @@ -181,10 +183,10 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Declareops.cons_side_effects - (Safe_typing.sideff_of_scheme + s, Safe_typing.add_private + (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind, s]) - Declareops.no_seff + Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index d0844dd94..abd951c31 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -20,9 +20,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Declareops.side_effects + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants (** Main functions to register a scheme builder *) @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Declareops.side_effects + Id.t option -> inductive -> constant * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Declareops.side_effects + (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Declareops.side_effects +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ae8ee7670..0b021254e 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -371,7 +371,7 @@ let do_mutual_induction_scheme lnamedepindsort = let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in (* let decltype = refresh_universes decltype in *) - let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref in @@ -469,7 +469,7 @@ let do_combined_scheme name schemes = schemes in let body,typ = build_combined_scheme (Global.env ()) csts in - let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Declareops.no_seff) in + let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); fixpoint_message None [snd name] diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 665926922..e488f84f8 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -541,7 +541,7 @@ let compute_possible_guardness_evidences (n,_) fixbody fixtype = let ctx = fst (decompose_prod_n_assum m fixtype) in List.map_i (fun i _ -> i) 0 ctx -let mk_proof c = ((c, Univ.ContextSet.empty), Declareops.no_seff) +let mk_proof c = ((c, Univ.ContextSet.empty), Safe_typing.empty_private_constants) let declare_mutual_definition l = let len = List.length l in @@ -619,7 +619,7 @@ let declare_obligation prg obl body ty uctx = shrink_body body else [], body, [||] in let ce = - { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Declareops.no_seff); + { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = if List.is_empty ctx then ty else None; const_entry_polymorphic = poly; @@ -796,12 +796,12 @@ let solve_by_tac name evi t poly ctx = let (entry,_,ctx') = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in - let entry = Term_typing.handle_entry_side_effects env entry in - let body, eff = Future.force entry.Entries.const_entry_body in - assert(Declareops.side_effects_is_empty eff); + let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in + let body, eff = Future.force entry.const_entry_body in + assert(Safe_typing.empty_private_constants = eff); let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); - (fst body), entry.Entries.const_entry_type, Evd.evar_universe_context ctx' + (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' let obligation_hook prg obl num auto ctx' _ gr = let obls, rem = prg.prg_obligations in diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 40f124ca3..61a8ee520 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -17,11 +17,11 @@ open Decl_kinds (** Forward declaration. *) val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref + Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref val declare_definition_ref : (Id.t -> definition_kind -> - Entries.definition_entry -> Impargs.manual_implicits + Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits -> global_reference Lemmas.declaration_hook -> global_reference) ref val check_evars : env -> evar_map -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml index 60fe76bb8..b1be4c92a 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -160,8 +160,8 @@ let degenerate_decl (na,b,t) = | Name id -> id | Anonymous -> anomaly (Pp.str "Unnamed record variable") in match b with - | None -> (id, Entries.LocalAssum t) - | Some b -> (id, Entries.LocalDef b) + | None -> (id, LocalAssum t) + | Some b -> (id, LocalDef b) type record_error = | MissingProj of Id.t * Id.t list @@ -297,7 +297,7 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field try let entry = { const_entry_body = - Future.from_val (Term_typing.mk_pure_proof proj); + Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_polymorphic = poly; |