6 polymorphism. |
6 polymorphism. |
7 *) |
7 *) |
8 |
8 |
9 signature SPECIFICATION = |
9 signature SPECIFICATION = |
10 sig |
10 sig |
11 val pretty_consts: theory -> (string * typ) list -> Pretty.T |
11 val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T |
12 val read_specification: |
12 val read_specification: |
13 (string * string option * mixfix) list * ((string * Attrib.src list) * string list) list -> |
13 (string * string option * mixfix) list * |
14 Proof.context -> |
14 ((string * Attrib.src list) * string list) list -> Proof.context -> |
15 ((string * typ * mixfix) list * ((string * theory attribute list) * term list) list) * |
15 ((string * typ * mixfix) list * |
16 Proof.context |
16 ((string * Context.generic attribute list) * term list) list) * Proof.context |
17 val cert_specification: |
17 val cert_specification: |
18 (string * typ option * mixfix) list * ((string * theory attribute list) * term list) list -> |
18 (string * typ option * mixfix) list * |
19 Proof.context -> |
19 ((string * Context.generic attribute list) * term list) list -> Proof.context -> |
20 ((string * typ * mixfix) list * ((string * theory attribute list) * term list) list) * |
20 ((string * typ * mixfix) list * |
21 Proof.context |
21 ((string * Context.generic attribute list) * term list) list) * Proof.context |
22 val axiomatize: |
22 val axiomatize: |
23 (string * string option * mixfix) list * ((bstring * Attrib.src list) * string list) list -> |
23 (string * string option * mixfix) list * |
24 theory -> thm list list * theory |
24 ((bstring * Attrib.src list) * string list) list -> theory -> thm list list * theory |
25 val axiomatize_i: |
25 val axiomatize_i: |
26 (string * typ option * mixfix) list * ((bstring * theory attribute list) * term list) list -> |
26 (string * typ option * mixfix) list * |
27 theory -> thm list list * theory |
27 ((bstring * Context.generic attribute list) * term list) list -> theory -> |
|
28 thm list list * theory |
28 end; |
29 end; |
29 |
30 |
30 structure Specification: SPECIFICATION = |
31 structure Specification: SPECIFICATION = |
31 struct |
32 struct |
32 |
33 |
33 (* pretty_consts *) |
34 (* pretty_consts *) |
34 |
35 |
35 fun pretty_const thy (c, T) = |
36 fun pretty_const ctxt (c, T) = |
36 Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
37 Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, |
37 Pretty.quote (Sign.pretty_typ thy T)]; |
38 Pretty.quote (ProofContext.pretty_typ ctxt T)]; |
38 |
39 |
39 fun pretty_consts thy decls = |
40 fun pretty_consts ctxt decls = |
40 Pretty.big_list "constants" (map (pretty_const thy) decls); |
41 Pretty.big_list "constants" (map (pretty_const ctxt) decls); |
41 |
42 |
42 |
43 |
43 (* prepare specification *) |
44 (* prepare specification *) |
44 |
45 |
45 fun prep_specification prep_typ prep_propp prep_att |
46 fun prep_specification prep_typ prep_propp prep_att |
62 val names = map (fst o fst) raw_specs; |
63 val names = map (fst o fst) raw_specs; |
63 val atts = map (map (prep_att (ProofContext.theory_of context)) o snd o fst) raw_specs; |
64 val atts = map (map (prep_att (ProofContext.theory_of context)) o snd o fst) raw_specs; |
64 in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
65 in ((params, (names ~~ atts) ~~ specs), specs_ctxt) end; |
65 |
66 |
66 fun read_specification x = |
67 fun read_specification x = |
67 prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.global_attribute x; |
68 prep_specification ProofContext.read_typ ProofContext.read_propp Attrib.generic_attribute x; |
68 fun cert_specification x = |
69 fun cert_specification x = |
69 prep_specification ProofContext.cert_typ ProofContext.cert_propp (K I) x; |
70 prep_specification ProofContext.cert_typ ProofContext.cert_propp (K I) x; |
70 |
71 |
71 |
72 |
72 (* axiomatize *) |
73 (* axiomatize *) |
73 |
74 |
74 fun gen_axiomatize prep args thy = |
75 fun gen_axiomatize prep args thy = |
75 let |
76 let |
76 val ((consts, specs), ctxt) = prep args (ProofContext.init thy); |
77 val ((consts, specs), ctxt) = prep args (ProofContext.init thy); |
77 val subst = map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T))) consts; |
78 val subst = consts |> map (fn (x, T, _) => (Free (x, T), Const (Sign.full_name thy x, T))); |
78 val axioms = |
79 val axioms = specs |> map (fn ((name, att), ts) => |
79 map (fn ((name, att), ts) => ((name, map (Term.subst_atomic subst) ts), att)) specs; |
80 ((name, map (Term.subst_atomic subst) ts), map Attrib.theory att)); |
80 val (thms, thy') = |
81 val (thms, thy') = |
81 thy |
82 thy |
82 |> Theory.add_consts_i consts |
83 |> Theory.add_consts_i consts |
83 |> PureThy.add_axiomss_i axioms |
84 |> PureThy.add_axiomss_i axioms |
84 ||> Theory.add_finals_i false (map snd subst); |
85 ||> Theory.add_finals_i false (map snd subst); |
85 in Pretty.writeln (pretty_consts thy' (map (dest_Free o fst) subst)); (thms, thy') end; |
86 in Pretty.writeln (pretty_consts ctxt (map (dest_Free o fst) subst)); (thms, thy') end; |
86 |
87 |
87 val axiomatize = gen_axiomatize read_specification; |
88 val axiomatize = gen_axiomatize read_specification; |
88 val axiomatize_i = gen_axiomatize cert_specification; |
89 val axiomatize_i = gen_axiomatize cert_specification; |
89 |
90 |
90 end; |
91 end; |