• R/O
  • HTTP
  • SSH
  • HTTPS

提交

标签
No Tags

Frequently used words (click to add to your profile)

javac++androidlinuxc#windowsobjective-ccocoa誰得qtpythonphprubygameguibathyscaphec計画中(planning stage)翻訳omegatframeworktwitterdomtestvb.netdirectxゲームエンジンbtronarduinopreviewer

A categorical programming language


Commit MetaInfo

修订版11c65e3a9b88211bce593edcd4ab09fa5efd24b4 (tree)
时间2023-03-24 14:13:43
作者Corbin <cds@corb...>
CommiterCorbin

Log Message

Use a side stack for folding lists in CAM.

This Forth-inspired hack seems like a reasonable alternative to
recursion, and hopefully is more legible to the GC than stack frames.

Everything worked on the first try, modulo RPython translation errors.
This is not normal, and I poked around a bit to double-check the
correctness of output.

更改概述

差异

--- a/movelist/cammy-repl.scm
+++ b/movelist/cammy-repl.scm
@@ -173,6 +173,7 @@
173173 (car tys))))
174174
175175 (define (cammy-display-template expr)
176+ (set! most-recent-template expr)
176177 (display expr) (display (format-type-judgement (expr->ty expr))) (newline))
177178
178179 (define (cammy-display index)
@@ -269,7 +270,8 @@
269270 [(? list? l)
270271 (cons (car l) (map (lambda (t) (apply-template t vars)) (cdr l)))]))
271272
272-(define most-recent-expr 'id)
273+(define most-recent-expr #f)
274+(define most-recent-template #f)
273275
274276 (define (lookup name)
275277 (let
--- /dev/null
+++ b/prims.json
@@ -0,0 +1,36 @@
1+[
2+ "id",
3+ "ignore",
4+ "fst",
5+ "snd",
6+ "swap",
7+ "dup",
8+ "left",
9+ "right",
10+ "t",
11+ "f",
12+ "conj",
13+ "disj",
14+ "not",
15+ "either",
16+ "zero",
17+ "succ",
18+ "nil",
19+ "cons",
20+ "f-zero",
21+ "f-one",
22+ "f-pi",
23+ "f-sign",
24+ "f-lt",
25+ "f-negate",
26+ "f-recip",
27+ "f-sin",
28+ "f-cos",
29+ "f-exp",
30+ "f-floor",
31+ "f-sqrt",
32+ "f-log1p",
33+ "f-add",
34+ "f-mul",
35+ "f-atan2"
36+]
--- a/sampler/cammylib/arrows.py
+++ b/sampler/cammylib/arrows.py
@@ -3,7 +3,7 @@ import math
33 from rpython.rlib.objectmodel import specialize
44 # from rpython.rlib.rbigint import rbigint
55
6-from cammylib.elements import B, F, N, T
6+from cammylib.elements import F, N, thePoint, theTrue, theFalse, endOfList
77
88
99 def arrowEq(arr1, arr2): return arr1 is arr2 or arr1.eq(arr2)
@@ -37,7 +37,7 @@ class Comp(Arrow):
3737
3838 class Ignore(Arrow):
3939 _immutable_ = True
40- def compileCAM(self, compiler): compiler.quote(T())
40+ def compileCAM(self, compiler): compiler.quote(thePoint)
4141 def types(self, cs): return cs.fresh(), cs.concrete("1")
4242
4343 class First(Arrow):
@@ -250,7 +250,7 @@ class PrimRec(Arrow):
250250
251251 def compileCAM(self, compiler):
252252 compiler.push()
253- compiler.quote(T())
253+ compiler.quote(thePoint)
254254 self._x.compileCAM(compiler)
255255 compiler.swap()
256256 # At the top of the loop, the nat is in the register.
@@ -276,7 +276,7 @@ class PrimRec(Arrow):
276276
277277 class Nil(Arrow):
278278 _immutable_ = True
279- def compileCAM(self, compiler): compiler.quote(T())
279+ def compileCAM(self, compiler): compiler.quote(endOfList)
280280 def types(self, cs):
281281 return cs.concrete("1"), cs.functor("list", [cs.fresh()])
282282
@@ -301,29 +301,34 @@ class Fold(Arrow):
301301 # Folds in CAM/ZINC are always foldl, but Cammy is always foldr.
302302 # So, we reverse the input list before folding.
303303 # Conveniently, this can be done with foldl!
304- self.compileBody(Ignore(), Cons(), compiler)
304+ # self.compileBody(Ignore(), Cons(), compiler)
305305 self.compileBody(self._n, self._c, compiler)
306306
307307 def compileBody(self, nil, cons, compiler):
308- compiler.push()
309- compiler.quote(T())
308+ # Stash the entire list onto the side stack.
309+ compiler.startList()
310+ compiler.quote(thePoint)
310311 nil.compileCAM(compiler)
311- compiler.swap()
312- # At the top of the loop, the rest of the list is in the register.
312+ # At the top of the loop, the accumulator is in the register and the
313+ # rest of the list is in the side stack.
313314 loop = compiler.here()
314315 compiler.push()
315- compiler.isNil()
316+ compiler.iter()
317+ compiler.push()
318+ # This test is backwards, so we swap before jumping.
319+ compiler.isEndOfList()
320+ compiler.sumSwap()
316321 compiler.gotoRight()
317322 isNil = compiler.jumpForward()
318323 compiler.pop()
319- compiler.swap()
320- compiler.assoc()
324+ compiler.cons()
325+ compiler.pairSwap()
321326 cons.compileCAM(compiler)
322- compiler.swap()
323327 compiler.goto()
324328 compiler.jumpBackwardTo(loop)
325329 compiler.jumpHere(isNil)
326- # Pop the point from the isNil check, and then pop the (nil) list.
330+ # There are two points on top of the accumulator. Pop the point from
331+ # the isNil check, and then pop endOfList.
327332 compiler.pop()
328333 compiler.pop()
329334
@@ -398,8 +403,8 @@ unaryFunctors = {
398403 "left": Left(),
399404 "right": Right(),
400405 "either": Either(),
401- "t": makeConstant(B(True), "2"),
402- "f": makeConstant(B(False), "2"),
406+ "t": makeConstant(theTrue, "2"),
407+ "f": makeConstant(theFalse, "2"),
403408 "not": NotArr(),
404409 "conj": Conj(),
405410 "disj": Disj(),
--- a/sampler/cammylib/cam.py
+++ b/sampler/cammylib/cam.py
@@ -4,7 +4,7 @@ from rpython.rlib.jit import JitDriver, isconstant, we_are_jitted
44 from rpython.rlib.rvmprof import get_unique_id, register_code, register_code_object_class, vmprof_execute_code
55
66 from cammylib.arrows import indexOfArrow
7-from cammylib.elements import B, F, L, N, P, R, T, equal
7+from cammylib.elements import F, L, N, P, R, T, eltsEq, endOfList, theBool, thePoint, theTrue, theFalse
88
99 # A basic CAM, as in the original paper:
1010 # https://doi.org/10.1016/0167-6423(87)90020-7
@@ -12,9 +12,9 @@ from cammylib.elements import B, F, L, N, P, R, T, equal
1212 # The original core opcodes.
1313 (QUOTE, CUR, PUSH, POP, SWAP, CONS, APP, RET, GOTO, HALT,
1414 # Custom opcodes for our structures.
15-GOTORIGHT,
15+GOTORIGHT, STARTLIST, ITER,
1616 # Custom opcodes for our data.
17-ASSOC) = range(12)
17+ASSOC) = range(14)
1818
1919 # To facilitate profiling, the term operations are factored out into a table.
2020
@@ -37,20 +37,24 @@ register_code_object_class(TermOp, lambda op: "cam:%s:0:builtin" % op.name)
3737
3838 # Some term ops are too complicated for an inline lambda.
3939
40+def sumSwap(term):
41+ isLeft, x = term.asSum()
42+ return R(x) if isLeft else L(x)
43+
4044 def predMaybe(term):
4145 n = term.n()
42- return L(N(n - 1)) if n else R(T())
46+ return L(N(n - 1)) if n else R(thePoint)
4347
4448 def lessThan(term):
4549 f1 = term.first().f()
4650 f2 = term.second().f()
47- return B(True) if f1 == -0.0 and f2 == 0.0 else B(f1 < f2)
51+ return theTrue if f1 == -0.0 and f2 == 0.0 else theBool(f1 < f2)
4852
4953 def floor(f):
5054 try:
5155 return L(F(float(math.floor(f))))
5256 except (ValueError, OverflowError):
53- return R(T())
57+ return R(thePoint)
5458
5559 def add(y, z):
5660 # The only time addition can NaN is Infinity - Infinity, which is 0.0.
@@ -89,34 +93,34 @@ def recip(f):
8993
9094 def sign(f): return abs(f) == f
9195
92-def sqrt(f): return L(F(math.sqrt(f))) if sign(f) else R(T())
96+def sqrt(f): return L(F(math.sqrt(f))) if sign(f) else R(thePoint)
9397
94-def log1p(f): return L(F(math.log1p(f))) if f > -1.0 else R(T())
98+def log1p(f): return L(F(math.log1p(f))) if f > -1.0 else R(thePoint)
9599
96100 termOps = [
97101 # Core term ops.
98102 TermOp("fst", lambda term: term.first()),
99103 TermOp("snd", lambda term: term.second()),
100- TermOp("branch", lambda term: L(T()) if term.b() else R(T())),
104+ TermOp("branch", lambda term: L(thePoint) if term.b() else R(thePoint)),
101105 TermOp("dup", lambda term: P(term, term)),
102106 TermOp("pairSwap", lambda term: P(term.second(), term.first())),
103107 # Custom structure term ops.
104108 TermOp("left", lambda term: L(term)),
105- TermOp("right",lambda term: R(term)),
109+ TermOp("right", lambda term: R(term)),
110+ TermOp("sumSwap", sumSwap),
106111 # Custom data term ops.
107- TermOp("notOp", lambda term: B(not term.b())),
108- TermOp("andOp", lambda term: B(term.first().b() and term.second().b())),
109- TermOp("orOp", lambda term: B(term.first().b() or term.second().b())),
112+ TermOp("notOp", lambda term: theBool(not term.b())),
113+ TermOp("andOp", lambda term: theBool(term.first().b() and term.second().b())),
114+ TermOp("orOp", lambda term: theBool(term.first().b() or term.second().b())),
110115 TermOp("predMaybe", predMaybe),
111116 TermOp("succ", lambda term: N(term.n() + 1)),
112117 TermOp("nDouble", lambda term: N(term.n() << 1)),
113118 TermOp("nAdd", lambda term: N(term.first().n() + term.second().n())),
114119 TermOp("nMul", lambda term: N(term.first().n() * term.second().n())),
115- # XXX confusingly backwards name
116- TermOp("isNil",
117- lambda term: L(T()) if not isinstance(term, T) else R(T())),
120+ TermOp("isEndOfList",
121+ lambda term: L(thePoint) if term is endOfList else R(thePoint)),
118122 # Custom floating-point term ops.
119- TermOp("sign", lambda term: B(sign(term.f()))),
123+ TermOp("sign", lambda term: theBool(sign(term.f()))),
120124 TermOp("floor", lambda term: floor(term.f())),
121125 TermOp("negate", lambda term: F(-term.f())),
122126 TermOp("recip", lambda term: F(recip(term.f()))),
@@ -136,7 +140,7 @@ print "CAM: Created %d term ops" % len(termOps)
136140
137141 ops = [
138142 "QUOTE", "CUR", "PUSH", "POP", "SWAP", "CONS", "APP", "RET", "GOTO",
139- "HALT", "GOTORIGHT", "ASSOC",
143+ "HALT", "GOTORIGHT", "STARTLIST", "ITER", "ASSOC",
140144 ]
141145 def hasParam(op):
142146 return op in (QUOTE, CUR, GOTO, GOTORIGHT)
@@ -208,7 +212,10 @@ def runTermOp(op, term):
208212 @vmprof_execute_code("cam", get_code_fn=lambda cam, term: cam)
209213 def runCAM(cam, term):
210214 pc = 0
211- stack = T()
215+ stack = thePoint
216+ # My way of avoiding recursion when folding: Values are pushed to a
217+ # secondary stack.
218+ sideStack = []
212219
213220 while pc < len(cam.code):
214221 CAMDriver.jit_merge_point(pc=pc, cam=cam,
@@ -262,12 +269,16 @@ def runCAM(cam, term):
262269 elif op == GOTORIGHT:
263270 isLeft, term = term.asSum()
264271 address = code[pc]
265- if isLeft:
266- pc += 1
267- else:
268- pc = address
272+ pc = pc + 1 if isLeft else address
269273 CAMDriver.can_enter_jit(pc=pc, cam=cam,
270274 term=term, stack=stack)
275+ elif op == STARTLIST:
276+ sideStack.append(endOfList)
277+ while term is not endOfList:
278+ sideStack.append(term.first())
279+ term = term.second()
280+ elif op == ITER:
281+ term = sideStack.pop()
271282 elif op == ASSOC:
272283 pair = stack.first()
273284 term = P(pair.first(), term)
@@ -330,7 +341,7 @@ class Compiler(object):
330341 def addConstant(self, constant):
331342 # XXX should use a set somehow
332343 for i, const in enumerate(self.constants):
333- if equal(const, constant):
344+ if eltsEq(const, constant):
334345 return i
335346 else:
336347 c = len(self.constants)
@@ -416,6 +427,8 @@ class Compiler(object):
416427 def goto(self): self.emit(GOTO)
417428 def halt(self): self.emit(HALT)
418429 def gotoRight(self): self.emit(GOTORIGHT)
430+ def startList(self): self.emit(STARTLIST)
431+ def iter(self): self.emit(ITER)
419432 def assoc(self): self.emit(ASSOC)
420433
421434 for i, op in enumerate(termOps):
--- a/sampler/cammylib/elements.py
+++ b/sampler/cammylib/elements.py
@@ -38,12 +38,17 @@ class Element(object):
3838 class T(Element):
3939 _immutable_ = True
4040 def asStr(self): return "*"
41+thePoint = T()
42+endOfList = T()
4143
4244 class B(Element):
4345 _immutable_ = True
4446 def __init__(self, b): self._b = b
4547 def b(self): return self._b
4648 def asStr(self): return "true" if self._b else "false"
49+theTrue = B(True)
50+theFalse = B(False)
51+def theBool(b): return theTrue if b else theFalse
4752
4853 class N(Element):
4954 _immutable_ = True
@@ -110,23 +115,18 @@ class R(Element):
110115 return "R(%s)" % self._x.asStr()
111116
112117
113-def equal(e1, e2):
114- if e1 is e2:
115- return True
118+def eltsEq(e1, e2):
119+ if e1 is e2: return True
116120 return False
117- # if isinstance(e1, T) and isinstance(e2, T):
118- # return True
119- # elif isinstance(e1, B) and isinstance(e2, B):
120- # return e1.b() == e2.b()
121121 # elif isinstance(e1, N) and isinstance(e2, N):
122122 # return e1.n() == e2.n()
123123 # elif isinstance(e1, F) and isinstance(e2, F):
124124 # # XXX should use same code as user-level eq
125125 # return e1.f() == e2.f()
126126 # elif isinstance(e1, P) and isinstance(e2, P):
127- # return (equal(e1.first(), e2.first())
128- # and equal(e1.second(), e2.second()))
127+ # return (eltsEq(e1.first(), e2.first())
128+ # and eltsEq(e1.second(), e2.second()))
129129 # elif isinstance(e1, L) and isinstance(e2, L):
130- # return equal(e1._x, e2._x)
130+ # return eltsEq(e1._x, e2._x)
131131 # elif isinstance(e1, R) and isinstance(e2, R):
132- # return equal(e1._x, e2._x)
132+ # return eltsEq(e1._x, e2._x)
--- a/todo.txt
+++ b/todo.txt
@@ -32,6 +32,7 @@
3232 * Attempted to implement them, but ran into a problem: tree traversals on
3333 CAM are not obvious
3434 * Defunctionalization might work: can the tree traversal be linearized?
35+ * Can be linearized on a second stack...
3536 * I know how to compile to cats!
3637 * For cat of interest, make hive/cats/cat/id, hive/cats/cat/comp, etc.
3738 * Then, we'll apply a stack of functors by just looking up each layer in the
@@ -139,8 +140,7 @@
139140 does a linear number of heap allocations
140141 * fun/app = (uncurry id)
141142 * done
142- * uncurry distills down to fun/app, as in the literature
143- * (uncurry @0) could be defined as (comp (pair/mapfst @0) fun/app)
143+ * (uncurry @0) could be defined as (comp (pair/mapfst @0) fun/app)
144144 * list/uncons
145145 * has particularly simple bytecode, becoming a term op
146146 * Missing optimizations
@@ -203,20 +203,21 @@
203203 * Given f : X -> Y, (dmap f): DX -> DY
204204 * Given a : X -> DY, (dchain m) : DX -> DY
205205 * With trampoline monad, all of this should be possible
206-* Priority queues
207- * Given min : X × X -> X
208- * findMin : Q -> X + 1
209- * insert : X x Q -> Q
210- * meld : Q × Q -> Q
211- * deleteMin: Q -> Q + 1
212- * empty : 1 -> Q
213- * empty? : Q -> 2
214- * (comp (comp (pair @0 (fun/const empty)) insert) findMin) == (comp @0 left)
215-* An optimized natset: [N] × N × [N, 2]
216- * The idea is that it's just [N, 2], but with a memoizing cache
217- * The list stores all of the members
218- * The lone nat is the lower bound for what's been checked so far
219- * (ns, k, f) where ns = { f(n) | n < k }
206+* Advanced data structures (requires state monad)
207+ * Priority queues
208+ * Given min : X × X -> X
209+ * findMin : Q -> X + 1
210+ * insert : X x Q -> Q
211+ * meld : Q × Q -> Q
212+ * deleteMin: Q -> Q + 1
213+ * empty : 1 -> Q
214+ * empty? : Q -> 2
215+ * (comp (comp (pair @0 (fun/const empty)) insert) findMin) == (comp @0 left)
216+ * An optimized natset: [N] × N × [N, 2]
217+ * The idea is that it's just [N, 2], but with a memoizing cache
218+ * The list stores all of the members
219+ * The lone nat is the lower bound for what's been checked so far
220+ * (ns, k, f) where ns = { f(n) | n < k }
220221 * Isomorphisms
221222 * CCC isos are fully characterized by a list of axioms
222223 * https://en.wikipedia.org/wiki/Cartesian_closed_category#Equational_theory
@@ -357,3 +358,27 @@
357358 * Cammy is compositional
358359 * Cammy is chimeric
359360 * Cammy is category-theoretic
361+* REPL features
362+ * Save templates
363+ * Half-implemented, need to encode templates as JSON
364+ * Save jets
365+ * Had a false start, but should be straightforward
366+* Hoare logic
367+ * Assume some arrow f : X → Y
368+ * f's preconditions are like pre : X → 2 guarding subtypes of X
369+ * f's postconditions are like post : Y → 2 guarding subtypes of Y
370+ * f fulfills a precondition when (comp f post) = pre
371+ * Example: n * 2 is even for all n
372+ * f is n-double : N → N
373+ * precondition is trivially (comp ignore t) : N → 2
374+ * postcondition is nat/even? (pr t not) : N → 2
375+ * So then (comp n-double (pr t not)) = (comp ignore t)
376+* Scratchpad
377+ * (comp (list/map f) (list/map g))
378+ = (comp (fold nil (comp (pair (comp fst f) snd) cons)) (fold nil (comp (pair (comp fst g) snd) cons)))
379+ ...
380+ = (comp (fold nil (comp (pair (comp fst (comp f g)) snd) cons)))
381+ * Elliot's important monoids
382+ * nats under addition
383+ * lists/strings
384+ * goal: express that length is a monoid homomorphism