79 fun chk1_mis _(*mvat*) itms model = foldl and_ (true, map (chk1_m itms) model); |
79 fun chk1_mis _(*mvat*) itms model = foldl and_ (true, map (chk1_m itms) model); |
80 fun chk1_mis' oris model = map pair0vatsfalse ((flat o (map (chk1_m' oris))) model); |
80 fun chk1_mis' oris model = map pair0vatsfalse ((flat o (map (chk1_m' oris))) model); |
81 |
81 |
82 (* check a problem (ie. ori list) for matching a problemtype, |
82 (* check a problem (ie. ori list) for matching a problemtype, |
83 takes the I_Model.variables for concluding completeness (FIXME could be another!) *) |
83 takes the I_Model.variables for concluding completeness (FIXME could be another!) *) |
84 fun match_oris thy where_rls oris (pbt,pre) = |
84 fun match_oris thy where_rls oris (pbt,where_) = |
85 let |
85 let |
86 val itms = (flat o (map (chk1_ thy pbt))) oris; |
86 val itms = (flat o (map (chk1_ thy pbt))) oris; |
87 val mvat = I_Model.variables itms; |
87 val mvat = I_Model.variables itms; |
88 val complete = chk1_mis mvat itms pbt; |
88 val complete = chk1_mis mvat itms pbt; |
89 val (pb, _(*pre'*)) = Pre_Conds.check where_rls pre itms mvat; |
89 val (pb, _(*where_'*)) = Pre_Conds.check where_rls where_ itms mvat; |
90 in if complete andalso pb then true else false end; |
90 in if complete andalso pb then true else false end; |
91 |
91 |
92 (* check a problem (ie. ori list) for matching a problemtype, |
92 (* check a problem (ie. ori list) for matching a problemtype, |
93 returns items for output to math-experts *) |
93 returns items for output to math-experts *) |
94 fun match_oris' thy oris (model, pre, where_rls) = |
94 fun match_oris' thy oris (model, where_, where_rls) = |
95 let |
95 let |
96 val itms = (flat o (map (chk1_ thy model))) oris; |
96 val itms = (flat o (map (chk1_ thy model))) oris; |
97 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris; |
97 val sups = ((map ori2itmSup) o (filter (field_eq "#undef"))) oris; |
98 val mvat = I_Model.variables itms; |
98 val mvat = I_Model.variables itms; |
99 val miss = chk1_mis' oris model; |
99 val miss = chk1_mis' oris model; |
100 val (pb, pre') = Pre_Conds.check where_rls pre itms mvat; |
100 val (pb, where_') = Pre_Conds.check where_rls where_ itms mvat; |
101 in (miss = [] andalso pb, (itms @ miss @ sups, pre')) end; |
101 in (miss = [] andalso pb, (itms @ miss @ sups, where_')) end; |
102 |
102 |
103 |
103 |
104 (** check a problem (ie. itm list) for matching a problemtype **) |
104 (** check a problem (ie. itm list) for matching a problemtype **) |
105 |
105 |
106 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt, |
106 (* check a problem (or method) pbl (ie. itm list) for matching a problemtype pbt, |
110 (0) determine the most frequent variant mv in pbl |
110 (0) determine the most frequent variant mv in pbl |
111 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => |
111 ALL pbt. (1) dsc(pbt) notmem dsc(pbls) => |
112 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; |
112 (2) filter (dsc(pbt) = dsc(oris)) oris; -> news; |
113 (3) newitms = filter (mv mem vat(news)) news |
113 (3) newitms = filter (mv mem vat(news)) news |
114 (4) pbt @ newitms *) |
114 (4) pbt @ newitms *) |
115 fun match_itms_oris (_: theory) pbl (pbt, pre, where_rls) oris = |
115 fun match_itms_oris (_: theory) pbl (pbt, where_, where_rls) oris = |
116 let |
116 let |
117 (*0*)val mv = I_Model.max_variant pbl; |
117 (*0*)val mv = I_Model.max_variant pbl; |
118 |
118 |
119 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; |
119 fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_; |
120 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of |
120 fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of |
126 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; |
126 (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris; |
127 val news = (flat o (map (oris2itms oris))) mis; |
127 val news = (flat o (map (oris2itms oris))) mis; |
128 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv; |
128 (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv; |
129 val newitms = filter mem_vat news; |
129 val newitms = filter mem_vat news; |
130 (*4*)val itms' = pbl @ newitms; |
130 (*4*)val itms' = pbl @ newitms; |
131 val (pb, pre') = Pre_Conds.check where_rls pre itms' mv; |
131 val (pb, where_') = Pre_Conds.check where_rls where_ itms' mv; |
132 in (length mis = 0 andalso pb, (itms', pre')) end; |
132 in (length mis = 0 andalso pb, (itms', where_')) end; |
133 |
133 |
134 |
134 |
135 (** for use by math-authors **) |
135 (** for use by math-authors **) |
136 |
136 |
137 datatype match' = (* for the user *) |
137 datatype match' = (* for the user *) |
138 Matches' of P_Model.T |
138 Matches' of P_Model.T |
139 | NoMatch' of P_Model.T; |
139 | NoMatch' of P_Model.T; |
140 |
140 |
141 (* match a formalization with a problem type, for tests *) |
141 (* match a formalization with a problem type, for tests *) |
142 fun match_pbl fmz ({thy = thy, where_ = pre, model, where_rls = er, ...}: Problem.T) = |
142 fun match_pbl fmz ({thy = thy, where_ = where_, model, where_rls = er, ...}: Problem.T) = |
143 let |
143 let |
144 val oris = O_Model.init thy fmz model(* |> #1*); |
144 val oris = O_Model.init thy fmz model(* |> #1*); |
145 val (bool, (itms, pre')) = match_oris' thy oris (model, pre, er); |
145 val (bool, (itms, where_')) = match_oris' thy oris (model, where_, er); |
146 in |
146 in |
147 if bool |
147 if bool |
148 then Matches' (P_Model.from thy itms pre') |
148 then Matches' (P_Model.from thy itms where_') |
149 else NoMatch' (P_Model.from thy itms pre') |
149 else NoMatch' (P_Model.from thy itms where_') |
150 end; |
150 end; |
151 |
151 |
152 (* split type-wrapper from scr-arg and build part of an ori; |
152 (* split type-wrapper from program-arg and build part of an ori; |
153 an type-error is reported immediately, raises an exn, |
153 an type-error is reported immediately, raises an exn, |
154 subsequent handling of exn provides 2nd part of error message *) |
154 subsequent handling of exn provides 2nd part of error message *) |
155 fun mtc thy (str, (dsc, _)) (ty $ var) = |
155 fun mtc thy (str, (dsc, _)) (ty $ var) = |
156 ((Thm.global_cterm_of thy (dsc $ var);(*type check*) |
156 ((Thm.global_cterm_of thy (dsc $ var);(*type check*) |
157 SOME (([1], str, dsc, (*[var]*) |
157 SOME (([1], str, dsc, (*[var]*) |