{-# 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.CertifierReport
import qualified MAlonzo.Code.RawU
import qualified MAlonzo.Code.Utils
import qualified MAlonzo.Code.VerifiedCompilation
import qualified MAlonzo.Code.VerifiedCompilation.Trace

-- Certifier.runCertifier
d_runCertifier_2 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_NonEmptySep_90
    (MAlonzo.Code.Utils.T__'215'__436
       (MAlonzo.Code.Utils.T_Either_6
          MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
       MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
    MAlonzo.Code.RawU.T_Untyped_208 ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.VerifiedCompilation.T_Error_2
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_runCertifier_2 :: T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
v0
  = (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> T_Either_6 T_Error_2 T_Σ_14
forall a b. a -> b
coe
      T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_54
      ((Maybe Any -> Any -> T_Either_6 Any Any) -> Any -> Any -> Any
forall a b. a -> b
coe
         Maybe Any -> Any -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_try_102
         ((T_NonEmptySep_90
   (T__'215'__436
      (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
   T_Untyped_208
 -> Maybe
      (T_NonEmptySep_90
         (T__'215'__436
            (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
         T__'8866'_14))
-> Any -> Any
forall a b. a -> b
coe
            T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> Maybe
     (T_NonEmptySep_90
        (T__'215'__436
           (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
        T__'8866'_14)
MAlonzo.Code.VerifiedCompilation.d_checkScope'7511'_102 (T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> Any
forall a b. a -> b
coe T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
v0))
         (T_Error_2 -> Any
forall a b. a -> b
coe T_Error_2
MAlonzo.Code.VerifiedCompilation.C_illScoped_6))
      ((Any -> Any) -> Any
forall a b. a -> b
coe
         (\ Any
v1 ->
            (T_Either_6 Any Any
 -> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any)
-> Any -> Any -> Any
forall a b. a -> b
coe
              T_Either_6 Any Any
-> (Any -> T_Either_6 Any Any) -> T_Either_6 Any Any
MAlonzo.Code.Utils.du_eitherBind_54
              ((T_NonEmptySep_90
   (T__'215'__436
      (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
   T__'8866'_14
 -> T_Either_6 T_Error_2 Any)
-> Any -> Any
forall a b. a -> b
coe T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T__'8866'_14
-> T_Either_6 T_Error_2 Any
MAlonzo.Code.VerifiedCompilation.d_certify_46 (Any -> Any
forall a b. a -> b
coe Any
v1))
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    (Any -> T_Either_6 Any Any) -> Any -> Any
forall a b. a -> b
coe
                      Any -> T_Either_6 Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                      ((Any -> Any -> T_Σ_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                         Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (Any -> Any
forall a b. a -> b
coe Any
v1) (Any -> Any
forall a b. a -> b
coe Any
v2))))))
-- Certifier.runCertifierMain
runCertifierMain ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_NonEmptySep_90
    (MAlonzo.Code.Utils.T__'215'__436
       (MAlonzo.Code.Utils.T_Either_6
          MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
       MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
    MAlonzo.Code.RawU.T_Untyped_208 ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10
    () MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122 ->
  MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
    ()
    (MAlonzo.Code.Utils.T__'215'__436
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
runCertifierMain :: T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_List_10 () T_EvalResult_122
-> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
runCertifierMain = (T_NonEmptySep_90
   (T__'215'__436
      (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
   T_Untyped_208
 -> T_List_10 () T_EvalResult_122
 -> T_Maybe_10 () (T__'215'__436 Bool T_String_6))
-> T_NonEmptySep_90
     (T__'215'__436
        (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
     T_Untyped_208
-> T_List_10 () T_EvalResult_122
-> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
forall a b. a -> b
coe T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_List_10 () T_EvalResult_122
-> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
d_runCertifierMain_10
d_runCertifierMain_10 ::
  MAlonzo.Code.VerifiedCompilation.Trace.T_NonEmptySep_90
    (MAlonzo.Code.Utils.T__'215'__436
       (MAlonzo.Code.Utils.T_Either_6
          MAlonzo.Code.VerifiedCompilation.Trace.T_UncertifiedOptTag_4
          MAlonzo.Code.VerifiedCompilation.Trace.T_CertifiedOptTag_12)
       MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_80)
    MAlonzo.Code.RawU.T_Untyped_208 ->
  [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_122] ->
  Maybe
    (MAlonzo.Code.Utils.T__'215'__436
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
d_runCertifierMain_10 :: T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_List_10 () T_EvalResult_122
-> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
d_runCertifierMain_10 T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
v0 T_List_10 () T_EvalResult_122
v1
  = let v2 :: T_Either_6 T_Error_2 T_Σ_14
v2 = T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 (T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
-> T_NonEmptySep_90
     (T__'215'__436
        (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
     T_Untyped_208
forall a b. a -> b
coe T_NonEmptySep_90
  (T__'215'__436
     (T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12) T_Hints_80)
  T_Untyped_208
v0) in
    Any -> T_Maybe_10 () (T__'215'__436 Bool T_String_6)
forall a b. a -> b
coe
      (case T_Either_6 T_Error_2 T_Σ_14 -> T_Either_6 Any Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v2 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v3
           -> case Any -> T_Error_2
forall a b. a -> b
coe Any
v3 of
                T_Error_2
MAlonzo.Code.VerifiedCompilation.C_emptyDump_4
                  -> Maybe Any -> Any
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Error_2
MAlonzo.Code.VerifiedCompilation.C_illScoped_6
                  -> 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.VerifiedCompilation.C_counterExample_8 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4
                  -> (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 -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                          (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                          ((T_Either_6 T_Error_2 T_Σ_14
 -> T_List_10 () T_EvalResult_122 -> T_String_6)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 T_Error_2 T_Σ_14
-> T_List_10 () T_EvalResult_122 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_334 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v2) (T_List_10 () T_EvalResult_122 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_122
v1)))
                MAlonzo.Code.VerifiedCompilation.C_abort_10 T_Either_6 T_UncertifiedOptTag_4 T_CertifiedOptTag_12
v4
                  -> (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 -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                          (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                          ((T_Either_6 T_Error_2 T_Σ_14
 -> T_List_10 () T_EvalResult_122 -> T_String_6)
-> Any -> Any -> Any
forall a b. a -> b
coe
                             T_Either_6 T_Error_2 T_Σ_14
-> T_List_10 () T_EvalResult_122 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_334 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v2) (T_List_10 () T_EvalResult_122 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_122
v1)))
                T_Error_2
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v3
           -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v3)
                ((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 -> (Any, Any)) -> Any -> Any -> Any
forall a b. a -> b
coe
                      Any -> Any -> (Any, Any)
forall {a} {b}. a -> b -> (a, b)
MAlonzo.Code.Utils.C__'44'__450
                      (Bool -> Any
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      ((T_Either_6 T_Error_2 T_Σ_14
 -> T_List_10 () T_EvalResult_122 -> T_String_6)
-> Any -> Any -> Any
forall a b. a -> b
coe
                         T_Either_6 T_Error_2 T_Σ_14
-> T_List_10 () T_EvalResult_122 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_334 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v2) (T_List_10 () T_EvalResult_122 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_122
v1))))
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)