提交: c4d2e50723df88e4003105ab3e422a92a637778a - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: c4d2e50723df88e4003105ab3e422a92a637778a (tree)
• 时间: 2021-09-16 13:35:45
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

movelist: Use 1 and 2 for the unit and Boolean types.

更改概述

• modified: movelist/movelist.scm

差异

--- a/movelist/movelist.scm
+++ b/movelist/movelist.scm
@@ -12,25 +12,25 @@
   ; constructors before trivial constructors.
   (conde
     ; Literal s and t.
-    ((== expr 'conj) (== s (list 'pair 'truth 'truth)) (== t 'truth))
-    ((== expr 'disj) (== s (list 'pair 'truth 'truth)) (== t 'truth))
+    ((== expr 'conj) (== s (list 'pair '2 '2)) (== t '2))
+    ((== expr 'disj) (== s (list 'pair '2 '2)) (== t '2))
     ((== expr 'f-add) (== s (list 'pair 'F 'F)) (== t 'F))
     ((== expr 'f-mul) (== s (list 'pair 'F 'F)) (== t 'F))
     ; Compound before trivial.
     ((== expr 'succ) (== s 'N) (== t 'N))
-    ((== expr 'zero) (== s 'unit) (== t 'N))
-    ((== expr 't) (== s 'unit) (== t 'truth))
-    ((== expr 'f) (== s 'unit) (== t 'truth))
-    ((== expr 'not) (== s 'truth) (== t 'truth))
-    ((== expr 'f-zero) (== s 'unit) (== t 'F))
-    ((== expr 'f-one) (== s 'unit) (== t 'F))
+    ((== expr 'zero) (== s '1) (== t 'N))
+    ((== expr 't) (== s '1) (== t '2))
+    ((== expr 'f) (== s '1) (== t '2))
+    ((== expr 'not) (== s '2) (== t '2))
+    ((== expr 'f-zero) (== s '1) (== t 'F))
+    ((== expr 'f-one) (== s '1) (== t 'F))
     ((== expr 'f-negate) (== s 'F) (== t 'F))
-    ((== expr 'f-sqrt) (== s 'F) (== t (list 'sum 'F 'unit)))
+    ((== expr 'f-sqrt) (== s 'F) (== t (list 'sum 'F '1)))
     ; Literal s, recursive t.
     ((fresh (f x y) (== expr (list 'name f))
-            (== s 'unit) (== t (list 'hom x y)) (cammyo f x y)))
+            (== s '1) (== t (list 'hom x y)) (cammyo f x y)))
     ((fresh (x f) (== expr (list 'pr x f))
-            (== s 'N) (cammyo x 'unit t) (cammyo f t t)))
+            (== s 'N) (cammyo x '1 t) (cammyo f t t)))
     ; Parametric polymorphism with structural recursion on both sides.
     ((== expr 'swap) (fresh (x y) (== s (list 'pair x y)) (== t (list 'pair y x))))
     ((== expr 'assl)
@@ -39,18 +39,18 @@
      (fresh (x y z) (== s (list 'pair (list 'pair x y) z)) (== t (list 'pair x (list 'pair y z)))))
     ; Compound before trivial.
     ((== expr 'cons) (fresh (l) (== s (list 'pair l t)) (== t (list 'list l))))
-    ((== expr 'nil) (== s 'unit) (fresh (l) (== t (list 'list l))))
+    ((== expr 'nil) (== s '1) (fresh (l) (== t (list 'list l))))
     ((fresh (f y z) (== expr (list 'curry f))
             (== t (list 'hom y z)) (cammyo f (list 'pair s y) z)))
     ((fresh (f x y) (== expr (list 'uncurry f))
             (== s (list 'pair x y)) (cammyo f x (list 'hom y t))))
     ((fresh (x f l) (== expr (list 'fold x f))
-            (== s (list 'list l)) (cammyo x 'unit t) (cammyo f (list 'pair l t) t)))
+            (== s (list 'list l)) (cammyo x '1 t) (cammyo f (list 'pair l t) t)))
     ((fresh (f x y) (== expr (list 'map f))
             (== s (list 'list x)) (== t (list 'list y)) (cammyo f x y)))
     ; Literal t. But this is too easy of an answer, so we don't want it at the
     ; top of the list.
-    ((== expr 'ignore) (== t 'unit))
+    ((== expr 'ignore) (== t '1))
     ; Parametric polymorphism on both sides, but one side recurses.
     ((== expr 'fst) (fresh (x) (== s (list 'pair t x))))
     ((== expr 'snd) (fresh (x) (== s (list 'pair x t))))