46256ab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add ':addclause' command at the REPL

46256abEdwin Brady13 years ago

contribs/idriscasesplit.vim+52−8

compare with master

unifiedsplit

@@ -1,21 +1,65 @@

1+function IdrisReload()

2+ let tc = system("idris --client :r")

3+ if (! (tc is ""))

4+ echo tc

5+ endif

6+ return tc

7+endfunction

9+function IdrisShowType()

10+ let word = expand("<cword>")

11+ let tc = IdrisReload()

12+ if (! (tc is ""))

13+ echo tc

14+ else

15+ let ty = system("idris --client :t " . word)

16+ echo ty

17+ endif

18+ return tc

19+endfunction

2−function CaseSplit()

21+function IdrisCaseSplit()

3 let view = winsaveview()

22 let view = winsaveview()

4 w

23 w

5 let cline = line(".")

24 let cline = line(".")

6 let word = expand("<cword>")

25 let word = expand("<cword>")

7− let fn = "idris --client :cs! " . cline . " " . word

26+ let tc = IdrisReload()

8− let tc = system("idris --client :r")

27+

9 if (tc is "")

28 if (tc is "")

29+ let fn = "idris --client :cs! " . cline . " " . word

10 let result = system(fn)

30 let result = system(fn)

11− e

12− call winrestview(view)

13 if (! (result is ""))

31 if (! (result is ""))

14 echo result

32 echo result

33+ else

34+ e

35+ call winrestview(view)

15 endif

36 endif

16− else

17− echo tc

18 endif

37 endif

19endfunction

38endfunction

21−map ci :call CaseSplit()<ENTER>

40+function IdrisAddClause()

41+ let view = winsaveview()

42+ w

43+ let cline = line(".")

44+ let word = expand("<cword>")

45+ let tc = IdrisReload()

46+

47+ if (tc is "")

48+ let fn = "idris --client :ac! " . cline . " " . word

49+ let result = system(fn)

50+ if (! (result is ""))

51+ echo result

52+ else

53+ e

54+ call winrestview(view)

55+ call search(word)

56+

57+ endif

58+ endif

59+endfunction

60+

61+map ct :call IdrisShowType()<ENTER>

62+map cr :call IdrisReload()<ENTER>

63+map ci :call IdrisCaseSplit()<ENTER>

64+map cd ?:<ENTER>b:call IdrisAddClause()<ENTER>w

65+

src/Idris/AbsSyntax.hs+6−6

@@ -668,7 +668,7 @@ piBind = piBindp expl

668

669piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm

670piBindp p [] t = t

671−piBindp p ((n, ty):ns) t = PPi p n ty (piBind ns t)

671+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

672

673-- Dealing with parameters

674

@@ -761,7 +761,7 @@ expandParamsD :: Bool -> -- True = RHS only

761expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)

762 = if n `elem` ns && (not rhsonly)

763 then -- trace (show (n, expandParams dec ps ns ty)) $

764− PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns [] ty))

764+ PTy doc syn fc o (dec n) (piBindp expl_param ps (expandParams dec ps ns [] ty))

765 else --trace (show (n, expandParams dec ps ns ty)) $

766 PTy doc syn fc o n (expandParams dec ps ns [] ty)

767expandParamsD rhsonly ist dec ps ns (PPostulate doc syn fc o n ty)

@@ -989,13 +989,13 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

989 = do (decls, ns) <- get

990 let isn = concatMap (namesIn uvars ist) (map getTm as)

991 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

992− imps top env (PPi (Imp l _ doc) n ty sc)

992+ imps top env (PPi (Imp l _ doc _) n ty sc)

993 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

994 (decls , ns) <- get

995 put (PImp (getPriority ist ty) True l n ty doc : decls,

996 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

997 imps True (n:env) sc

998− imps top env (PPi (Exp l _ doc) n ty sc)

998+ imps top env (PPi (Exp l _ doc _) n ty sc)

999 = do let isn = nub (namesIn uvars ist ty ++ case sc of

1000 (PRef _ x) -> namesIn uvars ist sc `dropAll` [n]

1001 _ -> [])

@@ -1057,8 +1057,8 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

1057 pibind using [] sc = sc

1058 pibind using (n:ns) sc

1059 = case lookup n using of

1060− Just ty -> PPi (Imp False Dynamic "") n ty (pibind using ns sc)

1060+ Just ty -> PPi (Imp False Dynamic "" False) n ty (pibind using ns sc)

1061− Nothing -> PPi (Imp False Dynamic "") n Placeholder

1061+ Nothing -> PPi (Imp False Dynamic "" False) n Placeholder

1062 (pibind using ns sc)

1063

1064-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+15−9

@@ -241,6 +241,7 @@ data Command = Quit

241 | Search PTerm

242 | CaseSplit Name PTerm

243 | CaseSplitAt Bool Int Name

244+ | AddClauseFrom Bool Int Name

244 | SetOpt Opt

245 | SetOpt Opt

245 | UnsetOpt Opt

246 | UnsetOpt Opt

246 | NOP

247 | NOP

@@ -331,10 +332,12 @@ deriving instance Binary Static

331-- Mark bindings with their explicitness, and laziness

332-- Mark bindings with their explicitness, and laziness

332data Plicity = Imp { plazy :: Bool,

333data Plicity = Imp { plazy :: Bool,

333 pstatic :: Static,

334 pstatic :: Static,

334− pdocstr :: String }

335+ pdocstr :: String,

336+ pparam :: Bool }

335 | Exp { plazy :: Bool,

337 | Exp { plazy :: Bool,

336 pstatic :: Static,

338 pstatic :: Static,

337− pdocstr :: String }

339+ pdocstr :: String,

340+ pparam :: Bool }

338 | Constraint { plazy :: Bool,

341 | Constraint { plazy :: Bool,

339 pstatic :: Static,

342 pstatic :: Static,

340 pdocstr :: String }

343 pdocstr :: String }

@@ -348,8 +351,9 @@ data Plicity = Imp { plazy :: Bool,

348deriving instance Binary Plicity

351deriving instance Binary Plicity

349!-}

352!-}

350

353

351−impl = Imp False Dynamic ""

354+impl = Imp False Dynamic "" False

352−expl = Exp False Dynamic ""

355+expl = Exp False Dynamic "" False

356+expl_param = Exp False Dynamic "" True

353constraint = Constraint False Dynamic ""

357constraint = Constraint False Dynamic ""

354tacimpl t = TacImp False Dynamic t ""

358tacimpl t = TacImp False Dynamic t ""

355

359

@@ -916,7 +920,7 @@ prettyImp impl = prettySe 10

916 else

920 else

917 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

921 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

918 prettySe 10 sc

922 prettySe 10 sc

919− prettySe p (PPi (Exp l s _) n ty sc)

923+ prettySe p (PPi (Exp l s _ _) n ty sc)

920 | n `elem` allNamesIn sc || impl =

924 | n `elem` allNamesIn sc || impl =

921 let open = if l then text "|" <> lparen else lparen in

925 let open = if l then text "|" <> lparen else lparen in

922 bracket p 2 $

926 bracket p 2 $

@@ -937,7 +941,7 @@ prettyImp impl = prettySe 10

937 case s of

941 case s of

938 Static -> text "[static]"

942 Static -> text "[static]"

939 _ -> empty

943 _ -> empty

940− prettySe p (PPi (Imp l s _) n ty sc)

944+ prettySe p (PPi (Imp l s _ _) n ty sc)

941 | impl =

945 | impl =

942 let open = if l then text "|" <> lbrace else lbrace in

946 let open = if l then text "|" <> lbrace else lbrace in

943 bracket p 2 $

947 bracket p 2 $

@@ -1128,18 +1132,20 @@ showImp ist impl colour tm = se 10 [] tm where

1128 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

1132 se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++

1129 " = " ++ se 10 bnd v ++

1133 " = " ++ se 10 bnd v ++

1130 " in " ++ se 10 ((n, False):bnd) sc

1134 " in " ++ se 10 ((n, False):bnd) sc

1131− se p bnd (PPi (Exp l s _) n ty sc)

1135+ se p bnd (PPi (Exp l s _ param) n ty sc)

1132 | n `elem` allNamesIn sc || impl

1136 | n `elem` allNamesIn sc || impl

1133 = bracket p 2 $

1137 = bracket p 2 $

1134 (if l then "|(" else "(") ++

1138 (if l then "|(" else "(") ++

1135 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1139 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1140+ ") " ++

1141+ (if (impl && param) then "P" else "") ++

1136− ") " ++ st ++

1142+ st ++

1137 "-> " ++ se 10 ((n, False):bnd) sc

1143 "-> " ++ se 10 ((n, False):bnd) sc

1138 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

1144 | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc

1139 where st = case s of

1145 where st = case s of

1140 Static -> "[static] "

1146 Static -> "[static] "

1141 _ -> ""

1147 _ -> ""

1142− se p bnd (PPi (Imp l s _) n ty sc)

1148+ se p bnd (PPi (Imp l s _ _) n ty sc)

1143 | impl = bracket p 2 $ (if l then "|{" else "{") ++

1149 | impl = bracket p 2 $ (if l then "|{" else "{") ++

1144 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1150 perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++

1145 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

1151 "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc

src/Idris/CaseSplit.hs+18−1

@@ -1,6 +1,6 @@

1{-# LANGUAGE PatternGuards #-}

3−module Idris.CaseSplit(split, splitOnLine, replaceSplits) where

3+module Idris.CaseSplit(split, splitOnLine, replaceSplits, getClause) where

5-- splitting a variable in a pattern clause

@@ -224,5 +224,22 @@ replaceSplits l ups = map (rep (expandBraces l)) ups

224 addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

225 | otherwise = tm

226

227+getClause :: Int -> -- ^ Line type is declared on

228+ Name -> -- ^ Function name

229+ FilePath -> -- ^ Source file name

230+ Idris String

231+getClause l fn fp = do ty <- getInternalApp fp l

232+ let ap = mkApp ty [1..]

233+ return (show fn ++ " " ++ ap ++

234+ "= ?" ++ show fn ++ "_rhs")

235+ where mkApp (PPi (Exp _ _ _ False) (MN _ _) _ sc) (n : ns)

236+ = "x" ++ show n ++ " " ++ mkApp sc ns

237+ mkApp (PPi (Exp _ _ _ False) n _ sc) ns

238+ = show n ++ " " ++ mkApp sc ns

239+ mkApp (PPi _ _ _ sc) ns = mkApp sc ns

240+ mkApp _ _ = ""

241+

242+

243+

227

244

228

245

src/Idris/ElabDecls.hs+17−11

@@ -52,9 +52,15 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

52 do checkUndefined fc n

53 ctxt <- getContext

54 i <- getIState

55+

56+ -- Add user one, not implicitsed one

57+ addInternalApp (fc_fname fc) (fc_line fc) ty'

58+ addIBC (IBCLineApp (fc_fname fc) (fc_line fc) ty')

59+

55 logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

60 logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

56 ty' <- addUsingConstraints syn fc ty'

61 ty' <- addUsingConstraints syn fc ty'

57 ty' <- implicit syn n ty'

62 ty' <- implicit syn n ty'

63+

58 let ty = addImpl i ty'

64 let ty = addImpl i ty'

59 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

65 logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

60 ((tyT, defer, is), log) <-

66 ((tyT, defer, is), log) <-

@@ -406,10 +412,10 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

406 show fn ++ " (" ++ show ty ++ ")"

412 show fn ++ " (" ++ show ty ++ ")"

407 putIState i)

413 putIState i)

408

414

409− getImplB k (PPi (Imp l s _) n Placeholder sc)

415+ getImplB k (PPi (Imp l s _ _) n Placeholder sc)

410 = getImplB k sc

416 = getImplB k sc

411− getImplB k (PPi (Imp l s d) n ty sc)

417+ getImplB k (PPi (Imp l s d p) n ty sc)

412− = getImplB (\x -> k (PPi (Imp l s d) n ty x)) sc

418+ = getImplB (\x -> k (PPi (Imp l s d p) n ty x)) sc

413 getImplB k (PPi _ n ty sc)

419 getImplB k (PPi _ n ty sc)

414 = getImplB k sc

420 = getImplB k sc

415 getImplB k _ = k

421 getImplB k _ = k

@@ -1244,8 +1250,8 @@ elabClass info syn doc fc constraints tn ps ds

1244 return [PTy doc syn fc o m ty',

1250 return [PTy doc syn fc o m ty',

1245 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1251 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1246

1252

1247− getMArgs (PPi (Imp _ _ _) n ty sc) = IA : getMArgs sc

1253+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

1248− getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

1254+ getMArgs (PPi (Exp _ _ _ _) n ty sc) = EA : getMArgs sc

1249 getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1255 getMArgs (PPi (Constraint _ _ _) n ty sc) = CA : getMArgs sc

1250 getMArgs _ = []

1256 getMArgs _ = []

1251

1257

@@ -1262,14 +1268,14 @@ elabClass info syn doc fc constraints tn ps ds

1262 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1268 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

1263 rhsArgs [] _ = []

1269 rhsArgs [] _ = []

1264

1270

1265− insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

1271+ insertConstraint c (PPi p@(Imp _ _ _ _) n ty sc)

1266 = PPi p n ty (insertConstraint c sc)

1272 = PPi p n ty (insertConstraint c sc)

1267 insertConstraint c sc = PPi constraint (MN 0 "class") c sc

1273 insertConstraint c sc = PPi constraint (MN 0 "class") c sc

1268

1274

1269 -- make arguments explicit and don't bind class parameters

1275 -- make arguments explicit and don't bind class parameters

1270− toExp ns e (PPi (Imp l s _) n ty sc)

1276+ toExp ns e (PPi (Imp l s _ p) n ty sc)

1271 | n `elem` ns = toExp ns e sc

1277 | n `elem` ns = toExp ns e sc

1272− | otherwise = PPi (e l s "") n ty (toExp ns e sc)

1278+ | otherwise = PPi (e l s "" p) n ty (toExp ns e sc)

1273 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1279 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

1274 toExp ns e sc = sc

1280 toExp ns e sc = sc

1275

1281

@@ -1364,9 +1370,9 @@ elabInstance info syn fc cs n ps t expn ds

1364 lamBind i (PPi _ n ty sc) sc'

1370 lamBind i (PPi _ n ty sc) sc'

1365 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

1371 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

1366 lamBind i _ sc = sc

1372 lamBind i _ sc = sc

1367− methArgs i (PPi (Imp _ _ _) n ty sc)

1373+ methArgs i (PPi (Imp _ _ _ _) n ty sc)

1368 = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1374 = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1369− methArgs i (PPi (Exp _ _ _) n ty sc)

1375+ methArgs i (PPi (Exp _ _ _ _) n ty sc)

1370 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1376 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1371 methArgs i (PPi (Constraint _ _ _) n ty sc)

1377 methArgs i (PPi (Constraint _ _ _) n ty sc)

1372 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

1378 = PConstraint 0 False (PResolveTC fc) "" : methArgs (i+1) sc

@@ -1393,7 +1399,7 @@ elabInstance info syn fc cs n ps t expn ds

1393 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1399 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)

1394 conbind [] x = x

1400 conbind [] x = x

1395

1401

1396− coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1402+ coninsert cs (PPi p@(Imp _ _ _ _) n t sc) = PPi p n t (coninsert cs sc)

1397 coninsert cs sc = conbind cs sc

1403 coninsert cs sc = conbind cs sc

1398

1404

1399 insertDefaults :: IState -> Name ->

1405 insertDefaults :: IState -> Name ->

src/Idris/IBC.hs+9−5

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

25ibcVersion :: Word8

26−ibcVersion = 43

26+ibcVersion = 44

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -1008,16 +1008,18 @@ instance Binary Static where

1008instance Binary Plicity where

1009 put x

1010 = case x of

1011− Imp x1 x2 x3 ->

1011+ Imp x1 x2 x3 x4 ->

1012 do putWord8 0

1013 put x1

1014 put x2

1015 put x3

1016+ put x4

1016− Exp x1 x2 x3 ->

1017+ Exp x1 x2 x3 x4 ->

1017 do putWord8 1

1018 do putWord8 1

1018 put x1

1019 put x1

1019 put x2

1020 put x2

1020 put x3

1021 put x3

1022+ put x4

1021 Constraint x1 x2 x3 ->

1023 Constraint x1 x2 x3 ->

1022 do putWord8 2

1024 do putWord8 2

1023 put x1

1025 put x1

@@ -1035,11 +1037,13 @@ instance Binary Plicity where

1035 0 -> do x1 <- get

1037 0 -> do x1 <- get

1036 x2 <- get

1038 x2 <- get

1037 x3 <- get

1039 x3 <- get

1040+ x4 <- get

1038− return (Imp x1 x2 x3)

1041+ return (Imp x1 x2 x3 x4)

1039 1 -> do x1 <- get

1042 1 -> do x1 <- get

1040 x2 <- get

1043 x2 <- get

1041 x3 <- get

1044 x3 <- get

1045+ x4 <- get

1042− return (Exp x1 x2 x3)

1046+ return (Exp x1 x2 x3 x4)

1043 2 -> do x1 <- get

1047 2 -> do x1 <- get

1044 x2 <- get

1048 x2 <- get

1045 x3 <- get

1049 x3 <- get

src/Idris/ParseExpr.hs+3−3

@@ -699,7 +699,7 @@ pi syn =

699 doc <- option "" (docComment '^')

700 symbol "->"

701 sc <- expr syn

702− return (bindList (PPi (Exp lazy st doc)) xt sc)) <|> (do

702+ return (bindList (PPi (Exp lazy st doc False)) xt sc)) <|> (do

703 lchar '{'

704 (do reserved "auto"

705 when (lazy || (st == Static)) $ fail "auto type constraints can not be lazy or static"

@@ -722,13 +722,13 @@ pi syn =

722 t <- expr' syn

723 symbol "->"

724 sc <- expr syn

725− return (PPi (Exp False Static "") (MN 42 "__pi_arg") t sc)) <|> (

725+ return (PPi (Exp False Static "" False) (MN 42 "__pi_arg") t sc)) <|> (

726 if implicitAllowed syn then do

727 xt <- typeDeclList syn

728 lchar '}'

729 symbol "->"

730 sc <- expr syn

731− return (bindList (PPi (Imp lazy st "")) xt sc)

731+ return (bindList (PPi (Imp lazy st "" False)) xt sc)

732 else do fail "no implicit arguments allowed here"))

733 <?> "dependent type signature"

734

src/Idris/REPL.hs+23−1

@@ -140,8 +140,10 @@ processNetCmd stvar orig i h fn cmd

140 processNet fn Reload =

141 do let ist = orig { idris_options = idris_options i

142 , idris_colourTheme = idris_colourTheme i

143+ , idris_colourRepl = False

143 }

144 }

144− putIState orig

145+ putIState ist

146+ setErrContext True

145 setOutH h

147 setOutH h

146 setQuiet True

148 setQuiet True

147 setVerbose False

149 setVerbose False

@@ -511,6 +513,26 @@ process h fn (CaseSplitAt updatefile l n)

511 runIO $ copyFile fb fn

513 runIO $ copyFile fb fn

512 else do ihputStrLn h (show res)

514 else do ihputStrLn h (show res)

513 ihputStrLn h new

515 ihputStrLn h new

516+process h fn (AddClauseFrom updatefile l n)

517+ = do src <- runIO $ readFile fn

518+ let (before, tyline : later) = splitAt (l-1) (lines src)

519+ let indent = getIndent 0 (show n) tyline

520+ cl <- getClause l n fn

521+ -- add clause before first blank line in 'later'

522+ let (nonblank, rest) = span (not . all isSpace) (tyline:later)

523+ if updatefile then

524+ do let fb = fn ++ "~"

525+ runIO $ writeFile fb (unlines (before ++ nonblank)

526+ ++ replicate indent ' ' ++

527+ cl ++ "\n" ++

528+ unlines rest)

529+ runIO $ copyFile fb fn

530+ else ihputStrLn h cl

531+ where

532+ getIndent i n [] = 0

533+ getIndent i n xs | take (length n) xs == n = i

534+ getIndent i n (x : xs) = getIndent (i + 1) n xs

535+

514

536

515

537

516process h fn (Spec t)

538process h fn (Spec t)

src/Idris/REPLParser.hs+7−3

@@ -45,9 +45,6 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

45 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

46 <|> try (do cmd ["proofs"]; eof; return Proofs)

47 <|> try (do cmd ["p", "prove"]; n <- P.name; eof; return (Prove n))

48− <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

49− return (Just x))

50− eof; return (AddProof n))

51 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

48 <|> try (do cmd ["rmproof"]; n <- P.name; eof; return (RmProof n))

52 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

49 <|> try (do cmd ["showproof"]; n <- P.name; eof; return (ShowProof n))

53 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

50 <|> try (do cmd ["log"]; i <- P.natural; eof; return (LogLvl (fromIntegral i)))

@@ -78,6 +75,13 @@ pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

78 n <- P.name;

75 n <- P.name;

79 t <- P.fullExpr defaultSyntax;

76 t <- P.fullExpr defaultSyntax;

80 return (CaseSplit n t))

77 return (CaseSplit n t))

78+ <|> try (do cmd ["ac", "addclause"]; P.whiteSpace;

79+ upd <- option False (do P.lchar '!'; return True)

80+ l <- P.natural; n <- P.name;

81+ return (AddClauseFrom upd (fromInteger l) n))

82+ <|> try (do cmd ["a", "addproof"]; do n <- option Nothing (do x <- P.name;

83+ return (Just x))

84+ eof; return (AddProof n))

81 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

85 <|> try (do cmd ["x"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (ExecVal t))

82 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

86 <|> try (do cmd ["patt"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Pattelab t))

83 <|> do P.whiteSpace; do eof; return NOP

87 <|> do P.whiteSpace; do eof; return NOP