author | haftmann |
Wed, 15 Feb 2006 17:09:45 +0100 | |
changeset 19042 | 630b8dd0b31a |
parent 19038 | 62c5f7591a43 |
child 19136 | 00ade10f611d |
permissions | -rw-r--r-- |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
1 |
(* Title: Pure/Tools/codegen_thingol.ML |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
2 |
ID: $Id$ |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann, TU Muenchen |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
4 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
5 |
Intermediate language ("Thin-gol") for code extraction. |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
6 |
*) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
7 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
8 |
signature CODEGEN_THINGOL = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
9 |
sig |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
10 |
type vname = string; |
18885 | 11 |
datatype classlookup = Instance of string * classlookup list list |
12 |
| Lookup of class list * (string * int); |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
13 |
datatype itype = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
14 |
IType of string * itype list |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
15 |
| IFun of itype * itype |
18885 | 16 |
| IVarT of vname * sort; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
17 |
datatype iexpr = |
18885 | 18 |
IConst of (string * itype) * classlookup list list |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
19 |
| IVarE of vname * itype |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
20 |
| IApp of iexpr * iexpr |
19038 | 21 |
| IAbs of iexpr * iexpr |
18885 | 22 |
| ICase of iexpr * (iexpr * iexpr) list; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
23 |
val mk_funs: itype list * itype -> itype; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
24 |
val mk_apps: iexpr * iexpr list -> iexpr; |
19038 | 25 |
val mk_abss: iexpr list * iexpr -> iexpr; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
26 |
val pretty_itype: itype -> Pretty.T; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
27 |
val pretty_iexpr: iexpr -> Pretty.T; |
18216 | 28 |
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list; |
29 |
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
30 |
val unfold_fun: itype -> itype list * itype; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
31 |
val unfold_app: iexpr -> iexpr * iexpr list; |
19038 | 32 |
val unfold_abs: iexpr -> iexpr list * iexpr; |
18865 | 33 |
val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr; |
34 |
val unfold_const_app: iexpr -> |
|
18885 | 35 |
(((string * itype) * classlookup list list) * iexpr list) option; |
18912 | 36 |
val ensure_pat: iexpr -> iexpr; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
37 |
val itype_of_iexpr: iexpr -> itype; |
18170 | 38 |
|
18850 | 39 |
val `%% : string * itype list -> itype; |
40 |
val `-> : itype * itype -> itype; |
|
41 |
val `--> : itype list * itype -> itype; |
|
42 |
val `$ : iexpr * iexpr -> iexpr; |
|
43 |
val `$$ : iexpr * iexpr list -> iexpr; |
|
19038 | 44 |
val `|-> : iexpr * iexpr -> iexpr; |
45 |
val `|--> : iexpr list * iexpr -> iexpr; |
|
18850 | 46 |
|
18865 | 47 |
type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
48 |
type datatyp = (vname * sort) list * (string * itype list) list; |
18850 | 49 |
datatype prim = |
50 |
Pretty of Pretty.T |
|
18963 | 51 |
| Name; |
18170 | 52 |
datatype def = |
18702 | 53 |
Undef |
18963 | 54 |
| Prim of (string * prim list) list |
18702 | 55 |
| Fun of funn |
19038 | 56 |
| Typesyn of (vname * sort) list * itype |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
57 |
| Datatype of datatyp |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
58 |
| Datatypecons of string |
19038 | 59 |
| Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
60 |
| Classmember of class |
18865 | 61 |
| Classinst of ((class * (string * (vname * sort) list)) |
18885 | 62 |
* (class * classlookup list list) list) |
18865 | 63 |
* (string * funn) list; |
18170 | 64 |
type module; |
65 |
type transact; |
|
66 |
type 'dst transact_fin; |
|
18702 | 67 |
type gen_defgen = string -> transact -> def transact_fin; |
18170 | 68 |
val pretty_def: def -> Pretty.T; |
18282 | 69 |
val pretty_module: module -> Pretty.T; |
18360 | 70 |
val pretty_deps: module -> Pretty.T; |
18170 | 71 |
val empty_module: module; |
18963 | 72 |
val add_prim: string -> (string * prim list) -> module -> module; |
18702 | 73 |
val ensure_prim: string -> string -> module -> module; |
18170 | 74 |
val get_def: module -> string -> def; |
75 |
val merge_module: module * module -> module; |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
76 |
val diff_module: module * module -> (string * def) list; |
18170 | 77 |
val partof: string list -> module -> module; |
18516 | 78 |
val has_nsp: string -> string -> bool; |
18170 | 79 |
val succeed: 'a -> transact -> 'a transact_fin; |
80 |
val fail: string -> transact -> 'a transact_fin; |
|
81 |
val gen_ensure_def: (string * gen_defgen) list -> string |
|
82 |
-> string -> transact -> transact; |
|
18963 | 83 |
val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module; |
18216 | 84 |
|
18172 | 85 |
val eta_expand: (string -> int) -> module -> module; |
18216 | 86 |
val eta_expand_poly: module -> module; |
18963 | 87 |
val unclash_vars_tvars: module -> module; |
18172 | 88 |
|
18702 | 89 |
val debug_level: int ref; |
90 |
val debug: int -> ('a -> string) -> 'a -> 'a; |
|
18231 | 91 |
val soft_exc: bool ref; |
18216 | 92 |
|
93 |
val serialize: |
|
19038 | 94 |
((string -> string -> string) -> string -> (string * def) list -> 'a option) |
18850 | 95 |
-> (string list -> (string * string) * 'a list -> 'a option) |
18216 | 96 |
-> (string -> string option) |
18919 | 97 |
-> (string * string -> string) |
18850 | 98 |
-> string list list -> string -> module -> 'a option; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
99 |
end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
100 |
|
18850 | 101 |
structure CodegenThingol: CODEGEN_THINGOL = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
102 |
struct |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
103 |
|
18170 | 104 |
(** auxiliary **) |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
105 |
|
18170 | 106 |
val debug_level = ref 0; |
107 |
fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x); |
|
18231 | 108 |
val soft_exc = ref true; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
109 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
110 |
fun unfoldl dest x = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
111 |
case dest x |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
112 |
of NONE => (x, []) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
113 |
| SOME (x1, x2) => |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
114 |
let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
115 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
116 |
fun unfoldr dest x = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
117 |
case dest x |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
118 |
of NONE => ([], x) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
119 |
| SOME (x1, x2) => |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
120 |
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
121 |
|
18172 | 122 |
fun map_yield f [] = ([], []) |
123 |
| map_yield f (x::xs) = |
|
124 |
let |
|
125 |
val (y, x') = f x |
|
126 |
val (ys, xs') = map_yield f xs |
|
127 |
in (y::ys, x'::xs') end; |
|
128 |
||
18454 | 129 |
fun get_prefix eq ([], ys) = ([], ([], ys)) |
130 |
| get_prefix eq (xs, []) = ([], (xs, [])) |
|
18170 | 131 |
| get_prefix eq (xs as x::xs', ys as y::ys') = |
132 |
if eq (x, y) then |
|
18454 | 133 |
let val (ps', xys'') = get_prefix eq (xs', ys') |
134 |
in (x::ps', xys'') end |
|
135 |
else ([], (xs, ys)); |
|
18170 | 136 |
|
137 |
||
138 |
(** language core - types, pattern, expressions **) |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
139 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
140 |
(* language representation *) |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
141 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
142 |
infix 8 `%%; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
143 |
infixr 6 `->; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
144 |
infixr 6 `-->; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
145 |
infix 4 `$; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
146 |
infix 4 `$$; |
18885 | 147 |
infixr 3 `|->; |
148 |
infixr 3 `|-->; |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
149 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
150 |
type vname = string; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
151 |
|
18885 | 152 |
datatype classlookup = Instance of string * classlookup list list |
153 |
| Lookup of class list * (string * int); |
|
154 |
||
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
155 |
datatype itype = |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
156 |
IType of string * itype list |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
157 |
| IFun of itype * itype |
18885 | 158 |
| IVarT of vname * sort; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
159 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
160 |
datatype iexpr = |
18885 | 161 |
IConst of (string * itype) * classlookup list list |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
162 |
| IVarE of vname * itype |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
163 |
| IApp of iexpr * iexpr |
19038 | 164 |
| IAbs of iexpr * iexpr |
18885 | 165 |
| ICase of iexpr * (iexpr * iexpr) list; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
166 |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
167 |
(* |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
168 |
variable naming conventions |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
169 |
|
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
170 |
bare names: |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
171 |
variable names v |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
172 |
class names cls |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
173 |
type constructor names tyco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
174 |
datatype names dtco |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
175 |
const names (general) c |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
176 |
constructor names co |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
177 |
class member names m |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
178 |
arbitrary name s |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
179 |
|
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
180 |
constructs: |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
181 |
sort sort |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
182 |
type ty |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
183 |
expression e |
18702 | 184 |
pattern p, pat |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
185 |
instance (cls, tyco) inst |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
186 |
variable (v, ty) var |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
187 |
class member (m, ty) membr |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
188 |
constructors (co, tys) constr |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
189 |
*) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
190 |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
191 |
val mk_funs = Library.foldr IFun; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
192 |
val mk_apps = Library.foldl IApp; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
193 |
val mk_abss = Library.foldr IAbs; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
194 |
|
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
195 |
val op `%% = IType; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
196 |
val op `-> = IFun; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
197 |
val op `$ = IApp; |
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
198 |
val op `|-> = IAbs; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
199 |
val op `--> = mk_funs; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
200 |
val op `$$ = mk_apps; |
18247
b17724cae935
code generator: case expressions, improved name resolving
haftmann
parents:
18231
diff
changeset
|
201 |
val op `|--> = mk_abss; |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
202 |
|
18885 | 203 |
fun pretty_itype (IType (tyco, tys)) = |
204 |
Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys) |
|
205 |
| pretty_itype (IFun (ty1, ty2)) = |
|
206 |
Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2] |
|
207 |
| pretty_itype (IVarT (v, sort)) = |
|
208 |
Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort)); |
|
209 |
||
210 |
fun pretty_iexpr (IConst ((c, ty), _)) = |
|
211 |
Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty] |
|
212 |
| pretty_iexpr (IVarE (v, ty)) = |
|
213 |
Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty] |
|
214 |
| pretty_iexpr (IApp (e1, e2)) = |
|
215 |
Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2] |
|
19038 | 216 |
| pretty_iexpr (IAbs (e1, e2)) = |
217 |
Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, Pretty.str "|->", Pretty.brk 1, pretty_iexpr e2] |
|
18885 | 218 |
| pretty_iexpr (ICase (e, cs)) = |
219 |
Pretty.enclose "(" ")" [ |
|
220 |
Pretty.str "case ", |
|
221 |
pretty_iexpr e, |
|
222 |
Pretty.enclose "(" ")" (map (fn (p, e) => |
|
223 |
Pretty.block [ |
|
224 |
pretty_iexpr p, |
|
225 |
Pretty.str " => ", |
|
226 |
pretty_iexpr e |
|
227 |
] |
|
228 |
) cs) |
|
229 |
]; |
|
230 |
||
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
231 |
val unfold_fun = unfoldr |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
232 |
(fn IFun t => SOME t |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
233 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
234 |
|
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
235 |
val unfold_app = unfoldl |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
236 |
(fn IApp e => SOME e |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
237 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
238 |
|
18282 | 239 |
val unfold_abs = unfoldr |
240 |
(fn IAbs b => SOME b |
|
241 |
| _ => NONE) |
|
242 |
||
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
243 |
val unfold_let = unfoldr |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
244 |
(fn ICase (e, [(p, e')]) => SOME ((p, e), e') |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
245 |
| _ => NONE); |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
246 |
|
18865 | 247 |
fun unfold_const_app e = |
248 |
case unfold_app e |
|
249 |
of (IConst x, es) => SOME (x, es) |
|
250 |
| _ => NONE; |
|
251 |
||
18172 | 252 |
fun map_itype f_itype (IType (tyco, tys)) = |
253 |
tyco `%% map f_itype tys |
|
254 |
| map_itype f_itype (IFun (t1, t2)) = |
|
255 |
f_itype t1 `-> f_itype t2 |
|
256 |
| map_itype _ (ty as IVarT _) = |
|
257 |
ty; |
|
258 |
||
18885 | 259 |
fun map_iexpr f (IApp (e1, e2)) = |
260 |
f e1 `$ f e2 |
|
261 |
| map_iexpr f (IAbs (v, e)) = |
|
262 |
v `|-> f e |
|
263 |
| map_iexpr f (ICase (e, ps)) = |
|
264 |
ICase (f e, map (fn (p, e) => (f p, f e)) ps) |
|
265 |
| map_iexpr _ (e as IConst _) = |
|
18172 | 266 |
e |
18885 | 267 |
| map_iexpr _ (e as IVarE _) = |
18865 | 268 |
e; |
18172 | 269 |
|
18885 | 270 |
fun map_atype f (ty as IVarT _) = |
271 |
f ty |
|
272 |
| map_atype f ty = |
|
273 |
map_itype (map_atype f) ty; |
|
274 |
||
275 |
fun map_aexpr f (e as IConst _) = |
|
276 |
f e |
|
277 |
| map_aexpr f (e as IVarE _) = |
|
278 |
f e |
|
279 |
| map_aexpr f e = |
|
280 |
map_iexpr (map_aexpr f) e; |
|
281 |
||
282 |
fun map_iexpr_itype f = |
|
283 |
let |
|
284 |
fun mapp (IConst ((c, ty), ctxt)) = IConst ((c, f ty), ctxt) |
|
285 |
| mapp (IVarE (v, ty)) = IVarE (v, f ty) |
|
286 |
in map_aexpr mapp end; |
|
18172 | 287 |
|
18885 | 288 |
fun fold_atype f (IFun (ty1, ty2)) = |
289 |
fold_atype f ty1 #> fold_atype f ty2 |
|
290 |
| fold_atype f (ty as IType _) = |
|
291 |
f ty |
|
292 |
| fold_atype f (ty as IVarT _) = |
|
293 |
f ty; |
|
18172 | 294 |
|
18885 | 295 |
fun fold_aexpr f (IApp (e1, e2)) = |
296 |
fold_aexpr f e1 #> fold_aexpr f e2 |
|
297 |
| fold_aexpr f (IAbs (v, e)) = |
|
298 |
fold_aexpr f e |
|
299 |
| fold_aexpr f (ICase (e, ps)) = |
|
300 |
fold_aexpr f e #> fold (fn (p, e) => fold_aexpr f p #> fold_aexpr f e) ps |
|
301 |
| fold_aexpr f (e as IConst _) = |
|
302 |
f e |
|
303 |
| fold_aexpr f (e as IVarE _) = |
|
304 |
f e; |
|
18282 | 305 |
|
306 |
fun eq_itype (ty1, ty2) = |
|
307 |
let |
|
308 |
exception NO_MATCH; |
|
309 |
fun eq (IVarT (v1, sort1)) (IVarT (v2, sort2)) subs = |
|
310 |
if sort1 <> sort2 |
|
311 |
then raise NO_MATCH |
|
312 |
else |
|
313 |
(case AList.lookup (op =) subs v1 |
|
314 |
of NONE => subs |> AList.update (op =) (v1, v2) |
|
315 |
| (SOME v1') => |
|
316 |
if v1' <> v2 |
|
317 |
then raise NO_MATCH |
|
318 |
else subs) |
|
319 |
| eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs = |
|
320 |
if tyco1 <> tyco2 |
|
321 |
then raise NO_MATCH |
|
322 |
else subs |> fold2 eq tys1 tys2 |
|
323 |
| eq (IFun (ty11, ty12)) (IFun (ty21, ty22)) subs = |
|
324 |
subs |> eq ty11 ty21 |> eq ty12 ty22 |
|
325 |
| eq _ _ _ = raise NO_MATCH; |
|
326 |
in |
|
327 |
(eq ty1 ty2 []; true) |
|
328 |
handle NO_MATCH => false |
|
329 |
end; |
|
330 |
||
18885 | 331 |
fun instant_itype f = |
332 |
let |
|
333 |
fun instant (IVarT x) = f x |
|
334 |
| instant y = map_itype instant y; |
|
335 |
in map_itype instant end; |
|
336 |
||
18865 | 337 |
fun itype_of_iexpr (IConst ((_, ty), s)) = ty |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
338 |
| itype_of_iexpr (IVarE (_, ty)) = ty |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
339 |
| itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1 |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
340 |
of (IFun (ty2, ty')) => |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
341 |
if ty2 = itype_of_iexpr e2 |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
342 |
then ty' |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
343 |
else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e) |
18850 | 344 |
^ ", " ^ (Pretty.output o pretty_itype) ty2 |
345 |
^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2) |
|
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
346 |
| _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1))) |
19038 | 347 |
| itype_of_iexpr (IAbs (e1, e2)) = itype_of_iexpr e1 `-> itype_of_iexpr e2 |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
348 |
| itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e; |
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
349 |
|
18912 | 350 |
fun ensure_pat (e as IConst (_, [])) = e |
351 |
| ensure_pat (e as IVarE _) = e |
|
352 |
| ensure_pat (e as IApp (e1, e2)) = |
|
353 |
(ensure_pat e1 `$ ensure_pat e2; e) |
|
354 |
| ensure_pat e = |
|
355 |
error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e); |
|
356 |
||
18885 | 357 |
fun type_vnames ty = |
18216 | 358 |
let |
18885 | 359 |
fun extr (IVarT (v, _)) = |
19038 | 360 |
insert (op =) v |
361 |
| extr _ = I; |
|
18885 | 362 |
in fold_atype extr ty end; |
18216 | 363 |
|
18885 | 364 |
fun expr_names e = |
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
365 |
let |
18885 | 366 |
fun extr (IConst ((c, _), _)) = |
18865 | 367 |
insert (op =) c |
18885 | 368 |
| extr (IVarE (v, _)) = |
18304 | 369 |
insert (op =) v |
18885 | 370 |
in fold_aexpr extr e end; |
371 |
||
372 |
fun invent seed used = |
|
373 |
let |
|
374 |
val x = Term.variant used seed |
|
375 |
in (x, x :: used) end; |
|
376 |
||
18304 | 377 |
|
18282 | 378 |
|
18170 | 379 |
(** language module system - definitions, modules, transactions **) |
380 |
||
381 |
(* type definitions *) |
|
382 |
||
18865 | 383 |
type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype); |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
384 |
type datatyp = (vname * sort) list * (string * itype list) list; |
18702 | 385 |
|
18850 | 386 |
datatype prim = |
387 |
Pretty of Pretty.T |
|
18963 | 388 |
| Name; |
18850 | 389 |
|
18170 | 390 |
datatype def = |
18702 | 391 |
Undef |
18963 | 392 |
| Prim of (string * prim list) list |
18702 | 393 |
| Fun of funn |
19038 | 394 |
| Typesyn of (vname * sort) list * itype |
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
395 |
| Datatype of datatyp |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
396 |
| Datatypecons of string |
19038 | 397 |
| Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list) |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
398 |
| Classmember of class |
18865 | 399 |
| Classinst of ((class * (string * (vname * sort) list)) |
18885 | 400 |
* (class * classlookup list list) list) |
18865 | 401 |
* (string * funn) list; |
18170 | 402 |
|
403 |
datatype node = Def of def | Module of node Graph.T; |
|
404 |
type module = node Graph.T; |
|
18702 | 405 |
type transact = Graph.key option * module; |
18231 | 406 |
datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option; |
18702 | 407 |
type 'dst transact_fin = 'dst transact_res * module; |
408 |
type gen_defgen = string -> transact -> def transact_fin; |
|
18231 | 409 |
exception FAIL of string list * exn option; |
18170 | 410 |
|
411 |
val eq_def = (op =); |
|
412 |
||
413 |
(* simple diagnosis *) |
|
414 |
||
18702 | 415 |
fun pretty_def Undef = |
416 |
Pretty.str "<UNDEF>" |
|
417 |
| pretty_def (Prim prims) = |
|
418 |
Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">") |
|
18170 | 419 |
| pretty_def (Fun (eqs, (_, ty))) = |
18812 | 420 |
Pretty.enum " |" "" "" ( |
18170 | 421 |
map (fn (ps, body) => |
422 |
Pretty.block [ |
|
18865 | 423 |
Pretty.enum "," "[" "]" (map pretty_iexpr ps), |
18170 | 424 |
Pretty.str " |->", |
425 |
Pretty.brk 1, |
|
426 |
pretty_iexpr body, |
|
427 |
Pretty.str "::", |
|
428 |
pretty_itype ty |
|
429 |
]) eqs |
|
430 |
) |
|
18172 | 431 |
| pretty_def (Typesyn (vs, ty)) = |
18170 | 432 |
Pretty.block [ |
433 |
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), |
|
434 |
Pretty.str " |=> ", |
|
435 |
pretty_itype ty |
|
436 |
] |
|
19038 | 437 |
| pretty_def (Datatype (vs, cs)) = |
18170 | 438 |
Pretty.block [ |
439 |
Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), |
|
440 |
Pretty.str " |=> ", |
|
18852 | 441 |
Pretty.enum " |" "" "" |
18850 | 442 |
(map (fn (c, tys) => (Pretty.block o Pretty.breaks) |
19038 | 443 |
(Pretty.str c :: map pretty_itype tys)) cs) |
18170 | 444 |
] |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
445 |
| pretty_def (Datatypecons dtname) = |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
446 |
Pretty.str ("cons " ^ dtname) |
19038 | 447 |
| pretty_def (Class (supcls, (v, mems))) = |
18170 | 448 |
Pretty.block [ |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
449 |
Pretty.str ("class var " ^ v ^ "extending "), |
18812 | 450 |
Pretty.enum "," "[" "]" (map Pretty.str supcls), |
18282 | 451 |
Pretty.str " with ", |
18852 | 452 |
Pretty.enum "," "[" "]" |
18850 | 453 |
(map (fn (m, (_, ty)) => Pretty.block |
19038 | 454 |
[Pretty.str (m ^ "::"), pretty_itype ty]) mems) |
18231 | 455 |
] |
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
456 |
| pretty_def (Classmember clsname) = |
18231 | 457 |
Pretty.block [ |
458 |
Pretty.str "class member belonging to ", |
|
18282 | 459 |
Pretty.str clsname |
18231 | 460 |
] |
18865 | 461 |
| pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) = |
18231 | 462 |
Pretty.block [ |
463 |
Pretty.str "class instance (", |
|
18282 | 464 |
Pretty.str clsname, |
18231 | 465 |
Pretty.str ", (", |
466 |
Pretty.str tyco, |
|
467 |
Pretty.str ", ", |
|
18852 | 468 |
Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o |
18850 | 469 |
map Pretty.str o snd) arity), |
18515 | 470 |
Pretty.str "))" |
18231 | 471 |
]; |
18170 | 472 |
|
473 |
fun pretty_module modl = |
|
474 |
let |
|
475 |
fun pretty (name, Module modl) = |
|
476 |
Pretty.block ( |
|
477 |
Pretty.str ("module " ^ name ^ " {") |
|
478 |
:: Pretty.brk 1 |
|
479 |
:: Pretty.chunks (map pretty (AList.make (Graph.get_node modl) |
|
480 |
(Graph.strong_conn modl |> List.concat |> rev))) |
|
481 |
:: Pretty.str "}" :: nil |
|
482 |
) |
|
483 |
| pretty (name, Def def) = |
|
484 |
Pretty.block [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def] |
|
485 |
in pretty ("//", Module modl) end; |
|
486 |
||
18360 | 487 |
fun pretty_deps modl = |
488 |
let |
|
489 |
fun one_node key = |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
490 |
let |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
491 |
val preds_ = Graph.imm_preds modl key; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
492 |
val succs_ = Graph.imm_succs modl key; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
493 |
val mutbs = gen_inter (op =) (preds_, succs_); |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
494 |
val preds = fold (remove (op =)) mutbs preds_; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
495 |
val succs = fold (remove (op =)) mutbs succs_; |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
496 |
in |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
497 |
(Pretty.block o Pretty.fbreaks) ( |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
498 |
Pretty.str key |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
499 |
:: map (fn s => Pretty.str ("<-> " ^ s)) mutbs |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
500 |
@ map (fn s => Pretty.str ("<-- " ^ s)) preds |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
501 |
@ map (fn s => Pretty.str ("--> " ^ s)) succs |
18850 | 502 |
@ (the_list oo Option.mapPartial) |
503 |
((fn Module modl' => SOME (pretty_deps modl') |
|
504 |
| _ => NONE) o Graph.get_node modl) (SOME key) |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
505 |
) |
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
506 |
end |
18360 | 507 |
in |
508 |
modl |
|
509 |
|> Graph.strong_conn |
|
510 |
|> List.concat |
|
511 |
|> rev |
|
512 |
|> map one_node |
|
513 |
|> Pretty.chunks |
|
514 |
end; |
|
515 |
||
18170 | 516 |
|
517 |
(* name handling *) |
|
518 |
||
519 |
fun dest_name name = |
|
520 |
let |
|
521 |
val name' = NameSpace.unpack name |
|
522 |
val (name'', name_base) = split_last name' |
|
523 |
val (modl, shallow) = split_last name'' |
|
524 |
in (modl, NameSpace.pack [shallow, name_base]) end |
|
525 |
handle Empty => error ("not a qualified name: " ^ quote name); |
|
526 |
||
18516 | 527 |
fun has_nsp name shallow = |
528 |
NameSpace.is_qualified name |
|
529 |
andalso let |
|
530 |
val name' = NameSpace.unpack name |
|
531 |
val (name'', _) = split_last name' |
|
532 |
val (_, shallow') = split_last name'' |
|
533 |
in shallow' = shallow end; |
|
534 |
||
18170 | 535 |
fun dest_modl (Module m) = m; |
536 |
fun dest_def (Def d) = d; |
|
537 |
||
538 |
||
539 |
(* modules *) |
|
540 |
||
541 |
val empty_module = Graph.empty; (*read: "depends on"*) |
|
542 |
||
543 |
fun get_def modl name = |
|
544 |
case dest_name name |
|
545 |
of (modlname, base) => |
|
546 |
let |
|
547 |
fun get (Module node) [] = |
|
548 |
(dest_def o Graph.get_node node) base |
|
549 |
| get (Module node) (m::ms) = |
|
550 |
get (Graph.get_node node m) ms |
|
551 |
in get (Module modl) modlname end; |
|
552 |
||
553 |
fun add_def (name, def) = |
|
554 |
let |
|
555 |
val (modl, base) = dest_name name; |
|
556 |
fun add [] = |
|
557 |
Graph.new_node (base, Def def) |
|
558 |
| add (m::ms) = |
|
559 |
Graph.default_node (m, Module empty_module) |
|
560 |
#> Graph.map_node m (Module o add ms o dest_modl) |
|
561 |
in add modl end; |
|
562 |
||
563 |
fun add_dep (name1, name2) modl = |
|
564 |
if name1 = name2 then modl |
|
565 |
else |
|
566 |
let |
|
567 |
val m1 = dest_name name1 |> apsnd single |> (op @); |
|
568 |
val m2 = dest_name name2 |> apsnd single |> (op @); |
|
18454 | 569 |
val (ms, (r1, r2)) = get_prefix (op =) (m1, m2); |
570 |
val (ms, (s1::r1, s2::r2)) = get_prefix (op =) (m1, m2); |
|
18170 | 571 |
val add_edge = |
572 |
if null r1 andalso null r2 |
|
573 |
then Graph.add_edge |
|
19038 | 574 |
else fn edge => (Graph.add_edge_acyclic edge |
575 |
handle Graph.CYCLES _ => error ("adding dependency " |
|
576 |
^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle")) |
|
18170 | 577 |
fun add [] node = |
578 |
node |
|
579 |
|> add_edge (s1, s2) |
|
580 |
| add (m::ms) node = |
|
581 |
node |
|
582 |
|> Graph.map_node m (Module o add ms o dest_modl); |
|
583 |
in add ms modl end; |
|
584 |
||
18885 | 585 |
fun map_def name f = |
586 |
let |
|
587 |
val (modl, base) = dest_name name; |
|
588 |
fun mapp [] = |
|
589 |
Graph.map_node base (Def o f o dest_def) |
|
590 |
| mapp (m::ms) = |
|
591 |
Graph.map_node m (Module o mapp ms o dest_modl) |
|
592 |
in mapp modl end; |
|
593 |
||
594 |
fun map_defs f = |
|
595 |
let |
|
596 |
fun mapp (Def def) = |
|
597 |
(Def o f) def |
|
598 |
| mapp (Module modl) = |
|
599 |
(Module o Graph.map_nodes mapp) modl |
|
600 |
in dest_modl o mapp o Module end; |
|
601 |
||
602 |
fun fold_defs f = |
|
603 |
let |
|
604 |
fun fol prfix (name, Def def) = |
|
605 |
f (NameSpace.pack (prfix @ [name]), def) |
|
606 |
| fol prfix (name, Module modl) = |
|
607 |
Graph.fold_nodes (fol (prfix @ [name])) modl |
|
608 |
in Graph.fold_nodes (fol []) end; |
|
609 |
||
610 |
fun add_deps f modl = |
|
611 |
modl |
|
612 |
|> fold add_dep ([] |> fold_defs (append o f) modl); |
|
613 |
||
614 |
fun ensure_def (name, Undef) module = |
|
615 |
(case try (get_def module) name |
|
616 |
of NONE => (error "attempted to add Undef to module") |
|
617 |
| SOME Undef => (error "attempted to add Undef to module") |
|
618 |
| SOME def' => map_def name (K def') module) |
|
619 |
| ensure_def (name, def) module = |
|
620 |
(case try (get_def module) name |
|
621 |
of NONE => add_def (name, def) module |
|
622 |
| SOME Undef => map_def name (K def) module |
|
623 |
| SOME def' => if eq_def (def, def') |
|
624 |
then module |
|
625 |
else error ("tried to overwrite definition " ^ name)); |
|
626 |
||
18963 | 627 |
fun add_prim name (target, primdef as _::_) = |
18516 | 628 |
let |
629 |
val (modl, base) = dest_name name; |
|
630 |
fun add [] module = |
|
631 |
(case try (Graph.get_node module) base |
|
632 |
of NONE => |
|
633 |
module |
|
18963 | 634 |
|> Graph.new_node (base, (Def o Prim) [(target, primdef)]) |
18516 | 635 |
| SOME (Def (Prim prim)) => |
18702 | 636 |
if AList.defined (op =) prim target |
18850 | 637 |
then error ("already primitive definition (" ^ target |
638 |
^ ") present for " ^ name) |
|
18516 | 639 |
else |
640 |
module |
|
18850 | 641 |
|> Graph.map_node base ((K o Def o Prim) (AList.update (op =) |
18963 | 642 |
(target, primdef) prim)) |
18516 | 643 |
| _ => error ("already non-primitive definition present for " ^ name)) |
644 |
| add (m::ms) module = |
|
645 |
module |
|
646 |
|> Graph.default_node (m, Module empty_module) |
|
647 |
|> Graph.map_node m (Module o add ms o dest_modl) |
|
18963 | 648 |
in add modl end; |
18516 | 649 |
|
18702 | 650 |
fun ensure_prim name target = |
18516 | 651 |
let |
652 |
val (modl, base) = dest_name name; |
|
653 |
fun ensure [] module = |
|
654 |
(case try (Graph.get_node module) base |
|
655 |
of NONE => |
|
656 |
module |
|
18963 | 657 |
|> Graph.new_node (base, (Def o Prim) [(target, [])]) |
18702 | 658 |
| SOME (Def (Prim prim)) => |
18516 | 659 |
module |
18850 | 660 |
|> Graph.map_node base ((K o Def o Prim) (AList.default (op =) |
18963 | 661 |
(target, []) prim)) |
18850 | 662 |
| _ => module) |
18516 | 663 |
| ensure (m::ms) module = |
664 |
module |
|
665 |
|> Graph.default_node (m, Module empty_module) |
|
666 |
|> Graph.map_node m (Module o ensure ms o dest_modl) |
|
667 |
in ensure modl end; |
|
668 |
||
18170 | 669 |
fun merge_module modl12 = |
670 |
let |
|
19025 | 671 |
fun join_module _ (Module m1, Module m2) = |
672 |
Module (merge_module (m1, m2)) |
|
673 |
| join_module name (Def d1, Def d2) = |
|
674 |
if eq_def (d1, d2) then Def d1 else raise Graph.DUP name |
|
675 |
| join_module name _ = raise Graph.DUP name |
|
676 |
in Graph.join join_module modl12 end; |
|
18170 | 677 |
|
19042
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
678 |
fun diff_module modl12 = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
679 |
let |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
680 |
fun diff_entry prefix modl2 (name, Def def1) = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
681 |
let |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
682 |
val e2 = try (Graph.get_node modl2) name |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
683 |
in if is_some e2 andalso eq_def (def1, (dest_def o the) e2) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
684 |
then I |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
685 |
else cons (NameSpace.pack (prefix @ [name]), def1) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
686 |
end |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
687 |
| diff_entry prefix modl2 (name, Module modl1) = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
688 |
diff_modl (prefix @ [name]) (modl1, |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
689 |
(the_default empty_module o Option.map dest_modl o try (Graph.get_node modl2)) name) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
690 |
and diff_modl prefix (modl1, modl2) = |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
691 |
fold (diff_entry prefix modl2) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
692 |
((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1) |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
693 |
in diff_modl [] modl12 [] end; |
630b8dd0b31a
exported some interfaces useful for other code generator approaches
haftmann
parents:
19038
diff
changeset
|
694 |
|
18170 | 695 |
fun partof names modl = |
18335 | 696 |
let |
697 |
datatype pathnode = PN of (string list * (string * pathnode) list); |
|
698 |
fun mk_ipath ([], base) (PN (defs, modls)) = |
|
699 |
PN (base :: defs, modls) |
|
700 |
| mk_ipath (n::ns, base) (PN (defs, modls)) = |
|
701 |
modls |
|
702 |
|> AList.default (op =) (n, PN ([], [])) |
|
703 |
|> AList.map_entry (op =) n (mk_ipath (ns, base)) |
|
704 |
|> (pair defs #> PN); |
|
705 |
fun select (PN (defs, modls)) (Module module) = |
|
706 |
module |
|
707 |
|> Graph.subgraph (Graph.all_succs module (defs @ map fst modls)) |
|
708 |
|> fold (fn (name, modls) => Graph.map_node name (select modls)) modls |
|
709 |
|> Module; |
|
710 |
in |
|
711 |
Module modl |
|
18850 | 712 |
|> select (fold (mk_ipath o dest_name) |
713 |
(filter NameSpace.is_qualified names) (PN ([], []))) |
|
18335 | 714 |
|> dest_modl |
715 |
end; |
|
18170 | 716 |
|
18850 | 717 |
fun imports_of modl name = |
18702 | 718 |
let |
719 |
fun imports prfx [] modl = |
|
720 |
[] |
|
721 |
| imports prfx (m::ms) modl = |
|
722 |
map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m)) |
|
18850 | 723 |
@ map single (Graph.imm_succs modl m); |
18702 | 724 |
in |
18850 | 725 |
modl |
726 |
|> imports [] name |
|
18702 | 727 |
|> map NameSpace.pack |
728 |
end; |
|
729 |
||
730 |
fun check_samemodule names = |
|
731 |
fold (fn name => |
|
732 |
let |
|
733 |
val modn = (fst o dest_name) name |
|
734 |
in |
|
735 |
fn NONE => SOME modn |
|
18850 | 736 |
| SOME mod' => if modn = mod' then SOME modn |
737 |
else error "inconsistent name prefix for simultanous names" |
|
18702 | 738 |
end |
739 |
) names NONE; |
|
740 |
||
741 |
fun check_funeqs eqs = |
|
742 |
(fold (fn (pats, _) => |
|
743 |
let |
|
744 |
val l = length pats |
|
745 |
in |
|
746 |
fn NONE => SOME l |
|
18850 | 747 |
| SOME l' => if l = l' then SOME l |
748 |
else error "function definition with different number of arguments" |
|
18702 | 749 |
end |
750 |
) eqs NONE; eqs); |
|
751 |
||
752 |
fun check_prep_def modl Undef = |
|
753 |
Undef |
|
754 |
| check_prep_def modl (d as Prim _) = |
|
755 |
d |
|
756 |
| check_prep_def modl (Fun (eqs, d)) = |
|
757 |
Fun (check_funeqs eqs, d) |
|
758 |
| check_prep_def modl (d as Typesyn _) = |
|
759 |
d |
|
19038 | 760 |
| check_prep_def modl (d as Datatype _) = |
761 |
d |
|
18702 | 762 |
| check_prep_def modl (Datatypecons dtco) = |
763 |
error "attempted to add bare datatype constructor" |
|
19038 | 764 |
| check_prep_def modl (d as Class _) = |
765 |
d |
|
18702 | 766 |
| check_prep_def modl (Classmember _) = |
767 |
error "attempted to add bare class member" |
|
18865 | 768 |
| check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) = |
18170 | 769 |
let |
19038 | 770 |
val Class (_, (v, membrs)) = get_def modl class; |
18702 | 771 |
val _ = if length memdefs > length memdefs |
772 |
then error "too many member definitions given" |
|
773 |
else (); |
|
18885 | 774 |
fun instant (w, ty) (var as (v, _)) = |
775 |
if v = w then ty else IVarT var; |
|
18702 | 776 |
fun mk_memdef (m, (ctxt, ty)) = |
777 |
case AList.lookup (op =) memdefs m |
|
778 |
of NONE => error ("missing definition for member " ^ quote m) |
|
779 |
| SOME (eqs, (ctxt', ty')) => |
|
18885 | 780 |
if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty') |
18702 | 781 |
then (m, (check_funeqs eqs, (ctxt', ty'))) |
782 |
else error ("inconsistent type for member definition " ^ quote m) |
|
783 |
in Classinst (d, map mk_memdef membrs) end; |
|
18170 | 784 |
|
19038 | 785 |
fun postprocess_def (name, Datatype (_, constrs)) = |
18702 | 786 |
(check_samemodule (name :: map fst constrs); |
787 |
fold (fn (co, _) => |
|
788 |
ensure_def (co, Datatypecons name) |
|
789 |
#> add_dep (co, name) |
|
790 |
#> add_dep (name, co) |
|
791 |
) constrs |
|
792 |
) |
|
19038 | 793 |
| postprocess_def (name, Class (_, (_, membrs))) = |
18702 | 794 |
(check_samemodule (name :: map fst membrs); |
795 |
fold (fn (m, _) => |
|
796 |
ensure_def (m, Classmember name) |
|
797 |
#> add_dep (m, name) |
|
798 |
#> add_dep (name, m) |
|
799 |
) membrs |
|
800 |
) |
|
801 |
| postprocess_def _ = |
|
802 |
I; |
|
18380
9668764224a7
substantial improvements for class code generation
haftmann
parents:
18361
diff
changeset
|
803 |
|
18702 | 804 |
fun succeed some (_, modl) = (Succeed some, modl); |
805 |
fun fail msg (_, modl) = (Fail ([msg], NONE), modl); |
|
18170 | 806 |
|
18231 | 807 |
fun check_fail _ (Succeed dst, trns) = (dst, trns) |
808 |
| check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); |
|
18170 | 809 |
|
18702 | 810 |
fun select_generator _ src [] modl = |
811 |
(SOME src, modl) |> fail ("no code generator available") |
|
18231 | 812 |
| select_generator mk_msg src gens modl = |
813 |
let |
|
814 |
fun handle_fail msgs f = |
|
815 |
let |
|
816 |
in |
|
817 |
if ! soft_exc |
|
818 |
then |
|
18702 | 819 |
(SOME src, modl) |> f |
820 |
handle FAIL exc => (Fail exc, modl) |
|
821 |
| e => (Fail (msgs, SOME e), modl) |
|
18231 | 822 |
else |
18702 | 823 |
(SOME src, modl) |> f |
824 |
handle FAIL exc => (Fail exc, modl) |
|
18231 | 825 |
end; |
826 |
fun select msgs [(gname, gen)] = |
|
18702 | 827 |
handle_fail (msgs @ [mk_msg gname]) (gen src) |
828 |
| select msgs ((gname, gen)::gens) = |
|
829 |
let |
|
830 |
val msgs' = msgs @ [mk_msg gname] |
|
831 |
in case handle_fail msgs' (gen src) |
|
832 |
of (Fail (_, NONE), _) => |
|
833 |
select msgs' gens |
|
834 |
| result => result |
|
18231 | 835 |
end; |
836 |
in select [] gens end; |
|
18170 | 837 |
|
18702 | 838 |
fun gen_ensure_def defgens msg name (dep, modl) = |
18170 | 839 |
let |
18702 | 840 |
val msg' = case dep |
841 |
of NONE => msg |
|
842 |
| SOME dep => msg ^ ", with dependency " ^ quote dep; |
|
843 |
fun add_dp NONE = I |
|
844 |
| add_dp (SOME dep) = |
|
845 |
debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) |
|
846 |
#> add_dep (dep, name); |
|
847 |
fun prep_def def modl = |
|
848 |
(check_prep_def modl def, modl); |
|
18170 | 849 |
in |
850 |
modl |
|
18702 | 851 |
|> (if can (get_def modl) name |
852 |
then |
|
853 |
debug 9 (fn _ => "asserting node " ^ quote name) |
|
854 |
#> add_dp dep |
|
855 |
else |
|
856 |
debug 9 (fn _ => "allocating node " ^ quote name) |
|
857 |
#> add_def (name, Undef) |
|
858 |
#> add_dp dep |
|
859 |
#> debug 9 (fn _ => "creating node " ^ quote name) |
|
18850 | 860 |
#> select_generator (fn gname => "trying code generator " |
861 |
^ gname ^ " for definition of " ^ quote name) name defgens |
|
18702 | 862 |
#> debug 9 (fn _ => "checking creation of node " ^ quote name) |
863 |
#> check_fail msg' |
|
864 |
#-> (fn def => prep_def def) |
|
865 |
#-> (fn def => |
|
866 |
debug 10 (fn _ => "addition of " ^ name |
|
867 |
^ " := " ^ (Pretty.output o pretty_def) def) |
|
868 |
#> debug 10 (fn _ => "adding") |
|
869 |
#> ensure_def (name, def) |
|
870 |
#> debug 10 (fn _ => "postprocessing") |
|
871 |
#> postprocess_def (name, def) |
|
872 |
#> debug 10 (fn _ => "adding done") |
|
873 |
)) |
|
874 |
|> pair dep |
|
18170 | 875 |
end; |
876 |
||
18963 | 877 |
fun start_transact init f modl = |
18231 | 878 |
let |
18963 | 879 |
fun handle_fail f x = |
880 |
(f x |
|
18231 | 881 |
handle FAIL (msgs, NONE) => |
882 |
(error o cat_lines) ("code generation failed, while:" :: msgs)) |
|
883 |
handle FAIL (msgs, SOME e) => |
|
884 |
((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e); |
|
885 |
in |
|
18963 | 886 |
(init, modl) |
18231 | 887 |
|> handle_fail f |
888 |
|-> (fn x => fn (_, module) => (x, module)) |
|
889 |
end; |
|
18172 | 890 |
|
891 |
||
18335 | 892 |
|
893 |
(** generic transformation **) |
|
18304 | 894 |
|
18885 | 895 |
fun map_def_fun f (Fun funn) = |
896 |
Fun (f funn) |
|
897 |
| map_def_fun _ def = def; |
|
898 |
||
899 |
fun map_def_fun_expr f (eqs, cty) = |
|
900 |
(map (fn (ps, rhs) => (map f ps, f rhs)) eqs, cty); |
|
901 |
||
18172 | 902 |
fun eta_expand query = |
903 |
let |
|
18885 | 904 |
fun eta e = |
18865 | 905 |
case unfold_const_app e |
18885 | 906 |
of SOME (((f, ty), ls), es) => |
907 |
let |
|
908 |
val delta = query f - length es; |
|
909 |
val add_n = if delta < 0 then 0 else delta; |
|
910 |
val tys = |
|
911 |
(fst o unfold_fun) ty |
|
912 |
|> curry Library.drop (length es) |
|
913 |
|> curry Library.take add_n |
|
914 |
val add_vars = |
|
19038 | 915 |
map2 (curry IVarE) (Term.invent_names (fold expr_names es []) "x" add_n) tys; |
18885 | 916 |
in |
19038 | 917 |
add_vars `|--> IConst ((f, ty), ls) `$$ es `$$ add_vars |
18885 | 918 |
end |
919 |
| NONE => map_iexpr eta e; |
|
920 |
in (map_defs o map_def_fun o map_def_fun_expr) eta end; |
|
18172 | 921 |
|
18216 | 922 |
val eta_expand_poly = |
923 |
let |
|
18885 | 924 |
fun eta (funn as ([([], e)], cty as (sortctxt, (ty as IFun (ty1, ty2))))) = |
18216 | 925 |
if (not o null) sortctxt |
18885 | 926 |
orelse null (type_vnames ty []) |
927 |
then funn |
|
18216 | 928 |
else |
19038 | 929 |
(case unfold_abs e |
930 |
of ([], e) => |
|
931 |
let |
|
932 |
val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1) |
|
933 |
in (([([add_var], add_var `|-> e)], cty)) end |
|
934 |
| eq => |
|
935 |
(([eq], cty))) |
|
18885 | 936 |
| eta funn = funn; |
937 |
in (map_defs o map_def_fun) eta end; |
|
938 |
||
18963 | 939 |
val unclash_vars_tvars = |
18885 | 940 |
let |
941 |
fun unclash (eqs, (sortctxt, ty)) = |
|
942 |
let |
|
943 |
val used_expr = |
|
944 |
fold (fn (pats, rhs) => fold expr_names pats #> expr_names rhs) eqs []; |
|
945 |
val used_type = map fst sortctxt; |
|
946 |
val clash = gen_union (op =) (used_expr, used_type); |
|
947 |
val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst; |
|
948 |
fun rename (v, sort) = |
|
949 |
(perhaps (AList.lookup (op =) rename_map) v, sort); |
|
950 |
val rename_typ = instant_itype (IVarT o rename); |
|
951 |
val rename_expr = map_iexpr_itype rename_typ; |
|
952 |
fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs) |
|
953 |
in |
|
954 |
(map rename_eq eqs, (map rename sortctxt, rename_typ ty)) |
|
955 |
end; |
|
956 |
in (map_defs o map_def_fun) unclash end; |
|
18216 | 957 |
|
18172 | 958 |
|
18216 | 959 |
(** generic serialization **) |
960 |
||
961 |
(* resolving *) |
|
962 |
||
18885 | 963 |
structure NameMangler = NameManglerFun ( |
964 |
type ctxt = (string * string -> string) * (string -> string option); |
|
18516 | 965 |
type src = string * string; |
966 |
val ord = prod_ord string_ord string_ord; |
|
18963 | 967 |
fun mk (postprocess, validate) ((shallow, name), 0) = |
968 |
let |
|
969 |
val name' = postprocess (shallow, name); |
|
970 |
in case validate name' |
|
971 |
of NONE => name' |
|
972 |
| _ => mk (postprocess, validate) ((shallow, name), 1) |
|
973 |
end |
|
974 |
| mk (postprocess, validate) (("", name), i) = |
|
975 |
postprocess ("", name ^ "_" ^ string_of_int (i+1)) |
|
18885 | 976 |
|> perhaps validate |
18963 | 977 |
| mk (postprocess, validate) ((shallow, name), i) = |
978 |
postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1)) |
|
18516 | 979 |
|> perhaps validate; |
980 |
fun is_valid _ _ = true; |
|
981 |
fun maybe_unique _ _ = NONE; |
|
982 |
fun re_mangle _ dst = error ("no such definition name: " ^ quote dst); |
|
983 |
); |
|
984 |
||
18963 | 985 |
fun mk_deresolver module nsp_conn postprocess validate = |
18885 | 986 |
let |
987 |
datatype tabnode = N of string * tabnode Symtab.table option; |
|
988 |
fun mk module manglers tab = |
|
989 |
let |
|
990 |
fun mk_name name = |
|
991 |
case NameSpace.unpack name |
|
992 |
of [n] => ("", n) |
|
993 |
| [s, n] => (s, n); |
|
994 |
fun in_conn (shallow, conn) = |
|
995 |
member (op = : string * string -> bool) conn shallow; |
|
996 |
fun add_name name = |
|
997 |
let |
|
998 |
val n as (shallow, _) = mk_name name; |
|
999 |
in |
|
1000 |
AList.map_entry_yield in_conn shallow ( |
|
18963 | 1001 |
NameMangler.declare (postprocess, validate) n |
18885 | 1002 |
#-> (fn n' => pair (name, n')) |
18963 | 1003 |
) #> apfst the |
18885 | 1004 |
end; |
1005 |
val (renamings, manglers') = |
|
1006 |
fold_map add_name (Graph.keys module) manglers; |
|
1007 |
fun extend_tab (n, n') = |
|
1008 |
if (length o NameSpace.unpack) n = 1 |
|
1009 |
then |
|
1010 |
Symtab.update_new |
|
1011 |
(n, N (n', SOME (mk ((dest_modl o Graph.get_node module) n) manglers' Symtab.empty))) |
|
1012 |
else |
|
1013 |
Symtab.update_new (n, N (n', NONE)); |
|
1014 |
in fold extend_tab renamings tab end; |
|
1015 |
fun get_path_name [] tab = |
|
1016 |
([], SOME tab) |
|
1017 |
| get_path_name [p] tab = |
|
1018 |
let |
|
1019 |
val SOME (N (p', tab')) = Symtab.lookup tab p |
|
1020 |
in ([p'], tab') end |
|
1021 |
| get_path_name [p1, p2] tab = |
|
18919 | 1022 |
(case Symtab.lookup tab p1 |
18885 | 1023 |
of SOME (N (p', SOME tab')) => |
1024 |
let |
|
1025 |
val (ps', tab'') = get_path_name [p2] tab' |
|
1026 |
in (p' :: ps', tab'') end |
|
1027 |
| NONE => |
|
1028 |
let |
|
1029 |
val SOME (N (p', NONE)) = Symtab.lookup tab (NameSpace.pack [p1, p2]) |
|
18919 | 1030 |
in ([p'], NONE) end) |
18885 | 1031 |
| get_path_name (p::ps) tab = |
1032 |
let |
|
1033 |
val SOME (N (p', SOME tab')) = Symtab.lookup tab p |
|
1034 |
val (ps', tab'') = get_path_name ps tab' |
|
1035 |
in (p' :: ps', tab'') end; |
|
1036 |
fun deresolv tab prefix name = |
|
1037 |
if (is_some o Int.fromString) name |
|
1038 |
then name |
|
1039 |
else let |
|
1040 |
val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name); |
|
1041 |
val (_, SOME tab') = get_path_name common tab; |
|
1042 |
val (name', _) = get_path_name rem tab'; |
|
1043 |
in NameSpace.pack name' end; |
|
1044 |
in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end; |
|
1045 |
||
18216 | 1046 |
|
1047 |
(* serialization *) |
|
1048 |
||
18963 | 1049 |
fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module = |
18216 | 1050 |
let |
18963 | 1051 |
val resolver = mk_deresolver module nsp_conn postprocess validate; |
19038 | 1052 |
fun sresolver s = (resolver o NameSpace.unpack) s |
18702 | 1053 |
fun mk_name prfx name = |
18850 | 1054 |
let |
1055 |
val name_qual = NameSpace.pack (prfx @ [name]) |
|
1056 |
in (name_qual, resolver prfx name_qual) end; |
|
18756 | 1057 |
fun mk_contents prfx module = |
18850 | 1058 |
List.mapPartial (seri prfx) |
1059 |
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) |
|
18756 | 1060 |
and seri prfx ([(name, Module modl)]) = |
18850 | 1061 |
seri_module (map (resolver []) (imports_of module (prfx @ [name]))) |
1062 |
(mk_name prfx name, mk_contents (prfx @ [name]) modl) |
|
18756 | 1063 |
| seri prfx ds = |
19038 | 1064 |
seri_defs sresolver (NameSpace.pack prfx) |
18912 | 1065 |
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds) |
18216 | 1066 |
in |
18850 | 1067 |
seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev)) |
1068 |
(("", name_root), (mk_contents [] module)) |
|
18216 | 1069 |
end; |
1070 |
||
18169
45def66f86cb
added modules for code generator generation two, not operational yet
haftmann
parents:
diff
changeset
|
1071 |
end; (* struct *) |