0 | module Deriving.DepTyCheck.Util.ArgsPerm
 1 |
 2 | import public Data.List.Ex
 3 | import public Data.SortedMap
 4 | import public Data.Vect
 5 |
 6 | import public Decidable.Equality
 7 |
 8 | import public Language.Reflection
 9 | import public Language.Reflection.Syntax
10 | import public Language.Reflection.Syntax.Ops
11 |
12 | import public Syntax.IHateParens.List
13 | import public Syntax.IHateParens.Vect
14 |
15 | %default total
16 |
17 | --------------------------------
18 | --- Permutation of arguments ---
19 | --------------------------------
20 |
21 | export
22 | orderIndices : Ord a => (xs : List a) -> Vect xs.length $ Fin xs.length
23 | orderIndices [] = []
24 | orderIndices xs@(_::_) = do
25 |   let idxMap = SortedMap.fromList $ mapI (sort xs) $ flip $ rewrite sortedPreservesLength xs in (,)
26 |   fromMaybe FZ . lookup' idxMap <$> xs.asVect
27 |   --        ^^ - must never happen, if `Ord` is an order mathematically
28 |   where
29 |     sortedPreservesLength : (xs : List a) -> length (sort xs) = xs.length
30 |     sortedPreservesLength xs = believe_me $ Refl {x=Z} -- in the sake of honesty, we need to prove this
31 |
32 | export
33 | reorder : (perm : Vect n $ Fin n) -> Vect n a -> Vect n a
34 | reorder perm orig = perm <&> flip index orig
35 |
36 | export
37 | reorder' : (xs : List a) -> (perm : Vect xs.length $ Fin xs.length) -> (ys : List a ** ys.length = xs.length)
38 | reorder' orig perm = do
39 |   let xs = reorder perm orig.asVect
40 |   (toList xs ** toListLength xs)
41 |   where
42 |     toList : Vect n a -> List a
43 |     toList []      = []
44 |     toList (x::xs) = x :: toList xs
45 |
46 |     toListLength : (xs : Vect n a) -> length (toList xs) = n
47 |     toListLength []      = Refl
48 |     toListLength (x::xs) = rewrite toListLength xs in Refl
49 |
50 | export
51 | reorder'' : Maybe (n ** Vect n $ Fin n) -> List TTImp -> Maybe $ List TTImp
52 | reorder'' Nothing xs = pure xs
53 | reorder'' (Just (n ** perm)) xs = do
54 |   let Yes prf = decEq (length xs) n | No _ => Nothing
55 |   Just $ fst $ reorder' xs $ rewrite prf in perm
56 |
57 | ||| Produces expression returning a mkdpair in a different order, if needed
58 | |||
59 | ||| Direct means that given expression which returns ascending order, result is permutated; non-direct means vice versa.
60 | export
61 | reorderGend : (direct : Bool) -> {n : _} -> (perm : Vect n $ Fin n) -> TTImp -> TTImp
62 | reorderGend direct perm e = do
63 |   let perm = toList perm
64 |   let all = allFins _
65 |   let False = perm == all | True => e
66 |   let (lhs, rhs) : (_, _) := if direct then (all, perm) else (perm, all)
67 |   let lhs = simpleMkdpair True lhs
68 |   let rhs = simpleMkdpair False rhs
69 |   let lamName : Name := "^lam_arg^"
70 |   `(Prelude.(<&>)) .$ e .$ lam (lambdaArg lamName) (iCase (var lamName) implicitFalse $ pure $ patClause lhs rhs)
71 |   where
72 |     v : (bind : Bool) -> Name -> TTImp
73 |     v bind = if bind then bindVar else var
74 |     simpleMkdpair : (bind : Bool) -> List (Fin n) -> TTImp
75 |     simpleMkdpair bind = foldr (app . (app `(Builtin.DPair.MkDPair)) . v bind . UN . Basic . ("^a" ++) . show) (v bind "^res^")
76 |