File: NoInclude.hs

package info (click to toggle)
haskell-cryptol 2.8.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 1,644 kB
  • sloc: haskell: 20,847; yacc: 652; makefile: 5
file content (188 lines) | stat: -rw-r--r-- 6,070 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
-- |
-- 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 modPath m = runNoIncM modPath (noIncludeModule m)

data IncludeError
  = IncludeFailed (Located FilePath)
  | IncludeParseError ParseError
  | IncludeCycle [Located FilePath]
    deriving (Show, Generic, NFData)

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

  IncludeFailed lp -> (char '`' <.> text (thing lp) <.> char '`')
                  <+> text "included at"
                  <+> pp (srcRange lp)
                  <+> text "was not found"

  IncludeParseError pe -> ppError pe

  IncludeCycle is -> text "includes form a cycle:"
                  $$ nest 2 (vcat (map (pp . srcRange) is))


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

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

runNoIncM :: FilePath -> NoIncM a -> IO (Either [IncludeError] a)
runNoIncM sourcePath m =
  do incPath <- getIncPath sourcePath
     runM (unM m) Env { envSeen = [], envIncPath = incPath }

tryNoIncM :: NoIncM a -> NoIncM (Either [IncludeError] a)
tryNoIncM m = M (try (unM m))

-- | Get the absolute directory name of a file that contains cryptol source.
getIncPath :: FilePath -> IO FilePath
getIncPath file = makeAbsolute (takeDirectory 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 path (M body) = M $
  do incPath <- inBase (getIncPath path)
     env     <- ask
     local env { envIncPath = incPath } body

-- | Adjust an included file with the current include path.
fromIncPath :: FilePath -> NoIncM FilePath
fromIncPath path
  | isAbsolute path = return path
  | otherwise       = M $
    do Env { .. } <- ask
       return (envIncPath </> path)


instance Functor NoIncM where
  fmap = liftM

instance A.Applicative NoIncM where
  pure = return
  (<*>) = ap

instance Monad NoIncM where
  return x = M (return x)
  m >>= f  = M (unM m >>= unM . f)

instance MonadFail NoIncM where
  fail x   = M (fail x)

-- | Raise an 'IncludeFailed' error.
includeFailed :: Located FilePath -> NoIncM a
includeFailed path = M (raise [IncludeFailed 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 path m = M $ do
  Env { .. } <- ask
  let alreadyIncluded l = thing path == thing l
  when (any alreadyIncluded envSeen) (raise [IncludeCycle envSeen])
  local Env { envSeen = path:envSeen, .. } (unM 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 m k = M $ do
  e <- inBase (X.try m)
  case e of
    Right a  -> return a
    Left exn -> unM (k exn)

-- | Like 'mapM', but tries to collect as many errors as possible before
-- failing.
collectErrors :: (a -> NoIncM b) -> [a] -> NoIncM [b]
collectErrors f ts = do
  es <- mapM (tryNoIncM . f) ts
  let (ls,rs) = partitionEithers es
      errs    = concat ls
  unless (null errs) (M (raise errs))
  return rs

-- | Remove includes from a module.
noIncludeModule :: Module PName -> NoIncM (Module PName)
noIncludeModule m = update `fmap` collectErrors noIncTopDecl (mDecls m)
  where
  update tds = m { mDecls = concat tds }

-- | Remove includes from a program.
noIncludeProgram :: Program PName -> NoIncM (Program PName)
noIncludeProgram (Program tds) =
  (Program . concat) `fmap` collectErrors noIncTopDecl tds

-- | Substitute top-level includes with the declarations from the files they
-- reference.
noIncTopDecl :: TopDecl PName -> NoIncM [TopDecl PName]
noIncTopDecl td = case td of
  Decl _     -> return [td]
  DPrimType {} -> pure [td]
  TDNewtype _-> return [td]
  DParameterType {} -> return [td]
  DParameterConstraint {} -> return [td]
  DParameterFun {} -> return [td]
  Include lf -> resolveInclude lf

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

    Right prog -> do
      Program ds <- withIncPath (thing lf) (noIncludeProgram prog)
      return ds

    Left err -> M (raise [IncludeParseError err])

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