3 | module Pack.Core.Ipkg

  5 | import Core.Core

  6 | import Core.FC

  7 | import Core.Name.Namespace

  8 | import Idris.Package.Types

  9 | import Libraries.Data.String.Extra

 10 | import Libraries.Text.Parser

 11 | import Pack.Core.Types

 12 | import Pack.Core.IO

 13 | import Parser.Package

 14 | import System.File

 16 | %default total

 22 | data DescField  : Type where

 23 |   PVersion      : FC -> PkgVersion -> DescField

 24 |   PLangVersions : FC -> PkgVersionBounds -> DescField

 25 |   PVersionDep   : FC -> String -> DescField

 26 |   PAuthors      : FC -> String -> DescField

 27 |   PMaintainers  : FC -> String -> DescField

 28 |   PLicense      : FC -> String -> DescField

 29 |   PBrief        : FC -> String -> DescField

 30 |   PReadMe       : FC -> String -> DescField

 31 |   PHomePage     : FC -> String -> DescField

 32 |   PSourceLoc    : FC -> String -> DescField

 33 |   PBugTracker   : FC -> String -> DescField

 34 |   PDepends      : List Depends -> DescField

 35 |   PModules      : List (FC, ModuleIdent) -> DescField

 36 |   PMainMod      : FC -> ModuleIdent -> DescField

 37 |   PExec         : String -> DescField

 38 |   POpts         : FC -> String -> DescField

 39 |   PSourceDir    : FC -> String -> DescField

 40 |   PBuildDir     : FC -> String -> DescField

 41 |   POutputDir    : FC -> String -> DescField

 42 |   PPrebuild     : FC -> String -> DescField

 43 |   PPostbuild    : FC -> String -> DescField

 44 |   PPreinstall   : FC -> String -> DescField

 45 |   PPostinstall  : FC -> String -> DescField

 46 |   PPreclean     : FC -> String -> DescField

 47 |   PPostclean    : FC -> String -> DescField

 49 | field : String -> Rule DescField

 50 | field fname =

 51 |       strField PAuthors "authors"

 52 |   <|> strField PMaintainers "maintainers"

 53 |   <|> strField PLicense "license"

 54 |   <|> strField PBrief "brief"

 55 |   <|> strField PReadMe "readme"

 56 |   <|> strField PHomePage "homepage"

 57 |   <|> strField PSourceLoc "sourceloc"

 58 |   <|> strField PBugTracker "bugtracker"

 59 |   <|> strField POpts "options"

 60 |   <|> strField POpts "opts"

 61 |   <|> strField PSourceDir "sourcedir"

 62 |   <|> strField PBuildDir "builddir"

 63 |   <|> strField POutputDir "outputdir"

 64 |   <|> strField PPrebuild "prebuild"

 65 |   <|> strField PPostbuild "postbuild"

 66 |   <|> strField PPreinstall "preinstall"

 67 |   <|> strField PPostinstall "postinstall"

 68 |   <|> strField PPreclean "preclean"

 69 |   <|> strField PPostclean "postclean"

 70 |   <|> do start <- location

 71 |          ignore $ exactProperty "version"

 72 |          equals

 73 |          vs <- sepBy1 dot' integerLit

 74 |          end <- location

 75 |          pure (PVersion (MkFC (PhysicalPkgSrc fname) start end)

 76 |                         (MkPkgVersion (fromInteger <$> vs)))

 77 |   <|> do start <- location

 78 |          ignore $ exactProperty "langversion"

 79 |          lvs <- langversions

 80 |          end <- location

 81 |          pure (PLangVersions (MkFC (PhysicalPkgSrc fname) start end) lvs)

 82 |   <|> do start <- location

 83 |          ignore $ exactProperty "version"

 84 |          equals

 85 |          v <- stringLit

 86 |          end <- location

 87 |          pure (PVersionDep (MkFC (PhysicalPkgSrc fname) start end) v)

 88 |   <|> do ignore $ exactProperty "depends"

 89 |          equals

 90 |          ds <- sep depends

 91 |          pure (PDepends ds)

 92 |   <|> do ignore $ exactProperty "modules"

 93 |          equals

 94 |          ms <- sep (do start <- location

 95 |                        m <- moduleIdent

 96 |                        end <- location

 97 |                        pure (MkFC (PhysicalPkgSrc fname) start end, m))

 98 |          pure (PModules ms)

 99 |   <|> do ignore $ exactProperty "main"

100 |          equals

101 |          start <- location

102 |          m <- moduleIdent

103 |          end <- location

104 |          pure (PMainMod (MkFC (PhysicalPkgSrc fname) start end) m)

105 |   <|> do ignore $ exactProperty "executable"

106 |          equals

107 |          e <- (stringLit <|> packageName)

108 |          pure (PExec e)

109 |   where

110 |     data Bound = LT PkgVersion Bool | GT PkgVersion Bool

112 |     bound : Rule (List Bound)

113 |     bound

114 |         = do lte

115 |              vs <- sepBy1 dot' integerLit

116 |              pure [LT (MkPkgVersion (fromInteger <$> vs)) True]

117 |       <|> do gte

118 |              vs <- sepBy1 dot' integerLit

119 |              pure [GT (MkPkgVersion (fromInteger <$> vs)) True]

120 |       <|> do lt

121 |              vs <- sepBy1 dot' integerLit

122 |              pure [LT (MkPkgVersion (fromInteger <$> vs)) False]

123 |       <|> do gt

124 |              vs <- sepBy1 dot' integerLit

125 |              pure [GT (MkPkgVersion (fromInteger <$> vs)) False]

126 |       <|> do eqop

127 |              vs <- sepBy1 dot' integerLit

128 |              pure

129 |                [ LT (MkPkgVersion (fromInteger <$> vs)) True

130 |                , GT (MkPkgVersion (fromInteger <$> vs)) True

131 |                ]

133 |     mkBound : List Bound -> PkgVersionBounds -> EmptyRule PkgVersionBounds

134 |     mkBound (LT b i :: bs) pkgbs =

135 |       maybe

136 |         (mkBound bs ({ upperBound := Just b, upperInclusive := i } pkgbs))

137 |         (\_ => fail "Dependency already has an upper bound")

138 |         pkgbs.upperBound

139 |     mkBound (GT b i :: bs) pkgbs =

140 |       maybe

141 |         (mkBound bs ({ lowerBound := Just b, lowerInclusive := i } pkgbs))

142 |         (\_ => fail "Dependency already has a lower bound")

143 |         pkgbs.lowerBound

144 |     mkBound [] pkgbs = pure pkgbs

146 |     langversions : EmptyRule PkgVersionBounds

147 |     langversions = do

148 |       bs <- sepBy andop bound

149 |       mkBound (concat bs) anyBounds

151 |     depends : Rule Depends

152 |     depends = do

153 |       name <- packageName

154 |       bs <- sepBy andop bound

155 |       pure (MkDepends name !(mkBound (concat bs) anyBounds))

157 |     strField : (FC -> String -> DescField) -> String -> Rule DescField

158 |     strField fieldConstructor fieldName = do

159 |       start <- location

160 |       ignore $ exactProperty fieldName

161 |       equals

162 |       str <- stringLit

163 |       end <- location

164 |       pure $ fieldConstructor (MkFC (PhysicalPkgSrc fname) start end) str

166 | pkgDesc : String -> Rule (String, List DescField)

167 | pkgDesc fname = do

168 |   ignore $ exactProperty "package"

169 |   name <- packageName

170 |   fields <- many (field fname)

171 |   pure (name, fields)

173 | addField : PkgDesc -> DescField -> PkgDesc

174 | addField p (PVersion fc n)       = { version := Just n } p

175 | addField p (PLangVersions fc bs) = { langversion := Just bs } p

176 | addField p (PVersionDep fc n)    = p

177 | addField p (PAuthors fc a)       = { authors := Just a } p

178 | addField p (PMaintainers fc a)   = { maintainers := Just a } p

179 | addField p (PLicense fc a)       = { license := Just a } p

180 | addField p (PBrief fc a)         = { brief := Just a } p

181 | addField p (PReadMe fc a)        = { readme := Just a } p

182 | addField p (PHomePage fc a)      = { homepage := Just a } p

183 | addField p (PSourceLoc fc a)     = { sourceloc := Just a } p

184 | addField p (PBugTracker fc a)    = { bugtracker := Just a } p

185 | addField p (PDepends ds)         = { depends := ds } p

186 | addField p (PModules ms)         = { modules := map (\(_,i) => (i,"")) ms } p

187 | addField p (PMainMod loc n)      = { mainmod := Just (n,"") } p

188 | addField p (PExec e)             = { executable := Just e } p

189 | addField p (POpts fc e)          = { options := Just (fc, e) } p

190 | addField p (PSourceDir fc a)     = { sourcedir := Just a } p

191 | addField p (PBuildDir fc a)      = { builddir := Just a } p

192 | addField p (POutputDir fc a)     = { outputdir := Just a } p

193 | addField p (PPrebuild fc e)      = { prebuild := Just (fc, e) } p

194 | addField p (PPostbuild fc e)     = { postbuild := Just (fc, e) } p

195 | addField p (PPreinstall fc e)    = { preinstall := Just (fc, e) } p

196 | addField p (PPostinstall fc e)   = { postinstall := Just (fc, e) } p

197 | addField p (PPreclean fc e)      = { preclean := Just (fc, e) } p

198 | addField p (PPostclean fc e)     = { postclean := Just (fc, e) } p

200 | addFields : (name : String) -> List DescField -> PkgDesc

201 | addFields = foldl addField . initPkgDesc

203 | parseIpkg : File Abs -> String -> Either PackErr PkgDesc

204 | parseIpkg file str =

205 |   let err := InvalidIpkgFile file

206 |    in do

207 |      toks           <- mapFst (const err) $ lex str

208 |      (_, (n,fs), _) <- mapFst (const err) $ parse (pkgDesc "\{file}") toks

209 |      Right $ addFields n fs

211 | export covering

212 | parseIpkgFile :

213 |      {auto _ : HasIO io}

214 |   -> (file   : File Abs)

215 |   -> (tmpLoc : File Abs)

216 |   -> EitherT PackErr io (Desc U)

217 | parseIpkgFile file loc = do

218 |   str  <- read file

219 |   desc <- liftEither (parseIpkg file str)

220 |   pure (MkDesc desc str loc ())

229 | sourcePath : Desc t -> Path Abs

230 | sourcePath d =

231 |   maybe

232 |     d.path.parent

233 |     (toAbsPath d.path.parent . fromString)

234 |     d.desc.sourcedir

239 | buildPath : Desc t -> Path Abs

240 | buildPath d =

241 |   maybe

242 |     (d.path.parent /> "build")

243 |     (toAbsPath d.path.parent . fromString)

244 |     d.desc.builddir

249 | exec : Desc t -> Maybe Body

250 | exec d = d.desc.executable >>= parse

255 | execPath : Desc t -> (Maybe $ File Abs)

256 | execPath d = (MkF $ buildPath d /> "exec") <$> exec d

264 | public export

265 | record DocSources where

266 |   constructor MkDS

267 |   htmlDoc : File Abs

268 |   srcFile : File Abs

269 |   ttmFile : File Abs

270 |   srcHtml : File Abs

272 | replaceDot : Char -> Char

273 | replaceDot '.' = '/'

274 | replaceDot c   = c

277 | srcExists : HasIO io => DocSources -> EitherT PackErr io Bool

278 | srcExists (MkDS _ s t _) = do

279 |   es <- fileExists s

280 |   et <- fileExists t

281 |   pure (es && et)

286 | sourceForDoc : TTCVersion => Desc t -> File Abs -> Maybe DocSources

287 | sourceForDoc d f = do

288 |   MkBody cs p <- fileStem f

289 |   rf          <- RelFile.parse . pack $ map replaceDot cs

290 |   Just $

291 |     MkDS

292 |       { htmlDoc = f

293 |       , srcFile = (sourcePath d </> rf) <.> "idr"

294 |       , ttmFile = ttm rf

295 |       , srcHtml = MkF (f.parent) (MkBody cs p <.> "src.html")

296 |       }

298 |   where

299 |     ttm : (rf : File Rel) -> File Abs

300 |     ttm rf = case ttcVersion of

301 |       Just v  => (buildPath d </> "ttc" /> v </> rf) <.> "ttm"

302 |       Nothing => (buildPath d </> "ttc" </> rf) <.> "ttm"

306 | export covering

307 | insertSources : HasIO io => DocSources -> EitherT PackErr io ()

308 | insertSources x = do

309 |   str <- read x.htmlDoc

310 |   write x.htmlDoc (unlines . map (pack . insertSrc . unpack) $ lines str)

311 |   where

312 |     beforeH1 : List Char -> List Char

313 |     beforeH1 [] = []

314 |     beforeH1 ('<' :: '/' :: 'h' :: '1' :: '>' :: t) =

315 |       unpack "</h1><span style=\"float:right\">" ++

316 |       unpack "(<a href=\"\{x.srcHtml.file}\">source</a>)</span>" ++ t

317 |     beforeH1 (h :: t) = h :: beforeH1 t

319 |     insertSrc : List Char -> List Char

320 |     insertSrc []                              = []

321 |     insertSrc ('<' :: 'h' :: '1' :: '>' :: t) = unpack "<h1>" ++ beforeH1 t

322 |     insertSrc (h :: t)                        = h :: insertSrc t