1module Compiler.NaturalOperation
2
3-- Shared syntax/Core operation vocabulary; no dependency on either tree.
4family CoreNaturalOperation : Type 0
5constructor CoreNaturalAdd
6constructor CoreNaturalSubtract
7constructor CoreNaturalMultiply
8constructor CoreNaturalDivide
9constructor CoreNaturalModulo
10
11end-family
12
13family NaturalOperationLookup : Type 0
14constructor NaturalOperationFound
15field unrestricted foundNaturalOperation : (family CoreNaturalOperation)
16constructor NaturalOperationMissing
17
18end-family
19
20def naturalOperationCode =
21 (lambda unrestricted operation : (family CoreNaturalOperation) .
22 (eliminate
23 CoreNaturalOperation
24 (lambda unrestricted value : (family CoreNaturalOperation) . Byte)
25 operation
26 (branch CoreNaturalAdd . (byte 0))
27 (branch CoreNaturalSubtract . (byte 1))
28 (branch CoreNaturalMultiply . (byte 2))
29 (branch CoreNaturalDivide . (byte 3))
30 (branch CoreNaturalModulo . (byte 4))))
31
32def lookupNaturalOperation =
33 (lambda unrestricted input : Bytes .
34 (app
35 (nat-eliminate
36 (lambda unrestricted flag : Nat .
37 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
38 (lambda unrestricted force : Nat .
39 (app
40 (nat-eliminate
41 (lambda unrestricted flag : Nat .
42 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
43 (lambda unrestricted force : Nat .
44 (app
45 (nat-eliminate
46 (lambda unrestricted flag : Nat .
47 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
48 (lambda unrestricted force : Nat .
49 (app
50 (nat-eliminate
51 (lambda unrestricted flag : Nat .
52 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
53 (lambda unrestricted force : Nat .
54 (app
55 (nat-eliminate
56 (lambda unrestricted flag : Nat .
57 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
58 (lambda unrestricted force : Nat .
59 (constructor NaturalOperationLookup NaturalOperationMissing))
60 (lambda unrestricted predecessor : Nat .
61 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
62 (lambda unrestricted force : Nat .
63 (constructor
64 NaturalOperationLookup
65 NaturalOperationFound
66 (constructor CoreNaturalOperation CoreNaturalModulo)))))
67 (bytes-equal input b"nat-modulo"))
68 zero))
69 (lambda unrestricted predecessor : Nat .
70 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
71 (lambda unrestricted force : Nat .
72 (constructor
73 NaturalOperationLookup
74 NaturalOperationFound
75 (constructor CoreNaturalOperation CoreNaturalDivide)))))
76 (bytes-equal input b"nat-divide"))
77 zero))
78 (lambda unrestricted predecessor : Nat .
79 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
80 (lambda unrestricted force : Nat .
81 (constructor
82 NaturalOperationLookup
83 NaturalOperationFound
84 (constructor CoreNaturalOperation CoreNaturalMultiply)))))
85 (bytes-equal input b"nat-multiply"))
86 zero))
87 (lambda unrestricted predecessor : Nat .
88 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
89 (lambda unrestricted force : Nat .
90 (constructor
91 NaturalOperationLookup
92 NaturalOperationFound
93 (constructor CoreNaturalOperation CoreNaturalSubtract)))))
94 (bytes-equal input b"nat-subtract"))
95 zero))
96 (lambda unrestricted predecessor : Nat .
97 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
98 (lambda unrestricted force : Nat .
99 (constructor
100 NaturalOperationLookup
101 NaturalOperationFound
102 (constructor CoreNaturalOperation CoreNaturalAdd)))))
103 (bytes-equal input b"nat-add"))
104 zero))
105
106def decodeNaturalOperation =
107 (lambda unrestricted input : Byte .
108 (app
109 (nat-eliminate
110 (lambda unrestricted flag : Nat .
111 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
112 (lambda unrestricted force : Nat .
113 (app
114 (nat-eliminate
115 (lambda unrestricted flag : Nat .
116 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
117 (lambda unrestricted force : Nat .
118 (app
119 (nat-eliminate
120 (lambda unrestricted flag : Nat .
121 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
122 (lambda unrestricted force : Nat .
123 (app
124 (nat-eliminate
125 (lambda unrestricted flag : Nat .
126 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
127 (lambda unrestricted force : Nat .
128 (app
129 (nat-eliminate
130 (lambda unrestricted flag : Nat .
131 (pi unrestricted force : Nat . (family NaturalOperationLookup)))
132 (lambda unrestricted force : Nat .
133 (constructor NaturalOperationLookup NaturalOperationMissing))
134 (lambda unrestricted predecessor : Nat .
135 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
136 (lambda unrestricted force : Nat .
137 (constructor
138 NaturalOperationLookup
139 NaturalOperationFound
140 (constructor CoreNaturalOperation CoreNaturalModulo)))))
141 (byte-equal input (byte 4)))
142 zero))
143 (lambda unrestricted predecessor : Nat .
144 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
145 (lambda unrestricted force : Nat .
146 (constructor
147 NaturalOperationLookup
148 NaturalOperationFound
149 (constructor CoreNaturalOperation CoreNaturalDivide)))))
150 (byte-equal input (byte 3)))
151 zero))
152 (lambda unrestricted predecessor : Nat .
153 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
154 (lambda unrestricted force : Nat .
155 (constructor
156 NaturalOperationLookup
157 NaturalOperationFound
158 (constructor CoreNaturalOperation CoreNaturalMultiply)))))
159 (byte-equal input (byte 2)))
160 zero))
161 (lambda unrestricted predecessor : Nat .
162 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
163 (lambda unrestricted force : Nat .
164 (constructor
165 NaturalOperationLookup
166 NaturalOperationFound
167 (constructor CoreNaturalOperation CoreNaturalSubtract)))))
168 (byte-equal input (byte 1)))
169 zero))
170 (lambda unrestricted predecessor : Nat .
171 (lambda unrestricted induction : (pi unrestricted force : Nat . (family NaturalOperationLookup)) .
172 (lambda unrestricted force : Nat .
173 (constructor
174 NaturalOperationLookup
175 NaturalOperationFound
176 (constructor CoreNaturalOperation CoreNaturalAdd)))))
177 (byte-equal input (byte 0)))
178 zero))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.