{-# LANGUAGE EmptyDataDecls, EmptyCase, ExistentialQuantification,
             ScopedTypeVariables, NoMonomorphismRestriction, Rank2Types,
             PatternSynonyms #-}
module MAlonzo.Code.Qfasttail where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, eqFloat, add64, sub64,
                    mul64, quot64, rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.IO
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Decidable
import qualified MAlonzo.Code.IO
import qualified MAlonzo.Code.List
import qualified MAlonzo.Code.Nat

name4 = "fasttail.findzero"
d4 :: [Integer] -> MAlonzo.Code.Decidable.T24
d4 v0
  = case coe v0 of
      [] -> coe (\ v1 -> MAlonzo.Code.Decidable.C30) erased
      (:) v1 v2
        -> let v3 = d4 (coe v2) in
           case coe v3 of
             MAlonzo.Code.Decidable.C28 v4
               -> coe
                    (MAlonzo.Code.Decidable.C28
                       (coe (\ v5 v6 v7 -> MAlonzo.Code.List.C110 v7) erased erased v4))
             MAlonzo.Code.Decidable.C30
               -> let v5 = MAlonzo.Code.Nat.d2 (coe (0 :: Integer)) (coe v1) in
                  case coe v5 of
                    MAlonzo.Code.Decidable.C28 v6
                      -> coe
                           (MAlonzo.Code.Decidable.C28
                              (coe
                                 (\ v7 v8 v9 -> MAlonzo.Code.List.C104 v9) erased erased erased))
                    MAlonzo.Code.Decidable.C30
                      -> coe (\ v7 -> MAlonzo.Code.Decidable.C30) erased
                    _ -> MAlonzo.RTE.mazUnreachableError
             _ -> MAlonzo.RTE.mazUnreachableError
      _ -> MAlonzo.RTE.mazUnreachableError
name33 = "fasttail..absurdlambda"
d33 :: MAlonzo.Code.List.T94 -> MAlonzo.Code.Decidable.T2
d33 = erased
name50 = "fasttail.mklist"
d50 :: Integer -> [Integer]
d50 v0
  = case coe v0 of
      0 -> coe
             (MAlonzo.Code.Agda.Builtin.List.C22
                (coe (0 :: Integer)) (coe MAlonzo.Code.Agda.Builtin.List.C16))
      _ -> let v1 = subInt (coe v0) (coe (1 :: Integer)) in
           coe
             (MAlonzo.Code.Agda.Builtin.List.C22 (coe v0) (coe (d50 (coe v1))))
name54 = "fasttail.test"
d54 :: Integer -> [Integer]
d54 v0
  = coe
      (MAlonzo.Code.Agda.Builtin.List.C22
         (coe (0 :: Integer)) (coe (d50 (coe v0))))
name58 = "fasttail.runfindzero"
d58 :: MAlonzo.Code.Agda.Builtin.String.T6
d58
  = let v0 = d4 (coe (d54 (coe (500 :: Integer)))) in
    case coe v0 of
      MAlonzo.Code.Decidable.C28 v1
        -> coe (Data.Text.pack "Found. Done.")
      MAlonzo.Code.Decidable.C30
        -> coe (Data.Text.pack "Not found. Done.")
      _ -> MAlonzo.RTE.mazUnreachableError
main = coe d64
name64 = "fasttail.main"
d64 ::
  MAlonzo.Code.Agda.Builtin.IO.T8
    AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T6
d64
  = coe
      (MAlonzo.Code.IO.du42
         (coe ()) (coe (MAlonzo.Code.IO.d150 (coe d58))))