module Data.Crystal

import Data.Fin
import Data.Vect

%default total

-- U_q(\mathcal{g}) q->0 limit
-- idk about superalgebra case
--todo: prove braiding relation
--todo: prove that we change i -> i+1

paren : Nat -> Nat -> Ordering
paren i j = 
    if i == j then GT
    else if j == S i then LT
    else EQ

(+) : Ordering -> Nat -> Maybe Nat
LT + Z = Nothing
LT + (S x) = Just x
EQ + x = Just $ x
GT + x = Just $ S $ x

scan : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)
scan (x, y) (w, z) with (w + y)
    _ | Nothing = (Just z, Z)
    _ | (Just v) = (x, v)

argmin : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n
argmin a = fst $ foldl scan (Nothing, Z) $ zip a $ allFins n

public export
e : {n : Nat} -> Nat -> Vect n Nat -> Maybe $ Vect n Nat
e i x = pure $ replaceAt (complement !(argmin $ paren i <$> reverse x)) i x

public export
f : {n : Nat} -> Nat -> Vect n Nat -> Maybe $ Vect n Nat
f i x = pure $ replaceAt !(argmin $ (contra . paren i) <$> x) (S i) x