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