Std.Foundation

1module Std.Foundation
2
3-- Foundation of the standard library (Language Platform PRD §28.2, LP-800):
4-- booleans, ordering, optional values, results, pairs, and equality helpers.
5-- Every type here is an ordinary checked family: the trusted core stays small
6-- and usability comes from the library (§28.1).
7-- A decision. Distinct from Nat so a decision cannot be mistaken for a count.
8family StdBool : Type 0
9constructor StdTrue
10constructor StdFalse
11
12end-family
13
14-- The result of comparing two values.
15family StdOrder : Type 0
16constructor StdLess
17constructor StdEqual
18constructor StdGreater
19
20end-family
21
22-- A value that may be absent. The parameter is the value's type, so
23-- `StdOption` is one family used at every element type rather than one family
24-- per type.
25family StdOption : Type 0
26parameter erased stdOptionElement : Type 0
27constructor StdNone
28constructor StdSome
29field unrestricted stdSomeValue : stdOptionElement
30
31end-family
32
33-- Either an error or a value. The error type is a parameter too, so a caller
34-- chooses how rich its errors are.
35family StdResult : Type 0
36parameter erased stdResultError : Type 0
37parameter erased stdResultValue : Type 0
38constructor StdFailure
39field unrestricted stdFailureError : stdResultError
40constructor StdSuccess
41field unrestricted stdSuccessValue : stdResultValue
42
43end-family
44
45-- An ordinary pair. The dependent pair is `sigma` in the core; this is the
46-- non-dependent case, which is what most library code wants.
47family StdPair : Type 0
48parameter erased stdPairLeftType : Type 0
49parameter erased stdPairRightType : Type 0
50constructor StdPairOf
51field unrestricted stdPairLeft : stdPairLeftType
52field unrestricted stdPairRight : stdPairRightType
53
54end-family
55
56-- Negation.
57def stdBoolNot =
58  (lambda unrestricted value : (family StdBool) .
59    (eliminate
60      StdBool
61      (lambda unrestricted current : (family StdBool) . (family StdBool))
62      value
63      (branch StdTrue . (constructor StdBool StdFalse))
64      (branch StdFalse . (constructor StdBool StdTrue))))
65
66-- Conjunction, evaluating both arguments (there is no short-circuiting to
67-- observe: the language is total).
68def stdBoolAnd =
69  (lambda unrestricted left : (family StdBool) .
70    (lambda unrestricted right : (family StdBool) .
71      (eliminate
72        StdBool
73        (lambda unrestricted current : (family StdBool) . (family StdBool))
74        left
75        (branch StdTrue . right)
76        (branch StdFalse . (constructor StdBool StdFalse)))))
77
78-- Disjunction.
79def stdBoolOr =
80  (lambda unrestricted left : (family StdBool) .
81    (lambda unrestricted right : (family StdBool) .
82      (eliminate
83        StdBool
84        (lambda unrestricted current : (family StdBool) . (family StdBool))
85        left
86        (branch StdTrue . (constructor StdBool StdTrue))
87        (branch StdFalse . right))))
88
89-- Exclusive disjunction.
90def stdBoolExclusiveOr =
91  (lambda unrestricted left : (family StdBool) .
92    (lambda unrestricted right : (family StdBool) .
93      (eliminate
94        StdBool
95        (lambda unrestricted current : (family StdBool) . (family StdBool))
96        left
97        (branch StdTrue . (stdBoolNot right))
98        (branch StdFalse . right))))
99
100-- The remaining binary Boolean functions. Together with `stdBoolAnd`,
101-- `stdBoolExclusiveOr`, and `stdBoolOr`, these name all sixteen possible
102-- truth tables over two decisions; callers never need to encode a table as a
103-- numeric flag or duplicate the logic in another package.
104def stdBoolFalse =
105  (lambda unrestricted left : (family StdBool) .
106    (lambda unrestricted right : (family StdBool) . (constructor StdBool StdFalse)))
107
108def stdBoolLeftAndNotRight =
109  (lambda unrestricted left : (family StdBool) .
110    (lambda unrestricted right : (family StdBool) . (stdBoolAnd left (stdBoolNot right))))
111
112def stdBoolLeft =
113  (lambda unrestricted left : (family StdBool) .
114    (lambda unrestricted right : (family StdBool) . left))
115
116def stdBoolNotLeftAndRight =
117  (lambda unrestricted left : (family StdBool) .
118    (lambda unrestricted right : (family StdBool) . (stdBoolAnd (stdBoolNot left) right)))
119
120def stdBoolRight =
121  (lambda unrestricted left : (family StdBool) .
122    (lambda unrestricted right : (family StdBool) . right))
123
124def stdBoolNor =
125  (lambda unrestricted left : (family StdBool) .
126    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolOr left right))))
127
128def stdBoolEquivalent =
129  (lambda unrestricted left : (family StdBool) .
130    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolExclusiveOr left right))))
131
132def stdBoolNotRight =
133  (lambda unrestricted left : (family StdBool) .
134    (lambda unrestricted right : (family StdBool) . (stdBoolNot right)))
135
136def stdBoolLeftOrNotRight =
137  (lambda unrestricted left : (family StdBool) .
138    (lambda unrestricted right : (family StdBool) . (stdBoolOr left (stdBoolNot right))))
139
140def stdBoolNotLeft =
141  (lambda unrestricted left : (family StdBool) .
142    (lambda unrestricted right : (family StdBool) . (stdBoolNot left)))
143
144def stdBoolNotLeftOrRight =
145  (lambda unrestricted left : (family StdBool) .
146    (lambda unrestricted right : (family StdBool) . (stdBoolOr (stdBoolNot left) right)))
147
148def stdBoolNand =
149  (lambda unrestricted left : (family StdBool) .
150    (lambda unrestricted right : (family StdBool) . (stdBoolNot (stdBoolAnd left right))))
151
152def stdBoolTrue =
153  (lambda unrestricted left : (family StdBool) .
154    (lambda unrestricted right : (family StdBool) . (constructor StdBool StdTrue)))
155
156-- A decision as a natural: zero is false, one is true. The conversion is
157-- explicit, so a count is never treated as a decision by accident.
158def stdBoolToNatural =
159  (lambda unrestricted value : (family StdBool) .
160    (eliminate
161      StdBool
162      (lambda unrestricted current : (family StdBool) . Nat)
163      value
164      (branch StdTrue . (succ zero))
165      (branch StdFalse . zero)))
166
167-- Zero is false, every other natural is true.
168def stdBoolFromNatural =
169  (lambda unrestricted value : Nat .
170    (nat-eliminate
171      (lambda unrestricted current : Nat . (family StdBool))
172      (constructor StdBool StdFalse)
173      (lambda unrestricted predecessor : Nat .
174        (lambda unrestricted induction : (family StdBool) . (constructor StdBool StdTrue)))
175      value))
176
177-- The opposite comparison: what `stdOrderCompare y x` would say.
178def stdOrderReverse =
179  (lambda unrestricted value : (family StdOrder) .
180    (eliminate
181      StdOrder
182      (lambda unrestricted current : (family StdOrder) . (family StdOrder))
183      value
184      (branch StdLess . (constructor StdOrder StdGreater))
185      (branch StdEqual . (constructor StdOrder StdEqual))
186      (branch StdGreater . (constructor StdOrder StdLess))))
187
188-- Is this comparison equality?
189def stdOrderIsEqual =
190  (lambda unrestricted value : (family StdOrder) .
191    (eliminate
192      StdOrder
193      (lambda unrestricted current : (family StdOrder) . (family StdBool))
194      value
195      (branch StdLess . (constructor StdBool StdFalse))
196      (branch StdEqual . (constructor StdBool StdTrue))
197      (branch StdGreater . (constructor StdBool StdFalse))))
198
199-- Is the left value the smaller one?
200def stdOrderIsLess =
201  (lambda unrestricted value : (family StdOrder) .
202    (eliminate
203      StdOrder
204      (lambda unrestricted current : (family StdOrder) . (family StdBool))
205      value
206      (branch StdLess . (constructor StdBool StdTrue))
207      (branch StdEqual . (constructor StdBool StdFalse))
208      (branch StdGreater . (constructor StdBool StdFalse))))
209
210-- Compare two naturals, answering with an order rather than a flag.
211def stdOrderCompareNatural =
212  (lambda unrestricted left : Nat .
213    (lambda unrestricted right : Nat .
214      (eliminate
215        StdBool
216        (lambda unrestricted current : (family StdBool) . (family StdOrder))
217        (stdBoolFromNatural (nat-less-than left right))
218        (branch StdTrue . (constructor StdOrder StdLess))
219        (branch
220          StdFalse
221          .
222          (eliminate
223            StdBool
224            (lambda unrestricted current : (family StdBool) . (family StdOrder))
225            (stdBoolFromNatural (nat-less-than right left))
226            (branch StdTrue . (constructor StdOrder StdGreater))
227            (branch StdFalse . (constructor StdOrder StdEqual)))))))
228
229-- The value an option holds, or the supplied default. The element type is
230-- explicit, because the library never guesses a type.
231def stdOptionValueOr =
232  (lambda erased element : Type 0 .
233    (lambda unrestricted fallback : element .
234      (lambda unrestricted value : (family StdOption element) .
235        (eliminate
236          StdOption
237          (lambda unrestricted current : (family StdOption element) . element)
238          value
239          (branch StdNone . fallback)
240          (branch StdSome held . held)))))
241
242-- Does this option hold a value?
243def stdOptionIsSome =
244  (lambda erased element : Type 0 .
245    (lambda unrestricted value : (family StdOption element) .
246      (eliminate
247        StdOption
248        (lambda unrestricted current : (family StdOption element) . (family StdBool))
249        value
250        (branch StdNone . (constructor StdBool StdFalse))
251        (branch StdSome held . (constructor StdBool StdTrue)))))
252
253-- The value a result holds, or the supplied default.
254def stdResultValueOr =
255  (lambda erased errorType : Type 0 .
256    (lambda erased valueType : Type 0 .
257      (lambda unrestricted fallback : valueType .
258        (lambda unrestricted value : (family StdResult errorType valueType) .
259          (eliminate
260            StdResult
261            (lambda unrestricted current : (family StdResult errorType valueType) . valueType)
262            value
263            (branch StdFailure held . fallback)
264            (branch StdSuccess held . held))))))
265
266-- Did this result succeed?
267def stdResultIsSuccess =
268  (lambda erased errorType : Type 0 .
269    (lambda erased valueType : Type 0 .
270      (lambda unrestricted value : (family StdResult errorType valueType) .
271        (eliminate
272          StdResult
273          (lambda unrestricted current : (family StdResult errorType valueType) . (family StdBool))
274          value
275          (branch StdFailure held . (constructor StdBool StdFalse))
276          (branch StdSuccess held . (constructor StdBool StdTrue))))))
277
278-- Compose checked operations without replacing an earlier error with a later
279-- default. The continuation receives a value only in the success branch.
280def stdResultBind =
281  (lambda erased errorType : Type 0 .
282    (lambda erased inputType : Type 0 .
283      (lambda erased outputType : Type 0 .
284        (lambda unrestricted input : (family StdResult errorType inputType) .
285          (lambda unrestricted next : (pi unrestricted value : inputType . (family StdResult errorType outputType)) .
286            (eliminate StdResult
287              (lambda unrestricted current : (family StdResult errorType inputType) . (family StdResult errorType outputType)) input
288              (branch StdFailure error . (constructor StdResult StdFailure errorType outputType error))
289              (branch StdSuccess value . (next value))))))))
290
291-- A result as an option, dropping the error.
292def stdResultToOption =
293  (lambda erased errorType : Type 0 .
294    (lambda erased valueType : Type 0 .
295      (lambda unrestricted value : (family StdResult errorType valueType) .
296        (eliminate
297          StdResult
298          (lambda unrestricted current : (family StdResult errorType valueType) .
299            (family StdOption valueType))
300          value
301          (branch StdFailure held . (constructor StdOption StdNone valueType))
302          (branch StdSuccess held . (constructor StdOption StdSome valueType held))))))
303
304-- The left component of a pair.
305def stdPairLeftOf =
306  (lambda erased leftType : Type 0 .
307    (lambda erased rightType : Type 0 .
308      (lambda unrestricted value : (family StdPair leftType rightType) .
309        (eliminate
310          StdPair
311          (lambda unrestricted current : (family StdPair leftType rightType) . leftType)
312          value
313          (branch StdPairOf left right . left)))))
314
315-- The right component of a pair.
316def stdPairRightOf =
317  (lambda erased leftType : Type 0 .
318    (lambda erased rightType : Type 0 .
319      (lambda unrestricted value : (family StdPair leftType rightType) .
320        (eliminate
321          StdPair
322          (lambda unrestricted current : (family StdPair leftType rightType) . rightType)
323          value
324          (branch StdPairOf left right . right)))))
325
326-- Equality is reflexive by construction: this is the proof that a value
327-- equals itself, named so library code can pass it around.
328def stdEqualReflexive =
329  (lambda erased element : Type 0 . (lambda unrestricted value : element . (refl element value)))