blob: c7b5e9b99a5ec4daacf0be26b9df134c33a0d001 (
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
|
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.Syntax
%prefix_record_projections off
rec_ : Doc ann
rec_ = "my-rec"
underscore : Doc ann
underscore = "_"
plus : Doc ann
plus = "+"
lambda : Doc ann
lambda = "lambda"
lit : Nat -> Doc ann
lit = pretty
getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx))
getSucs (Lit n) = (n, Nothing)
getSucs (Suc t) = mapFst S (getSucs t)
getSucs t = (0, Just t)
public export
data Len : SnocList a -> Type where
Z : Len [<]
S : Len sx -> Len (sx :< a)
%name Len k
lenToNat : Len sx -> Nat
lenToNat Z = 0
lenToNat (S k) = S (lenToNat k)
extend : sx `Thins` sy -> Len sz -> sx ++ sz `Thins` sy ++ sz
extend thin Z = thin
extend thin (S k) = Keep (extend thin k)
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 $
lambda <++> (parens $ underscore) <+> line <+>
compileFullTerm t thin
compileFullTerm (Abs t) thin =
parens $ group $ hang 2 $
lambda <++> (parens $ pretty $ index (lenToNat len) names) <+> line <+>
compileFullTerm t (Keep thin)
compileFullTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
parens $ group $ align $
compileFullTerm t (thin . thin1) <+> line <+>
compileFullTerm u (thin . thin2)
compileFullTerm (Lit n) thin = lit n
compileFullTerm t'@(Suc t) thin =
let (n, t) = getSucs t in
case t of
Just t =>
parens $ group $ align $
plus <++> lit (S n) <+> softline <+>
compileFullTerm (assert_smaller t' t) thin
Nothing => lit (S n)
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)
export
canonicalNames : Stream String
canonicalNames = map (fastPack . reverse . name) nats
public export
data ProfileMode = Run | Profile
builtin_rec : String
builtin_rec = """
(define (my-rec n z s)
(let loop ((k 0) (acc z))
(if (= k n)
acc
(loop (1+ k) (s acc)))))
"""
wrap_main : Len ctx => Term ty ctx -> Doc ann
wrap_main t =
parens $ group $ hang 2 $
"define (my-main)" <+> line <+>
compileFullTerm canonicalNames t.value t.thin
run_main : ProfileMode -> String
run_main Run = """
(display (my-main))
(newline)
"""
run_main Profile = """
(use-modules (statprof))
(statprof my-main)
"""
export
compileTerm : Len ctx => ProfileMode -> Term ty ctx -> Doc ann
compileTerm mode t =
pretty builtin_rec <+> hardline <+> hardline <+>
wrap_main t <+> hardline <+> hardline <+>
pretty (run_main mode)
|
