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