|
walther@59814
|
1 |
(* Title: Interpret/Interpret.thy
|
|
neuper@41905
|
2 |
Author: Walther Neuper 110226
|
|
neuper@41905
|
3 |
(c) due to copyright terms
|
|
walther@59814
|
4 |
|
|
walther@59814
|
5 |
Collect all defitions for the Lucas-Interpreter
|
|
walther@59814
|
6 |
*)
|
|
neuper@41905
|
7 |
|
|
neuper@48761
|
8 |
theory Interpret
|
|
walther@60182
|
9 |
imports Specify.Specify
|
|
neuper@41905
|
10 |
begin
|
|
walther@59737
|
11 |
ML_file istate.sml
|
|
walther@59916
|
12 |
ML_file "thy-read.sml"
|
|
Walther@60544
|
13 |
ML_file "li-tool.sml"
|
|
walther@59920
|
14 |
ML_file "solve-step.sml"
|
|
walther@59909
|
15 |
ML_file "error-pattern.sml"
|
|
walther@59906
|
16 |
ML_file derive.sml
|
|
wneuper@59594
|
17 |
ML_file "lucas-interpreter.sml"
|
|
walther@59748
|
18 |
ML_file "step-solve.sml"
|
|
walther@60081
|
19 |
|
|
wneuper@59472
|
20 |
ML \<open>
|
|
walther@60081
|
21 |
local
|
|
wenzelm@60282
|
22 |
val thys_known_sofar = Theory.nodes_of @{theory}
|
|
walther@60182
|
23 |
val isac_thys_known_sofar = take (
|
|
walther@60182
|
24 |
find_index (curry Context.eq_thy ThyC.last_isabelle_thy) thys_known_sofar,
|
|
walther@60182
|
25 |
thys_known_sofar)
|
|
walther@60182
|
26 |
val isac_names_known_sofar = map Context.theory_name isac_thys_known_sofar
|
|
walther@60081
|
27 |
in
|
|
walther@60182
|
28 |
val compare_dependencies__ThyC =
|
|
walther@60182
|
29 |
if isac_names_known_sofar = ThyC.session_interpret_names @ ThyC.session_specify_names then ()
|
|
walther@60182
|
30 |
else raise ERROR "theory dependencies not as anticipated in ThyC"
|
|
walther@60081
|
31 |
end
|
|
Walther@60631
|
32 |
\<close> ML \<open> (*\------------------------------------ keep ------------------------------------------/*)
|
|
Walther@60631
|
33 |
\<close> text \<open> (* error in Integrate, EqSystem *)
|
|
Walther@60631
|
34 |
open ThyC (* <---------------------------------------------------------------------------------*)
|
|
Walther@60631
|
35 |
|
|
Walther@60631
|
36 |
type authors = string list; (* no more for thm, rls, rew_ord, cal *)
|
|
Walther@60631
|
37 |
type metadata = {coursedesign: authors, html: string, mathauthors: authors}
|
|
Walther@60631
|
38 |
(*WAS IN Thy_Write: datatype thydata
|
|
Walther@60631
|
39 |
= ...
|
|
Walther@60631
|
40 |
| Html of {coursedesign: authors, guh: Check_Unique.id, html: string, mathauthors: authors}*)
|
|
Walther@60631
|
41 |
|
|
Walther@60631
|
42 |
structure Data = Theory_Data
|
|
Walther@60631
|
43 |
(
|
|
Walther@60631
|
44 |
type T = metadata option;
|
|
Walther@60631
|
45 |
val empty = NONE; (*####### TODO: Htmldefault mit 2006 nehmen ############################*)
|
|
Walther@60631
|
46 |
fun merge _ = NONE;
|
|
Walther@60631
|
47 |
);
|
|
Walther@60631
|
48 |
val the_metadata = the o Data.get;
|
|
Walther@60631
|
49 |
val set_metadata = Data.put o SOME;
|
|
Walther@60631
|
50 |
|
|
Walther@60631
|
51 |
the_metadata: theory -> metadata;
|
|
Walther@60631
|
52 |
set_metadata: metadata -> theory -> theory;
|
|
Walther@60631
|
53 |
\<close> text \<open>
|
|
Walther@60631
|
54 |
open Error_Pattern (* <------------------------------------------------------------------------*)
|
|
Walther@60631
|
55 |
\<close> ML \<open>
|
|
Walther@60631
|
56 |
\<close> text \<open> (*Pbl_Met_Hierarchy.update_metpair WITHIN Know_Store.add_mets AS MODEL*)
|
|
Walther@60631
|
57 |
fun insert_in_method thy metID errpats = 123
|
|
Walther@60631
|
58 |
|
|
walther@59664
|
59 |
\<close> ML \<open>
|
|
walther@59729
|
60 |
\<close> ML \<open>
|
|
wneuper@59472
|
61 |
\<close>
|
|
wneuper@59283
|
62 |
end
|