1local
2  open FunctionalRecordUpdate
3  fun makeUpdateT z = makeUpdate4 z
4in
5fun updateT z = let
6  fun from chattiness files_wmatches help tests =
7    {
8      chattiness = chattiness, files_wmatches = files_wmatches, help = help,
9      tests = tests
10    }
11  fun from' tests help files_wmatches chattiness =
12    {
13      chattiness = chattiness, files_wmatches = files_wmatches, help = help,
14      tests = tests
15    }
16  fun to f {chattiness, files_wmatches, help, tests} =
17    f chattiness files_wmatches help tests
18in
19  makeUpdateT (from, from', to)
20end z
21val U = U
22val $$ = $$
23end (* local *)
24
25
26fun warn s = TextIO.output(TextIO.stdErr, s ^ "\n")
27fun die s = (warn s; OS.Process.exit OS.Process.failure)
28fun succeed s = (print (s^"\n"); OS.Process.exit OS.Process.success)
29
30type checkfn = bool -> string -> int -> (string * Substring.substring) -> bool
31
32type t = {
33  chattiness : int,
34  files_wmatches : bool,
35  help : bool,
36  tests : (string * (checkfn * string)) list
37};
38
39
40(* acceptable Unicode characters are
41
42                  UTF-8
43    ���   U+2018   0xE28098
44    ���   U+2019   0xE28099
45    ���   U+201C   0xE2809C
46    ���   U+201D   0xE2809D
47*)
48
49fun includes_unicode s =
50  let
51    val sz = size s
52    fun recurse i =
53      if i = sz then false
54      else
55        let val c = ord (String.sub(s,i))
56        in
57          if c = 0xE2 then quote_char2 (i + 1)
58          else if c > 127 then true
59          else recurse (i + 1)
60        end
61    and quote_char2 i =
62        if i = sz then true
63        else if ord (String.sub(s,i)) = 0x80 then quote_char3 (i + 1)
64        else true
65    and quote_char3 i =
66        if i = sz then true
67        else
68          let val c = ord (String.sub(s,i))
69          in
70            if c = 0x98 orelse c = 0x99 orelse c = 0x9C orelse c = 0x9D then
71              recurse (i + 1)
72            else true
73          end
74  in
75    recurse 0
76  end
77
78fun line_error qp fname linenum tag line =
79  if qp then false
80  else
81    (print (fname^":"^Int.toString linenum^": " ^ tag ^ ": " ^ line);
82     false)
83
84
85fun check_unicode qp fname linenum (line,ss) =
86  let
87    val (p,s) = Substring.position "UOK" ss
88  in
89    if Substring.size s <> 0 then true
90    else
91      if includes_unicode line then
92        line_error qp fname linenum "Unicode violation" line
93      else true
94  end
95
96fun check_tabs qp fname linenum (line,ss) =
97  let
98    open Holmake_tools
99    val (p,s) = Substring.position "\t" ss
100    val highlightTAB =
101        String.translate (fn c => if c = #"\t" then boldred "\\t" else str c)
102  in
103    if Substring.size s = 0 then true
104    else
105      line_error qp fname linenum "Includes TAB" (highlightTAB line)
106  end
107
108fun check_length qp fname linenum (line,ss) =
109  let
110    val sz = String.size line
111  in
112    if String.sub(line, sz - 1) <> #"\n" then
113      line_error qp fname linenum "Last char not NL" line
114    else if sz > 81 then
115      line_error qp fname linenum "Line-length > 80" line
116    else true
117  end
118
119fun check_twspace qp fname linenum (line,ss) =
120  let
121    val sz = String.size line
122    val pos = if String.sub(line,sz - 1) = #"\n" then sz - 2 else sz - 1
123  in
124    if pos >= 0 andalso Char.isSpace (String.sub(line, pos)) then
125      line_error qp fname linenum "Trailing whitespace" line
126    else true
127  end
128
129fun inc k m =
130  case Binarymap.peek(m,k) of
131      NONE => Binarymap.insert(m,k,1)
132    | SOME i => Binarymap.insert(m,k,i+1)
133
134fun checkfile (opts as {chattiness,files_wmatches,...}:t) sofar fname =
135  let
136    val istrm = TextIO.openIn fname
137    fun recurse linenum tags sofar =
138      case TextIO.inputLine istrm of
139          NONE =>
140          let
141            fun tagfold (k,v,acc) = (k ^ "(" ^ Int.toString v ^ ")") :: acc
142            val tagdump = Binarymap.foldr tagfold [] tags
143          in
144            TextIO.closeIn istrm;
145            if files_wmatches andalso not (null tagdump) then
146              print (fname ^ ": " ^ String.concatWith ", " tagdump ^ "\n")
147            else ();
148            sofar
149          end
150        | SOME line =>
151          let
152            val ss = Substring.full line
153            val qp = (chattiness = 0) orelse files_wmatches
154            fun foldthis ((_, (f, tag)), (b, tags)) =
155              let
156                val b' = f qp fname linenum (line,ss)
157              in
158                (b andalso b', if not b' then inc tag tags else tags)
159              end
160            val (c, tags) = List.foldl foldthis (true, tags) (#tests opts)
161          in
162            if not c andalso chattiness = 0 then
163              (TextIO.closeIn istrm; false)
164            else
165              recurse (linenum + 1) tags (c andalso sofar)
166          end
167  in
168    recurse 1 (Binarymap.mkDict String.compare) sofar
169  end
170
171fun is_generated opts fname =
172  let
173    open String
174    val {base,ext} = OS.Path.splitBaseExt fname
175    fun suff s = isSuffix s base
176    fun suffs sl = List.exists suff sl
177  in
178    case ext of
179        SOME "uo" => true
180      | SOME "ui" => true
181      | SOME "sig" => suffs ["Theory", "ML"]
182      | SOME "sml" => suffs [".lex", ".grm", ".grm-sig", "Theory", "ML"]
183      | _ => false
184  end
185
186
187fun do_dirstream opts dname ds sofar wlist =
188  let
189    fun recurse sofar dworklist =
190      case OS.FileSys.readDir ds of
191          NONE => (OS.FileSys.closeDir ds; (sofar, dworklist))
192        | SOME fname =>
193          let
194            val fullp = OS.Path.concat(dname, fname)
195          in
196            if OS.FileSys.isLink fullp then recurse sofar dworklist
197            else if OS.FileSys.isDir fullp then recurse sofar (fullp::dworklist)
198            else
199              let
200                val {base,ext} = OS.Path.splitBaseExt fname
201              in
202                if (ext = SOME "sml" orelse ext = SOME "sig") andalso
203                   not (is_generated opts fname) andalso
204                   fname <> "selftest.sml" andalso
205                   fname <> "EmitTeX.sml"
206                then
207                  recurse (checkfile opts sofar fullp) dworklist
208                else
209                  recurse sofar dworklist
210              end
211          end
212  in
213    recurse sofar wlist
214  end
215and do_dirs (opts:t) sofar wlist =
216    case wlist of
217        [] => sofar
218      | d::res =>
219        let
220          val ds = OS.FileSys.openDir d
221          val _ = if #chattiness opts > 1 then warn ("Checking "^d) else ()
222          val (sofar, wlist) = do_dirstream opts d ds sofar res
223        in
224          do_dirs opts sofar wlist
225        end
226
227fun fupdbool sel b t = updateT t (U sel b) $$
228fun fupdchattiness c t = updateT t (U #chattiness c) $$
229
230val default : t =
231    { help = false, chattiness = 1, files_wmatches = false,
232      tests = [("unicode", (check_unicode, "Unicode present")),
233               ("tabs", (check_tabs, "TAB present")),
234               ("linelength", (check_length, "Line too long (or no final NL)")),
235               ("trailing_wspace", (check_twspace, "Trailing whitespace"))]
236    }
237
238fun remove_test s sl =
239  case sl of
240      [] => []
241    | (s',f) :: rest => if s' = s then rest else (s',f) :: remove_test s rest
242
243fun fupdtests f t = updateT t (U #tests (f (#tests t))) $$
244
245val options = let
246  open GetOpt
247in
248  [
249    {help = "show this message", long = ["help"], short = "h?",
250     desc = NoArg (fn () => fupdbool #help true)},
251    {help = "Just print files with problems", long = ["files-with-matches"],
252     short = "l", desc = NoArg (fn () => fupdbool #files_wmatches true)},
253    {help = "No line-length check", long = ["nolinelen"], short = "",
254     desc = NoArg (fn () => fupdtests (remove_test "linelength"))},
255    {help = "be less chatty", long = ["quiet"], short = "q",
256     desc = NoArg (fn () => fupdchattiness 0)},
257    {help = "allow Unicode", long = ["unicodeok"], short = "u",
258     desc = NoArg (fn () => fupdtests (remove_test "unicode"))},
259    {help = "be more verbose", long = [], short = "v",
260     desc = NoArg (fn () => fupdchattiness 2)}
261  ]
262end
263
264fun usage_str() =
265  GetOpt.usageInfo {
266    header =
267        "Usage:\n\
268        \  " ^ CommandLine.name() ^ " [options] dir1 dir2 .. dirn\n\n\
269        \Recursively grep over dirs looking for style violations.",
270    options = options
271  }
272
273fun read_cline args =
274  GetOpt.getOpt { argOrder = GetOpt.Permute,
275                  options = options,
276                  errFn = warn }
277                args
278
279
280
281fun main() =
282  let
283    val (upds, args) = read_cline(CommandLine.arguments())
284    val opts = List.foldl (fn (f,a) => f a) default upds
285  in
286    if #help opts then succeed (usage_str())
287    else if null args then die (usage_str())
288    else
289      let
290        val result = do_dirs opts true args
291      in
292        OS.Process.exit
293          (if result then OS.Process.success else OS.Process.failure)
294      end
295  end
296
297
298(*
299#!/bin/bash
300
301if [ $# -eq 1 ]
302then
303    if [ $1 = "-h" -o $1 = "-?" ]
304    then
305        echo "Usage:"
306        echo "  $0 dir1 dir2 .. dirn"
307        echo
308        echo "Recursively grep over dirs looking for non-ASCII characters"
309        echo "If no directories given, run in HOL's src directory"
310        exit 0
311    fi
312fi
313
314cmd="grep -R -n -v -E '^[[:print:][:space:]]*$|UOK' --include='*.sml' --exclude='*Theory.sml' --exclude='*Theory.sig' --exclude selftest.sml --exclude EmitTeX.sml"
315
316if [ $# -eq 0 ]
317then
318    LC_ALL=C eval $cmd $(dirname $0)/../src/
319else
320    LC_ALL=C eval $cmd "$@"
321fi
322*)
323