blob: fa4392368c6f321b0f0812c9371f1b4611a57072 (
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
|
(* This is an interface for the code extracted from bootstrap/Monad.v.
The relevant comments are overthere. *)
type ('a, 'b) list_view =
| Nil of exn
| Cons of 'a * 'b
type proofview = { initial : (Term.constr * Term.types) list;
solution : Evd.evar_map; comb : Goal.goal list }
type logicalState = proofview
type logicalEnvironment = Environ.env
(** status (safe/unsafe) * ( shelved goals * given up ) *)
type logicalMessageType = bool * ( Goal.goal list * Goal.goal list )
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)) list_view) t
val lift : 'a NonLogical.t -> 'a t
val run : 'a t -> logicalEnvironment -> logicalState -> (('a*logicalState)*logicalMessageType) NonLogical.t
end
|
