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