39 |
39 |
40 locate_input_tactic sc (pt, po) (fst is) (snd is) m; |
40 locate_input_tactic sc (pt, po) (fst is) (snd is) m; |
41 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac) |
41 "~~~~~ fun locate_input_tactic , args:"; val (Rule.Prog progr, cstate, istate, ctxt, tac) |
42 = (sc, (pt, po), (fst is), (snd is), m); |
42 = (sc, (pt, po), (fst is), (snd is), m); |
43 |
43 |
44 val Ackn_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*) |
44 val Accept_Tac1 (_, _, Subproblem' (_, _, _, _, _, _)) = (*case*) |
45 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*); |
45 scan_to_tactic1 (prog, (cstate, ctxt, tac)) istate (*of*); |
46 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), |
46 "~~~~~ fun scan_to_tactic1 , args:"; val ((prog, (cctt as ((_, p), _, _))), |
47 (Istate.Pstate (ist as {path, ...}))) |
47 (Istate.Pstate (ist as {path, ...}))) |
48 = ((progr, (cstate, ctxt, tac)), istate); |
48 = ((progr, (cstate, ctxt, tac)), istate); |
49 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); |
49 (*if*) path = [] orelse ((last_elem o fst) p = 0 andalso snd p = Res) (*else*); |
83 scan_up1 yyy (ist |> path_up) (go (path_up' path) prog); |
83 scan_up1 yyy (ist |> path_up) (go (path_up' path) prog); |
84 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _)) |
84 "~~~~~ fun scan_up1 , args:"; val ((yyy as (prog, xxx as (cstate, _, _))), ist, (Const ("HOL.Let"(*1*), _) $ _)) |
85 = ( yyy, (ist |> path_up), (go (path_up' path) prog)); |
85 = ( yyy, (ist |> path_up), (go (path_up' path) prog)); |
86 val (i, body) = check_Let_up ist prog |
86 val (i, body) = check_Let_up ist prog |
87 ; |
87 ; |
88 (*case*) scan_dn1 xxx (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef) body (*of*); |
88 (*case*) scan_dn1 xxx (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef) body (*of*); |
89 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) |
89 "~~~~~ fun scan_dn1 , args:"; val (xxx, ist, (Const ("HOL.Let", _) $ e $ (Abs (id, T, b)))) |
90 = (xxx, (ist |> path_up_down [R, D] |> upd_env i |> set_or Aundef), body); |
90 = (xxx, (ist |> path_up_down [R, D] |> upd_env i |> set_or ORundef), body); |
91 |
91 |
92 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); |
92 (*case*) scan_dn1 xxx (ist |> path_down [L, R]) e (*of*); |
93 (*======= end of scanning tacticals, a leaf =======*) |
93 (*======= end of scanning tacticals, a leaf =======*) |
94 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
94 "~~~~~ fun scan_dn1 , args:"; val (((pt, p), ctxt, tac), (ist as {env, eval, or, ...}), t) |
95 = (xxx, (ist |> path_down [L, R]), e); |
95 = (xxx, (ist |> path_down [L, R]), e); |
96 |
96 |
97 val (NONE, Program.Tac _) = (*case*) |
97 val (NONE, Program.Tac _) = (*case*) |
98 handle_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
98 interpret_leaf "locate" (Context.theory_name (Rule.Isac"")) eval (get_subst ist) t (*of*); |
99 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) |
99 "~~~~~ fun interpret_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) |
100 = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t); |
100 = ("locate", (Context.theory_name (Rule.Isac"")), eval, (get_subst ist), t); |
101 |
101 |
102 val (a', Program.Tac stac) = (*case*) Prog_Tac.subst_stacexpr E a v t (*of*); |
102 val (a', Program.Tac stac) = (*case*) Prog_Tac.eval_leaf E a v t (*of*); |
103 "~~~~~ fun subst_stacexpr , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _))) |
103 "~~~~~ fun eval_leaf , args:"; val (E, _, _, (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _))) |
104 = (E, a, v, t); |
104 = (E, a, v, t); |
105 |
105 |
106 (NONE, Program.Tac (subst_atomic E t)); (*return value*) |
106 (NONE, Program.Tac (subst_atomic E t)); (*return value*) |
107 "~~~~~ from subst_stacexpr to handle_leaf return val:"; val ((a', Program.Tac stac)) |
107 "~~~~~ from eval_leaf to interpret_leaf return val:"; val ((a', Program.Tac stac)) |
108 = ((NONE : term option, Program.Tac (subst_atomic E t))); |
108 = ((NONE : term option, Program.Tac (subst_atomic E t))); |
109 val stac' = |
109 val stac' = |
110 Rewrite.eval_listexpr_ (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac); |
110 Rewrite.eval_prog_expr (Celem.assoc_thy thy) srls (subst_atomic (update_opt E (a,v)) stac); |
111 |
111 |
112 (*return value*) (a', Program.Tac stac'); |
112 (*return value*) (a', Program.Tac stac'); |
113 "~~~~~ from handle_leaf to scan_dn1 return val:"; val (a', Program.Tac stac) |
113 "~~~~~ from interpret_leaf to scan_dn1 return val:"; val (a', Program.Tac stac) |
114 = ((a' : term option, Program.Tac stac')); |
114 = ((a' : term option, Program.Tac stac')); |
115 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); |
115 val Lucin.Ass (m, v', ctxt) = (*case*) Lucin.associate pt ctxt (m, stac) (*of*); |
116 |
116 |
117 (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else (); |
117 (*+*)if is_e_ctxt ctxt then error "ERROR: scan_dn1 returns e_ctxt" else (); |
118 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |
118 (*\\--1 end step into relevant call ----------------------------------------------------------//*) |