1open HolKernel boolLib bossLib Parse 2open EmitTeX combinSyntax PP 3open testutils 4 5fun udie() = testutils.die "FAILED!" 6fun gotdie s = testutils.die ("\nFAILED: Got >" ^ s ^ "<") 7 8val _ = tprint "Testing var v2 overridden to v1" 9val x_t = mk_var("x", alpha) 10val v1 = mk_var("v1",bool) 11val v2 = mk_var("v2",bool) 12val s1 = pp_to_string 5 pp_term_as_tex v1 13val s2 = pp_to_string 5 (raw_pp_term_as_tex(fn"v2"=>SOME("v1",2)|_=>NONE)) v2 14val _ = if s1 = s2 then OK() else udie() 15 16val _ = tprint "Testing const F overridden to T" 17val s1 = pp_to_string 5 pp_term_as_tex T 18val s2 = pp_to_string 5 (raw_pp_term_as_tex(fn"F"=>SOME("T",1)|_=>NONE)) F 19val _ = if s1 = s2 then OK() else udie() 20 21val _ = tprint "Testing syntactic-sugar overriding" 22val _ = temp_remove_rules_for_term "~" 23 (* Note that this is one of the few places where temp_remove_rules_for_term is 24 called; tests here are at least somewhat a test of its functionality too. *) 25val _ = temp_add_rule {term_name = "~", 26 fixity = Prefix 900, 27 pp_elements = [TOK "TOK1"], 28 paren_style = OnlyIfNecessary, 29 block_style = (AroundEachPhrase, (CONSISTENT, 0))} 30val _ = temp_add_rule {term_name = "I", 31 fixity = Prefix 900, 32 pp_elements = [TOK "TOK2"], 33 paren_style = OnlyIfNecessary, 34 block_style = (AroundEachPhrase, (CONSISTENT, 0))} 35val t1 = mk_neg(T) 36val t2 = mk_I(T) 37val s1 = pp_to_string 5 pp_term_as_tex t1 38val s2 = pp_to_string 5 (raw_pp_term_as_tex(fn"TOK2"=>SOME("TOK1",3)|_=>NONE)) t2 39val _ = if s1 = s2 then OK() else udie() 40 41val _ = tprint "Testing dollarised syntax (/\\)" 42val s = pp_to_string 70 pp_term_as_tex conjunction 43val _ = if s = "(\\HOLSymConst{\\HOLTokenConj{}})" then OK() else gotdie s 44 45val _ = tprint "Testing dollarised syntax (if)" 46val s = pp_to_string 70 pp_term_as_tex (mk_var("if", bool)) 47val _ = if s = "(\\HOLFreeVar{\\HOLKeyword{if}})" then OK() else gotdie s 48 49open Feedback 50val _ = tprint "Testing paren-less dollarised syntax /\\" 51val _ = set_trace "EmitTeX: dollar parens" 0 52val s = pp_to_string 70 pp_term_as_tex conjunction 53val _ = if s = "\\HOLSymConst{\\HOLTokenConj{}}" then OK() else gotdie s 54val _ = set_trace "EmitTeX: dollar parens" 1 55 56val _ = tprint "Testing UNIV printing (:'a)" 57val s = pp_to_string 70 pp_term_as_tex (pred_setSyntax.mk_univ alpha) 58val _ = if s = "\\ensuremath{\\cal{U}}(:'a)" then OK() else gotdie s 59 60val _ = tprint "Testing UNIV printing \"raw\" (:'a)" 61val s = pp_to_string 70 62 (raw_pp_term_as_tex (K NONE)) 63 (pred_setSyntax.mk_univ alpha) 64val _ = if s = "\\ensuremath{\\cal{U}}(:\\ensuremath{\\alpha})" then OK() 65 else gotdie s 66 67val _ = tprint "Testing UNIV printing (:num)" 68val s = pp_to_string 70 pp_term_as_tex (pred_setSyntax.mk_univ numSyntax.num) 69val _ = if s = "\\ensuremath{\\cal{U}}(:\\HOLTyOp{num})" then OK() 70 else udie() 71 72val _ = tprint "Testing const-annotation for binders" 73val P_t = mk_var("P", alpha --> bool) 74val s = pp_to_string 70 pp_term_as_tex (mk_forall(x_t, mk_comb(P_t, x_t))) 75val _ = if s = "\\HOLSymConst{\\HOLTokenForall{}}\\HOLBoundVar{x}. \\HOLFreeVar{P} \\HOLBoundVar{x}" 76 then OK() else gotdie s 77 78val _ = Feedback.emit_MESG := false 79fun dtype_test n s = pp_to_string n (raw_pp_theorem_as_tex (fn _ => NONE)) (theorem ("datatype_" ^ s)) 80val _ = Hol_datatype`foo = C of bool -> 'a -> bool | D of foo => 'a => num list | Econ of foo => foo => 'a`; 81val _ = tprint "Testing datatype printing (default)" 82val s = dtype_test 55 "foo" 83val expected_consistent = 84 "\\HOLFreeVar{foo} =\n\ 85 \ \\HOLConst{C} (\\HOLTyOp{bool} -> \\ensuremath{\\alpha} -> \\HOLTyOp{bool})\n\ 86 \ \\HOLTokenBar{} \\HOLConst{D} (\\ensuremath{\\alpha} \\HOLTyOp{foo}) \\ensuremath{\\alpha} (\\HOLTyOp{num} \\HOLTyOp{list})\n\ 87 \ \\HOLTokenBar{} \\HOLConst{Econ} (\\ensuremath{\\alpha} \\HOLTyOp{foo}) (\\ensuremath{\\alpha} \\HOLTyOp{foo}) \\ensuremath{\\alpha}" 88val _ = if s = expected_consistent then OK() 89 else die("Expected\n" ^ expected_consistent ^ "\nGot:\n" ^ s) 90 91val expected_inconsistent = 92 "\\HOLFreeVar{foo} = \ 93 \\\HOLConst{C} (\\HOLTyOp{bool} -> \\ensuremath{\\alpha} -> \\HOLTyOp{bool}) \ 94 \\\HOLTokenBar{} \\HOLConst{D} (\\ensuremath{\\alpha} \\HOLTyOp{foo}) \\ensuremath{\\alpha} (\\HOLTyOp{num} \\HOLTyOp{list})\n\ 95 \ \\HOLTokenBar{} \\HOLConst{Econ} (\\ensuremath{\\alpha} \\HOLTyOp{foo}) (\\ensuremath{\\alpha} \\HOLTyOp{foo}) \\ensuremath{\\alpha}" 96val _ = tprint "Testing datatype printing (compact)" 97val s = trace ("EmitTeX: print datatypes compactly", 1) 98 (dtype_test 55) "foo" 99val _ = if s = expected_inconsistent then OK() 100 else die("Expected\n" ^ expected_inconsistent ^ "\nGot:\n" ^ s) 101 102 103val _ = tprint "Testing enumerated datatype printing" 104val _ = Hol_datatype `bar = ETA | ETB | ETC | ETD | ETE | ETF | ETG | ETH | ETI | ETJ`; 105val s = dtype_test 20 "bar" 106val _ = if s = "\\HOLFreeVar{bar} = \\HOLConst{ETA} \\HOLTokenBar{} \\HOLConst{ETB}\n\ 107 \ \\HOLTokenBar{} \\HOLConst{ETC} \\HOLTokenBar{} \\HOLConst{ETD}\n\ 108 \ \\HOLTokenBar{} \\HOLConst{ETE} \\HOLTokenBar{} \\HOLConst{ETF}\n\ 109 \ \\HOLTokenBar{} \\HOLConst{ETG} \\HOLTokenBar{} \\HOLConst{ETH}\n\ 110 \ \\HOLTokenBar{} \\HOLConst{ETI} \\HOLTokenBar{} \\HOLConst{ETJ}" 111 then 112 OK() 113 else 114 gotdie s 115