26 *) |
26 *) |
27 fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)])) |
27 fun check (Tactic.Add_Find ct') _ = Applicable.Yes (Tactic.Add_Find' (ct', [(*filled later*)])) |
28 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*) |
28 (*Add_.. should reject (dsc //) (see fmz=[] in sqrt*) |
29 | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)])) |
29 | check (Tactic.Add_Given ct') _ = Applicable.Yes (Tactic.Add_Given' (ct', [(*filled later*)])) |
30 | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)])) |
30 | check (Tactic.Add_Relation ct') _ = Applicable.Yes (Tactic.Add_Relation' (ct', [(*filled later*)])) |
31 | check (Tactic.Apply_Method mI) (pt, (p, _)) = |
|
32 let |
|
33 val (dI, pI, probl, ctxt) = case Ctree.get_obj I pt p of |
|
34 Ctree.PblObj {origin = (_, (dI, pI, _), _), probl, ctxt, ...} => (dI, pI, probl, ctxt) |
|
35 | _ => raise ERROR "Specify_Step.check Apply_Method: uncovered case Ctree.get_obj" |
|
36 val {where_, ...} = Specify.get_pbt pI |
|
37 val pres = map (Model.mk_env probl |> subst_atomic) where_ |
|
38 val ctxt = if ContextC.is_empty ctxt (*vvvvvvvvvvvvvv DO THAT EARLIER?!?*) |
|
39 then ThyC.get_theory dI |> Proof_Context.init_global |> ContextC.insert_assumptions pres |
|
40 else ctxt |
|
41 in |
|
42 Applicable.Yes (Tactic.Apply_Method' (mI, NONE, Istate_Def.empty (*filled later*), ctxt)) |
|
43 end |
|
44 (*required for corner cases, e.g. test setup in inssort.sml*) |
31 (*required for corner cases, e.g. test setup in inssort.sml*) |
45 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct') |
32 | check (Tactic.Del_Find ct') _ = Applicable.Yes (Tactic.Del_Find' ct') |
46 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct') |
33 | check (Tactic.Del_Given ct') _ = Applicable.Yes (Tactic.Del_Given' ct') |
47 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct') |
34 | check (Tactic.Del_Relation ct') _ = Applicable.Yes (Tactic.Del_Relation' ct') |
48 | check Tactic.Model_Problem (pt, (p, _)) = |
35 | check Tactic.Model_Problem (pt, (p, _)) = |
98 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI) |
85 | check (Tactic.Specify_Theory dI)_ = Applicable.Yes (Tactic.Specify_Theory' dI) |
99 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" |
86 | check Tactic.Empty_Tac _ = Applicable.No "Empty_Tac is not applicable" |
100 | check tac (_, pos) = |
87 | check tac (_, pos) = |
101 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos); |
88 raise ERROR ("Specify_Step.check called for " ^ Tactic.input_to_string tac ^ " at" ^ Pos.pos'2str pos); |
102 |
89 |
|
90 fun generate1 (Tactic.Model_Problem' (_, itms, met)) (_, ctxt) (pt, pos as (p, _)) = |
|
91 let |
|
92 val pt = Ctree.update_pbl pt p itms |
|
93 val pt = Ctree.update_met pt p met |
|
94 in |
|
95 (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt) |
|
96 end |
|
97 | generate1 (Tactic.Add_Given' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = |
|
98 (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [][]), |
|
99 case p_ of |
|
100 Pos.Pbl => Ctree.update_pbl pt p itmlist |
|
101 | Pos.Met => Ctree.update_met pt p itmlist |
|
102 | _ => error ("uncovered case " ^ Pos.pos_2str p_)) |
|
103 (* WN110515 probably declare_constraints with input item (without dsc) -- |
|
104 -- important when specifying without formalisation *) |
|
105 | generate1 (Tactic.Add_Find' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = |
|
106 (pos, [], (Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] [])), |
|
107 case p_ of |
|
108 Pos.Pbl => Ctree.update_pbl pt p itmlist |
|
109 | Pos.Met => Ctree.update_met pt p itmlist |
|
110 | _ => error ("uncovered case " ^ Pos.pos_2str p_)) |
|
111 (*WN110515 probably declare_constraints with input item (without dsc)*) |
|
112 | generate1 (Tactic.Add_Relation' (_, itmlist)) (_, ctxt) (pt, pos as (p, p_)) = |
|
113 (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), |
|
114 case p_ of |
|
115 Pos.Pbl => Ctree.update_pbl pt p itmlist |
|
116 | Pos.Met => Ctree.update_met pt p itmlist |
|
117 | _ => error ("uncovered case " ^ Pos.pos_2str p_)) |
|
118 | generate1 (Tactic.Specify_Theory' domID) (_, ctxt) (pt, pos as (p,_)) = |
|
119 (pos, [] , Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), |
|
120 Ctree.update_domID pt p domID) |
|
121 | generate1 (Tactic.Specify_Problem' (pI, (_, (itms, _)))) (_, ctxt) (pt, (p, _)) = |
|
122 let |
|
123 val pt = Ctree.update_pbl pt p itms |
|
124 val pt = Ctree.update_pblID pt p pI |
|
125 in |
|
126 ((p, Pos.Pbl), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt) |
|
127 end |
|
128 | generate1 (Tactic.Specify_Method' (mID, oris, itms)) (_, ctxt) (pt, (p, _)) = |
|
129 let |
|
130 val pt = Ctree.update_oris pt p oris |
|
131 val pt = Ctree.update_met pt p itms |
|
132 val pt = Ctree.update_metID pt p mID |
|
133 in |
|
134 ((p, Pos.Met), [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt) |
|
135 end |
|
136 | generate1 (Tactic.Refine_Tacitly' (_, pIre, domID, metID, pbl)) (_, ctxt) (pt, pos as (p, _)) = |
|
137 let |
|
138 val pt = Ctree.update_pbl pt p pbl |
|
139 val pt = Ctree.update_orispec pt p (domID, pIre, metID) |
|
140 in |
|
141 (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt) |
|
142 end |
|
143 | generate1 (Tactic.Refine_Problem' (pI, _)) (_, ctxt) (pt, pos as (p, _)) = |
|
144 let |
|
145 val (dI, _, mI) = Ctree.get_obj Ctree.g_spec pt p |
|
146 val pt = Ctree.update_spec pt p (dI, pI, mI) |
|
147 in |
|
148 (pos, [], Generate.PpcKF (Generate.Upblmet, Specify.itms2itemppc (Proof_Context.theory_of ctxt) [] []), pt) |
|
149 end |
|
150 | generate1 (Tactic.Begin_Trans' t) l (pt, (p, Frm)) = |
|
151 let |
|
152 val (pt, c) = Ctree.cappend_form pt p l t |
|
153 val pt = Ctree.update_branch pt p Ctree.TransitiveB (*040312*) |
|
154 (* replace the old PrfOjb ~~~~~ *) |
|
155 val p = (Pos.lev_on o Pos.lev_dn (* starts with [...,0] *)) p |
|
156 val (pt, c') = Ctree.cappend_form pt p l t (*FIXME.0402 same istate ???*) |
|
157 in |
|
158 ((p, Frm), c @ c', Generate.FormKF (UnparseC.term t), pt) |
|
159 end |
|
160 | generate1 (Tactic.End_Trans' tasm) l (pt, (p, _)) = (* used at all ? *) |
|
161 let |
|
162 val p' = Pos.lev_up p |
|
163 val (pt, c) = Ctree.append_result pt p' l tasm Ctree.Complete |
|
164 in |
|
165 ((p', Pos.Res), c, Generate.FormKF "DUMMY" (*term2str t ..ERROR (t) has not been declared*), pt) |
|
166 end |
|
167 | generate1 m' _ (_, pos) = |
|
168 raise ERROR ("generate1: not impl.for " ^ Tactic.string_of m' ^ " at " ^ Pos.pos'2str pos) |
103 |
169 |
104 (**)end(**); |
170 (**)end(**); |