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
130
131
|
(************************************************************************)
(* 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. To this
ends, it defines a type of indexed evarmaps whose phantom typing ensures
monotonous use.
*)
(** {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. This is just a plain evarmap with a phantom type. *)
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 ->
Evd.rigid -> 'r t -> (Univ.universe_level, 'r) sigma
val new_univ_variable : ?loc:Loc.t -> ?name:string ->
Evd.rigid -> 'r t -> (Univ.universe, 'r) sigma
val new_sort_variable : ?loc:Loc.t -> ?name:string ->
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
|
