203 quote( |
203 quote( |
204 PrintMode.setmp [] ( |
204 PrintMode.setmp [] ( |
205 Library.setmp show_brackets false ( |
205 Library.setmp show_brackets false ( |
206 Library.setmp show_all_types true ( |
206 Library.setmp show_all_types true ( |
207 Library.setmp Syntax.ambiguity_is_error false ( |
207 Library.setmp Syntax.ambiguity_is_error false ( |
208 Library.setmp show_sorts true string_of_cterm)))) |
208 Library.setmp show_sorts true Display.string_of_cterm)))) |
209 ct) |
209 ct) |
210 end |
210 end |
211 |
211 |
212 exception SMART_STRING |
212 exception SMART_STRING |
213 |
213 |
225 | G 2 = Library.setmp show_all_types true (G 0) |
225 | G 2 = Library.setmp show_all_types true (G 0) |
226 | G 3 = Library.setmp show_brackets true (G 2) |
226 | G 3 = Library.setmp show_brackets true (G 2) |
227 | G _ = raise SMART_STRING |
227 | G _ = raise SMART_STRING |
228 fun F n = |
228 fun F n = |
229 let |
229 let |
230 val str = Library.setmp show_brackets false (G n string_of_cterm) ct |
230 val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct |
231 val u = Syntax.parse_term ctxt str |
231 val u = Syntax.parse_term ctxt str |
232 |> TypeInfer.constrain T |> Syntax.check_term ctxt |
232 |> TypeInfer.constrain T |> Syntax.check_term ctxt |
233 in |
233 in |
234 if match u |
234 if match u |
235 then quote str |
235 then quote str |
236 else F (n+1) |
236 else F (n+1) |
237 end |
237 end |
238 handle ERROR mesg => F (n+1) |
238 handle ERROR mesg => F (n+1) |
239 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct)) |
239 | SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 Display.string_of_cterm ct)) |
240 in |
240 in |
241 PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 |
241 PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 |
242 end |
242 end |
243 handle ERROR mesg => simple_smart_string_of_cterm ct |
243 handle ERROR mesg => simple_smart_string_of_cterm ct |
244 |
244 |
245 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
245 val smart_string_of_thm = smart_string_of_cterm o cprop_of |
246 |
246 |
247 fun prth th = writeln (PrintMode.setmp [] string_of_thm th) |
247 fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th) |
248 fun prc ct = writeln (PrintMode.setmp [] string_of_cterm ct) |
248 fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) |
249 fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ()); |
249 fun prin t = writeln (PrintMode.setmp [] (fn () => Sign.string_of_term (the_context ()) t) ()); |
250 fun pth (HOLThm(ren,thm)) = |
250 fun pth (HOLThm(ren,thm)) = |
251 let |
251 let |
252 (*val _ = writeln "Renaming:" |
252 (*val _ = writeln "Renaming:" |
253 val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*) |
253 val _ = app (fn(v,w) => (prin v; writeln " -->"; prin w)) ren*) |
1945 val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) |
1945 val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew))) |
1946 val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn |
1946 val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn |
1947 then |
1947 then |
1948 let |
1948 let |
1949 val p1 = quotename constname |
1949 val p1 = quotename constname |
1950 val p2 = string_of_ctyp (ctyp_of thy'' ctype) |
1950 val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype) |
1951 val p3 = string_of_mixfix csyn |
1951 val p3 = string_of_mixfix csyn |
1952 val p4 = smart_string_of_cterm crhs |
1952 val p4 = smart_string_of_cterm crhs |
1953 in |
1953 in |
1954 add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' |
1954 add_dump ("constdefs\n " ^p1^ " :: \"" ^p2^ "\" "^p3^ "\n " ^p4) thy'' |
1955 end |
1955 end |
1956 else |
1956 else |
1957 (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy'' ctype) ^ |
1957 (add_dump ("consts\n " ^ (quotename constname) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy'' ctype) ^ |
1958 "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) |
1958 "\" " ^ (string_of_mixfix csyn) ^ "\n\ndefs\n " ^ (quotename thmname) ^ ": " ^ (smart_string_of_cterm crhs)) |
1959 thy'') |
1959 thy'') |
1960 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of |
1960 val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of |
1961 SOME (_,res) => HOLThm(rens_of linfo,res) |
1961 SOME (_,res) => HOLThm(rens_of linfo,res) |
1962 | NONE => raise ERR "new_definition" "Bad conclusion" |
1962 | NONE => raise ERR "new_definition" "Bad conclusion" |
2015 val (_,cT,p) = dest_exists ex |
2015 val (_,cT,p) = dest_exists ex |
2016 in |
2016 in |
2017 ((cname,cT,mk_syn thy cname)::cs,p) |
2017 ((cname,cT,mk_syn thy cname)::cs,p) |
2018 end) (([],HOLogic.dest_Trueprop (concl_of th)),names) |
2018 end) (([],HOLogic.dest_Trueprop (concl_of th)),names) |
2019 val str = Library.foldl (fn (acc,(c,T,csyn)) => |
2019 val str = Library.foldl (fn (acc,(c,T,csyn)) => |
2020 acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) |
2020 acc ^ "\n " ^ (quotename c) ^ " :: \"" ^ Display.string_of_ctyp (ctyp_of thy T) ^ "\" " ^ (string_of_mixfix csyn)) ("consts",consts) |
2021 val thy' = add_dump str thy |
2021 val thy' = add_dump str thy |
2022 val _ = ImportRecorder.add_consts consts |
2022 val _ = ImportRecorder.add_consts consts |
2023 in |
2023 in |
2024 Sign.add_consts_i consts thy' |
2024 Sign.add_consts_i consts thy' |
2025 end |
2025 end |
2141 handle e => (message "exception in new_type_definition"; print_exn e) |
2141 handle e => (message "exception in new_type_definition"; print_exn e) |
2142 |
2142 |
2143 fun add_dump_constdefs thy defname constname rhs ty = |
2143 fun add_dump_constdefs thy defname constname rhs ty = |
2144 let |
2144 let |
2145 val n = quotename constname |
2145 val n = quotename constname |
2146 val t = string_of_ctyp (ctyp_of thy ty) |
2146 val t = Display.string_of_ctyp (ctyp_of thy ty) |
2147 val syn = string_of_mixfix (mk_syn thy constname) |
2147 val syn = string_of_mixfix (mk_syn thy constname) |
2148 (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) |
2148 (*val eq = smart_string_of_cterm (cterm_of thy (Const(rhs, ty)))*) |
2149 val eq = quote (constname ^ " == "^rhs) |
2149 val eq = quote (constname ^ " == "^rhs) |
2150 val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " |
2150 val d = case defname of NONE => "" | SOME defname => (quotename defname)^" : " |
2151 in |
2151 in |
2226 (string_of_mixfix tsyn) ^ " morphisms "^ |
2226 (string_of_mixfix tsyn) ^ " morphisms "^ |
2227 (quote rep_name)^" "^(quote abs_name)^"\n"^ |
2227 (quote rep_name)^" "^(quote abs_name)^"\n"^ |
2228 (" apply (rule light_ex_imp_nonempty[where t="^ |
2228 (" apply (rule light_ex_imp_nonempty[where t="^ |
2229 (proc_prop (cterm_of thy4 t))^"])\n"^ |
2229 (proc_prop (cterm_of thy4 t))^"])\n"^ |
2230 (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 |
2230 (" by (import " ^ thyname ^ " " ^ (quotename thmname) ^ ")"))) thy4 |
2231 val str_aty = string_of_ctyp (ctyp_of thy aty) |
2231 val str_aty = Display.string_of_ctyp (ctyp_of thy aty) |
2232 val thy = add_dump_syntax thy rep_name |
2232 val thy = add_dump_syntax thy rep_name |
2233 val thy = add_dump_syntax thy abs_name |
2233 val thy = add_dump_syntax thy abs_name |
2234 val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ |
2234 val thy = add_dump ("lemmas " ^ (quote (thmname^"_@intern")) ^ |
2235 " = typedef_hol2hollight \n"^ |
2235 " = typedef_hol2hollight \n"^ |
2236 " [where a=\"a :: "^str_aty^"\" and r=r" ^ |
2236 " [where a=\"a :: "^str_aty^"\" and r=r" ^ |