author  wenzelm 
Sun, 25 Oct 2009 20:54:21 +0100  
changeset 33172  61ee96bc9895 
parent 33029  2fefe039edf1 
child 33187  616be6d7997e 
permissions  rwrr 
24219  1 
(* Title: Tools/code/code_thingol.ML 
2 
Author: Florian Haftmann, TU Muenchen 

3 

4 
Intermediate language ("Thingol") 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 = 

18 
DictConst of string * dict list list 

19 
 DictVar of string list * (vname * (int * int)); 

20 
datatype itype = 

21 
`%% of string * itype list 

22 
 ITyVar of vname; 

31049  23 
type const = string * ((itype list * dict list list) * itype list (*types of arguments*)) 
24219  24 
datatype iterm = 
24591  25 
IConst of const 
31889  26 
 IVar of vname option 
24219  27 
 `$ of iterm * iterm 
31888  28 
 `=> of (vname option * itype) * iterm 
24219  29 
 ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; 
30 
(*((term, type), [(selector pattern, body term )]), primitive term)*) 

31 
val `$$ : iterm * iterm list > iterm; 

31888  32 
val `==> : (vname option * itype) list * iterm > iterm; 
24219  33 
type typscheme = (vname * sort) list * itype; 
34 
end; 

35 

36 
signature CODE_THINGOL = 

37 
sig 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

38 
include BASIC_CODE_THINGOL 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

39 
val unfoldl: ('a > ('a * 'b) option) > 'a > 'a * 'b list 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

40 
val unfoldr: ('a > ('b * 'a) option) > 'a > 'b list * 'a 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

41 
val unfold_fun: itype > itype list * itype 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

42 
val unfold_app: iterm > iterm * iterm list 
31888  43 
val unfold_abs: iterm > (vname option * itype) list * iterm 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

44 
val split_let: iterm > (((iterm * itype) * iterm) * iterm) option 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

45 
val unfold_let: iterm > ((iterm * itype) * iterm) list * iterm 
31889  46 
val split_pat_abs: iterm > ((iterm * itype) * iterm) option 
47 
val unfold_pat_abs: iterm > (iterm * itype) list * iterm 

31049  48 
val unfold_const_app: iterm > (const * iterm list) option 
32909  49 
val is_IVar: iterm > bool 
31049  50 
val eta_expand: int > const * iterm list > iterm 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

51 
val contains_dictvar: iterm > bool 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

52 
val locally_monomorphic: iterm > bool 
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

53 
val add_constnames: iterm > string list > string list 
32917  54 
val add_tyconames: iterm > string list > string list 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

55 
val fold_varnames: (string > 'a > 'a) > iterm > 'a > 'a 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

56 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

57 
type naming 
28706  58 
val empty_naming: naming 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

59 
val lookup_class: naming > class > string option 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

60 
val lookup_classrel: naming > class * class > string option 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

61 
val lookup_tyco: naming > string > string option 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

62 
val lookup_instance: naming > class * string > string option 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

63 
val lookup_const: naming > string > string option 
31054  64 
val ensure_declared_const: theory > string > naming > string * naming 
24219  65 

24918  66 
datatype stmt = 
27024  67 
NoStmt 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

68 
 Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

69 
 Datatype of string * ((vname * sort) list * (string * itype list) list) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

70 
 Datatypecons of string * string 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

71 
 Class of class * (vname * ((class * string) list * (string * itype) list)) 
24219  72 
 Classrel of class * class 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

73 
 Classparam of string * class 
24219  74 
 Classinst of (class * (string * (vname * sort) list)) 
75 
* ((class * (string * (string * dict list list))) list 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

76 
* ((string * const) * (thm * bool)) list) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

77 
type program = stmt Graph.T 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

78 
val empty_funs: program > string list 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

79 
val map_terms_bottom_up: (iterm > iterm) > iterm > iterm 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

80 
val map_terms_stmt: (iterm > iterm) > stmt > stmt 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

81 
val is_cons: program > string > bool 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

82 
val contr_classparam_typs: program > string > itype option list 
32895  83 
val labelled_name: theory > program > string > string 
84 
val group_stmts: theory > program 

85 
> ((string * stmt) list * (string * stmt) list 

86 
* ((string * stmt) list * (string * stmt) list)) list 

24219  87 

32358
98c00ee9e786
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents:
32353
diff
changeset

88 
val expand_eta: theory > int > thm > thm 
32928
6bcc35f7ff6d
more explicit notion of canonized code equations
haftmann
parents:
32917
diff
changeset

89 
val canonize_thms: theory > thm list > thm list 
31036  90 
val read_const_exprs: theory > string list > string list * string list 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

91 
val consts_program: theory > string list > string list * (naming * program) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

92 
val cached_program: theory > naming * program 
32123
8bac9ee4b28d
integrated add_triv_classes into evaluation stack
haftmann
parents:
31962
diff
changeset

93 
val eval_conv: theory 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

94 
> (naming > program > ((string * sort) list * typscheme) * iterm > string list > cterm > thm) 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

95 
> cterm > thm 
32123
8bac9ee4b28d
integrated add_triv_classes into evaluation stack
haftmann
parents:
31962
diff
changeset

96 
val eval: theory > ((term > term) > 'a > 'a) 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

97 
> (naming > program > ((string * sort) list * typscheme) * iterm > string list > 'a) 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

98 
> term > 'a 
24219  99 
end; 
100 

28054  101 
structure Code_Thingol: CODE_THINGOL = 
24219  102 
struct 
103 

104 
(** auxiliary **) 

105 

106 
fun unfoldl dest x = 

107 
case dest x 

108 
of NONE => (x, []) 

109 
 SOME (x1, x2) => 

110 
let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end; 

111 

112 
fun unfoldr dest x = 

113 
case dest x 

114 
of NONE => ([], x) 

115 
 SOME (x1, x2) => 

116 
let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end; 

117 

118 

29962
bd4dc7fa742d
tuned comments, stripped ID, deleted superfluous code
haftmann
parents:
29952
diff
changeset

119 
(** language core  types, terms **) 
24219  120 

121 
type vname = string; 

122 

123 
datatype dict = 

124 
DictConst of string * dict list list 

125 
 DictVar of string list * (vname * (int * int)); 

126 

127 
datatype itype = 

128 
`%% of string * itype list 

129 
 ITyVar of vname; 

130 

31049  131 
type const = string * ((itype list * dict list list) * itype list (*types of arguments*)) 
24591  132 

24219  133 
datatype iterm = 
24591  134 
IConst of const 
31889  135 
 IVar of vname option 
24219  136 
 `$ of iterm * iterm 
31888  137 
 `=> of (vname option * itype) * iterm 
24219  138 
 ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; 
139 
(*see also signature*) 

140 

32909  141 
fun is_IVar (IVar _) = true 
142 
 is_IVar _ = false; 

143 

24219  144 
val op `$$ = Library.foldl (op `$); 
31724  145 
val op `==> = Library.foldr (op `=>); 
24219  146 

147 
val unfold_app = unfoldl 

148 
(fn op `$ t => SOME t 

149 
 _ => NONE); 

150 

31874  151 
val unfold_abs = unfoldr 
152 
(fn op `=> t => SOME t 

24219  153 
 _ => NONE); 
154 

155 
val split_let = 

156 
(fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t) 

157 
 _ => NONE); 

158 

159 
val unfold_let = unfoldr split_let; 

160 

161 
fun unfold_const_app t = 

162 
case unfold_app t 

163 
of (IConst c, ts) => SOME (c, ts) 

164 
 _ => NONE; 

165 

32917  166 
fun fold_constexprs f = 
167 
let 

168 
fun fold' (IConst c) = f c 

169 
 fold' (IVar _) = I 

170 
 fold' (t1 `$ t2) = fold' t1 #> fold' t2 

171 
 fold' (_ `=> t) = fold' t 

172 
 fold' (ICase (((t, _), ds), _)) = fold' t 

173 
#> fold (fn (pat, body) => fold' pat #> fold' body) ds 

174 
in fold' end; 

175 

176 
val add_constnames = fold_constexprs (fn (c, _) => insert (op =) c); 

177 

178 
fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys 

179 
 add_tycos (ITyVar _) = I; 

180 

181 
val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys); 

24219  182 

183 
fun fold_varnames f = 

184 
let 

31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

185 
fun fold_aux add f = 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

186 
let 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

187 
fun fold_term _ (IConst _) = I 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

188 
 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

189 
 fold_term _ (IVar NONE) = I 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

190 
 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

191 
 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

192 
 fold_term vs ((NONE, _) `=> t) = fold_term vs t 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

193 
 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

194 
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

195 
in fold_term [] end; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

196 
fun add t = fold_aux add (insert (op =)) t; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

197 
in fold_aux add f end; 
24219  198 

31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

199 
fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false; 
31874  200 

31889  201 
fun split_pat_abs ((NONE, ty) `=> t) = SOME ((IVar NONE, ty), t) 
31888  202 
 split_pat_abs ((SOME v, ty) `=> t) = SOME (case t 
31889  203 
of ICase (((IVar (SOME w), _), [(p, t')]), _) => 
31888  204 
if v = w andalso (exists_var p v orelse not (exists_var t' v)) 
31889  205 
then ((p, ty), t') 
206 
else ((IVar (SOME v), ty), t) 

207 
 _ => ((IVar (SOME v), ty), t)) 

31888  208 
 split_pat_abs _ = NONE; 
31874  209 

210 
val unfold_pat_abs = unfoldr split_pat_abs; 

24219  211 

31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

212 
fun unfold_abs_eta [] t = ([], t) 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

213 
 unfold_abs_eta (_ :: tys) (v_ty `=> t) = 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

214 
let 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

215 
val (vs_tys, t') = unfold_abs_eta tys t; 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

216 
in (v_ty :: vs_tys, t') end 
31892  217 
 unfold_abs_eta tys t = 
31890
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

218 
let 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

219 
val ctxt = fold_varnames Name.declare t Name.context; 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

220 
val vs_tys = (map o apfst) SOME (Name.names ctxt "a" tys); 
e943b039f0ac
an intermediate step towards a refined translation of cases
haftmann
parents:
31889
diff
changeset

221 
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

222 

27711  223 
fun eta_expand k (c as (_, (_, tys)), ts) = 
24219  224 
let 
225 
val j = length ts; 

226 
val l = k  j; 

227 
val ctxt = (fold o fold_varnames) Name.declare ts Name.context; 

31889  228 
val vs_tys = (map o apfst) SOME 
229 
(Name.names ctxt "a" ((curry Library.take l o curry Library.drop j) tys)); 

230 
in vs_tys `==> IConst c `$$ ts @ map (IVar o fst) vs_tys end; 

24219  231 

24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset

232 
fun contains_dictvar t = 
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset

233 
let 
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

234 
fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

235 
 cont_dict (DictVar _) = true; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

236 
fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

237 
 cont_term (IVar _) = false 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

238 
 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

239 
 cont_term (_ `=> t) = cont_term t 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

240 
 cont_term (ICase (_, t)) = cont_term t; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

241 
in cont_term t end; 
24662
f79f6061525c
more precise treatment of free dictionary parameters for evaluation
haftmann
parents:
24591
diff
changeset

242 

25621  243 
fun locally_monomorphic (IConst _) = false 
244 
 locally_monomorphic (IVar _) = true 

245 
 locally_monomorphic (t `$ _) = locally_monomorphic t 

31724  246 
 locally_monomorphic (_ `=> t) = locally_monomorphic t 
25621  247 
 locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds; 
248 

249 

28688  250 
(** namings **) 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

251 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

252 
(* policies *) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

253 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

254 
local 
33172  255 
fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); 
256 
fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst 

257 
of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

258 
 thyname :: _ => thyname; 
28706  259 
fun thyname_of_const thy c = case AxClass.class_of_param thy c 
260 
of SOME class => thyname_of_class thy class 

261 
 NONE => (case Code.get_datatype_of_constr thy c 

33172  262 
of SOME dtco => Codegen.thyname_of_type thy dtco 
263 
 NONE => Codegen.thyname_of_const thy c); 

31036  264 
fun purify_base "op &" = "and" 
265 
 purify_base "op " = "or" 

266 
 purify_base "op >" = "implies" 

267 
 purify_base "op :" = "member" 

268 
 purify_base "op =" = "eq" 

269 
 purify_base "*" = "product" 

270 
 purify_base "+" = "sum" 

271 
 purify_base s = Name.desymbolize false s; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

272 
fun namify thy get_basename get_thyname name = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

273 
let 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

274 
val prefix = get_thyname thy name; 
31036  275 
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

276 
in Long_Name.append prefix base end; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

277 
in 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

278 

30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

279 
fun namify_class thy = namify thy Long_Name.base_name thyname_of_class; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

280 
fun namify_classrel thy = namify thy (fn (class1, class2) => 
33172  281 
Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) 
282 
(fn thy => thyname_of_class thy o fst); 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

283 
(*order fits nicely with composed projections*) 
28688  284 
fun namify_tyco thy "fun" = "Pure.fun" 
33172  285 
 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

286 
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

287 
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

288 
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

289 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

290 
end; (* local *) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

291 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

292 

28688  293 
(* data *) 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

294 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

295 
datatype naming = Naming of { 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

296 
class: class Symtab.table * Name.context, 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

297 
classrel: string Symreltab.table * Name.context, 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

298 
tyco: string Symtab.table * Name.context, 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

299 
instance: string Symreltab.table * Name.context, 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

300 
const: string Symtab.table * Name.context 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

301 
} 
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 
fun dest_Naming (Naming naming) = naming; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

304 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

305 
val empty_naming = Naming { 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

306 
class = (Symtab.empty, Name.context), 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

307 
classrel = (Symreltab.empty, Name.context), 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

308 
tyco = (Symtab.empty, Name.context), 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

309 
instance = (Symreltab.empty, Name.context), 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

310 
const = (Symtab.empty, Name.context) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

311 
}; 
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 
local 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

314 
fun mk_naming (class, classrel, tyco, instance, const) = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

315 
Naming { class = class, classrel = classrel, 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

316 
tyco = tyco, instance = instance, const = const }; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

317 
fun map_naming f (Naming { class, classrel, tyco, instance, const }) = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

318 
mk_naming (f (class, classrel, tyco, instance, const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

319 
in 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

320 
fun map_class f = map_naming 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

321 
(fn (class, classrel, tyco, inst, const) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

322 
(f class, classrel, tyco, inst, const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

323 
fun map_classrel f = map_naming 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

324 
(fn (class, classrel, tyco, inst, const) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

325 
(class, f classrel, tyco, inst, const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

326 
fun map_tyco f = map_naming 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

327 
(fn (class, classrel, tyco, inst, const) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

328 
(class, classrel, f tyco, inst, const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

329 
fun map_instance f = map_naming 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

330 
(fn (class, classrel, tyco, inst, const) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

331 
(class, classrel, tyco, f inst, const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

332 
fun map_const f = map_naming 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

333 
(fn (class, classrel, tyco, inst, const) => 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

334 
(class, classrel, tyco, inst, f const)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

335 
end; (*local*) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

336 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

337 
fun add_variant update (thing, name) (tab, used) = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

338 
let 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

339 
val (name', used') = yield_singleton Name.variants name used; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

340 
val tab' = update (thing, name') tab; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

341 
in (tab', used') end; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

342 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

343 
fun declare thy mapp lookup update namify thing = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

344 
mapp (add_variant update (thing, namify thy thing)) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

345 
#> `(fn naming => the (lookup naming thing)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

346 

28688  347 

348 
(* lookup and declare *) 

349 

350 
local 

351 

352 
val suffix_class = "class"; 

353 
val suffix_classrel = "classrel" 

354 
val suffix_tyco = "tyco"; 

355 
val suffix_instance = "inst"; 

356 
val suffix_const = "const"; 

357 

358 
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

359 
 add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp); 
28688  360 

361 
in 

362 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

363 
val lookup_class = add_suffix suffix_class 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

364 
oo Symtab.lookup o fst o #class o dest_Naming; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

365 
val lookup_classrel = add_suffix suffix_classrel 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

366 
oo Symreltab.lookup o fst o #classrel o dest_Naming; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

367 
val lookup_tyco = add_suffix suffix_tyco 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

368 
oo Symtab.lookup o fst o #tyco o dest_Naming; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

369 
val lookup_instance = add_suffix suffix_instance 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

370 
oo Symreltab.lookup o fst o #instance o dest_Naming; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

371 
val lookup_const = add_suffix suffix_const 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

372 
oo Symtab.lookup o fst o #const o dest_Naming; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

373 

bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

374 
fun declare_class thy = declare thy map_class 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

375 
lookup_class Symtab.update_new namify_class; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

376 
fun declare_classrel thy = declare thy map_classrel 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

377 
lookup_classrel Symreltab.update_new namify_classrel; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

378 
fun declare_tyco thy = declare thy map_tyco 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

379 
lookup_tyco Symtab.update_new namify_tyco; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

380 
fun declare_instance thy = declare thy map_instance 
30648
17365ef082f3
clarified relationship of modules Code_Name and Code_Printer
haftmann
parents:
30364
diff
changeset

381 
lookup_instance Symreltab.update_new namify_instance; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

382 
fun declare_const thy = declare thy map_const 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

383 
lookup_const Symtab.update_new namify_const; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

384 

31054  385 
fun ensure_declared_const thy const naming = 
386 
case lookup_const naming const 

387 
of SOME const' => (const', naming) 

388 
 NONE => declare_const thy const naming; 

389 

28688  390 
val unfold_fun = unfoldr 
391 
(fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2) 

392 
 _ => NONE); (*depends on suffix_tyco and namify_tyco!*) 

393 

394 
end; (* local *) 

395 

24219  396 

32353
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

397 
(** technical transformations of code equations **) 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

398 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

399 
fun expand_eta thy k thm = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

400 
let 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

401 
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

402 
val (head, args) = strip_comb lhs; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

403 
val l = if k = ~1 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

404 
then (length o fst o strip_abs) rhs 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

405 
else Int.max (0, k  length args); 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

406 
val (raw_vars, _) = Term.strip_abs_eta l rhs; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

407 
val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs []))) 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

408 
raw_vars; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

409 
fun expand (v, ty) thm = Drule.fun_cong_rule thm 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

410 
(Thm.cterm_of thy (Var ((v, 0), ty))); 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

411 
in 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

412 
thm 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

413 
> fold expand vars 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

414 
> Conv.fconv_rule Drule.beta_eta_conversion 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

415 
end; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

416 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

417 
fun same_arity thy thms = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

418 
let 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

419 
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; 
33029  420 
val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0; 
32353
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

421 
in map (expand_eta thy k) thms end; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

422 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

423 
fun mk_desymbolization pre post mk vs = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

424 
let 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

425 
val names = map (pre o fst o fst) vs 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

426 
> map (Name.desymbolize false) 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

427 
> Name.variant_list [] 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

428 
> map post; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

429 
in map_filter (fn (((v, i), x), v') => 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

430 
if v = v' andalso i = 0 then NONE 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

431 
else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names) 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

432 
end; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

433 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

434 
fun desymbolize_tvars thy thms = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

435 
let 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

436 
val tvs = fold (Term.add_tvars o Thm.prop_of) thms []; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

437 
val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

438 
in map (Thm.certify_instantiate (tvar_subst, [])) thms end; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

439 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

440 
fun desymbolize_vars thy thm = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

441 
let 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

442 
val vs = Term.add_vars (Thm.prop_of thm) []; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

443 
val var_subst = mk_desymbolization I I Var vs; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

444 
in Thm.certify_instantiate ([], var_subst) thm end; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

445 

32928
6bcc35f7ff6d
more explicit notion of canonized code equations
haftmann
parents:
32917
diff
changeset

446 
fun canonize_thms thy = map (Thm.transfer thy) 
32929  447 
#> Code.standard_typscheme thy #> desymbolize_tvars thy 
32928
6bcc35f7ff6d
more explicit notion of canonized code equations
haftmann
parents:
32917
diff
changeset

448 
#> same_arity thy #> map (desymbolize_vars thy); 
32353
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

449 

0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

450 

27103  451 
(** statements, abstract programs **) 
24219  452 

453 
type typscheme = (vname * sort) list * itype; 

24918  454 
datatype stmt = 
27024  455 
NoStmt 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

456 
 Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

457 
 Datatype of string * ((vname * sort) list * (string * itype list) list) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

458 
 Datatypecons of string * string 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

459 
 Class of class * (vname * ((class * string) list * (string * itype) list)) 
24219  460 
 Classrel of class * class 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

461 
 Classparam of string * class 
24219  462 
 Classinst of (class * (string * (vname * sort) list)) 
463 
* ((class * (string * (string * dict list list))) list 

28350  464 
* ((string * const) * (thm * bool)) list); 
24219  465 

27103  466 
type program = stmt Graph.T; 
24219  467 

27103  468 
fun empty_funs program = 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

469 
Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c 
27103  470 
 _ => I) program []; 
24219  471 

27711  472 
fun map_terms_bottom_up f (t as IConst _) = f t 
473 
 map_terms_bottom_up f (t as IVar _) = f t 

474 
 map_terms_bottom_up f (t1 `$ t2) = f 

475 
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) 

31724  476 
 map_terms_bottom_up f ((v, ty) `=> t) = f 
477 
((v, ty) `=> map_terms_bottom_up f t) 

27711  478 
 map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f 
479 
(ICase (((map_terms_bottom_up f t, ty), (map o pairself) 

480 
(map_terms_bottom_up f) ps), map_terms_bottom_up f t0)); 

481 

482 
fun map_terms_stmt f NoStmt = NoStmt 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

483 
 map_terms_stmt f (Fun (c, (tysm, eqs))) = Fun (c, (tysm, (map o apfst) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

484 
(fn (ts, t) => (map f ts, f t)) eqs)) 
27711  485 
 map_terms_stmt f (stmt as Datatype _) = stmt 
486 
 map_terms_stmt f (stmt as Datatypecons _) = stmt 

487 
 map_terms_stmt f (stmt as Class _) = stmt 

488 
 map_terms_stmt f (stmt as Classrel _) = stmt 

489 
 map_terms_stmt f (stmt as Classparam _) = stmt 

490 
 map_terms_stmt f (Classinst (arity, (superarities, classparms))) = 

491 
Classinst (arity, (superarities, (map o apfst o apsnd) (fn const => 

492 
case f (IConst const) of IConst const' => const') classparms)); 

493 

27103  494 
fun is_cons program name = case Graph.get_node program name 
24219  495 
of Datatypecons _ => true 
496 
 _ => false; 

497 

27103  498 
fun contr_classparam_typs program name = case Graph.get_node program name 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

499 
of Classparam (_, class) => let 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

500 
val Class (_, (_, (_, params))) = Graph.get_node program class; 
25621  501 
val SOME ty = AList.lookup (op =) params name; 
502 
val (tys, res_ty) = unfold_fun ty; 

503 
fun no_tyvar (_ `%% tys) = forall no_tyvar tys 

504 
 no_tyvar (ITyVar _) = false; 

505 
in if no_tyvar res_ty 

506 
then map (fn ty => if no_tyvar ty then NONE else SOME ty) tys 

507 
else [] 

508 
end 

509 
 _ => []; 

510 

32895  511 
fun labelled_name thy program name = case Graph.get_node program name 
512 
of Fun (c, _) => quote (Code.string_of_const thy c) 

513 
 Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) 

514 
 Datatypecons (c, _) => quote (Code.string_of_const thy c) 

515 
 Class (class, _) => "class " ^ quote (Sign.extern_class thy class) 

516 
 Classrel (sub, super) => let 

517 
val Class (sub, _) = Graph.get_node program sub 

518 
val Class (super, _) = Graph.get_node program super 

519 
in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end 

520 
 Classparam (c, _) => quote (Code.string_of_const thy c) 

521 
 Classinst ((class, (tyco, _)), _) => let 

522 
val Class (class, _) = Graph.get_node program class 

523 
val Datatype (tyco, _) = Graph.get_node program tyco 

524 
in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end 

525 

526 
fun group_stmts thy program = 

527 
let 

528 
fun is_fun (_, Fun _) = true  is_fun _ = false; 

529 
fun is_datatypecons (_, Datatypecons _) = true  is_datatypecons _ = false; 

530 
fun is_datatype (_, Datatype _) = true  is_datatype _ = false; 

531 
fun is_class (_, Class _) = true  is_class _ = false; 

532 
fun is_classrel (_, Classrel _) = true  is_classrel _ = false; 

533 
fun is_classparam (_, Classparam _) = true  is_classparam _ = false; 

534 
fun is_classinst (_, Classinst _) = true  is_classinst _ = false; 

535 
fun group stmts = 

536 
if forall (is_datatypecons orf is_datatype) stmts 

537 
then (filter is_datatype stmts, [], ([], [])) 

538 
else if forall (is_class orf is_classrel orf is_classparam) stmts 

539 
then ([], filter is_class stmts, ([], [])) 

540 
else if forall (is_fun orf is_classinst) stmts 

541 
then ([], [], List.partition is_fun stmts) 

542 
else error ("Illegal mutual dependencies: " ^ 

543 
(commas o map (labelled_name thy program o fst)) stmts) 

544 
in 

545 
rev (Graph.strong_conn program) 

546 
> map (AList.make (Graph.get_node program)) 

547 
> map group 

548 
end; 

549 

24219  550 

27103  551 
(** translation kernel **) 
24219  552 

28724  553 
(* generic mechanisms *) 
554 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

555 
fun ensure_stmt lookup declare generate thing (dep, (naming, program)) = 
24219  556 
let 
28706  557 
fun add_dep name = case dep of NONE => I 
558 
 SOME dep => Graph.add_edge (dep, name); 

559 
val (name, naming') = case lookup naming thing 

560 
of SOME name => (name, naming) 

561 
 NONE => declare thing naming; 

562 
in case try (Graph.get_node program) name 

563 
of SOME stmt => program 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

564 
> add_dep name 
28706  565 
> pair naming' 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

566 
> pair dep 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

567 
> pair name 
28706  568 
 NONE => program 
569 
> Graph.default_node (name, NoStmt) 

570 
> add_dep name 

571 
> pair naming' 

572 
> curry generate (SOME name) 

573 
> snd 

574 
> (fn stmt => (apsnd o Graph.map_node name) (K stmt)) 

575 
> pair dep 

576 
> pair name 

24219  577 
end; 
578 

26972  579 
fun not_wellsorted thy thm ty sort e = 
580 
let 

581 
val err_class = Sorts.class_error (Syntax.pp_global thy) e; 

582 
val err_thm = case thm 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31962
diff
changeset

583 
of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")"  NONE => ""; 
26972  584 
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort " 
585 
^ Syntax.string_of_sort_global thy sort; 

586 
in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end; 

587 

28724  588 

589 
(* translation *) 

590 

32873  591 
fun ensure_tyco thy algbr eqngr tyco = 
30932  592 
let 
593 
val stmt_datatype = 

594 
let 

595 
val (vs, cos) = Code.get_datatype thy tyco; 

596 
in 

32873  597 
fold_map (translate_tyvar_sort thy algbr eqngr) vs 
30932  598 
##>> fold_map (fn (c, tys) => 
32873  599 
ensure_const thy algbr eqngr c 
600 
##>> fold_map (translate_typ thy algbr eqngr) tys) cos 

30932  601 
#>> (fn info => Datatype (tyco, info)) 
602 
end; 

603 
in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end 

32873  604 
and ensure_const thy algbr eqngr c = 
30932  605 
let 
606 
fun stmt_datatypecons tyco = 

32873  607 
ensure_tyco thy algbr eqngr tyco 
30932  608 
#>> (fn tyco => Datatypecons (c, tyco)); 
609 
fun stmt_classparam class = 

32873  610 
ensure_class thy algbr eqngr class 
30932  611 
#>> (fn class => Classparam (c, class)); 
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset

612 
fun stmt_fun raw_eqns = 
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset

613 
let 
32928
6bcc35f7ff6d
more explicit notion of canonized code equations
haftmann
parents:
32917
diff
changeset

614 
val eqns = burrow_fst (canonize_thms thy) raw_eqns; 
32873  615 
val (vs, ty) = Code.typscheme_eqns thy c (map fst eqns); 
32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset

616 
in 
32873  617 
fold_map (translate_tyvar_sort thy algbr eqngr) vs 
618 
##>> translate_typ thy algbr eqngr ty 

619 
##>> fold_map (translate_eqn thy algbr eqngr) eqns 

32872
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset

620 
#>> (fn info => Fun (c, info)) 
019201eb7e07
variables in type schemes must be renamed simultaneously with variables in equations
haftmann
parents:
32795
diff
changeset

621 
end; 
30932  622 
val stmt_const = case Code.get_datatype_of_constr thy c 
623 
of SOME tyco => stmt_datatypecons tyco 

624 
 NONE => (case AxClass.class_of_param thy c 

625 
of SOME class => stmt_classparam class 

32873  626 
 NONE => stmt_fun (Code_Preproc.eqns eqngr c)) 
30932  627 
in ensure_stmt lookup_const (declare_const thy) stmt_const c end 
32873  628 
and ensure_class thy (algbr as (_, algebra)) eqngr class = 
24918  629 
let 
28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

630 
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; 
24969  631 
val cs = #params (AxClass.get_info thy class); 
24918  632 
val stmt_class = 
32873  633 
fold_map (fn superclass => ensure_class thy algbr eqngr superclass 
634 
##>> ensure_classrel thy algbr eqngr (class, superclass)) superclasses 

635 
##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr c 

636 
##>> translate_typ thy algbr eqngr ty) cs 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

637 
#>> (fn info => Class (class, (unprefix "'" Name.aT, info))) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

638 
in ensure_stmt lookup_class (declare_class thy) stmt_class class end 
32873  639 
and ensure_classrel thy algbr eqngr (subclass, superclass) = 
24918  640 
let 
641 
val stmt_classrel = 

32873  642 
ensure_class thy algbr eqngr subclass 
643 
##>> ensure_class thy algbr eqngr superclass 

24918  644 
#>> Classrel; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

645 
in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end 
32873  646 
and ensure_inst thy (algbr as (_, algebra)) eqngr (class, tyco) = 
24918  647 
let 
28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

648 
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; 
24969  649 
val classparams = these (try (#params o AxClass.get_info thy) class); 
24918  650 
val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]); 
651 
val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class]; 

652 
val vs' = map2 (fn (v, sort1) => fn sort2 => (v, 

653 
Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts'; 

654 
val arity_typ = Type (tyco, map TFree vs); 

655 
val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs'); 

28688  656 
fun translate_superarity superclass = 
32873  657 
ensure_class thy algbr eqngr superclass 
658 
##>> ensure_classrel thy algbr eqngr (class, superclass) 

659 
##>> translate_dicts thy algbr eqngr NONE (arity_typ, [superclass]) 

24918  660 
#>> (fn ((superclass, classrel), [DictConst (inst, dss)]) => 
661 
(superclass, (classrel, (inst, dss)))); 

28688  662 
fun translate_classparam_inst (c, ty) = 
24918  663 
let 
664 
val c_inst = Const (c, map_type_tfree (K arity_typ') ty); 

25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25485
diff
changeset

665 
val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst); 
24918  666 
val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd 
667 
o Logic.dest_equals o Thm.prop_of) thm; 

668 
in 

32873  669 
ensure_const thy algbr eqngr c 
670 
##>> translate_const thy algbr eqngr (SOME thm) c_ty 

28350  671 
#>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true))) 
24918  672 
end; 
673 
val stmt_inst = 

32873  674 
ensure_class thy algbr eqngr class 
675 
##>> ensure_tyco thy algbr eqngr tyco 

676 
##>> fold_map (translate_tyvar_sort thy algbr eqngr) vs 

28688  677 
##>> fold_map translate_superarity superclasses 
678 
##>> fold_map translate_classparam_inst classparams 

24918  679 
#>> (fn ((((class, tyco), arity), superarities), classparams) => 
680 
Classinst ((class, (tyco, arity)), (superarities, classparams))); 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

681 
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end 
32873  682 
and translate_typ thy algbr eqngr (TFree (v, _)) = 
30932  683 
pair (ITyVar (unprefix "'" v)) 
32873  684 
 translate_typ thy algbr eqngr (Type (tyco, tys)) = 
685 
ensure_tyco thy algbr eqngr tyco 

686 
##>> fold_map (translate_typ thy algbr eqngr) tys 

30932  687 
#>> (fn (tyco, tys) => tyco `%% tys) 
32873  688 
and translate_term thy algbr eqngr thm (Const (c, ty)) = 
689 
translate_app thy algbr eqngr thm ((c, ty), []) 

690 
 translate_term thy algbr eqngr thm (Free (v, _)) = 

31889  691 
pair (IVar (SOME v)) 
32873  692 
 translate_term thy algbr eqngr thm (Abs (v, ty, t)) = 
24918  693 
let 
32273  694 
val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t); 
695 
val v'' = if member (op =) (Term.add_free_names t' []) v' 

696 
then SOME v' else NONE 

24918  697 
in 
32873  698 
translate_typ thy algbr eqngr ty 
699 
##>> translate_term thy algbr eqngr thm t' 

32273  700 
#>> (fn (ty, t) => (v'', ty) `=> t) 
24918  701 
end 
32873  702 
 translate_term thy algbr eqngr thm (t as _ $ _) = 
24918  703 
case strip_comb t 
704 
of (Const (c, ty), ts) => 

32873  705 
translate_app thy algbr eqngr thm ((c, ty), ts) 
24918  706 
 (t', ts) => 
32873  707 
translate_term thy algbr eqngr thm t' 
708 
##>> fold_map (translate_term thy algbr eqngr thm) ts 

24918  709 
#>> (fn (t, ts) => t `$$ ts) 
32873  710 
and translate_eqn thy algbr eqngr (thm, proper) = 
30932  711 
let 
712 
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals 

713 
o Logic.unvarify o prop_of) thm; 

714 
in 

32873  715 
fold_map (translate_term thy algbr eqngr (SOME thm)) args 
716 
##>> translate_term thy algbr eqngr (SOME thm) rhs 

31088  717 
#>> rpair (thm, proper) 
30932  718 
end 
32873  719 
and translate_const thy algbr eqngr thm (c, ty) = 
26972  720 
let 
721 
val tys = Sign.const_typargs thy (c, ty); 

32873  722 
val sorts = Code_Preproc.sortargs eqngr c; 
26972  723 
val tys_args = (fst o Term.strip_type) ty; 
724 
in 

32873  725 
ensure_const thy algbr eqngr c 
726 
##>> fold_map (translate_typ thy algbr eqngr) tys 

727 
##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts) 

728 
##>> fold_map (translate_typ thy algbr eqngr) tys_args 

31049  729 
#>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args))) 
26972  730 
end 
32873  731 
and translate_app_const thy algbr eqngr thm (c_ty, ts) = 
732 
translate_const thy algbr eqngr thm c_ty 

733 
##>> fold_map (translate_term thy algbr eqngr thm) ts 

24918  734 
#>> (fn (t, ts) => t `$$ ts) 
32873  735 
and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) = 
24918  736 
let 
31892  737 
fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty; 
738 
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

739 
val ty = nth tys t_pos; 
31957  740 
fun mk_constr c t = let val n = Code.args_number thy c 
741 
in ((c, arg_types n (fastype_of t) > ty), n) end; 

31892  742 
val constrs = if null case_pats then [] 
743 
else map2 mk_constr case_pats (nth_drop t_pos ts); 

744 
fun casify naming constrs ty ts = 

24918  745 
let 
31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

746 
val undefineds = map_filter (lookup_const naming) (Code.undefineds thy); 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

747 
fun collapse_clause vs_map ts body = 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

748 
let 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

749 
in case body 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

750 
of IConst (c, _) => if member (op =) undefineds c 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

751 
then [] 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

752 
else [(ts, body)] 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

753 
 ICase (((IVar (SOME v), _), subclauses), _) => 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

754 
if forall (fn (pat', body') => exists_var pat' v 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

755 
orelse not (exists_var body' v)) subclauses 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

756 
then case AList.lookup (op =) vs_map v 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

757 
of SOME i => maps (fn (pat', body') => 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

758 
collapse_clause (AList.delete (op =) v vs_map) 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

759 
(nth_map i (K pat') ts) body') subclauses 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

760 
 NONE => [(ts, body)] 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

761 
else [(ts, body)] 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

762 
 _ => [(ts, body)] 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

763 
end; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

764 
fun mk_clause mk tys t = 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

765 
let 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

766 
val (vs, body) = unfold_abs_eta tys t; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

767 
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

768 
val ts = map (IVar o fst) vs; 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

769 
in map mk (collapse_clause vs_map ts body) end; 
31892  770 
val t = nth ts t_pos; 
771 
val ts_clause = nth_drop t_pos ts; 

31935
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

772 
val clauses = if null case_pats 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

773 
then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause) 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

774 
else maps (fn ((constr as IConst (_, (_, tys)), n), t) => 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

775 
mk_clause (fn (ts, body) => (constr `$$ ts, body)) (curry Library.take n tys) t) 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

776 
(constrs ~~ ts_clause); 
31892  777 
in ((t, ty), clauses) end; 
24918  778 
in 
32873  779 
translate_const thy algbr eqngr thm c_ty 
780 
##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs 

781 
##>> translate_typ thy algbr eqngr ty 

782 
##>> fold_map (translate_term thy algbr eqngr thm) ts 

31892  783 
#> (fn (((t, constrs), ty), ts) => 
784 
`(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts))) 

24918  785 
end 
32873  786 
and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) = 
29973  787 
if length ts < num_args then 
788 
let 

789 
val k = length ts; 

790 
val tys = (curry Library.take (num_args  k) o curry Library.drop k o fst o strip_type) ty; 

791 
val ctxt = (fold o fold_aterms) Term.declare_term_frees ts Name.context; 

792 
val vs = Name.names ctxt "a" tys; 

793 
in 

32873  794 
fold_map (translate_typ thy algbr eqngr) tys 
795 
##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs) 

31888  796 
#>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `==> t) 
29973  797 
end 
798 
else if length ts > num_args then 

32873  799 
translate_case thy algbr eqngr thm case_scheme ((c, ty), Library.take (num_args, ts)) 
800 
##>> fold_map (translate_term thy algbr eqngr thm) (Library.drop (num_args, ts)) 

29973  801 
#>> (fn (t, ts) => t `$$ ts) 
802 
else 

32873  803 
translate_case thy algbr eqngr thm case_scheme ((c, ty), ts) 
804 
and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) = 

29973  805 
case Code.get_case_scheme thy c 
32873  806 
of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts 
807 
 NONE => translate_app_const thy algbr eqngr thm c_ty_ts 

808 
and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) = 

809 
fold_map (ensure_class thy algbr eqngr) (proj_sort sort) 

30932  810 
#>> (fn sort => (unprefix "'" v, sort)) 
32873  811 
and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) = 
30932  812 
let 
813 
datatype typarg = 

814 
Global of (class * string) * typarg list list 

815 
 Local of (class * class) list * (string * (int * sort)); 

816 
fun class_relation (Global ((_, tyco), yss), _) class = 

817 
Global ((class, tyco), yss) 

818 
 class_relation (Local (classrels, v), subclass) superclass = 

819 
Local ((subclass, superclass) :: classrels, v); 

820 
fun type_constructor tyco yss class = 

821 
Global ((class, tyco), (map o map) fst yss); 

822 
fun type_variable (TFree (v, sort)) = 

823 
let 

824 
val sort' = proj_sort sort; 

825 
in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end; 

32795  826 
val typargs = Sorts.of_sort_derivation algebra 
30932  827 
{class_relation = class_relation, type_constructor = type_constructor, 
828 
type_variable = type_variable} (ty, proj_sort sort) 

829 
handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e; 

830 
fun mk_dict (Global (inst, yss)) = 

32873  831 
ensure_inst thy algbr eqngr inst 
30932  832 
##>> (fold_map o fold_map) mk_dict yss 
833 
#>> (fn (inst, dss) => DictConst (inst, dss)) 

31962  834 
 mk_dict (Local (classrels, (v, (n, sort)))) = 
32873  835 
fold_map (ensure_classrel thy algbr eqngr) classrels 
31962  836 
#>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort)))) 
30932  837 
in fold_map mk_dict typargs end; 
24918  838 

25969  839 

27103  840 
(* store *) 
841 

31962  842 
structure Program = Code_Data_Fun 
27103  843 
( 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

844 
type T = naming * program; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

845 
val empty = (empty_naming, Graph.empty); 
28706  846 
fun purge thy cs (naming, program) = 
27609  847 
let 
28706  848 
val names_delete = cs 
849 
> map_filter (lookup_const naming) 

850 
> filter (can (Graph.get_node program)) 

851 
> Graph.all_preds program; 

852 
val program' = Graph.del_nodes names_delete program; 

853 
in (naming, program') end; 

27103  854 
); 
855 

856 
val cached_program = Program.get; 

25969  857 

32873  858 
fun invoke_generation thy (algebra, eqngr) f name = 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

859 
Program.change_yield thy (fn naming_program => (NONE, naming_program) 
32873  860 
> f thy algebra eqngr name 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

861 
> (fn name => fn (_, naming_program) => (name, naming_program))); 
27103  862 

863 

864 
(* program generation *) 

865 

866 
fun consts_program thy cs = 

867 
let 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

868 
fun project_consts cs (naming, program) = 
27103  869 
let 
870 
val cs_all = Graph.all_succs program cs; 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

871 
in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; 
32873  872 
fun generate_consts thy algebra eqngr = 
873 
fold_map (ensure_const thy algebra eqngr); 

27103  874 
in 
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31088
diff
changeset

875 
invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs 
27103  876 
> project_consts 
877 
end; 

878 

879 

880 
(* value evaluation *) 

25969  881 

32873  882 
fun ensure_value thy algbr eqngr t = 
24918  883 
let 
884 
val ty = fastype_of t; 

885 
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =) 

886 
o dest_TFree))) t []; 

887 
val stmt_value = 

32873  888 
fold_map (translate_tyvar_sort thy algbr eqngr) vs 
889 
##>> translate_typ thy algbr eqngr ty 

890 
##>> translate_term thy algbr eqngr NONE t 

28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

891 
#>> (fn ((vs, ty), t) => Fun 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

892 
(Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))]))); 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

893 
fun term_value (dep, (naming, program1)) = 
25969  894 
let 
30947  895 
val Fun (_, (vs_ty, [(([], t), _)])) = 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

896 
Graph.get_node program1 Term.dummy_patternN; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

897 
val deps = Graph.imm_succs program1 Term.dummy_patternN; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

898 
val program2 = Graph.del_nodes [Term.dummy_patternN] program1; 
27103  899 
val deps_all = Graph.all_succs program2 deps; 
900 
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

901 
in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end; 
26011  902 
in 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

903 
ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN 
26011  904 
#> snd 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

905 
#> term_value 
26011  906 
end; 
24219  907 

32873  908 
fun base_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

909 
let 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

910 
val (((naming, program), (((vs', ty'), t'), deps)), _) = 
32873  911 
invoke_generation thy (algebra, eqngr) ensure_value t; 
30947  912 
val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs'; 
31063
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

913 
in evaluator naming program ((vs'', (vs', ty')), t') deps end; 
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

914 

32123
8bac9ee4b28d
integrated add_triv_classes into evaluation stack
haftmann
parents:
31962
diff
changeset

915 
fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy; 
8bac9ee4b28d
integrated add_triv_classes into evaluation stack
haftmann
parents:
31962
diff
changeset

916 
fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy; 
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

917 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

918 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

919 
(** diagnostic commands **) 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

920 

31036  921 
fun read_const_exprs thy = 
922 
let 

923 
fun consts_of some_thyname = 

924 
let 

925 
val thy' = case some_thyname 

926 
of SOME thyname => ThyInfo.the_theory thyname thy 

927 
 NONE => thy; 

928 
val cs = Symtab.fold (fn (c, (_, NONE)) => cons c  _ => I) 

929 
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') []; 

930 
fun belongs_here c = 

931 
not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy')) 

932 
in case some_thyname 

933 
of NONE => cs 

934 
 SOME thyname => filter belongs_here cs 

935 
end; 

936 
fun read_const_expr "*" = ([], consts_of NONE) 

937 
 read_const_expr s = if String.isSuffix ".*" s 

938 
then ([], consts_of (SOME (unsuffix ".*" s))) 

31156  939 
else ([Code.read_const thy s], []); 
31036  940 
in pairself flat o split_list o map read_const_expr end; 
941 

30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

942 
fun code_depgr thy consts = 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

943 
let 
31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31088
diff
changeset

944 
val (_, eqngr) = Code_Preproc.obtain thy consts []; 
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

945 
val select = Graph.all_succs eqngr consts; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

946 
in 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

947 
eqngr 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

948 
> not (null consts) ? Graph.subgraph (member (op =) select) 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

949 
> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy)) 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

950 
end; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

951 

31125
80218ee73167
transferred code generator preprocessor into separate module
haftmann
parents:
31088
diff
changeset

952 
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

953 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

954 
fun code_deps thy consts = 
27103  955 
let 
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

956 
val eqngr = code_depgr thy consts; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

957 
val constss = Graph.strong_conn eqngr; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

958 
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

959 
Symtab.update (const, consts)) consts) constss; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

960 
fun succs consts = consts 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

961 
> maps (Graph.imm_succs eqngr) 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

962 
> subtract (op =) consts 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

963 
> map (the o Symtab.lookup mapping) 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

964 
> distinct (op =); 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

965 
val conn = [] > fold (fn consts => cons (consts, succs consts)) constss; 
31156  966 
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

967 
> commas; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

968 
val prgr = map (fn (consts, constss) => 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

969 
{ 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

970 
path = "", parents = map namify constss }) conn; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

971 
in Present.display_graph prgr end; 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

972 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

973 
local 
27103  974 

30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

975 
structure P = OuterParse 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

976 
and K = OuterKeyword 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

977 

31036  978 
fun code_thms_cmd thy = code_thms thy o op @ o read_const_exprs thy; 
979 
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

980 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

981 
in 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

982 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

983 
val _ = 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

984 
OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

985 
(Scan.repeat P.term_group 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

986 
>> (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

987 
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

988 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

989 
val _ = 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

990 
OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

991 
(Scan.repeat P.term_group 
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

992 
>> (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

993 
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

994 

1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

995 
end; 
27103  996 

24219  997 
end; (*struct*) 
998 

999 

28054  1000 
structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol; 