| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Language.Law.Verify | ||
| 9 | Description : Validation of the uniqueness of definitions and the existence | ||
| 10 | of references. | ||
| 11 | Copyright : (c) Paulo Silva | ||
| 12 | License : LGPL | ||
| 13 | |||
| 14 | Maintainer : paufil@di.uminho.pt | ||
| 15 | Stability : experimental | ||
| 16 | Portability : portable | ||
| 17 | |||
| 18 | -} | ||
| 19 | |||
| 20 | ------------------------------------------------------------------------------- | ||
| 21 | |||
| 22 | module Language.Law.Verify ( | ||
| 23 | verify, | ||
| 24 | getDefs, | ||
| 25 | replaceDefs | ||
| 26 | ) where | ||
| 27 | |||
| 28 | import Control.GalcError | ||
| 29 | import Control.Monad.Error | ||
| 30 | import Control.Monad.Reader | ||
| 31 | import Data.Env | ||
| 32 | import Language.Law.SyntaxADT | ||
| 33 | import Language.R.SyntaxADT | ||
| 34 | import qualified Language.R.Verify as R | ||
| 35 | |||
| 36 | ------------------------------------------------------------------------------- | ||
| 37 | |||
| 38 | verify :: MonadError GalcError m => R.ExtEnv -> LawS -> m LawS | ||
| 39 | verify extEnv l = let | ||
| 40 | intEnv = getDefs l | ||
| 41 | ids = R.reps $ indexes extEnv ++ map fst intEnv | ||
| 42 | env = R.Env' {R.internal = fromListEnv intEnv, R.external = extEnv} | ||
| 43 | in if null ids | ||
| 44 | then runReaderT (replaceDefs l) env | ||
| 45 | else throwError $ MultiDefError . concatMap ((++"\n") . show) $ ids | ||
| 46 | |||
| 47 | ------------------------------------------------------------------------------- | ||
| 48 | |||
| 49 | getDefs :: LawS -> [(String, S)] | ||
| 50 | getDefs (EquivS _ _ s1 s2) = R.getDefs s1 ++ R.getDefs s2 | ||
| 51 | getDefs (ImplS _ _ s1 s2) = R.getDefs s1 ++ R.getDefs s2 | ||
| 52 | |||
| 53 | ------------------------------------------------------------------------------- | ||
| 54 | |||
| 55 | replaceDefs :: (MonadError GalcError m, MonadReader R.Env' m) | ||
| 56 | => LawS -> m LawS | ||
| 57 | replaceDefs (EquivS p n s1 s2) = do | ||
| 58 | s1' <- R.replaceDefs s1 | ||
| 59 | s2' <- R.replaceDefs s2 | ||
| 60 | return $ EquivS p n s1' s2' | ||
| 61 | replaceDefs (ImplS p n s1 s2) = do | ||
| 62 | s1' <- R.replaceDefs s1 | ||
| 63 | s2' <- R.replaceDefs s2 | ||
| 64 | return $ ImplS p n s1' s2' | ||
| 65 | |||
| 66 | ------------------------------------------------------------------------------- | ||
| 67 |