1 (* Title: Specify/specify-step.sml
3 (c) due to copyright terms
5 Code for the specify-phase in analogy to structure Solve_Step for the solve-phase.
8 signature SPECIFY_STEP =
10 val check: Tactic.input -> Calc.T -> Applicable.T
11 val add: Tactic.T -> Istate_Def.T * Proof.context -> Calc.T -> Test_Out.T
13 val complete_for: Method.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
16 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
18 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22 structure Specify_Step(**): SPECIFY_STEP(**) =
26 fun complete_for mID (ctree, pos) =
28 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, ctxt,
29 ...} = Calc.specify_data (ctree, pos);
30 val (dI, _, _) = References.select o_refs refs;
31 val {ppc = m_patt, pre, prls, ...} = Method.from_store mID
32 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
33 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
34 val thy = ThyC.get_theory dI
35 val (_, (i_model, _)) = M_Match.match_itms_oris thy i_prob (m_patt, pre, prls) o_model';
37 (o_model', ctxt', i_model)
41 check tactics (input by the user, mostly) for applicability
42 and determine as much of the result of the tactic as possible initially.
44 fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))
45 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
46 | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
47 | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
48 (*required for corner cases, e.g. test setup in inssort.sml*)
49 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
50 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
51 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
52 | check Tactic.Model_Problem (pt, (p, _)) =
54 val pI' = case Ctree.get_obj I pt p of
55 Ctree.PblObj {origin = (_, (_, pI', _),_), ...} => pI'
56 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
57 val {ppc, ...} = Problem.from_store pI'
58 val pbl = I_Model.init ppc
59 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
60 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
62 val (dI, dI', itms) = case Ctree.get_obj I pt p of
63 Ctree.PblObj {origin= (_, (dI, _, _), _), spec= (dI', _, _), probl = itms, ...}
65 | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
66 val thy = if dI' = ThyC.id_empty then dI else dI';
68 case Refine.problem (ThyC.get_theory thy) pI itms of
69 NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
70 | SOME (rf as (pI', _)) =>
72 then Applicable.No (Tactic.input_to_string (Tactic.Refine_Problem pI) ^ " not applicable")
73 else Applicable.Yes (Tactic.Refine_Problem' rf)
75 | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
77 val oris = case Ctree.get_obj I pt p of
78 Ctree.PblObj {origin = (oris, _, _), ...} => oris
79 | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
81 case Refine.refine_ori oris pI of
83 Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, Method.id_empty, [(*filled later*)]))
84 | NONE => Applicable.No (Tactic.input_to_string (Tactic.Refine_Tacitly pI) ^ " not applicable")
86 | check (Tactic.Specify_Method mID) (ctree, pos) =
88 val (o_model, _, i_model) = complete_for mID (ctree, pos)
90 Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
92 | check (Tactic.Specify_Problem pID) (pt, (p, _)) =
94 val (oris, dI, pI, dI', pI', itms) = case Ctree.get_obj I pt p of
95 Ctree.PblObj {origin = (oris, (dI, pI, _), _), spec = (dI', pI', _), probl = itms, ...}
96 => (oris, dI, pI, dI', pI', itms)
97 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
98 val thy = ThyC.get_theory (if dI' = ThyC.id_empty then dI else dI');
99 val {ppc, where_, prls, ...} = Problem.from_store pID;
100 val pbl = if pI' = Problem.id_empty andalso pI = Problem.id_empty
101 then (false, (I_Model.init ppc, []))
102 else M_Match.match_itms_oris thy itms (ppc, where_, prls) oris;
104 Applicable.Yes (Tactic.Specify_Problem' (pID, pbl))
106 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
107 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
108 | check tac (_, pos) =
109 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos);
111 (* exceed line length, because result type will change *)
112 fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
114 val pt = Ctree.update_pbl pt p itms
115 val pt = Ctree.update_met pt p met
117 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
119 | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
120 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
122 Pos.Pbl => Ctree.update_pbl pt p itmlist
123 | Pos.Met => Ctree.update_met pt p itmlist
124 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
125 | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
126 (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
128 Pos.Pbl => Ctree.update_pbl pt p itmlist
129 | Pos.Met => Ctree.update_met pt p itmlist
130 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
131 | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
132 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
134 Pos.Pbl => Ctree.update_pbl pt p itmlist
135 | Pos.Met => Ctree.update_met pt p itmlist
136 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
137 | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
138 (pos, [] , Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
139 Ctree.update_domID pt p domID)
140 | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
142 val pt = Ctree.update_pbl pt p itms
143 val pt = Ctree.update_pblID pt p pI
145 ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
147 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
149 val pt = Ctree.update_oris pt p oris
150 val pt = Ctree.update_met pt p itms
151 val pt = Ctree.update_metID pt p mID
153 ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
155 | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
157 val pt = Ctree.update_pbl pt p pbl
158 val pt = Ctree.update_orispec pt p (domID, pIre, metID)
160 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
162 | add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =
164 val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p
165 val pt = Ctree.update_spec pt p (dI, pI, mI)
167 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
169 | add (Tactic.Begin_Trans' t) l (pt, (p, Frm)) =
171 val (pt, c) = Ctree.cappend_form pt p l t
172 val pt = Ctree.update_branch pt p Ctree.TransitiveB
173 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
174 val (pt, c') = Ctree.cappend_form pt p l t
176 ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term t), pt)
178 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
180 val p' = Pos.lev_up p
181 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
183 ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
185 | add m' _ (_, pos) =
186 raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos)