1 (* Title: Tools/isac/Testcode/test-code.sml
2 Author: Walther Neuper 200222
4 Code used ONLY for $ISABELLE_ISAC_TEST/Tools/isac/*
9 type NEW (* TODO: refactor "fun me" with Calc.state_pre and remove *)
10 val f2str : Test_Out.mout -> TermC.as_string
11 val TESTg_form : Proof.context -> Calc.T -> Test_Out.mout
13 val init_calc : Proof.context -> Formalise.T list -> Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree
14 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
15 Pos.pos' * NEW * Test_Out.mout * Tactic.input * Celem.safe * Ctree.ctree
17 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
18 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
19 Calc.T * Tactic.input * Test_Out.mout
21 val init_calc': Proof.context -> Formalise.T list -> Tactic.input * Calc.T
22 val me': Tactic.input * Calc.T -> Tactic.input * Calc.T
24 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
28 structure Test_Code(**): TEST_CODE(**) =
34 (** test Step.by_tactic + Step.do_next **)
36 type NEW = int list; (*TODO remove*)
38 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
39 delete as soon as TESTg_form -> _mout_ dropped *)
40 fun TESTg_form ctxt ptp =
42 val (form, _, _) = ME_Misc.pt_extract ctxt ptp
45 Ctree.Form t => Test_Out.FormKF (UnparseC.term ctxt t)
46 | Ctree.ModSpec (_, p_, _, gfr, where_, _) =>
48 (case p_ of Pos.Pbl => Test_Out.Problem []
49 | Pos.Met => Test_Out.MethodC []
50 | _ => raise ERROR "TESTg_form: uncovered case",
51 P_Model.from (Proof_Context.theory_of ctxt) gfr where_))
53 (* for quick test-print-out, until 'type inout' is removed *)
54 fun f2str (Test_Out.FormKF cterm') = cterm'
55 | f2str _ = raise ERROR "f2str: uncovered case in fun.def.";
57 (* create a calc-tree *)
58 fun init_calc ctxt [(model, refs as (thy_id, _, _))] =
60 (*old* )val ctxt = thy_id |> ThyC.get_theory_PIDE ctxt |> Proof_Context.init_global
61 ( *new*)val thy = thy_id |> ThyC.get_theory_PIDE ctxt (*^^^^^^^^^^^^^^^^^^^^^^^^^ misleading*)
62 val ((pt, p), tacis) = Step_Specify.initialise' thy (model, refs)
63 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
64 val f = TESTg_form ctxt (pt,p)
65 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
66 | init_calc _ _ = raise ERROR "Tess_Code.init_calc: uncovered case"
68 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
69 | me*) tac p _(*NEW remove*) pt =
71 val ctxt = Ctree.get_ctxt pt p
73 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
74 case Step.by_tactic tac (pt, p) of
75 ("ok", (_, _, ptp)) => ptp
76 | ("unsafe-ok", (_, _, ptp)) => ptp
77 | ("not-applicable",_) => (pt, p)
78 | ("end-of-calculation", (_, _, ptp)) => ptp
79 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
80 | _ => raise ERROR "me: uncovered case Step.by_tactic"
82 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
83 (case Step.do_next p ((pt, Pos.e_pos'), []) of
84 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
85 | ("helpless", _) => ("helpless: cannot propose tac", [])
86 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
87 | ("end-of-calculation", (ts, _, _)) => ("", ts)
88 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
89 | _ => raise ERROR "me: uncovered case Step.do_next")
92 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
93 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
95 (p, [] : NEW, TESTg_form ctxt (pt, p) (* form output comes from Step.by_tactic *),
96 tac, Celem.Sundef, pt)
100 (** traces for me_trace **)
102 fun (*quiet (Model_Problem) = true
103 |*) quiet (Add_Given _) = true
104 | quiet (Add_Find _) = true
105 | quiet (Add_Relation _) = true
106 | quiet (Specify_Method _) = true
107 | quiet (Specify_Problem _) = true
108 | quiet (Specify_Theory _) = true
111 fun mk_string (ist, ctxt) =
112 ("(" ^ Istate.string_of' ist ^ ",\n"
113 ^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> UnparseC.terms ctxt) ^ ")")
115 fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
116 | trace_ist_ctxt (pt, (p, _)) tac =
120 case get_obj g_loc pt p of
122 writeln "Frm, Res: (NONE, NONE)"
123 | (SOME ist_ctxt, NONE) =>
124 (writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");
125 writeln ("Res ..... NONE)"))
126 | (NONE, SOME ist_ctxt) =>
127 (writeln ("Frm ..... (NONE,");
128 writeln ("Res ..... SOME " ^ mk_string ist_ctxt ^ " )"))
129 | (SOME ic_frm, SOME ic_res) =>
130 (writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");
131 writeln ("Res ..... SOME " ^ mk_string ic_res ^ " )"))
134 (** test Step.by_tactic + Step.do_next with tracing **)
136 fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
137 | me*) (pt, p) tac trace =
139 val ctxt = Ctree.get_ctxt pt p
140 val _ = if quiet tac then () else
141 writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^
142 Tactic.input_to_string ctxt tac ^ " ==================================");
144 case Step.by_tactic tac (pt, p) of
145 ("ok", (_, _, ptp)) => ptp
146 | ("unsafe-ok", (_, _, ptp)) => ptp
147 | ("not-applicable",_) => (pt, p)
148 | ("end-of-calculation", (_, _, ptp)) => ptp
149 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
150 | _ => raise ERROR "me: uncovered case Step.by_tactic"
151 val _ = trace (pt', p') tac
152 val (_, ts, (pt'', p'')) =
153 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
154 ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
155 | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
156 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state)
157 | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
158 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
159 | _ => raise ERROR "me: uncovered case Step.do_next")
162 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
163 | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
164 val _ = if quiet tac then () else
165 writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^
166 Tactic.input_to_string ctxt tac'' ^ "----------------------------------");
167 val _ = trace (pt'', p'') tac
169 ((pt', p'), tac'', TESTg_form ctxt (pt', p') (* form output comes from Step.by_tactic *))
172 fun tac2tac_ pt p m =
174 val ctxt = Ctree.get_ctxt pt p
176 case Step.check m (pt, p) of
177 Applicable.Yes m' => m'
178 | Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string ctxt m)
183 fun init_calc' ctxt [(model, refs as (thy_id, _, _))] =
185 val thy = thy_id |> ThyC.get_theory_PIDE ctxt
186 val ((pt, p), _) = Step_Specify.initialise' thy (model, refs)
188 (Tactic.Model_Problem, (pt, p)) (* thus <Output> shows Tactic on top *)
190 | init_calc' _ _ = raise ERROR "Test_Code.init_calc' @{context}: uncovered case"
192 fun me' (tac, (pt, p)) = (* thus <Output> shows Tactic on top *)
195 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
196 case Step.by_tactic tac (pt, p) of
197 ("ok", (_, _, ptp)) => ptp
198 | ("unsafe-ok", (_, _, ptp)) => ptp
199 | ("not-applicable",_) => (pt, p)
200 | ("end-of-calculation", (_, _, ptp)) => ptp
201 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
202 | _ => raise ERROR "me: uncovered case Step.by_tactic"
204 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
205 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
206 ("ok", ((tac', _, _) :: _, _, _)) => tac'
207 | ("helpless", _) => Tactic.Empty_Tac
208 | ("dummy", ((tac', _, _) :: _, _, _)) => tac'
209 | ("end-of-calculation", _) => Tactic.End_Proof'
210 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
211 | _ => raise ERROR "me: uncovered case Step.do_next")
213 (tac', (pt', p')) (* thus <Output> shows Tactic on top *)
214 (* ^^^^----- is the next step after "(pt', p')", but we prefer ----------------^^^^^^^^^^^^^ *)