author | haftmann |
Fri, 14 Jun 2019 08:34:28 +0000 | |
changeset 70347 | e5cd5471c18a |
parent 69576 | cfac69e7b962 |
child 74561 | 8e6c973003c8 |
permissions | -rw-r--r-- |
31325 | 1 |
(* Title: Pure/ML/ml_env.ML |
2 |
Author: Makarius |
|
3 |
||
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
4 |
Toplevel environment for Standard ML and Isabelle/ML within the |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
5 |
implicit context. |
31325 | 6 |
*) |
7 |
||
8 |
signature ML_ENV = |
|
9 |
sig |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
10 |
val Isabelle: string |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
11 |
val SML: string |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
12 |
val ML_environment: string Config.T |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
13 |
val ML_read_global: bool Config.T |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
14 |
val ML_write_global: bool Config.T |
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
15 |
val inherit: Context.generic list -> Context.generic -> Context.generic |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
16 |
type operations = |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
17 |
{read_source: Input.source -> ML_Lex.token Antiquote.antiquote list, |
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
18 |
explode_token: ML_Lex.token -> char list, |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
19 |
ML_system: bool} |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
20 |
type environment = {read: string, write: string} |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
21 |
val parse_environment: Context.generic option -> string -> environment |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
22 |
val print_environment: environment -> string |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
23 |
val SML_export: string |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
24 |
val SML_import: string |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
25 |
val setup: string -> operations -> theory -> theory |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
26 |
val Isabelle_operations: operations |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
27 |
val SML_operations: operations |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
28 |
val operations: Context.generic option -> string -> operations |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
29 |
val forget_structure: string -> Context.generic -> Context.generic |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
30 |
val bootstrap_name_space: Context.generic -> Context.generic |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
31 |
val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
32 |
val make_name_space: string -> ML_Name_Space.T |
62495 | 33 |
val context: ML_Compiler0.context |
34 |
val name_space: ML_Name_Space.T |
|
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
35 |
val check_functor: string -> unit |
68818 | 36 |
val get_breakpoint: Context.generic -> serial -> (bool Unsynchronized.ref * Position.T) option |
37 |
val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit |
|
31325 | 38 |
end |
39 |
||
40 |
structure ML_Env: ML_ENV = |
|
41 |
struct |
|
42 |
||
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
43 |
(* named environments *) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
44 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
45 |
val Isabelle = "Isabelle"; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
46 |
val SML = "SML"; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
47 |
|
69575 | 48 |
val ML_environment = Config.declare_string ("ML_environment", \<^here>) (K Isabelle); |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
49 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
50 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
51 |
(* global read/write *) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
52 |
|
69575 | 53 |
val ML_read_global = Config.declare_bool ("ML_read_global", \<^here>) (K true); |
54 |
val ML_write_global = Config.declare_bool ("ML_write_global", \<^here>) (K true); |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
55 |
|
69576 | 56 |
val read_global = Config.apply_generic ML_read_global; |
57 |
val write_global = Config.apply_generic ML_write_global; |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
58 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
59 |
|
68814 | 60 |
(* name space tables *) |
31328 | 61 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
62 |
type tables = |
62934 | 63 |
PolyML.NameSpace.Values.value Symtab.table * |
64 |
PolyML.NameSpace.TypeConstrs.typeConstr Symtab.table * |
|
65 |
PolyML.NameSpace.Infixes.fixity Symtab.table * |
|
66 |
PolyML.NameSpace.Structures.structureVal Symtab.table * |
|
67 |
PolyML.NameSpace.Signatures.signatureVal Symtab.table * |
|
68 |
PolyML.NameSpace.Functors.functorVal Symtab.table; |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
69 |
|
68814 | 70 |
val empty_tables: tables = |
71 |
(Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty); |
|
72 |
||
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
73 |
fun merge_tables |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
74 |
((val1, type1, fixity1, structure1, signature1, functor1), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
75 |
(val2, type2, fixity2, structure2, signature2, functor2)) : tables = |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
76 |
(Symtab.merge (K true) (val1, val2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
77 |
Symtab.merge (K true) (type1, type2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
78 |
Symtab.merge (K true) (fixity1, fixity2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
79 |
Symtab.merge (K true) (structure1, structure2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
80 |
Symtab.merge (K true) (signature1, signature2), |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
81 |
Symtab.merge (K true) (functor1, functor2)); |
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
82 |
|
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
83 |
fun update_tables_values vals (val1, type1, fixity1, structure1, signature1, functor1) : tables = |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
84 |
(fold Symtab.update vals val1, type1, fixity1, structure1, signature1, functor1); |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
85 |
|
68814 | 86 |
val sml_tables: tables = |
87 |
(Symtab.make ML_Name_Space.sml_val, |
|
88 |
Symtab.make ML_Name_Space.sml_type, |
|
89 |
Symtab.make ML_Name_Space.sml_fixity, |
|
90 |
Symtab.make ML_Name_Space.sml_structure, |
|
91 |
Symtab.make ML_Name_Space.sml_signature, |
|
92 |
Symtab.make ML_Name_Space.sml_functor); |
|
93 |
||
94 |
||
95 |
(* context data *) |
|
96 |
||
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
97 |
type operations = |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
98 |
{read_source: Input.source -> ML_Lex.token Antiquote.antiquote list, |
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
99 |
explode_token: ML_Lex.token -> char list, |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
100 |
ML_system: bool}; |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
101 |
|
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
102 |
local |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
103 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
104 |
type env = tables * operations; |
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
105 |
type data = env Name_Space.table * (bool Unsynchronized.ref * Position.T) Inttab.table; |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
106 |
|
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
107 |
val empty_data: data = (Name_Space.empty_table "ML_environment", Inttab.empty); |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
108 |
|
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
109 |
fun merge_data ((envs1, breakpoints1), (envs2, breakpoints2)) : data = |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
110 |
((envs1, envs2) |> Name_Space.join_tables |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
111 |
(K (fn ((tables1, ops), (tables2, _)) => (merge_tables (tables1, tables2), ops))), |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
112 |
Inttab.merge (K true) (breakpoints1, breakpoints2)); |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
113 |
|
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
114 |
in |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
115 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
116 |
structure Data = Generic_Data |
31325 | 117 |
( |
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
118 |
type T = data; |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
119 |
val empty = empty_data; |
68818 | 120 |
val extend = I; |
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
121 |
val merge = merge_data; |
31325 | 122 |
); |
123 |
||
68865
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
124 |
fun inherit contexts = Data.put (Library.foldl1 merge_data (map Data.get contexts)); |
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
125 |
|
dd44e31ca2c6
support multiple inheritance of ML environments, with canonical merge order as in Context.begin_theory;
wenzelm
parents:
68823
diff
changeset
|
126 |
end; |
31325 | 127 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
128 |
val get_env = Name_Space.get o #1 o Data.get; |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
129 |
val get_tables = #1 oo get_env; |
60746 | 130 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
131 |
fun update_tables env_name f context = context |> (Data.map o apfst) (fn envs => |
68818 | 132 |
let val _ = Name_Space.get envs env_name; |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
133 |
in Name_Space.map_table_entry env_name (apfst f) envs end); |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
134 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
135 |
fun forget_structure name context = |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
136 |
(if write_global context then ML_Name_Space.forget_structure name else (); |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
137 |
context |> update_tables Isabelle (fn tables => |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
138 |
(#1 tables, #2 tables, #3 tables, Symtab.delete_safe name (#4 tables), #5 tables, #6 tables))); |
62902
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
139 |
|
3c0f53eae166
more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
wenzelm
parents:
62889
diff
changeset
|
140 |
|
68817 | 141 |
(* environment name *) |
142 |
||
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
143 |
type environment = {read: string, write: string}; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
144 |
|
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
145 |
val separator = ">"; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
146 |
|
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
147 |
fun parse_environment opt_context environment = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
148 |
let |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
149 |
fun check name = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
150 |
(case opt_context of |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
151 |
NONE => |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
152 |
if name = Isabelle then name |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
153 |
else error ("Bad ML environment name " ^ quote name ^ " -- no context") |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
154 |
| SOME context => if name = Isabelle then name else (get_env context name; name)); |
68817 | 155 |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
156 |
val spec = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
157 |
if environment = "" then |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
158 |
(case opt_context of |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
159 |
NONE => Isabelle |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
160 |
| SOME context => Config.get_generic context ML_environment) |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
161 |
else environment; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
162 |
val (read, write) = |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
163 |
(case space_explode separator spec of |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
164 |
[a] => (a, a) |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
165 |
| [a, b] => (a, b) |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
166 |
| _ => error ("Malformed ML environment specification: " ^ quote spec)); |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
167 |
in {read = check read, write = check write} end; |
68817 | 168 |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
169 |
fun print_environment {read, write} = read ^ separator ^ write; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
170 |
|
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
171 |
val SML_export = print_environment {read = SML, write = Isabelle}; |
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
172 |
val SML_import = print_environment {read = Isabelle, write = SML}; |
68817 | 173 |
|
174 |
||
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
175 |
(* setup operations *) |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
176 |
|
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
177 |
val ML_system_values = |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
178 |
#allVal (ML_Name_Space.global) () |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
179 |
|> filter (member (op =) ["ML_system_pretty", "ML_system_pp", "ML_system_overload"] o #1); |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
180 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
181 |
fun setup env_name ops thy = |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
182 |
thy |> (Context.theory_map o Data.map o apfst) (fn envs => |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
183 |
let |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
184 |
val thy' = Sign.map_naming (K Name_Space.global_naming) thy; |
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
185 |
val tables = |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
186 |
(if env_name = Isabelle then empty_tables else sml_tables) |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
187 |
|> #ML_system ops ? update_tables_values ML_system_values; |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
188 |
val (_, envs') = |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
189 |
Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs; |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
190 |
in envs' end); |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
191 |
|
68823 | 192 |
val Isabelle_operations: operations = |
193 |
{read_source = ML_Lex.read_source, |
|
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
194 |
explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode), |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
195 |
ML_system = false}; |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
196 |
|
68823 | 197 |
val SML_operations: operations = |
198 |
{read_source = ML_Lex.read_source_sml, |
|
68917
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
199 |
explode_token = ML_Lex.check_content_of #> String.explode, |
75691a5c8fb6
setup option ML_system for special values that cannot be rebound within regular ML;
wenzelm
parents:
68865
diff
changeset
|
200 |
ML_system = false}; |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
201 |
|
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
202 |
val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations); |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
203 |
|
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
204 |
fun operations opt_context environment = |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
205 |
let val env = #read (parse_environment opt_context environment) in |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
206 |
(case opt_context of |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
207 |
NONE => Isabelle_operations |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
208 |
| SOME context => #2 (get_env context env)) |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
209 |
end; |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
210 |
|
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
211 |
|
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
212 |
(* name space *) |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56203
diff
changeset
|
213 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
214 |
val bootstrap_name_space = |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
215 |
update_tables Isabelle (fn (tables: tables) => |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
216 |
let |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
217 |
fun update entries (x, y) = member (op =) entries x ? Symtab.update (x, y); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
218 |
val bootstrap_val = update ML_Name_Space.bootstrap_values; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
219 |
val bootstrap_structure = update ML_Name_Space.bootstrap_structures; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
220 |
val bootstrap_signature = update ML_Name_Space.bootstrap_signatures; |
62873
2f9c8a18f832
support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
wenzelm
parents:
62839
diff
changeset
|
221 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
222 |
val (val1, type1, fixity1, structure1, signature1, functor1) = sml_tables; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
223 |
val val2 = val1 |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
224 |
|> fold bootstrap_val (#allVal ML_Name_Space.global ()) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
225 |
|> Symtab.fold bootstrap_val (#1 tables); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
226 |
val structure2 = structure1 |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
227 |
|> fold bootstrap_structure (#allStruct ML_Name_Space.global ()) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
228 |
|> Symtab.fold bootstrap_structure (#4 tables); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
229 |
val signature2 = signature1 |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
230 |
|> fold bootstrap_signature (#allSig ML_Name_Space.global ()) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
231 |
|> Symtab.fold bootstrap_signature (#5 tables); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
232 |
in (val2, type1, fixity1, structure2, signature2, functor1) end); |
68276 | 233 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
234 |
fun add_name_space env (space: ML_Name_Space.T) = |
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
235 |
update_tables env (fn (val1, type1, fixity1, structure1, signature1, functor1) => |
60858 | 236 |
let |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
237 |
val val2 = fold Symtab.update (#allVal space ()) val1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
238 |
val type2 = fold Symtab.update (#allType space ()) type1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
239 |
val fixity2 = fold Symtab.update (#allFix space ()) fixity1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
240 |
val structure2 = fold Symtab.update (#allStruct space ()) structure1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
241 |
val signature2 = fold Symtab.update (#allSig space ()) signature1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
242 |
val functor2 = fold Symtab.update (#allFunct space ()) functor1; |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
243 |
in (val2, type2, fixity2, structure2, signature2, functor2) end); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
244 |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
245 |
fun make_name_space environment : ML_Name_Space.T = |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
246 |
let |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
247 |
val {read, write} = parse_environment (Context.get_generic_context ()) environment; |
60858 | 248 |
|
68821
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
249 |
fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_tables context read)) name; |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
250 |
fun dest_env sel1 context = Symtab.dest (sel1 (get_tables context read)); |
877534be1930
explicit setup of operations: avoid hardwired stuff;
wenzelm
parents:
68820
diff
changeset
|
251 |
fun enter_env ap1 entry = update_tables write (ap1 (Symtab.update entry)); |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
252 |
|
31325 | 253 |
fun lookup sel1 sel2 name = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
254 |
if read = Isabelle then |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
255 |
(case Context.get_generic_context () of |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
256 |
NONE => sel2 ML_Name_Space.global name |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
257 |
| SOME context => |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
258 |
(case lookup_env sel1 context name of |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
259 |
NONE => if read_global context then sel2 ML_Name_Space.global name else NONE |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
260 |
| some => some)) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
261 |
else lookup_env sel1 (Context.the_generic_context ()) name; |
31325 | 262 |
|
263 |
fun all sel1 sel2 () = |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
264 |
sort_distinct (string_ord o apply2 #1) |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
265 |
(if read = Isabelle then |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
266 |
(case Context.get_generic_context () of |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
267 |
NONE => sel2 ML_Name_Space.global () |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
268 |
| SOME context => |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
269 |
dest_env sel1 context @ |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
270 |
(if read_global context then sel2 ML_Name_Space.global () else [])) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
271 |
else dest_env sel1 (Context.the_generic_context ())); |
31325 | 272 |
|
273 |
fun enter ap1 sel2 entry = |
|
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
274 |
if write = Isabelle then |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
275 |
(case Context.get_generic_context () of |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
276 |
NONE => sel2 ML_Name_Space.global entry |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
277 |
| SOME context => |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
278 |
(if write_global context then sel2 ML_Name_Space.global entry else (); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
279 |
Context.>> (enter_env ap1 entry))) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
280 |
else Context.>> (enter_env ap1 entry); |
31325 | 281 |
in |
282 |
{lookupVal = lookup #1 #lookupVal, |
|
283 |
lookupType = lookup #2 #lookupType, |
|
284 |
lookupFix = lookup #3 #lookupFix, |
|
285 |
lookupStruct = lookup #4 #lookupStruct, |
|
286 |
lookupSig = lookup #5 #lookupSig, |
|
287 |
lookupFunct = lookup #6 #lookupFunct, |
|
288 |
enterVal = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal, |
|
289 |
enterType = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType, |
|
290 |
enterFix = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix, |
|
291 |
enterStruct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct, |
|
292 |
enterSig = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig, |
|
293 |
enterFunct = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct, |
|
294 |
allVal = all #1 #allVal, |
|
295 |
allType = all #2 #allType, |
|
296 |
allFix = all #3 #allFix, |
|
297 |
allStruct = all #4 #allStruct, |
|
298 |
allSig = all #5 #allSig, |
|
299 |
allFunct = all #6 #allFunct} |
|
300 |
end; |
|
301 |
||
62495 | 302 |
val context: ML_Compiler0.context = |
68820
2e4df245754e
clarified environment: allow "read>write" specification;
wenzelm
parents:
68818
diff
changeset
|
303 |
{name_space = make_name_space "", |
62716
d80b9f4990e4
explicit print_depth for the sake of Spec_Check.determine_type;
wenzelm
parents:
62657
diff
changeset
|
304 |
print_depth = NONE, |
62493 | 305 |
here = Position.here oo Position.line_file, |
31325 | 306 |
print = writeln, |
307 |
error = error}; |
|
308 |
||
62495 | 309 |
val name_space = #name_space context; |
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56275
diff
changeset
|
310 |
|
62495 | 311 |
val is_functor = is_some o #lookupFunct name_space; |
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
312 |
|
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
313 |
fun check_functor name = |
36165 | 314 |
if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then () |
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
315 |
else error ("Unknown ML functor: " ^ quote name); |
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
33519
diff
changeset
|
316 |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
317 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
318 |
(* breakpoints *) |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
319 |
|
68818 | 320 |
val get_breakpoint = Inttab.lookup o #2 o Data.get; |
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
321 |
|
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
322 |
fun add_breakpoints more_breakpoints = |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
323 |
if is_some (Context.get_generic_context ()) then |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
324 |
Context.>> |
68818 | 325 |
((Data.map o apsnd) |
326 |
(fold (Inttab.update_new o (apsnd o apsnd) Position.make) more_breakpoints)) |
|
68816
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
327 |
else (); |
5a53724fe247
support named ML environments, notably "Isabelle", "SML";
wenzelm
parents:
68814
diff
changeset
|
328 |
|
31325 | 329 |
end; |