@@ -396,10 +396,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) =
396396 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
397397runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
398398 do ist <- getIState
399− let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
399+ let mvs = reverse $ [ (n, i)
400+ | (n, (_, i, _, _, _)) <- idris_metavars ist
401+ , not (n `elem` primDefs)
402+ ]
400403 let ppo = ppOptionIst ist
401404 -- splitMvs is a list of pairs of names and their split types
402− let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
405+ let splitMvs = [ (n, (premises, concl, tm))
406+ | (n, i, ty) <- mvTys ist mvs
407+ , let (premises, concl, tm) = splitPi ist i ty]
403408 -- mvOutput is the pretty-printed version ready for conversion to SExpr
404409 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
405410 mapPair show
@@ -413,20 +418,24 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
413418 runIO . hPutStrLn h $
414419 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
415420 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
416− mapSnd f xs = zip (map fst xs) (map (f . snd) xs)
421+ firstOfThree (x, y, z) = x
422+ mapThird f xs = map (\(x, y, z) -> (x, y, f z)) xs
417423
418424 -- | Split a function type into a pair of premises, conclusion.
419425 -- Each maintains both the original and delaborated versions.
420− splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
421− splitPi ist (Bind n (Pi _ _ t _) rest) =
422− let (hs, c, pc) = splitPi ist rest in
426+ splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
427+ splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =
428+ let (hs, c, pc) = splitPi ist (i - 1) rest in
423429 ((n, t, delabTy' ist [] t False False True):hs,
424430 c, delabTy' ist [] c False False True)
425− splitPi ist tm = ([], tm, delabTy' ist [] tm False False True)
431+ splitPi ist i tm = ([], tm, delabTy' ist [] tm False False True)
426432
427433 -- | Get the types of a list of metavariable names
428− mvTys :: IState -> [Name] -> [(Name, Type)]
429− mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
434+ mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
435+ mvTys ist mvs = [ (n, i, ty)
436+ | (n, i) <- mvs
437+ , ty <- maybeToList (fmap (vToP . snd) (lookupTyNameExact n (tt_ctxt ist)))
438+ ]
430439
431440 -- | Show a type and its corresponding PTerm in a format suitable
432441 -- for the IDE - that is, pretty-printed and annotated.