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

module _ where

-- open import Data.List.Base using (List; []; _∷_)
open import Size
open import Function using (_∘_)

variable i : Size

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

  (A : Set)              -- Alphabet.
  where

  data Word : Size → Set where
    []  : Word i
    _∷_ : (a : A) (w : Word i) → Word (↑ i)

  -- Language.

  Lang = λ i → Word i → O

  ν : Lang i → O
  ν L = L []

  δ : Lang (↑ i) → A → Lang i
  δ L a = λ w → L (a ∷ w)

  -- Language constructions

  -- Empty language

  const : O → Lang i
  const o _ = o

  ∅ : Lang i
  ∅ = const ⊥

  -- Language of everything

  all : Lang i
  all = const ⊤

  -- Language of the empty word

  ε : Lang i
  ε []      = ⊤
  ε (a ∷ w) = ⊥

  -- Language complement

  map : (O → O) → Lang i → Lang i
  map f L = f ∘ L

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

  -- Language union

  zipWith : (O → O → O) → Lang i → Lang i → Lang i
  zipWith _⊕_ L L' w   = L w ⊕ L' w

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

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

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

  -- Language concatenation

  _∙_ : (L L' : Lang i) → Lang i
  (L ∙ L') []      = L [] ∧ L' []
  (L ∙ L') (a ∷ w) = (L [] ∧ L' (a ∷ w)) ∨ (δ L a ∙ L') w

  -- Language iteration (Kleene star)

  _* : Lang i → Lang i
  (L *) []      = ⊤
  (L *) (a ∷ w) = (δ L a ∙ (L *)) w

-- -}
-- -}
-- -}
-- -}
-- -}