From d7b1cbe3ca275baa924e387bbecdb2f5aeebc058 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/allocation.lisp | 4 +- loam/data.lisp | 210 +++++--- loam/datalog.lisp | 77 +-- loam/evaluation.lisp | 1135 ++++++++++++++++++++++++++++++++++++++++++ loam/package.lisp | 48 +- 6 files changed, 1370 insertions(+), 105 deletions(-) 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/allocation.lisp b/loam/allocation.lisp index 2e89b01..e25657b 100644 --- a/loam/allocation.lisp +++ b/loam/allocation.lisp @@ -112,7 +112,7 @@ (defclass lurk-allocation (allocation) () - (:default-initargs :tag-names #(:nil :cons :sym :fun :num :str :char :comm :u64 :key :env :err :thunk :builtin :bignum))) + (:default-initargs :tag-names #(:u64 :num :bignum :comm :char :str :key :fun :builtin :coroutine :sym :cons :env :thunk :err))) (defmethod initialize-program :after ((a lurk-allocation) &key &allow-other-keys) (setf (allocation-tag-names a) (coerce (allocation-tag-names a) 'vector)) @@ -199,7 +199,7 @@ (:method ((allocation allocation) ((tag element) t) ((initial-address dual) t)) (let* ((allocation-map (allocation-allocation-map allocation)) (last-address (gethash tag allocation-map)) - (allocated (if last-address (dual (1+ (dual-value last-address))) (dual 0)))) + (allocated (if last-address (dual (1+ (dual-value last-address))) initial-address))) (setf (gethash tag allocation-map) allocated))) (:method ((allocation allocation) ((tag-spec keyword) symbol) ((initial-address dual) t)) (allocate allocation (tag-address tag-spec) initial-address)) diff --git a/loam/data.lisp b/loam/data.lisp index c8b3162..d2079f9 100644 --- a/loam/data.lisp +++ b/loam/data.lisp @@ -7,12 +7,102 @@ (def-suite* data-suite :in loam:master-suite) ;; '(:nil :cons :sym :fun :num :str :char :comm :u64 :key :env :err :thunk :builtin :bignum) -(deflexical +tags+ (allocation-tag-names (make-instance 'lurk-allocation))) +; (deflexical +tags+ (allocation-tag-names (make-instance 'lurk-allocation))) (let ((builtin-package (find-package :lurk.builtin))) (defun* lurk-builtin-p ((s symbol)) (eq (symbol-package s) builtin-package))) +;; Getting them via do-external-symbols doesn't preserve the order, so here we are... +(defparameter *builtin-list* + (list 'lurk.builtin:atom + 'lurk.builtin:apply + 'lurk.builtin:begin + 'lurk.builtin:car + 'lurk.builtin:cdr + 'lurk.builtin:char + 'lurk.builtin:commit + 'lurk.builtin:comm + 'lurk.builtin:bignum + 'lurk.builtin:cons + 'lurk.builtin:current-env + 'lurk.builtin:emit + 'lurk.builtin:empty-env + 'lurk.builtin:eval + 'lurk.builtin:eq + 'lurk.builtin:eqq + 'lurk.builtin:type-eq + 'lurk.builtin:type-eqq + 'lurk.builtin:hide + 'lurk.builtin:if + 'lurk.builtin:lambda + 'lurk.builtin:let + 'lurk.builtin:letrec + 'lurk.builtin:u64 + 'lurk.builtin:open + 'lurk.builtin:quote + 'lurk.builtin:secret + 'lurk.builtin:strcons + 'lurk.builtin:list + 'lurk.builtin:+ + 'lurk.builtin:- + 'lurk.builtin:* + 'lurk.builtin:/ + 'lurk.builtin:% + 'lurk.builtin:= + 'lurk.builtin:< + 'lurk.builtin:> + 'lurk.builtin:<= + 'lurk.builtin:>= + 'lurk.builtin:breakpoint + 'lurk.builtin:fail)) + +;; Forgive the heresy. +(defun builtin-idx (b) + (case b + (lurk.builtin:atom 0) + (lurk.builtin:apply 1) + (lurk.builtin:begin 2) + (lurk.builtin:car 3) + (lurk.builtin:cdr 4) + (lurk.builtin:char 5) + (lurk.builtin:commit 6) + (lurk.builtin:comm 7) + (lurk.builtin:bignum 8) + (lurk.builtin:cons 9) + (lurk.builtin:current-env 10) + (lurk.builtin:emit 11) + (lurk.builtin:empty-env 12) + (lurk.builtin:eval 13) + (lurk.builtin:eq 14) + (lurk.builtin:eqq 15) + (lurk.builtin:type-eq 16) + (lurk.builtin:type-eqq 17) + (lurk.builtin:hide 18) + (lurk.builtin:if 19) + (lurk.builtin:lambda 20) + (lurk.builtin:let 21) + (lurk.builtin:letrec 22) + (lurk.builtin:u64 23) + (lurk.builtin:open 24) + (lurk.builtin:quote 25) + (lurk.builtin:secret 26) + (lurk.builtin:strcons 27) + (lurk.builtin:list 28) + (lurk.builtin:+ 29) + (lurk.builtin:- 30) + (lurk.builtin:* 31) + (lurk.builtin:/ 32) + (lurk.builtin:% 33) + (lurk.builtin:= 34) + (lurk.builtin:< 35) + (lurk.builtin:> 36) + (lurk.builtin:<= 37) + (lurk.builtin:>= 38) + (lurk.builtin:breakpoint 39) + (lurk.builtin:fail 40) + )) + ;; bignum is reserved. (deftype wide-num () '(unsigned-byte 256)) @@ -23,7 +113,7 @@ (deftype maybe-env () '(or null env)) (defstruct (env (:constructor env (key value next-env))) - (key nil :type symbol) + (key nil :type t) ; Key can be of type :sym, :builtin, or :coroutine. (value nil :type t) (next-env nil :type maybe-env)) @@ -31,11 +121,12 @@ (defstruct (fun (:constructor fun (args body closed-env))) (args nil :type list) (body nil :type t) - (closed-env maybe-env)) + (closed-env cons)) (defun tag (thing) (etypecase thing - (null :nil) + (null :sym) ; nil is also a sym. + (boolean :sym) ; nil and t are both sym. (cons :cons) (keyword :key) (symbol (if (lurk-builtin-p thing) :builtin :sym)) @@ -47,7 +138,7 @@ (character :char) (comm :comm) (thunk :thunk) - (env :env) + (env :cons) (fun :fun))) ;; size is number of elements, bits is bits per 'element' @@ -67,9 +158,6 @@ (list (symbol-name symbol) (package-name (symbol-package symbol)))) (defgeneric value<-expr (tag expr) - (:method ((tag (eql :nil)) x) - (assert (null x)) - (value<-expr :sym nil)) (:method ((tag (eql :cons)) (x cons)) (let ((car (intern-wide-ptr (car x))) (cdr (intern-wide-ptr (cdr x)))) @@ -103,11 +191,15 @@ (:method ((tag (eql :bignum)) x) (make-wide :elements (le-elements<- x :size 8 :bits +element-bits+))) (:method ((tag (eql :env)) x) - (let ((env-value (intern-wide-ptr (env-value x)))) - (hash (value<-expr :sym (env-key x)) (wide-ptr-tag env-value) - (wide-ptr-value env-value) (etypecase (env-next-env x) - (env (wide-ptr-value (intern-wide-ptr (env-next-env x)))) - (null (widen 0)))))) + (let ((env-key (intern-wide-ptr (env-key x))) + (env-value (intern-wide-ptr (env-value x)))) + (hash (wide-ptr-tag env-key) + (wide-ptr-value env-key) + (wide-ptr-tag env-value) + (wide-ptr-value env-value) + (etypecase (env-next-env x) + (env (wide-ptr-value (intern-wide-ptr (env-next-env x)))) + (null (widen 0)))))) (:method ((tag (eql :thunk)) x) (let ((body (intern-wide-ptr (thunk-body x))) (closed-env (intern-wide-ptr (thunk-closed-env x)))) @@ -119,14 +211,9 @@ (closed-env (intern-wide-ptr (fun-closed-env x)))) (hash (wide-ptr-tag args) (wide-ptr-value args) (wide-ptr-tag body) (wide-ptr-value body) - (wide-ptr-tag closed-env) (wide-ptr-value closed-env))))) + (wide-ptr-value closed-env))))) (defgeneric expr<-wide (tag wide) - (:method ((tag (eql :nil)) (w wide)) - (assert (== (value<-expr :nil nil) w)) ;; todo: this is expensive. We should also just cache original values when - ;; interning. however, we need to be able to do this since we may be constructing - ;; for the first time from preimages. - nil) (:method ((tag (eql :num)) (w wide)) (assert (one-non-zero-limb-p w)) (num (wide-nth 0 w))) @@ -156,15 +243,15 @@ (thunk (expr<-wide-ptr-parts body-tag body-value) (expr<-wide-ptr-parts env-tag env-value)))) (:method ((tag (eql :fun)) (w wide)) - (destructuring-bind (args-tag args-value body-tag body-value env-tag env-value) - (unhash w 6) + (destructuring-bind (args-tag args-value body-tag body-value env-value) + (unhash w 5) (fun (expr<-wide-ptr-parts args-tag args-value) (expr<-wide-ptr-parts body-tag body-value) - (expr<-wide-ptr-parts env-tag env-value)))) + (expr<-wide-ptr-parts (tag-value :cons) env-value)))) (:method ((tag (eql :env)) (w wide)) - (destructuring-bind (key-value val-tag val-value next-env) - (unhash w 4) - (env (expr<-wide :sym key-value) + (destructuring-bind (key-tag key-value val-tag val-value next-env) + (unhash w 5) + (env (expr<-wide key-tag key-value) (expr<-wide-ptr-parts val-tag val-value) (unless (wide-zero-p next-env) (expr<-wide :env next-env))))) @@ -218,41 +305,45 @@ (test intern-wide-ptr (let ((*program* (make-program-instance 'test-program))) - (is (== (make-wide-ptr (tag-value :nil) - (wide 3988418742 3372394342 3989293407 3622167317 - 481098280 1226104118 3434725496 1157621715)) + (is (== (make-wide-ptr (tag-value :sym) + (wide 281884145 1129688213 4120351968 327773871 + 384021070 117463301 2561106250 2236819005)) (intern-wide-ptr nil))) + #+nil(is (== (make-wide-ptr (tag-value :sym) + (wide 3513864683 4092952692 2311625634 434126079 + 1771964958 3138455192 216228261 3651295992)) + (intern-wide-ptr t))) (is (== (make-wide-ptr (tag-value :cons) - (wide 1971744287 3641459736 3774975494 1609894661 - 2629299411 3809236520 3595245074 62596448)) + (wide 2469980295 1055013087 2071707850 3745798905 + 3182302750 3162655254 201317758 1580638714)) (intern-wide-ptr (cons 123 456)))) (is (== (make-wide-ptr (tag-value :sym) - (wide 3397136945 3387145446 234774522 2107533973 - 1504082815 1984471249 3548321992 3338191787)) + (wide 4271245205 4041199923 139311603 1349105236 + 664727753 2939019886 3736723608 3286357898)) (intern-wide-ptr 'asparagus))) (is (== (make-wide-ptr (tag-value :builtin) - (wide 1260038541 2992399590 2762133428 3260290791 - 4207369508 543827090 3180187974 2412760993)) + (wide 3968199370 1224537180 3052128672 2224715904 + 3672658990 2925916735 1411103358 1335116285)) (intern-wide-ptr 'lurk:current-env))) (is (== (make-wide-ptr (tag-value :num) (widen 987)) (intern-wide-ptr (num 987)))) (is (== (make-wide-ptr (tag-value :str) (widen 0)) (intern-wide-ptr ""))) - (is (== (make-wide-ptr (tag-value :str) (wide 3915542193 3963547268 1543020646 761117776 - 2609865840 67719049 4263057193 3398353849)) + (is (== (make-wide-ptr (tag-value :str) (wide 3076722117 4024338722 2289365418 698970534 + 3323852321 2245302033 976266832 315509495)) (intern-wide-ptr "boo"))) (is (== (make-wide-ptr (tag-value :char) (widen 65)) (intern-wide-ptr #\A))) - (is (== (make-wide-ptr (tag-value :comm) (wide 1397905034 3832045063 2843405970 3708064556 - 1931248981 1080144743 1379707257 644801363)) + (is (== (make-wide-ptr (tag-value :comm) (wide 311654523 2666201238 1854678539 1180780569 + 3514416075 3591153456 1110633005 2917630731)) (intern-wide-ptr (comm 0 123)))) - (is (== (make-wide-ptr (tag-value :comm) (wide 236359359 1527390219 2343696523 758167213 - 871965242 1355972474 190653183 4160106812)) + (is (== (make-wide-ptr (tag-value :comm) (wide 1168834247 1827588988 2006807406 2556695211 + 2853839954 3698934260 4200172904 2878587015)) (intern-wide-ptr (comm 1 123)))) - (is (== (make-wide-ptr (tag-value :comm) (wide 172617292 3084003310 1424146954 835899195 - 355959493 4174224837 4227269854 3448899362)) + (is (== (make-wide-ptr (tag-value :comm) (wide 434704492 2111142387 1382466299 1563109978 + 294220625 1775261771 3288317254 2170675192)) (intern-wide-ptr (comm 0 '(brass monkey))))) (is (== (make-wide-ptr (tag-value :u64) (widen 123)) (intern-wide-ptr 123))) (is (== (make-wide-ptr (tag-value :key) - (wide 1431751249 3279460643 1685215955 1633314351 - 299894911 3402633075 3048470820 3631157086)) + (wide 1228499544 2092597812 598601078 363335323 + 111897536 3513321278 2999164444 2314684892)) (intern-wide-ptr :asparagus))) (is (== (make-wide-ptr (tag-value :bignum) (wide #xffffffff #xffffffff #xffffffff #xffffffff @@ -264,26 +355,26 @@ ;; check endianness: the first limb should be affected. (intern-wide-ptr (- (expt 2 256) 2)))) (is (== (make-wide-ptr (tag-value :cons) - (wide 3601906325 1188897660 3210004168 2644944356 - 514402910 756461026 1647625721 2397550761)) + (wide 3232492942 3172902725 3905286198 3869388357 + 3770444062 3474609343 2951998298 4004311820)) (intern-wide-ptr `(foo (bar 1) (:baz #\x "monkey") ,(num 123) ,(1- (expt 2 256)))))) - (let* ((env1 (env 'a 123 nil)) + #+nil(let* ((env1 (env 'a 123 nil)) (env2 (env 'b :xxx env1))) (is (== (make-wide-ptr (tag-value :env) - (wide 597130475 2448729965 2094617081 3023196126 - 2451788936 308612520 3598067228 2002918837)) + (wide 2064456524 2837991327 1206943432 1993810858 + 165399524 1338455424 3431677448 3424566788)) (intern-wide-ptr env1))) (is (== (make-wide-ptr (tag-value :env) - (wide 3077842195 572091283 2801462678 1065752347 - 522695411 544506590 3675411477 2546351666)) + (wide 3920784138 2081306664 3462857731 2435250064 + 1090130623 216254371 3470941065 2646990734)) (intern-wide-ptr env2))) (is (== (make-wide-ptr (tag-value :thunk) - (wide 1398018567 2260761747 719070819 1427893169 - 225825928 2996049430 2412858216 2883049183)) + (wide 3496672372 2677663421 2116635234 3871946652 + 3542027988 2162033960 208146369 2711802215)) (intern-wide-ptr (thunk '(we want the thunk) env2))))) (is (== (make-wide-ptr (tag-value :fun) - (wide 2071419739 2190085449 200730859 790264635 - 1557685556 3998478079 4149964193 2656130860)) + (wide 2457271655 1361316774 3992440303 3109589054 + 3087846088 326130256 771752173 918216196)) (intern-wide-ptr (fun '(a b c) '(+ a (* b c)) nil)))))) (test expr<-wide-ptr @@ -299,13 +390,14 @@ (test-roundtrip '(1 2 (3 4))) (test-roundtrip 'a) (test-roundtrip :mango) - (let* ((env1 (env 'a 123 nil)) + #+nil(let* ((env1 (env 'a 123 nil)) (env2 (env 'b "xxx" env1))) (test-roundtrip env1) (test-roundtrip env2) - (test-roundtrip (thunk '(give up the thunk) env2)) + (test-roundtrip (thunk '(give up the thunk) '((b . "xxx") (a . 123)))) ) (test-roundtrip "roundtrip") (test-roundtrip (comm 0 123)) - (test-roundtrip (fun '(a b c) '(+ a (* b c)) nil)) - (test-roundtrip 'lurk:lambda)))) + (test-roundtrip (fun '(a b c) '(+ a (* b c)) '((x . 1)))) + (test-roundtrip 'lurk:lambda) + (test-roundtrip '('lurk:cons 1 2))))) diff --git a/loam/datalog.lisp b/loam/datalog.lisp index bc28c51..61bc8e2 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) @@ -757,35 +771,42 @@ and a list of free variables in FORM." finally (return output-rules)))) (defun synthesize-segments (segments curr-rhs end-handle) + (display 'synthesize-segments segments curr-rhs end-handle) (loop with first = t - for (segment . rest) on segments - for kind = (segment-kind segment) - for (lhs-signal . rhs-handle) = (handle-signal *prototype* segment) - when first append curr-rhs into curr-rhs-tail and do (setq first nil) - when (eql kind :predicate) - collect (make-rule `(,lhs-signal <-- ,@(copy-list curr-rhs-tail))) into output-rules - and collect rhs-handle into curr-rhs-tail - when (typep kind '(member :rule-binding :restriction)) - collect segment into curr-rhs-tail - when (eql kind :case) - ;; Case statements must be the last segment, because they split the execution into branches. - ;; When synthesizing the case, the final rule must be handled differently for each branch, - ;; so it is the responsibility of each branch (processed in the loop of `synthesize-case-segment`) - ;; to correctly finish each set rules. Thus, after `synthesize-case-segment` returns, we should - ;; immediately return as synthesis should be completed. - 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 :if) - ;; Ditto the above for if statements. - do (assert (eql rest nil)) - and append (synthesize-if-segment segment (copy-list curr-rhs-tail) end-handle) into output-rules - and do (return output-rules) - finally - ;; If we don't hit a case statement, then after we process all segments, - ;; we must finish with an final rule. - (let ((final-rule (make-rule `(,end-handle <-- ,@curr-rhs-tail)))) - (return `(,@output-rules ,final-rule))))) + for (segment . rest) on segments + for kind = (segment-kind segment) + for (lhs-signal . rhs-handle) = (handle-signal *prototype* segment) + when first append curr-rhs into curr-rhs-tail and do (setq first nil) + when (eql kind :predicate) + collect (make-rule (display `(,lhs-signal <-- ,@(copy-list curr-rhs-tail)))) into output-rules + and collect rhs-handle into curr-rhs-tail + when (typep kind '(member :rule-binding :restriction)) + collect segment into curr-rhs-tail + and do (display curr-rhs-tail) + when (eql kind :case) + ;; Case statements must be the last segment, because they split the execution into branches. + ;; When synthesizing the case, the final rule must be handled differently for each branch, + ;; so it is the responsibility of each branch (processed in the loop of `synthesize-case-segment`) + ;; to correctly finish each set rules. Thus, after `synthesize-case-segment` returns, we should + ;; immediately return as synthesis should be completed. + 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)) + and append (synthesize-if-segment segment (copy-list curr-rhs-tail) end-handle) into output-rules + and do (return output-rules) + finally + ;; If we don't hit a case statement, then after we process all segments, + ;; we must finish with an final rule. + (let ((final-rule (make-rule (display `(,end-handle <-- ,@curr-rhs-tail))))) + (return `(,@output-rules ,final-rule))))) ;; This function takes a unsynthesized rule and synthesizes it. ;; diff --git a/loam/evaluation.lisp b/loam/evaluation.lisp new file mode 100644 index 0000000..7df1e15 --- /dev/null +++ b/loam/evaluation.lisp @@ -0,0 +1,1135 @@ +(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+)) + +(setq *trace* nil) + +(defun prog-trace (&rest args) + (display args)) + +(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)) ; (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 (input-ptr expr-ptr env-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) + #+nil(let ((x (prog-trace 'output-expr ptr)))))) + +;; 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 (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))) + +;; hash-cache takes precedence over program in superclass list +(defprogram hash5 (hash-cache) + (include ptr-program) + (relation (hash5 wide wide wide wide wide)) ; (a b c d e) + (relation (unhash5 wide)) ; (digest) + (relation (hash5-rel wide wide wide wide wide wide)) ; (a b c d e digest) + + ;; signal + ;; FIXME: We assume that the c-tag must be a :cons. + (rule (alloc a-tag a-value) (alloc b-tag b-value) (alloc (tag-address :cons) c-value) <-- + (unhash5 digest) + (hash5-rel wide-a-tag a-value wide-b-tag b-value c-value digest) + (tag a-tag wide-a-tag) + (tag b-tag wide-b-tag))) + +(defprogram cons-mem (hash-cache) + (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))) + +;; FIXME: Align with Lurk by dropping closed-env-tag in the hash. +(defprogram thunk-mem (hash-cache) + (include ptr-program) + (include hash4) + + ; signal + (relation (thunk ptr ptr)) ; (body closed-env) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;;; Memory + + ;; The canonical thunk Ptr relation. + (relation (thunk-rel ptr ptr ptr)) ; (body closed-env thunk) + + ;; Memory to support thunks allocated by digest or contents. + (lattice (thunk-digest-mem wide dual-element)) ; (digest addr) + (lattice (thunk-mem ptr ptr dual-element)) ; (body closed-env addr) + + ;; Populating alloc(...) triggers allocation in thunk-digest-mem. + (rule (thunk-digest-mem value (alloc :thunk (dual 0))) <-- + (alloc (tag-address :thunk) value)) + + ;; Populating thunk(...) triggers allocation in thunk-mem. + (rule (thunk-mem body closed-env (alloc :thunk (dual 0))) <-- (thunk body closed-env)) + + ;; Populate thunk-digest-mem if a thunk in thunk-mem has been hashed in hash4-rel. + (rule (thunk-digest-mem digest addr) <-- + (thunk-mem body closed-env addr) + (ptr-value body body-value) (ptr-value closed-env closed-env-value) + (tag (ptr-tag body) body-tag) (tag (ptr-tag closed-env) closed-env-tag) + (hash4-rel body-tag body-value closed-env-tag closed-env-value digest)) + + ;; Other way around. + (rule (thunk-mem body closed-env addr) <-- + (thunk-digest-mem digest addr) + (hash4-rel body-tag body-value closed-env-tag closed-env-value digest) + (ptr-value body body-value) (ptr-value closed-env closed-env-value) + (tag (ptr-tag body) body-tag) (tag (ptr-tag closed-env) closed-env-tag)) + + ;; Register a thunk value. + (rule (ptr-value thunk value) <-- + (thunk-digest-mem value addr) (let ((thunk (ptr :thunk (dual-value addr)))))) + + ;; Register a thunk relation. + (rule (thunk-rel body closed-env thunk) <-- + (thunk-mem body closed-env addr) + (let ((thunk (ptr :cons (dual-value addr)))))) + + ;; signal + (rule (unhash4 digest) <-- + (ingress ptr) (when (has-tag-p ptr :thunk)) (ptr-value ptr digest)) + + ;; signal + (rule (hash4 body-tag body-value closed-env-tag closed-env-value) <-- + (egress thunk) + (thunk-rel body closed-env thunk) + (tag (ptr-tag body) body-tag) (tag (ptr-tag closed-env) closed-env-tag) + (ptr-value body body-value) (ptr-value closed-env closed-env-value))) + +(defprogram fun-mem (hash-cache) + (include ptr-program) + (include hash5) + + ; signal + (relation (fun ptr ptr ptr)) ; (args body closed-env) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + ;;; Memory + + ;; The canonical fun Ptr relation. + (relation (fun-rel ptr ptr ptr ptr)) ; (args body closed-env fun) + + ;; Memory to support funs allocated by digest or contents. + (lattice (fun-digest-mem wide dual-element)) ; (digest addr) + (lattice (fun-mem ptr ptr ptr dual-element)) ; (args body closed-env addr) + + ;; Populating alloc(...) triggers allocation in fun-digest-mem. + (rule (fun-digest-mem value addr) <-- + (alloc (tag-address :fun) value) + (let ((addr (alloc :fun (dual 0))) + (x (prog-trace 'alloc-fun-digest-mem addr))))) + + ;; Populating fun(...) triggers allocation in fun-mem. + (rule (fun-mem args body closed-env addr) <-- + (fun args body closed-env) + (let ((addr (alloc :fun (dual 0))) + (x (prog-trace 'alloc-fun-mem addr))))) + + ;; Populate fun-digest-mem if a fun in fun-mem has been hashed in hash5-rel. + (rule (fun-digest-mem digest addr) <-- + (fun-mem args body closed-env addr) + (ptr-value args args-value) (ptr-value body body-value) (ptr-value closed-env closed-env-value) + (tag (ptr-tag args) args-tag) (tag (ptr-tag body) body-tag) + (hash5-rel args-tag args-value body-tag body-value closed-env-value digest) + (let ((x (prog-trace 'digest<-mem addr))))) + + ;; Other way around. + (rule (fun-mem args body closed-env addr) <-- + (fun-digest-mem digest addr) + (hash5-rel args-tag args-value body-tag body-value closed-env-value digest) + (ptr-value args args-value) + (ptr-value body body-value) + (ptr-value closed-env closed-env-value) + (tag (ptr-tag args) args-tag) + (tag (ptr-tag body) body-tag) + (tag (ptr-tag closed-env) (tag-address :cons))) ; FIXME: Change to :env. + + ;; Register a fun value. + (rule (ptr-value fun value) <-- + (fun-digest-mem value addr) (let ((fun (ptr :fun (dual-value addr))))) + (let ((x (prog-trace 'fun-ptr-value))))) + + ;; Register a fun relation. + (rule (fun-rel args body closed-env fun) <-- + (fun-mem args body closed-env addr) + (let ((fun (ptr :fun (dual-value addr)))))) + + ;; signal + (rule (unhash5 digest) <-- + (ingress ptr) (when (has-tag-p ptr :fun)) (ptr-value ptr digest)) + + ;; signal + (rule (hash5 args-tag args-value body-tag body-value closed-env-value) <-- + (egress fun) + (fun-rel args body closed-env fun) + (tag (ptr-tag args) args-tag) (tag (ptr-tag body) body-tag) + (ptr-value args args-value) + (ptr-value body body-value) + (ptr-value closed-env closed-env-value)) + + ;; signal + (rule (egress args) (egress body) (egress closed-env) <-- + (egress fun) (fun-rel args body closed-env fun))) + +(defparameter *initial-sym-addr* 2) + +(defprogram sym-mem () + (include ptr-program) + + (lattice (sym-digest-mem wide dual-element)) + + ;; Populating alloc(...) triggers allocation in sym-digest-mem. + (rule (sym-digest-mem value (alloc :sym (dual *initial-sym-addr*))) <-- + (alloc (tag-address :sym) value)) + + ;; Register a sym value. + (rule (ptr-value sym value) <-- + (sym-digest-mem value addr) (let ((sym (ptr :sym (dual-value addr))))) + (let ((x (prog-trace 'sym-ptr-value sym addr)))))) + +(defparameter *initial-builtin-addr* 41) + +(defprogram builtin-mem () + (include ptr-program) + + (lattice (builtin-digest-mem wide dual-element)) + + ;; Populating alloc(...) triggers allocation in builtin-digest-mem. + (rule (builtin-digest-mem value (alloc :builtin (dual *initial-builtin-addr*))) <-- + (alloc (tag-address :builtin) value)) + + ;; Register a builtin value. + (rule (ptr-value builtin value) <-- + (builtin-digest-mem value addr) (let ((builtin (ptr :builtin (dual-value addr))))) + (let ((x (prog-trace 'builtin-ptr-value builtin addr)))))) + +(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))) + (x (prog-trace 'alloc-num tag ptr value))))) + + (rule (ptr-value ptr value) <-- + (egress ptr) (when (has-tag-p ptr :num)) + (let ((value (widen (ptr-value ptr))))))) + +;; FIXME for PQ: This is a hack for binding a value in a relation. +;; When I just write a '0', I get something like: 'etypecase failed, expected one of SYMBOL or DATALOG:VAL-FORM'. +(defun zero () 0) + +;; The Lurk evaluation. +(defprogram evaluation (hash-cache) + (include ptr-program) + (include cons-mem) + (include thunk-mem) + (include fun-mem) + (include sym-mem) + (include builtin-mem) + (include immediate-num) + + ;; Generate the necessary signal relations + + ;; Input and output. + (signal-relation (input-output (expr env evaled) (input-ptr expr env) (output-ptr evaled))) + + ;; Eval signals. + (relation (eval-input ptr ptr)) + (relation (eval ptr ptr ptr)) + (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 (body closed-env thunk) + (ingress thunk) + (thunk-rel body closed-env thunk))) + (signal-relation (signal-thunk (body closed-env thunk) + (thunk body closed-env) + (thunk-rel body closed-env thunk))) + + ;; Fun signals. + (signal-relation (ingress-fun (args body closed-env fun) + (ingress fun) + (fun-rel args body closed-env fun))) + (signal-relation (signal-fun (args body closed-env fun) + (fun args body closed-env) + (fun-rel args body closed-env fun))) + + ;; The hashing rules below are due to a design restriction of the hash-cache. + ;; Because the hash-cache is local to the subprogram it is defined from, + ;; when we intern the input and env in the outermost scope, we hash into the + ;; local hash-cache of the evaluation program instead. + + ;; signal + (rule (hash4-rel a b c d digest) <-- + (unhash4 digest) + (let ((preimage (unhash digest 4)) + (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 (hash5-rel a b c d e digest) <-- + (unhash5 digest) + (let ((preimage (unhash digest 5)) + (a (nth 0 preimage)) + (b (nth 1 preimage)) + (c (nth 2 preimage)) + (d (nth 3 preimage)) + (e (nth 4 preimage))))) + + ;; signal + (rule (hash5-rel a b c d e (hash a b c d e)) <-- (hash5 a b c d e)) + + ;; 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 + ;; Self-evaluating forms. + ((has-tag-p expr :num) ((let ((evaled expr))))) + ((has-tag-p expr :err) ((let ((evaled expr))))) + ((is-nil expr) ((let ((evaled expr))))) + ((is-t expr) ((let ((evaled expr))))) + ((has-tag-p expr :sym) ((signal-lookup expr env evaled))) + + ;; Interesting cons case: + ((has-tag-p expr :cons) + ((ingress-cons head rest expr) + (cond + ;; Evaluate cons operator. + #+nil + ((== head (builtin-ptr '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. + #+nil + ((== head (builtin-ptr 'lurk:if)) ((ingress-cons cond branches rest) + (signal-eval cond env evaled-cond) + (ingress-cons a more branches) + (if (is-nil evaled-cond) + ((ingress-cons b end more) + (when (is-nil end)) + (signal-eval b env evaled)) + ((signal-eval a env evaled))))) + ;; Evaluate let/letrec. + + ((or (== head (builtin-ptr 'lurk:let)) (== head (builtin-ptr 'lurk:letrec))) + ((ingress-cons bindings tail rest) + (ingress-cons body end tail) + (when (is-nil end)) + (signal-eval-bindings bindings env (== head (builtin-ptr 'lurk:letrec)) extended-env) + (signal-eval body extended-env evaled))) + ;; Evaluate lambda. + ((== head (builtin-ptr 'lurk:lambda)) ((ingress-cons args tail rest) + (ingress-cons body end tail) + (when (is-nil end)) + (signal-fun args body env evaled))) + ;; Evaluate +. FIXME: Generalize to more ops. + ((== head (builtin-ptr 'lurk:+)) ((signal-fold-left head (zero) rest acc) + (let ((evaled (ptr :num acc)))))) + ;; Evaluate =. FIXME: Generalize to more ops and bool-fold. + #+nil + ((== head (builtin-ptr 'lurk:=)) ((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 env evaled))) + ((and (not (has-tag-p head :fun)) (not (has-tag-p head :builtin))) + ((signal-eval head env fun) + (ingress-fun args body closed-env fun) + (signal-funcall args body closed-env rest env evaled))) + + ))))) + + ;; 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)))) + + (synthesize-rule (signal-eval-bindings bindings extended-env is-rec final-env) <-- + (if (is-nil bindings) + ((let ((final-env extended-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) + (signal-cons env-binding extended-env new-env) + (signal-eval-bindings more-bindings new-env is-rec final-env)) + ;; Non-recursive case: just evaluate. + ;; 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. + ((signal-eval unevaled extended-env evaled) + (signal-cons var evaled env-binding) + (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 (cond ;; Slightly annoying thing: case doesn't produce == and incorrectly checks ptr equality. + ((== op (builtin-ptr 'lurk:+)) (+ (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)))) + ) + +(defprogram syn-evaluation (hash-cache) + (include ptr-program) + (include cons-mem) + (include thunk-mem) + (include fun-mem) + (include sym-mem) + (include builtin-mem) + (include immediate-num) + + ;; Generate the necessary signal relations + + ;; Input and output. + (signal-relation (input-output (expr env evaled) (input-ptr expr env) (output-ptr evaled))) + + ;; Eval signals. + (relation (eval-input ptr ptr)) + (relation (eval ptr ptr ptr)) + (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 (body closed-env thunk) + (ingress thunk) + (thunk-rel body closed-env thunk))) + (signal-relation (signal-thunk (body closed-env thunk) + (thunk body closed-env) + (thunk-rel body closed-env thunk))) + + ;; Fun signals. + (signal-relation (ingress-fun (args body closed-env fun) + (ingress fun) + (fun-rel args body closed-env fun))) + (signal-relation (signal-fun (args body closed-env fun) + (fun args body closed-env) + (fun-rel args body closed-env fun))) + + ;; The hashing rules below are due to a design restriction of the hash-cache. + ;; Because the hash-cache is local to the subprogram it is defined from, + ;; when we intern the input and env in the outermost scope, we hash into the + ;; local hash-cache of the evaluation program instead. + + ;; signal + (rule (hash4-rel a b c d digest) <-- + (unhash4 digest) + (let ((preimage (unhash digest 4)) + (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 (hash5-rel a b c d e digest) <-- + (unhash5 digest) + (let ((preimage (unhash digest 5)) + (a (nth 0 preimage)) + (b (nth 1 preimage)) + (c (nth 2 preimage)) + (d (nth 3 preimage)) + (e (nth 4 preimage))))) + + ;; signal + (rule (hash5-rel a b c d e (hash a b c d e)) <-- (hash5 a b c d e)) + + ;; Connect eval to input/output. + (synthesize-rule (input-output expr env evaled) <-- (signal-eval expr env evaled)) + + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :NUM)) + (LET ((EVALED EXPR)))) + + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :ERR)) + (LET ((EVALED EXPR)))) + + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (IS-NIL EXPR)) + (LET ((EVALED EXPR)))) + + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (IS-T EXPR)) + (LET ((EVALED EXPR)))) + + (RULE + (LOOKUP-INPUT EXPR ENV) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :SYM)) + (let ((x (prog-trace 'lookup-start expr env))))) + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :SYM)) + (LOOKUP EXPR ENV EVALED) + (let ((x (prog-trace 'lookup-end expr env evaled))))) + + (RULE + (INGRESS REST) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :CONS)) + (CONS-REL HEAD REST EXPR) + (WHEN + (OR (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LET)) + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC))))) + (RULE + (INGRESS TAIL) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :CONS)) + (CONS-REL HEAD REST EXPR) + (WHEN + (OR (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LET)) + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)))) + (CONS-REL BINDINGS TAIL REST)) + (RULE + (EVAL-BINDINGS-INPUT BINDINGS ENV + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC))) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :CONS)) + (CONS-REL HEAD REST EXPR) + (WHEN + (OR (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LET)) + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)))) + (CONS-REL BINDINGS TAIL REST) + (CONS-REL BODY END TAIL) + (WHEN (IS-NIL END)) + (let ((x (prog-trace 'bindings-start))))) + (RULE + (EVAL-INPUT BODY EXTENDED-ENV) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :CONS)) + (CONS-REL HEAD REST EXPR) + (WHEN + (OR (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LET)) + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)))) + (CONS-REL BINDINGS TAIL REST) + (CONS-REL BODY END TAIL) + (WHEN (IS-NIL END)) + (EVAL-BINDINGS BINDINGS ENV + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)) EXTENDED-ENV) + (let ((x (prog-trace 'bindings-end))))) + (RULE + (EVAL EXPR ENV EVALED) + <-- + (EVAL-INPUT EXPR ENV) + (WHEN (HAS-TAG-P EXPR :CONS)) + (CONS-REL HEAD REST EXPR) + (WHEN + (OR (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LET)) + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)))) + (CONS-REL BINDINGS TAIL REST) + (CONS-REL BODY END TAIL) + (WHEN (IS-NIL END)) + (EVAL-BINDINGS BINDINGS ENV + (== HEAD (BUILTIN-PTR 'LURK.BUILTIN:LETREC)) EXTENDED-ENV) + (EVAL BODY EXTENDED-ENV EVALED)) + + ;;;;; LOOKUP + + (RULE + (INGRESS ENV) + <-- + (LOOKUP-INPUT VAR ENV) + (let ((x (prog-trace 'lookup-ingress-env var env))))) + (RULE + (INGRESS BINDING) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (let ((x (prog-trace 'lookup-ingress-binding var binding more-env))))) + (RULE + (INGRESS BOUND-VALUE) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (== VAR BOUND-VAR)) + (WHEN (HAS-TAG-P BOUND-VALUE :THUNK))) + (RULE + (CONS BINDING CLOSED-ENV) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (== VAR BOUND-VAR)) + (WHEN (HAS-TAG-P BOUND-VALUE :THUNK)) + (THUNK-REL BODY CLOSED-ENV BOUND-VALUE)) + (RULE + (EVAL-INPUT BODY EXTENDED-ENV) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (== VAR BOUND-VAR)) + (WHEN (HAS-TAG-P BOUND-VALUE :THUNK)) + (THUNK-REL BODY CLOSED-ENV BOUND-VALUE) + (CONS-REL BINDING CLOSED-ENV EXTENDED-ENV)) + (RULE + (LOOKUP VAR ENV VALUE) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (== VAR BOUND-VAR)) + (WHEN (HAS-TAG-P BOUND-VALUE :THUNK)) + (THUNK-REL BODY CLOSED-ENV BOUND-VALUE) + (CONS-REL BINDING CLOSED-ENV EXTENDED-ENV) + (EVAL BODY EXTENDED-ENV VALUE)) + (RULE + (LOOKUP VAR ENV VALUE) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (== VAR BOUND-VAR)) + (WHEN (NOT (HAS-TAG-P BOUND-VALUE :THUNK))) + (LET ((VALUE BOUND-VALUE) + (x (prog-trace 'lookup-not-thunk-eq var bound-var value))))) + (RULE + (LOOKUP-INPUT VAR MORE-ENV) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (NOT (== VAR BOUND-VAR))) + (let ((x (prog-trace 'lookup-recurse-start var more-env))))) + (RULE + (LOOKUP VAR ENV VALUE) + <-- + (LOOKUP-INPUT VAR ENV) + (CONS-REL BINDING MORE-ENV ENV) + (CONS-REL BOUND-VAR BOUND-VALUE BINDING) + (WHEN (NOT (== VAR BOUND-VAR))) + (LOOKUP VAR MORE-ENV VALUE) + (let ((x (prog-trace 'lookup-recurse-end var more-env value))))) + + ;;;;; EVAL-BINDINGS + + (RULE + (INGRESS BINDINGS) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (let ((x (prog-trace 'bindings-ingress is-rec))))) + (RULE + (INGRESS BINDING) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (let ((x (prog-trace 'bindings-ingress-binding binding more-bindings))))) + (RULE + (INGRESS BINDING-TAIL) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (let ((x (prog-trace 'bindings-ingress-tail var))))) + (RULE + (THUNK UNEVALED EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (let ((x (prog-trace 'bindings-signal-thunk unevaled (is-nil end) is-rec))))) + (RULE + (CONS VAR THUNK) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (let ((x (prog-trace 'bindings-signal-cons-binding thunk))))) + (RULE + (CONS ENV-BINDING EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (CONS-REL VAR THUNK ENV-BINDING) + (WHEN (IS-NIL MORE-BINDINGS)) + (let ((x (prog-trace 'bindings-signal-cons-final-env env-binding extended-env))))) + (RULE + (EVAL-BINDINGS BINDINGS EXTENDED-ENV IS-REC FINAL-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (CONS-REL VAR THUNK ENV-BINDING) + (WHEN (IS-NIL MORE-BINDINGS)) + (CONS-REL ENV-BINDING EXTENDED-ENV FINAL-ENV) + (let ((x (prog-trace 'bindings-signal-return final-env))))) + (RULE + (CONS ENV-BINDING EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (CONS-REL VAR THUNK ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS)))) + (RULE + (EVAL-BINDINGS-INPUT MORE-BINDINGS NEW-ENV IS-REC) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (CONS-REL VAR THUNK ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS))) + (CONS-REL ENV-BINDING EXTENDED-ENV NEW-ENV)) + (RULE + (EVAL-BINDINGS BINDINGS EXTENDED-ENV IS-REC FINAL-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN IS-REC) + (THUNK-REL UNEVALED EXTENDED-ENV THUNK) + (CONS-REL VAR THUNK ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS))) + (CONS-REL ENV-BINDING EXTENDED-ENV NEW-ENV) + (EVAL-BINDINGS MORE-BINDINGS NEW-ENV IS-REC FINAL-ENV)) + (RULE + (EVAL-INPUT UNEVALED EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC))) + (RULE + (CONS VAR EVALED) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED)) + (RULE + (CONS ENV-BINDING EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED) + (CONS-REL VAR EVALED ENV-BINDING) + (WHEN (IS-NIL MORE-BINDINGS))) + (RULE + (EVAL-BINDINGS BINDINGS EXTENDED-ENV IS-REC FINAL-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED) + (CONS-REL VAR EVALED ENV-BINDING) + (WHEN (IS-NIL MORE-BINDINGS)) + (CONS-REL ENV-BINDING EXTENDED-ENV FINAL-ENV) + (let ((x (prog-trace 'bindings- thunk))))) + (RULE + (CONS ENV-BINDING EXTENDED-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED) + (CONS-REL VAR EVALED ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS)))) + (RULE + (EVAL-BINDINGS-INPUT MORE-BINDINGS NEW-ENV IS-REC) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED) + (CONS-REL VAR EVALED ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS))) + (CONS-REL ENV-BINDING EXTENDED-ENV NEW-ENV) + (let ((x (prog-trace 'bindings-recurse-start more-bindings new-env))))) + (RULE + (EVAL-BINDINGS BINDINGS EXTENDED-ENV IS-REC FINAL-ENV) + <-- + (EVAL-BINDINGS-INPUT BINDINGS EXTENDED-ENV IS-REC) + (CONS-REL BINDING MORE-BINDINGS BINDINGS) + (CONS-REL VAR BINDING-TAIL BINDING) + (CONS-REL UNEVALED END BINDING-TAIL) + (WHEN (IS-NIL END)) + (WHEN (NOT IS-REC)) + (EVAL UNEVALED EXTENDED-ENV EVALED) + (CONS-REL VAR EVALED ENV-BINDING) + (WHEN (NOT (IS-NIL MORE-BINDINGS))) + (CONS-REL ENV-BINDING EXTENDED-ENV NEW-ENV) + (EVAL-BINDINGS MORE-BINDINGS NEW-ENV IS-REC FINAL-ENV) + (let ((x (prog-trace 'bindings-recurse-end bindings final-env))))) + ) + + +(defparameter *ptr-nil* (make-ptr 10 0)) +(defparameter *ptr-t* (make-ptr 10 1)) + +(defun is-nil (ptr) (== ptr *ptr-nil*)) +(defun is-t (ptr) (== ptr *ptr-t*)) +(defun builtin-ptr (sym) + (make-ptr 8 (builtin-idx sym))) + +(defun initial-sym-digest-mem () + (loop for sym in (list nil t) + for i from 0 + for sym-value = (wide-ptr-value (intern-wide-ptr sym)) + collect (list sym-value (dual i)))) + +;; FIXME for PQ: When I try to load in all the builtins, the program just freezes up and spins. +;; i.e. tests that were passing before instantly now hang and don't return unless I forcibly exit. +#+nil +(defun initial-builtin-digest-mem () + (loop for b in *builtin-list* + for i from 0 + for builtin-value = (wide-ptr-value (intern-wide-ptr b)) + collect (list builtin-value (dual i)))) + +(defun initial-builtin-digest-mem () + (loop for b in (list 'lurk:lambda 'lurk:+ 'lurk:let) + for i = (builtin-idx b) + for builtin-value = (wide-ptr-value (intern-wide-ptr b)) + collect (list builtin-value (dual i)))) + +(defun display-relation (program relation) + (let ((x (find-relation program relation))) + (display relation (relation-tuple-list x)))) + +(defun test-aux (input env expected-output) + (let* ((program (make-program-instance 'evaluation)) + (*program* program) + ; (src (spec (find-prototype 'evaluation))) + ) + ; (display 'src src) + (init program `(toplevel-input ((,(display (intern-wide-ptr input)) ,(intern-wide-ptr env))) + sym-digest-mem ,(initial-sym-digest-mem) + builtin-digest-mem ,(initial-builtin-digest-mem))) + (run program) + + (display-relation program 'alloc) + (display-relation program 'ingress) + (display-relation program 'cons-mem) + (display-relation program 'cons-digest-mem) + + (display-relation program 'ptr-value) + (display-relation program 'unhash4) + (display-relation program 'hash4-rel) + + (display-relation program 'eval) + (display-relation program 'output-ptr) + + (is (== `((,(intern-wide-ptr expected-output))) (relation-tuple-list (find-relation program 'output-expr)))))) + +(test self-evaluating-num + (test-aux (num 123) nil (num 123))) + +(test self-evaluating-nil + (test-aux nil nil nil)) + +(test self-evaluating-t + (test-aux t nil t)) + +(test zero-arg-addition + (test-aux '(lurk:+) nil (num 0))) + +(test one-arg-addition + (test-aux `(lurk:+ ,(num 1)) nil (num 1))) + +(test two-arg-addition + (test-aux `(lurk:+ ,(num 1) ,(num 2)) nil (num 3))) + +(test three-arg-addition + (test-aux `(lurk:+ ,(num 1) ,(num 2) ,(num 3)) nil (num 6))) + +(test relational-t + (test-aux `(lurk:= ,(num 1) ,(num 1)) nil t)) + +(test relational-nil + (test-aux `(lurk:= ,(num 1) ,(num 2)) nil nil)) + +(test if-t + (test-aux `(lurk:if (lurk:= ,(num 1) ,(num 1)) ,(num 123) ,(num 456)) nil (num 123))) + +(test if-nil + (test-aux `(lurk:if (lurk:= ,(num 1) ,(num 2)) ,(num 123) ,(num 456)) nil (num 456))) + +(test var-lookup + (test-aux 'x `((x . ,(num 9))) (num 9))) + +(test deep-var-lookup + (test-aux 'y `((x . ,(num 9)) (y . ,(num 10))) (num 10))) + +(test let-plain + (test-aux `(lurk:let ((x ,(num 1))) x) nil (num 1))) + +(test lambda-plain + (test-aux `(lurk:lambda (x) (lurk:+ x ,(num 1))) nil (fun '(x) `(lurk:+ x ,(num 1)) nil))) + +(test funcall + (test-aux `(lurk:let ((f (lurk:lambda (x) (lurk:+ x ,(num 1))))) + (f ,(num 2))) + nil + (num 3))) + +(test letrec-plain + (test-aux `(lurk:letrec ((x ,(num 1))) x) nil (num 1))) + +(test evaluation-spec + (is (compare-spec 'evaluation 'syn-evaluation))) diff --git a/loam/package.lisp b/loam/package.lisp index efebe38..644adf4 100644 --- a/loam/package.lisp +++ b/loam/package.lisp @@ -29,28 +29,28 @@ #: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+ )) + (:export #:*program* #:element #:dual-element #:ptr #:make-ptr #:ptr-tag #:ptr-value #: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 #:tag-address #:nth-tag #:lurk-allocation + #:allocation-tag-names #:alloc #:hash-cache #:hash #:unhash #:+element-bits+ #:is-tag-p #:has-tag-p)) (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 - #:t #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint)) + (:export #:atom #:apply #:begin #:car #:cdr #:char #:commit #:comm #:bignum #:cons #:current-env #:emit #:empty-env #:eval + #:eq #:eqq #:type-eq #:type-eqq #:hide #:if #:lambda #:let #:letrec #:u64 #:open #:quote #:secret #:strcons #:list + #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint #:fail)) (defpackage lurk - (:import-from #:lurk.builtin #: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 #:t #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint) - (: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 #:t #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint) + (:import-from #:lurk.builtin #:atom #:apply #:begin #:car #:cdr #:char #:commit #:comm #:bignum #:cons #:current-env #:emit + #:empty-env #:eval #:eq #:eqq #:type-eq #:type-eqq #:hide #:if #:lambda #:let #:letrec #:u64 #:open + #:quote #:secret #:strcons #:list #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint #:fail) + (:export #:atom #:apply #:begin #:car #:cdr #:char #:commit #:comm #:bignum #:cons #:current-env #:emit #:empty-env #:eval + #:eq #:eqq #:type-eq #:type-eqq #:hide #:if #:lambda #:let #:letrec #:u64 #:open #:quote #:secret #:strcons #:list + #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint #:fail #:nil #:t) ) (defpackage lurk-user - (:import-from #:lurk #: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 #:t #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint)) + (:import-from #:lurk #:atom #:apply #:begin #:car #:cdr #:char #:commit #:comm #:bignum #:cons #:current-env #:emit #:empty-env #:eval + #:eq #:eqq #:type-eq #:type-eqq #:hide #:if #:lambda #:let #:letrec #:u64 #:open #:quote #:secret #:strcons #:list + #:+ #:- #:* #:/ #:% #:= #:< #:> #:<= #:>= #:breakpoint #:fail #:nil #:t)) (defpackage data (:use #:common-lisp) @@ -61,7 +61,23 @@ (:import-from #:allocation #:*program* #:lurk-allocation #:allocation-tag-names #:element #:wide #:wide-elements #:wide-nth #:make-wide #:widen #:wide-ptr #:make-wide-ptr #:wide-ptr-tag #:wide-ptr-value #:tag-name #:tag-value #:tag #:== #:hash-cache #:hash #:unhash #:+element-bits+ #:nth-tag) - (:export #:intern-wide-ptr)) + (:export #:builtin-idx #:*builtin-list* #:intern-wide-ptr #:num #:env #:thunk #:fu)) + +(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) + (:import-from #:allocation #:*program* #:element #:dual-element #:ptr #:make-ptr #:ptr-tag #:ptr-value #: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 #:tag-address #:nth-tag #:lurk-allocation + #:allocation-tag-names #:alloc #:hash-cache #:hash #:unhash #:+element-bits+ #:is-tag-p #:has-tag-p) + (:import-from #:data #:builtin-idx #:*builtin-list* #:intern-wide-ptr #:num #:env #:thunk #:fun)) (defpackage loam (:use #:common-lisp)