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) =
|
25002
|
41 |
Class.these_params thy sort
|
24592
|
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 |
axioms = LocalTheory.axioms,
|
|
51 |
abbrev = LocalTheory.abbrev,
|
25016
|
52 |
define = LocalTheory.define,
|
24592
|
53 |
notes = LocalTheory.notes,
|
|
54 |
type_syntax = LocalTheory.type_syntax,
|
|
55 |
term_syntax = LocalTheory.term_syntax,
|
|
56 |
declaration = LocalTheory.pretty,
|
|
57 |
reinit = LocalTheory.reinit,
|
|
58 |
exit = LocalTheory.exit
|
|
59 |
};
|
|
60 |
in TheoryTarget.begin "" ctxt end;
|
|
61 |
|
|
62 |
in
|
|
63 |
|
|
64 |
val begin_instantiation = gen_begin_instantiation Sign.cert_arity;
|
|
65 |
val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity;
|
|
66 |
|
|
67 |
end;
|
|
68 |
|
|
69 |
fun gen_proof_instantiation do_proof after_qed lthy =
|
|
70 |
let
|
|
71 |
val ctxt = LocalTheory.target_of lthy;
|
|
72 |
val arities = case Instantiation.get ctxt
|
|
73 |
of ([], _) => error "no instantiation target"
|
|
74 |
| (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities;
|
|
75 |
val thy = ProofContext.theory_of ctxt;
|
|
76 |
in (do_proof after_qed arities) thy end;
|
|
77 |
|
|
78 |
val proof_instantiation = gen_proof_instantiation Class.instance_arity I;
|
|
79 |
|
|
80 |
end;
|