Skip to content

Commit

Permalink
Uncurry the Compilation to Geb
Browse files Browse the repository at this point in the history
Changes the compilation to Geb where lambda is interpreted in
uncurried form. Changes the function application term accordingly
  • Loading branch information
agureev committed May 4, 2023
1 parent 9fee3d3 commit e716b3f
Showing 1 changed file with 7 additions and 10 deletions.
17 changes: 7 additions & 10 deletions src/lambda/trans.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -85,17 +85,14 @@ produces an error. Error of such kind mind pop up both on the level of evaluatin
(comp (<-right (mcar tottt) (mcadr tottt))
(compile-checked-term context term))))
((lamb tdom term)
(curry (commutes-left
(rec (cons tdom context) term))))
(rec (append tdom context) term))
((app fun term)
(let ((tofun (ttype fun)))
(comp
(so-eval (fun-to-hom (mcar tofun))
(fun-to-hom (mcadr tofun)))
(geb:pair (rec context
fun)
(rec context
term)))))
(comp (rec context fun)
(reduce #'geb:pair
(append (mapcar (lambda (x) (rec context x))
term)
(stlc-ctx-to-mu context))
:from-end t)))
((index pos)
(stlc-ctx-proj context pos)))))
(let ((ann-term (ann-term1 context tterm)))
Expand Down

0 comments on commit e716b3f

Please sign in to comment.