blob: d198fbfbe9bee391bc2c1beaaf02c99febc3f861 (
plain)
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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** This file defines universe unification states which are part of evarmaps.
Most of the API below is reexported in {!Evd}. Consider using higher-level
primitives when needed. *)
open Names
exception UniversesDiffer
type t
(** Type of universe unification states. They allow the incremental building of
universe constraints during an interactive proof. *)
(** {5 Constructors} *)
val empty : t
val make : UGraph.t -> t
val is_empty : t -> bool
val union : t -> t -> t
val of_context_set : Univ.universe_context_set -> t
val of_binders : Universes.universe_binders -> t
(** {5 Projections} *)
val context_set : t -> Univ.universe_context_set
(** The local context of the state, i.e. a set of bound variables together
with their associated constraints. *)
val subst : t -> Universes.universe_opt_subst
(** The local universes that are unification variables *)
val ugraph : t -> UGraph.t
(** The current graph extended with the local constraints *)
val algebraics : t -> Univ.LSet.t
(** The subset of unification variables that can be instantiated with algebraic
universes as they appear in inferred types only. *)
val constraints : t -> Univ.constraints
(** Shorthand for {!context_set} composed with {!ContextSet.constraints}. *)
val context : t -> Univ.universe_context
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
(** {5 Constraints handling} *)
val add_constraints : t -> Univ.constraints -> t
(**
@raise UniversesDiffer when universes differ
*)
val add_universe_constraints : t -> Universes.universe_constraints -> t
(**
@raise UniversesDiffer when universes differ
*)
(** {5 Names} *)
val add_universe_name : t -> string -> Univ.Level.t -> t
(** Associate a human-readable name to a local variable. *)
val universe_of_name : t -> string -> Univ.Level.t
(** Retrieve the universe associated to the name. *)
(** {5 Unification} *)
val restrict : t -> Univ.universe_set -> t
type rigid =
| UnivRigid
| UnivFlexible of bool (** Is substitution by an algebraic ok? *)
val univ_rigid : rigid
val univ_flexible : rigid
val univ_flexible_alg : rigid
val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> t
val merge_subst : t -> Universes.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
val new_univ_variable : ?loc:Loc.t -> rigid -> string option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
(** [make_flexible_variable g algebraic l]
Turn the variable [l] flexible, and algebraic if [algebraic] is true
and [l] can be. That is if there are no strict upper constraints on
[l] and and it does not appear in the instance of any non-algebraic
universe. Otherwise the variable is just made flexible. *)
val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t
val is_sort_variable : t -> Sorts.t -> Univ.Level.t option
val normalize_variables : t -> Univ.universe_subst * t
val constrain_variables : Univ.LSet.t -> t -> Univ.constraints
val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
val normalize : t -> t
(** {5 TODO: Document me} *)
val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context
val update_sigma_env : t -> Environ.env -> t
(** {5 Pretty-printing} *)
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
|
