author | aspinall |
Fri, 07 May 2004 13:34:13 +0200 | |
changeset 14712 | 81362115cedd |
parent 14664 | 148f6175fa78 |
child 14719 | d1157ff6ffcb |
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 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
5 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
6 |
Standard constant definitions, with type-inference and optional |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
7 |
structure context; specifications need to observe strictly sequential |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
8 |
dependencies; no support for overloading. |
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 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
11 |
signature CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
12 |
sig |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
13 |
val add_constdefs: (string list * string option) list * |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
14 |
((bstring * string option * Syntax.mixfix) option * |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
15 |
((bstring * Args.src list) * string)) list |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
16 |
-> theory -> theory |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
17 |
val add_constdefs_i: (string list * typ option) list * |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
18 |
((bstring * typ option * Syntax.mixfix) option * |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
19 |
((bstring * theory attribute list) * term)) list |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
20 |
-> theory -> theory |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
21 |
end; |
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 |
structure Constdefs: CONSTDEFS = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
24 |
struct |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
25 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
26 |
(** add_constdefs(_i) **) |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
27 |
|
14664 | 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 |
||
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
35 |
fun gen_constdef prep_typ prep_term prep_att |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
36 |
structs (thy, (decl, ((raw_name, raw_atts), raw_prop))) = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
37 |
let |
14664 | 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 |
||
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
42 |
val ctxt = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
43 |
ProofContext.init thy |> ProofContext.add_fixes |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
44 |
(flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs)); |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
45 |
val (ctxt', mx) = |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
46 |
(case decl of None => (ctxt, Syntax.NoSyn) | Some (x, raw_T, mx) => |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
47 |
(ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx)); |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
48 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
49 |
val prop = prep_term ctxt' raw_prop; |
14664 | 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 ()); |
|
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
60 |
|
14664 | 61 |
val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop; |
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
62 |
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
|
63 |
val atts = map (prep_att thy) raw_atts; |
14664 | 64 |
|
65 |
val thy' = |
|
66 |
thy |
|
67 |
|> Theory.add_consts_i [(c, T, mx)] |
|
68 |
|> PureThy.add_defs_i false [((name, def), atts)] |> #1; |
|
69 |
in (thy', (c, T)) end; |
|
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 |
fun gen_constdefs prep_vars prep_typ prep_term prep_att (raw_structs, specs) thy = |
14664 | 72 |
let |
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; |
|
14657
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
77 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
78 |
val add_constdefs = gen_constdefs ProofContext.read_vars |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
79 |
ProofContext.read_typ ProofContext.read_term Attrib.global_attribute; |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
80 |
val add_constdefs_i = gen_constdefs ProofContext.cert_vars |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
81 |
ProofContext.cert_typ ProofContext.cert_term (K I); |
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
82 |
|
c7cc01735801
'constdefs' with automatic type-inference and structure context;
wenzelm
parents:
diff
changeset
|
83 |
end; |