import Langlib.Grammars.ContextSensitive.Toolbox
import Langlib.Utilities.ListUtils


/-! # Context-Sensitive Examples

This file contains example context-sensitive grammars and sample derivation proofs.

## Main declarations

- `Te`
- `Nt`
-/

inductive Te
  | a_ : Te
  | b_ : Te
  | c_ : Te
  deriving DecidableEq

inductive Nt
  | B_ : Nt
  | C_ : Nt
  | R_ : Nt
  | S_ : Nt
  | X_ : Nt
  | Y_ : Nt
  | Z_ : Nt
  deriving DecidableEq

private def a : symbol Te Nt := symbol.terminal Te.a_
private def b : symbol Te Nt := symbol.terminal Te.b_
private def c : symbol Te Nt := symbol.terminal Te.c_

private def B : symbol Te Nt := symbol.nonterminal Nt.B_
private def C : symbol Te Nt := symbol.nonterminal Nt.C_
private def R : symbol Te Nt := symbol.nonterminal Nt.R_
private def S : symbol Te Nt := symbol.nonterminal Nt.S_
private def X : symbol Te Nt := symbol.nonterminal Nt.X_
private def Y : symbol Te Nt := symbol.nonterminal Nt.Y_
private def Z : symbol Te Nt := symbol.nonterminal Nt.Z_


/-- rule `S → aSBC | aRC` as two context-sensitive rules -/
private def r₁ : csrule Te Nt := csrule.mk [] Nt.S_ [] [a, S, B, C]
private def r₂ : csrule Te Nt := csrule.mk [] Nt.S_ [] [a, R, C]

/-- non-contracting rule `CB → BC` modelled by `CB → XB → XC → BC` which is context-sensitive -/
private def r₃  : csrule Te Nt := csrule.mk [] Nt.C_ [B] [X]
private def r₃' : csrule Te Nt := csrule.mk [X] Nt.B_ [] [C]
private def r₃'': csrule Te Nt := csrule.mk [] Nt.X_ [C] [B]

/-- non-contracting rule `RB → bR` modelled by `RB → YB → YR → bR` which is context-sensitive -/
private def r₄  : csrule Te Nt := csrule.mk [] Nt.R_ [B] [Y]
private def r₄' : csrule Te Nt := csrule.mk [Y] Nt.B_ [] [R]
private def r₄'': csrule Te Nt := csrule.mk [] Nt.Y_ [R] [b]

/-- non-contracting rule `RC → bc` modelled by `RC → ZC → Zc → bc` which is context-sensitive -/
private def r₅  : csrule Te Nt := csrule.mk [] Nt.R_ [C] [Z]
private def r₅' : csrule Te Nt := csrule.mk [Z] Nt.C_ [] [c]
private def r₅'': csrule Te Nt := csrule.mk [] Nt.Z_ [c] [b]

/-- context-sensitive rule `cC → cc` -/
private def r₆ : csrule Te Nt := csrule.mk [c] Nt.C_ [] [c]


private def my_grammar : CS_grammar Te :=
  CS_grammar.mk Nt Nt.S_ [r₁, r₂, r₃, r₃', r₃'', r₄, r₄', r₄'', r₅, r₅', r₅'', r₆]
    (by intro r hr
        simp only [List.mem_cons, List.mem_nil_iff, or_false] at hr
        rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;>
          simp [r₁, r₂, r₃, r₃', r₃'', r₄, r₄', r₄'', r₅, r₅', r₅'', r₆])


-- A macro for performing one context-sensitive derivation step (with continuation).
macro "CS_step" rule:term "," pref:term "," post:term : tactic =>
  `(tactic| (
    apply CS_deri_of_tran_deri
    · refine ⟨$rule, $pref, $post, ?_, ?_, ?_⟩
      · simp [my_grammar]
      · rfl
      · rfl
  ))


/-- generate `abc` by the grammar above -/
example : [Te.a_, Te.b_, Te.c_] ∈ CS_language my_grammar := by
  CS_step r₂, [], []
  CS_step r₅, [a], []
  CS_step r₅', [a], []
  apply CS_deri_of_tran
  · refine ⟨r₅'', [a], [], ?_, ?_, ?_⟩
    · simp [my_grammar]
    · rfl
    · rfl


/-- generate `aabbcc` by the grammar above -/
example : [Te.a_, Te.a_, Te.b_, Te.b_, Te.c_, Te.c_] ∈ CS_language my_grammar := by
  -- S
  CS_step r₁, [], []
  -- aSBC
  CS_step r₂, [a], [B, C]
  -- aaRCBC
  CS_step r₃,   [a, a, R], [C]
  CS_step r₃',  [a, a, R], [C]
  CS_step r₃'', [a, a, R], [C]
  -- aaRBCC
  CS_step r₄,   [a, a], [C, C]
  CS_step r₄',  [a, a], [C, C]
  CS_step r₄'', [a, a], [C, C]
  -- aabRCC
  CS_step r₅,   [a, a, b], [C]
  CS_step r₅',  [a, a, b], [C]
  CS_step r₅'', [a, a, b], [C]
  -- aabbcC
  CS_step r₆, [a, a, b, b], []
  -- aabbcc
  apply CS_deri_self


-- A macro for the three combined steps of rule r₃ (CB → BC).
macro "combined_steps_r₃" pre:term "," pos:term : tactic =>
  `(tactic| (
    CS_step r₃,   $pre, $pos
    CS_step r₃',  $pre, $pos
    CS_step r₃'', $pre, $pos
  ))

-- A macro for the three combined steps of rule r₄ (RB → bR).
macro "combined_steps_r₄" pre:term "," pos:term : tactic =>
  `(tactic| (
    CS_step r₄,   $pre, $pos
    CS_step r₄',  $pre, $pos
    CS_step r₄'', $pre, $pos
  ))

/-- generate `aaabbbccc` by the grammar above -/
example : [Te.a_, Te.a_, Te.a_, Te.b_, Te.b_, Te.b_, Te.c_, Te.c_, Te.c_]
    ∈ CS_language my_grammar := by
  -- S
  CS_step r₁, [], []
  -- aSBC
  CS_step r₁, [a], [B, C]
  -- aaSBCBC
  CS_step r₂, [a, a], [B, C, B, C]
  -- aaaRCBCBC
  combined_steps_r₃ [a, a, a, R], [C, B, C]
  -- aaaRBCCBC
  combined_steps_r₃ [a, a, a, R, B, C], [C]
  -- aaaRBCBCC
  combined_steps_r₃ [a, a, a, R, B], [C, C]
  -- aaaRBBCCC
  combined_steps_r₄ [a, a, a], [B, C, C, C]
  -- aaabRBCCC
  combined_steps_r₄ [a, a, a, b], [C, C, C]
  -- aaabbRCCC
  CS_step r₅,   [a, a, a, b, b], [C, C]
  CS_step r₅',  [a, a, a, b, b], [C, C]
  CS_step r₅'', [a, a, a, b, b], [C, C]
  -- aaabbbcCC
  CS_step r₆, [a, a, a, b, b, b], [C]
  -- aaabbbccC
  CS_step r₆, [a, a, a, b, b, b, c], []
  -- aaabbbccc
  apply CS_deri_self


/-- generate ` a^4 . b^4 . c^4 ` by the grammar above -/
example : [Te.a_, Te.a_, Te.a_, Te.a_,
           Te.b_, Te.b_, Te.b_, Te.b_,
           Te.c_, Te.c_, Te.c_, Te.c_]
    ∈ CS_language my_grammar := by
  -- .S.
  CS_step r₁, [], []
  -- .aSBC.

  -- a.S.BC
  CS_step r₁, [a], [B, C]
  -- a.aSBC.BC

  -- aa.S.BCBC
  CS_step r₁, [a, a], [B, C, B, C]
  -- aa.aSBC.BCBC

  -- aaa.S.BCBCBC
  CS_step r₂, [a, a, a], [B, C, B, C, B, C]
  -- aaa.aRC.BCBCBC

  -- aaaaR.CB.CBCBC
  combined_steps_r₃ [a, a, a, a, R], [C, B, C, B, C]
  -- aaaaR.BC.CBCBC

  -- aaaaRBC.CB.CBC
  combined_steps_r₃ [a, a, a, a, R, B, C], [C, B, C]
  -- aaaaRBC.BC.CBC

  -- aaaaRB.CB.CCBC
  combined_steps_r₃ [a, a, a, a, R, B], [C, C, B, C]
  -- aaaaRB.BC.CCBC

  -- aaaaRBBCC.CB.C
  combined_steps_r₃ [a, a, a, a, R, B, B, C, C], [C]
  -- aaaaRBBCC.BC.C

  -- aaaaRBBC.CB.CC
  combined_steps_r₃ [a, a, a, a, R, B, B, C], [C, C]
  -- aaaaRBBC.BC.CC

  -- aaaaRBB.CB.CCC
  combined_steps_r₃ [a, a, a, a, R, B, B], [C, C, C]
  -- aaaaRBB.BC.CCC

  -- aaaa.RB.BBCCCC
  combined_steps_r₄ [a, a, a, a], [B, B, C, C, C, C]
  -- aaaa.bR.BBCCCC

  -- aaaab.RB.BCCCC
  combined_steps_r₄ [a, a, a, a, b], [B, C, C, C, C]
  -- aaaab.bR.BCCCC

  -- aaaabb.RB.CCCC
  combined_steps_r₄ [a, a, a, a, b, b], [C, C, C, C]
  -- aaaabb.bR.CCCC

  -- aaaabbb.RC.CCC
  CS_step r₅,   [a, a, a, a, b, b, b], [C, C, C]
  -- aaaabbb.ZC.CCC
  CS_step r₅',  [a, a, a, a, b, b, b], [C, C, C]
  -- aaaabbb.Zc.CCC
  CS_step r₅'', [a, a, a, a, b, b, b], [C, C, C]
  -- aaaabbb.bc.CCC

  -- aaaabbbb.cC.CC
  CS_step r₆, [a, a, a, a, b, b, b, b], [C, C]
  -- aaaabbbb.cc.CC

  -- aaaabbbbc.cC.C
  CS_step r₆, [a, a, a, a, b, b, b, b, c], [C]
  -- aaaabbbbc.cc.C

  -- aaaabbbbcc.cC.
  CS_step r₆, [a, a, a, a, b, b, b, b, c, c], []
  -- aaaabbbbcc.cc.

  apply CS_deri_self