module Term.Maude.Types (
MaudeLit(..)
, MSubst
, MTerm
, lTermToMTerm
, lTermToMTerm'
, mTermToLNTerm
, runConversion
, msubstToLSubstVFresh
, msubstToLSubstVFree
) where
import Term.Term
import Term.LTerm
import Term.Substitution
import Utils.Misc
import Control.Monad.Fresh
import Control.Monad.Bind
import Control.Applicative
import Data.Traversable hiding (mapM)
import Data.Maybe
import qualified Data.Map as M
import Data.Map ( Map )
data MaudeLit = MaudeVar Integer LSort
| FreshVar Integer LSort
| MaudeConst Integer LSort
deriving (Eq, Ord, Show)
type MTerm = Term MaudeLit
type MSubst = [((LSort, Integer), MTerm)]
lTermToMTerm' :: (MonadBind (Lit Name LVar) MaudeLit m, MonadFresh m)
=> LNTerm
-> m MTerm
lTermToMTerm' = lTermToMTerm sortOfName
lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show (Lit c LVar), Ord c)
=> (c -> LSort)
-> VTerm c LVar
-> m MTerm
lTermToMTerm sortOf =
go . viewTerm
where
go (Lit l) = lit <$> exportLit l
go (FApp o as) = fApp o <$> mapM (go . viewTerm) as
exportLit a@(Var lv) =
importBinding (\_ i -> MaudeVar i (lvarSort lv)) a "x"
exportLit a@(Con n) = importBinding (\_ i -> MaudeConst i (sortOf n)) a "a"
mTermToLNTerm :: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c)
=> String
-> MTerm
-> m (VTerm c LVar)
mTermToLNTerm nameHint =
go . viewTerm
where
go (Lit l) = lit <$> importLit l
go (FApp o as) = fApp o <$> mapM (go . viewTerm) as
importLit a@(MaudeVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint
importLit a@(FreshVar _ lsort) = importBinding (\n i -> Var (LVar n lsort i)) a nameHint
importLit a = fromMaybe (error $ "fromMTerm: unknown constant `" ++ show a ++ "'") <$>
lookupBinding a
runConversion :: Ord c
=> BindT (Lit c LVar) MaudeLit Fresh a
-> (a, Map MaudeLit (Lit c LVar))
runConversion to =
(x, invertMap bindings)
where (x, bindings) = runBindT to noBindings `evalFresh` nothingUsed
runBackConversion :: BindT MaudeLit (Lit c LVar) Fresh a
-> Map MaudeLit (Lit c LVar)
-> a
runBackConversion back bindings =
evalBindT back bindings `evalFreshAvoiding` M.elems bindings
msubstToLSubstVFresh :: (Ord c, Show (Lit c LVar), Show c)
=> Map MaudeLit (Lit c LVar)
-> MSubst
-> SubstVFresh c LVar
msubstToLSubstVFresh bindings substMaude
| not $ null [i | (_,t) <- substMaude, MaudeVar _ i <- lits t] =
error $ "msubstToLSubstVFresh: nonfresh variables in `"++show substMaude++"'"
| otherwise = removeRenamings $ substFromListVFresh slist
where
slist = runBackConversion (traverse translate substMaude) bindings
translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt
lookupVar s i = do b <- lookupBinding (MaudeVar i s)
case b of
Just (Var lv) -> return lv
_ -> error $ "msubstToLSubstVFrsh: binding for maude variable `"
++show (s,i) ++"' not found in "++show bindings
msubstToLSubstVFree :: (Ord c, Show (Lit c LVar), Show c)
=> Map MaudeLit (Lit c LVar) -> MSubst -> Subst c LVar
msubstToLSubstVFree bindings substMaude
| not $ null [i | (_,t) <- substMaude, FreshVar _ i <- lits t] =
error $ "msubstToLSubstVFree: fresh variables in `"++show substMaude
| otherwise = substFromList slist
where
slist = evalBindT (traverse translate substMaude) bindings
`evalFreshAvoiding` M.elems bindings
translate ((s,i),mt) = (,) <$> lookupVar s i <*> mTermToLNTerm "x" mt
lookupVar s i = do b <- lookupBinding (MaudeVar i s)
case b of
Just (Var lv) -> return lv
_ -> error $ "msubstToLSubstVFree: binding for maude variable `"
++show (s,i)++"' not found in "++show bindings