11 Matches of Problem.id * P_Model.T |
11 Matches of Problem.id * P_Model.T |
12 | NoMatch of Problem.id * P_Model.T |
12 | NoMatch of Problem.id * P_Model.T |
13 val matchs2str : T list -> string |
13 val matchs2str : T list -> string |
14 (*/------- rename: TODO 220917 review -------\*) |
14 (*/------- rename: TODO 220917 review -------\*) |
15 (*val o_model: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*) |
15 (*val o_model: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool*) |
16 val match_oris: theory -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool |
16 val match_oris: Proof.context -> Rule_Set.T -> O_Model.T -> Model_Pattern.T * term list -> bool |
17 (*unify ^^^^^^^^^^ vvvvvvvvvv |
17 (*unify ^^^^^^^^^^ vvvvvvvvvv |
18 vvvvvvvvv ^^^^^^^^^*) |
18 vvvvvvvvv ^^^^^^^^^*) |
19 (*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> |
19 (*val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list * Rule_Set.T -> |
20 bool * (I_Model.T * Pre_Conds.T)*) |
20 bool * (I_Model.T * Pre_Conds.T)*) |
21 val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list(*Pre_Cond.unchecked*) * Rule_Set.T -> |
21 val match_oris': theory -> O_Model.T -> Model_Pattern.T * term list(*Pre_Cond.unchecked*) * Rule_Set.T -> |
61 |
61 |
62 fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts)); |
62 fun ori2itmSup (i, v, _, d, ts) = (i, v, true, "#Given", I_Model.Sup (d, ts)); |
63 |
63 |
64 (* check an ori for matching a problemtype by description; |
64 (* check an ori for matching a problemtype by description; |
65 returns true only for itms found in pbt *) |
65 returns true only for itms found in pbt *) |
66 fun chk1_ (_: theory) pbt (i, vats, f, d, vs) = |
66 fun chk1_ pbt (i, vats, f, d, vs) = |
67 case find_first (eq1 d) pbt of |
67 case find_first (eq1 d) pbt of |
68 SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))] |
68 SOME (_, (_, id)) => [(i, vats, true, f, I_Model.Cor ((d, vs), (id, [Input_Descript.join'''' (d, vs)])))] |
69 | NONE => []; |
69 | NONE => []; |
70 |
70 |
71 (* elem 'p' of pbt contained in itms ? *) |
71 (* elem 'p' of pbt contained in itms ? *) |
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,where_) = |
84 fun match_oris ctxt 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_ 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, _(*where_'*)) = Pre_Conds.check where_rls where_ itms mvat; |
89 val (pb, _(*where_'*)) = Pre_Conds.check ctxt 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, where_, 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_ 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, where_') = Pre_Conds.check where_rls where_ itms mvat; |
100 val (pb, where_') = Pre_Conds.check (Proof_Context.init_global thy) where_rls where_ itms mvat; |
101 in (miss = [] andalso pb, (itms @ miss @ sups, where_')) 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 |
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, where_, where_rls) oris = |
115 fun match_itms_oris ctxt 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, where_') = Pre_Conds.check where_rls where_ itms' mv; |
131 val (pb, where_') = Pre_Conds.check ctxt where_rls where_ itms' mv; |
132 in (length mis = 0 andalso pb, (itms', where_')) 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 |