1
- (* This example implements a simplified version of Prolog and serves to
2
- illustrate the combination of implicit parameters and effect capabilities. *)
1
+ {# This example implements a simplified version of Prolog and serves to
2
+ illustrate the combination of implicit parameters and effect capabilities. #}
3
3
4
4
import List
5
5
6
- (* Prolog terms and clauses are fairly standard. Here variables are
7
- identified by integers and functors by strings. *)
6
+ {# Prolog terms and clauses are fairly standard. Here variables are
7
+ identified by integers and functors by strings. #}
8
8
data rec Term = TVar of Int | TFun of String, List Term
9
9
10
10
data Clause = Cl of Term, List Term
11
11
12
- (* The signature of the standard reader effect, with a single operation
12
+ {# The signature of the standard reader effect, with a single operation
13
13
used to obtain a value of type X. While we do not need to wrap functions
14
14
`{effect=E} -> Unit ->[E] X` in a data type to use them as capabilities,
15
- this improves readability and allows us to define methods on the type. *)
15
+ this improves readability and allows us to define methods on the type. #}
16
16
data Reader (effect E) X = Reader of (Unit ->[E] X)
17
17
18
- (* We expose the `ask` operation of `Reader` as a method. *)
18
+ {# We expose the `ask` operation of `Reader` as a method. #}
19
19
method ask {E, self = Reader ask : Reader E _} = ask
20
20
21
- (* The standard state effect, with its accompanying methods. *)
21
+ {# The standard state effect, with its accompanying methods. #}
22
22
data State (effect E) X = State of
23
23
{ get : Unit ->[E] X
24
24
, put : X ->[E] Unit
@@ -29,7 +29,7 @@ method put {E, self = State { put } : State E _} = put
29
29
30
30
method update {E, self : State E _} f = self.put (f (self.get ()))
31
31
32
- (* The standard backtracking effect. *)
32
+ {# The standard backtracking effect. #}
33
33
data BT (effect E) = BT of
34
34
{ flip : Unit ->[E] Bool
35
35
, fail : {type X} -> Unit ->[E] X
@@ -38,8 +38,8 @@ data BT (effect E) = BT of
38
38
method flip {E, self = BT { flip } : BT E} = flip
39
39
method fail {E, self = BT { fail } : BT E} = fail
40
40
41
- (* The method `choose` on `BT` non-deterministically selects an element
42
- from a list. *)
41
+ {# The method `choose` on `BT` non-deterministically selects an element
42
+ from a list. #}
43
43
method choose {E, self : BT E} =
44
44
let rec choose xs =
45
45
match xs with
@@ -48,15 +48,15 @@ method choose {E, self : BT E} =
48
48
end
49
49
in choose
50
50
51
- (* The `Fresh` effect is used to model the generation of fresh variable
52
- identifiers in the evaluator. *)
51
+ {# The `Fresh` effect is used to model the generation of fresh variable
52
+ identifiers in the evaluator. #}
53
53
data Fresh (effect E) X = Fresh of (Unit ->[E] X)
54
54
55
55
method fresh {E, self = Fresh fresh : Fresh E _} = fresh
56
56
57
- (* ========================================================================= *)
57
+ {# ========================================================================= #}
58
58
59
- (* The standard state handler, defined as a higher order function. *)
59
+ {# The standard state handler, defined as a higher order function. #}
60
60
let hState init (f : {effect=E} -> State E _ ->[E|_] _) =
61
61
handle st = State
62
62
{ get = effect () / r => fn s => r s s
@@ -66,8 +66,8 @@ let hState init (f : {effect=E} -> State E _ ->[E|_] _) =
66
66
finally f => f init
67
67
in f st
68
68
69
- (* A handler for backtracking which returns the first result wrapped in Some,
70
- or None if no result is available. *)
69
+ {# A handler for backtracking which returns the first result wrapped in Some,
70
+ or None if no result is available. #}
71
71
let hBT (f : {effect=E} -> BT E ->[E|_] _) =
72
72
handle bt = BT
73
73
{ flip = effect () / r =>
@@ -80,9 +80,9 @@ let hBT (f : {effect=E} -> BT E ->[E|_] _) =
80
80
return x => Some x
81
81
in f bt
82
82
83
- (* ========================================================================= *)
84
- (* The following few functions on lists require a notion of equality, which is
85
- passed as the implicit parameter `~eq`. *)
83
+ {# ========================================================================= #}
84
+ {# The following few functions on lists require a notion of equality, which is
85
+ passed as the implicit parameter `~eq`. #}
86
86
87
87
implicit ~eq
88
88
@@ -101,9 +101,9 @@ let rec assoc x xs =
101
101
| (y, v) :: xs => if ~eq x y then Some v else assoc x xs
102
102
end
103
103
104
- (* ========================================================================= *)
105
- (* Methods on terms and clauses that are useful for implementing variable
106
- refreshing. *)
104
+ {# ========================================================================= #}
105
+ {# Methods on terms and clauses that are useful for implementing variable
106
+ refreshing. #}
107
107
108
108
method vars =
109
109
let ~eq (x : Int) = x.equal in
@@ -134,26 +134,26 @@ method rename sub =
134
134
method rename { self = Cl t ts } sub =
135
135
Cl (t.rename sub) (List.map (fn (t : Term) => t.rename sub) ts)
136
136
137
- (* ========================================================================= *)
137
+ {# ========================================================================= #}
138
138
139
- (* The instantiation of unification variables is represented using `State`
139
+ {# The instantiation of unification variables is represented using `State`
140
140
containing an association list of instantiations. As this effect is pervasive
141
141
throughout our implementation, we declare it as an implicit, so that it and
142
- the associated effect variable E_st are generalized automatically. *)
142
+ the associated effect variable E_st are generalized automatically. #}
143
143
implicit ~st {E_st} : State E_st (List (Pair Int Term))
144
144
145
- (* We also define a pair of functions that let us modify and read `~st`. *)
145
+ {# We also define a pair of functions that let us modify and read `~st`. #}
146
146
147
147
let setVar (x : Int) t = ~st.update (fn xs => (x, t) :: xs)
148
148
149
149
let getVar x =
150
150
let ~eq (x : Int) = x.equal in
151
151
assoc x (~st.get ())
152
152
153
- (* The `view` method on terms can be used to view the outer-most shape of a
153
+ {# The `view` method on terms can be used to view the outer-most shape of a
154
154
term, accounting for the instantiation of unification variables.
155
155
In a realistic implementation we would keep terms that haven't been viewed
156
- abstract to prevent accidentally pattern-matching on them. *)
156
+ abstract to prevent accidentally pattern-matching on them. #}
157
157
method rec view {self : Term} =
158
158
match self with
159
159
| TVar x =>
@@ -167,34 +167,34 @@ method rec view {self : Term} =
167
167
| TFun f ts => self
168
168
end
169
169
170
- (* As with `~st`, the capability to generate fresh identifiers ~fresh is also
171
- declared implicit. *)
170
+ {# As with `~st`, the capability to generate fresh identifiers ~fresh is also
171
+ declared implicit. #}
172
172
implicit ~fresh {E_fresh} : Fresh E_fresh Int
173
173
174
- (* To further reduce verbosity, we define a function `fresh` to call the
175
- `fresh` method of the implicit capability. *)
174
+ {# To further reduce verbosity, we define a function `fresh` to call the
175
+ `fresh` method of the implicit capability. #}
176
176
let fresh () = ~fresh.fresh ()
177
177
178
- (* We attach additional `refresh` methods to terms and clauses, which replace
179
- all the variables in terms with fresh unification variables. *)
178
+ {# We attach additional `refresh` methods to terms and clauses, which replace
179
+ all the variables in terms with fresh unification variables. #}
180
180
181
181
method refresh {self : Term} =
182
182
self.rename (List.map (fn x => (x, fresh ())) self.vars)
183
183
184
184
method refresh {self : Clause} =
185
185
self.rename (List.map (fn x => (x, fresh ())) self.vars)
186
186
187
- (* ========================================================================= *)
187
+ {# ========================================================================= #}
188
188
189
- (* Finally, we make the interpreter's knowledge base and the backtracking
189
+ {# Finally, we make the interpreter's knowledge base and the backtracking
190
190
capability implicit as well. The knowledge base is represented as a reader
191
- effect providing a simple list of clauses. *)
191
+ effect providing a simple list of clauses. #}
192
192
implicit ~kb {E_kb} : Reader E_kb (List Clause)
193
193
implicit ~bt {E_bt} : BT E_bt
194
194
195
195
let fail () = ~bt.fail ()
196
196
197
- (* Check whether a variable occurs in a term. *)
197
+ {# Check whether a variable occurs in a term. #}
198
198
method occurs (x : Int) =
199
199
let rec occurs (t : Term) =
200
200
match t.view with
@@ -203,7 +203,7 @@ method occurs (x : Int) =
203
203
end
204
204
in occurs self
205
205
206
- (* Attempt to unify two terms, and signal the need to backtrack on failure. *)
206
+ {# Attempt to unify two terms, and signal the need to backtrack on failure. #}
207
207
let rec unify (t1 : Term) (t2 : Term) =
208
208
match t1.view, t2.view with
209
209
| TVar x, TVar y =>
@@ -217,24 +217,24 @@ let rec unify (t1 : Term) (t2 : Term) =
217
217
else fail ()
218
218
end
219
219
220
- (* Retrieve some clause from the knowledge base non-deterministically. *)
220
+ {# Retrieve some clause from the knowledge base non-deterministically. #}
221
221
let kbChoose () = ~bt.choose (~kb.ask ())
222
222
223
- (* Try to derive a term using the knowledge base. *)
223
+ {# Try to derive a term using the knowledge base. #}
224
224
let rec eval (t : Term) =
225
225
let Cl t' ts = (kbChoose ()).refresh in
226
226
let _ = unify t t' in
227
227
List.iter eval ts
228
228
229
- (* Perform a query by substituting fresh unification variables in a term and
230
- calling the `eval` function. *)
229
+ {# Perform a query by substituting fresh unification variables in a term and
230
+ calling the `eval` function. #}
231
231
let query (t : Term) = eval t.refresh
232
232
233
- (* ========================================================================= *)
234
- (* Below we finally install some handlers for the interpreter and show its
235
- use on a simple hardcoded query. *)
233
+ {# ========================================================================= #}
234
+ {# Below we finally install some handlers for the interpreter and show its
235
+ use on a simple hardcoded query. #}
236
236
237
- (* Example database. *)
237
+ {# Example database. #}
238
238
let kb = [Cl (TFun "f" [TVar 0, TVar 0]) []]
239
239
240
240
handle ~kb = Reader (fn () => kb)
@@ -247,7 +247,7 @@ let _ =
247
247
match
248
248
hBT (fn ~bt =>
249
249
hState [] (fn ~st =>
250
- (* Example query. *)
250
+ {# Example query. #}
251
251
query (TFun "f" [TFun "a" [], TFun "a" []])))
252
252
with
253
253
| Some _ => printStrLn "Yes."
0 commit comments