From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- vernac/command.ml | 7 ++++--- vernac/command.mli | 10 +++++----- vernac/discharge.ml | 1 + vernac/record.ml | 13 +++++++------ vernac/record.mli | 7 ++++--- vernac/vernacentries.ml | 28 +++++++++++++++++++++------- 6 files changed, 42 insertions(+), 24 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 6c5997623..2345cb4c5 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -573,7 +573,7 @@ let check_param = function | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false -let interp_mutual_inductive (paramsl,indl) notations poly prv finite = +let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = check_all_names_different indl; List.iter check_param paramsl; let env0 = Global.env() in @@ -657,6 +657,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = mind_entry_finite = finite; mind_entry_inds = entries; mind_entry_polymorphic = poly; + mind_entry_cumulative = cum; mind_entry_private = if prv then Some false else None; mind_entry_universes = ground_uinfind; } @@ -747,10 +748,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 indl cum poly prv finite = let indl,coes,ntns = extract_mutual_inductive_declaration_components indl in (* Interpret the types *) - let mie,pl,impls = interp_mutual_inductive indl ntns poly prv finite in + let mie,pl,impls = interp_mutual_inductive indl ntns cum 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 *) diff --git a/vernac/command.mli b/vernac/command.mli index 2a52d9bcb..a636bc03c 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -90,9 +90,9 @@ type one_inductive_impls = Impargs.manual_implicits list (** for constrs *) val interp_mutual_inductive : - structured_inductive_expr -> decl_notation list -> polymorphic -> - private_flag -> Decl_kinds.recursivity_kind -> - mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list + structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its associated schemes *) @@ -104,8 +104,8 @@ val declare_mutual_inductive_with_eliminations : (** Entry points for the vernacular commands Inductive and CoInductive *) val do_mutual_inductive : - (one_inductive_expr * decl_notation list) list -> polymorphic -> - private_flag -> Decl_kinds.recursivity_kind -> unit + (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> + polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/vernac/discharge.ml b/vernac/discharge.ml index c7a741c13..738e27f63 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -116,6 +116,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib = mind_entry_params = params'; mind_entry_inds = inds'; mind_entry_polymorphic = mib.mind_polymorphic; + mind_entry_cumulative = mib.mind_cumulative; mind_entry_private = mib.mind_private; mind_entry_universes = univ_info_ind } diff --git a/vernac/record.ml b/vernac/record.ml index 093a31c19..8a83dceef 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -377,7 +377,7 @@ let structure_signature ctx = open Typeclasses -let declare_structure finite poly ctx id idbuild paramimpls params arity template +let declare_structure finite cum 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 mkRel nfields params in @@ -401,6 +401,7 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat mind_entry_finite = finite; mind_entry_inds = [mie_ind]; mind_entry_polymorphic = poly; + mind_entry_cumulative = cum; mind_entry_private = None; mind_entry_universes = ctx; } @@ -435,7 +436,7 @@ let implicits_of_context ctx = in ExplByPos (i, explname), (true, true, true)) 1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx))) -let declare_class finite def poly ctx id idbuild paramimpls params arity +let declare_class finite def cum 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. *) @@ -478,7 +479,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 (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls + let ind = declare_structure BiFinite cum poly (Universes.univ_inf_ind_from_universe_context ctx) (snd id) idbuild paramimpls params arity template fieldimpls fields ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign in @@ -552,7 +553,7 @@ 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),pl)),ps,cfs,idbuild,s) = +let definition_structure (kind,cum,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 @@ -576,14 +577,14 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id let gr = match kind with | Class def -> let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in - let gr = declare_class finite def poly ctx (loc,idstruc) idbuild + let gr = declare_class finite def cum 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 (Universes.univ_inf_ind_from_universe_context ctx) idstruc + let ind = declare_structure Finite cum poly (Universes.univ_inf_ind_from_universe_context 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/vernac/record.mli b/vernac/record.mli index ec5d2cf83..c43d833b0 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -26,7 +26,8 @@ val declare_projections : val declare_structure : Decl_kinds.recursivity_kind -> - bool (** polymorphic?*) -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Univ.universe_info_ind (** universe and subtyping constraints *) -> Id.t -> Id.t -> manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *) @@ -39,8 +40,8 @@ val declare_structure : inductive val definition_structure : - inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * - plident with_coercion * local_binder_expr list * + inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * + Decl_kinds.recursivity_kind * plident with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d0f9c7de7..f130708c4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -526,7 +526,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 k poly finite struc binders sort nameopt cfs = +let vernac_record cum 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) -> @@ -537,13 +537,13 @@ 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)) + ignore(Record.definition_structure (k,cum,poly,finite,struc,binders,cfs,const,sort)) (** 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 poly lo finite indl = +let vernac_inductive cum poly lo finite indl = if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -559,14 +559,14 @@ let vernac_inductive poly lo finite indl = | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> user_err Pp.(str "The Variant keyword does not support syntax { ... }.") | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record (match b with Class _ -> Class false | _ -> b) + vernac_record cum (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs | [ ( id , bl , c , Class _, 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 cum (Class true) poly finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") | [ ( id , bl , c , Class _, _), _ :: _ ] -> @@ -580,7 +580,7 @@ let vernac_inductive poly lo finite indl = | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.") in let indl = List.map unpack indl in - do_mutual_inductive indl poly lo finite + do_mutual_inductive indl cum poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in @@ -1364,6 +1364,14 @@ let _ = optread = Flags.is_universe_polymorphism; optwrite = Flags.make_universe_polymorphism } +let _ = + declare_bool_option + { optdepr = false; + optname = "inductive cumulativity"; + optkey = ["Inductive"; "Cumulativity"]; + optread = Flags.is_universe_polymorphism; + optwrite = Flags.make_universe_polymorphism } + let _ = declare_int_option { optdepr = false; @@ -1933,7 +1941,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 poly priv finite l + | VernacInductive (cum, priv,finite,l) -> vernac_inductive cum 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 @@ -2083,6 +2091,12 @@ let enforce_polymorphism = function | None -> Flags.is_universe_polymorphism () | Some b -> Flags.make_polymorphic_flag b; b +let check_vernac_supports_cumulativity c p = + match p, c with + | None, _ -> () + | Some _, (VernacInductive _ ) -> () + | Some _, _ -> CErrors.error "This command does not support Cumulativity" + (** A global default timeout, controlled by option "Set Default Timeout n". Use "Unset Default Timeout" to deactivate it (or set it to 0). *) -- cgit v1.2.3