compdata 0.8.1.1 → 0.8.1.2

raw patch · 2 files changed

+88/−4 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• compdata.cabal +1/−1
• src/Data/Comp/SubsumeCommon.hs +87/−3

@@ -1,5 +1,5 @@ Name:			compdata-Version:		0.8.1.1+Version:		0.8.1.2 Synopsis:            	Compositional Data Types Description: 

@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}+{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances, TypeOperators #-}  -------------------------------------------------------------------------------- -- |@@ -14,35 +14,119 @@ -- -------------------------------------------------------------------------------- -module Data.Comp.SubsumeCommon where+module Data.Comp.SubsumeCommon+    ( ComprEmb+    , Pos (..)+    , Emb (..)+    ) where +-- | This type is used in its promoted form only. It represents+-- pointers from the left-hand side of a subsumption to the right-hand+-- side. data Pos = Here | Le Pos | Ri Pos | Sum Pos Pos++-- | This type is used in its promoted form only. It represents+-- possible results for checking for subsumptions. 'Found' indicates a+-- subsumption was found; 'NotFound' indicates no such subsumption was+-- found. 'Ambiguous' indicates that there are duplicates on the left-+-- or the right-hand side. data Emb = Found Pos | NotFound | Ambiguous +-- | This type family takes a position type and compresses it. That+-- means it replaces each nested occurrence of +-- +-- @+--   Sum (prefix (Le Here)) (prefix (Ri Here))@+-- @+---+-- with +-- +-- @+--   prefix Here@+-- @+-- +-- where @prefix@ is some composition of @Le@ and @Ri@. The rational+-- behind this type family is that it provides a more compact proof+-- term of a subsumption, and thus yields more efficient+-- implementations of 'inj' and 'prj'.+ type family ComprPos (p :: Pos) :: Pos where     ComprPos Here = Here     ComprPos (Le p) = Le (ComprPos p)     ComprPos (Ri p) = Ri (ComprPos p)     ComprPos (Sum l r) = CombineMaybe (Sum l r) (Combine (ComprPos l) (ComprPos r)) +-- | Helper type family for 'ComprPos'. type family CombineMaybe (p :: Pos) (p' :: Maybe Pos) where     CombineMaybe p (Just p') = p'     CombineMaybe p p'        = p ++-- | Helper type family for 'ComprPos'. type family Combine (l :: Pos) (r :: Pos) :: Maybe Pos where     Combine (Le l) (Le r) = Le' (Combine l r)     Combine (Ri l) (Ri r) = Ri' (Combine l r)     Combine (Le Here) (Ri Here) = Just Here     Combine l r = Nothing +-- | 'Ri' lifted to 'Maybe'. type family Ri' (p :: Maybe Pos) :: Maybe Pos where     Ri' Nothing = Nothing     Ri' (Just p) = Just (Ri p) +-- | 'Le' lifted to 'Maybe'. type family Le' (p :: Maybe Pos) :: Maybe Pos where     Le' Nothing = Nothing     Le' (Just p) = Just (Le p) ++-- | If the argument is not 'Found', this type family is the+-- identity. Otherwise, the argument is of the form @Found p@, and+-- this type family does two things: (1) it checks whether @p@ the+-- contains duplicates; and (2) it compresses @p@ using 'ComprPos'. If+-- (1) finds no duplicates, @Found (ComprPos p)@ is returned;+-- otherwise @Ambiguous@ is returned.+-- +-- For (1) it is assumed that @p@ does not contain 'Sum' nested+-- underneath a 'Le' or 'Ri' (i.e. only at the root or underneath a+-- 'Sum'). We will refer to such positions below as /atomic position/.+-- Positions not containing 'Sum' are called /simple positions/. type family ComprEmb (e :: Emb) :: Emb where-    ComprEmb (Found p) = Found (ComprPos p)+    ComprEmb (Found p) = Check (Dupl p) (ComprPos p)     ComprEmb e = e++-- | Helper type family for 'ComprEmb'.+type family Check (b :: Bool) (p :: Pos) where+    Check False p = Found p+    Check True  p = Ambiguous++-- | This type family turns a list of /atomic position/ into a list of+-- /simple positions/ by recursively splitting each position of the+-- form @Sum p1 p2@ into @p1@ and @p2@.+type family ToList (s :: [Pos]) :: [Pos] where+    ToList (Sum p1 p2 ': s) = ToList (p1 ': p2 ': s)+    ToList (p ': s) = p ': ToList s+    ToList '[] = '[]++-- | This type checks whether the argument (atomic) position has+-- duplicates.+type Dupl s = Dupl' (ToList '[s])++-- | This type family checks whether the list of positions given as an+-- argument contains any duplicates.+type family Dupl' (s :: [Pos]) :: Bool where+    Dupl' (p ': r) = OrDupl' (Find p r) r+    Dupl' '[] = False++-- | This type family checks whether its first argument is contained+-- its second argument.+type family Find (p :: Pos) (s :: [Pos]) :: Bool where+    Find p (p ': r)  = True+    Find p (p' ': r) = Find p r+    Find p '[] = False++-- | This type family returns @True@ if the first argument is true;+-- otherwise it checks the second argument for duplicates.+type family OrDupl' (a :: Bool) (b :: [Pos]) :: Bool where+    OrDupl'  True  c  = True+    OrDupl'  False c  = Dupl' c