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
127
128
129
|
(************************************************************************)
(* 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 *)
(************************************************************************)
open Names
open Constr
(** Monotonous state enforced by typing.
This module allows to constrain uses of evarmaps in a monotonous fashion,
and in particular statically suppress evar leaks and the like.
*)
(** {5 Stages} *)
type ('a, 'b) le
(** Relationship stating that stage ['a] is anterior to stage ['b] *)
val refl : ('a, 'a) le
(** Reflexivity of anteriority *)
val cons : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
(** Transitivity of anteriority *)
val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
(** Alias for {!cons} *)
(** {5 Monotonous evarmaps} *)
type 'r t
(** Stage-indexed evarmaps. *)
type ('a, 'r) sigma = Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma
(** Return values at a later stage *)
type 'r evar
(** Stage-indexed evars *)
(** {5 Constructors} *)
val here : 'a -> 'r t -> ('a, 'r) sigma
(** [here x s] is a shorthand for [Sigma (x, s, refl)] *)
(** {5 Postponing} *)
val lift_evar : 'r evar -> ('r, 's) le -> 's evar
(** Any evar existing at stage ['r] is also valid at any later stage. *)
(** {5 Downcasting} *)
val to_evar_map : 'r t -> Evd.evar_map
val to_evar : 'r evar -> Evar.t
(** {5 Monotonous API} *)
type 'r fresh = Fresh : 's evar * 's t * ('r, 's) le -> 'r fresh
val new_evar : 'r t -> ?naming:Misctypes.intro_pattern_naming_expr ->
Evd.evar_info -> 'r fresh
val define : 'r evar -> Constr.t -> 'r t -> (unit, 'r) sigma
(** Polymorphic universes *)
val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool ->
Evd.rigid -> 'r t -> (Sorts.t, 'r) sigma
val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:Evd.rigid -> Environ.env ->
'r t -> Term.sorts_family -> (Term.sorts, 'r) sigma
val fresh_constant_instance :
?loc:Loc.t -> Environ.env -> 'r t -> constant -> (pconstant, 'r) sigma
val fresh_inductive_instance :
?loc:Loc.t -> Environ.env -> 'r t -> inductive -> (pinductive, 'r) sigma
val fresh_constructor_instance : ?loc:Loc.t -> Environ.env -> 'r t -> constructor ->
(pconstructor, 'r) sigma
val fresh_global : ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
'r t -> Globnames.global_reference -> (constr, 'r) sigma
(** FILLME *)
(** {5 Run} *)
type 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
val run : Evd.evar_map -> 'a run -> 'a * Evd.evar_map
(** {5 Imperative monotonic functions} *)
type evdref
(** Monotonic references over evarmaps *)
val apply : evdref -> 'a run -> 'a
(** Apply a monotonic function on a reference. *)
val purify : (evdref -> 'a) -> 'a run
(** Converse of {!apply}. *)
(** {5 Unsafe primitives} *)
module Unsafe :
sig
val le : ('a, 'b) le
val of_evar_map : Evd.evar_map -> 'r t
val of_evar : Evd.evar -> 'r evar
val of_ref : Evd.evar_map ref -> evdref
val of_pair : ('a * Evd.evar_map) -> ('a, 'r) sigma
end
(** {5 Notations} *)
module Notations :
sig
type ('a, 'r) sigma_ = ('a, 'r) sigma =
Sigma : 'a * 's t * ('r, 's) le -> ('a, 'r) sigma_
type 'a run_ = 'a run = { run : 'r. 'r t -> ('a, 'r) sigma }
val (+>) : ('a, 'b) le -> ('b, 'c) le -> ('a, 'c) le
(** Alias for {!cons} *)
end
|
