fb2d914 · Idris-dev · git.iko.soy

27parseCmd i inputname = P.runparser pCmd i inputname

28

29cmd :: [String] -> P.IdrisParser ()

30−cmd xs = do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs)

30+cmd xs = try (do P.lchar ':'; docmd (sortBy (\x y -> compare (length y) (length x)) xs))

31 where docmd [] = fail "No such command"

32 docmd (x:xs) = try (discard (P.symbol x)) <|> docmd xs

33

34pCmd :: P.IdrisParser Command

35−pCmd = do P.whiteSpace; try (do cmd ["q", "quit"]; eof; return Quit)

35+pCmd = do P.whiteSpace; do cmd ["q", "quit"]; eof; return Quit

36− <|> try (do cmd ["h", "?", "help"]; eof; return Help)

36+ <|> do cmd ["h", "?", "help"]; eof; return Help

37− <|> try (do cmd ["w", "warranty"]; eof; return Warranty)

37+ <|> do cmd ["w", "warranty"]; eof; return Warranty

38− <|> try (do cmd ["r", "reload"]; eof; return Reload)

38+ <|> do cmd ["r", "reload"]; eof; return Reload

39− <|> try (do cmd ["module"]; f <- P.identifier; eof;

39+ <|> do cmd ["module"]; f <- P.identifier; eof;

40− return (ModImport (toPath f)))

40+ return (ModImport (toPath f))

41− <|> try (do cmd ["e", "edit"]; eof; return Edit)

41+ <|> do cmd ["e", "edit"]; eof; return Edit

42− <|> try (do cmd ["exec", "execute"]; eof; return Execute)

42+ <|> do cmd ["exec", "execute"]; eof; return Execute

43− <|> try (do cmd ["c", "compile"]

43+ <|> do cmd ["c", "compile"]

44− i <- get

44+ i <- get

45− c <- option (opt_codegen $ idris_options i) codegenOption

45+ c <- option (opt_codegen $ idris_options i) codegenOption

46− f <- P.identifier

46+ f <- P.identifier

47− eof

47+ eof

48− return (Compile c f))

48+ return (Compile c f)

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

49+ <|> do cmd ["proofs"]; eof; return Proofs

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

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

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

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

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

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

53− <|> try (do cmd ["let"]

53+ <|> do cmd ["let"]

54− defn <- concat <$> many (P.decl defaultSyntax)

54+ defn <- concat <$> many (P.decl defaultSyntax)

55− return (NewDefn defn))

55+ return (NewDefn defn)

56− <|> try (do cmd ["lto", "loadto"];

56+ <|> do cmd ["lto", "loadto"];

57− toline <- P.natural

57+ toline <- P.natural

58− f <- many anyChar;

58+ f <- many anyChar;

59− return (Load f (Just (fromInteger toline))))

59+ return (Load f (Just (fromInteger toline)))

60− <|> try (do cmd ["l", "load"]; f <- many anyChar;

60+ <|> do cmd ["l", "load"]; f <- many anyChar;

61− return (Load f Nothing))

61+ return (Load f Nothing)

62− <|> try (do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f))

62+ <|> do cmd ["cd"]; f <- many anyChar; return (ChangeDirectory f)

63− <|> try (do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t))

63+ <|> do cmd ["spec"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Spec t)

64− <|> try (do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t))

64+ <|> do cmd ["hnf"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (HNF t)

65− <|> try (do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t))

65+ <|> do cmd ["inline"]; P.whiteSpace; t <- P.fullExpr defaultSyntax; return (TestInline t)

66− <|> try (do cmd ["doc"]; c <- P.constant; eof; return (DocStr (Right c)))

66+ <|> do c <- try (cmd ["doc"] *> P.constant); eof; return (DocStr (Right c))

67− <|> try (do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n)))

67+ <|> do cmd ["doc"]; n <- (P.fnName <|> (P.string "_|_" >> return falseTy)); eof; return (DocStr (Left n))

68− <|> try (do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n))

68+ <|> do cmd ["d", "def"]; P.whiteSpace; n <- P.fnName; eof; return (Defn n)

69− <|> try (do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n))

69+ <|> do cmd ["total"]; do n <- P.fnName; eof; return (TotCheck n)

70− <|> try (do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t))

70+ <|> do cmd ["t", "type"]; do P.whiteSpace; t <- P.fullExpr defaultSyntax; return (Check t)

71− <|> try (do cmd ["u", "universes"]; eof; return Universes)

71+ <|> do cmd ["u", "universes"]; eof; return Universes

72− <|> try (do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n))

72+ <|> do cmd ["di", "dbginfo"]; n <- P.fnName; eof; return (DebugInfo n)

73− <|> try (do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n))

73+ <|> do cmd ["miss", "missing"]; n <- P.fnName; eof; return (Missing n)

74 <|> try (do cmd ["dynamic"]; eof; return ListDynamic)

75− <|> try (do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l))

75+ <|> do cmd ["dynamic"]; l <- many anyChar; return (DynamicLink l)

76− <|> try (do cmd ["color", "colour"]; pSetColourCmd)

76+ <|> do cmd ["color", "colour"]; pSetColourCmd

77− <|> try (do cmd ["set"]; o <- pOption; return (SetOpt o))

77+ <|> do cmd ["set"]; o <- pOption; return (SetOpt o)

78− <|> try (do cmd ["unset"]; o <- pOption; return (UnsetOpt o))

78+ <|> do cmd ["unset"]; o <- pOption; return (UnsetOpt o)

79− <|> try (do cmd ["s", "search"]; P.whiteSpace;

79+ <|> do cmd ["s", "search"]; P.whiteSpace;

80− t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t))

80+ t <- P.typeExpr (defaultSyntax { implicitAllowed = True }); return (Search t)

81− <|> try (do cmd ["cs", "casesplit"]; P.whiteSpace;

81+ <|> do cmd ["cs", "casesplit"]; P.whiteSpace;

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

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

83− l <- P.natural; n <- P.name;

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

84− return (CaseSplitAt upd (fromInteger l) n))

84+ return (CaseSplitAt upd (fromInteger l) n)

85− <|> try (do cmd ["apc", "addproofclause"]; P.whiteSpace;

85+ <|> do cmd ["apc", "addproofclause"]; P.whiteSpace;

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

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

87− l <- P.natural; n <- P.name;

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

88− return (AddProofClauseFrom upd (fromInteger l) n))

88+ return (AddProofClauseFrom upd (fromInteger l) n)

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

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

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

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

91− l <- P.natural; n <- P.name;

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

92− return (AddClauseFrom upd (fromInteger l) n))

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

93− <|> try (do cmd ["am", "addmissing"]; P.whiteSpace;

93+ <|> do cmd ["am", "addmissing"]; P.whiteSpace;

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

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

95− l <- P.natural; n <- P.name;

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

96− return (AddMissing upd (fromInteger l) n))

96+ return (AddMissing upd (fromInteger l) n)

97− <|> try (do cmd ["mw", "makewith"]; P.whiteSpace;

97+ <|> do cmd ["mw", "makewith"]; P.whiteSpace;

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

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

99− l <- P.natural; n <- P.name;

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

100− return (MakeWith upd (fromInteger l) n))

100+ return (MakeWith upd (fromInteger l) n)

101− <|> try (do cmd ["ml", "makelemma"]; P.whiteSpace;

101+ <|> do cmd ["ml", "makelemma"]; P.whiteSpace;

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

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

103− l <- P.natural; n <- P.name;

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

104− return (MakeLemma upd (fromInteger l) n))

104+ return (MakeLemma upd (fromInteger l) n)

105− <|> try (do cmd ["ps", "proofsearch"]; P.whiteSpace;

105+ <|> do cmd ["ps", "proofsearch"]; P.whiteSpace;

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

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

107− l <- P.natural; n <- P.name;

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

108− hints <- many P.fnName

108+ hints <- many P.fnName

109− return (DoProofSearch upd True (fromInteger l) n hints))

109+ return (DoProofSearch upd True (fromInteger l) n hints)

110− <|> try (do cmd ["ref", "refine"]; P.whiteSpace;

110+ <|> do cmd ["ref", "refine"]; P.whiteSpace;

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

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

112− l <- P.natural; n <- P.name;

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

113− hint <- P.fnName

113+ hint <- P.fnName

114− return (DoProofSearch upd False (fromInteger l) n [hint]))

114+ return (DoProofSearch upd False (fromInteger l) n [hint])

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

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

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

116+ <|> do cmd ["m", "metavars"]; eof; return Metavars

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

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

118− return (Just x))

118+ return (Just x))

119− eof; return (AddProof n))

119+ eof; return (AddProof n)

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

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

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

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

122− <|> try (do cmd ["errorhandlers"]; eof ; return ListErrorHandlers)

122+ <|> do cmd ["errorhandlers"]; eof ; return ListErrorHandlers

123− <|> try (do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w))

123+ <|> do cmd ["consolewidth"]; w <- pConsoleWidth ; return (SetConsoleWidth w)

124− <|> try (do cmd ["apropos"]; str <- many anyChar ; return (Apropos str))

124+ <|> do cmd ["apropos"]; str <- many anyChar ; return (Apropos str)

125− <|> try (do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n))

125+ <|> do cmd ["wc", "whocalls"]; P.whiteSpace; n <- P.fnName ; return (WhoCalls n)

126− <|> try (do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n))

126+ <|> do cmd ["cw", "callswho"]; P.whiteSpace; n <- P.fnName ; return (CallsWho n)

127− <|> try (do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str))

127+ <|> do cmd ["mkdoc"]; str <- many anyChar; return (MakeDoc str)

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

129 <|> do t <- P.fullExpr defaultSyntax; return (Eval t)

130