@@ -88,6 +88,10 @@ addDyLib libs = do i <- getIState
8888addHdr :: Codegen -> String -> Idris ()
8989addHdr tgt f = do i <- getIState; putIState $ i { idris_hdrs = nub $ (tgt, f) : idris_hdrs i }
9090
91+addImported :: FilePath -> Idris ()
92+addImported f = do i <- getIState
93+ putIState $ i { idris_imported = nub $ f : idris_imported i }
94+
9195addLangExt :: LanguageExt -> Idris ()
9296addLangExt TypeProviders = do i <- getIState
9397 putIState $ i {
@@ -357,6 +361,9 @@ addNameIdx' i n
357361getHdrs :: Codegen -> Idris [String]
358362getHdrs tgt = do i <- getIState; return (forCodegen tgt $ idris_hdrs i)
359363
364+getImported :: Idris [FilePath]
365+getImported = do i <- getIState; return (idris_imported i)
366+
360367setErrSpan :: FC -> Idris ()
361368setErrSpan x = do i <- getIState;
362369 case (errSpan i) of
@@ -490,6 +497,12 @@ getUndefined :: Idris [Name]
490497getUndefined = do i <- getIState
491498 return (map fst (idris_metavars i) \\ primDefs)
492499
500+isMetavarName :: Name -> IState -> Bool
501+isMetavarName n ist
502+ = case lookupNames n (tt_ctxt ist) of
503+ (t:_) -> isJust $ lookup t (idris_metavars ist)
504+ _ -> False
505+
493506getWidth :: Idris ConsoleWidth
494507getWidth = fmap idris_consolewidth getIState
495508
@@ -505,155 +518,16 @@ renderWidth = do iw <- getWidth
505518 AutomaticWidth -> runIO getScreenWidth
506519
507520
508−iRender :: Doc a -> Idris (SimpleDoc a)
509−iRender d = do w <- getWidth
510− ist <- getIState
511− let ideSlave = case idris_outputmode ist of
512− IdeSlave _ -> True
513− _ -> False
514− case w of
515− InfinitelyWide -> return $ renderPretty 1.0 1000000000 d
516− ColsWide n -> return $
517− if n < 1
518− then renderPretty 1.0 1000000000 d
519− else renderPretty 0.8 n d
520− AutomaticWidth | ideSlave -> return $ renderPretty 1.0 1000000000 d
521− | otherwise -> do width <- runIO getScreenWidth
522− return $ renderPretty 0.8 width d
523−
524−ihPrintResult :: Handle -> String -> Idris ()
525−ihPrintResult h s = do i <- getIState
526− case idris_outputmode i of
527− RawOutput -> case s of
528− "" -> return ()
529− s -> runIO $ hPutStrLn h s
530− IdeSlave n ->
531− let good = SexpList [SymbolAtom "ok", toSExp s] in
532− runIO $ hPutStrLn h $ convSExp "return" good n
533−
534−-- | Write a pretty-printed term to the console with semantic coloring
535−consoleDisplayAnnotated :: Handle -> Doc OutputAnnotation -> Idris ()
536−consoleDisplayAnnotated h output = do ist <- getIState
537− rendered <- iRender $ output
538− runIO . hPutStrLn h .
539− displayDecorated (consoleDecorate ist) $
540− rendered
541−
542−
543−-- | Write pretty-printed output to IDESlave with semantic annotations
544−ideSlaveReturnAnnotated :: Integer -> Handle -> Doc OutputAnnotation -> Idris ()
545−ideSlaveReturnAnnotated n h out = do ist <- getIState
546− (str, spans) <- fmap displaySpans .
547− iRender .
548− fmap (fancifyAnnots ist) $
549− out
550− let good = [SymbolAtom "ok", toSExp str, toSExp spans]
551− runIO . hPutStrLn h $ convSExp "return" good n
552−
553−ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()
554−ihPrintTermWithType h tm ty = do ist <- getIState
555− let output = tm <+> colon <+> ty
556− case idris_outputmode ist of
557− RawOutput -> consoleDisplayAnnotated h output
558− IdeSlave n -> ideSlaveReturnAnnotated n h output
559−
560−-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name
561−ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()
562−ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n
563−ihPrintFunTypes h bnd n overloads = do imp <- impShow
564− ist <- getIState
565− let output = vsep (map (uncurry (ppOverload imp)) overloads)
566− case idris_outputmode ist of
567− RawOutput -> consoleDisplayAnnotated h output
568− IdeSlave n -> ideSlaveReturnAnnotated n h output
569− where fullName n = prettyName True bnd n
570− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)
571−
572−ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
573−ihRenderResult h d = do ist <- getIState
574− case idris_outputmode ist of
575− RawOutput -> consoleDisplayAnnotated h d
576− IdeSlave n -> ideSlaveReturnAnnotated n h d
577−
578−fancifyAnnots :: IState -> OutputAnnotation -> OutputAnnotation
579−fancifyAnnots ist annot@(AnnName n _ _) =
580− do let ctxt = tt_ctxt ist
581− case () of
582− _ | isDConName n ctxt -> AnnName n (Just DataOutput) Nothing
583− _ | isFnName n ctxt -> AnnName n (Just FunOutput) Nothing
584− _ | isTConName n ctxt -> AnnName n (Just TypeOutput) Nothing
585− _ | otherwise -> annot
586−fancifyAnnots _ annot = annot
587521
588522type1Doc :: Doc OutputAnnotation
589523type1Doc = (annotate AnnConstType $ text "Type 1")
590524
591−-- | Show an error with semantic highlighting
592−ihRenderError :: Handle -> Doc OutputAnnotation -> Idris ()
593−ihRenderError h e = do ist <- getIState
594− case idris_outputmode ist of
595− RawOutput -> consoleDisplayAnnotated h e
596− IdeSlave n -> do
597− (str, spans) <- fmap displaySpans .
598− iRender .
599− fmap (fancifyAnnots ist) $
600− e
601− let good = [SymbolAtom "error", toSExp str, toSExp spans]
602− runIO . hPutStrLn h $ convSExp "return" good n
603−
604−ihPrintError :: Handle -> String -> Idris ()
605−ihPrintError h s = do i <- getIState
606− case idris_outputmode i of
607− RawOutput -> case s of
608− "" -> return ()
609− s -> runIO $ hPutStrLn h s
610− IdeSlave n ->
611− let good = SexpList [SymbolAtom "error", toSExp s] in
612− runIO . hPutStrLn h $ convSExp "return" good n
613−
614−ihputStrLn :: Handle -> String -> Idris ()
615−ihputStrLn h s = do i <- getIState
616− case idris_outputmode i of
617− RawOutput -> runIO $ hPutStrLn h s
618− IdeSlave n -> runIO . hPutStrLn h $ convSExp "write-string" s n
619−
620−iputStrLn = ihputStrLn stdout
621−iPrintError = ihPrintError stdout
622−iPrintResult = ihPrintResult stdout
623−iWarn = ihWarn stdout
624−
625−ideslavePutSExp :: SExpable a => String -> a -> Idris ()
626−ideslavePutSExp cmd info = do i <- getIState
627− case idris_outputmode i of
628− IdeSlave n -> runIO . putStrLn $ convSExp cmd info n
629− _ -> return ()
630−
631−-- this needs some typing magic and more structured output towards emacs
632−iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
633−iputGoal g = do i <- getIState
634− case idris_outputmode i of
635− RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
636− IdeSlave n -> runIO . putStrLn $
637− convSExp "write-goal" (displayS (fmap (fancifyAnnots i) g) "") n
638525
639526isetPrompt :: String -> Idris ()
640527isetPrompt p = do i <- getIState
641528 case idris_outputmode i of
642529 IdeSlave n -> runIO . putStrLn $ convSExp "set-prompt" p n
643530
644−ihWarn :: Handle -> FC -> Doc OutputAnnotation -> Idris ()
645−ihWarn h fc err = do i <- getIState
646− case idris_outputmode i of
647− RawOutput ->
648− do err' <- iRender . fmap (fancifyAnnots i) $
649− text (show fc) <> colon <//> err
650− runIO . hPutStrLn h $ displayDecorated (consoleDecorate i) err'
651− IdeSlave n ->
652− do err' <- iRender . fmap (fancifyAnnots i) $ err
653− let (str, spans) = displaySpans err'
654− runIO . hPutStrLn h $
655− convSExp "warning" (fc_fname fc, fc_start fc, fc_end fc, str, spans) n
656−
657531setLogLevel :: Int -> Idris ()
658532setLogLevel l = do i <- getIState
659533 let opts = idris_options i
@@ -1701,8 +1575,6 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
17011575 = do mf <- match' f f'
17021576 ms <- zipWithM matchArg args args'
17031577 return (mf ++ concat ms)
1704−-- match (PRef _ n) (PRef _ n') | n == n' = return []
1705−-- | otherwise = Nothing
17061578 match (PRef f n) (PApp _ x []) = match (PRef f n) x
17071579 match (PPatvar f n) xr = match (PRef f n) xr
17081580 match xr (PPatvar f n) = match xr (PRef f n)
@@ -1712,7 +1584,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
17121584 (not (isConName n (tt_ctxt i) || isFnName n (tt_ctxt i))
17131585 || tm == Placeholder)
17141586 = return [(n, tm)]
1715− | n == n' = return []
1587+ -- if one namespace is missing, drop the other
1588+ | n == n' || n == dropNS n' || dropNS n == n' = return []
1589+ where dropNS (NS n _) = n
1590+ dropNS n = n
17161591 match (PRef _ n) tm
17171592 | not names && (not (isConName n (tt_ctxt i) ||
17181593 isFnName n (tt_ctxt i)) || tm == Placeholder)
@@ -1855,6 +1730,12 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
18551730 mkUniqA arg = do t' <- mkUniq (getTm arg)
18561731 return (arg { getTm = t' })
18571732
1733+ -- Initialise the unique name with the environment length (so we're not
1734+ -- looking for too long...)
1735+ initN (UN n) l = UN $ txt (str n ++ show l)
1736+ initN (MN i s) l = MN (i+l) s
1737+ initN n l = n
1738+
18581739 -- FIXME: Probably ought to do this for completeness! It's fine as
18591740 -- long as there are no bindings inside tactics though.
18601741 mkUniqT tac = return tac
@@ -1864,7 +1745,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
18641745 = do env <- get
18651746 (n', sc') <-
18661747 if n `elem` env
1867− then do let n' = uniqueName n (env ++ inScope)
1748+ then do let n' = uniqueName (initN n (length env))
1749+ (env ++ inScope)
18681750 return (n', shadow n n' sc)
18691751 else return (n, sc)
18701752 put (n' : env)
@@ -1875,7 +1757,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
18751757 = do env <- get
18761758 (n', sc') <-
18771759 if n `elem` env
1878− then do let n' = uniqueName n (env ++ inScope)
1760+ then do let n' = uniqueName (initN n (length env))
1761+ (env ++ inScope)
18791762 return (n', shadow n n' sc)
18801763 else return (n, sc)
18811764 put (n' : env)
@@ -1886,7 +1769,8 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
18861769 = do env <- get
18871770 (n', sc') <-
18881771 if n `elem` env
1889− then do let n' = uniqueName n (env ++ inScope)
1772+ then do let n' = uniqueName (initN n (length env))
1773+ (env ++ inScope)
18901774 return (n', shadow n n' sc)
18911775 else return (n, sc)
18921776 put (n' : env)