0 | module Collie.Usage
 1 |
 2 | import Data.SnocList
 3 | import Data.List
 4 | import Data.String
 5 |
 6 | import Collie.Core
 7 |
 8 | import Data.SnocList
 9 | import Data.String
10 |
11 | %default total
12 |
13 | reflow : (width : Nat) -> String -> List String
14 | reflow w = map unwords . init . assert_total words
15 |   where
16 |     init : List String -> List (List String)
17 |     go : Nat -> SnocList String -> List String -> List (List String)
18 |
19 |     init [] = []
20 |     init (" " :: xs) = init xs -- remove initial space
21 |     init (x :: xs) = go (w `minus` length x) [< x] xs
22 |
23 |     go Z acc xs        = (acc <>> []) :: init xs
24 |     go n acc []        = [acc <>> []]
25 |     go n acc (x :: xs) =
26 |       let l = length x in
27 |       if n < l + 1 then (acc <>> []) :: init (x :: xs)
28 |       else go (assert_smaller n (n `minus` (1 + l))) (acc :< x) xs
29 |
30 | public export
31 | Printer : Type
32 | Printer = Nat -> List String
33 |
34 | mapFstAndRest : (fst, rest : a -> b) -> List a -> List b
35 | mapFstAndRest fst rest []  = []
36 | mapFstAndRest fst rest (x :: xs) = fst x :: map rest xs
37 |
38 | export
39 | namedBlock : (name : String) -> String -> (nameWidth, maxWidth : Nat) -> Printer
40 | namedBlock name text nameWidth maxWidth i
41 |   = let padInitial = 2 + nameWidth `minus` length name
42 |         padRest    = 2 + nameWidth
43 |     in mapFstAndRest ((indent i name ++) . (indent padInitial))
44 |                      (indent (i + padRest))
45 |                      (concat $ map (\u => if i + padRest + length u > maxWidth
46 |                                           then reflow (maxWidth `minus` (i + padRest)) u
47 |                                           else [u]) $ lines text)
48 |
49 |
50 | (.description) : Modifier str -> String
51 | (MkFlag   flg).description = flg.project "description"
52 | (MkOption opt).description = opt.project "description"
53 |
54 | maxNameWidth : Fields a -> Nat
55 | maxNameWidth xs = foldl (\ u,v => max u (length (fst v))) 0 xs
56 |
57 | export
58 | usageModifiers : Fields Modifier -> (nameWidth, maxWidth : Nat) -> Printer
59 | usageModifiers xs nameWidth maxWidth
60 |   = foldr (\(name ** mod),u,i =>
61 |     namedBlock name mod.description nameWidth maxWidth i ++ u i) (const []) xs
62 |
63 | export
64 | usageCommand :
65 |   {cmdName : String} -> Command cmdName ->
66 |   (nameWidth, maxWidth : Nat) -> Printer
67 | usageCommand cmd nameWidth maxWidth i =
68 |   let subWidth : Nat := max (maxNameWidth cmd.subcommands) (maxNameWidth cmd.modifiers) in
69 |   (namedBlock cmdName cmd.description nameWidth maxWidth i) ++
70 |   case assert_total (foldr (\ (_ ** u) => (usageCommand u subWidth maxWidth (2 + i) ++)) [] cmd.subcommands
71 |        , usageModifiers cmd.modifiers subWidth maxWidth (2 + i)) of
72 |     (a, b) => intercalate [""] $ filter ([] /=) [a, b]
73 |
74 | export
75 | (.usage) : {cmdName : String} -> {default 80 maxWidth : Nat} -> Command cmdName -> String
76 | cmd.usage = unlines $ usageCommand cmd (length cmdName) maxWidth 0
77 |