14516
|
1 |
signature HOL4_IMPORT_SYNTAX =
|
|
2 |
sig
|
|
3 |
type token = OuterSyntax.token
|
|
4 |
|
|
5 |
val import_segment: token list -> (theory -> theory) * token list
|
|
6 |
val import_theory : token list -> (theory -> theory) * token list
|
|
7 |
val end_import : token list -> (theory -> theory) * token list
|
|
8 |
|
|
9 |
val setup_theory : token list -> (theory -> theory) * token list
|
|
10 |
val end_setup : token list -> (theory -> theory) * token list
|
|
11 |
|
|
12 |
val thm_maps : token list -> (theory -> theory) * token list
|
|
13 |
val ignore_thms : token list -> (theory -> theory) * token list
|
|
14 |
val type_maps : token list -> (theory -> theory) * token list
|
|
15 |
val def_maps : token list -> (theory -> theory) * token list
|
|
16 |
val const_maps : token list -> (theory -> theory) * token list
|
|
17 |
val const_moves : token list -> (theory -> theory) * token list
|
|
18 |
val const_renames : token list -> (theory -> theory) * token list
|
|
19 |
|
|
20 |
val setup : unit -> unit
|
|
21 |
end
|
|
22 |
|
|
23 |
structure HOL4ImportSyntax :> HOL4_IMPORT_SYNTAX =
|
|
24 |
struct
|
|
25 |
|
|
26 |
type token = OuterSyntax.token
|
|
27 |
|
|
28 |
local structure P = OuterParse and K = OuterSyntax.Keyword in
|
|
29 |
|
|
30 |
(* Parsers *)
|
|
31 |
|
|
32 |
val import_segment = P.name >> set_import_segment
|
|
33 |
|
|
34 |
val import_theory = P.name >> (fn thyname =>
|
|
35 |
fn thy =>
|
|
36 |
thy |> set_generating_thy thyname
|
|
37 |
|> Theory.add_path thyname
|
|
38 |
|> add_dump (";setup_theory " ^ thyname))
|
|
39 |
|
|
40 |
val end_import = Scan.succeed
|
|
41 |
(fn thy =>
|
|
42 |
let
|
|
43 |
val thyname = get_generating_thy thy
|
|
44 |
val segname = get_import_segment thy
|
|
45 |
val (int_thms,facts) = Replay.setup_int_thms thyname thy
|
|
46 |
val thmnames = filter (not o should_ignore thyname thy) facts
|
|
47 |
in
|
|
48 |
thy |> clear_import_thy
|
|
49 |
|> set_segment thyname segname
|
|
50 |
|> set_used_names facts
|
|
51 |
|> Replay.import_thms thyname int_thms thmnames
|
|
52 |
|> clear_used_names
|
|
53 |
|> export_hol4_pending
|
|
54 |
|> Theory.parent_path
|
|
55 |
|> dump_import_thy thyname
|
|
56 |
|> add_dump ";end_setup"
|
|
57 |
end)
|
|
58 |
|
|
59 |
val ignore_thms = Scan.repeat1 P.name
|
|
60 |
>> (fn ignored =>
|
|
61 |
fn thy =>
|
|
62 |
let
|
|
63 |
val thyname = get_import_thy thy
|
|
64 |
in
|
|
65 |
foldl (fn (thy,thmname) => ignore_hol4 thyname thmname thy) (thy,ignored)
|
|
66 |
end)
|
|
67 |
|
|
68 |
val thm_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
|
|
69 |
>> (fn thmmaps =>
|
|
70 |
fn thy =>
|
|
71 |
let
|
|
72 |
val thyname = get_import_thy thy
|
|
73 |
in
|
|
74 |
foldl (fn (thy,(hol,isa)) => add_hol4_mapping thyname hol isa thy) (thy,thmmaps)
|
|
75 |
end)
|
|
76 |
|
|
77 |
val type_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
|
|
78 |
>> (fn typmaps =>
|
|
79 |
fn thy =>
|
|
80 |
let
|
|
81 |
val thyname = get_import_thy thy
|
|
82 |
in
|
|
83 |
foldl (fn (thy,(hol,isa)) => add_hol4_type_mapping thyname hol false isa thy) (thy,typmaps)
|
|
84 |
end)
|
|
85 |
|
|
86 |
val def_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname)
|
|
87 |
>> (fn defmaps =>
|
|
88 |
fn thy =>
|
|
89 |
let
|
|
90 |
val thyname = get_import_thy thy
|
|
91 |
in
|
|
92 |
foldl (fn (thy,(hol,isa)) => add_defmap thyname hol isa thy) (thy,defmaps)
|
|
93 |
end)
|
|
94 |
|
|
95 |
val const_renames = Scan.repeat1 (P.name --| P.$$$ ">" -- P.name)
|
|
96 |
>> (fn renames =>
|
|
97 |
fn thy =>
|
|
98 |
let
|
|
99 |
val thyname = get_import_thy thy
|
|
100 |
in
|
|
101 |
foldl (fn (thy,(hol,isa)) => add_hol4_const_renaming thyname hol isa thy) (thy,renames)
|
|
102 |
end)
|
|
103 |
|
|
104 |
val const_maps = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
|
|
105 |
>> (fn constmaps =>
|
|
106 |
fn thy =>
|
|
107 |
let
|
|
108 |
val thyname = get_import_thy thy
|
|
109 |
in
|
|
110 |
foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol false isa thy
|
|
111 |
| (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol false isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
|
|
112 |
end)
|
|
113 |
|
|
114 |
val const_moves = Scan.repeat1 (P.name --| P.$$$ ">" -- P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
|
|
115 |
>> (fn constmaps =>
|
|
116 |
fn thy =>
|
|
117 |
let
|
|
118 |
val thyname = get_import_thy thy
|
|
119 |
in
|
|
120 |
foldl (fn (thy,((hol,isa),None)) => add_hol4_const_mapping thyname hol true isa thy
|
|
121 |
| (thy,((hol,isa),Some ty)) => add_hol4_const_wt_mapping thyname hol true isa (typ_of (read_ctyp (sign_of thy) ty)) thy) (thy,constmaps)
|
|
122 |
end)
|
|
123 |
|
|
124 |
fun import_thy s =
|
|
125 |
let
|
|
126 |
val is = TextIO.openIn(s ^ ".imp")
|
|
127 |
val inp = TextIO.inputAll is
|
|
128 |
val _ = TextIO.closeIn is
|
|
129 |
val orig_source = Source.of_string inp
|
|
130 |
val symb_source = Symbol.source false orig_source
|
|
131 |
val lexes = ref (OuterLex.make_lexicon ["import_segment","ignore_thms","import","end",">","::","const_maps","const_moves","thm_maps","const_renames","type_maps","def_maps"],
|
|
132 |
Scan.empty_lexicon)
|
|
133 |
val get_lexes = fn () => !lexes
|
|
134 |
val token_source = OuterLex.source false get_lexes (Position.line 1) symb_source
|
|
135 |
val token_list = filter (not o (OuterLex.is_kind OuterLex.Space)) (Source.exhaust token_source)
|
|
136 |
val import_segmentP = OuterParse.$$$ "import_segment" |-- import_segment
|
|
137 |
val type_mapsP = OuterParse.$$$ "type_maps" |-- type_maps
|
|
138 |
val def_mapsP = OuterParse.$$$ "def_maps" |-- def_maps
|
|
139 |
val const_mapsP = OuterParse.$$$ "const_maps" |-- const_maps
|
|
140 |
val const_movesP = OuterParse.$$$ "const_moves" |-- const_moves
|
|
141 |
val const_renamesP = OuterParse.$$$ "const_renames" |-- const_renames
|
|
142 |
val ignore_thmsP = OuterParse.$$$ "ignore_thms" |-- ignore_thms
|
|
143 |
val thm_mapsP = OuterParse.$$$ "thm_maps" |-- thm_maps
|
|
144 |
val parser = type_mapsP || def_mapsP || const_mapsP || const_movesP || const_renamesP || thm_mapsP || ignore_thmsP || import_segmentP
|
|
145 |
val importP = OuterParse.$$$ "import" |-- Scan.repeat parser --| OuterParse.$$$ "end"
|
|
146 |
fun apply [] thy = thy
|
|
147 |
| apply (f::fs) thy = apply fs (f thy)
|
|
148 |
in
|
|
149 |
apply (set_replaying_thy s::Theory.add_path s::(fst (importP token_list)))
|
|
150 |
end
|
|
151 |
|
|
152 |
val setup_theory = P.name
|
|
153 |
>>
|
|
154 |
(fn thyname =>
|
|
155 |
fn thy =>
|
|
156 |
case HOL4DefThy.get thy of
|
|
157 |
NoImport => thy |> import_thy thyname
|
|
158 |
| Generating _ => error "Currently generating a theory!"
|
|
159 |
| Replaying _ => thy |> clear_import_thy |> import_thy thyname)
|
|
160 |
|
|
161 |
val end_setup = Scan.succeed (fn thy =>
|
|
162 |
let
|
|
163 |
val thyname = get_import_thy thy
|
|
164 |
val segname = get_import_segment thy
|
|
165 |
in
|
|
166 |
thy |> set_segment thyname segname
|
|
167 |
|> clear_import_thy
|
|
168 |
|> Theory.parent_path
|
|
169 |
end)
|
|
170 |
|
|
171 |
val set_dump = P.string -- P.string >> setup_dump
|
|
172 |
val fl_dump = Scan.succeed flush_dump
|
|
173 |
val append_dump = (P.verbatim || P.string) >> add_dump
|
|
174 |
|
|
175 |
val parsers =
|
|
176 |
[OuterSyntax.command "import_segment"
|
|
177 |
"Set import segment name"
|
|
178 |
K.thy_decl (import_segment >> Toplevel.theory),
|
|
179 |
OuterSyntax.command "import_theory"
|
|
180 |
"Set default HOL4 theory name"
|
|
181 |
K.thy_decl (import_theory >> Toplevel.theory),
|
|
182 |
OuterSyntax.command "end_import"
|
|
183 |
"End HOL4 import"
|
|
184 |
K.thy_decl (end_import >> Toplevel.theory),
|
|
185 |
OuterSyntax.command "setup_theory"
|
|
186 |
"Setup HOL4 theory replaying"
|
|
187 |
K.thy_decl (setup_theory >> Toplevel.theory),
|
|
188 |
OuterSyntax.command "end_setup"
|
|
189 |
"End HOL4 setup"
|
|
190 |
K.thy_decl (end_setup >> Toplevel.theory),
|
|
191 |
OuterSyntax.command "setup_dump"
|
|
192 |
"Setup the dump file name"
|
|
193 |
K.thy_decl (set_dump >> Toplevel.theory),
|
|
194 |
OuterSyntax.command "append_dump"
|
|
195 |
"Add text to dump file"
|
|
196 |
K.thy_decl (append_dump >> Toplevel.theory),
|
|
197 |
OuterSyntax.command "flush_dump"
|
|
198 |
"Write the dump to file"
|
|
199 |
K.thy_decl (fl_dump >> Toplevel.theory),
|
|
200 |
OuterSyntax.command "ignore_thms"
|
|
201 |
"Theorems to ignore in next HOL4 theory import"
|
|
202 |
K.thy_decl (ignore_thms >> Toplevel.theory),
|
|
203 |
OuterSyntax.command "type_maps"
|
|
204 |
"Map HOL4 type names to existing Isabelle/HOL type names"
|
|
205 |
K.thy_decl (type_maps >> Toplevel.theory),
|
|
206 |
OuterSyntax.command "def_maps"
|
|
207 |
"Map HOL4 constant names to their primitive definitions"
|
|
208 |
K.thy_decl (def_maps >> Toplevel.theory),
|
|
209 |
OuterSyntax.command "thm_maps"
|
|
210 |
"Map HOL4 theorem names to existing Isabelle/HOL theorem names"
|
|
211 |
K.thy_decl (thm_maps >> Toplevel.theory),
|
|
212 |
OuterSyntax.command "const_renames"
|
|
213 |
"Rename HOL4 const names"
|
|
214 |
K.thy_decl (const_renames >> Toplevel.theory),
|
|
215 |
OuterSyntax.command "const_moves"
|
|
216 |
"Rename HOL4 const names to other HOL4 constants"
|
|
217 |
K.thy_decl (const_moves >> Toplevel.theory),
|
|
218 |
OuterSyntax.command "const_maps"
|
|
219 |
"Map HOL4 const names to existing Isabelle/HOL const names"
|
|
220 |
K.thy_decl (const_maps >> Toplevel.theory)]
|
|
221 |
|
|
222 |
fun setup () = (OuterSyntax.add_keywords[">"];
|
|
223 |
OuterSyntax.add_parsers parsers)
|
|
224 |
|
|
225 |
end
|
|
226 |
|
|
227 |
end
|