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