84 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post |
84 val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> Calc.state_post |
85 (*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*) |
85 (*val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post*) |
86 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
86 val specify_additem: string -> TermC.as_string -> Calc.T -> string * Calc.state_post |
87 ( *\------- to Specify from Specification -------/*) |
87 ( *\------- to Specify from Specification -------/*) |
88 |
88 |
89 (*/------- to P_Model from Specification -------\*) |
|
90 val ppc2list: 'a P_Model.ppc -> 'a list |
|
91 val mk_delete: theory -> string -> I_Model.feedback -> Tactic.input |
|
92 val mk_additem: string -> TermC.as_string -> Tactic.input |
|
93 (*\------- to P_Model from Specification -------/*) |
|
94 |
|
95 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
89 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *) |
96 (*NONE*) |
90 (*NONE*) |
97 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
91 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* ) |
98 val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context |
92 val get: Calc.T -> I_Model.T * O_Model.T * References.T * I_Model.T * References.T * Proof.context |
99 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T |
93 val make: I_Model.m_field -> TermC.as_string * I_Model.T -> Tactic.T |
123 (* is the calchead complete ? *) |
117 (* is the calchead complete ? *) |
124 fun ocalhd_complete its pre (dI, pI, mI) = |
118 fun ocalhd_complete its pre (dI, pI, mI) = |
125 foldl and_ (true, map #3 (its: I_Model.T)) andalso |
119 foldl and_ (true, map #3 (its: I_Model.T)) andalso |
126 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso |
120 foldl and_ (true, map #1 (pre: Pre_Conds.T)) andalso |
127 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty |
121 dI <> ThyC.id_empty andalso pI <> Problem.id_empty andalso mI <> Method.id_empty |
128 |
|
129 fun ppc2list {Given = gis, Where = whs, Find = fis, With = wis, Relate = res} = |
|
130 gis @ whs @ fis @ wis @ res |
|
131 |
122 |
132 (* get the number of variants in a problem in 'original', |
123 (* get the number of variants in a problem in 'original', |
133 assumes equal descriptions in immediate sequence *) |
124 assumes equal descriptions in immediate sequence *) |
134 fun variants_in ts = |
125 fun variants_in ts = |
135 let |
126 let |
223 case find_first (test_subset (hd icl)) vors of |
214 case find_first (test_subset (hd icl)) vors of |
224 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt" |
215 NONE => raise ERROR "nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt" |
225 | SOME ori => SOME (geti_ct thy ori (hd icl)) |
216 | SOME ori => SOME (geti_ct thy ori (hd icl)) |
226 end |
217 end |
227 |
218 |
228 fun mk_delete thy "#Given" itm_ = Tactic.Del_Given (I_Model.to_p_model thy itm_) |
|
229 | mk_delete thy "#Find" itm_ = Tactic.Del_Find (I_Model.to_p_model thy itm_) |
|
230 | mk_delete thy "#Relate" itm_ = Tactic.Del_Relation (I_Model.to_p_model thy itm_) |
|
231 | mk_delete _ str _ = raise ERROR ("mk_delete: called with field \"" ^ str ^ "\"") |
|
232 fun mk_additem "#Given" ct = Tactic.Add_Given ct |
|
233 | mk_additem "#Find" ct = Tactic.Add_Find ct |
|
234 | mk_additem "#Relate"ct = Tactic.Add_Relation ct |
|
235 | mk_additem str _ = raise ERROR ("mk_additem: called with field \"" ^ str ^ "\"") |
|
236 |
|
237 (*/------- to Specify from Specification -------\*) |
219 (*/------- to Specify from Specification -------\*) |
238 (* |
220 (* |
239 TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met |
221 TODO: unify with Specify.find_next_step ! ! ! USED ONLY to determine Pos.Pbl .. Pos.Met |
240 |
222 |
241 determine the next step of specification; |
223 determine the next step of specification; |
254 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI') |
236 (if dI' = ThyC.id_empty andalso dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI') |
255 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI') |
237 else if pI' = Problem.id_empty andalso pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI') |
256 else |
238 else |
257 case find_first (I_Model.is_error o #5) pbl of |
239 case find_first (I_Model.is_error o #5) pbl of |
258 SOME (_, _, _, fd, itm_) => |
240 SOME (_, _, _, fd, itm_) => |
259 (Pos.Pbl, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_) |
241 (Pos.Pbl, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_) |
260 | NONE => |
242 | NONE => |
261 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of |
243 (case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris pbt pbl of |
262 SOME (fd, ct') => (Pos.Pbl, mk_additem fd ct') |
244 SOME (fd, ct') => (Pos.Pbl, P_Model.mk_additem fd ct') |
263 | NONE => (*pbl-items complete*) |
245 | NONE => (*pbl-items complete*) |
264 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI') |
246 if not preok then (Pos.Pbl, Tactic.Refine_Problem pI') |
265 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI') |
247 else if dI = ThyC.id_empty then (Pos.Pbl, Tactic.Specify_Theory dI') |
266 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI') |
248 else if pI = Problem.id_empty then (Pos.Pbl, Tactic.Specify_Problem pI') |
267 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI') |
249 else if mI = Method.id_empty then (Pos.Pbl, Tactic.Specify_Method mI') |
268 else |
250 else |
269 case find_first (I_Model.is_error o #5) met of |
251 case find_first (I_Model.is_error o #5) met of |
270 SOME (_, _, _, fd, itm_) => (Pos.Met, mk_delete (ThyC.get_theory dI) fd itm_) |
252 SOME (_, _, _, fd, itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory dI) fd itm_) |
271 | NONE => |
253 | NONE => |
272 (case nxt_add (ThyC.get_theory dI) oris mpc met of |
254 (case nxt_add (ThyC.get_theory dI) oris mpc met of |
273 SOME (fd, ct') => (Pos.Met, mk_additem fd ct') (*30.8.01: pre?!?*) |
255 SOME (fd, ct') => (Pos.Met, P_Model.mk_additem fd ct') (*30.8.01: pre?!?*) |
274 | NONE => (Pos.Met, Tactic.Apply_Method mI)))) |
256 | NONE => (Pos.Met, Tactic.Apply_Method mI)))) |
275 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = |
257 | nxt_spec Pos.Met preok oris (dI', pI', _) (_, met) (_ ,mpc) (dI, pI, mI) = |
276 (case find_first (I_Model.is_error o #5) met of |
258 (case find_first (I_Model.is_error o #5) met of |
277 SOME (_,_,_,fd,itm_) => (Pos.Met, mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_) |
259 SOME (_,_,_,fd,itm_) => (Pos.Met, P_Model.mk_delete (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) fd itm_) |
278 | NONE => |
260 | NONE => |
279 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of |
261 case nxt_add (ThyC.get_theory (if dI = ThyC.id_empty then dI' else dI)) oris mpc met of |
280 SOME (fd,ct') => (Pos.Met, mk_additem fd ct') |
262 SOME (fd,ct') => (Pos.Met, P_Model.mk_additem fd ct') |
281 | NONE => |
263 | NONE => |
282 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI') |
264 (if dI = ThyC.id_empty then (Pos.Met, Tactic.Specify_Theory dI') |
283 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI') |
265 else if pI = Problem.id_empty then (Pos.Met, Tactic.Specify_Problem pI') |
284 else if not preok then (Pos.Met, Tactic.Specify_Method mI) |
266 else if not preok then (Pos.Met, Tactic.Specify_Method mI) |
285 else (Pos.Met, Tactic.Apply_Method mI))) |
267 else (Pos.Met, Tactic.Apply_Method mI))) |