module ModalRewriter where
 open BaseDefinitions.Product
 open BaseDefinitions.Sum
 open BaseDefinitions.Bool
 open BaseDefinitions.Equality.Definition
 open Equality.Properties
 open BaseDefinitions.List
 open Containers.List.Operations
 open BaseDefinitions.Nat
 open BaseDefinitions.Vector
 open BaseDefinitions.Unit
 open Functions.Composition.Definition
 open Boolean.Operations
 open Boolean.Complex
 open Boolean.Conversions
 open BaseDefinitions.BaseTypes.Fin
 open BaseArithmetic
 open BaseArithmetic.Operations
 open BaseArithmetic.Results hiding (_+_)
 open Containers.Maybe.Definition
 open Containers.Maybe.BooleanPredicates
 open Containers.Maybe.Complex
 open Containers.List.BooleanPredicates
 open Containers.Vector.BooleanPredicates
 open Containers.BinTree
 open Character
 open String

 -- rule = pair(input-pattern , output-pattern)
 -- ruleset = list of rules
 -- pick applicable rule
 -- queue semantics
 -- list of tokens
 -- parse string
 --

 data Token : Set where
  const : String → Token
  var : Nat → Token

 TokenEq : Token → Token → Bool
 TokenEq (const c) (const d) = StringEq c d
 TokenEq (const c) x         = false
 TokenEq (var   v) (var   w) = NatEq v w
 TokenEq (var   v) x         = false

 data AST : Set where
  token : Token → AST
  term : List AST → AST

 TermEqHelper : List AST → List AST → Bool
 TermEqHelper [] [] = true
 TermEqHelper (a ∷ as) [] = false
 TermEqHelper []        (b ∷ bs) = false
 TermEqHelper ((token t) ∷ rest) ((token u) ∷ rest2) = TokenEq t u
 TermEqHelper ((token t) ∷ rest) (x ∷ rest2)         = false
 TermEqHelper ((term as) ∷ rest) ((term bs) ∷ rest2) = (TermEqHelper as bs) and (TermEqHelper rest rest2)
 TermEqHelper ((term as) ∷ rest) (x ∷ rest2)         = false

 TermEq : AST → AST → Bool
 TermEq x y = TermEqHelper [ x ] [ y ]

 data AST₂ : Nat → Set where
  token : Token → AST₂ 0
  term : {n : Nat} → List (AST₂ n) → AST₂ (suc n)

 data AST₃ : Nat → Set where
  token : {n : Nat} → Token → AST₃ n
  term : {n : Nat} → List (AST₃ n) → AST₃ (suc n)

 addToken' : {n : Nat} → List Char → List AST → List AST
 addToken' [] ast = ast
 addToken' t  ast = ast ++ [ token (const t) ]

 addToken : {n : Nat} → List Char → Vector (List AST) (suc n) → Vector (List AST) (suc n)
 addToken [] ast = ast
 addToken t  (ast ∷ asts) = (ast ++ [ token (const t) ]) ∷ asts

 merge : { n : Nat} → Vector (List AST) (suc (suc n)) → Vector (List AST) (suc n)
 merge {n} (ast₁ ∷ ast₂ ∷ asts) = (ast₂ ++ [ term ast₁ ]) ∷ asts

 VecFirst : {A : Set} {n : Nat} → Vector A (suc n) → A
 VecFirst (a ∷ as) = a

 getTerm : Vector (List AST) 1 → AST
 getTerm ast = term (VecFirst ast)

 parseState : Nat → Set
 parseState n = List Char × Vector (List AST) (suc n)

 emptyState : parseState 0
 emptyState = ([] , ([] ∷ []))

 doLPAREN : {n : Nat} → parseState n → Maybe (parseState (suc n))
 doLPAREN (t , ast) = Just ([] , ([] ∷ (addToken t ast)))

 doRPAREN2 : {n : Nat} → parseState (suc n) → parseState n
 doRPAREN2 {n} (t , ast) = [] , (merge (addToken t ast))

 doRPAREN : {n : Nat} → parseState n → Maybe (parseState (n - 1))
 doRPAREN {0}     s     = Nothing
 doRPAREN {suc n} s     = coerce (Just (doRPAREN-sub s)) (cong (λ q → Maybe (parseState q)) (n=n-0 n))
  where
   doRPAREN-sub : {m : Nat} → parseState (suc m) → parseState m
   doRPAREN-sub (t , ast) = [] , (merge (addToken t ast))

 doSPACE : {n : Nat} → parseState n → Maybe (parseState n)
 doSPACE (t , ast) = Just ([] , (addToken t ast))

 doCHAR : {n : Nat} → Char → parseState n → Maybe (parseState n)
 doCHAR c (t , ast) = Just ((t ++ [ c ]) , ast)




 -- not the best parser
 -- put them in in reverse order and then just reverse once
 parse : {n : Nat} → List Char → parseState n → Maybe AST
 parse {0}       []       ([] , ([] ∷ [])) = Nothing
 parse {0}       []       (t , ast)         = Just (getTerm (addToken t ast))
 parse {(suc n)} []       state             = Nothing
 parse {n}       (c ∷ x) state             =
  dite
  (checkMaybe (π₂ nextState))
  (λ p → (parse x (extractMaybe (π₂ nextState) p)))
  (λ p → Nothing)
   where
     nextState : ∃ m ∈ Nat , (Maybe (parseState m))
     nextState =
      if         (CharEq c LPAREN) then ((1 + n)    , (doLPAREN state))
       else (if  (CharEq c RPAREN) then ((n - 1)    , (doRPAREN state))
        else (if (CharEq c SPACE ) then (n          , (doSPACE  state))
         else                           (n          , (doCHAR   c state))
      ))


 parseInput : List Char → Maybe AST
 parseInput s = parse s emptyState



 -- disjoint-set roots either: point to some term, or point back to themselves
 -- could alternatively have the vars themselves be trees as in unifying-variables
  -- this is really the underlying data-structure that union-find exploits;
 find-check : {A : Set} {n : Nat} → Vector Bool n → (A ∨ (Vector Bool n)) → Bool
 find-check v (inl a) = true
 find-check v (inr w) = VectorEq BoolEq v w

 {-
 find-helper2 : {A : Set} {n : Nat} → Vector Bool n → (A ∨ (Vector Bool n)) →
 -}

 find-checkLemma : {A : Set} {n : Nat} → (v : Vector Bool n) → (p : (A ∨ (Vector Bool n))) → (find-check v p) ≡ false → ∃ w ∈ (Vector Bool n) , (p ≡ (inr w))
 find-checkLemma {A} {n} v (inl a) ()
 find-checkLemma {A} {n} v (inr w) p = w , refl


 find-checkLemma2 : {A : Set} {n : Nat} → (v : Vector Bool n) → (s : (BinTree (A ∨ (Vector Bool n)) n)) → (find-check v (retrieve s v)) ≡ false → ∃ w ∈ (Vector Bool n) , ((retrieve s v) ≡ (inr w))
 find-checkLemma2 {A} {n} v s p = find-checkLemma v (retrieve s v) p

 check-inl : {A B : Set} → A ∨ B → Bool
 check-inl (inl a) = true
 check-inl (inr b) = false

 check-inr : {A B : Set} → A ∨ B → Bool
 check-inr (inl a) = false
 check-inr (inr b) = true

 extract-inl : {A B : Set} → (p : A ∨ B) → (check-inl p) ≡ true → A
 extract-inl (inl a) p = a
 extract-inl (inr b) ()

 extract-inr : {A B : Set} → (p : A ∨ B) → (check-inr p) ≡ true → B
 extract-inr (inl a) ()
 extract-inr (inr b) p = b


 find-helper : {A : Set} {n : Nat} → BinTree (A ∨ (Vector Bool n)) n → Vector Bool n → List (Vector Bool n) → Nat → Maybe ((Vector Bool n) × (List (Vector Bool n)))
 find-helper s v l 0 = Nothing
 find-helper s v l (suc n) =
  -- check if the retrieved node is a root (constant or self-pointing var), otherwise retrieve again
  dite (find-check v (retrieve s v))
   (λ p → (Just (v , l)))
   (λ p → (find-helper s (π₁ (find-checkLemma2 v s p)) (v ∷ l) n))

 binTree-find : {A : Set} {n : Nat} → BinTree (A ∨ (Vector Bool n)) n → Vector Bool n → Maybe ((Vector Bool n) × (List (Vector Bool n)))
 binTree-find {A} {n} s v = find-helper s v [] (2 ^ n)

 union-helper : {A : Set} {n : Nat} (f : A → A → A) → (a b : A ∨ (Vector Bool n)) → A ∨ (Vector Bool n)
 union-helper {A} f (inl a) (inl b) = inl (f a b)
 union-helper {A} f (inl a) (inr w) = inl a
 union-helper {A} f (inr v) (inl b) = inl b
 union-helper {A} f (inr v) (inr w) = inr v