/-
Copyright (c) 2025 Harmonic. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/
import Langlib.Grammars.Unrestricted.Definition
import Langlib.Classes.ContextFree.Definition
import Langlib.Classes.Regular.Definition

/-! # Linear Languages

This file defines the class of linear languages. A linear grammar is a context-free
grammar in which every production has **at most one** nonterminal on the right-hand
side. Equivalently, every rule has the form `A → w` or `A → u B v` where `u`, `v`
are terminal strings and `B` is a nonterminal.

Linear languages sit strictly between the regular and the context-free languages
in the Chomsky hierarchy:

    Regular ⊊ Linear ⊊ Context-Free

## Main declarations

- `linear_output`    — Predicate: a symbol string has at most one nonterminal.
- `grammar_linear`   — Predicate: an unrestricted grammar is linear.
- `is_Linear`        — A language is linear.
- `Linear`           — The class of linear languages.
-/

variable {T : Type}

/-- A symbol string has **linear output form** if it contains at most one nonterminal.
Concretely, it is either a purely terminal string or can be decomposed as
`map terminal u ++ [nonterminal B] ++ map terminal v`. -/
def linear_output {N : Type} (s : List (symbol T N)) : Prop :=
  (∀ x ∈ s, ∃ t, x = symbol.terminal t) ∨
  (∃ (u : List T) (B : N) (v : List T),
    s = List.map symbol.terminal u ++ [symbol.nonterminal B] ++ List.map symbol.terminal v)

/-- An unrestricted grammar is **linear** if every rule is context-free
(empty left/right context) and has linear output. -/
def grammar_linear (g : grammar T) : Prop :=
  ∀ r ∈ g.rules,
    r.input_L = [] ∧ r.input_R = [] ∧ linear_output r.output_string

/-- A language is **linear** if it is generated by some linear unrestricted grammar. -/
def is_Linear (L : Language T) : Prop :=
  ∃ g : grammar T, grammar_linear g ∧ grammar_language g = L

/-- The class of linear languages. -/
def Linear : Set (Language T) :=
  setOf is_Linear