author | berghofe |
Fri, 15 Jan 2010 13:37:41 +0100 | |
changeset 34916 | f625d8d6fcf3 |
parent 33756 | 47b7c9e0bf6e |
child 35624 | c4e29a0bb8c1 |
permissions | -rw-r--r-- |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/constdefs.ML |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
3 |
|
18779 | 4 |
Old-style constant definitions, with type-inference and optional |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
5 |
structure context; specifications need to observe strictly sequential |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
6 |
dependencies; no support for overloading. |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
7 |
*) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
8 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
9 |
signature CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
10 |
sig |
29579 | 11 |
val add_constdefs: (binding * string option) list * |
30211 | 12 |
((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory |
29579 | 13 |
val add_constdefs_i: (binding * typ option) list * |
30211 | 14 |
((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
15 |
end; |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
16 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
17 |
structure Constdefs: CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
18 |
struct |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
19 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
20 |
(** add_constdefs(_i) **) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
21 |
|
22710 | 22 |
fun gen_constdef prep_vars prep_prop prep_att |
18668 | 23 |
structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy = |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
24 |
let |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
25352
diff
changeset
|
25 |
fun err msg ts = error (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); |
14664 | 26 |
|
18948 | 27 |
val thy_ctxt = ProofContext.init thy; |
30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30585
diff
changeset
|
28 |
val struct_ctxt = #2 (ProofContext.add_fixes structs thy_ctxt); |
18948 | 29 |
val ((d, mx), var_ctxt) = |
18668 | 30 |
(case raw_decl of |
18948 | 31 |
NONE => ((NONE, NoSyn), struct_ctxt) |
18668 | 32 |
| SOME raw_var => |
18948 | 33 |
struct_ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] => |
30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30585
diff
changeset
|
34 |
ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx))); |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
35 |
|
22710 | 36 |
val prop = prep_prop var_ctxt raw_prop; |
18948 | 37 |
val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop)); |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
38 |
val _ = |
30585
6b2ba4666336
use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
wenzelm
parents:
30434
diff
changeset
|
39 |
(case Option.map Name.of_binding d of |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
40 |
NONE => () |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
41 |
| SOME c' => |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
42 |
if c <> c' then |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
43 |
err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') [] |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27691
diff
changeset
|
44 |
else ()); |
30434 | 45 |
val b = Binding.name c; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
46 |
|
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset
|
47 |
val head = Const (Sign.full_bname thy c, T); |
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset
|
48 |
val def = Term.subst_atomic [(Free (c, T), head)] prop; |
30434 | 49 |
val name = Thm.def_binding_optional b raw_name; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
50 |
val atts = map (prep_att thy) raw_atts; |
14664 | 51 |
|
52 |
val thy' = |
|
53 |
thy |
|
30434 | 54 |
|> Sign.add_consts_i [(b, T, mx)] |
30344
10a67c5ddddb
more uniform handling of binding in targets and derived elements;
wenzelm
parents:
30242
diff
changeset
|
55 |
|> PureThy.add_defs false [((name, def), atts)] |
33455
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset
|
56 |
|-> (fn [thm] => (* FIXME thm vs. atts !? *) |
4da71b27b3fe
declare Spec_Rules for most basic definitional packages;
wenzelm
parents:
33389
diff
changeset
|
57 |
Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #> |
33756
47b7c9e0bf6e
replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules
bulwahn
parents:
33455
diff
changeset
|
58 |
Code.add_default_eqn thm); |
17853 | 59 |
in ((c, T), thy') end; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
60 |
|
22710 | 61 |
fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = |
14664 | 62 |
let |
18638 | 63 |
val ctxt = ProofContext.init thy; |
18668 | 64 |
val (structs, _) = prep_vars (map (fn (x, T) => (x, T, Structure)) raw_structs) ctxt; |
22710 | 65 |
val (decls, thy') = fold_map (gen_constdef prep_vars prep_prop prep_att structs) specs thy; |
33389 | 66 |
in Pretty.writeln (Proof_Display.pretty_consts ctxt (K true) decls); thy' end; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
67 |
|
25352 | 68 |
val add_constdefs = gen_constdefs ProofContext.read_vars Syntax.read_prop Attrib.attribute; |
69 |
val add_constdefs_i = gen_constdefs ProofContext.cert_vars ProofContext.cert_prop (K I); |
|
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
70 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
71 |
end; |