module Term.LTerm (
Name(..)
, NameTag(..)
, NameId(..)
, NTerm
, sortOfName
, freshTerm
, pubTerm
, LSort(..)
, LVar(..)
, NodeId
, LTerm
, LNTerm
, freshLVar
, sortPrefix
, sortSuffix
, sortCompare
, sortOfLTerm
, sortOfLNTerm
, sortOfLit
, isMsgVar
, isFreshVar
, isSimpleTerm
, niFactors
, containsPrivate
, neverContainsFreshPriv
, ltermVar
, ltermVar'
, ltermNodeId
, ltermNodeId'
, bltermNodeId
, bltermNodeId'
, HasFrees(..)
, MonotoneFunction(..)
, occurs
, freesList
, frees
, someInst
, rename
, eqModuloFreshnessNoAC
, avoid
, evalFreshAvoiding
, evalFreshTAvoiding
, renameAvoiding
, avoidPrecise
, renamePrecise
, renameDropNamehint
, varOccurences
, BVar(..)
, BLVar
, BLTerm
, foldBVar
, fromFree
, prettyLVar
, prettyNodeId
, prettyNTerm
, prettyLNTerm
, module Term.VTerm
) where
import Term.Rewriting.Definitions
import Term.VTerm
import Text.PrettyPrint.Class
import Control.Applicative
import Control.DeepSeq
import Control.Monad.Bind
import Control.Monad.Identity
import qualified Control.Monad.Trans.PreciseFresh as Precise
import Data.Binary
import qualified Data.DList as D
import Data.DeriveTH
import Data.Foldable hiding (concatMap, elem, notElem, any)
import Data.Generics hiding (GT)
import qualified Data.Map as M
import Data.Monoid
import qualified Data.Set as S
import Data.Traversable
import qualified Data.ByteString.Char8 as BC
import Safe (fromJustNote)
import Extension.Data.Monoid
import Extension.Prelude
import Logic.Connectives
data LSort = LSortPub
| LSortFresh
| LSortMsg
| LSortNode
deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data )
sortCompare :: LSort -> LSort -> Maybe Ordering
sortCompare s1 s2 = case (s1, s2) of
(a, b) | a == b -> Just EQ
(LSortNode, _ ) -> Nothing
(_, LSortNode) -> Nothing
(LSortMsg, _ ) -> Just GT
(_, LSortMsg ) -> Just LT
_ -> Nothing
sortPrefix :: LSort -> String
sortPrefix LSortMsg = ""
sortPrefix LSortFresh = "~"
sortPrefix LSortPub = "$"
sortPrefix LSortNode = "#"
sortSuffix :: LSort -> String
sortSuffix LSortMsg = "msg"
sortSuffix LSortFresh = "fresh"
sortSuffix LSortPub = "pub"
sortSuffix LSortNode = "node"
newtype NameId = NameId { getNameId :: String }
deriving( Eq, Ord, Typeable, Data, NFData, Binary )
data NameTag = FreshName | PubName
deriving( Eq, Ord, Show, Typeable, Data )
data Name = Name {nTag :: NameTag, nId :: NameId}
deriving( Eq, Ord, Typeable, Data )
type NTerm v = VTerm Name v
instance IsConst Name where
instance Show Name where
show (Name FreshName n) = "~'" ++ show n ++ "'"
show (Name PubName n) = "'" ++ show n ++ "'"
instance Show NameId where
show = getNameId
freshTerm :: String -> NTerm v
freshTerm = lit . Con . Name FreshName . NameId
pubTerm :: String -> NTerm v
pubTerm = lit . Con . Name PubName . NameId
sortOfName :: Name -> LSort
sortOfName (Name FreshName _) = LSortFresh
sortOfName (Name PubName _) = LSortPub
data LVar = LVar
{ lvarName :: String
, lvarSort :: !LSort
, lvarIdx :: !Integer
}
deriving( Typeable, Data )
type NodeId = LVar
type LTerm c = VTerm c LVar
type LNTerm = VTerm Name LVar
freshLVar :: MonadFresh m => String -> LSort -> m LVar
freshLVar n s = LVar n s <$> freshIdent n
sortOfLTerm :: Show c => (c -> LSort) -> LTerm c -> LSort
sortOfLTerm sortOfConst t = case viewTerm2 t of
Lit2 (Con c) -> sortOfConst c
Lit2 (Var lv) -> lvarSort lv
_ -> LSortMsg
sortOfLNTerm :: LNTerm -> LSort
sortOfLNTerm = sortOfLTerm sortOfName
sortOfLit :: Lit Name LVar -> LSort
sortOfLit (Con n) = sortOfName n
sortOfLit (Var v) = lvarSort v
isMsgVar :: LNTerm -> Bool
isMsgVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortMsg)
isMsgVar _ = False
isFreshVar :: LNTerm -> Bool
isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh)
isFreshVar _ = False
niFactors :: LNTerm -> [LNTerm]
niFactors t = case viewTerm2 t of
FMult ts -> concatMap niFactors ts
FInv t1 -> niFactors t1
_ -> [t]
containsPrivate :: Term t -> Bool
containsPrivate t = case viewTerm t of
Lit _ -> False
FApp (NoEq (_,(_,Private))) _ -> True
FApp _ as -> any containsPrivate as
isSimpleTerm :: LNTerm -> Bool
isSimpleTerm t =
not (containsPrivate t) &&
(getAll . foldMap (All . (LSortFresh /=) . sortOfLit) $ t)
neverContainsFreshPriv :: LNTerm -> Bool
neverContainsFreshPriv t =
not (containsPrivate t) &&
(getAll . foldMap (All . (`notElem` [LSortMsg, LSortFresh]) . sortOfLit) $ t)
ltermVar :: LSort -> LTerm c -> Maybe LVar
ltermVar s t = do v <- termVar t; guard (s == lvarSort v); return v
ltermVar' :: Show c => LSort -> LTerm c -> LVar
ltermVar' s t =
fromJustNote err (ltermVar s t)
where
err = "ltermVar': expected variable term of sort " ++ show s ++ ", but got " ++ show t
ltermNodeId :: LTerm c -> Maybe LVar
ltermNodeId = ltermVar LSortNode
ltermNodeId' :: Show c => LTerm c -> LVar
ltermNodeId' = ltermVar' LSortNode
data BVar v = Bound Integer
| Free v
deriving( Eq, Ord, Show, Data, Typeable )
type BLVar = BVar LVar
type BLTerm = NTerm BLVar
foldBVar :: (Integer -> a) -> (v -> a) -> BVar v -> a
foldBVar fBound fFree = go
where
go (Bound i) = fBound i
go (Free v) = fFree v
instance Functor BVar where
fmap f = foldBVar Bound (Free . f)
instance Foldable BVar where
foldMap f = foldBVar mempty f
instance Traversable BVar where
traverse f = foldBVar (pure . Bound) (fmap Free . f)
instance Applicative BVar where
pure = return
(<*>) = ap
instance Monad BVar where
return = Free
m >>= f = foldBVar Bound f m
fromFree :: BVar v -> v
fromFree (Free v) = v
fromFree (Bound i) = error $ "fromFree: bound variable '" ++ show i ++ "'"
bltermNodeId :: BLTerm -> Maybe LVar
bltermNodeId t = do
Free v <- termVar t; guard (LSortNode == lvarSort v); return v
bltermNodeId' :: BLTerm -> LVar
bltermNodeId' t =
fromJustNote err (bltermNodeId t)
where
err = "bltermNodeId': expected free node-id variable term, but got " ++
show t
instance Eq LVar where
(LVar n1 s1 i1) == (LVar n2 s2 i2) = i1 == i2 && s1 == s2 && n1 == n2
instance Ord LVar where
compare (LVar x1 x2 x3) (LVar y1 y2 y3) =
compare x3 y3 & compare x2 y2 & compare x1 y1 & EQ
where
EQ & x = x
x & _ = x
instance Show LVar where
show (LVar v s i) =
sortPrefix s ++ body
where
body | null v = show i
| i == 0 = v
| otherwise = v ++ "." ++ show i
instance IsVar LVar where
type Occurence = [String]
data MonotoneFunction f = Monotone (LVar -> f LVar )
| Arbitrary (LVar -> f LVar )
class HasFrees t where
foldFrees :: Monoid m => (LVar -> m ) -> t -> m
foldFreesOcc :: Monoid m => (Occurence -> LVar -> m) -> Occurence -> t -> m
mapFrees :: Applicative f => MonotoneFunction f -> t -> f t
occurs :: HasFrees t => LVar -> t -> Bool
occurs x = getAny . foldFrees (Any . (x ==))
freesDList :: HasFrees t => t -> D.DList LVar
freesDList = foldFrees pure
freesList :: HasFrees t => t -> [LVar]
freesList = D.toList . freesDList
frees :: HasFrees t => t -> [LVar]
frees = sortednub . freesList
varOccurences :: HasFrees a => a -> [(LVar, S.Set Occurence)]
varOccurences t =
map (\((v,ctx1):rest) -> (v, S.fromList (ctx1:(map snd rest)))) . groupOn fst . sortOn fst
. foldFreesOcc (\ c v -> [(v,c)]) [] $ t
someInst :: (MonadFresh m, MonadBind LVar LVar m, HasFrees t) => t -> m t
someInst = mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x (lvarName x))
rename :: (MonadFresh m, HasFrees a) => a -> m a
rename x = case boundsVarIdx x of
Nothing -> return x
Just (minVarIdx, maxVarIdx) -> do
freshStart <- freshIdents (succ (maxVarIdx minVarIdx))
return . runIdentity . mapFrees (Monotone $ incVar (freshStart minVarIdx)) $ x
where
incVar shift (LVar n so i) = pure $ LVar n so (i+shift)
eqModuloFreshnessNoAC :: (HasFrees a, Eq a) => a -> a -> Bool
eqModuloFreshnessNoAC t1 =
(normIndices t1 ==) . normIndices
where
normIndices = (`evalFresh` nothingUsed) . (`evalBindT` noBindings) .
mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "")
boundsVarIdx :: HasFrees t => t -> Maybe (Integer, Integer)
boundsVarIdx = getMinMax . foldFrees (minMaxSingleton . lvarIdx)
avoid :: HasFrees t => t -> FreshState
avoid = maybe 0 (succ . snd) . boundsVarIdx
evalFreshAvoiding :: HasFrees t => Fresh a -> t -> a
evalFreshAvoiding m = evalFresh m . avoid
evalFreshTAvoiding :: (Monad m, HasFrees t) => FreshT m a -> t -> m a
evalFreshTAvoiding m = evalFreshT m . avoid
renameAvoiding :: (HasFrees s, HasFrees t) => s -> t -> s
s `renameAvoiding` t = rename s `evalFreshAvoiding` t
avoidPrecise :: HasFrees t => t -> Precise.FreshState
avoidPrecise =
foldl' ins M.empty . frees
where
ins m v = M.insertWith' max (lvarName v) (lvarIdx v + 1) m
renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a
renamePrecise x = evalBindT (someInst x) noBindings
renameDropNamehint :: (MonadFresh m, MonadBind LVar LVar m, HasFrees a) => a -> m a
renameDropNamehint =
mapFrees (Arbitrary $ \x -> importBinding (`LVar` lvarSort x) x "")
instance HasFrees LVar where
foldFrees = id
foldFreesOcc f c v = f c v
mapFrees (Arbitrary f) = f
mapFrees (Monotone f) = f
instance HasFrees v => HasFrees (Lit c v) where
foldFrees f (Var x) = foldFrees f x
foldFrees _ _ = mempty
foldFreesOcc f c (Var x) = foldFreesOcc f c x
foldFreesOcc _ _ _ = mempty
mapFrees f (Var x) = Var <$> mapFrees f x
mapFrees _ l = pure l
instance HasFrees v => HasFrees (BVar v) where
foldFrees _ (Bound _) = mempty
foldFrees f (Free v) = foldFrees f v
foldFreesOcc _ _ (Bound _) = mempty
foldFreesOcc f c (Free v) = foldFreesOcc f c v
mapFrees _ b@(Bound _) = pure b
mapFrees f (Free v) = Free <$> mapFrees f v
instance (HasFrees l, Ord l) => HasFrees (Term l) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f c t = case viewTerm t of
Lit l -> foldFreesOcc f c l
FApp (NoEq o) as -> foldFreesOcc f ((BC.unpack . fst $ o):c) as
FApp o as -> mconcat $ map (foldFreesOcc f (show o:c)) as
mapFrees f (viewTerm -> Lit l) = lit <$> mapFrees f l
mapFrees f@(Arbitrary _) (viewTerm -> FApp o l) = fApp o <$> mapFrees f l
mapFrees f@(Monotone _) (viewTerm -> FApp o l) = unsafefApp o <$> mapFrees f l
instance HasFrees a => HasFrees (Equal a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f p (Equal a b) = foldFreesOcc f p (a,b)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Match a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc _ _ NoMatch = mempty
foldFreesOcc f p (DelayedMatches ms) = foldFreesOcc f p ms
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (RRule a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f p (RRule a b) = foldFreesOcc f p (a,b)
mapFrees f = traverse (mapFrees f)
instance HasFrees () where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees Int where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees Integer where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees Bool where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees Char where
foldFrees _ = const mempty
foldFreesOcc _ _ = const mempty
mapFrees _ = pure
instance HasFrees a => HasFrees (Maybe a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc _ _ Nothing = mempty
foldFreesOcc f p (Just x) = foldFreesOcc f p x
mapFrees f = traverse (mapFrees f)
instance (HasFrees a, HasFrees b) => HasFrees (Either a b) where
foldFrees f = either (foldFrees f) (foldFrees f)
foldFreesOcc f p = either (foldFreesOcc f ("0":p)) (foldFreesOcc f ("1":p))
mapFrees f = either (fmap Left . mapFrees f) (fmap Right . mapFrees f)
instance (HasFrees a, HasFrees b) => HasFrees (a, b) where
foldFrees f (x, y) = foldFrees f x `mappend` foldFrees f y
foldFreesOcc f p (x, y) = foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y
mapFrees f (x, y) = (,) <$> mapFrees f x <*> mapFrees f y
instance (HasFrees a, HasFrees b, HasFrees c) => HasFrees (a, b, c) where
foldFrees f (x, y, z) = foldFrees f (x, (y, z))
foldFreesOcc f p (x, y, z) =
foldFreesOcc f ("0":p) x `mappend` foldFreesOcc f ("1":p) y `mappend` foldFreesOcc f ("2":p) z
mapFrees f (x0, y0, z0) =
(\(x, (y, z)) -> (x, y, z)) <$> mapFrees f (x0, (y0, z0))
instance HasFrees a => HasFrees [a] where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f c xs = mconcat $ (map (\(i,x) -> foldFreesOcc f (show i:c) x)) $ zip [(0::Int)..] xs
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Disj a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f p d = foldFreesOcc f p (getDisj d)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Conj a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f p c = foldFreesOcc f p (getConj c)
mapFrees f = traverse (mapFrees f)
instance (Ord a, HasFrees a) => HasFrees (S.Set a) where
foldFrees f = foldMap (foldFrees f)
foldFreesOcc f p = foldMap (foldFreesOcc f ("0":p))
mapFrees f = fmap S.fromList . mapFrees f . S.toList
instance (Ord k, HasFrees k, HasFrees v) => HasFrees (M.Map k v) where
foldFrees f = M.foldrWithKey combine mempty
where
combine k v m = foldFrees f k `mappend` (foldFrees f v `mappend` m)
foldFreesOcc f p = M.foldrWithKey combine mempty
where
combine k v m = foldFreesOcc f p (k,v) `mappend` m
mapFrees f = fmap M.fromList . mapFrees f . M.toList
prettyLVar :: Document d => LVar -> d
prettyLVar = text . show
prettyNodeId :: Document d => NodeId -> d
prettyNodeId = text . show
prettyNTerm :: (Show v, Document d) => NTerm v -> d
prettyNTerm = prettyTerm (text . show)
prettyLNTerm :: Document d => LNTerm -> d
prettyLNTerm = prettyNTerm
$( derive makeBinary ''NameTag)
$( derive makeBinary ''Name)
$( derive makeBinary ''LSort)
$( derive makeBinary ''LVar)
$( derive makeBinary ''BVar)
$( derive makeNFData ''NameTag)
$( derive makeNFData ''Name)
$( derive makeNFData ''LSort)
$( derive makeNFData ''LVar)
$( derive makeNFData ''BVar)