Skip to content

Instantly share code, notes, and snippets.

@ahmadsalim

ahmadsalim/CyclicTags.agda

Last active May 8, 2019 05:03
Show Gist options
  • Save ahmadsalim/11077308 to your computer and use it in GitHub Desktop.
Save ahmadsalim/11077308 to your computer and use it in GitHub Desktop.
Download ZIP
Proof that Agda is Turing complete
Raw
CyclicTags.agda
module CyclicTags where
open import Data.Colist as Col
open import Data.Vec as V
open import Data.Fin as F
open import Data.Nat
open import Data.Maybe
open import Coinduction
open import Data.Unit
open import IO
-- Simple type for cyclic tags isomorphic to booleans
data Tag : Set where
`0 : Tag
`1 : Tag
weak-incr : ∀ {n} -> Fin (suc n) -> Maybe (Fin (suc n))
weak-incr {zero} f = nothing
weak-incr {suc n} zero = just (suc zero)
weak-incr {suc n} (suc f) with weak-incr f
weak-incr {suc n} (suc f) | just x = just (suc x)
weak-incr {suc n} (suc f) | nothing = nothing
mod-incr : ∀ {n} -> (Fin (suc n)) -> (Fin (suc n))
mod-incr f with weak-incr f
mod-incr f | just x = x
mod-incr f | nothing = zero
cycle' : ∀ {n} -> (Fin (suc n)) -> Vec (Colist Tag) (suc n) -> Colist Tag -> Colist Tag
cycle' i p [] = []
cycle' i p (`0 ∷ xs) = `0 ∷ ♯ cycle' (mod-incr i) p (♭ xs)
cycle' i p (`1 ∷ xs) = `1 ∷ ♯ cycle' (mod-incr i) p (♭ xs Col.++ V.lookup i p)
cycle : ∀ {n} (productions : Vec (Colist Tag) (suc n)) -> (queue : Colist Tag) -> Colist Tag
cycle = cycle' zero
putTags : Colist Tag -> IO Unit
putTags [] = return unit
putTags (`0 ∷ xs) = ♯ putStrLn "0\n" >> ♯ putTags (♭ xs)
putTags (`1 ∷ xs) = ♯ putStrLn "1\n" >> ♯ putTags (♭ xs)
main = putTags (cycle ((`0 ∷ ♯ (`1 ∷ ♯ (`1 ∷ ♯ [])))
∷ (`1 ∷ ♯ (`0 ∷ ♯ []))
∷ (`1 ∷ ♯ (`0 ∷ ♯ (`1 ∷ ♯ []))) ∷ [])
(`1 ∷ ♯ []))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment