Skip to content

Commit c0df0c1

Browse files
effectfullyeffectfully
committed
[Builtins] Allow casing on booleans
1 parent 27d2bc3 commit c0df0c1

File tree

362 files changed

+7840
-8811
lines changed

Some content is hidden

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

362 files changed

+7840
-8811
lines changed

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
2164
1+
2085

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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 549796171, exBudgetMemory = ExMemory 2648818}
1+
ExBudget {exBudgetCPU = ExCPU 472454709, exBudgetMemory = ExMemory 2373180}

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

+46-59
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
@@ -232,16 +233,12 @@ program
232233
(CConsOrd
233234
{integer}
234235
(\(x : integer) (y : integer) ->
235-
ifThenElse {Bool} (equalsInteger x y) True False)
236+
case Bool (equalsInteger x y) [False, True])
236237
`$fOrdInteger_$ccompare`
237238
(\(x : integer) (y : integer) ->
238-
ifThenElse {Bool} (lessThanInteger x y) True False)
239+
case Bool (lessThanInteger x y) [False, True])
239240
(\(x : integer) (y : integer) ->
240-
ifThenElse
241-
{Bool}
242-
(lessThanEqualsInteger x y)
243-
True
244-
False)
241+
case Bool (lessThanEqualsInteger x y) [False, True])
245242
(\(x : integer) (y : integer) ->
246243
ifThenElse
247244
{Bool}
@@ -252,22 +249,14 @@ program
252249
ifThenElse {Bool} (lessThanInteger x y) False True)
253250
(\(x : integer) (y : integer) ->
254251
Bool_match
255-
(ifThenElse
256-
{Bool}
257-
(lessThanEqualsInteger x y)
258-
True
259-
False)
252+
(case Bool (lessThanEqualsInteger x y) [False, True])
260253
{all dead. integer}
261254
(/\dead -> y)
262255
(/\dead -> x)
263256
{all dead. dead})
264257
(\(x : integer) (y : integer) ->
265258
Bool_match
266-
(ifThenElse
267-
{Bool}
268-
(lessThanEqualsInteger x y)
269-
True
270-
False)
259+
(case Bool (lessThanEqualsInteger x y) [False, True])
271260
{all dead. integer}
272261
(/\dead -> x)
273262
(/\dead -> y)
@@ -292,18 +281,16 @@ program
292281
{Bool}
293282
(\(n' : integer) (d' : integer) ->
294283
Bool_match
295-
(ifThenElse
296-
{Bool}
284+
(case
285+
Bool
297286
(equalsInteger n n')
298-
True
299-
False)
287+
[False, True])
300288
{all dead. Bool}
301289
(/\dead ->
302-
ifThenElse
303-
{Bool}
290+
case
291+
Bool
304292
(equalsInteger d d')
305-
True
306-
False)
293+
[False, True])
307294
(/\dead -> False)
308295
{all dead. dead})))
309296
(\(ds : Rational) (ds : Rational) ->
@@ -327,13 +314,12 @@ program
327314
ds
328315
{Bool}
329316
(\(n' : integer) (d' : integer) ->
330-
ifThenElse
331-
{Bool}
317+
case
318+
Bool
332319
(lessThanInteger
333320
(multiplyInteger n d')
334321
(multiplyInteger n' d))
335-
True
336-
False)))
322+
[False, True])))
337323
`$fOrdRational0_$c<=`
338324
(\(ds : Rational) (ds : Rational) ->
339325
Rational_match
@@ -344,11 +330,13 @@ program
344330
ds
345331
{Bool}
346332
(\(n' : integer) (d' : integer) ->
333+
let
334+
!x : integer = multiplyInteger n d'
335+
!y : integer = multiplyInteger n' d
336+
in
347337
ifThenElse
348338
{Bool}
349-
(lessThanEqualsInteger
350-
(multiplyInteger n d')
351-
(multiplyInteger n' d))
339+
(lessThanEqualsInteger x y)
352340
False
353341
True)))
354342
(\(ds : Rational) (ds : Rational) ->
@@ -360,11 +348,13 @@ program
360348
ds
361349
{Bool}
362350
(\(n' : integer) (d' : integer) ->
351+
let
352+
!x : integer = multiplyInteger n d'
353+
!y : integer = multiplyInteger n' d
354+
in
363355
ifThenElse
364356
{Bool}
365-
(lessThanInteger
366-
(multiplyInteger n d')
367-
(multiplyInteger n' d))
357+
(lessThanInteger x y)
368358
False
369359
True)))
370360
(\(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

+1-1
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 86181157, exBudgetMemory = ExMemory 380205}
1+
ExBudget {exBudgetCPU = ExCPU 66780110, exBudgetMemory = ExMemory 307802}

0 commit comments

Comments
 (0)