{-# 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.Utils.T__'215'__426
     MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__426
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_52
        (MAlonzo.Code.Utils.T__'215'__426
           MAlonzo.Code.RawU.T_Untyped_208
           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__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 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_94
         (([T__'215'__426
    T_SimplifierTag_4
    (T__'215'__426
       T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
 -> Maybe T_Trace_60)
-> Any -> Any
forall a b. a -> b
coe [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_60
MAlonzo.Code.VerifiedCompilation.Trace.d_toTrace_78 ([T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> Any
forall a b. a -> b
coe [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
v0))
         (T_Error_2 -> Any
forall a b. a -> b
coe T_Error_2
MAlonzo.Code.VerifiedCompilation.C_emptyDump_4))
      ((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
              ((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_94
                 ((T_Trace_60 -> Maybe T_Trace_60) -> Any -> Any
forall a b. a -> b
coe
                    T_Trace_60 -> Maybe T_Trace_60
MAlonzo.Code.VerifiedCompilation.d_checkScope'7511'_100 (Any -> Any
forall a b. a -> b
coe Any
v1))
                 (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
v2 ->
                    (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_Trace_60 -> T_Either_6 T_Error_2 Any) -> Any -> Any
forall a b. a -> b
coe T_Trace_60 -> T_Either_6 T_Error_2 Any
MAlonzo.Code.VerifiedCompilation.d_certify_44 (Any -> Any
forall a b. a -> b
coe Any
v2))
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v3 ->
                            (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
v2)
                                 (Any -> Any
forall a b. a -> b
coe Any
v3))))))))
-- Certifier.runCertifierMain
runCertifierMain ::
  MAlonzo.Code.Agda.Builtin.List.T_List_10
    ()
    (MAlonzo.Code.Utils.T__'215'__426
       MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
       (MAlonzo.Code.Utils.T__'215'__426
          MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_52
          (MAlonzo.Code.Utils.T__'215'__426
             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'__426
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
runCertifierMain :: [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Maybe_10 () (T__'215'__426 Bool T_String_6)
runCertifierMain = ([T__'215'__426
    T_SimplifierTag_4
    (T__'215'__426
       T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
 -> T_Maybe_10 () (T__'215'__426 Bool T_String_6))
-> [T__'215'__426
      T_SimplifierTag_4
      (T__'215'__426
         T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Maybe_10 () (T__'215'__426 Bool T_String_6)
forall a b. a -> b
coe [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Maybe_10 () (T__'215'__426 Bool T_String_6)
d_runCertifierMain_12
d_runCertifierMain_12 ::
  [MAlonzo.Code.Utils.T__'215'__426
     MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__426
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_52
        (MAlonzo.Code.Utils.T__'215'__426
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  Maybe
    (MAlonzo.Code.Utils.T__'215'__426
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
d_runCertifierMain_12 :: [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Maybe_10 () (T__'215'__426 Bool T_String_6)
d_runCertifierMain_12 [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
v0
  = let v1 :: T_Either_6 T_Error_2 T_Σ_14
v1 = [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 ([T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
-> [T__'215'__426
      T_SimplifierTag_4
      (T__'215'__426
         T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
forall a b. a -> b
coe [T__'215'__426
   T_SimplifierTag_4
   (T__'215'__426
      T_Hints_52 (T__'215'__426 T_Untyped_208 T_Untyped_208))]
v0) in
    Any -> T_Maybe_10 () (T__'215'__426 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
v1 of
         MAlonzo.Code.Utils.C_inj'8321'_12 Any
v2
           -> case Any -> T_Error_2
forall a b. a -> b
coe Any
v2 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_SimplifierTag_4
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'__440
                          (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_String_6) -> Any -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_264 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v1)))
                MAlonzo.Code.VerifiedCompilation.C_abort_10 T_SimplifierTag_4
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'__440
                          (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_String_6) -> Any -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_264 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v1)))
                T_Error_2
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
         MAlonzo.Code.Utils.C_inj'8322'_14 Any
v2
           -> (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
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
                   ((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'__440
                      (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_String_6) -> Any -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_264 (T_Either_6 T_Error_2 T_Σ_14 -> Any
forall a b. a -> b
coe T_Either_6 T_Error_2 T_Σ_14
v1))))
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)