0 | module Idris.Package.Types

  2 | import Core.FC

  3 | import Core.Name.Namespace

  4 | import Data.List

  5 | import Data.Maybe

  6 | import Data.String

  7 | import Idris.Version

  8 | import Libraries.Text.PrettyPrint.Prettyprinter

  9 | import Libraries.Text.PrettyPrint.Prettyprinter.Util

 11 | %default total

 16 | public export

 17 | data PkgVersion = MkPkgVersion (List1 Nat)

 20 | Show PkgVersion where

 21 |   show (MkPkgVersion vs) = showSep "." (map show (forget vs))

 24 | Pretty Void PkgVersion where

 25 |   pretty = pretty . show

 28 | Eq PkgVersion where

 29 |   MkPkgVersion p == MkPkgVersion q = p == q

 32 | Ord PkgVersion where

 33 |   -- list ordering gives us what we want

 34 |   compare (MkPkgVersion p) (MkPkgVersion q) = compare p q

 41 | public export

 42 | record PkgVersionBounds where

 43 |   constructor MkPkgVersionBounds

 44 |   lowerBound : Maybe PkgVersion

 45 |   lowerInclusive : Bool -- >= if true

 46 |   upperBound : Maybe PkgVersion

 47 |   upperInclusive : Bool -- <= if true

 50 | Show PkgVersionBounds where

 51 |   show p = if noBounds then "any" else concat . intersperse " && " $ catMaybes [lowerBounds, upperBounds]

 53 |     where

 55 |       noBounds : Bool

 56 |       noBounds = isNothing p.lowerBound && isNothing p.upperBound

 58 |       lowerBounds : Maybe String

 59 |       lowerBounds = p.lowerBound <&> \v => (if p.lowerInclusive then ">= " else "> ") ++ show v

 61 |       upperBounds : Maybe String

 62 |       upperBounds = p.upperBound <&> \v => (if p.upperInclusive then "<= " else "< ") ++ show v

 65 | Pretty Void PkgVersionBounds where

 66 |   pretty (MkPkgVersionBounds lowerBound lowerInclusive upperBound upperInclusive)

 67 |       = concatWith (surround " && ") $

 68 |           catMaybes [ bounds True lowerInclusive lowerBound

 69 |                     , bounds False upperInclusive upperBound

 70 |                     ]

 71 |     where

 72 |       operator : (greater : Bool) -> (inclusive : Bool) -> Doc Void

 73 |       operator greater inclusive = pretty $ the String

 74 |         (if greater then ">" else "<") ++ (if inclusive then "=" else "")

 76 |       bounds : (greater : Bool) -> (inclusive : Bool) -> Maybe PkgVersion -> Maybe (Doc Void)

 77 |       bounds greater inclusive Nothing = Nothing

 78 |       bounds greater inclusive (Just v) = Just $ operator greater inclusive <++> pretty v

 81 | anyBounds : PkgVersionBounds

 82 | anyBounds = MkPkgVersionBounds Nothing True Nothing True

 85 | exactBounds : Maybe PkgVersion -> PkgVersionBounds

 86 | exactBounds mv = MkPkgVersionBounds mv True mv True

 89 | current : PkgVersionBounds

 90 | current = let (maj,min,patch) = semVer version

 91 |               version = Just (MkPkgVersion (maj ::: [min, patch])) in

 92 |               MkPkgVersionBounds version True version True

 94 | export %inline

 95 | defaultVersion : PkgVersion

 96 | defaultVersion = MkPkgVersion $ 0 ::: []

 99 | inBounds : Maybe PkgVersion -> PkgVersionBounds -> Bool

100 | inBounds mv bounds

101 |    = let v = fromMaybe defaultVersion mv in

102 |      maybe True (\v' => if bounds.lowerInclusive

103 |                            then v >= v'

104 |                            else v > v') bounds.lowerBound &&

105 |      maybe True (\v' => if bounds.upperInclusive

106 |                            then v <= v'

107 |                            else v < v') bounds.upperBound

109 | namespace Version

110 |   ||| Check if a Version is within the bounds of a PkgVersionBounds.

119 |   export

120 |   inBounds : Version -> PkgVersionBounds -> Bool

121 |   inBounds (MkVersion (maj, min, patch) tag) bounds

122 |      = let v = MkPkgVersion (maj ::: [min, patch]) in

123 |        maybe True (\v' => if bounds.lowerInclusive

124 |                              then v >= v'

125 |                              else v > v' || (v == v' && tag /= Nothing)) bounds.lowerBound &&

126 |        maybe True (\v' => if bounds.upperInclusive

127 |                              then v < v' || (v == v' && tag == Nothing)

128 |                              else v < v') bounds.upperBound

130 |   -- "0.1.0-abcd" > "0.1.0"

131 |   inBoundsBecauseOfTag : inBounds (MkVersion (0,1,0) (Just "abcd"))

132 |                                   (MkPkgVersionBounds (Just $ MkPkgVersion (0 ::: [1,0])) False

133 |                                   (Just $ MkPkgVersion (0 ::: [2,0])) False) = True

134 |   inBoundsBecauseOfTag = Refl

136 |   -- not ("0.2.0-abcd" <= "0.2.0")

137 |   outOfBoundsBecauseOfTag : inBounds (MkVersion (0,2,0) (Just "abcd"))

138 |                                      (MkPkgVersionBounds (Just $ MkPkgVersion (0 ::: [1,0])) False

139 |                                      (Just $ MkPkgVersion (0 ::: [2,0])) True) = False

140 |   outOfBoundsBecauseOfTag = Refl

145 | public export

146 | record Depends where

147 |   constructor MkDepends

148 |   pkgname : String

149 |   pkgbounds : PkgVersionBounds

152 | Show Depends where

153 |   show p = p.pkgname ++ " " ++ show p.pkgbounds

156 | Pretty Void Depends where

157 |   pretty dep = pretty dep.pkgname <+> pretty dep.pkgbounds

162 | public export

163 | record PkgDesc where

164 |   constructor MkPkgDesc

165 |   name : String

166 |   version : Maybe PkgVersion

167 |   langversion : Maybe PkgVersionBounds

168 |   authors : Maybe String

169 |   maintainers : Maybe String

170 |   license : Maybe String

171 |   brief   : Maybe String

172 |   readme  : Maybe String

173 |   homepage : Maybe String

174 |   sourceloc : Maybe String

175 |   bugtracker : Maybe String

176 |   depends : List Depends -- packages to add to search path

177 |   modules : List (ModuleIdent, String) -- modules to install (namespace, filename)

178 |   mainmod : Maybe (ModuleIdent, String) -- main file (i.e. file to load at REPL)

179 |   executable : Maybe String -- name of executable

180 |   options : Maybe (FC, String)

181 |   sourcedir : Maybe String

182 |   builddir : Maybe String

183 |   outputdir : Maybe String

184 |   prebuild : Maybe (FC, String) -- Script to run before building

185 |   postbuild : Maybe (FC, String) -- Script to run after building

186 |   preinstall : Maybe (FC, String) -- Script to run after building, before installing

187 |   postinstall : Maybe (FC, String) -- Script to run after installing

188 |   preclean : Maybe (FC, String) -- Script to run before cleaning

189 |   postclean : Maybe (FC, String) -- Script to run after cleaning

192 | initPkgDesc : String -> PkgDesc

193 | initPkgDesc pname

194 |     = MkPkgDesc pname Nothing Nothing Nothing Nothing Nothing

195 |                 Nothing Nothing Nothing Nothing Nothing

196 |                 [] []

197 |                 Nothing Nothing Nothing Nothing Nothing Nothing Nothing Nothing

198 |                 Nothing Nothing Nothing Nothing

201 | Show PkgDesc where

202 |   show pkg = "Package: " ++ name pkg ++ "\n" ++

203 |              maybe "" (\m => "Version: "     ++ m ++ "\n") (show <$> version pkg) ++

204 |              maybe "" (\v => "Language Version: " ++ v ++ "\n") (show <$> langversion pkg) ++

205 |              maybe "" (\m => "Authors: "     ++ m ++ "\n") (authors pkg)     ++

206 |              maybe "" (\m => "Maintainers: " ++ m ++ "\n") (maintainers pkg) ++

207 |              maybe "" (\m => "License: "     ++ m ++ "\n") (license pkg)     ++

208 |              maybe "" (\m => "Brief: "       ++ m ++ "\n") (brief pkg)       ++

209 |              maybe "" (\m => "ReadMe: "      ++ m ++ "\n") (readme pkg)      ++

210 |              maybe "" (\m => "HomePage: "    ++ m ++ "\n") (homepage pkg)    ++

211 |              maybe "" (\m => "SourceLoc: "   ++ m ++ "\n") (sourceloc pkg)   ++

212 |              maybe "" (\m => "BugTracker: "  ++ m ++ "\n") (bugtracker pkg)  ++

213 |              "Depends: " ++ show (depends pkg) ++ "\n" ++

214 |              "Modules: " ++ show (map snd (modules pkg)) ++ "\n" ++

215 |              maybe "" (\m => "Main: " ++ snd m ++ "\n") (mainmod pkg) ++

216 |              maybe "" (\m => "Exec: " ++ m ++ "\n") (executable pkg) ++

217 |              maybe "" (\m => "Opts: " ++ snd m ++ "\n") (options pkg) ++

218 |              maybe "" (\m => "SourceDir: " ++ m ++ "\n") (sourcedir pkg) ++

219 |              maybe "" (\m => "BuildDir: " ++ m ++ "\n") (builddir pkg) ++

220 |              maybe "" (\m => "OutputDir: " ++ m ++ "\n") (outputdir pkg) ++

221 |              maybe "" (\m => "Prebuild: " ++ snd m ++ "\n") (prebuild pkg) ++

222 |              maybe "" (\m => "Postbuild: " ++ snd m ++ "\n") (postbuild pkg) ++

223 |              maybe "" (\m => "Preinstall: " ++ snd m ++ "\n") (preinstall pkg) ++

224 |              maybe "" (\m => "Postinstall: " ++ snd m ++ "\n") (postinstall pkg) ++

225 |              maybe "" (\m => "Preclean: " ++ snd m ++ "\n") (preclean pkg) ++

226 |              maybe "" (\m => "Postclean: " ++ snd m ++ "\n") (postclean pkg)

229 | Pretty Void PkgDesc where

230 |   pretty desc = vcat

231 |     [ "package" <++> pretty desc.name

232 |     , verField "version"     desc.version

233 |     , strField "authors"     desc.authors

234 |     , strField "maintainers" desc.maintainers

235 |     , strField "license"     desc.license

236 |     , strField "brief"       desc.brief

237 |     , strField "readme"      desc.readme

238 |     , strField "homepage"    desc.homepage

239 |     , strField "sourceloc"   desc.sourceloc

240 |     , strField "bugtracker"  desc.bugtracker

242 |     , comment "the Idris2 version required (e.g. langversion >= 0.5.1)"

243 |     , verSeqField "langversion" desc.langversion

245 |     , comment  "packages to add to search path"

246 |     , seqField "depends"     desc.depends

248 |     , comment "modules to install"

249 |     , seqField "modules"     (fst <$> desc.modules)

251 |     , comment "main file (i.e. file to load at REPL)"

252 |     , field    "main"        (map (pretty . fst) desc.mainmod)

254 |     , comment "name of executable"

255 |     , strField "executable"  desc.executable

256 |     , strField "opts"        (snd <$> desc.options)

257 |     , strField "sourcedir"   desc.sourcedir

258 |     , strField "builddir"    desc.builddir

259 |     , strField "outputdir"   desc.outputdir

261 |     , comment "script to run before building"

262 |     , strField "prebuild"    (snd <$> desc.prebuild)

264 |     , comment "script to run after building"

265 |     , strField "postbuild"   (snd <$> desc.postbuild)

267 |     , comment "script to run after building, before installing"

268 |     , strField "preinstall"  (snd <$> desc.preinstall)

270 |     , comment "script to run after installing"

271 |     , strField "postinstall" (snd <$> desc.postinstall)

273 |     , comment "script to run before cleaning"

274 |     , strField "preclean"    (snd <$> desc.preclean)

276 |     , comment "script to run after cleaning"

277 |     , strField "postclean"   (snd <$> desc.postclean)

278 |     ]

280 |   where

282 |     comment : String -> Doc Void

283 |     comment str =

284 |       let ws = "--" :: words str in

285 |       let commSoftLine = Union (Chara ' ') (hcat [Line, "-- "]) in

286 |       Line <+> concatWith (\x, y => x <+> commSoftLine <+> y) ws

288 |     field : {default True printEquals : Bool} -> String -> Maybe (Doc Void) -> Doc Void

289 |     field {printEquals} nm Nothing = hsep $ catMaybes

290 |       [ Just $ "--"

291 |       , Just $ pretty nm

292 |       , (guard printEquals *> Just equals) ]

293 |     field {printEquals} nm (Just d) = hsep $ catMaybes

294 |       [ Just $ pretty nm

295 |       , (guard printEquals *> Just equals)

296 |       , Just d ]

298 |     verField : String -> Maybe PkgVersion -> Doc Void

299 |     verField nm = field nm . map pretty

301 |     verSeqField : String -> Maybe PkgVersionBounds -> Doc Void

302 |     verSeqField nm = field {printEquals=False} nm . map pretty

304 |     strField : String -> Maybe String -> Doc Void

305 |     strField nm = field nm . map (pretty . show)

307 |     seqField : Pretty Void a => String -> List a -> Doc Void

308 |     seqField nm [] = hsep [ pretty "--", pretty nm, equals ]

309 |     seqField nm xs = pretty nm

310 |                 <++> equals

311 |                 <++> align (sep (punctuate comma (map pretty xs)))

317 | public export

318 | record CSS where

319 |   constructor MkCSS

320 |   stylename : String

321 |   filename  : String

324 | cssFiles : List CSS

325 | cssFiles = [ MkCSS "Default"       "default"

326 |            , MkCSS "Alternative"   "alternative"

327 |            , MkCSS "Black & White" "blackandwhite"

328 |            ]