[api] Move universe syntax to Glob_term

ejgallego · ejgallego · commit a47bd32c261a · 2018-05-08T01:13:04.000+02:00
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 (rocq-prover#6515) moving universe declaration to their proper place make `Misctypes` into basically an empty file save for introduction patterns.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
