1open Lib Type PP smpp PPBackEnd testutils 2 3(* -------------------------------------------------------------------------- *) 4(* Test code for terminal styles *) 5(* -------------------------------------------------------------------------- *) 6 7val color_name_fw_spaces = " "; 8fun color_name_fw Black = "Black " 9 | color_name_fw RedBrown = "RedBrown " 10 | color_name_fw Green = "Green " 11 | color_name_fw BrownGreen = "BrownGreen" 12 | color_name_fw DarkBlue = "DarkBlue " 13 | color_name_fw Purple = "Purple " 14 | color_name_fw BlueGreen = "BlueGreen " 15 | color_name_fw DarkGrey = "DarkGrey " 16 | color_name_fw LightGrey = "LightGrey " 17 | color_name_fw OrangeRed = "OrangeRed " 18 | color_name_fw VividGreen = "VividGreen" 19 | color_name_fw Yellow = "Yellow " 20 | color_name_fw Blue = "Blue " 21 | color_name_fw PinkPurple = "PinkPurple" 22 | color_name_fw LightBlue = "LightBlue " 23 | color_name_fw White = "White "; 24 25 26val color_list = 27 [ Black , RedBrown , Green , BrownGreen, 28 DarkBlue , Purple , BlueGreen , DarkGrey, 29 LightGrey , OrangeRed , VividGreen , Yellow, 30 Blue , PinkPurple , LightBlue , White] 31 32val _ = tprint "Basic vt100 style" 33val s = HOLPP.pp_to_string 34 70 35 (fn s => Parse.mlower 36 (#ustyle vt100_terminal [FG Blue] (smpp.add_string s))) 37 "should be blue" 38val _ = if s = "\027[0;1;34mshould be blue\027[0m" then OK() 39 else die "FAILED!"; 40 41 42fun test_terminal test_bg (terminal:t) = 43let 44 val {add_string, add_xstring, add_newline, add_break, 45 ustyle, ublock, ...} = terminal 46 fun add_ann_string (s,ann) = add_xstring {s=s,ann=SOME ann,sz=NONE} 47 48 val fg_styles = 49 ((" - "^color_name_fw_spaces), []):: 50 map (fn c => 51 ((" - Foreground "^(color_name_fw c)), [FG c])) color_list 52 val bold_fg_styles = 53 (map (fn (s, styL) => (" - "^s, styL)) fg_styles)@ 54 (map (fn (s, styL) => (" - Bold"^s, Bold::styL)) fg_styles) 55 val und_fg_styles = 56 (map (fn (s, styL) => (" "^s, styL)) bold_fg_styles)@ 57 (map (fn (s, styL) => ("Underline"^s, Underline::styL)) bold_fg_styles) 58 59 val full_styles = if not test_bg then und_fg_styles else 60 (flatten ( 61 (map (fn (s, styL) => 62 ((s^" - "^color_name_fw_spaces), styL)) und_fg_styles):: 63 (map (fn c => 64 map (fn (s, styL) => 65 ((s^" - Background "^(color_name_fw c)), (BG c)::styL)) und_fg_styles) 66 color_list))) 67 val m = 68 ublock INCONSISTENT 0 ( 69 add_string "Terminal testing" >> add_newline >> 70 add_string "================" >> add_newline >> add_newline >> 71 72 add_string "Annotations:" >> add_newline >> 73 add_string "------------" >> add_newline >> 74 add_ann_string ("Bound variable", BV (bool, fn () => ": bool")) >> 75 add_newline >> 76 add_ann_string ("Free variable", FV (bool, fn () => ": bool")) >> 77 add_newline >> 78 add_ann_string ("Type variable", TyV) >> 79 add_newline >> 80 add_ann_string ("TySyn", TySyn (fn () => "TySyn")) >> 81 add_newline >> 82 add_ann_string ("TyOp", TyOp (fn () => "TyOp")) >> 83 add_newline >> 84 add_ann_string ("Const", Const {Name = "test-name", Thy = "test-thy", 85 Ty = (Type.bool, fn () => "bool")}) >> 86 add_newline >> 87 add_ann_string ("Note", Note "Some note") >> 88 add_newline >> 89 90 add_newline >> add_newline >> 91 92 add_string "Basic styles:" >> add_newline >> 93 add_string "-------------" >> add_newline >> 94 add_string "default style" >> add_newline >> 95 ustyle [Bold] (add_string "Bold") >> add_newline >> 96 ustyle [Underline] (add_string "Underline") >> add_newline >> 97 mapp (fn c => ( 98 add_string "Foreground " >> 99 ustyle [FG c] (add_string (color_name_fw c)) >> 100 add_newline)) 101 color_list >> 102 mapp (fn c => ( 103 add_string "Background " >> 104 ustyle [BG c] (add_string (color_name_fw c)) >> 105 add_newline)) color_list >> 106 add_newline >> add_newline >> 107 108 (if test_bg then 109 add_string "All style combinations:" >> add_newline >> 110 add_string "------------------------" >> add_newline 111 else 112 add_string "All style combinations (without background color):" >> 113 add_newline >> 114 add_string "--------------------------------------------------" >> 115 add_newline) >> 116 mapp (fn (s, styL) => ustyle styL (add_string s) >> add_newline) 117 full_styles >> 118 add_newline >> add_newline 119 ) 120in 121 HOLPP.prettyPrint (TextIO.print, 75) (Parse.mlower m) 122end; 123 124 125val _ = print "raw terminal\n"; 126val _ = print "============\n\n"; 127val _ = test_terminal false (PPBackEnd.raw_terminal); 128 129val _ = print "emacs terminal\n"; 130val _ = print "==============\n\n"; 131val _ = test_terminal false (PPBackEnd.emacs_terminal); 132 133val _ = print "vt100 terminal\n"; 134val _ = print "==============\n\n"; 135val _ = test_terminal false (PPBackEnd.vt100_terminal); 136 137 138 139(* ---------------------------------------------------------------------- 140 Tests of the base lexer 141 ---------------------------------------------------------------------- *) 142 143val _ = print "** Testing basic lexing functionality\n\n" 144open base_tokens 145 146exception InternalDie of string 147fun idie s = raise InternalDie s 148 149fun quoteToString [QUOTE s] = "`"^s^"`" 150 | quoteToString _ = idie "Bad test quotation" 151 152fun test (q, slist) = let 153 val _ = tprint ("Testing " ^ quoteToString q) 154 fun prs s = "\"" ^ String.toString s ^ "\"" 155 fun prsl sl = "[" ^ String.concatWith ", " (map prs sl) ^ "]" 156in 157 require_msg (check_result (equal slist)) prsl 158 (map (base_tokens.toString o #1) o qbuf.lex_to_toklist) q 159end handle InternalDie s => die s 160 161val _ = app test [(`abc`, ["abc"]), 162 (`12`, ["12"]), 163 (`3.0`, ["3.0"]), 164 (`3.00`, ["3.00"]), 165 (`0xab`, ["171"]), 166 (`12.1`, ["12.1"]), 167 (`12.01`, ["12.01"]), 168 (`12.010`, ["12.010"]), 169 (`(`, ["("]), 170 (`a(a`, ["a(a"]), 171 (`x+y`, ["x+y"]), 172 (`x +y`, ["x", "+y"]), 173 (`x ++ y`, ["x", "++", "y"]), 174 (`x (* *)y`, ["x", "y"]), 175 (`x(**)y`, ["x", "y"]), 176 (`+(**)y`, ["+", "y"]), 177 (`((*x*)`, ["("]), 178 (`+(%*%((*"*)-*foo`,["+(%*%(", "-*foo"]), 179 (`"(*"`, ["BTStrL(\",\"(*\")"]), 180 (`foo$bar`, ["foo$bar"]), 181 (`+foo$bar`, ["+", "foo$bar"]), 182 (`+foo$bar+`, ["+", "foo$bar", "+"]) 183 ] 184 185(* tests of the term lexer *) 186local 187 open term_tokens 188 fun prtoks l = 189 "["^ String.concatWith ", " (map (toString (fn _ => "()")) l) ^ "]" 190 val testf = lextest ["--b->", "=��=>���", "(<", ">)", "-->"] 191 192fun test (s, toklist : unit term_token list) = let 193 val _ = tprint ("Term token testing " ^ Lib.quote (String.toString s)) 194in 195 require_msg (check_result (equal toklist)) prtoks testf s 196end 197 198fun failtest (s, substring) = 199 let 200 fun pr s = "Testing failing lex of " ^ Lib.quote (String.toString s) 201 fun check substring (LEX_ERR(s, _)) = 202 String.isSubstring substring s 203 | check _ _ = false 204 in 205 shouldfail {testfn = testf, printresult = prtoks, printarg = pr, 206 checkexn = check substring} 207 s 208 end 209 210val ai = Arbnum.fromInt 211fun snum i = Numeral(ai i, NONE) 212fun stdstr s = StrLit{ldelim = "\"", contents = s} 213fun charstr s = StrLit{ldelim = "#\"", contents = s} 214fun guillstr s = StrLit{ldelim = "��", contents = s} 215fun sguillstr s = StrLit{ldelim = "���", contents = s} 216in 217val _ = app (ignore o test) [ 218 ("abc", [Ident "abc"]), 219 ("���", [Ident "\226\128\153"]), 220 ("\"\\172\"", [stdstr "\172"]), 221 ("#\"c\"", [charstr "c"]), 222 ("f#\"c\"", [Ident "f", charstr "c"]), 223 ("f(#\"c\"", [Ident "f", Ident "(", charstr "c"]), 224 ("(\"ab\\172\"++z)", 225 [Ident "(", stdstr "ab\172", Ident "++", Ident "z", Ident ")"]), 226 ("f\"ab\\172x\"++", [Ident "f", stdstr "ab\172x", Ident "++"]), 227 ("+\"ab\\172\"++", [Ident "+", stdstr "ab\172", Ident "++"]), 228 ("$+\"ab\\172\"++", [Ident "$+", stdstr "ab\172", Ident "++"]), 229 ("12", [snum 12]), 230 ("-12", [Ident "-", snum 12]), 231 ("((-12", [Ident "(", Ident "(", Ident "-", snum 12]), 232 ("0a", [Numeral(ai 0, SOME #"a")]), 233 ("0", [snum 0]), 234 ("(0xF", [Ident "(", snum 15]), 235 ("01", [snum 1]), 236 ("1.2", [Fraction{wholepart = ai 1, fracpart = ai 2, places = 1}]), 237 ("-1.2", [Ident "-", 238 Fraction{wholepart = ai 1, fracpart = ai 2, places = 1}]), 239 ("~1.2", [Ident "~", 240 Fraction{wholepart = ai 1, fracpart = ai 2, places = 1}]), 241 ("(2n*e", [Ident "(", Numeral (ai 2, SOME #"n"), Ident "*", Ident "e"]), 242 ("2_001", [snum 2001]), 243 ("2.000_023", [Fraction{wholepart = ai 2, places = 6, fracpart = ai 23}]), 244 ("(", [Ident "("]), 245 (".", [Ident "."]), 246 ("0.", [snum 0, Ident "."]), 247 ("a0.", [Ident "a0", Ident "."]), 248 ("-0.", [Ident "-", snum 0, Ident "."]), 249 ("{2.3", 250 [Ident "{", Fraction{wholepart = ai 2, places = 1, fracpart = ai 3}]), 251 ("(a+1", [Ident "(", Ident"a", Ident"+", snum 1]), 252 ("a--b->c", [Ident "a", Ident"--b->", Ident"c"]), 253 ("(+)", [Ident "(", Ident "+", Ident ")"]), 254 ("$ $$ $$$ $+ $if $a", 255 [Ident "$", Ident "$$", Ident "$$$", Ident "$+", Ident "$if", 256 Ident "$a"]), 257 ("thy$id", [QIdent("thy", "id")]), 258 ("(thy$id", [Ident "(", QIdent("thy", "id")]), 259 ("(thy$id +", [Ident "(", QIdent("thy", "id"), Ident "+"]), 260 ("(thy$id+", [Ident "(", QIdent("thy", "id"), Ident "+"]), 261 ("+thy$id", [Ident "+", QIdent("thy", "id")]), 262 ("thy$0", [QIdent("thy", "0")]), 263 ("(thy$id\"foo\"", [Ident "(", QIdent ("thy", "id"), stdstr "foo"]), 264 ("(thy$id#\"f\"", [Ident "(", QIdent ("thy", "id"), charstr "f"]), 265 ("(thy$id��foo b��", [Ident "(", QIdent ("thy", "id"), guillstr "foo b"]), 266 ("x+�� f��", [Ident "x", Ident "+", guillstr " f"]), 267 ("(thy$id���foo b���", [Ident "(", QIdent ("thy", "id"), sguillstr "foo b"]), 268 ("x+��� f���", [Ident "x", Ident "+", sguillstr " f"]), 269 ("foo$bar<foo$baz", [QIdent ("foo", "bar"), Ident "<", 270 QIdent ("foo", "baz")]), 271 ("(bool$/\\", [Ident "(", QIdent ("bool", "/\\")]), 272 ("*foo$bar<foo$baz", [Ident "*", QIdent ("foo", "bar"), Ident "<", 273 QIdent ("foo", "baz")]), 274 ("nm_sub$id", [QIdent ("nm_sub", "id")]), 275 ("+nm$id\"bar\"", [Ident "+", QIdent ("nm", "id"), stdstr "bar"]), 276 ("+nm$id\"\"", [Ident "+", QIdent ("nm", "id"), stdstr ""]), 277 ("nm$**", [QIdent("nm", "**")]), 278 ("$+a", [Ident "$+", Ident "a"]), 279 ("$==>", [Ident "$==>"]), 280 ("bool$~", [QIdent("bool", "~")]), 281 ("$~", [Ident "$~"]), 282 ("$��", [Ident "$��"]), 283 ("(<a+b>)", [Ident "(<", Ident "a", Ident "+", Ident "b", Ident ">)"]), 284 ("f(<a+b>)", [Ident "f", Ident "(<", Ident "a", Ident "+", Ident "b", 285 Ident ">)"]), 286 ("+(<a+b>)", [Ident "+", Ident "(<", Ident "a", Ident "+", Ident "b", 287 Ident ">)"]), 288 ("((<a+b>)", [Ident "(", Ident "(<", Ident "a", Ident "+", Ident "b", 289 Ident ">)"]), 290 ("::_", [Ident "::", Ident "_"]), (* case pattern with CONS *) 291 ("=\"\"", [Ident "=", stdstr ""]), (* e.g., stringScript *) 292 ("$-->", [Ident "$-->"]), (* e.g., quotientScript *) 293 ("$var$(ab)", [Ident "ab"]), 294 ("$var$(ab\\nc)", [Ident "ab\nc"]), 295 ("$var$(ab\\nc\\))", [Ident "ab\nc)"]), 296 ("$var$(% foo )", [Ident "% foo "]), 297 ("$var$(% foo* )", [Ident "% foo* "]), 298 ("$var$(% foo*\\z)", [Ident "% foo*"]), 299 ("$var$(((foo)", [Ident "((foo"]), 300 ("$var$(foo\"bar)", [Ident "foo\"bar"]), 301 ("$var$(foo\\172bar)", [Ident "foo\172bar"]), 302 ("($var$(foo\"bar)", [Ident "(", Ident "foo\"bar"]), 303 ("$$var$(foo\"bar)", [Ident "$foo\"bar"]), 304 ("(')", [Ident "(", Ident "'", Ident ")"]), (* e.g., finite_mapScript *) 305 ("��x.x", [Ident "��", Ident "x", Ident ".", Ident "x"]), 306 ("x'0,y)", [Ident "x'0", Ident ",", Ident "y", Ident ")"]), 307 ("x'0)", [Ident "x'0", Ident ")"]), 308 ("(x'0)", [Ident "(", Ident "x'0", Ident ")"]), 309 ("x'��,y)", [Ident "x'", Ident "��", Ident ",", Ident "y", Ident ")"]), 310 ("x'", [Ident "x'"]), 311 ("x''", [Ident "x''"]), 312 ("x'3'", [Ident "x'''"]), 313 ("xa'3'a'", [Ident "xa'3'a'"]), 314 ("x'���'", [Ident "x''''"]), 315 ("map:=��h.", [Ident "map", Ident ":=", Ident "��", Ident "h", Ident "."]), 316 ("map:=\\h.", [Ident "map", Ident ":=\\", Ident "h", Ident "."]) 317 ] 318val _ = List.app (ignore o failtest) [ 319 ("thy$$$", "qualified ident"), 320 ("$var$(ab\n c)", "quoted variable"), 321 ("'a", "can't begin with prime"), 322 ("thy$1", "qualified ident") 323] 324end (* local - tests of term lexer *) 325 326(* tests of type lexer *) 327val _ = let 328 open type_tokens 329 fun prtoklist ts = 330 "[" ^ String.concatWith ", " (map (token_string (fn _ => "_")) ts) ^ "]" 331 fun test (s,toklist) = 332 (tprint ("Type-lexing \"" ^ s ^ "\""); 333 require_msg (check_result (equal toklist)) prtoklist lextest s) 334in 335 List.app (ignore o test) [ 336 ("bool", [TypeIdent "bool"]), 337 ("min$bool", [QTypeIdent("min", "bool")]), 338 ("��", [TypeVar "��"]), 339 ("'a", [TypeVar "'a"]), 340 ("bool->'a", [TypeIdent "bool", TypeSymbol "->", TypeVar "'a"]), 341 ("min$bool1->min$bool2", [QTypeIdent("min", "bool1"), TypeSymbol "->", 342 QTypeIdent("min", "bool2")]), 343 ("(��,bool)fun", [LParen, TypeVar "��", Comma, TypeIdent "bool", RParen, 344 TypeIdent "fun"]), 345 ("(foo$ty2,foo$ty2) ty1", 346 [LParen, QTypeIdent("foo", "ty2"), Comma, QTypeIdent("foo", "ty2"), 347 RParen, TypeIdent"ty1"]) 348 ] 349end (* let - tests of type lexer *) 350 351val g0 = term_grammar.stdhol; 352fun mTOK s = term_grammar_dtype.RE (HOLgrammars.TOK s) 353val mTM = term_grammar_dtype.RE HOLgrammars.TM 354 355local 356 open term_grammar term_grammar_dtype 357in 358val cond_g = 359 add_rule { 360 term_name = "COND", 361 fixity = Prefix 70, 362 pp_elements = [PPBlock([mTOK "if", BreakSpace(1,2), mTM, 363 BreakSpace(1,0), 364 mTOK "then"], (CONSISTENT, 0)), 365 BreakSpace(1,2), mTM, BreakSpace(1,0), 366 mTOK "else", BreakSpace(1,2)], 367 paren_style = OnlyIfNecessary, 368 block_style = (AroundEachPhrase, (CONSISTENT, 0))} g0 369val let_g = 370 add_rule { pp_elements = [mTOK "let", 371 ListForm { 372 separator = [mTOK ";"], 373 cons = GrammarSpecials.letcons_special, 374 nilstr = GrammarSpecials.letnil_special, 375 block_info = (INCONSISTENT, 0)}, 376 mTOK "in"], 377 term_name = GrammarSpecials.let_special, 378 paren_style = OnlyIfNecessary, fixity = Prefix 8, 379 block_style = (AroundEachPhrase, (CONSISTENT, 0))} g0 380val lf_g = add_listform g0 381 { block_info = (CONSISTENT, 0), 382 separator = [mTOK ";", BreakSpace(1,0)], 383 leftdelim = [mTOK "["], 384 rightdelim= [mTOK "]"], 385 nilstr = "NIL", cons = "CONS"} 386end; 387fun isabsynlist slist a = 388 let 389 open Absyn 390 in 391 case slist of 392 [] => (case a of IDENT (_, "NIL") => true | _ => false) 393 | s1 :: rest => 394 (case a of 395 APP(_, APP (_, IDENT(_, "CONS"), IDENT (_, el1)), a_rest) => 396 el1 = s1 andalso isabsynlist rest a_rest 397 | _ => false) 398 end 399val _ = PP.prettyPrint 400 (print, 75) 401 (Parse.mlower 402 (term_grammar.prettyprint_grammar 403 (fn g =>fn _ => smpp.add_string "<term>") 404 lf_g)) 405 406fun parsetest sl = 407 let 408 val s = "["^String.concatWith ";" sl^"]" 409 val _ = tprint ("Parsing "^s) 410 val a = TermParse.absyn lf_g type_grammar.min_grammar [QUOTE s] 411 in 412 if isabsynlist sl a then OK() else die "FAILED!" 413 end 414 415val _ = parsetest [] 416val _ = parsetest (map str (explode "ab")) 417val _ = parsetest (map str (explode "abcdef")) 418 419fun find_named_rule nm g = 420 let 421 open term_grammar_dtype term_grammar 422 in 423 List.map 424 (fn PREFIX (STD_prefix rrs) => 425 List.filter (fn rr => #term_name rr = nm) rrs 426 | _ => []) 427 (grammar_rules g) |> List.concat 428 end; 429 430val _ = tprint "term_grammar.grammar_tokens (LET)" 431val _ = 432 let val result = term_grammar.grammar_tokens let_g 433 in 434 if Lib.set_eq result 435 ["\\", "|>", "<|", ")", "(", ".", ":", "updated_by", 436 ":=", "with", "let", "in", ";", "$"] 437 then OK() 438 else die ("\nFAILED ["^ 439 String.concatWith "," (map (fn s => "\""^s^"\"") result) ^ "]") 440 end; 441 442val _ = tprint "term_grammar.rule_elements (COND)" 443val cond_rule = hd (find_named_rule "COND" cond_g) 444val cond_rels = term_grammar.rule_elements (#elements cond_rule) 445val _ = let 446 open HOLgrammars 447in 448 if cond_rels = [TOK "if", TM, TOK "then", TM, TOK "else"] then OK() 449 else die "FAILED" 450end; 451 452val _ = tprint "PrecAnalysis.rule_equalities (COND)" 453val cond_eqns = PrecAnalysis.rule_equalities cond_rule 454val _ = if Lib.set_eq cond_eqns [("if", true, "then"), ("then", true, "else")] 455 then OK() 456 else die "FAILED"; 457 458val _ = tprint "term_grammar.rule_elements (LET)" 459val let_rule = hd (find_named_rule GrammarSpecials.let_special let_g) 460val let_rels = term_grammar.rule_elements (#elements let_rule) 461val _ = let 462 open HOLgrammars GrammarSpecials 463in 464 if let_rels = 465 [TOK"let", ListTM{nilstr=letnil_special, cons=letcons_special, sep=";"}, 466 TOK "in"] 467 then OK () 468 else die "FAILED" 469end; 470 471fun prlist eqns = 472 "[" ^ String.concatWith ", " 473 (map (fn (s1,b,s2) => "(\"" ^ s1 ^ "\"," ^ Bool.toString b ^ ",\"" ^ 474 s2 ^"\")") 475 eqns) ^ "]"; 476 477val _ = tprint "PrecAnalysis.rule_equalities (LET)" 478val let_eqns = PrecAnalysis.rule_equalities let_rule 479val _ = if Lib.set_eq let_eqns 480 [("let", true, ";"), (";", true, ";"), (";", true, "in"), 481 ("let", false, "in"), ("let", true, "in"), 482 (";", false, "in")] 483 then OK() 484 else die ("FAILED\n got: "^prlist let_eqns); 485 486val _ = tprint "term_grammar.rules_for (LET)" 487val let_rules = term_grammar.rules_for let_g GrammarSpecials.let_special 488val _ = if length let_rules = 1 then OK() else die "FAILED" 489 490val lsp1 = {nilstr="lnil",cons="lcons",sep=";"} 491val lsp2 = {nilstr="lnil2",cons="lcons2",sep=";;"} 492fun check (s1,s2) = 493 case (s1,s2) of 494 ("let", "in") => SOME lsp1 495 | ("in", "end") => SOME lsp2 496 | _ => NONE 497 498val f = PrecAnalysis.check_for_listreductions check 499 500open term_grammar_dtype GrammarSpecials 501val S = HOLPP.add_string 502fun prmsp {nilstr,cons,sep} = "{" ^ nilstr ^ "," ^ cons ^ "," ^ sep ^ "}" 503fun prlr (s1,s2,sp) = "(" ^ s1 ^ ", " ^ s2 ^ ", " ^ prmsp sp ^ ")" 504fun prlist p l = "[" ^ String.concatWith ", " (map p l) ^ "]" 505fun prlrs lrs = prlist prlr lrs 506fun prrel (TOK s) = "TOK \""^s^"\"" 507 | prrel TM = "TM" 508 | prrel _ = "<Unexpected rule-element>" 509fun prlspi (lsp,i1,i2) = 510 "(" ^ prmsp lsp ^ "," ^ Int.toString i1 ^ "," ^ Int.toString i2 ^ ")" 511fun prrm_result (rels,lspis) = 512 "(" ^ prlist prrel rels ^ ", " ^ prlist prlspi lspis ^ ")" 513fun require_msg_eqk v pr f k x = require_msgk (check_result (equal v)) pr f k x 514fun require_msg_eq v pr f x = require_msg_eqk v pr f (fn _ => ()) x 515fun require_eq v f x = require (check_result (equal v)) f x 516fun rmlistrels r i = PrecAnalysis.remove_listrels (Exn.release r) i 517 518fun listredn_test (nm, input, input', expected1, testseq) = 519 let 520 val _ = tprint ("check_for_listreductions (" ^ nm ^ ")") 521 fun kont result = 522 (tprint ("remove_listrels (" ^ nm ^ ")"); 523 require_msg_eq (input', testseq) (S o prrm_result) 524 (rmlistrels result) input) 525 in 526 require_msg_eqk expected1 (S o prlrs) f kont input 527 end 528val bare_let = [TOK "let", TM, TOK "in", TM] 529val suffix_let = [TM, TOK "let", TM, TOK "in"] 530 531val _ = List.app listredn_test [ 532 ("1 element prefix", [TOK "let", TM, TOK "in", TM], bare_let, 533 [("let", "in", lsp1)], [(lsp1, 0, 1)]), 534 ("0 element prefix", [TOK "let", TOK "in", TM], bare_let, 535 [("let", "in", lsp1)], [(lsp1, 0, 0)]), 536 ("1 element + ; prefix", [TOK "let", TM, TOK ";", TOK "in", TM], bare_let, 537 [("let", "in", lsp1)], [(lsp1, 0, 1)]), 538 ("2 element prefix", [TOK "let", TM, TOK ";", TM, TOK "in", TM], bare_let, 539 [("let", "in", lsp1)], [(lsp1, 0, 2)]), 540 ("1 element suffix", [TM, TOK "let", TM, TOK "in"], suffix_let, 541 [("let", "in", lsp1)], [(lsp1, 1, 1)]), 542 ("2 element suffix", [TM, TOK "let", TM, TOK ";", TM, TOK "in"], 543 suffix_let, [("let", "in", lsp1)], [(lsp1,1,2)]), 544 ("2 element + ; suffix", 545 [TM, TOK "let", TM, TOK ";", TM, TOK ";", TOK "in"], 546 suffix_let, [("let", "in", lsp1)], [(lsp1,1,2)]), 547 ("0 element suffix", [TM, TOK "let", TOK "in"], suffix_let, 548 [("let", "in", lsp1)], [(lsp1, 1, 0)]) 549 ] 550 551val mk_var = Term.mk_var 552val mk_comb = Term.mk_comb 553val bool = Type.bool 554val alpha = Type.alpha 555val CONS_t = mk_var("CONS", bool --> (bool --> bool)) 556val NIL_t = mk_var("NIL", bool) 557fun mk_list00 elty n c tmlist = 558 let 559 fun recurse ts = 560 case ts of 561 [] => Term.inst [alpha |-> elty] n 562 | x::xs => mk_comb(mk_comb(Term.inst [alpha |-> elty] c, x), 563 recurse xs) 564 in 565 recurse tmlist 566 end 567 568fun mk_list0 elty n c s = 569 mk_list00 elty n c (map (fn c => mk_var(str c, elty)) (String.explode s)) 570 571val mk_list = mk_list0 bool NIL_t CONS_t; 572 573fun tmprint g = 574 PP.pp_to_string 70 575 (fn t => 576 Parse.mlower 577 (term_pp.pp_term g 578 type_grammar.min_grammar 579 PPBackEnd.raw_terminal 580 t)) 581 582fun tpp msg expected g t = 583 let 584 val _ = tprint msg 585 val result = tmprint g t 586 in 587 if result = expected then OK() 588 else die ("\nFAILED - got >" ^ result ^"<") 589 end handle e => die ("EXN-FAILED: "^General.exnMessage e) 590 591val _ = tpp "Printing empty list form (var)" "[]" lf_g NIL_t 592val _ = tpp "Printing CONS-list form [x] (var)" "[x]" lf_g (mk_list "x") 593val _ = tpp "Printing CONS-list form [x;y] (var)" "[x; y]" lf_g (mk_list "xy") 594 595val cCONS_t = 596 Term.prim_new_const {Thy = "min", Name = "CONS"} (bool --> (bool --> bool)) 597val cNIL_t = Term.prim_new_const {Thy = "min", Name = "NIL"} bool 598val cmk_list = mk_list0 bool cNIL_t cCONS_t 599 600val _ = tpp "Printing nil (const, no overload)" "min$NIL" lf_g cNIL_t 601 602val lfco_g = lf_g |> term_grammar.fupdate_overload_info 603 (Overload.add_overloading ("NIL", cNIL_t)) 604 |> term_grammar.fupdate_overload_info 605 (Overload.add_overloading ("CONS", cCONS_t)); 606 607val _ = tpp "Printing nil (const, overload)" "[]" lfco_g cNIL_t 608val _ = tpp "Printing CONS-list [x] (const, overload)" "[x]" 609 lfco_g (cmk_list "x") 610 611(* listform, const, overload, nil overloaded again (as EMPTY is in pred_set) *) 612val lfcono_g = 613 lfco_g |> term_grammar.fupdate_overload_info 614 (Overload.add_overloading ("altNIL", cNIL_t)) 615 616val _ = tpp "Printing nil (const, double-overload)" "[x]" lfcono_g 617 (cmk_list "x") 618 619val cINS_t = Term.prim_new_const{Thy = "min", Name = "INS"} 620 (alpha --> (alpha --> bool) --> (alpha --> bool)) 621val cEMP_t = Term.prim_new_const{Thy = "min", Name = "EMP"} (alpha --> bool) 622fun add_setlistform g = 623 term_grammar.add_listform g { 624 block_info = (CONSISTENT, 0), 625 separator = [mTOK ";", BreakSpace(1,0)], 626 leftdelim = [mTOK "{"], 627 rightdelim= [mTOK "}"], 628 nilstr = "EMP", cons = "INS"} 629 |> term_grammar.fupdate_overload_info 630 (Overload.add_overloading ("EMP", cEMP_t)) 631 |> term_grammar.fupdate_overload_info 632 (Overload.add_overloading ("INS", cINS_t)) 633 634val lfcop_g = g0 |> add_setlistform 635 636 637val pbmk_list = mk_list0 bool cEMP_t cINS_t 638fun ptpp msg exp t = tpp msg exp lfcop_g t 639 640val _ = ptpp "Printing INS-list {x} (const, overload, polymorphic inst)" "{x}" 641 (pbmk_list "x") 642 643val _ = ptpp "Printing INS-list {x;y} (const, overload, polymorphic inst)" 644 "{x; y}" 645 (pbmk_list "xy") 646 647val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha)) 648val y = mk_var("y", bool) 649val bINS = Term.inst[alpha |-> bool] cINS_t 650val bEMP = Term.inst[alpha |-> bool] cEMP_t 651val l = mk_comb(mk_comb(bINS, fx), mk_comb(mk_comb(bINS, y), bEMP)) 652val _ = ptpp "Printing INS-list {f x;y} (const, overload, polymorphic inst)" 653 "{f x; y}" 654 655val lfcopuo_g = (* as before + Unicode-ish overload on EMP *) 656 lfcop_g 657 |> term_grammar.fupdate_overload_info 658 (Overload.add_overloading ("���", cEMP_t)) 659val _ = tpp "Printing INS-list (Unicode EMP) {x;y}" "{x; y}" 660 lfcopuo_g (pbmk_list "xy") 661 662 663 664val add_infixINS = 665 term_grammar.add_rule { 666 block_style = (AroundEachPhrase, (INCONSISTENT, 0)), 667 fixity = Parse.Infixr 490, 668 term_name = "INS", 669 pp_elements = [HardSpace 1, mTOK "INSERT", BreakSpace(1,0)], 670 paren_style = OnlyIfNecessary} 671 672val lf_infixfirst_cop = g0 |> add_infixINS |> add_setlistform 673val lf_copinfix_g = (* list first + infix INS *) 674 g0 |> add_setlistform |> add_infixINS 675fun get_stamps g = 676 let 677 open term_grammar_dtype 678 val rules = term_grammar.rules_for g "INS" 679 fun stamp fxty = 680 Option.map #1 681 (List.find (fn (_, GRULE {fixity,...}) => fixity = fxty 682 | _ => false) 683 rules) 684 in 685 {c = stamp Closefix, i = stamp (Infix(RIGHT, 490))} 686 end 687fun optionToString f NONE = "NONE" 688 | optionToString f (SOME x) = "SOME("^f x^")" 689fun recordic {i,c} = "i="^optionToString Int.toString i^"; "^ 690 "c="^optionToString Int.toString c 691 692val _ = tprint "infix INS first grule timestamps" 693val ic as {c, i} = get_stamps lf_infixfirst_cop 694val _ = case ic of 695 {i = SOME i0, c = SOME c0} => 696 if i0 < c0 then OK() 697 else die ("\n FAILED: "^recordic ic) 698 | _ => die ("\n FAILED: "^recordic ic) 699 700val _ = tprint "infix INS second grule timestamps" 701val ic as {c, i} = get_stamps lf_copinfix_g 702val _ = case ic of 703 {i = SOME i0, c = SOME c0} => 704 if c0 < i0 then OK() 705 else die ("\n FAILED: "^recordic ic) 706 | _ => die ("\n FAILED: "^recordic ic) 707 708val _ = tpp "Printing INS-list (w/infix INS first) {x}" "{x}" 709 lf_infixfirst_cop (pbmk_list "x") 710 711 712val _ = tpp "Printing INS-list (w/infix INS second) {x}" "x INSERT {}" 713 lf_copinfix_g (pbmk_list "x") 714 715val _ = tpp "Printing applied EMPTY: {} x" "{} x" lf_infixfirst_cop 716 (mk_comb(cEMP_t, mk_var("x", alpha))) 717 718val _ = tpp "Printing applied non-empty 1: {x} y" "{x} y" lf_infixfirst_cop 719 (mk_comb(pbmk_list "x", mk_var("y", bool))) 720 721val _ = tpp "Printing applied non-empty 2: {x; y} z" "{x; y} z" 722 lf_infixfirst_cop 723 (mk_comb(pbmk_list "xy", mk_var("z", bool))) 724 725open ParseDatatype 726val _ = tprint 727val ASTL_toString = 728 ParseDatatype_dtype.list_toString ParseDatatype_dtype.toString 729val mintyg = type_grammar.min_grammar 730val vbool = dTyop{Tyop = "bool", Thy = SOME "min", Args = []} 731fun pdparse s = parse mintyg [QUOTE s] 732fun hdparse s = hparse mintyg [QUOTE s] 733 734fun pdtest0 (nm, s,expected) = 735 let 736 val _ = tprint (nm ^ ": " ^ s) 737 val res = (if nm = "p" then pdparse else hdparse) s 738 in 739 if res = expected then OK() 740 else die ("FAILED:\n "^ASTL_toString res) 741 end 742infix -=> 743fun nm2parse nm = if nm = "p" then pdparse else hdparse 744fun pdtest (nm, s, expected) = 745 let 746 val _ = tprint (nm ^ ": " ^ s) 747 in 748 timed (nm2parse nm) 749 (exncheck (fn r => if r = expected then OK() 750 else die ("FAILED:\n "^ASTL_toString r))) 751 s 752 end 753fun pdfail (nm, s) = 754 shouldfail {printarg = (fn s => nm ^ ": " ^ s ^ " (should fail)"), 755 printresult = ASTL_toString, 756 testfn = nm2parse nm, 757 checkexn = is_struct_HOL_ERR "ParseDatatype"} s 758 759fun vty1 -=> vty2 = dTyop{Tyop = "fun", Thy = SOME "min", Args = [vty1,vty2]} 760fun recop s = dTyop{Thy = NONE, Tyop = s, Args = []} 761val expected1 = [("ty", Constructors [("Cons", [vbool])])] 762val expected2 = [("ty", Constructors [("Cons1", [vbool]), 763 ("Cons2", [vbool, vbool -=> vbool])])] 764val expected3 = [("ty", Record [("fld1", vbool), ("fld2", vbool -=> vbool)])] 765fun listnm nm = 766 [(nm, Constructors[("N", []), ("C",[dVartype "'a", recop "ty"])])] 767val expected4 = listnm "ty" 768val expected5 = [("C", Constructors[("foo", []), ("bar",[])])] 769val expected6 = [("C", Constructors[("foo", [vbool, vbool])]), 770 ("D", Constructors[("bar", [vbool]), ("baz", [])])] 771val _ = List.app pdtest [ 772 ("p", "ty = Cons of bool;", expected1), 773 ("h", "ty = Cons bool;", expected1), 774 ("h", "ty = Cons1 bool | Cons2 bool (bool -> bool);", expected2), 775 ("h", "ty = Cons1 bool | Cons2 bool (bool->bool);", expected2), 776 ("p", "ty = Cons1 of bool | Cons2 of bool => bool -> bool;", expected2), 777 ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool |>;", expected3), 778 ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool; |>;", expected3), 779 ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;", expected3), 780 ("h", "ty = N | C 'a ty;", expected4), 781 ("p", "ty = N | C of 'a => ty", expected4), 782 ("h", "ty=N|C 'a ty;", expected4), 783 ("h", "ty=N|C 'a ty", expected4), 784 ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;ty2=N|C 'a ty", 785 expected3 @ listnm "ty2"), 786 ("h", "C = | foo | bar", expected5), 787 ("h", "C = foo bool bool; D = bar bool|baz", expected6) 788] 789 790val _ = List.app (ignore o pdfail) [("h", "C = foo bool->bool")] 791 792 793(* string find-replace *) 794local 795val theta = map (fn (a,b) => {redex = a, residue = b}) 796 [("a", "xxx"), ("b", "zzzz"), ("abc", "y"), ("c", ""), 797 ("ca", "uu"), ("cb", "vv")] 798val f = stringfindreplace.subst theta 799fun test (inp,out) = 800 let 801 val _ = tprint ("String find/replace "^inp^" = "^out) 802 val res = f inp 803 in 804 if res = out then OK() 805 else die ("FAILED - Got "^res) 806 end 807in 808val _ = List.app test [("abcd", "yd"), ("ab", "xxxzzzz"), ("c", ""), 809 ("cab", "uuzzzz"), ("", ""), ("xyz", "xyz"), 810 ("ccb", "vv")] 811end (* local *) 812 813val _ = tprint "rules_for finds record rule" 814val G0 = term_grammar.stdhol 815val recrules = term_grammar.rules_for G0 GrammarSpecials.reccons_special 816val _ = 817 let 818 open term_grammar 819 in 820 case recrules of 821 [(_, GRULE {pp_elements = RE (TOK "<|") :: _,...})] => OK() 822 | _ => die "Couldn't find it" 823 end 824 825val _ = tprint "remove_termtok \"<|\" removes record rule" 826val G' = 827 term_grammar.remove_form_with_tok G0 { 828 term_name = GrammarSpecials.recd_lform_name, tok = "<|" 829 } 830val _ = 831 let 832 open term_grammar 833 in 834 case term_grammar.rules_for G' GrammarSpecials.reccons_special of 835 [] => OK() 836 | _ => die "Nope - something still there!" 837 end 838 839local 840 val pr = PP.pp_to_string 77 type_grammar.prettyprint_grammar 841 fun testvs(testname, fname, g) = 842 let 843 val expected0 = let 844 val istrm = TextIO.openIn fname 845 in 846 TextIO.inputAll istrm before TextIO.closeIn istrm 847 end 848 val expected = if String.sub(expected0, size expected0 - 1) = #"\n" then 849 String.extract(expected0, 0, SOME (size expected0 - 1)) 850 else expected0 851 val res = delete_trailing_wspace (pr g) 852 in 853 tprint testname; 854 if res = expected then OK() else die ("\nFAILED!\n" ^ res) 855 end 856 open type_grammar 857in 858 val _ = app testvs [ 859 ("Testing ty-grammar p/printing (min_grammar)", "tygrammar.txt", 860 min_grammar), 861 ("Testing ty-grammar p/printing (min_grammar with non-printing abbrev)", 862 "noprint_tygrammar.txt", 863 min_grammar |> new_abbreviation {knm = {Name = "set", Thy = "scratch"}, 864 ty = alpha --> bool, print = true} 865 |> disable_abbrev_printing "set") 866 ] 867end (* tygrammar p/printing local *) 868 869local 870 open term_tokens 871 fun test (s, expected) = 872 let 873 val _ = tprint ("Non-aggregating lex-test on "^s) 874 fun check (Exn.Res (SOME (r, _))) = 875 (case r of Ident s' => s' = expected | _ => false) 876 | check _ = false 877 fun pr NONE = "NONE" 878 | pr (SOME (t, _)) = "SOME(" ^ token_string t ^ ")" 879 in 880 require_msg check pr (lex []) (qbuf.new_buffer [QUOTE s]) 881 end 882in 883val _ = List.app (ignore o test) [ 884 ("aa(", "aa"), ("((a", "("), ("����", "��"), ("����p", "��") 885 ] 886end (* local open term_tokens *) 887 888val _ = let 889 open term_grammar Absyn Portable 890 val rTOK = RE o TOK 891 datatype sexp = id of string | app of string * sexp list 892 fun toString (id s) = s 893 | toString (app(f,xs)) = 894 "(" ^ f ^ 895 (case xs of [] => "" 896 | _ => " " ^ String.concatWith " " (map toString xs)) ^ ")" 897 fun dropA A a = 898 case a of 899 APP (_, a1, a2) => dropA (dropA [] a2::A) a1 900 | IDENT (_, s) => (case A of [] => id s | _ => app(s, A)) 901 | _ => raise Fail "Unexpected Absyn form" 902 val G = min_grammar 903 |> add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 904 fixity = Suffix 2100, 905 paren_style = OnlyIfNecessary, 906 pp_elements = [ 907 rTOK "{", 908 ListForm { 909 separator = [rTOK ";", BreakSpace(1,0)], 910 block_info = (PP.CONSISTENT, 1), 911 cons = "icons", 912 nilstr = "inil" 913 }, 914 rTOK "}"], 915 term_name = "top"} 916 val testfn = 917 toString o dropA [] o TermParse.absyn G type_grammar.min_grammar o 918 single o QUOTE 919 fun test (s,expected) = 920 (tprint ("listspec-suffix: " ^ s); 921 require_msg_eq expected HOLPP.add_string testfn s) 922in 923 List.app (ignore o test) [ 924 ("x {y}", "(top x (icons y inil))"), 925 ("x {y;z;}", "(top x (icons y (icons z inil)))"), 926 ("x {}", "(top x inil)") 927 ] 928end; 929