walther@59894
|
1 |
(* Title: MathEngBasic/problem.sml
|
walther@59894
|
2 |
Author: Walther Neuper 2019
|
walther@59894
|
3 |
(c) due to copyright terms
|
Walther@60555
|
4 |
|
Walther@60555
|
5 |
\<open>ML_structure Problem\<close> holds the essential information required for automated doing
|
Walther@60555
|
6 |
\<open>ML_structure Specification\<close> and \<open>ML_structure Solution\<close>.
|
Walther@60555
|
7 |
|
Walther@60555
|
8 |
Why \<open>ML_structure Problem\<close> is not parsed on the fly within the current \<open>ML_structure Context\<close>
|
Walther@60555
|
9 |
see \<open>ML_structure Refine\<close>.
|
walther@59894
|
10 |
*)
|
walther@59894
|
11 |
|
walther@59894
|
12 |
signature PROBLEM =
|
walther@59894
|
13 |
sig
|
walther@59894
|
14 |
type T = Probl_Def.T
|
Walther@60442
|
15 |
val empty: T
|
walther@59894
|
16 |
|
walther@59972
|
17 |
type id = Probl_Def.id
|
walther@59972
|
18 |
type id_reverse
|
walther@59903
|
19 |
val id_empty: id
|
walther@59903
|
20 |
val id_to_string: id -> string
|
walther@59903
|
21 |
|
Walther@60454
|
22 |
type input
|
walther@59973
|
23 |
type model_input
|
Walther@60559
|
24 |
val split_did: term -> term * term
|
Walther@60559
|
25 |
(* TODO: ---------- remove always empty ----- vvvvvvvvvvv -- vvv*)
|
Walther@60559
|
26 |
val prep_input : theory -> Check_Unique.id -> string list -> id -> input -> T * id
|
walther@59973
|
27 |
|
wenzelm@60306
|
28 |
val set_data: Rule_Def.rule_set -> theory -> theory
|
wenzelm@60306
|
29 |
val the_data: theory -> Rule_Def.rule_set
|
wenzelm@60306
|
30 |
|
wenzelm@60306
|
31 |
val parse_item: string parser -> 'a parser -> 'a parser
|
wenzelm@60314
|
32 |
val parse_item_name: string parser -> string -> string parser
|
wenzelm@60314
|
33 |
val parse_item_names: string parser -> string list parser
|
wenzelm@60306
|
34 |
val parse_model_input: model_input parser
|
wenzelm@60306
|
35 |
val parse_authors: string list parser
|
Walther@60434
|
36 |
val parse_cas: Token.T list -> string option * Token.T list
|
Walther@60434
|
37 |
val parse_methods: string list parser
|
Walther@60434
|
38 |
val ml: string -> ML_Lex.token Antiquote.antiquote list
|
wenzelm@60306
|
39 |
|
Walther@60556
|
40 |
(*val adapt_to_type: Proof.context -> T -> T*)
|
Walther@60556
|
41 |
(** )val from_store: id -> T( **)
|
Walther@60559
|
42 |
val from_store: Proof.context -> id -> T
|
walther@59894
|
43 |
end
|
walther@59894
|
44 |
|
walther@59894
|
45 |
(**)
|
walther@59894
|
46 |
structure Problem(**): PROBLEM(**) =
|
walther@59894
|
47 |
struct
|
walther@59894
|
48 |
(**)
|
walther@59894
|
49 |
|
walther@59894
|
50 |
type T = Probl_Def.T;
|
Walther@60442
|
51 |
val empty = Probl_Def.empty
|
walther@59894
|
52 |
|
walther@59970
|
53 |
(*
|
walther@60154
|
54 |
elements if the id are in reverse order as compared to MethodC:
|
walther@59970
|
55 |
e.g. ["linear", "univariate", "equation"] has "equation" as parent node --
|
walther@59970
|
56 |
-- this makes the id readable.
|
walther@59970
|
57 |
*)
|
walther@59903
|
58 |
type id = Probl_Def.id;
|
walther@60154
|
59 |
(* same order as for MethodC (used in Store )*)
|
walther@59972
|
60 |
type id_reverse = Probl_Def.id;
|
walther@59970
|
61 |
|
walther@59903
|
62 |
val id_empty = Probl_Def.id_empty;
|
walther@59903
|
63 |
val id_to_string = Probl_Def.id_to_string;
|
walther@59894
|
64 |
|
walther@59973
|
65 |
|
walther@59973
|
66 |
(** prepare Problem for Store **)
|
walther@59973
|
67 |
|
walther@60004
|
68 |
type model_input =
|
walther@60004
|
69 |
(Model_Pattern.m_field * (* "#Given", "#Find", "#Where", "#Relate" *)
|
walther@60004
|
70 |
TermC.as_string list) (* list of items belonging to m_field *)
|
walther@60004
|
71 |
list; (* list of "#Given" .. "#Relate" *)
|
walther@59973
|
72 |
type input =
|
walther@60004
|
73 |
id * (* the key into the problem hierarchy *)
|
walther@60004
|
74 |
model_input * (* e.g. ("#Given", ["unsorted u_u"]) list *)
|
walther@60004
|
75 |
Rule_Set.T * (* for evaluating "#Where" *)
|
walther@60004
|
76 |
TermC.as_string option * (* CAS_Cmd *)
|
walther@60004
|
77 |
Meth_Def.id list; (* methods that can solve the problem *)
|
walther@59973
|
78 |
|
walther@59973
|
79 |
(* split a term into description and (id | structured variable) for pbt, met.ppc *)
|
walther@59973
|
80 |
fun split_did t =
|
walther@59973
|
81 |
let
|
walther@59973
|
82 |
val (hd, arg) = case strip_comb t of
|
walther@59973
|
83 |
(hd, [arg]) => (hd, arg)
|
Walther@60559
|
84 |
| _ => raise ERROR ("split_did: doesn't match (hd,[arg]) for t = xxxxx" (*^ UnparseC.term t*))
|
Walther@60487
|
85 |
in (hd, arg) end
|
walther@59973
|
86 |
|
walther@59973
|
87 |
(* prepare problem-types before storing in pbltypes;
|
Walther@60559
|
88 |
dont forget to "check_guh_unique" before inserting *)
|
Walther@60559
|
89 |
fun prep_input thy guh maa init (pblID, dsc_dats, ev, ca, metIDs) =
|
walther@59973
|
90 |
let
|
walther@59973
|
91 |
fun eq f (f', _) = f = f';
|
Walther@60559
|
92 |
val _ = writeln "#prep_input 1";
|
walther@59973
|
93 |
val gi = filter (eq "#Given") dsc_dats;
|
Walther@60559
|
94 |
val _ = writeln "#prep_input 1a";
|
walther@59973
|
95 |
val gi = (case gi of
|
walther@59973
|
96 |
[] => []
|
walther@60265
|
97 |
| ((_, gi') :: []) =>
|
Walther@60559
|
98 |
map (split_did o (Syntax.read_term_global thy)) gi'
|
Walther@60559
|
99 |
| _ => raise ERROR ("prep_input: more than one '#Given' in xxxxx" (*^ strs2str pblID*)));
|
Walther@60559
|
100 |
val _ = writeln "#prep_input 1b";
|
walther@59973
|
101 |
val gi = map (pair "#Given") gi;
|
walther@59973
|
102 |
|
Walther@60559
|
103 |
val _ = writeln "#prep_input 2";
|
walther@59973
|
104 |
val fi = filter (eq "#Find") dsc_dats;
|
walther@59973
|
105 |
val fi = (case fi of
|
walther@59973
|
106 |
[] => []
|
walther@60265
|
107 |
| ((_, fi') :: []) =>
|
Walther@60559
|
108 |
(*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) fi'(*\<close> of
|
walther@60265
|
109 |
SOME x => x
|
Walther@60559
|
110 |
| NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Find' of " ^ strs2str pblID))*)
|
Walther@60559
|
111 |
| _ => raise ERROR ("prep_input: more than one '#Find' in xxxxx" (*^ strs2str pblID*)));
|
walther@59973
|
112 |
val fi = map (pair "#Find") fi;
|
walther@59973
|
113 |
|
Walther@60559
|
114 |
val _ = writeln "#prep_input 3";
|
walther@59973
|
115 |
val re = filter (eq "#Relate") dsc_dats;
|
walther@59973
|
116 |
val re = (case re of
|
walther@59973
|
117 |
[] => []
|
walther@60265
|
118 |
| ((_, re') :: []) =>
|
Walther@60559
|
119 |
(*(case \<^try>\<open> *)map (split_did o (Syntax.read_term_global thy)) re'(*\<close> of
|
walther@60265
|
120 |
SOME x => x
|
Walther@60559
|
121 |
| NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Relate' of " ^ strs2str pblID))*)
|
Walther@60559
|
122 |
| _ => raise ERROR ("prep_input: more than one '#Relate' in xxxxx" (*^ strs2str pblID*)));
|
walther@59973
|
123 |
val re = map (pair "#Relate") re;
|
walther@59973
|
124 |
|
Walther@60559
|
125 |
val _ = writeln "#prep_input 4";
|
Walther@60487
|
126 |
val wh = filter (eq "#Where") dsc_dats;
|
Walther@60487
|
127 |
val wh = (case wh of
|
Walther@60487
|
128 |
[] => []
|
Walther@60556
|
129 |
| ((_, wh') :: []) => (*special case in parsing*)
|
Walther@60574
|
130 |
(*(case \<^try>\<open> *)map (TermC.parse_patt thy) wh'(*\<close> of
|
Walther@60487
|
131 |
SOME x => x
|
Walther@60559
|
132 |
| NONE => raise ERROR ("prep_input: syntax raise ERROR in '#Where' of " ^ strs2str pblID))*)
|
Walther@60559
|
133 |
| _ => raise ERROR ("prep_input: more than one '#Where' in xxxxx" (*^ strs2str pblID*)));
|
Walther@60487
|
134 |
in
|
Walther@60487
|
135 |
({guh = guh, mathauthors = maa, init = init, thy = thy,
|
Walther@60487
|
136 |
cas = Option.map (Syntax.read_term_global thy) ca,
|
Walther@60487
|
137 |
prls = ev, where_ = wh, ppc = gi @ fi @ re, met = metIDs}, pblID)
|
Walther@60487
|
138 |
end;
|
walther@59973
|
139 |
|
walther@59973
|
140 |
|
wenzelm@60306
|
141 |
(** Isar command **)
|
wenzelm@60306
|
142 |
|
wenzelm@60306
|
143 |
(* theory data *)
|
wenzelm@60306
|
144 |
|
wenzelm@60306
|
145 |
structure Data = Theory_Data
|
wenzelm@60306
|
146 |
(
|
walther@60373
|
147 |
type T = Rule_Set.T option;
|
wenzelm@60306
|
148 |
val empty = NONE;
|
wenzelm@60306
|
149 |
val extend = I;
|
wenzelm@60306
|
150 |
fun merge _ = NONE;
|
wenzelm@60306
|
151 |
);
|
wenzelm@60306
|
152 |
|
wenzelm@60306
|
153 |
val set_data = Data.put o SOME;
|
wenzelm@60306
|
154 |
val the_data = the o Data.get;
|
wenzelm@60306
|
155 |
|
wenzelm@60306
|
156 |
|
wenzelm@60306
|
157 |
(* auxiliary parsers *)
|
wenzelm@60306
|
158 |
|
wenzelm@60306
|
159 |
fun parse_item (keyword: string parser) (parse: 'a parser) =
|
wenzelm@60306
|
160 |
(keyword -- Args.colon) |-- Parse.!!! parse;
|
wenzelm@60306
|
161 |
|
wenzelm@60314
|
162 |
fun parse_item_name keyword =
|
wenzelm@60314
|
163 |
Scan.optional (parse_item keyword Parse.name);
|
wenzelm@60314
|
164 |
|
wenzelm@60314
|
165 |
fun parse_item_names (keyword: string parser) =
|
wenzelm@60314
|
166 |
Scan.optional (parse_item keyword (Scan.repeat1 Parse.name)) [];
|
wenzelm@60314
|
167 |
|
wenzelm@60306
|
168 |
fun parse_tagged_terms keyword (tag: string) =
|
wenzelm@60306
|
169 |
Scan.optional (parse_item keyword (Scan.repeat Parse.term) >> (fn ts => [(tag, ts)])) [];
|
wenzelm@60306
|
170 |
|
wenzelm@60306
|
171 |
val parse_model_input : model_input parser =
|
wenzelm@60306
|
172 |
parse_tagged_terms \<^keyword>\<open>Given\<close> "#Given" @@@
|
wenzelm@60306
|
173 |
parse_tagged_terms \<^keyword>\<open>Where\<close> "#Where" @@@
|
wenzelm@60306
|
174 |
parse_tagged_terms \<^keyword>\<open>Find\<close> "#Find" @@@
|
wenzelm@60306
|
175 |
parse_tagged_terms \<^keyword>\<open>Relate\<close> "#Relate";
|
wenzelm@60306
|
176 |
|
wenzelm@60314
|
177 |
val parse_authors = parse_item_names \<^keyword>\<open>Author\<close>;
|
Walther@60434
|
178 |
val parse_cas = Scan.option (parse_item \<^keyword>\<open>CAS\<close> Parse.term);
|
Walther@60449
|
179 |
val parse_methods = parse_item_names \<^keyword>\<open>Method_Ref\<close>;
|
Walther@60434
|
180 |
val ml = ML_Lex.read;
|
wenzelm@60306
|
181 |
|
wenzelm@60306
|
182 |
|
wenzelm@60306
|
183 |
(* command definition *)
|
wenzelm@60306
|
184 |
|
wenzelm@60306
|
185 |
local
|
wenzelm@60306
|
186 |
|
wenzelm@60306
|
187 |
val _ =
|
wenzelm@60306
|
188 |
Outer_Syntax.command \<^command_keyword>\<open>problem\<close>
|
wenzelm@60306
|
189 |
"prepare ISAC problem type and register it to Knowledge Store"
|
wenzelm@60306
|
190 |
(Parse.name -- Parse.!!! (\<^keyword>\<open>:\<close> |-- Parse.name --
|
wenzelm@60306
|
191 |
Parse.!!! (\<^keyword>\<open>=\<close> |-- Parse.ML_source -- parse_authors --
|
wenzelm@60306
|
192 |
parse_methods -- parse_cas -- parse_model_input)) >>
|
wenzelm@60306
|
193 |
(fn (name, (id, ((((source, maa), mets), cas), model_input))) =>
|
wenzelm@60306
|
194 |
Toplevel.theory (fn thy =>
|
wenzelm@60306
|
195 |
let
|
Walther@60487
|
196 |
(*Ouptut from Biegelinie.problem pbl_bieg : "Biegelinien":*)
|
wenzelm@60306
|
197 |
val pblID = References_Def.explode_id id;
|
wenzelm@60306
|
198 |
val metIDs = map References_Def.explode_id mets;
|
Walther@60488
|
199 |
(*val _ = writeln ("#problem source: " ^ @{make_string} source)*)
|
wenzelm@60314
|
200 |
val set_data =
|
wenzelm@60306
|
201 |
ML_Context.expression (Input.pos_of source)
|
wenzelm@60306
|
202 |
(ml "Theory.setup (Problem.set_data (" @ ML_Lex.read_source source @ ml "))")
|
wenzelm@60306
|
203 |
|> Context.theory_map;
|
Walther@60488
|
204 |
(*val _ = writeln ("#problem set_data: " ^ @{make_string} set_data)*)
|
Walther@60487
|
205 |
(* Context.theory_map HAS STORED THE ml-source IN Theory_Data ALREADY,
|
Walther@60559
|
206 |
BUT prep_input REQUIRES ml-source AGAIN ... *)
|
wenzelm@60314
|
207 |
val input = the_data (set_data thy);
|
Walther@60488
|
208 |
(*val _ = writeln ("#problem input: " ^ @{make_string} input)*)
|
Walther@60487
|
209 |
|
Walther@60488
|
210 |
(*
|
Walther@60487
|
211 |
val _ = writeln ("#problem model_input: " ^ @{make_string} model_input)
|
Walther@60487
|
212 |
val (m1, m2) = case model_input of
|
Walther@60487
|
213 |
("#Given", [m1, m2]) :: _ => (m1, m2) (*=("<markup>", "<markup>")*)
|
Walther@60487
|
214 |
| _ => ("different case model_input", "different case model_input")
|
Walther@60487
|
215 |
val _ = writeln ("#problem m1: " ^ m1) (*= Traegerlaenge l_l*)
|
Walther@60487
|
216 |
val _ = writeln ("#problem m2: " ^ m2) (*= Streckenlast q_q *)
|
Walther@60488
|
217 |
( * TODO:
|
Walther@60487
|
218 |
* parse_model_input should preserve Position.T, Position.range, etc
|
Walther@60487
|
219 |
* ? preserve Position.T etc within ML_Lex.token Antiquote.antiquote list ?..
|
Walther@60487
|
220 |
..in analogy to set_data ?!?
|
Walther@60487
|
221 |
* by Context.theory_map notify Isabelle/PIDE of errors from model_input at Position.T
|
Walther@60559
|
222 |
* in case there are no errors, do prep_input (to be simplified)
|
Walther@60487
|
223 |
*)
|
Walther@60559
|
224 |
val arg = prep_input thy name maa id_empty (pblID, model_input, input, cas, metIDs);
|
Walther@60502
|
225 |
in KEStore_Elems.add_pbls @{context} [arg] thy end)))
|
wenzelm@60306
|
226 |
|
wenzelm@60306
|
227 |
in end;
|
wenzelm@60306
|
228 |
|
wenzelm@60306
|
229 |
|
wenzelm@60306
|
230 |
|
Walther@60488
|
231 |
(** get Problem from Store **)
|
walther@59973
|
232 |
|
Walther@60556
|
233 |
fun adapt_to_type ctxt ({guh, mathauthors, init, thy, cas, met, prls, where_, ppc} : Probl_Def.T) =
|
Walther@60556
|
234 |
let
|
Walther@60556
|
235 |
val cas = case cas of
|
Walther@60556
|
236 |
SOME t => SOME (Model_Pattern.adapt_term_to_type ctxt t)
|
Walther@60556
|
237 |
| NONE => NONE
|
Walther@60556
|
238 |
val where_ = map (Model_Pattern.adapt_term_to_type ctxt) where_
|
Walther@60556
|
239 |
val model = map (Model_Pattern.adapt_to_type ctxt) ppc
|
Walther@60556
|
240 |
in
|
Walther@60556
|
241 |
{guh = guh, mathauthors = mathauthors, init = init, thy = thy, cas = cas, met = met,
|
Walther@60556
|
242 |
prls = prls, where_ = where_, ppc = model}
|
Walther@60556
|
243 |
end
|
Walther@60556
|
244 |
|
Walther@60556
|
245 |
(** )
|
Walther@60517
|
246 |
fun from_store id =
|
Walther@60517
|
247 |
(Store.get (get_pbls ()) id (rev id))
|
Walther@60517
|
248 |
handle ERROR _ =>
|
Walther@60517
|
249 |
raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
|
Walther@60556
|
250 |
( **)
|
Walther@60559
|
251 |
fun from_store ctxt id =
|
Walther@60556
|
252 |
let
|
Walther@60556
|
253 |
val pbl = Store.get (get_pbls ()) id (rev id)
|
Walther@60556
|
254 |
in adapt_to_type ctxt pbl end
|
Walther@60556
|
255 |
handle ERROR _ =>
|
Walther@60556
|
256 |
raise error ("*** ERROR Problem.from_store " ^ strs2str id ^ " not found");
|
walther@59970
|
257 |
|
walther@59894
|
258 |
(**)end(**)
|