From 4c97e4ce19ca4c387039cfdcb4f24658100230b0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Jul 2014 22:50:37 +0200 Subject: Add toplevel commands to declare global universes and constraints. --- intf/vernacexpr.mli | 2 ++ kernel/univ.ml | 11 +++++++++++ kernel/univ.mli | 2 ++ library/declare.ml | 50 +++++++++++++++++++++++++++++++++++++++++++++++ library/declare.mli | 7 +++++++ library/global.ml | 1 + library/global.mli | 4 +--- library/universes.ml | 10 ++++++++++ library/universes.mli | 7 ++++++- parsing/g_vernac.ml4 | 6 ++++++ pretyping/detyping.ml | 7 ++++++- pretyping/pretyping.ml | 13 ++++++++---- printing/ppvernac.ml | 10 +++++++++- stm/vernac_classifier.ml | 1 + toplevel/command.ml | 3 +++ toplevel/command.mli | 3 +++ toplevel/vernacentries.ml | 5 +++++ 17 files changed, 132 insertions(+), 10 deletions(-) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index af65f6541..5aa9d51fc 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -303,6 +303,8 @@ type vernac_expr = locality option * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list + | VernacUniverse of lident list + | VernacConstraint of (lident * Univ.constraint_type * lident) list (* Gallina extensions *) | VernacBeginSection of lident diff --git a/kernel/univ.ml b/kernel/univ.ml index 1e7d2c83c..b42de5a76 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -539,6 +539,10 @@ struct let pr x = str(to_string x) + let pr_with f (v, n) = + if Int.equal n 0 then f v + else f v ++ str"+" ++ int n + let is_level = function | (v, 0) -> true | _ -> false @@ -591,6 +595,13 @@ struct str "max(" ++ hov 0 (prlist_with_sep pr_comma Expr.pr (to_list l)) ++ str ")" + + let pr_with f l = match node l with + | Cons (u, n) when is_nil n -> Expr.pr_with f u + | _ -> + str "max(" ++ hov 0 + (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++ + str ")" let atom l = match node l with | Cons (l, n) when is_nil n -> Some l diff --git a/kernel/univ.mli b/kernel/univ.mli index 832da157e..8166d75e6 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -79,6 +79,8 @@ sig val pr : t -> Pp.std_ppcmds (** Pretty-printing *) + val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) diff --git a/library/declare.ml b/library/declare.ml index 7a80d103d..f746282d1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -430,3 +430,53 @@ let definition_message id = let assumption_message id = Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + +(** Global universe names, in a different summary *) + +type universe_names = + (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) + +let input_universes : universe_names -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe name state") with + cache_function = (fun (na, pi) -> Universes.set_global_universe_names pi); + load_function = (fun _ (_, pi) -> Universes.set_global_universe_names pi); + discharge_function = (fun (_, a) -> Some a); + classify_function = (fun a -> Keep a) } + +let do_universe l = + let glob = Universes.global_universe_names () in + let glob' = + List.fold_left (fun (idl,lid) (l, id) -> + let lev = Universes.new_univ_level (Global.current_dirpath ()) in + (Idmap.add id lev idl, Univ.LMap.add lev id lid)) + glob l + in + Lib.add_anonymous_leaf (input_universes glob') + + +let input_constraints : Univ.constraints -> Libobject.obj = + let open Libobject in + declare_object + { (default_object "Global universe constraints") with + cache_function = (fun (na, c) -> Global.add_constraints c); + load_function = (fun _ (_, c) -> Global.add_constraints c); + discharge_function = (fun (_, a) -> Some a); + classify_function = (fun a -> Keep a) } + +let do_constraint l = + let u_of_id = + let names, _ = Universes.global_universe_names () in + fun (loc, id) -> + try Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + in + let constraints = List.fold_left (fun acc (l, d, r) -> + let lu = u_of_id l and ru = u_of_id r in + Univ.Constraint.add (lu, d, ru) acc) + Univ.Constraint.empty l + in + Lib.add_anonymous_leaf (input_constraints constraints) + diff --git a/library/declare.mli b/library/declare.mli index ed3e4dcc3..a9fd8956e 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -85,3 +85,10 @@ val recursive_message : bool (** true = fixpoint *) -> int array option -> Id.t list -> unit val exists_name : Id.t -> bool + + + +(** Global universe names and constraints *) + +val do_universe : Id.t Loc.located list -> unit +val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit diff --git a/library/global.ml b/library/global.ml index 378e7aaa3..c3c309c39 100644 --- a/library/global.ml +++ b/library/global.ml @@ -237,3 +237,4 @@ let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) + diff --git a/library/global.mli b/library/global.mli index de19e888c..9e47c16ff 100644 --- a/library/global.mli +++ b/library/global.mli @@ -28,9 +28,6 @@ val named_context : unit -> Context.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit -(** Extra universe constraints *) -val add_constraints : Univ.constraints -> unit - (** Variables, Local definitions, constants, inductive types *) val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit @@ -41,6 +38,7 @@ val add_constant : val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive +(** Extra universe constraints *) val add_constraints : Univ.constraints -> unit val push_context : Univ.universe_context -> unit diff --git a/library/universes.ml b/library/universes.ml index 0699326c5..e84f1f975 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -13,6 +13,16 @@ open Term open Environ open Univ +type universe_names = + Univ.universe_level Idmap.t * Id.t Univ.LMap.t + +let global_universes = Summary.ref ~name:"Global universe names" + ((Idmap.empty, Univ.LMap.empty) : universe_names) + +let global_universe_names () = !global_universes +let set_global_universe_names s = global_universes := s + + type universe_constraint_type = ULe | UEq | ULub type universe_constraint = universe * universe_constraint_type * universe diff --git a/library/universes.mli b/library/universes.mli index 691f404aa..5b0951928 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -17,6 +17,12 @@ open Univ (** Universes *) +type universe_names = + Univ.universe_level Idmap.t * Id.t Univ.LMap.t + +val global_universe_names : unit -> universe_names +val set_global_universe_names : universe_names -> unit + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer @@ -237,4 +243,3 @@ val minimize_univ_variables : Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints - diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 39c93e316..5f49a318d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -210,6 +210,8 @@ GEXTEND Gram l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) | IDENT "Register"; IDENT "Inline"; id = identref -> VernacRegister(id, RegisterInline) + | IDENT "Universe"; l = LIST1 identref -> VernacUniverse l + | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> VernacConstraint l ] ] ; @@ -256,6 +258,10 @@ GEXTEND Gram | IDENT "Inline" -> DefaultInline | -> NoInline] ] ; + univ_constraint: + [ [ l = identref; ord = [ "<" -> Univ.Lt | "=" -> Univ.Eq | "<=" -> Univ.Le ]; + r = identref -> (l, ord, r) ] ] + ; finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) | "CoInductive" -> (CoInductive,CoFinite) ] ] diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index a7a8bf5be..92a29fce7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -370,7 +370,12 @@ let detype_sort = function | Type u -> GType (if !print_universes - then Some (Pp.string_of_ppcmds (Univ.Universe.pr u)) + then + let _, map = Universes.global_universe_names () in + let pr_level u = + try Nameops.pr_id (Univ.LMap.find u map) with Not_found -> Univ.Level.pr u + in + Some (Pp.string_of_ppcmds (Univ.Universe.pr_with pr_level u)) else None) type binder_kind = BProd | BLambda | BLetIn diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c8c1d0e21..9609a959b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -96,10 +96,15 @@ let ((constr_in : constr -> Dyn.t), let interp_universe_name evd = function | None -> new_univ_level_variable univ_rigid evd | Some s -> - try let level = Evd.universe_of_name evd s in - evd, level - with Not_found -> - new_univ_level_variable ~name:s univ_rigid evd + try + let id = try Id.of_string s with _ -> raise Not_found in + let names, _ = Universes.global_universe_names () in + evd, Idmap.find id names + with Not_found -> + try let level = Evd.universe_of_name evd s in + evd, level + with Not_found -> + new_univ_level_variable ~name:s univ_rigid evd let interp_sort evd = function | GProp -> evd, Prop Null diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index d89731147..f088477e7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -691,7 +691,15 @@ let rec pr_vernac = function hov 2 (str"Combined Scheme" ++ spc() ++ pr_lident id ++ spc() ++ str"from" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ str", ") pr_lident l) - + | VernacUniverse v -> + hov 2 (str"Universe" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_lident v) + | VernacConstraint v -> + let pr_uconstraint (l, d, r) = + pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r + in + hov 2 (str"Constraint" ++ spc () ++ + prlist_with_sep (fun _ -> str",") pr_uconstraint v) (* Gallina extensions *) | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id) diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 05c8fdd0d..12d3a3787 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -139,6 +139,7 @@ let rec classify_vernac e = let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater + | VernacUniverse _ | VernacConstraint _ | VernacBeginSection _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ diff --git a/toplevel/command.ml b/toplevel/command.ml index faa4b12df..95ddf1fb0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -38,6 +38,9 @@ open Indschemes open Misctypes open Vernacexpr +let do_universe l = Declare.do_universe l +let do_constraint l = Declare.do_constraint l + let rec under_binders env f n c = if Int.equal n 0 then f env Evd.empty c else match kind_of_term c with diff --git a/toplevel/command.mli b/toplevel/command.mli index 4d1c74907..d14af7394 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,6 +21,9 @@ open Pfedit (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) +val do_universe : Id.t Loc.located list -> unit +val do_constraint : (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit + (** {6 Hooks for Pcoq} *) val set_declare_definition_hook : (definition_entry -> unit) -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index b1ed564d8..1d05f4e62 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -605,6 +605,9 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l +let vernac_universe l = do_universe l +let vernac_constraint l = do_constraint l + (**********************) (* Modules *) @@ -1721,6 +1724,8 @@ let interp ?proof locality poly c = | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l + | VernacUniverse l -> vernac_universe l + | VernacConstraint l -> vernac_constraint l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> -- cgit v1.2.3