1open HolKernel Parse goalStack Tactic Tactical
2open testutils
3
4val _ = set_trace "Unicode" 0
5
6val _ = goalStack.chatting := false
7
8val _ = tprint "Itself case-eq properly polymorphic"
9val _ =
10    let
11      open boolLib
12      val cthm = TypeBase.case_eq_of ``:'a itself``
13      val l = cthm |> concl |> lhs |> lhs
14      val (_, args) = strip_comb l
15      val xv = hd args
16    in
17      if xv |> type_of |> Type.polymorphic then OK()
18      else die "FAILED!"
19    end
20
21val _ = tprint "Type parsing with newlines"
22val ty = ``:
23   'a
24``;
25val _ = if Type.compare(ty,Type.alpha) = EQUAL then OK()
26        else die ("\nFAILED: got (" ^ type_to_string ty ^ ")")
27
28local
29infixr $
30fun f $ x = mk_comb(f,x)
31val f = mk_var("f", alpha --> alpha)
32val gg = mk_var("g", beta --> gamma --> alpha)
33val g = mk_var("g", gamma --> alpha)
34val x = mk_var("x", gamma)
35val b = mk_var("b", beta)
36val fgx = f $ g $ x
37in
38
39val _ = tprint "Parsing dollar-sign terms (1)"
40val res1 = ���^f $ ^g $ x���
41val _ = if aconv res1 fgx then OK() else die "FAILED"
42
43val _ = tprint "Parsing dollar-sign terms (2)"
44val res2 = ���^f (^f $ ^g $ ^x)���
45val _ = if aconv res2 (mk_comb(f, fgx)) then OK() else die "FAILED"
46
47val _ = tprint "Parsing dollar-sign terms (3)"
48val res3 = ���^f $ ^gg b $ x���
49val _ = if aconv res3 (f $ (gg $ b) $ x) then OK() else die "FAILED"
50end (* dollar-sign tests local *)
51
52val _ = tprint "test of flatn"
53val _ = let
54    val g = ([], ``a ==> b ==> c ==> d ==> e ==> a /\ b /\ c /\ d /\ e``) : goal
55    val gstk = new_goal g Lib.I ;
56    val gstk = expand (REPEAT DISCH_TAC) gstk ;
57    val gstk = expand (REVERSE CONJ_TAC) gstk ;
58    val gstk = expand (REVERSE CONJ_TAC) gstk ;
59    val gstk = expand (REVERSE CONJ_TAC) gstk ;
60    val gstk = expand (REVERSE CONJ_TAC) gstk ;
61    val gstk = expand ALL_TAC gstk  ; val 1 = length (top_goals gstk) ;
62    val gstk = flatn gstk 2 ; val 3 = length (top_goals gstk) ;
63    val gstk = flatn gstk 2 ; val 5 = length (top_goals gstk) ;
64    val gstk = flatn gstk 2 ; val 5 = length (top_goals gstk) ;
65    val gstk = expand_list (ALLGOALS (FIRST_ASSUM ACCEPT_TAC)) gstk ;
66    val th = extract_thm gstk ;
67  in if (hyp th, concl th) = g then OK() else die "FAILED" end ;
68
69fun mkstk0 t tacopt =
70  let
71    open goalStack
72    val g0 = new_goal ([], t) (fn x => x)
73  in
74    case tacopt of
75        NONE => g0
76      | SOME t => expand t g0
77  end
78
79fun mkstk t = mkstk0 t (SOME (rpt strip_tac))
80
81val _ = set_trace "Goalstack.other_subgoals_pretty_limit" 5
82
83val _ = current_backend := PPBackEnd.vt100_terminal;
84
85fun blue s = "\027[0;1;34m" ^ s ^ "\027[0m"
86fun stksfx n = "\n\n\n" ^ Int.toString n ^ " subgoals"
87
88fun goalstr slist =
89  "\n" ^ String.concatWith "\n\n\n\n" (map blue (List.rev slist)) ^
90  stksfx (length slist)
91
92fun rawstr slist =
93  case slist of
94      [] => raise Fail "Can't happen"
95    | h::t => "\n" ^ String.concatWith "\n\n\n\n" (List.rev t @ [blue h]) ^
96              stksfx (length slist)
97
98fun mkgstkstr strings =
99  let
100    val t = boolSyntax.list_mk_conj (map(fn s => mk_var(s,bool)) strings)
101    val gstk = with_flag (goalStack.chatting, false) mkstk t
102  in
103    HOLPP.pp_to_string 70 goalStack.pp_gstk gstk
104  end
105
106fun test nm pred s =
107  let
108    val _ = tprint nm
109    val strings = map str (explode s)
110    val expected = pred strings
111    val got = mkgstkstr strings
112  in
113    if got = expected then OK()
114    else die ("\nExpected: " ^ String.toString expected ^
115              "\nGot     : " ^ String.toString got)
116  end
117
118val _ = test "Stack printing; small stack" goalstr "abcde"
119val _ = test "Stack printing; big stack" rawstr "abcdefg"
120
121fun narrow_uni_off f =
122  HOLPP.pp_to_string 50
123       (f |> with_flag (Parse.current_backend, PPBackEnd.raw_terminal)
124          |> trace ("Unicode", 0))
125
126val ppgstk = narrow_uni_off goalStack.pp_gstk
127
128fun mkgstkstr t =
129  let
130    val gstk = with_flag (goalStack.chatting, false) mkstk t
131  in
132    ppgstk gstk
133  end
134
135fun mkg0 t = ppgstk (mkstk0 t NONE)
136
137fun mkprfs t =
138    let
139      open Manager
140      val prfs0 = PRFS []
141      val p = new_goalstack ([], t) (fn x => x)
142      val prfs = add p prfs0
143    in
144      narrow_uni_off pp_proofs prfs
145    end
146
147fun testf(nm, t, mk, expected) =
148  let
149    val _ = tprint nm
150    val gstr = mk t
151  in
152    if expected = gstr then OK()
153    else die ("\nFAILED: got:\n\"" ^ String.toString gstr ^ "\"\n" ^
154              "Expected:\n\"" ^ String.toString expected ^ "\"\n")
155  end
156
157val _ = List.app testf [
158("Stack printing; breaks in multiple assumptions",
159 ``(P a b ==> !x y z. Q a x /\ R b y (f z) ==> R2 (ggg a b x y)) /\
160   P (f a) (hhhh b) ==>
161     R2 (ggg (hhhh a) b c dd)``, mkgstkstr,
162 "\n\n\
163 \R2 (ggg (hhhh a) b c dd)\n\
164 \------------------------------------\n\
165 \  0.  P a b ==>\n\
166 \      !x y z.\n\
167 \          Q a x /\\ R b y (f z) ==>\n\
168 \          R2 (ggg a b x y)\n\
169 \  1.  P (f a) (hhhh b)"),
170("Stack printing; more than 10 assumptions",
171 ``p1 /\ p2 /\ p3 /\ p4 /\ p5 /\ p6 /\ p7 /\ p8 /\ p9 /\ p10 /\ p11 ==> q``,
172 mkgstkstr,
173 "\n\n\
174 \q\n\
175 \------------------------------------\n\
176 \  0.  p1\n\
177 \  1.  p2\n\
178 \  2.  p3\n\
179 \  3.  p4\n\
180 \  4.  p5\n\
181 \  5.  p6\n\
182 \  6.  p7\n\
183 \  7.  p8\n\
184 \  8.  p9\n\
185 \  9.  p10\n\
186 \ 10.  p11"),
187("Stack printing; initial goal", ``p /\ q ==> p``, mkg0,
188 "Initial goal:\n\
189 \\n\
190 \\n\
191 \p /\\ q ==> p\n"),
192("Proofs printing; initial goal", ``p /\ q``, mkprfs,
193 "Proof manager status: 1 proof.\n\
194 \1. Incomplete goalstack:\n\
195 \     Initial goal:\n\
196 \     \n\
197 \     p /\\ q\n\
198 \     \n\
199 \     ")
200]
201
202val _ = Parse.current_backend := PPBackEnd.raw_terminal
203
204val _ = app (fn (w,s) => Portable.with_flag(testutils.linewidth,w) tpp s)
205            [(20, "f\n  (longterm =\n   longterm)"),
206             (20, "f\n  (term001 = term002)"),
207             (30, "let\n\
208                  \  v =\n\
209                  \    if gd then th\n\
210                  \    else if gd then th\n\
211                  \    else el\n\
212                  \in\n\
213                  \  v /\\ y"),
214             (80, "f\n\
215                  \  (let\n\
216                  \     x = long expression ;\n\
217                  \     y = long expression ;\n\
218                  \     z = long expression\n\
219                  \   in\n\
220                  \     x /\\ y /\\ z)")
221            ]
222