提交: dced8f9d1557e94b91e62630f19b29d4c70d0e33 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修訂: dced8f9d1557e94b91e62630f19b29d4c70d0e33 (tree)
• 時間: 2022-12-28 12:10:43
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Rewrite djinn core.

Now we pull apart types first, synthesizing expressions from the pieces.
The results are quite good; with only a few tactics, we are able to
synthesize all of the existing testcases, including the three that used
to fail.

Change Summary

• modified: accept-jelly.py
• modified: movelist/cammyo.scm
• modified: movelist/movelist.scm

差異

--- a/accept-jelly.py
+++ b/accept-jelly.py
@@ -6,7 +6,7 @@ import sys
 movelist = sys.argv[-2]
 jelly = sys.argv[-1]
 timeout = 5
-difficulty = 15
+difficulty = 5
 
 def jellify(expr):
     return subprocess.run([jelly], input=expr.encode("utf-8"),

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -1,32 +1,12 @@
-(module cammyo (cammy° normal-form°)
+(module cammyo (cammy° cammy-prim° cammy-synth°)
   (import scheme)
+  (import (chicken pretty-print))
   (import (mini-kanren))
 
-  ; Require that a Cammy expression is in a basic normal form.
-  (define (normal-form° expr)
-    (fresh (x y)
-      ; NF: disallow (comp id ...) and (comp ... id)
-      (=/= expr `(comp id ,x))
-      (=/= expr `(comp ,x id))
-      ; NF: disallow (comp ... ignore)
-      (=/= expr `(comp ,x ignore))
-      ; NF: disallow (comp left/right (case ...))
-      (=/= expr `(comp left (case ,x ,y)))
-      (=/= expr `(comp right (case ,x ,y)))
-      ; NF: disallow (comp (pair ...) fst/snd)
-      (=/= expr `(comp (pair ,x ,y) fst))
-      (=/= expr `(comp (pair ,x ,y) snd))
-      ; NF: disallow (curry (uncurry ...)) and (uncurry (curry ...))
-      (=/= expr `(curry (uncurry ,x)))
-      (=/= expr `(uncurry (curry ,x)))
-      ))
-
-  ; Expr <=> Ty × Ty
-  ; Relate a Cammy expression to its input and output types.
-  ; cammy° is functional; expr fixes s and t together.
-  (define (cammy° expr s t)
-    (fresh ()
-    ; (project (expr s t) (begin (pp `(enter ,expr ,s ,t)) succeed))
+  ; Relate a monomorphic Cammy primitive to its input and output types.
+  ; This relation is just a table.
+  ; Expr <-> Ty × Ty
+  (define (cammy-prim° expr s t)
     (conde
       ; Boolean algebra
       ((== expr 't) (== s '1) (== t '2))
@@ -52,6 +32,20 @@
       ((== expr 'f-atan2) (== s '(pair F F)) (== t 'F))
       ((== expr 'f-exp) (== s 'F) (== t 'F))
       ((== expr 'f-log1p) (== s 'F) (== t '(sum F 1)))
+      ; NNO
+      ((== expr 'succ) (== s 'N) (== t 'N))
+      ((== expr 'zero) (== s '1) (== t 'N))
+      ((== expr 'n-pred-maybe) (== s 'N) (== t '(sum N 1)))
+      ((== expr 'n-add) (== s '(pair N N)) (== t 'N))
+      ))
+
+  ; Relate a Cammy expression to its input and output types.
+  ; cammy° is functional; expr fixes s and t together.
+  ; Expr <-> Ty × Ty
+  (define (cammy° expr s t)
+    (conde
+      ; Primitives
+      ((cammy-prim° expr s t))
       ; Cartesian Closed Categories
       ((fresh (f y z) (== expr `(curry ,f))
               (== t `(hom ,y ,z)) (cammy° f `(pair ,s ,y) z)))
@@ -72,24 +66,82 @@
       ((fresh (f g s1 s2) (== expr `(case ,f ,g))
               (== s `(sum ,s1 ,s2)) (cammy° f s1 t) (cammy° g s2 t)))
       ; NNO
-      ((== expr 'succ) (== s 'N) (== t 'N))
-      ((== expr 'zero) (== s '1) (== t 'N))
       ((fresh (x f) (== expr `(pr ,x ,f))
               (== s 'N) (cammy° x '1 t) (cammy° f t t)))
-      ((== expr 'n-pred-maybe) (== s 'N) (== t '(sum N 1)))
-      ((== expr 'n-add) (== s '(pair N N)) (== t 'N))
       ; Free Monoids
       ((== expr 'cons) (fresh (l) (== s `(pair ,l ,t)) (== t `(list ,l))))
       ((== expr 'nil) (== s '1) (fresh (l) (== t `(list ,l))))
       ((fresh (x f l) (== expr `(fold ,x ,f))
               (== s `(list ,l)) (cammy° x '1 t) (cammy° f `(pair ,l ,t) t)))
       ; Terminal Object
-      ((== expr 'ignore) (== t '1))
+      ; NB: ignore : X -> 1 but only when X ≠ 1, because otherwise it is the unique
+      ; arrow,  id : 1 -> 1
+      ((== expr 'ignore) (=/= s '1) (== t '1))
       ; Categories
       ((== expr 'id) (== s t))
-      ((fresh (f g y) (== expr `(comp ,f ,g))
-              (cammy° f s y) (cammy° g y t)))
-      )
-    ; (project (expr s t) (begin (pp `(exit ,expr ,s ,t)) succeed))
-  ))
+      ((fresh (f g) (== expr `(comp ,f ,g))
+              (fresh (y) (cammy° f s y) (cammy° g y t))))
+      ))
+
+  ; Syntactic composition enforcing normal form. This is just a synthesis helper.
+  ; Cammy × Cammy <-> Cammy
+  (define (comp-s° f g fg) (=/= f 'id) (=/= g 'id) (== fg `(comp ,f ,g)))
+
+  ; Like cammy°, but suitable for type-directed term synthesis. All expressions
+  ; are normalized, and logical clauses are ordered to try some expert strategies.
+  ; Cammy <-> Ty × Ty
+  (define (cammy-synth° expr s t)
+    ; s, t, u, v are types
+    ; f, g are Cammy expressions
+    (fresh (f g u v)
+      ; (project (expr s t) (begin (pp `(synth? ,expr : ,s -> ,t)) succeed))
+      (conde
+        ; Try primitives first.
+        ((cammy-prim° expr s t))
+        ; Is it the unique identity arrow?
+        ((== s t) (== expr 'id))
+        ; Is it any arrow into 1?
+        ((== t '1) (=/= s '1) (== expr 'ignore))
+        ; Is it an NT?
+        ((== `(pair ,s ,s) t) (== expr 'dup))
+        ((== s `(pair ,t ,u)) (== expr 'fst))
+        ((== s `(pair ,u ,t)) (== expr 'snd))
+        ((== s `(pair ,u ,v)) (== t `(pair ,v ,u)) (== expr 'swap))
+        ((== s `(pair (hom ,u ,t) ,u)) (== expr 'app))
+        ((== `(sum ,s ,u) t) (== expr 'left))
+        ((== `(sum ,u ,s) t) (== expr 'right))
+        ; Is it a tuple lookup?
+        ((== s `(pair ,u ,v))
+         (conde
+           ((comp-s° 'fst f expr) (cammy-synth° f u t))
+           ((comp-s° 'snd f expr) (cammy-synth° f v t))))
+        ; Is it a case analysis?
+        ((== s `(sum ,u ,v)) (cammy-synth° f u t) (cammy-synth° g v t) (== expr `(case ,f ,g)))
+        ; Is it a tagging or return value?
+        ((== t `(sum ,u ,v))
+         (conde
+           ((comp-s° f 'left expr) (cammy-synth° f s u))
+           ((comp-s° f 'right expr) (cammy-synth° f s v))))
+        ; Is it a graph?
+        ; NB: Want to disallow (pair id id)
+        ((== `(pair ,s ,u) t) (=/= f 'id) (cammy-synth° f s u) (== expr `(pair id ,f)))
+        ((== `(pair ,u ,s) t) (=/= f 'id) (cammy-synth° f s u) (== expr `(pair ,f id)))
+        ; Is it a curry?
+        ((== t `(hom ,u ,v)) (cammy-synth° f `(pair ,s ,u) v) (== expr `(curry ,f)))
+        ; Is it an application?
+        ((cammy-synth° f s `(hom ,u ,t)) (cammy-synth° g s u) (comp-s° `(pair ,f ,g) 'app expr))
+        ; Is it a pair-builder?
+        ((== `(pair ,u ,v) t) (cammy-synth° f s u) (cammy-synth° g s v) (== expr `(pair ,f ,g)))
+        ; Does it result in a list?
+        ((== t `(list ,u))
+         (conde
+           ((== s '1) (== expr 'nil))
+           ((== s `(pair ,u (list ,u))) (== expr 'cons))))
+        ; Is it primitive recursive?
+        ((== s 'N) (cammy-synth° f '1 t) (=/= g 'id) (cammy-synth° g t t) (== expr `(pr ,f ,g)))
+        ; Is it a composition?
+        ; ((comp-s° f g expr) (cammy-synth° f s u) (cammy-synth° g u t))
+        )
+      ; (project (expr s t) (begin (pp `(found: ,expr : ,s -> ,t)) succeed))
+      ))
 )

--- a/movelist/movelist.scm
+++ b/movelist/movelist.scm
@@ -5,13 +5,13 @@
 
 (import (cammyo))
 
-(define (last xs)
-  (if (null? (cdr xs)) (car xs) (last (cdr xs))))
+(define (print-each xs)
+  (if (null? xs) #f
+    (begin (display (car xs)) (newline) (print-each (cdr xs)))))
 
 (define (djinn x s t)
-  (last (run x (q) (normal-form° q) (cammy° q s t))))
+  (print-each (run x (q) (cammy-synth° q s t))))
 
 (match (map (lambda (s) (read (open-input-string s)))
             (command-line-arguments))
-       [(in out (? number? count)) (begin (display (djinn count in out))
-                                          (newline))])
+       [(in out (? number? count)) (djinn count in out)])