author | wenzelm |
Tue, 09 Oct 2007 17:10:44 +0200 | |
changeset 24931 | e0a2c154df26 |
parent 24848 | 5dbbd33c3236 |
child 24984 | 952045a8dcf2 |
permissions | -rw-r--r-- |
24592 | 1 |
(* Title: Pure/Isar/instance.ML |
2 |
ID: $Id$ |
|
3 |
Author: Florian Haftmann, TU Muenchen |
|
4 |
||
5 |
User-level instantiation interface for classes. |
|
6 |
FIXME not operative for the moment |
|
7 |
*) |
|
8 |
||
9 |
signature INSTANCE = |
|
10 |
sig |
|
11 |
val begin_instantiation: arity list -> theory -> local_theory |
|
12 |
val begin_instantiation_cmd: (xstring * string list * string) list |
|
13 |
-> theory -> local_theory |
|
14 |
val proof_instantiation: local_theory -> Proof.state |
|
15 |
end; |
|
16 |
||
17 |
structure Instance : INSTANCE = |
|
18 |
struct |
|
19 |
||
24713 | 20 |
structure Instantiation = ProofDataFun |
21 |
( |
|
24592 | 22 |
type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list; |
23 |
fun init _ = ([], []); |
|
24713 | 24 |
); |
24592 | 25 |
|
26 |
local |
|
27 |
||
28 |
fun gen_begin_instantiation prep_arity raw_arities thy = |
|
29 |
let |
|
30 |
fun prep_arity' raw_arity names = |
|
31 |
let |
|
32 |
val arity as (tyco, sorts, sort) = prep_arity thy raw_arity; |
|
24848 | 33 |
val vs = Name.invents names Name.aT (length sorts); |
34 |
val names' = fold Name.declare vs names; |
|
24592 | 35 |
in (((tyco, vs ~~ sorts), sort), names') end; |
36 |
val (arities, _) = fold_map prep_arity' raw_arities Name.context; |
|
37 |
fun get_param tyco ty_subst (param, (c, ty)) = |
|
38 |
((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty), |
|
39 |
Class.unoverload_const thy (c, ty)); |
|
40 |
fun get_params ((tyco, vs), sort) = |
|
41 |
Class.params_of_sort thy sort |
|
42 |
|> map (get_param tyco (Type (tyco, map TFree vs))); |
|
43 |
val params = maps get_params arities; |
|
44 |
val ctxt = |
|
45 |
ProofContext.init thy |
|
46 |
|> Instantiation.put (arities, params); |
|
47 |
val thy_target = TheoryTarget.begin "" ctxt; |
|
48 |
val operations = { |
|
49 |
pretty = LocalTheory.pretty, |
|
50 |
consts = LocalTheory.consts, |
|
51 |
axioms = LocalTheory.axioms, |
|
52 |
abbrev = LocalTheory.abbrev, |
|
24931
e0a2c154df26
removed LocalTheory.defs/target_morphism operations;
wenzelm
parents:
24848
diff
changeset
|
53 |
def = LocalTheory.def, |
24592 | 54 |
notes = LocalTheory.notes, |
55 |
type_syntax = LocalTheory.type_syntax, |
|
56 |
term_syntax = LocalTheory.term_syntax, |
|
57 |
declaration = LocalTheory.pretty, |
|
58 |
target_naming = LocalTheory.target_naming, |
|
59 |
reinit = LocalTheory.reinit, |
|
60 |
exit = LocalTheory.exit |
|
61 |
}; |
|
62 |
in TheoryTarget.begin "" ctxt end; |
|
63 |
||
64 |
in |
|
65 |
||
66 |
val begin_instantiation = gen_begin_instantiation Sign.cert_arity; |
|
67 |
val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity; |
|
68 |
||
69 |
end; |
|
70 |
||
71 |
fun gen_proof_instantiation do_proof after_qed lthy = |
|
72 |
let |
|
73 |
val ctxt = LocalTheory.target_of lthy; |
|
74 |
val arities = case Instantiation.get ctxt |
|
75 |
of ([], _) => error "no instantiation target" |
|
76 |
| (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities; |
|
77 |
val thy = ProofContext.theory_of ctxt; |
|
78 |
in (do_proof after_qed arities) thy end; |
|
79 |
||
80 |
val proof_instantiation = gen_proof_instantiation Class.instance_arity I; |
|
81 |
||
82 |
end; |