13 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T_POS * Pre_Conds.T |
13 val initcontext_met : Ctree.ctree -> Pos.pos' -> bool * string list * Program.T * I_Model.T_POS * Pre_Conds.T |
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T_POS * Pre_Conds.T |
14 val initcontext_pbl : Ctree.ctree -> Pos.pos' -> bool * string list * term * I_Model.T_POS * Pre_Conds.T |
15 val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
15 val set_method : MethodC.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
16 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
16 val set_problem : Problem.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
17 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
17 val set_theory : ThyC.id -> Calc.T -> Ctree.ctree * SpecificationC.T |
18 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T * Pre_Conds.T |
18 val tryrefine : Problem.id -> Ctree.ctree -> Pos.pos' -> bool * Problem.id * term * I_Model.T_POS * Pre_Conds.T |
19 end |
19 end |
20 |
20 |
21 (**) |
21 (**) |
22 structure Math_Engine(**): MATH_ENGINE(**) = |
22 structure Math_Engine(**): MATH_ENGINE(**) = |
23 struct |
23 struct |
172 |> References.select_input ospec |
172 |> References.select_input ospec |
173 |> #1 |
173 |> #1 |
174 |> Know_Store.get_via_last_thy |
174 |> Know_Store.get_via_last_thy |
175 |> Proof_Context.init_global |
175 |> Proof_Context.init_global |
176 in |
176 in |
177 case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (probl) of |
177 case Refine.problem (Know_Store.get_via_last_thy "Isac_Knowledge") pI (I_Model.OLD_to_POS probl) of |
178 NONE => (*copy from context_pbl*) |
178 NONE => (*copy from context_pbl*) |
179 let |
179 let |
180 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI |
180 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI |
181 val (_, (pbl, where_)) = M_Match.by_i_models ctxt os |
181 val (_, (pbl, where_)) = M_Match.by_i_models ctxt os |
182 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls) |
182 (I_Model.OLD_to_POS probl, I_Model.OLD_to_POS meth) (model, where_, where_rls) |
183 in |
183 in |
184 (false, pI, hdl, I_Model.TEST_to_OLD pbl, where_) |
184 (false, pI, hdl, pbl, where_) |
185 end |
185 end |
186 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_) |
186 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_) |
187 end |
187 end |
188 |
188 |
189 (**)end(**) |
189 (**)end(**) |