32 |
37 |
33 type id = Meth_Def.id; |
38 type id = Meth_Def.id; |
34 val id_empty = Meth_Def.id_empty; |
39 val id_empty = Meth_Def.id_empty; |
35 val id_to_string = Meth_Def.id_to_string; |
40 val id_to_string = Meth_Def.id_to_string; |
36 |
41 |
|
42 |
|
43 (** prepare Method for Store **) |
|
44 |
|
45 (* a subset of Method.T record's fields *) |
|
46 type input = |
|
47 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T, |
|
48 prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T} |
|
49 |
|
50 fun prep_input thy guh maa init |
|
51 (metID, ppc, |
|
52 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr, |
|
53 errpats = ep, nrls = nr}, scr) = |
|
54 let |
|
55 fun eq f (f', _) = f = f'; |
|
56 val gi = filter (eq "#Given") ppc; |
|
57 val gi = (case gi of |
|
58 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); []) |
|
59 | ((_, gi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi' |
|
60 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID)) |
|
61 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID)); |
|
62 val gi = map (pair "#Given") gi; |
|
63 |
|
64 val fi = filter (eq "#Find") ppc; |
|
65 val fi = (case fi of |
|
66 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); []) |
|
67 | ((_, fi') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi' |
|
68 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID)) |
|
69 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID)); |
|
70 val fi = map (pair "#Find") fi; |
|
71 |
|
72 val re = filter (eq "#Relate") ppc; |
|
73 val re = (case re of |
|
74 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); []) |
|
75 | ((_,re') :: []) => (map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re' |
|
76 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID)) |
|
77 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID)); |
|
78 val re = map (pair "#Relate") re; |
|
79 |
|
80 val wh = filter (eq "#Where") ppc; |
|
81 val wh = (case wh of |
|
82 [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); []) |
|
83 | ((_, wh') :: []) => (map (TermC.parse_patt thy) wh' |
|
84 handle _ => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID)) |
|
85 | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID)); |
|
86 val sc = Program.prep_program scr |
|
87 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc |
|
88 in |
|
89 ({guh = guh, mathauthors = maa, init = init, ppc = gi @ fi @ re, pre = wh, rew_ord' = ro, |
|
90 erls = rls, srls = srls, prls = prls, calc = calc, |
|
91 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID) |
|
92 end; |
|
93 |
|
94 |
|
95 (** get Method from Store **) |
|
96 |
37 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *) |
97 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *) |
38 fun from_store metID = Store.get (get_mets ()) metID metID; |
98 fun from_store metID = Store.get (get_mets ()) metID metID; |
39 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID; |
99 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID; |
40 |
100 |
41 (**)end(**) |
101 (**)end(**) |