1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Sun Oct 09 09:01:29 2022 +0200
1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Wed Oct 19 10:43:04 2022 +0200
1.3 @@ -24,13 +24,103 @@
1.4 CalcTreeTEST
1.5 [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],
1.6 ("Integrate", ["integrate", "function"], ["diff", "integration"]))];
1.7 -val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
1.8 +val (p,_,f,nxt,_,pt) = me nxt p c pt; (*\<rightarrow> Add_Given "functionTerm (x \<up> 2 + 1)"*)
1.9 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.10 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.11 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.12 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.13 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.14 -val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.15 +
1.16 +val (p''',_,f,nxt''',_,pt''') = me nxt p c pt; (*nxt'''= Specify_Method ["diff", "integration"]*)
1.17 +(*/------------------- step into me Specify_Method ["diff", "integration"] -----------------\*)
1.18 +"~~~~~ fun me , args:"; val (tac, p, _, pt) = (nxt''', p''', c, pt''');
1.19 + val (pt, p) =
1.20 + (*Step.by_tactic is here for testing by me; do_next would suffice in me*)
1.21 + case Step.by_tactic tac (pt, p) of
1.22 + ("ok", (_, _, ptp)) => ptp
1.23 +
1.24 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) = (*case*)
1.25 + Step.do_next p ((pt, Pos.e_pos'), []) (*of*);
1.26 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
1.27 + = (p, ((pt, Pos.e_pos'), []));
1.28 + (*if*) Pos.on_calc_end ip (*else*);
1.29 + val (_, probl_id, _) = Calc.references (pt, p);
1.30 +val _ =
1.31 + (*case*) tacis (*of*);
1.32 + (*if*) probl_id = Problem.id_empty (*else*);
1.33 +
1.34 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
1.35 + Step.switch_specify_solve p_ (pt, ip);
1.36 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
1.37 + (*if*) Pos.on_specification ([], state_pos) (*then*);
1.38 +
1.39 + Step.specify_do_next (pt, input_pos);
1.40 +"~~~~~ fun specify_do_next , args:"; val (ptp as (pt, (p, p_))) = (pt, input_pos);
1.41 + val (_, (p_', tac)) = Specify.find_next_step ptp
1.42 + val ist_ctxt = Ctree.get_loc pt (p, p_)
1.43 +val Tactic.Apply_Method mI =
1.44 + (*case*) tac (*of*);
1.45 +
1.46 +val ("ok", ([(Apply_Method ["diff", "integration"], _, _)], _, _)) =
1.47 + LI.by_tactic (Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty))
1.48 + ist_ctxt (pt, (p, p_'));
1.49 +"~~~~~ fun by_tactic , args:"; val ((Tactic.Apply_Method' (mI, _, _, _)), (_, ctxt), (pt, pos as (p, _)))
1.50 + = ((Tactic.Apply_Method' (mI, NONE, Istate.empty, ContextC.empty)),
1.51 + ist_ctxt, (pt, (p, p_')));
1.52 + val (itms, oris, probl) = case get_obj I pt p of (*STILL asms=[]*)
1.53 + PblObj {meth = itms, origin = (oris, _, _), probl, ...} => (itms, oris, probl)
1.54 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case get_obj"
1.55 + val {ppc, ...} = MethodC.from_store ctxt mI;
1.56 + val itms = if itms <> [] then itms else I_Model.complete oris probl [] ppc
1.57 + val srls = LItool.get_simplifier (pt, pos)
1.58 + val (is, env, ctxt, prog) = case LItool.init_pstate srls ctxt itms mI of
1.59 + (is as Pstate {env, ...}, ctxt, scr) => (is, env, ctxt, scr)
1.60 + | _ => raise ERROR "LI.by_tactic Apply_Method': uncovered case init_pstate"
1.61 + val ini = LItool.implicit_take prog env;
1.62 + val pos = start_new_level pos
1.63 +val NONE =
1.64 + (*case*) ini (*of*);
1.65 +
1.66 +val Next_Step (iii, ccc, ttt) = (*case*)
1.67 + LI.find_next_step prog (pt, (lev_dn p, Res)) is ctxt (*of*);
1.68 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Pstate ist), ctxt)
1.69 + = (prog, (pt, (lev_dn p, Res)), is, ctxt);
1.70 +
1.71 + (*case*)
1.72 + scan_to_tactic (prog, (ptp, ctxt)) (Pstate ist) (*of*);
1.73 +"~~~~~ fun scan_to_tactic , args:"; val ((prog, cc), (Pstate (ist as {path, ...})))
1.74 + = ((prog, (ptp, ctxt)), (Pstate ist));
1.75 + (*if*) path = [] (*then*);
1.76 +
1.77 +val Accept_Tac (ttt, sss, ccc) =
1.78 + scan_dn cc (trans_scan_dn ist) (Program.body_of prog);
1.79 +"~~~~~ fun scan_dn , args:"; val (cc, ist, (Const (\<^const_name>\<open>Let\<close>(*1*), _) $ e $ (Abs (i, T, b))))
1.80 + = (cc, (trans_scan_dn ist), (Program.body_of prog));
1.81 +
1.82 +val Accept_Tac (ttt, sss, ccc) = (*case*)
1.83 + scan_dn cc (ist |> path_down [L, R]) e (*of*);
1.84 +"~~~~~ fun scan_dn , args:"; val ((cc as (_, ctxt)), (ist as {eval, ...}), t)
1.85 + = (cc, (ist |> path_down [L, R]), e);
1.86 + (*if*) Tactical.contained_in t (*else*);
1.87 +val (Program.Tac prog_tac, form_arg) =
1.88 + (*case*) LItool.check_leaf "next " ctxt eval (get_subst ist) t (*of*);
1.89 +
1.90 +val Accept_Tac (ttt, sss, ccc) =
1.91 + check_tac cc ist (prog_tac, form_arg);
1.92 +"~~~~~ fun check_tac , args:"; val (((pt, p), ctxt), ist, (prog_tac, form_arg))
1.93 + = (cc, ist, (prog_tac, form_arg));
1.94 + val m = LItool.tac_from_prog pt (Proof_Context.theory_of ctxt) prog_tac
1.95 +val _ =
1.96 + (*case*) m (*of*);
1.97 +
1.98 + (*case*)
1.99 +Solve_Step.check m (pt, p) (*of*);
1.100 +"~~~~~ fun check , args:"; val ((Tactic.Take str), (pt, pos as (p_, p))) = (m, (pt, p));
1.101 +
1.102 +(*+*)val ([0], Res) = pos; (*<<<-------------------------*)
1.103 +(*-------------------- stop step into me Specify_Method ["diff", "integration"] -------------*)
1.104 +(*\------------------- step into me Specify_Method ["diff", "integration"] -----------------/*)
1.105 +
1.106 +val (p,_,f,nxt,_,pt) = me nxt''' p''' c pt''';
1.107 case nxt of (Apply_Method ["diff", "integration"]) => ()
1.108 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
1.109 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";