?prevdifflink? - Blame
|
{-# LANGUAGE FlexibleContexts #-} {-# OPTIONS_GHC -Wall #-} ------------------------------------------------------------------------------- {- | Module : Language.Law.Verify Description : Validation of the uniqueness of definitions and the existence of references. Copyright : (c) Paulo Silva License : LGPL Maintainer : paufil@di.uminho.pt Stability : experimental Portability : portable -} ------------------------------------------------------------------------------- module Language.Law.Verify ( verify, getDefs, replaceDefs ) where import Control.GalcError import Control.Monad.Error import Control.Monad.Reader import Data.Env import Language.Law.SyntaxADT import Language.R.SyntaxADT import qualified Language.R.Verify as R ------------------------------------------------------------------------------- verify :: MonadError GalcError m => R.ExtEnv -> LawS -> m LawS verify extEnv l = let intEnv = getDefs l ids = R.reps $ indexes extEnv ++ map fst intEnv env = R.Env' {R.internal = fromListEnv intEnv, R.external = extEnv} in if null ids then runReaderT (replaceDefs l) env else throwError $ MultiDefError . concatMap ((++"\n") . show) $ ids ------------------------------------------------------------------------------- getDefs :: LawS -> [(String, S)] getDefs (EquivS _ _ s1 s2) = R.getDefs s1 ++ R.getDefs s2 getDefs (ImplS _ _ s1 s2) = R.getDefs s1 ++ R.getDefs s2 ------------------------------------------------------------------------------- replaceDefs :: (MonadError GalcError m, MonadReader R.Env' m) => LawS -> m LawS replaceDefs (EquivS p n s1 s2) = do s1' <- R.replaceDefs s1 s2' <- R.replaceDefs s2 return $ EquivS p n s1' s2' replaceDefs (ImplS p n s1 s2) = do s1' <- R.replaceDefs s1 s2' <- R.replaceDefs s2 return $ ImplS p n s1' s2' ------------------------------------------------------------------------------- |