-- Big Proof @ Newton Institute
-- 30 June 2017
-- Cambridge, UK
--
--   Andreas Abel, Agda Tutorial
--
-- Part 2: Formal languages, coinductively treated via copatterns

{-# OPTIONS --allow-unsolved-metas #-}
{-# OPTIONS --postfix-projections #-}

module Copatterns 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
  cons = {!!}

  -- Stream zipping

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

  -- Fibonacci

  -- {-# TERMINATING #-}
  fib : Stream ℕ
  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
  cons = {!!}

  -- Stream zipping

  zipWith : ∀ {i A B C} (f : A → B → C) (s : Stream i A) (t : Stream i B) → Stream i C
  zipWith = {!!}

  -- Fibonacci

  fib : ∀{i} → Stream i ℕ
  fib = {!!}


module SizedLanguages where

  -- Decidable language

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

  -- empty language

  ∅ : ∀{i A} → Lang i A
  ∅ = {!!}

  -- empty word

  ε : ∀{i A} → Lang i A
  ε = {!!}

  -- union

  infixl  4 _∪_

  _∪_ : ∀{i A} (l k : Lang i A) → Lang i A
  _∪_ = {!!}

  -- concatenation

  infixl  6 _∙_

  _∙_ : ∀{i A} (l k : Lang i A) → Lang i A
  _∙_ = {!!}

  -- star
  infixr 15 _*

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

  -- δ (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 ∅)