e3cfa93 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add command to IDESlave for metavars

Fixes #1036.

commite3cfa93334bf7663d36a1ed1026cdbbd53f39d9e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 9 Apr 2014, 13:51 (13 years ago) parentd53dc76

2 files changed+33

compare with master

unifiedsplit

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

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

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

286286 do setErrContext b

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

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

289+ Just (IdeSlave.Metavariables cols) ->

290+ do ist <- getIState

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

292+ imp <- impShow

293+ let mvarTys = map (delabTy ist) mvs

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

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

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

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

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

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

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

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

@@ -295,6 +305,27 @@ ideslave orig mods

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

296306 [n] -> Right $ sUN n

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

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

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

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

311+ getGoal tm = ([], tm)

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

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

314+ (String, SpanList OutputAnnotation))

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

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

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

318+ in ([], concl')

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

320+ let n' = case n of

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

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

323+ | otherwise -> str nm

324+ _ -> "_"

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

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

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

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

298329

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

300331ideslaveProcess fn Help = process stdout fn Help