git.iko.soy/Idris-dev
on master help sign in
Crude support for completion in prover
66d8360David Christiansen
src/Idris/Completion.hs+24−22
compare with master
unifiedsplit
@@ -49,24 +49,22 @@ commands = map fst cmdArgs
49-- | A specification of the arguments that tactics can take
49-- | A specification of the arguments that tactics can take
50data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
50data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
51 | ExprTArg
51 | ExprTArg
52− | TacticTArg
52+ | AltsTArg
53− | CommasTArg TacticArg
54− | AltTArg TacticArg TacticArg
55
53
56-- | A list of available tactics and their argument requirements
54-- | A list of available tactics and their argument requirements
57tacticArgs :: [(String, Maybe TacticArg)]
55tacticArgs :: [(String, Maybe TacticArg)]
58−tacticArgs = [ ("intro", Just $ CommasTArg NameTArg)
56+tacticArgs = [ ("intro", Nothing)
59 , ("intros", Nothing)
57 , ("intros", Nothing)
60− , ("refine", Just NameTArg)
58+ , ("refine", Just ExprTArg)
61− , ("rewrite", Just NameTArg)
59+ , ("rewrite", Just ExprTArg)
62 , ("let", Nothing) -- FIXME syntax for let
60 , ("let", Nothing) -- FIXME syntax for let
63− , ("focus", Just NameTArg)
61+ , ("focus", Just ExprTArg)
64 , ("exact", Just ExprTArg)
62 , ("exact", Just ExprTArg)
65 , ("reflect", Just ExprTArg)
63 , ("reflect", Just ExprTArg)
66− , ("try", Just $ AltTArg TacticTArg TacticTArg)
64+ , ("try", Just AltsTArg)
67 ] ++ map (\x -> (x, Nothing)) [
65 ] ++ map (\x -> (x, Nothing)) [
68− "compute", "trivial", "solve", "attack", "state",
66+ "intro", "intros", "compute", "trivial", "solve", "attack",
69− "term", "undo", "qed", "abandon", ":q"
67+ "state", "term", "undo", "qed", "abandon", ":q"
70 ]
68 ]
71tactics = map fst tacticArgs
69tactics = map fst tacticArgs
72
70
@@ -100,12 +98,12 @@ completeWith ns n = if uniqueExists
100 where prefixMatches = filter (isPrefixOf n) ns
98 where prefixMatches = filter (isPrefixOf n) ns
101 uniqueExists = n `elem` prefixMatches
99 uniqueExists = n `elem` prefixMatches
102
100
103−completeName :: String -> Idris [Completion]
101+completeName :: [String] -> String -> Idris [Completion]
104−completeName n = do ns <- names
102+completeName extra n = do ns <- names
105− return $ completeWith ns n
103+ return $ completeWith (extra ++ ns) n
106
104
107−completeExpr :: CompletionFunc Idris
105+completeExpr :: [String] -> CompletionFunc Idris
108−completeExpr = completeWord Nothing " \t" completeName
106+completeExpr extra = completeWord Nothing " \t" (completeName extra)
109
107
110completeOption :: CompletionFunc Idris
108completeOption :: CompletionFunc Idris
111completeOption = completeWord Nothing " \t" completeOpt
109completeOption = completeWord Nothing " \t" completeOpt
@@ -118,24 +116,28 @@ isWhitespace = (flip elem) " \t\n"
118completeCmd :: String -> CompletionFunc Idris
116completeCmd :: String -> CompletionFunc Idris
119completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
117completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
120 where completeArg FileArg = completeFilename (prev, next)
118 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
122 completeArg OptionArg = completeOption (prev, next)
120 completeArg OptionArg = completeOption (prev, next)
123 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
121 completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
124− completeArg ExprArg = completeExpr (prev, next)
122+ completeArg ExprArg = completeExpr [] (prev, next)
125 completeCmdName = return $ ("", completeWith commands cmd)
123 completeCmdName = return $ ("", completeWith commands cmd)
126
124
127replCompletion :: CompletionFunc Idris
125replCompletion :: CompletionFunc Idris
128replCompletion (prev, next) = case firstWord of
126replCompletion (prev, next) = case firstWord of
129 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
127 ':':cmdName -> completeCmd (':':cmdName) (prev, next)
130− _ -> completeExpr (prev, next)
128+ _ -> completeExpr [] (prev, next)
131 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
129 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
132
130
133
131
134−completeTactic :: String -> CompletionFunc Idris
132+completeTactic :: [String] -> String -> CompletionFunc Idris
135−completeTactic tac (prev, next) = return $ completeTacName tac
133+completeTactic as tac (prev, next) = fromMaybe completeTacName $ fmap completeArg $ lookup tac tacticArgs
136 where completeTacName = return $ ("", completeWith tactics tac)
134 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
137
139
138
140
139−proverCompletion :: CompletionFunc Idris
141+proverCompletion :: [String] -> CompletionFunc Idris
140−proverCompletion (prev, next) = completeTactic firstWord (prev, next)
142+proverCompletion assumptions (prev, next) = completeTactic assumptions firstWord (prev, next)
141 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
143 where firstWord = fst $ break isWhitespace $ dropWhile isWhitespace $ reverse prev
src/Idris/Prover.hs+13−8
@@ -38,13 +38,18 @@ showProof lit n ps
38 where bird = if lit then "> " else ""
38 where bird = if lit then "> " else ""
39 break = "\n" ++ bird
39 break = "\n" ++ bird
40
40
41−proverSettings :: Settings Idris
41+proverSettings :: ElabState [PDecl] -> Settings Idris
42−proverSettings = setComplete proverCompletion defaultSettings
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
43
48
44prove :: Context -> Bool -> Name -> Type -> Idris ()
49prove :: Context -> Bool -> Name -> Type -> Idris ()
45prove ctxt lit n ty
50prove ctxt lit n ty
46 = do let ps = initElaborator n ctxt ty
51 = 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)
48 iLOG $ "Adding " ++ show tm
53 iLOG $ "Adding " ++ show tm
49 iputStrLn $ showProof lit n prf
54 iputStrLn $ showProof lit n prf
50 i <- getIState
55 i <- getIState
@@ -112,18 +117,18 @@ lifte :: ElabState [PDecl] -> ElabD a -> Idris a
112lifte st e = do (v, _) <- elabStep st e
117lifte st e = do (v, _) <- elabStep st e
113 return v
118 return v
114
119
115−ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> InputT Idris (Term, [String])
120+ploop :: Bool -> String -> [String] -> ElabState [PDecl] -> Idris (Term, [String])
116ploop d prompt prf e
121ploop d prompt prf e
117− = do i <- lift getIState
122+ = do i <- getIState
118 when d $ liftIO $ dumpState i (proof e)
123 when d $ liftIO $ dumpState i (proof e)
119− x <- getInputLine (prompt ++ "> ")
124+ x <- runInputT (proverSettings e) $ getInputLine (prompt ++ "> ")
120 (cmd, step) <- case x of
125 (cmd, step) <- case x of
121 Nothing -> fail "Abandoned"
126 Nothing -> fail "Abandoned"
122 Just input -> do return (parseTac i input, input)
127 Just input -> do return (parseTac i input, input)
123 case cmd of
128 case cmd of
124 Right Abandon -> fail "Abandoned"
129 Right Abandon -> fail "Abandoned"
125 _ -> return ()
130 _ -> return ()
126− (d, st, done, prf') <- lift $ idrisCatch
131+ (d, st, done, prf') <- idrisCatch
127 (case cmd of
132 (case cmd of
128 Left err -> do iputStrLn (show err)
133 Left err -> do iputStrLn (show err)
129 return (False, e, False, prf)
134 return (False, e, False, prf)
@@ -144,7 +149,7 @@ ploop d prompt prf e
144 return (True, st, False, prf ++ [step]))
149 return (True, st, False, prf ++ [step]))
145 (\err -> do iputStrLn (show err)
150 (\err -> do iputStrLn (show err)
146 return (False, e, False, prf))
151 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
148 return (tm, prf')
153 return (tm, prf')
149 else ploop d prompt prf' st
154 else ploop d prompt prf' st
150
155