author | bulwahn |
Fri, 09 Sep 2011 14:43:50 +0200 | |
changeset 44855 | f4a6786057d9 |
parent 44854 | 0b3d3570ab31 |
child 44996 | 410eea28b0f7 |
permissions | -rw-r--r-- |
37744 | 1 |
(* Title: Tools/Code/code_thingol.ML |
24219 | 2 |
Author: Florian Haftmann, TU Muenchen |
3 |
||
4 |
Intermediate language ("Thin-gol") representing executable code. |
|
24918 | 5 |
Representation and translation. |
24219 | 6 |
*) |
7 |
||
8 |
infix 8 `%%; |
|
9 |
infix 4 `$; |
|
10 |
infix 4 `$$; |
|
31724 | 11 |
infixr 3 `|=>; |
12 |
infixr 3 `|==>; |
|
24219 | 13 |
|
14 |
signature BASIC_CODE_THINGOL = |
|
15 |
sig |
|
16 |
type vname = string; |
|
17 |
datatype dict = |
|
41782 | 18 |
Dict of string list * plain_dict |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
19 |
and plain_dict = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
20 |
Dict_Const of string * dict list list |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
21 |
| Dict_Var of vname * (int * int) |
24219 | 22 |
datatype itype = |
23 |
`%% of string * itype list |
|
24 |
| ITyVar of vname; |
|
44789
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
25 |
type const = string * (((itype list * dict list list) * (itype list * itype)) * bool) |
41782 | 26 |
(* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *) |
24219 | 27 |
datatype iterm = |
24591 | 28 |
IConst of const |
31889 | 29 |
| IVar of vname option |
24219 | 30 |
| `$ of iterm * iterm |
31888 | 31 |
| `|=> of (vname option * itype) * iterm |
24219 | 32 |
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
33 |
(*((term, type), [(selector pattern, body term )]), primitive term)*) |
|
34 |
val `$$ : iterm * iterm list -> iterm; |
|
31888 | 35 |
val `|==> : (vname option * itype) list * iterm -> iterm; |
24219 | 36 |
type typscheme = (vname * sort) list * itype; |
37 |
end; |
|
38 |
||
39 |
signature CODE_THINGOL = |
|
40 |
sig |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
41 |
include BASIC_CODE_THINGOL |
34084 | 42 |
val fun_tyco: string |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
43 |
val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
44 |
val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
45 |
val unfold_fun: itype -> itype list * itype |
37640 | 46 |
val unfold_fun_n: int -> itype -> itype list * itype |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
47 |
val unfold_app: iterm -> iterm * iterm list |
31888 | 48 |
val unfold_abs: iterm -> (vname option * itype) list * iterm |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
49 |
val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
50 |
val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm |
31889 | 51 |
val split_pat_abs: iterm -> ((iterm * itype) * iterm) option |
52 |
val unfold_pat_abs: iterm -> (iterm * itype) list * iterm |
|
31049 | 53 |
val unfold_const_app: iterm -> (const * iterm list) option |
32909 | 54 |
val is_IVar: iterm -> bool |
41782 | 55 |
val is_IAbs: iterm -> bool |
31049 | 56 |
val eta_expand: int -> const * iterm list -> iterm |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
57 |
val contains_dict_var: iterm -> bool |
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
58 |
val add_constnames: iterm -> string list -> string list |
32917 | 59 |
val add_tyconames: iterm -> string list -> string list |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
60 |
val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
61 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
62 |
type naming |
28706 | 63 |
val empty_naming: naming |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
64 |
val lookup_class: naming -> class -> string option |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
65 |
val lookup_classrel: naming -> class * class -> string option |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
66 |
val lookup_tyco: naming -> string -> string option |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
67 |
val lookup_instance: naming -> class * string -> string option |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
68 |
val lookup_const: naming -> string -> string option |
31054 | 69 |
val ensure_declared_const: theory -> string -> naming -> string * naming |
24219 | 70 |
|
24918 | 71 |
datatype stmt = |
27024 | 72 |
NoStmt |
37437 | 73 |
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
74 |
| Datatype of string * ((vname * sort) list * |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
75 |
((string * vname list (*type argument wrt. canonical order*)) * itype list) list) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
76 |
| Datatypecons of string * string |
37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset
|
77 |
| Class of class * (vname * ((class * string) list * (string * itype) list)) |
24219 | 78 |
| Classrel of class * class |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
79 |
| Classparam of string * class |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
80 |
| Classinst of (class * (string * (vname * sort) list) (*class and arity*)) |
37445
e372fa3c7239
dropped obscure type argument weakening mapping -- was only a misunderstanding
haftmann
parents:
37440
diff
changeset
|
81 |
* ((class * (string * (string * dict list list))) list (*super instances*) |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
82 |
* (((string * const) * (thm * bool)) list (*class parameter instances*) |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
83 |
* ((string * const) * (thm * bool)) list (*super class parameter instances*))) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
84 |
type program = stmt Graph.T |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
85 |
val empty_funs: program -> string list |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
86 |
val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
87 |
val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
88 |
val is_cons: program -> string -> bool |
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
89 |
val is_case: stmt -> bool |
32895 | 90 |
val labelled_name: theory -> program -> string -> string |
91 |
val group_stmts: theory -> program |
|
92 |
-> ((string * stmt) list * (string * stmt) list |
|
93 |
* ((string * stmt) list * (string * stmt) list)) list |
|
24219 | 94 |
|
31036 | 95 |
val read_const_exprs: theory -> string list -> string list * string list |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
96 |
val consts_program: theory -> bool -> string list -> string list * (naming * program) |
41184 | 97 |
val dynamic_conv: theory -> (naming -> program |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
98 |
-> ((string * sort) list * typscheme) * iterm -> string list -> conv) |
38672
f1f64375f662
preliminary versions of static_eval_conv(_simple)
haftmann
parents:
38669
diff
changeset
|
99 |
-> conv |
41184 | 100 |
val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
101 |
-> ((string * sort) list * typscheme) * iterm -> string list -> 'a) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
102 |
-> term -> 'a |
41346 | 103 |
val static_conv: theory -> string list -> (naming -> program -> string list |
104 |
-> ((string * sort) list * typscheme) * iterm -> string list -> conv) |
|
38672
f1f64375f662
preliminary versions of static_eval_conv(_simple)
haftmann
parents:
38669
diff
changeset
|
105 |
-> conv |
41184 | 106 |
val static_conv_simple: theory -> string list |
41346 | 107 |
-> (program -> (string * sort) list -> term -> conv) -> conv |
41184 | 108 |
val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list -> |
41346 | 109 |
(naming -> program -> string list |
110 |
-> ((string * sort) list * typscheme) * iterm -> string list -> 'a) |
|
39475 | 111 |
-> term -> 'a |
24219 | 112 |
end; |
113 |
||
28054 | 114 |
structure Code_Thingol: CODE_THINGOL = |
24219 | 115 |
struct |
116 |
||
117 |
(** auxiliary **) |
|
118 |
||
119 |
fun unfoldl dest x = |
|
120 |
case dest x |
|
121 |
of NONE => (x, []) |
|
122 |
| SOME (x1, x2) => |
|
123 |
let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; |
|
124 |
||
125 |
fun unfoldr dest x = |
|
126 |
case dest x |
|
127 |
of NONE => ([], x) |
|
128 |
| SOME (x1, x2) => |
|
129 |
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; |
|
130 |
||
131 |
||
29962
bd4dc7fa742d
tuned comments, stripped ID, deleted superfluous code
haftmann
parents:
29952
diff
changeset
|
132 |
(** language core - types, terms **) |
24219 | 133 |
|
134 |
type vname = string; |
|
135 |
||
136 |
datatype dict = |
|
41782 | 137 |
Dict of string list * plain_dict |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
138 |
and plain_dict = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
139 |
Dict_Const of string * dict list list |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
140 |
| Dict_Var of vname * (int * int) |
24219 | 141 |
|
142 |
datatype itype = |
|
143 |
`%% of string * itype list |
|
144 |
| ITyVar of vname; |
|
145 |
||
44789
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
146 |
type const = string * (((itype list * dict list list) * |
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
147 |
(itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*)) |
24591 | 148 |
|
24219 | 149 |
datatype iterm = |
24591 | 150 |
IConst of const |
31889 | 151 |
| IVar of vname option |
24219 | 152 |
| `$ of iterm * iterm |
31888 | 153 |
| `|=> of (vname option * itype) * iterm |
24219 | 154 |
| ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; |
155 |
(*see also signature*) |
|
156 |
||
32909 | 157 |
fun is_IVar (IVar _) = true |
158 |
| is_IVar _ = false; |
|
159 |
||
41782 | 160 |
fun is_IAbs (_ `|=> _) = true |
161 |
| is_IAbs _ = false; |
|
162 |
||
24219 | 163 |
val op `$$ = Library.foldl (op `$); |
31724 | 164 |
val op `|==> = Library.foldr (op `|=>); |
24219 | 165 |
|
166 |
val unfold_app = unfoldl |
|
167 |
(fn op `$ t => SOME t |
|
168 |
| _ => NONE); |
|
169 |
||
31874 | 170 |
val unfold_abs = unfoldr |
171 |
(fn op `|=> t => SOME t |
|
24219 | 172 |
| _ => NONE); |
173 |
||
174 |
val split_let = |
|
175 |
(fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) |
|
176 |
| _ => NONE); |
|
177 |
||
178 |
val unfold_let = unfoldr split_let; |
|
179 |
||
180 |
fun unfold_const_app t = |
|
181 |
case unfold_app t |
|
182 |
of (IConst c, ts) => SOME (c, ts) |
|
183 |
| _ => NONE; |
|
184 |
||
32917 | 185 |
fun fold_constexprs f = |
186 |
let |
|
187 |
fun fold' (IConst c) = f c |
|
188 |
| fold' (IVar _) = I |
|
189 |
| fold' (t1 `$ t2) = fold' t1 #> fold' t2 |
|
190 |
| fold' (_ `|=> t) = fold' t |
|
191 |
| fold' (ICase (((t, _), ds), _)) = fold' t |
|
192 |
#> fold (fn (pat, body) => fold' pat #> fold' body) ds |
|
193 |
in fold' end; |
|
194 |
||
195 |
val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c); |
|
196 |
||
197 |
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys |
|
198 |
| add_tycos (ITyVar _) = I; |
|
199 |
||
44788
8b935f1b3cf8
changing const type to pass along if typing annotations are necessary for disambigous terms
bulwahn
parents:
44338
diff
changeset
|
200 |
val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys); |
24219 | 201 |
|
202 |
fun fold_varnames f = |
|
203 |
let |
|
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
204 |
fun fold_aux add f = |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
205 |
let |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
206 |
fun fold_term _ (IConst _) = I |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
207 |
| fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
208 |
| fold_term _ (IVar NONE) = I |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
209 |
| fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2 |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
210 |
| fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
211 |
| fold_term vs ((NONE, _) `|=> t) = fold_term vs t |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
212 |
| fold_term vs (ICase (((t, _), ds), _)) = fold_term vs t #> fold (fold_case vs) ds |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
213 |
and fold_case vs (p, t) = fold_term (add p vs) t; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
214 |
in fold_term [] end; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
215 |
fun add t = fold_aux add (insert (op =)) t; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
216 |
in fold_aux add f end; |
24219 | 217 |
|
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
218 |
fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; |
31874 | 219 |
|
31889 | 220 |
fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t) |
31888 | 221 |
| split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t |
31889 | 222 |
of ICase (((IVar (SOME w), _), [(p, t')]), _) => |
31888 | 223 |
if v = w andalso (exists_var p v orelse not (exists_var t' v)) |
31889 | 224 |
then ((p, ty), t') |
225 |
else ((IVar (SOME v), ty), t) |
|
226 |
| _ => ((IVar (SOME v), ty), t)) |
|
31888 | 227 |
| split_pat_abs _ = NONE; |
31874 | 228 |
|
229 |
val unfold_pat_abs = unfoldr split_pat_abs; |
|
24219 | 230 |
|
31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
231 |
fun unfold_abs_eta [] t = ([], t) |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
232 |
| unfold_abs_eta (_ :: tys) (v_ty `|=> t) = |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
233 |
let |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
234 |
val (vs_tys, t') = unfold_abs_eta tys t; |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
235 |
in (v_ty :: vs_tys, t') end |
31892 | 236 |
| unfold_abs_eta tys t = |
31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
237 |
let |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
238 |
val ctxt = fold_varnames Name.declare t Name.context; |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
239 |
val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys); |
31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
240 |
in (vs_tys, t `$$ map (IVar o fst) vs_tys) end; |
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset
|
241 |
|
44789
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
242 |
fun eta_expand k (c as (name, ((_, (tys, _)), _)), ts) = |
24219 | 243 |
let |
244 |
val j = length ts; |
|
245 |
val l = k - j; |
|
37841 | 246 |
val _ = if l > length tys |
247 |
then error ("Impossible eta-expansion for constant " ^ quote name) else (); |
|
24219 | 248 |
val ctxt = (fold o fold_varnames) Name.declare ts Name.context; |
31889 | 249 |
val vs_tys = (map o apfst) SOME |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
250 |
(Name.invent_names ctxt "a" ((take l o drop j) tys)); |
31889 | 251 |
in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; |
24219 | 252 |
|
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
253 |
fun contains_dict_var t = |
24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset
|
254 |
let |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
255 |
fun cont_dict (Dict (_, d)) = cont_plain_dict d |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
256 |
and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
257 |
| cont_plain_dict (Dict_Var _) = true; |
44788
8b935f1b3cf8
changing const type to pass along if typing annotations are necessary for disambigous terms
bulwahn
parents:
44338
diff
changeset
|
258 |
fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss |
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
259 |
| cont_term (IVar _) = false |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
260 |
| cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2 |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
261 |
| cont_term (_ `|=> t) = cont_term t |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
262 |
| cont_term (ICase (_, t)) = cont_term t; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
263 |
in cont_term t end; |
25621 | 264 |
|
265 |
||
28688 | 266 |
(** namings **) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
267 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
268 |
(* policies *) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
269 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
270 |
local |
33172 | 271 |
fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); |
272 |
fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst |
|
273 |
of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
274 |
| thyname :: _ => thyname; |
28706 | 275 |
fun thyname_of_const thy c = case AxClass.class_of_param thy c |
276 |
of SOME class => thyname_of_class thy class |
|
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
277 |
| NONE => (case Code.get_type_of_constr_or_abstr thy c |
35226 | 278 |
of SOME (tyco, _) => Codegen.thyname_of_type thy tyco |
33172 | 279 |
| NONE => Codegen.thyname_of_const thy c); |
33420 | 280 |
fun purify_base "==>" = "follows" |
39566 | 281 |
| purify_base "==" = "meta_eq" |
31036 | 282 |
| purify_base s = Name.desymbolize false s; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
283 |
fun namify thy get_basename get_thyname name = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
284 |
let |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
285 |
val prefix = get_thyname thy name; |
31036 | 286 |
val base = (purify_base o get_basename) name; |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
287 |
in Long_Name.append prefix base end; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
288 |
in |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
289 |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
290 |
fun namify_class thy = namify thy Long_Name.base_name thyname_of_class; |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
291 |
fun namify_classrel thy = namify thy (fn (sub_class, super_class) => |
37431 | 292 |
Long_Name.base_name super_class ^ "_" ^ Long_Name.base_name sub_class) |
33172 | 293 |
(fn thy => thyname_of_class thy o fst); |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
294 |
(*order fits nicely with composed projections*) |
28688 | 295 |
fun namify_tyco thy "fun" = "Pure.fun" |
33172 | 296 |
| namify_tyco thy tyco = namify thy Long_Name.base_name Codegen.thyname_of_type tyco; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
297 |
fun namify_instance thy = namify thy (fn (class, tyco) => |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
298 |
Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance; |
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
299 |
fun namify_const thy = namify thy Long_Name.base_name thyname_of_const; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
300 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
301 |
end; (* local *) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
302 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
303 |
|
28688 | 304 |
(* data *) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
305 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
306 |
datatype naming = Naming of { |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
307 |
class: class Symtab.table * Name.context, |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
308 |
classrel: string Symreltab.table * Name.context, |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
309 |
tyco: string Symtab.table * Name.context, |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
310 |
instance: string Symreltab.table * Name.context, |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
311 |
const: string Symtab.table * Name.context |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
312 |
} |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
313 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
314 |
fun dest_Naming (Naming naming) = naming; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
315 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
316 |
val empty_naming = Naming { |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
317 |
class = (Symtab.empty, Name.context), |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
318 |
classrel = (Symreltab.empty, Name.context), |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
319 |
tyco = (Symtab.empty, Name.context), |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
320 |
instance = (Symreltab.empty, Name.context), |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
321 |
const = (Symtab.empty, Name.context) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
322 |
}; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
323 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
324 |
local |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
325 |
fun mk_naming (class, classrel, tyco, instance, const) = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
326 |
Naming { class = class, classrel = classrel, |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
327 |
tyco = tyco, instance = instance, const = const }; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
328 |
fun map_naming f (Naming { class, classrel, tyco, instance, const }) = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
329 |
mk_naming (f (class, classrel, tyco, instance, const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
330 |
in |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
331 |
fun map_class f = map_naming |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
332 |
(fn (class, classrel, tyco, inst, const) => |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
333 |
(f class, classrel, tyco, inst, const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
334 |
fun map_classrel f = map_naming |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
335 |
(fn (class, classrel, tyco, inst, const) => |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
336 |
(class, f classrel, tyco, inst, const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
337 |
fun map_tyco f = map_naming |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
338 |
(fn (class, classrel, tyco, inst, const) => |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
339 |
(class, classrel, f tyco, inst, const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
340 |
fun map_instance f = map_naming |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
341 |
(fn (class, classrel, tyco, inst, const) => |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
342 |
(class, classrel, tyco, f inst, const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
343 |
fun map_const f = map_naming |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
344 |
(fn (class, classrel, tyco, inst, const) => |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
345 |
(class, classrel, tyco, inst, f const)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
346 |
end; (*local*) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
347 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
348 |
fun add_variant update (thing, name) (tab, used) = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
349 |
let |
43326
47cf4bc789aa
simplified Name.variant -- discontinued builtin fold_map;
wenzelm
parents:
43048
diff
changeset
|
350 |
val (name', used') = Name.variant name used; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
351 |
val tab' = update (thing, name') tab; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
352 |
in (tab', used') end; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
353 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
354 |
fun declare thy mapp lookup update namify thing = |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
355 |
mapp (add_variant update (thing, namify thy thing)) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
356 |
#> `(fn naming => the (lookup naming thing)); |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
357 |
|
28688 | 358 |
|
359 |
(* lookup and declare *) |
|
360 |
||
361 |
local |
|
362 |
||
363 |
val suffix_class = "class"; |
|
364 |
val suffix_classrel = "classrel" |
|
365 |
val suffix_tyco = "tyco"; |
|
366 |
val suffix_instance = "inst"; |
|
367 |
val suffix_const = "const"; |
|
368 |
||
369 |
fun add_suffix nsp NONE = NONE |
|
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
370 |
| add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp); |
28688 | 371 |
|
372 |
in |
|
373 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
374 |
val lookup_class = add_suffix suffix_class |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
375 |
oo Symtab.lookup o fst o #class o dest_Naming; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
376 |
val lookup_classrel = add_suffix suffix_classrel |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
377 |
oo Symreltab.lookup o fst o #classrel o dest_Naming; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
378 |
val lookup_tyco = add_suffix suffix_tyco |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
379 |
oo Symtab.lookup o fst o #tyco o dest_Naming; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
380 |
val lookup_instance = add_suffix suffix_instance |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
381 |
oo Symreltab.lookup o fst o #instance o dest_Naming; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
382 |
val lookup_const = add_suffix suffix_const |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
383 |
oo Symtab.lookup o fst o #const o dest_Naming; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
384 |
|
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
385 |
fun declare_class thy = declare thy map_class |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
386 |
lookup_class Symtab.update_new namify_class; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
387 |
fun declare_classrel thy = declare thy map_classrel |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
388 |
lookup_classrel Symreltab.update_new namify_classrel; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
389 |
fun declare_tyco thy = declare thy map_tyco |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
390 |
lookup_tyco Symtab.update_new namify_tyco; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
391 |
fun declare_instance thy = declare thy map_instance |
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset
|
392 |
lookup_instance Symreltab.update_new namify_instance; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
393 |
fun declare_const thy = declare thy map_const |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
394 |
lookup_const Symtab.update_new namify_const; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
395 |
|
31054 | 396 |
fun ensure_declared_const thy const naming = |
397 |
case lookup_const naming const |
|
398 |
of SOME const' => (const', naming) |
|
399 |
| NONE => declare_const thy const naming; |
|
400 |
||
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
401 |
val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
402 |
(*depends on add_suffix*); |
34084 | 403 |
|
28688 | 404 |
val unfold_fun = unfoldr |
34084 | 405 |
(fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
406 |
| _ => NONE); |
28688 | 407 |
|
37640 | 408 |
fun unfold_fun_n n ty = |
409 |
let |
|
410 |
val (tys1, ty1) = unfold_fun ty; |
|
411 |
val (tys3, tys2) = chop n tys1; |
|
412 |
val ty3 = Library.foldr (fn (ty1, ty2) => fun_tyco `%% [ty1, ty2]) (tys2, ty1); |
|
413 |
in (tys3, ty3) end; |
|
414 |
||
28688 | 415 |
end; (* local *) |
416 |
||
24219 | 417 |
|
27103 | 418 |
(** statements, abstract programs **) |
24219 | 419 |
|
420 |
type typscheme = (vname * sort) list * itype; |
|
37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset
|
421 |
datatype stmt = |
27024 | 422 |
NoStmt |
37437 | 423 |
| Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option) |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
424 |
| Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
425 |
| Datatypecons of string * string |
37447
ad3e04f289b6
transitive superclasses were also only a misunderstanding
haftmann
parents:
37446
diff
changeset
|
426 |
| Class of class * (vname * ((class * string) list * (string * itype) list)) |
24219 | 427 |
| Classrel of class * class |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
428 |
| Classparam of string * class |
24219 | 429 |
| Classinst of (class * (string * (vname * sort) list)) |
37445
e372fa3c7239
dropped obscure type argument weakening mapping -- was only a misunderstanding
haftmann
parents:
37440
diff
changeset
|
430 |
* ((class * (string * (string * dict list list))) list |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
431 |
* (((string * const) * (thm * bool)) list |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
432 |
* ((string * const) * (thm * bool)) list)) |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
433 |
(*see also signature*); |
24219 | 434 |
|
27103 | 435 |
type program = stmt Graph.T; |
24219 | 436 |
|
27103 | 437 |
fun empty_funs program = |
37437 | 438 |
Graph.fold (fn (name, (Fun (c, ((_, []), _)), _)) => cons c |
27103 | 439 |
| _ => I) program []; |
24219 | 440 |
|
27711 | 441 |
fun map_terms_bottom_up f (t as IConst _) = f t |
442 |
| map_terms_bottom_up f (t as IVar _) = f t |
|
443 |
| map_terms_bottom_up f (t1 `$ t2) = f |
|
444 |
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) |
|
31724 | 445 |
| map_terms_bottom_up f ((v, ty) `|=> t) = f |
446 |
((v, ty) `|=> map_terms_bottom_up f t) |
|
27711 | 447 |
| map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f |
448 |
(ICase (((map_terms_bottom_up f t, ty), (map o pairself) |
|
449 |
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0)); |
|
450 |
||
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
451 |
fun map_classparam_instances_as_term f = |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
452 |
(map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const') |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
453 |
|
27711 | 454 |
fun map_terms_stmt f NoStmt = NoStmt |
37437 | 455 |
| map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst) |
456 |
(fn (ts, t) => (map f ts, f t)) eqs), case_cong)) |
|
27711 | 457 |
| map_terms_stmt f (stmt as Datatype _) = stmt |
458 |
| map_terms_stmt f (stmt as Datatypecons _) = stmt |
|
459 |
| map_terms_stmt f (stmt as Class _) = stmt |
|
460 |
| map_terms_stmt f (stmt as Classrel _) = stmt |
|
461 |
| map_terms_stmt f (stmt as Classparam _) = stmt |
|
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
462 |
| map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) = |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
463 |
Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances)); |
27711 | 464 |
|
27103 | 465 |
fun is_cons program name = case Graph.get_node program name |
24219 | 466 |
of Datatypecons _ => true |
467 |
| _ => false; |
|
468 |
||
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
469 |
fun is_case (Fun (_, (_, SOME _))) = true |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
470 |
| is_case _ = false; |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
471 |
|
43048
c62bed03fbce
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents:
42385
diff
changeset
|
472 |
fun lookup_classparam_instance program name = program |> Graph.get_first |
c62bed03fbce
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents:
42385
diff
changeset
|
473 |
(fn (_, (Classinst ((class, _), (_, (param_insts, _))), _)) => |
c62bed03fbce
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents:
42385
diff
changeset
|
474 |
Option.map (fn ((const, _), _) => (class, const)) |
c62bed03fbce
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents:
42385
diff
changeset
|
475 |
(find_first (fn ((_, (inst_const, _)), _) => inst_const = name) param_insts) | _ => NONE) |
c62bed03fbce
improving heuristics of type annotations in contravariant positions for the special case with instances of the class partial_term_of
bulwahn
parents:
42385
diff
changeset
|
476 |
|
42359 | 477 |
fun labelled_name thy program name = |
42361 | 478 |
let val ctxt = Proof_Context.init_global thy in |
42359 | 479 |
case Graph.get_node program name of |
480 |
Fun (c, _) => quote (Code.string_of_const thy c) |
|
42361 | 481 |
| Datatype (tyco, _) => "type " ^ quote (Proof_Context.extern_type ctxt tyco) |
42359 | 482 |
| Datatypecons (c, _) => quote (Code.string_of_const thy c) |
42361 | 483 |
| Class (class, _) => "class " ^ quote (Proof_Context.extern_class ctxt class) |
42359 | 484 |
| Classrel (sub, super) => |
485 |
let |
|
486 |
val Class (sub, _) = Graph.get_node program sub; |
|
487 |
val Class (super, _) = Graph.get_node program super; |
|
488 |
in |
|
42361 | 489 |
quote (Proof_Context.extern_class ctxt sub ^ " < " ^ Proof_Context.extern_class ctxt super) |
42359 | 490 |
end |
491 |
| Classparam (c, _) => quote (Code.string_of_const thy c) |
|
492 |
| Classinst ((class, (tyco, _)), _) => |
|
493 |
let |
|
494 |
val Class (class, _) = Graph.get_node program class; |
|
495 |
val Datatype (tyco, _) = Graph.get_node program tyco; |
|
496 |
in |
|
42361 | 497 |
quote (Proof_Context.extern_type ctxt tyco ^ " :: " ^ Proof_Context.extern_class ctxt class) |
42359 | 498 |
end |
499 |
end; |
|
32895 | 500 |
|
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
501 |
fun linear_stmts program = |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
502 |
rev (Graph.strong_conn program) |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
503 |
|> map (AList.make (Graph.get_node program)); |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
504 |
|
32895 | 505 |
fun group_stmts thy program = |
506 |
let |
|
507 |
fun is_fun (_, Fun _) = true | is_fun _ = false; |
|
508 |
fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false; |
|
509 |
fun is_datatype (_, Datatype _) = true | is_datatype _ = false; |
|
510 |
fun is_class (_, Class _) = true | is_class _ = false; |
|
511 |
fun is_classrel (_, Classrel _) = true | is_classrel _ = false; |
|
512 |
fun is_classparam (_, Classparam _) = true | is_classparam _ = false; |
|
513 |
fun is_classinst (_, Classinst _) = true | is_classinst _ = false; |
|
514 |
fun group stmts = |
|
515 |
if forall (is_datatypecons orf is_datatype) stmts |
|
516 |
then (filter is_datatype stmts, [], ([], [])) |
|
517 |
else if forall (is_class orf is_classrel orf is_classparam) stmts |
|
518 |
then ([], filter is_class stmts, ([], [])) |
|
519 |
else if forall (is_fun orf is_classinst) stmts |
|
520 |
then ([], [], List.partition is_fun stmts) |
|
521 |
else error ("Illegal mutual dependencies: " ^ |
|
522 |
(commas o map (labelled_name thy program o fst)) stmts) |
|
523 |
in |
|
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
524 |
linear_stmts program |
32895 | 525 |
|> map group |
526 |
end; |
|
527 |
||
24219 | 528 |
|
27103 | 529 |
(** translation kernel **) |
24219 | 530 |
|
28724 | 531 |
(* generic mechanisms *) |
532 |
||
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
533 |
fun ensure_stmt lookup declare generate thing (dep, (naming, program)) = |
24219 | 534 |
let |
28706 | 535 |
fun add_dep name = case dep of NONE => I |
536 |
| SOME dep => Graph.add_edge (dep, name); |
|
537 |
val (name, naming') = case lookup naming thing |
|
538 |
of SOME name => (name, naming) |
|
539 |
| NONE => declare thing naming; |
|
540 |
in case try (Graph.get_node program) name |
|
541 |
of SOME stmt => program |
|
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
542 |
|> add_dep name |
28706 | 543 |
|> pair naming' |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
544 |
|> pair dep |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
545 |
|> pair name |
28706 | 546 |
| NONE => program |
547 |
|> Graph.default_node (name, NoStmt) |
|
548 |
|> add_dep name |
|
549 |
|> pair naming' |
|
550 |
|> curry generate (SOME name) |
|
551 |
||> snd |
|
552 |
|-> (fn stmt => (apsnd o Graph.map_node name) (K stmt)) |
|
553 |
|> pair dep |
|
554 |
|> pair name |
|
24219 | 555 |
end; |
556 |
||
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
557 |
exception PERMISSIVE of unit; |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
558 |
|
37698 | 559 |
fun translation_error thy permissive some_thm msg sub_msg = |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
560 |
if permissive |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
561 |
then raise PERMISSIVE () |
42385
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
562 |
else |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
563 |
let |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
564 |
val err_thm = |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
565 |
(case some_thm of |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
566 |
SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
567 |
| NONE => ""); |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
568 |
in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end; |
37698 | 569 |
|
570 |
fun not_wellsorted thy permissive some_thm ty sort e = |
|
571 |
let |
|
42385
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
572 |
val ctxt = Syntax.init_pretty_global thy; |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
573 |
val err_class = Sorts.class_error ctxt e; |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
574 |
val err_typ = |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
575 |
"Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^ |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
576 |
Syntax.string_of_sort_global thy sort; |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
577 |
in |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
578 |
translation_error thy permissive some_thm "Wellsortedness error" |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
579 |
(err_typ ^ "\n" ^ err_class) |
b46b47775cbe
simplified Sorts.class_error: plain Proof.context;
wenzelm
parents:
42383
diff
changeset
|
580 |
end; |
26972 | 581 |
|
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
582 |
(* inference of type annotations for disambiguation with type classes *) |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
583 |
|
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
584 |
fun annotate_term (Const (c', T'), Const (c, T)) tvar_names = |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
585 |
let |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
586 |
val tvar_names' = Term.add_tvar_namesT T' tvar_names |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
587 |
in |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
588 |
(Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names') |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
589 |
end |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
590 |
| annotate_term (t1 $ u1, t $ u) tvar_names = |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
591 |
let |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
592 |
val (u', tvar_names') = annotate_term (u1, u) tvar_names |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
593 |
val (t', tvar_names'') = annotate_term (t1, t) tvar_names' |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
594 |
in |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
595 |
(t' $ u', tvar_names'') |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
596 |
end |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
597 |
| annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names = |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
598 |
apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names) |
44855
f4a6786057d9
stating more explicitly our expectation that these two terms have the same term structure
bulwahn
parents:
44854
diff
changeset
|
599 |
| annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names) |
f4a6786057d9
stating more explicitly our expectation that these two terms have the same term structure
bulwahn
parents:
44854
diff
changeset
|
600 |
| annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names) |
f4a6786057d9
stating more explicitly our expectation that these two terms have the same term structure
bulwahn
parents:
44854
diff
changeset
|
601 |
| annotate_term (Bound _, t as Bound _) tvar_names = (t, tvar_names) |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
602 |
|
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
603 |
fun annotate_eqns thy (c, ty) eqns = |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
604 |
let |
44795
238c6c7da908
setting const_sorts to false in the type inference of the code generator
bulwahn
parents:
44793
diff
changeset
|
605 |
val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
606 |
val erase = map_types (fn _ => Type_Infer.anyT []) |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
607 |
val reinfer = singleton (Type_Infer_Context.infer_types ctxt) |
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
608 |
fun add_annotations (args, (rhs, some_abs)) = |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
609 |
let |
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
610 |
val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args) |
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
611 |
val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs)))) |
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
612 |
val (rhs', _) = annotate_term (reinferred_rhs, rhs) [] |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
613 |
in |
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
614 |
(args, (rhs', some_abs)) |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
615 |
end |
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
616 |
in |
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
617 |
map (apfst add_annotations) eqns |
44790
c13fdf710a40
adding type inference for disambiguation annotations in code equation
bulwahn
parents:
44789
diff
changeset
|
618 |
end; |
28724 | 619 |
|
620 |
(* translation *) |
|
621 |
||
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
622 |
fun ensure_tyco thy algbr eqngr permissive tyco = |
30932 | 623 |
let |
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40711
diff
changeset
|
624 |
val ((vs, cos), _) = Code.get_type thy tyco; |
30932 | 625 |
val stmt_datatype = |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
626 |
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs |
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40711
diff
changeset
|
627 |
##>> fold_map (fn (c, (vs, tys)) => |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
628 |
ensure_const thy algbr eqngr permissive c |
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40711
diff
changeset
|
629 |
##>> pair (map (unprefix "'" o fst) vs) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
630 |
##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
631 |
#>> (fn info => Datatype (tyco, info)); |
30932 | 632 |
in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
633 |
and ensure_const thy algbr eqngr permissive c = |
30932 | 634 |
let |
635 |
fun stmt_datatypecons tyco = |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
636 |
ensure_tyco thy algbr eqngr permissive tyco |
30932 | 637 |
#>> (fn tyco => Datatypecons (c, tyco)); |
638 |
fun stmt_classparam class = |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
639 |
ensure_class thy algbr eqngr permissive class |
30932 | 640 |
#>> (fn class => Classparam (c, class)); |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34251
diff
changeset
|
641 |
fun stmt_fun cert = |
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset
|
642 |
let |
35226 | 643 |
val ((vs, ty), eqns) = Code.equations_of_cert thy cert; |
44854
0b3d3570ab31
revisiting type annotations for Haskell: necessary type annotations are not inferred on the provided theorems but using the arguments and right hand sides, as these might differ in the case of constants with abstract code types
bulwahn
parents:
44796
diff
changeset
|
644 |
val eqns' = annotate_eqns thy (c, ty) eqns |
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
645 |
val some_case_cong = Code.get_case_cong thy c; |
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset
|
646 |
in |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
647 |
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
648 |
##>> translate_typ thy algbr eqngr permissive ty |
44791 | 649 |
##>> translate_eqns thy algbr eqngr permissive eqns' |
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
650 |
#>> (fn info => Fun (c, (info, some_case_cong))) |
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset
|
651 |
end; |
35299
4f4d5bf4ea08
proper distinction of code datatypes and abstypes
haftmann
parents:
35226
diff
changeset
|
652 |
val stmt_const = case Code.get_type_of_constr_or_abstr thy c |
35226 | 653 |
of SOME (tyco, _) => stmt_datatypecons tyco |
30932 | 654 |
| NONE => (case AxClass.class_of_param thy c |
655 |
of SOME class => stmt_classparam class |
|
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34251
diff
changeset
|
656 |
| NONE => stmt_fun (Code_Preproc.cert eqngr c)) |
30932 | 657 |
in ensure_stmt lookup_const (declare_const thy) stmt_const c end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
658 |
and ensure_class thy (algbr as (_, algebra)) eqngr permissive class = |
24918 | 659 |
let |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
660 |
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; |
24969 | 661 |
val cs = #params (AxClass.get_info thy class); |
24918 | 662 |
val stmt_class = |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
663 |
fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
664 |
##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
665 |
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
666 |
##>> translate_typ thy algbr eqngr permissive ty) cs |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
667 |
#>> (fn info => Class (class, (unprefix "'" Name.aT, info))) |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
668 |
in ensure_stmt lookup_class (declare_class thy) stmt_class class end |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
669 |
and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) = |
24918 | 670 |
let |
671 |
val stmt_classrel = |
|
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
672 |
ensure_class thy algbr eqngr permissive sub_class |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
673 |
##>> ensure_class thy algbr eqngr permissive super_class |
24918 | 674 |
#>> Classrel; |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
675 |
in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
676 |
and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) = |
24918 | 677 |
let |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
678 |
val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
679 |
val these_classparams = these o try (#params o AxClass.get_info thy); |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
680 |
val classparams = these_classparams class; |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
681 |
val further_classparams = maps these_classparams |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
682 |
((Sorts.complete_sort algebra o Sorts.super_classes algebra) class); |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
683 |
val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); |
24918 | 684 |
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; |
685 |
val vs' = map2 (fn (v, sort1) => fn sort2 => (v, |
|
686 |
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; |
|
687 |
val arity_typ = Type (tyco, map TFree vs); |
|
688 |
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); |
|
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
689 |
fun translate_super_instance super_class = |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
690 |
ensure_class thy algbr eqngr permissive super_class |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
691 |
##>> ensure_classrel thy algbr eqngr permissive (class, super_class) |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
692 |
##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class]) |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
693 |
#>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) => |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
694 |
(super_class, (classrel, (inst, dss)))); |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
695 |
fun translate_classparam_instance (c, ty) = |
24918 | 696 |
let |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
697 |
val raw_const = Const (c, map_type_tfree (K arity_typ') ty); |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
698 |
val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const); |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
699 |
val const = (apsnd Logic.unvarifyT_global o dest_Const o snd |
24918 | 700 |
o Logic.dest_equals o Thm.prop_of) thm; |
701 |
in |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
702 |
ensure_const thy algbr eqngr permissive c |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
703 |
##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE) |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
704 |
#>> (fn (c, IConst const') => ((c, const'), (thm, true))) |
24918 | 705 |
end; |
706 |
val stmt_inst = |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
707 |
ensure_class thy algbr eqngr permissive class |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
708 |
##>> ensure_tyco thy algbr eqngr permissive tyco |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
709 |
##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs |
37384
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
710 |
##>> fold_map translate_super_instance super_classes |
5aba26803073
more consistent naming aroud type classes and instances
haftmann
parents:
37216
diff
changeset
|
711 |
##>> fold_map translate_classparam_instance classparams |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
712 |
##>> fold_map translate_classparam_instance further_classparams |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
713 |
#>> (fn (((((class, tyco), arity_args), super_instances), |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
714 |
classparam_instances), further_classparam_instances) => |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
715 |
Classinst ((class, (tyco, arity_args)), (super_instances, |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
716 |
(classparam_instances, further_classparam_instances)))); |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
717 |
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
718 |
and translate_typ thy algbr eqngr permissive (TFree (v, _)) = |
30932 | 719 |
pair (ITyVar (unprefix "'" v)) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
720 |
| translate_typ thy algbr eqngr permissive (Type (tyco, tys)) = |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
721 |
ensure_tyco thy algbr eqngr permissive tyco |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
722 |
##>> fold_map (translate_typ thy algbr eqngr permissive) tys |
30932 | 723 |
#>> (fn (tyco, tys) => tyco `%% tys) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
724 |
and translate_term thy algbr eqngr permissive some_thm (Const (c, ty), some_abs) = |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
725 |
translate_app thy algbr eqngr permissive some_thm (((c, ty), []), some_abs) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
726 |
| translate_term thy algbr eqngr permissive some_thm (Free (v, _), some_abs) = |
31889 | 727 |
pair (IVar (SOME v)) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
728 |
| translate_term thy algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) = |
24918 | 729 |
let |
42284 | 730 |
val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize false v, ty, t); |
32273 | 731 |
val v'' = if member (op =) (Term.add_free_names t' []) v' |
732 |
then SOME v' else NONE |
|
24918 | 733 |
in |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
734 |
translate_typ thy algbr eqngr permissive ty |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
735 |
##>> translate_term thy algbr eqngr permissive some_thm (t', some_abs) |
32273 | 736 |
#>> (fn (ty, t) => (v'', ty) `|=> t) |
24918 | 737 |
end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
738 |
| translate_term thy algbr eqngr permissive some_thm (t as _ $ _, some_abs) = |
24918 | 739 |
case strip_comb t |
740 |
of (Const (c, ty), ts) => |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
741 |
translate_app thy algbr eqngr permissive some_thm (((c, ty), ts), some_abs) |
24918 | 742 |
| (t', ts) => |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
743 |
translate_term thy algbr eqngr permissive some_thm (t', some_abs) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
744 |
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts |
24918 | 745 |
#>> (fn (t, ts) => t `$$ ts) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
746 |
and translate_eqn thy algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) = |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
747 |
fold_map (translate_term thy algbr eqngr permissive some_thm) args |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
748 |
##>> translate_term thy algbr eqngr permissive some_thm (rhs, some_abs) |
35226 | 749 |
#>> rpair (some_thm, proper) |
37440
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
750 |
and translate_eqns thy algbr eqngr permissive eqns prgrm = |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
751 |
prgrm |> fold_map (translate_eqn thy algbr eqngr permissive) eqns |
a5d44161ba2a
maintain cong rules for case combinators; more precise permissiveness
haftmann
parents:
37437
diff
changeset
|
752 |
handle PERMISSIVE () => ([], prgrm) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
753 |
and translate_const thy algbr eqngr permissive some_thm ((c, ty), some_abs) = |
30932 | 754 |
let |
37698 | 755 |
val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs)) |
35226 | 756 |
andalso Code.is_abstr thy c |
37698 | 757 |
then translation_error thy permissive some_thm |
758 |
"Abstraction violation" ("constant " ^ Code.string_of_const thy c) |
|
759 |
else () |
|
44792
26b19918e670
adding minimalistic implementation for printing the type annotations
bulwahn
parents:
44791
diff
changeset
|
760 |
val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty')) |
26b19918e670
adding minimalistic implementation for printing the type annotations
bulwahn
parents:
44791
diff
changeset
|
761 |
val arg_typs = Sign.const_typargs thy (c, ty'); |
32873 | 762 |
val sorts = Code_Preproc.sortargs eqngr c; |
44792
26b19918e670
adding minimalistic implementation for printing the type annotations
bulwahn
parents:
44791
diff
changeset
|
763 |
val (function_typs, body_typ) = Term.strip_type ty'; |
26972 | 764 |
in |
37698 | 765 |
ensure_const thy algbr eqngr permissive c |
37448
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
766 |
##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs |
3bd4b3809bee
explicit type variable arguments for constructors
haftmann
parents:
37447
diff
changeset
|
767 |
##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts) |
44789
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
768 |
##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs) |
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
769 |
#>> (fn (((c, arg_typs), dss), body_typ :: function_typs) => |
44792
26b19918e670
adding minimalistic implementation for printing the type annotations
bulwahn
parents:
44791
diff
changeset
|
770 |
IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate))) |
26972 | 771 |
end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
772 |
and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
773 |
translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
774 |
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts |
24918 | 775 |
#>> (fn (t, ts) => t `$$ ts) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
776 |
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) = |
24918 | 777 |
let |
40844 | 778 |
fun arg_types num_args ty = fst (chop num_args (binder_types ty)); |
31892 | 779 |
val tys = arg_types num_args (snd c_ty); |
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29277
diff
changeset
|
780 |
val ty = nth tys t_pos; |
31957 | 781 |
fun mk_constr c t = let val n = Code.args_number thy c |
782 |
in ((c, arg_types n (fastype_of t) ---> ty), n) end; |
|
31892 | 783 |
val constrs = if null case_pats then [] |
784 |
else map2 mk_constr case_pats (nth_drop t_pos ts); |
|
785 |
fun casify naming constrs ty ts = |
|
24918 | 786 |
let |
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
787 |
val undefineds = map_filter (lookup_const naming) (Code.undefineds thy); |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
788 |
fun collapse_clause vs_map ts body = |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
789 |
let |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
790 |
in case body |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
791 |
of IConst (c, _) => if member (op =) undefineds c |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
792 |
then [] |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
793 |
else [(ts, body)] |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
794 |
| ICase (((IVar (SOME v), _), subclauses), _) => |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
795 |
if forall (fn (pat', body') => exists_var pat' v |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
796 |
orelse not (exists_var body' v)) subclauses |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
797 |
then case AList.lookup (op =) vs_map v |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
798 |
of SOME i => maps (fn (pat', body') => |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
799 |
collapse_clause (AList.delete (op =) v vs_map) |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
800 |
(nth_map i (K pat') ts) body') subclauses |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
801 |
| NONE => [(ts, body)] |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
802 |
else [(ts, body)] |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
803 |
| _ => [(ts, body)] |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
804 |
end; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
805 |
fun mk_clause mk tys t = |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
806 |
let |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
807 |
val (vs, body) = unfold_abs_eta tys t; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
808 |
val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs []; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
809 |
val ts = map (IVar o fst) vs; |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
810 |
in map mk (collapse_clause vs_map ts body) end; |
31892 | 811 |
val t = nth ts t_pos; |
812 |
val ts_clause = nth_drop t_pos ts; |
|
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
813 |
val clauses = if null case_pats |
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
814 |
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) |
44789
5a062c23c7db
adding the body type as well to the code generation for constants as it is required for type annotations of constants
bulwahn
parents:
44788
diff
changeset
|
815 |
else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) => |
33957 | 816 |
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t) |
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset
|
817 |
(constrs ~~ ts_clause); |
31892 | 818 |
in ((t, ty), clauses) end; |
24918 | 819 |
in |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
820 |
translate_const thy algbr eqngr permissive some_thm (c_ty, NONE) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
821 |
##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
822 |
#>> rpair n) constrs |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
823 |
##>> translate_typ thy algbr eqngr permissive ty |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
824 |
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts |
31892 | 825 |
#-> (fn (((t, constrs), ty), ts) => |
826 |
`(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts))) |
|
24918 | 827 |
end |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
828 |
and translate_app_case thy algbr eqngr permissive some_thm (case_scheme as (num_args, _)) ((c, ty), ts) = |
29973 | 829 |
if length ts < num_args then |
830 |
let |
|
831 |
val k = length ts; |
|
33957 | 832 |
val tys = (take (num_args - k) o drop k o fst o strip_type) ty; |
29973 | 833 |
val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context; |
43329
84472e198515
tuned signature: Name.invent and Name.invent_names;
wenzelm
parents:
43326
diff
changeset
|
834 |
val vs = Name.invent_names ctxt "a" tys; |
29973 | 835 |
in |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
836 |
fold_map (translate_typ thy algbr eqngr permissive) tys |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
837 |
##>> translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts @ map Free vs) |
31888 | 838 |
#>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t) |
29973 | 839 |
end |
840 |
else if length ts > num_args then |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
841 |
translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), take num_args ts) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
842 |
##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts) |
29973 | 843 |
#>> (fn (t, ts) => t `$$ ts) |
844 |
else |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
845 |
translate_case thy algbr eqngr permissive some_thm case_scheme ((c, ty), ts) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
846 |
and translate_app thy algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) = |
29973 | 847 |
case Code.get_case_scheme thy c |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
848 |
of SOME case_scheme => translate_app_case thy algbr eqngr permissive some_thm case_scheme c_ty_ts |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
849 |
| NONE => translate_app_const thy algbr eqngr permissive some_thm (c_ty_ts, some_abs) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
850 |
and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr permissive (v, sort) = |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
851 |
fold_map (ensure_class thy algbr eqngr permissive) (proj_sort sort) |
30932 | 852 |
#>> (fn sort => (unprefix "'" v, sort)) |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
853 |
and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) = |
30932 | 854 |
let |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
855 |
datatype typarg_witness = |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
856 |
Weakening of (class * class) list * plain_typarg_witness |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
857 |
and plain_typarg_witness = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
858 |
Global of (class * string) * typarg_witness list list |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
859 |
| Local of string * (int * sort); |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
860 |
fun class_relation ((Weakening (classrels, x)), sub_class) super_class = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
861 |
Weakening ((sub_class, super_class) :: classrels, x); |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
862 |
fun type_constructor (tyco, _) dss class = |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
863 |
Weakening ([], Global ((class, tyco), (map o map) fst dss)); |
30932 | 864 |
fun type_variable (TFree (v, sort)) = |
865 |
let |
|
866 |
val sort' = proj_sort sort; |
|
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
867 |
in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end; |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
868 |
val typarg_witnesses = Sorts.of_sort_derivation algebra |
36102
a51d1d154c71
of_sort_derivation: pass-through full type information -- following the version by krauss/schropp;
wenzelm
parents:
35961
diff
changeset
|
869 |
{class_relation = K (Sorts.classrel_derivation algebra class_relation), |
35961
00e48e1d9afd
Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
wenzelm
parents:
35845
diff
changeset
|
870 |
type_constructor = type_constructor, |
37698 | 871 |
type_variable = type_variable} (ty, proj_sort sort) |
872 |
handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e; |
|
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
873 |
fun mk_dict (Weakening (classrels, x)) = |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
874 |
fold_map (ensure_classrel thy algbr eqngr permissive) classrels |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
875 |
##>> mk_plain_dict x |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
876 |
#>> Dict |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
877 |
and mk_plain_dict (Global (inst, dss)) = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
878 |
ensure_inst thy algbr eqngr permissive inst |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
879 |
##>> (fold_map o fold_map) mk_dict dss |
41118
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
880 |
#>> (fn (inst, dss) => Dict_Const (inst, dss)) |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
881 |
| mk_plain_dict (Local (v, (n, sort))) = |
b290841cd3b0
separated dictionary weakning into separate type
haftmann
parents:
41100
diff
changeset
|
882 |
pair (Dict_Var (unprefix "'" v, (n, length sort))) |
41100
6c0940392fb4
dictionary constants must permit explicit weakening of classes;
haftmann
parents:
40844
diff
changeset
|
883 |
in fold_map mk_dict typarg_witnesses end; |
24918 | 884 |
|
25969 | 885 |
|
27103 | 886 |
(* store *) |
887 |
||
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
34084
diff
changeset
|
888 |
structure Program = Code_Data |
27103 | 889 |
( |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
890 |
type T = naming * program; |
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
891 |
val empty = (empty_naming, Graph.empty); |
27103 | 892 |
); |
893 |
||
39397 | 894 |
fun invoke_generation ignore_cache thy (algebra, eqngr) f name = |
895 |
Program.change_yield (if ignore_cache then NONE else SOME thy) |
|
896 |
(fn naming_program => (NONE, naming_program) |
|
897 |
|> f thy algebra eqngr name |
|
898 |
|-> (fn name => fn (_, naming_program) => (name, naming_program))); |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
899 |
|
27103 | 900 |
|
901 |
(* program generation *) |
|
902 |
||
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
903 |
fun consts_program thy permissive consts = |
27103 | 904 |
let |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
905 |
fun project_consts consts (naming, program) = |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
906 |
if permissive then (consts, (naming, program)) |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
907 |
else (consts, (naming, Graph.subgraph |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
908 |
(member (op =) (Graph.all_succs program consts)) program)); |
32873 | 909 |
fun generate_consts thy algebra eqngr = |
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
910 |
fold_map (ensure_const thy algebra eqngr permissive); |
27103 | 911 |
in |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
912 |
invoke_generation permissive thy (Code_Preproc.obtain false thy consts []) |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
913 |
generate_consts consts |
27103 | 914 |
|-> project_consts |
915 |
end; |
|
916 |
||
917 |
||
918 |
(* value evaluation *) |
|
25969 | 919 |
|
32873 | 920 |
fun ensure_value thy algbr eqngr t = |
24918 | 921 |
let |
922 |
val ty = fastype_of t; |
|
923 |
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) |
|
924 |
o dest_TFree))) t []; |
|
925 |
val stmt_value = |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
926 |
fold_map (translate_tyvar_sort thy algbr eqngr false) vs |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
927 |
##>> translate_typ thy algbr eqngr false ty |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
928 |
##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE) |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
929 |
#>> (fn ((vs, ty), t) => Fun |
37437 | 930 |
(Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE))); |
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset
|
931 |
fun term_value (dep, (naming, program1)) = |
25969 | 932 |
let |
37437 | 933 |
val Fun (_, ((vs_ty, [(([], t), _)]), _)) = |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
934 |
Graph.get_node program1 Term.dummy_patternN; |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43329
diff
changeset
|
935 |
val deps = Graph.immediate_succs program1 Term.dummy_patternN; |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
936 |
val program2 = Graph.del_nodes [Term.dummy_patternN] program1; |
27103 | 937 |
val deps_all = Graph.all_succs program2 deps; |
938 |
val program3 = Graph.subgraph (member (op =) deps_all) program2; |
|
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset
|
939 |
in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end; |
26011 | 940 |
in |
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset
|
941 |
ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN |
26011 | 942 |
#> snd |
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset
|
943 |
#> term_value |
26011 | 944 |
end; |
24219 | 945 |
|
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
946 |
fun original_sorts vs = |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
947 |
map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)); |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
948 |
|
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
949 |
fun dynamic_evaluator thy evaluator algebra eqngr vs t = |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
950 |
let |
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset
|
951 |
val (((naming, program), (((vs', ty'), t'), deps)), _) = |
39397 | 952 |
invoke_generation false thy (algebra, eqngr) ensure_value t; |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
953 |
in evaluator naming program ((original_sorts vs vs', (vs', ty')), t') deps end; |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
954 |
|
41184 | 955 |
fun dynamic_conv thy evaluator = |
956 |
Code_Preproc.dynamic_conv thy (dynamic_evaluator thy evaluator); |
|
39475 | 957 |
|
41184 | 958 |
fun dynamic_value thy postproc evaluator = |
959 |
Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator); |
|
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
960 |
|
41365 | 961 |
fun lift_evaluation thy evaluation' algebra eqngr naming program vs t = |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
962 |
let |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
963 |
val (((_, program'), (((vs', ty'), t'), deps)), _) = |
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
964 |
ensure_value thy algebra eqngr t (NONE, (naming, program)); |
41365 | 965 |
in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end; |
966 |
||
967 |
fun lift_evaluator thy evaluator' consts algebra eqngr = |
|
968 |
let |
|
969 |
fun generate_consts thy algebra eqngr = |
|
970 |
fold_map (ensure_const thy algebra eqngr false); |
|
971 |
val (consts', (naming, program)) = |
|
972 |
invoke_generation true thy (algebra, eqngr) generate_consts consts; |
|
973 |
val evaluation' = evaluator' naming program consts'; |
|
974 |
in lift_evaluation thy evaluation' algebra eqngr naming program end; |
|
975 |
||
976 |
fun lift_evaluator_simple thy evaluator' consts algebra eqngr = |
|
977 |
let |
|
978 |
fun generate_consts thy algebra eqngr = |
|
979 |
fold_map (ensure_const thy algebra eqngr false); |
|
980 |
val (consts', (naming, program)) = |
|
981 |
invoke_generation true thy (algebra, eqngr) generate_consts consts; |
|
982 |
in evaluator' program end; |
|
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
983 |
|
41184 | 984 |
fun static_conv thy consts conv = |
41365 | 985 |
Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts); |
38672
f1f64375f662
preliminary versions of static_eval_conv(_simple)
haftmann
parents:
38669
diff
changeset
|
986 |
|
41184 | 987 |
fun static_conv_simple thy consts conv = |
41365 | 988 |
Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts); |
38672
f1f64375f662
preliminary versions of static_eval_conv(_simple)
haftmann
parents:
38669
diff
changeset
|
989 |
|
41184 | 990 |
fun static_value thy postproc consts evaluator = |
41365 | 991 |
Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts); |
39487
80b2cf3b0779
proper closures for static evaluation; no need for FIXMEs any longer
haftmann
parents:
39475
diff
changeset
|
992 |
|
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
993 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
994 |
(** diagnostic commands **) |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
995 |
|
31036 | 996 |
fun read_const_exprs thy = |
997 |
let |
|
36272
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
998 |
fun consts_of thy' = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I) |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
999 |
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
1000 |
fun belongs_here thy' c = forall |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
1001 |
(fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); |
4d358c582ffb
optionally ignore errors during translation of equations; tuned representation of abstraction points
haftmann
parents:
36210
diff
changeset
|
1002 |
fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); |
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
39566
diff
changeset
|
1003 |
fun read_const_expr "_" = ([], consts_of thy) |
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
39566
diff
changeset
|
1004 |
| read_const_expr s = if String.isSuffix "._" s |
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
39566
diff
changeset
|
1005 |
then ([], consts_of_select (Context.this_theory thy (unsuffix "._" s))) |
31156 | 1006 |
else ([Code.read_const thy s], []); |
31036 | 1007 |
in pairself flat o split_list o map read_const_expr end; |
1008 |
||
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1009 |
fun code_depgr thy consts = |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1010 |
let |
39397 | 1011 |
val (_, eqngr) = Code_Preproc.obtain true thy consts []; |
34173
458ced35abb8
reduced code generator cache to the baremost minimum
haftmann
parents:
34084
diff
changeset
|
1012 |
val all_consts = Graph.all_succs eqngr consts; |
34891
99b9a6290446
code certificates as integral part of code generation
haftmann
parents:
34251
diff
changeset
|
1013 |
in Graph.subgraph (member (op =) all_consts) eqngr end; |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1014 |
|
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31088
diff
changeset
|
1015 |
fun code_thms thy = Pretty.writeln o Code_Preproc.pretty thy o code_depgr thy; |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1016 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1017 |
fun code_deps thy consts = |
27103 | 1018 |
let |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1019 |
val eqngr = code_depgr thy consts; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1020 |
val constss = Graph.strong_conn eqngr; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1021 |
val mapping = Symtab.empty |> fold (fn consts => fold (fn const => |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1022 |
Symtab.update (const, consts)) consts) constss; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1023 |
fun succs consts = consts |
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
43329
diff
changeset
|
1024 |
|> maps (Graph.immediate_succs eqngr) |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1025 |
|> subtract (op =) consts |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1026 |
|> map (the o Symtab.lookup mapping) |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1027 |
|> distinct (op =); |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1028 |
val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; |
31156 | 1029 |
fun namify consts = map (Code.string_of_const thy) consts |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1030 |
|> commas; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1031 |
val prgr = map (fn (consts, constss) => |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1032 |
{ name = namify consts, ID = namify consts, dir = "", unfold = true, |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1033 |
path = "", parents = map namify constss }) conn; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1034 |
in Present.display_graph prgr end; |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1035 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1036 |
local |
27103 | 1037 |
|
31036 | 1038 |
fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy; |
1039 |
fun code_deps_cmd thy = code_deps thy o op @ o read_const_exprs thy; |
|
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1040 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1041 |
in |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1042 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1043 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36272
diff
changeset
|
1044 |
Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36272
diff
changeset
|
1045 |
(Scan.repeat1 Parse.term_group |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1046 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1047 |
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1048 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1049 |
val _ = |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36272
diff
changeset
|
1050 |
Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code" |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36272
diff
changeset
|
1051 |
Keyword.diag |
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36272
diff
changeset
|
1052 |
(Scan.repeat1 Parse.term_group |
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1053 |
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1054 |
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); |
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1055 |
|
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset
|
1056 |
end; |
27103 | 1057 |
|
24219 | 1058 |
end; (*struct*) |
1059 |
||
1060 |
||
28054 | 1061 |
structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol; |