22d4f7e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1046 from david-christiansen/metavar-ideslave

Add command to IDESlave for metavars

commit22d4f7e13ff76e8b57e18816e4b6cdd73c8a953e authorEdwin Brady <edwin.brady@gmail.com> dateWed 9 Apr 2014, 13:48 (13 years ago) parentc074709 8374804

3 files changed+37

compare with master

unifiedsplit

CHANGELOG+4 src/Idris/IdeSlave.hs+2 src/Idris/REPL.hs+31

CHANGELOG+4

@@ -1,3 +1,7 @@

1+New in 0.9.13:

2+--------------

3+* IDE support for retrieving structured information about metavariables

15New in 0.9.12:

26--------------

src/Idris/IdeSlave.hs+2

@@ -151,6 +151,7 @@ data IdeSlaveCommand = REPLCompletions String

151151 | Apropos String

152152 | GetOpts

153153 | SetOpt Opt Bool

154+ | Metavariables Int -- ^^ the Int is the column count for pretty-printing

154155 deriving Show

155156

156157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

@@ -174,6 +175,7 @@ sexpToCommand (SymbolAtom "get-options")

174175sexpToCommand (SexpList [SymbolAtom "set-option", SymbolAtom s, BoolAtom b])

175176 | Just opt <- lookup s opts = Just (SetOpt opt b)

176177 where opts = [("show-implicits", ShowImpl), ("error-context", ErrContext)] --TODO support more

178+sexpToCommand (SexpList [SymbolAtom "metavariables", IntegerAtom cols]) = Just (Metavariables (fromIntegral cols))

177179sexpToCommand _ = Nothing

178180

179181parseMessage :: String -> Either Err (SExp, Integer)

src/Idris/REPL.hs+31

@@ -284,6 +284,16 @@ ideslave orig mods

284284 do setErrContext b

285285 let msg = (IdeSlave.SymbolAtom "ok", b)

286286 runIO . putStrLn $ IdeSlave.convSExp "return" msg id

287+ Just (IdeSlave.Metavariables cols) ->

288+ do ist <- getIState

289+ let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

290+ imp <- impShow

291+ let mvarTys = map (delabTy ist) mvs

292+ let res = (IdeSlave.SymbolAtom "ok",

293+ zipWith (\ n (prems, concl) -> (n, prems, concl))

294+ (map (IdeSlave.StringAtom . show) mvs)

295+ (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

296+ runIO . putStrLn $ IdeSlave.convSExp "return" res id

287297 Nothing -> do iPrintError "did not understand")

288298 (\e -> do iPrintError $ show e))

289299 (\e -> do iPrintError $ show e)

@@ -293,6 +303,27 @@ ideslave orig mods

293303 [] -> Left ("Didn't understand name '" ++ s ++ "'")

294304 [n] -> Right $ sUN n

295305 (n:ns) -> Right $ sNS (sUN n) ns

306+ getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

307+ getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

308+ in ((n, t):prems, conc)

309+ getGoal tm = ([], tm)

310+ sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

311+ -> ([(String, String, SpanList OutputAnnotation)],

312+ (String, SpanList OutputAnnotation))

313+ sexpGoal ist cols imp ns ([], concl) =

314+ let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

315+ pprintPTerm imp (zip ns (repeat False)) [] concl

316+ in ([], concl')

317+ sexpGoal ist cols imp ns ((n, t):ps, concl) =

318+ let n' = case n of

319+ NS (UN nm) ns -> str nm

320+ UN nm | ('_':'_':_) <- str nm -> "_"

321+ | otherwise -> str nm

322+ _ -> "_"

323+ (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

324+ pprintPTerm imp (zip ns (repeat False)) [] t

325+ rest = sexpGoal ist cols imp (n:ns) (ps, concl)

326+ in ((n', t', spans) : fst rest, snd rest)

296327

297328ideslaveProcess :: FilePath -> Command -> Idris ()

298329ideslaveProcess fn Help = process stdout fn Help