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