| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE MultiParamTypeClasses, PatternSignatures, FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Galculator.State | ||
| 9 | Description : Global state of Galculator. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | This module needs some improvements. | ||
| 18 | |||
| 19 | -} | ||
| 20 | |||
| 21 | ------------------------------------------------------------------------------- | ||
| 22 | |||
| 23 | module Galculator.State ( | ||
| 24 | GalcState(..), | ||
| 25 | GalcStateT, | ||
| 26 | GalcSt, | ||
| 27 | emptyState, | ||
| 28 | |||
| 29 | OpMode(..), | ||
| 30 | getOpMode, | ||
| 31 | 7 | paulosilva | inMode, |
| 32 | 1 | paulosilva | |
| 33 | 7 | paulosilva | updateProof, |
| 34 | enterProofMode, | ||
| 35 | enterFinalProofMode, | ||
| 36 | enterIndirectProofMode, | ||
| 37 | |||
| 38 | 1 | paulosilva | setProof, |
| 39 | resetProof, | ||
| 40 | |||
| 41 | getEnvironment, | ||
| 42 | addAssumption, | ||
| 43 | getLoadedModules, | ||
| 44 | getLaws, | ||
| 45 | getLaw, | ||
| 46 | getDefinitions, | ||
| 47 | addDefinition, | ||
| 48 | addModule, | ||
| 49 | |||
| 50 | getCurExpr, | ||
| 51 | saveProof, | ||
| 52 | restartProof, | ||
| 53 | |||
| 54 | undo, | ||
| 55 | removeModule, | ||
| 56 | getGC, | ||
| 57 | getGCs, | ||
| 58 | getAssumptions, | ||
| 59 | |||
| 60 | getCurrentProof, | ||
| 61 | getExpression, | ||
| 62 | |||
| 63 | getInitialExpr | ||
| 64 | ) where | ||
| 65 | |||
| 66 | import Control.GalcError | ||
| 67 | import Control.Monad.Error | ||
| 68 | import Control.Monad.Fresh | ||
| 69 | import Control.Monad.State | ||
| 70 | import Control.Monad.Trans | ||
| 71 | import Data.Env | ||
| 72 | import Data.Existential | ||
| 73 | import Data.Maybe | ||
| 74 | import Data.IORef | ||
| 75 | 7 | paulosilva | import Galculator.Proof |
| 76 | 1 | paulosilva | import Language.Law.Syntax |
| 77 | import Language.Module.Syntax | ||
| 78 | import Language.R.Syntax | ||
| 79 | |||
| 80 | |||
| 81 | ------------------------------------------------------------------------------- | ||
| 82 | |||
| 83 | type GalcStateT t = ErrorT GalcError (FreshT [String] GalcState) t | ||
| 84 | |||
| 85 | ------------------------------------------------------------------------------- | ||
| 86 | |||
| 87 | data GalcState a = GalcState { | ||
| 88 | unGalcState :: IORef GalcSt -> IO a } | ||
| 89 | |||
| 90 | ------------------------------------------------------------------------------- | ||
| 91 | |||
| 92 | data GalcSt = GalcSt { | ||
| 93 | opMode :: OpMode, | ||
| 94 | |||
| 95 | modules :: Env Module, | ||
| 96 | rtAssumpt :: Env Law, | ||
| 97 | rtDefinitions :: Env RType, | ||
| 98 | |||
| 99 | proof :: Maybe ProofSt | ||
| 100 | } | ||
| 101 | |||
| 102 | ------------------------------------------------------------------------------- | ||
| 103 | |||
| 104 | data OpMode = | ||
| 105 | GlobalMode | ||
| 106 | | SetProofMode | ||
| 107 | | ProofMode | ||
| 108 | | IndirectProofMode | ||
| 109 | | FinalProofMode | ||
| 110 | deriving Eq | ||
| 111 | |||
| 112 | ------------------------------------------------------------------------------- | ||
| 113 | |||
| 114 | getOpMode :: GalcStateT OpMode | ||
| 115 | getOpMode = ggets opMode | ||
| 116 | |||
| 117 | ------------------------------------------------------------------------------- | ||
| 118 | |||
| 119 | enterGlobalMode :: GalcStateT () | ||
| 120 | enterGlobalMode = updateGalcState $ \st -> st {opMode = GlobalMode} | ||
| 121 | |||
| 122 | ------------------------------------------------------------------------------- | ||
| 123 | |||
| 124 | enterSetProofMode :: GalcStateT () | ||
| 125 | enterSetProofMode = updateGalcState $ \st -> st {opMode = SetProofMode} | ||
| 126 | |||
| 127 | ------------------------------------------------------------------------------- | ||
| 128 | |||
| 129 | enterProofMode :: GalcStateT () | ||
| 130 | enterProofMode = updateGalcState $ \st -> st {opMode = ProofMode} | ||
| 131 | |||
| 132 | ------------------------------------------------------------------------------- | ||
| 133 | |||
| 134 | enterIndirectProofMode :: GalcStateT () | ||
| 135 | enterIndirectProofMode = | ||
| 136 | updateGalcState $ \st -> st {opMode = IndirectProofMode} | ||
| 137 | |||
| 138 | ------------------------------------------------------------------------------- | ||
| 139 | |||
| 140 | enterFinalProofMode :: GalcStateT () | ||
| 141 | enterFinalProofMode = updateGalcState $ \st -> st {opMode = FinalProofMode} | ||
| 142 | |||
| 143 | ------------------------------------------------------------------------------- | ||
| 144 | 7 | paulosilva | inMode :: [OpMode] -> GalcStateT () -> GalcStateT () |
| 145 | inMode lmod a = do | ||
| 146 | cmod <- getOpMode | ||
| 147 | if cmod `elem` lmod then a else throwError ModeError | ||
| 148 | 1 | paulosilva | |
| 149 | 7 | paulosilva | ------------------------------------------------------------------------------- |
| 150 | |||
| 151 | 1 | paulosilva | instance Monad GalcState where |
| 152 | (GalcState m) >>= k = GalcState $ \r -> m r >>= \a -> unGalcState (k a) r | ||
| 153 | return a = GalcState $ \_ -> return a | ||
| 154 | |||
| 155 | ------------------------------------------------------------------------------- | ||
| 156 | |||
| 157 | instance MonadIO GalcState where | ||
| 158 | liftIO m = GalcState $ \_ -> m >>= return -- !?? | ||
| 159 | |||
| 160 | ------------------------------------------------------------------------------- | ||
| 161 | |||
| 162 | instance MonadState GalcSt GalcState where | ||
| 163 | get = GalcState $ \r -> readIORef r | ||
| 164 | put s = GalcState $ \r -> writeIORef r s | ||
| 165 | |||
| 166 | ------------------------------------------------------------------------------- | ||
| 167 | |||
| 168 | glift :: GalcState a -> GalcStateT a | ||
| 169 | glift = lift . lift | ||
| 170 | |||
| 171 | ------------------------------------------------------------------------------- | ||
| 172 | gget :: GalcStateT GalcSt | ||
| 173 | gget = glift get | ||
| 174 | ------------------------------------------------------------------------------- | ||
| 175 | gput :: GalcSt -> GalcStateT () | ||
| 176 | gput = glift . put | ||
| 177 | ------------------------------------------------------------------------------- | ||
| 178 | ggets :: (GalcSt -> a) -> GalcStateT a | ||
| 179 | ggets = glift . gets | ||
| 180 | ------------------------------------------------------------------------------- | ||
| 181 | |||
| 182 | emptyState :: GalcSt | ||
| 183 | emptyState = | ||
| 184 | GalcSt { | ||
| 185 | opMode = GlobalMode, | ||
| 186 | modules = emptyEnv, | ||
| 187 | rtAssumpt = emptyEnv, | ||
| 188 | rtDefinitions = emptyEnv, | ||
| 189 | |||
| 190 | proof = Nothing | ||
| 191 | } | ||
| 192 | |||
| 193 | ------------------------------------------------------------------------------- | ||
| 194 | |||
| 195 | updateGalcState :: (GalcSt -> GalcSt) -> GalcStateT () | ||
| 196 | updateGalcState f = glift . GalcState $ \r -> modifyIORef r f | ||
| 197 | |||
| 198 | ------------------------------------------------------------------------------- | ||
| 199 | -- | Updates the proof information. | ||
| 200 | updateProof :: (ProofSt -> GalcStateT ProofSt) -> GalcStateT () | ||
| 201 | updateProof f = do | ||
| 202 | st <- gget | ||
| 203 | prf <- maybe2error NoProofError . proof $ st | ||
| 204 | prf' <- f prf | ||
| 205 | gput $ st {proof = Just prf'} | ||
| 206 | |||
| 207 | ------------------------------------------------------------------------------- | ||
| 208 | -- | Sets the law to prove and enters the set proof mode. | ||
| 209 | setProof :: Law -> GalcStateT () | ||
| 210 | setProof e = (updateGalcState $ | ||
| 211 | \st -> st { proof = Just $ ProofSt (getName e) e (Left (getLeft e)) [] }) | ||
| 212 | >> enterSetProofMode | ||
| 213 | |||
| 214 | ------------------------------------------------------------------------------- | ||
| 215 | -- | Removes all the proof information and entes the global mode. | ||
| 216 | resetProof :: GalcStateT () | ||
| 217 | resetProof = | ||
| 218 | (updateGalcState $ \st -> st { proof = Nothing }) >> enterGlobalMode | ||
| 219 | |||
| 220 | ------------------------------------------------------------------------------- | ||
| 221 | -- | Returns the environment where expressions can be evaluated. | ||
| 222 | -- The environment is composed of definitions, galois connections and | ||
| 223 | -- run-definitions. | ||
| 224 | getEnvironment :: GalcStateT (Env RType) | ||
| 225 | getEnvironment = do | ||
| 226 | mds <- ggets modules | ||
| 227 | let defs = map definitions . values $ mds | ||
| 228 | gcl = map gcs . values $ mds | ||
| 229 | rtd <- ggets rtDefinitions | ||
| 230 | return $ foldr joinEnv rtd (defs ++ gcl) | ||
| 231 | |||
| 232 | ------------------------------------------------------------------------------- | ||
| 233 | -- | Adds an assumption (law) into the run-time assumption environment. | ||
| 234 | addAssumption :: Law -> GalcStateT () | ||
| 235 | addAssumption l = do | ||
| 236 | let nm = getName l | ||
| 237 | st <- gget | ||
| 238 | lookupGuard ExistingRefError nm (rtAssumpt st) | ||
| 239 | gput $ st {rtAssumpt = addEnv nm l (rtAssumpt st)} | ||
| 240 | |||
| 241 | ------------------------------------------------------------------------------- | ||
| 242 | -- | Returns the name of the loaded modules. | ||
| 243 | getLoadedModules :: GalcStateT [String] | ||
| 244 | getLoadedModules = return . indexes =<< ggets modules | ||
| 245 | |||
| 246 | ------------------------------------------------------------------------------- | ||
| 247 | -- | Returns the list of laws of a given module. | ||
| 248 | getLaws :: String -> GalcStateT [Law] | ||
| 249 | getLaws mdl = | ||
| 250 | return . values . laws =<< lookupE ModuleRefError mdl =<< ggets modules | ||
| 251 | |||
| 252 | ------------------------------------------------------------------------------- | ||
| 253 | -- | Given a name, returns the law definitions. | ||
| 254 | getLaw :: String -> GalcStateT Law | ||
| 255 | getLaw nm = | ||
| 256 | maybe2error (ReferenceError nm) . msum . map (lookupEnv nm . laws) . values | ||
| 257 | =<< ggets modules | ||
| 258 | |||
| 259 | ------------------------------------------------------------------------------- | ||
| 260 | -- | Returns the list of definitions of a given module. | ||
| 261 | getDefinitions :: String -> GalcStateT [RType] | ||
| 262 | getDefinitions mdl = | ||
| 263 | return . values . definitions =<< lookupE ModuleRefError mdl =<< ggets modules | ||
| 264 | |||
| 265 | ------------------------------------------------------------------------------- | ||
| 266 | -- | Adds a definitions into the run-time definition environment. | ||
| 267 | addDefinition :: RType -> GalcStateT () | ||
| 268 | addDefinition def = do | ||
| 269 | let nm = defName def | ||
| 270 | st <- gget | ||
| 271 | lookupGuard ExistingRefError nm (rtDefinitions st) | ||
| 272 | gput $ st { rtDefinitions = addEnv nm def (rtDefinitions st) } | ||
| 273 | |||
| 274 | ------------------------------------------------------------------------------- | ||
| 275 | -- Repeated: | ||
| 276 | -- Language.Module.TypeInference | ||
| 277 | defName :: RType -> String | ||
| 278 | defName (Exists _ (DEF n _)) = n | ||
| 279 | defName _ = "" | ||
| 280 | |||
| 281 | ------------------------------------------------------------------------------- | ||
| 282 | -- | Returns the current expression in the proof. | ||
| 283 | getCurExpr :: GalcStateT RType | ||
| 284 | getCurExpr = | ||
| 285 | return . eitherId . curExpr =<< maybe2error NoProofError =<< ggets proof | ||
| 286 | |||
| 287 | eitherId :: Either a a -> a | ||
| 288 | eitherId = either id id | ||
| 289 | |||
| 290 | ------------------------------------------------------------------------------- | ||
| 291 | -- | Adds a new module into the module environement | ||
| 292 | addModule :: String -> Module -> GalcStateT () | ||
| 293 | addModule nm m = do | ||
| 294 | st <- gget | ||
| 295 | lookupGuard ExistingRefError nm (modules st) | ||
| 296 | gput $ st { modules = addEnv nm m (modules st) } | ||
| 297 | |||
| 298 | ------------------------------------------------------------------------------- | ||
| 299 | |||
| 300 | saveProof :: GalcStateT () | ||
| 301 | saveProof = (updateGalcState $ | ||
| 302 | \st -> st ) >> enterGlobalMode | ||
| 303 | |||
| 304 | ------------------------------------------------------------------------------- | ||
| 305 | |||
| 306 | undo :: Int -> GalcStateT () | ||
| 307 | undo n = updateProof $ return | ||
| 308 | |||
| 309 | ------------------------------------------------------------------------------- | ||
| 310 | -- | Restarts a proof, assuming a left expression. | ||
| 311 | restartProof :: GalcStateT () | ||
| 312 | restartProof = (updateProof $ \prf -> | ||
| 313 | return prf {curExpr = Left . getLeft . expression $ prf, curProof = []}) >> | ||
| 314 | enterSetProofMode | ||
| 315 | |||
| 316 | ------------------------------------------------------------------------------- | ||
| 317 | -- | Removes a module from the module environment. | ||
| 318 | removeModule :: String -> GalcStateT () | ||
| 319 | removeModule nm = do | ||
| 320 | st <- gget | ||
| 321 | lookupE ModuleRefError nm (modules st) | ||
| 322 | gput $ st { modules = delete nm (modules st) } | ||
| 323 | |||
| 324 | ------------------------------------------------------------------------------- | ||
| 325 | |||
| 326 | 7 | paulosilva | -- TODO: MonadOr? |
| 327 | 1 | paulosilva | getGC :: MonadPlus m => String -> GalcStateT (m RType) |
| 328 | getGC nm = return . msum . map (lookupEnv nm . gcs) . values =<< ggets modules | ||
| 329 | |||
| 330 | getGCs :: String -> GalcStateT [RType] | ||
| 331 | getGCs nm = return . msum . map (lookupEnv nm . gcs) . values =<< ggets modules | ||
| 332 | |||
| 333 | getAssumptions :: GalcStateT [Law] | ||
| 334 | getAssumptions = return . values =<< ggets rtAssumpt | ||
| 335 | |||
| 336 | getAssumption :: String -> GalcStateT Law | ||
| 337 | getAssumption nm = lookupE ReferenceError nm =<< ggets rtAssumpt | ||
| 338 | |||
| 339 | --- ====================== | ||
| 340 | getExpression :: GalcStateT Law | ||
| 341 | getExpression = return . expression =<< maybe2error NoProofError =<< ggets proof | ||
| 342 | |||
| 343 | 7 | paulosilva | getInitialExpr :: GalcStateT RType |
| 344 | getInitialExpr = | ||
| 345 | return . getLeft . expression =<< maybe2error NoProofError =<< ggets proof | ||
| 346 | 1 | paulosilva | |
| 347 | getCurrentProof :: GalcStateT Proof | ||
| 348 | 7 | paulosilva | getCurrentProof = |
| 349 | return . curProof =<< maybe2error NoProofError =<< ggets proof | ||
| 350 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 351 | |||
| 352 | lookupGuard :: MonadError GalcError m | ||
| 353 | => (String -> GalcError) -> String -> Env a -> m () | ||
| 354 | lookupGuard err nm = | ||
| 355 | maybe (return ()) (const $ throwError (err nm)) . lookupEnv nm | ||
| 356 | |||
| 357 | ------------------------------------------------------------------------------- | ||
| 358 | |||
| 359 | lookupE :: MonadError GalcError m | ||
| 360 | => (String -> GalcError) -> String -> Env a -> m a | ||
| 361 | lookupE err nm = maybe2error (err nm) . lookupEnv nm | ||
| 362 | |||
| 363 | ------------------------------------------------------------------------------- | ||
| 364 | |||
| 365 |