提交: b8a799e5bd63d1760337d688ab95dc417edfc0b0 - cammy (git)

A categorical programming language

Commit MetaInfo

• 修订版: b8a799e5bd63d1760337d688ab95dc417edfc0b0 (tree)
• 时间: 2023-01-04 15:36:05
• 作者: Corbin <cds@corb...>
• Commiter: Corbin

Log Message

Try a new approach to compiling to WASM.

This is based on a graph-and-ports architecture, as used in Elliott's
"Compiling to Categories" and almost certainly elsewhere.

更改概述

• modified: movelist/cammy-wasm.scm

差异

--- a/movelist/cammy-wasm.scm
+++ b/movelist/cammy-wasm.scm
@@ -4,6 +4,53 @@
 
 (import (cammyo))
 
+; A port is one of:
+; - a typed WASM local
+; - nothing: '()
+; - a pair of ports: '(pair p1 p2)
+; See Chapter 7 of
+; http://conal.net/papers/compiling-to-categories/compiling-to-categories.pdf
+
+; A port context is a pair (p, ls) containing a port and a list of WASM locals.
+
+; Port <-> WAT Ty × WAT Insts × WAT Insts
+(define (port-alloc° p ty before after)
+  (fresh (len) (lengtho before len) (conso len ty p) (conso ty before after)))
+
+; Ignore inputs and generate outputs of the given type.
+; WAT Ty <-> Context × Context
+(define (context-elt° t input output)
+  (fresh (po ins outs)
+         (cdro input ins)
+         (conso po outs output)
+         (port-alloc° po t ins outs)))
+
+; Consume inputs and generate outputs of the given type.
+; WAT Ty × WAT Ty <-> Context × Context
+(define (context-prim° s t input output)
+  (fresh (pi po ins outs)
+         (conso pi ins input) (cdro pi s)
+         (conso po outs output)
+         (port-alloc° po t ins outs)))
+
+; Relate expressions to operations and input+output port contexts.
+; Cammy <-> WAT Insts × Port × Port
+(define (ops-ports° expr insts input output)
+  (conde
+    ((== expr 'id) (nullo insts) (== input output))
+    ((== expr 'ignore) (nullo insts) (fresh (ps) (cdro input ps) (conso '() ps output)))
+    ((== expr 'fst) (nullo insts)
+                    (fresh (ps s t _p) (conso s ps input) (conso t ps output)
+                           (== s `(pair ,t ,_p))))
+    ((== expr 'zero) (== insts '((i32.const 0)))
+                     (context-elt° 'i32 input output))
+    ((== expr 'succ) (== insts '((i32.const 1) (i32.add)))
+                     (context-prim° 'i32 'i32 input output))
+    ((fresh (f g finsts ginsts ctx)
+            (== expr `(comp ,f ,g)) (appendo finsts ginsts insts)
+            (ops-ports° f finsts input ctx) (ops-ports° g ginsts ctx output)))
+    ))
+
 ; Create a fresh symbol ala (gensym s) and bind it to a logic variable.
 ; Meant for creating fresh locals for WASM.
 ; string -> WAT Symbol
@@ -22,7 +69,7 @@
 ; Cammy <-> WAT Insts
 (define (stack-ops° expr ops)
   (conde
-    ((== expr 'id) (== ops '()))
+    ((== expr 'id) (nullo ops))
     ((fresh (f g x y) (== expr `(comp ,f ,g)) (stack-ops° f x) (stack-ops° g y) (appendo x y ops)))
     ; 1
     ((== expr 'ignore) (== ops '((drop))))
@@ -110,6 +157,7 @@
          (appendo decls body func)
          ))
 
+; The relational boundary for compiling a single function.
 (define (wasm-func expr name)
   (car (run 1 (func) (wasm-func° expr name func))))
 
@@ -128,9 +176,19 @@
              (global.set $bump)))
     funcs))
 
-(let*
-  ((expr (read))
-   (func (wasm-func expr '$main)))
-  (begin
-    (pp (wasm-module (list func)))
-    (newline)))
+; (let*
+;   ((expr (read))
+;    (func (wasm-func expr '$main)))
+;   (begin
+;     (pp (wasm-module (list func)))
+;     (newline)))
+
+(define results
+  (run 1 (q)
+       (fresh (insts input output inp outp)
+              (ops-ports° (read) insts input output)
+              (caro input inp) (caro output outp)
+              (== q `(wip (insts ,insts) (input ,inp) (output ,outp))))))
+
+(pp (car results))
+(newline)