{-# LANGUAGE FlexibleContexts #-}
-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
--
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Types for communicating with Maude.
module Term.Maude.Types (
  -- * Maude terms
    MaudeLit(..)
  , MSubst
  , MTerm

  -- * conversion from/to maude terms
  , 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)

-- Maude Terms
----------------------------------------------------------------------

data MaudeLit = MaudeVar   Integer LSort
              | FreshVar   Integer LSort
              | MaudeConst Integer LSort
  deriving (Eq, Ord, Show)

type MTerm = Term MaudeLit

type MSubst = [((LSort, Integer), MTerm)]


------------------------------------------------------------------------
-- Convert between MTerms and LNTerms
------------------------------------------------------------------------

-- | Convert an @LNTerm@ to an @MTerm@.
lTermToMTerm' :: (MonadBind (Lit Name LVar) MaudeLit m, MonadFresh m)
              => LNTerm -- ^ The term to translate.
              -> m MTerm
lTermToMTerm' = lTermToMTerm sortOfName


-- | Convert an @LNTerm@ with arbitrary names to an @MTerm@.
lTermToMTerm :: (MonadBind (Lit c LVar) MaudeLit m, MonadFresh m, Show c, Show (Lit c LVar), Ord c)
             => (c -> LSort) -- ^ A function that returns the sort of a constant.
             -> VTerm c LVar -- ^ The term to translate.
             -> 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"


-- | Convert an 'MTerm' to an 'LNTerm' under the assumption that the bindings
-- for the constants are already available.
mTermToLNTerm :: (MonadBind MaudeLit (Lit c LVar) m, MonadFresh m, Show (Lit c LVar), Ord c, Show c)
             => String -- ^ Name hint for freshly generated variables.
             -> MTerm  -- ^ The maude term to convert.
             -> 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


-- Back and forth conversions
------------------------------------------------------------------------

-- | Run a @BindT (Lit c LVar) MaudeLit Fresh@ computation
--   with an empty fresh supply and an empty binding map and return
--   the result and the resulting inverted binding map.
runConversion :: Ord c
              => BindT (Lit c LVar) MaudeLit Fresh a -- ^ Computation to execute.
              -> (a, Map MaudeLit (Lit c LVar))
runConversion to =
    (x, invertMap bindings)
  where (x, bindings) = runBindT to noBindings `evalFresh` nothingUsed

-- | Run a @BindT  MaudeLit (Lit c LVar) Fresh@ computation using the
--   supplied binding map and the corresponding fresh supply.
runBackConversion :: BindT MaudeLit (Lit c LVar) Fresh a -- ^ Computation to execute.
                  -> Map MaudeLit (Lit c LVar) -- ^ Binding map that should be used.
                  -> a
runBackConversion back bindings =
    evalBindT back bindings `evalFreshAvoiding` M.elems bindings

------------------------------------------------------------------------
-- Conversion between Maude and Standard substitutions
------------------------------------------------------------------------

-- | @msubstToLSubstVFresh bindings substMaude@ converts a substitution
--   returned by Maude to a 'VFresh' substitution. It expects that the
--   range of the maude substitution contains only fresh variables in its
--   range and raises an error otherwise.
msubstToLSubstVFresh :: (Ord c, Show (Lit c LVar), Show c)
                     => Map MaudeLit (Lit c LVar) -- ^ The binding map to use for constants.
                     -> MSubst -- ^ The maude substitution.
                     -> 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
   -- try to keep variable name for xi -> xj mappings
   -- commented out, seems wrong
   --  translate ((s,i), mt@(Lit (FreshVar _ _))) = do
   --    lv <- lookupVar s i
   --    (lv,)  <$> mTermToLNTerm (lvarName lv) mt
   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 bindings substMaude@ converts a substitution
--   returned by Maude to a 'VFree' substitution. It expects that the
--   maude substitution contains no fresh variables in its range and raises an
--   error otherwise.
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