Merge pull request #410 from edwinb/import-revise

A variety of namespace and import goodies

Author: edwinb

CHANGELOG.md

@@ -17,6 +17,11 @@ 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`.
+* `do` notation can now be qualified with a namespace
+   + `MyDo.do` opens a `do` block where the `>>=` operator used is `MyDo.(>>=)`
 
 Library changes:
 

bootstrap/idris2_app/idris2.rkt

@@ -272,6 +272,23 @@ are both available, or return ``Nothing`` if one or both are not ("fail fast").
     Main> m_add (Just 82) Nothing
     Nothing
 
+The translation of ``do`` notation is entirely syntactic, so there is no
+need for the ``(>>=)`` operator to be the operator defined in the ``Monad``
+interface. Idris will, in general, try to disambiguate which ``(>>=)`` you
+mean by type, but you can explicitly choose with qualified do notation,
+for example:
+
+.. code-block:: idris
+
+    m_add : Maybe Int -> Maybe Int -> Maybe Int
+    m_add x y = Prelude.do
+                   x' <- x -- Extract value from x
+                   y' <- y -- Extract value from y
+                   pure (x' + y') -- Add them
+
+The ``Prelude.do`` means that Idris will use the ``(>>=)`` operator defined
+in the ``Prelude``.
+
 Pattern Matching Bind
 ~~~~~~~~~~~~~~~~~~~~~
 

bootstrap/idris2_app/idris2.ss

@@ -179,6 +179,35 @@ The module ``A`` will export the name ``a``, as well as any public or
 abstract names in module ``C``, but will not re-export anything from
 module ``B``.
 
+Renaming imports
+----------------
+
+Sometimes it is convenient to be able to access the names in another module
+via a different namespace (typically, a shorter one). For this, you can
+use `import...as`. For example:
+
+::
+
+    module A
+
+    import Data.List as L
+
+This module ``A`` has access to the exported names from module ``Data.List``,
+but can also explicitly access them via the module name ``L``. ``import...as``
+can also be combined with ``import public`` to create a module which exports
+a larger API from other sub-modules:
+
+::
+
+    module Books
+
+    import Books.Hardback as Books
+    import Books.Comic as Books
+
+Here, any module which imports ``Books`` will have access to the exported
+interfaces of ``Books.Hardback`` and ``Books.Comic`` both under the namespace
+``Books``.
+
 Explicit Namespaces
 ===================
 

docs/source/tutorial/interfaces.rst

@@ -2,8 +2,8 @@ module Prelude
 
 import public Builtin
 import public PrimIO
-import public Prelude.Basics
-import public Prelude.Uninhabited
+import public Prelude.Basics as Prelude
+import public Prelude.Uninhabited as Prelude
 
 %default total
 

docs/source/tutorial/modules.rst

@@ -162,14 +162,6 @@ HasNames e => HasNames (TTCFile e) where
       resolvedPrim gam (MkPrimNs mi ms mc)
           = pure $ MkPrimNs !(resolved gam mi) !(resolved gam ms) !(resolved gam mc)
 
-
-asName : List String -> Maybe (List String) -> Name -> Name
-asName mod (Just ns) (NS oldns n)
-    = if mod == oldns
-         then NS ns n -- TODO: What about if there are nested namespaces in a module?
-         else NS oldns n
-asName _ _ n = n
-
 -- NOTE: TTC files are only compatible if the version number is the same,
 -- *and* the 'annot/extra' type are the same, or there are no holes/constraints
 writeTTCFile : (HasNames extra, TTC extra) =>
@@ -284,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
@@ -295,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
@@ -429,23 +424,26 @@ readFromTTC nestedns loc reexp fname modNS importAs
          -- interested in is returning which other modules to load.
          -- Otherwise, add the data
          let ex = extraData ttc
-         if ((modNS, importAs) `elem` map getNSas (allImported defs))
+         if alreadyDone modNS importAs (allImported defs)
             then pure (Just (ex, ifaceHash ttc, imported ttc))
             else do
                traverse (addGlobalDef modNS as) (context ttc)
                traverse_ addUserHole (userHoles ttc)
                setNS (currentNS ttc)
                when nestedns $ setNestedNS (nestedNS ttc)
+               -- Only do the next batch if the module hasn't been loaded
+               -- in any form
+               when (not (modNS `elem` map (fst . getNSas) (allImported defs))) $
                -- Set up typeHints and autoHints based on the loaded data
-               traverse_ (addTypeHint loc) (typeHints ttc)
-               traverse_ addAutoHint (autoHints ttc)
-               -- Set up pair/rewrite etc names
-               updatePair (pairnames ttc)
-               updateRewrite (rewritenames ttc)
-               updatePrims (primnames ttc)
-               updateNameDirectives (reverse (namedirectives ttc))
-               updateCGDirectives (cgdirectives ttc)
-               updateTransforms (transforms ttc)
+                 do traverse_ (addTypeHint loc) (typeHints ttc)
+                    traverse_ addAutoHint (autoHints ttc)
+                    -- Set up pair/rewrite etc names
+                    updatePair (pairnames ttc)
+                    updateRewrite (rewritenames ttc)
+                    updatePrims (primnames ttc)
+                    updateNameDirectives (reverse (namedirectives ttc))
+                    updateCGDirectives (cgdirectives ttc)
+                    updateTransforms (transforms ttc)
 
                when (not reexp) clearSavedHints
                resetFirstEntry
@@ -455,6 +453,19 @@ readFromTTC nestedns loc reexp fname modNS importAs
                ust <- get UST
                put UST (record { nextName = nextVar ttc } ust)
                pure (Just (ex, ifaceHash ttc, imported ttc))
+  where
+    alreadyDone : List String -> List String ->
+                  List (String, (List String, Bool, List String)) ->
+                  Bool
+    alreadyDone modns importAs [] = False
+    -- If we've already imported 'modns' as 'importAs', or we're importing
+    -- 'modns' as itself and it's already imported as anything, then no
+    -- need to load again.
+    alreadyDone modns importAs ((_, (m, _, a)) :: rest)
+        = if ((modns == m && importAs == a) ||
+              (modns == m && modns == importAs))
+             then True
+             else alreadyDone modns importAs rest
 
 getImportHashes : String -> Ref Bin Binary ->
                   Core (List (List String, Int))

libs/prelude/Prelude.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
@@ -327,6 +333,7 @@ record Context where
     allPublic : Bool -- treat everything as public. This is only intended
                      -- for checking partially evaluated definitions
     inlineOnly : Bool -- only return things with the 'alwaysReduce' flag
+    hidden : NameMap () -- Never return these
 
 export
 getContent : Context -> Ref Arr (IOArray ContextEntry)
@@ -348,21 +355,31 @@ initCtxtS : Int -> Core Context
 initCtxtS s
     = do arr <- coreLift $ newArray s
          aref <- newRef Arr arr
-         pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False)
+         pure (MkContext 0 0 empty empty aref 0 empty [["_PE"]] False False empty)
 
 export
 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 +407,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 +520,41 @@ 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)
+       = case lookup fulln (hidden ctxt) of
+              Nothing =>
+                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 ps
+    lookupPossibles acc (Alias asn fulln i :: ps)
+       = case lookup fulln (hidden ctxt) of
+              Nothing =>
+                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
+              _ => lookupPossibles acc ps
+
+hideName : Name -> Context -> Context
+hideName n ctxt = record { hidden $= insert n () } ctxt
 
 branchCtxt : Context -> Core Context
 branchCtxt ctxt = pure (record { branchDepth $= S } ctxt)
@@ -918,6 +954,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 +1060,16 @@ 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
+         Nothing <- lookupCtxtExact alias (gamma defs)
+             | _ => pure () -- Don't add the alias if the name exists already
+         gam' <- newAlias alias full (gamma defs)
+         put Ctxt (record { gamma = gam' } defs)
+
 export
 addBuiltin : {arity : _} ->
              {auto x : Ref Ctxt Defs} ->
@@ -1347,7 +1425,7 @@ hide fc n
          [(nsn, _)] <- lookupCtxtName n (gamma defs)
               | [] => throw (UndefinedName fc n)
               | res => throw (AmbiguousName fc (map fst res))
-         setVisibility fc nsn Private
+         put Ctxt (record { gamma $= hideName nsn } defs)
 
 export
 getVisibility : {auto c : Ref Ctxt Defs} ->