diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 46 | ||||
| -rw-r--r-- | toplevel/command.mli | 12 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 12 |
3 files changed, 38 insertions, 32 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index c6d67b13ac..b6dd2718fa 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -139,9 +139,9 @@ let get_locality id = function | Local -> true | Global -> false -let declare_global_definition ~chkguard ident ce local k imps = +let declare_global_definition ~flags ident ce local k imps = let local = get_locality ident local in - let kn = declare_constant ~chkguard ident ~local (DefinitionEntry ce, IsDefinition k) in + let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in let () = definition_message ident in @@ -151,7 +151,7 @@ let declare_definition_hook = ref ignore let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook -let declare_definition ~chkguard ident (local, p, k) ce imps hook = +let declare_definition ~flags ident (local, p, k) ce imps hook = let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -167,10 +167,11 @@ let declare_definition ~chkguard ident (local, p, k) ce imps hook = in gr | Discharge | Local | Global -> - declare_global_definition ~chkguard ident ce local k imps in + declare_global_definition ~flags ident ce local k imps in Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r -let _ = Obligations.declare_definition_ref := declare_definition ~chkguard:true +let _ = Obligations.declare_definition_ref := + declare_definition ~flags:{Declarations.check_guarded=true} let do_definition ident k bl red_option c ctypopt hook = let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in @@ -191,7 +192,7 @@ let do_definition ident k bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ~chkguard:true ident k ce imps + ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -752,11 +753,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl = let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx -let declare_fix ~chkguard ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = +let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in - declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) + declare_definition ~flags f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) -let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true) +let _ = Obligations.declare_fix_ref := + (declare_fix ~flags:{Declarations.check_guarded=true}) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1044,7 +1046,7 @@ let interp_cofixpoint l ntns = check_recursive false env evd fix; fix,Evd.evar_universe_context evd,info -let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = +let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1072,7 +1074,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim let ctx = Universes.restrict_universe_context ctx vars in let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in let ctx = Univ.ContextSet.to_context ctx in - ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx) + ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1080,7 +1082,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns = +let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1103,7 +1105,7 @@ let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fix let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in let ctx = Univ.ContextSet.to_context ctx in - ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx) + ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -1168,7 +1170,11 @@ let do_program_recursive local p fixkind fixl ntns = in let indexes = Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in - List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl + List.iteri (fun i _ -> + Inductive.check_fix env + ~flags:{Declarations.check_guarded=true} + ((indexes,i),fixdecls)) + fixl end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with @@ -1202,21 +1208,21 @@ let do_program_fixpoint local poly l = errorlabstrm "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_fixpoint ~chkguard local poly l = +let do_fixpoint ~flags local poly l = if Flags.is_program_mode () then do_program_fixpoint local poly l else let fixl, ntns = extract_fixpoint_components true l in let fix = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences (pi3 fix) in - declare_fixpoint ~chkguard local poly fix possible_indexes ntns; - if not chkguard then Pp.feedback Feedback.AddedAxiom else () + declare_fixpoint ~flags local poly fix possible_indexes ntns; + if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else () -let do_cofixpoint ~chkguard local poly l = +let do_cofixpoint ~flags local poly l = let fixl,ntns = extract_cofixpoint_components l in if Flags.is_program_mode () then do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint ~chkguard local poly cofix ntns; - if not chkguard then Pp.feedback Feedback.AddedAxiom else () + declare_cofixpoint ~flags local poly cofix ntns; + if not flags.Declarations.check_guarded then Pp.feedback Feedback.AddedAxiom else () diff --git a/toplevel/command.mli b/toplevel/command.mli index 7578e26c16..73f8f98065 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -34,7 +34,7 @@ val interp_definition : local_binder list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits -val declare_definition : chkguard:bool -> +val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind -> definition_entry -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference @@ -147,14 +147,14 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : - chkguard:bool -> + flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : - chkguard:bool -> locality -> polymorphic -> + flags:Declarations.typing_flags -> locality -> polymorphic -> recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -162,11 +162,11 @@ val declare_cofixpoint : (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : - chkguard:bool -> (* When [false], assume guarded. *) + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : - chkguard:bool -> (* When [false], assume guarded. *) + flags:Declarations.typing_flags -> (* When [false], assume guarded. *) locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) @@ -174,6 +174,6 @@ val do_cofixpoint : val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit val declare_fix : - chkguard:bool -> + flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a0af1d5730..40dfa1b9a5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -578,17 +578,17 @@ let vernac_inductive chk poly lo finite indl = let indl = List.map unpack indl in do_mutual_inductive chk indl poly lo finite -let vernac_fixpoint ~chkguard locality poly local l = +let vernac_fixpoint ~flags locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_fixpoint ~chkguard local poly l + do_fixpoint ~flags local poly l -let vernac_cofixpoint ~chkguard locality poly local l = +let vernac_cofixpoint ~flags locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; - do_cofixpoint ~chkguard local poly l + do_cofixpoint ~flags local poly l let vernac_scheme l = if Dumpglob.dump () then @@ -1895,8 +1895,8 @@ let interp ?proof locality poly c = | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l - | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l - | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l + | VernacFixpoint (flags,local, l) -> vernac_fixpoint ~flags locality poly local l + | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe l |