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