22 structure Constdefs: CONSTDEFS = |
22 structure Constdefs: CONSTDEFS = |
23 struct |
23 struct |
24 |
24 |
25 (** add_constdefs(_i) **) |
25 (** add_constdefs(_i) **) |
26 |
26 |
27 fun pretty_const sg (c, T) = |
27 fun pretty_const thy (c, T) = |
28 Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
28 Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
29 Pretty.quote (Sign.pretty_typ sg T)]; |
29 Pretty.quote (Sign.pretty_typ thy T)]; |
30 |
30 |
31 fun pretty_constdefs sg decls = |
31 fun pretty_constdefs thy decls = |
32 Pretty.big_list "constants" (map (pretty_const sg) decls); |
32 Pretty.big_list "constants" (map (pretty_const thy) decls); |
33 |
33 |
34 fun gen_constdef prep_typ prep_term prep_att |
34 fun gen_constdef prep_typ prep_term prep_att |
35 structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) = |
35 structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) = |
36 let |
36 let |
37 val sign = Theory.sign_of thy; |
|
38 fun err msg ts = |
37 fun err msg ts = |
39 error (cat_lines (msg :: map (Sign.string_of_term sign) ts)); |
38 error (cat_lines (msg :: map (Sign.string_of_term thy) ts)); |
40 |
39 |
41 val ctxt = |
40 val ctxt = |
42 ProofContext.init thy |> ProofContext.add_fixes |
41 ProofContext.init thy |> ProofContext.add_fixes |
43 (List.concat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs)); |
42 (List.concat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs)); |
44 val (ctxt', d, mx) = |
43 val (ctxt', d, mx) = |
58 val _ = (case d of NONE => () | SOME c' => |
57 val _ = (case d of NONE => () | SOME c' => |
59 if c <> c' then |
58 if c <> c' then |
60 err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') [] |
59 err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') [] |
61 else ()); |
60 else ()); |
62 |
61 |
63 val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop; |
62 val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop; |
64 val name = if raw_name = "" then Thm.def_name c else raw_name; |
63 val name = if raw_name = "" then Thm.def_name c else raw_name; |
65 val atts = map (prep_att thy) raw_atts; |
64 val atts = map (prep_att thy) raw_atts; |
66 |
65 |
67 val thy' = |
66 val thy' = |
68 thy |
67 thy |
73 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = |
72 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = |
74 let |
73 let |
75 val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs)); |
74 val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs)); |
76 val (thy', decls) = (thy, specs) |
75 val (thy', decls) = (thy, specs) |
77 |> foldl_map (gen_constdef prep_typ prep_term prep_att structs); |
76 |> foldl_map (gen_constdef prep_typ prep_term prep_att structs); |
78 in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end; |
77 in Pretty.writeln (pretty_constdefs thy' decls); thy' end; |
79 |
78 |
80 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal |
79 val add_constdefs = gen_constdefs ProofContext.read_vars_liberal |
81 ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute; |
80 ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute; |
82 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal |
81 val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal |
83 ProofContext.cert_typ ProofContext.cert_term (K I); |
82 ProofContext.cert_typ ProofContext.cert_term (K I); |