Skip to content

[Builtins] Allow casing on booleans #7029

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
Original file line number Diff line number Diff line change
@@ -1 +1 @@
2143
2085
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 540900171, exBudgetMemory = ExMemory 2593218}
ExBudget {exBudgetCPU = ExCPU 472454709, exBudgetMemory = ExMemory 2373180}
Original file line number Diff line number Diff line change
Expand Up @@ -139,12 +139,12 @@ program
!`$fOrdInteger_$ccompare` : integer -> integer -> Ordering
= \(eta : integer) (eta : integer) ->
Bool_match
(ifThenElse {Bool} (equalsInteger eta eta) True False)
(case Bool (equalsInteger eta eta) [False, True])
{all dead. Ordering}
(/\dead -> EQ)
(/\dead ->
Bool_match
(ifThenElse {Bool} (lessThanEqualsInteger eta eta) True False)
(case Bool (lessThanEqualsInteger eta eta) [False, True])
{all dead. Ordering}
(/\dead -> LT)
(/\dead -> GT)
Expand All @@ -162,19 +162,18 @@ program
ds
{Bool}
(\(n' : integer) (d' : integer) ->
ifThenElse
{Bool}
case
Bool
(lessThanEqualsInteger
(multiplyInteger n d')
(multiplyInteger n' d))
True
False))
[False, True]))
in
letrec
!euclid : integer -> integer -> integer
= \(x : integer) (y : integer) ->
Bool_match
(ifThenElse {Bool} (equalsInteger 0 y) True False)
(case Bool (equalsInteger 0 y) [False, True])
{all dead. integer}
(/\dead -> x)
(/\dead -> euclid y (modInteger x y))
Expand All @@ -184,12 +183,12 @@ program
!unsafeRatio : integer -> integer -> Rational
= \(n : integer) (d : integer) ->
Bool_match
(ifThenElse {Bool} (equalsInteger 0 d) True False)
(case Bool (equalsInteger 0 d) [False, True])
{all dead. Rational}
(/\dead -> error {Rational})
(/\dead ->
Bool_match
(ifThenElse {Bool} (lessThanInteger d 0) True False)
(case Bool (lessThanInteger d 0) [False, True])
{all dead. Rational}
(/\dead ->
unsafeRatio (subtractInteger 0 n) (subtractInteger 0 d))
Expand All @@ -211,6 +210,8 @@ program
(\v -> List (Tuple2 PredKey (List v))) Rational -> ParamValue
in
let
!ifThenElse : all a. bool -> a -> a -> a
= /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
data Unit | Unit_match where
Unit : Unit
in
Expand All @@ -232,16 +233,12 @@ program
(CConsOrd
{integer}
(\(x : integer) (y : integer) ->
ifThenElse {Bool} (equalsInteger x y) True False)
case Bool (equalsInteger x y) [False, True])
`$fOrdInteger_$ccompare`
(\(x : integer) (y : integer) ->
ifThenElse {Bool} (lessThanInteger x y) True False)
case Bool (lessThanInteger x y) [False, True])
(\(x : integer) (y : integer) ->
ifThenElse
{Bool}
(lessThanEqualsInteger x y)
True
False)
case Bool (lessThanEqualsInteger x y) [False, True])
(\(x : integer) (y : integer) ->
ifThenElse
{Bool}
Expand All @@ -252,22 +249,14 @@ program
ifThenElse {Bool} (lessThanInteger x y) False True)
(\(x : integer) (y : integer) ->
Bool_match
(ifThenElse
{Bool}
(lessThanEqualsInteger x y)
True
False)
(case Bool (lessThanEqualsInteger x y) [False, True])
{all dead. integer}
(/\dead -> y)
(/\dead -> x)
{all dead. dead})
(\(x : integer) (y : integer) ->
Bool_match
(ifThenElse
{Bool}
(lessThanEqualsInteger x y)
True
False)
(case Bool (lessThanEqualsInteger x y) [False, True])
{all dead. integer}
(/\dead -> x)
(/\dead -> y)
Expand All @@ -292,18 +281,16 @@ program
{Bool}
(\(n' : integer) (d' : integer) ->
Bool_match
(ifThenElse
{Bool}
(case
Bool
(equalsInteger n n')
True
False)
[False, True])
{all dead. Bool}
(/\dead ->
ifThenElse
{Bool}
case
Bool
(equalsInteger d d')
True
False)
[False, True])
(/\dead -> False)
{all dead. dead})))
(\(ds : Rational) (ds : Rational) ->
Expand All @@ -327,13 +314,12 @@ program
ds
{Bool}
(\(n' : integer) (d' : integer) ->
ifThenElse
{Bool}
case
Bool
(lessThanInteger
(multiplyInteger n d')
(multiplyInteger n' d))
True
False)))
[False, True])))
`$fOrdRational0_$c<=`
(\(ds : Rational) (ds : Rational) ->
Rational_match
Expand All @@ -344,11 +330,13 @@ program
ds
{Bool}
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{Bool}
(lessThanEqualsInteger
(multiplyInteger n d')
(multiplyInteger n' d))
(lessThanEqualsInteger x y)
False
True)))
(\(ds : Rational) (ds : Rational) ->
Expand All @@ -360,11 +348,13 @@ program
ds
{Bool}
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{Bool}
(lessThanInteger
(multiplyInteger n d')
(multiplyInteger n' d))
(lessThanInteger x y)
False
True)))
(\(x : Rational) (y : Rational) ->
Expand Down Expand Up @@ -399,7 +389,7 @@ program
ds
{list data -> Bool}
(\(eta : list data) ->
ifThenElse {Bool} (nullList {data} eta) True False)
case Bool (nullList {data} eta) [False, True])
(\(paramValueHd : ParamValue)
(paramValueTl : List ParamValue)
(actualValueData : list data) ->
Expand Down Expand Up @@ -499,12 +489,12 @@ program
!args : list data = sndPair {integer} {list data} tup
in
Bool_match
(ifThenElse {Bool} (equalsInteger 1 index) True False)
(case Bool (equalsInteger 1 index) [False, True])
{all dead. Maybe a}
(/\dead -> Nothing {a})
(/\dead ->
Bool_match
(ifThenElse {Bool} (equalsInteger 0 index) True False)
(case Bool (equalsInteger 0 index) [False, True])
{all dead. Maybe a}
(/\dead ->
Just {a} (`$dUnsafeFromData` (headList {data} args)))
Expand Down Expand Up @@ -5330,13 +5320,12 @@ program
(unConstrData ds)))))
in
Bool_match
(ifThenElse
{Bool}
(case
Bool
(equalsInteger
5
(fstPair {integer} {list data} tup))
True
False)
[False, True])
{all dead. data}
(/\dead ->
headList
Expand All @@ -5357,11 +5346,10 @@ program
!tup : pair integer (list data) = unConstrData scrut
in
Bool_match
(ifThenElse
{Bool}
(case
Bool
(equalsInteger 0 (fstPair {integer} {list data} tup))
True
False)
[False, True])
{all dead. r}
(/\dead ->
let
Expand Down Expand Up @@ -5397,11 +5385,10 @@ program
!tup : pair integer (list data) = unConstrData scrut
in
Bool_match
(ifThenElse
{Bool}
(case
Bool
(equalsInteger 2 (fstPair {integer} {list data} tup))
True
False)
[False, True])
{all dead. r}
(/\dead ->
let
Expand Down
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 82853157, exBudgetMemory = ExMemory 359405}
ExBudget {exBudgetCPU = ExCPU 66780110, exBudgetMemory = ExMemory 307802}
Loading
Loading