leesongun/SuperCombinatorics - Change CMHGXE7Y2WB5BVYQWGKXKVUGPURGAZVX75HGZ6DDZVUOHAFFKNNAC

concise implementation (type theoretically and computationally slightly worse)

Created by leesongun on March 10, 2023

CMHGXE7Y2WB5BVYQWGKXKVUGPURGAZVX75HGZ6DDZVUOHAFFKNNAC

Dependencies

[2] VLK55FT2FAYBLPUG4RXT3MWIERJZCOIMLWIXQ5LHUZU6DO2MK4XQC

In channels

main

Change contents

Insertion in Data/Crystal.idr at line 3 [2.36]
[2.58]
[2.58]
```
import Data.Fin
```
Deletion in Data/Crystal.idr at line 5 [2.36]
B:BD[2.75] → [2.75:95]
```
import Control.Fold
```
Replacement in Data/Crystal.idr at line 6 [2.36]
B:BD[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.36]

B:BD[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.36]

B:BD[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.36]

B:BD[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.36]

B:BD[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.36]

B:BD[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.36]

B:BD[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