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