1 (* MathEngine/mathengine-stateless.sml
2 The _functional_ mathematics engine, ie. without a state.
3 Input and output are Isabelle's formulae as strings.
4 authors: Walther Neuper 2000
5 (c) due to copyright terms
8 signature MATH_ENGINE =
10 val autocalc : Pos.pos' list -> Pos.pos' -> Calc.T * State_Steps.T ->
11 Solve.auto -> string * Pos.pos' list * Calc.T
13 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T * Pre_Conds.T
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T * Pre_Conds.T
15 val context_met : MethodC.id -> Ctree.ctree -> Pos.pos -> bool * MethodC.id * Program.T * I_Model.T * Pre_Conds.T
16 val context_pbl : Problem.id -> Ctree.ctree -> Pos.pos -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
17 val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
18 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T
19 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T
20 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T
24 structure Math_Engine(**): MATH_ENGINE(**) =
30 | Nexts of Calc.T * State_Steps.T (**)
32 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
33 fun set_method mI ptp =
36 case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of
37 (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p)
38 | _ => raise ERROR "set_method: case 1 uncovered"
39 val pre = [] (*...from Specify_Method'*)
40 val complete = true (*...from Specify_Method'*)
41 (*from Specify_Method' ? vvv, vvv ?*)
43 case Ctree.get_obj I pt p of
44 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
45 | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"
47 (pt, (complete, Pos.Met, hdf, mits, pre, spec) : SpecificationC.T)
50 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
51 fun set_problem pI ptp =
53 val (complete, pits, pre, pt, p) =
54 case Step_Specify.by_tactic_input (Tactic.Specify_Problem pI) ptp of
55 (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))
56 => (complete, pits, pre, pt, p)
57 | _ => raise ERROR "set_problem: case 1 uncovered"
58 (*from Specify_Problem' ? vvv, vvv ?*)
60 case Ctree.get_obj I pt p of
61 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
62 | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"
64 (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T)
67 fun set_theory tI ptp =
69 val (complete, pits, pre, pt, p) =
70 case Step_Specify.by_tactic_input (Tactic.Specify_Theory tI) ptp of
71 (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))
72 => (complete, pits, pre, pt, p)
73 | _ => raise ERROR "set_theory: case 1 uncovered"
74 (*from Specify_Theory' ? vvv, vvv ?*)
76 case Ctree.get_obj I pt p of
77 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
78 | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"
79 in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T) end;
81 (* does several steps within one calculation as given by "type auto";
82 the steps may arbitrarily go into and leave different phases,
83 i.e. specify-phase and solve-phase *)
84 fun autocalc c ip cs (Solve.Steps s) =
87 let val (str, (_, c', ptp)) = Step.do_next ip cs; (* autoord = 1, probably does 1 do_next too much*)
88 in (str, c@c', ptp) end
90 let val (str, (_, c', ptp as (_, p))) = Step.do_next ip cs;
93 then autocalc (c@c') p (ptp, []) (Solve.Steps (s - 1))
94 else (str, c@c', ptp) end
95 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
96 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
97 if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
100 val ptp = Specify.do_all (pt, pos);
101 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
103 if member op = [Pos.Pbl, Pos.Met] p_
105 if not (SpecificationC.is_complete (pt, pos))
107 let val ptp = Specify.finish_phase (pt, pos) (*... auto = 2 | 3 *)
109 if Solve.autoord auto < 3 then ("ok", c, ptp)
111 if not (References.are_complete ptp)
113 let val ptp = References.complete ptp
115 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
117 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
120 if not (References.are_complete (pt,pos))
122 let val ptp = References.complete (pt, pos)
124 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
127 if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
128 else Solve.complete_solve auto c (pt, pos);
130 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
131 if no pbl has been specified, take the init from origin.*)
132 fun initcontext_pbl pt (p, _) =
134 val (probl, os, pI, hdl, pI', ctxt) =
135 case Ctree.get_obj I pt p of
136 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec = (_, pI', _), ctxt, ...}
137 => (probl, os, pI, hdl, pI', ctxt)
138 | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case"
140 if pI' = Problem.id_empty
141 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
143 val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID
144 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge")
145 probl (model, where_, where_rls) os
147 (model_ok, pblID, hdl, pbl, pre)
150 fun initcontext_met pt (p,_) =
152 val (meth, os, mI, mI', ctxt) =
153 case Ctree.get_obj I pt p of
154 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} =>
155 (meth, os, mI, mI', ctxt)
156 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"
157 val metID = if mI' = MethodC.id_empty
158 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
160 val {ppc, pre, prls, scr, ...} = MethodC.from_store ctxt metID
161 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
163 (model_ok, metID, scr, pbl, pre)
166 (* match the model of a problem at pos p with the model-pattern of the problem with pI *)
167 fun context_pbl pI pt p =
169 val (probl, os, ospec, hdl, spec) =
170 case Ctree.get_obj I pt p of
171 Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
172 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
173 val ctxt = spec |> References.select_input ospec |> #1 |> ThyC.get_theory |> Proof_Context.init_global
174 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
175 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl
176 (model, where_, where_rls) os
178 (model_ok, pI, hdl, pbl, pre)
181 fun context_met mI pt p =
183 val (meth, os, ctxt) =
184 case Ctree.get_obj I pt p of
185 Ctree.PblObj {meth, origin = (os, _, _), ctxt, ...} => (meth, os, ctxt)
186 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
187 val {ppc,pre,prls,scr,...} = MethodC.from_store ctxt mI
188 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
190 (model_ok, mI, scr, pbl, pre)
193 fun tryrefine pI pt (p,_) =
195 val (probl, os, ospec, hdl, spec) =
196 case Ctree.get_obj I pt p of
197 Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec)
198 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
199 val ctxt = spec |> References.select_input ospec |> #1 |> ThyC.get_theory |> Proof_Context.init_global
201 case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
202 NONE => (*copy from context_pbl*)
204 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI
205 val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl
206 (model, where_, where_rls) os
208 (false, pI, hdl, pbl, pre)
210 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)