1 (* Title: ~~/test/../Testcode/test-code.sml
2 Author: Walther Neuper 200222
4 Code used ONLY for ~~/test/*
9 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
10 val f2str : Generate.mout -> TermC.as_string
11 val TESTg_form : Calc.T -> Generate.mout
13 val CalcTreeTEST : Formalise.T list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Celem.safe * Ctree.ctree
14 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
15 Pos.pos' * NEW * Generate.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 * Generate.mout
21 val tac2tac_ : Ctree.ctree -> Pos.pos' -> Tactic.input -> Tactic.T
25 structure Test_Code(**): TEST_CODE(**) =
31 (** test Step.by_tactic + Step.do_next **)
33 type NEW = int list; (*TODO remove*)
35 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
36 delete as soon as TESTg_form -> _mout_ dropped *)
39 val (form, _, _) = Chead.pt_extract ptp
42 Ctree.Form t => Generate.FormKF (UnparseC.term t)
43 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
45 (case p_ of Pos.Pbl => Generate.Problem []
46 | Pos.Met => Generate.Method []
47 | _ => error "TESTg_form: uncovered case",
48 Specify.itms2itemppc (ThyC.get_theory"Isac_Knowledge") gfr pre))
50 (* for quick test-print-out, until 'type inout' is removed *)
51 fun f2str (Generate.FormKF cterm') = cterm'
52 | f2str _ = error "f2str: uncovered case in fun.def.";
54 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
55 compare "fun CalcTree" which DOES decode *)
56 fun CalcTreeTEST [(fmz, sp)] =
58 val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
59 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
60 val f = TESTg_form (pt,p)
61 in (p, []:NEW, f, tac, Celem.Sundef, pt) end
62 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
64 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
65 | me*) tac p _(*NEW remove*) pt =
68 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
69 case Step.by_tactic tac (pt, p) of
70 ("ok", (_, _, ptp)) => ptp
71 | ("unsafe-ok", (_, _, ptp)) => ptp
72 | ("not-applicable",_) => (pt, p)
73 | ("end-of-calculation", (_, _, ptp)) => ptp
74 | ("failure", _) => error "sys-error"
75 | _ => error "me: uncovered case Step.by_tactic"
77 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
78 (case Step.do_next p ((pt, Pos.e_pos'), []) of
79 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
80 | ("helpless", _) => ("helpless: cannot propose tac", [])
81 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
82 | ("end-of-calculation", (ts, _, _)) => ("", ts)
83 | _ => error "me: uncovered case do_next")
86 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
87 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
89 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
90 tac, Celem.Sundef, pt)
94 (** traces for me_trace **)
96 fun (*quiet (Model_Problem) = true
97 |*) quiet (Add_Given _) = true
98 | quiet (Add_Find _) = true
99 | quiet (Add_Relation _) = true
100 | quiet (Specify_Method _) = true
101 | quiet (Specify_Problem _) = true
102 | quiet (Specify_Theory _) = true
105 fun mk_string (ist, ctxt) =
106 ("(" ^ Istate.string_of' ist ^ ",\n"
107 ^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> UnparseC.terms) ^ ")")
109 fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
110 | trace_ist_ctxt (pt, (p, _)) tac =
114 case get_obj g_loc pt p of
116 writeln "Frm, Res: (NONE, NONE)"
117 | (SOME ist_ctxt, NONE) =>
118 (writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");
119 writeln ("Res ..... NONE)"))
120 | (NONE, SOME ist_ctxt) =>
121 (writeln ("Frm ..... (NONE,");
122 writeln ("Res ..... SOME " ^ mk_string ist_ctxt ^ " )"))
123 | (SOME ic_frm, SOME ic_res) =>
124 (writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");
125 writeln ("Res ..... SOME " ^ mk_string ic_res ^ " )"))
128 (** test Step.by_tactic + Step.do_next with tracing **)
130 fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
131 | me*) (pt, p) tac trace =
133 val _ = if quiet tac then () else
134 writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
136 (*Step.by_tactic is here for testing by me; do_next would suffice for doing steps*)
137 case Step.by_tactic tac (pt, p) of
138 ("ok", (_, _, ptp)) => ptp
139 | ("unsafe-ok", (_, _, ptp)) => ptp
140 | ("not-applicable",_) => (pt, p)
141 | ("end-of-calculation", (_, _, ptp)) => ptp
142 | ("failure", _) => error "sys-error"
143 | _ => error "me: uncovered case Step.by_tactic"
144 val _ = trace (pt', p') tac
145 val (_, ts, (pt'', p'')) =
146 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
147 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
148 ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
149 | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
150 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state) (*intermed.from specify*)
151 | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
152 | _ => error "me: uncovered case do_next")
155 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
156 | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
157 val _ = if quiet tac then () else
158 writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
159 val _ = trace (pt'', p'') tac
161 ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))
164 fun tac2tac_ pt p m =
165 case Step.check m (pt, p) of
166 Applicable.Yes m' => m'
167 | Applicable.No _ => error ("tac2mstp': fails with" ^ Tactic.input_to_string m);