{-# 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.Algorithmic.Evaluation 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.Algorithmic
import qualified MAlonzo.Code.Algorithmic.ReductionEC
import qualified MAlonzo.Code.Algorithmic.ReductionEC.Progress
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Utils

-- Algorithmic.Evaluation.Gas
d_Gas_4 :: ()
d_Gas_4 = ()
newtype T_Gas_4 = C_gas_6 Integer
-- Algorithmic.Evaluation.Finished
d_Finished_12 :: p -> p -> ()
d_Finished_12 p
a0 p
a1 = ()
data T_Finished_12
  = C_done_18 MAlonzo.Code.Algorithmic.ReductionEC.T_Value_28 |
    C_out'45'of'45'gas_22 |
    C_error_26 MAlonzo.Code.Algorithmic.ReductionEC.T_Error_338
-- Algorithmic.Evaluation.Steps
d_Steps_30 :: p -> p -> ()
d_Steps_30 p
a0 p
a1 = ()
data T_Steps_30
  = C_steps_38 MAlonzo.Code.Algorithmic.T__'8866'__168
               MAlonzo.Code.Algorithmic.ReductionEC.T__'8212''8608'__780
               T_Finished_12
-- Algorithmic.Evaluation.eval—→
d_eval'8212''8594'_46 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.ReductionEC.T__'8212''8594'__750 ->
  T_Steps_30 -> T_Steps_30
d_eval'8212''8594'_46 :: T__'8866'Nf'8902'__4
-> T__'8866'__168
-> T__'8866'__168
-> T__'8212''8594'__750
-> T_Steps_30
-> T_Steps_30
d_eval'8212''8594'_46 ~T__'8866'Nf'8902'__4
v0 ~T__'8866'__168
v1 T__'8866'__168
v2 T__'8212''8594'__750
v3 T_Steps_30
v4
  = T__'8866'__168 -> T__'8212''8594'__750 -> T_Steps_30 -> T_Steps_30
du_eval'8212''8594'_46 T__'8866'__168
v2 T__'8212''8594'__750
v3 T_Steps_30
v4
du_eval'8212''8594'_46 ::
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.ReductionEC.T__'8212''8594'__750 ->
  T_Steps_30 -> T_Steps_30
du_eval'8212''8594'_46 :: T__'8866'__168 -> T__'8212''8594'__750 -> T_Steps_30 -> T_Steps_30
du_eval'8212''8594'_46 T__'8866'__168
v0 T__'8212''8594'__750
v1 T_Steps_30
v2
  = case T_Steps_30 -> T_Steps_30
forall a b. a -> b
coe T_Steps_30
v2 of
      C_steps_38 T__'8866'__168
v5 T__'8212''8608'__780
v6 T_Finished_12
v7
        -> (T__'8866'__168
 -> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30)
-> T__'8866'__168 -> Any -> T_Finished_12 -> T_Steps_30
forall a b. a -> b
coe
             T__'8866'__168
-> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30
C_steps_38 T__'8866'__168
v5
             ((T__'8866'__168
 -> T__'8212''8594'__750
 -> T__'8212''8608'__780
 -> T__'8212''8608'__780)
-> T__'8866'__168
-> T__'8212''8594'__750
-> T__'8212''8608'__780
-> Any
forall a b. a -> b
coe
                T__'8866'__168
-> T__'8212''8594'__750
-> T__'8212''8608'__780
-> T__'8212''8608'__780
MAlonzo.Code.Algorithmic.ReductionEC.C_trans'8212''8608'_796 T__'8866'__168
v0 T__'8212''8594'__750
v1
                T__'8212''8608'__780
v6)
             T_Finished_12
v7
      T_Steps_30
_ -> T_Steps_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.Evaluation.eval
d_eval_58 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_Gas_4 -> MAlonzo.Code.Algorithmic.T__'8866'__168 -> T_Steps_30
d_eval_58 :: T__'8866'Nf'8902'__4 -> T_Gas_4 -> T__'8866'__168 -> T_Steps_30
d_eval_58 T__'8866'Nf'8902'__4
v0 T_Gas_4
v1 T__'8866'__168
v2
  = case T_Gas_4 -> T_Gas_4
forall a b. a -> b
coe T_Gas_4
v1 of
      C_gas_6 Integer
v3
        -> case Integer -> Integer
forall a b. a -> b
coe Integer
v3 of
             Integer
0 -> (T__'8866'__168
 -> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30)
-> T__'8866'__168 -> Any -> Any -> T_Steps_30
forall a b. a -> b
coe
                    T__'8866'__168
-> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30
C_steps_38 T__'8866'__168
v2
                    (T__'8212''8608'__780 -> Any
forall a b. a -> b
coe T__'8212''8608'__780
MAlonzo.Code.Algorithmic.ReductionEC.C_refl'8212''8608'_786)
                    (T_Finished_12 -> Any
forall a b. a -> b
coe T_Finished_12
C_out'45'of'45'gas_22)
             Integer
_ -> let v4 :: Integer
v4 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                  Any -> T_Steps_30
forall a b. a -> b
coe
                    ((T__'8866'Nf'8902'__4
 -> T_Gas_4 -> T__'8866'__168 -> T_Progress_10 -> T_Steps_30)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                       T__'8866'Nf'8902'__4
-> T_Gas_4 -> T__'8866'__168 -> T_Progress_10 -> T_Steps_30
d_evalProg_64 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) ((Integer -> T_Gas_4) -> Any -> Any
forall a b. a -> b
coe Integer -> T_Gas_4
C_gas_6 (Integer -> Any
forall a b. a -> b
coe Integer
v4)) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2)
                       ((T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Progress_10)
-> Any -> Any -> Any
forall a b. a -> b
coe
                          T__'8866'Nf'8902'__4 -> T__'8866'__168 -> T_Progress_10
MAlonzo.Code.Algorithmic.ReductionEC.Progress.d_progress_86
                          (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v2)))
      T_Gas_4
_ -> T_Steps_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.Evaluation.evalProg
d_evalProg_64 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  T_Gas_4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  MAlonzo.Code.Algorithmic.ReductionEC.Progress.T_Progress_10 ->
  T_Steps_30
d_evalProg_64 :: T__'8866'Nf'8902'__4
-> T_Gas_4 -> T__'8866'__168 -> T_Progress_10 -> T_Steps_30
d_evalProg_64 T__'8866'Nf'8902'__4
v0 T_Gas_4
v1 T__'8866'__168
v2 T_Progress_10
v3
  = case T_Progress_10 -> T_Progress_10
forall a b. a -> b
coe T_Progress_10
v3 of
      MAlonzo.Code.Algorithmic.ReductionEC.Progress.C_step_18 T__'8866'__168
v4 T__'8212''8594'__750
v5
        -> let v6 :: t
v6
                 = (T__'8866'__168
 -> T__'8212''8594'__750 -> T_Steps_30 -> T_Steps_30)
-> Any -> Any -> Any -> t
forall a b. a -> b
coe
                     T__'8866'__168 -> T__'8212''8594'__750 -> T_Steps_30 -> T_Steps_30
du_eval'8212''8594'_46 (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v4) (T__'8212''8594'__750 -> Any
forall a b. a -> b
coe T__'8212''8594'__750
v5)
                     ((T__'8866'Nf'8902'__4 -> T_Gas_4 -> T__'8866'__168 -> T_Steps_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4 -> T_Gas_4 -> T__'8866'__168 -> T_Steps_30
d_eval_58 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) (T_Gas_4 -> Any
forall a b. a -> b
coe T_Gas_4
v1) (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v4)) in
           Any -> T_Steps_30
forall a b. a -> b
coe
             (case T__'8212''8594'__750 -> T__'8212''8594'__750
forall a b. a -> b
coe T__'8212''8594'__750
v5 of
                MAlonzo.Code.Algorithmic.ReductionEC.C_ruleErr_776 T__'8866'Nf'8902'__4
v7 T_EC_476
v9
                  -> case T_EC_476 -> T_EC_476
forall a b. a -> b
coe T_EC_476
v9 of
                       T_EC_476
MAlonzo.Code.Algorithmic.ReductionEC.C_'91''93'_480
                         -> (T__'8866'__168
 -> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              T__'8866'__168
-> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30
C_steps_38
                              ((T__'8866'Nf'8902'__4
 -> T_EC_476 -> T__'8866'__168 -> T__'8866'__168)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                 T__'8866'Nf'8902'__4
-> T_EC_476 -> T__'8866'__168 -> T__'8866'__168
MAlonzo.Code.Algorithmic.ReductionEC.du__'91'_'93''7473'_574
                                 (T__'8866'Nf'8902'__4 -> Any
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) (T_EC_476 -> Any
forall a b. a -> b
coe T_EC_476
MAlonzo.Code.Algorithmic.ReductionEC.C_'91''93'_480)
                                 (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258))
                              (T__'8212''8608'__780 -> Any
forall a b. a -> b
coe T__'8212''8608'__780
MAlonzo.Code.Algorithmic.ReductionEC.C_refl'8212''8608'_786)
                              ((T_Error_338 -> T_Finished_12) -> Any -> Any
forall a b. a -> b
coe
                                 T_Error_338 -> T_Finished_12
C_error_26
                                 (T_Error_338 -> Any
forall a b. a -> b
coe T_Error_338
MAlonzo.Code.Algorithmic.ReductionEC.C_E'45'error_346))
                       T_EC_476
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v6
                T__'8212''8594'__750
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v6)
      MAlonzo.Code.Algorithmic.ReductionEC.Progress.C_done_20 T_Value_28
v4
        -> (T__'8866'__168
 -> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30)
-> T__'8866'__168 -> Any -> Any -> T_Steps_30
forall a b. a -> b
coe
             T__'8866'__168
-> T__'8212''8608'__780 -> T_Finished_12 -> T_Steps_30
C_steps_38 T__'8866'__168
v2
             (T__'8212''8608'__780 -> Any
forall a b. a -> b
coe T__'8212''8608'__780
MAlonzo.Code.Algorithmic.ReductionEC.C_refl'8212''8608'_786)
             ((T_Value_28 -> T_Finished_12) -> T_Value_28 -> Any
forall a b. a -> b
coe T_Value_28 -> T_Finished_12
C_done_18 T_Value_28
v4)
      T_Progress_10
_ -> T_Steps_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Algorithmic.Evaluation.stepper
d_stepper_86 ::
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Algorithmic.T__'8866'__168 ->
  Integer ->
  MAlonzo.Code.Utils.T_Either_6
    MAlonzo.Code.Utils.T_RuntimeError_348
    MAlonzo.Code.Algorithmic.T__'8866'__168
d_stepper_86 :: T__'8866'Nf'8902'__4
-> T__'8866'__168
-> Integer
-> T_Either_6 T_RuntimeError_348 T__'8866'__168
d_stepper_86 T__'8866'Nf'8902'__4
v0 T__'8866'__168
v1 Integer
v2
  = let v3 :: T_Steps_30
v3 = T__'8866'Nf'8902'__4 -> T_Gas_4 -> T__'8866'__168 -> T_Steps_30
d_eval_58 (T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v0) ((Integer -> T_Gas_4) -> Any -> T_Gas_4
forall a b. a -> b
coe Integer -> T_Gas_4
C_gas_6 (Integer -> Any
forall a b. a -> b
coe Integer
v2)) (T__'8866'__168 -> T__'8866'__168
forall a b. a -> b
coe T__'8866'__168
v1) in
    Any -> T_Either_6 T_RuntimeError_348 T__'8866'__168
forall a b. a -> b
coe
      (case T_Steps_30 -> T_Steps_30
forall a b. a -> b
coe T_Steps_30
v3 of
         C_steps_38 T__'8866'__168
v6 T__'8212''8608'__780
v7 T_Finished_12
v8
           -> case T_Finished_12 -> T_Finished_12
forall a b. a -> b
coe T_Finished_12
v8 of
                C_done_18 T_Value_28
v10 -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14 (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
v6)
                T_Finished_12
C_out'45'of'45'gas_22
                  -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                       Any -> Either Any Any
forall {a} {b}. a -> Either a b
MAlonzo.Code.Utils.C_inj'8321'_12
                       (T_RuntimeError_348 -> Any
forall a b. a -> b
coe T_RuntimeError_348
MAlonzo.Code.Utils.C_gasError_350)
                C_error_26 T_Error_338
v10
                  -> (Any -> Either Any Any) -> Any -> Any
forall a b. a -> b
coe
                       Any -> Either Any Any
forall {a} {b}. b -> Either a b
MAlonzo.Code.Utils.C_inj'8322'_14
                       (T__'8866'__168 -> Any
forall a b. a -> b
coe T__'8866'__168
MAlonzo.Code.Algorithmic.C_error_258)
                T_Finished_12
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
         T_Steps_30
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)