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