aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Main.hs30
1 files changed, 30 insertions, 0 deletions
diff --git a/src/Main.hs b/src/Main.hs
index bcb1f00..61dc3bc 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -37,6 +37,33 @@ splitOn spl (x:xs)
| otherwise = let (r : rs) = splitOn spl xs in (x:r) : rs
+usageString :: String
+usageString =
+ "\x1B[1mMeta-commands\x1B[0m\n\
+ \ env -- Show the current environment\n\
+ \ exit -- Exit program immediately\n\
+ \ undo -- Undo last operation\n\
+ \ focus \x1B[4mx\x1B[0m -- Watch and operate on given variable\n\
+ \ focus -- Unfocus currently focused variable\n\
+ \ log -- Print list of commands that reproduces current environment\n\
+ \ help -- Show this help\n\
+ \\n\
+ \\x1B[1mExpression rewrite commands\x1B[0m\n\
+ \These commands operate on the currently-focused expression.\n\
+ \ rew \x1B[4mx\x1B[0m -- Replaces occurrences of \x1B[4mx\x1B[0m with its value\n\
+ \ beta -- Applies some beta-reductions ((\\x -> M) y => M[y/x])\n\
+ \ eta -- Applies some eta-reductions ((\\x -> f x) => f)\n\
+ \ case -- Evaluates case statements\n\
+ \ case! -- Evaluates case statements, choosing first hit if multiple branches unify\n\
+ \ etacase -- If all case branches are the same as their patterns, remove case statement\n\
+ \ casecase -- case (case x of {A->a;B->b}) of {C->c;D->d} \n\
+ \ => case x of {A->case a of {C->c;D->d}; B->case b of {C->c;D->d}}\n\
+ \ repeat \x1B[4mcmd\x1B[0m -- Repeat \x1B[4mcmd\x1B[0m until no change occurs\n\
+ \\n\
+ \To evaluate a rewrite command on an unfocused variable, use:\n\
+ \ action \x1B[4mx\x1B[0m \x1B[4mcmd\x1B[0m -- Evaluate \x1B[4mcmd\x1B[0m on variable \x1B[4mx\x1B[0m"
+
+
data AppState = AppState { asCtx :: Context, asFocus :: Maybe Name }
deriving (Show)
@@ -64,6 +91,7 @@ data UserCmd = UCCmd Cmd
| CUnFocus
| CFocus Name
| CLog
+ | CHelp
deriving (Show)
instance Pretty Action where
@@ -145,6 +173,7 @@ applyUserCmd appstate = \case
CLog -> do
mapM_ (putStrLn . pretty) $ map fst (reverse $ cStack (asCtx appstate))
return (Right (Just appstate))
+ CHelp -> putStrLn usageString >> return (Right (Just appstate))
applyUserCmds :: AppState -> [UserCmd] -> IO (Either String (Maybe AppState))
applyUserCmds appstate [] = return (Right (Just appstate))
@@ -200,6 +229,7 @@ parseCmd ["env"] = Right CShowEnv
parseCmd ["focus"] = Right CUnFocus
parseCmd ["focus", name] = Right (CFocus name)
parseCmd ["log"] = Right CLog
+parseCmd ["help"] = Right CHelp
parseCmd ["rew", func] = Right (UCCmd (CRewrite func))
parseCmd ["beta"] = Right (UCCmd CBeta)
parseCmd ["eta"] = Right (UCCmd CEta)