diff --git a/generics-mrsop-gdiff.cabal b/generics-mrsop-gdiff.cabal --- a/generics-mrsop-gdiff.cabal +++ b/generics-mrsop-gdiff.cabal @@ -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 diff --git a/src/Generics/MRSOP/GDiff.hs b/src/Generics/MRSOP/GDiff.hs --- a/src/Generics/MRSOP/GDiff.hs +++ b/src/Generics/MRSOP/GDiff.hs @@ -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) diff --git a/src/Generics/MRSOP/GDiff/Util.hs b/src/Generics/MRSOP/GDiff/Util.hs --- a/src/Generics/MRSOP/GDiff/Util.hs +++ b/src/Generics/MRSOP/GDiff/Util.hs @@ -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)