{-# OPTIONS --postfix-projections #-}

module _ where

open import Data.List.Base using (List; []; _∷_)

module _ ℓ
  (O : Set ℓ)            -- Propositions.
  (⊥ ⊤ : O)              -- Truth values.
  (_∨_ _∧_ : O → O → O)  -- Binary connectives.
  (¬_ : O → O)           -- Negation.

  (A : Set)              -- Alphabet.
  where

  Word = List A

  -- Dictionary (trie).

  record Lang : Set ℓ where
    coinductive
    field ν : O
          δ : A → Lang
  open Lang public

  -- Lang ≅ (Word → O)

  lookup : Lang → Word → O
  lookup L []      = L .ν
  lookup L (a ∷ w) = lookup (L .δ a) w

  tabulate : (List A → O) → Lang
  tabulate f .ν   = f []
  tabulate f .δ a = tabulate λ w → f (a ∷ w)

  -- Language constructions

  -- Empty language

  const : O → Lang
  const o .ν   = o
  const o .δ a = const o

  ∅ : Lang
  ∅ = const ⊥

  -- Language of everything

  all : Lang
  all = const ⊤

  -- Language of the empty word

  ε : Lang
  ε .ν   = ⊤
  ε .δ a = ∅

  -- Language complement

  map : (O → O) → Lang → Lang
  map f L .ν   = f (L .ν)
  map f L .δ a = map f (L .δ a)

  compl : Lang → Lang
  compl L = map ¬_ L

  -- Language union

  zipWith : (O → O → O) → Lang → Lang → Lang
  zipWith _⊕_ L L' .ν   = L .ν ⊕ L' .ν
  zipWith _⊕_ L L' .δ a = zipWith _⊕_ (L .δ a) (L' .δ a)

  _∪_ : (L L' : Lang) → Lang
  L ∪ L' = zipWith _∨_ L L'

  -- Conditional language
  -- ⊤ & L = L = all ∩ L = const ⊤ ∩ L = map (⊤ ∧_) L
  -- ⊥ & L = ∅ = ∅   ∩ L = const ⊥ ∩ L = map (⊥ ∧_) L

  _&_ : O → Lang → Lang
  o & L = map (o ∧_) L

  -- Language concatenation

  _∙_ : (L L' : Lang) → Lang
  (L ∙ L') .ν   = L .ν ∧ L' .ν
  (L ∙ L') .δ a = (L .δ a ∙ L')
                ∪ (L .ν & L' .δ a)