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
12 val complete_for: MethodC.id -> Calc.T -> O_Model.T * Proof.context * I_Model.T
16 structure Specify_Step(**): SPECIFY_STEP(**) =
20 fun complete_for mID (ctree, pos) =
22 val {origin = (o_model, o_refs, _), spec = refs, probl = i_prob, meth = met_imod, ctxt,
23 ...} = Calc.specify_data (ctree, pos);
24 val ctxt = Ctree.get_ctxt ctree pos
25 val (dI, _, _) = References.select_input o_refs refs;
26 val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
27 val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
28 val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
29 val (_, (i_model, _)) = M_Match.by_i_models ctxt o_model' (i_prob, i_prob)
30 (m_patt, where_, where_rls);
32 (o_model', ctxt', i_model)
36 check tactics (input by the user, mostly) for applicability
37 and determine as much of the result of the tactic as possible initially.
39 fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)]))
40 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*)
41 | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)]))
42 | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)]))
43 (*required for corner cases, e.g. test setup in inssort.sml*)
44 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct')
45 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct')
46 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct')
47 | check Tactic.Model_Problem (pt, pos as (p, _)) =
49 val (ctxt, o_model, pI') = case Ctree.get_obj I pt p of
50 Ctree.PblObj {ctxt, origin = (o_model, (_, pI', _), _), ...} => (ctxt, o_model, pI')
51 | _ => raise ERROR "Specify_Step.check Model_Problem: uncovered case Ctree.get_obj"
52 val {model = model_patt, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pI'
53 val pbl = I_Model.init ctxt o_model model_patt
54 in Applicable.Yes (Tactic.Model_Problem' (pI', pbl, [])) end
55 | check (Tactic.Refine_Problem pI) (pt, (p, _)) =
57 val (dI, dI', itms, ctxt) = case Ctree.get_obj I pt p of
58 Ctree.PblObj {origin = (_, (dI, _, _), _), spec = (dI', _, _), probl = itms, ctxt, ...}
59 => (dI, dI', itms, ctxt)
60 | _ => raise ERROR "Specify_Step.check Refine_Problem: uncovered case Ctree.get_obj"
61 val thy = if dI' = ThyC.id_empty then dI else dI';
63 case Refine.problem (ThyC.get_theory ctxt thy) pI itms of
65 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
66 | SOME (pI', (i_model, prec)) =>
69 (Tactic.input_to_string ctxt (Tactic.Refine_Problem pI) ^ " not applicable")
70 else Applicable.Yes (Tactic.Refine_Problem' (pI', (i_model, prec)))
72 | check (Tactic.Refine_Tacitly pI) (pt, (p, _)) =
74 val (oris, ctxt) = case Ctree.get_obj I pt p of
75 Ctree.PblObj {origin = (oris, _, _), ctxt, ...} => (oris, ctxt)
76 | _ => raise ERROR "Specify_Step.check Refine_Tacitly: uncovered case Ctree.get_obj"
78 case Refine.by_o_model ctxt oris pI of
80 Applicable.Yes (Tactic.Refine_Tacitly' (pI, pblID, ThyC.id_empty, MethodC.id_empty, [(*filled later*)]))
81 | NONE => Applicable.No
82 (Tactic.input_to_string ctxt (Tactic.Refine_Tacitly pI) ^ " not applicable")
84 | check (Tactic.Specify_Method mID) (ctree, pos) =
86 val (o_model, _, i_model) = complete_for mID (ctree, pos)
88 Applicable.Yes (Tactic.Specify_Method' (mID, o_model, i_model))
90 | check (Tactic.Specify_Problem pID) (pt, pos as (p, _)) =
92 val (oris, pI, pI', probl, meth, ctxt) = case Ctree.get_obj I pt p of
93 Ctree.PblObj {origin = (oris, (_, pI, _), _), spec = (_, pI', _), probl, meth, ctxt, ...}
94 => (oris, pI, pI', probl, meth, ctxt)
95 | _ => raise ERROR "Specify_Step.check Specify_Problem: uncovered case Ctree.get_obj"
96 val {model, where_, where_rls, ...} = Problem.from_store (Ctree.get_ctxt pt pos) pID;
97 val (check, (i_model, preconds)) = if pI' = Problem.id_empty andalso pI = Problem.id_empty
98 then (false, (I_Model.init ctxt oris model, []: (bool * term) list))
99 else M_Match.by_i_models ctxt oris (probl, meth) (model, where_, where_rls)
101 Applicable.Yes (Tactic.Specify_Problem' (pID, (check, (i_model, preconds))))
103 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI)
104 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable"
105 | check tac (ctree, pos) =
107 val ctxt = Ctree.get_ctxt ctree pos
109 raise ERROR ("Specify_Step.check called for " ^
110 Tactic.input_to_string ctxt tac ^ " at" ^ Pos.pos'2str pos)
113 (* exceed line length, because result type will change *)
114 fun add (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) =
116 val pt = Ctree.update_pbl pt p itms
117 val pt = Ctree.update_met pt p met
119 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
121 | add (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
122 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet,P_Model.from (Proof_Context.theory_of ctxt) [][]),
124 Pos.Pbl => Ctree.update_pbl pt p itmlist
125 | Pos.Met => Ctree.update_met pt p itmlist
126 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
127 | add (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
128 (pos, [], (Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] [])),
130 Pos.Pbl => Ctree.update_pbl pt p itmlist
131 | Pos.Met => Ctree.update_met pt p itmlist
132 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
133 | add (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) =
134 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
136 Pos.Pbl => Ctree.update_pbl pt p itmlist
137 | Pos.Met => Ctree.update_met pt p itmlist
138 | _ => raise ERROR ("uncovered case " ^ Pos.pos_2str p_))
139 | add (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) =
140 (pos, [] , Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []),
141 Ctree.update_domID pt p domID)
142 | add (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) =
144 val pt = Ctree.update_pbl pt p itms
145 val pt = Ctree.update_pblID pt p pI
147 ((p, Pos.Pbl), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
149 | add (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) =
151 val pt = Ctree.update_oris pt p oris
152 val pt = Ctree.update_met pt p itms
153 val pt = Ctree.update_metID pt p mID
155 ((p, Pos.Met), [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
157 | add (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) =
159 val pt = Ctree.update_pbl pt p pbl
160 val pt = Ctree.update_orispec pt p (domID, pIre, metID)
162 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
164 | add (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) =
166 val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p
167 val pt = Ctree.update_spec pt p (dI, pI, mI)
169 (pos, [], Test_Out.PpcKF (Test_Out.Upblmet, P_Model.from (Proof_Context.theory_of ctxt) [] []), pt)
171 | add (Tactic.Begin_Trans' t) l (pt, pos as (p, Frm)) =
173 val (pt, c) = Ctree.cappend_form pt p l t
174 val pt = Ctree.update_branch pt p Ctree.TransitiveB
175 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p
176 val (pt, c') = Ctree.cappend_form pt p l t
177 val ctxt = Ctree.get_ctxt pt pos
179 ((p, Frm), c @ c', Test_Out.FormKF (UnparseC.term ctxt t), pt)
181 | add (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *)
183 val p' = Pos.lev_up p
184 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete
186 ((p', Pos.Res), c, Test_Out.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt)
188 | add m' (_, ctxt) (_, pos) =
189 raise ERROR ("Specify_Step.add: not impl.for " ^ Tactic.string_of ctxt m' ^ " at " ^ Pos.pos'2str pos)