diff options
| -rw-r--r-- | interp/declare.ml | 151 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 3 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 12 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 6 | ||||
| -rw-r--r-- | library/global.mli | 6 |
6 files changed, 90 insertions, 94 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 0adad1419..8781c8719 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -31,64 +31,6 @@ type internal_flag = | 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 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 false ctx - | Inr (id,(p,d,mk)) -> - (* Constr raisonne sur les noms courts *) - if variable_exists id then - alreadydeclared (Id.print id ++ str " already exists"); - - 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,poly),ctx) in - let impl = if impl then Implicit else Explicit in - impl, true, poly, ctx - | SectionLocalDef (de) -> - let univs = Global.push_named_def (id,de) in - let poly = match de.const_entry_universes with - | Monomorphic_const_entry _ -> false - | Polymorphic_const_entry _ -> true - in - Explicit, de.const_entry_opaque, - poly, 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,_) -> - if variable_polymorphic id then None - else Some (Inl (variable_context id)) - | Inl _ -> Some o - -type variable_obj = - (Univ.ContextSet.t, Id.t * variable_declaration) union - -let inVariable : variable_obj -> obj = - declare_object { (default_object "VARIABLE") with - cache_function = cache_variable; - discharge_function = discharge_variable; - classify_function = (fun _ -> Dispose) } - -(* for initial declaration *) -let declare_variable id obj = - let oname = add_leaf id (inVariable (Inr (id,obj))) in - declare_var_implicits id; - Notation.declare_ref_arguments_scope (VarRef id); - Heads.declare_head (EvalVarRef id); - oname - - (** Declaration of constants and parameters *) type constant_obj = { @@ -195,6 +137,20 @@ let update_tables c = Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c) +let register_side_effect (c, role) = + let o = inConstant { + cst_decl = None; + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + } 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|] + let declare_constant_common id cst = let o = inConstant cst in let _, kn as oname = add_leaf id o in @@ -229,25 +185,11 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e (** This globally defines the side-effects in the environment. We mark exported constants as being side-effect not to redeclare them at caching time. *) - let cd, export = Global.export_private_constants ~in_section cd in - export, ConstantEntry (PureEntry, cd) + let de, export = Global.export_private_constants ~in_section de in + export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) in - let iter_eff (c, role) = - let o = inConstant { - cst_decl = None; - cst_hyps = [] ; - cst_kind = IsProof Theorem; - cst_locl = false; - } 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|] - in - let () = List.iter iter_eff export in + let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; cst_hyps = [] ; @@ -265,6 +207,65 @@ let declare_definition ?(internal=UserIndividualRequest) declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) +(** Declaration of section variables and local definitions *) + +type section_variable_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 false ctx + | Inr (id,(p,d,mk)) -> + (* Constr raisonne sur les noms courts *) + if variable_exists id then + alreadydeclared (Id.print id ++ str " already exists"); + + 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,poly),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx + | SectionLocalDef (de) -> + let (de, eff) = Global.export_private_constants ~in_section:true de in + let () = List.iter register_side_effect eff in + let univs = Global.push_named_def (id,de) in + let poly = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in + Explicit, de.const_entry_opaque, + poly, 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,_) -> + if variable_polymorphic id then None + else Some (Inl (variable_context id)) + | Inl _ -> Some o + +type variable_obj = + (Univ.ContextSet.t, Id.t * variable_declaration) union + +let inVariable : variable_obj -> obj = + declare_object { (default_object "VARIABLE") with + cache_function = cache_variable; + discharge_function = discharge_variable; + classify_function = (fun _ -> Dispose) } + +(* for initial declaration *) +let declare_variable id obj = + let oname = add_leaf id (inVariable (Inr (id,obj))) in + declare_var_implicits id; + Notation.declare_ref_arguments_scope (VarRef id); + Heads.declare_head (EvalVarRef id); + oname + (** Declaration of inductive blocks *) let declare_inductive_argument_scopes kn mie = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 5150ad411..fa984515a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -383,8 +383,7 @@ let safe_push_named d env = let push_named_def (id,de) senv = let open Entries in - let trust = Term_typing.SideEffects senv.revstruct in - let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in + let c,typ,univs = Term_typing.translate_local_def senv.env id de in let poly = match de.Entries.const_entry_universes with | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a30bb37e6..fbc398a2a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -90,7 +90,7 @@ val push_named_assum : (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : - Id.t * private_constants Entries.definition_entry -> Univ.ContextSet.t safe_transformer + Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer (** Insertion of global axioms or definitions *) @@ -106,8 +106,8 @@ type exported_private_constant = Constant.t * private_constant_role val export_private_constants : in_section:bool -> - private_constants Entries.constant_entry -> - (unit Entries.constant_entry * exported_private_constant list) safe_transformer + private_constants Entries.definition_entry -> + (unit Entries.definition_entry * exported_private_constant list) safe_transformer (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 70dd6438d..761eab511 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -533,14 +533,10 @@ type side_effect_role = type exported_side_effect = Constant.t * constant_body * side_effect_role -let export_side_effects mb env ce = - match ce with - | ParameterEntry e -> [], ParameterEntry e - | ProjectionEntry e -> [], ProjectionEntry e - | DefinitionEntry c -> +let export_side_effects mb env c = let { const_entry_body = body } = c in let _, eff = Future.force body in - let ce = DefinitionEntry { c with + let ce = { c with const_entry_body = Future.chain body (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = @@ -609,9 +605,9 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) -let translate_local_def mb env id centry = +let translate_local_def env id centry = let open Cooking in - let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in let typ = decl.cook_type in if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin match decl.cook_body with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 55da4197e..c771452a1 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -18,7 +18,7 @@ type _ trust = | Pure : unit trust | SideEffects : structure_body -> side_effects trust -val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> +val translate_local_def : env -> Id.t -> unit definition_entry -> constant_def * types * Univ.ContextSet.t val translate_local_assum : env -> types -> types @@ -62,8 +62,8 @@ type exported_side_effect = * be pushed in the safe_env by safe typing. The main constant entry * needs to be translated as usual after this step. *) val export_side_effects : - structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * unit constant_entry + structure_body -> env -> side_effects definition_entry -> + exported_side_effect list * unit definition_entry val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/library/global.mli b/library/global.mli index 324181e79..2a646386e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,11 +32,11 @@ val set_typing_flags : Declarations.typing_flags -> 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 * Safe_typing.private_constants Entries.definition_entry) -> Univ.ContextSet.t +val push_named_def : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t val export_private_constants : in_section:bool -> - Safe_typing.private_constants Entries.constant_entry -> - unit Entries.constant_entry * Safe_typing.exported_private_constant list + Safe_typing.private_constants Entries.definition_entry -> + unit Entries.definition_entry * Safe_typing.exported_private_constant list val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t |