From a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Apr 2018 03:26:40 +0200 Subject: [api] Move universe syntax to `Glob_term` We move syntax for universes from `Misctypes` to `Glob_term`. There is basically no reason that this type is there instead of the proper file, as witnessed by the diff. Unfortunately the change is not compatible due to moving a type to a higher level in the hierarchy, but we expect few problems. This change plus the related PR (#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns. --- dev/doc/changes.md | 6 ++++++ interp/constrextern.mli | 1 - interp/constrintern.ml | 18 +++++++++--------- interp/declare.mli | 2 +- library/misctypes.ml | 19 ------------------- parsing/g_constr.ml4 | 1 + parsing/pcoq.mli | 4 ++-- pretyping/constr_matching.ml | 2 +- pretyping/constrexpr.ml | 6 +++--- pretyping/detyping.mli | 1 - pretyping/glob_term.ml | 19 +++++++++++++++++++ pretyping/miscops.ml | 2 +- pretyping/miscops.mli | 2 +- pretyping/pattern.ml | 2 +- pretyping/pretyping.ml | 4 ++-- pretyping/pretyping.mli | 2 +- pretyping/vernacexpr.ml | 2 +- printing/ppconstr.ml | 6 +++--- printing/ppconstr.mli | 4 ++-- vernac/comInductive.ml | 3 +-- vernac/record.ml | 2 +- 21 files changed, 56 insertions(+), 52 deletions(-) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 6d7c0d368..e9faa61c0 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,12 @@ ### ML API +Misctypes + + Syntax for universe sorts and kinds has been moved from `Misctypes` + to `Glob_term`, as these are turned into kernel terms by + `Pretyping`. + Proof engine - More functions have been changed to use `EConstr`, notably the diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 6f5887ca2..73c108319 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -18,7 +18,6 @@ open Pattern open Constrexpr open Notation_term open Notation -open Misctypes open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax diff --git a/interp/constrintern.ml b/interp/constrintern.ml index def8425ec..48f15f897 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -980,17 +980,17 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = match info with - | Misctypes.UAnonymous -> None - | Misctypes.UUnknown -> None - | Misctypes.UNamed id -> Some (id, 0) + | UAnonymous -> None + | UUnknown -> None + | UNamed id -> Some (id, 0) -let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = +let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | Misctypes.GProp -> Misctypes.GProp - | Misctypes.GSet -> Misctypes.GSet - | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + | GProp -> GProp + | GSet -> GSet + | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) let intern_qualid qid intern env ntnvars us args = @@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) diff --git a/interp/declare.mli b/interp/declare.mli index f8cffbb1e..de4d8346a 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -88,5 +88,5 @@ val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Misctypes.lident list -> unit -val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> +val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list -> unit diff --git a/library/misctypes.ml b/library/misctypes.ml index 72db3b31c..b5d30559d 100644 --- a/library/misctypes.ml +++ b/library/misctypes.ml @@ -50,25 +50,6 @@ type 'id move_location = | MoveFirst | MoveLast (** can be seen as "no move" when doing intro *) -(** Sorts *) - -type 'a glob_sort_gen = - | GProp (** representation of [Prop] literal *) - | GSet (** representation of [Set] literal *) - | GType of 'a (** representation of [Type] literal *) - -type 'a universe_kind = - | UAnonymous - | UUnknown - | UNamed of 'a - -type level_info = Libnames.reference universe_kind -type glob_level = level_info glob_sort_gen -type glob_constraint = glob_level * Univ.constraint_type * glob_level - -type sort_info = (Libnames.reference * int) option list -type glob_sort = sort_info glob_sort_gen - (** A synonym of [Evar.t], also defined in Term *) type existential_key = Evar.t diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9c2806bea..a03ef268d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -10,6 +10,7 @@ open Names open Libnames +open Glob_term open Constrexpr open Constrexpr_ops open Util diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 0fbf2f567..387a62604 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -227,8 +227,8 @@ module Constr : val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry val global : reference Gram.entry - val universe_level : glob_level Gram.entry - val sort : glob_sort Gram.entry + val universe_level : Glob_term.glob_level Gram.entry + val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 89d490a41..57ca03f5e 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -20,7 +20,6 @@ open EConstr open Vars open Pattern open Patternops -open Misctypes open Context.Rel.Declaration open Ltac_pretype (*i*) @@ -277,6 +276,7 @@ let matches_core env sigma allow_bound_rels | PSort ps, Sort s -> + let open Glob_term in begin match ps, ESorts.kind sigma s with | GProp, Prop Null -> subst | GSet, Prop Pos -> subst diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml index fda31756a..1443dfb51 100644 --- a/pretyping/constrexpr.ml +++ b/pretyping/constrexpr.ml @@ -17,7 +17,7 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl +type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option @@ -50,7 +50,7 @@ type prim_token = | Numeral of raw_natural_number * sign | String of string -type instance_expr = Misctypes.glob_level list +type instance_expr = Glob_term.glob_level list type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname @@ -98,7 +98,7 @@ and constr_expr_r = | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of patvar | CEvar of Glob_term.existential_name * (Id.t * constr_expr) list - | CSort of glob_sort + | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr cast_type | CNotation of notation * constr_notation_substitution | CGeneralization of binding_kind * abstraction_kind option * constr_expr diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 817b8ba6e..5310455fe 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -14,7 +14,6 @@ open EConstr open Glob_term open Termops open Mod_subst -open Misctypes open Evd open Ltac_pretype diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 3c3f75a68..6ecb479e6 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -22,6 +22,25 @@ open Misctypes type existential_name = Id.t +(** Sorts *) + +type 'a glob_sort_gen = + | GProp (** representation of [Prop] literal *) + | GSet (** representation of [Set] literal *) + | GType of 'a (** representation of [Type] literal *) + +type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + +type level_info = Libnames.reference universe_kind +type glob_level = level_info glob_sort_gen +type glob_constraint = glob_level * Univ.constraint_type * glob_level + +type sort_info = (Libnames.reference * int) option list +type glob_sort = sort_info glob_sort_gen + (** The kind of patterns that occurs in "match ... with ... end" locs here refers to the ident's location, not whole pat *) diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 0f0af5409..1b536bfda 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -29,7 +29,7 @@ let smartmap_cast_type f c = (** Equalities on [glob_sort] *) -let glob_sort_eq g1 g2 = match g1, g2 with +let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index abe817fe5..1d4504541 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -18,7 +18,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Equalities on [glob_sort] *) -val glob_sort_eq : glob_sort -> glob_sort -> bool +val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool (** Equalities on [intro_pattern_naming] *) diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 7dd0954bc..996a2dc36 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -30,7 +30,7 @@ type constr_pattern = | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of glob_sort + | PSort of Glob_term.glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e68a25a87..01e0c7e24 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -245,7 +245,7 @@ let interp_known_level_info ?loc evd = function with Not_found -> user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) -let interp_level_info ?loc evd : Misctypes.level_info -> _ = function +let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s @@ -499,7 +499,7 @@ let interp_known_glob_level ?loc evd = function | GSet -> Univ.Level.set | GType s -> interp_known_level_info ?loc evd s -let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function +let interp_glob_level ?loc evd : glob_level -> _ = function | GProp -> evd, Univ.Level.prop | GSet -> evd, Univ.Level.set | GType s -> interp_level_info ?loc evd s diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 415c4e172..73f5b77e0 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -22,7 +22,7 @@ open Ltac_pretype open Evardefine val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> - Misctypes.glob_level -> Univ.Level.t + glob_level -> Univ.Level.t (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml index 3a49d6cf8..e15c3ad04 100644 --- a/pretyping/vernacexpr.ml +++ b/pretyping/vernacexpr.ml @@ -338,7 +338,7 @@ type nonrec vernac_expr = | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list - | VernacConstraint of glob_constraint list + | VernacConstraint of Glob_term.glob_constraint list (* Gallina extensions *) | VernacBeginSection of lident diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 412a1cbb4..60268c9de 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -170,13 +170,13 @@ let tag_var = tag Tag.variable let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}" - let pr_glob_sort = function + let pr_glob_sort = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType [] -> tag_type (str "Type") | GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u) - let pr_glob_level = function + let pr_glob_level = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") @@ -199,7 +199,7 @@ let tag_var = tag Tag.variable let pr_qualid = pr_qualid let pr_patvar = pr_id - let pr_glob_sort_instance = function + let pr_glob_sort_instance = let open Glob_term in function | GProp -> tag_type (str "Prop") | GSet -> diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 1f1308b0d..127c4471c 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -41,8 +41,8 @@ val pr_name : Name.t -> Pp.t val pr_qualid : qualid -> Pp.t val pr_patvar : patvar -> Pp.t -val pr_glob_level : glob_level -> Pp.t -val pr_glob_sort : glob_sort -> Pp.t +val pr_glob_level : Glob_term.glob_level -> Pp.t +val pr_glob_sort : Glob_term.glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> lident option * recursion_order_expr -> diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 101298ef4..b2532485a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -29,7 +29,6 @@ open Indtypes open Pretyping open Evarutil open Indschemes -open Misctypes open Context.Rel.Declaration open Entries @@ -380,7 +379,7 @@ let extract_params indl = let extract_inductive indl = List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; - ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; + ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType [])) ar; ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl diff --git a/vernac/record.ml b/vernac/record.ml index b89c0060d..b0f229294 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -122,7 +122,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env = EConstr.push_rel_context newps env0 in let poly = match t with - | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in + | { CAst.v = CSort (Glob_term.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with -- cgit v1.2.3