19884
|
1 |
(* Title: Pure/Tools/codegen_simtype.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Axiomatic extension of code generator: implement ("simulate") types
|
|
6 |
by other type expressions. Requires user proof but does not use
|
|
7 |
the proven theorems!
|
|
8 |
*)
|
|
9 |
|
|
10 |
signature CODEGEN_SIMTYPE =
|
|
11 |
sig
|
|
12 |
end;
|
|
13 |
|
|
14 |
structure CodegenSimtype: CODEGEN_SIMTYPE =
|
|
15 |
struct
|
|
16 |
|
|
17 |
local
|
|
18 |
|
|
19 |
fun gen_simtype prep_term do_proof (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe thy =
|
|
20 |
let
|
|
21 |
val repm = prep_term thy raw_repm;
|
|
22 |
val absm = prep_term thy raw_absm;
|
|
23 |
val repi = prep_term thy raw_repi;
|
|
24 |
val absi = prep_term thy raw_absi;
|
|
25 |
val (repe, repe_ty) = (dest_Const o prep_term thy) raw_repe;
|
|
26 |
val repe_ty' = (snd o strip_type) repe_ty;
|
|
27 |
fun dest_fun (ty as Type (_, [ty1, ty2])) =
|
|
28 |
if is_funtype ty then (ty1, ty2)
|
|
29 |
else raise TYPE ("dest_fun", [ty], [])
|
|
30 |
| dest_fun ty = raise TYPE ("dest_fun", [ty], []);
|
|
31 |
val PROP = ObjectLogic.ensure_propT thy
|
20105
|
32 |
val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;
|
19884
|
33 |
val (tyco_abs, ty_parms) = dest_Type ty_abs;
|
|
34 |
val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else ();
|
|
35 |
val repv = Free ("x", ty_rep);
|
|
36 |
val absv = Free ("x", ty_abs);
|
|
37 |
val rep_mor = Logic.mk_implies
|
|
38 |
(PROP (absi $ absv), Logic.mk_equals (absm $ (repm $ absv), absv));
|
|
39 |
val abs_mor = Logic.mk_implies
|
|
40 |
(PROP (repi $ repv), PROP (Const (repe, ty_rep --> ty_rep --> repe_ty') $ (repm $ (absm $ repv)) $ repv));
|
|
41 |
val rep_inv = Logic.mk_implies
|
|
42 |
(PROP (absi $ absv), PROP (repi $ (repm $ absv)));
|
|
43 |
val abs_inv = Logic.mk_implies
|
|
44 |
(PROP (repi $ repv), PROP (absi $ (absm $ repv)));
|
|
45 |
in
|
|
46 |
thy
|
|
47 |
|> do_proof (K I) [rep_mor, abs_mor, rep_inv, abs_inv]
|
|
48 |
end;
|
|
49 |
|
|
50 |
fun gen_e_simtype do_proof = gen_simtype Sign.read_term do_proof;
|
|
51 |
fun gen_i_simtype do_proof = gen_simtype Sign.cert_term do_proof;
|
|
52 |
|
|
53 |
fun setup_proof after_qed props thy =
|
|
54 |
thy
|
|
55 |
|> ProofContext.init
|
|
56 |
|> Proof.theorem_i PureThy.internalK NONE after_qed NONE ("", [])
|
|
57 |
(map (fn t => (("", []), [(t, [])])) props);
|
|
58 |
|
|
59 |
in
|
|
60 |
|
|
61 |
val simtype = gen_e_simtype setup_proof;
|
|
62 |
val simtype_i = gen_i_simtype setup_proof;
|
|
63 |
|
|
64 |
end; (*local*)
|
|
65 |
|
|
66 |
local
|
|
67 |
|
|
68 |
structure P = OuterParse
|
|
69 |
and K = OuterKeyword
|
|
70 |
|
|
71 |
in
|
|
72 |
|
|
73 |
val simtypeK = "code_simtype"
|
|
74 |
|
|
75 |
val simtypeP =
|
|
76 |
OuterSyntax.command simtypeK "simulate type in executable code" K.thy_goal (
|
|
77 |
(P.term -- P.term -- P.term -- P.term -- P.term)
|
|
78 |
>> (fn ((((raw_repm, raw_absm), raw_repi), raw_absi), raw_repe) =>
|
|
79 |
(Toplevel.print oo Toplevel.theory_to_proof)
|
|
80 |
(simtype (raw_repm, raw_absm) (raw_repi, raw_absi) raw_repe))
|
|
81 |
);
|
|
82 |
|
|
83 |
val _ = OuterSyntax.add_parsers [simtypeP];
|
|
84 |
|
|
85 |
end; (*local*)
|
|
86 |
|
|
87 |
end; (*struct*)
|