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 --- API/API.mli | 12 +- ide/texmacspp.ml | 769 ++++++++++++++++++++++++++++++++ intf/decl_kinds.ml | 4 +- intf/vernacexpr.ml | 2 +- kernel/declarations.ml | 2 + kernel/declareops.ml | 1 + kernel/entries.mli | 3 +- kernel/indtypes.ml | 7 +- kernel/reduction.ml | 190 +++++--- kernel/reduction.mli | 11 +- lib/flags.ml | 4 + lib/flags.mli | 4 + library/declare.ml | 4 +- parsing/g_vernac.ml4 | 14 +- plugins/funind/glob_term_to_relation.ml | 8 +- plugins/funind/merge.ml | 2 +- pretyping/evarconv.ml | 2 + pretyping/reductionops.ml | 64 ++- printing/ppvernac.ml | 14 +- stm/vernac_classifier.ml | 2 +- test-suite/bugs/closed/3330.v | 11 +- test-suite/success/polymorphism.v | 52 ++- vernac/command.ml | 7 +- vernac/command.mli | 10 +- vernac/discharge.ml | 1 + vernac/record.ml | 13 +- vernac/record.mli | 7 +- vernac/vernacentries.ml | 28 +- 28 files changed, 1093 insertions(+), 155 deletions(-) create mode 100644 ide/texmacspp.ml diff --git a/API/API.mli b/API/API.mli index a4ae6347c..a993b0277 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1095,6 +1095,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; + mind_cumulative : bool; mind_universes : Univ.universe_info_ind; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; @@ -1907,6 +1908,7 @@ end module Decl_kinds : sig type polymorphic = bool + type cumulative_inductive_flag = bool type recursivity_kind = Decl_kinds.recursivity_kind = | Finite | CoFinite @@ -2388,7 +2390,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.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of Decl_kinds.cumulative_inductive_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 @@ -4743,7 +4745,9 @@ sig type one_inductive_impls = Command.one_inductive_impls val do_mutual_inductive : - (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> + (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> @@ -4767,7 +4771,9 @@ sig structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list val interp_mutual_inductive : - structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic -> + structured_inductive_expr -> Vernacexpr.decl_notation list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml new file mode 100644 index 000000000..8409c7521 --- /dev/null +++ b/ide/texmacspp.ml @@ -0,0 +1,769 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (List.filter (fun (a,_) -> a = attr) attrs) + | _ -> []) + xml_list in + match List.flatten attrs_list with + | [] -> (attr, "") + | l -> (List.hd l) + +let backstep_loc xmllist = + let start_att = get_fst_attr_in_xml_list "begin" xmllist in + let stop_att = get_fst_attr_in_xml_list "end" (List.rev xmllist) in + [start_att ; stop_att] + +let compare_begin_att xml1 xml2 = + let att1 = get_fst_attr_in_xml_list "begin" [xml1] in + let att2 = get_fst_attr_in_xml_list "begin" [xml2] in + match att1, att2 with + | (_, s1), (_, s2) when s1 == "" || s2 == "" -> 0 + | (_, s1), (_, s2) when int_of_string s1 > int_of_string s2 -> 1 + | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1 + | _ -> 0 + +let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] [] + +let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] [] + +let xmlThm ?loc typ name xml = + xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml + +let xmlDef ?loc typ name xml = + xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml + +let xmlNotation ?loc attr name xml = + xmlWithLoc ?loc "notation" (("name", name) :: attr) xml + +let xmlReservedNotation ?loc attr name = + xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) [] + +let xmlCst ?loc ?(attr=[]) name = + xmlWithLoc ?loc "constant" (("name", name) :: attr) [] + +let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name = + xmlWithLoc ?loc "operator" + (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) [] + +let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml + +let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml + +let xmlTyped xml = Element("typed", (backstep_loc xml), xml) + +let xmlReturn ?(attr=[]) xml = Element("return", attr, xml) + +let xmlCase xml = Element("case", [], xml) + +let xmlScrutinee ?(attr=[]) xml = Element("scrutinee", attr, xml) + +let xmlWith xml = Element("with", [], xml) + +let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml]) + +let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml + +let xmlCoFixpoint xml = Element("cofixpoint", [], xml) + +let xmlFixpoint xml = Element("fixpoint", [], xml) + +let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml + +let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml + +let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml + +let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr [] + +let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr [] + +let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] [] + +let xmlReference ref = + let name = Libnames.string_of_reference ref in + let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in + let b, e = string_of_int i, string_of_int j in + Element("reference",["name", name; "begin", b; "end", e] ,[]) + +let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml +let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml + +let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml +let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr +let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr + +let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml + +let xmlScope ?loc ?(attr=[]) action name xml = + xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml + +let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] [] + +let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml + +let xmlSectionSubsetDescr name ssd = + Element("sectionsubsetdescr",["name",name], + [PCData (Proof_using.to_string ssd)]) + +let xmlDeclareMLModule ?loc s = + xmlWithLoc ?loc "declarexmlmodule" [] + (List.map (fun x -> Element("path",["value",x],[])) s) + +(* tactics *) +let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml + +(* toplevel commands *) +let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml + +let xmlTODO ?loc x = + xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + +let string_of_name n = + match n with + | Anonymous -> "_" + | Name id -> Id.to_string id + +let string_of_glob_sort s = + match s with + | GProp -> "Prop" + | GSet -> "Set" + | GType _ -> "Type" + +let string_of_cast_sort c = + match c with + | CastConv _ -> "CastConv" + | CastVM _ -> "CastVM" + | CastNative _ -> "CastNative" + | CastCoerce -> "CastCoerce" + +let string_of_case_style s = + match s with + | LetStyle -> "Let" + | IfStyle -> "If" + | LetPatternStyle -> "LetPattern" + | MatchStyle -> "Match" + | RegularStyle -> "Regular" + +let attribute_of_syntax_modifier sm = +match sm with + | SetItemLevel (sl, NumLevel n) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", string_of_int n] + | SetItemLevel (sl, NextLevel) -> + List.map (fun s -> ("itemlevel", s)) sl @ ["level", "next"] + | SetLevel i -> ["level", string_of_int i] + | SetAssoc a -> + begin match a with + | NonA -> ["",""] + | RightA -> ["associativity", "right"] + | LeftA -> ["associativity", "left"] + end + | SetEntryType (s, _) -> ["entrytype", s] + | SetOnlyPrinting -> ["onlyprinting", ""] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] + | SetFormat (system, (loc, s)) -> + let start, stop = unlock ?loc in + ["format-"^system, s; "begin", start; "end", stop] + +let string_of_assumption_kind l a many = + match l, a, many with + | (Discharge, Logical, true) -> "Hypotheses" + | (Discharge, Logical, false) -> "Hypothesis" + | (Discharge, Definitional, true) -> "Variables" + | (Discharge, Definitional, false) -> "Variable" + | (Global, Logical, true) -> "Axioms" + | (Global, Logical, false) -> "Axiom" + | (Global, Definitional, true) -> "Parameters" + | (Global, Definitional, false) -> "Parameter" + | (Local, Logical, true) -> "Local Axioms" + | (Local, Logical, false) -> "Local Axiom" + | (Local, Definitional, true) -> "Local Parameters" + | (Local, Definitional, false) -> "Local Parameter" + | (Global, Conjectural, _) -> "Conjecture" + | ((Discharge | Local), Conjectural, _) -> assert false + +let rec pp_bindlist bl = + let tlist = + List.flatten + (List.map + (fun (loc_names, _, e) -> + let names = + (List.map + (fun (loc, name) -> + xmlCst ?loc (string_of_name name)) loc_names) in + match e.CAst.v with + | CHole _ -> names + | _ -> names @ [pp_expr e]) + bl) in + match tlist with + | [e] -> e + | l -> xmlTyped l +and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) + Element ("decl_notation", ["name", s], [pp_expr ce]) +and pp_local_binder lb = (* don't know what it is for now *) + match lb with + | CLocalDef ((loc, nam), ce, ty) -> + let attrs = ["name", string_of_name nam] in + let value = match ty with + Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t) + | None -> ce in + pp_expr ~attr:attrs value + | CLocalAssum (namll, _, ce) -> + let ppl = + List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in + xmlTyped (ppl @ [pp_expr ce]) + | CLocalPattern _ -> + assert false +and pp_local_decl_expr lde = (* don't know what it is for now *) + match lde with + | AssumExpr (_, ce) -> pp_expr ce + | DefExpr (_, ce, _) -> pp_expr ce +and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) = + (* inductive_expr *) + let b,e = Option.cata Loc.unloc (0,0) l in + let location = ["begin", string_of_int b; "end", string_of_int e] in + [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *) + begin match cl_or_rdexpr with + | Constructors coel -> List.map (fun (_, (_, ce)) -> pp_expr ce) coel + | RecordDecl (_, ldewwwl) -> + List.map (fun (((_, x), _), _) -> pp_local_decl_expr x) ldewwwl + end @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end @ + (List.map pp_local_binder lbl) +and pp_recursion_order_expr optid roe = (* don't know what it is for now *) + let attrs = + match optid with + | None -> [] + | Some (loc, id) -> + let start, stop = unlock ?loc in + ["begin", start; "end", stop ; "name", Id.to_string id] in + let kind, expr = + match roe with + | CStructRec -> "struct", [] + | CWfRec e -> "rec", [pp_expr e] + | CMeasureRec (e, None) -> "mesrec", [pp_expr e] + | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in + Element ("recursion_order", ["kind", kind] @ attrs, expr) +and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) = + (* fixpoint_expr *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* fixpoint name *) + [pp_recursion_order_expr optid roe] @ + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) + (* Nota: it is like fixpoint_expr without (optid, roe) + * so could be merged if there is no more differences *) + let start, stop = unlock ?loc in + let id = Id.to_string id in + [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @ + (* cofixpoint name *) + (List.map pp_local_binder lbl) @ + [pp_expr ce] @ + begin match ceo with (* don't know what it is for now *) + | Some ce -> [pp_expr ce] + | None -> [] + end +and pp_lident (loc, id) = xmlCst ?loc (Id.to_string id) +and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce] +and pp_cases_pattern_expr {loc ; CAst.v = cpe} = + match cpe with + | CPatAlias (cpe, id) -> + xmlApply ?loc + (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" :: + [pp_cases_pattern_expr cpe]) + | CPatCstr (ref, None, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], []); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatCstr (ref, Some cpel1, cpel2) -> + xmlApply ?loc + (xmlOperator ?loc "reference" + ~attr:["name", Libnames.string_of_reference ref] :: + [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1)); + Element ("args", [], (List.map pp_cases_pattern_expr cpel2))]) + | CPatAtom optr -> + let attrs = match optr with + | None -> [] + | Some r -> ["name", Libnames.string_of_reference r] in + xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: []) + | CPatOr cpel -> + xmlApply ?loc (xmlOperator ?loc "or" :: List.map pp_cases_pattern_expr cpel) + | CPatNotation (n, (subst_constr, subst_rec), cpel) -> + xmlApply ?loc + (xmlOperator ?loc "notation" :: + [xmlOperator ?loc n; + Element ("subst", [], + [Element ("subterms", [], + List.map pp_cases_pattern_expr subst_constr); + Element ("recsubterms", [], + List.map + (fun (cpel) -> + Element ("recsubterm", [], + List.map pp_cases_pattern_expr cpel)) + subst_rec)]); + Element ("args", [], (List.map pp_cases_pattern_expr cpel))]) + | CPatPrim tok -> pp_token ?loc tok + | CPatRecord rcl -> + xmlApply ?loc + (xmlOperator ?loc "record" :: + List.map (fun (r, cpe) -> + Element ("field", + ["reference", Libnames.string_of_reference r], + [pp_cases_pattern_expr cpe])) + rcl) + | CPatDelimiters (delim, cpe) -> + xmlApply ?loc + (xmlOperator ?loc "delimiter" ~attr:["name", delim] :: + [pp_cases_pattern_expr cpe]) + | CPatCast _ -> assert false +and pp_case_expr (e, name, pat) = + match name, pat with + | None, None -> xmlScrutinee [pp_expr e] + | Some (loc, name), None -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] [pp_expr e] + | Some (loc, name), Some p -> + let start, stop= unlock ?loc in + xmlScrutinee ~attr:["name", string_of_name name; + "begin", start; "end", stop] + [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] + | None, Some p -> + xmlScrutinee [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e] +and pp_branch_expr_list bel = + xmlWith + (List.map + (fun (_, (cpel, e)) -> + let ppcepl = + List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in + let ppe = [pp_expr e] in + xmlCase (ppcepl @ ppe)) + bel) +and pp_token ?loc tok = + let tokstr = + match tok with + | String s -> PCData s + | Numeral n -> PCData (to_string n) in + xmlToken ?loc [tokstr] +and pp_local_binder_list lbl = + let l = (List.map pp_local_binder lbl) in + Element ("recurse", (backstep_loc l), l) +and pp_const_expr_list cel = + let l = List.map pp_expr cel in + Element ("recurse", (backstep_loc l), l) +and pp_expr ?(attr=[]) { loc; CAst.v = e } = + match e with + | CRef (r, _) -> + xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r) + | CProdN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e]) + | CApp ((_, hd), args) -> + xmlApply ?loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args) + | CAppExpl ((_, r, _), args) -> + xmlApply ?loc ~attr + (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r) + :: List.map pp_expr args) + | CNotation (notation, ([],[],[])) -> + xmlOperator ?loc notation + | CNotation (notation, (args, cell, lbll)) -> + let fmts = Notation.find_notation_extra_printing_rules notation in + let oper = xmlOperator ?loc notation ~pprules:fmts in + let cels = List.map pp_const_expr_list cell in + let lbls = List.map pp_local_binder_list lbll in + let args = List.map pp_expr args in + xmlApply ?loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls))) + | CSort(s) -> + xmlOperator ?loc (string_of_glob_sort s) + | CDelimiters (scope, ce) -> + xmlApply ?loc (xmlOperator ?loc "delimiter" ~attr:["name", scope] :: + [pp_expr ce]) + | CPrim tok -> pp_token ?loc tok + | CGeneralization (kind, _, e) -> + let kind= match kind with + | Explicit -> "explicit" + | Implicit -> "implicit" in + xmlApply ?loc + (xmlOperator ?loc ~attr:["kind", kind] "generalization" :: [pp_expr e]) + | CCast (e, tc) -> + begin match tc with + | CastConv t | CastVM t |CastNative t -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", (string_of_cast_sort tc)] :: + [pp_expr e; pp_expr t]) + | CastCoerce -> + xmlApply ?loc + (xmlOperator ?loc ":" ~attr:["kind", "CastCoerce"] :: + [pp_expr e]) + end + | CEvar (ek, cel) -> + let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in + xmlApply ?loc + (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] :: + ppcel) + | CPatVar id -> xmlPatvar ?loc (string_of_id id) + | CHole (_, _, _) -> xmlCst ?loc ~attr "_" + | CIf (test, (_, ret), th, el) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "if" :: + return @ [pp_expr th] @ [pp_expr el]) + | CLetTuple (names, (_, ret), value, body) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc "lettuple" :: + return @ + (List.map (fun (loc, var) -> xmlCst ?loc (string_of_name var)) names) @ + [pp_expr value; pp_expr body]) + | CCases (sty, ret, cel, bel) -> + let return = match ret with + | None -> [] + | Some r -> [xmlReturn [pp_expr r]] in + xmlApply ?loc + (xmlOperator ?loc ~attr:["style", (string_of_case_style sty)] "match" :: + (return @ + [Element ("scrutinees", [], List.map pp_case_expr cel)] @ + [pp_branch_expr_list bel])) + | CRecord _ -> assert false + | CLetIn ((varloc, var), value, typ, body) -> + let value = match typ with + | Some t -> + CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t)) + | None -> value in + xmlApply ?loc + (xmlOperator ?loc "let" :: + [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body]) + | CLambdaN (bl, e) -> + xmlApply ?loc + (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e]) + | CCoFix (_, _) -> assert false + | CFix (lid, fel) -> + xmlApply ?loc + (xmlOperator ?loc "fix" :: + List.flatten (List.map + (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d)) + fel)) + +let pp_comment c = + match c with + | CommentConstr e -> [pp_expr e] + | CommentString s -> [Element ("string", [], [PCData s])] + | CommentInt i -> [PCData (string_of_int i)] + +let rec tmpp ?loc v = + match v with + (* Control *) + | VernacLoad (verbose,f) -> + xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] [] + | VernacTime (loc,e) -> + xmlApply ?loc (Element("time",[],[]) :: + [tmpp ?loc e]) + | VernacRedirect (s, (loc,e)) -> + xmlApply ?loc (Element("redirect",["path", s],[]) :: + [tmpp ?loc e]) + | VernacTimeout (s,e) -> + xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) :: + [tmpp ?loc e]) + | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e]) + + (* Syntax *) + | VernacSyntaxExtension (_, ((_, name), sml)) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + xmlReservedNotation ?loc attrs name + + | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name [] + | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name [] + | VernacDelimiters (name,Some tag) -> + xmlScope ?loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope ?loc "undelimit" name ~attr:[] [] + | VernacInfix (_,((_,name),sml),ce,sn) -> + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacNotation (_, ce, (lstr, sml), sn) -> + let name = snd lstr in + let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in + let sc_attr = + match sn with + | Some scope -> ["scope", scope] + | None -> [] in + xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce] + | VernacBindScope _ as x -> xmlTODO ?loc x + | VernacNotationAddFormat _ as x -> xmlTODO ?loc x + | VernacUniverse _ + | VernacConstraint _ + | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x + (* Gallina *) + | VernacDefinition (ldk, ((_,id),_), de) -> + let l, dk = + match ldk with + | Some l, dk -> (l, dk) + | None, dk -> (Global, dk) in (* Like in ppvernac.ml, l 585 *) + let e = + match de with + | ProveBody (_, ce) -> ce + | DefineBody (_, Some _, ce, None) -> ce + | DefineBody (_, None , ce, None) -> ce + | DefineBody (_, Some _, ce, Some _) -> ce + | DefineBody (_, None , ce, Some _) -> ce in + let str_dk = Kindops.string_of_definition_kind (l, false, dk) in + let str_id = Id.to_string id in + (xmlDef ?loc str_dk str_id [pp_expr e]) + | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> + let str_tk = Kindops.string_of_theorem_kind tk in + let str_id = Id.to_string id in + (xmlThm ?loc str_tk str_id [pp_expr statement]) + | VernacStartTheoremProof _ as x -> xmlTODO ?loc x + | VernacEndProof pe -> + begin + match pe with + | Admitted -> xmlQed ?loc ?attr:None + | Proved (_, Some ((_, id), Some tk)) -> + let nam = Id.to_string id in + let typ = Kindops.string_of_theorem_kind tk in + xmlQed ?loc ~attr:["name", nam; "type", typ] + | Proved (_, Some ((_, id), None)) -> + let nam = Id.to_string id in + xmlQed ?loc ~attr:["name", nam] + | Proved _ -> xmlQed ?loc ?attr:None + end + | VernacExactProof _ as x -> xmlTODO ?loc x + | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in + let many = + List.length (List.flatten (List.map fst binders)) > 1 in + let exprs = + List.flatten (List.map pp_simple_binder binders) in + let l = match l with Some x -> x | None -> Decl_kinds.Global in + let kind = string_of_assumption_kind l a many in + xmlAssumption ?loc kind exprs + | VernacInductive (_, _, _, iednll) -> + let kind = + let (_, _, _, k, _), _ = List.hd iednll in + begin + match k with + | Record -> "Record" + | Structure -> "Structure" + | Inductive_kw -> "Inductive" + | CoInductive -> "CoInductive" + | Class _ -> "Class" + | Variant -> "Variant" + end in + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (ie, dnl) -> (pp_inductive_expr ie) @ + (List.map pp_decl_notation dnl)) iednll) in + xmlInductive ?loc kind exprs + | 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) -> + (* Nota: it is like VernacFixpoint without so could be merged *) + let exprs = + List.flatten (* should probably not be flattened *) + (List.map + (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @ + (List.map pp_decl_notation dnl)) cfednll) in + xmlCoFixpoint exprs + | VernacScheme _ as x -> xmlTODO ?loc x + | VernacCombinedScheme _ as x -> xmlTODO ?loc x + + (* Gallina extensions *) + | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id) + | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id) + | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x + | VernacRequire (from, import, l) -> + let import = match import with + | None -> [] + | Some true -> ["export","true"] + | Some false -> ["import","true"] + in + let from = match from with + | None -> [] + | Some r -> ["from", Libnames.string_of_reference r] + in + xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (true,l) -> + xmlImport ?loc ~attr:["export","true"] (List.map (fun ref -> + xmlReference ref) l) + | VernacImport (false,l) -> + xmlImport ?loc (List.map (fun ref -> xmlReference ref) l) + | VernacCanonical r -> + let attr = + match r with + | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q] + | AN (Ident (_, id)) -> ["id", Id.to_string id] + | ByNotation (_, (s, _)) -> ["notation", s] in + xmlCanonicalStructure ?loc attr + | VernacCoercion _ as x -> xmlTODO ?loc x + | VernacIdentityCoercion _ as x -> xmlTODO ?loc x + + (* Type classes *) + | VernacInstance _ as x -> xmlTODO ?loc x + + | VernacContext _ as x -> xmlTODO ?loc x + + | VernacDeclareInstances _ as x -> xmlTODO ?loc x + + | VernacDeclareClass _ as x -> xmlTODO ?loc x + + (* Modules and Module Types *) + | VernacDeclareModule _ as x -> xmlTODO ?loc x + | VernacDefineModule _ as x -> xmlTODO ?loc x + | VernacDeclareModuleType _ as x -> xmlTODO ?loc x + | VernacInclude _ as x -> xmlTODO ?loc x + + (* Solving *) + + | (VernacSolveExistential _) as x -> + xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Auxiliary file and library management *) + | VernacAddLoadPath (recf,name,None) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacAddLoadPath (recf,name,Some dp) -> + xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] + [PCData (Names.DirPath.to_string dp)] + | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] [] + | VernacAddMLPath (recf,name) -> + xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] [] + | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl + | VernacChdir _ as x -> xmlTODO ?loc x + + (* State management *) + | VernacWriteState _ as x -> xmlTODO ?loc x + | VernacRestoreState _ as x -> xmlTODO ?loc x + + (* Resetting *) + | VernacResetName _ as x -> xmlTODO ?loc x + | VernacResetInitial as x -> xmlTODO ?loc x + | VernacBack _ as x -> xmlTODO ?loc x + | VernacBackTo _ -> PCData "VernacBackTo" + + (* Commands *) + | VernacCreateHintDb _ as x -> xmlTODO ?loc x + | VernacRemoveHints _ as x -> xmlTODO ?loc x + | VernacHints _ as x -> xmlTODO ?loc x + | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) -> + let name = Id.to_string name in + let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in + xmlNotation ?loc attrs name [pp_expr ce] + | VernacDeclareImplicits _ as x -> xmlTODO ?loc x + | VernacArguments _ as x -> xmlTODO ?loc x + | VernacArgumentsScope _ as x -> xmlTODO ?loc x + | VernacReserve _ as x -> xmlTODO ?loc x + | VernacGeneralizable _ as x -> xmlTODO ?loc x + | VernacSetOpacity _ as x -> xmlTODO ?loc x + | VernacSetStrategy _ as x -> xmlTODO ?loc x + | VernacUnsetOption _ as x -> xmlTODO ?loc x + | VernacSetOption _ as x -> xmlTODO ?loc x + | VernacSetAppendOption _ as x -> xmlTODO ?loc x + | VernacAddOption _ as x -> xmlTODO ?loc x + | VernacRemoveOption _ as x -> xmlTODO ?loc x + | VernacMemOption _ as x -> xmlTODO ?loc x + | VernacPrintOption _ as x -> xmlTODO ?loc x + | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e] + | VernacGlobalCheck _ as x -> xmlTODO ?loc x + | VernacDeclareReduction _ as x -> xmlTODO ?loc x + | VernacPrint _ as x -> xmlTODO ?loc x + | VernacSearch _ as x -> xmlTODO ?loc x + | VernacLocate _ as x -> xmlTODO ?loc x + | VernacRegister _ as x -> xmlTODO ?loc x + | VernacComments (cl) -> + xmlComment ?loc (List.flatten (List.map pp_comment cl)) + + (* Stm backdoor *) + | VernacStm _ as x -> xmlTODO ?loc x + + (* Proof management *) + | VernacGoal _ as x -> xmlTODO ?loc x + | VernacAbort _ as x -> xmlTODO ?loc x + | VernacAbortAll -> PCData "VernacAbortAll" + | VernacRestart as x -> xmlTODO ?loc x + | VernacUndo _ as x -> xmlTODO ?loc x + | VernacUndoTo _ as x -> xmlTODO ?loc x + | VernacBacktrack _ as x -> xmlTODO ?loc x + | VernacFocus _ as x -> xmlTODO ?loc x + | VernacUnfocus as x -> xmlTODO ?loc x + | VernacUnfocused as x -> xmlTODO ?loc x + | VernacBullet _ as x -> xmlTODO ?loc x + | VernacSubproof _ as x -> xmlTODO ?loc x + | VernacEndSubproof as x -> xmlTODO ?loc x + | VernacShow _ as x -> xmlTODO ?loc x + | VernacCheckGuard as x -> xmlTODO ?loc x + | VernacProof (tac,using) -> + let tac = None (** FIXME *) in + let using = Option.map (xmlSectionSubsetDescr "using") using in + xmlProof ?loc (Option.List.(cons tac (cons using []))) + | VernacProofMode name -> xmlProofMode ?loc name + + (* Toplevel control *) + | VernacToplevelControl _ as x -> xmlTODO ?loc x + + (* For extension *) + | VernacExtend _ as x -> + xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))] + + (* Flags *) + | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e]) + | VernacLocal (b,e) -> + xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) :: + [tmpp ?loc e]) + +let tmpp ?loc v = + match tmpp ?loc v with + | Element("ltac",_,_) as x -> x + | xml -> xmlGallina ?loc [xml] diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index 8254b1b80..c15c00988 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -14,7 +14,9 @@ type binding_kind = Explicit | Implicit type polymorphic = bool -type private_flag = bool +type private_flag = bool + +type cumulative_inductive_flag = bool type theorem_kind = | Theorem diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index cabd06735..26a6db4ec 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -336,7 +336,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 private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_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/kernel/declarations.ml b/kernel/declarations.ml index 1bb1e885f..ae4732456 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -188,6 +188,8 @@ type mutual_inductive_body = { mind_polymorphic : bool; (** Is it polymorphic or not *) + mind_cumulative : bool; (** Is it cumulative or not *) + mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *) mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 883896652..1d91b2d41 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -267,6 +267,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; + mind_cumulative = mib.mind_cumulative; mind_universes = mib.mind_universes; mind_private = mib.mind_private; mind_typing_flags = mib.mind_typing_flags; diff --git a/kernel/entries.mli b/kernel/entries.mli index 97c28025a..9c17346f2 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -49,7 +49,8 @@ type mutual_inductive_entry = { mind_entry_finite : Decl_kinds.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; - mind_entry_polymorphic : bool; + mind_entry_polymorphic : bool; + mind_entry_cumulative : bool; mind_entry_universes : Univ.universe_info_ind; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index a4c7a0573..5cfcbba60 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -392,7 +392,7 @@ let typecheck_inductive env mie = in (* Check that the subtyping information inferred for inductive types in the block is correct. *) (* This check produces a value of the unit type if successful or raises an anomaly if check fails. *) - let () = check_subtyping mie paramsctxt env_arities inds + let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -864,7 +864,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 = +let build_inductive env cum 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 @@ -969,6 +969,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_params_ctxt = paramsctxt; mind_packets = packets; mind_polymorphic = p; + mind_cumulative = cum; mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp); mind_private = prv; mind_typing_flags = Environ.typing_flags env; @@ -984,7 +985,7 @@ let check_inductive env kn mie = 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 + build_inductive env mie.mind_entry_cumulative 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 diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 33dd53a5b..ea583fdac 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -191,7 +191,10 @@ type 'a universe_compare = { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - leq_inductives : flex:bool -> Univ.UInfoInd.t -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> + Univ.Instance.t -> int -> 'a -> 'a; + conv_constructors : (Declarations.mutual_inductive_body * int * int) -> + Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare @@ -207,9 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) = constructors. *) let convert_instances ~flex u u' (s, check) = (check.compare_instances ~flex u u' s, check) + +let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) = + (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check) -let compare_leq_inductives ~flex uinfind u u' (s, check) = - (check.leq_inductives ~flex uinfind u u' s, check) +let convert_constructors cons u1 sv1 u2 sv2 (s, check) = + (check.conv_constructors cons u1 sv1 u2 sv2 s, check) let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else @@ -487,64 +493,31 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | _ -> raise NotConvertible) (* Inductive types: MutInd MutConstruct Fix Cofix *) - | (FInd (ind1,u1), FInd (ind2,u2)) -> - if eq_ind ind1 ind2 - then - begin - let fall_back () = - let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - in - let mind = Environ.lookup_mind (fst ind1) env in - if mind.Declarations.mind_polymorphic then - begin - let num_param_arity = - mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_nrealargs - in - if not (num_param_arity = CClosure.stack_args_size v1 && num_param_arity = CClosure.stack_args_size v2) then - fall_back () - else - begin - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = if cv_pb = CONV then compare_leq_inductives ~flex:false uinfind u2 u1 cuniv else cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - end - end + if eq_ind ind1 ind2 then + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv else - fall_back () - end + convert_instances ~flex:false u1 u2 cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 - then - begin - let fall_back () = - let cuniv = convert_instances ~flex:false u1 u2 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - in - let mind = Environ.lookup_mind (fst ind1) env in - if mind.Declarations.mind_polymorphic then - begin - let num_cnstr_args = - let nparamsctxt = Context.Rel.length mind.Declarations.mind_params_ctxt in - nparamsctxt + mind.Declarations.mind_packets.(snd ind1).Declarations.mind_consnrealargs.(j1 - 1) - in - if not (num_cnstr_args = CClosure.stack_args_size v1 && num_cnstr_args = CClosure.stack_args_size v2) then - fall_back () - else - begin (* we consider subtyping for constructors. *) - let uinfind = mind.Declarations.mind_universes in - let cuniv = compare_leq_inductives ~flex:false uinfind u1 u2 cuniv in - let cuniv = compare_leq_inductives ~flex:false uinfind u2 u1 cuniv in - convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv - end - end + if Int.equal j1 j2 && eq_ind ind1 ind2 then + let mind = Environ.lookup_mind (fst ind1) env in + let cuniv = + if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then + convert_constructors + (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1) + u2 (CClosure.stack_args_size v2) cuniv else - fall_back () - end + convert_instances ~flex:false u1 u2 cuniv + in + convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv else raise NotConvertible (* Eta expansion of records *) @@ -659,24 +632,79 @@ let check_convert_instances ~flex u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible -let check_leq_inductives ~flex uinfind u u' univs = +(* general conversion and inference functions *) +let infer_check_conv_inductives + infer_check_convert_instances + infer_check_inductive_instances + cv_pb (mind, ind) u1 sv1 u2 sv2 univs = + if mind.Declarations.mind_polymorphic then + let num_param_arity = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + infer_check_convert_instances ~flex:false u1 u2 univs + else + let uinfind = mind.Declarations.mind_universes in + infer_check_inductive_instances cv_pb uinfind u1 u2 univs + else infer_check_convert_instances ~flex:false u1 u2 univs + +let infer_check_conv_constructors + infer_check_convert_instances + infer_check_inductive_instances + (mind, ind, cns) u1 sv1 u2 sv2 univs = + if mind.Declarations.mind_polymorphic then + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + infer_check_convert_instances ~flex:false u1 u2 univs + else + let uinfind = mind.Declarations.mind_universes in + infer_check_inductive_instances CONV uinfind u1 u2 univs + else infer_check_convert_instances ~flex:false u1 u2 univs + +let check_inductive_instances cv_pb uinfind u u' univs = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - begin - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - if UGraph.check_constraints comp_cst univs then univs - else raise NotConvertible - end + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + in + if (UGraph.check_constraints comp_cst univs) then univs + else raise NotConvertible + +let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = + infer_check_conv_inductives + check_convert_instances + check_inductive_instances + cv_pb ind u1 sv1 u2 sv2 univs + +let check_conv_constructors cns u1 sv1 u2 sv2 univs = + infer_check_conv_constructors + check_convert_instances + check_inductive_instances + cns u1 sv1 u2 sv2 univs let checked_universes = { compare = checked_sort_cmp_universes; compare_instances = check_convert_instances; - leq_inductives = check_leq_inductives } + conv_inductives = check_conv_inductives; + conv_constructors = check_conv_constructors} let infer_eq (univs, cstrs as cuniv) u u' = if UGraph.check_eq univs u u' then cuniv @@ -718,21 +746,45 @@ let infer_convert_instances ~flex u u' (univs,cstrs) = else Univ.enforce_eq_instances u u' cstrs in (univs, cstrs') -let infer_leq_inductives ~flex uinfind u u' (univs, cstrs) = +let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - (univs, Univ.Constraint.union cstrs comp_cst) - + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | CUMUL -> comp_cst + in + (univs, Univ.Constraint.union cstrs comp_cst) + + +let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs = + infer_check_conv_inductives + infer_convert_instances + infer_inductive_instances + cv_pb ind u1 sv1 u2 sv2 univs + +let infer_conv_constructors cns u1 sv1 u2 sv2 univs = + infer_check_conv_constructors + infer_convert_instances + infer_inductive_instances + cns u1 sv1 u2 sv2 univs + let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances; - leq_inductives = infer_leq_inductives } + conv_inductives = infer_conv_inductives; + conv_constructors = infer_conv_constructors} let gen_conv cv_pb l2r reds env evars univs t1 t2 = let b = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 72f0ecffd..b6d88c2b9 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,12 +36,13 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible or UnivInconsistency *) + { (* Might raise NotConvertible *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; - compare_instances: flex:bool -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - leq_inductives : flex:bool -> Univ.UInfoInd.t -> - Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> + Univ.Instance.t -> int -> 'a -> 'a; + conv_constructors : (Declarations.mutual_inductive_body * int * int) -> + Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; } type 'a universe_state = 'a * 'a universe_compare diff --git a/lib/flags.ml b/lib/flags.ml index 13539bced..46bbba8e5 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -163,6 +163,10 @@ let use_polymorphic_flag () = let make_polymorphic_flag b = local_polymorphic_flag := Some b +let inductive_cumulativity = ref false +let make_inductive_cumulativity b = inductive_cumulativity := b +let is_inductive_cumulativity () = !inductive_cumulativity + (** [program_mode] tells that Program mode has been activated, either globally via [Set Program] or locally via the Program command prefix. *) diff --git a/lib/flags.mli b/lib/flags.mli index 0026aba2e..5e78f0a04 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -119,6 +119,10 @@ val is_universe_polymorphism : unit -> bool val make_polymorphic_flag : bool -> unit val use_polymorphic_flag : unit -> bool +(** Global inductive cumulativity flag. *) +val make_inductive_cumulativity : bool -> unit +val is_inductive_cumulativity : unit -> bool + val warn : bool ref val make_warn : bool -> unit val if_warn : ('a -> unit) -> 'a -> unit diff --git a/library/declare.ml b/library/declare.ml index bf5313545..e2b726f45 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -352,13 +352,14 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_finite = Decl_kinds.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; + mind_entry_cumulative = false; mind_entry_universes = Univ.UInfoInd.empty; mind_entry_private = None; }) (* reinfer subtyping constraints for inductive after section is dischared. *) let infer_inductive_subtyping (pth, mind_ent) = - if mind_ent.mind_entry_polymorphic then + if mind_ent.mind_entry_polymorphic && mind_ent.mind_entry_cumulative then begin let env = Global.env () in let env' = @@ -370,7 +371,6 @@ let infer_inductive_subtyping (pth, mind_ent) = end else (pth, mind_ent) - type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry let inInductive : inductive_obj -> obj = diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b605a44c8..e6b28b1d8 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -162,11 +162,16 @@ GEXTEND Gram | IDENT "Let"; id = identref; b = def_body -> VernacDefinition ((Some Discharge, Definition), (id, None), b) (* Gallina inductive declarations *) - | priv = private_token; f = finite_token; + | cum = cumulativity_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 (priv,f,indl) + 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_inductive_cumulativity () + in + VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> VernacFixpoint (None, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> @@ -234,6 +239,9 @@ GEXTEND Gram | IDENT "Structure" -> (Structure,BiFinite) | IDENT "Class" -> (Class true,BiFinite) ] ] ; + cumulativity_token: + [ [ IDENT "Cumulative" -> Some true | IDENT "NonCumulative" -> Some false | -> None ] ] + ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 0e2ca4900..db2af2be5 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1459,7 +1459,9 @@ 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 rel_inds (Flags.is_universe_polymorphism ()) false false)) + Decl_kinds.Finite with | UserError(s,msg) as e -> let _time3 = System.get_time () in @@ -1470,7 +1472,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(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ msg in @@ -1485,7 +1487,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(false,false,Decl_kinds.Finite,repacked_rel_inds)) ++ fnl () ++ CErrors.print reraise in diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index c75f7f868..ba88563d3 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -880,7 +880,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive) (* Declare inductive *) let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in let mie,pl,impls = Command.interp_mutual_inductive indl [] - false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in + false (* non-cumulative *) 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/pretyping/evarconv.ml b/pretyping/evarconv.ml index ea22c3708..be2fd8129 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -494,6 +494,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty if mind.Declarations.mind_polymorphic then begin let num_param_arity = + (* Context.Rel.length (mind.Declarations.mind_packets.(snd ind).Declarations.mind_arity_ctxt) *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in if not (num_param_arity = nparamsaplied && num_param_arity = nparamsaplied') then @@ -521,6 +522,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty begin let num_cnstr_args = let nparamsctxt = + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(snd ind).Declarations.mind_nrealargs in nparamsctxt + mind.Declarations.mind_packets.(snd ind).Declarations.mind_consnrealargs.(j - 1) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index e374f7b3b..2040acba7 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1361,24 +1361,68 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_leq_inductives ~flex uinfind i0 i1 sigma = +let sigma_check_inductive_instances cv_pb uinfind u u' sigma = let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in - if not ((Univ.Instance.length ind_instance = Univ.Instance.length i0) && - (Univ.Instance.length ind_instance = Univ.Instance.length i1)) then + if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) && + (Univ.Instance.length ind_instance = Univ.Instance.length u')) then anomaly (Pp.str "Invalid inductive subtyping encountered!") else - let comp_subst = (Univ.Instance.append i0 i1) in - let comp_cst = Univ.subst_instance_constraints comp_subst ind_sbcst in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible + let comp_cst = + let comp_subst = (Univ.Instance.append u u') in + Univ.subst_instance_constraints comp_subst ind_sbcst + in + let comp_cst = + match cv_pb with + Reduction.CONV -> + let comp_subst = (Univ.Instance.append u' u) in + let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in + Univ.Constraint.union comp_cst comp_cst' + | Reduction.CUMUL -> comp_cst + in + try Evd.add_constraints sigma comp_cst + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible + +let sigma_conv_inductives + cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + if mind.Declarations.mind_polymorphic then + let num_param_arity = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + in + if not (num_param_arity = sv1 && num_param_arity = sv2) then + raise Reduction.NotConvertible + else + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances cv_pb uinfind u1 u2 sigma + else raise Reduction.NotConvertible + +let sigma_conv_constructors + (mind, ind, cns) u1 sv1 u2 sv2 sigma = + try sigma_compare_instances ~flex:false u1 u2 sigma with + Reduction.NotConvertible -> + if mind.Declarations.mind_polymorphic then + let num_cnstr_args = + let nparamsctxt = + mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs + (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in + nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) + in + if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then + raise Reduction.NotConvertible + else + let uinfind = mind.Declarations.mind_universes in + sigma_check_inductive_instances Reduction.CONV uinfind u1 u2 sigma + else raise Reduction.NotConvertible let sigma_univ_state = { Reduction.compare = sigma_compare_sorts; Reduction.compare_instances = sigma_compare_instances; - Reduction.leq_inductives = sigma_leq_inductives } + Reduction.conv_inductives = sigma_conv_inductives; + Reduction.conv_constructors = sigma_conv_constructors} let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9d28bc4f8..6a47c308d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -727,7 +727,7 @@ open Decl_kinds let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) stre ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -754,13 +754,17 @@ open Decl_kinds in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + let cm = if cum then "Cumulative" else "NonCumulative" in + cm ^ " " ^ kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 471e05e45..87d9e411a 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -142,7 +142,7 @@ let rec classify_vernac e = let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) 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/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e3b5e9435..a497e7a98 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -41,6 +41,8 @@ Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function Open Scope function_scope. +Set Printing Universes. Set Printing All. + Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. @@ -156,7 +158,8 @@ Delimit Scope morphism_scope with morphism. Delimit Scope category_scope with category. Delimit Scope object_scope with object. - +Set Printing Universes. +Set Printing All. Record PreCategory := Build_PreCategory' { object :> Type; @@ -1069,8 +1072,10 @@ Section Adjunction. Variable F : Functor C D. Variable G : Functor D C. - Let Adjunction_Type := - Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G). +(* Let Adjunction_Type := + Eval simpl in (hom_functor D) o (F^op, 1) <~=~> (hom_functor C) o (1, G).*) + + Set Printing All. Set Printing Universes. Record AdjunctionHom := { diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 3e90825ab..f57cbcc2b 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -316,26 +316,6 @@ Module Hurkens'. Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. -Section test_letin_subtyping. - Universe i j k i' j' k'. - Constraint j < j'. - - Context (W : Type) (X : box@{i j k} W). - Definition Y := X : box@{i' j' k'} W. - - Universe i1 j1 k1 i2 j2 k2. - Constraint i1 < i2, k2 < k1. - Definition Z : box@{i1 j1 k1} W := {| unwrap := W |}. - Definition Z' : box@{i2 j2 k2} W := {| unwrap := W |}. - Lemma ZZ' : @eq (box@{i2 j2 k2} W) Z Z'. - Proof. - Set Printing All. Set Printing Universes. - cbv. - reflexivity. - Qed. - -End test_letin_subtyping. - Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ @@ -372,3 +352,35 @@ Module Anonymous. Check collapsethemiddle@{_ _}. End Anonymous. + +Module F. + Context {A B : Type}. + Definition foo : Type := B. +End F. + +Set Universe Polymorphism. + +Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Section test_letin_subtyping. + Universe i j k i' j' k'. + Constraint j < j'. + + Context (W : Type) (X : box@{i j k} W). + Definition Y := X : box@{i' j' k'} W. + + Universe i1 j1 k1 i2 j2 k2. + Constraint i1 < i2. + Constraint k2 < k1. + Context (V : Type). + + Definition Z : box@{i1 j1 k1} V := {| unwrap := V |}. + Definition Z' : box@{i2 j2 k2} V := {| unwrap := V |}. + Lemma ZZ' : @eq (box@{i2 j2 k2} V) Z Z'. + Proof. + Set Printing All. Set Printing Universes. + cbv. + reflexivity. + Qed. + +End test_letin_subtyping. 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