From db3d2bc6fe429d479abd49882eef048f8553838f Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Tue, 30 May 2023 14:08:08 +0800 Subject: [PATCH 1/3] STLC to Geb Compilation Fix Fixes the compilation of STLC to Geb discarding previous uncurrying changes in favour of uncurrying only the final result. Further this commit adds tests to make sure that furhter issues from this problem does not happen --- src/lambda/trans.lisp | 126 +++++++++++++++++++++++++++++++++-------- test/lambda-trans.lisp | 44 +++++++++++++- 2 files changed, 144 insertions(+), 26 deletions(-) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index 69a88aace..b65f52553 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -84,7 +84,13 @@ s-1 ``` as we count indeces from the left of the context while appending new types to -the context on the left as well. For more info check [LAMB][class]" +the context on the left as well. For more info check [LAMB][class] + +Finally, note that the compilation uncurries the final morphism. That is, +if the type of the term is an exponential object, [TO-CAT] uncurries the +morphism in the Geb category instead producing a morphism into the domain +of the exponential from a corresponding product. If the exponential is +iterated, so is the uncurrying." (labels ((rec (context tterm) (match-of stlc tterm ((absurd tcod term) @@ -101,18 +107,15 @@ the context on the left as well. For more info check [LAMB][class]" (comp (->right (mcar tott) (mcadr tott)) (rec context term)))) ((case-on on ltm rtm) - (let ((ctx (stlc-ctx-to-mu context)) - (mcr (mcar (ttype on))) - (mcdr (mcadr (ttype on)))) - (comp (comp (mcase (commutes-left (rec - (cons mcr context) ltm)) - (commutes-left (rec - (cons mcdr context) rtm))) - (commutes-left (distribute ctx - (fun-to-hom mcr) - (fun-to-hom mcdr)))) - (geb:pair (rec context on) - ctx)))) + (let ((mcartoon (mcar (ttype on))) + (mcadrtoon (mcadr (ttype on))) + (ctx (stlc-ctx-to-mu context))) + (comp (mcase (commutes-left (rec + (cons (fun-to-hom mcartoon) context) ltm)) + (commutes-left (rec + (cons (fun-to-hom mcadrtoon) context) rtm))) + (comp (distribute ctx mcartoon mcadrtoon) + (geb:pair ctx (rec context on)))))) ((pair ltm rtm) (geb:pair (rec context ltm) (rec context rtm))) @@ -125,21 +128,80 @@ the context on the left as well. For more info check [LAMB][class]" (comp (<-right (mcar tottt) (mcadr tottt)) (to-cat context term)))) ((lamb tdom term) - (rec (append tdom context) term)) + (apply-n (length tdom) + #'(lambda (x) (curry (commutes-left x))) + (rec (append tdom context) term))) ((app fun term) - (comp (rec context fun) - (reduce #'geb:pair - (mapcar (lambda (x) (rec context x)) - term) - :initial-value (stlc-ctx-to-mu context) - :from-end t))) + (let ((tofun (ttype fun))) + (comp + (so-eval (fun-to-hom (mcar tofun)) + (fun-to-hom (mcadr tofun))) + (geb:pair (rec context fun) + (reduce #'geb:pair + (mapcar #'(lambda (x) (rec context x)) term) + :from-end t))))) ((index pos) (stlc-ctx-proj context pos))))) - (if (well-defp context tterm) - (rec context (ann-term1 context tterm)) - (error "not a well-defined ~A in said ~A" tterm context)))) + (cond ((not (well-defp context tterm)) + (error "not a well-defined ~A in said ~A" tterm context)) + ((typep (type-of-term-w-fun context tterm) 'fun-type) + (fun-uncurry-prod (type-of-term-w-fun context tterm) + (rec context (ann-term1 context tterm)))) + (t + (rec context (ann-term1 context tterm)))))) + +(defun fun-depth (obj) + "Looks at how iterated a function type is with [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] +being 0 iterated looking at the [MCADR][generic-function]. E.g.: + +```lisp +TRANS> (fun-depth so1) +0 + +TRANS> (fun-depth (fun-type so1 so1)) +1 +TRANS> (fun-depth (fun-type so1 (fun-type so1 so1))) +2 +TRANS> (fun-depth (fun-type (fun-type so1 so1) so1)) +1 +```" + (if (not (typep obj 'fun-type)) + 0 + (1+ (fun-depth (mcadr obj))))) + +(defun fun-uncurry-prod (obj f) + "Takes a morphism f : X -> obj where obj is an iterated function type +represented in Geb as B^(A1 x ... x An) and uncurries it but looking at the +iteration as product to a morphism f' : (A1 x ... An) x X -> B. E.g: + +``lisp +TRANS> (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1)) +(∘ (∘ (∘ (<-left s-1 s-1) + ((∘ (<-left s-1 s-1) + ((<-left s-1 (× s-1 s-1)) + (∘ (<-left s-1 s-1) (<-right s-1 (× s-1 s-1))))) + (∘ (<-right s-1 s-1) (<-right s-1 (× s-1 s-1))))) + ((∘ (0-> s-1) (<-left s-0 (× s-1 s-1))) (<-right s-0 (× s-1 s-1)))) + ((<-right (× s-1 s-1) s-0) (<-left (× s-1 s-1) s-0))) + +TRANS> (dom (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1))) +(× (× s-1 s-1) s-0) + +TRANS> (codom (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1))) +s-1 +```" + (labels ((lst-mcar (num ob) + (if (= num 1) + (list (mcar ob)) + (cons (mcar (apply-n (1- num) #'mcadr ob)) + (lst-mcar (1- num) ob))))) + (commutes-left (uncurry (reduce #'prod + (lst-mcar (fun-depth obj) obj) + :from-end t) + (apply-n (fun-depth obj) #'mcadr obj) + f)))) (-> stlc-ctx-to-mu (stlc-context) substobj) (defun stlc-ctx-to-mu (context) @@ -176,6 +238,24 @@ length with fibrations given by [PROD][class] projections." (<-right (fun-to-hom (car context)) (stlc-ctx-to-mu (cdr context)))))) +(defun prod-rem (num obj) + "Given a product A0 x A1 x ... x An and a positive integer k gives a +corresponding composition of morphisms projecting to Ak x ... x An" + (if (= num 1) + (<-right (mcar obj) (mcadr obj)) + (comp (<-right (mcar (apply-n (- num 1) #'mcadr obj)) + (apply-n num #'mcadr obj)) + (prod-rem (1- num) obj)))) + +(defun prod-proj (num obj) + "Given a product A0 x ... x An and an integer k less than n gives a +corresponding composition of projection morphism to Ak" + (if (zerop num) + (<-left (mcar obj) (mcadr obj)) + (let ((codm (codom (prod-rem num obj)))) + (comp (<-left (mcar codm) codm) + (prod-rem num obj))))) + (defun index-to-projection (depth typ-a typ-b prod) (if (zerop depth) (comp (<-left typ-a typ-b) prod) diff --git a/test/lambda-trans.lisp b/test/lambda-trans.lisp index 7d627f36f..8029514ff 100644 --- a/test/lambda-trans.lisp +++ b/test/lambda-trans.lisp @@ -22,11 +22,21 @@ (lambda:right so1 (lambda:unit)) (lambda:left so1 (lambda:unit))))) +(def proper-not + (lambda:lamb + (list (coprod so1 so1)) + (lambda:case-on (lambda:index 0) + (lambda:right so1 (lambda:index 0)) + (lambda:left so1 (lambda:index 0))))) + (def lambda-pairing (lambda:lamb (list geb-bool:bool) (lambda:pair (lambda:right so1 (lambda:index 0)) (lambda:left so1 (lambda:index 0))))) +(def bool-id + (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0))) + (def issue-58-circuit (to-circuit (lambda:case-on @@ -35,6 +45,18 @@ (lambda:lamb (list so1) (lambda:left so1 (lambda:unit)))) :tc_issue_58)) +(defparameter *issue-94-circuit* + (lambda:app (lambda:lamb (list (lambda:fun-type + (lambda:fun-type (coprod so1 so1) + (coprod so1 so1)) + (coprod so1 so1))) + (lambda:app (lambda:index 0) + (list (lambda:lamb (list (coprod so1 so1)) + (lambda:index 0))))) + (list (lambda:lamb (list (lambda:fun-type (coprod so1 so1) + (coprod so1 so1))) + (lambda:left so1 (lambda:unit)))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Interpreter tests ;; @@ -63,13 +85,23 @@ (is obj-equalp (right so1) (gapply - (to-cat nil (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0))) + (to-cat nil bool-id) (list (right so1) so1))) (is obj-equalp (left so1) (gapply - (to-cat nil (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0))) - (list (left so1) so1)))) + (to-cat nil bool-id) + (list (left so1) so1))) + (is obj-equalp #*0 (gapply (to-bitc bool-id) #*0)) + (is obj-equalp #*1 (gapply (to-bitc bool-id) #*1))) + +(define-test lambda.not-works :parent lambda.trans-eval + (is obj-equalp (left so1) (gapply (to-cat nil proper-not) + (list (geb:right so1) so1))) + (is obj-equalp (right so1) (gapply (to-cat nil proper-not) + (list (geb:left so1) so1))) + (is equalp #*0 (gapply (to-bitc proper-not) #*1)) + (is equalp #*1 (gapply (to-bitc proper-not) #*0))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Compile checked term tests ;; @@ -131,3 +163,9 @@ (lambda:absurd so1 (lambda:index 0))) :tc_void_to_unit)) (of-type list issue-58-circuit)) + +(define-test issue-94-compiles :parent geb.lambda.trans + (parachute:finish + (geb.entry:compile-down :stlc t + :entry "geb-test::*issue-94-circuit*" + :stream nil))) From d52745d5085b15901a030bd228049c8129c3f393 Mon Sep 17 00:00:00 2001 From: mariari Date: Tue, 30 May 2023 16:43:54 +0800 Subject: [PATCH 2/3] Create a generic maybe function that can take the maybe of any object This includes the generic function and all valid instances, and documentation for how it works --- src/geb/geb.lisp | 20 ++++++++++++++++++++ src/geb/package.lisp | 5 ++++- src/generics/generics.lisp | 19 +++++++++++++++++++ src/generics/package.lisp | 1 + src/lambda/lambda.lisp | 19 +++++++++++++++++++ src/lambda/package.lisp | 3 +-- 6 files changed, 64 insertions(+), 3 deletions(-) diff --git a/src/geb/geb.lisp b/src/geb/geb.lisp index 8f472a8b2..c30ab6028 100644 --- a/src/geb/geb.lisp +++ b/src/geb/geb.lisp @@ -266,6 +266,26 @@ This is the morphism part of the product functor Geb x Geb → Geb" (defmethod text-name ((morph cat-obj)) "Id") +(defmethod maybe ((obj )) + "I recursively add maybe terms to all [\\][class] terms, +for what maybe means checkout [my generic function documentation][maybe]. + +turning [products][prod] of A x B into Maybe (Maybe A x Maybe B), + +turning [coproducts][coprod] of A | B into Maybe (Maybe A | Maybe B), + +turning [SO1] into Maybe [SO1] + +and [SO0] into Maybe [SO0]" + (typecase-of substobj obj + (so0 (coprod so1 so0)) + (so1 (coprod so1 so1)) + (coprod (coprod so1 (coprod (maybe (mcar obj)) + (maybe (mcadr obj))))) + (prod (coprod so1 (prod (maybe (mcar obj)) + (maybe (mcadr obj))))) + (otherwise (subclass-responsibility obj)))) + (defun curry (f) "Curries the given object, returns a [cat-morph] diff --git a/src/geb/package.lisp b/src/geb/package.lisp index ab01f987d..bde4b8647 100644 --- a/src/geb/package.lisp +++ b/src/geb/package.lisp @@ -29,7 +29,10 @@ (coprod-mor pax:function) (prod-mor pax:function) (uncurry pax:function) - (text-name pax:generic-function)) + (text-name pax:generic-function) + + "These utilities are ontop of [CAT-OBJ]" + (maybe (pax:method () ()))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Standard Library throughout the codebase diff --git a/src/generics/generics.lisp b/src/generics/generics.lisp index 75e78ed54..3d79bbb8a 100644 --- a/src/generics/generics.lisp +++ b/src/generics/generics.lisp @@ -23,6 +23,25 @@ GEB> (gapply (comp (left s-1) ```")) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Object Functions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defgeneric maybe (object) + (:documentation + "Wraps the given OBJECT into a Maybe monad The Maybe monad in this +case is simply wrapping the term in a [coprod][geb.spec:coprod] +of [so1][geb.spec:so1] + +``` lisp +;; Before +x + +;; After +(COPROD SO1 X) +```")) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Conversion functions ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/src/generics/package.lisp b/src/generics/package.lisp index 7f6738404..db520b679 100644 --- a/src/generics/package.lisp +++ b/src/generics/package.lisp @@ -13,6 +13,7 @@ You can view their documentation in their respective API sections. The main documentation for the functionality is given here, with examples often given in the specific methods" (gapply pax:generic-function) + (maybe pax:generic-function) (to-circuit pax:generic-function) (to-bitc pax:generic-function) (to-poly pax:generic-function) diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp index 8a4da47cb..6aaa3b896 100644 --- a/src/lambda/lambda.lisp +++ b/src/lambda/lambda.lisp @@ -18,6 +18,25 @@ pointwise.")) (defun fun-type (mcar mcadr) (make-instance 'fun-type :mcar mcar :mcadr mcadr)) +(defmethod maybe ((object fun-type)) + "I recursively add maybe terms to my domain and codomain, and even +return a maybe function. Thus if the original function was + +``` +f : a -> b +``` + +we would now be + +``` +f : maybe (maybe a -> maybe b) +``` + +for what maybe means checkout [my generic function documentation][maybe]." + (coprod so1 + (fun-type (maybe (mcar object)) + (maybe (mcadr object))))) + ;; Below we list all possible ways of getting a term of the exponential, ;; namely: projections, casing, absurd, lambda-abstraction and application diff --git a/src/lambda/package.lisp b/src/lambda/package.lisp index ced7cdf71..fdb3a0889 100644 --- a/src/lambda/package.lisp +++ b/src/lambda/package.lisp @@ -30,8 +30,7 @@ (mcar (pax:method () (fun-type))) (mcadr (pax:method () (fun-type))) - (mcar pax:generic-function) - (mcadr pax:generic-function)) + (maybe (pax:method () (fun-type)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; trans module From ffcb198ec4d3b2795b381e8bfb59a6e787f971e5 Mon Sep 17 00:00:00 2001 From: Artem Gureev Date: Tue, 30 May 2023 14:21:20 +0800 Subject: [PATCH 3/3] Error Node Extension of STLC and Maybe Compilation Wrapper Adds an error node of an arbitrary type as a new STLC constructor. Appropriatelly changes the compilation procedure to Geb in case an STLC term has an error subterm and wraps the compilation in a Maybe monad. --- src/lambda/lambda.lisp | 25 +++- src/lambda/package.lisp | 1 + src/lambda/trans.lisp | 212 ++++++++++++++++++++++++++++++++-- src/specs/lambda-printer.lisp | 1 + src/specs/lambda.lisp | 22 +++- src/specs/package.lisp | 5 + test/lambda-trans.lisp | 40 +++++++ 7 files changed, 290 insertions(+), 16 deletions(-) diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp index 6aaa3b896..8f0de2fba 100644 --- a/src/lambda/lambda.lisp +++ b/src/lambda/lambda.lisp @@ -65,6 +65,7 @@ to the codomain." ((typep f 'lamb) (mcadr (ttype rec))) ((typep f 'app) (hom-cod ctx (fun f))) ((typep f 'index) (mcadr (ttype rec))) + ((typep f 'err) (mcadr (ttype f))) (t (error "not a valid STLC exponential term"))))) (-> index-check (fixnum list) cat-obj) @@ -162,6 +163,7 @@ the context on the left as well. For more info check [LAMB][class]")) :ttype (hom-cod ctx fun))) ((index pos) (index pos :ttype (index-check pos ctx))) + ((err ttype) (err ttype)) ((case-on on ltm rtm) (let* ((ann-on (ann-term1 ctx on)) (type-of-on (ttype ann-on)) @@ -227,7 +229,8 @@ occurences - re-annotates the term and its subterms with actual (mapcar #'ann-term2 term) :ttype (fun-to-hom (ttype tterm)))) ((index pos) (index pos - :ttype (fun-to-hom (ttype tterm)))))) + :ttype (fun-to-hom (ttype tterm)))) + ((err ttype) (err (fun-to-hom ttype))))) (defun annotated-term (ctx term) "Given a context consisting of a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] @@ -307,7 +310,25 @@ nil")) (and (check fun) (check (reduce #'pair term)))) (index t) - (unit t)))) + (unit t) + (err t)))) (let ((term (ignore-errors (ann-term1 ctx tterm)))) (and term (check term))))) + +(defun errorp (tterm) + "Evaluates to true iff the term has an error subterm." + (cond ((or (typep tterm 'index) + (typep tterm 'unit)) nil) + ((typep tterm 'err) t) + ((typep tterm 'case-on) (or (errorp (on tterm)) + (errorp (rtm tterm)) + (errorp (ltm tterm)))) + ((typep tterm 'pair) (or (errorp (ltm tterm)) + (errorp (rtm tterm)))) + ((typep tterm 'app) (or (errorp (fun tterm)) + (some #'identity + (mapcar + (lambda (x) (errorp x)) + (term tterm))))) + (t (errorp (term tterm))))) diff --git a/src/lambda/package.lisp b/src/lambda/package.lisp index fdb3a0889..bfd36b00a 100644 --- a/src/lambda/package.lisp +++ b/src/lambda/package.lisp @@ -26,6 +26,7 @@ (well-defp pax:generic-function) (fun-type pax:class) (fun-type pax:function) + (errorp pax:function) (mcar (pax:method () (fun-type))) (mcadr (pax:method () (fun-type))) diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp index b65f52553..d128e1ed2 100644 --- a/src/lambda/trans.lisp +++ b/src/lambda/trans.lisp @@ -47,6 +47,189 @@ calling me" (defmethod empty ((class (eql (find-class 'list)))) nil) (defmethod to-cat (context (tterm )) + "Compiles a checked term in said context to a Geb morphism. If the term has +an instance of an erorr term, wraps it in a Maybe monad, otherwise, compiles +according to the term model interpretation of STLC" + (if (errorp tterm) + (to-cat-err context tterm) + (to-cat-cor context tterm))) + +(defun maybe-comp (ob) + "Takes a [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with possible fun-type instances +and removes them" + (fun-to-hom (maybe ob))) + +(defun maybe-rest (ob) + "Takes a Geb object wrapped in Maybe and gives out the part without the +error node" + (mcadr (maybe-comp ob))) + +(defmethod to-cat-err (context (tterm )) + "Compiles a checked term with an error term in an appropriate context into the +morphism of the GEB category using a Maybe monad wrapper, that is, given a +context G and a term t of type A produces a morphism with domain +(stlc-ctx-maybe context) and codomain (maybe A). + +Terms come from [STLC][type] with occurences of [SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] +replaced by [FUN-TYPE][class] and should come without the slow of +[TTYPE][generic-function] accessor filled for any of the subterms. Context should +be a list of [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] with the caveat that instead of +[SO-HOM-OBJ][GEB.MAIN:SO-HOM-OBJ] we ought to use [FUN-TYPE][class], a stand-in +for the internal hom object with explicit accessors to the domain and the +codomain. Once again, note that it is important for the context and term to be +giving as per above description. While not always, not doing so result in an +error upon evaluation. As an example of a valid entry we have + +```lisp + (to-cat-err (list so1 (fun-type so1 so1)) (app (index 1) (list (error so1)))) +``` + +while + +```lisp +(to-cat-err (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (error so1)))) +``` + +produces an error. Error of such kind mind pop up both on the level of evaluating +[WELL-DEFP][generic-function] and [ANN-TERM1][generic-function]. + +Moreover, note that for terms whose typing needs addition of new context +we append contexts on the left rather than on the right contra usual type +theoretic notation for the convenience of computation. That means, e.g. that +asking for a type of a lambda term as below produces: + +```lisp +LAMBDA> (ttype (term (ann-term1 nil (lamb (list so1 so0) (index 0))))) +s-1 +``` + +as we count indeces from the left of the context while appending new types to +the context on the left as well. For more info check [LAMB][class] + +Note that the Maybe wrapper also applies to the context elements due to +functoriality concerns. Hence if one wanted to check the whether the term +(case-on (index 0) (err so1) (unit)) with a bool in contexts fails on the +left entry, one would need to evaluate + +```lisp +LAMBDA> (gapply (to-cat (list (coprod so1 so1)) + (case-on (index 0) + (err so1) + (unit))) + (list (geb:right (geb:left (geb:right so1))) so1)) +(left s-1) +``` + +and hence get an error part of the wrapper. While evaluating the right branch +will be done by: + +```lisp + LAMBDA> (gapply (to-cat (list (coprod so1 so1)) + (case-on (index 0) + (err so1) + (unit))) + (list (geb:right (geb:right (geb:right so1))) so1)) +(right s-1) +``` + +This follows from the fact that bool arapped in maybe is 1 + (bool + bool)" + (labels ((rec (context tterm) + (match-of stlc tterm + ((absurd tcod term) + (comp (mcase (->left so1 (maybe-rest tcod)) + (init (maybe-comp tcod))) + (rec context term))) + (unit + (comp (->right so1 so1) + (terminal (stlc-ctx-maybe context)))) + ((left rty term) + (comp (->right so1 (maybe-rest (ttype tterm))) + (comp (->left (maybe-comp (ttype term)) + (maybe-comp rty)) + (rec context term)))) + ((right lty term) + (comp (->right so1 (maybe-rest (ttype tterm))) + (comp (->right (maybe-comp lty) + (maybe-comp (ttype term))) + (rec context term)))) + ((case-on on ltm rtm) + (let ((mcartoon (mcar (ttype on))) + (mcadrtoon (mcadr (ttype on))) + (ctx (stlc-ctx-maybe context))) + (comp (mcase (comp (->left so1 (maybe-rest (ttype tterm))) + (terminal (prod ctx so1))) + (comp (mcase (commutes-left + (rec + (cons mcartoon + context) + ltm)) + (commutes-left + (rec + (cons mcadrtoon + context) + rtm))) + (distribute ctx + (maybe-comp mcartoon) + (maybe-comp mcadrtoon)))) + (comp (distribute ctx + so1 + (maybe-rest (coprod mcartoon + mcadrtoon))) + (geb:pair ctx (rec context on)))))) + ((pair ltm rtm) + (let ((lty (ttype ltm)) + (rty (ttype rtm))) + (comp (->right so1 (prod (maybe-comp lty) + (maybe-comp rty))) + (geb:pair (rec context ltm) + (rec context rtm))))) + ((fst term) + (let ((mcarttot (mcar (ttype term)))) + (comp (mcase (->left so1 (maybe-rest mcarttot)) + (<-left (maybe-comp mcarttot) + (maybe (mcadr (ttype term))))) + (rec context term)))) + ((snd term) + (let ((mcadrttot (mcadr (ttype term)))) + (comp (mcase (->left so1 (maybe-rest mcadrttot)) + (<-right (maybe-comp (mcar (ttype term))) + (maybe-comp mcadrttot))) + (rec context term)))) + ((lamb tdom term) + (comp (->right so1 (maybe-rest (fun-to-hom (ttype tterm)))) + (apply-n (length tdom) + #'(lambda (x) (curry (commutes-left x))) + (rec (append + (mapcar #'maybe-comp tdom) + context) term)))) + ((app fun term) + (let ((tofun (ttype fun))) + (comp + (mcase (->left so1 (maybe-rest tofun)) + (commutes-left + (so-eval (maybe-comp (mcar tofun)) + (maybe-comp (mcadr tofun))))) + (comp (distribute (reduce #'prod + (mapcar #'maybe-comp term) + :from-end t) + so1 + (maybe-rest tofun)) + (geb:pair (reduce #'geb:pair + (mapcar #'(lambda (x) (rec context x)) term) + :from-end t) + (rec context + fun)))))) + ((index pos) + (stlc-ctx-proj (mapcar #'maybe context) pos)) + ((err ttype) + (comp (->left so1 (maybe-comp ttype)) + (terminal (stlc-ctx-maybe context))))))) + (if (not (well-defp context tterm)) + (error "not a well-defined ~A in said ~A" tterm context) + (rec context (ann-term1 context tterm))))) + + +(defmethod to-cat-cor (context (tterm )) "Compiles a checked term in an appropriate context into the morphism of the GEB category. In detail, it takes a context and a term with following restrictions: Terms come from [STLC][type] with occurences of @@ -61,13 +244,13 @@ always, not doing so result in an error upon evaluation. As an example of a valid entry we have ```lisp - (to-cat (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0)))) + (to-cat-cor (list so1 (fun-type so1 so1)) (app (index 1) (list (index 0)))) ``` while ```lisp -(to-cat (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) +(to-cat-cor (list so1 (so-hom-obj so1 so1)) (app (index 1) (list (index 0)))) ``` produces an error. Error of such kind mind pop up both on the level of evaluating @@ -87,7 +270,7 @@ as we count indeces from the left of the context while appending new types to the context on the left as well. For more info check [LAMB][class] Finally, note that the compilation uncurries the final morphism. That is, -if the type of the term is an exponential object, [TO-CAT] uncurries the +if the type of the term is an exponential object, [TO-CAT-COR] uncurries the morphism in the Geb category instead producing a morphism into the domain of the exponential from a corresponding product. If the exponential is iterated, so is the uncurrying." @@ -98,14 +281,12 @@ iterated, so is the uncurrying." (rec context term))) (unit (terminal (stlc-ctx-to-mu context))) - ((left term) - (let ((tott (ttype tterm))) - (comp (->left (mcar tott) (mcadr tott)) - (rec context term)))) - ((right term) - (let ((tott (ttype tterm))) - (comp (->right (mcar tott) (mcadr tott)) - (rec context term)))) + ((left rty term) + (comp (->left (ttype term) rty) + (rec context term))) + ((right lty term) + (comp (->right lty (ttype term)) + (rec context term))) ((case-on on ltm rtm) (let ((mcartoon (mcar (ttype on))) (mcadrtoon (mcadr (ttype on))) @@ -141,7 +322,9 @@ iterated, so is the uncurrying." (mapcar #'(lambda (x) (rec context x)) term) :from-end t))))) ((index pos) - (stlc-ctx-proj context pos))))) + (stlc-ctx-proj context pos)) + (err + (error "Not meant for the compiler"))))) (cond ((not (well-defp context tterm)) (error "not a well-defined ~A in said ~A" tterm context)) ((typep (type-of-term-w-fun context tterm) 'fun-type) @@ -218,6 +401,11 @@ LAMBDA> (stlc-ctx-to-mu (list so1 (fun-to-hom (fun-type geb-bool:bool geb-bool:b ```" (mvfoldr #'prod (mapcar #'fun-to-hom context) so1)) +(defun stlc-ctx-maybe (context) + "Takes a context seen as product of appropriate [SUBSTOBJ][GEB.SPEC:SUBSTOBJ] +and iteratively applies Maybe to its elements." + (mvfoldr #'prod (mapcar (lambda (x) (maybe-comp x)) context) so1)) + (-> so-hom (substobj substobj) (or t substobj)) (defun so-hom (dom cod) "Computes the hom-object of two [SUBSTMORPH]s" diff --git a/src/specs/lambda-printer.lisp b/src/specs/lambda-printer.lisp index 53202022f..fdc1b71bb 100644 --- a/src/specs/lambda-printer.lisp +++ b/src/specs/lambda-printer.lisp @@ -17,3 +17,4 @@ (easy-printer lamb) (easy-printer app) (easy-printer index) +(easy-printer err) diff --git a/src/specs/lambda.lisp b/src/specs/lambda.lisp index 1b0a3d3e9..1259fb390 100644 --- a/src/specs/lambda.lisp +++ b/src/specs/lambda.lisp @@ -10,8 +10,7 @@ unit types as well as coproduct, product, and function types.")) "Type of untyped terms of [STLC][type]. Each class of a term has a slot for a type, which can be filled by auxillary functions or by user. Types are represented as [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]." - '(or absurd unit left right case-on pair fst snd lamb app index)) - + '(or absurd unit left right case-on pair fst snd lamb app index err)) ;; New defgenerics @@ -537,4 +536,23 @@ type-theoretic notation.")) (values (make-instance 'index :pos pos :ttype ttype))) +(defclass err () + ((ttype :initarg :ttype + :initform nil + :accessor ttype + :documentation "")) + (:documentation + "An error term of a type supplied by the user. The formal grammar of +[ERR][class] is +```lisp +(err ttype) +``` +The intended semantics are as follows: [ERR][class] represents an error node +currently having no particular feedback but with functionality to be of an +arbitrary type. Note that this is the only STLC term class which does not +have [TTYPE][generic-function] a possibly empty accessor.")) +(-> err (cat-obj) err) +(defun err (ttype) + (values + (make-instance 'err :ttype ttype))) diff --git a/src/specs/package.lisp b/src/specs/package.lisp index fdf43a74c..b1e060dd5 100644 --- a/src/specs/package.lisp +++ b/src/specs/package.lisp @@ -158,6 +158,7 @@ constructors" (lamb pax:class) (app pax:class) (index pax:class) + (err pax:class) (absurd pax:function) (unit pax:function) @@ -170,6 +171,7 @@ constructors" (lamb pax:function) (app pax:function) (index pax:function) + (err pax:function) "Accessors of [ABSURD][class]" @@ -223,6 +225,9 @@ constructors" (pos (pax:method () (index))) (ttype (pax:method () (index))) + "Accessors of [ERR][class]" + (ttype (pax:method () (err))) + (tcod pax:generic-function) (tdom pax:generic-function) (term pax:generic-function) diff --git a/test/lambda-trans.lisp b/test/lambda-trans.lisp index 8029514ff..78ecef022 100644 --- a/test/lambda-trans.lisp +++ b/test/lambda-trans.lisp @@ -37,6 +37,26 @@ (def bool-id (lambda:lamb (list (coprod so1 so1)) (geb.lambda:index 0))) +(def case-error-left + (lambda:case-on (lambda:left so1 (lambda:unit)) + (lambda:err so1) + (lambda:unit))) + +(def case-error-right + (lambda:case-on (lambda:left so1 (lambda:unit)) + (lambda:unit) + (lambda:err so1))) + +(def case-error-top + (lambda:case-on (lambda:err (coprod so1 so1)) + (lambda:unit) + (lambda:unit))) + +(def context-dependent-case + (lambda:case-on (lambda:index 0) + (lambda:err so1) + (lambda:unit))) + (def issue-58-circuit (to-circuit (lambda:case-on @@ -103,6 +123,26 @@ (is equalp #*0 (gapply (to-bitc proper-not) #*1)) (is equalp #*1 (gapply (to-bitc proper-not) #*0))) +(define-test error-handling-case :parent lambda.trans-eval + (is obj-equalp (left so1) (gapply (to-cat nil case-error-left) + (list so1))) + (is obj-equalp (right so1) (gapply (to-cat nil case-error-right) + (list so1))) + (is obj-equalp (left so1) (gapply (to-cat nil case-error-top) + (list so1))) + (is obj-equalp (left so1) (gapply (to-cat (list (coprod so1 so1)) + context-dependent-case) + (list (right + (left + (right so1))) + so1))) + (is obj-equalp (right so1) (gapply (to-cat (list (coprod so1 so1)) + context-dependent-case) + (list (right + (right + (right so1))) + so1)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Compile checked term tests ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;