walther@59920
|
1 |
(* Title: Specify/specify-step.sml
|
walther@59920
|
2 |
Author: Walther Neuper
|
walther@59920
|
3 |
(c) due to copyright terms
|
walther@59923
|
4 |
|
walther@59920
|
5 |
Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.
|
walther@59920
|
6 |
*)
|
walther@59920
|
7 |
|
walther@59920
|
8 |
signature SPECIFY_STEP =
|
walther@59920
|
9 |
sig
|
walther@59922
|
10 |
val check: Tactic.input -> Calc.T -> Applicable.T
|
walther@59959
|
11 |
val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
|
Walther@60782
|
12 |
val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
|
walther@59920
|
13 |
end
|
walther@59920
|
14 |
|
walther@59920
|
15 |
(**)
|
walther@59920
|
16 |
structure Specify_Step(**): SPECIFY_STEP(**) =
|
walther@59920
|
17 |
struct
|
walther@59920
|
18 |
(**)
|
walther@59920
|
19 |
|
walther@60014
|
20 |
fun complete_for mID (ctree, pos) =
|
walther@60009
|
21 |
let
|
Walther@60760
|
22 |
val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
|
Walther@60760
|
23 |
...} = Calc.specify_data (ctree, pos);
|
Walther@60760
|
24 |
val ctxt = Ctree.get_ctxt ctree pos
|
Walther@60760
|
25 |
val (dI, _, _) = References.select_input o_refs refs;
|
Walther@60760
|
26 |
val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
|
Walther@60760
|
27 |
val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
|
Walther@60760
|
28 |
val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
|
Walther@60779
|
29 |
val (_, (i_model, _)) = M_Match.by_i_models ctxt o_model' (i_prob, i_prob)
|
Walther@60779
|
30 |
(m_patt, where_, where_rls);
|
Walther@60760
|
31 |
in
|
Walther@60760
|
32 |
(o_model', ctxt', i_model)
|
Walther@60760
|
33 |
end
|
walther@60009
|
34 |
|
walther@59922
|
35 |
(*
|
walther@59922
|
36 |
check tactics (input by the user, mostly) for applicability
|
walther@59922
|
37 |
and determine as much of the result of the tactic as possible initially.
|
walther@59922
|
38 |
*)
|
walther@59930
|
39 |
fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))
|
walther@59930
|
40 |
(*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
|
walther@59930
|
41 |
| check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
|
walther@59930
|
42 |
| check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
|
walther@59930
|
43 |
(*required for corner cases, e.g. test setup in inssort.sml*)
|
walther@59930
|
44 |
| check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
|
walther@59930
|
45 |
| check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
|
walther@59930
|
46 |
| check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
|
Walther@60715
|
47 |
| check Tactic.Model_Problem (pt, pos as (p, _)) =
|
Walther@60715
|
48 |
let
|
Walther@60764
|
49 |
val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of
|
Walther@60764
|
50 |
Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
|
Walther@60715
|
51 |
| _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
|
Walther@60715
|
52 |
val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
|
Walther@60782
|
53 |
val pbl = I_Model.init ctxt o_model model_patt
|
Walther@60774
|
54 |
in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
|
walther@59930
|
55 |
| check (Tactic.Refine_Problem pI) (pt, (p, _)) =
|
walther@59923
|
56 |
let
|
Walther@60628
|
57 |
val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60628
|
58 |
Ctree.PblObj {origin = (_, (dI, _, _), _), spec = (dI', _, _), probl = itms, ctxt, ...}
|
Walther@60628
|
59 |
=> (dI, dI', itms, ctxt)
|
walther@59930
|
60 |
| _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
|
walther@59923
|
61 |
val thy = if dI' = ThyC.id_empty then dI else dI';
|
walther@59923
|
62 |
in
|
Walther@60779
|
63 |
case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
|
Walther@60628
|
64 |
NONE => Applicable.No
|
Walther@60628
|
65 |
(Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
|
Walther@60774
|
66 |
| SOME (pI', (i_model, prec)) =>
|
walther@59923
|
67 |
if pI' = pI
|
Walther@60628
|
68 |
then Applicable.No
|
Walther@60628
|
69 |
(Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
|
Walther@60775
|
70 |
else Applicable.Yes (Tactic.Refine_Problem' (pI', (i_model, prec)))
|
walther@59923
|
71 |
end
|
Walther@60628
|
72 |
| check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
|
walther@59930
|
73 |
let
|
Walther@60628
|
74 |
val (oris, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60628
|
75 |
Ctree.PblObj {origin = (oris, _, _), ctxt, ...} => (oris, ctxt)
|
walther@59930
|
76 |
| _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
|
walther@59930
|
77 |
in
|
Walther@60742
|
78 |
case Refine.by_o_model ctxt oris pI of
|
walther@59930
|
79 |
SOME pblID =>
|
walther@60154
|
80 |
Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, MethodC.id_empty, [(*filled later*)]))
|
Walther@60628
|
81 |
| NONE => Applicable.No
|
Walther@60628
|
82 |
(Tactic.input_to_string ctxt (Tactic.Refine_Tacitly pI) ^ " not applicable")
|
walther@59930
|
83 |
end
|
walther@60009
|
84 |
| check (Tactic.Specify_Method mID) (ctree, pos) =
|
walther@60009
|
85 |
let
|
walther@60014
|
86 |
val (o_model, _, i_model) = complete_for mID (ctree, pos)
|
walther@60009
|
87 |
in
|
Walther@60774
|
88 |
Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
|
walther@60009
|
89 |
end
|
Walther@60556
|
90 |
| check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
|
walther@59923
|
91 |
let
|
Walther@60760
|
92 |
val (oris, pI, pI', probl, meth, ctxt) = case Ctree.get_obj I pt p of
|
Walther@60760
|
93 |
Ctree.PblObj {origin = (oris, (_, pI, _), _), spec = (_, pI', _), probl, meth, ctxt, ...}
|
Walther@60760
|
94 |
=> (oris, pI, pI', probl, meth, ctxt)
|
walther@59930
|
95 |
| _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
|
Walther@60585
|
96 |
val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
|
Walther@60760
|
97 |
val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
|
Walther@60782
|
98 |
then (false, (I_Model.init ctxt oris model, []: (bool * term) list))
|
Walther@60779
|
99 |
else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
|
walther@59923
|
100 |
in
|
Walther@60774
|
101 |
Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))
|
walther@59930
|
102 |
end
|
walther@59930
|
103 |
| check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
|
walther@59922
|
104 |
| check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
|
Walther@60628
|
105 |
| check tac (ctree, pos) =
|
Walther@60628
|
106 |
let
|
Walther@60628
|
107 |
val ctxt = Ctree.get_ctxt ctree pos
|
Walther@60628
|
108 |
in
|
Walther@60628
|
109 |
raise ERROR ("Specify_Step.check called for " ^
|
Walther@60628
|
110 |
Tactic.input_to_string ctxt tac ^ " at" ^ Pos.pos'2str pos)
|
Walther@60628
|
111 |
end;
|
walther@59920
|
112 |
|
walther@59933
|
113 |
(* exceed line length, because result type will change *)
|
walther@59933
|
114 |
fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
|
walther@59933
|
115 |
let
|
Walther@60779
|
116 |
val pt = Ctree.update_pbl pt p itms
|
Walther@60779
|
117 |
val pt = Ctree.update_met pt p met
|
walther@59933
|
118 |
in
|
walther@59969
|
119 |
(pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
|
walther@59933
|
120 |
end
|
walther@59933
|
121 |
| add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
|
walther@59969
|
122 |
(pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
|
walther@59933
|
123 |
case p_ of
|
Walther@60779
|
124 |
Pos.Pbl => Ctree.update_pbl pt p itmlist
|
Walther@60779
|
125 |
| Pos.Met => Ctree.update_met pt p itmlist
|
walther@59933
|
126 |
| _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
|
walther@59933
|
127 |
| add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
|
walther@59969
|
128 |
(pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
|
walther@59933
|
129 |
case p_ of
|
Walther@60779
|
130 |
Pos.Pbl => Ctree.update_pbl pt p itmlist
|
Walther@60779
|
131 |
| Pos.Met => Ctree.update_met pt p itmlist
|
walther@59933
|
132 |
| _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
|
walther@59933
|
133 |
| add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
|
walther@59969
|
134 |
(pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
|
walther@59933
|
135 |
case p_ of
|
Walther@60779
|
136 |
Pos.Pbl => Ctree.update_pbl pt p itmlist
|
Walther@60779
|
137 |
| Pos.Met => Ctree.update_met pt p itmlist
|
walther@59933
|
138 |
| _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
|
walther@59933
|
139 |
| add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
|
walther@59969
|
140 |
(pos, [] , Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
|
walther@59933
|
141 |
Ctree.update_domID pt p domID)
|
walther@59933
|
142 |
| add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
|
walther@59933
|
143 |
let
|
Walther@60779
|
144 |
val pt = Ctree.update_pbl pt p itms
|
walther@59933
|
145 |
val pt = Ctree.update_pblID pt p pI
|
walther@59933
|
146 |
in
|
walther@59969
|
147 |
((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
|
walther@59933
|
148 |
end
|
walther@59933
|
149 |
| add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
|
walther@59933
|
150 |
let
|
walther@59933
|
151 |
val pt = Ctree.update_oris pt p oris
|
Walther@60779
|
152 |
val pt = Ctree.update_met pt p itms
|
walther@59933
|
153 |
val pt = Ctree.update_metID pt p mID
|
walther@59933
|
154 |
in
|
walther@59969
|
155 |
((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
|
walther@59933
|
156 |
end
|
walther@59933
|
157 |
| add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
|
walther@59933
|
158 |
let
|
Walther@60779
|
159 |
val pt = Ctree.update_pbl pt p pbl
|
walther@59933
|
160 |
val pt = Ctree.update_orispec pt p (domID, pIre, metID)
|
walther@59933
|
161 |
in
|
walther@59969
|
162 |
(pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
|
walther@59933
|
163 |
end
|
walther@59933
|
164 |
| add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =
|
walther@59933
|
165 |
let
|
walther@59933
|
166 |
val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p
|
walther@59933
|
167 |
val pt = Ctree.update_spec pt p (dI, pI, mI)
|
walther@59933
|
168 |
in
|
walther@59969
|
169 |
(pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
|
walther@59933
|
170 |
end
|
Walther@60630
|
171 |
| add (Tactic.Begin_Trans' t) l (pt, pos as (p, Frm)) =
|
walther@59933
|
172 |
let
|
walther@59933
|
173 |
val (pt, c) = Ctree.cappend_form pt p l t
|
walther@59933
|
174 |
val pt = Ctree.update_branch pt p Ctree.TransitiveB
|
walther@59933
|
175 |
val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
|
walther@59933
|
176 |
val (pt, c') = Ctree.cappend_form pt p l t
|
Walther@60630
|
177 |
val ctxt = Ctree.get_ctxt pt pos
|
walther@59933
|
178 |
in
|
Walther@60675
|
179 |
((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term ctxt t), pt)
|
walther@59933
|
180 |
end
|
walther@59933
|
181 |
| add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
|
walther@59933
|
182 |
let
|
walther@59933
|
183 |
val p' = Pos.lev_up p
|
walther@59933
|
184 |
val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
|
walther@59933
|
185 |
in
|
walther@59959
|
186 |
((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
|
walther@59933
|
187 |
end
|
Walther@60655
|
188 |
| add m' (_, ctxt) (_, pos) =
|
Walther@60655
|
189 |
raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of ctxt m' ^ " at " ^ Pos.pos'2str pos)
|
walther@59920
|
190 |
|
walther@59920
|
191 |
(**)end(**);
|