Testing agda's optimisation

fasttail.agda

-- WARNING: type checking this might crash your computer
open import Decidable
open import List
open import Nat

open import IO
open import Agda.Builtin.String

findzero : ∀ xs → Dec (zero ∈ xs)
findzero [] = no (λ ())
findzero (x ∷ xs) with findzero xs
...               | yes found = yes (x ∷ found)
...               | no ¬found with natEq zero x
...                           | yes refl = yes [ refl ]
...                           | no  0≢x  = no λ { [ 0≡x ] → 0≢x 0≡x
                                                ; (_ ∷ found) → ¬found found }

mklist : ℕ → List ℕ
mklist zero = zero ∷ []
mklist (suc n) = suc n ∷ mklist n

test : ℕ → List ℕ
test n = zero ∷ (mklist n)

runfindzero : String
runfindzero with findzero (test 500000)
...         | yes _ = "Found. Done."
...         | no  _ = "Not found. Done."

main = run (putStrLn runfindzero)

head.agda

open import Decidable
open import List
open import Nat

open import IO
open import Agda.Builtin.String

findzero : ∀ xs → Dec (zero ∈ xs)
findzero [] = no (λ ())
findzero (x ∷ xs) with natEq zero x
...               | yes refl = yes [ refl ]
...               | no  0≢x  with findzero xs
...                          | yes found = yes (x ∷ found)
...                          | no ¬found = no λ { [ 0≡x ] → 0≢x 0≡x
                                                ; (_ ∷ found) → ¬found found }

mklist : ℕ → List ℕ
mklist zero = zero ∷ []
mklist (suc n) = suc n ∷ mklist n

test : ℕ → List ℕ
test n = zero ∷ (mklist n)

runfindzero : ℕ → String
runfindzero n with findzero (test n)
...           | yes _ = "Found. Done."
...           | no  _ = "Not found. Done."

main = run (putStrLn (runfindzero 500000))

Qfasttail.hs

{-# 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))))

Qtail.hs

{-# LANGUAGE EmptyDataDecls, EmptyCase, ExistentialQuantification,
             ScopedTypeVariables, NoMonomorphismRestriction, Rank2Types,
             PatternSynonyms #-}
module MAlonzo.Code.Qtail 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 = "tail.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 = "tail..absurdlambda"
d33 :: MAlonzo.Code.List.T94 -> MAlonzo.Code.Decidable.T2
d33 = erased
name50 = "tail.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 = "tail.test"
d54 :: Integer -> [Integer]
d54 v0
  = coe
      (MAlonzo.Code.Agda.Builtin.List.C22
         (coe (0 :: Integer)) (coe (d50 (coe v0))))
name58 = "tail.runfindzero"
d58 :: Integer -> MAlonzo.Code.Agda.Builtin.String.T6
d58 v0
  = let v1 = d4 (coe (d54 (coe v0))) in
    case coe v1 of
      MAlonzo.Code.Decidable.C28 v2
        -> coe (Data.Text.pack "Found. Done.")
      MAlonzo.Code.Decidable.C30
        -> coe (Data.Text.pack "Not found. Done.")
      _ -> MAlonzo.RTE.mazUnreachableError
main = coe d70
name70 = "tail.main"
d70 ::
  MAlonzo.Code.Agda.Builtin.IO.T8
    AgdaAny MAlonzo.Code.Agda.Builtin.Unit.T6
d70
  = coe
      (MAlonzo.Code.IO.du42
         (coe ())
         (coe (MAlonzo.Code.IO.d150 (coe (d58 (coe (509000 :: Integer)))))))

tail.agda

open import Decidable
open import List
open import Nat

open import IO
open import Agda.Builtin.String

findzero : ∀ xs → Dec (zero ∈ xs)
findzero [] = no (λ ())
findzero (x ∷ xs) with findzero xs
...               | yes found = yes (x ∷ found)
...               | no ¬found with natEq zero x
...                           | yes refl = yes [ refl ]
...                           | no  0≢x  = no λ { [ 0≡x ] → 0≢x 0≡x
                                                ; (_ ∷ found) → ¬found found }

mklist : ℕ → List ℕ
mklist zero = zero ∷ []
mklist (suc n) = suc n ∷ mklist n

test : ℕ → List ℕ
test n = zero ∷ (mklist n)

runfindzero : ℕ → String
runfindzero n with findzero (test n)
...           | yes _ = "Found. Done."
...           | no  _ = "Not found. Done."

main = run (putStrLn (runfindzero 500000))