@@ -342,34 +342,62 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =
342342 do ist <- getIState
343343 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
344344 let ppo = ppOptionIst ist
345− let mvarTys = map (delabTy ist) mvs
346− let res = (IdeSlave.SymbolAtom "ok",
347− zipWith (\ n (prems, concl) -> (n, prems, concl))
348− (map (IdeSlave.StringAtom . show) mvs)
349− (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))
350− runIO . putStrLn $ IdeSlave.convSExp "return" res id
351− where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)
352− getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc
353− in ((n, t):prems, conc)
354− getGoal tm = ([], tm)
355− sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)
356− -> ([(String, String, SpanList OutputAnnotation)],
357− (String, SpanList OutputAnnotation))
358− sexpGoal ist cols ppo ns ([], concl) =
359− let infixes = idris_infixes ist
360− concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
361− pprintPTerm ppo (zip ns (repeat False)) [] infixes concl
362− in ([], concl')
363− sexpGoal ist cols ppo ns ((n, t):ps, concl) =
364− let n' = case n of
365− NS (UN nm) ns -> str nm
366− UN nm | ('_':'_':_) <- str nm -> "_"
367− | otherwise -> str nm
368− _ -> "_"
369− (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $
370− pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t
371− rest = sexpGoal ist cols ppo (n:ns) (ps, concl)
372− in ((n', t', spans) : fst rest, snd rest)
345+ -- splitMvs is a list of pairs of names and their split types
346+ let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
347+ -- mvOutput is the pretty-printed version ready for conversion to SExpr
348+ let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
349+ mapPair show
350+ (\(hs, c, pc) ->
351+ let bnd = [ n | (n,_,_) <- hs ] in
352+ let bnds = inits bnd in
353+ (map (\(bnd, h) -> processPremise ist bnd h)
354+ (zip bnds hs),
355+ render ist bnd c pc))
356+ splitMvs
357+ runIO . putStrLn $
358+ IdeSlave.convSExp "return" (IdeSlave.SymbolAtom "ok", mvOutput) id
359+ where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
360+ mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
361+
362+ -- | Split a function type into a pair of premises, conclusion.
363+ -- Each maintains both the original and delaborated versions.
364+ splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
365+ splitPi ist (Bind n (Pi t) rest) =
366+ let (hs, c, pc) = splitPi ist rest in
367+ ((n, t, delabTy' ist [] t False False):hs,
368+ c, delabTy' ist [] c False False)
369+ splitPi ist tm = ([], tm, delabTy' ist [] tm False False)
370+
371+ -- | Get the types of a list of metavariable names
372+ mvTys :: IState -> [Name] -> [(Name, Type)]
373+ mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
374+
375+ -- | Show a type and its corresponding PTerm in a format suitable
376+ -- for the IDE - that is, pretty-printed and annotated.
377+ render :: IState -> [Name] -> Type -> PTerm -> (String, SpanList OutputAnnotation)
378+ render ist bnd t pt =
379+ let prettyT = pprintPTerm (ppOptionIst ist)
380+ (zip bnd (repeat False))
381+ []
382+ (idris_infixes ist)
383+ pt
384+ in
385+ displaySpans .
386+ renderPretty 0.9 cols .
387+ fmap (fancifyAnnots ist) .
388+ annotate (AnnTerm t) $ prettyT
389+
390+ -- | Juggle the bits of a premise to prepare for output.
391+ processPremise :: IState
392+ -> [Name] -- ^ the names to highlight as bound
393+ -> (Name, Type, PTerm)
394+ -> (String,
395+ String,
396+ SpanList OutputAnnotation)
397+ processPremise ist bnd (n, t, pt) =
398+ let (out, spans) = render ist bnd t pt in
399+ (show n , out, spans)
400+
373401runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =
374402 case splitName n of
375403 Left err -> iPrintError err