author | wenzelm |
Tue, 24 Jan 2006 00:43:34 +0100 | |
changeset 18771 | 63efe00371af |
parent 18728 | 6790126ab5f6 |
child 18786 | 591a37d48794 |
permissions | -rw-r--r-- |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/specification.ML |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
3 |
Author: Makarius |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
4 |
|
18771 | 5 |
Common theory/locale specifications --- with type-inference, but |
6 |
without internal polymorphism. |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
7 |
*) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
8 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
9 |
signature SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
10 |
sig |
18771 | 11 |
val read_specification: (string * string option * mixfix) list -> |
12 |
((string * Attrib.src list) * string list) list -> Proof.context -> |
|
13 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
|
14 |
Proof.context |
|
15 |
val cert_specification: (string * typ option * mixfix) list -> |
|
16 |
((string * Attrib.src list) * term list) list -> Proof.context -> |
|
17 |
(((string * typ) * mixfix) list * ((string * Attrib.src list) * term list) list) * |
|
18 |
Proof.context |
|
19 |
val axiomatization: xstring option -> (string * string option * mixfix) list -> |
|
20 |
((bstring * Attrib.src list) * string list) list -> theory -> |
|
21 |
(term list * (bstring * thm list) list) * (theory * Proof.context) |
|
22 |
val axiomatization_i: string option -> (string * typ option * mixfix) list -> |
|
23 |
((bstring * Attrib.src list) * term list) list -> theory -> |
|
24 |
(term list * (bstring * thm list) list) * (theory * Proof.context) |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
25 |
end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
26 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
27 |
structure Specification: SPECIFICATION = |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
28 |
struct |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
29 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
30 |
(* prepare specification *) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
31 |
|
18670 | 32 |
fun prep_specification prep_vars prep_propp prep_att |
18771 | 33 |
raw_vars raw_specs ctxt = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
34 |
let |
18670 | 35 |
val thy = ProofContext.theory_of ctxt; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
36 |
|
18670 | 37 |
val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars; |
38 |
val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars; |
|
39 |
val ((specs, vs), specs_ctxt) = |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
40 |
prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs) |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
41 |
|> swap |>> map (map fst) |
18771 | 42 |
||>> fold_map ProofContext.inferred_param xs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
43 |
|
18771 | 44 |
val params = vs ~~ map #3 vars; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
45 |
val names = map (fst o fst) raw_specs; |
18670 | 46 |
val atts = map (map (prep_att thy) o snd o fst) raw_specs; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
47 |
in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
48 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
49 |
fun read_specification x = |
18771 | 50 |
prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
51 |
fun cert_specification x = |
18670 | 52 |
prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x; |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
53 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
54 |
|
18771 | 55 |
(* axiomatization *) |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
56 |
|
18771 | 57 |
fun gen_axiomatization prep init locale raw_vars raw_specs thy = |
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
58 |
let |
18771 | 59 |
val ((vars, specs), ctxt) = init locale thy |> prep raw_vars raw_specs; |
60 |
val (consts, consts_ctxt) = ctxt |> LocalTheory.consts vars; |
|
61 |
val subst = Term.subst_atomic (map (Free o fst) vars ~~ consts); |
|
62 |
val (axioms, axioms_ctxt) = |
|
63 |
consts_ctxt |
|
64 |
|> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props))) |
|
65 |
||> LocalTheory.map_theory (Theory.add_finals_i false (map Term.head_of consts)); |
|
66 |
val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars)); |
|
67 |
in ((consts, axioms), `LocalTheory.exit axioms_ctxt) end; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
68 |
|
18771 | 69 |
val axiomatization = gen_axiomatization read_specification LocalTheory.init; |
70 |
val axiomatization_i = gen_axiomatization cert_specification LocalTheory.init_i; |
|
18620
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
71 |
|
fc8b5f275359
Theory specifications --- with type-inference, but no internal polymorphism.
wenzelm
parents:
diff
changeset
|
72 |
end; |