Skip to content

Commit a51dda2

Browse files
SkySkimmerSkySkimmer
committed
Split off Universes functions dealing with generating new universes.
1 parent b0ef649 commit a51dda2

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

44 files changed

+533
-396
lines changed

‎engine/engine.mllib

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
UnivNames
2+
UnivGen
23
Universes
34
Univops
45
UState

‎engine/evd.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -804,19 +804,19 @@ let make_flexible_variable evd ~algebraic u =
804804
(****************************************)
805805

806806
let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s =
807-
with_context_set ?loc rigid evd (Universes.fresh_sort_in_family env s)
807+
with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s)
808808

809809
let fresh_constant_instance ?loc env evd c =
810-
with_context_set ?loc univ_flexible evd (Universes.fresh_constant_instance env c)
810+
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c)
811811

812812
let fresh_inductive_instance ?loc env evd i =
813-
with_context_set ?loc univ_flexible evd (Universes.fresh_inductive_instance env i)
813+
with_context_set ?loc univ_flexible evd (UnivGen.fresh_inductive_instance env i)
814814

815815
let fresh_constructor_instance ?loc env evd c =
816-
with_context_set ?loc univ_flexible evd (Universes.fresh_constructor_instance env c)
816+
with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c)
817817

818818
let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr =
819-
with_context_set ?loc rigid evd (Universes.fresh_global_instance ?names env gr)
819+
with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr)
820820

821821
let whd_sort_variable evd t = t
822822

‎engine/uState.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -471,7 +471,7 @@ let emit_side_effects eff u =
471471

472472
let new_univ_variable ?loc rigid name
473473
({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
474-
let u = Universes.new_univ_level () in
474+
let u = UnivGen.new_univ_level () in
475475
let ctx' = Univ.ContextSet.add_universe u ctx in
476476
let uctx', pred =
477477
match rigid with
@@ -582,7 +582,7 @@ let fix_undefined_variables uctx =
582582
uctx_univ_algebraic = algs' }
583583

584584
let refresh_undefined_univ_variables uctx =
585-
let subst, ctx' = Universes.fresh_universe_context_set_instance uctx.uctx_local in
585+
let subst, ctx' = UnivGen.fresh_universe_context_set_instance uctx.uctx_local in
586586
let subst_fn u = Univ.subst_univs_level_level subst u in
587587
let alg = Univ.LSet.fold (fun u acc -> Univ.LSet.add (subst_fn u) acc)
588588
uctx.uctx_univ_algebraic Univ.LSet.empty

‎engine/univGen.ml

Lines changed: 246 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,246 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
4+
(* <O___,, * (see CREDITS file for the list of authors) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
open Sorts
12+
open Names
13+
open Constr
14+
open Environ
15+
open Univ
16+
17+
(* Generator of levels *)
18+
type universe_id = DirPath.t * int
19+
20+
let new_univ_id, set_remote_new_univ_id =
21+
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
22+
~build:(fun n -> Global.current_dirpath (), n)
23+
24+
let new_univ_level () =
25+
let dp, id = new_univ_id () in
26+
Univ.Level.make dp id
27+
28+
let fresh_level () = new_univ_level ()
29+
30+
(* TODO: remove *)
31+
let new_univ dp = Univ.Universe.make (new_univ_level dp)
32+
let new_Type dp = mkType (new_univ dp)
33+
let new_Type_sort dp = Type (new_univ dp)
34+
35+
let fresh_universe_instance ctx =
36+
let init _ = new_univ_level () in
37+
Instance.of_array (Array.init (AUContext.size ctx) init)
38+
39+
let fresh_instance_from_context ctx =
40+
let inst = fresh_universe_instance ctx in
41+
let constraints = AUContext.instantiate inst ctx in
42+
inst, constraints
43+
44+
let fresh_instance ctx =
45+
let ctx' = ref LSet.empty in
46+
let init _ =
47+
let u = new_univ_level () in
48+
ctx' := LSet.add u !ctx'; u
49+
in
50+
let inst = Instance.of_array (Array.init (AUContext.size ctx) init)
51+
in !ctx', inst
52+
53+
let existing_instance ctx inst =
54+
let () =
55+
let len1 = Array.length (Instance.to_array inst)
56+
and len2 = AUContext.size ctx in
57+
if not (len1 == len2) then
58+
CErrors.user_err ~hdr:"Universes"
59+
Pp.(str "Polymorphic constant expected " ++ int len2 ++
60+
str" levels but was given " ++ int len1)
61+
else ()
62+
in LSet.empty, inst
63+
64+
let fresh_instance_from ctx inst =
65+
let ctx', inst =
66+
match inst with
67+
| Some inst -> existing_instance ctx inst
68+
| None -> fresh_instance ctx
69+
in
70+
let constraints = AUContext.instantiate inst ctx in
71+
inst, (ctx', constraints)
72+
73+
(** Fresh universe polymorphic construction *)
74+
75+
let fresh_constant_instance env c inst =
76+
let cb = lookup_constant c env in
77+
match cb.Declarations.const_universes with
78+
| Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty)
79+
| Declarations.Polymorphic_const auctx ->
80+
let inst, ctx =
81+
fresh_instance_from auctx inst
82+
in
83+
((c, inst), ctx)
84+
85+
let fresh_inductive_instance env ind inst =
86+
let mib, mip = Inductive.lookup_mind_specif env ind in
87+
match mib.Declarations.mind_universes with
88+
| Declarations.Monomorphic_ind _ ->
89+
((ind,Instance.empty), ContextSet.empty)
90+
| Declarations.Polymorphic_ind uactx ->
91+
let inst, ctx = (fresh_instance_from uactx) inst in
92+
((ind,inst), ctx)
93+
| Declarations.Cumulative_ind acumi ->
94+
let inst, ctx =
95+
fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst
96+
in ((ind,inst), ctx)
97+
98+
let fresh_constructor_instance env (ind,i) inst =
99+
let mib, mip = Inductive.lookup_mind_specif env ind in
100+
match mib.Declarations.mind_universes with
101+
| Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty)
102+
| Declarations.Polymorphic_ind auctx ->
103+
let inst, ctx = fresh_instance_from auctx inst in
104+
(((ind,i),inst), ctx)
105+
| Declarations.Cumulative_ind acumi ->
106+
let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in
107+
(((ind,i),inst), ctx)
108+
109+
open Globnames
110+
111+
let fresh_global_instance ?names env gr =
112+
match gr with
113+
| VarRef id -> mkVar id, ContextSet.empty
114+
| ConstRef sp ->
115+
let c, ctx = fresh_constant_instance env sp names in
116+
mkConstU c, ctx
117+
| ConstructRef sp ->
118+
let c, ctx = fresh_constructor_instance env sp names in
119+
mkConstructU c, ctx
120+
| IndRef sp ->
121+
let c, ctx = fresh_inductive_instance env sp names in
122+
mkIndU c, ctx
123+
124+
let fresh_constant_instance env sp =
125+
fresh_constant_instance env sp None
126+
127+
let fresh_inductive_instance env sp =
128+
fresh_inductive_instance env sp None
129+
130+
let fresh_constructor_instance env sp =
131+
fresh_constructor_instance env sp None
132+
133+
let constr_of_global gr =
134+
let c, ctx = fresh_global_instance (Global.env ()) gr in
135+
if not (Univ.ContextSet.is_empty ctx) then
136+
if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then
137+
(* Should be an error as we might forget constraints, allow for now
138+
to make firstorder work with "using" clauses *)
139+
c
140+
else CErrors.user_err ~hdr:"constr_of_global"
141+
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
142+
str " would forget universes.")
143+
else c
144+
145+
let constr_of_global_univ (gr,u) =
146+
match gr with
147+
| VarRef id -> mkVar id
148+
| ConstRef sp -> mkConstU (sp,u)
149+
| ConstructRef sp -> mkConstructU (sp,u)
150+
| IndRef sp -> mkIndU (sp,u)
151+
152+
let fresh_global_or_constr_instance env = function
153+
| IsConstr c -> c, ContextSet.empty
154+
| IsGlobal gr -> fresh_global_instance env gr
155+
156+
let global_of_constr c =
157+
match kind c with
158+
| Const (c, u) -> ConstRef c, u
159+
| Ind (i, u) -> IndRef i, u
160+
| Construct (c, u) -> ConstructRef c, u
161+
| Var id -> VarRef id, Instance.empty
162+
| _ -> raise Not_found
163+
164+
open Declarations
165+
166+
let type_of_reference env r =
167+
match r with
168+
| VarRef id -> Environ.named_type id env, ContextSet.empty
169+
| ConstRef c ->
170+
let cb = Environ.lookup_constant c env in
171+
let ty = cb.const_type in
172+
begin
173+
match cb.const_universes with
174+
| Monomorphic_const _ -> ty, ContextSet.empty
175+
| Polymorphic_const auctx ->
176+
let inst, ctx = fresh_instance_from auctx None in
177+
Vars.subst_instance_constr inst ty, ctx
178+
end
179+
| IndRef ind ->
180+
let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
181+
begin
182+
match mib.mind_universes with
183+
| Monomorphic_ind _ ->
184+
let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in
185+
ty, ContextSet.empty
186+
| Polymorphic_ind auctx ->
187+
let inst, ctx = fresh_instance_from auctx None in
188+
let ty = Inductive.type_of_inductive env (specif, inst) in
189+
ty, ctx
190+
| Cumulative_ind cumi ->
191+
let inst, ctx =
192+
fresh_instance_from (ACumulativityInfo.univ_context cumi) None
193+
in
194+
let ty = Inductive.type_of_inductive env (specif, inst) in
195+
ty, ctx
196+
end
197+
198+
| ConstructRef cstr ->
199+
let (mib,oib as specif) =
200+
Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
201+
in
202+
begin
203+
match mib.mind_universes with
204+
| Monomorphic_ind _ ->
205+
Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty
206+
| Polymorphic_ind auctx ->
207+
let inst, ctx = fresh_instance_from auctx None in
208+
Inductive.type_of_constructor (cstr,inst) specif, ctx
209+
| Cumulative_ind cumi ->
210+
let inst, ctx =
211+
fresh_instance_from (ACumulativityInfo.univ_context cumi) None
212+
in
213+
Inductive.type_of_constructor (cstr,inst) specif, ctx
214+
end
215+
216+
let type_of_global t = type_of_reference (Global.env ()) t
217+
218+
let fresh_sort_in_family env = function
219+
| InProp -> Sorts.prop, ContextSet.empty
220+
| InSet -> Sorts.set, ContextSet.empty
221+
| InType ->
222+
let u = fresh_level () in
223+
Type (Univ.Universe.make u), ContextSet.singleton u
224+
225+
let new_sort_in_family sf =
226+
fst (fresh_sort_in_family (Global.env ()) sf)
227+
228+
let extend_context (a, ctx) (ctx') =
229+
(a, ContextSet.union ctx ctx')
230+
231+
let new_global_univ () =
232+
let u = fresh_level () in
233+
(Univ.Universe.make u, ContextSet.singleton u)
234+
235+
let fresh_universe_context_set_instance ctx =
236+
if ContextSet.is_empty ctx then LMap.empty, ctx
237+
else
238+
let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
239+
let univs',subst = LSet.fold
240+
(fun u (univs',subst) ->
241+
let u' = fresh_level () in
242+
(LSet.add u' univs', LMap.add u u' subst))
243+
univs (LSet.empty, LMap.empty)
244+
in
245+
let cst' = subst_univs_level_constraints subst cst in
246+
subst, (univs', cst')

‎engine/univGen.mli

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
(************************************************************************)
2+
(* * The Coq Proof Assistant / The Coq Development Team *)
3+
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
4+
(* <O___,, * (see CREDITS file for the list of authors) *)
5+
(* \VV/ **************************************************************)
6+
(* // * This file is distributed under the terms of the *)
7+
(* * GNU Lesser General Public License Version 2.1 *)
8+
(* * (see LICENSE file for the text of the license) *)
9+
(************************************************************************)
10+
11+
open Names
12+
open Constr
13+
open Environ
14+
open Univ
15+
16+
17+
(** The global universe counter *)
18+
type universe_id = DirPath.t * int
19+
20+
val set_remote_new_univ_id : universe_id RemoteCounter.installer
21+
22+
(** Side-effecting functions creating new universe levels. *)
23+
24+
val new_univ_id : unit -> universe_id
25+
val new_univ_level : unit -> Level.t
26+
val new_univ : unit -> Universe.t
27+
val new_Type : unit -> types
28+
val new_Type_sort : unit -> Sorts.t
29+
30+
val new_global_univ : unit -> Universe.t in_universe_context_set
31+
val new_sort_in_family : Sorts.family -> Sorts.t
32+
33+
(** Build a fresh instance for a given context, its associated substitution and
34+
the instantiated constraints. *)
35+
36+
val fresh_instance_from_context : AUContext.t ->
37+
Instance.t constrained
38+
39+
val fresh_instance_from : AUContext.t -> Instance.t option ->
40+
Instance.t in_universe_context_set
41+
42+
val fresh_sort_in_family : env -> Sorts.family ->
43+
Sorts.t in_universe_context_set
44+
val fresh_constant_instance : env -> Constant.t ->
45+
pconstant in_universe_context_set
46+
val fresh_inductive_instance : env -> inductive ->
47+
pinductive in_universe_context_set
48+
val fresh_constructor_instance : env -> constructor ->
49+
pconstructor in_universe_context_set
50+
51+
val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
52+
constr in_universe_context_set
53+
54+
val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr ->
55+
constr in_universe_context_set
56+
57+
(** Get fresh variables for the universe context.
58+
Useful to make tactics that manipulate constrs in universe contexts polymorphic. *)
59+
val fresh_universe_context_set_instance : ContextSet.t ->
60+
universe_level_subst * ContextSet.t
61+
62+
(** Raises [Not_found] if not a global reference. *)
63+
val global_of_constr : constr -> GlobRef.t puniverses
64+
65+
val constr_of_global_univ : GlobRef.t puniverses -> constr
66+
67+
val extend_context : 'a in_universe_context_set -> ContextSet.t ->
68+
'a in_universe_context_set
69+
70+
(** Create a fresh global in the global environment, without side effects.
71+
BEWARE: this raises an ANOMALY on polymorphic constants/inductives:
72+
the constraints should be properly added to an evd.
73+
See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
74+
the proper way to get a fresh copy of a global reference. *)
75+
val constr_of_global : GlobRef.t -> constr
76+
77+
(** Returns the type of the global reference, by creating a fresh instance of polymorphic
78+
references and computing their instantiated universe context. (side-effect on the
79+
universe counter, use with care). *)
80+
val type_of_global : GlobRef.t -> types in_universe_context_set

0 commit comments

Comments
 (0)