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@60557
|
32 |
val ctxt = Ctree.get_ctxt pt pos
|
walther@59823
|
33 |
val metID = get_obj g_metID pt pp;
|
walther@60154
|
34 |
val metID' = if metID = MethodC.id_empty then (thd3 o snd3) (get_obj g_origin pt pp) else metID
|
Walther@60557
|
35 |
val (sc, srls) = (case MethodC.from_store_PIDE ctxt metID' of
|
walther@59823
|
36 |
{scr = Rule.Prog sc, srls, ...} => (sc, srls) | _ => raise ERROR "from_prog 1")
|
walther@59823
|
37 |
val subst = get_istate_LI pt (p, p_) |> Istate.the_pstate |> Istate.get_subst
|
walther@59823
|
38 |
val ctxt = get_ctxt pt (p, p_)
|
walther@59823
|
39 |
in map ((LItool.tac_from_prog pt thy) o Program.rep_stacexpr o #1 o
|
walther@59823
|
40 |
(LItool.check_leaf "selrul" ctxt srls subst)) (Auto_Prog.stacpbls sc)
|
walther@59823
|
41 |
end;
|
walther@59823
|
42 |
|
walther@59823
|
43 |
(* fetch tactics from script and filter _applicable_ tactics;
|
walther@59823
|
44 |
in case of Rewrite_Set* go down to _atomic_ rewrite-tactics *)
|
walther@59823
|
45 |
fun specific_from_prog _ (([], Res) : pos') =
|
walther@59823
|
46 |
raise PTREE "no tactics applicable at the end of a calculation"
|
walther@59932
|
47 |
| specific_from_prog pt (pos as (p, p_)) =
|
walther@59932
|
48 |
if Pos.on_specification pos
|
walther@59823
|
49 |
then [get_obj g_tac pt p]
|
walther@59823
|
50 |
else
|
walther@59823
|
51 |
let
|
Walther@60534
|
52 |
val pp = par_pblobj pt p
|
Walther@60534
|
53 |
val ctxt = Ctree.get_loc pt pos |> snd
|
Walther@60534
|
54 |
val thy = Ctree.get_loc pt pos |> snd |> Proof_Context.theory_of
|
Walther@60534
|
55 |
|
walther@59823
|
56 |
val metID = get_obj g_metID pt pp
|
walther@59823
|
57 |
val metID' =
|
walther@60154
|
58 |
if metID = MethodC.id_empty
|
Walther@60534
|
59 |
then (get_obj g_origin pt pp) |> #2 |> #3
|
walther@59823
|
60 |
else metID
|
Walther@60557
|
61 |
val (sc, srls, erls, ro) = (case MethodC.from_store_PIDE ctxt metID' of
|
walther@59823
|
62 |
{scr = Rule.Prog sc, srls, erls, rew_ord' = ro, ...} => (sc, srls, erls, ro)
|
walther@59823
|
63 |
| _ => raise ERROR "specific_from_prog 1")
|
Walther@60534
|
64 |
val (env, (a, v)) = (case get_istate_LI pt pos of
|
walther@59823
|
65 |
Istate.Pstate pst => (Istate.get_subst pst) | _ => error "specific_from_prog 2")
|
Walther@60534
|
66 |
val alltacs = sc
|
Walther@60534
|
67 |
|> Auto_Prog.stacpbls
|
Walther@60534
|
68 |
|> map (fn tac_pbl => tac_pbl
|
Walther@60534
|
69 |
|> LItool.check_leaf "selrul" ctxt srls (env, (a, v))
|
Walther@60534
|
70 |
|> #1
|
Walther@60534
|
71 |
|> Program.rep_stacexpr
|
Walther@60534
|
72 |
|> LItool.tac_from_prog pt thy)
|
walther@59823
|
73 |
val f =
|
walther@59823
|
74 |
(case p_ of Frm => get_obj g_form pt p | Res => (fst o (get_obj g_result pt)) p
|
Walther@60534
|
75 |
| _ => raise ERROR "specific_from_prog 3")
|
walther@59823
|
76 |
(*WN071231 ? replace atomic_appl_tacs with applicable_in (ineff!) ?*)
|
walther@59914
|
77 |
in
|
Walther@60534
|
78 |
alltacs
|
Walther@60534
|
79 |
|> map (Tactic.applicable ctxt ro erls f)
|
Walther@60534
|
80 |
|> flat
|
Walther@60534
|
81 |
|> distinct Tactic.eq_tac
|
walther@59914
|
82 |
end;
|
walther@59823
|
83 |
|
Walther@60557
|
84 |
(**)end(**)
|