| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 1 | paulosilva | |
| 2 | {-# LANGUAGE PatternSignatures, FlexibleContexts #-} | ||
| 3 | {-# OPTIONS_GHC -Wall #-} | ||
| 4 | |||
| 5 | ------------------------------------------------------------------------------- | ||
| 6 | |||
| 7 | {- | | ||
| 8 | Module : Galculator.RunCommand | ||
| 9 | Description : Evaluation of the commands. | ||
| 10 | Copyright : (c) Paulo Silva | ||
| 11 | License : LGPL | ||
| 12 | |||
| 13 | Maintainer : paufil@di.uminho.pt | ||
| 14 | Stability : experimental | ||
| 15 | Portability : portable | ||
| 16 | |||
| 17 | -} | ||
| 18 | |||
| 19 | ------------------------------------------------------------------------------- | ||
| 20 | |||
| 21 | module Galculator.RunCommand ( | ||
| 22 | runCommand, | ||
| 23 | keepGoing | ||
| 24 | ) where | ||
| 25 | |||
| 26 | import Control.GalcError | ||
| 27 | import qualified Control.Exception | ||
| 28 | import Control.Monad.Error | ||
| 29 | import Control.Monad.Trans | ||
| 30 | import Data.Existential | ||
| 31 | import Galculator.Evaluate | ||
| 32 | 7 | paulosilva | import Galculator.Proof |
| 33 | 1 | paulosilva | import Galculator.State |
| 34 | 7 | paulosilva | import Galculator.StepEval |
| 35 | 1 | paulosilva | import Language.Command.Syntax |
| 36 | import qualified Language.Law.Refresh as LR | ||
| 37 | import Language.Law.Syntax | ||
| 38 | import Language.Law.SyntaxADT | ||
| 39 | import qualified Language.Law.TypeInference as LI | ||
| 40 | import qualified Language.Law.Verify as LV | ||
| 41 | import qualified Language.Module.Parser as MP | ||
| 42 | import qualified Language.Module.Refresh as MR | ||
| 43 | import Language.Module.Syntax | ||
| 44 | import Language.Module.SyntaxADT | ||
| 45 | import qualified Language.Module.TypeInference as MI | ||
| 46 | import qualified Language.Module.Verify as MV | ||
| 47 | import qualified Language.R.Refresh as RR | ||
| 48 | import Language.R.Syntax | ||
| 49 | import Language.R.SyntaxADT | ||
| 50 | import qualified Language.R.TypeInference as RI | ||
| 51 | import qualified Language.R.Verify as RV | ||
| 52 | |||
| 53 | ------------------------------------------------------------------------------- | ||
| 54 | |||
| 55 | runCommand :: Command -> GalcStateT Bool | ||
| 56 | ------------------------------------------------------------------------------- | ||
| 57 | runCommand Abort = | ||
| 58 | 7 | paulosilva | keepGoing . inMode [SetProofMode, ProofMode, IndirectProofMode, FinalProofMode] $ |
| 59 | 1 | paulosilva | resetProof >> galcShow "Aborted..." |
| 60 | ------------------------------------------------------------------------------- | ||
| 61 | runCommand (Assume l) = | ||
| 62 | keepGoing . addAssumption =<< compileLaw l | ||
| 63 | ------------------------------------------------------------------------------- | ||
| 64 | runCommand Auto = | ||
| 65 | 7 | paulosilva | keepGoing . inMode [ProofMode, IndirectProofMode] $ solve |
| 66 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 67 | runCommand (Browse mdl) = keepGoing $ do | ||
| 68 | modules <- getLoadedModules | ||
| 69 | when (not $ mdl `elem` modules) (throwError (ModuleRefError mdl)) | ||
| 70 | showLaws =<< getLaws mdl | ||
| 71 | showDefinitions =<< getDefinitions mdl | ||
| 72 | showGCs =<< getGCs mdl | ||
| 73 | ------------------------------------------------------------------------------- | ||
| 74 | 7 | paulosilva | runCommand (Comb comb) = keepGoing . inMode [SetProofMode, ProofMode, IndirectProofMode] $ |
| 75 | stepEval comb | ||
| 76 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 77 | runCommand (Define def) = | ||
| 78 | keepGoing . addDefinition =<< compileR def | ||
| 79 | ------------------------------------------------------------------------------- | ||
| 80 | runCommand (Derive drv) = keepGoing . showLaw =<< evalDerivation drv | ||
| 81 | ------------------------------------------------------------------------------- | ||
| 82 | runCommand Help = keepGoing . galcShow $ helpScreen | ||
| 83 | ------------------------------------------------------------------------------- | ||
| 84 | 7 | paulosilva | runCommand Hint = keepGoing . inMode [ProofMode, IndirectProofMode] $ do |
| 85 | 1 | paulosilva | Exists t r <- getCurExpr |
| 86 | modules <- getLoadedModules | ||
| 87 | lws <- foldM (\res v -> (getLaws v >>= \x -> return (x++res))) [] modules | ||
| 88 | return () | ||
| 89 | ------------------------------------------------------------------------------- | ||
| 90 | runCommand (Info _) = undefined | ||
| 91 | ------------------------------------------------------------------------------- | ||
| 92 | runCommand (Load mdl) = keepGoing $ do | ||
| 93 | modules <- getLoadedModules | ||
| 94 | when (mdl `elem` modules) (runCommand (Unload mdl) >> return ()) | ||
| 95 | addModule mdl =<< compileModule =<< MP.parser =<< readModule mdl | ||
| 96 | galcShow $ "Module loaded: " ++ mdl | ||
| 97 | ------------------------------------------------------------------------------- | ||
| 98 | runCommand Modules = | ||
| 99 | keepGoing . showModules =<< getLoadedModules | ||
| 100 | ------------------------------------------------------------------------------- | ||
| 101 | runCommand (Prove prf) = | ||
| 102 | 7 | paulosilva | keepGoing . inMode [GlobalMode] . setProof =<< compileLaw prf |
| 103 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 104 | runCommand Quit = return True | ||
| 105 | ------------------------------------------------------------------------------- | ||
| 106 | runCommand Reload = | ||
| 107 | 7 | paulosilva | keepGoing . inMode [GlobalMode] . |
| 108 | 1 | paulosilva | mapM_ (\m -> runCommand (Unload m) >> runCommand (Load m)) =<< |
| 109 | getLoadedModules | ||
| 110 | ------------------------------------------------------------------------------- | ||
| 111 | runCommand Restart = | ||
| 112 | 7 | paulosilva | keepGoing . inMode [ProofMode, IndirectProofMode, FinalProofMode] $ restartProof |
| 113 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 114 | runCommand Rules = keepGoing . galcShow $ rulesScreen | ||
| 115 | ------------------------------------------------------------------------------- | ||
| 116 | runCommand Save = | ||
| 117 | 7 | paulosilva | keepGoing . inMode [FinalProofMode] $ saveProof |
| 118 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 119 | runCommand Show = | ||
| 120 | 7 | paulosilva | keepGoing . inMode [SetProofMode, ProofMode, IndirectProofMode, FinalProofMode] $ showProof |
| 121 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 122 | runCommand (Type expr) = keepGoing . galcShow . show =<< compileR expr | ||
| 123 | ------------------------------------------------------------------------------- | ||
| 124 | runCommand (Undo mn) = | ||
| 125 | 7 | paulosilva | keepGoing . inMode [ProofMode, IndirectProofMode] . undo . maybe 1 id $ mn |
| 126 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 127 | runCommand (Unload nm) = | ||
| 128 | 7 | paulosilva | keepGoing . inMode [GlobalMode] . removeModule $ nm |
| 129 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 130 | |||
| 131 | solve :: GalcStateT () | ||
| 132 | 7 | paulosilva | solve = galcShow "To be implemented..." |
| 133 | 1 | paulosilva | |
| 134 | ------------------------------------------------------------------------------- | ||
| 135 | |||
| 136 | showLaw :: Law -> GalcStateT () | ||
| 137 | 7 | paulosilva | showLaw = galcShow . show |
| 138 | 1 | paulosilva | |
| 139 | ------------------------------------------------------------------------------- | ||
| 140 | |||
| 141 | showLaws :: [Law] -> GalcStateT () | ||
| 142 | showLaws lst = do | ||
| 143 | galcShow "Laws:" | ||
| 144 | mapM_ showLaw lst | ||
| 145 | |||
| 146 | ------------------------------------------------------------------------------- | ||
| 147 | |||
| 148 | showDefinitions :: [RType] -> GalcStateT () | ||
| 149 | showDefinitions defs = do | ||
| 150 | galcShow "Definitions:" | ||
| 151 | mapM_ showExpr defs | ||
| 152 | |||
| 153 | ------------------------------------------------------------------------------- | ||
| 154 | |||
| 155 | showExpr :: RType -> GalcStateT () | ||
| 156 | showExpr = galcShow . show | ||
| 157 | |||
| 158 | ------------------------------------------------------------------------------- | ||
| 159 | |||
| 160 | showProof :: GalcStateT () | ||
| 161 | 7 | paulosilva | showProof = do |
| 162 | galcShow "Current proof:" | ||
| 163 | galcShow "---------------------------------------------------------------" | ||
| 164 | galcShow . show =<< getExpression | ||
| 165 | galcShow "---------------------------------------------------------------" | ||
| 166 | galcShow . show =<< getInitialExpr | ||
| 167 | --galcShow . show =<< getCurrentProof | ||
| 168 | mapM_ (galcShow . sp) . reverse =<< getCurrentProof | ||
| 169 | galcShow . show =<< getCurExpr | ||
| 170 | 1 | paulosilva | |
| 171 | 7 | paulosilva | where |
| 172 | sp :: ProofStep -> String | ||
| 173 | sp (RewriteStep r lrs) = show r ++ "\n\t{ " ++ concatMap slrs lrs ++ " }\n" | ||
| 174 | sp (IndirectProof r (Left o) lps) = "indirect low:\n<" ++ concatMap sip (reverse lps) ++ ">\n" | ||
| 175 | sp (IndirectProof r (Right o) lps) = "indirect up:\n<" ++ concatMap sip (reverse lps) ++ ">\n" | ||
| 176 | sp QED = "Qed" | ||
| 177 | |||
| 178 | slrs (l, _) = show l ++ "\n" | ||
| 179 | sip (RewriteStep l lrs) = show l ++ "\n\t{ " ++ concatMap slrs lrs ++ " }\n" | ||
| 180 | sip QED = "indirect end\n" | ||
| 181 | sip _ = "" | ||
| 182 | |||
| 183 | 1 | paulosilva | ------------------------------------------------------------------------------- |
| 184 | |||
| 185 | showModules :: [String] -> GalcStateT () | ||
| 186 | showModules [] = galcShow "No loaded modules" | ||
| 187 | showModules mds = do | ||
| 188 | galcShow "Loaded Modules:" | ||
| 189 | mapM_ galcShow mds | ||
| 190 | |||
| 191 | ------------------------------------------------------------------------------- | ||
| 192 | |||
| 193 | rulesScreen :: String | ||
| 194 | rulesScreen = | ||
| 195 | "--------------------------------------------------\n" ++ | ||
| 196 | "Available Rules\n" ++ | ||
| 197 | "--------------------------------------------------\n" ++ | ||
| 198 | "Shunting\t\t\tshunt\n" ++ | ||
| 199 | "Distributive (upper adjoint)\tdistr_up\n" ++ | ||
| 200 | "Distributive (lower adjoint)\tdistr_low\n" ++ | ||
| 201 | "Monotonicity (upper adjoint)\tmonot_up\n" ++ | ||
| 202 | "Monotonicity (lower adjoint)\tmonot_low\n" ++ | ||
| 203 | "Top preserving\t\t\ttop_preserving\n" ++ | ||
| 204 | "Bottom preserving\t\tbot_preserving\n" ++ | ||
| 205 | "Cancellation (upper adjoint)\tcanc_up\n" ++ | ||
| 206 | "Cancellation (lower adjoint)\tcanc_low\n" ++ | ||
| 207 | "Free theorem\t\t\tfree\n" ++ | ||
| 208 | "General law\t\t\tapply <law name>\n" | ||
| 209 | |||
| 210 | ------------------------------------------------------------------------------- | ||
| 211 | |||
| 212 | showGCs :: [RType] -> GalcStateT () | ||
| 213 | showGCs gclst = do | ||
| 214 | galcShow "Galois connections:" | ||
| 215 | mapM_ showExpr gclst | ||
| 216 | |||
| 217 | ------------------------------------------------------------------------------- | ||
| 218 | |||
| 219 | compileR :: S -> GalcStateT RType | ||
| 220 | compileR s = do | ||
| 221 | env <- getEnvironment | ||
| 222 | RI.infer =<< RR.refresh =<< RV.verify env s | ||
| 223 | |||
| 224 | ------------------------------------------------------------------------------- | ||
| 225 | |||
| 226 | compileLaw :: LawS -> GalcStateT Law | ||
| 227 | compileLaw l = do | ||
| 228 | env <- getEnvironment | ||
| 229 | LI.infer =<< LR.refresh =<< LV.verify env l | ||
| 230 | |||
| 231 | ------------------------------------------------------------------------------- | ||
| 232 | |||
| 233 | compileModule :: ModuleS -> GalcStateT Module | ||
| 234 | compileModule = MI.infer <=< MR.refresh <=< MV.verify | ||
| 235 | |||
| 236 | ------------------------------------------------------------------------------- | ||
| 237 | |||
| 238 | readModule :: String -> GalcStateT String | ||
| 239 | readModule mdl = | ||
| 240 | either2error (const $ ModuleFileError mdl) <=< | ||
| 241 | liftIO . Control.Exception.try . readFile $ mdl ++ ".gal" | ||
| 242 | |||
| 243 | ------------------------------------------------------------------------------- | ||
| 244 | |||
| 245 | galcShow :: String -> GalcStateT () | ||
| 246 | galcShow = liftIO . putStrLn | ||
| 247 | |||
| 248 | ------------------------------------------------------------------------------- | ||
| 249 | |||
| 250 | keepGoing :: GalcStateT () -> GalcStateT Bool | ||
| 251 | keepGoing arg = arg >> return False | ||
| 252 | |||
| 253 | ------------------------------------------------------------------------------- | ||
| 254 | |||
| 255 | helpScreen :: String | ||
| 256 | 6 | paulosilva | helpScreen = |
| 257 | showString "--------------------------------------------------\n" . | ||
| 258 | showString " Commands\n" . | ||
| 259 | showString "--------------------------------------------------\n" . | ||
| 260 | showString "abort\t\tAborts the execution of the current proof\n" . | ||
| 261 | showString "assume\t\tAdds an assumption to the available rules\n" . | ||
| 262 | showString "auto\t\tTries to automatically prove the goal\n" . | ||
| 263 | showString "browse\t\tShows the content of a given module\n" . | ||
| 264 | showString "define\t\tAdds a new definition\n" . | ||
| 265 | showString "derive\t\tDerives a property\n" . | ||
| 266 | showString "help\t\tShows this help screen\n" . | ||
| 267 | showString "hint\t\tShows a hint of the possible applicable rules\n" . | ||
| 268 | showString "info\t\tShows information about a given identifier\n" . | ||
| 269 | showString "load\t\tLoad a given module\n" . | ||
| 270 | showString "modules\t\tShows the currently loaded modules\n" . | ||
| 271 | showString "prove\t\tIntroduces a goal to prove\n" . | ||
| 272 | showString "quit\t\tExists Galculator\n" . | ||
| 273 | showString "reload\t\tReloads all modules\n" . | ||
| 274 | showString "restart\t\tRestarts the current proof\n" . | ||
| 275 | showString "rules\t\tLists the available rules\n" . | ||
| 276 | showString "save\t\tSaves the current proof\n" . | ||
| 277 | showString "show\t\tShows the current proof\n" . | ||
| 278 | showString "type\t\tShows the type of a given expression\n" . | ||
| 279 | showString "undo\t\tUndos a proof step\n" . | ||
| 280 | showString "unload\t\tUnloads a given module" $ "" | ||
| 281 | 1 | paulosilva | |
| 282 | ------------------------------------------------------------------------------- | ||
| 283 |