edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-06 21:28:25 +03:00
Code Issues Projects Releases Wiki Activity

[wip] process returns result object instead of printing directly

Browse Source
This commit is contained in:
Arnaud Bailly 2019-10-13 19:50:05 +02:00
parent 85e6e9ca7a
commit 4485b16ef8
1 changed files with 152 additions and 154 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

294
src/Idris/REPL.idr
View File

@ -210,7 +210,7 @@ setOpt (Editor e)
setOpt (CG e) setOpt (CG e)
= case getCG e of = case getCG e of
Just cg => setCG cg Just cg => setCG cg
Nothing => coreLift $ putStrLn "No such code generator available" Nothing => iputStrLn "No such code generator available"
findCG : {auto c : Ref Ctxt Defs} -> Core Codegen findCG : {auto c : Ref Ctxt Defs} -> Core Codegen
findCG findCG
@ -220,38 +220,6 @@ findCG
Chicken => pure codegenChicken Chicken => pure codegenChicken
Racket => pure codegenRacket Racket => pure codegenRacket
export
compileExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> String -> Core ()
compileExp ctm outfile
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
ok <- compile !findCG tm_erased outfile
maybe (pure ())
(\fname => iputStrLn (outfile ++ " written"))
ok
export
execExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
PTerm -> Core ()
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
inidx <- resolveName (UN "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
execute !findCG tm_erased
anyAt : (FC -> Bool) -> FC -> a -> Bool anyAt : (FC -> Bool) -> FC -> a -> Bool
anyAt p loc y = p loc anyAt p loc y = p loc
@ -277,12 +245,18 @@ lookupDefTyName : Name -> Context ->
Core (List (Name, Int, (Def, ClosedTerm))) Core (List (Name, Int, (Def, ClosedTerm)))
lookupDefTyName = lookupNameBy (\g => (definition g, type g)) lookupDefTyName = lookupNameBy (\g => (definition g, type g))
public export
data EditResult : Type where
DisplayEdit : List String -> EditResult
EditError : String -> EditResult
MadeLemma : Name -> PTerm -> String -> EditResult
processEdit : {auto c : Ref Ctxt Defs} -> processEdit : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
EditCmd -> Core () EditCmd -> Core EditResult
processEdit (TypeAt line col name) processEdit (TypeAt line col name)
= do defs <- get Ctxt = do defs <- get Ctxt
glob <- lookupCtxtName name (gamma defs) glob <- lookupCtxtName name (gamma defs)
@ -293,23 +267,23 @@ processEdit (TypeAt line col name)
Just (n, num, t) <- findTypeAt (\p, n => within (line-1, col-1) p) Just (n, num, t) <- findTypeAt (\p, n => within (line-1, col-1) p)
| Nothing => if res == "" | Nothing => if res == ""
then throw (UndefinedName (MkFC "(interactive)" (0,0) (0,0)) name) then throw (UndefinedName (MkFC "(interactive)" (0,0) (0,0)) name)
else printResult res else pure (DisplayEdit [res])
if res == "" if res == ""
then printResult (nameRoot n ++ " : " ++ then pure (DisplayEdit [ nameRoot n ++ " : " ++
!(displayTerm defs t)) !(displayTerm defs t)])
else pure () else pure (DisplayEdit []) -- ? Why () This means there is a global name and a type at (line,col)
processEdit (CaseSplit line col name) processEdit (CaseSplit line col name)
= do let find = if col > 0 = do let find = if col > 0
then within (line-1, col-1) then within (line-1, col-1)
else onLine (line-1) else onLine (line-1)
OK splits <- getSplits (anyAt find) name OK splits <- getSplits (anyAt find) name
| SplitFail err => printError (show err) | SplitFail err => pure (EditError (show err))
lines <- updateCase splits (line-1) (col-1) lines <- updateCase splits (line-1) (col-1)
printResult $ showSep "\n" lines ++ "\n" pure $ DisplayEdit lines
processEdit (AddClause line name) processEdit (AddClause line name)
= do Just c <- getClause line name = do Just c <- getClause line name
| Nothing => printError (show name ++ " not defined here") | Nothing => pure (EditError (show name ++ " not defined here"))
printResult c pure $ DisplayEdit [c]
processEdit (ExprSearch line name hints all) processEdit (ExprSearch line name hints all)
= do defs <- get Ctxt = do defs <- get Ctxt
syn <- get Syn syn <- get Syn
@ -324,15 +298,15 @@ processEdit (ExprSearch line name hints all)
do let (_ ** (env, tm')) = dropLams locs [] tm do let (_ ** (env, tm')) = dropLams locs [] tm
resugar env tm') restms) resugar env tm') restms)
if all if all
then printResult $ showSep "\n" (map show itms) then pure $ DisplayEdit (map show itms)
else case itms of else case itms of
[] => printError "No search results" [] => pure $ EditError "No search results"
(x :: xs) => printResult (x :: xs) => pure $ DisplayEdit
(show (if brack [show (if brack
then addBracket replFC x then addBracket replFC x
else x)) else x)]
[] => printError $ "Unknown name " ++ show name [] => pure $ EditError $ "Unknown name " ++ show name
_ => printError "Not a searchable hole" _ => pure $ EditError "Not a searchable hole"
where where
dropLams : Nat -> Env Term vars -> Term vars -> dropLams : Nat -> Env Term vars -> Term vars ->
(vars' ** (Env Term vars', Term vars')) (vars' ** (Env Term vars', Term vars'))
@ -342,17 +316,17 @@ processEdit (ExprSearch line name hints all)
processEdit (GenerateDef line name) processEdit (GenerateDef line name)
= do defs <- get Ctxt = do defs <- get Ctxt
Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p) Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine line p)
| Nothing => printError ("Can't find declaration for " ++ show name ++ " on line " ++ show line) | Nothing => pure (EditError ("Can't find declaration for " ++ show name ++ " on line " ++ show line))
case !(lookupDefExact n' (gamma defs)) of case !(lookupDefExact n' (gamma defs)) of
Just None => Just None =>
catch catch
(do Just (fc, cs) <- makeDef (\p, n => onLine line p) n' (do Just (fc, cs) <- makeDef (\p, n => onLine line p) n'
| Nothing => processEdit (AddClause line name) | Nothing => processEdit (AddClause line name)
ls <- traverse (printClause (cast (snd (startPos fc)))) cs ls <- traverse (printClause (cast (snd (startPos fc)))) cs
printResult $ showSep "\n" ls) pure $ DisplayEdit ls)
(\err => printError $ "Can't find a definition for " ++ show n') (\err => pure $ EditError $ "Can't find a definition for " ++ show n')
Just _ => printError "Already defined" Just _ => pure $ EditError "Already defined"
Nothing => printError $ "Can't find declaration for " ++ show name Nothing => pure $ EditError $ "Can't find declaration for " ++ show name
processEdit (MakeLemma line name) processEdit (MakeLemma line name)
= do defs <- get Ctxt = do defs <- get Ctxt
syn <- get Syn syn <- get Syn
@ -366,24 +340,77 @@ processEdit (MakeLemma line name)
let pappstr = show (if brack let pappstr = show (if brack
then addBracket replFC papp then addBracket replFC papp
else papp) else papp)
case idemode opts of pure $ MadeLemma name pty pappstr
REPL _ => printResult (show name ++ " : " ++ show pty ++ "\n" ++ pappstr) _ => pure $ EditError "Can't make lifted definition"
IDEMode i _ f =>
send f (SExpList [SymbolAtom "return",
SExpList [SymbolAtom "ok",
SExpList [SymbolAtom "metavariable-lemma",
SExpList [SymbolAtom "replace-metavariable",
StringAtom pappstr],
SExpList [SymbolAtom "definition-type",
StringAtom (show name ++ " : " ++ show pty)]]],
toSExp i])
_ => printError "Can't make lifted definition"
processEdit (MakeCase line name) processEdit (MakeCase line name)
= printError "Not implemented yet" = pure $ EditError "Not implemented yet"
processEdit (MakeWith line name) processEdit (MakeWith line name)
= do Just l <- getSourceLine line = do Just l <- getSourceLine line
| Nothing => printError "Source line not available" | Nothing => pure (EditError "Source line not available")
printResult (makeWith name l) pure $ DisplayEdit [makeWith name l]
public export
data MissedResult : Type where
CasesMissing : Name -> List String -> MissedResult
CallsNonCovering : Name -> List a -> MissedResult
AllCasesCovered : Name -> MissedResult
public export
data REPLResult : Type where
Done : REPLResult
REPLError : String -> REPLResult
Executed : PTerm -> REPLResult
Evaluated : PTerm -> (Maybe PTerm) -> REPLResult
Printed : List String -> REPLResult
TermChecked : PTerm -> PTerm -> REPLResult
FileLoaded : String -> REPLResult
ErrorsLoadingFile : String -> List a -> REPLResult
NoFileLoaded : REPLResult
ChangedDirectory : String -> REPLResult
CompilationFailed: REPLResult
Compiled : String -> REPLResult
ProofFound : PTerm -> REPLResult
Missed : List MissedResult -> REPLResult
CheckedTotal : List (Name, Totality) -> REPLResult
FoundHoles : List Name -> REPLResult
LogLevelSet : Nat -> REPLResult
VersionIs : Version -> REPLResult
Exited : REPLResult
Edited : EditResult -> REPLResult
export
execExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
PTerm -> Core REPLResult
execExp ctm
= do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
inidx <- resolveName (UN "[input]")
(tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
execute !findCG tm_erased
pure $ Executed ctm
export
compileExp : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} ->
PTerm -> String -> Core REPLResult
compileExp ctm outfile
= do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN "unsafePerformIO")) ctm)
(tm, gty) <- elabTerm inidx InExpr [] (MkNested [])
[] ttimp Nothing
tm_erased <- linearCheck replFC Rig1 True [] tm
ok <- compile !findCG tm_erased outfile
maybe (pure CompilationFailed)
(pure . Compiled)
ok
export export
loadMainFile : {auto c : Ref Ctxt Defs} -> loadMainFile : {auto c : Ref Ctxt Defs} ->
@ -391,27 +418,35 @@ loadMainFile : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
String -> Core () String -> Core REPLResult
loadMainFile f loadMainFile f
= do resetContext = do resetContext
Right res <- coreLift (readFile f) Right res <- coreLift (readFile f)
| Left err => do emitError (FileErr f err) | Left err => do setSource ""
setSource "" pure (ErrorsLoadingFile f [err])
updateErrorLine !(buildDeps f) errs <- buildDeps f
updateErrorLine errs
setSource res setSource res
case errs of
[] => pure (FileLoaded f)
_ => pure (ErrorsLoadingFile f errs)
-- Returns 'True' if the REPL should continue
||| Process a single `REPLCmd`
|||
||| Returns `REPLResult` for display by the higher level shell which
||| is invoking this interactive command processing.
export export
process : {auto c : Ref Ctxt Defs} -> process : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
REPLCmd -> Core Bool REPLCmd -> Core REPLResult
process (Eval itm) process (Eval itm)
= do opts <- get ROpts = do opts <- get ROpts
case evalMode opts of case evalMode opts of
Execute => do execExp itm; pure True Execute => do execExp itm; pure (Executed itm)
_ => _ =>
do ttimp <- desugar AnyExpr [] itm do ttimp <- desugar AnyExpr [] itm
inidx <- resolveName (UN "[input]") inidx <- resolveName (UN "[input]")
@ -424,9 +459,8 @@ process (Eval itm)
if showTypes opts if showTypes opts
then do ty <- getTerm gty then do ty <- getTerm gty
ity <- resugar [] !(norm defs [] ty) ity <- resugar [] !(norm defs [] ty)
printResult (show itm ++ " : " ++ show ity) pure (Evaluated itm (Just ity))
else printResult (show itm) else pure (Evaluated itm Nothing)
pure True
where where
emode : REPLEval -> ElabMode emode : REPLEval -> ElabMode
emode EvalTC = InType emode EvalTC = InType
@ -440,8 +474,7 @@ process (Check (PRef fc fn))
case !(lookupCtxtName fn (gamma defs)) of case !(lookupCtxtName fn (gamma defs)) of
[] => throw (UndefinedName fc fn) [] => throw (UndefinedName fc fn)
ts => do tys <- traverse (displayType defs) ts ts => do tys <- traverse (displayType defs) ts
printResult (showSep "\n" tys) pure (Printed tys)
pure True
process (Check itm) process (Check itm)
= do inidx <- resolveName (UN "[input]") = do inidx <- resolveName (UN "[input]")
ttimp <- desugar AnyExpr [] itm ttimp <- desugar AnyExpr [] itm
@ -451,48 +484,38 @@ process (Check itm)
itm <- resugar [] !(normaliseHoles defs [] tm) itm <- resugar [] !(normaliseHoles defs [] tm)
ty <- getTerm gty ty <- getTerm gty
ity <- resugar [] !(normaliseScope defs [] ty) ity <- resugar [] !(normaliseScope defs [] ty)
printResult (show itm ++ " : " ++ show ity) pure (TermChecked itm ity)
pure True
process (PrintDef fn) process (PrintDef fn)
= do defs <- get Ctxt = do defs <- get Ctxt
case !(lookupCtxtName fn (gamma defs)) of case !(lookupCtxtName fn (gamma defs)) of
[] => throw (UndefinedName replFC fn) [] => throw (UndefinedName replFC fn)
ts => do defs <- traverse (displayPats defs) ts ts => do defs <- traverse (displayPats defs) ts
printResult (showSep "\n" defs) pure (Printed defs)
pure True
process Reload process Reload
= do opts <- get ROpts = do opts <- get ROpts
case mainfile opts of case mainfile opts of
Nothing => do printError "No file loaded" Nothing => pure NoFileLoaded
pure True Just f => loadMainFile f
Just f => do loadMainFile f
pure True
process (Load f) process (Load f)
= do opts <- get ROpts = do opts <- get ROpts
put ROpts (record { mainfile = Just f } opts) put ROpts (record { mainfile = Just f } opts)
-- Clear the context and load again -- Clear the context and load again
loadMainFile f loadMainFile f
pure True
process (CD dir) process (CD dir)
= do setWorkingDir dir = do setWorkingDir dir
printResult ("Changed directory to " ++ dir) pure (ChangedDirectory dir)
pure True
process Edit process Edit
= do opts <- get ROpts = do opts <- get ROpts
case mainfile opts of case mainfile opts of
Nothing => do coreLift $ putStrLn "No file loaded" Nothing => pure NoFileLoaded
pure True
Just f => Just f =>
do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts) do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
coreLift $ system (editor opts ++ " " ++ f ++ line) coreLift $ system (editor opts ++ " " ++ f ++ line)
loadMainFile f loadMainFile f
pure True
process (Compile ctm outfile) process (Compile ctm outfile)
= do compileExp ctm outfile = compileExp ctm outfile
pure True
process (Exec ctm) process (Exec ctm)
= do execExp ctm = execExp ctm
pure True
process (ProofSearch n_in) process (ProofSearch n_in)
= do defs <- get Ctxt = do defs <- get Ctxt
[(n, i, ty)] <- lookupTyName n_in (gamma defs) [(n, i, ty)] <- lookupTyName n_in (gamma defs)
@ -500,91 +523,67 @@ process (ProofSearch n_in)
| ns => throw (AmbiguousName replFC (map fst ns)) | ns => throw (AmbiguousName replFC (map fst ns))
tm <- search replFC RigW False 1000 n ty [] tm <- search replFC RigW False 1000 n ty []
itm <- resugar [] !(normaliseHoles defs [] tm) itm <- resugar [] !(normaliseHoles defs [] tm)
printResult (show itm) pure $ ProofFound itm
pure True
process (Missing n) process (Missing n)
= do defs <- get Ctxt = do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName replFC n) [] => throw (UndefinedName replFC n)
ts => do traverse (\fn => ts => map Missed $ traverse (\fn =>
do tot <- getTotality replFC fn do tot <- getTotality replFC fn
the (Core ()) $ case isCovering tot of the (Core MissedResult) $ case isCovering tot of
MissingCases cs => MissingCases cs =>
do tms <- traverse (displayPatTerm defs) cs do tms <- traverse (displayPatTerm defs) cs
printResult (show fn ++ ":\n" ++ pure $ CasesMissing fn tms
showSep "\n" tms)
NonCoveringCall ns_in => NonCoveringCall ns_in =>
do ns <- traverse getFullName ns_in do ns <- traverse getFullName ns_in
printResult pure $ CallsNonCovering fn ns
(show fn ++ ": Calls non covering function" _ => pure $ AllCasesCovered fn)
++ case ns of
[fn] => " " ++ show fn
_ => "s: " ++ showSep ", " (map show ns))
_ => printResult (show fn ++ ": All cases covered"))
(map fst ts) (map fst ts)
pure True
process (Total n) process (Total n)
= do defs <- get Ctxt = do defs <- get Ctxt
case !(lookupCtxtName n (gamma defs)) of case !(lookupCtxtName n (gamma defs)) of
[] => throw (UndefinedName replFC n) [] => throw (UndefinedName replFC n)
ts => do traverse (\fn => ts => map CheckedTotal $
traverse (\fn =>
do checkTotal replFC fn do checkTotal replFC fn
tot <- getTotality replFC fn tot <- getTotality replFC fn
iputStrLn (show fn ++ " is " ++ show !(toFullNames tot))) pure $ (fn, tot))
(map fst ts) (map fst ts)
pure True
process (DebugInfo n) process (DebugInfo n)
= do defs <- get Ctxt = do defs <- get Ctxt
traverse_ showInfo !(lookupCtxtName n (gamma defs)) traverse_ showInfo !(lookupCtxtName n (gamma defs))
pure True pure Done
process (SetOpt opt) process (SetOpt opt)
= do setOpt opt = do setOpt opt
pure True pure Done
process (SetLog lvl) process (SetLog lvl)
= do setLogLevel lvl = do setLogLevel lvl
printResult $ "Log level to set " ++ show lvl pure $ LogLevelSet lvl
pure True
process Metavars process Metavars
= do ms <- getUserHoles = do ms <- getUserHoles
case ms of pure $ FoundHoles ms
[] => printResult $ "No holes"
[x] => printResult $ "1 hole: " ++ show x
xs => printResult $ show (length xs) ++ " holes: " ++
showSep ", " (map show xs)
pure True
process (Editing cmd) process (Editing cmd)
= do ppopts <- getPPrint = do ppopts <- getPPrint
-- Since we're working in a local environment, don't do the usual -- Since we're working in a local environment, don't do the usual
-- thing of printing out the full environment for parameterised -- thing of printing out the full environment for parameterised
-- calls or calls in where blocks -- calls or calls in where blocks
setPPrint (record { showFullEnv = False } ppopts) setPPrint (record { showFullEnv = False } ppopts)
processEdit cmd res <- processEdit cmd
setPPrint ppopts setPPrint ppopts
pure True pure $ Edited res
process Quit process Quit
= pure False = pure Exited
process NOP process NOP
= pure True = pure Done
process ShowVersion process ShowVersion
= do opts <- get ROpts = pure $ VersionIs version
case idemode opts of
REPL _ => do iputStrLn $ showVersion version
pure True
IDEMode i _ f => do
let MkVersion (maj, min, patch) t = version
send f (SExpList [SymbolAtom "return",
SExpList [SymbolAtom "ok",
SExpList [SExpList (map (IntegerAtom . cast) [maj, min, patch]),
SExpList [ StringAtom $ fromMaybe "" t ]]],
toSExp i])
pure False
processCatch : {auto c : Ref Ctxt Defs} -> processCatch : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} -> {auto u : Ref UST UState} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
REPLCmd -> Core Bool REPLCmd -> Core REPLResult
processCatch cmd processCatch cmd
= do c' <- branch = do c' <- branch
u' <- get UST u' <- get UST
@ -598,8 +597,8 @@ processCatch cmd
put UST u' put UST u'
put Syn s' put Syn s'
put ROpts o' put ROpts o'
printError !(display err) pure $ REPLError !(display err)
pure True) )
parseEmptyCmd : EmptyRule (Maybe REPLCmd) parseEmptyCmd : EmptyRule (Maybe REPLCmd)
parseEmptyCmd = eoi *> (pure Nothing) parseEmptyCmd = eoi *> (pure Nothing)
@ -631,12 +630,11 @@ interpret : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} -> {auto s : Ref Syn SyntaxInfo} ->
{auto m : Ref MD Metadata} -> {auto m : Ref MD Metadata} ->
{auto o : Ref ROpts REPLOpts} -> {auto o : Ref ROpts REPLOpts} ->
String -> Core Bool String -> Core REPLResult
interpret inp interpret inp
= case parseRepl inp of = case parseRepl inp of
Left err => do printError (show err) Left err => pure $ REPLError (show err)
pure True Right Nothing => pure Done
Right Nothing => pure True
Right (Just cmd) => processCatch cmd Right (Just cmd) => processCatch cmd
export export