concise implementation (type theoretically and computationally slightly worse)

leesongun

Mar 10, 2023, 11:29 PM

CMHGXE7Y2WB5BVYQWGKXKVUGPURGAZVX75HGZ6DDZVUOHAFFKNNAC

Dependencies

• [2] VLK55FT2 initial implementation of crystal operators

Change contents

• edit in Data/Crystal.idr at line 3
  [2.58]

  [2.58]
  + import Data.Fin
• edit in Data/Crystal.idr at line 5
  [2.75]→[2.75:95](∅→∅)
  − import Control.Fold
• replacement in Data/Crystal.idr at line 6
  [2.96]→[2.96:166](∅→∅)
  − red : Fin (S n) -> Maybe (Fin n)

  − red (FS t) = Just t

  − red FZ = Nothing
  [2.96]

  [2.166]
  + %default total
• replacement in Data/Crystal.idr at line 17
  [2.319]→[2.319:484](∅→∅)
  − 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
  [2.319]

  [2.484]
  + 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
• replacement in Data/Crystal.idr at line 23
  [2.485]→[2.485:654](∅→∅)
  − 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]
  [2.485]

  [2.654]
  + scanner : (Maybe $ Fin n, Nat) -> (Ordering, Fin n) -> (Maybe $ Fin n, Nat)

  + scanner (x, y) (w, z) with (scan w y)

  + _ | Nothing = (Just z, Z)

  + _ | (Just v) = (x, v)
• replacement in Data/Crystal.idr at line 28
  [2.655]→[2.655:697](∅→∅)
  − init : Vect 3 (Fin 1)

  − init = [FZ, FZ, FZ]
  [2.655]

  [2.697]
  + fi : {n : Nat} -> Vect n Ordering -> Maybe $ Fin n

  + fi a = fst $ foldl scanner (Nothing, Z) $ zip a $ allFins n
• replacement in Data/Crystal.idr at line 31
  [2.698]→[2.698:850](∅→∅)
  − 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
  [2.698]

  [2.850]
  + public export
• replacement in Data/Crystal.idr at line 33
  [2.907]→[2.907:982](∅→∅)
  − e i x = pure $ replaceAt (complement !(red $ fi $ e' i <$> reverse x)) i x
  [2.907]

  [2.982]
  + e i x = pure $ replaceAt (complement !(fi $ e' i <$> reverse x)) i x
• replacement in Data/Crystal.idr at line 35
  [2.983]→[2.983:1092](∅→∅)
  − export

  − f : Nat -> Vect n Nat -> Maybe $ Vect n Nat

  − f i x = pure $ replaceAt !(red $ fi $ f' i <$> x) (S i) x
  [2.983]
  + public export

  + f : {n : Nat} -> Nat -> Vect n Nat -> Maybe $ Vect n Nat

  + f i x = pure $ replaceAt !(fi $ f' i <$> x) (S i) x