blob: bdebe658c198147549617d504d4f4a1f430671b1 (
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
|
(* This is an interface for the code extracted from bootstrap/Monad.v.
The relevant comments are overthere. *)
type proofview = { initial : (Term.constr * Term.types) list;
solution : Evd.evar_map; comb : Goal.goal list }
type logicalState = proofview
type logicalEnvironment = Environ.env
type logicalMessageType = bool
module NonLogical : sig
type +'a t
type 'a ref
val ret : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val ignore : 'a t -> unit t
val seq : unit t -> 'a t -> 'a t
val new_ref : 'a -> 'a ref t
val set : 'a ref -> 'a -> unit t
val get : 'a ref -> 'a t
val read_line : string t
val print_char : char -> unit t
val print : Pp.std_ppcmds -> unit t
val raise : exn -> 'a t
val catch : 'a t -> (exn -> 'a t) -> 'a t
val timeout : int -> 'a t -> 'a t
(* [run] performs effects. *)
val run : 'a t -> 'a
end
module Logical : sig
type +'a t
val ret : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val ignore : 'a t -> unit t
val seq : unit t -> 'a t -> 'a t
val set : logicalState -> unit t
val get : logicalState t
val put : logicalMessageType -> unit t
val current : logicalEnvironment t
val zero : exn -> 'a t
val plus : 'a t -> (exn -> 'a t) -> 'a t
val split : 'a t -> (('a*(exn->'a t),exn) Util.union) t
val lift : 'a NonLogical.t -> 'a t
val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t
end
|
