module Data.Crystal
import Data.Vect
import Control.Fold
red : Fin (S n) -> Maybe (Fin n)
red (FS t) = Just t
red FZ = Nothing
e' : Nat -> Nat -> Ordering
e' i j = 
    if i == j then GT
    else if j == S i then LT
    else EQ
f' : Nat -> Nat -> Ordering
f' i = contra . e' i
scan : Ordering -> Fin n -> Maybe $ Fin $ S n
scan LT FZ = Nothing
scan LT (FS x) = Just $ weaken $ weaken $ x
scan EQ x = Just $ weaken x
scan GT x = Just $ FS $ x
scanner : Vect 3 (Fin n) -> Ordering -> Vect 3 $ Fin $ S n
scanner [x, y, z] w with (scan w z)
    _ | Nothing = [FS x, FS x, FZ]
    _ | (Just v) = [FS x, weaken y, v]
init : Vect 3 (Fin 1)
init = [FZ, FZ, FZ]
fi : Vect n Ordering -> Fin $ S n
fi x = 
    let [_, p, _] = dfoldl {b = Vect 3 . Fin} scanner init x in 
    rewrite plusCommutative 1 n in p
export
e : {n : Nat} -> Nat -> Vect n Nat -> Maybe $ Vect n Nat
e i x = pure $ replaceAt (complement !(red $ fi $ e' i <$> reverse x)) i x
export
f : Nat -> Vect n Nat -> Maybe $ Vect n Nat
f i x = pure $ replaceAt !(red $ fi $ f' i <$> x) (S i) x