git.iko.soy/Idris-dev
on master help sign in
Crude support for completion in prover

The prover can use the local proof state and the global environment for completion. Right now, it doesn't always stop completing when it should (f.x. tactics that take an already defined name are being completed with whole expressions) but it's already useful.

commit66d8360553325849bc456df3ec59ac15bc50a53d authorDavid Christiansen <david@davidchristiansen.dk> dateMon 11 Feb 2013, 16:51 (14 years ago) parent52203a3
2 files changed+37−30
compare with master
unifiedsplit
src/Idris/Completion.hs+24−22 src/Idris/Prover.hs+13−8
src/Idris/Completion.hs+24−22
@@ -49,24 +49,22 @@ commands = map fst cmdArgs
4949-- | A specification of the arguments that tactics can take
5050data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
5151 | ExprTArg
52− | TacticTArg
53− | CommasTArg TacticArg
54− | AltTArg TacticArg TacticArg
52+ | AltsTArg
5553
5654-- | A list of available tactics and their argument requirements
5755tacticArgs :: [(String, Maybe TacticArg)]
58−tacticArgs = [ ("intro", Just $ CommasTArg NameTArg)
56+tacticArgs = [ ("intro", Nothing)
5957 , ("intros", Nothing)
60− , ("refine", Just NameTArg)
61− , ("rewrite", Just NameTArg)
58+ , ("refine", Just ExprTArg)
59+ , ("rewrite", Just ExprTArg)
6260 , ("let", Nothing) -- FIXME syntax for let
63− , ("focus", Just NameTArg)
61+ , ("focus", Just ExprTArg)
6462 , ("exact", Just ExprTArg)
6563 , ("reflect", Just ExprTArg)
66− , ("try", Just $ AltTArg TacticTArg TacticTArg)
64+ , ("try", Just AltsTArg)
6765 ] ++ map (\x -> (x, Nothing)) [
68− "compute", "trivial", "solve", "attack", "state",
69− "term", "undo", "qed", "abandon", ":q"
66+ "intro", "intros", "compute", "trivial", "solve", "attack",
67+ "state", "term", "undo", "qed", "abandon", ":q"
7068 ]
7169tactics = map fst tacticArgs
7270
@@ -100,12 +98,12 @@ completeWith ns n = if uniqueExists
10098 where prefixMatches = filter (isPrefixOf n) ns
10199 uniqueExists = n `elem` prefixMatches
102100
103−completeName :: String -> Idris [Completion]
104−completeName n = do ns <- names
105− return $ completeWith ns n
101+completeName :: [String] -> String -> Idris [Completion]
102+completeName extra n = do ns <- names
103+ return $ completeWith (extra ++ ns) n
106104
107−completeExpr :: CompletionFunc Idris
108−completeExpr = completeWord Nothing " \t" completeName
105+completeExpr :: [String] -> CompletionFunc Idris
106+completeExpr extra = completeWord Nothing " \t" (completeName extra)
109107
110108completeOption :: CompletionFunc Idris
111109completeOption = completeWord Nothing " \t" completeOpt
@@ -118,24 +116,28 @@ isWhitespace = (flip elem) " \t\n"
118116completeCmd :: String -> CompletionFunc Idris
119117completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
120118 where completeArg FileArg = completeFilename (prev, next)
121− completeArg NameArg = completeExpr (prev, next) -- FIXME only complete one name
119+ completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
122120 completeArg OptionArg = completeOption (prev, next)
123121 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
124− completeArg ExprArg = completeExpr (prev, next)
122+ completeArg ExprArg = completeExpr [] (prev, next)
125123 completeCmdName = return $ ("", completeWith commands cmd)
126124
127125replCompletion :: CompletionFunc Idris
128126replCompletion (prev, next) = case firstWord of
129127 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
130− _ -> completeExpr (prev, next)
128+ _ -> completeExpr [] (prev, next)
131129 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
132130
133131
134−completeTactic :: String -> CompletionFunc Idris
135−completeTactic tac (prev, next) = return $ completeTacName tac
132+completeTactic :: [String] -> String -> CompletionFunc Idris
133+completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs
136134 where completeTacName = return $ ("", completeWith tactics tac)
135+ completeArg Nothing = noCompletion (prev, next)
136+ completeArg (Just NameTArg) = noCompletion (prev, next) -- this is for binding new names!
137+ completeArg (Just ExprTArg) = completeExpr as (prev, next)
138+ completeArg (Just AltsTArg) = noCompletion (prev, next) -- TODO
137139
138140
139−proverCompletion :: CompletionFunc Idris
140−proverCompletion (prev, next) = completeTactic firstWord (prev, next)
141+proverCompletion :: [String] -> CompletionFunc Idris
142+proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
141143 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
src/Idris/Prover.hs+13−8
@@ -38,13 +38,18 @@ showProof lit n ps
3838 where bird = if lit then "> " else ""
3939 break = "\n" ++ bird
4040
41−proverSettings :: Settings Idris
42−proverSettings = setComplete proverCompletion defaultSettings
41+proverSettings :: ElabState [PDecl] -> Settings Idris
42+proverSettings e = setComplete (proverCompletion assumptionNames) defaultSettings
43+ where assumptionNames = case envAtFocus (proof e) of
44+ OK env -> names env
45+ names [] = []
46+ names ((MN _ _, _) : bs) = names bs
47+ names ((n, _) : bs) = show n : names bs
4348
4449prove :: Context -> Bool -> Name -> Type -> Idris ()
4550prove ctxt lit n ty
4651 = do let ps = initElaborator n ctxt ty
47− (tm, prf) <- runInputT proverSettings $ ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)
52+ (tm, prf) <- ploop True ("-" ++ show n) [] (ES (ps, []) "" Nothing)
4853 iLOG $ "Adding " ++ show tm
4954 iputStrLn $ showProof lit n prf
5055 i <- getIState
@@ -112,18 +117,18 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
112117lifte st e = do (v, _) <- elabStep st e
113118 return v
114119
115−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> InputT Idris (Term, [String])
120+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
116121ploop d prompt prf e
117− = do i <- lift getIState
122+ = do i <- getIState
118123 when d $ liftIO $ dumpState i (proof e)
119− x <- getInputLine (prompt ++ "> ")
124+ x <- runInputT (proverSettings e) $ getInputLine (prompt ++ "> ")
120125 (cmd, step) <- case x of
121126 Nothing -> fail "Abandoned"
122127 Just input -> do return (parseTac i input, input)
123128 case cmd of
124129 Right Abandon -> fail "Abandoned"
125130 _ -> return ()
126− (d, st, done, prf') <- lift $ idrisCatch
131+ (d, st, done, prf') <- idrisCatch
127132 (case cmd of
128133 Left err -> do iputStrLn (show err)
129134 return (False, e, False, prf)
@@ -144,7 +149,7 @@ ploop d prompt prf e
144149 return (True, st, False, prf ++ [step]))
145150 (\err -> do iputStrLn (show err)
146151 return (False, e, False, prf))
147− if done then do (tm, _) <- lift $ elabStep st get_term
152+ if done then do (tm, _) <- elabStep st get_term
148153 return (tm, prf')
149154 else ploop d prompt prf' st
150155