From 8589b9b487c1e9b996975bd5dc58f548d0d9280c Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Mon, 22 Jun 2015 13:42:13 +0200 Subject: Add a field in `mutual_inductive_body` to represent mutual inductive whose positivity is assumed. --- kernel/declarations.mli | 1 + kernel/declareops.ml | 4 +++- kernel/indtypes.ml | 1 + 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 27c1c3f3f..ef3e1bb6a 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -184,6 +184,7 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) } (** {6 Module declarations } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a7051d5c1..870aef1d2 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -258,7 +258,9 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_private = mib.mind_private } + mind_private = mib.mind_private; + mind_checked_positive = mib.mind_checked_positive; + } let inductive_instance mib = if mib.mind_polymorphic then diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 92e121402..72b615cc8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -857,6 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_polymorphic = p; mind_universes = ctx; mind_private = prv; + mind_checked_positive = true; } (************************************************************************) -- cgit v1.2.3 From 9a1e80524e1650311b019fedbd7e774242d80ea4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 09:24:43 +0200 Subject: Add a corresponding field in `mutual_inductive_entry` (part 1). The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been. --- kernel/entries.mli | 5 ++++- kernel/indtypes.ml | 6 +++--- library/declare.ml | 3 ++- toplevel/command.ml | 3 ++- toplevel/discharge.ml | 3 ++- toplevel/record.ml | 3 ++- 6 files changed, 15 insertions(+), 8 deletions(-) diff --git a/kernel/entries.mli b/kernel/entries.mli index 303d27d35..1a27aa9f6 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,7 +51,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; - mind_entry_private : bool option } + mind_entry_private : bool option; + mind_entry_check_positivity : bool; + (** [false] if positivity is to be assumed. *) +} (** {6 Constants (Definition/Axiom) } *) type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 72b615cc8..620c0f6d8 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -752,7 +752,7 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs = +let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs is_checked = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -857,7 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_polymorphic = p; mind_universes = ctx; mind_private = prv; - mind_checked_positive = true; + mind_checked_positive = is_checked; } (************************************************************************) @@ -872,4 +872,4 @@ let check_inductive env kn mie = build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar params kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs + inds nmr recargs mie.mind_entry_check_positivity diff --git a/library/declare.ml b/library/declare.ml index c3181e4c7..02e6dadde 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -366,7 +366,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; + mind_entry_check_positivity = true; }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/toplevel/command.ml b/toplevel/command.ml index 1b396d57b..49bd37c69 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -553,7 +553,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_inds = entries; mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; - mind_entry_universes = Evd.universe_context evd }, + mind_entry_universes = Evd.universe_context evd; + mind_entry_check_positivity = true; }, impls (* Very syntactical equality *) diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 7d5d61fb8..df4f77fa1 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -115,5 +115,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; - mind_entry_universes = univs + mind_entry_universes = univs; + mind_entry_check_positivity = mib.mind_checked_positive; } diff --git a/toplevel/record.ml b/toplevel/record.ml index 737b7fb59..2f7215adf 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -365,7 +365,8 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; mind_entry_private = None; - mind_entry_universes = ctx } in + mind_entry_universes = ctx; + mind_entry_check_positivity = true; } in let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in -- cgit v1.2.3 From 4a73e6b2bfb75451bcda7c74cf7478726a459799 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 15:44:31 +0200 Subject: Add a corresponding field in `mutual_inductive_entry` (part 2). The request for positivity to be assumed is honored. --- kernel/indtypes.ml | 46 +++++++++++++++++++++++++++++++--------------- 1 file changed, 31 insertions(+), 15 deletions(-) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 620c0f6d8..3516d4ef6 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -480,8 +480,12 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else for use by the guard condition (terms at these positions are considered sub-terms) as well as the number of of non-uniform arguments (used to generate induction schemes, so a priori less - relevant to the kernel). *) -let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = + relevant to the kernel). + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity_one ~chkpos (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc = let lparams = rel_context_length hyps in let nmr = rel_context_nhyps hyps in (** Positivity of one argument [c] of a constructor (i.e. the @@ -498,9 +502,12 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname recursive call. Occurrences in the right-hand side of the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with - None -> failwith_non_pos_list n ntypes [b] + | None when chkpos -> + failwith_non_pos_list n ntypes [b] + | None -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in let largs = List.map (whd_betadeltaiota env) largs in @@ -512,7 +519,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** The case where one of the inductives of the mutually inductive block occurs as an argument of another is not known to be safe. So Coq rejects it. *) - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) @@ -527,8 +535,9 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) - if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + if not chkpos || + (noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs) then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) @@ -550,7 +559,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname (** Inductives of the inductive block being defined are only allowed to appear nested in the parameters of another inductive type. Not in the proper indices. *) - if not (List.for_all (noccur_between n ntypes) auxlargs) then + if chkpos && + not (List.for_all (noccur_between n ntypes) auxlargs) then failwith_non_pos_list n ntypes auxlargs; (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in @@ -608,7 +618,8 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname | _ -> raise (IllFormedInd LocalNotConstructor) end else - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs in (nmr, List.rev lrec) @@ -628,9 +639,13 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -(** [check_positivity kn env_ar params] checks that the mutually - inductive block [inds] is strictly positive. *) -let check_positivity kn env_ar params inds = +(** [check_positivity ~chkpos kn env_ar params] checks that the mutually + inductive block [inds] is strictly positive. + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity ~chkpos kn env_ar params inds = let ntypes = Array.length inds in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = Array.rev_to_list rc in @@ -641,7 +656,7 @@ let check_positivity kn env_ar params inds = List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in let ienv = (env_ar, 1+lparams, ntypes, ra_env) in let nargs = rel_context_nhyps sign - nmr in - check_positivity_one ienv params (kn,i) nargs lcnames lc + check_positivity_one ~chkpos ienv params (kn,i) nargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -866,10 +881,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in + let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par params inds in + let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par params inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar params kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs mie.mind_entry_check_positivity + inds nmr recargs chkpos -- cgit v1.2.3 From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 17:45:04 +0200 Subject: Add corresponding field in `VernacInductive`. Makes sure not to generate inductive schemes of assumed positive types. --- intf/vernacexpr.mli | 4 +++- parsing/g_vernac.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 6 +++--- plugins/funind/merge.ml | 2 +- printing/ppvernac.ml | 2 +- stm/texmacspp.ml | 2 +- stm/vernac_classifier.ml | 2 +- toplevel/command.ml | 8 ++++---- toplevel/command.mli | 2 ++ toplevel/indschemes.ml | 2 +- toplevel/record.ml | 21 +++++++++++---------- toplevel/record.mli | 5 ++++- toplevel/vernacentries.ml | 21 +++++++++++++-------- 13 files changed, 46 insertions(+), 33 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d7b269a1d..5fff21e27 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -303,7 +303,9 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * simple_binder with_coercion list - | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of + bool (*[false] => assume positive*) * + private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e8a1b512c..be11b86ad 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -204,7 +204,7 @@ GEXTEND Gram indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (priv,f,indl) + VernacInductive (true,priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 065c12a2d..b4febba66 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1424,7 +1424,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1435,7 +1435,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1450,7 +1450,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index ea699580b..8c4bd484f 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -884,7 +884,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in - let mie,impls = Command.interp_mutual_inductive indl [] + let mie,impls = Command.interp_mutual_inductive true indl [] false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in (* Declare the mutual inductive block with its associated schemes *) ignore (Command.declare_mutual_inductive_with_eliminations mie impls) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0..a65bfd44d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -761,7 +761,7 @@ module Make (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) ) - | VernacInductive (p,f,l) -> + | VernacInductive (chk,p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 9edc1f1c7..4cc362dda 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_, _, iednll) -> + | VernacInductive (_,_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2b5eb8683..03ade646b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,l) -> + | VernacInductive (_,_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ diff --git a/toplevel/command.ml b/toplevel/command.ml index 49bd37c69..ca925d490 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -475,7 +475,7 @@ let check_param = function | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -554,7 +554,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = Evd.universe_context evd; - mind_entry_check_positivity = true; }, + mind_entry_check_positivity = chk; }, impls (* Very syntactical equality *) @@ -636,10 +636,10 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive indl poly prv finite = +let do_mutual_inductive chk indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,impls = interp_mutual_inductive chk indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie impls); (* Declare the possible notations of inductive types *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 3a38e52ce..3ec65b487 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -88,6 +88,7 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) structured_inductive_expr -> decl_notation list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> mutual_inductive_entry * one_inductive_impls list @@ -102,6 +103,7 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : + bool -> (* if [false], then positivity is assumed *) (one_inductive_expr * decl_notation list) list -> polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fbc45b4ae..ca3b0c290 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -478,7 +478,7 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_checked_positive then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; diff --git a/toplevel/record.ml b/toplevel/record.ml index 2f7215adf..259a35c58 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -340,7 +340,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite poly ctx id idbuild paramimpls params arity template +let declare_structure chk finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in let args = Termops.extended_rel_list nfields params in @@ -366,7 +366,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx; - mind_entry_check_positivity = true; } in + mind_entry_check_positivity = chk; } in let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in let rsp = (kn,0) in (* This is ind path of idstruc *) let cstr = (rsp,1) in @@ -385,7 +385,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map pi1 ctx))) -let declare_class finite def poly ctx id idbuild paramimpls params arity +let declare_class chk finite def poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign = let fieldimpls = (* Make the class implicit in the projections, and the params if applicable. *) @@ -424,7 +424,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -500,10 +500,11 @@ let declare_existing_class g = open Vernacexpr -(* [fs] corresponds to fields and [ps] to parameters; [coers] is a - list telling if the corresponding fields must me declared as coercions - or subinstances *) -let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = +(** [fs] corresponds to fields and [ps] to parameters; [coers] is a + list telling if the corresponding fields must me declared as + coercions or subinstances. When [chk] is false positivity is + assumed. *) +let definition_structure chk (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in @@ -524,14 +525,14 @@ let definition_structure (kind,poly,finite,(is_coe,(loc,idstruc)),ps,cfs,idbuild let sign = structure_signature (fields@params) in match kind with | Class def -> - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild implpars params arity template implfs fields is_coe coers priorities sign in gr | _ -> let implfs = List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in - let ind = declare_structure finite poly ctx idstruc + let ind = declare_structure chk finite poly ctx idstruc idbuild implpars params arity template implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in IndRef ind diff --git a/toplevel/record.mli b/toplevel/record.mli index 91dccb96e..be0450258 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -25,7 +25,9 @@ val declare_projections : coercion_flag list -> manual_explicitation list list -> rel_context -> (Name.t * bool) list * constant option list -val declare_structure : Decl_kinds.recursivity_kind -> +val declare_structure : + bool -> (** check positivity? *) + Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> Univ.universe_context -> Id.t -> Id.t -> manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *) @@ -38,6 +40,7 @@ val declare_structure : Decl_kinds.recursivity_kind -> inductive val definition_structure : + bool -> (** check positivity? *) inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * lident with_coercion * local_binder list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d9f8f52c..c925719fb 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -521,7 +521,7 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Pp.feedback Feedback.AddedAxiom -let vernac_record k poly finite struc binders sort nameopt cfs = +let vernac_record chk k poly finite struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) | Some (_,id as lid) -> @@ -532,9 +532,14 @@ let vernac_record k poly finite struc binders sort nameopt cfs = match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" | _ -> ()) cfs); - ignore(Record.definition_structure (k,poly,finite,struc,binders,cfs,const,sort)) - -let vernac_inductive poly lo finite indl = + ignore(Record.definition_structure chk (k,poly,finite,struc,binders,cfs,const,sort)) + +(** When [chk] is false, positivity is assumed. When [poly] is true + the type is declared polymorphic. When [lo] is true, then the type + is declared private (as per the [Private] keyword). [finite] + indicates whether the type is inductive, co-inductive or + neither. *) +let vernac_inductive chk poly lo finite indl = if Dumpglob.dump () then List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> match cstrs with @@ -550,14 +555,14 @@ let vernac_inductive poly lo finite indl = | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record (match b with Class true -> Class false | _ -> b) + vernac_record chk (match b with Class true -> Class false | _ -> b) poly finite id bl c oc fs | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) - in vernac_record (Class true) poly finite id bl c None [f] + in vernac_record chk (Class true) poly finite id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Errors.error "Definitional classes must have a single method" | [ ( id , bl , c , Class false, Constructors _), _ ] -> @@ -571,7 +576,7 @@ let vernac_inductive poly lo finite indl = | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo finite + do_mutual_inductive chk indl poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1889,7 +1894,7 @@ let interp ?proof locality poly c = | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl - | VernacInductive (priv,finite,l) -> vernac_inductive poly priv finite l + | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l -- cgit v1.2.3 From ec74137b4e4b96135c43570b5f149e7e1ec0db9c Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 24 Jun 2015 14:45:41 +0200 Subject: Add syntax entry to assume strict positivity of an inductive type. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…). --- parsing/g_vernac.ml4 | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index be11b86ad..25e679ba8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -71,6 +71,14 @@ let make_bullet s = | '*' -> Star n | _ -> assert false +type nl_assumption = + | Positive +let eq_nl_assumption x y = + match x,y with + | Positive,Positive -> true +let check_positivity l = + not (List.mem_f eq_nl_assumption Positive l) + let default_command_entry = Gram.Entry.of_parser "command_entry" (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) @@ -200,11 +208,11 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), id, b) (* Gallina inductive declarations *) - | priv = private_token; f = finite_token; + | priv = private_token; a = assume_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (true,priv,f,indl) + VernacInductive (check_positivity a,priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -269,6 +277,12 @@ GEXTEND Gram | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; + assume_token: + [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ] + ; + nl_assumption: + [ [ IDENT "Positive" -> Positive ] ] + ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; -- cgit v1.2.3 From 75381f7356133f68637fc9bbc0a213dcfa6e2c71 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 24 Jun 2015 15:24:49 +0200 Subject: When assuming an inductive type positive, then it is declared "unsafe" to the interfaces. --- toplevel/command.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index ca925d490..6beaf54c5 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -645,7 +645,10 @@ let do_mutual_inductive chk indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + (* If [chk] is [false] (i.e. positivity is assumed) declares itself + as unsafe. *) + if not chk then Pp.feedback Feedback.AddedAxiom else () (* 3c| Fixpoints and co-fixpoints *) -- cgit v1.2.3 From 476189527703aaf9caf5612e8395ce3b8ddb088f Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 24 Jun 2015 16:10:29 +0200 Subject: Make inductives that were assumed positive appear in `Print Assumptions`. They appear as axioms of the form `Foo is positive`. --- library/assumptions.ml | 26 ++++++++++++++++++++++---- library/assumptions.mli | 7 +++++-- printing/printer.ml | 11 +++++++++-- 3 files changed, 36 insertions(+), 8 deletions(-) diff --git a/library/assumptions.ml b/library/assumptions.ml index 62645b236..b2363bce6 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -23,9 +23,12 @@ open Declarations open Mod_subst open Globnames +type axiom = + | Constant of constant (* An axiom or a constant. *) + | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) + | Axiom of axiom (* An assumed fact. *) | Opaque of constant (* An opaque constant. *) | Transparent of constant @@ -33,10 +36,20 @@ type context_object = module OrderedContextObject = struct type t = context_object + + let compare_axiom x y = + match x,y with + | Constant k1 , Constant k2 -> + con_ord k1 k2 + | Positive m1 , Positive m2 -> + MutInd.CanOrd.compare m1 m2 + | Positive _ , Constant _ -> 1 + | _ -> -1 + let compare x y = match x , y with | Variable i1 , Variable i2 -> Id.compare i1 i2 - | Axiom k1 , Axiom k2 -> con_ord k1 k2 + | Axiom a1 , Axiom a2 -> compare_axiom a1 a2 | Opaque k1 , Opaque k2 -> con_ord k1 k2 | Transparent k1 , Transparent k2 -> con_ord k1 k2 | Axiom _ , Variable _ -> 1 @@ -211,7 +224,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = let cb = lookup_constant kn in if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in - ContextObjectMap.add (Axiom kn) t accu + ContextObjectMap.add (Axiom (Constant kn)) t accu else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then let t = type_of_constant cb in ContextObjectMap.add (Opaque kn) t accu @@ -220,6 +233,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = ContextObjectMap.add (Transparent kn) t accu else accu - | IndRef _ | ConstructRef _ -> accu + | IndRef (m,_) | ConstructRef ((m,_),_) -> + let mind = Global.lookup_mind m in + if mind.mind_checked_positive then + accu + else + ContextObjectMap.add (Axiom (Positive m)) Constr.mkProp accu in Refmap.fold fold graph ContextObjectMap.empty diff --git a/library/assumptions.mli b/library/assumptions.mli index bb36a9725..72ed6acf0 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -13,9 +13,12 @@ open Globnames (** A few declarations for the "Print Assumption" command @author spiwack *) +type axiom = + | Constant of constant (** An axiom or a constant. *) + | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *) type context_object = - | Variable of Id.t (** A section variable or a Let definition *) - | Axiom of constant (** An axiom or a constant. *) + | Variable of Id.t (** A section variable or a Let definition. *) + | Axiom of axiom (** An assumed fact. *) | Opaque of constant (** An opaque constant. *) | Transparent of constant (** A transparent constant *) diff --git a/printing/printer.ml b/printing/printer.ml index 652542825..b57fa9079 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -729,14 +729,21 @@ let pr_assumptionset env s = try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in + let pr_axiom env ax typ = + match ax with + | Constant kn -> + safe_pr_constant env kn ++ safe_pr_ltype typ + | Positive m -> + hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) - | Axiom kn -> - let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in + | Axiom axiom -> + let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) | Opaque kn -> let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in -- cgit v1.2.3 From 28855216037570aeabc544ab232bb896d7a7327f Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 25 Jun 2015 09:52:45 +0200 Subject: Adjust checker after `Assume [Positive]`. --- checker/cic.mli | 2 ++ checker/values.ml | 5 +++-- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/checker/cic.mli b/checker/cic.mli index e875e40f0..82eb35bcb 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -312,6 +312,8 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) + (** {8 Data for native compilation } *) mind_native_name : native_name ref; (** status of the code (linked or not, and where) *) diff --git a/checker/values.ml b/checker/values.ml index b2d74821d..cf56bbd98 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli +MD5 6f563f1f75706b28e5d3e3ef59e1681c checker/cic.mli *) @@ -265,7 +265,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body" v_rctxt; v_bool; v_context; - Opt v_bool|] + Opt v_bool; + v_bool|] let v_with = Sum ("with_declaration_body",0, -- cgit v1.2.3 From 42b7e36ddb68f53ada686900e5a98435d9ff7fde Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 25 Jun 2015 18:01:23 +0200 Subject: Add coqide syntax highlighting for `Assume`. --- ide/coq.lang | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/ide/coq.lang b/ide/coq.lang index c65432bdb..a31eadc70 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,12 +29,13 @@ (\%{ident}\.)*\%{ident} \.(\s|\z) ([-+*]+|{)(\s|\z)|}(\s*})* + (?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space} Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)? ((Local|Global)\%{space})? Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property Qed|Defined|Admitted|Abort|Save - ((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) + ((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) @@ -106,6 +107,7 @@ \%{dot_sep} + -- cgit v1.2.3 From 576d7a815174106f337fca2f19ad7f26a7e87cc4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 11:24:16 +0200 Subject: Add a flag to deactivate guard checking in the kernel. --- kernel/fast_typeops.ml | 4 ++-- kernel/inductive.ml | 54 ++++++++++++++++++++++++++--------------------- kernel/inductive.mli | 7 ++++-- kernel/typeops.ml | 4 ++-- pretyping/inductiveops.ml | 4 ++-- pretyping/pretyping.ml | 6 +++--- pretyping/typing.ml | 4 ++-- toplevel/command.ml | 2 +- 8 files changed, 47 insertions(+), 38 deletions(-) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 86fb1b64c..358795666 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -410,12 +410,12 @@ let rec execute env cstr = | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; fix_ty + check_fix env ~chk:true fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; fix_ty + check_cofix env ~chk:true cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4c1614bac..532287c30 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1065,21 +1065,24 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = - let (minds, rdef) = inductive_of_mutfix env fix in - let get_tree (kn,i) = - let mib = Environ.lookup_mind kn env in - mib.mind_packets.(i).mind_recargs - in - let trees = Array.map (fun (mind,_) -> get_tree mind) minds in - for i = 0 to Array.length bodies - 1 do - let (fenv,body) = rdef.(i) in - let renv = make_renv fenv nvect.(i) trees.(i) in - try check_one_fix renv nvect trees body - with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i - (push_rec_types recdef env) (judgment_of_fixpoint recdef) - done +let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) = + if chk then + let (minds, rdef) = inductive_of_mutfix env fix in + let get_tree (kn,i) = + let mib = Environ.lookup_mind kn env in + mib.mind_packets.(i).mind_recargs + in + let trees = Array.map (fun (mind,_) -> get_tree mind) minds in + for i = 0 to Array.length bodies - 1 do + let (fenv,body) = rdef.(i) in + let renv = make_renv fenv nvect.(i) trees.(i) in + try check_one_fix renv nvect trees body + with FixGuardError (fixenv,err) -> + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) + done + else + () (* let cfkey = Profile.declare_profile "check_fix";; @@ -1190,12 +1193,15 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in - for i = 0 to nbfix-1 do - let fixenv = push_rec_types recdef env in - try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i - fixenv (judgment_of_fixpoint recdef) - done +let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) = + if chk then + let nbfix = Array.length bodies in + for i = 0 to nbfix-1 do + let fixenv = push_rec_types recdef env in + try check_one_cofix fixenv nbfix bodies.(i) types.(i) + with CoFixGuardError (errenv,err) -> + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) + done + else + () diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 5847d25f6..36f32b30c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -95,8 +95,11 @@ val inductive_sort_family : one_inductive_body -> sorts_family val check_case_info : env -> pinductive -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) -val check_fix : env -> fixpoint -> unit -val check_cofix : env -> cofixpoint -> unit + +(** When [chk] is false, the guard condition is not actually + checked. *) +val check_fix : env -> chk:bool -> fixpoint -> unit +val check_cofix : env -> chk:bool -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 48dbacf1a..9e9f18aaa 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -494,13 +494,13 @@ let rec execute env cstr = | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; + check_fix ~chk:true env fix; make_judge (mkFix fix) fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix ~chk:true env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index dfdc24d48..efea4bec8 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix e cofix + Inductive.check_cofix ~chk:true e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix e fix + Inductive.check_fix ~chk:true e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 03fe2122c..d9f490ba5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env fix + (try check_fix env ~chk:true fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env fix; raise (Found indexes) + try check_fix env ~chk:true fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env ~chk:true cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index fb5927dbf..0bb2979c2 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env fix; + check_fix env ~chk:true fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env cofix; + check_cofix env ~chk:true cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index 6beaf54c5..06d7c629a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1168,7 +1168,7 @@ 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 ((indexes,i),fixdecls)) fixl + List.iteri (fun i _ -> Inductive.check_fix env ~chk:true ((indexes,i),fixdecls)) fixl end in let ctx = Evd.evar_universe_context evd in let kind = match fixkind with -- cgit v1.2.3 From e0547f9e9134a9fff122df900942a094c53535c3 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 21:15:36 +0200 Subject: Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness. --- intf/vernacexpr.mli | 2 ++ parsing/g_vernac.ml4 | 8 ++++---- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/indfun.ml | 2 +- printing/ppvernac.ml | 17 +++++++++++++---- stm/texmacspp.ml | 4 ++-- stm/vernac_classifier.ml | 4 ++-- toplevel/command.ml | 12 ++++++------ toplevel/command.mli | 6 +++++- toplevel/vernacentries.ml | 12 ++++++------ 10 files changed, 42 insertions(+), 27 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 5fff21e27..ba9ac16b6 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -307,8 +307,10 @@ type vernac_expr = bool (*[false] => assume positive*) * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of + bool * (* [false] => assume guarded *) locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of + bool * (* [false] => assume guarded *) locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 25e679ba8..b71028942 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -214,13 +214,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (check_positivity a,priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (None, recs) + VernacFixpoint (true,None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (Some Discharge, recs) + VernacFixpoint (true,Some Discharge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (None, corecs) + VernacCoFixpoint (true,None, corecs) | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (Some Discharge, corecs) + VernacCoFixpoint (true,Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 61f03d6f2..53ec304cc 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5dcb0c043..5c849ba41 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) (((_,fname),_,_,_,_),_) -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a65bfd44d..93cd35472 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -399,6 +399,15 @@ module Make | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i + let pr_assume ?(positive=false) ?(guarded=false) () = + let assumed = + (if guarded then [str"Guarded"] else []) @ + (if positive then [str"Positive"] else []) + in + match assumed with + | [] -> mt () + | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc() + (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -797,7 +806,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (local, recs) -> + | VernacFixpoint (chkguard,local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -812,11 +821,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (local, corecs) -> + | VernacCoFixpoint (chkguard,local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -829,7 +838,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4cc362dda..4f014be2d 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -598,14 +598,14 @@ let rec tmpp v loc = (fun (ie, dnl) -> (pp_inductive_expr ie) @ (List.map pp_decl_notation dnl)) iednll) in xmlInductive kind loc exprs - | VernacFixpoint (_, fednll) -> + | VernacFixpoint (_,_, fednll) -> let exprs = List.flatten (* should probably not be flattened *) (List.map (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ (List.map pp_decl_notation dnl)) fednll) in xmlFixpoint exprs - | VernacCoFixpoint (_, cfednll) -> + | VernacCoFixpoint (_,_, cfednll) -> (* Nota: it is like VernacFixpoint without so could be merged *) let exprs = List.flatten (* should probably not be flattened *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 03ade646b..574cc0044 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -125,14 +125,14 @@ let rec classify_vernac e = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + | VernacFixpoint (_,_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (_,_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in diff --git a/toplevel/command.ml b/toplevel/command.ml index 06d7c629a..14a1efe4d 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1044,7 +1044,7 @@ let interp_cofixpoint l ntns = check_recursive false env evd fix; fix,Evd.evar_universe_context evd,info -let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns = +let declare_fixpoint ~chkguard 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 = @@ -1080,7 +1080,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe (* Declare notations *) List.iter Metasyntax.add_notation_interpretation ntns -let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns = +let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns = if List.exists Option.is_empty fixdefs then (* Some bodies to define by proof *) let thms = @@ -1202,19 +1202,19 @@ let do_program_fixpoint local poly l = errorlabstrm "do_program_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_fixpoint local poly l = +let do_fixpoint ~chkguard 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 local poly fix possible_indexes ntns + declare_fixpoint ~chkguard local poly fix possible_indexes ntns -let do_cofixpoint local poly l = +let do_cofixpoint ~chkguard 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 local poly cofix ntns + declare_cofixpoint ~chkguard local poly cofix ntns diff --git a/toplevel/command.mli b/toplevel/command.mli index 3ec65b487..7112591fe 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -146,12 +146,14 @@ val interp_cofixpoint : (** Registering fixpoints and cofixpoints in the environment *) val declare_fixpoint : + chkguard:bool -> 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 : locality -> polymorphic -> +val declare_cofixpoint : + chkguard:bool -> locality -> polymorphic -> recursive_preentry * Evd.evar_universe_context * (Name.t list * Impargs.manual_implicits * int option) list -> decl_notation list -> unit @@ -159,9 +161,11 @@ val declare_cofixpoint : locality -> polymorphic -> (** Entry points for the vernacular commands Fixpoint and CoFixpoint *) val do_fixpoint : + chkguard:bool -> (* When [false], assume guarded. *) locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit val do_cofixpoint : + chkguard:bool -> (* When [false], assume guarded. *) locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit (** Utils *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c925719fb..a0af1d573 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 locality poly local l = +let vernac_fixpoint ~chkguard 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 local poly l + do_fixpoint ~chkguard local poly l -let vernac_cofixpoint locality poly local l = +let vernac_cofixpoint ~chkguard 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 local poly l + do_cofixpoint ~chkguard 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 (local, l) -> vernac_fixpoint locality poly local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l + | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l + | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe l -- cgit v1.2.3 From d50aa51b4a3d39e708bc5ab3acb9f549857bceef Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 23 Jul 2015 09:46:21 +0200 Subject: Add `Guarded` to the assumption tokens. --- parsing/g_vernac.ml4 | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b71028942..263792ef0 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -73,11 +73,16 @@ let make_bullet s = type nl_assumption = | Positive + | Guarded let eq_nl_assumption x y = match x,y with | Positive,Positive -> true + | Guarded,Guarded -> true + | _ , _ -> false let check_positivity l = not (List.mem_f eq_nl_assumption Positive l) +let check_guardedness l = + not (List.mem_f eq_nl_assumption Guarded l) let default_command_entry = Gram.Entry.of_parser "command_entry" @@ -281,7 +286,8 @@ GEXTEND Gram [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ] ; nl_assumption: - [ [ IDENT "Positive" -> Positive ] ] + [ [ IDENT "Positive" -> Positive + | IDENT "Guarded" -> Guarded ] ] ; private_token: [ [ IDENT "Private" -> true | -> false ] ] -- cgit v1.2.3 From 8f64e84a3560bcf668b00ac93ab33542456a9bda Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Thu, 23 Jul 2015 09:51:18 +0200 Subject: Add (temporary) syntax for assuming guardedness in (co-)fixed points. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The syntax is `Fixpoint Assume[Guarded] …`. For some reason `Assume [Guarded] Fixpoint` broke the parser. --- parsing/g_vernac.ml4 | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 263792ef0..ced2da7a5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -218,14 +218,14 @@ GEXTEND Gram let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (check_positivity a,priv,f,indl) - | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (true,None, recs) - | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (true,Some Discharge, recs) - | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (true,None, corecs) - | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (true,Some Discharge, corecs) + | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (check_guardedness a,None, recs) + | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (check_guardedness a,Some Discharge, recs) + | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (check_guardedness a,None, corecs) + | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (check_guardedness a,Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) -- cgit v1.2.3 From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 24 Jul 2015 08:46:09 +0200 Subject: Propagate `Guarded` flag from syntax to kernel. The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here. --- kernel/fast_typeops.ml | 69 ++++++++++++++++++++++++++----------------------- kernel/fast_typeops.mli | 6 ++--- kernel/safe_typing.ml | 13 +++++----- kernel/safe_typing.mli | 4 ++- kernel/term_typing.ml | 28 ++++++++++---------- kernel/term_typing.mli | 8 +++--- library/declare.ml | 18 ++++++------- library/declare.mli | 2 ++ library/global.ml | 4 +-- library/global.mli | 6 +++-- toplevel/command.ml | 22 ++++++++-------- toplevel/command.mli | 7 +++-- 12 files changed, 100 insertions(+), 87 deletions(-) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 358795666..8c14f5e04 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft = (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) -let rec execute env cstr = +let rec execute ~chkguard env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -345,12 +345,12 @@ let rec execute env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute env c in + let ct = execute ~chkguard env c in judge_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in + let argst = execute_array ~chkguard env args in let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> @@ -363,7 +363,7 @@ let rec execute env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute env f + execute ~chkguard env f in judge_of_apply env f ft args argst @@ -371,25 +371,25 @@ let rec execute env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (name,None,c1) env in - let c2t = execute env1 c2 in + let c2t = execute ~chkguard env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in + let vars = execute_is_type ~chkguard env c1 in let env1 = push_rel (name,None,c1) env in - let vars' = execute_is_type env1 c2 in + let vars' = execute_is_type ~chkguard env1 c2 in judge_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in + let c1t = execute ~chkguard env c1 in let _c2s = execute_is_type env c2 in let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (name,Some c1,c2) env in - let c3t = execute env1 c3 in + let c3t = execute ~chkguard env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in + let ct = execute ~chkguard env c in let _ts = execute_type env t in let _ = judge_of_cast env c ct k t in t @@ -402,20 +402,20 @@ let rec execute env cstr = judge_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in + let ct = execute ~chkguard env c in + let pt = execute ~chkguard env p in + let lft = execute_array ~chkguard env lf in judge_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in let fix = (vni,recdef') in - check_fix env ~chk:true fix; fix_ty + check_fix env ~chk:chkguard fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in let cofix = (i,recdef') in - check_cofix env ~chk:true cofix; fix_ty + check_cofix env ~chk:chkguard cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -424,38 +424,41 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type env constr = - let t = execute env constr in +and execute_is_type ~chkguard env constr = + let t = execute ~chkguard env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in +and execute_type ~chkguard env constr = + let t = execute ~chkguard env constr in type_judgment env constr t -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in +and execute_recdef ~chkguard env (names,lar,vdef) i = + let lart = execute_array ~chkguard env lar in let lara = Array.map2 (assumption_of_judgment env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in + let vdeft = execute_array ~chkguard env1 vdef in let () = type_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) -and execute_array env = Array.map (execute env) +and execute_array ~chkguard env = Array.map (execute ~chkguard env) (* Derived functions *) -let infer env constr = - let t = execute env constr in +let infer ~chkguard env constr = + let t = execute ~chkguard env constr in make_judge constr t let infer = if Flags.profile then let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key infer - else infer + Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c) + else (fun a b c -> infer ~chkguard:a b c) -let infer_type env constr = - execute_type env constr +(* Restores the labels of [infer] lost to profiling. *) +let infer ~chkguard env t = infer chkguard env t -let infer_v env cv = - let jv = execute_array env cv in +let infer_type ~chkguard env constr = + execute_type ~chkguard env constr + +let infer_v ~chkguard env cv = + let jv = execute_array ~chkguard env cv in make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 90d9c55f1..98dbefad1 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -18,6 +18,6 @@ open Environ *) -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment +val infer : chkguard:bool -> env -> constr -> unsafe_judgment +val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array +val infer_type : chkguard:bool -> env -> types -> unsafe_type_judgment diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d9adca0c9..18d897817 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env -let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.env id de in +let push_named_def ~chkguard (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with | Def c -> Mod_subst.force_constr c, senv' @@ -346,9 +346,9 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} -let push_named_assum ((id,t),ctx) senv = +let push_named_assum ~chkguard ((id,t),ctx) senv = let senv' = push_context_set ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in + let t = Term_typing.translate_local_assum ~chkguard senv'.env t in let env'' = safe_push_named (id,None,t) senv'.env in {senv' with env=env''} @@ -439,13 +439,14 @@ 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 Entries.constant_entry * bool (* check guard *) | 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 + | ConstantEntry (ce,chkguard) -> + Term_typing.translate_constant ~chkguard 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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a57fb108c..80b9bb495 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,14 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : + chkguard:bool -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : + chkguard:bool -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry + | ConstantEntry of Entries.constant_entry * bool (* chkguard *) | GlobalRecipe of Cooking.recipe val add_constant : diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a316b4492..539305ed1 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -23,18 +23,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly subst = function +let constrain_type ~chkguard env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) | `Some t -> - let tj = infer_type env t in + let tj = infer_type ~chkguard env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) | `SomeWJ (t, tj) -> - let tj = infer_type env t in + let tj = infer_type ~chkguard env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) @@ -101,11 +101,11 @@ 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 ~chkguard env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context uctx env in - let j = infer env t in + let j = infer ~chkguard env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in @@ -122,7 +122,7 @@ let infer_declaration env kn dcl = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> let body = handle_side_effects env body side_eff in let env' = push_context_set ctx env in - let j = infer env' body in + let j = infer ~chkguard env' body 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,8 +143,8 @@ let infer_declaration env kn dcl = let body = handle_side_effects env body side_eff in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let j = infer ~chkguard env body in + let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) @@ -266,20 +266,20 @@ 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 ~chkguard env kn ce = + build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce) -let translate_local_assum env t = - let j = infer env t in +let translate_local_assum ~chkguard env t = + let j = infer ~chkguard env t in let t = Typeops.assumption_of_judgment env j in 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 ~chkguard env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration env None (DefinitionEntry centry) in + infer_declaration ~chkguard env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in def, typ, univs diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 1b54b1ea1..a71587f0f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,10 +12,10 @@ open Environ open Declarations open Entries -val translate_local_def : env -> Id.t -> definition_entry -> +val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry -> constant_def * types * constant_universes -val translate_local_assum : env -> types -> types +val translate_local_assum : chkguard:bool -> env -> types -> types val mk_pure_proof : constr -> proof_output @@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry {!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 translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,7 +37,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : env -> constant option -> +val infer_declaration : chkguard:bool -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : diff --git a/library/declare.ml b/library/declare.ml index 02e6dadde..4be13109a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ((id,ty),ctx) in + let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def (id,de) in + let () = Global.push_named_def ~chkguard:true (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, (Univ.ContextSet.of_context de.const_entry_universes) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -232,7 +232,7 @@ let declare_sideff env fix_exn se = const_entry_feedback = None; const_entry_polymorphic = cb.const_polymorphic; const_entry_universes = univs; - }); + }, true); cst_hyps = [] ; cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; cst_locl = true; @@ -253,7 +253,7 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -275,7 +275,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff | _ -> cd in let cst = { - cst_decl = ConstantEntry cd; + cst_decl = ConstantEntry (cd,chkguard); cst_hyps = [] ; cst_kind = kind; cst_locl = local; @@ -283,13 +283,13 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff let kn = declare_constant_common id cst in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?chkguard ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in - declare_constant ~internal ~local id + declare_constant ?chkguard ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) @@ -387,7 +387,7 @@ let declare_projections mind = Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, + let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true diff --git a/library/declare.mli b/library/declare.mli index d8a00db0c..94cebe3bd 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,9 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : + ?chkguard:bool -> (** default [true] (check guardedness) *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : + ?chkguard:bool -> (** default [true] (check guardedness) *) ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant diff --git a/library/global.ml b/library/global.ml index 49fa2ef28..27f7f5266 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,8 +77,8 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) -let push_named_def d = globalize0 (Safe_typing.push_named_def d) +let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a) +let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) diff --git a/library/global.mli b/library/global.mli index 248e1f86d..388fee527 100644 --- a/library/global.mli +++ b/library/global.mli @@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit -val push_named_def : (Id.t * Entries.definition_entry) -> unit +val push_named_assum : + chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_def : + chkguard:bool -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant diff --git a/toplevel/command.ml b/toplevel/command.ml index 14a1efe4d..ac46b439c 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 ident ce local k imps = +let declare_global_definition ~chkguard ident ce local k imps = let local = get_locality ident local in - let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in + let kn = declare_constant ~chkguard 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 ident (local, p, k) ce imps hook = +let declare_definition ~chkguard 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,10 @@ let declare_definition ident (local, p, k) ce imps hook = in gr | Discharge | Local | Global -> - declare_global_definition ident ce local k imps in + declare_global_definition ~chkguard 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 +let _ = Obligations.declare_definition_ref := declare_definition ~chkguard: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 +191,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 ident k ce imps + ignore(declare_definition ~chkguard:true ident k ce imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -752,11 +752,11 @@ 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 ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps = +let declare_fix ~chkguard ?(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 f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) + declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r)) -let _ = Obligations.declare_fix_ref := declare_fix +let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1072,7 +1072,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 (local, poly, Fixpoint) ctx) + ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -1103,7 +1103,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 (local, poly, CoFixpoint) ctx) + ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames diff --git a/toplevel/command.mli b/toplevel/command.mli index 7112591fe..7578e26c1 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -34,7 +34,8 @@ 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 : Id.t -> definition_kind -> +val declare_definition : chkguard:bool -> + Id.t -> definition_kind -> definition_entry -> Impargs.manual_implicits -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference @@ -172,5 +173,7 @@ 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 -> +val declare_fix : + chkguard:bool -> + ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference -- cgit v1.2.3 From 9f4e67a7c9f22ca853e76f4837a276a6111bf159 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Sep 2015 09:27:50 +0200 Subject: Prevent pretyping from checking well-guardedness unnecessarily. The `search_guard` function is called to infer the recursive argument of fixpoints. For each potential argument, it tests whether it is called structurally, calling the kernel test. When a single argument is available either because `{struct x}` was specified, or because there is a single inductive argument, the kernel test is performed, despite the fact that the kernel will do it later, and the kernel error reraised. It is unnecessary. --- pretyping/pretyping.ml | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d9f490ba5..94749648e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -73,14 +73,9 @@ let search_guard loc env possible_indexes fixdefs = (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then - let indexes = Array.of_list (List.map List.hd possible_indexes) in - let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~chk:true fix - with reraise -> - let (e, info) = Errors.push reraise in - let info = Loc.add_loc info loc in - iraise (e, info)); - indexes + (* in this case, errors are delegated to the kernel, which will + check well-guardedness if required. *) + Array.of_list (List.map List.hd possible_indexes) else (* we now search recursively among all combinations *) (try -- cgit v1.2.3 From 0b20282c49253aea4429384467b75a5bdb1f8ba4 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Sep 2015 09:39:56 +0200 Subject: Declare assumptions of well-founded definitions as unsafe. So that fixpoints and cofixpoints which are assumed to be total are highlighted in yellow in Coqide, for instance. --- toplevel/command.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index ac46b439c..c6d67b13a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1209,7 +1209,8 @@ let do_fixpoint ~chkguard local poly l = 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 + declare_fixpoint ~chkguard local poly fix possible_indexes ntns; + if not chkguard then Pp.feedback Feedback.AddedAxiom else () let do_cofixpoint ~chkguard local poly l = let fixl,ntns = extract_cofixpoint_components l in @@ -1217,4 +1218,5 @@ let do_cofixpoint ~chkguard local poly l = do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint ~chkguard local poly cofix ntns + declare_cofixpoint ~chkguard local poly cofix ntns; + if not chkguard then Pp.feedback Feedback.AddedAxiom else () -- cgit v1.2.3 From caf8402e4af75d85223e10cba68a6a145e050dab Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Sep 2015 15:09:15 +0200 Subject: Add a field in `constant_body` to track constant whose well-foundedness is assumed. --- kernel/declarations.mli | 4 +++- kernel/declareops.ml | 3 ++- kernel/term_typing.ml | 9 +++++---- kernel/term_typing.mli | 2 +- 4 files changed, 11 insertions(+), 7 deletions(-) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ef3e1bb6a..591a7d404 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -74,7 +74,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) +} type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 870aef1d2..068bc498a 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -132,7 +132,8 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; - const_inline_code = cb.const_inline_code } + const_inline_code = cb.const_inline_code; + const_checked_guarded = cb.const_checked_guarded } (** {7 Hash-consing of constants } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 539305ed1..8a105ac97 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -186,7 +186,7 @@ let record_aux env s1 s2 = let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -261,13 +261,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = tps; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_checked_guarded = chkguard } (*s Global and local constant declaration. *) let translate_constant ~chkguard env kn ce = - build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce) + build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce) let translate_local_assum ~chkguard env t = let j = infer ~chkguard env t in @@ -275,7 +276,7 @@ let translate_local_assum ~chkguard env t = t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r) let translate_local_def ~chkguard env id centry = let def,typ,proj,poly,univs,inline_code,ctx = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index a71587f0f..ba4d96a5f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -41,7 +41,7 @@ val infer_declaration : chkguard:bool -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + chkguard:bool -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit -- cgit v1.2.3 From 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 25 Sep 2015 15:11:01 +0200 Subject: Show assumptions of well-foundedness in `Print Assumptions` --- library/assumptions.ml | 12 ++++++++++-- library/assumptions.mli | 1 + printing/printer.ml | 2 ++ 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/library/assumptions.ml b/library/assumptions.ml index b2363bce6..463527820 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -26,6 +26,7 @@ open Globnames type axiom = | Constant of constant (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *) type context_object = | Variable of Id.t (* A section variable or a Let definition *) | Axiom of axiom (* An assumed fact. *) @@ -43,7 +44,10 @@ struct con_ord k1 k2 | Positive m1 , Positive m2 -> MutInd.CanOrd.compare m1 m2 - | Positive _ , Constant _ -> 1 + | Guarded k1 , Guarded k2 -> + con_ord k1 k2 + | _ , Constant _ -> 1 + | _ , Positive _ -> 1 | _ -> -1 let compare x y = @@ -221,7 +225,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = if Option.is_empty body then ContextObjectMap.add (Variable id) t accu else accu | ConstRef kn -> - let cb = lookup_constant kn in + let cb = lookup_constant kn in + let accu = + if cb.const_checked_guarded then accu + else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu + in if not (Declareops.constant_has_body cb) then let t = type_of_constant cb in ContextObjectMap.add (Axiom (Constant kn)) t accu diff --git a/library/assumptions.mli b/library/assumptions.mli index 72ed6acf0..499e2b42e 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -16,6 +16,7 @@ open Globnames type axiom = | Constant of constant (** An axiom or a constant. *) | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *) + | Guarded of constant (** A constant whose (co)fixpoints have been assumed to be guarded *) type context_object = | Variable of Id.t (** A section variable or a Let definition. *) | Axiom of axiom (** An assumed fact. *) diff --git a/printing/printer.ml b/printing/printer.ml index b57fa9079..8609b19c9 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -735,6 +735,8 @@ let pr_assumptionset env s = safe_pr_constant env kn ++ safe_pr_ltype typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + | Guarded kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in let fold t typ accu = let (v, a, o, tr) = accu in -- cgit v1.2.3 From 64e94267cb80adc1b4df782cc83a579ee521b59b Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 5 Apr 2016 09:25:54 +0200 Subject: Revert "Prevent pretyping from checking well-guardedness unnecessarily." This reverts commit 9f4e67a7c9f22ca853e76f4837a276a6111bf159. --- pretyping/pretyping.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 94749648e..d9f490ba5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -73,9 +73,14 @@ let search_guard loc env possible_indexes fixdefs = (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then - (* in this case, errors are delegated to the kernel, which will - check well-guardedness if required. *) - Array.of_list (List.map List.hd possible_indexes) + let indexes = Array.of_list (List.map List.hd possible_indexes) in + let fix = ((indexes, 0),fixdefs) in + (try check_fix env ~chk:true fix + with reraise -> + let (e, info) = Errors.push reraise in + let info = Loc.add_loc info loc in + iraise (e, info)); + indexes else (* we now search recursively among all combinations *) (try -- cgit v1.2.3 From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 7 Jun 2016 09:52:43 +0200 Subject: Assume totality: dedicated type rather than bool The rational is that 1. further typing flags may be available in the future 2. it makes it easier to trace and document the argument --- intf/vernacexpr.mli | 4 +-- kernel/declarations.mli | 13 ++++++++- kernel/declareops.ml | 2 +- kernel/fast_typeops.ml | 68 ++++++++++++++++++++++----------------------- kernel/fast_typeops.mli | 7 +++-- kernel/inductive.ml | 8 +++--- kernel/inductive.mli | 4 +-- kernel/safe_typing.ml | 14 +++++----- kernel/safe_typing.mli | 6 ++-- kernel/term_typing.ml | 34 +++++++++++------------ kernel/term_typing.mli | 10 +++---- kernel/typeops.ml | 4 +-- library/assumptions.ml | 2 +- library/declare.ml | 18 ++++++------ library/declare.mli | 4 +-- library/global.ml | 4 +-- library/global.mli | 4 +-- parsing/g_vernac.ml4 | 8 +++--- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/indfun.ml | 2 +- pretyping/inductiveops.ml | 4 +-- pretyping/pretyping.ml | 6 ++-- pretyping/typing.ml | 4 +-- printing/ppvernac.ml | 8 +++--- toplevel/command.ml | 46 +++++++++++++++++------------- toplevel/command.mli | 12 ++++---- toplevel/vernacentries.ml | 12 ++++---- 27 files changed, 164 insertions(+), 146 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index ba9ac16b6..2f2f97376 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -307,10 +307,10 @@ type vernac_expr = bool (*[false] => assume positive*) * private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - bool * (* [false] => assume guarded *) + Declarations.typing_flags * locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - bool * (* [false] => assume guarded *) + Declarations.typing_flags * locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 591a7d404..0c085df39 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -64,6 +64,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { @@ -75,7 +84,9 @@ type constant_body = { const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; - const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) + const_typing_flags : typing_flags; (** The typing options which + were used for + type-checking. *) } type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 068bc498a..98d287737 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -133,7 +133,7 @@ let subst_const_body sub cb = const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; - const_checked_guarded = cb.const_checked_guarded } + const_typing_flags = cb.const_typing_flags } (** {7 Hash-consing of constants } *) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 8c14f5e04..32583f531 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft = (* ATTENTION : faudra faire le typage du contexte des Const, Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) -let rec execute ~chkguard env cstr = +let rec execute ~flags env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -345,12 +345,12 @@ let rec execute ~chkguard env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute ~chkguard env c in + let ct = execute ~flags env c in judge_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array ~chkguard env args in + let argst = execute_array ~flags env args in let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> @@ -363,7 +363,7 @@ let rec execute ~chkguard env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute ~chkguard env f + execute ~flags env f in judge_of_apply env f ft args argst @@ -371,25 +371,25 @@ let rec execute ~chkguard env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (name,None,c1) env in - let c2t = execute ~chkguard env1 c2 in + let c2t = execute ~flags env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type ~chkguard env c1 in + let vars = execute_is_type ~flags env c1 in let env1 = push_rel (name,None,c1) env in - let vars' = execute_is_type ~chkguard env1 c2 in + let vars' = execute_is_type ~flags env1 c2 in judge_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute ~chkguard env c1 in + let c1t = execute ~flags env c1 in let _c2s = execute_is_type env c2 in let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in let env1 = push_rel (name,Some c1,c2) env in - let c3t = execute ~chkguard env1 c3 in + let c3t = execute ~flags env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute ~chkguard env c in + let ct = execute ~flags env c in let _ts = execute_type env t in let _ = judge_of_cast env c ct k t in t @@ -402,20 +402,20 @@ let rec execute ~chkguard env cstr = judge_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute ~chkguard env c in - let pt = execute ~chkguard env p in - let lft = execute_array ~chkguard env lf in + let ct = execute ~flags env c in + let pt = execute ~flags env p in + let lft = execute_array ~flags env lf in judge_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let fix = (vni,recdef') in - check_fix env ~chk:chkguard fix; fix_ty + check_fix env ~flags fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let cofix = (i,recdef') in - check_cofix env ~chk:chkguard cofix; fix_ty + check_cofix env ~flags cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -424,41 +424,41 @@ let rec execute ~chkguard env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type ~chkguard env constr = - let t = execute ~chkguard env constr in +and execute_is_type ~flags env constr = + let t = execute ~flags env constr in check_type env constr t -and execute_type ~chkguard env constr = - let t = execute ~chkguard env constr in +and execute_type ~flags env constr = + let t = execute ~flags env constr in type_judgment env constr t -and execute_recdef ~chkguard env (names,lar,vdef) i = - let lart = execute_array ~chkguard env lar in +and execute_recdef ~flags env (names,lar,vdef) i = + let lart = execute_array ~flags env lar in let lara = Array.map2 (assumption_of_judgment env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array ~chkguard env1 vdef in + let vdeft = execute_array ~flags env1 vdef in let () = type_fixpoint env1 names lara vdef vdeft in (lara.(i),(names,lara,vdef)) -and execute_array ~chkguard env = Array.map (execute ~chkguard env) +and execute_array ~flags env = Array.map (execute ~flags env) (* Derived functions *) -let infer ~chkguard env constr = - let t = execute ~chkguard env constr in +let infer ~flags env constr = + let t = execute ~flags env constr in make_judge constr t let infer = if Flags.profile then let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c) - else (fun a b c -> infer ~chkguard:a b c) + Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c) + else (fun a b c -> infer ~flags:a b c) (* Restores the labels of [infer] lost to profiling. *) -let infer ~chkguard env t = infer chkguard env t +let infer ~flags env t = infer flags env t -let infer_type ~chkguard env constr = - execute_type ~chkguard env constr +let infer_type ~flags env constr = + execute_type ~flags env constr -let infer_v ~chkguard env cv = - let jv = execute_array ~chkguard env cv in +let infer_v ~flags env cv = + let jv = execute_array ~flags env cv in make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 98dbefad1..1c0146bae 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -8,6 +8,7 @@ open Term open Environ +open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -18,6 +19,6 @@ open Environ *) -val infer : chkguard:bool -> env -> constr -> unsafe_judgment -val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array -val infer_type : chkguard:bool -> env -> types -> unsafe_type_judgment +val infer : flags:typing_flags -> env -> constr -> unsafe_judgment +val infer_v : flags:typing_flags -> env -> constr array -> unsafe_judgment array +val infer_type : flags:typing_flags -> env -> types -> unsafe_type_judgment diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 532287c30..fdca5ce26 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) = - if chk then +let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) = + if flags.check_guarded then let (minds, rdef) = inductive_of_mutfix env fix in let get_tree (kn,i) = let mib = Environ.lookup_mind kn env in @@ -1193,8 +1193,8 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) = - if chk then +let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) = + if flags.check_guarded then let nbfix = Array.length bodies in for i = 0 to nbfix-1 do let fixenv = push_rec_types recdef env in diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 36f32b30c..54036d86a 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -98,8 +98,8 @@ val check_case_info : env -> pinductive -> case_info -> unit (** When [chk] is false, the guard condition is not actually checked. *) -val check_fix : env -> chk:bool -> fixpoint -> unit -val check_cofix : env -> chk:bool -> cofixpoint -> unit +val check_fix : env -> flags:typing_flags -> fixpoint -> unit +val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 18d897817..2cea50d9e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env -let push_named_def ~chkguard (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with | Def c -> Mod_subst.force_constr c, senv' @@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv = let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} -let push_named_assum ~chkguard ((id,t),ctx) senv = +let push_named_assum ~flags ((id,t),ctx) senv = let senv' = push_context_set ctx senv in - let t = Term_typing.translate_local_assum ~chkguard senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (id,None,t) senv'.env in {senv' with env=env''} @@ -439,14 +439,14 @@ 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 * bool (* check guard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | 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,chkguard) -> - Term_typing.translate_constant ~chkguard senv.env kn ce + | ConstantEntry (ce,flags) -> + Term_typing.translate_constant ~flags 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 diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 80b9bb495..c5e43e42a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - chkguard:bool -> + flags:Declarations.typing_flags -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : - chkguard:bool -> + flags:Declarations.typing_flags -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* chkguard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe val add_constant : diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8a105ac97..64597469a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -23,18 +23,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type ~chkguard env j poly subst = function +let constrain_type ~flags env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) | `Some t -> - let tj = infer_type ~chkguard env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) | `SomeWJ (t, tj) -> - let tj = infer_type ~chkguard env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) @@ -101,11 +101,11 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration ~chkguard env kn dcl = +let infer_declaration ~flags env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context uctx env in - let j = infer ~chkguard env t in + let j = infer ~flags env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in @@ -122,7 +122,7 @@ let infer_declaration ~chkguard env kn dcl = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> let body = handle_side_effects env body side_eff in let env' = push_context_set ctx env in - let j = infer ~chkguard env' body in + let j = infer ~flags env' body 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,8 +143,8 @@ let infer_declaration ~chkguard env kn dcl = let body = handle_side_effects env body side_eff in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in - let j = infer ~chkguard env body in - let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let j = infer ~flags env body in + let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) @@ -186,7 +186,7 @@ let record_aux env s1 s2 = let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) = +let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) = let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -262,25 +262,25 @@ let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_ const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; - const_checked_guarded = chkguard } + const_typing_flags = flags } (*s Global and local constant declaration. *) -let translate_constant ~chkguard env kn ce = - build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce) +let translate_constant ~flags env kn ce = + build_constant_declaration ~flags kn env (infer_declaration ~flags env (Some kn) ce) -let translate_local_assum ~chkguard env t = - let j = infer ~chkguard env t in +let translate_local_assum ~flags env t = + let j = infer ~flags env t in let t = Typeops.assumption_of_judgment env j in t let translate_recipe env kn r = - build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r) + build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r) -let translate_local_def ~chkguard env id centry = +let translate_local_def ~flags env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration ~chkguard env None (DefinitionEntry centry) in + infer_declaration ~flags env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in def, typ, univs diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ba4d96a5f..f167603a7 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,10 +12,10 @@ open Environ open Declarations open Entries -val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry -> +val translate_local_def : flags:typing_flags -> env -> Id.t -> definition_entry -> constant_def * types * constant_universes -val translate_local_assum : chkguard:bool -> env -> types -> types +val translate_local_assum : flags:typing_flags -> env -> types -> types val mk_pure_proof : constr -> proof_output @@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body +val translate_constant : flags:typing_flags -> env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,11 +37,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : chkguard:bool -> env -> constant option -> +val infer_declaration : flags:typing_flags -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : - chkguard:bool -> constant -> env -> Cooking.result -> constant_body + flags:typing_flags -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9e9f18aaa..1c3117725 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -494,13 +494,13 @@ let rec execute env cstr = | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix ~chk:true env fix; + check_fix ~flags:{check_guarded=true} env fix; make_judge (mkFix fix) fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix ~chk:true env cofix; + check_cofix ~flags:{check_guarded=true} env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) diff --git a/library/assumptions.ml b/library/assumptions.ml index 463527820..f374f6dbe 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -227,7 +227,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t = | ConstRef kn -> let cb = lookup_constant kn in let accu = - if cb.const_checked_guarded then accu + if cb.const_typing_flags.check_guarded then accu else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu in if not (Declareops.constant_has_body cb) then diff --git a/library/declare.ml b/library/declare.ml index 4be13109a..c49284bbc 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in + let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let () = Global.push_named_def ~chkguard:true (id,de) in + let () = Global.push_named_def ~flags:{check_guarded=true} (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, (Univ.ContextSet.of_context de.const_entry_universes) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = - ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true) + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true}) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -232,7 +232,7 @@ let declare_sideff env fix_exn se = const_entry_feedback = None; const_entry_polymorphic = cb.const_polymorphic; const_entry_universes = univs; - }, true); + }, {check_guarded=true}); cst_hyps = [] ; cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; cst_locl = true; @@ -253,7 +253,7 @@ let declare_sideff env fix_exn se = if Constant.equal c c' then Some (x,kn) else None) inds_consts) knl)) -let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(flags={check_guarded=true}) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) = let cd = (* We deal with side effects *) match cd with | Entries.DefinitionEntry de -> @@ -275,7 +275,7 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) | _ -> cd in let cst = { - cst_decl = ConstantEntry (cd,chkguard); + cst_decl = ConstantEntry (cd,flags); cst_hyps = [] ; cst_kind = kind; cst_locl = local; @@ -283,13 +283,13 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) let kn = declare_constant_common id cst in kn -let declare_definition ?chkguard ?(internal=UserVerbose) +let declare_definition ?flags ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) ?(poly=false) id ?types (body,ctx) = let cb = definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in - declare_constant ?chkguard ~internal ~local id + declare_constant ?flags ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of inductive blocks *) @@ -387,7 +387,7 @@ let declare_projections mind = Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry, + let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true diff --git a/library/declare.mli b/library/declare.mli index 94cebe3bd..cda8855d2 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -53,11 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> constr -> definition_entry val declare_constant : - ?chkguard:bool -> (** default [true] (check guardedness) *) + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : - ?chkguard:bool -> (** default [true] (check guardedness) *) + ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant diff --git a/library/global.ml b/library/global.ml index 27f7f5266..ab326e37d 100644 --- a/library/global.ml +++ b/library/global.ml @@ -77,8 +77,8 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a) -let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d) +let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a) +let push_named_def ~flags d = globalize0 (Safe_typing.push_named_def ~flags d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) let push_context_set c = globalize0 (Safe_typing.push_context_set c) let push_context c = globalize0 (Safe_typing.push_context c) diff --git a/library/global.mli b/library/global.mli index 388fee527..f7306fe57 100644 --- a/library/global.mli +++ b/library/global.mli @@ -32,9 +32,9 @@ val set_type_in_type : unit -> unit (** Variables, Local definitions, constants, inductive types *) val push_named_assum : - chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit + flags:Declarations.typing_flags -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit val push_named_def : - chkguard:bool -> (Id.t * Entries.definition_entry) -> unit + flags:Declarations.typing_flags -> (Id.t * Entries.definition_entry) -> unit val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ced2da7a5..3ad5e77fc 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -219,13 +219,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in VernacInductive (check_positivity a,priv,f,indl) | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (check_guardedness a,None, recs) + VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs) | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (check_guardedness a,Some Discharge, recs) + VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs) | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (check_guardedness a,None, corecs) + VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs) | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (check_guardedness a,Some Discharge, corecs) + VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 53ec304cc..91fcb3f8b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 5c849ba41..0ea90ecd1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) (((_,fname),_,_,_,_),_) -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index efea4bec8..930b0413e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -593,9 +593,9 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix ~chk:true e cofix + Inductive.check_cofix ~flags:{check_guarded=true} e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix ~chk:true e fix + Inductive.check_fix ~flags:{check_guarded=true} e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index d9f490ba5..8fbcc8e5e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~chk:true fix + (try check_fix env ~flags:{Declarations.check_guarded=true} fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env ~chk:true fix; raise (Found indexes) + try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~chk:true cofix + (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0bb2979c2..fa6fd9677 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env ~chk:true fix; + check_fix env ~flags:{Declarations.check_guarded=true} fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env ~chk:true cofix; + check_cofix env ~flags:{Declarations.check_guarded=true} cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 93cd35472..8a8521ccc 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -806,7 +806,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (chkguard,local, recs) -> + | VernacFixpoint (flags,local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -821,11 +821,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (chkguard,local, corecs) -> + | VernacCoFixpoint (flags,local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -838,7 +838,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> diff --git a/toplevel/command.ml b/toplevel/command.ml index c6d67b13a..b6dd2718f 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 7578e26c1..73f8f9806 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 a0af1d573..40dfa1b9a 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 -- cgit v1.2.3 From 4d239ab9f096843dc1c78744dfc9b316ab49d6d9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Wed, 15 Jun 2016 19:19:58 +0200 Subject: Allow `Pretyping.search_guard` to not check guard This is a minimal modification to the pretyping interface which allows for toplevel fixed points to be accepted by the pretyper. Toplevel co-fixed points are accepted without this. However (co-)fixed point _nested_ inside a `Definition` or a `Fixpoint` are always checked for guardedness by the pretyper. --- pretyping/pretyping.ml | 21 +++++++++++++++++---- pretyping/pretyping.mli | 2 +- stm/lemmas.ml | 2 +- toplevel/command.ml | 6 ++++-- toplevel/obligations.ml | 3 ++- 5 files changed, 25 insertions(+), 9 deletions(-) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8fbcc8e5e..c86a4e3e4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -68,14 +68,17 @@ open Inductiveops exception Found of int array -let search_guard loc env possible_indexes fixdefs = +(* spiwack: I chose [tflags] rather than [flags], like in the rest of + the code, for the argument name to avoid interference with the + argument for [inference_flags] also used in this module. *) +let search_guard ~tflags loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env ~flags:{Declarations.check_guarded=true} fix + (try check_fix env ~flags:tflags fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -87,7 +90,13 @@ let search_guard loc env possible_indexes fixdefs = List.iter (fun l -> let indexes = Array.of_list l in - let fix = ((indexes, 0),fixdefs) in + let fix = ((indexes, 0),fixdefs) in + (* spiwack: We search for a unspecified structural + argument under the assumption that we need to check the + guardedness condition (otherwise the first inductive argument + will be chosen). A more robust solution may be to raise an + error when totality is assumed but the strutural argument is + not specified. *) try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); @@ -533,7 +542,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var vn) in let fixdecls = (names,ftys,fdefs) in - let indexes = search_guard loc env possible_indexes fixdecls in + let indexes = + search_guard + ~tflags:{Declarations.check_guarded=true} + loc env possible_indexes fixdecls + in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 142b54513..1ef3da150 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Misctypes (** An auxiliary function for searching for fixpoint guard indexes *) -val search_guard : +val search_guard : tflags:Declarations.typing_flags -> Loc.t -> env -> int list list -> rec_declaration -> int array type typing_constraint = OfType of types | IsType | WithoutTypeConstraint diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c766f3fab..1d591e1be 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -76,7 +76,7 @@ let adjust_guardness_conditions const = function List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Declareops.uniquize_side_effects eff) in let indexes = - search_guard Loc.ghost env + search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env possible_indexes fixdecls in (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } diff --git a/toplevel/command.ml b/toplevel/command.ml index b6dd2718f..c4f0b7b17 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1065,7 +1065,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let env = Global.env() in - let indexes = search_guard Loc.ghost env indexes fixdecls in + let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in let fiximps = List.map (fun (n,r,p) -> r) fiximps in let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in let fixdecls = @@ -1169,7 +1169,9 @@ let do_program_recursive local p fixkind fixl ntns = Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) in let indexes = - Pretyping.search_guard Loc.ghost (Global.env ()) possible_indexes fixdecls in + Pretyping.search_guard + ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env ~flags:{Declarations.check_guarded=true} diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9df5a411b..ec58392d5 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -582,7 +582,8 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard Loc.ghost (Global.env()) + Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, List.map_i (fun i _ -> -- cgit v1.2.3 From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 5 Jun 2016 21:50:22 +0200 Subject: Remove the syntax changes introduced by this branch. We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6. --- ide/coq.lang | 4 +--- intf/vernacexpr.mli | 6 +---- parsing/g_vernac.ml4 | 40 +++++++++------------------------ plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 4 ++-- printing/ppvernac.ml | 19 +++++----------- stm/texmacspp.ml | 6 ++--- stm/vernac_classifier.ml | 6 ++--- toplevel/vernacentries.ml | 7 +++--- 9 files changed, 30 insertions(+), 64 deletions(-) diff --git a/ide/coq.lang b/ide/coq.lang index a31eadc70..c65432bdb 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -29,13 +29,12 @@ (\%{ident}\.)*\%{ident} \.(\s|\z) ([-+*]+|{)(\s|\z)|}(\s*})* - (?'gal0'Assume)\%{space}\[\%{ident}*\]\%{space} Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)? ((Local|Global)\%{space})? Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property Qed|Defined|Admitted|Abort|Save - ((\%{assume})?(?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) + ((?'gal'\%{locality}(Program\%{space})?(\%{single_decl}|\%{begin_proof}))\%{space}(?'id'\%{ident}))|((?'gal4list'\%{mult_decl})(?'id_list'(\%{space}\%{ident})*))|(?'gal2'Goal) @@ -107,7 +106,6 @@ \%{dot_sep} - diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 2f2f97376..d7b269a1d 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -303,14 +303,10 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * simple_binder with_coercion list - | VernacInductive of - bool (*[false] => assume positive*) * - private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - Declarations.typing_flags * locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - Declarations.typing_flags * locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3ad5e77fc..e8a1b512c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -71,19 +71,6 @@ let make_bullet s = | '*' -> Star n | _ -> assert false -type nl_assumption = - | Positive - | Guarded -let eq_nl_assumption x y = - match x,y with - | Positive,Positive -> true - | Guarded,Guarded -> true - | _ , _ -> false -let check_positivity l = - not (List.mem_f eq_nl_assumption Positive l) -let check_guardedness l = - not (List.mem_f eq_nl_assumption Guarded l) - let default_command_entry = Gram.Entry.of_parser "command_entry" (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm) @@ -213,19 +200,19 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), id, b) (* Gallina inductive declarations *) - | priv = private_token; a = assume_token; f = finite_token; + | priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> let (k,f) = f in let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in - VernacInductive (check_positivity a,priv,f,indl) - | "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint ({Declarations.check_guarded=check_guardedness a},None, recs) - | IDENT "Let"; "Fixpoint"; a=assume_token; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, recs) - | "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},None, corecs) - | IDENT "Let"; "CoFixpoint"; a=assume_token; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint ({Declarations.check_guarded=check_guardedness a},Some Discharge, corecs) + VernacInductive (priv,f,indl) + | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (None, recs) + | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> + VernacFixpoint (Some Discharge, recs) + | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (None, corecs) + | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> + VernacCoFixpoint (Some Discharge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) @@ -282,13 +269,6 @@ GEXTEND Gram | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; - assume_token: - [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ] - ; - nl_assumption: - [ [ IDENT "Positive" -> Positive - | IDENT "Guarded" -> Guarded ] ] - ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 91fcb3f8b..61f03d6f2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint({Declarations.check_guarded=true},None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index b4febba66..f1c379ecc 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1435,7 +1435,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1450,7 +1450,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ Errors.print reraise in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8a8521ccc..832c08fe0 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -399,15 +399,6 @@ module Make | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i - let pr_assume ?(positive=false) ?(guarded=false) () = - let assumed = - (if guarded then [str"Guarded"] else []) @ - (if positive then [str"Positive"] else []) - in - match assumed with - | [] -> mt () - | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc() - (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -770,7 +761,7 @@ module Make (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) ) - | VernacInductive (chk,p,f,l) -> + | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -806,7 +797,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (flags,local, recs) -> + | VernacFixpoint (local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -821,11 +812,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (flags,local, corecs) -> + | VernacCoFixpoint (local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -838,7 +829,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 4f014be2d..9edc1f1c7 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -580,7 +580,7 @@ let rec tmpp v loc = let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs - | VernacInductive (_,_, _, iednll) -> + | VernacInductive (_, _, iednll) -> let kind = let (_, _, _, k, _),_ = List.hd iednll in begin @@ -598,14 +598,14 @@ let rec tmpp v loc = (fun (ie, dnl) -> (pp_inductive_expr ie) @ (List.map pp_decl_notation dnl)) iednll) in xmlInductive kind loc exprs - | VernacFixpoint (_,_, fednll) -> + | VernacFixpoint (_, fednll) -> let exprs = List.flatten (* should probably not be flattened *) (List.map (fun (fe, dnl) -> (pp_fixpoint_expr fe) @ (List.map pp_decl_notation dnl)) fednll) in xmlFixpoint exprs - | VernacCoFixpoint (_,_, cfednll) -> + | VernacCoFixpoint (_, cfednll) -> (* Nota: it is like VernacFixpoint without so could be merged *) let exprs = List.flatten (* should probably not be flattened *) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 574cc0044..2b5eb8683 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -125,14 +125,14 @@ let rec classify_vernac e = CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,_,l) -> + | VernacFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,_,l) -> + | VernacCoFixpoint (_,l) -> let ids, open_proof = List.fold_left (fun (l,b) (((_,id),_,_,p),_) -> id::l, b || p = None) ([],false) l in @@ -144,7 +144,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in VtSideff ids, VtLater | VernacDefinition (_,(_,id),DefineBody _) -> VtSideff [id], VtLater - | VernacInductive (_,_,_,l) -> + | VernacInductive (_,_,l) -> let ids = List.map (fun (((_,(_,id)),_,_,_,cl),_) -> id :: match cl with | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 40dfa1b9a..a5e771d75 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1856,6 +1856,7 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () +let all_checks = { Declarations.check_guarded = true } (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands @@ -1894,9 +1895,9 @@ let interp ?proof locality poly c = | VernacEndProof e -> vernac_end_proof ?proof e | 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 (flags,local, l) -> vernac_fixpoint ~flags locality poly local l - | VernacCoFixpoint (flags,local, l) -> vernac_cofixpoint ~flags locality poly local l + | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l + | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l + | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe l -- cgit v1.2.3 From 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 15 Jun 2016 12:16:18 +0200 Subject: Fixing the checker. This is a stupid fix that only allows to take into account the change in memory layout. The check will simply fail when encountering a unguarded inductive or (co)fixpoint. --- checker/cic.mli | 13 ++++++++++++- checker/values.ml | 8 ++++++-- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/checker/cic.mli b/checker/cic.mli index 82eb35bcb..cac2384fc 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -208,6 +208,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; @@ -216,7 +225,9 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; +} (** {6 Representation of mutual inductive types } *) diff --git a/checker/values.ml b/checker/values.ml index cf56bbd98..5f67b17d3 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 6f563f1f75706b28e5d3e3ef59e1681c checker/cic.mli +MD5 27a5893c01d6f80e7a8741ef98874e63 checker/cic.mli *) @@ -208,6 +208,9 @@ let v_projbody = v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|]; v_constr|] +let v_typing_flags = + v_tuple "typing_flags" [|v_bool|] + let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; @@ -216,7 +219,8 @@ let v_cb = v_tuple "constant_body" v_bool; v_context; Opt v_projbody; - v_bool|] + v_bool; + v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) [|[|v_ind|] (* Mrec *);[|v_ind|] (* Imbr *)|] -- cgit v1.2.3