f936366 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1817 from bmsherman/repl

f936366Edwin Brady12 years ago

libs/prelude/Builtins.idr+2−2

compare with master

unifiedsplit

@@ -116,14 +116,14 @@ par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

116 -- is better in any case?

117par (Delay x) = x

118

119−||| Assert to the totality checker than y is always structurally smaller than

119+||| Assert to the totality checker that y is always structurally smaller than

120||| x (which is typically a pattern argument)

121||| @ x the larger value (typically a pattern argument)

122||| @ y the smaller value (typically an argument to a recursive call)

123assert_smaller : (x : a) -> (y : b) -> b

124assert_smaller x y = y

125

126−||| Assert to the totality checker than the given expression will always

126+||| Assert to the totality checker that the given expression will always

127||| terminate.

128assert_total : a -> a

129assert_total x = x

src/Idris/Completion.hs+13−46

@@ -8,7 +8,9 @@ import Idris.AbsSyntaxTree

8import Idris.Help

9import Idris.Colours

10import Idris.ParseHelpers(opChars)

11−

11+import qualified Idris.ParseExpr (constants, tactics)

12+import Idris.ParseExpr (TacticArg (..))

13+import Idris.REPLParser (allHelp)

12import Control.Monad.State.Strict

14import Control.Monad.State.Strict

14import Data.List

16import Data.List

@@ -19,44 +21,11 @@ import System.Console.Haskeline

19import System.Console.ANSI (Color)

21import System.Console.ANSI (Color)

22−fst3 :: (a, b, c) -> a

23−fst3 (a, b, c) = a

24−

25−commands = concatMap fst3 (help ++ extraHelp)

24+commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

26−

27−-- | A specification of the arguments that tactics can take

28−data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

29− | ExprTArg

30− | AltsTArg

32−-- The FIXMEs are Issue #1766 in the issue tracker.

33−-- https://github.com/idris-lang/Idris-dev/issues/1766

34−-- | A list of available tactics and their argument requirements

35tacticArgs :: [(String, Maybe TacticArg)]

26tacticArgs :: [(String, Maybe TacticArg)]

36−tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

27+tacticArgs = [ (name, args) | (names, args, _) <- Idris.ParseExpr.tactics

37− , ("refine", Just ExprTArg)

28+ , name <- names ]

38− , ("mrefine", Just ExprTArg)

39− , ("rewrite", Just ExprTArg)

40− , ("let", Nothing) -- FIXME syntax for let

41− , ("focus", Just ExprTArg)

42− , ("exact", Just ExprTArg)

43− , ("equiv", Just ExprTArg)

44− , ("applyTactic", Just ExprTArg)

45− , ("byReflection", Just ExprTArg)

46− , ("reflect", Just ExprTArg)

47− , ("fill", Just ExprTArg)

48− , ("try", Just AltsTArg)

49− , ("induction", Just ExprTArg)

50− , ("case", Just ExprTArg)

51− , (":t", Just ExprTArg)

52− , (":type", Just ExprTArg)

53− , (":e", Just ExprTArg)

54− , (":eval", Just ExprTArg)

55− ] ++ map (\x -> (x, Nothing)) [

56− "intros", "compute", "trivial", "search", "solve", "attack",

57− "unify", "state", "term", "undo", "qed", "abandon", ":q",

58− "sourceLocation"

59− ]

60tactics = map fst tacticArgs

29tactics = map fst tacticArgs

62-- | Convert a name into a string usable for completion. Filters out names

31-- | Convert a name into a string usable for completion. Filters out names

@@ -77,10 +46,7 @@ names = do i <- get

77 let ctxt = tt_ctxt i

46 let ctxt = tt_ctxt i

78 return . nub $

47 return . nub $

79 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++

48 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++

80− -- Explicitly add primitive types, as these are special-cased in the parser

49+ "Type" : map fst Idris.ParseExpr.constants

81− ["Int", "Integer", "Float", "Char", "String", "Type",

82− "Ptr", "Bits8", "Bits16", "Bits32", "Bits64",

83− "Bits8x16", "Bits16x8", "Bits32x4", "Bits64x2"]

85metavars :: Idris [String]

51metavars :: Idris [String]

86metavars = do i <- get

52metavars = do i <- get

@@ -129,7 +95,7 @@ isWhitespace :: Char -> Bool

129isWhitespace = (flip elem) " \t\n"

95isWhitespace = (flip elem) " \t\n"

130

131lookupInHelp :: String -> Maybe CmdArg

97lookupInHelp :: String -> Maybe CmdArg

132−lookupInHelp cmd = lookupInHelp' cmd help

98+lookupInHelp cmd = lookupInHelp' cmd allHelp

133 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg

99 where lookupInHelp' cmd ((cmds, arg, _):xs) | elem cmd cmds = Just arg

134 | otherwise = lookupInHelp' cmd xs

100 | otherwise = lookupInHelp' cmd xs

135 lookupInHelp' cmd [] = Nothing

101 lookupInHelp' cmd [] = Nothing

@@ -195,10 +161,11 @@ completeTactic :: [String] -> String -> CompletionFunc Idris

195completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $

161completeTactic as tac (prev, next) = fromMaybe completeTacName . fmap completeArg $

196 lookup tac tacticArgs

162 lookup tac tacticArgs

197 where completeTacName = return $ ("", completeWith tactics tac)

163 where completeTacName = return $ ("", completeWith tactics tac)

198− completeArg Nothing = noCompletion (prev, next)

164+ completeArg Nothing = noCompletion (prev, next)

199− completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!

165+ completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!

200− completeArg (Just ExprTArg) = completeExpr as (prev, next)

166+ completeArg (Just ExprTArg) = completeExpr as (prev, next)

167+ completeArg (Just StringLitTArg) = noCompletion (prev, next)

201− completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO

168+ completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO

202

169

203-- | Complete tactics and their arguments

170-- | Complete tactics and their arguments

204proverCompletion :: [String] -- ^ The names of current local assumptions

171proverCompletion :: [String] -- ^ The names of current local assumptions

src/Idris/Help.hs+2−50

@@ -1,4 +1,4 @@

1−module Idris.Help (CmdArg(..), help, extraHelp) where

1+module Idris.Help (CmdArg(..), extraHelp) where

3data CmdArg = ExprArg -- ^ The command takes an expression

4 | NameArg -- ^ The command takes a name

@@ -37,62 +37,14 @@ instance Show CmdArg where

37 show (OptionalArg a) = "[" ++ show a ++ "]"

38 show (SeqArgs a b) = show a ++ " " ++ show b

40−help :: [([String], CmdArg, String)]

41−help =

42− [ (["<expr>"], NoArg, "Evaluate an expression"),

43− ([":t"], ExprArg, "Check the type of an expression"),

44− ([":miss", ":missing"], NameArg, "Show missing clauses"),

45− ([":doc"], NameArg, "Show internal documentation"),

46− ([":mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"),

47− ([":apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"),

48− ([":search", ":s"], SeqArgs (OptionalArg PkgArgs) ExprArg, " Search for values by type"),

49− ([":whocalls", ":wc"], NameArg, "List the callers of some name"),

50− ([":callswho", ":cw"], NameArg, "List the callees of some name"),

51− ([":total"], NameArg, "Check the totality of a name"),

52− ([":r",":reload"], NoArg, "Reload current file"),

53− ([":l",":load"], FileArg, "Load a new file"),

54− ([":cd"], FileArg, "Change working directory"),

55− ([":module"], ModuleArg, "Import an extra module"), -- NOTE: dragons

56− ([":e",":edit"], NoArg, "Edit current file using $EDITOR or $VISUAL"),

57− ([":m",":metavars"], NoArg, "Show remaining proof obligations (metavariables)"),

58− ([":p",":prove"], MetaVarArg, "Prove a metavariable"),

59− ([":a",":addproof"], NameArg, "Add proof to source file"),

60− ([":rmproof"], NameArg, "Remove proof from proof stack"),

61− ([":showproof"], NameArg, "Show proof"),

62− ([":proofs"], NoArg, "Show available proofs"),

63− ([":x"], ExprArg, "Execute IO actions resulting from an expression using the interpreter"),

64− ([":c",":compile"], FileArg, "Compile to an executable [codegen] <filename>"),

65− ([":exec",":execute"], NoArg, "Compile to an executable and run"),

66− ([":dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)"),

67− ([":dynamic"], NoArg, "List dynamically loaded C libraries"),

68− ([":?",":h",":help"], NoArg, "Display this help text"),

69− ([":set"], OptionArg, "Set an option (errorcontext, showimplicits)"),

70− ([":unset"], OptionArg, "Unset an option"),

71− ([":colour", ":color"], ColourArg, "Turn REPL colours on or off; set a specific colour"),

72− ([":consolewidth"], ConsoleWidthArg, "Set the width of the console"),

73− ([":q",":quit"], NoArg, "Exit the Idris system"),

74− ([":w", ":warranty"], NoArg, "Displays warranty information"),

75− ([":let"], ManyArgs DeclArg, "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"),

76− ([":undefine",":unlet"], ManyArgs NameArg, "Remove the listed repl definitions, or all repl definitions if no names given"),

77− ([":printdef"], NameArg, "Show the definition of a function"),

78− ([":pp", ":pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg)), "Pretty prints an Idris function in either LaTeX or HTML and for a specified width.")

79− ]

80−

81-- | Use these for completion, but don't show them in :help

40-- | Use these for completion, but don't show them in :help

82extraHelp ::[([String], CmdArg, String)]

41extraHelp ::[([String], CmdArg, String)]

83extraHelp =

42extraHelp =

84− [ ([":casesplit", ":cs"], NoArg, ":cs <line> <name> splits the pattern variable on the line")

85− , ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")

43+ [ ([":casesplit!", ":cs!"], NoArg, ":cs! <line> <name> destructively splits the pattern variable on the line")

86− , ([":addclause", ":ac"], NoArg, ":ac <line> <name> adds a clause for the definition of the name on the line")

87 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")

44 , ([":addclause!", ":ac!"], NoArg, ":ac! <line> <name> destructively adds a clause for the definition of the name on the line")

88− , ([":addmissing", ":am"], NoArg, ":am <line> <name> adds all missing pattern matches for the name on the line")

89 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")

45 , ([":addmissing!", ":am!"], NoArg, ":am! <line> <name> destructively adds all missing pattern matches for the name on the line")

90− , ([":makewith", ":mw"], NoArg, ":mw <line> <name> adds a with clause for the definition of the name on the line")

91 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

46 , ([":makewith!", ":mw!"], NoArg, ":mw! <line> <name> destructively adds a with clause for the definition of the name on the line")

92− , ([":proofsearch", ":ps"], NoArg, ":ps <line> <name> <names> does proof search for name on line, with names as hints")

93 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

47 , ([":proofsearch!", ":ps!"], NoArg, ":ps! <line> <name> <names> destructively does proof search for name on line, with names as hints")

94− , ([":addproofclause", ":apc"], NoArg, ":apc <line> <name> adds a pattern-matching proof clause to name on line")

95 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

48 , ([":addproofclause!", ":apc!"], NoArg, ":apc! <line> <name> destructively adds a pattern-matching proof clause to name on line")

96− , ([":refine", ":ref"], NoArg, ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

97 , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

49 , ([":refine!", ":ref!"], NoArg, ":ref! <line> <name> <name'> destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable")

98 ]

50 ]

src/Idris/ParseExpr.hs+116−117

@@ -1140,23 +1140,29 @@ Constant ::=

1140 ;

1141@

1142-}

1143+

1144+constants :: [(String, Idris.Core.TT.Const)]

1145+constants =

1146+ [ ("Integer", AType (ATInt ITBig))

1147+ , ("Int", AType (ATInt ITNative))

1148+ , ("Char", AType (ATInt ITChar))

1149+ , ("Float", AType ATFloat)

1150+ , ("String", StrType)

1151+ , ("Ptr", PtrType)

1152+ , ("ManagedPtr", ManagedPtrType)

1153+ , ("prim__UnsafeBuffer", BufferType)

1154+ , ("Bits8", AType (ATInt (ITFixed IT8)))

1155+ , ("Bits16", AType (ATInt (ITFixed IT16)))

1156+ , ("Bits32", AType (ATInt (ITFixed IT32)))

1157+ , ("Bits64", AType (ATInt (ITFixed IT64)))

1158+ , ("Bits8x16", AType (ATInt (ITVec IT8 16)))

1159+ , ("Bits16x8", AType (ATInt (ITVec IT16 8)))

1160+ , ("Bits32x4", AType (ATInt (ITVec IT32 4)))

1161+ , ("Bits64x2", AType (ATInt (ITVec IT64 2)))

1162+ ]

1163+

1143constant :: IdrisParser Idris.Core.TT.Const

1164constant :: IdrisParser Idris.Core.TT.Const

1144−constant = do reserved "Integer"; return (AType (ATInt ITBig))

1165+constant = choice [ do reserved name; return ty | (name, ty) <- constants ]

1145− <|> do reserved "Int"; return (AType (ATInt ITNative))

1146− <|> do reserved "Char"; return (AType (ATInt ITChar))

1147− <|> do reserved "Float"; return (AType ATFloat)

1148− <|> do reserved "String"; return StrType

1149− <|> do reserved "Ptr"; return PtrType

1150− <|> do reserved "ManagedPtr"; return ManagedPtrType

1151− <|> do reserved "prim__UnsafeBuffer"; return BufferType

1152− <|> do reserved "Bits8"; return (AType (ATInt (ITFixed IT8)))

1153− <|> do reserved "Bits16"; return (AType (ATInt (ITFixed IT16)))

1154− <|> do reserved "Bits32"; return (AType (ATInt (ITFixed IT32)))

1155− <|> do reserved "Bits64"; return (AType (ATInt (ITFixed IT64)))

1156− <|> do reserved "Bits8x16"; return (AType (ATInt (ITVec IT8 16)))

1157− <|> do reserved "Bits16x8"; return (AType (ATInt (ITVec IT16 8)))

1158− <|> do reserved "Bits32x4"; return (AType (ATInt (ITVec IT32 4)))

1159− <|> do reserved "Bits64x2"; return (AType (ATInt (ITVec IT64 2)))

1160 <|> do f <- try float; return $ Fl f

1166 <|> do f <- try float; return $ Fl f

1161 <|> do i <- natural; return $ BI i

1167 <|> do i <- natural; return $ BI i

1162 <|> do s <- verbatimStringLiteral; return $ Str s

1168 <|> do s <- verbatimStringLiteral; return $ Str s

@@ -1229,116 +1235,109 @@ TacticSeq ::=

1229@

1235@

1230-}

1236-}

1231

1237

1238+-- | A specification of the arguments that tactics can take

1239+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

1240+ | ExprTArg

1241+ | AltsTArg

1242+ | StringLitTArg

1243+

1244+-- The FIXMEs are Issue #1766 in the issue tracker.

1245+-- https://github.com/idris-lang/Idris-dev/issues/1766

1246+-- | A list of available tactics and their argument requirements

1247+tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1248+tactics =

1249+ [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1250+ do ns <- sepBy (spaced name) (lchar ','); return $ Intro ns)

1251+ , noArgs ["intros"] Intros

1252+ , (["refine"], Just ExprTArg, const $

1253+ do n <- spaced fnName

1254+ imps <- many imp

1255+ return $ Refine n imps)

1256+ , (["mrefine"], Just ExprTArg, const $

1257+ do n <- spaced fnName

1258+ return $ MatchRefine n)

1259+ , expressionTactic ["rewrite"] Rewrite

1260+ , expressionTactic ["case"] CaseTac

1261+ , expressionTactic ["induction"] Induction

1262+ , expressionTactic ["equiv"] Equiv

1263+ , (["let"], Nothing, \syn -> -- FIXME syntax for let

1264+ do n <- (indentPropHolds gtProp *> name)

1265+ (do indentPropHolds gtProp *> lchar ':'

1266+ ty <- indentPropHolds gtProp *> expr' syn

1267+ indentPropHolds gtProp *> lchar '='

1268+ t <- indentPropHolds gtProp *> expr syn

1269+ i <- get

1270+ return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1271+ <|> (do indentPropHolds gtProp *> lchar '='

1272+ t <- indentPropHolds gtProp *> expr syn

1273+ i <- get

1274+ return $ LetTac n (desugar syn i t)))

1275+

1276+ , (["focus"], Just ExprTArg, const $

1277+ do n <- spaced name

1278+ return $ Focus n)

1279+ , expressionTactic ["exact"] Exact

1280+ , expressionTactic ["applyTactic"] ApplyTactic

1281+ , expressionTactic ["byReflection"] ByReflection

1282+ , expressionTactic ["reflect"] Reflect

1283+ , expressionTactic ["fill"] Fill

1284+ , (["try"], Just AltsTArg, \syn ->

1285+ do t <- spaced (tactic syn)

1286+ lchar '|'

1287+ t1 <- spaced (tactic syn)

1288+ return $ Try t t1)

1289+ , noArgs ["compute"] Compute

1290+ , noArgs ["trivial"] Trivial

1291+ , noArgs ["unify"] DoUnify

1292+ , (["search"], Nothing, const $

1293+ do depth <- option 10 natural

1294+ return (ProofSearch True True (fromInteger depth) Nothing []))

1295+ , noArgs ["instance"] TCInstance

1296+ , noArgs ["solve"] Solve

1297+ , noArgs ["attack"] Attack

1298+ , noArgs ["state"] ProofState

1299+ , noArgs ["term"] ProofTerm

1300+ , noArgs ["undo"] Undo

1301+ , noArgs ["qed"] Qed

1302+ , noArgs ["abandon", ":q"] Abandon

1303+ , noArgs ["skip"] Skip

1304+ , noArgs ["sourceLocation"] SourceFC

1305+ , expressionTactic [":e", ":eval"] TEval

1306+ , expressionTactic [":t", ":type"] TCheck

1307+ , expressionTactic [":search"] TSearch

1308+ , (["fail"], Just StringLitTArg, const $

1309+ do msg <- stringLiteral

1310+ return $ TFail [Idris.Core.TT.TextPart msg])

1311+ , ([":doc"], Just ExprTArg, const $

1312+ do whiteSpace

1313+ doc <- (Right <$> constant) <|> (Left <$> fnName)

1314+ eof

1315+ return (TDocStr doc))

1316+ ]

1317+ where

1318+ expressionTactic names tactic = (names, Just ExprTArg, \syn ->

1319+ do t <- spaced (expr syn)

1320+ i <- get

1321+ return $ tactic (desugar syn i t))

1322+ noArgs names tactic = (names, Nothing, const (return tactic))

1323+ spaced parser = indentPropHolds gtProp *> parser

1324+ imp :: IdrisParser Bool

1325+ imp = do lchar '?'; return False

1326+ <|> do lchar '_'; return True

1327+

1328+

1232tactic :: SyntaxInfo -> IdrisParser PTactic

1329tactic :: SyntaxInfo -> IdrisParser PTactic

1233−tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (lchar ',')

1330+tactic syn = choice [ do choice (map reserved names); parser syn

1234− return $ Intro ns

1331+ | (names, _, parser) <- tactics ]

1235− <|> do reserved "intros"; return Intros

1236− <|> try (do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)

1237− imps <- some imp

1238− return $ Refine n imps)

1239− <|> do reserved "refine"; n <- (indentPropHolds gtProp *> fnName)

1240− i <- get

1241− return $ Refine n []

1242− <|> do reserved "mrefine"; n <- (indentPropHolds gtProp *> fnName)

1243− i <- get

1244− return $ MatchRefine n

1245− <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);

1246− i <- get

1247− return $ Rewrite (desugar syn i t)

1248− <|> do reserved "case"; t <- (indentPropHolds gtProp *> expr syn);

1249− i <- get

1250− return $ CaseTac (desugar syn i t)

1251− <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);

1252− i <- get

1253− return $ Induction (desugar syn i t)

1254− <|> do reserved "equiv"; t <- (indentPropHolds gtProp *> expr syn);

1255− i <- get

1256− return $ Equiv (desugar syn i t)

1257− <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar ':');

1258− ty <- (indentPropHolds gtProp *> expr' syn); (indentPropHolds gtProp *> lchar '='); t <- (indentPropHolds gtProp *> expr syn);

1259− i <- get

1260− return $ LetTacTy n (desugar syn i ty) (desugar syn i t))

1261− <|> try (do reserved "let"; n <- (indentPropHolds gtProp *> name); (indentPropHolds gtProp *> lchar '=');

1262− t <- (indentPropHolds gtProp *> expr syn);

1263− i <- get

1264− return $ LetTac n (desugar syn i t))

1265− <|> do reserved "focus"; n <- (indentPropHolds gtProp *> name)

1266− return $ Focus n

1267− <|> do reserved "exact"; t <- (indentPropHolds gtProp *> expr syn);

1268− i <- get

1269− return $ Exact (desugar syn i t)

1270− <|> do reserved "applyTactic"; t <- (indentPropHolds gtProp *> expr syn);

1271− i <- get

1272− return $ ApplyTactic (desugar syn i t)

1273− <|> do reserved "byReflection"; t <- (indentPropHolds gtProp *> expr syn);

1274− i <- get

1275− return $ ByReflection (desugar syn i t)

1276− <|> do reserved "reflect"; t <- (indentPropHolds gtProp *> expr syn);

1277− i <- get

1278− return $ Reflect (desugar syn i t)

1279− <|> do reserved "fill"; t <- (indentPropHolds gtProp *> expr syn);

1280− i <- get

1281− return $ Fill (desugar syn i t)

1282− <|> do reserved "try"; t <- (indentPropHolds gtProp *> tactic syn);

1283− lchar '|';

1284− t1 <- (indentPropHolds gtProp *> tactic syn)

1285− return $ Try t t1

1286 <|> do lchar '{'

1332 <|> do lchar '{'

1287 t <- tactic syn;

1333 t <- tactic syn;

1288 lchar ';';

1334 lchar ';';

1289 ts <- sepBy1 (tactic syn) (lchar ';')

1335 ts <- sepBy1 (tactic syn) (lchar ';')

1290 lchar '}'

1336 lchar '}'

1291 return $ TSeq t (mergeSeq ts)

1337 return $ TSeq t (mergeSeq ts)

1292− <|> do reserved "compute"; return Compute

1293− <|> do reserved "trivial"; return Trivial

1294− <|> do reserved "unify"; return DoUnify

1295− <|> do reserved "search"

1296− depth <- option 10 natural

1297− return (ProofSearch True True (fromInteger depth) Nothing [])

1298− <|> do reserved "instance"; return TCInstance

1299− <|> do reserved "solve"; return Solve

1300− <|> do reserved "attack"; return Attack

1301− <|> do reserved "state"; return ProofState

1302− <|> do reserved "term"; return ProofTerm

1303− <|> do reserved "undo"; return Undo

1304− <|> do reserved "qed"; return Qed

1305− <|> do reserved "abandon"; return Abandon

1306− <|> do reserved "skip"; return Skip

1307− <|> do reserved "fail"

1308− msg <- stringLiteral

1309− return $ TFail [Idris.Core.TT.TextPart msg]

1310− <|> do reserved "sourceLocation"; return SourceFC

1311− <|> do lchar ':';

1312− ( (do reserved "q"; return Abandon)

1313− <|> (do (reserved "e" <|> reserved "eval");

1314− t <- (indentPropHolds gtProp *> expr syn);

1315− i <- get

1316− return $ TEval (desugar syn i t))

1317− <|> (do (reserved "t" <|> reserved "type");

1318− t <- (indentPropHolds gtProp *> expr syn);

1319− i <- get

1320− return $ TCheck (desugar syn i t))

1321− <|> try (do reserved "doc"

1322− whiteSpace

1323− c <- constant

1324− eof

1325− return (TDocStr (Right c)))

1326− <|> try (do reserved "doc"

1327− whiteSpace

1328− n <- fnName

1329− eof

1330− return (TDocStr (Left n)))

1331− <|> try (do reserved "search"

1332− whiteSpace

1333− t <- (indentPropHolds gtProp *> expr syn);

1334− i <- get

1335− return $ TSearch (desugar syn i t))

1336− <?> "prover command")

1338+ <|> ((lchar ':' >> empty) <?> "prover command")

1337 <?> "tactic"

1339 <?> "tactic"

1338 where

1340 where

1339− imp :: IdrisParser Bool

1340− imp = do lchar '?'; return False

1341− <|> do lchar '_'; return True

1342 mergeSeq :: [PTactic] -> PTactic

1341 mergeSeq :: [PTactic] -> PTactic

1343 mergeSeq [t] = t

1342 mergeSeq [t] = t

1344 mergeSeq (t:ts) = TSeq t (mergeSeq ts)

1343 mergeSeq (t:ts) = TSeq t (mergeSeq ts)

src/Idris/ParseHelpers.hs+1−1

@@ -488,7 +488,7 @@ notEndBlock = do ist <- get

488data IndentProperty = IndentProperty (Int -> Int -> Bool) String

489

490-- | Allows comparison of indent, and fails if property doesn't hold

491−indentPropHolds :: IndentProperty -> IdrisParser()

491+indentPropHolds :: IndentProperty -> IdrisParser ()

492indentPropHolds (IndentProperty op msg) = do

493 li <- lastIndent

494 i <- indent

src/Idris/Parser.hs+3−3

@@ -1197,13 +1197,13 @@ parseProg syn fname input mrk

1197 return (ds, i')

1198

1199{- | Load idris module and show error if something wrong happens -}

1200−loadModule :: FilePath -> Idris String

1200+loadModule :: FilePath -> Idris (Maybe String)

1201loadModule f

1202− = idrisCatch (loadModule' f)

1202+ = idrisCatch (fmap Just (loadModule' f))

1203 (\e -> do setErrSpan (getErrSpan e)

1204 ist <- getIState

1205 iWarn (getErrSpan e) $ pprintErr ist e

1206− return "")

1206+ return Nothing)

1207

1208{- | Load idris module -}

1209loadModule' :: FilePath -> Idris String

src/Idris/REPL.hs+2−2

@@ -14,13 +14,13 @@ import Idris.Error

14import Idris.ErrReverse

15import Idris.Delaborate

16import Idris.Docstrings (Docstring, overview, renderDocstring)

17+import Idris.Help

17import Idris.IdrisDoc

18import Idris.IdrisDoc

18import Idris.Prover

19import Idris.Prover

19import Idris.Parser hiding (indent)

20import Idris.Parser hiding (indent)

20import Idris.Primitives

21import Idris.Primitives

21import Idris.Coverage

22import Idris.Coverage

22import Idris.Docs hiding (Doc)

23import Idris.Docs hiding (Doc)

23−import Idris.Help

24import Idris.Completion

25import qualified Idris.IdeSlave as IdeSlave

26import Idris.Chaser

@@ -637,7 +637,7 @@ processInput cmd orig inputs efile

637 Success (Right (ModImport f)) ->

638 do clearErr

639 fmod <- loadModule f

640− return (Just (inputs ++ [fmod]))

640+ return (Just (inputs ++ maybe [] (:[]) fmod))

641 Success (Right Edit) -> do -- takeMVar stvar

642 edit efile orig

643 return (Just inputs)

src/Idris/REPLParser.hs+180−153

@@ -1,5 +1,5 @@

2−module Idris.REPLParser(parseCmd) where

2+module Idris.REPLParser (parseCmd, help, allHelp) where

4import System.FilePath ((</>))

5import System.Console.ANSI (Color(..))

@@ -7,6 +7,7 @@ import System.Console.ANSI (Color(..))

7import Idris.Colours

8import Idris.AbsSyntax

9import Idris.Core.TT

10+import Idris.Help

10import qualified Idris.Parser as P

11import qualified Idris.Parser as P

12import Control.Applicative

13import Control.Applicative

@@ -26,82 +27,135 @@ import qualified Data.ByteString.UTF8 as UTF8

26parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd :: IState -> String -> String -> Result (Either String Command)

27parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace

28parseCmd i inputname = P.runparser pCmd i inputname . dropWhile isSpace

30+type CommandTable = [ ( [String], CmdArg, String

31+ , String -> P.IdrisParser (Either String Command) ) ]

32+

33+help :: [([String], CmdArg, String)]

34+help = (["<expr>"], NoArg, "Evaluate an expression") :

35+ [ (map (':' :) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]

36+

37+allHelp :: [([String], CmdArg, String)]

38+allHelp = [ (map (':' :) names, args, text)

39+ | (names, args, text, _) <- parserCommandsForHelp ++ parserCommands ]

40+

41+parserCommandsForHelp :: CommandTable

42+parserCommandsForHelp =

43+ [ exprArgCmd ["t", "type"] Check "Check the type of an expression"

44+ , nameArgCmd ["miss", "missing"] Missing "Show missing clauses"

45+ , (["doc"], NameArg, "Show internal documentation", cmd_doc)

46+ , (["mkdoc"], NamespaceArg, "Generate IdrisDoc for namespace(s) and dependencies"

47+ , genArg "namespace" (many anyChar) MakeDoc)

48+ , (["apropos"], SeqArgs (OptionalArg PkgArgs) NameArg, " Search names, types, and documentation"

49+ , cmd_apropos)

50+ , (["s", "search"], SeqArgs (OptionalArg PkgArgs) ExprArg

51+ , " Search for values by type", cmd_search)

52+ , nameArgCmd ["wc", "whocalls"] WhoCalls "List the callers of some name"

53+ , nameArgCmd ["cw", "callswho"] CallsWho "List the callees of some name"

54+ , nameArgCmd ["total"] TotCheck "Check the totality of a name"

55+ , noArgCmd ["r", "reload"] Reload "Reload current file"

56+ , (["l", "load"], FileArg, "Load a new file"

57+ , strArg (\f -> Load f Nothing))

58+ , (["cd"], FileArg, "Change working directory"

59+ , strArg ChangeDirectory)

60+ , (["module"], ModuleArg, "Import an extra module", moduleArg ModImport) -- NOTE: dragons

61+ , noArgCmd ["e", "edit"] Edit "Edit current file using $EDITOR or $VISUAL"

62+ , noArgCmd ["m", "metavars"] Metavars "Show remaining proof obligations (metavariables)"

63+ , (["p", "prove"], MetaVarArg, "Prove a metavariable"

64+ , nameArg Prove)

65+ , (["a", "addproof"], NameArg, "Add proof to source file", cmd_addproof)

66+ , (["rmproof"], NameArg, "Remove proof from proof stack"

67+ , nameArg RmProof)

68+ , (["showproof"], NameArg, "Show proof"

69+ , nameArg ShowProof)

70+ , noArgCmd ["proofs"] Proofs "Show available proofs"

71+ , exprArgCmd ["x"] ExecVal "Execute IO actions resulting from an expression using the interpreter"

72+ , (["c", "compile"], FileArg, "Compile to an executable [codegen] <filename>", cmd_compile)

73+ , noArgCmd ["exec", "execute"] Execute "Compile to an executable and run"

74+ , (["dynamic"], FileArg, "Dynamically load a C library (similar to %dynamic)", cmd_dynamic)

75+ , (["dynamic"], NoArg, "List dynamically loaded C libraries", cmd_dynamic)

76+ , noArgCmd ["?", "h", "help"] Help "Display this help text"

77+ , optArgCmd ["set"] SetOpt "Set an option (errorcontext, showimplicits)"

78+ , optArgCmd ["unset"] UnsetOpt "Unset an option"

79+ , (["color", "colour"], ColourArg

80+ , "Turn REPL colours on or off; set a specific colour"

81+ , cmd_colour)

82+ , (["consolewidth"], ConsoleWidthArg, "Set the width of the console", cmd_consolewidth)

83+ , noArgCmd ["q", "quit"] Quit "Exit the Idris system"

84+ , noArgCmd ["w", "warranty"] Warranty "Displays warranty information"

85+ , (["let"], ManyArgs DeclArg

86+ , "Evaluate a declaration, such as a function definition, instance implementation, or fixity declaration"

87+ , cmd_let)

88+ , (["unlet", "undefine"], ManyArgs NameArg

89+ , "Remove the listed repl definitions, or all repl definitions if no names given"

90+ , cmd_unlet)

91+ , nameArgCmd ["printdef"] PrintDef "Show the definition of a function"

92+ , (["pp", "pprint"], (SeqArgs OptionArg (SeqArgs NumberArg NameArg))

93+ , "Pretty prints an Idris function in either LaTeX or HTML and for a specified width."

94+ , cmd_pprint)

95+ ]

96+

97+parserCommands =

98+ [ noArgCmd ["u", "universes"] Universes "Display universe constraints"

99+ , noArgCmd ["errorhandlers"] ListErrorHandlers "List registered error handlers"

100+

101+ , nameArgCmd ["d", "def"] Defn "Display a name's internal definitions"

102+ , nameArgCmd ["transinfo"] TransformInfo "Show relevant transformation rules for a name"

103+ , nameArgCmd ["di", "dbginfo"] DebugInfo "Show debugging information for a name"

104+

105+ , exprArgCmd ["patt"] Pattelab "(Debugging) Elaborate pattern expression"

106+ , exprArgCmd ["spec"] Spec "?"

107+ , exprArgCmd ["hnf"] HNF "?"

108+ , exprArgCmd ["inline"] TestInline "?"

109+ , proofArgCmd ["cs", "casesplit"] CaseSplitAt

110+ ":cs <line> <name> splits the pattern variable on the line"

111+ , proofArgCmd ["apc", "addproofclause"] AddProofClauseFrom

112+ ":apc <line> <name> adds a pattern-matching proof clause to name on line"

113+ , proofArgCmd ["ac", "addclause"] AddClauseFrom

114+ ":ac <line> <name> adds a clause for the definition of the name on the line"

115+ , proofArgCmd ["am", "addmissing"] AddMissing

116+ ":am <line> <name> adds all missing pattern matches for the name on the line"

117+ , proofArgCmd ["mw", "makewith"] MakeWith

118+ ":mw <line> <name> adds a with clause for the definition of the name on the line"

119+ , proofArgCmd ["ml", "makelemma"] MakeLemma "?"

120+ , (["log"], NumberArg, "Set logging verbosity level", cmd_log)

121+ , (["lto", "loadto"], SeqArgs NumberArg FileArg

122+ , "Load file up to line number", cmd_loadto)

123+ , (["ps", "proofsearch"], NoArg

124+ , ":ps <line> <name> <names> does proof search for name on line, with names as hints"

125+ , cmd_proofsearch)

126+ , (["ref", "refine"], NoArg

127+ , ":ref <line> <name> <name'> attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable"

128+ , cmd_refine)

129+ , (["debugunify"], SeqArgs ExprArg ExprArg

130+ , "(Debugging) Try to unify two expressions", const $ do

131+ l <- P.simpleExpr defaultSyntax

132+ r <- P.simpleExpr defaultSyntax

133+ eof

134+ return (Right (DebugUnify l r))

135+ )

136+ ]

137+

138+noArgCmd names command doc =

139+ (names, NoArg, doc, noArgs command)

140+nameArgCmd names command doc =

141+ (names, NameArg, doc, fnNameArg command)

142+exprArgCmd names command doc =

143+ (names, ExprArg, doc, exprArg command)

144+metavarArgCmd names command doc =

145+ (names, MetaVarArg, doc, fnNameArg command)

146+optArgCmd names command doc =

147+ (names, OptionArg, doc, optArg command)

148+proofArgCmd names command doc =

149+ (names, NoArg, doc, proofArg command)

150+

29pCmd :: P.IdrisParser (Either String Command)

151pCmd :: P.IdrisParser (Either String Command)

30−pCmd = choice [ do c <- cmd ["q", "quit"]; noArgs c Quit

152+pCmd = choice [ do c <- cmd names; parser c

31− , do c <- cmd ["h", "?", "help"]; noArgs c Help

153+ | (names, _, _, parser) <- parserCommandsForHelp ++ parserCommands ]

32− , do c <- cmd ["w", "warranty"]; noArgs c Warranty

33− , do c <- cmd ["r", "reload"]; noArgs c Reload

34− , do c <- cmd ["exec", "execute"]; noArgs c Execute

35− , do c <- cmd ["proofs"]; noArgs c Proofs

36− , do c <- cmd ["u", "universes"]; noArgs c Universes

37− , do c <- cmd ["errorhandlers"]; noArgs c ListErrorHandlers

38− , do c <- cmd ["m", "metavars"]; noArgs c Metavars

39− , do c <- cmd ["e", "edit"]; noArgs c Edit

40−

41− , do c <- cmd ["d", "def"]; fnNameArg c Defn

42− , do c <- cmd ["total"]; fnNameArg c TotCheck

43− , do c <- cmd ["printdef"]; fnNameArg c PrintDef

44− , do c <- cmd ["transinfo"]; fnNameArg c TransformInfo

45− , do c <- cmd ["wc", "whocalls"]; fnNameArg c WhoCalls

46− , do c <- cmd ["cw", "callswho"]; fnNameArg c CallsWho

47− , do c <- cmd ["di", "dbginfo"]; fnNameArg c DebugInfo

48− , do c <- cmd ["miss", "missing"]; fnNameArg c Missing

49−

50− , do c <- cmd ["t", "type"]; exprArg c Check

51− , do c <- cmd ["x"]; exprArg c ExecVal

52− , do c <- cmd ["patt"]; exprArg c Pattelab

53− , do c <- cmd ["spec"]; exprArg c Spec

54− , do c <- cmd ["hnf"]; exprArg c HNF

55− , do c <- cmd ["inline"]; exprArg c TestInline

56−

57− , do c <- cmd ["rmproof"]; nameArg c RmProof

58− , do c <- cmd ["showproof"]; nameArg c ShowProof

59− , do c <- cmd ["p", "prove"]; nameArg c Prove

60−

61− , do c <- cmd ["set"]; optArg c SetOpt

62− , do c <- cmd ["unset"]; optArg c UnsetOpt

63−

64− , do c <- cmd ["l", "load"]; strArg c (\f -> Load f Nothing)

65− , do c <- cmd ["cd"]; strArg c ChangeDirectory

66− , do c <- cmd ["apropos"]; cmd_apropos c

67− , do c <- cmd ["mkdoc"]; strArg c MakeDoc

68−

69− , do c <- cmd ["cs", "casesplit"]; proofArg c CaseSplitAt

70− , do c <- cmd ["apc", "addproofclause"]; proofArg c AddProofClauseFrom

71− , do c <- cmd ["ac", "addclause"]; proofArg c AddClauseFrom

72− , do c <- cmd ["am", "addmissing"]; proofArg c AddMissing

73− , do c <- cmd ["mw", "makewith"]; proofArg c MakeWith

74− , do c <- cmd ["ml", "makelemma"]; proofArg c MakeLemma

75−

76− , do c <- cmd ["pp", "pprint"]; cmd_pprint c

77− , do c <- cmd ["doc"]; cmd_doc c

78− , do c <- cmd ["dynamic"]; cmd_dynamic c

79− , do c <- cmd ["consolewidth"]; cmd_consolewidth c

80− , do c <- cmd ["module"]; cmd_module c

81− , do c <- cmd ["c", "compile"]; cmd_compile c

82− , do c <- cmd ["a", "addproof"]; cmd_addproof c

83− , do c <- cmd ["log"]; cmd_log c

84− , do c <- cmd ["let"]; cmd_let c

85− , do c <- cmd ["unlet","undefine"]; cmd_unlet c

86− , do c <- cmd ["lto", "loadto"]; cmd_loadto c

87− , do c <- cmd ["color", "colour"]; cmd_colour c

88− , do c <- cmd ["s", "search"]; cmd_search c

89− , do c <- cmd ["ps", "proofsearch"]; cmd_proofsearch c

90− , do c <- cmd ["ref", "refine"]; cmd_refine c

91−

92− , do c <- cmd ["debugunify"];

93− P.whiteSpace

94− l <- P.simpleExpr defaultSyntax

95− r <- P.simpleExpr defaultSyntax

96− eof

97− return (Right (DebugUnify l r))

98−

99− , unrecognized

154+ <|> unrecognized

100− , nop

155+ <|> nop

101− ]

102− <|> eval

156+ <|> eval

103− where nop = do P.whiteSpace; eof; return (Right NOP)

157+ where nop = do eof; return (Right NOP)

104− eval = exprArg "" Eval

158+ eval = exprArg Eval ""

105 unrecognized = do

159 unrecognized = do

106 P.lchar ':'

160 P.lchar ':'

107 cmd <- many anyChar

161 cmd <- many anyChar

@@ -119,20 +173,18 @@ cmd xs = try $ do

119 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

173 sorted_xs = sortBy (\x y -> compare (length y) (length x)) xs

120

174

121

175

122−noArgs :: String -> Command -> P.IdrisParser (Either String Command)

176+noArgs :: Command -> String -> P.IdrisParser (Either String Command)

123−noArgs name cmd = do

177+noArgs cmd name = do

124 let emptyArgs = do

178 let emptyArgs = do

125− P.whiteSpace

126 eof

179 eof

127 return (Right cmd)

180 return (Right cmd)

128

181

129 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

182 let failure = return (Left $ ":" ++ name ++ " takes no arguments")

130

183

131− try emptyArgs <|> failure

184+ emptyArgs <|> failure

132

185

133−exprArg :: String -> (PTerm -> Command) -> P.IdrisParser (Either String Command)

186+exprArg :: (PTerm -> Command) -> String -> P.IdrisParser (Either String Command)

134−exprArg name cmd = do

187+exprArg cmd name = do

135− P.whiteSpace

136 let noArg = do

188 let noArg = do

137 eof

189 eof

138 return $ Left ("Usage is :" ++ name ++ " <expression>")

190 return $ Left ("Usage is :" ++ name ++ " <expression>")

@@ -143,51 +195,45 @@ exprArg name cmd = do

143 try noArg <|> properArg

195 try noArg <|> properArg

144

196

145

197

198+

146−fnNameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)

199+genArg :: String -> P.IdrisParser a -> (a -> Command)

147−fnNameArg name cmd = do

148− P.whiteSpace

149− let emptyArgs = do eof

150− return $ Left ("Usage is :" ++ name ++ " <functionname>")

151− oneArg = do n <- P.fnName

152− eof

153− return (Right (cmd n))

154− badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")

155− try emptyArgs <|> try oneArg <|> badArg

156−

157−nameArg :: String -> (Name -> Command) -> P.IdrisParser (Either String Command)

200+ -> String -> P.IdrisParser (Either String Command)

158−nameArg name cmd = do

201+genArg argName argParser cmd name = do

159− P.whiteSpace

160− let emptyArgs = do eof

202+ let emptyArgs = do eof; failure

161− return $ Left ("Usage is :" ++ name ++ " <functionname>")

162− oneArg = do n <- P.name

203+ oneArg = do arg <- argParser

163 eof

204 eof

164− return (Right (cmd n))

205+ return (Right (cmd arg))

206+ try emptyArgs <|> oneArg <|> failure

207+ where

165− badArg = return $ Left ("Usage is :" ++ name ++ " <functionname>")

208+ failure = return $ Left ("Usage is :" ++ name ++ " <" ++ argName ++ ">")

166− try emptyArgs <|> try oneArg <|> badArg

167

209

168−strArg :: String -> (String -> Command) -> P.IdrisParser (Either String Command)

210+nameArg, fnNameArg :: (Name -> Command) -> String -> P.IdrisParser (Either String Command)

169−strArg name cmd = do

211+nameArg = genArg "name" P.name

170− n <- many anyChar

212+fnNameArg = genArg "functionname" P.fnName

171− eof

172− return (Right (cmd n))

173

213

214+strArg :: (String -> Command) -> String -> P.IdrisParser (Either String Command)

215+strArg = genArg "string" (many anyChar)

216+

217+moduleArg :: (FilePath -> Command) -> String -> P.IdrisParser (Either String Command)

218+moduleArg = genArg "module" (fmap toPath P.identifier)

219+ where

220+ toPath n = foldl1' (</>) $ splitOn "." n

221+

174−optArg :: String -> (Opt -> Command) -> P.IdrisParser (Either String Command)

222+optArg :: (Opt -> Command) -> String -> P.IdrisParser (Either String Command)

175−optArg name cmd = do

223+optArg cmd name = do

176 let emptyArgs = do

224 let emptyArgs = do

177 eof

225 eof

178 return $ Left ("Usage is :" ++ name ++ " <option>")

226 return $ Left ("Usage is :" ++ name ++ " <option>")

179

227

180 let oneArg = do

228 let oneArg = do

181− P.whiteSpace

182 o <- pOption

229 o <- pOption

183 P.whiteSpace

230 P.whiteSpace

184 eof

231 eof

185 return (Right (cmd o))

232 return (Right (cmd o))

186

233

187− let failure = do

188− return $ Left "Unrecognized setting"

234+ let failure = return $ Left "Unrecognized setting"

189

235

190− try emptyArgs <|> try oneArg <|> failure

236+ try emptyArgs <|> oneArg <|> failure

191

237

192 where

238 where

193 pOption :: P.IdrisParser Opt

239 pOption :: P.IdrisParser Opt

@@ -198,9 +244,8 @@ optArg name cmd = do

198 <|> do discard (P.symbol "nobanner") ; return NoBanner

244 <|> do discard (P.symbol "nobanner") ; return NoBanner

199 <|> do discard (P.symbol "warnreach"); return WarnReach

245 <|> do discard (P.symbol "warnreach"); return WarnReach

200

246

201−proofArg :: String -> (Bool -> Int -> Name -> Command) -> P.IdrisParser (Either String Command)

247+proofArg :: (Bool -> Int -> Name -> Command) -> String -> P.IdrisParser (Either String Command)

202−proofArg name cmd = do

248+proofArg cmd name = do

203− P.whiteSpace

204 upd <- option False $ do

249 upd <- option False $ do

205 P.lchar '!'

250 P.lchar '!'

206 return True

251 return True

@@ -215,7 +260,7 @@ cmd_doc name = do

215 eof

260 eof

216 return $ Right (DocStr (Right c))

261 return $ Right (DocStr (Right c))

217

262

218− let fnName = fnNameArg name (\n -> DocStr (Left n))

263+ let fnName = fnNameArg (\n -> DocStr (Left n)) name

219

264

220 try constant <|> fnName

265 try constant <|> fnName

221

266

@@ -232,7 +277,7 @@ cmd_consolewidth name = do

232

277

233cmd_dynamic :: String -> P.IdrisParser (Either String Command)

278cmd_dynamic :: String -> P.IdrisParser (Either String Command)

234cmd_dynamic name = do

279cmd_dynamic name = do

235− let emptyArgs = noArgs name ListDynamic

280+ let emptyArgs = noArgs ListDynamic name

236

281

237 let oneArg = do l <- many anyChar

282 let oneArg = do l <- many anyChar

238 return $ Right (DynamicLink l)

283 return $ Right (DynamicLink l)

@@ -243,7 +288,6 @@ cmd_dynamic name = do

243

288

244cmd_pprint :: String -> P.IdrisParser (Either String Command)

289cmd_pprint :: String -> P.IdrisParser (Either String Command)

245cmd_pprint name = do

290cmd_pprint name = do

246− P.whiteSpace

247 fmt <- ppFormat

291 fmt <- ppFormat

248 P.whiteSpace

292 P.whiteSpace

249 n <- fmap fromInteger P.natural

293 n <- fmap fromInteger P.natural

@@ -257,13 +301,6 @@ cmd_pprint name = do

257 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

301 <|> (discard (P.symbol "latex") >> return LaTeXOutput)

258

302

259

303

260−cmd_module :: String -> P.IdrisParser (Either String Command)

261−cmd_module name = do

262− f <- P.identifier

263− eof;

264− return (Right (ModImport (toPath f)))

265− where

266− toPath n = foldl1' (</>) $ splitOn "." n

267

304

268cmd_compile :: String -> P.IdrisParser (Either String Command)

305cmd_compile :: String -> P.IdrisParser (Either String Command)

269cmd_compile name = do

306cmd_compile name = do

@@ -312,8 +349,7 @@ cmd_let name = do

312 return (Right (NewDefn defn))

349 return (Right (NewDefn defn))

313

350

314cmd_unlet :: String -> P.IdrisParser (Either String Command)

351cmd_unlet :: String -> P.IdrisParser (Either String Command)

315−cmd_unlet name = do

316− (Right . Undefine) `fmap` many P.name

352+cmd_unlet name = (Right . Undefine) `fmap` many P.name

317

353

318cmd_loadto :: String -> P.IdrisParser (Either String Command)

354cmd_loadto :: String -> P.IdrisParser (Either String Command)

319cmd_loadto name = do

355cmd_loadto name = do

@@ -322,8 +358,7 @@ cmd_loadto name = do

322 return (Right (Load f (Just (fromInteger toline))))

358 return (Right (Load f (Just (fromInteger toline))))

323

359

324cmd_colour :: String -> P.IdrisParser (Either String Command)

360cmd_colour :: String -> P.IdrisParser (Either String Command)

325−cmd_colour name = do

361+cmd_colour name = fmap Right pSetColourCmd

326− pSetColourCmd >>= return . Right

327

362

328 where

363 where

329 colours :: [(String, Maybe Color)]

364 colours :: [(String, Maybe Color)]

@@ -386,32 +421,25 @@ cmd_colour name = do

386idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

421idChar = oneOf (['a'..'z'] ++ ['A'..'Z'] ++ ['0'..'9'] ++ ['_'])

387

422

388cmd_apropos :: String -> P.IdrisParser (Either String Command)

423cmd_apropos :: String -> P.IdrisParser (Either String Command)

389−cmd_apropos name =

424+cmd_apropos = packageBasedCmd (some idChar) Apropos

390− try (do P.whiteSpace

425+

426+packageBasedCmd :: P.IdrisParser a -> ([String] -> a -> Command)

427+ -> String -> P.IdrisParser (Either String Command)

428+packageBasedCmd valParser cmd name = do

429+ pkgs <- option [] . try $ do

391− P.lchar '('

430+ P.lchar '('

392− pkgs <- sepBy (some idChar) (P.lchar ',')

431+ pks <- sepBy (some idChar) (P.lchar ',')

393− P.lchar ')'

432+ P.lchar ')'

394− nm <- some idChar

433+ return pks

395− return (Right (Apropos pkgs nm)))

434+ val <- valParser

396− <|> do P.whiteSpace;

397− nm <- some idChar

398− return (Right (Apropos [] nm))

435+ return (Right (cmd pkgs val))

399

436

400cmd_search :: String -> P.IdrisParser (Either String Command)

437cmd_search :: String -> P.IdrisParser (Either String Command)

401−cmd_search name =

438+cmd_search = packageBasedCmd

402− try (do P.whiteSpace

403− P.lchar '('

404− pkgs <- sepBy (some idChar) (P.lchar ',')

405− P.lchar ')'

406− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

439+ (P.typeExpr (defaultSyntax { implicitAllowed = True })) Search

407− return (Right (Search pkgs t)))

408− <|> do P.whiteSpace;

409− t <- P.typeExpr (defaultSyntax { implicitAllowed = True })

410− return (Right (Search [] t))

411

440

412cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

441cmd_proofsearch :: String -> P.IdrisParser (Either String Command)

413cmd_proofsearch name = do

442cmd_proofsearch name = do

414− P.whiteSpace

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

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

416 l <- P.natural; n <- P.name;

444 l <- P.natural; n <- P.name;

417 hints <- many P.fnName

445 hints <- many P.fnName

@@ -419,7 +447,6 @@ cmd_proofsearch name = do

419

447

420cmd_refine :: String -> P.IdrisParser (Either String Command)

448cmd_refine :: String -> P.IdrisParser (Either String Command)

421cmd_refine name = do

449cmd_refine name = do

422− P.whiteSpace

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

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

424 l <- P.natural; n <- P.name;

451 l <- P.natural; n <- P.name;

425 hint <- P.fnName

452 hint <- P.fnName

src/Idris/TypeSearch.hs+22−16

@@ -39,17 +39,15 @@ import Util.Pretty (text, char, vsep, (<>), Doc, annotate)

40searchByType :: [String] -> PTerm -> Idris ()

41searchByType pkgs pterm = do

42− orig <- getIState -- save original

42+ i <- getIState -- save original

43 when (not (null pkgs)) $

44 iputStrLn $ "Searching packages: " ++ showSep ", " pkgs

46 mapM_ loadPkgIndex pkgs

47 pterm' <- addUsingConstraints syn emptyFC pterm

48 pterm'' <- implicit toplevel syn name pterm'

49− i <- getIState

50 let pterm''' = addImpl i pterm''

49 let pterm''' = addImpl i pterm''

51 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

50 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

52− putIState i -- don't actually make any changes

53 let names = searchUsing searchPred i ty

51 let names = searchUsing searchPred i ty

54 let names' = take numLimit names

52 let names' = take numLimit names

55 let docs =

53 let docs =

@@ -60,7 +58,7 @@ searchByType pkgs pterm = do

60 RawOutput _ -> do mapM_ iRenderOutput docs

58 RawOutput _ -> do mapM_ iRenderOutput docs

61 iPrintResult ""

59 iPrintResult ""

62 IdeSlave _ _ -> iRenderResult (vsep docs)

60 IdeSlave _ _ -> iRenderResult (vsep docs)

63− putIState orig

61+ putIState i -- don't actually make any changes

64 where

62 where

65 numLimit = 50

63 numLimit = 50

66 syn = defaultSyntax { implicitAllowed = True } -- syntax

64 syn = defaultSyntax { implicitAllowed = True } -- syntax

@@ -85,7 +83,7 @@ searchUsing pred istate ty = pred istate nty . concat . M.elems $

85 || n `elem` map T.pack ["believe_me", "really_believe_me"]

83 || n `elem` map T.pack ["believe_me", "really_believe_me"]

86 special _ = False

84 special _ = False

88−-- Our default search predicate.

86+-- | Our default search predicate.

89searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]

87searchPred :: IState -> Type -> [(Name, Type)] -> [(Name, Score)]

90searchPred istate ty1 = matcher where

88searchPred istate ty1 = matcher where

91 maxScore = 100

89 maxScore = 100

@@ -174,10 +172,12 @@ sided f (Sided l r) = f l r

174both :: (a -> b) -> Sided a -> Sided b

172both :: (a -> b) -> Sided a -> Sided b

175both f (Sided l r) = Sided (f l) (f r)

173both f (Sided l r) = Sided (f l) (f r)

176

174

175+-- | Keeps a record of the modifications made to match one type

176+-- signature with another

177data Score = Score

178− { transposition :: !Int

178+ { transposition :: !Int -- ^ transposition of arguments

179− , equalityFlips :: !Int

179+ , equalityFlips :: !Int -- ^ application of symmetry of equality

180− , asymMods :: !(Sided AsymMods)

180+ , asymMods :: !(Sided AsymMods) -- ^ "directional" modifications

181 } deriving (Eq, Show)

182

183displayScore :: Score -> Doc OutputAnnotation

@@ -190,6 +190,9 @@ displayScore score = case both noMods (asymMods score) of

190 annotated ordr = annotate (AnnSearchResult ordr) . text

191 noMods (Mods app tcApp tcIntro) = app + tcApp + tcIntro == 0

192

193+-- | This allows the search to stop expanding on a certain state if its

194+-- score is already too high. Returns 'True' if the algorithm should keep

195+-- exploring from this state, and 'False' otherwise.

193scoreCriterion :: Score -> Bool

196scoreCriterion :: Score -> Bool

194scoreCriterion (Score _ _ amods) = not

197scoreCriterion (Score _ _ amods) = not

195 ( sided (&&) (both ((> 0) . argApp) amods)

198 ( sided (&&) (both ((> 0) . argApp) amods)

@@ -197,6 +200,8 @@ scoreCriterion (Score _ _ amods) = not

197 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)

200 || sided (||) (both (\(Mods _ tcApp tcIntro) -> tcApp > 3 || tcIntro > 3) amods)

198 )

201 )

199

202

203+-- | Convert a 'Score' to an 'Int' to provide an order for search results.

204+-- Lower scores are better.

200defaultScoreFunction :: Score -> Int

205defaultScoreFunction :: Score -> Int

201defaultScoreFunction (Score trans eqFlip amods) =

206defaultScoreFunction (Score trans eqFlip amods) =

202 trans + eqFlip + linearPenalty + upAndDowncastPenalty

207 trans + eqFlip + linearPenalty + upAndDowncastPenalty

@@ -208,6 +213,10 @@ defaultScoreFunction (Score trans eqFlip amods) =

208 upAndDowncastPenalty = 100 *

213 upAndDowncastPenalty = 100 *

209 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)

214 sided (*) (both (\(Mods app tcApp tcIntro) -> 2 * app + tcApp + tcIntro) amods)

210

215

216+instance Ord Score where

217+ compare = comparing defaultScoreFunction

218+

219+

211instance Monoid a => Monoid (Sided a) where

220instance Monoid a => Monoid (Sided a) where

212 mempty = Sided mempty mempty

221 mempty = Sided mempty mempty

213 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)

222 (Sided l1 r1) `mappend` (Sided l2 r2) = Sided (l1 `mappend` l2) (r1 `mappend` r2)

@@ -278,9 +287,6 @@ isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt c

278 getClassName _ = []

287 getClassName _ = []

279

288

280

289

281−instance Ord Score where

282− compare = comparing defaultScoreFunction

283−

284-- | Compute the power set

290-- | Compute the power set

285subsets :: [a] -> [[a]]

291subsets :: [a] -> [[a]]

286subsets [] = [[]]

292subsets [] = [[]]

@@ -429,17 +435,17 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

429 getClassName (P (TCon _ _) className _) = [className]

435 getClassName (P (TCon _ _) className _) = [className]

430 getClassName _ = []

436 getClassName _ = []

431

437

432− -- Just if the computation hasn't totally failed yet, Nothing if it has

438+ -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has

433− -- Left if we haven't found a terminal state, Right if we have

439+ -- 'Left' if we haven't found a terminal state, 'Right' if we have

434 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)

440 nextStepsQueue :: Q.PQueue Score State -> Maybe (Either (Q.PQueue Score State) Score)

435 nextStepsQueue queue = do

441 nextStepsQueue queue = do

436 ((nextScore, next), rest) <- Q.minViewWithKey queue

442 ((nextScore, next), rest) <- Q.minViewWithKey queue

437− if isFinal next

443+ Just $ if isFinal next

438− then Just $ Right nextScore

444+ then Right nextScore

439 else let additions = if scoreCriterion nextScore

445 else let additions = if scoreCriterion nextScore

440 then Q.fromList [ (score state, state) | state <- nextSteps next ]

446 then Q.fromList [ (score state, state) | state <- nextSteps next ]

441 else Q.empty in

447 else Q.empty in

442− Just $ Left (Q.union rest additions)

448+ Left (Q.union rest additions)

443 where

449 where

444 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True

450 isFinal (State [] (Sided ([], []) ([], [])) _ _) = True

445 isFinal _ = False

451 isFinal _ = False