{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.CertifierReport where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.Nat.Show
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation
import qualified MAlonzo.Code.VerifiedCompilation.Certificate
import qualified MAlonzo.Code.VerifiedCompilation.UntypedTranslation

-- CertifierReport.⇉_
d_'8649'__2 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_'8649'__2 :: Text -> Text
d_'8649'__2 Text
v0
  = (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
      (Text
"  " :: Data.Text.Text) Text
v0
-- CertifierReport.nl
d_nl_6 :: MAlonzo.Code.Agda.Builtin.String.T_String_6
d_nl_6 :: Text
d_nl_6 = Text -> Text
forall a b. a -> b
coe (Text
"\n" :: Data.Text.Text)
-- CertifierReport.hl
d_hl_8 :: MAlonzo.Code.Agda.Builtin.String.T_String_6
d_hl_8 :: Text
d_hl_8
  = Text -> Text
forall a b. a -> b
coe
      (Text
"\n\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\9472\n"
       ::
       Data.Text.Text)
-- CertifierReport.showTag
d_showTag_10 ::
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTag_10 :: T_SimplifierTag_4 -> Text
d_showTag_10 T_SimplifierTag_4
v0
  = case T_SimplifierTag_4 -> T_SimplifierTag_4
forall a b. a -> b
coe T_SimplifierTag_4
v0 of
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_floatDelayT_6
        -> Text -> Text
forall a b. a -> b
coe (Text
"Float Delay" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceDelayT_8
        -> Text -> Text
forall a b. a -> b
coe (Text
"Force-Delay Cancellation" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_forceCaseDelayT_10
        -> Text -> Text
forall a b. a -> b
coe (Text
"Float Force into Case Branches" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_12
        -> Text -> Text
forall a b. a -> b
coe (Text
"Case-of-Case" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseReduceT_14
        -> Text -> Text
forall a b. a -> b
coe
             (Text
"Case-Constr and Case-Constant Cancellation" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_inlineT_16
        -> Text -> Text
forall a b. a -> b
coe (Text
"Inlining" :: Data.Text.Text)
      T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_cseT_18
        -> Text -> Text
forall a b. a -> b
coe (Text
"Common Subexpression Elimination" :: Data.Text.Text)
      T_SimplifierTag_4
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.numSites′
d_numSites'8242'_20 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  Integer
d_numSites'8242'_20 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_12
-> Integer
d_numSites'8242'_20 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 = Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_numSites'8242'_20 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  Integer
du_numSites'8242'_20 :: Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> Any
-> T_Translation_12
-> Integer
forall a b. a -> b
coe
      Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)
      (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
-- CertifierReport._.go
d_go_34 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  Integer
d_go_34 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
d_go_34 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 Integer
v8 T_Translation_12
v9
  = Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 Integer
v8 T_Translation_12
v9
du_go_34 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_Translation_12 ->
  Integer
du_go_34 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 Integer
v3 T__'8866'_14
v4 T__'8866'_14
v5 Integer
v6 T_Translation_12
v7
  = case T_Translation_12 -> T_Translation_12
forall a b. a -> b
coe T_Translation_12
v7 of
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_istranslation_92 Any
v10
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v6)
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_match_98 T_TransMatch_18
v10
        -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_TransMatch_18
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_TransMatch_18
-> Integer
du_go'7504'_44 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v4)
             (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v5) (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_TransMatch_18 -> Any
forall a b. a -> b
coe T_TransMatch_18
v10)
      T_Translation_12
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport._.goᵐ
d_go'7504'_44 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_TransMatch_18 ->
  Integer
d_go'7504'_44 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_TransMatch_18
-> Integer
d_go'7504'_44 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v4 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 Integer
v8 T_TransMatch_18
v9
  = Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_TransMatch_18
-> Integer
du_go'7504'_44 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 Integer
v5 T__'8866'_14
v6 T__'8866'_14
v7 Integer
v8 T_TransMatch_18
v9
du_go'7504'_44 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  MAlonzo.Code.VerifiedCompilation.UntypedTranslation.T_TransMatch_18 ->
  Integer
du_go'7504'_44 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_TransMatch_18
-> Integer
du_go'7504'_44 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 Integer
v3 T__'8866'_14
v4 T__'8866'_14
v5 Integer
v6 T_TransMatch_18
v7
  = case T_TransMatch_18 -> T_TransMatch_18
forall a b. a -> b
coe T_TransMatch_18
v7 of
      T_TransMatch_18
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_var_26
        -> Integer -> Integer
forall a b. a -> b
coe Integer
v6
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_ƛ_32 T_Translation_12
v10
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v11
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v12
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)
                           ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v3)) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12)
                           (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v10)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_app_42 T_Translation_12
v12 T_Translation_12
v13
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v14 T__'8866'_14
v15
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v16 T__'8866'_14
v17
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v15) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v17)
                           ((Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v14) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v16)
                              (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v12))
                           (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v13)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_force_48 T_Translation_12
v10
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v11
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v12
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12)
                           (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v10)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_delay_54 T_Translation_12
v10
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v11
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v12
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v11) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v12)
                           (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v10)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_TransMatch_18
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_con_58
        -> Integer -> Integer
forall a b. a -> b
coe Integer
v6
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_constr_66 T_Pointwise_48
v11
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C_constr_34 Integer
v12 [T__'8866'_14]
v13
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C_constr_34 Integer
v14 [T__'8866'_14]
v15
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> [T__'8866'_14]
 -> [T__'8866'_14]
 -> Integer
 -> T_Pointwise_48
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
du_go'7510''695'_54 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v13)
                           ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v15) (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Pointwise_48 -> Any
forall a b. a -> b
coe T_Pointwise_48
v11)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_case_76 T_Pointwise_48
v12 T_Translation_12
v13
        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v4 of
             MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v14 [T__'8866'_14]
v15
               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v5 of
                    MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v16 [T__'8866'_14]
v17
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v14) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v16)
                           ((Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> [T__'8866'_14]
 -> [T__'8866'_14]
 -> Integer
 -> T_Pointwise_48
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
du_go'7510''695'_54 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v15)
                              ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v17) (Integer -> Any
forall a b. a -> b
coe Integer
v6) (T_Pointwise_48 -> Any
forall a b. a -> b
coe T_Pointwise_48
v12))
                           (T_Translation_12 -> Any
forall a b. a -> b
coe T_Translation_12
v13)
                    T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_TransMatch_18
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_builtin_80
        -> Integer -> Integer
forall a b. a -> b
coe Integer
v6
      T_TransMatch_18
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.C_error_82
        -> Integer -> Integer
forall a b. a -> b
coe Integer
v6
      T_TransMatch_18
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport._.goᵖʷ
d_go'7510''695'_54 ::
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (Integer ->
   MAlonzo.Code.Untyped.T__'8866'_14 ->
   MAlonzo.Code.Untyped.T__'8866'_14 -> ()) ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  Integer
d_go'7510''695'_54 :: (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> (Integer -> T__'8866'_14 -> T__'8866'_14 -> ())
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
d_go'7510''695'_54 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v0 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 ~Integer -> T__'8866'_14 -> T__'8866'_14 -> ()
v4 Integer
v5 [T__'8866'_14]
v6 [T__'8866'_14]
v7 Integer
v8 T_Pointwise_48
v9
  = Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
du_go'7510''695'_54 Integer
v1 T__'8866'_14
v2 T__'8866'_14
v3 Integer
v5 [T__'8866'_14]
v6 [T__'8866'_14]
v7 Integer
v8 T_Pointwise_48
v9
du_go'7510''695'_54 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  Integer ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  Integer
du_go'7510''695'_54 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
du_go'7510''695'_54 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 Integer
v3 [T__'8866'_14]
v4 [T__'8866'_14]
v5 Integer
v6 T_Pointwise_48
v7
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v7 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> Integer -> Integer
forall a b. a -> b
coe Integer
v6
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 Any
v12 T_Pointwise_48
v13
        -> case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v4 of
             (:) Any
v14 [Any]
v15
               -> case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v5 of
                    (:) Any
v16 [Any]
v17
                      -> (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> [T__'8866'_14]
 -> [T__'8866'_14]
 -> Integer
 -> T_Pointwise_48
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Integer
forall a b. a -> b
coe
                           Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> Integer
-> T_Pointwise_48
-> Integer
du_go'7510''695'_54 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) ([Any] -> Any
forall a b. a -> b
coe [Any]
v15)
                           ([Any] -> Any
forall a b. a -> b
coe [Any]
v17)
                           ((Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> Integer
 -> T_Translation_12
 -> Integer)
-> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> Integer
-> T_Translation_12
-> Integer
du_go_34 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Any -> Any
forall a b. a -> b
coe Any
v14) (Any -> Any
forall a b. a -> b
coe Any
v16)
                              (Integer -> Any
forall a b. a -> b
coe Integer
v6) (Any -> Any
forall a b. a -> b
coe Any
v12))
                           (T_Pointwise_48 -> Any
forall a b. a -> b
coe T_Pointwise_48
v13)
                    [Any]
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
             [Any]
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.numSites
d_numSites_114 ::
  Integer ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.T_Transformation_2 ->
  Maybe Integer
d_numSites_114 :: Integer
-> T_SimplifierTag_4
-> T__'8866'_14
-> T__'8866'_14
-> T_Transformation_2
-> Maybe Integer
d_numSites_114 Integer
v0 ~T_SimplifierTag_4
v1 T__'8866'_14
v2 T__'8866'_14
v3 T_Transformation_2
v4 = Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Transformation_2
-> Maybe Integer
du_numSites_114 Integer
v0 T__'8866'_14
v2 T__'8866'_14
v3 T_Transformation_2
v4
du_numSites_114 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.T_Transformation_2 ->
  Maybe Integer
du_numSites_114 :: Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Transformation_2
-> Maybe Integer
du_numSites_114 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Transformation_2
v3
  = case T_Transformation_2 -> T_Transformation_2
forall a b. a -> b
coe T_Transformation_2
v3 of
      MAlonzo.Code.VerifiedCompilation.C_isFD_10 T_Translation_12
v7
        -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_12
-> Any
forall a b. a -> b
coe Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v7)
      MAlonzo.Code.VerifiedCompilation.C_isFlD_18 T_Translation_12
v7
        -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_12
-> Any
forall a b. a -> b
coe Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v7)
      MAlonzo.Code.VerifiedCompilation.C_isCSE_26 T_Translation_12
v7
        -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_12
-> Any
forall a b. a -> b
coe Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v7)
      MAlonzo.Code.VerifiedCompilation.C_isInline_32 T_Inline_224
v6
        -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      MAlonzo.Code.VerifiedCompilation.C_isCaseReduce_40 T_Translation_12
v7
        -> (Any -> Maybe Any) -> Any -> Maybe Integer
forall a b. a -> b
coe
             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
             ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer)
-> Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Translation_12
-> Any
forall a b. a -> b
coe Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Translation_12 -> Integer
du_numSites'8242'_20 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Translation_12
v7)
      T_Transformation_2
MAlonzo.Code.VerifiedCompilation.C_forceCaseDelayNotImplemented_48
        -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      T_Transformation_2
MAlonzo.Code.VerifiedCompilation.C_cocNotImplemented_56
        -> Maybe Any -> Maybe Integer
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      T_Transformation_2
_ -> Maybe Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.showSites
d_showSites_132 ::
  Integer ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.T_Transformation_2 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showSites_132 :: Integer
-> T_SimplifierTag_4
-> T__'8866'_14
-> T__'8866'_14
-> T_Transformation_2
-> Text
d_showSites_132 Integer
v0 ~T_SimplifierTag_4
v1 T__'8866'_14
v2 T__'8866'_14
v3 T_Transformation_2
v4 = Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Transformation_2 -> Text
du_showSites_132 Integer
v0 T__'8866'_14
v2 T__'8866'_14
v3 T_Transformation_2
v4
du_showSites_132 ::
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.T_Transformation_2 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showSites_132 :: Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Transformation_2 -> Text
du_showSites_132 Integer
v0 T__'8866'_14
v1 T__'8866'_14
v2 T_Transformation_2
v3
  = let v4 :: Any
v4
          = (Integer
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_Transformation_2
 -> Maybe Integer)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe Integer
-> T__'8866'_14
-> T__'8866'_14
-> T_Transformation_2
-> Maybe Integer
du_numSites_114 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2) (T_Transformation_2 -> Any
forall a b. a -> b
coe T_Transformation_2
v3) in
    Any -> Text
forall a b. a -> b
coe
      (case Any -> Maybe Any
forall a b. a -> b
coe Any
v4 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 Any
v5
           -> (Text -> Text) -> Any -> Any
forall a b. a -> b
coe
                Text -> Text
d_'8649'__2
                ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   (Text
"Optimization sites: " :: Data.Text.Text)
                   ((Integer -> Text) -> Any -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Any
v5))
         Maybe Any
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
           -> Text -> Any
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
         Maybe Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- CertifierReport.termSize
d_termSize_148 ::
  Integer -> MAlonzo.Code.Untyped.T__'8866'_14 -> Integer
d_termSize_148 :: Integer -> T__'8866'_14 -> Integer
d_termSize_148 Integer
v0 T__'8866'_14
v1
  = case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
      MAlonzo.Code.Untyped.C_'96'_18 T_Fin_10
v2 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      MAlonzo.Code.Untyped.C_ƛ_20 T__'8866'_14
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
             ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> T__'8866'_14 -> Integer
d_termSize_148 ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Any
forall a b. a -> b
coe Integer
v0)) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v2 T__'8866'_14
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)))
             ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v3))
      MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v2
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer)) ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_con_28 T_TmCon_202
v2 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      MAlonzo.Code.Untyped.C_constr_34 Integer
v2 [T__'8866'_14]
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
             ((Integer -> [T__'8866'_14] -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> Integer
d_termSize'7510''695'_152 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v3))
      MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v2 [T__'8866'_14]
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt
             ((Integer -> Integer -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe
                Integer -> Integer -> Integer
addInt (Integer -> Any
forall a b. a -> b
coe (Integer
1 :: Integer))
                ((Integer -> [T__'8866'_14] -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> Integer
d_termSize'7510''695'_152 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([T__'8866'_14] -> Any
forall a b. a -> b
coe [T__'8866'_14]
v3)))
             ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2))
      MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v2 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      T__'8866'_14
MAlonzo.Code.Untyped.C_error_46 -> Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)
      T__'8866'_14
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.termSizeᵖʷ
d_termSize'7510''695'_152 ::
  Integer -> [MAlonzo.Code.Untyped.T__'8866'_14] -> Integer
d_termSize'7510''695'_152 :: Integer -> [T__'8866'_14] -> Integer
d_termSize'7510''695'_152 Integer
v0 [T__'8866'_14]
v1
  = case [T__'8866'_14] -> [Any]
forall a b. a -> b
coe [T__'8866'_14]
v1 of
      [] -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
      (:) Any
v2 [Any]
v3
        -> (Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
             Integer -> Integer -> Integer
addInt ((Integer -> [T__'8866'_14] -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> [T__'8866'_14] -> Integer
d_termSize'7510''695'_152 (Integer -> Any
forall a b. a -> b
coe Integer
v0) ([Any] -> Any
forall a b. a -> b
coe [Any]
v3))
             ((Integer -> T__'8866'_14 -> Integer) -> Any -> Any -> Any
forall a b. a -> b
coe Integer -> T__'8866'_14 -> Integer
d_termSize_148 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (Any -> Any
forall a b. a -> b
coe Any
v2))
      [Any]
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.reportPasses
d_reportPasses_182 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_414
    (MAlonzo.Code.Utils.T__'215'__396
       MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4
       (MAlonzo.Code.Utils.T__'215'__396
          MAlonzo.Code.VerifiedCompilation.Certificate.T_Hints_46
          (MAlonzo.Code.Utils.T__'215'__396
             MAlonzo.Code.Untyped.T__'8866'_14
             MAlonzo.Code.Untyped.T__'8866'_14))) ->
  Integer ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_CertResult_60 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_reportPasses_182 :: Integer
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> Integer
-> T_CertResult_60
-> Text
d_reportPasses_182 Integer
v0 T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
v1 Integer
v2 T_CertResult_60
v3
  = case T_CertResult_60 -> T_CertResult_60
forall a b. a -> b
coe T_CertResult_60
v3 of
      MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_66 Any
v4
        -> case Any -> T_Trace_60
forall a b. a -> b
coe Any
v4 of
             T_Trace_60
MAlonzo.Code.VerifiedCompilation.C_empty_64
               -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
             MAlonzo.Code.VerifiedCompilation.C_cons_78 T_Transformation_2
v11 T_Trace_60
v12
               -> case T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> [Any]
forall a b. a -> b
coe T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
v1 of
                    MAlonzo.Code.Utils.C__'8759'__420 Any
v13 [Any]
v14
                      -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v13 of
                           MAlonzo.Code.Utils.C__'44'__410 Any
v15 Any
v16
                             -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v16 of
                                  MAlonzo.Code.Utils.C__'44'__410 Any
v17 Any
v18
                                    -> case Any -> (Any, Any)
forall a b. a -> b
coe Any
v18 of
                                         MAlonzo.Code.Utils.C__'44'__410 Any
v19 Any
v20
                                           -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
                                                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
d_hl_8
                                                ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                   (Text
"Pass " :: Data.Text.Text)
                                                   ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                      ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v2)
                                                      ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                         (Text
": " :: Data.Text.Text)
                                                         ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                            (T_SimplifierTag_4 -> Text
d_showTag_10 (Any -> T_SimplifierTag_4
forall a b. a -> b
coe Any
v15))
                                                            ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                               Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                               (Text
"  \9989" :: Data.Text.Text)
                                                               ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                  Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                  Text
d_hl_8
                                                                  ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                     Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                     (Text -> Text
d_'8649'__2
                                                                        (Text -> Text
forall a b. a -> b
coe
                                                                           (Text
"Program Size Before: "
                                                                            ::
                                                                            Data.Text.Text)))
                                                                     ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                        Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                        ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe
                                                                           Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56
                                                                           (Integer -> T__'8866'_14 -> Integer
d_termSize_148
                                                                              (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Any -> T__'8866'_14
forall a b. a -> b
coe Any
v19)))
                                                                        ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                           Text
d_nl_6
                                                                           ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                              (Text -> Text
d_'8649'__2
                                                                                 (Text -> Text
forall a b. a -> b
coe
                                                                                    (Text
"Program Size After: "
                                                                                     ::
                                                                                     Data.Text.Text)))
                                                                              ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                                 ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe
                                                                                    Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56
                                                                                    (Integer -> T__'8866'_14 -> Integer
d_termSize_148
                                                                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0)
                                                                                       (Any -> T__'8866'_14
forall a b. a -> b
coe Any
v20)))
                                                                                 ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                                                                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                                    Text
d_nl_6
                                                                                    ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                       Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                                       ((Integer
 -> T__'8866'_14 -> T__'8866'_14 -> T_Transformation_2 -> Text)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                          Integer
-> T__'8866'_14 -> T__'8866'_14 -> T_Transformation_2 -> Text
du_showSites_132
                                                                                          (Integer -> Any
forall a b. a -> b
coe Integer
v0)
                                                                                          (Any -> Any
forall a b. a -> b
coe Any
v19)
                                                                                          (Any -> Any
forall a b. a -> b
coe Any
v20)
                                                                                          (T_Transformation_2 -> Any
forall a b. a -> b
coe T_Transformation_2
v11))
                                                                                       ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                                                                                          Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                                                                          Text
d_nl_6
                                                                                          (Integer
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> Integer
-> T_CertResult_60
-> Text
d_reportPasses_182
                                                                                             (Integer -> Integer
forall a b. a -> b
coe
                                                                                                Integer
v0)
                                                                                             ([Any]
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
forall a b. a -> b
coe
                                                                                                [Any]
v14)
                                                                                             ((Integer -> Integer -> Integer) -> Any -> Any -> Integer
forall a b. a -> b
coe
                                                                                                Integer -> Integer -> Integer
addInt
                                                                                                (Integer -> Any
forall a b. a -> b
coe
                                                                                                   (Integer
1 ::
                                                                                                      Integer))
                                                                                                (Integer -> Any
forall a b. a -> b
coe
                                                                                                   Integer
v2))
                                                                                             ((Any -> T_CertResult_60) -> Any -> T_CertResult_60
forall a b. a -> b
coe
                                                                                                Any -> T_CertResult_60
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_66
                                                                                                (T_Trace_60 -> Any
forall a b. a -> b
coe
                                                                                                   T_Trace_60
v12)))))))))))))))))
                                         (Any, Any)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  (Any, Any)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
                           (Any, Any)
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [Any]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Trace_60
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_74 T_SimplifierTag_4
v7 Any
v8 Any
v9
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
d_hl_8
             ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
"Pass " :: Data.Text.Text)
                ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v2)
                   ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      (Text
": " :: Data.Text.Text)
                      ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                         (T_SimplifierTag_4 -> Text
d_showTag_10 (T_SimplifierTag_4 -> T_SimplifierTag_4
forall a b. a -> b
coe T_SimplifierTag_4
v7))
                         ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                            (Text
"  \10060 FAILED" :: Data.Text.Text) Text
d_hl_8)))))
      MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_80 T_SimplifierTag_4
v6 Any
v7 Any
v8
        -> (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
d_hl_8
             ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                (Text
"Pass " :: Data.Text.Text)
                ((Text -> Text -> Text) -> Any -> Any -> Any
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                   ((Integer -> Text) -> Integer -> Any
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v2)
                   ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                      (Text
": " :: Data.Text.Text)
                      ((Text -> Text -> Text) -> Text -> Any -> Any
forall a b. a -> b
coe
                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                         (T_SimplifierTag_4 -> Text
d_showTag_10 (T_SimplifierTag_4 -> T_SimplifierTag_4
forall a b. a -> b
coe T_SimplifierTag_4
v6))
                         ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
                            Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                            (Text
"  \10060 FAILED" :: Data.Text.Text) Text
d_hl_8)))))
      T_CertResult_60
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- CertifierReport.makeReport
d_makeReport_210 ::
  Integer ->
  MAlonzo.Code.Utils.T_List_414
    (MAlonzo.Code.Utils.T__'215'__396
       MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4
       (MAlonzo.Code.Utils.T__'215'__396
          MAlonzo.Code.VerifiedCompilation.Certificate.T_Hints_46
          (MAlonzo.Code.Utils.T__'215'__396
             MAlonzo.Code.Untyped.T__'8866'_14
             MAlonzo.Code.Untyped.T__'8866'_14))) ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_CertResult_60 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_makeReport_210 :: Integer
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> T_CertResult_60
-> Text
d_makeReport_210 Integer
v0 T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
v1 T_CertResult_60
v2
  = (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
      (Text
"UPLC OPTIMIZATION: CERTIFIER REPORT" :: Data.Text.Text)
      ((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20 Text
d_nl_6
         (Integer
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> Integer
-> T_CertResult_60
-> Text
d_reportPasses_182
            (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
forall a b. a -> b
coe T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T__'8866'_14 T__'8866'_14)))
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (T_CertResult_60 -> T_CertResult_60
forall a b. a -> b
coe T_CertResult_60
v2)))