module Term.LTerm (
Name(..)
, NameTag(..)
, NameId(..)
, NTerm
, sortOfName
, freshTerm
, pubTerm
, LSort(..)
, LVar(..)
, LTerm
, LNTerm
, freshLVar
, sortPrefix
, sortSuffix
, sortCompare
, sortOfLTerm
, sortOfLNTerm
, isMsgVar
, isFreshVar
, trivial
, input
, HasFrees(..)
, MonotoneFunction(..)
, occurs
, freesList
, frees
, someInst
, rename
, renamePrecise
, eqModuloFreshnessNoAC
, avoid
, evalFreshAvoiding
, evalFreshTAvoiding
, renameAvoiding
, BVar(..)
, foldBVar
, fromFree
, prettyLVar
, prettyNTerm
, prettyLNTerm
, module Term.VTerm
) where
import Term.VTerm
import Term.Rewriting.Definitions
import Text.PrettyPrint.Class
import Control.Applicative
import Control.Monad.Fresh
import Control.Monad.Bind
import Control.DeepSeq
import Control.Monad.Identity
import Data.DeriveTH
import qualified Data.Set as S
import qualified Data.Map as M
import Data.Generics hiding (GT)
import qualified Data.DList as D
import Data.Traversable
import Data.Monoid
import Data.Binary
import Data.Foldable hiding (concatMap, elem)
import Extension.Prelude
import Extension.Data.Monoid
import Logic.Connectives
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 LSort = LSortPub
| LSortFresh
| LSortMsg
| LSortMSet
| LSortNode
deriving( Eq, Ord, Show, Enum, Bounded, Typeable, Data )
data LVar = LVar
{ lvarName :: String
, lvarSort :: !LSort
, lvarIdx :: !Integer
}
deriving( Typeable, Data )
type LTerm c = VTerm c LVar
type LNTerm = VTerm Name LVar
freshLVar :: MonadFresh m => String -> LSort -> m LVar
freshLVar n s = LVar n s <$> freshIdents 1
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
Empty -> LSortMSet
FUnion _ -> LSortMSet
_ -> LSortMsg
sortOfLNTerm :: LNTerm -> LSort
sortOfLNTerm = sortOfLTerm sortOfName
sortCompare :: LSort -> LSort -> Maybe Ordering
sortCompare s1 s2 = case (s1, s2) of
(a, b) | a == b -> Just EQ
(LSortNode, _ ) -> Nothing
(_, LSortNode) -> Nothing
(LSortMSet, _ ) -> Just GT
(_, LSortMSet) -> Just LT
(LSortMsg, _ ) -> Just GT
(_, LSortMsg ) -> Just LT
_ -> Nothing
sortPrefix :: LSort -> String
sortPrefix LSortMsg = ""
sortPrefix LSortFresh = "~"
sortPrefix LSortPub = "$"
sortPrefix LSortNode = "#"
sortPrefix LSortMSet = "%"
sortSuffix :: LSort -> String
sortSuffix LSortMsg = "msg"
sortSuffix LSortFresh = "fresh"
sortSuffix LSortPub = "pub"
sortSuffix LSortNode = "node"
sortSuffix LSortMSet = "mset"
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
input :: LNTerm -> [LNTerm]
input (viewTerm2 -> FMult ts) = concatMap input ts
input (viewTerm2 -> FInv t1) = input t1
input (viewTerm2 -> FPair t1 t2) = input t1 ++ input t2
input t = [t]
trivial :: LNTerm -> Bool
trivial (viewTerm -> FApp _ []) = True
trivial (viewTerm -> Lit (Con (Name PubName _))) = True
trivial (viewTerm -> Lit (Var v)) = case lvarSort v of
LSortPub -> True
LSortMsg -> True
_ -> False
trivial _ = False
data BVar v = Bound Integer
| Free v
deriving( Eq, Ord, Show, Data, Typeable )
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 ++ "'"
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
data MonotoneFunction f = Monotone (LVar -> f LVar )
| Arbitrary (LVar -> f LVar )
class HasFrees t where
foldFrees :: Monoid m => (LVar -> m ) -> 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
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)
renamePrecise :: (MonadFresh m, HasFrees a) => a -> m a
renamePrecise x = evalBindT (someInst x) noBindings
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
instance HasFrees LVar where
foldFrees = id
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
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
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)
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)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Match a) where
foldFrees f = foldMap (foldFrees f)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (RRule a) where
foldFrees f = foldMap (foldFrees f)
mapFrees f = traverse (mapFrees f)
instance HasFrees () where
foldFrees _ = const mempty
mapFrees _ = pure
instance HasFrees Int where
foldFrees _ = const mempty
mapFrees _ = pure
instance HasFrees Integer where
foldFrees _ = const mempty
mapFrees _ = pure
instance HasFrees Bool where
foldFrees _ = const mempty
mapFrees _ = pure
instance HasFrees Char where
foldFrees _ = const mempty
mapFrees _ = pure
instance HasFrees a => HasFrees (Maybe a) where
foldFrees f = foldMap (foldFrees f)
mapFrees f = traverse (mapFrees f)
instance (HasFrees a, HasFrees b) => HasFrees (Either a b) where
foldFrees f = either (foldFrees f) (foldFrees f)
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
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))
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)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Disj a) where
foldFrees f = foldMap (foldFrees f)
mapFrees f = traverse (mapFrees f)
instance HasFrees a => HasFrees (Conj a) where
foldFrees f = foldMap (foldFrees f)
mapFrees f = traverse (mapFrees f)
instance (Ord a, HasFrees a) => HasFrees (S.Set a) where
foldFrees f = foldMap (foldFrees f)
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)
mapFrees f = fmap M.fromList . mapFrees f . M.toList
prettyLVar :: Document d => LVar -> d
prettyLVar = 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)