-
Notifications
You must be signed in to change notification settings - Fork 1
/
combinators2.ml
124 lines (100 loc) · 2.92 KB
/
combinators2.ml
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
open Derivations2
module type MONAD = sig
type 'a m
val return: 'a -> 'a m
val bind: 'a m -> ('a -> 'b m) -> 'b m
val ( >>= ): 'a m -> ('a -> 'b m) -> 'b m
val nothing: 'a m
val extract: 'a m -> 'a option
val search: ('a -> 'b m) -> 'a list -> 'b m
end
module MOption: MONAD with type 'a m = 'a option = struct
type 'a m = 'a option
let return x = Some x
let bind x f =
match x with
| Some x -> f x
| None -> None
let ( >>= ) = bind
let nothing = None
let extract x = x
let rec search f l =
match l with
| [] -> None
| x :: xs ->
match f x with
| Some x -> Some x
| None -> search f xs
end
module MExplore: MONAD with type 'a m = 'a LazyList.t = struct
open LazyList
type 'a m = 'a t
let return = one
let bind x f = flattenl (map f x)
let ( >>= ) = bind
let nothing = nil
let extract x =
match next x with
| Nil -> None
| Cons (x, _) -> Some x
let search f l =
bind (of_list l) f
end
module type MONOID = sig
type a
val empty: a
val append: a -> a -> a
end
module WriterT (M: MONAD) (L: MONOID): sig
type 'a m = (L.a * 'a) M.m
val return: 'a -> 'a m
val tell: L.a -> unit m
val bind: 'a m -> ('a -> 'b m) -> 'b m
val ( >>= ): 'a m -> ('a -> 'b m) -> 'b m
end = struct
type 'a m = (L.a * 'a) M.m
let return x = M.return (L.empty, x)
let tell log = M.return (log, ())
let bind x f =
M.bind x (fun (log, x) ->
M.bind (f x) (fun (log', y) ->
M.return (L.append log log', y)))
let ( >>= ) = bind
end
module Make(Logic: LOGIC)(M: MONAD) = struct
module Proofs = Derivations2.Make(Logic)
(* The monoid of derivation lists. *)
module L: MONOID with type a = Proofs.derivation list = struct
type a = Proofs.derivation list
let empty = []
let append = List.append
end
include WriterT(M)(L)
include Proofs
(* The result of a proof search. *)
type 'a outcome =
('a * derivation) M.m
(* Injection of an ['a outcome] into the monad (it becomes a premise). *)
let premise (outcome: 'a outcome): 'a m =
M.bind outcome (fun (env, derivation) ->
tell [ derivation ] >>= fun () ->
return env
)
(* Equivalent of [runMProof]: collect the premises in order to compute the
* outcome. *)
let prove (goal: goal) (x: ('a * rule_name) m): 'a outcome =
M.(x >>= fun (premises, (env, rule)) ->
return (env, (goal, (rule, Premises premises))))
(* Create an outcome from an axiom. *)
let axiom (env: 'a) (goal: goal) (axiom: rule_name): 'a outcome =
prove goal (return (env, axiom))
(* The failed outcome. *)
let fail: 'a outcome =
M.nothing
(* Multiple choices -- may or may not backtrack, depending on [M]. *)
let choice (goal: goal) (args: 'a list) (f: 'a -> ('b * rule_name) m): 'b outcome =
M.search (fun x -> prove goal (f x)) args
(* Syntactic convenience operator: it's nice to end proof with [qed]! *)
let qed r e =
return (e, r)
end