walther@59894
|
1 |
(* Title: Interpret/lucas-interpreter.sml
|
walther@59894
|
2 |
Author: Walther Neuper 2019
|
walther@59894
|
3 |
(c) due to copyright terms
|
walther@59894
|
4 |
*)
|
walther@59894
|
5 |
|
walther@59894
|
6 |
signature METHOD =
|
walther@59894
|
7 |
sig
|
walther@59895
|
8 |
type T = Meth_Def.T
|
walther@59903
|
9 |
val empty: T
|
walther@59903
|
10 |
|
walther@59903
|
11 |
type id = Meth_Def.id
|
walther@59903
|
12 |
val id_empty: id
|
walther@59903
|
13 |
val id_to_string: id -> string
|
walther@59970
|
14 |
|
walther@59973
|
15 |
type input
|
walther@59973
|
16 |
(* TODO: ------------- remove always empty --- vvvvvvvvvvv -- vvv*)
|
walther@59973
|
17 |
val prep_input : theory -> Check_Unique.id -> string list -> id ->
|
walther@59973
|
18 |
id * Problem.model_input * input * thm -> T * id
|
walther@59973
|
19 |
|
wenzelm@60303
|
20 |
val set_input: input -> theory -> theory
|
wenzelm@60303
|
21 |
val the_input: theory -> input
|
wenzelm@60303
|
22 |
|
walther@59970
|
23 |
val from_store: id -> T
|
walther@59970
|
24 |
val from_store': theory -> id -> T
|
walther@59894
|
25 |
end
|
walther@59894
|
26 |
|
walther@59894
|
27 |
(**)
|
walther@60154
|
28 |
structure MethodC(**): METHOD(**) =
|
walther@59894
|
29 |
struct
|
walther@59894
|
30 |
(**)
|
walther@59894
|
31 |
|
walther@59895
|
32 |
type T = Meth_Def.T;
|
walther@59903
|
33 |
val empty = Meth_Def.empty;
|
walther@59903
|
34 |
|
walther@59903
|
35 |
type id = Meth_Def.id;
|
walther@59903
|
36 |
val id_empty = Meth_Def.id_empty;
|
walther@59903
|
37 |
val id_to_string = Meth_Def.id_to_string;
|
walther@59894
|
38 |
|
walther@59973
|
39 |
|
walther@60154
|
40 |
(** prepare MethodC for Store **)
|
walther@59973
|
41 |
|
walther@60154
|
42 |
(* a subset of MethodC.T record's fields *)
|
walther@59973
|
43 |
type input =
|
walther@59973
|
44 |
{calc: Rule_Def.calc list, crls: Rule_Set.T, errpats: Error_Pattern_Def.T list, nrls: Rule_Set.T,
|
walther@59973
|
45 |
prls: Rule_Set.T, rew_ord': Rewrite_Ord.rew_ord', rls': Rule_Set.T, srls: Rule_Set.T}
|
walther@59973
|
46 |
|
wenzelm@60303
|
47 |
fun prep_input thy guh (mathauthors: string list) (init: References_Def.id)
|
walther@59973
|
48 |
(metID, ppc,
|
walther@59973
|
49 |
{rew_ord' = ro, rls' = rls, srls = srls, prls = prls, calc = _(*scr_isa_fns*), crls = cr,
|
walther@59973
|
50 |
errpats = ep, nrls = nr}, scr) =
|
walther@59973
|
51 |
let
|
walther@59973
|
52 |
fun eq f (f', _) = f = f';
|
walther@59973
|
53 |
val gi = filter (eq "#Given") ppc;
|
walther@59973
|
54 |
val gi = (case gi of
|
walther@59973
|
55 |
[] => (writeln ("prep_input: in " ^ guh ^ " #Given is empty ?!?"); [])
|
walther@60265
|
56 |
| ((_, gi') :: []) =>
|
walther@60265
|
57 |
(case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) gi'\<close> of
|
walther@60265
|
58 |
SOME x => x
|
walther@60265
|
59 |
| NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Given' of " ^ strs2str metID))
|
walther@59973
|
60 |
| _ => raise ERROR ("prep_pbt: more than one '#Given' in " ^ strs2str metID));
|
walther@59973
|
61 |
val gi = map (pair "#Given") gi;
|
walther@59973
|
62 |
|
walther@59973
|
63 |
val fi = filter (eq "#Find") ppc;
|
walther@59973
|
64 |
val fi = (case fi of
|
walther@59973
|
65 |
[] => (writeln ("prep_input: in " ^ guh ^ " #Find is empty ?!?"); [])
|
walther@60265
|
66 |
| ((_, fi') :: []) =>
|
walther@60265
|
67 |
(case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) fi'\<close> of
|
walther@60265
|
68 |
SOME x => x
|
walther@60265
|
69 |
| NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Find' of " ^ strs2str metID))
|
walther@59973
|
70 |
| _ => raise ERROR ("prep_pbt: more than one '#Find' in " ^ strs2str metID));
|
walther@59973
|
71 |
val fi = map (pair "#Find") fi;
|
walther@59973
|
72 |
|
walther@59973
|
73 |
val re = filter (eq "#Relate") ppc;
|
walther@59973
|
74 |
val re = (case re of
|
walther@59973
|
75 |
[] => (writeln ("prep_input: in " ^ guh ^ " #Relate is empty ?!?"); [])
|
walther@60265
|
76 |
| ((_,re') :: []) =>
|
walther@60265
|
77 |
(case \<^try>\<open> map (Problem.split_did o Thm.term_of o the o (TermC.parse thy)) re'\<close> of
|
walther@60265
|
78 |
SOME x => x
|
walther@60265
|
79 |
| NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Relate' of " ^ strs2str metID))
|
walther@59973
|
80 |
| _ => raise ERROR ("prep_pbt: more than one '#Relate' in " ^ strs2str metID));
|
walther@59973
|
81 |
val re = map (pair "#Relate") re;
|
walther@59973
|
82 |
|
walther@59973
|
83 |
val wh = filter (eq "#Where") ppc;
|
walther@59973
|
84 |
val wh = (case wh of
|
walther@59973
|
85 |
[] => (writeln ("prep_input: in " ^ guh ^ " #Where is empty ?!?"); [])
|
walther@60265
|
86 |
| ((_, wh') :: []) =>
|
walther@60265
|
87 |
(case \<^try>\<open> map (TermC.parse_patt thy) wh'\<close> of
|
walther@60265
|
88 |
SOME x => x
|
walther@60265
|
89 |
| NONE => raise ERROR ("prep_pbt: syntax raise ERROR in '#Where' of " ^ strs2str metID))
|
walther@59973
|
90 |
| _ => raise ERROR ("prep_pbt: more than one '#Where' in " ^ strs2str metID));
|
walther@59973
|
91 |
val sc = Program.prep_program scr
|
walther@59973
|
92 |
val calc = if Thm.eq_thm (scr, @{thm refl}) then [] else Auto_Prog.get_calcs thy sc
|
walther@59973
|
93 |
in
|
wenzelm@60303
|
94 |
({guh = guh, mathauthors = mathauthors, init = init, ppc = gi @ fi @ re, pre = wh,
|
wenzelm@60303
|
95 |
rew_ord' = ro, erls = rls, srls = srls, prls = prls, calc = calc,
|
walther@59973
|
96 |
crls = cr, errpats = ep, nrls = nr, scr = Rule.Prog sc}, metID)
|
walther@59973
|
97 |
end;
|
walther@59973
|
98 |
|
walther@59973
|
99 |
|
wenzelm@60303
|
100 |
(** Isar command **)
|
wenzelm@60303
|
101 |
|
wenzelm@60303
|
102 |
structure Data = Theory_Data
|
wenzelm@60303
|
103 |
(
|
wenzelm@60303
|
104 |
type T = input option;
|
wenzelm@60303
|
105 |
val empty = NONE;
|
wenzelm@60303
|
106 |
val extend = I;
|
wenzelm@60303
|
107 |
fun merge _ = NONE;
|
wenzelm@60303
|
108 |
);
|
wenzelm@60303
|
109 |
|
wenzelm@60303
|
110 |
val set_input = Data.put o SOME;
|
wenzelm@60303
|
111 |
val the_input = the o Data.get;
|
wenzelm@60303
|
112 |
|
wenzelm@60303
|
113 |
local
|
wenzelm@60303
|
114 |
|
wenzelm@60303
|
115 |
fun parse_item keyword parse = (keyword -- Args.colon) |-- Parse.!!! parse;
|
wenzelm@60303
|
116 |
|
wenzelm@60303
|
117 |
val parse_authors =
|
wenzelm@60303
|
118 |
Scan.optional (parse_item \<^keyword>\<open>Author\<close> (Scan.repeat1 Parse.name)) [];
|
wenzelm@60303
|
119 |
|
wenzelm@60303
|
120 |
val parse_program =
|
wenzelm@60303
|
121 |
Scan.option (parse_item \<^keyword>\<open>Program\<close> (Parse.position Parse.name));
|
wenzelm@60303
|
122 |
|
wenzelm@60303
|
123 |
fun parse_terms keyword (tag: string) =
|
wenzelm@60303
|
124 |
Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
|
wenzelm@60303
|
125 |
|
wenzelm@60303
|
126 |
val parse_ppc =
|
wenzelm@60303
|
127 |
parse_terms \<^keyword>\<open>Given\<close> "#Given" @@@
|
wenzelm@60303
|
128 |
parse_terms \<^keyword>\<open>Where\<close> "#Where" @@@
|
wenzelm@60303
|
129 |
parse_terms \<^keyword>\<open>Find\<close> "#Find" @@@
|
wenzelm@60303
|
130 |
parse_terms \<^keyword>\<open>Relate\<close> "#Relate";
|
wenzelm@60303
|
131 |
|
wenzelm@60303
|
132 |
val ml = ML_Lex.read;
|
wenzelm@60303
|
133 |
|
wenzelm@60303
|
134 |
val _ =
|
wenzelm@60303
|
135 |
Outer_Syntax.command \<^command_keyword>\<open>method\<close>
|
wenzelm@60303
|
136 |
"prepare ISAC method and register it to Knowledge Store"
|
wenzelm@60303
|
137 |
(Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
|
wenzelm@60303
|
138 |
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors -- parse_program -- parse_ppc)) >>
|
wenzelm@60303
|
139 |
(fn (name, (id, (((source, mathauthors), simp), ppc))) => Toplevel.theory (fn thy =>
|
wenzelm@60303
|
140 |
let
|
wenzelm@60303
|
141 |
val metID = References_Def.explode_id id;
|
wenzelm@60303
|
142 |
val eval_input =
|
wenzelm@60303
|
143 |
ML_Context.expression (Input.pos_of source)
|
wenzelm@60303
|
144 |
(ml "Theory.setup (MethodC.set_input (" @ ML_Lex.read_source source @ ml "))")
|
wenzelm@60303
|
145 |
|> Context.theory_map;
|
wenzelm@60303
|
146 |
val input = the_input (eval_input thy);
|
wenzelm@60303
|
147 |
val thm =
|
wenzelm@60303
|
148 |
(case simp of
|
wenzelm@60303
|
149 |
NONE => @{thm refl}
|
wenzelm@60303
|
150 |
| SOME a => Global_Theory.get_thm thy (Global_Theory.check_fact thy a));
|
wenzelm@60303
|
151 |
val arg = prep_input thy name mathauthors id_empty (metID, ppc, input, thm);
|
wenzelm@60303
|
152 |
in KEStore_Elems.add_mets [arg] thy end)))
|
wenzelm@60303
|
153 |
|
wenzelm@60303
|
154 |
in end;
|
wenzelm@60303
|
155 |
|
walther@60154
|
156 |
(** get MethodC from Store **)
|
walther@59973
|
157 |
|
walther@59970
|
158 |
(* TODO: throws exn 'get_pbt not found: ' ... confusing !! take 'ketype' as an argument *)
|
walther@59970
|
159 |
fun from_store metID = Store.get (get_mets ()) metID metID;
|
walther@59970
|
160 |
fun from_store' thy metID = Store.get (KEStore_Elems.get_mets thy) metID metID;
|
walther@59970
|
161 |
|
walther@59894
|
162 |
(**)end(**)
|