Skip to content

[Builtins] Allow casing on lists #7188

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.

Sign up for GitHub

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

Merged
SeungheonOh merged 18 commits into from
Jul 14, 2025
Merged

[Builtins] Allow casing on lists #7188

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
27bf49d
Casing on list
SeungheonOh Jul 7, 2025
5ba8215
Allow `HeadSpine` to have different type for head
SeungheonOh Jul 8, 2025
eff07b7
Use `HeadSpine` for casing
SeungheonOh Jul 8, 2025
6333e3e
changelog
SeungheonOh Jul 8, 2025
60d1df1
Rename
SeungheonOh Jul 8, 2025
8c04b5d
review updates
SeungheonOh Jul 9, 2025
99a85a3
Update golden
SeungheonOh Jul 9, 2025
7fcccbb
Fix test, number of branches is checked on type checker for caseing o…
SeungheonOh Jul 9, 2025
f1ea79a
Add benchmark for builtin casing
SeungheonOh Jul 9, 2025
848bb52
use 1.49
SeungheonOh Jul 9, 2025
599de21
Merge branch 'master' into sho/6602-list
SeungheonOh Jul 10, 2025
b85a4cf
Allow builtin casing type checking to allow higher typed builtins to …
SeungheonOh Jul 10, 2025
87639ad
Use builtin casing for `caseList`
SeungheonOh Jul 10, 2025
bea80d6
Update golden
SeungheonOh Jul 10, 2025
e9eb134
Add list casing golden case
SeungheonOh Jul 10, 2025
ae5feee
Update more golden
SeungheonOh Jul 10, 2025
aeebc5c
Add property tests for builtin list casing
SeungheonOh Jul 10, 2025
91a31fa
review changes
SeungheonOh Jul 14, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion ...constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.cbor.size.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
2044
2033
2 changes: 1 addition & 1 deletion ...stitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.large.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 436822709, exBudgetMemory = ExMemory 2150480}
ExBudget {exBudgetCPU = ExCPU 420427505, exBudgetMemory = ExMemory 2101768}
9 changes: 1 addition & 8 deletions cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.pir.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -508,14 +508,7 @@ program
a = pair data data
in
/\r ->
\(z : r) (f : a -> list a -> r) (xs : list a) ->
chooseList
{a}
{all dead. r}
xs
(/\dead -> z)
(/\dead -> f (headList {a} xs) (tailList {a} xs))
{r})
\(z : r) (f : a -> list a -> r) (xs : list a) -> case r xs [z, f])
{List (Tuple2 data data)}
(Nil {Tuple2 data data})
(\(x : pair data data) (xs : list (pair data data)) ->
Expand Down
2 changes: 1 addition & 1 deletion ...stitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.small.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 62348110, exBudgetMemory = ExMemory 280102}
ExBudget {exBudgetCPU = ExCPU 61549309, exBudgetMemory = ExMemory 277674}
112 changes: 52 additions & 60 deletions cardano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/sorted.uplc.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -730,7 +730,11 @@ program
[ ])
, (constr 1
[ cse
, cse ]) ])
, (constr 1
[ (cse
5)
, (constr 0
[ ]) ]) ]) ])
, (constr 0
[ ]) ]) ]) ]))
(constr 3
Expand All @@ -742,11 +746,7 @@ program
[ ])
, (constr 1
[ cse
, (constr 1
[ (cse
5)
, (constr 0
[ ]) ]) ]) ])
, cse ]) ])
, (constr 0
[ ]) ]) ]) ]))
(constr 1
Expand Down Expand Up @@ -779,16 +779,16 @@ program
[ ])
, (constr 1
[ cse
, (constr 1
[ cse
, (constr 0
[ ]) ]) ]) ]))
, cse ]) ]))
(constr 0
[ (constr 1
[ ])
, (constr 1
[ cse
, cse ]) ]))
, (constr 1
[ cse
, (constr 0
[ ]) ]) ]) ]))
(constr 1
[ (constr 0
[ (constr 0
Expand All @@ -813,81 +813,73 @@ program
, (constr 0
[ ]) ]))
(constr 1
[ cse
[ (constr 0
[ (constr 0
[ ])
, (constr 1
[ 500000000
, (constr 0
[ ]) ]) ])
, (constr 0
[ ]) ]))
(constr 1
[ (constr 0
[ (constr 0
[ ])
, (constr 1
[ 500000000
, (constr 0
[ ]) ]) ])
[ (cse
4)
, (constr 0
[ ]) ]))
(constr 1
[ (cse
1)
[ cse
, (constr 0
[ ]) ]))
(constr 1
[ cse
, (constr 0
[ ]) ]))
(cse
10))
1))
(cse
10))
(constr 0
[ (constr 1
[ ])
, cse ]))
(cse 1))
(cse 100))
(cse 4))
(constr 0
[ (constr 1 [])
, (constr 1
[ 1
, (constr 0
[ ]) ]) ]))
(cse 2))
(unsafeRatio 9))
(cse 2))
(constr 0
[ (constr 1
[])
, (constr 1
[ 1
, (constr 0
[ ]) ]) ]))
(cse 10))
(cse 100))
(cse 1))
(unsafeRatio 1))
(unsafeRatio 3))
(unsafeRatio 0))
(constr 1 [0, (constr 0 [])]))
(unsafeRatio 51))
(unsafeRatio 4))
(unsafeRatio 1))
(unsafeRatio 4))
(constr 1 [0, (constr 0 [])]))
(unsafeRatio 9))
(unsafeRatio 51))
((\s -> s s)
(\s arg ->
delay
(\xs ->
force
(force (force chooseList)
xs
(delay (constr 0 []))
(delay
((\x ->
constr 1
[ (constr 0
[ (force
(force
fstPair)
x)
, (force
(force
sndPair)
x) ])
case
xs
[ (constr 0 [])
, (\x xs ->
constr 1
[ (constr 0
[ (force
(force fstPair)
x)
, (force
(s
s
(delay
(\x -> x)))
(force tailList
xs)) ])
(force headList xs))))))
(force sndPair)
x) ])
, (force
(s s (delay (\x -> x)))
xs) ]) ]))
(delay (\x -> x))))
((\s -> s s)
(\s ds cparams ->
Expand Down
2 changes: 1 addition & 1 deletion ...nstitution/test/Cardano/Constitution/Validator/Data/GoldenTests/unsorted.cbor.size.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
2042
2023
2 changes: 1 addition & 1 deletion ...itution/test/Cardano/Constitution/Validator/Data/GoldenTests/unsorted.large.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 599331564, exBudgetMemory = ExMemory 3024315}
ExBudget {exBudgetCPU = ExCPU 582792360, exBudgetMemory = ExMemory 2974703}
9 changes: 1 addition & 8 deletions ...ano-constitution/test/Cardano/Constitution/Validator/Data/GoldenTests/unsorted.pir.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -438,14 +438,7 @@ program
a = pair data data
in
/\r ->
\(z : r) (f : a -> list a -> r) (xs : list a) ->
chooseList
{a}
{all dead. r}
xs
(/\dead -> z)
(/\dead -> f (headList {a} xs) (tailList {a} xs))
{r})
\(z : r) (f : a -> list a -> r) (xs : list a) -> case r xs [z, f])
{List (Tuple2 data data)}
(Nil {Tuple2 data data})
(\(x : pair data data) (xs : list (pair data data)) ->
Expand Down
2 changes: 1 addition & 1 deletion ...itution/test/Cardano/Constitution/Validator/Data/GoldenTests/unsorted.small.budget.golden
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
ExBudget {exBudgetCPU = ExCPU 60810367, exBudgetMemory = ExMemory 271603}
ExBudget {exBudgetCPU = ExCPU 59867566, exBudgetMemory = ExMemory 268275}
Loading