{-# 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'__428
     MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           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'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 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'__428
    T_SimplifierTag_4
    (T__'215'__428
       T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> Maybe T_Trace_62)
-> Any -> Any
forall a b. a -> b
coe [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> Maybe T_Trace_62
MAlonzo.Code.VerifiedCompilation.Trace.d_toTrace_80 ([T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> Any
forall a b. a -> b
coe [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 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_62 -> Maybe T_Trace_62) -> Any -> Any
forall a b. a -> b
coe
                    T_Trace_62 -> Maybe T_Trace_62
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_62 -> T_Either_6 T_Error_2 Any) -> Any -> Any
forall a b. a -> b
coe T_Trace_62 -> 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'__428
       MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
       (MAlonzo.Code.Utils.T__'215'__428
          MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_54
          (MAlonzo.Code.Utils.T__'215'__428
             MAlonzo.Code.RawU.T_Untyped_208
             MAlonzo.Code.RawU.T_Untyped_208))) ->
  MAlonzo.Code.Agda.Builtin.List.T_List_10
    () MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_116 ->
  MAlonzo.Code.Agda.Builtin.Maybe.T_Maybe_10
    ()
    (MAlonzo.Code.Utils.T__'215'__428
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
runCertifierMain :: [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_List_10 () T_EvalResult_116
-> T_Maybe_10 () (T__'215'__428 Bool T_String_6)
runCertifierMain = ([T__'215'__428
    T_SimplifierTag_4
    (T__'215'__428
       T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
 -> T_List_10 () T_EvalResult_116
 -> T_Maybe_10 () (T__'215'__428 Bool T_String_6))
-> [T__'215'__428
      T_SimplifierTag_4
      (T__'215'__428
         T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_List_10 () T_EvalResult_116
-> T_Maybe_10 () (T__'215'__428 Bool T_String_6)
forall a b. a -> b
coe [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_List_10 () T_EvalResult_116
-> T_Maybe_10 () (T__'215'__428 Bool T_String_6)
d_runCertifierMain_12
d_runCertifierMain_12 ::
  [MAlonzo.Code.Utils.T__'215'__428
     MAlonzo.Code.VerifiedCompilation.Trace.T_SimplifierTag_4
     (MAlonzo.Code.Utils.T__'215'__428
        MAlonzo.Code.VerifiedCompilation.Trace.T_Hints_54
        (MAlonzo.Code.Utils.T__'215'__428
           MAlonzo.Code.RawU.T_Untyped_208
           MAlonzo.Code.RawU.T_Untyped_208))] ->
  [MAlonzo.Code.VerifiedCompilation.Trace.T_EvalResult_116] ->
  Maybe
    (MAlonzo.Code.Utils.T__'215'__428
       Bool MAlonzo.Code.Agda.Builtin.String.T_String_6)
d_runCertifierMain_12 :: [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_List_10 () T_EvalResult_116
-> T_Maybe_10 () (T__'215'__428 Bool T_String_6)
d_runCertifierMain_12 [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0 T_List_10 () T_EvalResult_116
v1
  = let v2 :: T_Either_6 T_Error_2 T_Σ_14
v2 = [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> T_Either_6 T_Error_2 T_Σ_14
d_runCertifier_2 ([T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
-> [T__'215'__428
      T_SimplifierTag_4
      (T__'215'__428
         T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
forall a b. a -> b
coe [T__'215'__428
   T_SimplifierTag_4
   (T__'215'__428
      T_Hints_54 (T__'215'__428 T_Untyped_208 T_Untyped_208))]
v0) in
    Any -> T_Maybe_10 () (T__'215'__428 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_SimplifierTag_4
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'__442
                          (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_116 -> 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_116 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_290 (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_116 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_116
v1)))
                MAlonzo.Code.VerifiedCompilation.C_abort_10 T_SimplifierTag_4
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'__442
                          (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_116 -> 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_116 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_290 (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_116 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_116
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'__442
                      (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_116 -> 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_116 -> T_String_6
MAlonzo.Code.CertifierReport.d_makeReport_290 (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_116 -> Any
forall a b. a -> b
coe T_List_10 () T_EvalResult_116
v1))))
         T_Either_6 Any Any
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)