|
walther@59963
|
1 |
(* Title: Specify/pre-conds.sml
|
|
walther@59960
|
2 |
Author: Walther Neuper 110226
|
|
walther@59960
|
3 |
(c) due to copyright terms
|
|
walther@59960
|
4 |
|
|
walther@59960
|
5 |
Operations on models.
|
|
walther@59960
|
6 |
*)
|
|
walther@59960
|
7 |
|
|
walther@59960
|
8 |
signature PRE_CONDITIONS =
|
|
walther@59960
|
9 |
sig
|
|
walther@59963
|
10 |
type T
|
|
walther@59967
|
11 |
val to_string : T -> string
|
|
walther@59967
|
12 |
|
|
walther@60018
|
13 |
val check: Rule_Set.T -> term list -> I_Model.T -> 'a -> bool * (bool * term) list (**)
|
|
wenzelm@60223
|
14 |
\<^isac_test>\<open>
|
|
walther@59960
|
15 |
val eval: Rule_Set.T -> bool * term -> bool * term
|
|
wenzelm@60223
|
16 |
\<close>
|
|
walther@59960
|
17 |
end
|
|
walther@59960
|
18 |
|
|
walther@59965
|
19 |
(**)
|
|
walther@59960
|
20 |
structure Pre_Conds(**) : PRE_CONDITIONS(**) =
|
|
walther@59960
|
21 |
struct
|
|
walther@59965
|
22 |
(**)
|
|
walther@59960
|
23 |
|
|
walther@59963
|
24 |
type T = Pre_Conds_Def.T;
|
|
walther@59963
|
25 |
|
|
walther@59963
|
26 |
fun to_str (b, t) = pair2str (bool2str b, UnparseC.term t);
|
|
walther@59963
|
27 |
fun to_string pres = strs2str' (map (linefeed o to_str) pres);
|
|
walther@59960
|
28 |
|
|
walther@59960
|
29 |
(*NOT ALL Free's have been substituted*)
|
|
walther@59960
|
30 |
fun eval _ (false, pre) = (false, pre)
|
|
walther@59960
|
31 |
| eval prls (true, pre) =
|
|
walther@59960
|
32 |
if Rewrite.eval_true (ThyC.get_theory "Isac_Knowledge") [pre] prls
|
|
walther@59960
|
33 |
then (true , pre)
|
|
walther@59960
|
34 |
else (false , pre);
|
|
walther@59960
|
35 |
|
|
walther@60018
|
36 |
fun check _ [] _ _ = (true, [])
|
|
walther@59960
|
37 |
| check prls pres pbl (_ (* FIXME.WN0308 mvat re-introduce *)) =
|
|
walther@59960
|
38 |
let
|
|
walther@59960
|
39 |
val env = I_Model.mk_env pbl;
|
|
walther@59960
|
40 |
val pres' = map (TermC.subst_atomic_all env) pres;
|
|
walther@60018
|
41 |
val evals = map (eval prls) pres';
|
|
walther@60018
|
42 |
in (foldl and_ (true, map fst evals), evals) end;
|
|
walther@59965
|
43 |
|
|
walther@59965
|
44 |
(**)end(**)
|