@@ -23,7 +23,7 @@ import Data.List.Split(splitOn)
2323import Data.Char(toLower)
2424import qualified Data.ByteString.UTF8 as UTF8
2525
26−parseCmd :: IState -> String -> String -> Result Command
26+parseCmd :: IState -> String -> String -> Result (Either String Command)
2727parseCmd i inputname = P.runparser pCmd i inputname
2828
2929cmd :: [String] -> P.IdrisParser ()
@@ -31,109 +31,108 @@ cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length
3131 where docmd [] = fail "No such command"
3232 docmd (x:xs) = try (discard (P.reserved x)) <|> docmd xs
3333
34−pCmd :: P.IdrisParser Command
35−
36−pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit
37− <|> do cmd ["h", "?", "help"]; eof; return Help
38− <|> do cmd ["w", "warranty"]; eof; return Warranty
39− <|> do cmd ["r", "reload"]; eof; return Reload
34+pCmd :: P.IdrisParser (Either String Command)
35+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return (Right Quit)
36+ <|> do cmd ["h", "?", "help"]; eof; return (Right Help)
37+ <|> do cmd ["w", "warranty"]; eof; return (Right Warranty)
38+ <|> do cmd ["r", "reload"]; eof; return (Right Reload)
4039 <|> do cmd ["module"]; f <- P.identifier; eof;
41− return (ModImport (toPath f))
42− <|> do cmd ["e", "edit"]; eof; return Edit
43− <|> do cmd ["exec", "execute"]; eof; return Execute
40+ return (Right (ModImport (toPath f)))
41+ <|> do cmd ["e", "edit"]; eof; return (Right Edit)
42+ <|> do cmd ["exec", "execute"]; ((try $ eof >> return (Right Execute)) <|> return (Left "exec(ute) does not take any parameters"))
4443 <|> try (do cmd ["c", "compile"]
4544 i <- get
4645 f <- P.identifier
4746 eof
48− return (Compile (Via "c") f))
47+ return (Right (Compile (Via "c") f)))
4948 <|> do cmd ["c", "compile"]
5049 i <- get
5150 c <- codegenOption
5251 f <- P.identifier
5352 eof
54− return (Compile c f)
55− <|> do cmd ["proofs"]; eof; return Proofs
56− <|> do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n)
57− <|> do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n)
58− <|> do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i))
53+ return (Right (Compile c f))
54+ <|> do cmd ["proofs"]; eof; return (Right Proofs)
55+ <|> do cmd ["rmproof"]; n <- P.name; eof; return (Right (RmProof n))
56+ <|> do cmd ["showproof"]; n <- P.name; eof; return (Right (ShowProof n))
57+ <|> do cmd ["log"]; i <- P.natural; eof; return (Right (LogLvl (fromIntegral i)))
5958 <|> do cmd ["let"]
6059 defn <- concat <$> many (P.decl defaultSyntax)
61− return (NewDefn defn)
60+ return (Right (NewDefn defn))
6261 <|> do cmd ["unlet","undefine"]
63− Undefine `fmap` many P.name
62+ (Right . Undefine) `fmap` many P.name
6463 <|> do cmd ["lto", "loadto"];
6564 toline <- P.natural
6665 f <- many anyChar;
67− return (Load f (Just (fromInteger toline)))
66+ return (Right (Load f (Just (fromInteger toline))))
6867 <|> do cmd ["l", "load"]; f <- many anyChar;
69− return (Load f Nothing)
70− <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)
71− <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)
72− <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)
73− <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)
74− <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))
75− <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))
76− <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)
77− <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)
78− <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)
79− <|> do cmd ["u", "universes"]; eof; return Universes
80− <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)
81− <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)
82− <|> try (do cmd ["dynamic"]; eof; return ListDynamic)
83− <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)
84− <|> do cmd ["color", "colour"]; pSetColourCmd
85− <|> do cmd ["set"]; o <- pOption; return (SetOpt o)
86− <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)
68+ return (Right (Load f Nothing))
69+ <|> do cmd ["cd"]; f <- many anyChar; return (Right (ChangeDirectory f))
70+ <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Spec t))
71+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (HNF t))
72+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (TestInline t))
73+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (Right (DocStr (Right c)))
74+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (Right (DocStr (Left n)))
75+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Right (Defn n))
76+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (Right (TotCheck n))
77+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Check t))
78+ <|> do cmd ["u", "universes"]; eof; return (Right Universes)
79+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (Right (DebugInfo n))
80+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Right (Missing n))
81+ <|> try (do cmd ["dynamic"]; eof; return (Right ListDynamic))
82+ <|> do cmd ["dynamic"]; l <- many anyChar; return (Right (DynamicLink l))
83+ <|> do cmd ["color", "colour"]; pSetColourCmd >>= return . Right
84+ <|> do cmd ["set"]; o <- pOption; return (Right (SetOpt o))
85+ <|> do cmd ["unset"]; o <- pOption; return (Right (UnsetOpt o))
8786 <|> do cmd ["s", "search"]; P.whiteSpace;
88− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)
87+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Right (Search t))
8988 <|> do cmd ["cs", "casesplit"]; P.whiteSpace;
9089 upd <- option False (do P.lchar '!'; return True)
9190 l <- P.natural; n <- P.name;
92− return (CaseSplitAt upd (fromInteger l) n)
91+ return (Right (CaseSplitAt upd (fromInteger l) n))
9392 <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;
9493 upd <- option False (do P.lchar '!'; return True)
9594 l <- P.natural; n <- P.name;
96− return (AddProofClauseFrom upd (fromInteger l) n)
95+ return (Right (AddProofClauseFrom upd (fromInteger l) n))
9796 <|> do cmd ["ac", "addclause"]; P.whiteSpace;
9897 upd <- option False (do P.lchar '!'; return True)
9998 l <- P.natural; n <- P.name;
100− return (AddClauseFrom upd (fromInteger l) n)
99+ return (Right (AddClauseFrom upd (fromInteger l) n))
101100 <|> do cmd ["am", "addmissing"]; P.whiteSpace;
102101 upd <- option False (do P.lchar '!'; return True)
103102 l <- P.natural; n <- P.name;
104− return (AddMissing upd (fromInteger l) n)
103+ return (Right (AddMissing upd (fromInteger l) n))
105104 <|> do cmd ["mw", "makewith"]; P.whiteSpace;
106105 upd <- option False (do P.lchar '!'; return True)
107106 l <- P.natural; n <- P.name;
108− return (MakeWith upd (fromInteger l) n)
107+ return (Right (MakeWith upd (fromInteger l) n))
109108 <|> do cmd ["ml", "makelemma"]; P.whiteSpace;
110109 upd <- option False (do P.lchar '!'; return True)
111110 l <- P.natural; n <- P.name;
112− return (MakeLemma upd (fromInteger l) n)
111+ return (Right (MakeLemma upd (fromInteger l) n))
113112 <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;
114113 upd <- option False (do P.lchar '!'; return True)
115114 l <- P.natural; n <- P.name;
116115 hints <- many P.fnName
117− return (DoProofSearch upd True (fromInteger l) n hints)
116+ return (Right (DoProofSearch upd True (fromInteger l) n hints))
118117 <|> do cmd ["ref", "refine"]; P.whiteSpace;
119118 upd <- option False (do P.lchar '!'; return True)
120119 l <- P.natural; n <- P.name;
121120 hint <- P.fnName
122− return (DoProofSearch upd False (fromInteger l) n [hint])
123− <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n)
124− <|> do cmd ["m", "metavars"]; eof; return Metavars
121+ return (Right (DoProofSearch upd False (fromInteger l) n [hint]))
122+ <|> do cmd ["p", "prove"]; n <- P.name; eof; return (Right (Prove n))
123+ <|> do cmd ["m", "metavars"]; eof; return (Right Metavars)
125124 <|> do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;
126125 return (Just x))
127− eof; return (AddProof n)
128− <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t)
129− <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t)
130− <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers
131− <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)
132− <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)
133− <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)
134− <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)
135− <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)
136− <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (PrintDef n)
126+ eof; return (Right (AddProof n))
127+ <|> do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (ExecVal t))
128+ <|> do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Right (Pattelab t))
129+ <|> do cmd ["errorhandlers"]; eof ; return (Right ListErrorHandlers)
130+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (Right (SetConsoleWidth w))
131+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Right (Apropos str))
132+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (Right (WhoCalls n))
133+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (Right (CallsWho n))
134+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (Right (MakeDoc str))
135+ <|> do cmd ["printdef"]; P.whiteSpace; n <- P.fnName; return (Right (PrintDef n))
137136 <|> do cmd ["pp", "pprint"]
138137 P.whiteSpace
139138 fmt <- ppFormat
@@ -141,9 +140,9 @@ pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit
141140 n <- fmap fromInteger P.natural
142141 P.whiteSpace
143142 t <- P.fullExpr defaultSyntax
144− return (PPrint fmt n t)
145− <|> do P.whiteSpace; do eof; return NOP
146− <|> do t <- P.fullExpr defaultSyntax; return (Eval t)
143+ return (Right (PPrint fmt n t))
144+ <|> do P.whiteSpace; do eof; return (Right NOP)
145+ <|> do t <- P.fullExpr defaultSyntax; return (Right (Eval t))
147146
148147 where toPath n = foldl1' (</>) $ splitOn "." n
149148