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

open import Library

module _ (A : Set) where

infix    _≅_
infix    _∋_
infixl   _∪_
infixl   _·_
infixr  _*

-- Altenkirch, Representation of first-order function types as terminal coalgebras
-- Hinze, Generalizing generalized tries
--
--   (List A → Bool)
--     ≅ (1 + A × List A) → Bool
--     ≅ (1 → Bool) × (A × List A) → Bool
--     ≅ Bool × (A → (List A → Bool))
--
--   Trie A ≅ Bool × (A → Trie A)
--
--   (μ X. 1 + A × X) → Bool ≅ ν Y. Bool × (A → Y)
--

-- A decidable language is a decidable set of words aka dictionary aka trie.

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

-- Word membership (by induction on word)

_∋_ : Lang → (List A → Bool)
l ∋ []     = ν l
l ∋ a ∷ as = δ l a ∋ as

-- Language from word membership (by coinduction)

lang : (List A → Bool) → Lang
ν (lang mem)   = mem []
δ (lang mem) a = lang λ as → mem (a ∷ as)

-- This makes Lang isomophic to (List A → Bool)

-- Constructions of language

-- empty language

∅ : Lang
ν ∅   = false
δ ∅ a = ∅

-- language consisting of the empty word

ε : Lang
ν ε   = true
δ ε a = ∅

-- union of languages

_∪_ : (k l : Lang) → Lang
ν (k ∪ l)   = ν k ∨ ν l
δ (k ∪ l) a = δ k a ∪ δ l a

-- concatenation of languages

{-# TERMINATING #-}
_·_ : (k l : Lang) → Lang
ν (k · l)   = ν k ∧ ν l
δ (k · l) a = if ν k then (δ k a · l) ∪ δ l a else (δ k a · l)

-- Kleene star

{-# TERMINATING #-}
_* : Lang → Lang
ν (l *) = true
δ (l *) a = δ l a · (l *)


-- Bisimilarity

record _≅_ (l k : Lang) : Set where
  coinductive
  field
    ≅ν : ν l ≡ ν k
    ≅δ : (a : A) → δ l a ≅ δ k a
open _≅_ public

-- Equivalence relation laws

≅refl : ∀{l} → l ≅ l
≅ν ≅refl = refl
≅δ ≅refl a = ≅refl

≅sym : ∀{k l} (p : l ≅ k) → k ≅ l
≅ν (≅sym p)   = sym (≅ν p)
≅δ (≅sym p) a = ≅sym (≅δ p a)

≅trans : ∀{k l m} (p : k ≅ l) (q : l ≅ m) → k ≅ m
≅ν (≅trans p q) = trans (≅ν p) (≅ν q)
≅δ (≅trans p q) a = ≅trans (≅δ p a) (≅δ q a)

-- Setoid

≅isEquivalence : IsEquivalence _≅_
IsEquivalence.refl  ≅isEquivalence = ≅refl
IsEquivalence.sym   ≅isEquivalence = ≅sym
IsEquivalence.trans ≅isEquivalence = ≅trans

Bis : Setoid lzero lzero
Setoid.Carrier       Bis = Lang
Setoid._≈_           Bis = _≅_
Setoid.isEquivalence Bis = ≅isEquivalence


union-cong : ∀{k k' l l' : Lang} (p : k ≅ k') (q : l ≅ l') → (k ∪ l) ≅ (k' ∪ l')
≅ν (union-cong p q) rewrite ≅ν p | ≅ν q = refl
≅δ (union-cong p q) a = union-cong (≅δ p a) (≅δ q a)


{-# TERMINATING #-}
dist : (k {l m} : Lang) → k · (l ∪ m) ≅ (k · l) ∪ (k · m)

≅ν (dist k) = ∧-∨-distribˡ (ν k) _ _

≅δ (dist k) a with ν k

≅δ (dist k {l} {m}) a | true = begin
    δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a)
  ≈⟨ union-cong (dist (δ k a)) {!!} ⟩
    (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a)
  ≈⟨ {!!} ⟩
    (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a)
  ∎
  where open EqR Bis

≅δ (dist k) a | false = dist (δ k a)