Skip to content

Commit 67adbe8

Browse files
effectfullyeffectfully
authored
[Builtins] Allow casing on booleans and integers (#7029)
Added support for `Case`ing on booleans and integers. For example, `case True a b` now evaluates to `b`.
1 parent 8b2c2dc commit 67adbe8

File tree

478 files changed

+9094
-9059
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

478 files changed

+9094
-9059
lines changed

‎cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.cbor.size.golden

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
2140
1+
2090

‎cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.large.budget.golden

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 540852171, exBudgetMemory = ExMemory 2592918}
1+
ExBudget {exBudgetCPU = ExCPU 472550709, exBudgetMemory = ExMemory 2373780}

‎cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.pir.golden

Lines changed: 46 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -139,12 +139,12 @@ program
139139
!`$fOrdInteger_$ccompare` : integer -> integer -> Ordering
140140
= \(eta : integer) (eta : integer) ->
141141
Bool_match
142-
(ifThenElse {Bool} (equalsInteger eta eta) True False)
142+
(case Bool (equalsInteger eta eta) [False, True])
143143
{all dead. Ordering}
144144
(/\dead -> EQ)
145145
(/\dead ->
146146
Bool_match
147-
(ifThenElse {Bool} (lessThanEqualsInteger eta eta) True False)
147+
(case Bool (lessThanEqualsInteger eta eta) [False, True])
148148
{all dead. Ordering}
149149
(/\dead -> LT)
150150
(/\dead -> GT)
@@ -162,19 +162,18 @@ program
162162
ds
163163
{Bool}
164164
(\(n' : integer) (d' : integer) ->
165-
ifThenElse
166-
{Bool}
165+
case
166+
Bool
167167
(lessThanEqualsInteger
168168
(multiplyInteger n d')
169169
(multiplyInteger n' d))
170-
True
171-
False))
170+
[False, True]))
172171
in
173172
letrec
174173
!euclid : integer -> integer -> integer
175174
= \(x : integer) (y : integer) ->
176175
Bool_match
177-
(ifThenElse {Bool} (equalsInteger 0 y) True False)
176+
(case Bool (equalsInteger 0 y) [False, True])
178177
{all dead. integer}
179178
(/\dead -> x)
180179
(/\dead -> euclid y (modInteger x y))
@@ -184,12 +183,12 @@ program
184183
!unsafeRatio : integer -> integer -> Rational
185184
= \(n : integer) (d : integer) ->
186185
Bool_match
187-
(ifThenElse {Bool} (equalsInteger 0 d) True False)
186+
(case Bool (equalsInteger 0 d) [False, True])
188187
{all dead. Rational}
189188
(/\dead -> error {Rational})
190189
(/\dead ->
191190
Bool_match
192-
(ifThenElse {Bool} (lessThanInteger d 0) True False)
191+
(case Bool (lessThanInteger d 0) [False, True])
193192
{all dead. Rational}
194193
(/\dead ->
195194
unsafeRatio (subtractInteger 0 n) (subtractInteger 0 d))
@@ -211,6 +210,8 @@ program
211210
(\v -> List (Tuple2 PredKey (List v))) Rational -> ParamValue
212211
in
213212
let
213+
!ifThenElse : all a. bool -> a -> a -> a
214+
= /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
214215
data Unit | Unit_match where
215216
Unit : Unit
216217
in
@@ -228,16 +229,12 @@ program
228229
(CConsOrd
229230
{integer}
230231
(\(x : integer) (y : integer) ->
231-
ifThenElse {Bool} (equalsInteger x y) True False)
232+
case Bool (equalsInteger x y) [False, True])
232233
`$fOrdInteger_$ccompare`
233234
(\(x : integer) (y : integer) ->
234-
ifThenElse {Bool} (lessThanInteger x y) True False)
235+
case Bool (lessThanInteger x y) [False, True])
235236
(\(x : integer) (y : integer) ->
236-
ifThenElse
237-
{Bool}
238-
(lessThanEqualsInteger x y)
239-
True
240-
False)
237+
case Bool (lessThanEqualsInteger x y) [False, True])
241238
(\(x : integer) (y : integer) ->
242239
ifThenElse
243240
{Bool}
@@ -248,22 +245,14 @@ program
248245
ifThenElse {Bool} (lessThanInteger x y) False True)
249246
(\(x : integer) (y : integer) ->
250247
Bool_match
251-
(ifThenElse
252-
{Bool}
253-
(lessThanEqualsInteger x y)
254-
True
255-
False)
248+
(case Bool (lessThanEqualsInteger x y) [False, True])
256249
{all dead. integer}
257250
(/\dead -> y)
258251
(/\dead -> x)
259252
{all dead. dead})
260253
(\(x : integer) (y : integer) ->
261254
Bool_match
262-
(ifThenElse
263-
{Bool}
264-
(lessThanEqualsInteger x y)
265-
True
266-
False)
255+
(case Bool (lessThanEqualsInteger x y) [False, True])
267256
{all dead. integer}
268257
(/\dead -> x)
269258
(/\dead -> y)
@@ -288,18 +277,16 @@ program
288277
{Bool}
289278
(\(n' : integer) (d' : integer) ->
290279
Bool_match
291-
(ifThenElse
292-
{Bool}
280+
(case
281+
Bool
293282
(equalsInteger n n')
294-
True
295-
False)
283+
[False, True])
296284
{all dead. Bool}
297285
(/\dead ->
298-
ifThenElse
299-
{Bool}
286+
case
287+
Bool
300288
(equalsInteger d d')
301-
True
302-
False)
289+
[False, True])
303290
(/\dead -> False)
304291
{all dead. dead})))
305292
(\(ds : Rational) (ds : Rational) ->
@@ -323,13 +310,12 @@ program
323310
ds
324311
{Bool}
325312
(\(n' : integer) (d' : integer) ->
326-
ifThenElse
327-
{Bool}
313+
case
314+
Bool
328315
(lessThanInteger
329316
(multiplyInteger n d')
330317
(multiplyInteger n' d))
331-
True
332-
False)))
318+
[False, True])))
333319
`$fOrdRational0_$c<=`
334320
(\(ds : Rational) (ds : Rational) ->
335321
Rational_match
@@ -340,11 +326,13 @@ program
340326
ds
341327
{Bool}
342328
(\(n' : integer) (d' : integer) ->
329+
let
330+
!x : integer = multiplyInteger n d'
331+
!y : integer = multiplyInteger n' d
332+
in
343333
ifThenElse
344334
{Bool}
345-
(lessThanEqualsInteger
346-
(multiplyInteger n d')
347-
(multiplyInteger n' d))
335+
(lessThanEqualsInteger x y)
348336
False
349337
True)))
350338
(\(ds : Rational) (ds : Rational) ->
@@ -356,11 +344,13 @@ program
356344
ds
357345
{Bool}
358346
(\(n' : integer) (d' : integer) ->
347+
let
348+
!x : integer = multiplyInteger n d'
349+
!y : integer = multiplyInteger n' d
350+
in
359351
ifThenElse
360352
{Bool}
361-
(lessThanInteger
362-
(multiplyInteger n d')
363-
(multiplyInteger n' d))
353+
(lessThanInteger x y)
364354
False
365355
True)))
366356
(\(x : Rational) (y : Rational) ->
@@ -399,7 +389,7 @@ program
399389
ds
400390
{list data -> Bool}
401391
(\(eta : list data) ->
402-
ifThenElse {Bool} (nullList {data} eta) True False)
392+
case Bool (nullList {data} eta) [False, True])
403393
(\(paramValueHd : ParamValue)
404394
(paramValueTl : List ParamValue)
405395
(actualValueData : list data) ->
@@ -499,12 +489,12 @@ program
499489
!args : list data = sndPair {integer} {list data} tup
500490
in
501491
Bool_match
502-
(ifThenElse {Bool} (equalsInteger 1 index) True False)
492+
(case Bool (equalsInteger 1 index) [False, True])
503493
{all dead. Maybe a}
504494
(/\dead -> Nothing {a})
505495
(/\dead ->
506496
Bool_match
507-
(ifThenElse {Bool} (equalsInteger 0 index) True False)
497+
(case Bool (equalsInteger 0 index) [False, True])
508498
{all dead. Maybe a}
509499
(/\dead ->
510500
Just {a} (`$dUnsafeFromData` (headList {data} args)))
@@ -5330,13 +5320,12 @@ program
53305320
(unConstrData ds)))))
53315321
in
53325322
Bool_match
5333-
(ifThenElse
5334-
{Bool}
5323+
(case
5324+
Bool
53355325
(equalsInteger
53365326
5
53375327
(fstPair {integer} {list data} tup))
5338-
True
5339-
False)
5328+
[False, True])
53405329
{all dead. data}
53415330
(/\dead ->
53425331
headList
@@ -5357,11 +5346,10 @@ program
53575346
!tup : pair integer (list data) = unConstrData scrut
53585347
in
53595348
Bool_match
5360-
(ifThenElse
5361-
{Bool}
5349+
(case
5350+
Bool
53625351
(equalsInteger 0 (fstPair {integer} {list data} tup))
5363-
True
5364-
False)
5352+
[False, True])
53655353
{all dead. r}
53665354
(/\dead ->
53675355
let
@@ -5397,11 +5385,10 @@ program
53975385
!tup : pair integer (list data) = unConstrData scrut
53985386
in
53995387
Bool_match
5400-
(ifThenElse
5401-
{Bool}
5388+
(case
5389+
Bool
54025390
(equalsInteger 2 (fstPair {integer} {list data} tup))
5403-
True
5404-
False)
5391+
[False, True])
54055392
{all dead. r}
54065393
(/\dead ->
54075394
let

‎cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.small.budget.golden

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 82805157, exBudgetMemory = ExMemory 359105}
1+
ExBudget {exBudgetCPU = ExCPU 66876110, exBudgetMemory = ExMemory 308402}

0 commit comments

Comments
 (0)