@@ -1,4 +1,4 @@
1−module Idris.Completion (replCompletion) where
1+module Idris.Completion (replCompletion, proverCompletion) where
22
33import Core.Evaluate (ctxtAlist)
44import Core.TT
@@ -46,6 +46,30 @@ cmdArgs = [ (":t", ExprArg)
4646 ]
4747commands = map fst cmdArgs
4848
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+
4973-- | Convert a name into a string usable for completion. Filters out names
5074-- that users probably don't want to see.
5175nameString :: Name -> Maybe String
@@ -57,16 +81,18 @@ nameString _ = Nothing
5781
5882-- FIXME: Respect module imports
5983-- | Get the user-visible names from the current interpreter state.
60−names :: StateT IState IO [String]
84+names :: Idris[String]
6185names = do i <- get
6286 let ctxt = tt_ctxt i
6387 return $ nub $ mapMaybe (nameString . fst) $ ctxtAlist ctxt
6488
6589
66−modules :: StateT IState IO [String]
90+modules :: Idris [String]
6791modules = do i <- get
6892 return $ map show $ imported i
6993
94+
95+
7096completeWith :: [String] -> String -> [Completion]
7197completeWith ns n = if uniqueExists
7298 then [simpleCompletion n]
@@ -74,14 +100,14 @@ completeWith ns n = if uniqueExists
74100 where prefixMatches = filter (isPrefixOf n) ns
75101 uniqueExists = n `elem` prefixMatches
76102
77−completeName :: String -> StateT IState IO [Completion]
103+completeName :: String -> Idris [Completion]
78104completeName n = do ns <- names
79105 return $ completeWith ns n
80106
81−completeExpr :: CompletionFunc (StateT IState IO)
107+completeExpr :: CompletionFunc Idris
82108completeExpr = completeWord Nothing " \t" completeName
83109
84−completeOption :: CompletionFunc (StateT IState IO)
110+completeOption :: CompletionFunc Idris
85111completeOption = completeWord Nothing " \t" completeOpt
86112 where completeOpt = return . (completeWith ["errorcontext", "showimplicits"])
87113
@@ -89,8 +115,8 @@ isWhitespace :: Char -> Bool
89115isWhitespace = (flip elem) " \t\n"
90116
91117-- | Get the completion function for a particular command
92−completeCmd :: String -> CompletionFunc (StateT IState IO)
93−completeCmd cmd (prev, next) = fromMaybe completeCmdName (fmap completeArg $ lookup cmd cmdArgs)
118+completeCmd :: String -> CompletionFunc Idris
119+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
94120 where completeArg FileArg = completeFilename (prev, next)
95121 completeArg NameArg = completeExpr (prev, next) -- FIXME only complete one name
96122 completeArg OptionArg = completeOption (prev, next)
@@ -98,8 +124,18 @@ completeCmd cmd (prev, next) = fromMaybe completeCmdName (fmap completeArg $ loo
98124 completeArg ExprArg = completeExpr (prev, next)
99125 completeCmdName = return $ ("", completeWith commands cmd)
100126
101−replCompletion :: CompletionFunc (StateT IState IO)
127+replCompletion :: CompletionFunc Idris
102128replCompletion (prev, next) = case firstWord of
103129 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
104130 _ -> 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