0 | module Pack.Runner.Query

  2 | import Core.Name.Namespace

  3 | import Data.List

  4 | import Data.IORef

  5 | import Data.Maybe

  6 | import Data.SortedMap

  7 | import Idris.Package.Types

  8 | import Pack.CmdLn.Types

  9 | import Pack.Config

 10 | import Pack.Core

 11 | import Pack.Database

 12 | import Pack.Database.Tree

 13 | import Pack.Runner.Database

 14 | import Pack.Runner.Install

 15 | import Pack.Version

 17 | %default total

 23 | public export

 24 | record AppInfo (p : Package) where

 25 |   constructor AI

 26 |   exec   : Body

 27 |   status : AppStatus p

 29 | public export

 30 | record QPkg where

 31 |   constructor QP

 32 |   lib : ResolvedLib U

 33 |   app : Maybe (AppInfo lib.pkg)

 35 | export %inline

 36 | name : QPkg -> PkgName

 37 | name = name . lib

 39 | export %inline

 40 | nameStr : QPkg -> String

 41 | nameStr = value . name

 43 | export %inline

 44 | dependencies : QPkg -> List PkgName

 45 | dependencies = dependencies . lib

 48 | isApp : QPkg -> Bool

 49 | isApp (QP _ a) = isJust a

 52 | installedLib : QPkg -> Bool

 53 | installedLib qp = case qp.lib.status of

 54 |   Installed _ _ => True

 55 |   Missing     _ => False

 58 | installedApp : QPkg -> Bool

 59 | installedApp qp = case map status qp.app of

 60 |   Just (Installed    _) => True

 61 |   Just (BinInstalled _) => True

 62 |   Just (Missing      _) => False

 63 |   Nothing               => False

 66 | resolve : HasIO io => Env => PkgName -> EitherT PackErr io QPkg

 67 | resolve n = do

 68 |   lib <- resolveLib n

 69 |   Just exe <- pure (exec lib.desc) | Nothing => pure (QP lib Nothing)

 70 |   st       <- appStatus n lib.hash lib.pkg exe

 71 |   pure $ QP lib (Just $ AI exe st)

 73 | pkgNames : (e : Env) => List PkgName

 74 | pkgNames = keys e.all

 76 | export covering

 77 | resolveAll :

 78 |      {auto h : HasIO io}

 79 |   -> {auto env : Env}

 80 |   -> EitherT PackErr io (SortedMap PkgName (ResolvedLib U), List QPkg)

 81 | resolveAll = do

 82 |   ps <- traverse resolve pkgNames

 83 |   sm <- readIORef env.cache

 84 |   pure (sm, ps)

 91 | hashLookup : PkgName -> SortedMap PkgName (ResolvedLib U) -> Hash

 92 | hashLookup x = maybe (MkHash "") hash . lookup x

 95 | query_ :

 96 |      {auto _ : HasIO io}

 97 |   -> {auto _ : Env}

 98 |   -> (q : Hash -> (parents,children : Tree PkgName) -> QPkg -> Maybe b)

 99 |   -> EitherT PackErr io (List b)

100 | query_ q = do

101 |   (sm,ps) <- resolveAll

103 |   let children := childMap sm

105 |       parents  := parentMap sm

107 |   pure $

108 |     mapMaybe

109 |       (\p => let n := name p in q (hashLookup n sm) (treeLookup n parents) (treeLookup n children) p)

110 |       ps

112 | shortDesc : QPkg -> Maybe String

113 | shortDesc q = q.lib.desc.desc.brief

115 | modules : QPkg -> List String

116 | modules = map (show . fst) . modules . desc . desc . lib

118 | prettyDeps : QPkg -> List String

119 | prettyDeps qp = case dependencies qp of

120 |   []     => ["Dependencies :"]

121 |   h :: t => "Dependencies : \{h}" :: map (indent 15 . interpolate) t

123 | prettyModules : String -> QPkg -> List String

124 | prettyModules s qp = case filter (isInfixOf s) (modules qp) of

125 |   []     => ["Modules :"]

126 |   h :: t => "Modules : \{h}" :: map (indent 10) t

128 | status : PkgStatus p -> String

129 | status (Missing   _)   = "not installed"

130 | status (Installed _ _) = "installed"

132 | status' : AppStatus p -> String

133 | status' (Missing h)      = "not installed"

134 | status' (Installed h)    = "installed"

135 | status' (BinInstalled h) = "installed and on $PATH"

137 | libStatus : QPkg -> List String

138 | libStatus q = [ "Library      : \{status q.lib.status}" ]

140 | appStatus : QPkg -> List String

141 | appStatus qp = case qp.app of

142 |   Nothing          => []

143 |   Just (AI exe st) =>

144 |     [ "Executable   : \{exe}"

145 |     , "App          : \{status' st}"

146 |     ]

148 | testFile : Maybe (File Rel) -> Maybe String

149 | testFile = map (\f => "Test File    : \{f}")

151 | notice : Maybe String -> Maybe String

152 | notice = map (\f =>   "Notice       : \{f}")

154 | details : Hash -> QPkg -> List String

155 | details hash qp = case qp.lib.pkg of

156 |   Git url commit ipkg _ t n => [

157 |     "Type         : Git project"

158 |   , "URL          : \{url}"

159 |   , "Commit       : \{commit}"

160 |   , "Install hash : \{hash}"

161 |   , "ipkg File    : \{ipkg}"

162 |   ] ++ (catMaybes [testFile t, notice n])

164 |   Local d i _ t =>

165 |     let ipkg := toAbsFile d i

166 |      in [ "Type         : Local Idris project"

167 |         , "Location     : \{ipkg.parent}"

168 |         , "Install hash : \{hash}"

169 |         , "ipkg File    : \{ipkg.file}"

170 |         ] ++ (catMaybes [testFile t])

172 |   Core _            => [

173 |     "Type         : Idris core package"

174 |   ]

176 | namePlusModules : String -> QPkg -> String

177 | namePlusModules n qp =

178 |   unlines $  nameStr qp :: map (indent 2) (prettyModules n qp)

180 | keep : QueryMode -> String -> QPkg -> Bool

181 | keep PkgName    q p = isInfixOf q (nameStr p)

182 | keep Dependency q p = any ((q ==) . value) (dependencies p)

183 | keep Module     q p = any (isInfixOf q . show . fst) (modules p.lib.desc.desc)

186 | resultString :

187 |      {auto e : Env}

188 |   -> (query : String)

189 |   -> QueryMode

190 |   -> Hash

191 |   -> (parents, children : Tree PkgName)

192 |   -> QPkg

193 |   -> String

194 | resultString q Module h _  _  qp = namePlusModules q qp

195 | resultString _ _      h ps cs qp = case e.config.queryType of

196 |   NameOnly => nameStr qp

198 |   ShortDesc =>

199 |     let Just d := shortDesc qp | Nothing => nameStr qp

200 |      in "\{name qp}\n  \{d}\n"

202 |   Dependencies =>

203 |     let ds@(_ :: _) := dependencies qp | [] => nameStr qp

204 |      in unlines $  nameStr qp :: map (indent 2 . interpolate) ds

206 |   Details => unlines . (nameStr qp ::) . map (indent 2) $ concat [

207 |       toList (("Brief        : " ++) <$> shortDesc qp)

208 |     , details h qp

209 |     , libStatus qp

210 |     , appStatus qp

211 |     , prettyDeps qp

212 |     ]

214 |   Ipkg => unlines $ nameStr qp :: map (indent 2) (lines qp.lib.desc.cont)

216 |   Tree => case filter ("base" /=) cs of

217 |     Just tr' => prettyTree False tr'

218 |     Nothing  => prettyTree False cs

220 |   ReverseTree => case filter ("base" /=) ps of

221 |     Just tr' => prettyTree True tr'

222 |     Nothing  => prettyTree True ps

224 | export covering

225 | query :

226 |      {auto _ : HasIO io}

227 |   -> QueryMode

228 |   -> String

229 |   -> Env

230 |   -> EitherT PackErr io ()

231 | query m n e = do

232 |   ss <- query_ $ \h,ps,cs,p => toMaybe (keep m n p) (resultString n m h ps cs p)

233 |   putStrLn $ unlines ss

239 | instLib : QPkg -> Maybe String

240 | instLib qp = case qp.lib.status of

241 |   Installed _ _ => Just "\{qp.lib.name}"

242 |   Missing     _ => Nothing

244 | instApp : QPkg -> Maybe String

245 | instApp (QP lib $ Just (AI _ st))  = case st of

246 |   Installed    _ => Just "\{lib.name} (not on $PATH)"

247 |   BinInstalled _ => Just "\{lib.name}"

248 |   Missing      _ => Nothing

249 | instApp _ = Nothing

251 | apps : List QPkg -> String

252 | apps ps = case mapMaybe instApp ps of

253 |   []      => ""

254 |   x :: xs => unlines $

255 |     "\n\nInstalled Apps      : \{x}" ::

256 |     map (indent 22) xs

258 | libs : List QPkg -> String

259 | libs ps = case mapMaybe instLib ps of

260 |   []      => ""

261 |   x :: xs => unlines $

262 |     "\nInstalled Libraries : \{x}" ::

263 |     map (indent 22) xs

266 | infoString : (e : Env) => List QPkg -> String

267 | infoString ps = """

274 |   """ ++ apps ps ++ libs ps

276 | export covering

277 | printInfo : HasIO io => Env -> EitherT PackErr io ()

278 | printInfo e = resolveAll >>= putStrLn . infoString . snd

285 | installedPkgs :

286 |      {auto _ : HasIO io}

287 |   -> {auto _ : IdrisEnv}

288 |   -> List PkgName

289 |   -> EitherT PackErr io (List QPkg, List QPkg)

290 | installedPkgs ns = do

291 |   all <- filter installedLib . snd <$> resolveAll

292 |   pure (all, filter inPkgs all)

293 |   where inPkgs : QPkg -> Bool

294 |         inPkgs qp = isNil ns || elem (name qp) ns

296 | imports : QPkg -> String

297 | imports = unlines . map ("import " ++) . modules

299 | pre : String

300 | pre = "Main> "

302 | noOut : String

303 | noOut = "Main> \nMain> \n"

305 | removePre : String -> String

306 | removePre s = case isPrefixOf pre s of

307 |   True  => pack . drop (length pre) $ unpack s

308 |   False => s

310 | fuzzyTrim : String -> String

311 | fuzzyTrim =

312 |     unlines

313 |   . map removePre

314 |   . filter (pre /=)

315 |   . lines

317 | fuzzyPkg :

318 |      {auto _ : HasIO io}

319 |   -> {auto _ : IdrisEnv}

320 |   -> String

321 |   -> (allPkgs   : List QPkg)

322 |   -> QPkg

323 |   -> EitherT PackErr io ()

324 | fuzzyPkg q allPkgs qp = do

325 |   mkDir tmpDir

326 |   finally (rmDir tmpDir) $ inDir tmpDir $ \d => do

327 |     putStrLn "\{name qp}:\n"

328 |     write (MkF d "test.idr") (imports qp)

329 |     write (MkF d "input") ":fs \{q}\n"

331 |     (cmd,env) <- idrisWithPkgs (map lib allPkgs)

333 |     str <-

334 |       sysRunWithEnv

335 |         (cmd ++

336 |            [ "--quiet"

337 |            , "--no-prelude"

338 |            , "--no-banner"

339 |            , "test.idr"

340 |            , NoEscape "<"

341 |            , "input"

342 |            ]

343 |         )

344 |         env

345 |     case noOut == str of

346 |       True  => pure ()

347 |       False => putStrLn (fuzzyTrim str)

349 | export covering

350 | fuzzy :

351 |      {auto _ : HasIO io}

352 |   -> List PkgName

353 |   -> String

354 |   -> IdrisEnv

355 |   -> EitherT PackErr io ()

356 | fuzzy m q e = do

357 |   (allPkgs,rps) <- installedPkgs m

358 |   traverse_ (fuzzyPkg q allPkgs) rps