Skip to content

[Builtins] Add constant casing for builtin unit and pair #7221

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 15 commits into from
Sep 2, 2025
Merged

[Builtins] Add constant casing for builtin unit and pair #7221

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
6b5873e
Add constant casing for unit and pair, make builtin use constant casing
SeungheonOh Jul 17, 2025
41dc567
Update goldens
SeungheonOh Jul 17, 2025
77ec468
changelog
SeungheonOh Jul 17, 2025
7d5291a
Add benchmark for comparing Pair/Unit builtins to casing
SeungheonOh Jul 17, 2025
befce26
Add headList builtin vs casing bench
SeungheonOh Jul 17, 2025
3477dce
Merge branch 'master' into sho/6602-unitpair
SeungheonOh Jul 17, 2025
1432908
Merge branch 'master' into sho/6602-unitpair
SeungheonOh Aug 21, 2025
574598a
comments
SeungheonOh Aug 21, 2025
40afc97
Merge branch 'master' into sho/6602-unitpair
SeungheonOh Aug 25, 2025
57dd8a0
Add conformance test for pair/unit casing
SeungheonOh Aug 29, 2025
ccf4ec9
casing unit should only allow single branch
SeungheonOh Aug 29, 2025
f141871
tidy
SeungheonOh Aug 29, 2025
c49099d
Add `casePair` and make `fromOpaque` use it
SeungheonOh Sep 1, 2025
7ff79e6
Make `FromData` use case pair
SeungheonOh Sep 2, 2025
d4bdf6e
blacklist pair/unit casing conformance on agda
SeungheonOh Sep 2, 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 @@
2041
2045
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 417755505, exBudgetMemory = ExMemory 2085068}
ExBudget {exBudgetCPU = ExCPU 406467137, exBudgetMemory = ExMemory 2070956}
85 changes: 54 additions & 31 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 @@ -488,18 +488,21 @@ program
all a. (\a -> data -> a) a -> data -> Maybe a
= /\a ->
\(`$dUnsafeFromData` : (\a -> data -> a) a) (d : data) ->
let
!tup : pair integer (list data) = unConstrData d
!index : integer = fstPair {integer} {list data} tup
!args : list data = sndPair {integer} {list data} tup
in
case
(list data -> Maybe a)
index
[ (\(ds : list data) ->
Just {a} (`$dUnsafeFromData` (headList {data} ds)))
, (\(ds : list data) -> Nothing {a}) ]
args
(let
b = list data
in
/\r ->
\(p : pair integer b) (f : integer -> b -> r) -> case r p [f])
{Maybe a}
(unConstrData d)
(\(index : integer) (args : list data) ->
case
(list data -> Maybe a)
index
[ (\(ds : list data) ->
Just {a} (`$dUnsafeFromData` (headList {data} ds)))
, (\(ds : list data) -> Nothing {a}) ]
args)
in
letrec
~matchData_go : list (pair data data) -> List (Tuple2 data data)
Expand All @@ -513,11 +516,10 @@ program
(\(x : pair data data) (xs : list (pair data data)) ->
Cons
{Tuple2 data data}
(Tuple2
{data}
{data}
(fstPair {data} {data} x)
(sndPair {data} {data} x))
(case
(Tuple2 data data)
x
[(\(l : data) (r : data) -> Tuple2 {data} {data} l r)])
(matchData_go xs))
in
let
Expand Down Expand Up @@ -5293,9 +5295,8 @@ program
{data}
(tailList
{data}
(sndPair
{integer}
{list data}
(case
(list data)
(unConstrData
(let
!tup : pair integer (list data)
Expand All @@ -5306,24 +5307,34 @@ program
{data}
(tailList
{data}
(sndPair
{integer}
{list data}
(unConstrData ds)))))
(case
(list data)
(unConstrData ds)
[ (\(l : integer)
(r : list data) ->
r) ]))))
in
case
(all dead. data)
(equalsInteger
5
(fstPair {integer} {list data} tup))
(case
integer
tup
[(\(l : integer) (r : list data) -> l)]))
[ (/\dead -> error {data})
, (/\dead ->
headList
{data}
(tailList
{data}
(sndPair {integer} {list data} tup))) ]
{all dead. dead})))))
(case
(list data)
tup
[ (\(l : integer) (r : list data) ->
r) ]))) ]
{all dead. dead}))
[(\(l : integer) (r : list data) -> r)])))
in
(let
r = Maybe (List (Tuple2 data data))
Expand All @@ -5336,11 +5347,17 @@ program
in
case
(all dead. r)
(equalsInteger 0 (fstPair {integer} {list data} tup))
(equalsInteger
0
(case integer tup [(\(l : integer) (r : list data) -> l)]))
[ (/\dead -> fail ())
, (/\dead ->
let
!l : list data = sndPair {integer} {list data} tup
!l : list data
= case
(list data)
tup
[(\(l : integer) (r : list data) -> r)]
!l : list data = tailList {data} l
in
cont
Expand Down Expand Up @@ -5372,11 +5389,17 @@ program
in
case
(all dead. r)
(equalsInteger 2 (fstPair {integer} {list data} tup))
(equalsInteger
2
(case integer tup [(\(l : integer) (r : list data) -> l)]))
[ (/\dead -> fail ())
, (/\dead ->
let
!l : list data = sndPair {integer} {list data} tup
!l : list data
= case
(list data)
tup
[(\(l : integer) (r : list data) -> r)]
in
cont
(unMapData (headList {data} l))
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 61469309, exBudgetMemory = ExMemory 277174}
ExBudget {exBudgetCPU = ExCPU 60269664, exBudgetMemory = ExMemory 276518}
Loading