提交: 123ca2bde1b4859de8825262f2716d7a6ac3207c - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: 123ca2bde1b4859de8825262f2716d7a6ac3207c (tree)
• 时间: 2021-09-08 10:17:38
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Use new typechecker for compilation.

More cleanup must be done.

更改概述

• modified: compile.sh
• delete: finish.py
• modified: hive/nat/add.cammy
• modified: movelist.scm
• modified: stub.scm

差异

--- a/compile.sh
+++ b/compile.sh
@@ -12,21 +12,17 @@ frame=$(nix-build frame/)
 jelly=$(nix-build jelly/Cargo.nix -A rootCrate.build)
 <"$1" $frame/bin/frame hive/ | $jelly/bin/jelly >"$tmpdir/program.cammy"
 
-# Assemble most of the program.
-cat stub.ml <(echo -n 'let program = ') "$tmpdir/program.cammy" >"$tmpdir/full.ml"
-
-# Ask OCaml about the type of the program.
-ocamlc -annot "$tmpdir/full.ml"
-
 fullname=$(basename -- $1)
 name="${fullname%.*}"
 
+# Typecheck with movelist.
+ty=$(./movelist type-check <"$tmpdir/program.cammy")
+
 # Compute the final piece.
 cat "$tmpdir/program.cammy"
-python3 finish.py "$tmpdir/program.cammy" "$tmpdir/full.annot" >"$tmpdir/$name.scm"
+cat stub.scm <(echo '(cammy-run') "$tmpdir/program.cammy" <(echo "'$ty)") >"$tmpdir/$name.scm"
 # Compile with Chicken.
 csc -O3 -o "$name" "$tmpdir/$name.scm"
 
 # Clean up temporary files.
 rm -r "$tmpdir"
-rm a.out

--- a/finish.py
+++ /dev/null
@@ -1,43 +0,0 @@
-#!/usr/bin/env python3
-
-import sys
-
-aliases = {
-    "nat * nat": "int",
-}
-
-def get_parser(ty):
-    if ty.endswith(" list"):
-        return "(arg-list {})".format(get_parser(ty[:-5]))
-    elif ty in aliases:
-        return get_parser(aliases[ty])
-    else:
-        return "arg-" + ty
-
-with open(sys.argv[-1], "r", encoding="utf-8") as handle:
-    line = handle.readlines()[-2]
-
-tys = [ty.strip() for ty in line.split("->")]
-ret = tys.pop()
-
-with open("stub.scm", "r", encoding="utf-8") as handle:
-    print(handle.read())
-
-with open(sys.argv[-2], "r", encoding="utf-8") as handle:
-    program = handle.read().strip()
-    for comb in ("case", "cons", "map"):
-        program = program.replace(comb, "cammy-" + comb)
-    print("(define program {})".format(program))
-
-print("""
-(import (chicken process-context))
-(define parsers (list {}))
-(define parsed-args
-    (map (lambda (arg p) (p (read-string arg)))
-        (command-line-arguments) parsers))
-(begin
-    (display (fold-left program (lambda (x f) (f x)) parsed-args))
-    (newline))
-""".format(
-    " ".join(get_parser(ty) for ty in tys),
-))

--- a/hive/nat/add.cammy
+++ b/hive/nat/add.cammy
@@ -1 +1 @@
-(pr (curry snd) (curry (comp app succ)))
+(uncurry (pr (curry snd) (curry (comp app succ))))

--- a/movelist.scm
+++ b/movelist.scm
@@ -8,49 +8,54 @@
   ; Clauses are ordered so that expr can become grounded quickly. Since we are
   ; functional in expr, we prefer literal types first, followed by structural
   ; recursion (on s and t!), and finally free composition of polymorphic functors.
+  ; But also, in order to avoid trivializing results, we will put compound
+  ; constructors before trivial constructors.
   (conde
-    ; Literal t.
-    ((== expr 'ignore) (== t 'unit))
     ; Literal s and t.
     ((== expr 't) (== s 'unit) (== t 'truth))
     ((== expr 'f) (== s 'unit) (== t 'truth))
     ((== expr 'not) (== s 'truth) (== t 'truth))
     ((== expr 'conj) (== s (cons 'truth 'truth)) (== t 'truth))
     ((== expr 'disj) (== s (cons 'truth 'truth)) (== t 'truth))
-    ((== expr 'zero) (== s 'unit) (== t 'N))
+    ; Compound before trivial.
     ((== expr 'succ) (== s 'N) (== t 'N))
+    ((== expr 'zero) (== s 'unit) (== t 'N))
     ; Literal s, recursive t.
-    ((== expr 'nil) (== s 'unit) (fresh (l) (== t (list 'list l))))
     ((fresh (f x y) (== expr (list 'name f))
             (== s 'unit) (== 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)))
     ; Parametric polymorphism with structural recursion on both sides.
-    ((== expr 'swap) (fresh (x y) (== s (cons x y)) (== t (cons y x))))
+    ((== expr 'swap) (fresh (x y) (== s (list 'pair x y)) (== t (list 'pair y x))))
     ((== expr 'assl)
-     (fresh (x y z) (== s (cons x (cons y z))) (== t (cons (cons x y) z))))
+     (fresh (x y z) (== s (list 'pair x (list 'pair y z))) (== t (list 'pair (list 'pair x y) z))))
     ((== expr 'assr)
-     (fresh (x y z) (== s (cons (cons x y) z)) (== t (cons x (cons y z)))))
-    ((== expr 'cons) (fresh (l) (== s (cons l t)) (== t (list 'list l))))
+     (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))))
     ((fresh (f y z) (== expr (list 'curry f))
-            (== t (list 'hom y z)) (cammyo f (cons s y) z)))
+            (== t (list 'hom y z)) (cammyo f (list 'pair s y) z)))
     ((fresh (f x y) (== expr (list 'uncurry f))
-            (== s (cons x y)) (cammyo f x (list 'hom y t))))
+            (== 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 (cons l t) t)))
+            (== s (list 'list l)) (cammyo x 'unit 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))
     ; Parametric polymorphism on both sides, but one side recurses.
-    ((== expr 'fst) (fresh (x) (== s (cons t x))))
-    ((== expr 'snd) (fresh (x) (== s (cons x t))))
+    ((== expr 'fst) (fresh (x) (== s (list 'pair t x))))
+    ((== expr 'snd) (fresh (x) (== s (list 'pair x t))))
     ((fresh (f g p1 p2) (== expr (list 'pair f g))
-            (== t (cons p1 p2)) (cammyo f s p1) (cammyo g s p2)))
-    ((== expr 'dup) (== t (cons s s)))
+            (== t (list 'pair p1 p2)) (cammyo f s p1) (cammyo g s p2)))
+    ((== expr 'dup) (== t (list 'pair s s)))
     ((== expr 'left) (fresh (x) (== t (list 'sum s x))))
     ((== expr 'right) (fresh (x) (== t (list 'sum x s))))
     ((fresh (f g s1 s2) (== expr (list 'case f g))
             (== s (list 'sum s1 s2)) (cammyo f s1 t) (cammyo g s2 t)))
-    ((== expr 'app) (fresh (x) (== s (cons (list 'hom x t) x))))
+    ((== expr 'app) (fresh (x) (== s (list 'pair (list 'hom x t) x))))
     ; Parametric polymorphism on both sides.
     ((== expr 'id) (== s t))
     ((fresh (f g y) (== expr (list 'comp f g))

--- a/stub.scm
+++ b/stub.scm
@@ -1,5 +1,6 @@
 (import (srfi 6) (srfi 189))
-(import (chicken condition) (chicken format) (chicken string))
+(import (chicken condition) (chicken format) (chicken process-context) (chicken string))
+(import (matchable))
 
 (define id (lambda (x) x))
 (define (comp f g) (lambda (x) (g (f x))))
@@ -37,11 +38,31 @@
 (define (read-string s) (read (open-input-string s)))
 (define (arg-error arg why)
   (signal (condition (list 'exn 'message (sprintf "Invalid argument ~A: ~A" arg why)))))
-(define (arg-unit x) '())
-(define (arg-bool x) (if (boolean? x) x (arg-error x "not bool")))
-(define (arg-nat x) (if (>= x 0) x (arg-error x "not a natural number")))
-(define (arg-int x)
-  (if (number? x) (if (>= x 0) (cons x 0) (cons 0 (abs x))) (arg-error x "not an integer")))
-(define (arg-list p) (lambda (x) (map p x)))
-
-(define (fold-left kn kc l) (if (null? l) kn (kc (car l) (fold-left kn kc (cdr l)))))
+(define (arg-unit args) (cons '() args))
+(define (arg-bool args)
+  (let ((x (car args)))
+    (if (boolean? x) (cons x (cdr args)) (arg-error x "not bool"))))
+(define (arg-nat args) 
+  (let ((x (car args)))
+    (if (>= x 0) (cons x (cdr args)) (arg-error x "not a natural number"))))
+(define (arg-int args)
+  (let ((x (car args)))
+    (if (number? x) (cons x (cdr args)) (arg-error x "not an integer"))))
+(define (arg-pair p1 p2)
+  (lambda (args1)
+    (let* ((pair1 (p1 args1)) (x (car pair1)) (args2 (cdr pair1))
+           (pair2 (p2 args2)) (y (car pair2)) (args3 (cdr pair2)))
+      (cons (cons x y) args3))))
+
+(define (parse-args parser)
+  (parser (map read-string (command-line-arguments))))
+
+(define ty-parse (match-lambda
+                   ['N arg-nat]
+                   [('pair x y) (arg-pair (ty-parse x) (ty-parse y))]))
+
+(define (cammy-run program ty)
+  (let*
+    ((input (car (parse-args (ty-parse (car ty)))))
+     (rv (program input)))
+    (begin (display rv) (newline))))