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
21 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
23 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
25 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
32 structure Math_Engine(**): MATH_ENGINE(**) =
38 | Nexts of Calc.T * State_Steps.T (**)
40 (* specify a new method; WN0512 impl.incomplete, see 'nxt_specif (Specify_Method ' *)
41 fun set_method mI ptp =
44 case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of
45 (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p)
46 | _ => raise ERROR "set_method: case 1 uncovered"
47 val pre = [] (*...from Specify_Method'*)
48 val complete = true (*...from Specify_Method'*)
49 (*from Specify_Method' ? vvv, vvv ?*)
51 case Ctree.get_obj I pt p of
52 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
53 | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered"
55 (pt, (complete, Pos.Met, hdf, mits, pre, spec) : SpecificationC.T)
58 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *)
59 fun set_problem pI ptp =
61 val (complete, pits, pre, pt, p) =
62 case Step_Specify.by_tactic_input (Tactic.Specify_Problem pI) ptp of
63 (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))
64 => (complete, pits, pre, pt, p)
65 | _ => raise ERROR "set_problem: case 1 uncovered"
66 (*from Specify_Problem' ? vvv, vvv ?*)
68 case Ctree.get_obj I pt p of
69 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
70 | Ctree.PrfObj _ => raise ERROR "set_problem: case 2 uncovered"
72 (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T)
75 fun set_theory tI ptp =
77 val (complete, pits, pre, pt, p) =
78 case Step_Specify.by_tactic_input (Tactic.Specify_Theory tI) ptp of
79 (_, ([(_, Tactic.Specify_Problem' (_, (complete, (pits, pre))), _)], _, (pt, (p, _))))
80 => (complete, pits, pre, pt, p)
81 | _ => raise ERROR "set_theory: case 1 uncovered"
82 (*from Specify_Theory' ? vvv, vvv ?*)
84 case Ctree.get_obj I pt p of
85 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec)
86 | Ctree.PrfObj _ => raise ERROR "set_theory: case 2 uncovered"
87 in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : SpecificationC.T) end;
89 (* does several steps within one calculation as given by "type auto";
90 the steps may arbitrarily go into and leave different phases,
91 i.e. specify-phase and solve-phase *)
92 fun autocalc c ip cs (Solve.Steps s) =
95 let val (str, (_, c', ptp)) = Step.do_next ip cs; (* autoord = 1, probably does 1 do_next too much*)
96 in (str, c@c', ptp) end
98 let val (str, (_, c', ptp as (_, p))) = Step.do_next ip cs;
101 then autocalc (c@c') p (ptp, []) (Solve.Steps (s - 1))
102 else (str, c@c', ptp) end
103 (* handles autoord <= 3, autoord > 3 handled by all_solve, complete_solve *)
104 | autocalc c (pos as (_, p_)) ((pt, _), _(*tacis could help 1x in solve*)) auto =
105 if Solve.autoord auto > 3 andalso Ctree.just_created (pt, pos)
107 let val ptp = Specify.do_all (pt, pos);
108 in Solve.all_solve auto c ptp end (*... auto = 4 | 5 | 6 *)
110 if member op = [Pos.Pbl, Pos.Met] p_
112 if not (SpecificationC.is_complete (pt, pos))
114 let val ptp = Specify.finish_phase (pt, pos) (*... auto = 2 | 3 *)
116 if Solve.autoord auto < 3 then ("ok", c, ptp)
118 if not (References.are_complete ptp)
120 let val ptp = References.complete ptp
122 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
124 else if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
127 if not (References.are_complete (pt,pos))
129 let val ptp = References.complete (pt, pos)
131 if Solve.autoord auto = 3 then ("ok", c, ptp) else Solve.all_solve auto c ptp
134 if Solve.autoord auto = 3 then ("ok", c, (pt, pos)) else Solve.all_solve auto c (pt, pos)
135 else Solve.complete_solve auto c (pt, pos);
137 (*.initialiye matching; before 'tryMatch' get the pblID to match with:
138 if no pbl has been specified, take the init from origin.*)
139 fun initcontext_pbl pt (p, _) =
141 val (probl, os, pI, hdl, pI') =
142 case Ctree.get_obj I pt p of
143 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec=(_, pI', _), ...}
144 => (probl, os, pI, hdl, pI')
145 | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case"
147 if pI' = Problem.id_empty
148 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
150 val {ppc, where_, prls, ...} = Problem.from_store pblID
151 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc, where_, prls) os
153 (model_ok, pblID, hdl, pbl, pre)
156 fun initcontext_met pt (p,_) =
158 val (meth, os, mI, mI') =
159 case Ctree.get_obj I pt p of
160 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ...} => (meth, os, mI, mI')
161 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case"
162 val metID = if mI' = MethodC.id_empty
163 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
165 val {ppc, pre, prls, scr, ...} = MethodC.from_store metID
166 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
168 (model_ok, metID, scr, pbl, pre)
171 (* match the model of a problem at pos p with the model-pattern of the problem with pI *)
172 fun context_pbl pI pt p =
174 val (probl, os, hdl) =
175 case Ctree.get_obj I pt p of
176 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
177 | Ctree.PrfObj _ => raise ERROR "context_pbl: uncovered case"
178 val {ppc, where_, prls, ...} = Problem.from_store pI
179 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
181 (model_ok, pI, hdl, pbl, pre)
184 fun context_met mI pt p =
187 case Ctree.get_obj I pt p of
188 Ctree.PblObj {meth, origin = (os, _, _),...} => (meth, os)
189 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
190 val {ppc,pre,prls,scr,...} = MethodC.from_store mI
191 val (model_ok, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") meth (ppc,pre,prls) os
193 (model_ok, mI, scr, pbl, pre)
196 fun tryrefine pI pt (p,_) =
198 val (probl, os, hdl) =
199 case Ctree.get_obj I pt p of
200 Ctree.PblObj {probl, origin = (os, _, hdl), ...} => (probl, os, hdl)
201 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case"
203 case Refine.problem (ThyC.get_theory "Isac_Knowledge") pI probl of
204 NONE => (*copy from context_pbl*)
206 val {ppc,where_,prls,...} = Problem.from_store pI
207 val (_, (pbl, pre)) = M_Match.match_itms_oris (ThyC.get_theory "Isac_Knowledge") probl (ppc,where_,prls) os
209 (false, pI, hdl, pbl, pre)
211 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)