walther@59823
|
1 |
(* Title: MathEngine/fetch-tactics.sml
|
walther@59823
|
2 |
Author: Walther Neuper
|
walther@59823
|
3 |
(c) due to copyright terms
|
walther@59823
|
4 |
|
walther@59823
|
5 |
Fetch tactics from a program in order to present them for selection by the user
|
walther@59823
|
6 |
*)
|
walther@59823
|
7 |
|
walther@59823
|
8 |
signature FETCH_TACTICS =
|
walther@59823
|
9 |
sig
|
walther@59846
|
10 |
val from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list
|
walther@59846
|
11 |
val specific_from_prog : Ctree.ctree -> Pos.pos' -> Tactic.input list
|
walther@59823
|
12 |
end
|
walther@59823
|
13 |
|
walther@59823
|
14 |
(**)
|
walther@59823
|
15 |
structure Fetch_Tacs(**): FETCH_TACTICS(**) =
|
walther@59823
|
16 |
struct
|
walther@59823
|
17 |
(**)
|
walther@59823
|
18 |
open Ctree
|
walther@59823
|
19 |
open Pos
|
walther@59823
|
20 |
|
walther@59823
|
21 |
(* fetch _all_ tactics from a program *)
|
walther@59823
|
22 |
fun from_prog _ ([], Res) =
|
walther@59823
|
23 |
raise PTREE "no tactics applicable at the end of a calculation"
|
walther@59932
|
24 |
| from_prog pt (pos as (p, p_)) =
|
walther@59932
|
25 |
if Pos.on_specification pos
|
walther@59823
|
26 |
then [get_obj g_tac pt p]
|
walther@59823
|
27 |
else
|
walther@59823
|
28 |
let
|
walther@59823
|
29 |
val pp = par_pblobj pt p;
|
walther@59823
|
30 |
val thy' = get_obj g_domID pt pp;
|
walther@59881
|
31 |
val thy = ThyC.get_theory thy';
|
walther@59823
|
32 |
val metID = get_obj g_metID pt pp;
|
walther@59903
|
33 |
val metID' = if metID = Method.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
|
walther@59823
|
34 |
val (sc, srls) = (case Specify.get_met metID' of
|
walther@59823
|
35 |
{scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
|
walther@59823
|
36 |
val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
|
walther@59823
|
37 |
val ctxt = get_ctxt pt (p, p_)
|
walther@59823
|
38 |
in map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
|
walther@59823
|
39 |
(LItool.check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
|
walther@59823
|
40 |
end;
|
walther@59823
|
41 |
|
walther@59823
|
42 |
(* fetch tactics from script and filter _applicable_ tactics;
|
walther@59823
|
43 |
in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
|
walther@59823
|
44 |
fun specific_from_prog _ (([], Res) : pos') =
|
walther@59823
|
45 |
raise PTREE "no tactics applicable at the end of a calculation"
|
walther@59932
|
46 |
| specific_from_prog pt (pos as (p, p_)) =
|
walther@59932
|
47 |
if Pos.on_specification pos
|
walther@59823
|
48 |
then [get_obj g_tac pt p]
|
walther@59823
|
49 |
else
|
walther@59823
|
50 |
let
|
walther@59823
|
51 |
val pp = par_pblobj pt p
|
walther@59823
|
52 |
val thy' = get_obj g_domID pt pp
|
walther@59881
|
53 |
val thy = ThyC.get_theory thy'
|
walther@59823
|
54 |
val metID = get_obj g_metID pt pp
|
walther@59823
|
55 |
val metID' =
|
walther@59903
|
56 |
if metID = Method.id_empty
|
walther@59823
|
57 |
then (thd3 o snd3) (get_obj g_origin pt pp)
|
walther@59823
|
58 |
else metID
|
walther@59823
|
59 |
val (sc, srls, erls, ro) = (case Specify.get_met metID' of
|
walther@59823
|
60 |
{scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
|
walther@59823
|
61 |
| _ => raise ERROR "specific_from_prog 1")
|
walther@59823
|
62 |
val (env, (a, v)) = (case get_istate_LI pt (p, p_) of
|
walther@59823
|
63 |
Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2")
|
walther@59823
|
64 |
val ctxt = get_ctxt pt (p, p_)
|
walther@59914
|
65 |
val alltacs = (*we expect at least 1 Prog_Tac in a program*)
|
walther@59823
|
66 |
map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
|
walther@59823
|
67 |
(LItool.check_leaf "selrul" ctxt srls (env, (a, v)))) (Auto_Prog.stacpbls sc)
|
walther@59823
|
68 |
val f =
|
walther@59823
|
69 |
(case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
|
walther@59823
|
70 |
| _ => raise ERROR "specific_from_prog 2")
|
walther@59823
|
71 |
(*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
|
walther@59914
|
72 |
in
|
walther@59914
|
73 |
((gen_distinct Tactic.eq_tac) o flat o (map (Tactic.applicable thy ro erls f))) alltacs
|
walther@59914
|
74 |
end;
|
walther@59823
|
75 |
|
walther@59823
|
76 |
(**)end(**) |