23 structure Constdefs: CONSTDEFS = |
23 structure Constdefs: CONSTDEFS = |
24 struct |
24 struct |
25 |
25 |
26 (** add_constdefs(_i) **) |
26 (** add_constdefs(_i) **) |
27 |
27 |
|
28 fun pretty_const sg (c, T) = |
|
29 Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
|
30 Pretty.quote (Sign.pretty_typ sg T)]; |
|
31 |
|
32 fun pretty_constdefs sg decls = |
|
33 Pretty.big_list "constants" (map (pretty_const sg) decls); |
|
34 |
28 fun gen_constdef prep_typ prep_term prep_att |
35 fun gen_constdef prep_typ prep_term prep_att |
29 structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) = |
36 structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) = |
30 let |
37 let |
|
38 val sign = Theory.sign_of thy; |
|
39 fun err msg ts = |
|
40 error (cat_lines (msg :: map (Sign.string_of_term sign) ts)); |
|
41 |
31 val ctxt = |
42 val ctxt = |
32 ProofContext.init thy |> ProofContext.add_fixes |
43 ProofContext.init thy |> ProofContext.add_fixes |
33 (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs)); |
44 (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs)); |
34 val (ctxt', mx) = |
45 val (ctxt', mx) = |
35 (case decl of None => (ctxt, Syntax.NoSyn) | Some (x, raw_T, mx) => |
46 (case decl of None => (ctxt, Syntax.NoSyn) | Some (x, raw_T, mx) => |
36 (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx)); |
47 (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx)); |
37 |
48 |
38 val prop = prep_term ctxt' raw_prop; |
49 val prop = prep_term ctxt' raw_prop; |
39 fun err msg = raise TERM (msg, [prop]); |
50 val concl = Logic.strip_imp_concl prop; |
|
51 val (lhs, _) = Logic.dest_equals concl handle TERM _ => |
|
52 err "Not a meta-equality (==):" [concl]; |
|
53 val head = Term.head_of lhs; |
|
54 val (c, T) = Term.dest_Free head handle TERM _ => |
|
55 err "Locally fixed variable required as head of definition:" [head]; |
|
56 val _ = (case decl of None => () | Some (d, _, _) => |
|
57 if c <> d then |
|
58 err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d) [] |
|
59 else ()); |
40 |
60 |
41 val (lhs, _) = Logic.dest_equals (Logic.strip_imp_concl prop) |
61 val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop; |
42 handle TERM _ => err "Not a meta-equality (==)"; |
|
43 val (c, T) = Term.dest_Free (Term.head_of lhs) |
|
44 handle TERM _ => err "Head of definition needs to turn out as fixed variable"; |
|
45 val _ = (case decl of None => () | Some (d, _, _) => |
|
46 if c = d then () |
|
47 else err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d)); |
|
48 |
|
49 val full = Sign.full_name (Theory.sign_of thy); |
|
50 val def = Term.subst_atomic [(Free (c, T), Const (full c, T))] prop; |
|
51 val name = if raw_name = "" then Thm.def_name c else raw_name; |
62 val name = if raw_name = "" then Thm.def_name c else raw_name; |
52 val atts = map (prep_att thy) raw_atts; |
63 val atts = map (prep_att thy) raw_atts; |
53 in |
64 |
54 thy |
65 val thy' = |
55 |> Theory.add_consts_i [(c, T, mx)] |
66 thy |
56 |> PureThy.add_defs_i false [((name, def), atts)] |> #1 |
67 |> Theory.add_consts_i [(c, T, mx)] |
57 end; |
68 |> PureThy.add_defs_i false [((name, def), atts)] |> #1; |
|
69 in (thy', (c, T)) end; |
58 |
70 |
59 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = |
71 fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = |
60 let val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs)) |
72 let |
61 in foldl (gen_constdef prep_typ prep_term prep_att structs) (thy, specs) end; |
73 val structs = #2 (foldl_map prep_vars (ProofContext.init thy, raw_structs)); |
|
74 val (thy', decls) = (thy, specs) |
|
75 |> foldl_map (gen_constdef prep_typ prep_term prep_att structs); |
|
76 in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end; |
62 |
77 |
63 val add_constdefs = gen_constdefs ProofContext.read_vars |
78 val add_constdefs = gen_constdefs ProofContext.read_vars |
64 ProofContext.read_typ ProofContext.read_term Attrib.global_attribute; |
79 ProofContext.read_typ ProofContext.read_term Attrib.global_attribute; |
65 val add_constdefs_i = gen_constdefs ProofContext.cert_vars |
80 val add_constdefs_i = gen_constdefs ProofContext.cert_vars |
66 ProofContext.cert_typ ProofContext.cert_term (K I); |
81 ProofContext.cert_typ ProofContext.cert_term (K I); |