From 34b411cca617548f45da472a61e5fadeafef6bdd Mon Sep 17 00:00:00 2001 From: Hanting Zhang Date: Tue, 29 Oct 2024 16:54:58 -0700 Subject: [PATCH] wip --- loam.asd | 1 + loam/datalog.lisp | 19 ++ loam/evaluation.lisp | 431 +++++++++++++++++++++++++++++++++++++++++++ loam/package.lisp | 15 ++ 4 files changed, 466 insertions(+) create mode 100644 loam/evaluation.lisp diff --git a/loam.asd b/loam.asd index e3fddfc..8a0e158 100644 --- a/loam.asd +++ b/loam.asd @@ -18,6 +18,7 @@ (:file "lattice") (:file "datalog") (:file "allocation") + (:file "evaluation") (:file "data") ))) diff --git a/loam/datalog.lisp b/loam/datalog.lisp index bc28c51..99474fd 100644 --- a/loam/datalog.lisp +++ b/loam/datalog.lisp @@ -729,6 +729,7 @@ and a list of free variables in FORM." (let :rule-binding) (when :restriction) (case :case) + (cond :cond) (if :if) (t :predicate))) @@ -743,6 +744,19 @@ and a list of free variables in FORM." (nconc (aux if-branch `(when ,condition)) (aux else-branch `(when (not ,condition))))))) + ;; Synthesizes a segment that starts with a case statement. + ;; Errors if the first segment is not a case segment. + (defun synthesize-cond-segment (case-segment curr-rhs end-handle) + (destructuring-bind (head &rest branches) + case-segment + (assert (eql head 'cond)) + (loop for (test branch-segments) in branches + for test-segment = `(when ,test) + for curr-rhs-tail = (append curr-rhs (list test-segment)) + append (synthesize-segments branch-segments (copy-list curr-rhs-tail) end-handle) + into output-rules + finally (return output-rules)))) + ;; Synthesizes a segment that starts with a case statement. ;; Errors if the first segment is not a case segment. (defun synthesize-case-segment (case-segment curr-rhs end-handle) @@ -776,6 +790,11 @@ and a list of free variables in FORM." do (assert (eql rest nil)) and append (synthesize-case-segment segment (copy-list curr-rhs-tail) end-handle) into output-rules and do (return output-rules) + when (eql kind :cond) + ;; Ditto the above for if statements. + do (assert (eql rest nil)) + and append (synthesize-cond-segment segment (copy-list curr-rhs-tail) end-handle) into output-rules + and do (return output-rules) when (eql kind :if) ;; Ditto the above for if statements. do (assert (eql rest nil)) diff --git a/loam/evaluation.lisp b/loam/evaluation.lisp new file mode 100644 index 0000000..3fb2968 --- /dev/null +++ b/loam/evaluation.lisp @@ -0,0 +1,431 @@ +(declaim (optimize safety)) + +(in-package #:evaluation) +(def-suite* evaluation-suite :in loam:master-suite) + +(defconstant +wide-size+ 8) +(defconstant +element-bytes+ 4) +(defconstant +element-bits+ (* 8 +element-bytes+)) + +(defprogram ptr-program (lurk-allocation) + (relation (tag element wide)) ; (short-tag wide-tag) + + ;; It may be confusing that this relation has the same name as the ptr struct's value accessor, since the struct's field is not wide. + (relation (ptr-value ptr wide)) ; (ptr value) + + (relation (alloc element wide)) ; (tag value) + + (relation (toplevel-input wide-ptr wide-ptr)) ; (wide-ptr) + (relation (output-expr wide-ptr)) ; (wide-ptr) + (relation (input-ptr ptr)) ; (ptr) + (relation (output-ptr ptr)) ; (ptr) + + (relation (ingress ptr)) ; (ptr) + (relation (egress ptr)) ; (ptr) + + ;; Ingress path + (rule (alloc expr-tag (wide-ptr-value expr)) (alloc env-tag (wide-ptr-value env)) <-- + (toplevel-input expr env) + (tag expr-tag (wide-ptr-tag expr)) + (tag env-tag (wide-ptr-tag env))) + + (rule (ingress ptr) (input-ptr ptr) <-- + (toplevel-input expr env) + (ptr-value expr-ptr (wide-ptr-value expr)) + (ptr-value env-ptr (wide-ptr-value env)) + (tag (ptr-tag expr-ptr) (wide-ptr-tag expr)) + (tag (ptr-tag env-ptr (wide-ptr-tag env)))) + + ;; Egress + (rule (egress ptr) <-- (output-ptr ptr)) + + ;; Construct output-expr from output-ptr + (rule (output-expr (make-wide-ptr wide-tag value)) <-- + (output-ptr ptr) + (ptr-value ptr value) + (tag (ptr-tag ptr) wide-tag))) + +;; hash-cache takes precedence over program in superclass list +(defprogram hash4 (hash-cache) + (include ptr-program) + (relation (hash4 wide wide wide wide)) ; (a b c d) + (relation (unhash4 wide)) ; (digest) + (relation (hash4-rel wide wide wide wide wide)) ; (a b c d digest) + + ;; signal + (rule (hash4-rel a b c d digest) <-- + (unhash4 digest) + (let ((preimage (unhash4 digest)) + (a (nth 0 preimage)) + (b (nth 1 preimage)) + (c (nth 2 preimage)) + (d (nth 3 preimage))))) + + ;; signal + (rule (hash4-rel a b c d (hash a b c d)) <-- (hash4 a b c d)) + + ;; signal + (rule (alloc a-tag a-value) (alloc b-tag b-value) <-- + (unhash4 digest) + (hash4-rel wide-a-tag a-value wide-b-tag b-value digest) + (tag a-tag wide-a-tag) + (tag b-tag wide-b-tag))) + +(defprogram cons-mem () + (include ptr-program) + (include hash4) + + ;; The following relations could be determined by something like: + ;; (constructor cons (:cons 0 hash4) (car ptr) (cdr ptr)) + ; signal + (relation (cons ptr ptr)) ; (car cdr) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;;; Memory + + ;; The canonical cons Ptr relation. + (relation (cons-rel ptr ptr ptr)) ; (car cdr cons) + + ;; Memory to support conses allocated by digest or contents. + (lattice (cons-digest-mem wide dual-element)) ; (digest addr) + (lattice (cons-mem ptr ptr dual-element)) ; (car cdr addr) + + ;; Populating alloc(...) triggers allocation in cons-digest-mem. + (rule (cons-digest-mem value (alloc :cons (dual 0))) <-- + (alloc (tag-address :cons) value)) + + ;; Populating cons(...) triggers allocation in cons-mem. + (rule (cons-mem car cdr (alloc :cons (dual 0))) <-- (cons car cdr)) + + ;; Populate cons-digest-mem if a cons in cons-mem has been hashed in hash4-rel. + (rule (cons-digest-mem digest addr) <-- + (cons-mem car cdr addr) + (ptr-value car car-value) (ptr-value cdr cdr-value) + (tag (ptr-tag car) car-tag) (tag (ptr-tag cdr) cdr-tag) + (hash4-rel car-tag car-value cdr-tag cdr-value digest)) + + ;; Other way around. + (rule (cons-mem car cdr addr) <-- + (cons-digest-mem digest addr) + (hash4-rel car-tag car-value cdr-tag cdr-value digest) + (ptr-value car car-value) (ptr-value cdr cdr-value) + (tag (ptr-tag car) car-tag) (tag (ptr-tag cdr) cdr-tag)) + + ;; Register a cons value. + (rule (ptr-value cons value) <-- + (cons-digest-mem value addr) (let ((cons (ptr :cons (dual-value addr)))))) + + ;; Register a cons relation. + (rule (cons-rel car cdr cons) <-- + (cons-mem car cdr addr) + (let ((cons (ptr :cons (dual-value addr)))))) + + ;; signal + (rule (unhash4 digest) <-- + (ingress ptr) (when (has-tag-p ptr :cons)) (ptr-value ptr digest)) + + ;; signal + (rule (hash4 car-tag car-value cdr-tag cdr-value) <-- + (egress cons) + (cons-rel car cdr cons) + (tag (ptr-tag car) car-tag) (tag (ptr-tag cdr) cdr-tag) + (ptr-value car car-value) (ptr-value cdr cdr-value)) + + ;; signal + (rule (egress car) (egress cdr) <-- + (egress cons) (cons-rel car cdr cons))) + +(defprogram immediate-num () + (include ptr-program) + ;; real + (rule (ptr-value ptr value) <-- + (alloc tag value) + (when (is-tag-p tag :num)) + (let ((ptr (ptr :num (wide-nth 0 value)))))) + + (rule (ptr-value ptr value) <-- + (egress ptr) (when (has-tag-p ptr :num)) + (let ((value (widen (ptr-value ptr))))))) + +;; The Lurk evaluation. +(defprogram eval () + (include ptr-program) + (include cons-mem) + (include immediate-num) + + (relation (map-double ptr ptr)) ; (input-ptr output-ptr) + (relation (map-double-input ptr)) + + ;; Generate the necessary signal relations + + ;; Input and output and eval. + (signal-relation (input-output (expr env evaled) (input-ptr expr env) (output-ptr evaled))) + (signal-relation (signal-eval (expr env evaled) (eval-input expr env) (eval expr env evaled))) + + (relation (lookup-input ptr ptr)) + (relation (lookup ptr ptr ptr)) + (signal-relation (signal-lookup (var env value) (lookup-input var env) (lookup var env value))) + + (relation (eval-bindings-input ptr ptr boolean)) + (relation (eval-bindings ptr ptr boolean ptr)) + (signal-relation (signal-eval-bindings (bindings env is-rec extended-env) + (eval-bindings-input bindings env is-rec) + (eval-bindings bindings env is-rec extended-env))) + + (relation (fold-left-input ptr element ptr)) + (relation (fold-left ptr element ptr element)) + (signal-relation (signal-fold-left (op initial args result) + (fold-left-input op initial args) + (fold-left op initial args result))) + + (relation (funcall-input ptr ptr ptr ptr ptr)) + (relation (funcall ptr ptr ptr ptr ptr ptr)) + (signal-relation (signal-funcall (args body closed-env values outer-env result) + (funcall-input args body closed-env values outer-env) + (funcall args body closed-env values outer-env result))) + + ;; Cons signals. + (signal-relation (ingress-cons (car cdr cons) (ingress cons) (cons-rel car cdr cons))) + (signal-relation (signal-cons (car cdr cons) (cons car cdr) (cons-rel car cdr cons))) + + ;; Thunk signals. + (signal-relation (ingress-thunk (car cdr cons) (ingress cons) (cons-rel car cdr cons))) + (signal-relation (signal-thunk (car cdr cons) (cons car cdr) (cons-rel car cdr cons))) + + ;; Fun signals. + (signal-relation (ingress-fun (car cdr cons) (ingress cons) (cons-rel car cdr cons))) + (signal-relation (signal-fun (car cdr cons) (cons car cdr) (cons-rel car cdr cons))) + + ;; Connect eval to input/output. + (synthesize-rule (input-output expr env evaled) <-- (signal-eval expr env evaled)) + + (synthesize-rule (signal-eval expr env evaled) <-- + (cond + ((has-tag-p expr :num) ()) ; This syntax is really weird, but it means that this branch is self-evaluating. + ((has-tag-p expr :err) ()) ; Ditto. + ((has-tag-p expr :sym) ((signal-lookup expr env evaled))) ; TODO. + + ;; Interesting cons case: + ((has-tag-p expr :cons) + ((ingress-cons head rest expr) + (cond + ;; Evaluate cons operator. + ((== head (builtin-sym 'cons)) ((ingress-cons car tail rest) + (ingress-cons cdr end tail) + (when (is-nil end)) + (signal-eval car env evaled-car) + (signal-eval cdr env evaled-cdr) + (signal-cons car cdr evaled))) + ;; Evaluate if. + ((== head (builtin-sym 'if)) ((ingress-cons cond branches rest) + (signal-eval cond env evaled-cond) + (ingress-cons a more branches) + (if (not-nil evaled-cond) + ((signal-eval a env evaled)) + ((ingress-cons b end more) + (when (is-nil end)) + (signal-eval b env evaled))))) + ;; Evaluate letrec, it's more interesting. FIXME: Add let. + ((== head (builtin-sym 'letrec)) ((ingress-cons bindings tail rest) + (ingress-cons body end tail) + (when (is-nil end)) + (signal-eval-bindings bindings env t extended-env) + (signal-eval body extended-env evaled))) + ;; Evaluate lambda. + ((== head (builtin-sym 'lambda)) ((ingress-cons args tail rest) + (ingress body end tail) + (when (is-nil end)) + (signal-fun args body env evaled))) + ;; Evaluate +. FIXME: Generalize to more ops. + ((== head (builtin-sym '+)) ((signal-fold-left head 0 rest acc) + (let ((evaled (ptr :num acc)))))) + ;; Evaluate =. FIXME: Generalize to more ops and bool-fold. + ((== head (builtin-sym '=)) ((ingress-cons arg1 tail rest) + (ingress-cons arg2 end tail) + (when (and (is-nil end) (has-tag-p arg1 :num) (has-tag-p arg2 :num))) + (if (== arg1 arg2) + (let ((evaled ptr-t))) + (let ((evaled ptr-nil))))) + ;; Evaluate function. + ((has-tag-p head :fun) ((ingress-fun args body closed-env head) + (signal-funcall args body closed-env rest evaled))) + ((and (not (has-tag-p head :fun)) (not (is-builtin head))) ((signal-eval head env fun) + (ingress-fun args body closed-env fun) + (signal-funcall args body closed-env rest evaled))) + + ))))) + + ;; I have no idea if this works... but it's nice that we have enough expressiveness to write something like this. + ;; FIXME: Error case when no lookup is found. + (synthesize-rule (signal-lookup var env value) <-- + (ingress-cons binding more-env env) + (ingress-cons bound-var bound-value binding) + (if (== var bound-var) + ((if (has-tag-p bound-value :thunk) + ;; If the looked-up value is a thunk. + ((ingress-thunk body closed-env bound-value) + (signal-cons binding closed-env extended-env) + (signal-eval body extended-env value)) + ((let ((value bound-value)))))) ;; Is this efficient? No... but it works. + ((signal-lookup var more-env value)))) + + ;; Still no idea. + (synthesize-rule (signal-eval-bindings bindings extended-env is-rec final-env) <-- + (ingress-cons binding more-bindings bindings) + (ingress-cons var binding-tail binding) + (ingress-cons unevaled end binding-tail) + (when (is-nil end)) + (if is-rec + ;; Recursive case: make a thunk. + ((signal-thunk unevaled extended-env thunk) + (signal-cons var thunk env-binding) + (if (is-nil more-bindings) + ;; If we have no more bindings, then just return the final-env. + ((signal-cons env-binding extended-env final-env)) + ;; Otherwise, we have to recurse to the next binding. + ((signal-cons env-binding extended-env new-env) + (signal-eval-bindings more-bindings new-env is-rec final-env)))) + ;; Non-recursive case: just evaluate. + ((signal-eval unevaled extended-env evaled) + (signal-cons var evaled env-binding) + ;; FIXME: There's unfortunate duplication here, change synthesis so that `if/case/cond` + ;; don't have to be the final segment. Kind of a headache. + (if (is-nil more-bindings) + ((signal-cons env-binding extended-env final-env)) + ((signal-cons env-binding extended-env new-env) + (signal-eval-bindings more-bindings new-env is-rec final-env)))))) + + (synthesize-rule (signal-fold-left op initial args result) <-- + (if (is-nil args) + ((let ((result initial)))) + ((ingress-cons arg more-args args) + (when (has-tag-p arg :num)) + (signal-fold-left op initial more-args acc) + (let ((result (case op + ((builtin-ptr '+) (+ (ptr-value arg) acc))))))))) + + (synthesize-rule (signal-funcall args body closed-env values outer-env result) <-- + (if (and (is-nil args) (is-nil values)) + ((signal-eval body closed-env result)) + ((ingress-cons arg more-args args) + (ingress-cons unevaled more-values values) + (signal-eval unevaled outer-env evaled) + (signal-cons arg evaled binding) + (signal-cons binding closed-env new-closed-env) + (signal-funcall more-args body new-closed-env more-values outer-env result)))) + ) + + #| + (synthesize-rule (signal-map-double ptr doubled) <-- + (when (has-tag-p ptr :num)) + (let ((doubled (ptr :num (* 2 (ptr-value ptr))))))) + + (synthesize-rule (signal-map-double ptr double-cons) <-- + (ingress-cons car cdr ptr) + (signal-map-double car double-car) + (signal-map-double cdr double-cdr) + (signal-cons double-car double-cdr double-cons))) + |# + +(defun make-cons (a-tag-spec a-wide b-tag-spec b-wide) + (hash4 (tag-value a-tag-spec) a-wide (tag-value b-tag-spec) b-wide)) + +(defmethod less ((a ptr) (b ptr)) + (less (cons (ptr-tag a) (ptr-value a)) + (cons (ptr-tag b) (ptr-value b)))) + +(defmethod cons-mem-contiguous-p ((program program)) + (let* ((cons-mem (find-relation program 'cons-mem)) + (tuples (sort (relation-tuple-list cons-mem) #'less :key #'third)) + (addrs (mapcar (compose #'dual-value #'third) tuples))) + (loop for (addr next-addr) on addrs + always (= next-addr (1+ addr))))) + +(test allocation + (let* ((program (make-program-instance 'map-double)) + (*program* program) ;; This is needed for MAKE-CONS. + (c1-2 (make-cons :num (widen 1) :num (widen 2))) ; (1 . 2) + (c2-3 (make-cons :num (widen 2) :num (widen 3))) ; (2 . 3) + (c2-4 (make-cons :num (widen 2) :num (widen 4))) ; (2 . 4) + (c4-6 (make-cons :num (widen 4) :num (widen 6))) ; (4 . 6) + (c1-2_2-3 (make-cons :cons c1-2 :cons c2-3)) + (c2-4_4-6 (make-cons :cons c2-4 :cons c4-6)) + (expected-output (wide-ptr :cons c2-4_4-6))) + (init program `(input-expr ((,(wide-ptr :cons c1-2_2-3))))) + + (run program) + + ;(datalog::print-relation-counts program t) + + (is (== `((,expected-output )) (relation-tuple-list (find-relation program 'output-expr)))) + (is (not (cons-mem-contiguous-p program))))) + +(test syn-allocation + (let* ((program (make-program-instance 'syn-map-double)) + (*program* program) ;; This is needed for MAKE-CONS. + (c1-2 (make-cons :num (widen 1) :num (widen 2))) ; (1 . 2) + (c2-3 (make-cons :num (widen 2) :num (widen 3))) ; (2 . 3) + (c2-4 (make-cons :num (widen 2) :num (widen 4))) ; (2 . 4) + (c4-6 (make-cons :num (widen 4) :num (widen 6))) ; (4 . 6) + (c1-2_2-3 (make-cons :cons c1-2 :cons c2-3)) + (c2-4_4-6 (make-cons :cons c2-4 :cons c4-6)) + (expected-output (wide-ptr :cons c2-4_4-6))) + (init program `(input-expr ((,(wide-ptr :cons c1-2_2-3))))) + (run program) + + ;(datalog::print-relation-counts program t) + + (is (== `((,expected-output )) (relation-tuple-list (find-relation program 'output-expr)))) + (is (not (cons-mem-contiguous-p program))))) + +(test syn-allocation-spec + (defprogram syn-map-double-spec () + (include ptr-program) + (include cons-mem) + (include immediate-num) + + (relation (map-double ptr ptr)) + (relation (map-double-input ptr)) + + (rule (map-double-input input) <-- + (input-ptr input)) + + (rule (output-ptr output) <-- + (input-ptr input) + (map-double input output)) + + (rule (map-double ptr doubled) <-- + (map-double-input ptr) + (when (has-tag-p ptr :num)) + (let ((doubled (ptr :num (* 2 (ptr-value ptr))))))) + + (rule (ingress ptr) <-- + (map-double-input ptr) + (when (not (has-tag-p ptr :num)))) + + (rule (map-double-input car) <-- + (map-double-input ptr) + (when (not (has-tag-p ptr :num))) + (cons-rel car cdr ptr)) + + (rule (map-double-input cdr) <-- + (map-double-input ptr) + (when (not (has-tag-p ptr :num))) + (cons-rel car cdr ptr) + (map-double car double-car)) + + (rule (cons double-car double-cdr) <-- + (map-double-input ptr) + (when (not (has-tag-p ptr :num))) + (cons-rel car cdr ptr) + (map-double car double-car) + (map-double cdr double-cdr)) + + (rule (map-double ptr doubled) <-- + (map-double-input ptr) + (when (not (has-tag-p ptr :num))) + (cons-rel car cdr ptr) + (map-double car double-car) + (map-double cdr double-cdr) + (cons-rel double-car double-cdr doubled))) + (is (compare-spec 'syn-map-double 'syn-map-double-spec))) diff --git a/loam/package.lisp b/loam/package.lisp index efebe38..ae77cfa 100644 --- a/loam/package.lisp +++ b/loam/package.lisp @@ -33,6 +33,21 @@ #:widen #:wide #:wide-elements #:wide-nth #:element #:tag #:tag-name #:tag-value #:nth-tag #:lurk-allocation #:allocation-tag-names #:hash-cache #:hash #:unhash #:+element-bits+ )) +(defpackage evaluation + (:use #:common-lisp) + (:import-from #:base #:todo #:compose) + (:import-from #:macros #:display #:awhen #:it) + (:import-from #:it.bese.FiveAm #:def-suite #:def-suite* #:in-suite #:test #:is #:run! #:signals #:finishes #:skip) + (:import-from #:defstar #:defun* #:defmethod* #:defgeneric* #:->) + (:import-from #:lattice #:dual #:dual-value #:defdual #:with-duals) + (:import-from #:datalog #:*program* #:*trace* #:*step* #:trace-log #:relation #:lattice #:signal-relation #:synthesize-rule #:dual #:rule #:rules #:make-program-instance + #:include #:includes #:included-programs #:<-- #:_ #:== #:run #:init #:program #:defprogram #:initialize-program + #:find-relation #:find-prototype #:relation-counts #:print-relation-counts #:relation-tuples + #:relation-tuple-list #:less #:spec #:compare-spec) + (:export #:*program* #:element #:ptr #:make-ptr #:wide-ptr #:make-wide-ptr #:wide-ptr-tag #:wide-ptr-value #:make-wide + #:widen #:wide #:wide-elements #:wide-nth #:element #:tag #:tag-name #:tag-value #:nth-tag #:lurk-allocation + #:allocation-tag-names #:hash-cache #:hash #:unhash #:+element-bits+ )) + (defpackage lurk.builtin (:export #:atom #:begin #:car #:cdr #:char #:commit #:comm #:bignum #:cons #:current-env #:emit #:empty-env #:eval #:eq #:type-eq #:type-eqq #:hide #:if #:lambda #:let #:letrec #:nil #:u64 #:open #:quote #:secret #:strcons