-- 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
    field head : A
          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)
  head (repeat a) = 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
  head (zipWith f s t) = f (head s) (head t)
  tail (zipWith f s t) = zipWith f (tail s) (tail t)

  evil : Stream   Stream   Stream 
  evil s t = tail t

  -- Fibonacci

  {-# TERMINATING #-}
  fib : Stream 
  head fib = 0
  head (tail fib) = 1
  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
    field head : A
          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)
  head (repeat a) = 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
  head (zipWith f s t) = f (head s) (head t)
  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 
  head fib = 0
  head (tail fib) = 1
  -- 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 ∅)