diff --git a/libs/base/Data/Fin.idr b/libs/base/Data/Fin.idr index 8b5671198..b714c24ba 100644 --- a/libs/base/Data/Fin.idr +++ b/libs/base/Data/Fin.idr @@ -1,6 +1,6 @@ module Data.Fin -import Data.Maybe +import public Data.Maybe import Data.Nat import Decidable.Equality diff --git a/libs/base/Data/List/Views.idr b/libs/base/Data/List/Views.idr index f0672d578..b285b94ef 100644 --- a/libs/base/Data/List/Views.idr +++ b/libs/base/Data/List/Views.idr @@ -2,6 +2,7 @@ module Data.List.Views import Control.WellFounded import Data.List +import Data.Nat import Data.Nat.Views lengthSuc : (xs : List a) -> (y : a) -> (ys : List a) -> diff --git a/libs/base/Data/Nat/Views.idr b/libs/base/Data/Nat/Views.idr index ca83b48b7..0cef32a11 100644 --- a/libs/base/Data/Nat/Views.idr +++ b/libs/base/Data/Nat/Views.idr @@ -1,6 +1,7 @@ module Data.Nat.Views import Control.WellFounded +import Data.Nat ||| View for dividing a Nat in half public export diff --git a/libs/base/System.idr b/libs/base/System.idr index 8880e90b9..261f7638a 100644 --- a/libs/base/System.idr +++ b/libs/base/System.idr @@ -1,6 +1,6 @@ module System -import Data.So +import public Data.So import Data.List import Data.Strings diff --git a/libs/contrib/Data/String/Extra.idr b/libs/contrib/Data/String/Extra.idr index a3d9c63a7..e2f815a3d 100644 --- a/libs/contrib/Data/String/Extra.idr +++ b/libs/contrib/Data/String/Extra.idr @@ -1,5 +1,7 @@ module Data.String.Extra +import Data.List +import Data.Nat import Data.Strings %default total diff --git a/libs/contrib/Language/JSON/String/Lexer.idr b/libs/contrib/Language/JSON/String/Lexer.idr index 282c97236..9778c78b0 100644 --- a/libs/contrib/Language/JSON/String/Lexer.idr +++ b/libs/contrib/Language/JSON/String/Lexer.idr @@ -1,5 +1,6 @@ module Language.JSON.String.Lexer +import Data.Nat import Language.JSON.String.Tokens import Text.Lexer diff --git a/libs/contrib/System/Path.idr b/libs/contrib/System/Path.idr index 70f4b3956..2122a0927 100644 --- a/libs/contrib/System/Path.idr +++ b/libs/contrib/System/Path.idr @@ -1,7 +1,9 @@ module System.Path +import Control.Delayed import Data.List import Data.Maybe +import Data.Nat import Data.Strings import Data.String.Extra import System.Info diff --git a/src/Compiler/Scheme/Chez.idr b/src/Compiler/Scheme/Chez.idr index a123772e7..d1522d828 100644 --- a/src/Compiler/Scheme/Chez.idr +++ b/src/Compiler/Scheme/Chez.idr @@ -17,7 +17,10 @@ import Data.Maybe import Data.NameMap import Data.Strings import Data.Vect + import System +import System.Directory +import System.File import System.Info %default covering diff --git a/src/Compiler/Scheme/Gambit.idr b/src/Compiler/Scheme/Gambit.idr index 505f0735f..67f6a76a3 100644 --- a/src/Compiler/Scheme/Gambit.idr +++ b/src/Compiler/Scheme/Gambit.idr @@ -17,7 +17,10 @@ import Data.Maybe import Data.NameMap import Data.Strings import Data.Vect + import System +import System.Directory +import System.File import System.Info %default covering diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 7fa6a6a01..6f36b5091 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -18,7 +18,10 @@ import Data.NameMap import Data.Nat import Data.Strings import Data.Vect + import System +import System.Directory +import System.File import System.Info %default covering diff --git a/src/Core/Binary.idr b/src/Core/Binary.idr index 0bd1ded30..f746893c2 100644 --- a/src/Core/Binary.idr +++ b/src/Core/Binary.idr @@ -13,6 +13,8 @@ import Data.IntMap import Data.List import Data.NameMap +import System.File + -- Reading and writing 'Defs' from/to a binary file -- In order to be saved, a name must have been flagged using 'toSave'. -- (Otherwise we'd save out everything, not just the things in the current @@ -322,7 +324,11 @@ addTypeHint fc (tyn, hintn, d) addAutoHint : {auto c : Ref Ctxt Defs} -> (Name, Bool) -> Core () -addAutoHint (hintn, d) = addGlobalHint hintn d +addAutoHint (hintn_in, d) + = do defs <- get Ctxt + hintn <- toResolvedNames hintn_in + + put Ctxt (record { autoHints $= insert hintn d } defs) export updatePair : {auto c : Ref Ctxt Defs} -> @@ -400,13 +406,15 @@ export readFromTTC : TTC extra => {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> - FC -> Bool -> + Bool -> -- set nested namespaces (for records, to use at the REPL) + FC -> + Bool -> -- importing as public (fname : String) -> -- file containing the module (modNS : List String) -> -- module namespace (importAs : List String) -> -- namespace to import as Core (Maybe (extra, Int, List (List String, Bool, List String))) -readFromTTC loc reexp fname modNS importAs +readFromTTC nestedns loc reexp fname modNS importAs = do defs <- get Ctxt -- If it's already in the context, with the same visibility flag, -- don't load it again (we do need to load it again if it's visible @@ -434,7 +442,7 @@ readFromTTC loc reexp fname modNS importAs traverse (addGlobalDef modNS as) (context ttc) traverse_ addUserHole (userHoles ttc) setNS (currentNS ttc) - setNestedNS (nestedNS ttc) + when nestedns $ setNestedNS (nestedNS ttc) -- Set up typeHints and autoHints based on the loaded data traverse_ (addTypeHint loc) (typeHints ttc) traverse_ addAutoHint (autoHints ttc) diff --git a/src/Core/Core.idr b/src/Core/Core.idr index f505d2fe4..217281797 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -8,6 +8,7 @@ import Parser.Source import public Data.IORef import System +import System.File %default covering diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 331e6ff80..b3f9f3d46 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -330,6 +330,13 @@ mutual pure (App fc f' aerased, glueBack defs env sc', fused ++ aused) + NApp _ (NRef _ n) _ => + do Just _ <- lookupCtxtExact n (gamma defs) + | _ => throw (UndefinedName fc n) + tfty <- getTerm gfty + throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++ + " (" ++ show tfty ++ " not a function type)")) + _ => do tfty <- getTerm gfty throw (GenericMsg fc ("Linearity checking failed on " ++ show f' ++ " (" ++ show tfty ++ " not a function type)")) @@ -567,14 +574,14 @@ mutual lcheckDef fc rig True env n = do defs <- get Ctxt Just def <- lookupCtxtExact n (gamma defs) - | Nothing => throw (InternalError ("Linearity checking failed on " ++ show n)) + | Nothing => throw (UndefinedName fc n) pure (type def) lcheckDef fc rig False env n = do defs <- get Ctxt let Just idx = getNameID n (gamma defs) - | Nothing => throw (InternalError ("Linearity checking failed on " ++ show n)) + | Nothing => throw (UndefinedName fc n) Just def <- lookupCtxtExact (Resolved idx) (gamma defs) - | Nothing => throw (InternalError ("Linearity checking failed on " ++ show n)) + | Nothing => throw (UndefinedName fc n) rigSafe (multiplicity def) rig if linearChecked def then pure (type def) diff --git a/src/Core/Metadata.idr b/src/Core/Metadata.idr index 26d8afbc5..8192c7875 100644 --- a/src/Core/Metadata.idr +++ b/src/Core/Metadata.idr @@ -13,6 +13,8 @@ import Data.List import Utils.Binary +import System.File + -- Additional data we keep about the context to support interactive editing public export diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index 3d6aa8041..334e390b5 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -788,7 +788,7 @@ export TTC Def where toBuf b None = tag 0 toBuf b (PMDef pi args ct rt pats) - = do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b rt; toBuf b pats + = do tag 1; toBuf b pi; toBuf b args; toBuf b ct; toBuf b pats toBuf b (ExternDef a) = do tag 2; toBuf b a toBuf b (ForeignDef a cs) @@ -815,9 +815,8 @@ TTC Def where 1 => do pi <- fromBuf b args <- fromBuf b ct <- fromBuf b - rt <- fromBuf b pats <- fromBuf b - pure (PMDef pi args ct rt pats) + pure (PMDef pi args ct (Unmatched "") pats) 2 => do a <- fromBuf b pure (ExternDef a) 3 => do a <- fromBuf b diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 2b2d0926e..37e16fa08 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -230,6 +230,11 @@ postpone blockedMetas loc mode logstr env x y yq <- quote defs env y pure (logstr ++ ": " ++ show !(toFullNames xq) ++ " =?= " ++ show !(toFullNames yq)) + + -- If we're blocked because a name is undefined, give up + checkDefined defs x + checkDefined defs y + xtm <- quote empty env x ytm <- quote empty env y -- Need to find all the metas in the constraint since solving any one @@ -249,6 +254,13 @@ postpone blockedMetas loc mode logstr env x y logTerm 10 "Y" ytm pure (constrain c) where + checkDefined : Defs -> NF vars -> Core () + checkDefined defs (NApp _ (NRef _ n) _) + = do Just _ <- lookupCtxtExact n (gamma defs) + | _ => throw (UndefinedName loc n) + pure () + checkDefined _ _ = pure () + undefinedN : Name -> Core Bool undefinedN n = do defs <- get Ctxt @@ -567,11 +579,11 @@ solveIfUndefined env metavar soln = pure False isDefInvertible : {auto c : Ref Ctxt Defs} -> - Int -> Core Bool -isDefInvertible i + FC -> Int -> Core Bool +isDefInvertible fc i = do defs <- get Ctxt Just gdef <- lookupCtxtExact (Resolved i) (gamma defs) - | Nothing => pure False + | Nothing => throw (UndefinedName fc (Resolved i)) pure (invertible gdef) mutual @@ -906,7 +918,7 @@ mutual (NApp yfc (NLocal yr y yp) yargs) -- If they're both holes, solve the one with the bigger context unifyBothApps mode loc env xfc (NMeta xn xi xargs) xargs' yfc (NMeta yn yi yargs) yargs' - = do invx <- isDefInvertible xi + = do invx <- isDefInvertible loc xi if xi == yi && (invx || umode mode == InSearch) -- Invertible, (from auto implicit search) -- so we can also unify the arguments. diff --git a/src/Data/ANameMap.idr b/src/Data/ANameMap.idr index 193d5617b..3a0f650e8 100644 --- a/src/Data/ANameMap.idr +++ b/src/Data/ANameMap.idr @@ -2,6 +2,8 @@ module Data.ANameMap import Core.Name + +import Data.List import Data.NameMap import Data.StringMap diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index de99e0a4f..7827541e1 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -12,6 +12,7 @@ import Idris.Syntax import Parser.Source import Data.List +import System.File %default covering diff --git a/src/Idris/IDEMode/REPL.idr b/src/Idris/IDEMode/REPL.idr index 7084c715c..f48cfb910 100644 --- a/src/Idris/IDEMode/REPL.idr +++ b/src/Idris/IDEMode/REPL.idr @@ -15,6 +15,8 @@ import Core.Options import Core.TT import Core.Unify +import Data.So + import Idris.Desugar import Idris.Error import Idris.ModTree @@ -24,8 +26,9 @@ import Idris.REPL import Idris.Syntax import Idris.Version -import Idris.IDEMode.Parser import Idris.IDEMode.Commands +import Idris.IDEMode.Holes +import Idris.IDEMode.Parser import Idris.IDEMode.SyntaxHighlight import TTImp.Interactive.CaseSplit @@ -37,6 +40,7 @@ import Utils.Hex import Data.List import System +import System.File import Network.Socket import Network.Socket.Data diff --git a/src/Idris/Main.idr b/src/Idris/Main.idr index ef8030744..4dacaa97b 100644 --- a/src/Idris/Main.idr +++ b/src/Idris/Main.idr @@ -22,9 +22,12 @@ import Idris.Syntax import Idris.Version import Data.List +import Data.So import Data.Strings import Data.Vect import System +import System.Directory +import System.File import Yaffle.Main @@ -171,7 +174,7 @@ stMain opts the (Core ()) $ case fname of Nothing => logTime "Loading prelude" $ when (not $ noprelude session) $ - readPrelude + readPrelude True Just f => logTime "Loading main file" $ (loadMainFile f >>= displayErrors) diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index afb4e7c87..58c98c263 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -11,6 +11,7 @@ import Core.Unify import Data.List import Data.Maybe +import Data.So import Data.StringMap import Data.Strings import Data.StringTrie @@ -18,6 +19,9 @@ import Data.These import Parser.Package import System +import System.Directory +import System.File + import Text.Parser import Utils.Binary import Utils.String diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index e150da538..3441c98d1 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -57,20 +57,20 @@ processDecls decls readModule : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> - (top : Bool) -> + (full : Bool) -> -- load everything transitively (needed for REPL and compiling) FC -> (visible : Bool) -> -- Is import visible to top level module? (reexp : Bool) -> -- Should the module be reexported? (imp : List String) -> -- Module name to import (as : List String) -> -- Namespace to import into Core () -readModule top loc vis reexp imp as +readModule full loc vis reexp imp as = do defs <- get Ctxt let False = (imp, vis, as) `elem` map snd (allImported defs) | True => when vis (setVisible imp) Right fname <- nsToPath loc imp | Left err => throw err - Just (syn, hash, more) <- readFromTTC {extra = SyntaxInfo} + Just (syn, hash, more) <- readFromTTC False {extra = SyntaxInfo} loc vis fname imp as | Nothing => when vis (setVisible imp) -- already loaded, just set visibility extendAs imp as syn @@ -82,15 +82,15 @@ readModule top loc vis reexp imp as do let m = fst mimp let reexp = fst (snd mimp) let as = snd (snd mimp) - readModule False loc (vis && reexp) reexp m as) more + when (reexp || full) $ readModule full loc (vis && reexp) reexp m as) more setNS modNS readImport : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> - Import -> Core () -readImport imp - = do readModule True (loc imp) True (reexport imp) (path imp) (nameAs imp) + Bool -> Import -> Core () +readImport full imp + = do readModule full (loc imp) True (reexport imp) (path imp) (nameAs imp) addImported (path imp, reexport imp, nameAs imp) readHash : {auto c : Ref Ctxt Defs} -> @@ -115,9 +115,10 @@ export readPrelude : {auto c : Ref Ctxt Defs} -> {auto u : Ref UST UState} -> {auto s : Ref Syn SyntaxInfo} -> - Core () -readPrelude = do readImport prelude - setNS ["Main"] + Bool -> Core () +readPrelude full + = do readImport full prelude + setNS ["Main"] -- Import a TTC for use as the main file (e.g. at the REPL) export @@ -127,7 +128,7 @@ readAsMain : {auto c : Ref Ctxt Defs} -> (fname : String) -> Core () readAsMain fname = do Just (syn, _, more) <- readFromTTC {extra = SyntaxInfo} - toplevelFC True fname [] [] + True toplevelFC True fname [] [] | Nothing => throw (InternalError "Already loaded") replNS <- getNS replNestedNS <- getNestedNS @@ -139,13 +140,13 @@ readAsMain fname traverse_ (\ mimp => do let m = fst mimp let as = snd (snd mimp) - readModule False emptyFC True True m as + readModule True emptyFC True True m as addImported (m, True, as)) more -- also load the prelude, if required, so that we have access to it -- at the REPL. when (not (noprelude !getSession)) $ - readModule False emptyFC True True ["Prelude"] ["Prelude"] + readModule True emptyFC True True ["Prelude"] ["Prelude"] -- We're in the namespace from the first TTC, so use the next name -- from that for the fresh metavariable name generation @@ -271,7 +272,7 @@ processMod srcf ttcf msg sourcecode -- (also that we only build child dependencies if rebuilding -- changes the interface - will need to store a hash in .ttc!) logTime "Reading imports" $ - traverse_ readImport imps + traverse_ (readImport False) imps -- Before we process the source, make sure the "hide_everywhere" -- names are set to private (TODO, maybe if we want this?) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 5f17a203c..0b53af754 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -50,6 +50,7 @@ import Data.Stream import Data.Strings import System +import System.File %default covering diff --git a/src/Idris/SetOptions.idr b/src/Idris/SetOptions.idr index 81881b60a..a636dae93 100644 --- a/src/Idris/SetOptions.idr +++ b/src/Idris/SetOptions.idr @@ -13,6 +13,7 @@ import Idris.Version import IdrisPaths +import Data.So import System -- TODO: Version numbers on dependencies diff --git a/src/TTImp/ProcessType.idr b/src/TTImp/ProcessType.idr index faebc3fc9..f983452cc 100644 --- a/src/TTImp/ProcessType.idr +++ b/src/TTImp/ProcessType.idr @@ -298,6 +298,7 @@ processType {vars} eopts nest env fc rig vis opts (MkImpTy tfc n_in ty_raw) addTyDecl fc (Resolved idx) env ty -- for definition generation addNameType fc (Resolved idx) env ty -- for looking up types + traverse_ addToSave (keys (getMetas ty)) addToSave n log 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty)) diff --git a/src/Yaffle/Main.idr b/src/Yaffle/Main.idr index b7d981e51..2ddbc988c 100644 --- a/src/Yaffle/Main.idr +++ b/src/Yaffle/Main.idr @@ -21,6 +21,7 @@ import TTImp.TTImp import Yaffle.REPL import Data.List +import Data.So import Data.Strings import System @@ -51,7 +52,7 @@ yaffleMain fname args addPrimitives case span (/= '.') fname of (_, ".ttc") => do coreLift $ putStrLn "Processing as TTC" - readFromTTC {extra = ()} emptyFC True fname [] [] + readFromTTC {extra = ()} True emptyFC True fname [] [] coreLift $ putStrLn "Read TTC" _ => do coreLift $ putStrLn "Processing as TTImp" ok <- processTTImpFile fname diff --git a/tests/idris2/coverage005/Cover.idr b/tests/idris2/coverage005/Cover.idr index d4e53ab4c..276141128 100644 --- a/tests/idris2/coverage005/Cover.idr +++ b/tests/idris2/coverage005/Cover.idr @@ -1,4 +1,5 @@ import Data.Fin +import Data.Maybe data NNat = NZ | NS NNat diff --git a/tests/idris2/import002/expected b/tests/idris2/import002/expected index 94a14a223..55ed33367 100644 --- a/tests/idris2/import002/expected +++ b/tests/idris2/import002/expected @@ -2,6 +2,6 @@ 2/3: Building Mult (Mult.idr) 3/3: Building Test (Test.idr) Test.idr:5:9--5:13:While processing type of thing at Test.idr:5:1--6:1: -Name Nat.Nat is inaccessible since Nat is not explicitly imported +Undefined name Nat Test.idr:6:1--8:1:No type declaration for Test.thing Test> Bye for now! diff --git a/tests/idris2/reg003/expected b/tests/idris2/reg003/expected index a66d0ed01..73cb02d37 100644 --- a/tests/idris2/reg003/expected +++ b/tests/idris2/reg003/expected @@ -1,11 +1,11 @@ 1/1: Building Holes (Holes.idr) Holes.idr:4:64--4:85:While processing type of Vect_ext at Holes.idr:4:1--7:1: -Name Builtin.~=~ is inaccessible since Builtin is not explicitly imported +Undefined name ~=~ Holes.idr:7:26--8:1:While processing type of Weird at Holes.idr:7:1--8:1: -Name Builtin.~=~ is inaccessible since Builtin is not explicitly imported +Undefined name ~=~ Holes.idr:8:1--10:1:No type declaration for Main.Weird Holes.idr:10:5--10:10:While processing type of f at Holes.idr:10:1--11:1: -Name Prelude.Bool is inaccessible since Prelude is not explicitly imported +Undefined name Bool Holes.idr:11:1--12:1:No type declaration for Main.f Main> (interactive):1:4--1:8:Undefined name help Main> (interactive):1:4--1:9:Undefined name hole0 diff --git a/tests/typedd-book/chapter14/Hangman.idr b/tests/typedd-book/chapter14/Hangman.idr index 0c8c0240b..986e3b234 100644 --- a/tests/typedd-book/chapter14/Hangman.idr +++ b/tests/typedd-book/chapter14/Hangman.idr @@ -2,6 +2,8 @@ import Data.Vect import Data.List import Data.Strings +import Decidable.Equality + %default total data GameState : Type where