提交: 6165ec9b2c325d1662942ff286c5402ca7dd473a - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 6165ec9b2c325d1662942ff286c5402ca7dd473a (tree)
• 时间: 2021-09-17 02:56:17
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Add Choice for Booleans.

This does not restrain the target category much; we are only saying that

2 = 1 + 1

Which is relatively standard for sums.

更改概述

• modified: frame/frame.ml
• add: hive/list/evens.cammy
• add: hive/nat/iter.cammy
• modified: movelist/movelist.scm
• modified: stub.scm

差异

--- a/frame/frame.ml
+++ b/frame/frame.ml
@@ -4,7 +4,7 @@ module CodeCache = Map.Make (String)
 
 let primitives =
   "id comp ignore fst snd pair left right case assl assr swap dup curry \
-   uncurry app name zero succ pr nil cons map fold t f not conj disj \
+   uncurry app name zero succ pr nil cons map fold t f not conj disj pick \
    f-zero f-one f-negate f-add f-mul f-sqrt"
 
 let filter =

--- /dev/null
+++ b/hive/list/evens.cammy
@@ -0,0 +1,2 @@
+(comp list/range
+  (fold nil (comp (pair (comp fst nat/is_even) (pair cons snd)) pick)))

--- /dev/null
+++ b/hive/nat/iter.cammy
@@ -0,0 +1 @@
+(pr (name id) (curry app))

--- a/movelist/movelist.scm
+++ b/movelist/movelist.scm
@@ -14,8 +14,10 @@
     ; Literal s and t.
     ((== expr 'conj) (== s (list 'pair '2 '2)) (== t '2))
     ((== expr 'disj) (== s (list 'pair '2 '2)) (== t '2))
+    ((== expr 'f-lt) (== s (list 'pair 'F 'F)) (== t '2))
     ((== expr 'f-add) (== s (list 'pair 'F 'F)) (== t 'F))
     ((== expr 'f-mul) (== s (list 'pair 'F 'F)) (== t 'F))
+    ((== expr 'f-sqrt) (== s 'F) (== t (list 'sum 'F '1)))
     ; Compound before trivial.
     ((== expr 'succ) (== s 'N) (== t 'N))
     ((== expr 'zero) (== s '1) (== t 'N))
@@ -25,12 +27,12 @@
     ((== 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 '1)))
     ; Literal s, recursive t.
     ((fresh (f x y) (== expr (list 'name f))
             (== s '1) (== t (list 'hom x y)) (cammyo f x y)))
     ((fresh (x f) (== expr (list 'pr x f))
             (== s 'N) (cammyo x '1 t) (cammyo f t t)))
+    ((== expr 'pick) (== s (list 'pair '2 (list 'pair 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)

--- a/stub.scm
+++ b/stub.scm
@@ -25,6 +25,9 @@
 (define f (lambda (x) #f))
 (define conj (lambda (xy) (and (car xy) (cdr xy))))
 (define disj (lambda (xy) (or (car xy) (cdr xy))))
+(define pick (lambda (bxy)
+               (let ((xy (cdr bxy)))
+                 (if (car bxy) (car xy) (cdr xy)))))
 
 (define zero (lambda (x) 0))
 (define succ (lambda (x) (+ x 1)))
@@ -39,6 +42,7 @@
 (define f-zero (flonum 0.0))
 (define f-one (flonum 1.0))
 (define (f-negate x) (fl- x))
+(define (f-lt xy) (fl<? (car xy) (cdr xy)))
 (define (f-add xy) (fl+ (car xy) (cdr xy)))
 (define (f-mul xy) (fl* (car xy) (cdr xy)))
 (define (f-sqrt x) (if (eqv? 0 (flsign-bit x)) (left (flsqrt x)) (right '())))