e3cfa93 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add command to IDESlave for metavars

e3cfa93David Raymond Christiansen13 years ago

src/Idris/IdeSlave.hs+2

compare with master

unifiedsplit

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

151 | Apropos String

152 | GetOpts

153 | SetOpt Opt Bool

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

154 deriving Show

155 deriving Show

155

156

156sexpToCommand :: SExp -> Maybe IdeSlaveCommand

157sexpToCommand :: SExp -> Maybe IdeSlaveCommand

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

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

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

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

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

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

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

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

177sexpToCommand _ = Nothing

179sexpToCommand _ = Nothing

178

180

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

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

src/Idris/REPL.hs+31

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

286 do setErrContext b

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

288 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

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

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

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

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

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

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

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

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

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

296 [n] -> Right $ sUN n

306 [n] -> Right $ sUN n

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

307 (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)

298

329

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

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

300ideslaveProcess fn Help = process stdout fn Help

331ideslaveProcess fn Help = process stdout fn Help