+ 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