@@ -396,10 +396,15 @@ runIdeModeCommand h id orig fn mods (IdeMode.SetOpt IdeMode.ErrContext b) =
396 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
396 runIO . hPutStrLn h $ IdeMode.convSExp "return" msg id
397runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
397runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
398 do ist <- getIState
398 do ist <- getIState
399+ let mvs = reverse $ [ (n, i)
399− let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs
400+ | (n, (_, i, _, _, _)) <- idris_metavars ist
401+ , not (n `elem` primDefs)
400 let ppo = ppOptionIst ist
403 let ppo = ppOptionIst ist
401 -- splitMvs is a list of pairs of names and their split types
404 -- splitMvs is a list of pairs of names and their split types
405+ let splitMvs = [ (n, (premises, concl, tm))
402− let splitMvs = mapSnd (splitPi ist) (mvTys ist mvs)
406+ | (n, i, ty) <- mvTys ist mvs
407+ , let (premises, concl, tm) = splitPi ist i ty]
403 -- mvOutput is the pretty-printed version ready for conversion to SExpr
408 -- mvOutput is the pretty-printed version ready for conversion to SExpr
404 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
409 let mvOutput = map (\(n, (hs, c)) -> (n, hs, c)) $
405 mapPair show
410 mapPair show
@@ -413,20 +418,24 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =
413 runIO . hPutStrLn h $
418 runIO . hPutStrLn h $
414 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
419 IdeMode.convSExp "return" (IdeMode.SymbolAtom "ok", mvOutput) id
415 where mapPair f g xs = zip (map (f . fst) xs) (map (g . snd) xs)
420 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
418 -- | Split a function type into a pair of premises, conclusion.
424 -- | Split a function type into a pair of premises, conclusion.
419 -- Each maintains both the original and delaborated versions.
425 -- Each maintains both the original and delaborated versions.
420− splitPi :: IState -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
426+ splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)
421− splitPi ist (Bind n (Pi _ _ t _) rest) =
427+ splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =
422− let (hs, c, pc) = splitPi ist rest in
428+ let (hs, c, pc) = splitPi ist (i - 1) rest in
423 ((n, t, delabTy' ist [] t False False True):hs,
429 ((n, t, delabTy' ist [] t False False True):hs,
424 c, delabTy' ist [] c False False True)
430 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)
427 -- | Get the types of a list of metavariable names
433 -- | Get the types of a list of metavariable names
428− mvTys :: IState -> [Name] -> [(Name, Type)]
434+ mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]
435+ mvTys ist mvs = [ (n, i, ty)
429− mvTys ist = mapSnd vToP . mapMaybe (flip lookupTyNameExact (tt_ctxt ist))
437+ , ty <- maybeToList (fmap (vToP . snd) (lookupTyNameExact n (tt_ctxt ist)))
431 -- | Show a type and its corresponding PTerm in a format suitable
440 -- | Show a type and its corresponding PTerm in a format suitable
432 -- for the IDE - that is, pretty-printed and annotated.
441 -- for the IDE - that is, pretty-printed and annotated.