```-- Autumn school "Proof and Computation"
-- 3-8 October 2016
-- Fischbachau, Bayern, DE
--
--   Andreas Abel, Agda Tutorial
--
-- Part 2: Formal languages, coinductively treated via copatterns

module CopatternsSolution where

open import Data.Nat.Base
open import Data.Bool.Base

open import Relation.Binary.PropositionalEquality

open import Size

module Streams where

-- Streams
record Stream (A : Set) : Set where
coinductive
tail : Stream A
open Stream

-- Constructor
cons : {A : Set} (a : A) (as : Stream A) → Stream A
head (cons a as) = a
tail (cons a as) = as

-- Repetition

repeat : {A : Set} (a : A) → Stream A
-- repeat a = cons a (repeat a)
tail (repeat a) = repeat a

-- C-c C-c split on result

-- Stream zipping

zipWith : {A B C : Set} (f : A → B → C) (s : Stream A) (t : Stream B) → Stream C
tail (zipWith f s t) = zipWith f (tail s) (tail t)

evil : Stream ℕ → Stream ℕ → Stream ℕ
evil s t = tail t

-- Fibonacci

{-# TERMINATING #-}
fib : Stream ℕ
tail (tail fib) = zipWith (_+_) fib (tail fib)
-- Termination hinges on the continuity of zipWith.
-- Compare with the similarly structured rhs
--   tail (tail fib) = evil fib (tail fib)
-- to understand why Agda refuses to certify termination
-- in the untyped termination checker.

module SizedStreams where

-- Streams
record Stream (i : Size) (A : Set) : Set where
coinductive
tail : ∀{j : Size< i} → Stream j A
open Stream

-- Constructor
cons : {i : Size} {A : Set} (a : A) (as : Stream i A) → Stream (↑ i) A
head (cons a as) = a
tail (cons a as) = as

-- Repetition

repeat : {i : Size} {A : Set} (a : A) → Stream i A
-- repeat {i} a = cons {i} a (repeat {i} a)
tail (repeat {i} a) {j} = repeat {j} a

-- C-c C-c split on result

-- Stream zipping
zipWith : ∀ {i A B C} (f : A → B → C) (s : Stream i A) (t : Stream i B) → Stream i C
tail (zipWith {i} f s t) {j} = zipWith f (tail s {j}) (tail t {j})

-- evil : ∀{i} → Stream i ℕ → Stream i ℕ → Stream i ℕ
-- evil s t = tail t

-- Fibonacci

fib : ∀{i} → Stream i ℕ
-- tail (tail fib) = evil fib (tail fib)
tail (tail (fib {i}) {j}) {k} =  zipWith (_+_) (fib {k}) (tail (fib {j}))

module Languages where

-- Decidable language

record Lang (A : Set) : Set where
coinductive
field ν : Bool
δ : A → Lang A
open Lang

-- empty language

∅ : ∀{A} → Lang A
ν ∅ = false
δ ∅ a = ∅

-- empty word

ε : ∀{A} → Lang A
ν ε = true
δ ε x = ∅

-- union

infixl  4 _∪_

_∪_ : ∀{A} (l k : Lang A) → Lang A
ν (l ∪ k)   = ν l ∨ ν k
δ (l ∪ k) x = δ l x ∪ δ k x

-- concatenation

-- infixl  6 _∙_

-- _∙_ : ∀{A} (l k : Lang A) → Lang A
-- ν (l ∙ k) = ν l ∧ ν k
-- δ (l ∙ k) x = if ν l then δ l x ∙ k ∪ δ k x else δ l x ∙ k

-- star
-- infixr 15 _*

-- _* : ∀{A} (l : Lang A) → Lang A
-- l * =  {!!}

module SizedLanguages where

-- Decidable language

record Lang (i : Size) (A : Set) : Set where
coinductive
field ν : Bool
δ : ∀{j : Size< i} → A → Lang j A
open Lang

-- empty language

∅ : ∀{i A} → Lang i A
ν ∅ = false
δ ∅ a = ∅

-- empty word

ε : ∀{i A} → Lang i A
ν ε = true
δ ε x = ∅

-- union

infixl  4 _∪_

_∪_ : ∀{i A} (l k : Lang i A) → Lang i A
ν (l ∪ k)   = ν l ∨ ν k
δ (l ∪ k) x = δ l x ∪ δ k x

-- concatenation

infixl  6 _∙_

_∙_ : ∀{i A} (l k : Lang i A) → Lang i A
ν (l ∙ k)   = ν l ∧ ν k
δ (l ∙ k) x = if ν l then δ l x ∙ k ∪ δ k x else δ l x ∙ k

-- star
infixr 15 _*

_* : ∀{i A} (l : Lang i A) → Lang i A
ν (l *)   = true
δ (l *) x = δ l x ∙ l *

-- δ (l *) x = δ (ε ∪ l ∙ l *) x
--           = δ ε x ∪ δ (l ∙ l *) x
--           = ∅ ∪ δ l x ∙ l * ∪ (if ν l then δ (l *) x else ∅)
--           = δ l x ∙ l * ∪ (if ν l then δ (l *) x else ∅)
```