-- 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 = 
  head (tail fib) = 
  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 = 
  head (tail fib) = 
  -- 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   _∪_

  _∪_ : ∀{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   _∪_

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

  -- concatenation

  infixl   _∙_

  _∙_ : ∀{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  _*

  _* : ∀{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 ∅)