content: {- |
  
  This module deals with imports of nested modules (@import submodule@).
  This is more complex than it might seem at first because to resolve a
  declaration like @import submodule X@ we need to resolve what @X@
  referes to before we know what it will import.
  
  Even triciker is the case for functor instantiations:
  
    module M = F { X }
    import M
  
  In this case, even if we know what `M` referes to, we first need to
  resolve `F`, so that we can generate the instantiation and generate
  fresh names for names defined by `M`.
  
  If we want to support applicative semantics, then before instantiation
  `M` we also need to resolve `X` so that we know if this instantiation has
  already been generated.
  
  An overall guiding principle of the design is that we assume that declarations
  can be ordered in dependency order, and submodules can be processed one
  at a time. In particular, this does not allow recursion across modules,
  or functor instantiations depending on their arguments.
  
  Thus, the following is OK:
  
  module A where
    x = 0x2
  
    submodule B where
      y = x
  
    z = B::y
  
  
  However, this is not OK:
  
    submodule A = F X
    submodule F where
      import A
  -}
  
  {-# Language BlockArguments #-}
  {-# Language TypeSynonymInstances, FlexibleInstances #-}
  module Cryptol.ModuleSystem.Renamer.Imports
    ( resolveImports
    , ResolvedModule(..)
    , ModKind(..)
    , ResolvedLocal
    , ResolvedExt
    )
    where
  
  import Data.Maybe(fromMaybe)
  import Data.Set(Set)
  import qualified Data.Set as Set
  import Data.Map (Map)
  import qualified Data.Map as Map
  import Data.List(foldl')
  import Control.Monad(when)
  import qualified MonadLib as M
  
  
  import Cryptol.Utils.PP(pp)
  import Cryptol.Utils.Panic(panic)
  import Cryptol.Utils.Ident(ModName,ModPath(..),Namespace(..),OrigName(..))
  
  import Cryptol.Parser.Position(Located(..))
  import Cryptol.Parser.AST
    ( ImportG(..),PName, ModuleInstanceArgs(..), ImpName(..) )
  import Cryptol.ModuleSystem.Binds
            ( Mod(..), TopDef(..), modNested, ModKind(..), newFunctorInst )
  import Cryptol.ModuleSystem.Name
            ( Name, Supply, SupplyT, runSupplyT, asOrigName, nameIdent
            , nameTopModule )
  import Cryptol.ModuleSystem.Names(Names(..))
  import Cryptol.ModuleSystem.NamingEnv
            ( NamingEnv(..), lookupNS, shadowing, travNamingEnv
            , interpImportEnv, zipByTextName, filterUNames )
  
  
  {- | This represents a resolved module or signaure.
  The type parameter helps us distinguish between two types of resolved modules:
  
    1. Resolved modules that are *inputs* to the algorithm (i.e., they are
       defined outside the current module).  For such modules the type
       parameter is @imps@ is ()
  
    2. Resolved modules that are *outputs* of the algorithm (i.e., they
       are defined within the current module).  For such modules the type
       parameter @imps@ contains the naming environment for things
       that came in through the import.
  
  Note that signaures are never "imported", however we do need to keep them
  here so that signatures in a functor are properly instantiated when
  the functor is instantiated.
  -}
  data ResolvedModule imps = ResolvedModule
    { rmodDefines   :: NamingEnv    -- ^ Things defined by the module/signature.
    , rmodPublic    :: !(Set Name)  -- ^ Exported names
    , rmodKind      :: ModKind      -- ^ What sort of thing are we
    , rmodNested    :: Set Name     -- ^ Modules and signatures nested in this one
    , rmodImports   :: imps
      {- ^ Resolved imports. External modules need not specify this field,
      it is just part of the thing we compute for local modules. -}
    }
  
  
  -- | A resolved module that's defined in (or is) the current top-level module
  type ResolvedLocal = ResolvedModule NamingEnv
  
  -- | A resolved module that's not defined in the current top-level module
  type ResolvedExt   = ResolvedModule ()
  
  
  resolveImports ::
    (ImpName Name -> Mod ()) ->
    TopDef ->
    Supply ->
    (Map (ImpName Name) ResolvedLocal, Supply)
  resolveImports ext def su =
    case def of
  
      TopMod m mo ->
        do let cur  = todoModule mo
               newS = doModuleStep CurState
                                     { curMod = cur
                                     , curTop = m
                                     , externalModules = ext
                                     , doneModules = mempty
                                     , nameSupply = su
                                     , changes = False
                                     }
  
  
           case tryFinishCurMod cur newS of
             Just r  -> add m r newS
             Nothing -> add m r s1
                where (r,s1) = forceFinish newS
  
      TopInst m f as ->
        do let s = CurState
                     { curMod = ()
                     , curTop = m
                     , externalModules = ext
                     , doneModules = mempty
                     , nameSupply = su
                     , changes = False
                     }
  
           case tryInstanceMaybe s (ImpTop m) (f,as) of
             Just (r,newS) -> add m r newS
             Nothing -> (Map.singleton (ImpTop m) forceResolveInst, su)
  
    where
    toNest m = Map.fromList [ (ImpNested k, v) | (k,v) <- Map.toList m ]
    add m r s  = ( Map.insert (ImpTop m) r (toNest (doneModules s))
                 , nameSupply s
                 )
  
  
  
  
  --------------------------------------------------------------------------------
  
  
  -- | This keeps track of the current state of resolution of a module.
  type Todo = Mod ModState
  
  data ModState = ModState
    { modOuter        :: NamingEnv
      -- ^ Things which come in scope from outer modules
  
    , modImported     :: NamingEnv
      -- ^ Things which come in scope via imports.  These shadow outer names.
    }
  
  
  -- | Initial state of a module that needs processing.
  todoModule :: Mod () -> Todo
  todoModule = fmap (const emptyModState)
    where
    emptyModState =
      ModState
        { modOuter    = mempty
        , modImported = mempty
        }
  
  {- | A module is fully processed when we are done with all its:
  
    * submodule imports
    * instantiations
    * nested things (signatures and modules)
  -}
  isDone :: Todo -> Bool
  isDone m = null     (modImports m)   &&
             Map.null (modInstances m) &&
             Map.null (modMods m)
  
  
  -- | Finish up all unfinished modules as best as we can
  forceFinish :: CurState -> (ResolvedLocal,CurState)
  forceFinish s0 =
    let this  = curMod s0
        add k v s = s { doneModules = Map.insert k v (doneModules s) }
        s1        = foldl' (\s k -> add k forceResolveInst s) s0
                           (Map.keys (modInstances this))
  
        doNestMod s (k,m) =
          let (r,s') = forceFinish s { curMod = m }
          in add k r s'
  
    in ( forceResolveMod this
       , foldl' doNestMod s1 (Map.toList (modMods this))
       )
  
  
  -- | A place-holder entry for instnatitations we couldn't resolve.
  forceResolveInst :: ResolvedLocal
  forceResolveInst =
    ResolvedModule
      { rmodDefines = mempty
      , rmodPublic  = mempty
      , rmodKind    = AModule
      , rmodNested  = Set.empty
      , rmodImports = mempty
      }
  
  -- | Finish up unresolved modules as well as we can, in situations where
  -- the program contains an error.
  forceResolveMod :: Todo -> ResolvedLocal
  forceResolveMod todo =
    ResolvedModule
      { rmodDefines   = modDefines todo
      , rmodPublic    = modPublic todo
      , rmodKind      = modKind todo
      , rmodNested    = Map.keysSet (modMods todo)
      , rmodImports   = modImported (modState todo)
      }
  
  
  
  
  
  pushImport :: ImportG (ImpName PName) -> Todo -> Todo
  pushImport i m = m { modImports = i : modImports m }
  
  pushInst :: Name -> (ImpName PName, ModuleInstanceArgs PName) -> Todo -> Todo
  pushInst k v m = m { modInstances = Map.insert k v (modInstances m) }
  
  pushMod :: Name -> Todo -> Todo -> Todo
  pushMod k v m = m { modMods = Map.insert k v (modMods m) }
  
  updMS :: (ModState -> ModState) -> Todo -> Todo
  updMS f m = m { modState = f (modState m) }
  --------------------------------------------------------------------------------
  
  
  
  externalMod :: Mod () -> ResolvedExt
  externalMod m = ResolvedModule
    { rmodDefines  = modDefines m
    , rmodPublic   = modPublic m
    , rmodKind     = modKind m
    , rmodNested   = modNested m
    , rmodImports  = ()
    }
  
  {- | This is used when we need to use a local resolved module as an input
       to another module. -}
  forget :: ResolvedLocal -> ResolvedExt
  forget r = r { rmodImports = () }
  
  type CurState = CurState' Todo
  
  data CurState' a = CurState
    { curMod      :: a
      -- ^ This is what needs to be done
  
    , curTop      :: !ModName
      {- ^ The top-level module we are working on.  This does not change
         throught the algorithm, it is just convenient to pass it here with 
         all the other stuff. -}
  
    , externalModules :: ImpName Name -> Mod ()
      -- ^ Modules defined outside the current top-level modules
  
    , doneModules :: Map Name ResolvedLocal
      {- ^ Nested modules/signatures in the current top-level modules.
           These may be either defined locally, or be the result of
           instantiating a functor.  Note that the functor itself may be
           either local or external.
      -}
  
    , nameSupply :: Supply
      -- ^ Use this to instantiate functors
  
    , changes :: Bool
      -- ^ True if something changed on the last iteration
    }
  
  updCur :: CurState -> (Todo -> Todo) -> CurState
  updCur m f = m { curMod = f (curMod m) }
  
  updCurMS :: CurState -> (ModState -> ModState) -> CurState
  updCurMS s f = updCur s (updMS f)
  
  class HasCurScope a where
    curScope :: CurState' a -> NamingEnv
  
  instance HasCurScope () where
    curScope _ = mempty
  
  instance HasCurScope Todo where
    curScope s = modDefines m `shadowing` modImported ms `shadowing` modOuter ms
      where
      m   = curMod s
      ms  = modState m
  
  
  -- | Keep applying a transformation while things are changing
  doStep :: (CurState -> CurState) -> (CurState -> CurState)
  doStep f s0 = go (changes s0) s0
    where
    go ch s = let s1 = f s { changes = False }
              in if changes s1
                  then go True s1
                  else s { changes = ch }
  
  -- | Is this a known name for a module in the current scope?
  knownPName :: HasCurScope a => CurState' a -> PName -> Maybe Name
  knownPName s x =
    do ns <- lookupNS NSModule x (curScope s)
       case ns of
         One n    -> pure n
         {- NOTE: since we build up what's in scope incrementally,
            it is possible that this would eventually be ambiguous,
            which we'll detect during actual renaming. -}
  
         Ambig {} -> Nothing
         {- We treat ambiguous imports as undefined, which may lead to
            spurious "undefined X" errors.  To avoid this we should prioritize
            reporting "ambiguous X" errors. -}
  
  -- | Is the module mentioned in this import known in the current scope?
  knownImpName ::
    HasCurScope a => CurState' a -> ImpName PName -> Maybe (ImpName Name)
  knownImpName s i =
    case i of
      ImpTop m    -> pure (ImpTop m)
      ImpNested m -> ImpNested <$> knownPName s m
  
  -- | Is the module mentioned in the import already resolved?
  knownModule ::
    HasCurScope a => CurState' a -> ImpName Name -> Maybe ResolvedExt
  knownModule s x
    | root == curTop s =
      case x of
        ImpNested y -> forget <$> Map.lookup y (doneModules s)
        ImpTop {}   -> Nothing   -- or panic? recursive import
  
    | otherwise = Just (externalMod (externalModules s x))
  
    where
    root = case x of
             ImpTop r    -> r
             ImpNested n -> nameTopModule n
  
  --------------------------------------------------------------------------------
  
  
  {- | Try to resolve an import. If the imported module can be resolved,
  and it refers to a module that's already been resolved, then we do the
  import and extend the current scoping environment.  Otherwise, we just
  queue the import back on the @modImports@ of the current module to be tried
  again later.-}
  tryImport :: CurState -> ImportG (ImpName PName) -> CurState
  tryImport s imp =
    fromMaybe (updCur s (pushImport imp))   -- not ready, put it back on the q
    do let srcName = iModule imp
       mname <- knownImpName s (thing srcName)
       ext   <- knownModule s mname
  
       let isPub x = x `Set.member` rmodPublic ext
           new = case rmodKind ext of
                   AModule    -> interpImportEnv imp
                                   (filterUNames isPub (rmodDefines ext))
                   AFunctor   -> mempty
                   ASignature -> mempty
  
       pure $ updCurMS s { changes = True }
              \ms -> ms { modImported = new <> modImported ms }
  
  -- | Resolve all imports in the current modules
  doImportStep :: CurState -> CurState
  doImportStep s = foldl' tryImport s1 (modImports (curMod s))
    where
    s1 = updCur s \m -> m { modImports = [] }
  
  
  {- | Try to instantiate a functor.  This succeeds if we can resolve the functor
  and the arguments and the both refer to already resolved names.
  Note: at the moment we ignore the arguments, but we'd have to do that in
  order to implment applicative behavior with caching. -}
  tryInstanceMaybe ::
    HasCurScope a =>
    CurState' a ->
    ImpName Name ->
    (ImpName PName, ModuleInstanceArgs PName)
    {- ^ Functor and arguments -}  ->
    Maybe (ResolvedLocal,CurState' a)
  tryInstanceMaybe s mn (f,_xs) =
    do fn <- knownImpName s f
       let path = case mn of
                    ImpTop m    -> TopModule m
                    ImpNested m ->
                      case asOrigName m of
                        Just og -> Nested (ogModule og) (ogName og)
                        Nothing ->
                          panic "tryInstanceMaybe" [ "Not a top-level name" ]
       doInstantiateByName False path fn s
  
  {- | Try to instantiate a functor.  If successful, then the newly instantiated
  module (and all things nested in it) are going to be added to the
  @doneModules@ field.  Otherwise, we queue up the instantiatation in
  @curMod@ for later processing -}
  tryInstance ::
    CurState ->
    Name ->
    (ImpName PName, ModuleInstanceArgs PName) ->
    CurState
  tryInstance s mn (f,xs) =
    case tryInstanceMaybe s (ImpNested mn) (f,xs) of
      Nothing       -> updCur s (pushInst mn (f,xs))
      Just (def,s1) -> s1 { changes = True
                          , doneModules = Map.insert mn def (doneModules s1)
                          }
  
  {- | Generate a fresh instance for the functor with the given name. -}
  doInstantiateByName ::
    HasCurScope a =>
    Bool
    {- ^ This indicates if the result is a functor or not.  When instantiating
      a functor applied to some arguments the result is not a functor.  However,
      if we are instantiating a functor nested within some functor that's being
      instantiated, then the result is still a functor. -} ->
    ModPath {- ^ Path for instantiated names -} ->
    ImpName Name {- ^ Name of the functor/module being instantiated -} ->
    CurState' a -> Maybe (ResolvedLocal,CurState' a)
  
  doInstantiateByName keepArgs mpath fname s =
    do def <- knownModule s fname
       pure (doInstantiate keepArgs mpath def s)
  
  
  
  {- | Generate a new instantiation of the given module/signature.
  Note that the module might not be a functor itself (e.g., if we are
  instantiating something nested in a functor -}
  doInstantiate ::
    HasCurScope a =>
    Bool               {- ^ See `doInstantiateByName` -} ->
    ModPath            {- ^ Path for instantiated names -} ->
    ResolvedExt        {- ^ The thing being instantiated -} ->
    CurState' a -> (ResolvedLocal,CurState' a)
  doInstantiate keepArgs mpath def s = (newDef, Set.foldl' doSub newS nestedToDo)
    where
    ((newEnv,newNameSupply),nestedToDo) =
        M.runId
      $ M.runStateT Set.empty
      $ runSupplyT (nameSupply s)
      $ travNamingEnv instName
      $ rmodDefines def
  
    newS = s { nameSupply = newNameSupply }
  
    pub = let inst = zipByTextName (rmodDefines def) newEnv
          in Set.fromList [ case Map.lookup og inst of
                              Just newN -> newN
                              Nothing -> panic "doInstantiate.pub"
                                             [ "Lost a name", show og ]
                          | og <- Set.toList (rmodPublic def)
                          ]
  
  
    newDef = ResolvedModule { rmodDefines   = newEnv
                            , rmodPublic    = pub
                            , rmodKind      = case rmodKind def of
                                                AFunctor ->
                                                   if keepArgs then AFunctor
                                                               else AModule
                                                ASignature -> ASignature
                                                AModule -> AModule
  
                            , rmodNested    = Set.map snd nestedToDo
                            , rmodImports   = mempty
                              {- we don't do name resolution on the instantiation
                                 the usual way: instead the functor and the
                                 arguments are renamed separately, then we
                                 we do a pass where we replace:
                                    defined names of functor by instantiations
                                    parameter by actual names in arguments.
                              -}
                            }
  
    doSub st (oldSubName,newSubName) =
      case doInstantiateByName True (Nested mpath (nameIdent newSubName))
                                    (ImpNested oldSubName) st of
        Just (idef,st1) -> st1 { doneModules = Map.insert newSubName idef
                                                          (doneModules st1) }
        Nothing  -> panic "doInstantiate.doSub"
                      [ "Missing nested module:", show (pp oldSubName) ]
  
    instName :: Name -> SupplyT (M.StateT (Set (Name,Name)) M.Id) Name
    instName x =
      do y <- newFunctorInst mpath x
         when (x `Set.member` rmodNested def)
              (M.lift (M.sets_ (Set.insert (x,y))))
         pure y
  
  
  -- | Try to make progress on all instantiations.
  doInstancesStep :: CurState -> CurState
  doInstancesStep s = Map.foldlWithKey' tryInstance s0 (modInstances (curMod s))
    where
    s0 = updCur s \m' -> m' { modInstances = Map.empty }
  
  tryFinishCurMod :: Todo -> CurState -> Maybe ResolvedLocal
  tryFinishCurMod m newS
    | isDone newM =
      Just ResolvedModule
             { rmodDefines = modDefines m
             , rmodPublic  = modPublic m
             , rmodKind    = modKind m
             , rmodNested  = Set.unions
                               [ Map.keysSet (modInstances m)
                               , Map.keysSet (modMods m)
                               ]
             , rmodImports  = modImported (modState newM)
             }
  
    | otherwise = Nothing
    where newM = curMod newS
  
  
  -- | Try to resolve the "normal" module with the given name.
  tryModule :: CurState -> Name -> Todo -> CurState
  tryModule s nm m =
    case tryFinishCurMod m newS of
      Just rMod ->
        newS { curMod      = curMod s
             , doneModules = Map.insert nm rMod (doneModules newS)
             , changes     = True
             }
      Nothing -> newS { curMod = pushMod nm newM (curMod s) }
    where
    s1     = updCur s \_ -> updMS (\ms -> ms { modOuter = curScope s }) m
    newS   = doModuleStep s1
    newM   = curMod newS
  
  -- | Process all submodules of a module.
  doModulesStep :: CurState -> CurState
  doModulesStep s = Map.foldlWithKey' tryModule s0 (modMods m)
    where
    m  = curMod s
    s0 = s { curMod = m { modMods = mempty } }
  
  
  
  -- | All steps involved in processing a module.
  doModuleStep :: CurState -> CurState
  doModuleStep = doStep step
    where
    step = doStep doModulesStep
         . doStep doInstancesStep
         . doStep doImportStep
  
  
  