module Data.Crystal
import Data.List
import Data.Maybe
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 . f' i
scan : Ordering -> Nat -> Maybe Nat
scan LT Z = Nothing
scan LT (S x) = Just x 
scan EQ x = Just x
scan GT x = Just $ S $ x
scanner : (Nat, Nat, Nat) -> Ordering -> (Nat, Nat, Nat) 
scanner (x, y, z) w with (scan w z)
    _ | Nothing = (S x, S x, Z)
    _ | (Just v) = (S x, y, v)
fi : List Ordering -> Maybe Nat
fi x = let (_, p, _) = foldl scanner (0,0,0) x in p
export
e : Nat -> List Nat -> Maybe $ List Nat
export
f : Nat -> List Nat -> Maybe $ List Nat
f i x = pure $ replaceAt !(scan LT $ fi $ f' i <$> x) (S i) x @{?idris_baka}