1 (* Title: solve an example by interpreting a method's script
2 Author: Walther Neuper 1999
3 (c) copyright due to lincense terms.
6 signature SOLVE_PHASE =
8 datatype auto = CompleteCalc | CompleteCalcHead | CompleteModel | CompleteSubpbl
9 | CompleteToSubpbl | Steps of int
10 val autoord : auto -> int
12 val all_solve : auto -> Ctree.pos' list -> Calc.T ->
13 string * Ctree.pos' list * (Ctree.ctree * (int list * Ctree.pos_))
15 auto -> Ctree.pos' list -> Calc.T -> string * Ctree.pos' list * Calc.T
16 val inform : Chead.calcstate' -> string -> string * Chead.calcstate'
18 val detailrls : Ctree.ctree -> Ctree.pos' -> string * Ctree.ctree * Ctree.pos'
19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
21 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
23 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
25 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
30 structure Solve(**): SOLVE_PHASE(**) =
36 type squ = ctree; (* TODO: safe etc. *)
38 (* tell how may steps of a calculation should be done by "fun autocalc"
39 FIXXXME040624: does NOT match interfaces/ITOCalc.java
40 TODO.WN0512 redesign togehter with autocalc ? *)
42 Steps of int (*1 do #int steps (may stop in model/specify)
43 IS VERY INEFFICIENT IN MODEL/SPECIY *)
44 | CompleteModel (*2 complete modeling
45 if model complete, finish specifying *)
46 | CompleteCalcHead (*3 complete model/specify in one go *)
47 | CompleteToSubpbl (*4 stop at the next begin of a subproblem,
48 if none, complete the actual (sub)problem *)
49 | CompleteSubpbl (*5 complete the actual (sub)problem (incl.ev.subproblems) *)
50 | CompleteCalc; (*6 complete the calculation as a whole *)
52 fun autoord (Steps _ ) = 1
53 | autoord CompleteModel = 2
54 | autoord CompleteCalcHead = 3
55 | autoord CompleteToSubpbl = 4
56 | autoord CompleteSubpbl = 5
57 | autoord CompleteCalc = 6;
59 fun complete_solve auto c (ptp as (_, p as (_, p_))) =
61 then ("end-of-calculation", [], ptp)
63 if member op = [Pbl,Met] p_
66 val ptp = Chead.all_modspec ptp
67 val (_, c', ptp) = all_solve auto c ptp
68 in complete_solve auto (c @ c') ptp end
70 case Step_Solve.do_next ptp of
71 (_, ((Tactic.Subproblem _, _, _) :: _, c', ptp')) =>
73 then ("ok", c @ c', ptp)
76 val ptp = Chead.all_modspec ptp'
77 val (_, c'', ptp) = all_solve auto (c @ c') ptp
78 in complete_solve auto (c @ c'@ c'') ptp end
79 | (_, ((Tactic.Check_Postcond _, _, _) :: _, c', ptp' as (_, p'))) =>
80 if autoord auto < 6 orelse p' = ([], Res)
81 then ("ok", c @ c', ptp')
82 else complete_solve auto (c @ c') ptp'
83 | (_, ((Tactic.End_Detail, _, _) :: _, c', ptp')) =>
85 then ("ok", c @ c', ptp')
86 else complete_solve auto (c @ c') ptp'
87 | (_, (_, c', ptp')) => complete_solve auto (c @ c') ptp'
88 and all_solve auto c (ptp as (pt, pos as (p,_)): ctree * pos') =
90 val (_, _, mI) = get_obj g_spec pt p
91 val ctxt = get_ctxt pt pos
92 val (_, (_, c', ptp)) = Lucin.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.e_istate, ctxt)) (Istate.e_istate, ctxt) ptp
94 complete_solve auto (c @ c') ptp
97 (* aux.fun for detailrls with Rrls, reverse rewriting *)
98 fun rul_terms_2nds _ nds _ [] = nds
99 | rul_terms_2nds thy nds t ((rule, res as (t', _)) :: rts) =
100 (append_atomic [] (Istate.e_istate, ContextC.e_ctxt) t (Tactic.rule2tac thy [] rule) res Complete EmptyPtree) ::
101 (rul_terms_2nds thy nds t' rts);
103 (* detail steps done internally by Rewrite_Set* into ctree by use of a script *)
104 fun detailrls pt (pos as (p, _)) =
106 val t = get_obj g_form pt p
107 val tac = get_obj g_tac pt p
108 val rls = (assoc_rls o Tactic.rls_of) tac
109 val ctxt = get_ctxt pt pos
112 Rule.Rrls {scr = Rule.Rfuns {init_state, ...}, ...} =>
114 val (_, _, _, rul_terms) = init_state t
115 val newnds = rul_terms_2nds (Proof_Context.theory_of ctxt) [] t rul_terms
116 val pt''' = ins_chn newnds pt p
117 in ("detailrls", pt''', (p @ [length newnds], Res)) end
120 val is = Generate.init_istate tac t
121 (*TODO.WN060602 Pstate (["(t_, Problem (Isac,[equation,univar]))"]
122 is wrong for simpl, but working ?!? *)
123 val tac_ = Tactic.Apply_Method' (Celem.e_metID(*WN0402: see generate1 !?!*), SOME t, is, ctxt)
124 val pos' = ((lev_on o lev_dn) p, Frm)
125 val thy = Celem.assoc_thy "Isac_Knowledge"
126 val (_, _, _, pt') = Generate.generate1 thy tac_ (is, ctxt) pos' pt (* implicit Take *)
127 val (_,_, (pt'', _)) = complete_solve CompleteSubpbl [] (pt', pos')
128 val newnds = children (get_nd pt'' p)
129 val pt''' = ins_chn newnds pt p (*complete_solve cuts branches after*)
130 in ("detailrls", pt''', (p @ [length newnds], Res)) end
133 fun inform (next_cs as (_, _, (pt, pos as (p, _))): Chead.calcstate') istr =
134 case TermC.parse (Celem.assoc_thy "Isac_Knowledge") istr of
135 NONE => ("syntax error in '" ^ istr ^ "'", Chead.e_calcstate' (*TODO: previous cs'*))
138 val f_in = Thm.term_of f_in
139 val pos_pred = lev_back(*'*) pos
140 val f_pred = Ctree.get_curr_formula (pt, pos_pred);
141 val f_succ = Ctree.get_curr_formula (pt, pos);
144 then ("same-formula", next_cs) (* ctree not cut with replaceFormula *)
146 case Inform.cas_input f_in of
147 SOME (pt, _) => ("ok",([], [], (pt, (p, Pos.Met))))
148 | NONE => (*/-------------------------------------- NEW fun locate_input_term------*)
150 val (_, _, metID) = get_obj g_spec pt (par_pblobj pt p)
151 val {scr = prog, ...} = Specify.get_met metID
152 val istate = get_istate pt pos
153 val ctxt = get_ctxt pt pos
155 case Lucin.locate_input_term prog (pt, pos) istate ctxt f_in of
156 Lucin.Found_Step (cstate, _(*istate*), _(*ctxt*)) =>
157 ("ok" , ([], [], cstate (* already contains istate, ctxt *)))
158 | Lucin.Not_Derivable calcstate' =>
160 val pp = Ctree.par_pblobj pt p
161 val (errpats, nrls, prog) = case Specify.get_met (Ctree.get_obj Ctree.g_metID pt pp) of
162 {errpats, nrls, scr = Rule.Prog prog, ...} => (errpats, nrls, prog)
163 | _ => error "inform: uncovered case of get_met"
164 val {env, ...} = Ctree.get_istate pt pos |> Istate.the_pstate
166 case Inform.check_error_patterns (f_pred, f_in) (prog, env) (errpats, nrls) of
167 SOME errpatID => ("error pattern #" ^ errpatID ^ "#", calcstate')
168 | NONE => ("no derivation found", calcstate')