43 |
43 |
44 val ("ok", ([], [], _)) = |
44 val ("ok", ([], [], _)) = |
45 Specify.by_tactic' "#Given" ct (pt, p); |
45 Specify.by_tactic' "#Given" ct (pt, p); |
46 "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) = |
46 "~~~~~ fun specify_additem , args:"; val (sel, ct, (pt, pos as (p,_(*Frm, Pbl*)))) = |
47 ("#Given", ct, (pt, p)); |
47 ("#Given", ct, (pt, p)); |
48 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = get (pt, pos) |
48 val (met, oris, (dI', pI', mI'), pbl, (dI, pI, mI), ctxt) = Specification.get_data (pt, pos) |
49 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI |
49 val thy = if dI = ThyC.id_empty then ThyC.get_theory dI' else ThyC.get_theory dI |
50 val cpI = if pI = Problem.id_empty then pI' else pI |
50 val cpI = if pI = Problem.id_empty then pI' else pI |
51 val cmI = if mI = Method.id_empty then mI' else mI |
51 val cmI = if mI = Method.id_empty then mI' else mI |
52 val {ppc, where_, prls, ...} = Problem.from_store cpI; |
52 val {ppc, where_, prls, ...} = Problem.from_store cpI; |
53 |
53 |
99 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])),\n" ^ |
99 "(1 ,[1] ,true ,#Given ,Cor Traegerlaenge L ,(l_l, [L])),\n" ^ |
100 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0]))]" |
100 "(2 ,[1] ,true ,#Given ,Cor Streckenlast q_0 ,(q_q, [q_0]))]" |
101 (*+*)then () else error "FINAL I_Model CHANGED"; |
101 (*+*)then () else error "FINAL I_Model CHANGED"; |
102 |
102 |
103 val (p, pt') = |
103 val (p, pt') = |
104 case Specify_Step.add (make sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of |
104 case Specify_Step.add (I_Model.get_tac sel (ct, pbl')) (Istate.Uistate, ctxt) (pt, (p, Pos.Pbl)) of |
105 ((p, Pbl), _, _, pt') => (p, pt') |
105 ((p, Pbl), _, _, pt') => (p, pt') |
106 val pre = Pre_Conds.check' thy prls where_ pbl' |
106 val pre = Pre_Conds.check' thy prls where_ pbl' |
107 val pb = foldl and_ (true, map fst pre) |
107 val pb = foldl and_ (true, map fst pre) |
108 val (p_, _) = |
108 val (p_, _) = |
109 Specify.find_next_step' Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI); |
109 Specify.find_next_step' Pos.Pbl pb oris (dI',pI',mI') (pbl',met) (ppc, (#ppc o Method.from_store) cmI) (dI, pI, mI); |