author | wenzelm |
Wed, 25 Jan 2006 00:21:37 +0100 | |
changeset 18779 | a9f41c380b2f |
parent 18765 | 97911ffe9222 |
child 18873 | 11c92ec2c29c |
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 |
ID: $Id$ |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
4 |
|
18779 | 5 |
Old-style constant definitions, with type-inference and optional |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
6 |
structure context; specifications need to observe strictly sequential |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
7 |
dependencies; no support for overloading. |
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 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
10 |
signature CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
11 |
sig |
18668 | 12 |
val add_constdefs: (string * string option) list * |
13 |
((bstring * string option * mixfix) option * ((bstring * Attrib.src list) * string)) list -> |
|
14 |
theory -> theory |
|
15 |
val add_constdefs_i: (string * typ option) list * |
|
18728 | 16 |
((bstring * typ option * mixfix) option * ((bstring * attribute list) * term)) list -> |
18668 | 17 |
theory -> theory |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
18 |
end; |
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 |
structure Constdefs: CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
21 |
struct |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
22 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
23 |
(** add_constdefs(_i) **) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
24 |
|
18668 | 25 |
fun gen_constdef prep_vars prep_term prep_att |
26 |
structs (raw_decl, ((raw_name, raw_atts), raw_prop)) thy = |
|
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
27 |
let |
14664 | 28 |
fun err msg ts = |
17065 | 29 |
error (cat_lines (msg :: map (Sign.string_of_term thy) ts)); |
14664 | 30 |
|
18668 | 31 |
val (_, ctxt) = thy |> ProofContext.init |> ProofContext.add_fixes_i structs; |
32 |
val ((d, mx), ctxt') = |
|
33 |
(case raw_decl of |
|
34 |
NONE => ((NONE, NoSyn), ctxt) |
|
35 |
| SOME raw_var => |
|
36 |
ctxt |> prep_vars [raw_var] |-> (fn [(x, T, mx)] => |
|
37 |
ProofContext.add_fixes_legacy [(x, T, mx)] #> snd #> pair (SOME x, mx))); |
|
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
38 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
39 |
val prop = prep_term ctxt' raw_prop; |
14664 | 40 |
val concl = Logic.strip_imp_concl prop; |
41 |
val (lhs, _) = Logic.dest_equals concl handle TERM _ => |
|
42 |
err "Not a meta-equality (==):" [concl]; |
|
43 |
val head = Term.head_of lhs; |
|
44 |
val (c, T) = Term.dest_Free head handle TERM _ => |
|
45 |
err "Locally fixed variable required as head of definition:" [head]; |
|
15531 | 46 |
val _ = (case d of NONE => () | SOME c' => |
14719 | 47 |
if c <> c' then |
48 |
err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') [] |
|
14664 | 49 |
else ()); |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
50 |
|
17065 | 51 |
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name thy c, T))] prop; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
52 |
val name = if raw_name = "" then Thm.def_name c else raw_name; |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
53 |
val atts = map (prep_att thy) raw_atts; |
14664 | 54 |
|
55 |
val thy' = |
|
56 |
thy |
|
57 |
|> Theory.add_consts_i [(c, T, mx)] |
|
18668 | 58 |
|> PureThy.add_defs_i false [((name, def), atts)] |> snd; |
17853 | 59 |
in ((c, T), thy') end; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
60 |
|
18668 | 61 |
fun gen_constdefs prep_vars prep_term 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; |
65 |
val (decls, thy') = fold_map (gen_constdef prep_vars prep_term prep_att structs) specs thy; |
|
18765 | 66 |
in Pretty.writeln (LocalTheory.pretty_consts ctxt decls); thy' end; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
67 |
|
18668 | 68 |
val add_constdefs = gen_constdefs ProofContext.read_vars_legacy |
18728 | 69 |
ProofContext.read_term_legacy Attrib.attribute; |
18668 | 70 |
val add_constdefs_i = gen_constdefs ProofContext.cert_vars_legacy ProofContext.cert_term (K I); |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
71 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
72 |
end; |