Merge pull request #177 from edwinb/fix-imports

Fix import loading

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
 

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) ->

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

libs/base/System.idr

@@ -1,6 +1,6 @@
 module System
 
-import Data.So
+import public Data.So
 import Data.List
 import Data.Strings
 

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

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
 

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

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

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

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

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)

src/Core/Core.idr

@@ -8,6 +8,7 @@ import Parser.Source
 
 import public Data.IORef
 import System
+import System.File
 
 %default covering
 

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)

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

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

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
+                  FC -> Int -> Core Bool
-isDefInvertible i
+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.

src/Data/ANameMap.idr

@@ -2,6 +2,8 @@
 module Data.ANameMap
 
 import Core.Name
+
+import Data.List
 import Data.NameMap
 import Data.StringMap
 

src/Idris/Error.idr

@@ -12,6 +12,7 @@ import Idris.Syntax
 import Parser.Source
 
 import Data.List
+import System.File
 
 %default covering
 

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

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)
 

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

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 ()
+             Bool -> Import -> Core ()
-readImport imp
+readImport full imp
-    = do readModule True (loc imp) True (reexport imp) (path imp) (nameAs 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 ()
+              Bool -> Core ()
-readPrelude = do readImport prelude
+readPrelude full
-                 setNS ["Main"]
+    = 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?)

src/Idris/REPL.idr

@@ -50,6 +50,7 @@ import Data.Stream
 import Data.Strings
 
 import System
+import System.File
 
 %default covering
 

src/Idris/SetOptions.idr

@@ -13,6 +13,7 @@ import Idris.Version
 
 import IdrisPaths
 
+import Data.So
 import System
 
 -- TODO: Version numbers on dependencies

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))

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

tests/idris2/coverage005/Cover.idr

@@ -1,4 +1,5 @@
 import Data.Fin
+import Data.Maybe
 
 data NNat = NZ | NS NNat
 

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!

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

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