blob: ba409a8e37e83ea7c43351bb37a17f88b4393191 (
plain)
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
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
module Term.Compile
import public Text.PrettyPrint.Prettyprinter
import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.Stream
import Data.String
import Term
import Term.Pretty
import Term.Syntax
%prefix_record_projections off
const_ : Doc ann
const_ = "squid-const"
rec_ : Doc ann
rec_ = "squid-rec"
identity_ : Doc ann
identity_ = "squid-identity"
underscore : Doc ann
underscore = "_"
plus : Doc ann
plus = "+"
lambda : Doc ann
lambda = "lambda"
lit : Nat -> Doc ann
lit = pretty
compileOp : Operator tys ty -> Doc ann
compileOp (Lit n) = lit n
compileOp Suc = "1+"
compileOp Plus = "squid-plus"
compileOp Mult = "squid-mult"
compileOp Pred = "1-" -- Confusing name, but correct
compileOp Minus = "squid-minus"
compileOp Div = "squid-div"
compileOp Mod = "squid-mod"
compileOp (Inl _ _) = identity_
compileOp (Inr _ _) = identity_
compileOp (Prl _ _) = identity_
compileOp (Prr _ _) = identity_
parameters (names : Stream String)
compileFullTerm : (len : Len ctx) => FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc ann
compileFullTerm Var thin =
pretty $ index (minus (lenToNat len) (S $ elemToNat $ index thin Here)) names
compileFullTerm (Const t) thin =
parens $ group $ hang 2 $
const_ <+> line <+>
compileFullTerm t thin
compileFullTerm (Abs Var) thin = identity_
compileFullTerm (Abs t) thin =
parens $ group $ hang 2 $
lambda <++> (parens $ pretty $ index (lenToNat len) names) <+> line <+>
compileFullTerm t (Keep thin)
compileFullTerm (App (MakePair (Const t `Over` thin1) (u `Over` thin2) _)) thin =
compileFullTerm t (thin . thin1)
compileFullTerm (App (MakePair (Abs Var `Over` thin1) (u `Over` thin2) _)) thin =
compileFullTerm u (thin . thin2)
compileFullTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
parens $ group $ align $
compileFullTerm t (thin . thin1) <+> line <+>
compileFullTerm u (thin . thin2)
compileFullTerm (Op op) thin = compileOp op
compileFullTerm
(Rec (MakePair
(t `Over` thin1)
(MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin') _))
thin =
parens $ group $ hang 2 $
rec_ <++> compileFullTerm t (thin . thin1) <+> line <+>
compileFullTerm u (thin . thin' . thin2) <+> line <+>
compileFullTerm v (thin . thin' . thin3)
finToChar : Fin 26 -> Char
finToChar 0 = 'x'
finToChar 1 = 'y'
finToChar 2 = 'z'
finToChar 3 = 'a'
finToChar 4 = 'b'
finToChar 5 = 'c'
finToChar 6 = 'd'
finToChar 7 = 'e'
finToChar 8 = 'f'
finToChar 9 = 'g'
finToChar 10 = 'h'
finToChar 11 = 'i'
finToChar 12 = 'j'
finToChar 13 = 'k'
finToChar 14 = 'l'
finToChar 15 = 'm'
finToChar 16 = 'n'
finToChar 17 = 'o'
finToChar 18 = 'p'
finToChar 19 = 'q'
finToChar 20 = 'r'
finToChar 21 = 's'
finToChar 22 = 't'
finToChar 23 = 'u'
finToChar 24 = 'v'
finToChar 25 = 'w'
name : Nat -> List Char
name k =
case divMod k 26 of
Fraction k 26 0 r prf => [finToChar r]
Fraction k 26 (S q) r prf => finToChar r :: name (assert_smaller k q)
public export
data ProfileMode = Run | Profile
builtins : String
builtins = """
(define-module (squid-module)
#:use-module (statprof)
#:declarative? #t)
(define (squid-rec n z s)
(let loop ((k 0) (acc z))
(if (= k n)
acc
(loop (1+ k) (s acc)))))
(define (squid-plus m) (lambda (n) (+ m n)))
(define (squid-mult m) (lambda (n) (* m n)))
(define (squid-minus m) (lambda (n) (- m n)))
(define (squid-div m) (lambda (n) (euclidean-quotient m n)))
(define (squid-mod m) (lambda (n) (euclidean-remainder m n)))
(define (squid-identity x) x)
(define (squid-const x) (lambda (_) x))
"""
wrap_main : Len ctx => Term ty ctx -> Doc ann
wrap_main t =
parens $ group $ hang 2 $
"define (squid-main)" <+> line <+>
compileFullTerm canonicalNames t.value t.thin
run_main : ProfileMode -> String
run_main Run = """
(display (squid-main))
(newline)
"""
run_main Profile = """
(statprof squid-main)
"""
export
compileTerm : Len ctx => ProfileMode -> Term ty ctx -> Doc ann
compileTerm mode t =
pretty builtins <+> hardline <+> hardline <+>
wrap_main t <+> hardline <+> hardline <+>
pretty (run_main mode)
|
