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

* Add constant casing for unit and pair, make builtin use constant casing

* Update goldens

* changelog

* Add benchmark for comparing Pair/Unit builtins to casing

* Add headList builtin vs casing bench

* comments

* Add conformance test for pair/unit casing

* casing unit should only allow single branch

* tidy

* Add `casePair` and make `fromOpaque` use it

* Make `FromData` use case pair

* blacklist pair/unit casing conformance on agda

Author: SeungheonOh

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

@@ -1 +1 @@
-2041
+2045

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

@@ -1 +1 @@
-ExBudget {exBudgetCPU = ExCPU 417755505, exBudgetMemory = ExMemory 2085068}
+ExBudget {exBudgetCPU = ExCPU 406467137, exBudgetMemory = ExMemory 2070956}

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

@@ -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)
@@ -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
@@ -5293,9 +5295,8 @@ program
                  {data}
                  (tailList
                     {data}
-                    (sndPair
-                       {integer}
-                       {list data}
+                    (case
+                       (list data)
                        (unConstrData
                           (let
                             !tup : pair integer (list data)
@@ -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))
@@ -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
@@ -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))

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

@@ -1 +1 @@
-ExBudget {exBudgetCPU = ExCPU 61469309, exBudgetMemory = ExMemory 277174}
+ExBudget {exBudgetCPU = ExCPU 60269664, exBudgetMemory = ExMemory 276518}