git.iko.soy/Idris-dev
on master help sign in
Complete tactic names in prover
52203a3David Christiansen
src/Idris/Completion.hs+46−10
compare with master
unifiedsplit
@@ -1,4 +1,4 @@
1−module Idris.Completion (replCompletion) where
1+module Idris.Completion (replCompletion, proverCompletion) where
2
2
3import Core.Evaluate (ctxtAlist)
3import Core.Evaluate (ctxtAlist)
4import Core.TT
4import Core.TT
@@ -46,6 +46,30 @@ cmdArgs = [ (":t", ExprArg)
46 ]
46 ]
47commands = map fst cmdArgs
47commands = map fst cmdArgs
48
48
49+-- | A specification of the arguments that tactics can take
50+data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
51+ | ExprTArg
52+ | TacticTArg
53+ | CommasTArg TacticArg
54+ | AltTArg TacticArg TacticArg
55+
56+-- | A list of available tactics and their argument requirements
57+tacticArgs :: [(String, Maybe TacticArg)]
58+tacticArgs = [ ("intro", Just $ CommasTArg NameTArg)
59+ , ("intros", Nothing)
60+ , ("refine", Just NameTArg)
61+ , ("rewrite", Just NameTArg)
62+ , ("let", Nothing) -- FIXME syntax for let
63+ , ("focus", Just NameTArg)
64+ , ("exact", Just ExprTArg)
65+ , ("reflect", Just ExprTArg)
66+ , ("try", Just $ AltTArg TacticTArg TacticTArg)
67+ ] ++ map (\x -> (x, Nothing)) [
68+ "compute", "trivial", "solve", "attack", "state",
69+ "term", "undo", "qed", "abandon", ":q"
70+ ]
71+tactics = map fst tacticArgs
72+
49-- | Convert a name into a string usable for completion. Filters out names
73-- | Convert a name into a string usable for completion. Filters out names
50-- that users probably don't want to see.
74-- that users probably don't want to see.
51nameString :: Name -> Maybe String
75nameString :: Name -> Maybe String
@@ -57,16 +81,18 @@ nameString _ = Nothing
57
81
58-- FIXME: Respect module imports
82-- FIXME: Respect module imports
59-- | Get the user-visible names from the current interpreter state.
83-- | Get the user-visible names from the current interpreter state.
60−names :: StateT IState IO [String]
84+names :: Idris[String]
61names = do i <- get
85names = do i <- get
62 let ctxt = tt_ctxt i
86 let ctxt = tt_ctxt i
63 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
87 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
64
88
65
89
66−modules :: StateT IState IO [String]
90+modules :: Idris [String]
67modules = do i <- get
91modules = do i <- get
68 return $ map show $ imported i
92 return $ map show $ imported i
69
93
94+
95+
70completeWith :: [String] -> String -> [Completion]
96completeWith :: [String] -> String -> [Completion]
71completeWith ns n = if uniqueExists
97completeWith ns n = if uniqueExists
72 then [simpleCompletion n]
98 then [simpleCompletion n]
@@ -74,14 +100,14 @@ completeWith ns n = if uniqueExists
74 where prefixMatches = filter (isPrefixOf n) ns
100 where prefixMatches = filter (isPrefixOf n) ns
75 uniqueExists = n `elem` prefixMatches
101 uniqueExists = n `elem` prefixMatches
76
102
77−completeName :: String -> StateT IState IO [Completion]
103+completeName :: String -> Idris [Completion]
78completeName n = do ns <- names
104completeName n = do ns <- names
79 return $ completeWith ns n
105 return $ completeWith ns n
80
106
81−completeExpr :: CompletionFunc (StateT IState IO)
107+completeExpr :: CompletionFunc Idris
82completeExpr = completeWord Nothing " \t" completeName
108completeExpr = completeWord Nothing " \t" completeName
83
109
84−completeOption :: CompletionFunc (StateT IState IO)
110+completeOption :: CompletionFunc Idris
85completeOption = completeWord Nothing " \t" completeOpt
111completeOption = completeWord Nothing " \t" completeOpt
86 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
112 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
87
113
@@ -89,8 +115,8 @@ isWhitespace :: Char -> Bool
89isWhitespace = (flip elem) " \t\n"
115isWhitespace = (flip elem) " \t\n"
90
116
91-- | Get the completion function for a particular command
117-- | Get the completion function for a particular command
92−completeCmd :: String -> CompletionFunc (StateT IState IO)
118+completeCmd :: String -> CompletionFunc Idris
93−completeCmd cmd (prev, next) = fromMaybe completeCmdName (fmap completeArg $ lookup cmd cmdArgs)
119+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
94 where completeArg FileArg = completeFilename (prev, next)
120 where completeArg FileArg = completeFilename (prev, next)
95 completeArg NameArg = completeExpr (prev, next) -- FIXME only complete one name
121 completeArg NameArg = completeExpr (prev, next) -- FIXME only complete one name
96 completeArg OptionArg = completeOption (prev, next)
122 completeArg OptionArg = completeOption (prev, next)
@@ -98,8 +124,18 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName (fmap completeArg $ loo
98 completeArg ExprArg = completeExpr (prev, next)
124 completeArg ExprArg = completeExpr (prev, next)
99 completeCmdName = return $ ("", completeWith commands cmd)
125 completeCmdName = return $ ("", completeWith commands cmd)
100
126
101−replCompletion :: CompletionFunc (StateT IState IO)
127+replCompletion :: CompletionFunc Idris
102replCompletion (prev, next) = case firstWord of
128replCompletion (prev, next) = case firstWord of
103 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
129 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
104 _ -> completeExpr (prev, next)
130 _ -> completeExpr (prev, next)
105− where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
131+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
132+
133+
134+completeTactic :: String -> CompletionFunc Idris
135+completeTactic tac (prev, next) = return $ completeTacName tac
136+ where completeTacName = return $ ("", completeWith tactics tac)
137+
138+
139+proverCompletion :: CompletionFunc Idris
140+proverCompletion (prev, next) = completeTactic firstWord (prev, next)
141+ where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
src/Idris/Prover.hs+3−1
@@ -13,6 +13,7 @@ import Idris.ElabTerm
13import Idris.Parser
13import Idris.Parser
14import Idris.Error
14import Idris.Error
15import Idris.DataOpts
15import Idris.DataOpts
16+import Idris.Completion
16
17
17import System.Console.Haskeline
18import System.Console.Haskeline
18import Control.Monad.State
19import Control.Monad.State
@@ -37,7 +38,8 @@ showProof lit n ps
37 where bird = if lit then "> " else ""
38 where bird = if lit then "> " else ""
38 break = "\n" ++ bird
39 break = "\n" ++ bird
39
40
40−proverSettings = defaultSettings -- TODO: Prover settings
41+proverSettings :: Settings Idris
42+proverSettings = setComplete proverCompletion defaultSettings
41
43
42prove :: Context -> Bool -> Name -> Type -> Idris ()
44prove :: Context -> Bool -> Name -> Type -> Idris ()
43prove ctxt lit n ty
45prove ctxt lit n ty
src/Idris/REPL.hs+1−1
@@ -491,7 +491,7 @@ help =
491 ]
491 ]
492
492
493
493
494−replSettings :: Settings (StateT IState IO)
494+replSettings :: Settings Idris
495replSettings = setComplete replCompletion defaultSettings
495replSettings = setComplete replCompletion defaultSettings
496
496
497-- invoke as if from command line
497-- invoke as if from command line