walther@59960
|
1 |
(* Title: Specify/model.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@59984
|
8 |
signature MODEL_MATCH =
|
walther@59960
|
9 |
sig
|
walther@60010
|
10 |
datatype T = (* ------------vvvvvvvvv--- adapt to PIDE *)
|
walther@59969
|
11 |
Matches of Problem.id * P_Model.T
|
walther@59971
|
12 |
| NoMatch of Problem.id * P_Model.T
|
walther@59984
|
13 |
val matchs2str : T list -> string
|
walther@60010
|
14 |
(*/------- rename -------\*)
|
walther@60010
|
15 |
(*val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*)
|
walther@59971
|
16 |
val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool
|
walther@59971
|
17 |
(*unify ^^^^^^^^^^ vvvvvvvvvv
|
walther@59971
|
18 |
vvvvvvvvv ^^^^^^^^^*)
|
walther@60010
|
19 |
(*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
|
walther@60010
|
20 |
bool * (I_Model.T * Pre_Conds.T)*)
|
walther@59971
|
21 |
val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
|
walther@60010
|
22 |
bool * (I_Model.T * Pre_Conds.T) (*^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v^v--- type*)
|
walther@60010
|
23 |
(*val o_i_model: O_Model.T * I_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> theory ->
|
walther@60010
|
24 |
bool * (I_Model.T * Pre_Conds.T) (*?values--^^^^^^^^^?*)*)
|
walther@60010
|
25 |
val match_itms_oris: theory -> I_Model.T -> Model_Pattern.T * term list * Rule_Set.T ->
|
walther@59971
|
26 |
O_Model.T -> bool * (I_Model.T * Pre_Conds.T)
|
walther@59987
|
27 |
|
walther@60010
|
28 |
(*val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T*)
|
walther@59996
|
29 |
val arguments: theory -> Model_Pattern.T -> term list -> O_Model.T
|
walther@60010
|
30 |
(*val arguments_msg: Problem.id -> term -> term list -> unit*)
|
walther@59987
|
31 |
val arguments_msg: Problem.id -> term -> term list -> unit
|
walther@59968
|
32 |
|
walther@60251
|
33 |
datatype match' = (* constructors for tests only *)
|
walther@60251
|
34 |
Matches' of P_Model.T | NoMatch' of P_Model.T
|
walther@59971
|
35 |
val match_pbl : Formalise.model -> Problem.T -> match'
|
wenzelm@60223
|
36 |
\<^isac_test>\<open>
|
walther@60010
|
37 |
(*val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T*)
|
walther@60010
|
38 |
val matc: theory -> Model_Pattern.T -> term list -> O_Model.T -> O_Model.T
|
wenzelm@60223
|
39 |
\<close>
|
walther@59987
|
40 |
(*\------- rename -------/*)
|
walther@59960
|
41 |
end
|
walther@59960
|
42 |
|
walther@59968
|
43 |
(**)
|
walther@59997
|
44 |
structure M_Match(** ) : MODEL_MATCH( **) =
|
walther@59960
|
45 |
struct
|
walther@59968
|
46 |
(**)
|
walther@59960
|
47 |
|
walther@59984
|
48 |
datatype T =
|
walther@59969
|
49 |
Matches of Problem.id * P_Model.T
|
walther@59969
|
50 |
| NoMatch of Problem.id * P_Model.T;
|
walther@59969
|
51 |
fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
|
walther@59969
|
52 |
| match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
|
walther@59965
|
53 |
fun matchs2str ms = (strs2str o (map match2str)) ms;
|
walther@59965
|
54 |
|
walther@59968
|
55 |
|
walther@59968
|
56 |
fun field_eq f (_, _, f', _, _) = f = f';
|
walther@59968
|
57 |
|
walther@59968
|
58 |
fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
|
walther@59968
|
59 |
fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
|
walther@59968
|
60 |
fun eq1 d (_, (d', _)) = (d = d');
|
walther@59968
|
61 |
|
walther@59968
|
62 |
fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
|
walther@59968
|
63 |
|
walther@59968
|
64 |
(* check an ori for matching a problemtype by description;
|
walther@59968
|
65 |
returns true only for itms found in pbt *)
|
walther@59968
|
66 |
fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
|
walther@59968
|
67 |
case find_first (eq1 d) pbt of
|
walther@59968
|
68 |
SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
|
walther@59968
|
69 |
| NONE => [];
|
walther@59968
|
70 |
|
walther@59968
|
71 |
(* elem 'p' of pbt contained in itms ? *)
|
walther@59968
|
72 |
fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
|
walther@59968
|
73 |
fun chk1_m' oris (p as (f, (d, t))) =
|
walther@59968
|
74 |
case find_first (eq2' p) oris of
|
walther@59968
|
75 |
SOME _ => []
|
walther@59968
|
76 |
| NONE => [(f, I_Model.Mis (d, t))];
|
walther@59968
|
77 |
fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
|
walther@59968
|
78 |
|
walther@59968
|
79 |
fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
|
walther@59968
|
80 |
fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
|
walther@59968
|
81 |
|
walther@59968
|
82 |
(* check a problem (ie. ori list) for matching a problemtype,
|
walther@59968
|
83 |
takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
|
walther@59968
|
84 |
fun match_oris thy prls oris (pbt,pre) =
|
walther@59968
|
85 |
let
|
walther@59968
|
86 |
val itms = (flat o (map (chk1_ thy pbt))) oris;
|
walther@59968
|
87 |
val mvat = I_Model.vars_of itms;
|
walther@59968
|
88 |
val complete = chk1_mis mvat itms pbt;
|
walther@60018
|
89 |
val (pb, pre') = Pre_Conds.check prls pre itms mvat;
|
walther@59968
|
90 |
in if complete andalso pb then true else false end;
|
walther@59968
|
91 |
|
walther@59968
|
92 |
(* check a problem (ie. ori list) for matching a problemtype,
|
walther@59968
|
93 |
returns items for output to math-experts *)
|
walther@59971
|
94 |
fun match_oris' thy oris (ppc, pre, prls) =
|
walther@59968
|
95 |
let
|
walther@59968
|
96 |
val itms = (flat o (map (chk1_ thy ppc))) oris;
|
walther@59968
|
97 |
val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
|
walther@59968
|
98 |
val mvat = I_Model.vars_of itms;
|
walther@59968
|
99 |
val miss = chk1_mis' oris ppc;
|
walther@60018
|
100 |
val (pb, pre') = Pre_Conds.check prls pre itms mvat;
|
walther@59968
|
101 |
in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
|
walther@59968
|
102 |
|
walther@59971
|
103 |
|
walther@59971
|
104 |
(** check a problem (ie. itm list) for matching a problemtype **)
|
walther@59971
|
105 |
|
walther@59971
|
106 |
(* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
|
walther@59971
|
107 |
for missing items get data from formalization (ie. ori list);
|
walther@59971
|
108 |
takes the I_Model.vars_of for concluding completeness (could be another!)
|
walther@59971
|
109 |
|
walther@59971
|
110 |
(0) determine the most frequent variant mv in pbl
|
walther@59971
|
111 |
ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
|
walther@59971
|
112 |
(2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
|
walther@59971
|
113 |
(3) newitms = filter (mv mem vat(news)) news
|
walther@59971
|
114 |
(4) pbt @ newitms *)
|
walther@59971
|
115 |
fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
|
walther@59971
|
116 |
let
|
walther@59971
|
117 |
(*0*)val mv = I_Model.max_vt pbl;
|
walther@59971
|
118 |
|
walther@59971
|
119 |
fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
|
walther@59971
|
120 |
fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
|
walther@59971
|
121 |
SOME _ => false | NONE => true;
|
walther@59971
|
122 |
(*1*)val mis = (filter (notmem pbl)) pbt;
|
walther@59971
|
123 |
|
walther@59971
|
124 |
fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
|
walther@59971
|
125 |
fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
|
walther@59971
|
126 |
(*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
|
walther@59971
|
127 |
val news = (flat o (map (oris2itms oris))) mis;
|
walther@59971
|
128 |
(*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
|
walther@59971
|
129 |
val newitms = filter mem_vat news;
|
walther@59971
|
130 |
(*4*)val itms' = pbl @ newitms;
|
walther@60018
|
131 |
val (pb, pre') = Pre_Conds.check prls pre itms' mv;
|
walther@59971
|
132 |
in (length mis = 0 andalso pb, (itms', pre')) end;
|
walther@59971
|
133 |
|
walther@59971
|
134 |
|
walther@59971
|
135 |
(** for use by math-authors **)
|
walther@59971
|
136 |
|
walther@59971
|
137 |
datatype match' = (* for the user *)
|
walther@59971
|
138 |
Matches' of P_Model.T
|
walther@59971
|
139 |
| NoMatch' of P_Model.T;
|
walther@59971
|
140 |
|
walther@59971
|
141 |
(* match a formalization with a problem type, for tests *)
|
walther@59971
|
142 |
fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
|
walther@59971
|
143 |
let
|
walther@59971
|
144 |
val oris = O_Model.init fmz thy ppc(* |> #1*);
|
walther@59971
|
145 |
val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
|
walther@59971
|
146 |
in
|
walther@59971
|
147 |
if bool
|
walther@59971
|
148 |
then Matches' (P_Model.from thy itms pre')
|
walther@59971
|
149 |
else NoMatch' (P_Model.from thy itms pre')
|
walther@59971
|
150 |
end;
|
walther@59971
|
151 |
|
walther@59987
|
152 |
(* split type-wrapper from scr-arg and build part of an ori;
|
walther@59987
|
153 |
an type-error is reported immediately, raises an exn,
|
walther@59987
|
154 |
subsequent handling of exn provides 2nd part of error message *)
|
walther@59987
|
155 |
fun mtc thy (str, (dsc, _)) (ty $ var) =
|
walther@59987
|
156 |
((Thm.global_cterm_of thy (dsc $ var);(*type check*)
|
walther@59987
|
157 |
SOME (([1], str, dsc, (*[var]*)
|
walther@59987
|
158 |
Input_Descript.split' (dsc, var))) (*:ori without leading #*))
|
walther@59987
|
159 |
handle e as TYPE _ =>
|
walther@59987
|
160 |
(tracing (dashs 70 ^ "\n"
|
walther@59987
|
161 |
^ "*** ERROR while creating the items for the model of the ->problem\n"
|
walther@59987
|
162 |
^ "*** from the ->stac with ->typeconstructor in arglist:\n"
|
walther@59987
|
163 |
^ "*** item (->description ->value): " ^ UnparseC.term dsc ^ " " ^ UnparseC.term var ^ "\n"
|
walther@59987
|
164 |
^ "*** description: " ^ TermC.term_detail2str dsc
|
walther@59987
|
165 |
^ "*** value: " ^ TermC.term_detail2str var
|
walther@59987
|
166 |
^ "*** typeconstructor in script: " ^ TermC.term_detail2str ty
|
walther@59987
|
167 |
^ "*** checked by theory: " ^ Context.theory_name thy ^ "\n"
|
walther@59987
|
168 |
^ "*** " ^ dots 66);
|
walther@59987
|
169 |
writeln (@{make_string} e);
|
walther@59987
|
170 |
Exn.reraise e; (*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
|
walther@59987
|
171 |
NONE))
|
walther@59987
|
172 |
| mtc _ _ t = raise ERROR ("mtc: uncovered case with" ^ UnparseC.term t)
|
walther@59987
|
173 |
|
walther@59987
|
174 |
(* match each pat of the model-pattern with an actual argument;
|
walther@59987
|
175 |
precondition: copy-named vars are filtered out *)
|
walther@59987
|
176 |
fun matc _ [] _ oris = oris
|
walther@59987
|
177 |
| matc _ pbt [] _ =
|
walther@59987
|
178 |
(tracing (dashs 70);
|
walther@59987
|
179 |
raise ERROR ("actual arg(s) missing for '" ^ Model_Pattern.to_string pbt ^ "' i.e. should be 'copy-named' by '*_._'"))
|
walther@59987
|
180 |
| matc thy ((p as (_, (_, t))) :: pbt) (a :: ags) oris =
|
walther@59987
|
181 |
(*del?..*)if (O_Model.is_copy_named_idstr o TermC.free2str) t then oris
|
walther@59987
|
182 |
else(*..del?*)
|
walther@59987
|
183 |
let val opt = mtc thy p a
|
walther@59987
|
184 |
in
|
walther@59987
|
185 |
case opt of
|
walther@59987
|
186 |
SOME ori => matc thy pbt ags (oris @ [ori])
|
walther@59987
|
187 |
| NONE => [](*WN050903 skipped by exn handled in arguments*)
|
walther@59987
|
188 |
end
|
walther@59987
|
189 |
|
walther@59987
|
190 |
(* match the actual arguments of a SubProblem with a model-pattern
|
walther@59987
|
191 |
and create an ori list (in root-pbl created from formalization).
|
walther@59987
|
192 |
expects ags:pats = 1:1, while copy-named are filtered out of pats;
|
walther@59987
|
193 |
if no 1:1 then exn raised by matc/mtc and handled at call.
|
walther@60152
|
194 |
copy-named pats are appended in order to get them into the Model-items *)
|
walther@59987
|
195 |
fun arguments thy pbt ags =
|
walther@59987
|
196 |
let
|
walther@59987
|
197 |
fun flattup (i, (var, bool, str, itm_)) = (i, var, bool, str, itm_)
|
walther@59987
|
198 |
val pbt' = filter_out O_Model.is_copy_named pbt
|
walther@59987
|
199 |
val cy = filter O_Model.is_copy_named pbt (* cy is NOT a (formal) argument, but the fun's result *)
|
walther@59987
|
200 |
val oris' = matc thy pbt' ags []
|
walther@59987
|
201 |
val cy' = map (O_Model.cpy_nam pbt' oris') cy
|
walther@60152
|
202 |
val ors = O_Model.add_id (oris' @ cy') (*...appended in order to get into the Model-items *)
|
walther@59987
|
203 |
in (map flattup ors) end
|
walther@59987
|
204 |
|
walther@59987
|
205 |
(* report part of the error-msg which is not available in match_args *)
|
walther@59987
|
206 |
fun arguments_msg pI stac ags =
|
walther@59987
|
207 |
let
|
walther@59987
|
208 |
val pats = (#ppc o Problem.from_store) pI
|
walther@59987
|
209 |
val msg = (dots 70 ^ "\n"
|
walther@59987
|
210 |
^ "*** problem " ^ strs2str pI ^ " has the ...\n"
|
walther@59987
|
211 |
^ "*** model-pattern " ^ Model_Pattern.to_string pats ^ "\n"
|
walther@59987
|
212 |
^ "*** stac '" ^ UnparseC.term stac ^ "' has the ...\n"
|
walther@59987
|
213 |
^ "*** arg-list " ^ UnparseC.terms ags ^ "\n"
|
walther@59987
|
214 |
^ dashs 70)
|
walther@59987
|
215 |
(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
|
walther@59987
|
216 |
in tracing msg end
|
walther@59987
|
217 |
|
walther@59968
|
218 |
(**)end(**)
|