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