diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 8 | ||||
| -rw-r--r-- | engine/uState.mli | 2 | ||||
| -rw-r--r-- | engine/univGen.ml | 21 | ||||
| -rw-r--r-- | engine/univGen.mli | 10 | ||||
| -rw-r--r-- | engine/univNames.ml | 18 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
7 files changed, 31 insertions, 32 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index eef8452e64..7920af8e0e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -290,7 +290,7 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool -val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 6aecc368e6..185283225c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -324,12 +324,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) + try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_qualid (qualid_of_level uctx l) + match qualid_of_level uctx l with + | Some qid -> Libnames.pr_qualid qid + | None -> Univ.Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) @@ -533,7 +535,7 @@ let emit_side_effects eff u = let new_univ_variable ?loc rigid name ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) = - let u = UnivGen.new_univ_level () in + let u = UnivGen.fresh_level () in let ctx' = Univ.ContextSet.add_universe u ctx in let uctx', pred = match rigid with diff --git a/engine/uState.mli b/engine/uState.mli index ad0cd5c1bb..5170184ef4 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t -val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid +val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univGen.ml b/engine/univGen.ml index 130aa06f53..40c4c909fe 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,26 +13,25 @@ open Names open Constr open Univ +type univ_unique_id = int (* Generator of levels *) -type universe_id = DirPath.t * int - let new_univ_id, set_remote_new_univ_id = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Global.current_dirpath (), n) + ~build:(fun n -> n) -let new_univ_level () = - let dp, id = new_univ_id () in - Univ.Level.make dp id +let new_univ_global () = + Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) -let fresh_level () = new_univ_level () +let fresh_level () = + Univ.Level.make (new_univ_global ()) (* TODO: remove *) -let new_univ dp = Univ.Universe.make (new_univ_level dp) -let new_Type dp = mkType (new_univ dp) -let new_Type_sort dp = Type (new_univ dp) +let new_univ () = Univ.Universe.make (fresh_level ()) +let new_Type () = mkType (new_univ ()) +let new_Type_sort () = Type (new_univ ()) let fresh_instance auctx = - let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in + let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in let ctx = Array.fold_right LSet.add inst LSet.empty in let inst = Instance.of_array inst in inst, (ctx, AUContext.instantiate inst auctx) diff --git a/engine/univGen.mli b/engine/univGen.mli index 8af5f8fdb0..b4598e10d0 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -15,14 +15,14 @@ open Univ (** The global universe counter *) -type universe_id = DirPath.t * int - -val set_remote_new_univ_id : universe_id RemoteCounter.installer +type univ_unique_id +val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer +val new_univ_id : unit -> univ_unique_id (** for the stm *) (** Side-effecting functions creating new universe levels. *) -val new_univ_id : unit -> universe_id -val new_univ_level : unit -> Level.t +val new_univ_global : unit -> Level.UGlobal.t +val fresh_level : unit -> Level.t val new_univ : unit -> Universe.t [@@ocaml.deprecated "Use [new_univ_level]"] diff --git a/engine/univNames.ml b/engine/univNames.ml index 1019f8f0c2..19705f9d36 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -15,17 +15,15 @@ open Univ let qualid_of_level l = match Level.name l with - | Some (d, n as na) -> - begin - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - end - | None -> - Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) + | Some qid -> + (try Some (Nametab.shortest_qualid_of_universe qid) + with Not_found -> None) + | None -> None -let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) +let pr_with_global_universes l = + match qualid_of_level l with + | Some qid -> Libnames.pr_qualid qid + | None -> Level.pr l (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) diff --git a/engine/univNames.mli b/engine/univNames.mli index 6e68153ac2..e9c517babf 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val qualid_of_level : Level.t -> Libnames.qualid +val qualid_of_level : Level.t -> Libnames.qualid option (** Local universe name <-> level mapping *) |