/
package.lisp
63 lines (48 loc) · 2.24 KB
/
package.lisp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(in-package :geb.utils)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; API module
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(geb.utils:muffle-package-variance
(uiop:define-package #:geb.lambda.main
(:documentation "A basic lambda calculus model")
(:mix #:geb.lambda.spec #:geb.common #:common-lisp)
(:reexport #:geb.lambda.spec)))
(in-package #:geb.lambda.main)
(pax:defsection @lambda-api (:title "Main functionality")
"This covers the main API for the STLC module")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; trans module
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package :geb.utils)
(geb.utils:muffle-package-variance
(uiop:define-package #:geb.lambda.trans
(:documentation "A basic lambda translator into other parts of geb")
(:shadow #:to-poly #:to-circuit)
(:mix #:geb.lambda.spec #:geb.common #:common-lisp :geb.lambda.main)))
(in-package #:geb.lambda.trans)
(pax:defsection @utility (:title "Utility Functionality")
"These are utility functions relating to translating lambda terms to other types"
(stlc-ctx-to-mu pax:function)
(so-hom pax:function))
(pax:defsection @stlc-conversion (:title "Transition Functions")
"These functions deal with transforming the data structure to other
data types"
(compile-checked-term pax:generic-function)
(to-poly pax:function)
(to-circuit pax:function)
(@utility pax:section))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; lambda module
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package :geb.utils)
(geb.utils:muffle-package-variance
(uiop:define-package #:geb.lambda
(:documentation "A basic lambda calculus model")
(:mix #:geb.lambda.spec #:geb.lambda.trans #:geb.common #:common-lisp)
(:use-reexport #:geb.lambda.spec #:geb.lambda.main #:geb.lambda.trans)))
(in-package #:geb.lambda)
(pax:defsection @stlc (:title "The Simply Typed Lambda Calculus model")
"This covers GEB's view on simply typed lambda calculus"
(@lambda-specs pax:section)
(@lambda-api pax:section)
(@stlc-conversion pax:section))