Add "import X as Y" properly

Instead of just the cursory name update that we used to do (which didn't
work properly anyway for a lot of reasons), now we add aliases for all
the names in the imported module.
So, like Idris 1, every global has a canonical name by which we can
refer to it, but it can also have aliases via "import ... as".

CHANGELOG.md

@@ -17,6 +17,9 @@ Language changes:
    + Implemented `%macro` function flag, to remove the syntactic noise of
      invoking elaborator scripts. This means the function must always
      be fully applied, and is run under `%runElab`
+* Add `import X as Y`
+   + This imports the module `X`, adding aliases for the definitions in
+     namespace `Y`, so they can be referred to as `Y`.
 
 Library changes:
 

src/Core/Binary.idr

@@ -276,7 +276,7 @@ writeToTTC extradata fname
 addGlobalDef : {auto c : Ref Ctxt Defs} ->
                (modns : List String) -> (importAs : Maybe (List String)) ->
                (Name, Binary) -> Core ()
-addGlobalDef modns as (n, def)
+addGlobalDef modns asm (n, def)
     = do defs <- get Ctxt
          codedentry <- lookupContextEntry n (gamma defs)
          -- Don't update the coded entry because some names might not be
@@ -287,8 +287,11 @@ addGlobalDef modns as (n, def)
                         codedentry
          if completeDef entry
             then pure ()
-            else do addContextEntry (asName modns as n) def
+            else do addContextEntry n def
                     pure ()
+         maybe (pure ())
+               (\as => addContextAlias (asName modns as n) n)
+               asm
   where
     -- If the definition already exists, don't overwrite it with an empty
     -- definition or hole. This might happen if a function is declared in one

src/Core/Context.idr

@@ -298,6 +298,12 @@ data ContextEntry : Type where
      Coded : Binary -> ContextEntry
      Decoded : GlobalDef -> ContextEntry
 
+data PossibleName : Type where
+     Direct : Name -> Int -> PossibleName -- full name and resolved name id
+     Alias : Name -> -- aliased name (from "import as")
+             Name -> Int -> -- real full name and resolved name, as above
+             PossibleName
+
 -- All the GlobalDefs. We can only have one context, because name references
 -- point at locations in here, and if we have more than one the indices won't
 -- match up. So, this isn't polymorphic.
@@ -309,7 +315,7 @@ record Context where
     -- Map from full name to its position in the context
     resolvedAs : NameMap Int
     -- Map from strings to all the possible names in all namespaces
-    possibles : StringMap (List (Name, Int))
+    possibles : StringMap (List PossibleName)
     -- Reference to the actual content, indexed by Int
     content : Ref Arr (IOArray ContextEntry)
     -- Branching depth, in a backtracking elaborator. 0 is top level; at lower
@@ -355,14 +361,24 @@ initCtxt : Core Context
 initCtxt = initCtxtS initSize
 
 addPossible : Name -> Int ->
-              StringMap (List (Name, Int)) -> StringMap (List (Name, Int))
+              StringMap (List PossibleName) -> StringMap (List PossibleName)
 addPossible n i ps
     = case userNameRoot n of
            Nothing => ps
            Just nr =>
               case lookup nr ps of
-                   Nothing => insert nr [(n, i)] ps
-                   Just nis => insert nr ((n, i) :: nis) ps
+                   Nothing => insert nr [Direct n i] ps
+                   Just nis => insert nr (Direct n i :: nis) ps
+
+addAlias : Name -> Name -> Int ->
+           StringMap (List PossibleName) -> StringMap (List PossibleName)
+addAlias alias full i ps
+    = case userNameRoot alias of
+           Nothing => ps
+           Just nr =>
+              case lookup nr ps of
+                   Nothing => insert nr [Alias alias full i] ps
+                   Just nis => insert nr (Alias alias full i :: nis) ps
 
 export
 newEntry : Name -> Context -> Core (Int, Context)
@@ -390,6 +406,11 @@ getPosition n ctxt
               do pure (idx, ctxt)
            Nothing => newEntry n ctxt
 
+newAlias : Name -> Name -> Context -> Core Context
+newAlias alias full ctxt
+    = do (idx, ctxt) <- getPosition full ctxt
+         pure $ record { possibles $= addAlias alias full idx } ctxt
+
 export
 getNameID : Name -> Context -> Maybe Int
 getNameID (Resolved idx) ctxt = Just idx
@@ -498,27 +519,32 @@ lookupCtxtName n ctxt
            Just r =>
               do let Just ps = lookup r (possibles ctxt)
                       | Nothing => pure []
-                 ps' <- the (Core (List (Maybe (Name, Int, GlobalDef)))) $
-                           traverse (\ (n, i) =>
-                                    do Just res <- lookupCtxtExact (Resolved i) ctxt
-                                            | _ => pure Nothing
-                                       pure (Just (n, i, res))) ps
-                 getMatches ps'
+                 lookupPossibles [] ps
   where
-    matches : Name -> (Name, Int, a) -> Bool
-    matches (NS ns _) (NS cns _, _, _) = ns `isPrefixOf` cns
+    matches : Name -> Name -> Bool
+    matches (NS ns _) (NS cns _) = ns `isPrefixOf` cns
     matches (NS _ _) _ = True -- no in library name, so root doesn't match
     matches _ _ = True -- no prefix, so root must match, so good
 
-    getMatches : List (Maybe (Name, Int, GlobalDef)) ->
-                 Core (List (Name, Int, GlobalDef))
-    getMatches [] = pure []
-    getMatches (Nothing :: rs) = getMatches rs
-    getMatches (Just r :: rs)
-        = if matches n r
-             then do rs' <- getMatches rs
-                     pure (r :: rs')
-             else getMatches rs
+    resn : (Name, Int, GlobalDef) -> Int
+    resn (_, i, _) = i
+
+    lookupPossibles : List (Name, Int, GlobalDef) -> -- accumulator
+                      List PossibleName ->
+                      Core (List (Name, Int, GlobalDef))
+    lookupPossibles acc [] = pure (reverse acc)
+    lookupPossibles acc (Direct fulln i :: ps)
+       = do Just res <- lookupCtxtExact (Resolved i) ctxt
+                 | Nothing => lookupPossibles acc ps
+            if (matches n fulln) && not (i `elem` map resn acc)
+               then lookupPossibles ((fulln, i, res) :: acc) ps
+               else lookupPossibles acc ps
+    lookupPossibles acc (Alias asn fulln i :: ps)
+       = do Just res <- lookupCtxtExact (Resolved i) ctxt
+                 | Nothing => lookupPossibles acc ps
+            if (matches n asn) && not (i `elem` map resn acc)
+               then lookupPossibles ((fulln, i, res) :: acc) ps
+               else lookupPossibles acc ps
 
 branchCtxt : Context -> Core Context
 branchCtxt ctxt = pure (record { branchDepth $= S } ctxt)
@@ -918,6 +944,38 @@ clearCtxt
     resetElab : Options -> Options
     resetElab = record { elabDirectives = defaultElab }
 
+-- Get the canonical name of something that might have been aliased via
+-- import as
+export
+canonicalName : {auto c : Ref Ctxt Defs} ->
+                FC -> Name -> Core Name
+canonicalName fc n
+    = do defs <- get Ctxt
+         case !(lookupCtxtName n (gamma defs)) of
+              [] => throw (UndefinedName fc n)
+              [(n, _, _)] => pure n
+              ns => throw (AmbiguousName fc (map fst ns))
+
+-- If the name is aliased, get the alias
+export
+aliasName : {auto c : Ref Ctxt Defs} ->
+            Name -> Core Name
+aliasName fulln
+    = do defs <- get Ctxt
+         let Just r = userNameRoot fulln
+                | Nothing => pure fulln
+         let Just ps = lookup r (possibles (gamma defs))
+                | Nothing => pure fulln
+         findAlias ps
+  where
+    findAlias : List PossibleName -> Core Name
+    findAlias [] = pure fulln
+    findAlias (Alias as full i :: ps)
+        = if full == fulln
+             then pure as
+             else findAlias ps
+    findAlias (_ :: ps) = findAlias ps
+
 -- Beware: if your hashable thing contains (potentially resolved) names,
 -- it'll be better to use addHashWithNames to make the hash independent
 -- of the internal numbering of names.
@@ -992,6 +1050,14 @@ addContextEntry n def
          put Ctxt (record { gamma = gam' } defs)
          pure idx
 
+export
+addContextAlias : {auto c : Ref Ctxt Defs} ->
+                  Name -> Name -> Core ()
+addContextAlias alias full
+    = do defs <- get Ctxt
+         gam' <- newAlias alias full (gamma defs)
+         put Ctxt (record { gamma = gam' } defs)
+
 export
 addBuiltin : {arity : _} ->
              {auto x : Ref Ctxt Defs} ->

src/Core/Name.idr

@@ -21,11 +21,11 @@ data Name : Type where
 -- Update a name imported with 'import as', for creating an alias
 export
 asName : List String -> -- Initial module name
-         Maybe (List String) -> -- 'as' module name
+         List String -> -- 'as' module name
          Name -> -- identifier
          Name
-asName mod (Just ns) (DN s n) = DN s (asName mod (Just ns) n)
-asName mod (Just ns) (NS oldns n)
+asName mod ns (DN s n) = DN s (asName mod ns n)
+asName mod ns (NS oldns n)
     = NS (updateNS mod oldns) n
   where
     updateNS : List String -> List String -> List String

src/Data/ANameMap.idr

@@ -83,27 +83,14 @@ fromList = fromList' empty
     fromList' acc [] = acc
     fromList' acc ((k, v) :: ns) = fromList' (addName k v acc) ns
 
--- Merge two contexts, with entries in the second overriding entries in
--- the first
+-- Merge two contexts, with entries in the first overriding entries in
+-- the second
 export
 merge : ANameMap a -> ANameMap a -> ANameMap a
-merge ctxt (MkANameMap exact hier)
+merge (MkANameMap exact hier) ctxt
     = insertFrom (toList exact) ctxt
   where
     insertFrom : List (Name, a) -> ANameMap a -> ANameMap a
     insertFrom [] ctxt = ctxt
     insertFrom ((n, val) :: cs) ctxt
         = insertFrom cs (addName n val ctxt)
-
-export
-mergeAs : List String -> List String ->
-          ANameMap a -> ANameMap a -> ANameMap a
-mergeAs oldns newns ctxt (MkANameMap exact hier)
-    = insertFrom (toList exact) ctxt
-  where
-    insertFrom : List (Name, a) -> ANameMap a -> ANameMap a
-    insertFrom [] ctxt = ctxt
-    insertFrom ((n, val) :: cs) ctxt
-        = insertFrom cs (addName n val ctxt)
-
-

src/Idris/Desugar.idr

@@ -54,13 +54,13 @@ ifThenElse True t e = t
 ifThenElse False t e = e
 
 export
-extendAs : {auto s : Ref Syn SyntaxInfo} ->
-           List String -> List String -> SyntaxInfo -> Core ()
-extendAs old as newsyn
+extendSyn : {auto s : Ref Syn SyntaxInfo} ->
+            SyntaxInfo -> Core ()
+extendSyn newsyn
     = do syn <- get Syn
          put Syn (record { infixes $= mergeLeft (infixes newsyn),
                            prefixes $= mergeLeft (prefixes newsyn),
-                           ifaces $= mergeAs old as (ifaces newsyn),
+                           ifaces $= merge (ifaces newsyn),
                            bracketholes $= ((bracketholes newsyn) ++) }
                   syn)
 

src/Idris/Elab/Implementation.idr

@@ -110,13 +110,17 @@ elabImplementation : {vars : _} ->
 elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nusing mbody
     = do let impName_in = maybe (mkImpl fc iname ps) id impln
          impName <- inCurrentNS impName_in
+         -- The interface name might be qualified, so check if it's an
+         -- alias for something
          syn <- get Syn
-         let [cndata] = lookupName iname (ifaces syn)
+         defs <- get Ctxt
+         inames <- lookupCtxtName iname (gamma defs)
+         let [cndata] = concatMap (\n => lookupName n (ifaces syn))
+                                  (map fst inames)
              | [] => throw (UndefinedName fc iname)
              | ns => throw (AmbiguousName fc (map fst ns))
          let cn : Name = fst cndata
          let cdata : IFaceInfo = snd cndata
-         defs <- get Ctxt
 
          Just ity <- lookupTyExact cn (gamma defs)
               | Nothing => throw (UndefinedName fc cn)

src/Idris/ProcessIdr.idr

@@ -75,7 +75,7 @@ readModule full loc vis reexp imp as
          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
+         extendSyn syn
 
          defs <- get Ctxt
          modNS <- getNS
@@ -140,7 +140,7 @@ readAsMain fname
               | Nothing => throw (InternalError "Already loaded")
          replNS <- getNS
          replNestedNS <- getNestedNS
-         extendAs replNS replNS syn
+         extendSyn syn
 
          -- Read the main file's top level imported modules, so we have access
          -- to their names (and any of their public imports)

src/Idris/REPL.idr

@@ -85,7 +85,7 @@ displayType : {auto c : Ref Ctxt Defs} ->
               Core String
 displayType defs (n, i, gdef)
     = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
-                pure (show (fullname gdef) ++ " : " ++ show tm))
+                pure (show !(aliasName (fullname gdef)) ++ " : " ++ show tm))
             (\num => showHole defs [] n num (type gdef))
             (isHole gdef)
 

src/TTImp/Unelab.idr

@@ -142,7 +142,7 @@ mutual
                | Nothing => case umode of
                                  ImplicitHoles => pure (Implicit fc True, gErased fc)
                                  _ => pure (IVar fc n, gErased fc)
-           pure (IVar fc !(getFullName n), gnf env (embed ty))
+           pure (IVar fc !(aliasName !(getFullName n)), gnf env (embed ty))
   unelabTy' umode env (Meta fc n i args)
       = do defs <- get Ctxt
            let mkn = nameRoot n

tests/Main.idr

@@ -49,7 +49,7 @@ idrisTests
        "error006", "error007", "error008", "error009", "error010",
        "error011",
        -- Modules and imports
-       "import001", "import002", "import003", "import004",
+       "import001", "import002", "import003", "import004", "import005",
        -- Interactive editing support
        "interactive001", "interactive002", "interactive003", "interactive004",
        "interactive005", "interactive006", "interactive007", "interactive008",

tests/idris2/import005/As.idr

@@ -0,0 +1,7 @@
+module As
+
+import Test as Toast
+
+Toast.Needle Int where
+  nardle x = x + x
+  noo x = x * x

tests/idris2/import005/Test.idr

@@ -0,0 +1,23 @@
+module Test
+
+export
+pythag : Int -> List (Int, Int, Int)
+pythag max
+    = [ (x,y,z) | z <- [1..max],
+                  y <- [1..z],
+                  x <- [1..y],
+                  
+                  x * x + y * y == z * z ]
+
+namespace Inside
+  -- Needs to be recursive (or at least refer to a name in this module)
+  -- to check that definitions are updated on import...as
+  export
+  fact : Nat -> Nat
+  fact Z = 1
+  fact (S k) = (S k) * fact k
+
+public export
+interface Needle a where
+  nardle : a -> a
+  noo : a -> a

tests/idris2/import005/expected

@@ -0,0 +1,12 @@
+1/2: Building Test (Test.idr)
+2/2: Building As (As.idr)
+As> Toast.pythag : Int -> List (Int, (Int, Int))
+As> Toast.Inside.fact : Nat -> Nat
+As> Toast.nardle : Needle a => a -> a
+As> Toast.noo : Needle a => a -> a
+As> 16
+As> [(3, (4, 5)), (6, (8, 10))]
+As> pythag
+As> 24
+As> 24
+As> Bye for now!

tests/idris2/import005/input

@@ -0,0 +1,10 @@
+:t pythag
+:t fact
+:t nardle
+:t noo
+Toast.nardle (the Int 8)
+Toast.pythag 10
+Test.pythag
+Toast.Inside.fact 4
+Test.Inside.fact 4
+:q

tests/idris2/import005/run

@@ -0,0 +1,3 @@
+$1 --no-banner As.idr < input
+
+rm -rf build