16381
|
1 |
(* Title: Pure/codegen.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Florian Haftmann, TU Muenchen
|
|
4 |
|
|
5 |
Stub code generator for (axiomatic) type classes
|
|
6 |
*)
|
|
7 |
|
|
8 |
(*!!! for now, only experimental scratch code !!!*)
|
|
9 |
|
|
10 |
type theory = unit;
|
|
11 |
type constname = string;
|
|
12 |
type typerepr = string;
|
|
13 |
type clsname = string;
|
|
14 |
type typname = string;
|
|
15 |
type defname = string;
|
|
16 |
type constdef = constname * typerepr;
|
|
17 |
type instdecl = typname * clsname list * defname list;
|
|
18 |
|
|
19 |
signature CODEGEN_AXCLASS =
|
|
20 |
sig
|
|
21 |
val gen_clsdict_typ: theory -> clsname -> clsname list -> constdef list -> string;
|
|
22 |
val gen_clsdict_insts: theory -> clsname -> clsname list -> instdecl list -> constdef list -> string;
|
|
23 |
val gen_clsdicts: theory -> clsname -> clsname list -> instdecl list -> constdef list -> string -> string;
|
|
24 |
end;
|
|
25 |
|
|
26 |
structure CodegenAxclass : CODEGEN_AXCLASS =
|
|
27 |
struct
|
|
28 |
|
|
29 |
fun enumerate ls = " " ^ (space_implode ",\n " ls) ^ "\n"
|
|
30 |
|
|
31 |
fun get_dictidf thy cls = cls ^ "_dict";
|
|
32 |
|
|
33 |
fun get_dictidf_inst thy cls ty = cls ^ "_" ^ ty ^ "_dict";
|
|
34 |
|
|
35 |
fun get_clsidf thy cls = cls ^ "_class";
|
|
36 |
|
|
37 |
fun get_memidf thy const = const;
|
|
38 |
|
|
39 |
fun gen_clsdict_typ thy cls supclss consts =
|
|
40 |
"type 'a " ^ (get_dictidf thy cls) ^ " = {\n"
|
|
41 |
^ (((supclss |> map (fn supcls => (get_clsidf thy supcls) ^ ": 'a " ^ (get_dictidf thy supcls)))
|
|
42 |
@ (consts |> map (fn (cname, ctyp) => (get_memidf thy cname) ^ ": " ^ ctyp)))
|
|
43 |
|> enumerate)
|
|
44 |
^ "};\n";
|
|
45 |
|
|
46 |
fun gen_clsdict_mem thy cls consts =
|
|
47 |
consts |> map (fn (cname, _) =>
|
|
48 |
"fun " ^ (get_memidf thy cname) ^ " (cdict:'a " ^ (get_dictidf thy cls) ^ ") = #" ^ (get_memidf thy cname) ^ " cdict;\n")
|
|
49 |
|> space_implode "";
|
|
50 |
|
|
51 |
fun gen_clsdict_inst thy cls supclss (ty, clsargs, constdefs) consts =
|
|
52 |
"val " ^ (get_dictidf_inst thy cls ty) ^ " = {\n"
|
|
53 |
^ (((supclss |> map (fn supcls => (get_clsidf thy cls) ^ " = " ^ (get_dictidf_inst thy supcls ty)))
|
|
54 |
@ ((fst (split_list consts) ~~ constdefs) |>
|
|
55 |
map (fn (cname, dname) => (get_memidf thy cname) ^ " = " ^ dname)))
|
|
56 |
|> enumerate)
|
|
57 |
^ "};\n";
|
|
58 |
|
|
59 |
fun gen_clsdict_insts thy cls supclss insts consts =
|
|
60 |
insts |> map (fn inst => gen_clsdict_inst thy cls supclss inst consts) |> cat_lines
|
|
61 |
|
|
62 |
fun gen_clsdicts thy cls supclss insts consts constdefs =
|
|
63 |
gen_clsdict_typ thy cls supclss consts ^ "\n"
|
|
64 |
^ gen_clsdict_mem thy cls consts ^ "\n"
|
|
65 |
^ constdefs ^ "\n"
|
|
66 |
^ (insts |> map (fn inst => gen_clsdict_inst thy cls supclss inst consts) |> cat_lines);
|
|
67 |
|
|
68 |
end;
|
|
69 |
|
|
70 |
open CodegenAxclass;
|
|
71 |
|
|
72 |
val ex_list =
|
|
73 |
"fun list_le _ _ [] _ = true\n" ^
|
|
74 |
" | list_le _ _ _ [] = false\n" ^
|
|
75 |
" | list_le (cdict:'a list ord_dict) (cdict1:'a ord_dict) (x::xs) (y::ys) = #lt cdict1 x y orelse #eq (#eq_class cdict1) x y andalso list_le cdict cdict1 xs ys;\n\n" ^
|
|
76 |
"fun list_lt _ _ [] [] = false\n" ^
|
|
77 |
" | list_lt _ _ [] _ = true\n" ^
|
|
78 |
" | list_lt _ _ _ [] = false\n" ^
|
|
79 |
" | list_lt (cdict:'a list ord_dict) (cdict1:'a ord_dict) (x::xs) (y::ys) = #lt cdict1 x y orelse #eq (#eq_class cdict1) x y andalso list_lt cdict cdict1 xs ys;\n\n"
|
|
80 |
|
|
81 |
val ex_eq = gen_clsdicts ()
|
|
82 |
"eq" []
|
|
83 |
[("int", [], ["(op =)"]),
|
|
84 |
("char", [], ["(op =)"]),
|
|
85 |
("list", [], ["(op =)"])]
|
|
86 |
[("eq", "'a -> 'a -> bool")]
|
|
87 |
"";
|
|
88 |
|
|
89 |
val ex_ord = gen_clsdicts ()
|
|
90 |
"ord" ["eq"]
|
|
91 |
[("int", [], ["(op <=)", "(op <)"]),
|
|
92 |
("char", [], ["(op <=)", "(op <)"]),
|
|
93 |
("list", ["ord"], ["list_le", "list_lt"])]
|
|
94 |
[("le", "'a -> 'a -> bool"), ("lt", "'a -> 'a -> bool")]
|
|
95 |
ex_list;
|
|
96 |
|
|
97 |
fun ex _ = TextIO.output (TextIO.stdOut, cat_lines [ex_eq, ex_ord]);
|
|
98 |
|
|
99 |
(* TODO:
|
|
100 |
- Dependency: dicttypdecl, members, (instancedef, instance)+
|
|
101 |
- Nahtstelle ausfindig machen
|
|
102 |
*) |