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 -> Rule.cterm'
11 val TESTg_form : Calc.T -> Generate.mout
12 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
13 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
14 Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
15 val trace_ist_ctxt: Calc.T -> Tactic.input -> unit
16 val me_trace: Calc.T -> Tactic.input -> (Calc.T -> Tactic.input -> unit) ->
17 Calc.T * Tactic.input * Generate.mout
21 structure Test_Code(**): TEST_CODE(**) =
27 (** test Step.by_tactic + Step.do_next **)
29 type NEW = int list; (*TODO remove*)
31 (* 15.8.03 for me with loc_specify/solve, nxt_specify/solve
32 delete as soon as TESTg_form -> _mout_ dropped *)
35 val (form, _, _) = Chead.pt_extract ptp
38 Ctree.Form t => Generate.FormKF (Rule.term2str t)
39 | Ctree.ModSpec (_, p_, _, gfr, pre, _) =>
41 (case p_ of Pos.Pbl => Generate.Problem []
42 | Pos.Met => Generate.Method []
43 | _ => error "TESTg_form: uncovered case",
44 Specify.itms2itemppc (Celem.assoc_thy"Isac_Knowledge") gfr pre))
46 (* for quick test-print-out, until 'type inout' is removed *)
47 fun f2str (Generate.FormKF cterm') = cterm'
48 | f2str _ = error "f2str: uncovered case in fun.def.";
50 (* create a calc-tree; for use within sml: thus "^^^" NOT decoded to "^" etc;
51 compare "fun CalcTree" which DOES decode *)
52 fun CalcTreeTEST [(fmz, sp)] =
54 val ((pt, p), tacis) = SpecifyNEW.nxt_specify_init_calc (fmz, sp)
55 val tac = case tacis of [] => Tactic.Empty_Tac | _ => (#1 o hd) tacis
56 val f = TESTg_form (pt,p)
57 in (p, []:NEW, f, tac, Telem.Sundef, pt) end
58 | CalcTreeTEST _ = error "CalcTreeTEST: uncovered case"
60 fun me (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
61 | me*) tac p _(*NEW remove*) pt =
64 (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
65 case Step.by_tactic tac (pt, p) of
66 ("ok", (_, _, ptp)) => ptp
67 | ("unsafe-ok", (_, _, ptp)) => ptp
68 | ("not-applicable",_) => (pt, p)
69 | ("end-of-calculation", (_, _, ptp)) => ptp
70 | ("failure", _) => error "sys-error"
71 | _ => error "me: uncovered case Step.by_tactic"
73 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
74 (case Step.do_next p ((pt, Pos.e_pos'), []) of
75 ("ok", (ts as (_, _, _) :: _, _, _)) => ("", ts)
76 | ("helpless", _) => ("helpless: cannot propose tac", [])
77 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts) (*intermed.from specify*)
78 | ("end-of-calculation", (ts, _, _)) => ("", ts)
79 | _ => error "me: uncovered case do_next")
82 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
83 | _ => if p = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
85 (p, [] : NEW, TESTg_form (pt, p) (* form output comes from Step.by_tactic *),
86 tac, Telem.Sundef, pt)
90 (** traces for me_trace **)
92 fun (*quiet (Model_Problem) = true
93 |*) quiet (Add_Given _) = true
94 | quiet (Add_Find _) = true
95 | quiet (Add_Relation _) = true
96 | quiet (Specify_Method _) = true
97 | quiet (Specify_Problem _) = true
98 | quiet (Specify_Theory _) = true
101 fun mk_string (ist, ctxt) =
102 ("(" ^ Istate.string_of' ist ^ ",\n"
103 ^ "... ctxt: " ^ (ctxt |> ContextC.get_assumptions |> Rule.terms2str) ^ ")")
105 fun trace_ist_ctxt (EmptyPtree , ([], Pos.Und)) _ = ()
106 | trace_ist_ctxt (pt, (p, _)) tac =
110 case get_obj g_loc pt p of
112 writeln "Frm, Res: (NONE, NONE)"
113 | (SOME ist_ctxt, NONE) =>
114 (writeln ("Frm ..... (SOME " ^ mk_string ist_ctxt ^ " ,");
115 writeln ("Res ..... NONE)"))
116 | (NONE, SOME ist_ctxt) =>
117 (writeln ("Frm ..... (NONE,");
118 writeln ("Res ..... SOME " ^ mk_string ist_ctxt ^ " )"))
119 | (SOME ic_frm, SOME ic_res) =>
120 (writeln ("Frm ..... (SOME " ^ mk_string ic_frm ^ " ,");
121 writeln ("Res ..... SOME " ^ mk_string ic_res ^ " )"))
124 (** test Step.by_tactic + Step.do_next with tracing **)
126 fun me_trace (*(Empty_Tac) p _ _ = raise ERROR ("me: Empty_Tac at " ^ pos'2str p)
127 | me*) (pt, p) tac trace =
129 val _ = if quiet tac then () else
130 writeln ("========= " ^ Pos.pos'2str p ^ "========= Step.by_tactic: " ^ Tactic.input_to_string tac ^ " ==================================");
132 (*Step.by_tactic is here for testing by me; do_next would suffice for doing steps*)
133 case Step.by_tactic tac (pt, p) of
134 ("ok", (_, _, ptp)) => ptp
135 | ("unsafe-ok", (_, _, ptp)) => ptp
136 | ("not-applicable",_) => (pt, p)
137 | ("end-of-calculation", (_, _, ptp)) => ptp
138 | ("failure", _) => error "sys-error"
139 | _ => error "me: uncovered case Step.by_tactic"
140 val _ = trace (pt', p') tac
141 val (_, ts, (pt'', p'')) =
142 (*step's correct ctree is not tested in me, but in autocalc or Step.by_term*)
143 (case Step.do_next p' ((pt', Pos.e_pos'), []) of
144 ("ok", (ts as [(_, _, _)(*, _, _, ...*)], _, (pt'', p''))) => ("", ts, (pt'', p''))
145 | ("helpless", _) => ("helpless: cannot propose tac", [], Ctree.e_state)
146 | ("dummy", (ts as (_, _, _) :: _, _, _)) => ("", ts, Ctree.e_state) (*intermed.from specify*)
147 | ("end-of-calculation", (ts, _, _)) => ("", ts, Ctree.e_state)
148 | _ => error "me: uncovered case do_next")
151 tacis as (_::_) => let val (tac, _, _) = last_elem tacis in tac end
152 | _ => if p' = ([], Pos.Res) then Tactic.End_Proof' else Tactic.Empty_Tac;
153 val _ = if quiet tac then () else
154 writeln ("--------- " ^ Pos.pos'2str p' ^ "--------- Step.do_next \<rightarrow> " ^ Tactic.input_to_string tac'' ^ "----------------------------------");
155 val _ = trace (pt'', p'') tac
157 ((pt', p'), tac'', TESTg_form (pt', p') (* form output comes from Step.by_tactic *))