31 fun set_method mI ptp = |
31 fun set_method mI ptp = |
32 let |
32 let |
33 val (mits, pt, p) = |
33 val (mits, pt, p) = |
34 case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of |
34 case Step_Specify.by_tactic_input (Tactic.Specify_Method mI) ptp of |
35 (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p) |
35 (_, ([(_, Tactic.Specify_Method' (_, _, mits), _)], [], (pt, (p, _)))) => (mits, pt, p) |
36 | _ => raise ERROR "set_method: case 1 uncovered" |
36 | _ => raise ERROR "Math_Engine.set_method: case 1 uncovered" |
37 val where_ = [] (*...from Specify_Method'*) |
37 val where_ = [] (*...from Specify_Method'*) |
38 val complete = true (*...from Specify_Method'*) |
38 val complete = true (*...from Specify_Method'*) |
39 (*from Specify_Method' ? vvv, vvv ?*) |
39 (*from Specify_Method' ? vvv, vvv ?*) |
40 val (hdf, spec) = |
40 val (hdf, spec) = |
41 case Ctree.get_obj I pt p of |
41 case Ctree.get_obj I pt p of |
42 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) |
42 Ctree.PblObj {origin = (_, _, hdf), spec, ...} => (hdf, spec) |
43 | Ctree.PrfObj _ => raise ERROR "set_method: case 2 uncovered" |
43 | Ctree.PrfObj _ => raise ERROR "Math_Engine.set_method: case 2 uncovered" |
44 in |
44 in |
45 (pt, (complete, Pos.Met, hdf, mits, where_, spec) : SpecificationC.T) |
45 (pt, (complete, Pos.Met, hdf, mits, where_, spec) : SpecificationC.T) |
46 end |
46 end |
47 |
47 |
48 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *) |
48 (* specify a new problem; WN0512 impl.incomplete, see 'nxt_specif (Specify_Problem ' *) |
127 |
127 |
128 (*.initialiye matching; before 'tryMatch' get the pblID to match with: |
128 (*.initialiye matching; before 'tryMatch' get the pblID to match with: |
129 if no pbl has been specified, take the init from origin.*) |
129 if no pbl has been specified, take the init from origin.*) |
130 fun initcontext_pbl pt (p, _) = |
130 fun initcontext_pbl pt (p, _) = |
131 let |
131 let |
132 val (probl, os, pI, hdl, pI', ctxt) = |
132 val (probl, meth, os, pI, hdl, pI', ctxt) = |
133 case Ctree.get_obj I pt p of |
133 case Ctree.get_obj I pt p of |
134 Ctree.PblObj {probl, origin = (os, (_, pI, _), hdl), spec = (_, pI', _), ctxt, ...} |
134 Ctree.PblObj {probl, meth, origin = (os, (_, pI, _), hdl), spec = (_, pI', _), ctxt, ...} |
135 => (probl, os, pI, hdl, pI', ctxt) |
135 => (probl, meth, os, pI, hdl, pI', ctxt) |
136 | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case" |
136 | Ctree.PrfObj _ => raise ERROR "initcontext_pbl: uncovered case" |
137 val pblID = |
137 val pblID = |
138 if pI' = Problem.id_empty |
138 if pI' = Problem.id_empty |
139 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) |
139 then (* TODO.WN051125 (#init o get_pbt) pI *) takelast (2, pI) |
140 else pI' |
140 else pI' |
141 val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID |
141 val {model, where_, where_rls, ...} = Problem.from_store ctxt pblID |
142 val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt |
142 val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt os |
143 probl (model, where_, where_rls) os |
143 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls) |
144 in |
144 in |
145 (model_ok, pblID, hdl, pbl, where_) |
145 (model_ok, pblID, hdl, pbl, where_) |
146 end |
146 end |
147 |
147 |
148 fun initcontext_met pt (p,_) = |
148 fun initcontext_met pt (p,_) = |
149 let |
149 let |
150 val (meth, os, mI, mI', ctxt) = |
150 val (probl, meth, os, mI, mI', ctxt) = |
151 case Ctree.get_obj I pt p of |
151 case Ctree.get_obj I pt p of |
152 Ctree.PblObj {meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} => |
152 Ctree.PblObj {probl, meth, origin = (os, (_, _, mI), _), spec=(_, _, mI'), ctxt, ...} => |
153 (meth, os, mI, mI', ctxt) |
153 (probl, meth, os, mI, mI', ctxt) |
154 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case" |
154 | Ctree.PrfObj _ => raise ERROR "initcontext_met: uncovered case" |
155 val metID = if mI' = MethodC.id_empty |
155 val metID = if mI' = MethodC.id_empty |
156 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) |
156 then (*TODO.WN051125 (#init o get_pbt) pI *) takelast (2, mI) |
157 else mI' |
157 else mI' |
158 val {model, where_, where_rls, program, ...} = MethodC.from_store ctxt metID |
158 val {model, where_, where_rls, program, ...} = MethodC.from_store ctxt metID |
159 val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt meth (model,where_,where_rls) os |
159 val (model_ok, (pbl, where_)) = M_Match.match_itms_oris ctxt os |
|
160 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls) |
160 in |
161 in |
161 (model_ok, metID, program, pbl, where_) |
162 (model_ok, metID, program, pbl, where_) |
162 end |
163 end |
163 |
164 |
164 fun tryrefine pI pt (p,_) = |
165 fun tryrefine pI pt (p,_) = |
165 let |
166 let |
166 val (probl, os, ospec, hdl, spec) = |
167 val (probl, meth, os, ospec, hdl, spec) = |
167 case Ctree.get_obj I pt p of |
168 case Ctree.get_obj I pt p of |
168 Ctree.PblObj {probl, origin = (os, ospec, hdl), spec, ...} => (probl, os, ospec, hdl, spec) |
169 Ctree.PblObj {probl, meth, origin = (os, ospec, hdl), spec, ...} => (probl, meth, os, ospec, hdl, spec) |
169 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case" |
170 | Ctree.PrfObj _ => raise ERROR "context_met: uncovered case" |
170 val ctxt = spec |
171 val ctxt = spec |
171 |> References.select_input ospec |
172 |> References.select_input ospec |
172 |> #1 |
173 |> #1 |
173 |> Know_Store.get_via_last_thy |
174 |> Know_Store.get_via_last_thy |
174 |> Proof_Context.init_global |
175 |> Proof_Context.init_global |
175 in |
176 in |
176 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 (probl) of |
177 NONE => (*copy from context_pbl*) |
178 NONE => (*copy from context_pbl*) |
178 let |
179 let |
179 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI |
180 val {model, where_, where_rls, ...} = Problem.from_store ctxt pI |
180 val (_, (pbl, where_)) = M_Match.match_itms_oris ctxt probl |
181 val (_, (pbl, where_)) = M_Match.match_itms_oris ctxt os |
181 (model, where_, where_rls) os |
182 (I_Model.OLD_to_TEST probl, I_Model.OLD_to_TEST meth) (model, where_, where_rls) |
182 in |
183 in |
183 (false, pI, hdl, pbl, where_) |
184 (false, pI, hdl, I_Model.TEST_to_OLD pbl, where_) |
184 end |
185 end |
185 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_) |
186 | SOME (pI, (pbl, where_)) => (true, pI, hdl, pbl, where_) |
186 end |
187 end |
187 |
188 |
188 (**)end(**) |
189 (**)end(**) |