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