Skip to content

Commit 65c6e4d

Browse files
SeungheonOhSeungheonOh
authored
[Builtins] Allow casing on lists (#7188)
* Casing on list * Allow `HeadSpine` to have different type for head * Use `HeadSpine` for casing * changelog * Rename * review updates * Update golden * Fix test, number of branches is checked on type checker for caseing on bool * Add benchmark for builtin casing * use 1.49 * Allow builtin casing type checking to allow higher typed builtins to take type variable * Use builtin casing for `caseList` * Update golden * Add list casing golden case * Update more golden * Add property tests for builtin list casing * review changes
1 parent 56e0834 commit 65c6e4d

File tree

280 files changed

+6864
-7401
lines changed

Some content is hidden

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

280 files changed

+6864
-7401
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-
2044
1+
2033

‎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 436822709, exBudgetMemory = ExMemory 2150480}
1+
ExBudget {exBudgetCPU = ExCPU 420427505, exBudgetMemory = ExMemory 2101768}

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

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -508,14 +508,7 @@ program
508508
a = pair data data
509509
in
510510
/\r ->
511-
\(z : r) (f : a -> list a -> r) (xs : list a) ->
512-
chooseList
513-
{a}
514-
{all dead. r}
515-
xs
516-
(/\dead -> z)
517-
(/\dead -> f (headList {a} xs) (tailList {a} xs))
518-
{r})
511+
\(z : r) (f : a -> list a -> r) (xs : list a) -> case r xs [z, f])
519512
{List (Tuple2 data data)}
520513
(Nil {Tuple2 data data})
521514
(\(x : pair data data) (xs : list (pair data data)) ->

‎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 62348110, exBudgetMemory = ExMemory 280102}
1+
ExBudget {exBudgetCPU = ExCPU 61549309, exBudgetMemory = ExMemory 277674}

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

Lines changed: 52 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -730,7 +730,11 @@ program
730730
[ ])
731731
, (constr 1
732732
[ cse
733-
, cse ]) ])
733+
, (constr 1
734+
[ (cse
735+
5)
736+
, (constr 0
737+
[ ]) ]) ]) ])
734738
, (constr 0
735739
[ ]) ]) ]) ]))
736740
(constr 3
@@ -742,11 +746,7 @@ program
742746
[ ])
743747
, (constr 1
744748
[ cse
745-
, (constr 1
746-
[ (cse
747-
5)
748-
, (constr 0
749-
[ ]) ]) ]) ])
749+
, cse ]) ])
750750
, (constr 0
751751
[ ]) ]) ]) ]))
752752
(constr 1
@@ -779,16 +779,16 @@ program
779779
[ ])
780780
, (constr 1
781781
[ cse
782-
, (constr 1
783-
[ cse
784-
, (constr 0
785-
[ ]) ]) ]) ]))
782+
, cse ]) ]))
786783
(constr 0
787784
[ (constr 1
788785
[ ])
789786
, (constr 1
790787
[ cse
791-
, cse ]) ]))
788+
, (constr 1
789+
[ cse
790+
, (constr 0
791+
[ ]) ]) ]) ]))
792792
(constr 1
793793
[ (constr 0
794794
[ (constr 0
@@ -813,81 +813,73 @@ program
813813
, (constr 0
814814
[ ]) ]))
815815
(constr 1
816-
[ cse
816+
[ (constr 0
817+
[ (constr 0
818+
[ ])
819+
, (constr 1
820+
[ 500000000
821+
, (constr 0
822+
[ ]) ]) ])
817823
, (constr 0
818824
[ ]) ]))
819825
(constr 1
820-
[ (constr 0
821-
[ (constr 0
822-
[ ])
823-
, (constr 1
824-
[ 500000000
825-
, (constr 0
826-
[ ]) ]) ])
826+
[ (cse
827+
4)
827828
, (constr 0
828829
[ ]) ]))
829830
(constr 1
830-
[ (cse
831-
1)
831+
[ cse
832832
, (constr 0
833833
[ ]) ]))
834834
(constr 1
835835
[ cse
836836
, (constr 0
837837
[ ]) ]))
838838
(cse
839-
10))
839+
1))
840840
(cse
841841
10))
842842
(constr 0
843843
[ (constr 1
844844
[ ])
845845
, cse ]))
846-
(cse 1))
847-
(cse 100))
848-
(cse 4))
849-
(constr 0
850-
[ (constr 1 [])
851-
, (constr 1
852-
[ 1
853-
, (constr 0
854-
[ ]) ]) ]))
855-
(cse 2))
856-
(unsafeRatio 9))
846+
(cse 2))
847+
(constr 0
848+
[ (constr 1
849+
[])
850+
, (constr 1
851+
[ 1
852+
, (constr 0
853+
[ ]) ]) ]))
854+
(cse 10))
855+
(cse 100))
856+
(cse 1))
857+
(unsafeRatio 1))
857858
(unsafeRatio 3))
858859
(unsafeRatio 0))
859-
(constr 1 [0, (constr 0 [])]))
860-
(unsafeRatio 51))
861-
(unsafeRatio 4))
862-
(unsafeRatio 1))
860+
(unsafeRatio 4))
861+
(constr 1 [0, (constr 0 [])]))
862+
(unsafeRatio 9))
863+
(unsafeRatio 51))
863864
((\s -> s s)
864865
(\s arg ->
865866
delay
866867
(\xs ->
867-
force
868-
(force (force chooseList)
869-
xs
870-
(delay (constr 0 []))
871-
(delay
872-
((\x ->
873-
constr 1
874-
[ (constr 0
875-
[ (force
876-
(force
877-
fstPair)
878-
x)
879-
, (force
880-
(force
881-
sndPair)
882-
x) ])
868+
case
869+
xs
870+
[ (constr 0 [])
871+
, (\x xs ->
872+
constr 1
873+
[ (constr 0
874+
[ (force
875+
(force fstPair)
876+
x)
883877
, (force
884-
(s
885-
s
886-
(delay
887-
(\x -> x)))
888-
(force tailList
889-
xs)) ])
890-
(force headList xs))))))
878+
(force sndPair)
879+
x) ])
880+
, (force
881+
(s s (delay (\x -> x)))
882+
xs) ]) ]))
891883
(delay (\x -> x))))
892884
((\s -> s s)
893885
(\s ds cparams ->

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
2042
1+
2023

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 599331564, exBudgetMemory = ExMemory 3024315}
1+
ExBudget {exBudgetCPU = ExCPU 582792360, exBudgetMemory = ExMemory 2974703}

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

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -438,14 +438,7 @@ program
438438
a = pair data data
439439
in
440440
/\r ->
441-
\(z : r) (f : a -> list a -> r) (xs : list a) ->
442-
chooseList
443-
{a}
444-
{all dead. r}
445-
xs
446-
(/\dead -> z)
447-
(/\dead -> f (headList {a} xs) (tailList {a} xs))
448-
{r})
441+
\(z : r) (f : a -> list a -> r) (xs : list a) -> case r xs [z, f])
449442
{List (Tuple2 data data)}
450443
(Nil {Tuple2 data data})
451444
(\(x : pair data data) (xs : list (pair data data)) ->

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
ExBudget {exBudgetCPU = ExCPU 60810367, exBudgetMemory = ExMemory 271603}
1+
ExBudget {exBudgetCPU = ExCPU 59867566, exBudgetMemory = ExMemory 268275}

0 commit comments

Comments
 (0)