Skip to content

Commit

Permalink
STLC to Geb Compilation Fix
Browse files Browse the repository at this point in the history 
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
  • Loading branch information
@agureev @mariari
agureev authored and mariari committed May 30, 2023
1 parent 3094c41 commit db3d2bc
Show file tree
Hide file tree
Showing 2 changed files with 144 additions and 26 deletions.
126 changes: 103 additions & 23 deletions src/lambda/trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)))
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
44 changes: 41 additions & 3 deletions test/lambda-trans.lisp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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 ;;
Expand Down Expand Up @@ -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 ;;
Expand Down Expand Up @@ -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)))

0 comments on commit db3d2bc

Please sign in to comment.