diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-17 20:26:35 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
commit | ecb032467557631ea60324c6afa55c91c133e40d (patch) | |
tree | 831803ca1db0e73ec3cea91c52f5f2e288d12341 | |
parent | 53ced0735f7e24735d78a02fc74588b8d9186eab (diff) |
Reuse the typing_flags datatype for inductives.
-rw-r--r-- | kernel/declarations.mli | 5 | ||||
-rw-r--r-- | kernel/declareops.ml | 3 | ||||
-rw-r--r-- | kernel/entries.mli | 2 | ||||
-rw-r--r-- | kernel/environ.ml | 3 | ||||
-rw-r--r-- | kernel/environ.mli | 1 | ||||
-rw-r--r-- | kernel/indtypes.ml | 9 | ||||
-rw-r--r-- | library/declare.ml | 2 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 2 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 2 | ||||
-rw-r--r-- | toplevel/assumptions.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 13 | ||||
-rw-r--r-- | toplevel/command.mli | 2 | ||||
-rw-r--r-- | toplevel/discharge.ml | 1 | ||||
-rw-r--r-- | toplevel/indschemes.ml | 2 | ||||
-rw-r--r-- | toplevel/record.ml | 18 | ||||
-rw-r--r-- | toplevel/record.mli | 2 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 19 |
17 files changed, 38 insertions, 50 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ef4d398c1..f89773fcc 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -190,11 +190,8 @@ type mutual_inductive_body = { mind_universes : Univ.universe_context; (** Local universe variables and constraints *) 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. *) - - mind_unsafe_universes : bool; (** generated with the type-in-type flag *) + mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *) } (** {6 Module declarations } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 5caf052ac..211e5e062 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -261,8 +261,7 @@ let subst_mind_body sub mib = mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; mind_private = mib.mind_private; - mind_checked_positive = mib.mind_checked_positive; - mind_unsafe_universes = mib.mind_unsafe_universes; + mind_typing_flags = mib.mind_typing_flags; } let inductive_instance mib = diff --git a/kernel/entries.mli b/kernel/entries.mli index 8b29e3abd..df2c4653f 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -52,8 +52,6 @@ type mutual_inductive_entry = { mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; mind_entry_private : bool option; - mind_entry_check_positivity : bool; - (** [false] if positivity is to be assumed. *) } (** {6 Constants (Definition/Axiom) } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 65aaa3f7b..9fb3bf79f 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -53,6 +53,7 @@ let is_impredicative_set env = | _ -> false let type_in_type env = not (typing_flags env).check_universes +let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context @@ -362,7 +363,7 @@ let polymorphic_pind (ind,u) env = else polymorphic_ind ind env let type_in_type_ind (mind,i) env = - (lookup_mind mind env).mind_unsafe_universes + not (lookup_mind mind env).mind_typing_flags.check_universes let template_polymorphic_ind (mind,i) env = match (lookup_mind mind env).mind_packets.(i).mind_arity with diff --git a/kernel/environ.mli b/kernel/environ.mli index 0edcb34de..b5e576435 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -53,6 +53,7 @@ val engagement : env -> engagement val typing_flags : env -> typing_flags val is_impredicative_set : env -> bool val type_in_type : env -> bool +val deactivated_guard : env -> bool (** is the local context empty *) val empty_context : env -> bool diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 34771034c..b6942e133 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -816,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) 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 paramsctxt kn isrecord isfinite inds nmr recargs is_checked = +let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -922,8 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_polymorphic = p; mind_universes = ctx; mind_private = prv; - mind_checked_positive = is_checked; - mind_unsafe_universes = type_in_type env; + mind_typing_flags = Environ.typing_flags env; } (************************************************************************) @@ -932,11 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in - let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) + let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs chkpos + inds nmr recargs diff --git a/library/declare.ml b/library/declare.ml index 4e9e68dff..f809e9742 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -354,7 +354,7 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; mind_entry_private = None; - mind_entry_check_positivity = true; }) +}) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index f69c4d821..c424fe122 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1432,7 +1432,7 @@ let do_build_inductive (* in *) let _time2 = System.get_time () in try - with_full_print (Flags.silently (Command.do_mutual_inductive true rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite + with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index a78eb1af7..99a165044 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -887,7 +887,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,pl,impls = Command.interp_mutual_inductive true indl [] + let mie,pl,impls = Command.interp_mutual_inductive 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 pl impls) diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml index 921c4a1d8..fb32ecac3 100644 --- a/toplevel/assumptions.ml +++ b/toplevel/assumptions.ml @@ -307,7 +307,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = accu | IndRef (m,_) | ConstructRef ((m,_),_) -> let mind = Global.lookup_mind m in - if mind.mind_checked_positive then + if mind.mind_typing_flags.check_guarded then accu else let l = try Refmap_env.find obj ax2ty with Not_found -> [] in diff --git a/toplevel/command.ml b/toplevel/command.ml index 643b06660..5041d78a3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -549,7 +549,7 @@ let check_param = function | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () -let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -631,7 +631,7 @@ let interp_mutual_inductive chk (paramsl,indl) notations poly prv finite = mind_entry_polymorphic = poly; mind_entry_private = if prv then Some false else None; mind_entry_universes = uctx; - mind_entry_check_positivity = chk; }, + }, pl, impls (* Very syntactical equality *) @@ -716,19 +716,18 @@ type one_inductive_impls = Impargs.manual_explicitation list (* for inds *)* Impargs.manual_explicitation list list (* for constrs *) -let do_mutual_inductive chk indl poly prv finite = +let do_mutual_inductive indl poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive chk indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in (* Declare the mutual inductive block with its associated schemes *) ignore (declare_mutual_inductive_with_eliminations mie pl impls); (* 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; - (* If [chk] is [false] (i.e. positivity is assumed) declares itself - as unsafe. *) - if not chk then Feedback.feedback Feedback.AddedAxiom else () + (* If positivity is assumed declares itself as unsafe. *) + if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () (* 3c| Fixpoints and co-fixpoints *) diff --git a/toplevel/command.mli b/toplevel/command.mli index a5132cc66..d35372429 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -91,7 +91,6 @@ 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 * Universes.universe_binders * one_inductive_impls list @@ -106,7 +105,6 @@ 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/discharge.ml b/toplevel/discharge.ml index 74361eb1c..fcb260f51 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -117,5 +117,4 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_polymorphic = mib.mind_polymorphic; mind_entry_private = mib.mind_private; mind_entry_universes = univs; - mind_entry_check_positivity = mib.mind_checked_positive; } diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index a43758e3c..a48bbf89d 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -497,7 +497,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) && mib.mind_checked_positive then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded 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 214d44d83..c9b46983e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -361,7 +361,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure chk finite poly ctx id idbuild paramimpls params arity template +let declare_structure 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 = Context.Rel.to_extended_list nfields params in @@ -387,7 +387,8 @@ let declare_structure chk finite poly ctx id idbuild paramimpls params arity tem mind_entry_polymorphic = poly; mind_entry_private = None; mind_entry_universes = ctx; - mind_entry_check_positivity = chk; } in + } + 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 @@ -406,7 +407,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map get_name ctx))) -let declare_class chk finite def poly ctx id idbuild paramimpls params arity +let declare_class 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. *) @@ -449,7 +450,7 @@ let declare_class chk finite def poly ctx id idbuild paramimpls params arity in cref, [Name proj_name, sub, Some proj_cst] | _ -> - let ind = declare_structure chk BiFinite poly ctx (snd id) idbuild paramimpls + let ind = declare_structure 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 @@ -528,9 +529,8 @@ 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. When [chk] is false positivity is - assumed. *) -let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = + or subinstances. *) +let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),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 @@ -551,14 +551,14 @@ let definition_structure chk (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf let sign = structure_signature (fields@params) in let gr = match kind with | Class def -> - let gr = declare_class chk finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class 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 chk finite poly ctx idstruc + let ind = declare_structure 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 525326237..b09425563 100644 --- a/toplevel/record.mli +++ b/toplevel/record.mli @@ -25,7 +25,6 @@ val declare_projections : (Name.t * bool) list * constant option list val declare_structure : - bool -> (** check positivity? *) Decl_kinds.recursivity_kind -> bool (** polymorphic?*) -> Univ.universe_context -> Id.t -> Id.t -> @@ -39,7 +38,6 @@ val declare_structure : inductive val definition_structure : - bool -> (** check positivity? *) inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident 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 29d6d7acd..82fe9751e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -519,7 +519,7 @@ let vernac_assumption locality poly (local, kind) l nl = let status = do_assumptions kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_record chk k poly finite struc binders sort nameopt cfs = +let vernac_record k poly finite struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -530,14 +530,13 @@ let vernac_record chk 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 chk (k,poly,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (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] +(** 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 = +let vernac_inductive poly lo finite indl = if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -553,14 +552,14 @@ let vernac_inductive chk 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 chk (match b with Class true -> Class false | _ -> b) + vernac_record (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 chk (Class true) poly finite id bl c None [f] + in vernac_record (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 _), _ ] -> @@ -574,7 +573,7 @@ let vernac_inductive chk poly lo finite indl = | _ -> Errors.error "Cannot handle mutually (co)inductive records." in let indl = List.map unpack indl in - do_mutual_inductive chk indl poly lo finite + do_mutual_inductive indl poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1767,7 +1766,7 @@ let interp ?proof ~loc 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 true poly priv finite l + | VernacInductive (priv,finite,l) -> vernac_inductive 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 |