1 (* Title: Specify/pre-conds.sml
2 Author: Walther Neuper 110226
3 (c) due to copyrigh,t terms
6 signature PRE_CONDITIONS =
18 val to_string : Proof.context -> T -> string
19 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term
21 val environment: Model_Pattern.T -> Model_Def.i_model -> Env.T
22 val make_environments: Model_Pattern.T -> Model_Def.i_model -> Env.T * (env_subst * env_eval)
23 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single) list ->
24 ((term * term) * (term * term)) list
26 val check_pos: Proof.context -> Rule_Set.T -> unchecked_pos ->
27 Model_Pattern.T * Model_Def.i_model -> checked_pos
28 val check_internal: Proof.context -> Model_Def.i_model -> (Pos.pos_ * References_Def.id)
30 val check_envs: Proof.context -> Rule_Set.T -> unchecked -> Env.T * (env_subst * env_eval)
32 val check: Proof.context -> Rule_Set.T -> unchecked ->
33 Model_Pattern.T * Model_Def.i_model -> checked
35 (*/----- from isac_test for Minisubpbl*)
36 val get_equal_descr: Model_Def.i_model -> Model_Pattern.single ->
37 (Model_Pattern.single * Model_Def.i_model_single) list
38 val unchecked_OLD_to: term list -> (term * Position.T) list
40 val all_lhs_atoms: term list -> bool
41 val handle_lists: term -> Model_Def.values -> Env.T
42 val filter_variants': Model_Def.i_model -> Model_Def.variant -> Model_Def.i_model
43 val switch_type: Model_Def.descriptor -> term list -> Model_Def.descriptor;
44 val discern_feedback: term -> Model_Def.i_model_feedback ->
45 ((term * term) * (term * term)) list
46 val discern_typ: term -> Model_Def.descriptor * term list ->
47 ((term * term) * (term * term)) list
49 val mk_env_model: term -> Model_Def.i_model_feedback -> Env.T
50 val make_env_model: (Model_Pattern.single * Model_Def.i_model_single) list -> Env.T
52 val get_values: Model_Def.i_model_feedback -> Model_Def.values
53 val get_descr_vnt: Model_Def.descriptor -> Model_Def.variants -> Model_Def.i_model ->
54 Model_Def.i_model_single
55 val get_descr_vnt': Model_Def.i_model_feedback -> Model_Def.variants -> O_Model.T ->
57 (*\----- from isac_test for Minisubpbl*)
65 structure Pre_Conds(**) : PRE_CONDITIONS(**) =
70 type T = Pre_Conds_Def.T; (*= (bool * term) list;*)
71 type unchecked = term list
72 type unchecked_pos = (term * Position.T) list
73 type checked = bool * (bool * term) list
74 type checked_pos = bool * ((bool * (term * Position.T)) list)
77 we have three kinds of Env.T in the specification-phase:
78 (*1*) Env.T produced by Pre_Conds.make_environments and required to create I_Model.T from
80 Env.T / (Constants, fixes) in Model_Pattern.T
81 e.g.[(fixes, [r = 7])] |
82 > (Constants, [<r = 7>]) in O/I_Model.T *)
84 (*2*) type env_subst = Env.T (* / 0 < fixes in Problem.{where_, ...}
87 (*3*) type env_eval = Env.T (* |
89 > 0 < 7 \<longrightarrow> true
91 (*1*) is required to produce (*2*) and (*3*); thus respective code is shifted to Pre_Conds.
92 (*2*) and (*3*) are produced from Pre_Conds.make_environments by restricting to "#Given".
94 There is a typing problem, probably to be solved by a language for Specification in the future:
95 term <fixes> in (*1*) has type "bool list"
96 term <fixes> in (*2*) has type "real". So for the transition from (*1*) to (*2..3*)
97 fun switch_type is required.
98 The transition requires better modelling by a novel language for Specification.
101 type input = TermC.as_string list;
106 fun to_str ctxt (b, t) = pair2str (bool2str b, UnparseC.term ctxt t);
107 fun to_string ctxt pres = strs2str' (map (linefeed o (to_str ctxt)) pres);
109 fun eval _ _ (false, where_) = (false, where_) (*NOT ALL Free's have been substituted*)
110 | eval ctxt where_rls (true, where_) =
111 if Rewrite.eval_true ctxt [where_] where_rls
113 else (false, where_);
116 (** find the maximal variant within an I_Model.T **)
118 fun get_equal_descr i_model (m_patt_single as (_, (descr, _))) =
121 filter (fn i_single => case get_descr_opt i_single of
123 | SOME descr' => descr' = descr) i_model
125 (map (pair m_patt_single) equal_descr)
128 fun get_values (Cor (_, values)) = values
129 | get_values (Syn _) = raise ERROR "Pre_Conds.get_values not for Syn"
130 | get_values (Inc (_, values)) = values
131 | get_values (Sup (_, values)) = values
134 get an appropriate (description, variant)-item from i_model, otherwise return empty item,
135 i.e. this function produces items with Sup.
137 fun get_descr_vnt descr vnts i_model =
139 val equal_descr = filter (fn (_, _, _, _, (feedb, _)) => case get_dscr_opt feedb of NONE => false
140 | SOME descr' => if descr = descr' then true else false) i_model
142 case filter (fn (_, vnts', _, _, _) => inter op= vnts' vnts <> []) equal_descr of
143 [] => (0, [], false, "i_model_empty", (Sup (descr, []), Position.none))
144 | items => Library.the_single items (*only applied to model_patt, which has each descr once*)
147 get an appropriate (description, variant) item from o_model;
148 called in case of item in met_imod is_empty_single
149 (i.e. was not transferred pbl_mod by \<open>fun get_descr_vnt\<close>).
151 fun get_descr_vnt' feedb vnts o_model =
152 filter (fn (_, vnts', _, descr', _) =>
153 case get_dscr_opt feedb of
154 SOME descr => if descr' = descr andalso inter op= vnts' vnts <> [] then true else false
155 | NONE => false) o_model
157 (* all_lhs_atoms: term list -> bool*)
158 fun all_lhs_atoms ts = fold (curry and_) (map (fn t =>
159 if can TermC.lhs t andalso not (TermC.is_num (TermC.lhs t))
160 then TermC.is_atom (TermC.lhs t)
163 fun handle_lists id values = [(id, values_to_present values)]
165 fun mk_env_model _ (Model_Def.Cor (_, [])) = []
166 | mk_env_model id (Model_Def.Cor (_, ts)) = handle_lists id ts
167 | mk_env_model _ (Model_Def.Syn _) = [] (*TODO handle correct list elements*)
168 | mk_env_model _ (Model_Def.Inc (_, [])) = []
169 | mk_env_model id (Model_Def.Inc (_, ts)) = handle_lists id ts
170 | mk_env_model _ (Model_Def.Sup _) = []
171 fun make_env_model equal_descr_pairs =
172 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _)))
173 => (mk_env_model id feedb)) equal_descr_pairs
176 fun switch_type descr [] = descr
177 | switch_type (Free (id_string, _)) ts =
178 Free (id_string, ts |> hd |> TermC.lhs |> type_of)
179 | switch_type descr _ = raise ERROR ("switch_type undefined argument " ^
180 quote (UnparseC.term (ContextC.for_ERROR ()) descr))
182 fun discern_typ _ (_, []) = []
183 | discern_typ id (descr, ts) =
184 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
186 val ts = if Model_Def.is_list_descr descr
187 then if TermC.is_list (hd ts)
188 then ts |> map TermC.isalist2list |> flat
192 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
193 if Model_Pattern.typ_of_element descr = HOLogic.boolT andalso all_lhs_atoms ts
196 then (writeln "model items of type 'bool' in lists with 'lengt ts > 1' NOT YET IMPLEMENTED";
198 else [((switch_type id ts, TermC.lhs (hd ts)),
199 (TermC.lhs (hd ts), TermC.rhs (hd ts)))]
201 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------\*)
203 (*TODO.md "review (descriptor, ts)" REMOVE--------------------------------------/*)
206 fun discern_feedback id (Model_Def.Cor (descr, ts)) = discern_typ id (descr, ts)
207 | discern_feedback _ (Model_Def.Syn _) = [] (*TODO: handle correct elements*)
208 | discern_feedback id (Model_Def.Inc (descr, ts)) = discern_typ id (descr, ts)
209 | discern_feedback _ (Model_Def.Sup _) = []
210 fun make_envs_preconds equal_givens =
211 map (fn ((_, (_, id)), (_, _, _, _, (feedb, _))) => discern_feedback id feedb) equal_givens
214 fun make_environments model_patt i_model =
216 val equal_descr_pairs = map (get_equal_descr i_model) model_patt
218 val env_model = make_env_model equal_descr_pairs
219 val equal_givens = filter (fn ((m_field, _), _) => m_field = "#Given") equal_descr_pairs
220 val subst_eval_list = make_envs_preconds equal_givens
221 val (env_subst, env_eval) = split_list subst_eval_list
223 (env_model, (env_subst, env_eval))
226 fun check_internal ctxt i_model (pbl_met, id) =
228 val (model, where_rls, where_) = case pbl_met of
229 Pos.Pbl => let val {model, where_rls, where_, ...} = Problem.from_store ctxt id
230 in (model, where_rls, where_) end
231 | Pos.Met => let val {model, where_rls, where_, ...} = MethodC.from_store ctxt id
232 in (model, where_rls, where_) end
233 | _ => raise ERROR ("Pre_Conds.check_internal calles with " ^ Pos.pos_2str pbl_met)
234 val (env_model, (env_subst, env_eval)) = make_environments model
235 ((*filter (fn (_, _, _, m_field ,_) => m_field = "#Given")*) i_model)
237 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
238 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
239 val full_subst = if env_eval = [] then pres_subst_other
240 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
241 val evals = map (eval ctxt where_rls) full_subst
243 (foldl and_ (true, map fst evals), pres_subst_other)
246 (*extract one environment rom make_environments *)
247 fun environment model_patt i_model = make_environments model_patt i_model |> #1
249 (** check pre-conditions **)
250 fun check_pos ctxt where_rls where_ (model_patt, i_model) =
252 val (_, (_, env_eval)) = make_environments model_patt
253 (filter (fn (_, _, _, m_field ,_) => m_field = "#Given") i_model)
254 val full_subst = if env_eval = []
255 then map (fn (t, pos) => ((true, t), pos)) where_
256 else map (fn (t, pos) => (TermC.subst_atomic_all env_eval t, pos)) where_
257 val evals = map (fn ((bool_t), pos) => (eval ctxt where_rls bool_t, pos)) full_subst;
258 val display = map (fn ((t, pos), ((bool, _), _)) => (bool, (t, pos))) (where_ ~~ evals)
260 (foldl and_ (true, map (fn ((bool, _: term), _: Position.T) => bool) evals), display)
263 (*takes the envs resulting from make_environments*)
264 fun check_envs ctxt where_rls where_ (env_model, (env_subst, env_eval)) =
266 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
267 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
268 val full_subst = if env_eval = [] then pres_subst_other
269 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
270 val evals = map (eval ctxt where_rls) full_subst
272 (foldl and_ (true, map fst evals), pres_subst_other)
275 (*expects the precondition from Problem, ie. needs substitution by env_model*)
276 fun check _ _ [] _ = (true, [])
277 | check ctxt where_rls where_ (model_patt, i_model) =
279 val (env_model, (env_subst, env_eval)) = make_environments model_patt i_model
280 val pres_subst = map (TermC.subst_atomic_all env_subst) where_;
281 val pres_subst_other = map (TermC.subst_atomic_all env_model) (map #2 pres_subst);
282 val full_subst = if env_eval = [] then pres_subst_other
283 else map (TermC.subst_atomic_all env_eval) (map #2 pres_subst_other)
284 val evals = map (eval ctxt where_rls) full_subst
286 (foldl and_ (true, map fst evals), pres_subst_other)
289 fun unchecked_OLD_to pres = map (fn t => (t, Position.none)) pres