generics-mrsop-gdiff 0.0.0 → 0.0.1
raw patch · 3 files changed
+47/−33 lines, 3 filesdep ~generics-mrsop
Dependency ranges changed: generics-mrsop
Files
- generics-mrsop-gdiff.cabal +3/−5
- src/Generics/MRSOP/GDiff.hs +38/−22
- src/Generics/MRSOP/GDiff/Util.hs +6/−6
generics-mrsop-gdiff.cabal view
@@ -6,13 +6,11 @@ -- PVP summary: +------- breaking API changes -- | +----- non-breaking API additions -- | | +--- code changes with no API change-version: 0.0.0+version: 0.0.1 license: BSD3 license-file: LICENSE synopsis: Reimplementation of the `gdiff` algorithm for `generics-mrsop`-description: Here we port the `gdiff` algorithm and library to work over- the `generics-mrsop`, enabling code that relies on the later- library to access the `gdiff` algorithm. +description: Here we port the gdiff algorithm and library to work over the generics-mrsop, enabling code that relies on the later library to access the gdiff algorithm. author: Arian van Putten and Victor Miraldo maintainer: arian.vanputten@gmail.com v.cacciarimiraldo@gmail.com category: Generics@@ -29,7 +27,7 @@ -- Other library packages from which modules are imported. build-depends: base < 5,- generics-mrsop >= 2.0.0+ generics-mrsop >= 2.2.0 -- Directories containing source files. hs-source-dirs: src
src/Generics/MRSOP/GDiff.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE DataKinds #-}@@ -29,11 +30,11 @@ import Generics.MRSOP.Base hiding (listPrfNP) import Generics.MRSOP.GDiff.Util import Generics.MRSOP.Util ( SNat- , EqHO(..)+ , EqHO , IsNat , (:++:) , Lkup- , ShowHO(..)+ , ShowHO , Idx , El(..) , getSNat)@@ -41,10 +42,10 @@ -- | A 'Cof' represents a leaf of the flattened representation of our tree. Hence, -- it will be either a constructor of a particular datatype or an opaque value. data Cof (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> [Atom kon] -> * where- -- ^ A constructor tells us the type of its arguments and which type in the family it constructs+ -- | A constructor tells us the type of its arguments and which type in the family it constructs ConstrI :: (IsNat c, IsNat n) => Constr (Lkup n codes) c -> ListPrf (Lkup c (Lkup n codes)) -> Cof ki codes ('I n) (Lkup c (Lkup n codes)) - -- ^ Requires no arguments to complete+ -- | Requires no arguments to complete ConstrK :: ki k -> Cof ki codes ('K k) '[] -- |Extracts a proxy from a 'Cof'@@ -70,7 +71,7 @@ cofHeq (ConstrK x) (ConstrK y) = case testEquality x y of Just Refl ->- if eqHO x y+ if x == y then Just (Refl, Refl) else Nothing Nothing -> Nothing@@ -85,6 +86,7 @@ Cpy :: Int -> Cof ki codes a t -> ES ki codes (t :++: i) (t :++: j) -> ES ki codes (a ': i) (a ': j) {-# INLINE cost #-}+-- |Extracts the cost of an edit script cost :: ES ki codes txs tys -> Int cost ES0 = 0 cost (Ins k _ _) = k@@ -156,7 +158,7 @@ -- -- A version of sop but over NA instead of Rep sopNA :: NA ki (Fix ki codes) a -> ViewNA ki codes a-sopNA (NA_K k) = TagNA (ConstrK k) NP0+sopNA (NA_K k) = TagNA (ConstrK k) Nil sopNA (NA_I (Fix (sop -> Tag c poa))) = TagNA (ConstrI c (listPrfNP poa)) poa data DES ki codes a xs ys where @@ -177,12 +179,12 @@ => PoA ki (Fix ki codes) xs -> PoA ki (Fix ki codes) ys -> EST ki codes xs ys-diffT NP0 NP0 = NN ES0-diffT ((sopNA -> TagNA c poa) :* xs) NP0 =- let d = diffT (appendNP poa xs) NP0+diffT Nil Nil = NN ES0+diffT ((sopNA -> TagNA c poa) :* xs) Nil =+ let d = diffT (appendNP poa xs) Nil in CN c (Del (1 + cost (getDiff d)) c (getDiff d)) d-diffT NP0 ((sopNA -> TagNA c poa) :* ys) =- let i = diffT NP0 (appendNP poa ys)+diffT Nil ((sopNA -> TagNA c poa) :* ys) =+ let i = diffT Nil (appendNP poa ys) in NC c (Ins (1 + cost (getDiff i)) c (getDiff i)) i diffT ((sopNA -> TagNA c1 poa1) :* xs) ((sopNA -> TagNA c2 poa2) :* ys) = let @@ -253,7 +255,7 @@ -> NA ki (Fix ki codes) a -> Maybe (PoA ki (Fix ki codes) t) matchCof (ConstrI c1 _) (NA_I (Fix x)) = match c1 x-matchCof (ConstrK k) (NA_K k2) = guard (eqHO k k2) >> Just NP0+matchCof (ConstrK k) (NA_K k2) = guard (k == k2) >> Just Nil -- we need to give Haskell a bit of a hint that Tyof codes c reduces to an IsList -- insCof is also really the only place where we _need_ IsList I think@@ -271,7 +273,14 @@ -> Maybe (PoA ki (Fix ki codes) (t :++: xs)) delCof c (x :* xs) = flip appendNP xs <$> matchCof c x +-- * Application Function Variations +-- $applydocs+--+-- Different interfaces to the application function are made+-- available. This enables one to always have an /apply/ function+-- handy on any stage of a generic pipeline.+ apply :: forall ki fam codes ty1 ty2 ix1 ix2. ( Family ki fam codes , ix1 ~ Idx ty1 fam@@ -283,7 +292,7 @@ , EqHO ki , TestEquality ki )- => ES ki codes '[ 'I ix1] '[ 'I ix2]+ => ES ki codes '[ 'I ix1] '[ 'I ix2] -- ^ -> ty1 -> Maybe ty2 apply es a =@@ -295,20 +304,20 @@ apply' :: (IsNat ix1, IsNat ix2, EqHO ki)- => ES ki codes '[ 'I ix1] '[ 'I ix2]+ => ES ki codes '[ 'I ix1] '[ 'I ix2] -- ^ -> Fix ki codes ix1 -> Maybe (Fix ki codes ix2) apply' es x = do- res <- applyES es (NA_I x :* NP0)+ res <- applyES es (NA_I x :* Nil) case res of- (NA_I y :* NP0) -> pure y+ (NA_I y :* Nil) -> pure y applyES :: EqHO ki- => ES ki codes xs ys+ => ES ki codes xs ys -- ^ -> PoA ki (Fix ki codes) xs -> Maybe (PoA ki (Fix ki codes) ys)-applyES ES0 _ = Just NP0+applyES ES0 _ = Just Nil applyES (Ins _ c es) xs = insCof c <$> applyES es xs applyES (Del _ c es) xs = delCof c xs >>= applyES es applyES (Cpy _ c es) xs = insCof c <$> (delCof c xs >>= applyES es)@@ -319,7 +328,7 @@ -- hence, we can not get the datatype info showCof :: forall ki fam codes a c. (HasDatatypeInfo ki fam codes, ShowHO ki) => Cof ki codes a c -> String-showCof (ConstrK k) = showHO k+showCof (ConstrK k) = show k showCof x@(ConstrI c _) = constructorName . constrInfoLkup c $ datatypeInfo (Proxy @fam) (cofIdx x) instance (HasDatatypeInfo ki fam codes, ShowHO ki) =>@@ -329,6 +338,13 @@ show (Del _ c d) = "Del " ++ showCof c ++ " $ " ++ show d show (Cpy _ c d) = "Cpy " ++ showCof c ++ " $ " ++ show d +-- * Diff Function Variations++-- $diffdocs+--+-- Different interfaces to the /diff/ function.++ diff :: forall fam ki codes ix1 ix2 ty1 ty2. ( Family ki fam codes , ix1 ~ Idx ty1 fam@@ -340,13 +356,13 @@ , EqHO ki , TestEquality ki )- => ty1+ => ty1 -- ^ -> ty2 -> ES ki codes '[ 'I ix1] '[ 'I ix2] diff a b = diff' (deep a) (deep b) diff' :: ( EqHO ki, IsNat ix1, IsNat ix2, TestEquality ki)- => Fix ki codes ix1+ => Fix ki codes ix1 -- ^ -> Fix ki codes ix2 -> ES ki codes '[ 'I ix1] '[ 'I ix2]-diff' a b = skipFront (NA_I a :* NP0) (NA_I b :* NP0) +diff' a b = skipFront (NA_I a :* Nil) (NA_I b :* Nil)
src/Generics/MRSOP/GDiff/Util.hs view
@@ -23,15 +23,15 @@ -- this seems more like "Coerce" to me {-# INLINE reify #-} reify :: ListPrf ts -> RList ts-reify Nil = RList-reify (Cons x) = case reify x of RList -> RList+reify LP_Nil = RList+reify (LP_Cons x) = case reify x of RList -> RList -- |Proves that the index of a value of type 'NP' is a list. -- This is useful for pattern matching on said list without -- having to carry the product around. listPrfNP :: NP p xs -> ListPrf xs-listPrfNP NP0 = Nil-listPrfNP (_ :* xs) = Cons $ listPrfNP xs+listPrfNP Nil = LP_Nil+listPrfNP (_ :* xs) = LP_Cons $ listPrfNP xs -- In Agda this would be: -- ++⁻ : {A : Set}@@ -49,8 +49,8 @@ -- carry around the Singleton LstPrf in order to -- discover on the type-level the list, by pattern matching split :: ListPrf xs -> NP p (xs :++: ys) -> (NP p xs, NP p ys)-split Nil poa = (NP0, poa)-split (Cons p) (x :* rs) =+split LP_Nil poa = (Nil, poa)+split (LP_Cons p) (x :* rs) = let (xs, rest) = split p rs in (x :* xs, rest)