{-# LANGUAGE PatternSignatures, FlexibleContexts #-}
{-# OPTIONS_GHC -Wall #-}
-------------------------------------------------------------------------------
{- |
Module : Galculator.RunCommand
Description : Evaluation of the commands.
Copyright : (c) Paulo Silva
License : LGPL
Maintainer : paufil@di.uminho.pt
Stability : experimental
Portability : portable
-}
-------------------------------------------------------------------------------
module Galculator.RunCommand (
runCommand,
keepGoing
) where
import Control.GalcError
import qualified Control.Exception
import Control.Monad.Error
import Control.Monad.Trans
import Data.Existential
import Galculator.Evaluate
import Galculator.Rule
import Galculator.State
import Language.Command.Syntax
import qualified Language.Law.Refresh as LR
import Language.Law.Syntax
import Language.Law.SyntaxADT
import qualified Language.Law.TypeInference as LI
import qualified Language.Law.Verify as LV
import qualified Language.Module.Parser as MP
import qualified Language.Module.Refresh as MR
import Language.Module.Syntax
import Language.Module.SyntaxADT
import qualified Language.Module.TypeInference as MI
import qualified Language.Module.Verify as MV
import qualified Language.R.Refresh as RR
import Language.R.Syntax
import Language.R.SyntaxADT
import qualified Language.R.TypeInference as RI
import qualified Language.R.Verify as RV
-------------------------------------------------------------------------------
runCommand :: Command -> GalcStateT Bool
-------------------------------------------------------------------------------
runCommand Abort =
inMode [SetProofMode, ProofMode, IndirectProofMode, FinalProofMode] $
resetProof >> galcShow "Aborted..."
-------------------------------------------------------------------------------
runCommand (Assume l) =
keepGoing . addAssumption =<< compileLaw l
-------------------------------------------------------------------------------
runCommand Auto =
inMode [ProofMode, IndirectProofMode] $ solve
-------------------------------------------------------------------------------
runCommand (Browse mdl) = keepGoing $ do
modules <- getLoadedModules
when (not $ mdl `elem` modules) (throwError (ModuleRefError mdl))
showLaws =<< getLaws mdl
showDefinitions =<< getDefinitions mdl
showGCs =<< getGCs mdl
-------------------------------------------------------------------------------
runCommand (Comb comb) = inMode [ProofMode, IndirectProofMode] $ do
rl <- evalCombinator comb
Exists t r <- getCurExpr
showExpr =<< maybe (return (Exists t r))
(\(expr,proof) -> do
addProofStep (Exists t expr) proof
return (Exists t expr))
(rewrite rl t r)
-------------------------------------------------------------------------------
runCommand (Define def) =
keepGoing . addDefinition =<< compileR def
-------------------------------------------------------------------------------
runCommand (Derive drv) = keepGoing . showLaw =<< evalDerivation drv
-------------------------------------------------------------------------------
runCommand Help = keepGoing . galcShow $ helpScreen
-------------------------------------------------------------------------------
runCommand Hint = inMode [ProofMode, IndirectProofMode] $ do
Exists t r <- getCurExpr
modules <- getLoadedModules
lws <- foldM (\res v -> (getLaws v >>= \x -> return (x++res))) [] modules
return ()
-------------------------------------------------------------------------------
runCommand (IndirectUp ord) =
inMode [ProofMode] . setIndirectProof . Left =<< compileR ord
-------------------------------------------------------------------------------
runCommand (IndirectLow ord) =
inMode [ProofMode] . setIndirectProof . Right =<< compileR ord
-------------------------------------------------------------------------------
runCommand IndirectOut =
inMode [IndirectProofMode] endIndirectProof
-------------------------------------------------------------------------------
runCommand (Info _) = undefined
-------------------------------------------------------------------------------
runCommand LeftP =
inMode [SetProofMode] chooseLeft
-------------------------------------------------------------------------------
runCommand (Load mdl) = keepGoing $ do
modules <- getLoadedModules
when (mdl `elem` modules) (runCommand (Unload mdl) >> return ())
addModule mdl =<< compileModule =<< MP.parser =<< readModule mdl
galcShow $ "Module loaded: " ++ mdl
-------------------------------------------------------------------------------
runCommand Modules =
keepGoing . showModules =<< getLoadedModules
-------------------------------------------------------------------------------
runCommand (Prove prf) =
inMode [GlobalMode] . setProof =<< compileLaw prf
-------------------------------------------------------------------------------
runCommand Qed = inMode [ProofMode] $ qed >> showProof
-------------------------------------------------------------------------------
runCommand Quit = return True
-------------------------------------------------------------------------------
runCommand Reload =
inMode [GlobalMode] .
mapM_ (\m -> runCommand (Unload m) >> runCommand (Load m)) =<<
getLoadedModules
-------------------------------------------------------------------------------
runCommand Restart =
inMode [ProofMode, IndirectProofMode, FinalProofMode] restartProof
-------------------------------------------------------------------------------
runCommand RightP =
inMode [SetProofMode] chooseRight
-------------------------------------------------------------------------------
runCommand Rules = keepGoing . galcShow $ rulesScreen
-------------------------------------------------------------------------------
runCommand Save =
inMode [FinalProofMode] saveProof
-------------------------------------------------------------------------------
runCommand Show =
inMode [SetProofMode, ProofMode, IndirectProofMode, FinalProofMode] showProof
-------------------------------------------------------------------------------
runCommand (Type expr) = keepGoing . galcShow . show =<< compileR expr
-------------------------------------------------------------------------------
runCommand (Undo mn) =
inMode [ProofMode, IndirectProofMode] . undo . maybe 1 id $ mn
-------------------------------------------------------------------------------
runCommand (Unload nm) =
inMode [GlobalMode] . removeModule $ nm
-------------------------------------------------------------------------------
inMode :: [OpMode] -> GalcStateT () -> GalcStateT Bool
inMode lmod a = keepGoing $ do
cmod <- getOpMode
if cmod `elem` lmod then a else throwError ModeError
-------------------------------------------------------------------------------
solve :: GalcStateT ()
solve = undefined
-------------------------------------------------------------------------------
showLaw :: Law -> GalcStateT ()
showLaw = galcShow . pretty
-------------------------------------------------------------------------------
showLaws :: [Law] -> GalcStateT ()
showLaws lst = do
galcShow "Laws:"
mapM_ showLaw lst
-------------------------------------------------------------------------------
showDefinitions :: [RType] -> GalcStateT ()
showDefinitions defs = do
galcShow "Definitions:"
mapM_ showExpr defs
-------------------------------------------------------------------------------
showExpr :: RType -> GalcStateT ()
showExpr = galcShow . show
-------------------------------------------------------------------------------
showProof :: GalcStateT ()
showProof = undefined
-------------------------------------------------------------------------------
showModules :: [String] -> GalcStateT ()
showModules [] = galcShow "No loaded modules"
showModules mds = do
galcShow "Loaded Modules:"
mapM_ galcShow mds
-------------------------------------------------------------------------------
rulesScreen :: String
rulesScreen =
"--------------------------------------------------\n" ++
"Available Rules\n" ++
"--------------------------------------------------\n" ++
"Shunting\t\t\tshunt\n" ++
"Distributive (upper adjoint)\tdistr_up\n" ++
"Distributive (lower adjoint)\tdistr_low\n" ++
"Monotonicity (upper adjoint)\tmonot_up\n" ++
"Monotonicity (lower adjoint)\tmonot_low\n" ++
"Top preserving\t\t\ttop_preserving\n" ++
"Bottom preserving\t\tbot_preserving\n" ++
"Cancellation (upper adjoint)\tcanc_up\n" ++
"Cancellation (lower adjoint)\tcanc_low\n" ++
"Free theorem\t\t\tfree\n" ++
"General law\t\t\tapply <law name>\n"
-------------------------------------------------------------------------------
showGCs :: [RType] -> GalcStateT ()
showGCs gclst = do
galcShow "Galois connections:"
mapM_ showExpr gclst
-------------------------------------------------------------------------------
compileR :: S -> GalcStateT RType
compileR s = do
env <- getEnvironment
RI.infer =<< RR.refresh =<< RV.verify env s
-------------------------------------------------------------------------------
compileLaw :: LawS -> GalcStateT Law
compileLaw l = do
env <- getEnvironment
LI.infer =<< LR.refresh =<< LV.verify env l
-------------------------------------------------------------------------------
compileModule :: ModuleS -> GalcStateT Module
compileModule = MI.infer <=< MR.refresh <=< MV.verify
-------------------------------------------------------------------------------
readModule :: String -> GalcStateT String
readModule mdl =
either2error (const $ ModuleFileError mdl) <=<
liftIO . Control.Exception.try . readFile $ mdl ++ ".gal"
-------------------------------------------------------------------------------
galcShow :: String -> GalcStateT ()
galcShow = liftIO . putStrLn
-------------------------------------------------------------------------------
keepGoing :: GalcStateT () -> GalcStateT Bool
keepGoing arg = arg >> return False
-------------------------------------------------------------------------------
helpScreen :: String
helpScreen = "Help"
-------------------------------------------------------------------------------
|
