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 : Ctree.pos' list -> Ctree.pos' -> (Calc.T) * Generate.taci list ->
11 Solve.auto -> string * Ctree.pos' list * (Calc.T)
13 val initcontext_met : Ctree.ctree -> Ctree.pos' -> bool * string list * Program.T * Model.itm list * (bool * term) list
14 val initcontext_pbl : Ctree.ctree -> Ctree.pos' -> bool * string list * term * Model.itm list * (bool * term) list
15 val context_met : Celem.metID -> Ctree.ctree -> Ctree.pos -> bool * Celem.metID * Program.T * Model.itm list * (bool * term) list
16 val context_pbl : Celem.pblID -> Ctree.ctree -> Ctree.pos -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
17 val set_method : Celem.metID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
18 val set_problem : Celem.pblID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
19 val set_theory : Rule.thyID -> Calc.T -> Ctree.ctree * Ctree.ocalhd
20 val tryrefine : Celem.pblID -> Ctree.ctree -> Ctree.pos' -> bool * Celem.pblID * term * Model.itm list * (bool * term) list
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 Chead.calcstate (**)
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 | _ => 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 _ => error "set_method: case 2 uncovered"
55 (pt, (complete, Pos.Met, hdf, mits, pre, spec) : Ctree.ocalhd)
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 | _ => 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 _ => error "set_problem: case 2 uncovered"
72 (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd)
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 | _ => 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 _ => error "set_theory: case 2 uncovered"
87 in (pt, (complete, Pos.Pbl, hdf, pits, pre, spec) : Ctree.ocalhd) 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 = Chead.all_modspec (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 (Chead.is_complete_mod (pt, pos))
114 let val ptp = Chead.complete_mod (pt, pos) (*... auto = 2 | 3 *)
116 if Solve.autoord auto < 3 then ("ok", c, ptp)
118 if not (Chead.is_complete_spec ptp)
120 let val ptp = Chead.complete_spec 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 (Chead.is_complete_spec (pt,pos))
129 let val ptp = Chead.complete_spec (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 _ => error "initcontext_pbl: uncovered case"
147 if pI' = Celem.e_pblID
148 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI)
150 val {ppc, where_, prls, ...} = Specify.get_pbt pblID
151 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "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 _ => error "initcontext_met: uncovered case"
162 val metID = if mI' = Celem.e_metID
163 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI)
165 val {ppc, pre, prls, scr, ...} = Specify.get_met metID
166 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "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 pblID *)
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 _ => error "context_pbl: uncovered case"
178 val {ppc,where_,prls,...} = Specify.get_pbt pI
179 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "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 _ => error "context_met: uncovered case"
190 val {ppc,pre,prls,scr,...} = Specify.get_met mI
191 val (model_ok, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "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 _ => error "context_met: uncovered case"
203 case Specify.refine_pbl (Celem.assoc_thy "Isac_Knowledge") pI probl of
204 NONE => (*copy from context_pbl*)
206 val {ppc,where_,prls,...} = Specify.get_pbt pI
207 val (_, (pbl, pre)) = Specify.match_itms_oris (Celem.assoc_thy "Isac_Knowledge") probl (ppc,where_,prls) os
209 (false, pI, hdl, pbl, pre)
211 | SOME (pI, (pbl, pre)) => (true, pI, hdl, pbl, pre)