    -- |
    -- Module      :  Cryptol.Parser.NoInclude
    -- Copyright   :  (c) 2013-2016 Galois, Inc.
    -- License     :  BSD3
    -- Maintainer  :  cryptol@galois.com
    -- Stability   :  provisional
    -- Portability :  portable

    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE RecordWildCards #-}
    module Cryptol.Parser.NoInclude
      ( removeIncludesModule
      , IncludeError(..), ppIncludeError
      ) where

    import qualified Control.Applicative as A
    import Control.DeepSeq
    import qualified Control.Exception as X
    import Data.Either (partitionEithers)
    import Data.Text(Text)
    import qualified Data.Text.IO as T
    import GHC.Generics (Generic)
    import MonadLib
    import System.Directory (makeAbsolute)
    import System.FilePath (takeDirectory,(</>),isAbsolute)

    import Cryptol.Parser (parseProgramWith)
    import Cryptol.Parser.AST
    import Cryptol.Parser.LexerUtils (Config(..),defaultConfig)
    import Cryptol.Parser.ParserUtils
    import Cryptol.Parser.Unlit (guessPreProc)
    import Cryptol.Utils.PP

    removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
    removeIncludesModule :: FilePath
    -> Module PName -> IO (Either [IncludeError] (Module PName))
    removeIncludesModule modPath :: FilePath
    modPath m :: Module PName
    m = FilePath
    -> NoIncM (Module PName)
    -> IO (Either [IncludeError] (Module PName))
    forall a. FilePath -> NoIncM a -> IO (Either [IncludeError] a)
    runNoIncM FilePath
    modPath (Module PName -> NoIncM (Module PName)
    noIncludeModule Module PName
    m)

    data IncludeError
      = IncludeFailed (Located FilePath)
      | IncludeParseError ParseError
      | IncludeCycle [Located FilePath]
        deriving (Int -> IncludeError -> ShowS
    [IncludeError] -> ShowS
    IncludeError -> FilePath
    (Int -> IncludeError -> ShowS)
    -> (IncludeError -> FilePath)
    -> ([IncludeError] -> ShowS)
    -> Show IncludeError
    forall a.
    (Int -> a -> ShowS) -> (a -> FilePath) -> ([a] -> ShowS) -> Show a
    showList :: [IncludeError] -> ShowS
    $cshowList :: [IncludeError] -> ShowS
    show :: IncludeError -> FilePath
    $cshow :: IncludeError -> FilePath
    showsPrec :: Int -> IncludeError -> ShowS
    $cshowsPrec :: Int -> IncludeError -> ShowS
    Show, (forall x. IncludeError -> Rep IncludeError x)
    -> (forall x. Rep IncludeError x -> IncludeError)
    -> Generic IncludeError
    forall x. Rep IncludeError x -> IncludeError
    forall x. IncludeError -> Rep IncludeError x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cto :: forall x. Rep IncludeError x -> IncludeError
    $cfrom :: forall x. IncludeError -> Rep IncludeError x
    Generic, IncludeError -> ()
    (IncludeError -> ()) -> NFData IncludeError
    forall a. (a -> ()) -> NFData a
    rnf :: IncludeError -> ()
    $crnf :: IncludeError -> ()
    NFData)

    ppIncludeError :: IncludeError -> Doc
    ppIncludeError :: IncludeError -> Doc
    ppIncludeError ie :: IncludeError
    ie = case IncludeError
    ie of

      IncludeFailed lp :: Located FilePath
    lp -> (Char -> Doc
    char '`' Doc -> Doc -> Doc
    <.> FilePath -> Doc
    text (Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    lp) Doc -> Doc -> Doc
    <.> Char -> Doc
    char '`')
                      Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "included at"
                      Doc -> Doc -> Doc
    <+> Range -> Doc
    forall a. PP a => a -> Doc
    pp (Located FilePath -> Range
    forall a. Located a -> Range
    srcRange Located FilePath
    lp)
                      Doc -> Doc -> Doc
    <+> FilePath -> Doc
    text "was not found"

      IncludeParseError pe :: ParseError
    pe -> ParseError -> Doc
    ppError ParseError
    pe

      IncludeCycle is :: [Located FilePath]
    is -> FilePath -> Doc
    text "includes form a cycle:"
                      Doc -> Doc -> Doc
    $$ Int -> Doc -> Doc
    nest 2 ([Doc] -> Doc
    vcat ((Located FilePath -> Doc) -> [Located FilePath] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map (Range -> Doc
    forall a. PP a => a -> Doc
    pp (Range -> Doc)
    -> (Located FilePath -> Range) -> Located FilePath -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Located FilePath -> Range
    forall a. Located a -> Range
    srcRange) [Located FilePath]
    is))

    newtype NoIncM a = M
      { NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM :: ReaderT Env (ExceptionT [IncludeError] IO) a }

    data Env = Env { Env -> [Located FilePath]
    envSeen    :: [Located FilePath]
                     -- ^ Files that have been loaded
                   , Env -> FilePath
    envIncPath :: FilePath
                     -- ^ The path that includes are relative to
                   }

    runNoIncM :: FilePath -> NoIncM a -> IO (Either [IncludeError] a)
    runNoIncM :: FilePath -> NoIncM a -> IO (Either [IncludeError] a)
    runNoIncM sourcePath :: FilePath
    sourcePath m :: NoIncM a
    m =
      do FilePath
    incPath <- FilePath -> IO FilePath
    getIncPath FilePath
    sourcePath
         ReaderT Env (ExceptionT [IncludeError] IO) a
    -> Env -> IO (Either [IncludeError] a)
    forall (m :: * -> *) a r. RunM m a r => m a -> r
    runM (NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM NoIncM a
    m) Env :: [Located FilePath] -> FilePath -> Env
    Env { envSeen :: [Located FilePath]
    envSeen = [], envIncPath :: FilePath
    envIncPath = FilePath
    incPath }

    tryNoIncM :: NoIncM a -> NoIncM (Either [IncludeError] a)
    tryNoIncM :: NoIncM a -> NoIncM (Either [IncludeError] a)
    tryNoIncM m :: NoIncM a
    m = ReaderT
      Env (ExceptionT [IncludeError] IO) (Either [IncludeError] a)
    -> NoIncM (Either [IncludeError] a)
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (ReaderT Env (ExceptionT [IncludeError] IO) a
    -> ReaderT
         Env (ExceptionT [IncludeError] IO) (Either [IncludeError] a)
    forall (m :: * -> *) i a.
    RunExceptionM m i =>
    m a -> m (Either i a)
    try (NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM NoIncM a
    m))

    -- | Get the absolute directory name of a file that contains cryptol source.
    getIncPath :: FilePath -> IO FilePath
    getIncPath :: FilePath -> IO FilePath
    getIncPath file :: FilePath
    file = FilePath -> IO FilePath
    makeAbsolute (ShowS
    takeDirectory FilePath
    file)

    -- | Run a 'NoIncM' action with a different include path.  The argument is
    -- expected to be the path of a file that contains cryptol source, and will be
    -- adjusted with getIncPath.
    withIncPath :: FilePath -> NoIncM a -> NoIncM a
    withIncPath :: FilePath -> NoIncM a -> NoIncM a
    withIncPath path :: FilePath
    path (M body :: ReaderT Env (ExceptionT [IncludeError] IO) a
    body) = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a)
    -> ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a b. (a -> b) -> a -> b
    $
      do FilePath
    incPath <- IO FilePath -> ReaderT Env (ExceptionT [IncludeError] IO) FilePath
    forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
    inBase (FilePath -> IO FilePath
    getIncPath FilePath
    path)
         Env
    env     <- ReaderT Env (ExceptionT [IncludeError] IO) Env
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         Env
    -> ReaderT Env (ExceptionT [IncludeError] IO) a
    -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local Env
    env { envIncPath :: FilePath
    envIncPath = FilePath
    incPath } ReaderT Env (ExceptionT [IncludeError] IO) a
    body

    -- | Adjust an included file with the current include path.
    fromIncPath :: FilePath -> NoIncM FilePath
    fromIncPath :: FilePath -> NoIncM FilePath
    fromIncPath path :: FilePath
    path
      | FilePath -> Bool
    isAbsolute FilePath
    path = FilePath -> NoIncM FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return FilePath
    path
      | Bool
    otherwise       = ReaderT Env (ExceptionT [IncludeError] IO) FilePath
    -> NoIncM FilePath
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (ReaderT Env (ExceptionT [IncludeError] IO) FilePath
     -> NoIncM FilePath)
    -> ReaderT Env (ExceptionT [IncludeError] IO) FilePath
    -> NoIncM FilePath
    forall a b. (a -> b) -> a -> b
    $
        do Env { .. } <- ReaderT Env (ExceptionT [IncludeError] IO) Env
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
           FilePath -> ReaderT Env (ExceptionT [IncludeError] IO) FilePath
    forall (m :: * -> *) a. Monad m => a -> m a
    return (FilePath
    envIncPath FilePath -> ShowS
    </> FilePath
    path)

    instance Functor NoIncM where
      fmap :: (a -> b) -> NoIncM a -> NoIncM b
    fmap = (a -> b) -> NoIncM a -> NoIncM b
    forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
    liftM

    instance A.Applicative NoIncM where
      pure :: a -> NoIncM a
    pure = a -> NoIncM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return
      <*> :: NoIncM (a -> b) -> NoIncM a -> NoIncM b
    (<*>) = NoIncM (a -> b) -> NoIncM a -> NoIncM b
    forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
    ap

    instance Monad NoIncM where
      return :: a -> NoIncM a
    return x :: a
    x = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    x)
      m :: NoIncM a
    m >>= :: NoIncM a -> (a -> NoIncM b) -> NoIncM b
    >>= f :: a -> NoIncM b
    f  = ReaderT Env (ExceptionT [IncludeError] IO) b -> NoIncM b
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM NoIncM a
    m ReaderT Env (ExceptionT [IncludeError] IO) a
    -> (a -> ReaderT Env (ExceptionT [IncludeError] IO) b)
    -> ReaderT Env (ExceptionT [IncludeError] IO) b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= NoIncM b -> ReaderT Env (ExceptionT [IncludeError] IO) b
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM (NoIncM b -> ReaderT Env (ExceptionT [IncludeError] IO) b)
    -> (a -> NoIncM b)
    -> a
    -> ReaderT Env (ExceptionT [IncludeError] IO) b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> NoIncM b
    f)

    instance MonadFail NoIncM where
      fail :: FilePath -> NoIncM a
    fail x :: FilePath
    x   = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (FilePath -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) a. MonadFail m => FilePath -> m a
    fail FilePath
    x)

    -- | Raise an 'IncludeFailed' error.
    includeFailed :: Located FilePath -> NoIncM a
    includeFailed :: Located FilePath -> NoIncM a
    includeFailed path :: Located FilePath
    path = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M ([IncludeError] -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [Located FilePath -> IncludeError
    IncludeFailed Located FilePath
    path])

    -- | Push a path on the stack of included files, and run an action.  If the path
    -- is already on the stack, an include cycle has happened, and an error is
    -- raised.
    pushPath :: Located FilePath -> NoIncM a -> NoIncM a
    pushPath :: Located FilePath -> NoIncM a -> NoIncM a
    pushPath path :: Located FilePath
    path m :: NoIncM a
    m = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a)
    -> ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a b. (a -> b) -> a -> b
    $ do
      Env { .. } <- ReaderT Env (ExceptionT [IncludeError] IO) Env
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
      let alreadyIncluded :: Located FilePath -> Bool
    alreadyIncluded l :: Located FilePath
    l = Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    path FilePath -> FilePath -> Bool
    forall a. Eq a => a -> a -> Bool
    == Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    l
      Bool
    -> ReaderT Env (ExceptionT [IncludeError] IO) ()
    -> ReaderT Env (ExceptionT [IncludeError] IO) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((Located FilePath -> Bool) -> [Located FilePath] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Located FilePath -> Bool
    alreadyIncluded [Located FilePath]
    envSeen) ([IncludeError] -> ReaderT Env (ExceptionT [IncludeError] IO) ()
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [[Located FilePath] -> IncludeError
    IncludeCycle [Located FilePath]
    envSeen])
      Env
    -> ReaderT Env (ExceptionT [IncludeError] IO) a
    -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) i a. RunReaderM m i => i -> m a -> m a
    local Env :: [Located FilePath] -> FilePath -> Env
    Env { envSeen :: [Located FilePath]
    envSeen = Located FilePath
    pathLocated FilePath -> [Located FilePath] -> [Located FilePath]
    forall a. a -> [a] -> [a]
    :[Located FilePath]
    envSeen, .. } (NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM NoIncM a
    m)

    -- | Lift an IO operation, with a way to handle the exception that it might
    -- throw.
    failsWith :: X.Exception e => IO a -> (e -> NoIncM a) -> NoIncM a
    failsWith :: IO a -> (e -> NoIncM a) -> NoIncM a
    failsWith m :: IO a
    m k :: e -> NoIncM a
    k = ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M (ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a)
    -> ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    forall a b. (a -> b) -> a -> b
    $ do
      Either e a
    e <- IO (Either e a)
    -> ReaderT Env (ExceptionT [IncludeError] IO) (Either e a)
    forall (m :: * -> *) (n :: * -> *) a. BaseM m n => n a -> m a
    inBase (IO a -> IO (Either e a)
    forall e a. Exception e => IO a -> IO (Either e a)
    X.try IO a
    m)
      case Either e a
    e of
        Right a :: a
    a  -> a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    a
        Left exn :: e
    exn -> NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    forall a. NoIncM a -> ReaderT Env (ExceptionT [IncludeError] IO) a
    unM (e -> NoIncM a
    k e
    exn)

    -- | Like 'mapM', but tries to collect as many errors as possible before
    -- failing.
    collectErrors :: (a -> NoIncM b) -> [a] -> NoIncM [b]
    collectErrors :: (a -> NoIncM b) -> [a] -> NoIncM [b]
    collectErrors f :: a -> NoIncM b
    f ts :: [a]
    ts = do
      [Either [IncludeError] b]
    es <- (a -> NoIncM (Either [IncludeError] b))
    -> [a] -> NoIncM [Either [IncludeError] b]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (NoIncM b -> NoIncM (Either [IncludeError] b)
    forall a. NoIncM a -> NoIncM (Either [IncludeError] a)
    tryNoIncM (NoIncM b -> NoIncM (Either [IncludeError] b))
    -> (a -> NoIncM b) -> a -> NoIncM (Either [IncludeError] b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> NoIncM b
    f) [a]
    ts
      let (ls :: [[IncludeError]]
    ls,rs :: [b]
    rs) = [Either [IncludeError] b] -> ([[IncludeError]], [b])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers [Either [IncludeError] b]
    es
          errs :: [IncludeError]
    errs    = [[IncludeError]] -> [IncludeError]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[IncludeError]]
    ls
      Bool -> NoIncM () -> NoIncM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([IncludeError] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [IncludeError]
    errs) (ReaderT Env (ExceptionT [IncludeError] IO) () -> NoIncM ()
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M ([IncludeError] -> ReaderT Env (ExceptionT [IncludeError] IO) ()
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [IncludeError]
    errs))
      [b] -> NoIncM [b]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [b]
    rs

    -- | Remove includes from a module.
    noIncludeModule :: Module PName -> NoIncM (Module PName)
    noIncludeModule :: Module PName -> NoIncM (Module PName)
    noIncludeModule m :: Module PName
    m = [[TopDecl PName]] -> Module PName
    forall (t :: * -> *) name.
    Foldable t =>
    t [TopDecl name] -> Module name
    update ([[TopDecl PName]] -> Module PName)
    -> NoIncM [[TopDecl PName]] -> NoIncM (Module PName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (TopDecl PName -> NoIncM [TopDecl PName])
    -> [TopDecl PName] -> NoIncM [[TopDecl PName]]
    forall a b. (a -> NoIncM b) -> [a] -> NoIncM [b]
    collectErrors TopDecl PName -> NoIncM [TopDecl PName]
    noIncTopDecl (Module PName -> [TopDecl PName]
    forall name. Module name -> [TopDecl name]
    mDecls Module PName
    m)
      where
      update :: t [TopDecl name] -> Module name
    update tds :: t [TopDecl name]
    tds = Module PName
    m { mDecls :: [TopDecl name]
    mDecls = t [TopDecl name] -> [TopDecl name]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat t [TopDecl name]
    tds }

    -- | Remove includes from a program.
    noIncludeProgram :: Program PName -> NoIncM (Program PName)
    noIncludeProgram :: Program PName -> NoIncM (Program PName)
    noIncludeProgram (Program tds :: [TopDecl PName]
    tds) =
      ([TopDecl PName] -> Program PName
    forall name. [TopDecl name] -> Program name
    Program ([TopDecl PName] -> Program PName)
    -> ([[TopDecl PName]] -> [TopDecl PName])
    -> [[TopDecl PName]]
    -> Program PName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[TopDecl PName]] -> [TopDecl PName]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat) ([[TopDecl PName]] -> Program PName)
    -> NoIncM [[TopDecl PName]] -> NoIncM (Program PName)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` (TopDecl PName -> NoIncM [TopDecl PName])
    -> [TopDecl PName] -> NoIncM [[TopDecl PName]]
    forall a b. (a -> NoIncM b) -> [a] -> NoIncM [b]
    collectErrors TopDecl PName -> NoIncM [TopDecl PName]
    noIncTopDecl [TopDecl PName]
    tds

    -- | Substitute top-level includes with the declarations from the files they
    -- reference.
    noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName]
    noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName]
    noIncTopDecl td :: TopDecl PName
    td = case TopDecl PName
    td of
      Decl _     -> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName
    td]
      DPrimType {} -> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [TopDecl PName
    td]
      TDNewtype _-> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName
    td]
      DParameterType {} -> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName
    td]
      DParameterConstraint {} -> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName
    td]
      DParameterFun {} -> [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName
    td]
      Include lf :: Located FilePath
    lf -> Located FilePath -> NoIncM [TopDecl PName]
    resolveInclude Located FilePath
    lf

    -- | Resolve the file referenced by a include into a list of top-level
    -- declarations.
    resolveInclude :: Located FilePath -> NoIncM [TopDecl PName]
    resolveInclude :: Located FilePath -> NoIncM [TopDecl PName]
    resolveInclude lf :: Located FilePath
    lf = Located FilePath
    -> NoIncM [TopDecl PName] -> NoIncM [TopDecl PName]
    forall a. Located FilePath -> NoIncM a -> NoIncM a
    pushPath Located FilePath
    lf (NoIncM [TopDecl PName] -> NoIncM [TopDecl PName])
    -> NoIncM [TopDecl PName] -> NoIncM [TopDecl PName]
    forall a b. (a -> b) -> a -> b
    $ do
      Text
    source <- Located FilePath -> NoIncM Text
    readInclude Located FilePath
    lf
      case Config -> Text -> Either ParseError (Program PName)
    parseProgramWith (Config
    defaultConfig { cfgSource :: FilePath
    cfgSource = Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    lf, cfgPreProc :: PreProc
    cfgPreProc = FilePath -> PreProc
    guessPreProc (Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    lf) }) Text
    source of

        Right prog :: Program PName
    prog -> do
          Program ds :: [TopDecl PName]
    ds <- FilePath -> NoIncM (Program PName) -> NoIncM (Program PName)
    forall a. FilePath -> NoIncM a -> NoIncM a
    withIncPath (Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    lf) (Program PName -> NoIncM (Program PName)
    noIncludeProgram Program PName
    prog)
          [TopDecl PName] -> NoIncM [TopDecl PName]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [TopDecl PName]
    ds

        Left err :: ParseError
    err -> ReaderT Env (ExceptionT [IncludeError] IO) [TopDecl PName]
    -> NoIncM [TopDecl PName]
    forall a. ReaderT Env (ExceptionT [IncludeError] IO) a -> NoIncM a
    M ([IncludeError]
    -> ReaderT Env (ExceptionT [IncludeError] IO) [TopDecl PName]
    forall (m :: * -> *) i a. ExceptionM m i => i -> m a
    raise [ParseError -> IncludeError
    IncludeParseError ParseError
    err])

    -- | Read a file referenced by an include.
    readInclude :: Located FilePath -> NoIncM Text
    readInclude :: Located FilePath -> NoIncM Text
    readInclude path :: Located FilePath
    path = do
      FilePath
    file   <- FilePath -> NoIncM FilePath
    fromIncPath (Located FilePath -> FilePath
    forall a. Located a -> a
    thing Located FilePath
    path)
      Text
    source <- FilePath -> IO Text
    T.readFile FilePath
    file IO Text -> (IOException -> NoIncM Text) -> NoIncM Text
    forall e a. Exception e => IO a -> (e -> NoIncM a) -> NoIncM a
    `failsWith` IOException -> NoIncM Text
    forall a. IOException -> NoIncM a
    handler
      Text -> NoIncM Text
    forall (m :: * -> *) a. Monad m => a -> m a
    return Text
    source
      where
      handler :: X.IOException -> NoIncM a
      handler :: IOException -> NoIncM a
    handler _ = Located FilePath -> NoIncM a
    forall a. Located FilePath -> NoIncM a
    includeFailed Located FilePath
    path