Try write correct inverse permutation function (incomplete)exper-invperm-proof

1 files changed, 77 insertions, 12 deletions

diff --git a/src/Data/Array/Mixed.hs b/src/Data/Array/Mixed.hs
index 3efa6a3..089e35b 100644
--- a/src/Data/Array/Mixed.hs
+++ b/src/Data/Array/Mixed.hs
@@ -24,6 +24,10 @@
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
 {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
+
+
+
+{-# LANGUAGE EmptyCase #-}
 module Data.Array.Mixed where
 
 import Control.DeepSeq (NFData(..))
@@ -38,6 +42,7 @@ import Data.Monoid (Sum(..))
 import Data.Proxy
 import Data.Type.Bool
 import Data.Type.Equality
+import Data.Type.Ord
 import qualified Data.Vector.Storable as VS
 import Foreign.Storable (Storable)
 import GHC.Generics (Generic)
@@ -764,21 +769,81 @@ ssxIndex p1 p2 = coerce (listxIndex @(SMayNat () SNat) p1 p2)
 ssxPermutePrefix :: HList SNat is -> StaticShX sh -> StaticShX (PermutePrefix is sh)
 ssxPermutePrefix = coerce (listxPermutePrefix @(SMayNat () SNat))
 
-shTakeLen :: forall is sh. HList SNat is -> IShX sh -> IShX (TakeLen is sh)
-shTakeLen = coerce (listxTakeLen @(SMayNat Int SNat))
-
-shDropLen :: HList SNat is -> IShX sh -> IShX (DropLen is sh)
-shDropLen = coerce (listxDropLen @(SMayNat Int SNat))
-
-shPermute :: HList SNat is -> IShX sh -> IShX (Permute is sh)
-shPermute = coerce (listxPermute @(SMayNat Int SNat))
-
-shIndex :: Proxy is -> Proxy shT -> SNat i -> IShX sh -> IShX (Permute is shT) -> IShX (Index i sh : Permute is shT)
-shIndex p1 p2 = coerce (listxIndex @(SMayNat Int SNat) p1 p2)
-
 shPermutePrefix :: HList SNat is -> IShX sh -> IShX (PermutePrefix is sh)
 shPermutePrefix = coerce (listxPermutePrefix @(SMayNat Int SNat))
 
+type family InversePerm perm where
+  InversePerm perm = InversePerm' 0 perm perm
+
+type family InversePerm' i ref perm where
+  InversePerm' n '[] perm = '[]
+  InversePerm' i (_ : ref) perm = FindIndex 0 i perm : InversePerm' (i + 1) ref perm
+
+type family FindIndex i tgt list where
+  FindIndex i tgt (tgt : _) = i
+  FindIndex i tgt (_ : list) = FindIndex (i + 1) tgt list
+
+lemSuccLeqZero :: Proxy i -> (i + 1 <=? 0) :~: False
+lemSuccLeqZero _ = unsafeCoerce Refl
+
+lemIndexPermute :: forall j is sh.
+                   Proxy sh -> SNat j -> HList SNat is -> (j + 1 <=? Rank is) :~: True
+                -> Index j (Permute is sh) :~: Index (Index j is) sh
+lemIndexPermute _ _ HNil Refl = case lemSuccLeqZero (Proxy @j) of {}
+lemIndexPermute _ SZ HCons{} _ = Refl
+lemIndexPermute psh (SS (jm1nat :: SNat jm1)) (HCons (SNat :: SNat i0) (perm :: HList SNat isT)) Refl
+  | Refl <- lemIndexSucc (Proxy @jm1) (Proxy @(Index i0 sh)) (Proxy @(Permute isT sh))
+  , Refl <- lemIndexSucc (Proxy @jm1) (Proxy @i0) (Proxy @isT)
+  = lemIndexPermute psh jm1nat perm Refl
+
+lemFindIndexNeq1 :: Compare tgt n ~ LT
+                 => Proxy i -> Proxy tgt -> Proxy n -> Proxy list
+                 -> FindIndex i tgt (n : list) :~: FindIndex (i + 1) tgt list
+lemFindIndexNeq1 _ _ _ _ = unsafeCoerce Refl
+
+lemFindIndexNeq2 :: Compare tgt n ~ GT
+                 => Proxy i -> Proxy tgt -> Proxy n -> Proxy list
+                 -> FindIndex i tgt (n : list) :~: FindIndex (i + 1) tgt list
+lemFindIndexNeq2 _ _ _ _ = unsafeCoerce Refl
+
+-- lemAllElemSplit :: AllElem (Count i )
+
+hlistFindIndex :: forall i tgt list. AllElem' (Count i (Rank list)) list ~ True
+               => SNat i -> SNat tgt -> HList SNat list
+               -> SNat (FindIndex i tgt list)
+hlistFindIndex inat@SNat tgtnat@SNat HNil = _
+hlistFindIndex inat@SNat tgtnat@SNat (HCons n@(SNat :: SNat n) (list :: HList SNat listT)) = case cmpNat tgtnat n of
+  EQI -> inat
+  LTI | Refl <- lemFindIndexNeq1 (Proxy @i) (Proxy @tgt) (Proxy @n) (Proxy @listT)
+      -> hlistFindIndex (SNat @(i + 1)) tgtnat list
+  GTI -> _
+
+lemFindIndex :: forall i is sh. Permutation is
+             => Proxy sh -> SNat i -> HList SNat is -> (i + 1 <=? Rank is) :~: True
+             -> Index (FindIndex 0 i is) (Permute is sh) :~: i
+lemFindIndex psh inat perm Refl
+  | Refl <- lemIndexPermute psh (SNat @(FindIndex 0 i is)) perm _
+  = _
+-- lemFindIndex _ _ HNil Refl = case lemSuccLeqZero (Proxy @i) of {}
+-- lemFindIndex psh inat@SNat (HCons xnat@SNat perm) Refl
+--   | Just Refl <- sameNat inat xnat = _
+--   | otherwise = _
+
+foo :: forall i is isT sh.
+       Proxy sh -> SNat i -> SNat (Rank is) -> HList SNat isT -> HList SNat is -> Rank sh :~: Rank is
+    -> Permute (InversePerm' i isT is) (Permute is sh) :~: TakeLen isT sh
+foo psh inat rank HNil perm _ = Refl
+foo psh inat@SNat rank@SNat (HCons _ permT) perm pshrank
+  | Refl <- foo psh (SNat @(i + 1)) rank permT perm pshrank
+  = _
+
+       -- _ :: (Index (FindIndex 0 i is) (Permute is sh) : TakeLen l sh)
+       --      :~: TakeLen (a1 : l) sh
+
+       -- _ :: (Index (FindIndex 0 i is) (Permute is sh)
+       --         : Permute (InversePerm' (i + 1) l is) (Permute is sh))
+       --      :~: TakeLen (a1 : l) sh
+
 class KnownNatList l where makeNatList :: HList SNat l
 instance KnownNatList '[] where makeNatList = HNil
 instance (KnownNat n, KnownNatList l) => KnownNatList (n : l) where makeNatList = natSing `HCons` makeNatList