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 146fun quoteToString [QUOTE s] = "`"^s^"`" 147 | quoteToString _ = die "Bad test quotation" 148 149fun test (q, slist) = let 150 val _ = tprint ("Testing " ^ quoteToString q) 151in 152 if map (base_tokens.toString o #1) (qbuf.lex_to_toklist q) <> slist then 153 die "FAILED!" 154 else OK() 155end handle LEX_ERR (s,_) => die ("FAILED!\n [LEX_ERR "^s^"]") 156 | e => die ("FAILED\n ["^exnMessage e^"]") 157 158val _ = app test [(`abc`, ["abc"]), 159 (`12`, ["12"]), 160 (`3.0`, ["3.0"]), 161 (`3.00`, ["3.00"]), 162 (`0xab`, ["171"]), 163 (`12.1`, ["12.1"]), 164 (`12.01`, ["12.01"]), 165 (`12.010`, ["12.010"]), 166 (`(`, ["("]), 167 (`a(a`, ["a(a"]), 168 (`x+y`, ["x+y"]), 169 (`x +y`, ["x", "+y"]), 170 (`x ++ y`, ["x", "++", "y"]), 171 (`x (* *)y`, ["x", "y"]), 172 (`x(**)y`, ["x", "y"]), 173 (`+(**)y`, ["+", "y"]), 174 (`((*x*)`, ["("]), 175 (`+(%*%((*"*)-*foo`,["+(%*%(", "-*foo"]), 176 (`"(*"`, ["\"(*\""]) 177 ] 178 179(* tests of the term lexer *) 180fun test (s, toklist : unit term_tokens.term_token list) = let 181 val _ = tprint ("Term token testing " ^ Lib.quote s) 182in 183 if term_tokens.lextest [] s = toklist then OK() 184 else die "FAILED!" 185end handle LEX_ERR (s,_) => die ("FAILED!\n [LEX_ERR "^s^"]") 186 | e => die ("FAILED\n ["^exnMessage e^"]") 187 188open term_tokens 189val ai = Arbnum.fromInt 190val _ = app test [("abc", [Ident "abc"]), 191 ("12", [Numeral (ai 12, NONE)]), 192 ("-12", [Ident "-", Numeral (ai 12, NONE)]), 193 ("((-12", [Ident "(", Ident "(", Ident "-", 194 Numeral (ai 12, NONE)]), 195 ("1.2", [Fraction{wholepart = ai 1, fracpart = ai 2, 196 places = 1}]), 197 ("-1.2", [Ident "-", 198 Fraction{wholepart = ai 1, fracpart = ai 2, 199 places = 1}]), 200 ("~1.2", [Ident "~", 201 Fraction{wholepart = ai 1, fracpart = ai 2, 202 places = 1}]), 203 ("(2n*e", [Ident "(", Numeral (ai 2, SOME #"n"), 204 Ident "*", Ident "e"]), 205 ("2_001", [Numeral (ai 2001, NONE)]), 206 ("2.000_023", [Fraction{wholepart = ai 2, places = 6, 207 fracpart = ai 23}]), 208 ("0.", [Numeral (ai 0, NONE), Ident "."]), 209 ("a0.", [Ident "a0", Ident "."]), 210 ("-0.", [Ident "-", Numeral (ai 0, NONE), Ident "."]), 211 ("{2.3", [Ident "{", Fraction{wholepart = ai 2, places = 1, 212 fracpart = ai 3}]) 213 ] 214 215val g0 = term_grammar.stdhol; 216fun mTOK s = term_grammar_dtype.RE (HOLgrammars.TOK s) 217val mTM = term_grammar_dtype.RE HOLgrammars.TM 218 219local 220 open term_grammar term_grammar_dtype 221in 222val cond_g = 223 add_rule { 224 term_name = "COND", 225 fixity = Prefix 70, 226 pp_elements = [PPBlock([mTOK "if", BreakSpace(1,2), mTM, 227 BreakSpace(1,0), 228 mTOK "then"], (CONSISTENT, 0)), 229 BreakSpace(1,2), mTM, BreakSpace(1,0), 230 mTOK "else", BreakSpace(1,2)], 231 paren_style = OnlyIfNecessary, 232 block_style = (AroundEachPhrase, (CONSISTENT, 0))} g0 233val let_g = 234 add_rule { pp_elements = [mTOK "let", 235 ListForm { 236 separator = [mTOK ";"], 237 cons = GrammarSpecials.letcons_special, 238 nilstr = GrammarSpecials.letnil_special, 239 block_info = (INCONSISTENT, 0)}, 240 mTOK "in"], 241 term_name = GrammarSpecials.let_special, 242 paren_style = OnlyIfNecessary, fixity = Prefix 8, 243 block_style = (AroundEachPhrase, (CONSISTENT, 0))} g0 244val lf_g = add_listform g0 245 { block_info = (CONSISTENT, 0), 246 separator = [mTOK ";", BreakSpace(1,0)], 247 leftdelim = [mTOK "["], 248 rightdelim= [mTOK "]"], 249 nilstr = "NIL", cons = "CONS"} 250end; 251fun isabsynlist slist a = 252 let 253 open Absyn 254 in 255 case slist of 256 [] => (case a of IDENT (_, "NIL") => true | _ => false) 257 | s1 :: rest => 258 (case a of 259 APP(_, APP (_, IDENT(_, "CONS"), IDENT (_, el1)), a_rest) => 260 el1 = s1 andalso isabsynlist rest a_rest 261 | _ => false) 262 end 263val _ = PP.prettyPrint 264 (print, 75) 265 (Parse.mlower 266 (term_grammar.prettyprint_grammar 267 (fn g =>fn _ => smpp.add_string "<term>") 268 lf_g)) 269 270fun parsetest sl = 271 let 272 val s = "["^String.concatWith ";" sl^"]" 273 val _ = tprint ("Parsing "^s) 274 val a = TermParse.absyn lf_g type_grammar.min_grammar [QUOTE s] 275 in 276 if isabsynlist sl a then OK() else die "FAILED!" 277 end 278 279val _ = parsetest [] 280val _ = parsetest (map str (explode "ab")) 281val _ = parsetest (map str (explode "abcdef")) 282 283fun find_named_rule nm g = 284 let 285 open term_grammar_dtype term_grammar 286 in 287 List.map 288 (fn PREFIX (STD_prefix rrs) => 289 List.filter (fn rr => #term_name rr = nm) rrs 290 | _ => []) 291 (grammar_rules g) |> List.concat 292 end; 293 294val _ = tprint "term_grammar.grammar_tokens (LET)" 295val _ = 296 let val result = term_grammar.grammar_tokens let_g 297 in 298 if Lib.set_eq result 299 ["\\", "|>", "<|", ")", "(", ".", ":", "updated_by", 300 ":=", "with", "let", "in", ";", "$"] 301 then OK() 302 else die ("\nFAILED ["^ 303 String.concatWith "," (map (fn s => "\""^s^"\"") result) ^ "]") 304 end; 305 306val _ = tprint "term_grammar.rule_elements (COND)" 307val cond_rule = hd (find_named_rule "COND" cond_g) 308val cond_rels = term_grammar.rule_elements (#elements cond_rule) 309val _ = let 310 open HOLgrammars 311in 312 if cond_rels = [TOK "if", TM, TOK "then", TM, TOK "else"] then OK() 313 else die "FAILED" 314end; 315 316val _ = tprint "PrecAnalysis.rule_equalities (COND)" 317val cond_eqns = PrecAnalysis.rule_equalities cond_rule 318val _ = if Lib.set_eq cond_eqns [("if", true, "then"), ("then", true, "else")] 319 then OK() 320 else die "FAILED"; 321 322val _ = tprint "term_grammar.rule_elements (LET)" 323val let_rule = hd (find_named_rule GrammarSpecials.let_special let_g) 324val let_rels = term_grammar.rule_elements (#elements let_rule) 325val _ = let 326 open HOLgrammars GrammarSpecials 327in 328 if let_rels = 329 [TOK"let", ListTM{nilstr=letnil_special, cons=letcons_special, sep=";"}, 330 TOK "in"] 331 then OK () 332 else die "FAILED" 333end; 334 335fun prlist eqns = 336 "[" ^ String.concatWith ", " 337 (map (fn (s1,b,s2) => "(\"" ^ s1 ^ "\"," ^ Bool.toString b ^ ",\"" ^ 338 s2 ^"\")") 339 eqns) ^ "]"; 340 341val _ = tprint "PrecAnalysis.rule_equalities (LET)" 342val let_eqns = PrecAnalysis.rule_equalities let_rule 343val _ = if Lib.set_eq let_eqns 344 [("let", true, ";"), (";", true, ";"), (";", true, "in"), 345 ("let", false, "in"), ("let", true, "in"), 346 (";", false, "in")] 347 then OK() 348 else die ("FAILED\n got: "^prlist let_eqns); 349 350val _ = tprint "term_grammar.rules_for (LET)" 351val let_rules = term_grammar.rules_for let_g GrammarSpecials.let_special 352val _ = if length let_rules = 1 then OK() else die "FAILED" 353 354val lsp1 = {nilstr="lnil",cons="lcons",sep=";"} 355val lsp2 = {nilstr="lnil2",cons="lcons2",sep=";;"} 356fun check (s1,s2) = 357 case (s1,s2) of 358 ("let", "in") => SOME lsp1 359 | ("in", "end") => SOME lsp2 360 | _ => NONE 361 362val f = PrecAnalysis.check_for_listreductions check 363 364open term_grammar_dtype GrammarSpecials 365val _ = tprint "PrecAnalysis.check_for_listreductions 1" 366val input = [TOK "let", TM, TOK "in", TM] 367val result = f input 368val _ = if result = [("let", "in", lsp1)] then OK() else die "FAILED"; 369 370val _ = tprint "PrecAnalysis.remove_listrels 1" 371val remove_result = PrecAnalysis.remove_listrels result input 372val _ = if remove_result = ([TOK "let", TM, TOK "in", TM], [(lsp1, [0])]) 373 then OK() 374 else die "FAILED"; 375 376val _ = tprint "PrecAnalysis.check_for_listreductions 2" 377val input = [TOK "let", TM, TOK ";", TOK "in", TM] 378val result = f input 379val _ = if result = [("let", "in", lsp1)] then OK() else die "FAILED"; 380 381val _ = tprint "PrecAnalysis.remove_listrels 2" 382val remove_result = PrecAnalysis.remove_listrels result input 383val _ = if remove_result = ([TOK "let", TM, TOK "in", TM], [(lsp1, [0])]) 384 then OK() 385 else die "FAILED"; 386 387val _ = tprint "PrecAnalysis.check_for_listreductions 3" 388val input = [TOK "let", TM, TOK ";", TM, TOK "in", TM] 389val result = f input 390val _ = if result = [("let", "in", lsp1)] then OK() else die "FAILED"; 391 392val _ = tprint "PrecAnalysis.remove_listrels 3" 393val remove_result = PrecAnalysis.remove_listrels result input 394val _ = if remove_result = ([TOK "let", TM, TOK "in", TM], [(lsp1, [0,1])]) 395 then OK() 396 else die "FAILED"; 397 398val mk_var = Term.mk_var 399val mk_comb = Term.mk_comb 400val bool = Type.bool 401val alpha = Type.alpha 402val CONS_t = mk_var("CONS", bool --> (bool --> bool)) 403val NIL_t = mk_var("NIL", bool) 404fun mk_list00 elty n c tmlist = 405 let 406 fun recurse ts = 407 case ts of 408 [] => Term.inst [alpha |-> elty] n 409 | x::xs => mk_comb(mk_comb(Term.inst [alpha |-> elty] c, x), 410 recurse xs) 411 in 412 recurse tmlist 413 end 414 415fun mk_list0 elty n c s = 416 mk_list00 elty n c (map (fn c => mk_var(str c, elty)) (String.explode s)) 417 418val mk_list = mk_list0 bool NIL_t CONS_t; 419 420fun tmprint g = 421 PP.pp_to_string 70 422 (fn t => 423 Parse.mlower 424 (term_pp.pp_term g 425 type_grammar.min_grammar 426 PPBackEnd.raw_terminal 427 t)) 428 429fun tpp msg expected g t = 430 let 431 val _ = tprint msg 432 val result = tmprint g t 433 in 434 if result = expected then OK() 435 else die ("\nFAILED - got >" ^ result ^"<") 436 end handle e => die ("EXN-FAILED: "^General.exnMessage e) 437 438val _ = tpp "Printing empty list form (var)" "[]" lf_g NIL_t 439val _ = tpp "Printing CONS-list form [x] (var)" "[x]" lf_g (mk_list "x") 440val _ = tpp "Printing CONS-list form [x;y] (var)" "[x; y]" lf_g (mk_list "xy") 441 442val cCONS_t = 443 Term.prim_new_const {Thy = "min", Name = "CONS"} (bool --> (bool --> bool)) 444val cNIL_t = Term.prim_new_const {Thy = "min", Name = "NIL"} bool 445val cmk_list = mk_list0 bool cNIL_t cCONS_t 446 447val _ = tpp "Printing nil (const, no overload)" "min$NIL" lf_g cNIL_t 448 449val lfco_g = lf_g |> term_grammar.fupdate_overload_info 450 (Overload.add_overloading ("NIL", cNIL_t)) 451 |> term_grammar.fupdate_overload_info 452 (Overload.add_overloading ("CONS", cCONS_t)); 453 454val _ = tpp "Printing nil (const, overload)" "[]" lfco_g cNIL_t 455val _ = tpp "Printing CONS-list [x] (const, overload)" "[x]" 456 lfco_g (cmk_list "x") 457 458(* listform, const, overload, nil overloaded again (as EMPTY is in pred_set) *) 459val lfcono_g = 460 lfco_g |> term_grammar.fupdate_overload_info 461 (Overload.add_overloading ("altNIL", cNIL_t)) 462 463val _ = tpp "Printing nil (const, double-overload)" "[x]" lfcono_g 464 (cmk_list "x") 465 466val cINS_t = Term.prim_new_const{Thy = "min", Name = "INS"} 467 (alpha --> (alpha --> bool) --> (alpha --> bool)) 468val cEMP_t = Term.prim_new_const{Thy = "min", Name = "EMP"} (alpha --> bool) 469fun add_setlistform g = 470 term_grammar.add_listform g { 471 block_info = (CONSISTENT, 0), 472 separator = [mTOK ";", BreakSpace(1,0)], 473 leftdelim = [mTOK "{"], 474 rightdelim= [mTOK "}"], 475 nilstr = "EMP", cons = "INS"} 476 |> term_grammar.fupdate_overload_info 477 (Overload.add_overloading ("EMP", cEMP_t)) 478 |> term_grammar.fupdate_overload_info 479 (Overload.add_overloading ("INS", cINS_t)) 480 481val lfcop_g = g0 |> add_setlistform 482 483 484val pbmk_list = mk_list0 bool cEMP_t cINS_t 485fun ptpp msg exp t = tpp msg exp lfcop_g t 486 487val _ = ptpp "Printing INS-list {x} (const, overload, polymorphic inst)" "{x}" 488 (pbmk_list "x") 489 490val _ = ptpp "Printing INS-list {x;y} (const, overload, polymorphic inst)" 491 "{x; y}" 492 (pbmk_list "xy") 493 494val fx = mk_comb(mk_var("f", alpha --> bool), mk_var("x", alpha)) 495val y = mk_var("y", bool) 496val bINS = Term.inst[alpha |-> bool] cINS_t 497val bEMP = Term.inst[alpha |-> bool] cEMP_t 498val l = mk_comb(mk_comb(bINS, fx), mk_comb(mk_comb(bINS, y), bEMP)) 499val _ = ptpp "Printing INS-list {f x;y} (const, overload, polymorphic inst)" 500 "{f x; y}" 501 502val lfcopuo_g = (* as before + Unicode-ish overload on EMP *) 503 lfcop_g 504 |> term_grammar.fupdate_overload_info 505 (Overload.add_overloading ("���", cEMP_t)) 506val _ = tpp "Printing INS-list (Unicode EMP) {x;y}" "{x; y}" 507 lfcopuo_g (pbmk_list "xy") 508 509 510 511val add_infixINS = 512 term_grammar.add_rule { 513 block_style = (AroundEachPhrase, (INCONSISTENT, 0)), 514 fixity = Parse.Infixr 490, 515 term_name = "INS", 516 pp_elements = [HardSpace 1, mTOK "INSERT", BreakSpace(1,0)], 517 paren_style = OnlyIfNecessary} 518 519val lf_infixfirst_cop = g0 |> add_infixINS |> add_setlistform 520val lf_copinfix_g = (* list first + infix INS *) 521 g0 |> add_setlistform |> add_infixINS 522fun get_stamps g = 523 let 524 open term_grammar_dtype 525 val rules = term_grammar.rules_for g "INS" 526 fun stamp fxty = 527 Option.map #1 528 (List.find (fn (_, GRULE {fixity,...}) => fixity = fxty 529 | _ => false) 530 rules) 531 in 532 {c = stamp Closefix, i = stamp (Infix(RIGHT, 490))} 533 end 534fun optionToString f NONE = "NONE" 535 | optionToString f (SOME x) = "SOME("^f x^")" 536fun recordic {i,c} = "i="^optionToString Int.toString i^"; "^ 537 "c="^optionToString Int.toString c 538 539val _ = tprint "infix INS first grule timestamps" 540val ic as {c, i} = get_stamps lf_infixfirst_cop 541val _ = case ic of 542 {i = SOME i0, c = SOME c0} => 543 if i0 < c0 then OK() 544 else die ("\n FAILED: "^recordic ic) 545 | _ => die ("\n FAILED: "^recordic ic) 546 547val _ = tprint "infix INS second grule timestamps" 548val ic as {c, i} = get_stamps lf_copinfix_g 549val _ = case ic of 550 {i = SOME i0, c = SOME c0} => 551 if c0 < i0 then OK() 552 else die ("\n FAILED: "^recordic ic) 553 | _ => die ("\n FAILED: "^recordic ic) 554 555val _ = tpp "Printing INS-list (w/infix INS first) {x}" "{x}" 556 lf_infixfirst_cop (pbmk_list "x") 557 558 559val _ = tpp "Printing INS-list (w/infix INS second) {x}" "x INSERT {}" 560 lf_copinfix_g (pbmk_list "x") 561 562val _ = tpp "Printing applied EMPTY: {} x" "{} x" lf_infixfirst_cop 563 (mk_comb(cEMP_t, mk_var("x", alpha))) 564 565val _ = tpp "Printing applied non-empty 1: {x} y" "{x} y" lf_infixfirst_cop 566 (mk_comb(pbmk_list "x", mk_var("y", bool))) 567 568val _ = tpp "Printing applied non-empty 2: {x; y} z" "{x; y} z" 569 lf_infixfirst_cop 570 (mk_comb(pbmk_list "xy", mk_var("z", bool))) 571 572open ParseDatatype 573val _ = tprint 574val ASTL_toString = 575 ParseDatatype_dtype.list_toString ParseDatatype_dtype.toString 576val mintyg = type_grammar.min_grammar 577val vbool = dTyop{Tyop = "bool", Thy = SOME "min", Args = []} 578fun pdparse s = parse mintyg [QUOTE s] 579fun hdparse s = hparse mintyg [QUOTE s] 580 581fun pdtest0 (nm, s,expected) = 582 let 583 val _ = tprint (nm ^ ": " ^ s) 584 val res = (if nm = "p" then pdparse else hdparse) s 585 in 586 if res = expected then OK() 587 else die ("FAILED:\n "^ASTL_toString res) 588 end 589infix -=> 590fun nm2parse nm = if nm = "p" then pdparse else hdparse 591fun pdtest (nm, s, expected) = 592 let 593 val _ = tprint (nm ^ ": " ^ s) 594 in 595 timed (nm2parse nm) 596 (exncheck (fn r => if r = expected then OK() 597 else die ("FAILED:\n "^ASTL_toString r))) 598 s 599 end 600fun pdfail (nm, s) = 601 shouldfail {printarg = (fn s => nm ^ ": " ^ s ^ " (should fail)"), 602 printresult = ASTL_toString, 603 testfn = nm2parse nm, 604 checkexn = is_struct_HOL_ERR "ParseDatatype"} s 605 606fun vty1 -=> vty2 = dTyop{Tyop = "fun", Thy = SOME "min", Args = [vty1,vty2]} 607fun recop s = dTyop{Thy = NONE, Tyop = s, Args = []} 608val expected1 = [("ty", Constructors [("Cons", [vbool])])] 609val expected2 = [("ty", Constructors [("Cons1", [vbool]), 610 ("Cons2", [vbool, vbool -=> vbool])])] 611val expected3 = [("ty", Record [("fld1", vbool), ("fld2", vbool -=> vbool)])] 612fun listnm nm = 613 [(nm, Constructors[("N", []), ("C",[dVartype "'a", recop "ty"])])] 614val expected4 = listnm "ty" 615val expected5 = [("C", Constructors[("foo", []), ("bar",[])])] 616val expected6 = [("C", Constructors[("foo", [vbool, vbool])]), 617 ("D", Constructors[("bar", [vbool]), ("baz", [])])] 618val _ = List.app pdtest [ 619 ("p", "ty = Cons of bool;", expected1), 620 ("h", "ty = Cons bool;", expected1), 621 ("h", "ty = Cons1 bool | Cons2 bool (bool -> bool);", expected2), 622 ("h", "ty = Cons1 bool | Cons2 bool (bool->bool);", expected2), 623 ("p", "ty = Cons1 of bool | Cons2 of bool => bool -> bool;", expected2), 624 ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool |>;", expected3), 625 ("h", "ty = <| fld1 : bool ; fld2 : bool -> bool; |>;", expected3), 626 ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;", expected3), 627 ("h", "ty = N | C 'a ty;", expected4), 628 ("p", "ty = N | C of 'a => ty", expected4), 629 ("h", "ty=N|C 'a ty;", expected4), 630 ("h", "ty=N|C 'a ty", expected4), 631 ("h", "ty= <|fld1:bool;fld2:bool->bool; |>;ty2=N|C 'a ty", 632 expected3 @ listnm "ty2"), 633 ("h", "C = | foo | bar", expected5), 634 ("h", "C = foo bool bool; D = bar bool|baz", expected6) 635] 636 637val _ = List.app pdfail [ 638 ("h", "C = foo bool->bool") 639] 640 641 642(* string find-replace *) 643local 644val theta = map (fn (a,b) => {redex = a, residue = b}) 645 [("a", "xxx"), ("b", "zzzz"), ("abc", "y"), ("c", ""), 646 ("ca", "uu"), ("cb", "vv")] 647val f = stringfindreplace.subst theta 648fun test (inp,out) = 649 let 650 val _ = tprint ("String find/replace "^inp^" = "^out) 651 val res = f inp 652 in 653 if res = out then OK() 654 else die ("FAILED - Got "^res) 655 end 656in 657val _ = List.app test [("abcd", "yd"), ("ab", "xxxzzzz"), ("c", ""), 658 ("cab", "uuzzzz"), ("", ""), ("xyz", "xyz"), 659 ("ccb", "vv")] 660end (* local *) 661 662val _ = tprint "rules_for finds record rule" 663val G0 = term_grammar.stdhol 664val recrules = term_grammar.rules_for G0 GrammarSpecials.reccons_special 665val _ = 666 let 667 open term_grammar 668 in 669 case recrules of 670 [(_, GRULE {pp_elements = RE (TOK "<|") :: _,...})] => OK() 671 | _ => die "Couldn't find it" 672 end 673 674val _ = tprint "remove_termtok \"<|\" removes record rule" 675val G' = 676 term_grammar.remove_form_with_tok G0 { 677 term_name = GrammarSpecials.recd_lform_name, tok = "<|" 678 } 679val _ = 680 let 681 open term_grammar 682 in 683 case term_grammar.rules_for G' GrammarSpecials.reccons_special of 684 [] => OK() 685 | _ => die "Nope - something still there!" 686 end 687 688local open term_tokens 689fun test (s,expected) = 690 let 691 val _ = tprint ("lexing "^s) 692 val toks : unit term_token list = lextest [] s 693 in 694 if toks = expected then OK() 695 else die "FAILED" 696 end 697in 698val _ = 699 List.app test [ 700 ("$ $$ $$$ $+ $if", [Ident "$", Ident "$$", Ident "$$$", Ident "$+", 701 Ident "$if"]), 702 ("thy$id", [QIdent("thy", "id")]), 703 ("thy$$$", [QIdent("thy", "$$")]) 704 ] 705end (* open term_tokens local *); 706 707local 708 val pr = PP.pp_to_string 77 type_grammar.prettyprint_grammar 709 fun testvs(testname, fname, g) = 710 let 711 val expected0 = let 712 val istrm = TextIO.openIn fname 713 in 714 TextIO.inputAll istrm before TextIO.closeIn istrm 715 end 716 val expected = if String.sub(expected0, size expected0 - 1) = #"\n" then 717 String.extract(expected0, 0, SOME (size expected0 - 1)) 718 else expected0 719 val res = delete_trailing_wspace (pr g) 720 in 721 tprint testname; 722 if res = expected then OK() else die ("\nFAILED!\n" ^ res) 723 end 724 open type_grammar 725in 726 val _ = app testvs [ 727 ("Testing ty-grammar p/printing (min_grammar)", "tygrammar.txt", 728 min_grammar), 729 ("Testing ty-grammar p/printing (min_grammar with non-printing abbrev)", 730 "noprint_tygrammar.txt", 731 min_grammar |> (fn g => 732 new_abbreviation g 733 ({Name = "set", Thy = "scratch"}, 734 alpha --> bool)) 735 |> disable_abbrev_printing "set") 736 ] 737end (* tygrammar p/printing local *) 738 739local 740 open term_tokens 741 fun test (s, expected) = 742 let 743 val _ = tprint ("Non-aggregating lex-test on "^s) 744 fun check (Exn.Res (SOME (r, _))) = 745 (case r of Ident s' => s' = expected | _ => false) 746 | check _ = false 747 fun pr NONE = "NONE" 748 | pr (SOME (t, _)) = "SOME(" ^ token_string t ^ ")" 749 in 750 require_msg check pr (lex []) (qbuf.new_buffer [QUOTE s]) 751 end 752in 753val _ = List.app test [("aa(", "aa"), ("((a", "("), ("����", "��"), 754 ("����p", "��")] 755end (* local open term_tokens *) 756