wenzelm@14657
|
1 |
(* Title: Pure/Isar/constdefs.ML
|
wenzelm@14657
|
2 |
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
|
wenzelm@14657
|
3 |
|
wenzelm@18779
|
4 |
Old-style constant definitions, with type-inference and optional
|
wenzelm@14657
|
5 |
structure context; specifications need to observe strictly sequential
|
wenzelm@14657
|
6 |
dependencies; no support for overloading.
|
wenzelm@14657
|
7 |
*)
|
wenzelm@14657
|
8 |
|
wenzelm@14657
|
9 |
signature CONSTDEFS =
|
wenzelm@14657
|
10 |
sig
|
haftmann@28965
|
11 |
val add_constdefs: (Binding.T * string option) list *
|
haftmann@28965
|
12 |
((Binding.T * string option * mixfix) option *
|
wenzelm@28084
|
13 |
(Attrib.binding * string)) list -> theory -> theory
|
haftmann@28965
|
14 |
val add_constdefs_i: (Binding.T * typ option) list *
|
haftmann@28965
|
15 |
((Binding.T * typ option * mixfix) option *
|
haftmann@28965
|
16 |
((Binding.T * attribute list) * term)) list -> theory -> theory
|
wenzelm@14657
|
17 |
end;
|
wenzelm@14657
|
18 |
|
wenzelm@14657
|
19 |
structure Constdefs: CONSTDEFS =
|
wenzelm@14657
|
20 |
struct
|
wenzelm@14657
|
21 |
|
wenzelm@14657
|
22 |
(** add_constdefs(_i) **)
|
wenzelm@14657
|
23 |
|
wenzelm@22710
|
24 |
fun gen_constdef prep_vars prep_prop prep_att
|
wenzelm@18668
|
25 |
structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy =
|
wenzelm@14657
|
26 |
let
|
wenzelm@26939
|
27 |
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts));
|
wenzelm@14664
|
28 |
|
wenzelm@18948
|
29 |
val thy_ctxt = ProofContext.init thy;
|
wenzelm@18948
|
30 |
val struct_ctxt = #2 (ProofContext.add_fixes_i structs thy_ctxt);
|
wenzelm@18948
|
31 |
val ((d, mx), var_ctxt) =
|
wenzelm@18668
|
32 |
(case raw_decl of
|
wenzelm@18948
|
33 |
NONE => ((NONE, NoSyn), struct_ctxt)
|
wenzelm@18668
|
34 |
| SOME raw_var =>
|
wenzelm@18948
|
35 |
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] =>
|
wenzelm@25352
|
36 |
ProofContext.add_fixes_i [(x, T, mx)] #> snd #> pair (SOME x, mx)));
|
wenzelm@14657
|
37 |
|
wenzelm@22710
|
38 |
val prop = prep_prop var_ctxt raw_prop;
|
wenzelm@18948
|
39 |
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
|
wenzelm@28083
|
40 |
val _ =
|
wenzelm@28083
|
41 |
(case Option.map Name.name_of d of
|
wenzelm@28083
|
42 |
NONE => ()
|
wenzelm@28083
|
43 |
| SOME c' =>
|
wenzelm@28083
|
44 |
if c <> c' then
|
wenzelm@28083
|
45 |
err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
|
wenzelm@28083
|
46 |
else ());
|
wenzelm@14657
|
47 |
|
haftmann@28965
|
48 |
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
|
wenzelm@28083
|
49 |
val name = Thm.def_name_optional c (Name.name_of raw_name);
|
wenzelm@14657
|
50 |
val atts = map (prep_att thy) raw_atts;
|
wenzelm@14664
|
51 |
|
wenzelm@14664
|
52 |
val thy' =
|
wenzelm@14664
|
53 |
thy
|
wenzelm@22796
|
54 |
|> Sign.add_consts_i [(c, T, mx)]
|
haftmann@27691
|
55 |
|> PureThy.add_defs false [((name, def), atts)]
|
haftmann@28370
|
56 |
|-> (fn [thm] => Code.add_default_eqn thm);
|
wenzelm@17853
|
57 |
in ((c, T), thy') end;
|
wenzelm@14657
|
58 |
|
wenzelm@22710
|
59 |
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
|
wenzelm@14664
|
60 |
let
|
wenzelm@18638
|
61 |
val ctxt = ProofContext.init thy;
|
wenzelm@18668
|
62 |
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt;
|
wenzelm@22710
|
63 |
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy;
|
wenzelm@20885
|
64 |
in Pretty.writeln (ProofDisplay.pretty_consts ctxt (K true) decls); thy' end;
|
wenzelm@14657
|
65 |
|
wenzelm@25352
|
66 |
val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute;
|
wenzelm@25352
|
67 |
val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I);
|
wenzelm@14657
|
68 |
|
wenzelm@14657
|
69 |
end;
|