diff options
| -rw-r--r-- | API/API.mli | 8 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 10 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 23 |
6 files changed, 46 insertions, 14 deletions
diff --git a/API/API.mli b/API/API.mli index 19726b52f2..d39d3cb25c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3780,6 +3780,12 @@ sig | DefaultInline | InlineAt of int + type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located @@ -3804,7 +3810,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 6ef9532ad7..2adf522b74 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -305,6 +305,14 @@ type inline = type module_ast_inl = module_ast * inline type module_binder = bool option * lident list * module_ast_inl +(** Cumulativity can be set globally, locally or unset locally and it + can not enabled at all. *) +type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + (** {6 The type of vernacular expressions} *) type vernac_expr = @@ -336,7 +344,7 @@ type vernac_expr = | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * inline * (plident list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * 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 568818c270..93a778274d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -168,8 +168,13 @@ GEXTEND Gram let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in let cum = match cum with - Some b -> b - | None -> Flags.is_polymorphic_inductive_cumulativity () + Some true -> LocalCumulativity + | Some false -> LocalNonCumulativity + | None -> + if Flags.is_polymorphic_inductive_cumulativity () then + GlobalCumulativity + else + GlobalNonCumulativity in VernacInductive (cum, priv,f,indl) | "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 379c83b245..e3010e3b53 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1471,7 +1471,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1486,7 +1486,7 @@ let do_build_inductive in let msg = str "while trying to define"++ spc () ++ - Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds)) + Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Vernacexpr.GlobalNonCumulativity,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a68b569cbe..4c50c2f368 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -760,7 +760,11 @@ open Decl_kinds | Class _ -> "Class" | Variant -> "Variant" in if p then - let cm = if cum then "Cumulative" else "NonCumulative" in + let cm = + match cum with + | GlobalCumulativity | LocalCumulativity -> "Cumulative" + | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + in cm ^ " " ^ kind else kind in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 12a31953c5..1556beb060 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -522,12 +522,21 @@ 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 check_cumulativity_polymorphism_flag cum poly = - if cum && not poly then - user_err Pp.(str "Monomorphic cumulative inductive types/records are not supported. ") +let should_treat_as_cumulative cum poly = + if poly then + match cum with + | GlobalCumulativity | LocalCumulativity -> true + | GlobalNonCumulativity | LocalNonCumulativity -> false + else + match cum with + | GlobalCumulativity | GlobalNonCumulativity -> false + | LocalCumulativity -> + user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.") + | LocalNonCumulativity -> + user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.") let vernac_record cum k poly finite struc binders sort nameopt cfs = - check_cumulativity_polymorphism_flag cum poly; + let is_cumulative = should_treat_as_cumulative cum poly in let const = match nameopt with | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> @@ -538,14 +547,14 @@ let vernac_record cum 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,cum,poly,finite,struc,binders,cfs,const,sort)) + ignore(Record.definition_structure (k,is_cumulative,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 cum poly lo finite indl = - check_cumulativity_polymorphism_flag cum poly; + let is_cumulative = should_treat_as_cumulative cum poly in if Dumpglob.dump () then List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with @@ -582,7 +591,7 @@ let vernac_inductive cum 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 cum poly lo finite + do_mutual_inductive indl is_cumulative poly lo finite let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in |