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

git.iko.soy/Idris-dev

on master help sign in

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

22d4f7eEdwin Brady13 years ago

CHANGELOG+4

compare with master

unifiedsplit

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

1+New in 0.9.13:

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

3+* IDE support for retrieving structured information about metavariables

1New in 0.9.12:

5New in 0.9.12:

2--------------

6--------------

src/Idris/IdeSlave.hs+2

@@ -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

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

284 do setErrContext b

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

286 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

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

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

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

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

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

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

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

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

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

294 [n] -> Right $ sUN n

304 [n] -> Right $ sUN n

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

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

296

327

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

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

298ideslaveProcess fn Help = process stdout fn Help

329ideslaveProcess fn Help = process stdout fn Help