[Agda] Closures

[Vag Vagoff]

> 10 seconds for what? The main problem with the compiler (as opposed to
> the type checker) is that it works on normalised terms, which can be
> huge.
>

In Emacs,
5 seconds if compiling/typechecking one module repeatedly,
9-10 seconds if compiling/typechecking one module after working on 
another module.

In command line,
compilation always takes 5 seconds, typechecking always takes 3 seconds.
But after switching from Thunderbird mail agent, for example, it takes 
11 seconds to compile.
Typecheckin still takes 3 seconds after any switching.

Seems like page cache trashing.
> | How to pass types of closed values for closures correctly? It throws 
> messages like type E != type E' for naive approach.
>
> If you explain your problem in more detail, then we may be able to help
> you.
>
Here, in function `execute', arguments of local functions in double pars 
((...)) is added to make compilation successful. Without them compiler 
complains by message " Type Σ != Σ' ".
How to remove arguments in double parenthesis?

module AgdaIsTuringComplete where

    open import Lib

    data LR : Set where
        L : LR
        R : LR

    record Tape (Σ : Set) : Set where
        field
            atLeft : List Σ
            underHead : Σ
            atRight : List Σ
    open Tape

    record TuringMachine (Σ Ω : Set) : Set where
        field
            blank : Σ
            program : Σ × Ω → Maybe (Σ × Ω × LR)
            initial : Ω
    open TuringMachine

    codata Trace (Σ : Set) (Ω : Set) : Set where
        trace : Σ × Ω → Trace Σ Ω → Trace Σ Ω
        traceEnd : Trace Σ Ω

    execute : ∀ {Σ Ω} → List Σ → TuringMachine Σ Ω → Trace Σ Ω
    execute input machine = unwind ((machine)) (loadTape ((machine)) 
input) (initial machine)
     where

        loadTape : ∀ {Σ Ω} → ((TuringMachine Σ Ω)) → List Σ → Tape Σ
        loadTape _ (x ∷ xs) = record { atLeft = [] ; underHead = x ; 
atRight = xs }
        loadTape ((machine)) [] = record { atLeft = [] ; underHead = 
blank machine ; atRight = [] }

        updateTape : ∀ {Σ} → Σ → Tape Σ → Tape Σ
        updateTape symbol tape = record { atLeft = atLeft tape ; 
underHead = symbol ; atRight = atRight tape }

        moveTape : ∀ {Σ Ω} → ((TuringMachine Σ Ω)) → LR → Tape Σ → Tape Σ
        moveTape ((machine)) dir tape with dir | atLeft tape | underHead 
tape | atRight tape
        ... | L | l ∷ ls | x | rs = record { atLeft = ls ; underHead = l 
; atRight = x ∷ rs }
        ... | L | [] | x | rs = record { atLeft = [] ; underHead = blank 
machine ; atRight = x ∷ rs }
        ... | R | ls | x | r ∷ rs = record { atLeft = x ∷ ls ; underHead 
= r ; atRight = rs }
        ... | R | ls | x | [] = record { atLeft = x ∷ ls ; underHead = 
blank machine ; atRight = [] }

        unwind : ∀ {Σ Ω} → ((TuringMachine Σ Ω)) → Tape Σ → Ω → Trace Σ Ω
        unwind ((machine)) tape state with program machine (underHead 
tape , state)
        ... | just (symbol , state' , dir) = trace (underHead tape , 
state) ( unwind ((machine)) (moveTape ((machine)) dir (updateTape symbol 
tape)) state' )
        ... | nothing = traceEnd