{-# 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.Certifier 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.CertifierReport
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Untyped
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation
import qualified MAlonzo.Code.VerifiedCompilation.Certificate

-- Certifier.runCertifier
d_runCertifier_2 ::
  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.RawU.T_Untyped_208
             MAlonzo.Code.RawU.T_Untyped_208))) ->
  Maybe MAlonzo.Code.VerifiedCompilation.T_Cert_656
d_runCertifier_2 :: T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> Maybe T_Cert_656
d_runCertifier_2 T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
v0
  = let v1 :: Any
v1
          = ((Any -> T_Either_6 Any Any)
 -> T_List_414
      (T__'215'__396
         T_SimplifierTag_4
         (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))
 -> T_Either_6
      Any
      (T_List_414
         (T__'215'__396
            T_SimplifierTag_4
            (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))))
-> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> T_Either_6 Any Any)
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))
-> T_Either_6
     Any
     (T_List_414
        (T__'215'__396
           T_SimplifierTag_4
           (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any))))
MAlonzo.Code.VerifiedCompilation.du_traverseEitherList_534
              ((T_Untyped_208 -> T_Either_6 T_ScopeError_576 T__'8866'_14) -> Any
forall a b. a -> b
coe T_Untyped_208 -> T_Either_6 T_ScopeError_576 T__'8866'_14
MAlonzo.Code.Untyped.d_scopeCheckU0_276) (T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> 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_Untyped_208 T_Untyped_208)))
v0) in
    Any -> Maybe T_Cert_656
forall a b. a -> b
coe
      (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v1 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v2
           -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v2
           -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                ((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
 -> T_Cert_656)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                   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
-> T_Cert_656
MAlonzo.Code.VerifiedCompilation.C_cert_662 (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
                   (Any -> Any
forall a b. a -> b
coe Any
v2)
                   ((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)
-> Any -> Any -> Any
forall a b. a -> b
coe
                      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
MAlonzo.Code.VerifiedCompilation.d_isTrace'63'_362
                      (Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer)) (Any -> Any
forall a b. a -> b
coe Any
v2)))
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Certifier.runCertifierMain
runCertifierMain ::
  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.RawU.T_Untyped_208
             MAlonzo.Code.RawU.T_Untyped_208))) ->
  MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
    ()
    (MAlonzo.Code.Utils.T__'215'__396
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
runCertifierMain :: T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
runCertifierMain = (T_List_414
   (T__'215'__396
      T_SimplifierTag_4
      (T__'215'__396
         T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
 -> T_Maybe_10 () (T__'215'__396 Bool T_String_6))
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396
           T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
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_Untyped_208 T_Untyped_208)))
-> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
d_runCertifierMain_16
d_runCertifierMain_16 ::
  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.RawU.T_Untyped_208
             MAlonzo.Code.RawU.T_Untyped_208))) ->
  Maybe
    (MAlonzo.Code.Utils.T__'215'__396
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
d_runCertifierMain_16 :: T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
d_runCertifierMain_16 T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
v0
  = let v1 :: Any
v1
          = ((Any -> T_Either_6 Any Any)
 -> T_List_414
      (T__'215'__396
         T_SimplifierTag_4
         (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))
 -> T_Either_6
      Any
      (T_List_414
         (T__'215'__396
            T_SimplifierTag_4
            (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))))
-> Any -> Any -> Any
forall a b. a -> b
coe
              (Any -> T_Either_6 Any Any)
-> T_List_414
     (T__'215'__396
        T_SimplifierTag_4
        (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any)))
-> T_Either_6
     Any
     (T_List_414
        (T__'215'__396
           T_SimplifierTag_4
           (T__'215'__396 T_Hints_46 (T__'215'__396 Any Any))))
MAlonzo.Code.VerifiedCompilation.du_traverseEitherList_534
              ((T_Untyped_208 -> T_Either_6 T_ScopeError_576 T__'8866'_14) -> Any
forall a b. a -> b
coe T_Untyped_208 -> T_Either_6 T_ScopeError_576 T__'8866'_14
MAlonzo.Code.Untyped.d_scopeCheckU0_276) (T_List_414
  (T__'215'__396
     T_SimplifierTag_4
     (T__'215'__396
        T_Hints_46 (T__'215'__396 T_Untyped_208 T_Untyped_208)))
-> 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_Untyped_208 T_Untyped_208)))
v0) in
    Any -> T_Maybe_10 () (T__'215'__396 Bool T_String_6)
forall a b. a -> b
coe
      (case Any -> T_Either_6 Any Any
forall a b. a -> b
coe Any
v1 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v2
           -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v2
           -> let v3 :: Integer
v3 = Integer
0 :: Integer in
              Any -> Any
forall a b. a -> b
coe
                (let v4 :: T_CertResult_60
v4
                       = 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
MAlonzo.Code.VerifiedCompilation.d_isTrace'63'_362
                           (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)) (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
v2) in
                 Any -> Any
forall a b. a -> b
coe
                   (case T_CertResult_60 -> T_CertResult_60
forall a b. a -> b
coe T_CertResult_60
v4 of
                      MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_66 Any
v5
                        -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                             ((Any -> Any -> T__'215'__396 Any Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                Any -> Any -> T__'215'__396 Any Any
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__410
                                (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                                ((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
 -> T_String_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                   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
-> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_210 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Any -> Any
forall a b. a -> b
coe Any
v2)
                                   (T_CertResult_60 -> Any
forall a b. a -> b
coe T_CertResult_60
v4)))
                      MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_74 T_SimplifierTag_4
v8 Any
v9 Any
v10
                        -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                             ((Any -> Any -> T__'215'__396 Any Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                Any -> Any -> T__'215'__396 Any Any
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__410
                                (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                                ((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
 -> T_String_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                   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
-> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_210 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Any -> Any
forall a b. a -> b
coe Any
v2)
                                   ((T_SimplifierTag_4 -> Any -> Any -> T_CertResult_60)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                      T_SimplifierTag_4 -> Any -> Any -> T_CertResult_60
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_74 T_SimplifierTag_4
v8 Any
v9
                                      Any
v10)))
                      MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_80 T_SimplifierTag_4
v7 Any
v8 Any
v9
                        -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
                             Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                             ((Any -> Any -> T__'215'__396 Any Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                Any -> Any -> T__'215'__396 Any Any
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__410
                                (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                                ((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
 -> T_String_6)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                   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
-> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_210 (Integer -> Any
forall a b. a -> b
coe Integer
v3) (Any -> Any
forall a b. a -> b
coe Any
v2)
                                   ((T_SimplifierTag_4 -> Any -> Any -> T_CertResult_60)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                      T_SimplifierTag_4 -> Any -> Any -> T_CertResult_60
MAlonzo.Code.VerifiedCompilation.Certificate.C_abort_80 T_SimplifierTag_4
v7 Any
v8
                                      Any
v9)))
                      T_CertResult_60
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)