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 : Calc.T -> Test_Out.mout
13 val CalcTreeTEST : 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 CalcTreeTEST': 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 *)
42 val (form, _, _) = ME_Misc.pt_extract ptp
45 Ctree.Form t => Test_Out.FormKF (UnparseC.term t)
46 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
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 (ThyC.get_theory"Isac_Knowledge") gfr pre))
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 CalcTreeTEST [(model, refs as (thy_id, _, _))] =
60 val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
61 val ((pt, p), tacis) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
62 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
63 val f = TESTg_form (pt,p)
64 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
65 | CalcTreeTEST _ = raise ERROR "CalcTreeTEST: uncovered case"
67 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
68 | me*) tac p _(*NEW remove*) pt =
71 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
72 case Step.by_tactic tac (pt, p) of
73 ("ok", (_, _, ptp)) => ptp
74 | ("unsafe-ok", (_, _, ptp)) => ptp
75 | ("not-applicable",_) => (pt, p)
76 | ("end-of-calculation", (_, _, ptp)) => ptp
77 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
78 | _ => raise ERROR "me: uncovered case Step.by_tactic"
80 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
81 (case Step.do_next p ((pt, Pos.e_pos'), []) of
82 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
83 | ("helpless", _) => ("helpless: cannot propose tac", [])
84 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
85 | ("end-of-calculation", (ts, _, _)) => ("", ts)
86 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
87 | _ => raise ERROR "me: uncovered case Step.do_next")
90 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
91 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
93 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
94 tac, Celem.Sundef, pt)
98 (** traces for me_trace **)
100 fun (*quiet (Model_Problem) = true
101 |*) quiet (Add_Given _) = true
102 | quiet (Add_Find _) = true
103 | quiet (Add_Relation _) = true
104 | quiet (Specify_Method _) = true
105 | quiet (Specify_Problem _) = true
106 | quiet (Specify_Theory _) = true
109 fun mk_string (ist, ctxt) =
110 ("(" ^ Istate.string_of' ist ^ ",\n"
111 ^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> UnparseC.terms) ^ ")")
113 fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
114 | trace_ist_ctxt (pt, (p, _)) tac =
118 case get_obj g_loc pt p of
120 writeln "Frm, Res: (NONE, NONE)"
121 | (SOME ist_ctxt, NONE) =>
122 (writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");
123 writeln ("Res ..... NONE)"))
124 | (NONE, SOME ist_ctxt) =>
125 (writeln ("Frm ..... (NONE,");
126 writeln ("Res ..... SOME " ^ mk_string ist_ctxt ^ " )"))
127 | (SOME ic_frm, SOME ic_res) =>
128 (writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");
129 writeln ("Res ..... SOME " ^ mk_string ic_res ^ " )"))
132 (** test Step.by_tactic + Step.do_next with tracing **)
134 fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
135 | me*) (pt, p) tac trace =
137 val _ = if quiet tac then () else
138 writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
140 case Step.by_tactic tac (pt, p) of
141 ("ok", (_, _, ptp)) => ptp
142 | ("unsafe-ok", (_, _, ptp)) => ptp
143 | ("not-applicable",_) => (pt, p)
144 | ("end-of-calculation", (_, _, ptp)) => ptp
145 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
146 | _ => raise ERROR "me: uncovered case Step.by_tactic"
147 val _ = trace (pt', p') tac
148 val (_, ts, (pt'', p'')) =
149 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
150 ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
151 | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
152 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state)
153 | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
154 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
155 | _ => raise ERROR "me: uncovered case Step.do_next")
158 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
159 | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
160 val _ = if quiet tac then () else
161 writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
162 val _ = trace (pt'', p'') tac
164 ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
167 fun tac2tac_ pt p m =
168 case Step.check m (pt, p) of
169 Applicable.Yes m' => m'
170 | Applicable.No _ => raise ERROR ("tac2mstp': fails with" ^ Tactic.input_to_string m);
174 fun CalcTreeTEST' [(model, refs as (thy_id, _, _))] =
176 val ctxt = thy_id |> ThyC.get_theory |> Proof_Context.init_global; (*will become an argument*)
177 val ((pt, p), _) = Step_Specify.nxt_specify_init_calc ctxt (model, refs)
179 (Tactic.Model_Problem, (pt, p)) (* thus <Output> shows Tactic on top *)
181 | CalcTreeTEST' _ = raise ERROR "CalcTreeTEST': uncovered case"
183 fun me' (tac, (pt, p)) = (* thus <Output> shows Tactic on top *)
186 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
187 case Step.by_tactic tac (pt, p) of
188 ("ok", (_, _, ptp)) => ptp
189 | ("unsafe-ok", (_, _, ptp)) => ptp
190 | ("not-applicable",_) => (pt, p)
191 | ("end-of-calculation", (_, _, ptp)) => ptp
192 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.by_tactic"
193 | _ => raise ERROR "me: uncovered case Step.by_tactic"
195 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
196 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
197 ("ok", ((tac', _, _) :: _, _, _)) => tac'
198 | ("helpless", _) => Tactic.Empty_Tac
199 | ("dummy", ((tac', _, _) :: _, _, _)) => tac'
200 | ("end-of-calculation", _) => Tactic.End_Proof'
201 | ("failure", _) => raise ERROR "sys-raise ERROR by Step.do_next"
202 | _ => raise ERROR "me: uncovered case Step.do_next")
204 (tac', (pt', p')) (* thus <Output> shows Tactic on top *)
205 (* ^^^^----- is the next step after "(pt', p')", but we prefer ----------------^^^^^^^^^^^^^ *)