wenzelm@60192
|
1 |
(* Title: Tools/isac/Testcode/test-code.sml
|
walther@59814
|
2 |
Author: Walther Neuper 200222
|
walther@59814
|
3 |
|
wenzelm@60217
|
4 |
Code used ONLY for $ISABELLE_ISAC_TEST/Tools/isac/*
|
walther@59814
|
5 |
*)
|
walther@59814
|
6 |
|
walther@59814
|
7 |
signature TEST_CODE =
|
walther@59814
|
8 |
sig
|
walther@59981
|
9 |
type NEW (* TODO: refactor "fun me" with Calc.state_pre and remove *)
|
walther@59959
|
10 |
val f2str : Test_Out.mout -> TermC.as_string
|
walther@59959
|
11 |
val TESTg_form : Calc.T -> Test_Out.mout
|
walther@59901
|
12 |
|
walther@59959
|
13 |
val CalcTreeTEST : Formalise.T list -> Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree
|
walther@59846
|
14 |
val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
|
walther@59959
|
15 |
Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree
|
walther@59901
|
16 |
|
walther@59814
|
17 |
val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
|
walther@59814
|
18 |
val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
|
walther@59959
|
19 |
Calc.T * Tactic.input * Test_Out.mout
|
walther@59922
|
20 |
|
walther@60024
|
21 |
val CalcTreeTEST': Formalise.T list -> Tactic.input * Calc.T
|
walther@60024
|
22 |
val me': Tactic.input * Calc.T -> Tactic.input * Calc.T
|
walther@60024
|
23 |
|
walther@59922
|
24 |
val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
|
walther@59814
|
25 |
end
|
walther@59814
|
26 |
|
walther@59814
|
27 |
(**)
|
walther@59814
|
28 |
structure Test_Code(**): TEST_CODE(**) =
|
walther@59814
|
29 |
struct
|
walther@59814
|
30 |
(**)
|
walther@59814
|
31 |
open Tactic
|
walther@59814
|
32 |
open Ctree
|
walther@59814
|
33 |
|
walther@59814
|
34 |
(** test Step.by_tactic + Step.do_next **)
|
walther@59814
|
35 |
|
walther@59814
|
36 |
type NEW = int list; (*TODO remove*)
|
walther@59814
|
37 |
|
walther@59814
|
38 |
(* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
|
walther@59814
|
39 |
delete as soon as TESTg_form -> _mout_ dropped *)
|
walther@59814
|
40 |
fun TESTg_form ptp =
|
walther@59814
|
41 |
let
|
walther@59983
|
42 |
val (form, _, _) = ME_Misc.pt_extract ptp
|
walther@59814
|
43 |
in
|
walther@59814
|
44 |
case form of
|
walther@59959
|
45 |
Ctree.Form t => Test_Out.FormKF (UnparseC.term t)
|
walther@59814
|
46 |
| Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
|
walther@59959
|
47 |
Test_Out.PpcKF (
|
walther@59959
|
48 |
(case p_ of Pos.Pbl => Test_Out.Problem []
|
walther@60154
|
49 |
| Pos.Met => Test_Out.MethodC []
|
walther@59962
|
50 |
| _ => raise ERROR "TESTg_form: uncovered case",
|
walther@59969
|
51 |
P_Model.from (ThyC.get_theory"Isac_Knowledge") gfr pre))
|
walther@59814
|
52 |
end
|
walther@59814
|
53 |
(* for quick test-print-out, until 'type inout' is removed *)
|
walther@59959
|
54 |
fun f2str (Test_Out.FormKF cterm') = cterm'
|
walther@59962
|
55 |
| f2str _ = raise ERROR "f2str: uncovered case in fun.def.";
|
walther@59814
|
56 |
|
Walther@60557
|
57 |
(* create a calc-tree *)
|
Walther@60557
|
58 |
fun CalcTreeTEST [(model, refs as (thy_id, _, _))] =
|
walther@59814
|
59 |
let
|
Walther@60557
|
60 |
val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
|
Walther@60557
|
61 |
val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
|
walther@59814
|
62 |
val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
|
walther@59814
|
63 |
val f = TESTg_form (pt,p)
|
walther@59937
|
64 |
in (p, []:NEW, f, tac, Celem.Sundef, pt) end
|
walther@59962
|
65 |
| CalcTreeTEST _ = raise ERROR "CalcTreeTEST: uncovered case"
|
walther@59814
|
66 |
|
walther@59814
|
67 |
fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
|
walther@59814
|
68 |
| me*) tac p _(*NEW remove*) pt =
|
walther@59814
|
69 |
let
|
walther@59814
|
70 |
val (pt, p) =
|
walther@59814
|
71 |
(*Step.by_tactic is here for testing by me; do_next would suffice in me*)
|
walther@59814
|
72 |
case Step.by_tactic tac (pt, p) of
|
walther@59814
|
73 |
("ok", (_, _, ptp)) => ptp
|
walther@59814
|
74 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
walther@59814
|
75 |
| ("not-applicable",_) => (pt, p)
|
walther@59814
|
76 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
walther@60021
|
77 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
|
walther@59962
|
78 |
| _ => raise ERROR "me: uncovered case Step.by_tactic"
|
walther@59814
|
79 |
val (_, ts) =
|
walther@59814
|
80 |
(*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
|
walther@59814
|
81 |
(case Step.do_next p ((pt, Pos.e_pos'), []) of
|
walther@59814
|
82 |
("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
|
walther@59814
|
83 |
| ("helpless", _) => ("helpless: cannot propose tac", [])
|
walther@59814
|
84 |
| ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
|
walther@59814
|
85 |
| ("end-of-calculation", (ts, _, _)) => ("", ts)
|
walther@60021
|
86 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
|
walther@60021
|
87 |
| _ => raise ERROR "me: uncovered case Step.do_next")
|
walther@59814
|
88 |
val tac =
|
walther@59814
|
89 |
case ts of
|
walther@59814
|
90 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@59814
|
91 |
| _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
walther@59814
|
92 |
in
|
walther@59814
|
93 |
(p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
|
walther@59937
|
94 |
tac, Celem.Sundef, pt)
|
walther@59814
|
95 |
end
|
walther@59814
|
96 |
|
walther@59814
|
97 |
|
walther@59814
|
98 |
(** traces for me_trace **)
|
walther@59814
|
99 |
|
walther@59814
|
100 |
fun (*quiet (Model_Problem) = true
|
walther@59814
|
101 |
|*) quiet (Add_Given _) = true
|
walther@59814
|
102 |
| quiet (Add_Find _) = true
|
walther@59814
|
103 |
| quiet (Add_Relation _) = true
|
walther@59814
|
104 |
| quiet (Specify_Method _) = true
|
walther@59814
|
105 |
| quiet (Specify_Problem _) = true
|
walther@59814
|
106 |
| quiet (Specify_Theory _) = true
|
walther@59814
|
107 |
| quiet _ = false
|
walther@59814
|
108 |
|
walther@59814
|
109 |
fun mk_string (ist, ctxt) =
|
walther@59844
|
110 |
("(" ^ Istate.string_of' ist ^ ",\n"
|
walther@59868
|
111 |
^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> UnparseC.terms) ^ ")")
|
walther@59814
|
112 |
|
walther@59814
|
113 |
fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
|
walther@59814
|
114 |
| trace_ist_ctxt (pt, (p, _)) tac =
|
walther@59814
|
115 |
if quiet tac
|
walther@59814
|
116 |
then ()
|
walther@59814
|
117 |
else
|
walther@59814
|
118 |
case get_obj g_loc pt p of
|
walther@59814
|
119 |
(NONE, NONE) =>
|
walther@59814
|
120 |
writeln "Frm, Res: (NONE, NONE)"
|
walther@59814
|
121 |
| (SOME ist_ctxt, NONE) =>
|
walther@59814
|
122 |
(writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");
|
walther@59814
|
123 |
writeln ("Res ..... NONE)"))
|
walther@59814
|
124 |
| (NONE, SOME ist_ctxt) =>
|
walther@59814
|
125 |
(writeln ("Frm ..... (NONE,");
|
walther@59814
|
126 |
writeln ("Res ..... SOME " ^ mk_string ist_ctxt ^ " )"))
|
walther@59814
|
127 |
| (SOME ic_frm, SOME ic_res) =>
|
walther@59814
|
128 |
(writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");
|
walther@59814
|
129 |
writeln ("Res ..... SOME " ^ mk_string ic_res ^ " )"))
|
walther@59814
|
130 |
|
walther@59814
|
131 |
|
walther@59814
|
132 |
(** test Step.by_tactic + Step.do_next with tracing **)
|
walther@59814
|
133 |
|
walther@59814
|
134 |
fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
|
walther@59814
|
135 |
| me*) (pt, p) tac trace =
|
walther@59814
|
136 |
let
|
walther@59814
|
137 |
val _ = if quiet tac then () else
|
walther@59846
|
138 |
writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
|
walther@59814
|
139 |
val (pt', p') =
|
walther@59814
|
140 |
case Step.by_tactic tac (pt, p) of
|
walther@59814
|
141 |
("ok", (_, _, ptp)) => ptp
|
walther@59814
|
142 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
walther@59814
|
143 |
| ("not-applicable",_) => (pt, p)
|
walther@59814
|
144 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
walther@60024
|
145 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
|
walther@59962
|
146 |
| _ => raise ERROR "me: uncovered case Step.by_tactic"
|
walther@59814
|
147 |
val _ = trace (pt', p') tac
|
walther@59814
|
148 |
val (_, ts, (pt'', p'')) =
|
walther@59814
|
149 |
(case Step.do_next p' ((pt', Pos.e_pos'), []) of
|
walther@59814
|
150 |
("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
|
walther@59814
|
151 |
| ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
|
walther@60024
|
152 |
| ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state)
|
walther@59814
|
153 |
| ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
|
walther@60024
|
154 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
|
walther@60024
|
155 |
| _ => raise ERROR "me: uncovered case Step.do_next")
|
walther@59814
|
156 |
val tac'' =
|
walther@59814
|
157 |
case ts of
|
walther@59814
|
158 |
tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
|
walther@59814
|
159 |
| _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
|
walther@59814
|
160 |
val _ = if quiet tac then () else
|
walther@59846
|
161 |
writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
|
walther@59814
|
162 |
val _ = trace (pt'', p'') tac
|
walther@59814
|
163 |
in
|
walther@59814
|
164 |
((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
|
walther@59814
|
165 |
end
|
walther@59814
|
166 |
|
walther@59922
|
167 |
fun tac2tac_ pt p m =
|
walther@59922
|
168 |
case Step.check m (pt, p) of
|
walther@59922
|
169 |
Applicable.Yes m' => m'
|
walther@59962
|
170 |
| Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string m);
|
walther@59922
|
171 |
|
walther@60024
|
172 |
|
walther@60024
|
173 |
(** me' for |> **)
|
Walther@60557
|
174 |
fun CalcTreeTEST' [(model, refs as (thy_id, _, _))] =
|
walther@60024
|
175 |
let
|
Walther@60557
|
176 |
val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
|
Walther@60557
|
177 |
val ((pt, p), _) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
|
walther@60024
|
178 |
in
|
walther@60024
|
179 |
(Tactic.Model_Problem, (pt, p)) (* thus <Output> shows Tactic on top *)
|
walther@60024
|
180 |
end
|
walther@60024
|
181 |
| CalcTreeTEST' _ = raise ERROR "CalcTreeTEST': uncovered case"
|
walther@60024
|
182 |
|
walther@60024
|
183 |
fun me' (tac, (pt, p)) = (* thus <Output> shows Tactic on top *)
|
walther@60024
|
184 |
let
|
walther@60024
|
185 |
val (pt', p') =
|
walther@60024
|
186 |
(*Step.by_tactic is here for testing by me; do_next would suffice in me*)
|
walther@60024
|
187 |
case Step.by_tactic tac (pt, p) of
|
walther@60024
|
188 |
("ok", (_, _, ptp)) => ptp
|
walther@60024
|
189 |
| ("unsafe-ok", (_, _, ptp)) => ptp
|
walther@60024
|
190 |
| ("not-applicable",_) => (pt, p)
|
walther@60024
|
191 |
| ("end-of-calculation", (_, _, ptp)) => ptp
|
walther@60024
|
192 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
|
walther@60024
|
193 |
| _ => raise ERROR "me: uncovered case Step.by_tactic"
|
walther@60024
|
194 |
val tac' =
|
walther@60024
|
195 |
(*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
|
walther@60024
|
196 |
(case Step.do_next p' ((pt', Pos.e_pos'), []) of
|
walther@60024
|
197 |
("ok", ((tac', _, _) :: _, _, _)) => tac'
|
walther@60024
|
198 |
| ("helpless", _) => Tactic.Empty_Tac
|
walther@60024
|
199 |
| ("dummy", ((tac', _, _) :: _, _, _)) => tac'
|
walther@60024
|
200 |
| ("end-of-calculation", _) => Tactic.End_Proof'
|
walther@60024
|
201 |
| ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
|
walther@60024
|
202 |
| _ => raise ERROR "me: uncovered case Step.do_next")
|
walther@60024
|
203 |
in
|
walther@60024
|
204 |
(tac', (pt', p')) (* thus <Output> shows Tactic on top *)
|
walther@60024
|
205 |
(* ^^^^----- is the next step after "(pt', p')", but we prefer ----------------^^^^^^^^^^^^^ *)
|
walther@60024
|
206 |
end
|
walther@60024
|
207 |
|
walther@59814
|
208 |
(**)end(**)
|