1 (* Title: Specify/model.sml
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
11 Matches of Problem.id * P_Model.T
12 | NoMatch of Problem.id * P_Model.T
13 val matchs2str : match 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)
23 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
24 datatype match' = Matches' of P_Model.T | NoMatch' of P_Model.T
25 val match_pbl : Formalise.model -> Problem.T -> match'
26 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
28 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
32 structure Model(** ) : MODEL( **) =
37 Matches of Problem.id * P_Model.T
38 | NoMatch of Problem.id * P_Model.T;
39 fun match2str (Matches (pI, ppc)) = "Matches (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")"
40 | match2str (NoMatch (pI, ppc)) = "NoMatch (" ^ strs2str pI ^ ", " ^ P_Model.to_string ppc ^ ")";
41 fun matchs2str ms = (strs2str o (map match2str)) ms;
44 fun field_eq f (_, _, f', _, _) = f = f';
46 fun eq2' (_, (d, _)) (_, _, _, d', _) = d = d';
47 fun eq2 (_, (d, _)) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
48 fun eq1 d (_, (d', _)) = (d = d');
50 fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts));
52 (* check an ori for matching a problemtype by description;
53 returns true only for itms found in pbt *)
54 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) =
55 case find_first (eq1 d) pbt of
56 SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, I_Model.pbl_ids' d vs)))]
59 (* elem 'p' of pbt contained in itms ? *)
60 fun chk1_m itms p = case find_first (eq2 p) itms of SOME _ => true | NONE => false;
61 fun chk1_m' oris (p as (f, (d, t))) =
62 case find_first (eq2' p) oris of
64 | NONE => [(f, I_Model.Mis (d, t))];
65 fun pair0vatsfalse (f, itm_) = (0, [], false, f, itm_);
67 fun chk1_mis _(*mvat*) itms ppc = foldl and_ (true, map (chk1_m itms) ppc);
68 fun chk1_mis' oris ppc = map pair0vatsfalse ((flat o (map (chk1_m' oris))) ppc);
70 (* check a problem (ie. ori list) for matching a problemtype,
71 takes the I_Model.vars_of for concluding completeness (FIXME could be another!) *)
72 fun match_oris thy prls oris (pbt,pre) =
74 val itms = (flat o (map (chk1_ thy pbt))) oris;
75 val mvat = I_Model.vars_of itms;
76 val complete = chk1_mis mvat itms pbt;
77 val pre' = Pre_Conds.check prls pre itms mvat;
78 val pb = foldl and_ (true, map fst pre');
79 in if complete andalso pb then true else false end;
81 (* check a problem (ie. ori list) for matching a problemtype,
82 returns items for output to math-experts *)
83 fun match_oris' thy oris (ppc, pre, prls) =
85 val itms = (flat o (map (chk1_ thy ppc))) oris;
86 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris;
87 val mvat = I_Model.vars_of itms;
88 val miss = chk1_mis' oris ppc;
89 val pre' = Pre_Conds.check prls pre itms mvat;
90 val pb = foldl and_ (true, map fst pre');
91 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end;
94 (** check a problem (ie. itm list) for matching a problemtype **)
96 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt,
97 for missing items get data from formalization (ie. ori list);
98 takes the I_Model.vars_of for concluding completeness (could be another!)
100 (0) determine the most frequent variant mv in pbl
101 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) =>
102 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news;
103 (3) newitms = filter (mv mem vat(news)) news
105 fun match_itms_oris (_: theory) pbl (pbt, pre, prls) oris =
107 (*0*)val mv = I_Model.max_vt pbl;
109 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.d_in itm_;
110 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
111 SOME _ => false | NONE => true;
112 (*1*)val mis = (filter (notmem pbl)) pbt;
114 fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
115 fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
116 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
117 val news = (flat o (map (oris2itms oris))) mis;
118 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
119 val newitms = filter mem_vat news;
120 (*4*)val itms' = pbl @ newitms;
121 val pre' = Pre_Conds.check prls pre itms' mv;
122 val pb = foldl and_ (true, map fst pre');
123 in (length mis = 0 andalso pb, (itms', pre')) end;
126 (** for use by math-authors **)
128 datatype match' = (* for the user *)
129 Matches' of P_Model.T
130 | NoMatch' of P_Model.T;
132 (* match a formalization with a problem type, for tests *)
133 fun match_pbl fmz ({thy = thy, where_ = pre, ppc, prls = er, ...}: Problem.T) =
135 val oris = O_Model.init fmz thy ppc(* |> #1*);
136 val (bool, (itms, pre')) = match_oris' thy oris (ppc, pre, er);
139 then Matches' (P_Model.from thy itms pre')
140 else NoMatch' (P_Model.from thy itms pre')