1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Sorts
open Names
open Constr
open Univ
type univ_unique_id = int
(* Generator of levels *)
let new_univ_id, set_remote_new_univ_id =
RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1)
~build:(fun n -> n)
let new_univ_global () =
Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ())
let fresh_level () =
Univ.Level.make (new_univ_global ())
let fresh_instance auctx =
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)
let existing_instance ?loc auctx inst =
let () =
let len1 = Array.length (Instance.to_array inst)
and len2 = AUContext.size auctx in
if not (len1 == len2) then
CErrors.user_err ?loc ~hdr:"Universes"
Pp.(str "Universe instance should have length " ++ int len2 ++ str ".")
else ()
in
inst, (LSet.empty, AUContext.instantiate inst auctx)
let fresh_instance_from ?loc ctx = function
| Some inst -> existing_instance ?loc ctx inst
| None -> fresh_instance ctx
(** Fresh universe polymorphic construction *)
let fresh_global_instance ?loc ?names env gr =
let auctx = Environ.universes_of_global env gr in
let u, ctx = fresh_instance_from ?loc auctx names in
u, ctx
let fresh_constant_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
(c, u), ctx
let fresh_inductive_instance env ind =
let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
(ind, u), ctx
let fresh_constructor_instance env c =
let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
(c, u), ctx
let fresh_array_instance env =
let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
let u, ctx = fresh_instance_from auctx None in
u, ctx
let fresh_global_instance ?loc ?names env gr =
let u, ctx = fresh_global_instance ?loc ?names env gr in
mkRef (gr, u), ctx
let constr_of_monomorphic_global gr =
if not (Global.is_polymorphic gr) then
fst (fresh_global_instance (Global.env ()) gr)
else CErrors.user_err ~hdr:"constr_of_global"
Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
str " would forget universes.")
let fresh_sort_in_family = function
| InSProp -> Sorts.sprop, ContextSet.empty
| InProp -> Sorts.prop, ContextSet.empty
| InSet -> Sorts.set, ContextSet.empty
| InType ->
let u = fresh_level () in
sort_of_univ (Univ.Universe.make u), ContextSet.singleton u
let new_global_univ () =
let u = fresh_level () in
(Univ.Universe.make u, ContextSet.singleton u)
let fresh_universe_context_set_instance ctx =
if ContextSet.is_empty ctx then LMap.empty, ctx
else
let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
let univs',subst = LSet.fold
(fun u (univs',subst) ->
let u' = fresh_level () in
(LSet.add u' univs', LMap.add u u' subst))
univs (LSet.empty, LMap.empty)
in
let cst' = subst_univs_level_constraints subst cst in
subst, (univs', cst')
|
