1 (* Title: Interpret/lucas-interpreter.sml
2 Author: Walther Neuper 2019
3 (c) due to copyright terms
13 val id_to_string: id -> string
16 (* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
17 val prep_input : theory -> Check_Unique.id -> string list -> id ->
18 id * Problem.model_input * input * thm -> T * id
20 val set_data: input -> theory -> theory
21 val the_data: theory -> input
23 val from_store: id -> T
24 val from_store': theory -> id -> T
28 structure MethodC(**): METHOD(**) =
33 val empty = Meth_Def.empty;
35 type id = Meth_Def.id;
36 val id_empty = Meth_Def.id_empty;
37 val id_to_string = Meth_Def.id_to_string;
40 (** prepare MethodC for Store **)
42 (* a subset of MethodC.T record's fields *)
44 {calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
45 prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
47 fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
49 {rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
50 errpats = ep, nrls = nr}, scr) =
52 fun eq f (f', _) = f = f';
53 val gi = filter (eq "#Given") ppc;
55 [] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
57 (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) gi'\<close> of
59 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
60 | _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
61 val gi = map (pair "#Given") gi;
63 val fi = filter (eq "#Find") ppc;
65 [] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
67 (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) fi'\<close> of
69 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
70 | _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
71 val fi = map (pair "#Find") fi;
73 val re = filter (eq "#Relate") ppc;
75 [] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
77 (case \<^try>\<open> map (Problem.split_did o (TermC.parseNEW'' thy)) re'\<close> of
79 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
80 | _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
81 val re = map (pair "#Relate") re;
83 val wh = filter (eq "#Where") ppc;
85 [] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
87 (case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
89 | NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
90 | _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
91 val sc = Program.prep_program scr
92 val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
94 ({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
95 rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
96 crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
102 structure Data = Theory_Data
104 type T = input option;
110 val set_data = Data.put o SOME;
111 val the_data = the o Data.get;
116 Scan.option (Problem.parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
118 val ml = ML_Lex.read;
121 Outer_Syntax.command \<^command_keyword>\<open>method\<close>
122 "prepare ISAC method and register it to Knowledge Store"
123 (Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
124 Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- Problem.parse_authors --
125 parse_program -- Problem.parse_model_input)) >>
126 (fn (name, (id, (((source, maa), program), model_input))) => Toplevel.theory (fn thy =>
128 val metID = References_Def.explode_id id;
130 ML_Context.expression (Input.pos_of source)
131 (ml "Theory.setup (MethodC.set_data (" @ ML_Lex.read_source source @ ml "))")
132 |> Context.theory_map;
133 val input = the_data (set_data thy);
137 | SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
138 val arg = prep_input thy name maa id_empty (metID, model_input, input, thm);
139 in KEStore_Elems.add_mets @{context} [arg] thy end)))
143 (** get MethodC from Store **)
145 (* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
146 fun from_store metID = Store.get (get_mets ()) metID metID;
147 fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;