Skip to content
Merged
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 @@
2039
2033
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 401320625, exBudgetMemory = ExMemory 2038256}
ExBudget {exBudgetCPU = ExCPU 398677958, exBudgetMemory = ExMemory 2022256}
Original file line number Diff line number Diff line change
Expand Up @@ -128,8 +128,6 @@ program
go expectedPredValues))
in
go ds
!ifThenElse : all a. bool -> a -> a -> a
= /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
in
letrec
!euclid : integer -> integer -> integer
Expand Down Expand Up @@ -211,14 +209,9 @@ program
(\(x : integer) (y : integer) -> lessThanInteger x y)
(\(x : integer) (y : integer) ->
lessThanEqualsInteger x y)
(\(x : integer) (y : integer) -> lessThanInteger y x)
(\(x : integer) (y : integer) ->
ifThenElse
{bool}
(lessThanEqualsInteger x y)
False
True)
(\(x : integer) (y : integer) ->
ifThenElse {bool} (lessThanInteger x y) False True)
lessThanEqualsInteger y x)
(\(x : integer) (y : integer) ->
case
(all dead. integer)
Expand Down Expand Up @@ -318,13 +311,8 @@ program
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{bool}
(lessThanEqualsInteger x y)
False
True)))
lessThanInteger (multiplyInteger n' d) x)))
(\(ds : Rational) (ds : Rational) ->
Rational_match
ds
Expand All @@ -336,13 +324,10 @@ program
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{bool}
(lessThanInteger x y)
False
True)))
lessThanEqualsInteger
(multiplyInteger n' d)
x)))
(\(x : Rational) (y : Rational) ->
Rational_match
x
Expand Down Expand Up @@ -380,8 +365,10 @@ program
!bl : list data = unListData eta
!bl' : list data = tailList {data} bl
in
ifThenElse
{Unit -> Rational}
(let
a = Unit -> Rational
in
\(b : bool) (x : a) (y : a) -> case a b [y, x])
(nullList {data} (tailList {data} bl'))
(\(ds : Unit) ->
unsafeRatio
Expand Down
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 58860489, exBudgetMemory = ExMemory 267518}
ExBudget {exBudgetCPU = ExCPU 58843036, exBudgetMemory = ExMemory 267418}

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -1 +1 @@
2019
2012
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 565605480, exBudgetMemory = ExMemory 2923191}
ExBudget {exBudgetCPU = ExCPU 562962813, exBudgetMemory = ExMemory 2907191}
Original file line number Diff line number Diff line change
Expand Up @@ -128,8 +128,6 @@ program
go expectedPredValues))
in
go ds
!ifThenElse : all a. bool -> a -> a -> a
= /\a -> \(b : bool) (x : a) (y : a) -> case a b [y, x]
in
letrec
!euclid : integer -> integer -> integer
Expand Down Expand Up @@ -211,14 +209,9 @@ program
(\(x : integer) (y : integer) -> lessThanInteger x y)
(\(x : integer) (y : integer) ->
lessThanEqualsInteger x y)
(\(x : integer) (y : integer) -> lessThanInteger y x)
(\(x : integer) (y : integer) ->
ifThenElse
{bool}
(lessThanEqualsInteger x y)
False
True)
(\(x : integer) (y : integer) ->
ifThenElse {bool} (lessThanInteger x y) False True)
lessThanEqualsInteger y x)
(\(x : integer) (y : integer) ->
case
(all dead. integer)
Expand Down Expand Up @@ -318,13 +311,8 @@ program
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{bool}
(lessThanEqualsInteger x y)
False
True)))
lessThanInteger (multiplyInteger n' d) x)))
(\(ds : Rational) (ds : Rational) ->
Rational_match
ds
Expand All @@ -336,13 +324,10 @@ program
(\(n' : integer) (d' : integer) ->
let
!x : integer = multiplyInteger n d'
!y : integer = multiplyInteger n' d
in
ifThenElse
{bool}
(lessThanInteger x y)
False
True)))
lessThanEqualsInteger
(multiplyInteger n' d)
x)))
(\(x : Rational) (y : Rational) ->
Rational_match
x
Expand Down Expand Up @@ -380,8 +365,10 @@ program
!bl : list data = unListData eta
!bl' : list data = tailList {data} bl
in
ifThenElse
{Unit -> Rational}
(let
a = Unit -> Rational
in
\(b : bool) (x : a) (y : a) -> case a b [y, x])
(nullList {data} (tailList {data} bl'))
(\(ds : Unit) ->
unsafeRatio
Expand Down
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 57466746, exBudgetMemory = ExMemory 259919}
ExBudget {exBudgetCPU = ExCPU 57449293, exBudgetMemory = ExMemory 259819}
Loading
Loading