Commit: 0f8f6b6e68ec2579b9b1a4381812864e9ab6e713 - cammy (git)

A categorical programming language

Commit MetaInfo

• Revision: 0f8f6b6e68ec2579b9b1a4381812864e9ab6e713 (tree)
• Time: 2023-01-25 02:01:07
• Author: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Evaluate images and preimages directly.

I've gotta figure out how to extract the results decently, but this is
amazing in general. The one thing I don't like is that 1 is in the image
of (comp succ succ), which suggests that succ° is broken somehow.

Change Summary

• modified: movelist/cammy-repl.scm
• modified: movelist/cammyo.scm

Incremental Difference

--- a/movelist/cammy-repl.scm
+++ b/movelist/cammy-repl.scm
@@ -59,13 +59,22 @@
 (define (cammy-image expr)
   (time
     (display
-      (map
+      ; (map
         ; need the type to display the value properly
-        (lambda (q) (elt->str (car q) (cdr q)))
+        ; (lambda (q) (elt->str (car q) (cdr q)))
         (run 10 (q) (fresh (s t i o)
                            ; package them up here
                            (conso t o q)
-                           (cammy° expr s t) (eval° expr i o)))))
+                           (cammy° expr s t) (eval° expr i o))))
+    (newline)))
+
+(define (cammy-preimage expr)
+  (time
+    (display
+      (run 10 (q) (fresh (s t i o)
+                         ; package them up here
+                         (conso s i q)
+                         (cammy° expr s t) (eval° expr i o))))
     (newline)))
 
 (define (repl!)
@@ -76,6 +85,7 @@
       ; command?
       ['? (display "help goes here?") (newline) (repl!)]
       ['image (cammy-image (read)) (repl!)]
+      ['preimage (cammy-preimage (read)) (repl!)]
       ; read
       [expr
         (if (eof-object? expr)

--- a/movelist/cammyo.scm
+++ b/movelist/cammyo.scm
@@ -170,11 +170,18 @@
     (conde
       ((== expr 'id) (== i o))
       ((fresh (f g u) (== expr `(comp ,f ,g)) (eval° f i u) (eval° g u o)))
+      ((== expr 'ignore) (== o 'star))
       ((== expr 'fst) (caro i o))
       ((== expr 'snd) (cdro i o))
       ((== expr 'dup) (conso i i o))
+      ((== expr 't) (== i 'star) (== o #t))
+      ((== expr 'f) (== i 'star) (== o #f))
       ((== expr 'not) (not° i o))
       ((== expr 'zero) (== i 'star) (zeroo o))
       ((== expr 'succ) (succ° i o))
+      ((fresh (f g n) (== expr `(pr ,f ,g))
+              (conde
+                ((zeroo i) (eval° f 'star o))
+                ((succ° n i) (eval° `(comp ,expr ,g) n o)))))
       ))
 )