56 val {srls, pre, prls, ...} = get_met mI; |
56 val {srls, pre, prls, ...} = get_met mI; |
57 val pres = check_preconds thy prls pre meth |> map snd; |
57 val pres = check_preconds thy prls pre meth |> map snd; |
58 val ctxt = ctxt |> ContextC.insert_assumptions pres; |
58 val ctxt = ctxt |> ContextC.insert_assumptions pres; |
59 val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI; |
59 val (is'''' as Pstate {env = env'''',...}, _, sc'''') = init_pstate srls ctxt meth mI; |
60 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI) |
60 "~~~~~ fun init_pstate , args:"; val (srls, thy, itms, metID) = (srls, thy, meth, mI) |
61 val actuals = itms2args thy metID itms |
61 val actuals = arguments_from_model metID itms |
62 val scr as Prog sc = (#scr o get_met) metID |
62 val scr as Prog sc = (#scr o get_met) metID |
63 val formals = formal_args sc |
63 val formals = formal_args sc |
64 (*expects same sequence of (actual) args in itms and (formal) args in met*) |
64 (*expects same sequence of (actual) args in itms and (formal) args in met*) |
65 fun msg_miss sc metID caller f formals actuals = |
65 fun msg_miss sc metID caller f formals actuals = |
66 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^ |
66 "ERROR in creating the environment from formal args. of partial_function \"" ^ fst (Program.get_fun_id sc) ^ "\"\n" ^ |
96 val {pre, prls, ...} = Specify.get_met metID; |
96 val {pre, prls, ...} = Specify.get_met metID; |
97 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd; |
97 val pres = Stool.check_preconds (Proof_Context.theory_of ctxt) prls pre itms |> map snd; |
98 val ctxt = ctxt |> ContextC.insert_assumptions pres; |
98 val ctxt = ctxt |> ContextC.insert_assumptions pres; |
99 |
99 |
100 "~~~~~ continue Step_Solve.by_tactic"; |
100 "~~~~~ continue Step_Solve.by_tactic"; |
101 val ini = implicit_take thy sc'''' env''''; |
101 val ini = implicit_take sc'''' env''''; |
102 val p = lev_dn p; |
102 val p = lev_dn p; |
103 val SOME t = ini; |
103 val SOME t = ini; |
104 val (pos,c,_,pt) = |
104 val (pos,c,_,pt) = |
105 generate1 (Apply_Method' (mI, SOME t, is'''', ctxt)) |
105 generate1 (Apply_Method' (mI, SOME t, is'''', ctxt)) |
106 (is'''', ctxt) (pt, (lev_on p, Frm))(*implicit Take*); |
106 (is'''', ctxt) (pt, (lev_on p, Frm))(*implicit Take*); |