author  wenzelm 
Fri, 02 Oct 2009 22:15:08 +0200  
changeset 32861  105f40051387 
parent 32795  a0f38d8d633a 
child 32872  019201eb7e07 
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 
49 
val eta_expand: int > const * iterm list > iterm 

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

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

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

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

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

54 

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

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

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

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

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

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

61 
val lookup_const: naming > string > string option 
31054  62 
val ensure_declared_const: theory > string > naming > string * naming 
24219  63 

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

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

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

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

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

71 
 Classparam of string * class 
24219  72 
 Classinst of (class * (string * (vname * sort) list)) 
73 
* ((class * (string * (string * dict list list))) list 

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

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

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

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

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

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

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

80 
val contr_classparam_typs: program > string > itype option list 
24219  81 

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

82 
val expand_eta: theory > int > thm > thm 
98c00ee9e786
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents:
32353
diff
changeset

83 
val clean_thms: theory > thm list > thm list 
31036  84 
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

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

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

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

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

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

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

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

92 
> term > 'a 
24219  93 
end; 
94 

28054  95 
structure Code_Thingol: CODE_THINGOL = 
24219  96 
struct 
97 

98 
(** auxiliary **) 

99 

100 
fun unfoldl dest x = 

101 
case dest x 

102 
of NONE => (x, []) 

103 
 SOME (x1, x2) => 

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

105 

106 
fun unfoldr dest x = 

107 
case dest x 

108 
of NONE => ([], x) 

109 
 SOME (x1, x2) => 

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

111 

112 

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

113 
(** language core  types, terms **) 
24219  114 

115 
type vname = string; 

116 

117 
datatype dict = 

118 
DictConst of string * dict list list 

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

120 

121 
datatype itype = 

122 
`%% of string * itype list 

123 
 ITyVar of vname; 

124 

31049  125 
type const = string * ((itype list * dict list list) * itype list (*types of arguments*)) 
24591  126 

24219  127 
datatype iterm = 
24591  128 
IConst of const 
31889  129 
 IVar of vname option 
24219  130 
 `$ of iterm * iterm 
31888  131 
 `=> of (vname option * itype) * iterm 
24219  132 
 ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; 
133 
(*see also signature*) 

134 

135 
val op `$$ = Library.foldl (op `$); 

31724  136 
val op `==> = Library.foldr (op `=>); 
24219  137 

138 
val unfold_app = unfoldl 

139 
(fn op `$ t => SOME t 

140 
 _ => NONE); 

141 

31874  142 
val unfold_abs = unfoldr 
143 
(fn op `=> t => SOME t 

24219  144 
 _ => NONE); 
145 

146 
val split_let = 

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

148 
 _ => NONE); 

149 

150 
val unfold_let = unfoldr split_let; 

151 

152 
fun unfold_const_app t = 

153 
case unfold_app t 

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

155 
 _ => NONE; 

156 

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

157 
fun add_constnames (IConst (c, _)) = insert (op =) c 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

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

159 
 add_constnames (t1 `$ t2) = add_constnames t1 #> add_constnames t2 
3896169e6ff9
cleaned up fundamental iml term functions; nested patterns
haftmann
parents:
31892
diff
changeset

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

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

162 
#> fold (fn (pat, body) => add_constnames pat #> add_constnames body) ds; 
24219  163 

164 
fun fold_varnames f = 

165 
let 

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

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

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

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

169 
 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

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

171 
 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

172 
 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

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

174 
 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

175 
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

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

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

178 
in fold_aux add f end; 
24219  179 

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

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

31889  182 
fun split_pat_abs ((NONE, ty) `=> t) = SOME ((IVar NONE, ty), t) 
31888  183 
 split_pat_abs ((SOME v, ty) `=> t) = SOME (case t 
31889  184 
of ICase (((IVar (SOME w), _), [(p, t')]), _) => 
31888  185 
if v = w andalso (exists_var p v orelse not (exists_var t' v)) 
31889  186 
then ((p, ty), t') 
187 
else ((IVar (SOME v), ty), t) 

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

31888  189 
 split_pat_abs _ = NONE; 
31874  190 

191 
val unfold_pat_abs = unfoldr split_pat_abs; 

24219  192 

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

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

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

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

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

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

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

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

201 
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

202 
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

203 

27711  204 
fun eta_expand k (c as (_, (_, tys)), ts) = 
24219  205 
let 
206 
val j = length ts; 

207 
val l = k  j; 

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

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

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

24219  212 

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

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

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

215 
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

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

217 
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

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

219 
 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

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

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

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

223 

25621  224 
fun locally_monomorphic (IConst _) = false 
225 
 locally_monomorphic (IVar _) = true 

226 
 locally_monomorphic (t `$ _) = locally_monomorphic t 

31724  227 
 locally_monomorphic (_ `=> t) = locally_monomorphic t 
25621  228 
 locally_monomorphic (ICase ((_, ds), _)) = exists (locally_monomorphic o snd) ds; 
229 

230 

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

232 

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

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

234 

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

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

236 
fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

237 
fun thyname_of_class thy = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

238 
thyname_of thy (ProofContext.query_class (ProofContext.init thy)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

239 
fun thyname_of_tyco thy = 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

240 
thyname_of thy (Type.the_tags (Sign.tsig_of thy)); 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

241 
fun thyname_of_instance thy inst = case AxClass.arity_property thy inst Markup.theory_nameN 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

242 
of [] => error ("no such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

243 
 thyname :: _ => thyname; 
28706  244 
fun thyname_of_const thy c = case AxClass.class_of_param thy c 
245 
of SOME class => thyname_of_class thy class 

246 
 NONE => (case Code.get_datatype_of_constr thy c 

247 
of SOME dtco => thyname_of_tyco thy dtco 

248 
 NONE => thyname_of thy (Consts.the_tags (Sign.consts_of thy)) c); 

31036  249 
fun purify_base "op &" = "and" 
250 
 purify_base "op " = "or" 

251 
 purify_base "op >" = "implies" 

252 
 purify_base "op :" = "member" 

253 
 purify_base "op =" = "eq" 

254 
 purify_base "*" = "product" 

255 
 purify_base "+" = "sum" 

256 
 purify_base s = Name.desymbolize false s; 

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

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

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

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

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

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

263 

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

264 
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

265 
fun namify_classrel thy = namify thy (fn (class1, class2) => 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

266 
Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst); 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

267 
(*order fits nicely with composed projections*) 
28688  268 
fun namify_tyco thy "fun" = "Pure.fun" 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

269 
 namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco; 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

270 
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

271 
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

272 
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

273 

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

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

275 

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

276 

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

278 

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

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

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

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

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

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

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

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

286 

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

287 
fun dest_Naming (Naming naming) = naming; 
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

288 

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

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

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

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

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

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

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

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

296 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

320 

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

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

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

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

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

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

326 

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

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

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

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

330 

28688  331 

332 
(* lookup and declare *) 

333 

334 
local 

335 

336 
val suffix_class = "class"; 

337 
val suffix_classrel = "classrel" 

338 
val suffix_tyco = "tyco"; 

339 
val suffix_instance = "inst"; 

340 
val suffix_const = "const"; 

341 

342 
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

343 
 add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp); 
28688  344 

345 
in 

346 

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

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

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

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

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

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

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

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

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

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

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

357 

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

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

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

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

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

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

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

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

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

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

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

368 

31054  369 
fun ensure_declared_const thy const naming = 
370 
case lookup_const naming const 

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

372 
 NONE => declare_const thy const naming; 

373 

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

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

377 

378 
end; (* local *) 

379 

24219  380 

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

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

382 

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

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

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

385 
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

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

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

388 
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

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

390 
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

391 
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

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

393 
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

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

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

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

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

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

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

400 

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

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

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

403 
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

404 
val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0; 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

405 
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

406 

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

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

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

409 
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

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

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

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

413 
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

414 
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

415 
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

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

417 

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

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

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

420 
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

421 
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

422 
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

423 

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

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

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

426 
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

427 
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

428 
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

429 

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

430 
fun desymbolize_all_vars thy = desymbolize_tvars thy #> map (desymbolize_vars thy); 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

431 

32545
8631b421ffc3
explicit transfer avoids spurious merge problems
haftmann
parents:
32358
diff
changeset

432 
fun clean_thms thy = map (Thm.transfer thy) #> same_arity thy #> desymbolize_all_vars thy; 
32353
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 

27103  435 
(** statements, abstract programs **) 
24219  436 

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

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

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

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

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

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

445 
 Classparam of string * class 
24219  446 
 Classinst of (class * (string * (vname * sort) list)) 
447 
* ((class * (string * (string * dict list list))) list 

28350  448 
* ((string * const) * (thm * bool)) list); 
24219  449 

27103  450 
type program = stmt Graph.T; 
24219  451 

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

453 
Graph.fold (fn (name, (Fun (c, (_, [])), _)) => cons c 
27103  454 
 _ => I) program []; 
24219  455 

27711  456 
fun map_terms_bottom_up f (t as IConst _) = f t 
457 
 map_terms_bottom_up f (t as IVar _) = f t 

458 
 map_terms_bottom_up f (t1 `$ t2) = f 

459 
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2) 

31724  460 
 map_terms_bottom_up f ((v, ty) `=> t) = f 
461 
((v, ty) `=> map_terms_bottom_up f t) 

27711  462 
 map_terms_bottom_up f (ICase (((t, ty), ps), t0)) = f 
463 
(ICase (((map_terms_bottom_up f t, ty), (map o pairself) 

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

465 

466 
fun map_terms_stmt f NoStmt = NoStmt 

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

467 
 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

468 
(fn (ts, t) => (map f ts, f t)) eqs)) 
27711  469 
 map_terms_stmt f (stmt as Datatype _) = stmt 
470 
 map_terms_stmt f (stmt as Datatypecons _) = stmt 

471 
 map_terms_stmt f (stmt as Class _) = stmt 

472 
 map_terms_stmt f (stmt as Classrel _) = stmt 

473 
 map_terms_stmt f (stmt as Classparam _) = stmt 

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

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

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

477 

27103  478 
fun is_cons program name = case Graph.get_node program name 
24219  479 
of Datatypecons _ => true 
480 
 _ => false; 

481 

27103  482 
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

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

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

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

488 
 no_tyvar (ITyVar _) = false; 

489 
in if no_tyvar res_ty 

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

491 
else [] 

492 
end 

493 
 _ => []; 

494 

24219  495 

27103  496 
(** translation kernel **) 
24219  497 

28724  498 
(* generic mechanisms *) 
499 

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

500 
fun ensure_stmt lookup declare generate thing (dep, (naming, program)) = 
24219  501 
let 
28706  502 
fun add_dep name = case dep of NONE => I 
503 
 SOME dep => Graph.add_edge (dep, name); 

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

505 
of SOME name => (name, naming) 

506 
 NONE => declare thing naming; 

507 
in case try (Graph.get_node program) name 

508 
of SOME stmt => program 

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

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

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

512 
> pair name 
28706  513 
 NONE => program 
514 
> Graph.default_node (name, NoStmt) 

515 
> add_dep name 

516 
> pair naming' 

517 
> curry generate (SOME name) 

518 
> snd 

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

520 
> pair dep 

521 
> pair name 

24219  522 
end; 
523 

26972  524 
fun not_wellsorted thy thm ty sort e = 
525 
let 

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

527 
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

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

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

532 

28724  533 

534 
(* translation *) 

535 

30932  536 
fun ensure_tyco thy algbr funcgr tyco = 
537 
let 

538 
val stmt_datatype = 

539 
let 

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

541 
in 

542 
fold_map (translate_tyvar_sort thy algbr funcgr) vs 

543 
##>> fold_map (fn (c, tys) => 

544 
ensure_const thy algbr funcgr c 

545 
##>> fold_map (translate_typ thy algbr funcgr) tys) cos 

546 
#>> (fn info => Datatype (tyco, info)) 

547 
end; 

548 
in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end 

549 
and ensure_const thy algbr funcgr c = 

550 
let 

551 
fun stmt_datatypecons tyco = 

552 
ensure_tyco thy algbr funcgr tyco 

553 
#>> (fn tyco => Datatypecons (c, tyco)); 

554 
fun stmt_classparam class = 

555 
ensure_class thy algbr funcgr class 

556 
#>> (fn class => Classparam (c, class)); 

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

557 
fun stmt_fun ((vs, ty), eqns) = 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

558 
fold_map (translate_tyvar_sort thy algbr funcgr) vs 
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

559 
##>> translate_typ thy algbr funcgr ty 
32358
98c00ee9e786
proper eta expansion in recfun_codegen.ML; no eta expansion at all in code_thingol.ML
haftmann
parents:
32353
diff
changeset

560 
##>> fold_map (translate_eqn thy algbr funcgr) (burrow_fst (clean_thms thy) eqns) 
32353
0ac26087464b
moved all technical processing of code equations to code_thingol.ML
haftmann
parents:
32350
diff
changeset

561 
#>> (fn info => Fun (c, info)); 
30932  562 
val stmt_const = case Code.get_datatype_of_constr thy c 
563 
of SOME tyco => stmt_datatypecons tyco 

564 
 NONE => (case AxClass.class_of_param thy c 

565 
of SOME class => stmt_classparam class 

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

566 
 NONE => stmt_fun (Code_Preproc.typ funcgr c, Code_Preproc.eqns funcgr c)) 
30932  567 
in ensure_stmt lookup_const (declare_const thy) stmt_const c end 
568 
and ensure_class thy (algbr as (_, algebra)) funcgr class = 

24918  569 
let 
28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

570 
val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; 
24969  571 
val cs = #params (AxClass.get_info thy class); 
24918  572 
val stmt_class = 
573 
fold_map (fn superclass => ensure_class thy algbr funcgr superclass 

574 
##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses 

575 
##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c 

28688  576 
##>> translate_typ thy algbr funcgr ty) cs 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

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

578 
in ensure_stmt lookup_class (declare_class thy) stmt_class class end 
24918  579 
and ensure_classrel thy algbr funcgr (subclass, superclass) = 
580 
let 

581 
val stmt_classrel = 

582 
ensure_class thy algbr funcgr subclass 

583 
##>> ensure_class thy algbr funcgr superclass 

584 
#>> Classrel; 

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

585 
in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end 
26972  586 
and ensure_inst thy (algbr as (_, algebra)) funcgr (class, tyco) = 
24918  587 
let 
28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

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

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

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

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

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

28688  596 
fun translate_superarity superclass = 
24918  597 
ensure_class thy algbr funcgr superclass 
598 
##>> ensure_classrel thy algbr funcgr (class, superclass) 

28688  599 
##>> translate_dicts thy algbr funcgr NONE (arity_typ, [superclass]) 
24918  600 
#>> (fn ((superclass, classrel), [DictConst (inst, dss)]) => 
601 
(superclass, (classrel, (inst, dss)))); 

28688  602 
fun translate_classparam_inst (c, ty) = 
24918  603 
let 
604 
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

605 
val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst); 
24918  606 
val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd 
607 
o Logic.dest_equals o Thm.prop_of) thm; 

608 
in 

609 
ensure_const thy algbr funcgr c 

28688  610 
##>> translate_const thy algbr funcgr (SOME thm) c_ty 
28350  611 
#>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true))) 
24918  612 
end; 
613 
val stmt_inst = 

614 
ensure_class thy algbr funcgr class 

615 
##>> ensure_tyco thy algbr funcgr tyco 

28688  616 
##>> fold_map (translate_tyvar_sort thy algbr funcgr) vs 
617 
##>> fold_map translate_superarity superclasses 

618 
##>> fold_map translate_classparam_inst classparams 

24918  619 
#>> (fn ((((class, tyco), arity), superarities), classparams) => 
620 
Classinst ((class, (tyco, arity)), (superarities, classparams))); 

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

621 
in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end 
30932  622 
and translate_typ thy algbr funcgr (TFree (v, _)) = 
623 
pair (ITyVar (unprefix "'" v)) 

624 
 translate_typ thy algbr funcgr (Type (tyco, tys)) = 

24918  625 
ensure_tyco thy algbr funcgr tyco 
30932  626 
##>> fold_map (translate_typ thy algbr funcgr) tys 
627 
#>> (fn (tyco, tys) => tyco `%% tys) 

28688  628 
and translate_term thy algbr funcgr thm (Const (c, ty)) = 
629 
translate_app thy algbr funcgr thm ((c, ty), []) 

630 
 translate_term thy algbr funcgr thm (Free (v, _)) = 

31889  631 
pair (IVar (SOME v)) 
32273  632 
 translate_term thy algbr funcgr thm (Abs (v, ty, t)) = 
24918  633 
let 
32273  634 
val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t); 
635 
val v'' = if member (op =) (Term.add_free_names t' []) v' 

636 
then SOME v' else NONE 

24918  637 
in 
28688  638 
translate_typ thy algbr funcgr ty 
32273  639 
##>> translate_term thy algbr funcgr thm t' 
640 
#>> (fn (ty, t) => (v'', ty) `=> t) 

24918  641 
end 
28688  642 
 translate_term thy algbr funcgr thm (t as _ $ _) = 
24918  643 
case strip_comb t 
644 
of (Const (c, ty), ts) => 

28688  645 
translate_app thy algbr funcgr thm ((c, ty), ts) 
24918  646 
 (t', ts) => 
28688  647 
translate_term thy algbr funcgr thm t' 
648 
##>> fold_map (translate_term thy algbr funcgr thm) ts 

24918  649 
#>> (fn (t, ts) => t `$$ ts) 
32350  650 
and translate_eqn thy algbr funcgr (thm, proper) = 
30932  651 
let 
652 
val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals 

653 
o Logic.unvarify o prop_of) thm; 

654 
in 

655 
fold_map (translate_term thy algbr funcgr (SOME thm)) args 

656 
##>> translate_term thy algbr funcgr (SOME thm) rhs 

31088  657 
#>> rpair (thm, proper) 
30932  658 
end 
28688  659 
and translate_const thy algbr funcgr thm (c, ty) = 
26972  660 
let 
661 
val tys = Sign.const_typargs thy (c, ty); 

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

662 
val sorts = (map snd o fst o Code_Preproc.typ funcgr) c; 
26972  663 
val tys_args = (fst o Term.strip_type) ty; 
664 
in 

665 
ensure_const thy algbr funcgr c 

31049  666 
##>> fold_map (translate_typ thy algbr funcgr) tys 
28688  667 
##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts) 
668 
##>> fold_map (translate_typ thy algbr funcgr) tys_args 

31049  669 
#>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args))) 
26972  670 
end 
29973  671 
and translate_app_const thy algbr funcgr thm (c_ty, ts) = 
28688  672 
translate_const thy algbr funcgr thm c_ty 
673 
##>> fold_map (translate_term thy algbr funcgr thm) ts 

24918  674 
#>> (fn (t, ts) => t `$$ ts) 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29277
diff
changeset

675 
and translate_case thy algbr funcgr thm (num_args, (t_pos, case_pats)) (c_ty, ts) = 
24918  676 
let 
31892  677 
fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty; 
678 
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

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

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

684 
fun casify naming constrs ty ts = 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

707 
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

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

709 
in map mk (collapse_clause vs_map ts body) end; 
31892  710 
val t = nth ts t_pos; 
711 
val ts_clause = nth_drop t_pos ts; 

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

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

713 
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

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

715 
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

716 
(constrs ~~ ts_clause); 
31892  717 
in ((t, ty), clauses) end; 
24918  718 
in 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29277
diff
changeset

719 
translate_const thy algbr funcgr thm c_ty 
31892  720 
##>> fold_map (fn (constr, n) => translate_const thy algbr funcgr thm constr #>> rpair n) constrs 
29952
9aed85067721
unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann
parents:
29277
diff
changeset

721 
##>> translate_typ thy algbr funcgr ty 
31892  722 
##>> fold_map (translate_term thy algbr funcgr thm) ts 
723 
#> (fn (((t, constrs), ty), ts) => 

724 
`(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts))) 

24918  725 
end 
29973  726 
and translate_app_case thy algbr funcgr thm (case_scheme as (num_args, _)) ((c, ty), ts) = 
727 
if length ts < num_args then 

728 
let 

729 
val k = length ts; 

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

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

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

733 
in 

734 
fold_map (translate_typ thy algbr funcgr) tys 

735 
##>> translate_case thy algbr funcgr thm case_scheme ((c, ty), ts @ map Free vs) 

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

739 
translate_case thy algbr funcgr thm case_scheme ((c, ty), Library.take (num_args, ts)) 

740 
##>> fold_map (translate_term thy algbr funcgr thm) (Library.drop (num_args, ts)) 

741 
#>> (fn (t, ts) => t `$$ ts) 

742 
else 

743 
translate_case thy algbr funcgr thm case_scheme ((c, ty), ts) 

744 
and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) = 

745 
case Code.get_case_scheme thy c 

30023
55954f726043
permissive check for pattern discipline in case schemes
haftmann
parents:
30009
diff
changeset

746 
of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts 
30932  747 
 NONE => translate_app_const thy algbr funcgr thm c_ty_ts 
748 
and translate_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) = 

749 
fold_map (ensure_class thy algbr funcgr) (proj_sort sort) 

750 
#>> (fn sort => (unprefix "'" v, sort)) 

751 
and translate_dicts thy (algbr as (proj_sort, algebra)) funcgr thm (ty, sort) = 

752 
let 

753 
datatype typarg = 

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

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

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

757 
Global ((class, tyco), yss) 

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

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

760 
fun type_constructor tyco yss class = 

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

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

763 
let 

764 
val sort' = proj_sort sort; 

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

32795  766 
val typargs = Sorts.of_sort_derivation algebra 
30932  767 
{class_relation = class_relation, type_constructor = type_constructor, 
768 
type_variable = type_variable} (ty, proj_sort sort) 

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

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

771 
ensure_inst thy algbr funcgr inst 

772 
##>> (fold_map o fold_map) mk_dict yss 

773 
#>> (fn (inst, dss) => DictConst (inst, dss)) 

31962  774 
 mk_dict (Local (classrels, (v, (n, sort)))) = 
30932  775 
fold_map (ensure_classrel thy algbr funcgr) classrels 
31962  776 
#>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort)))) 
30932  777 
in fold_map mk_dict typargs end; 
24918  778 

25969  779 

27103  780 
(* store *) 
781 

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

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

785 
val empty = (empty_naming, Graph.empty); 
28706  786 
fun purge thy cs (naming, program) = 
27609  787 
let 
28706  788 
val names_delete = cs 
789 
> map_filter (lookup_const naming) 

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

791 
> Graph.all_preds program; 

792 
val program' = Graph.del_nodes names_delete program; 

793 
in (naming, program') end; 

27103  794 
); 
795 

796 
val cached_program = Program.get; 

25969  797 

28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

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

799 
Program.change_yield thy (fn naming_program => (NONE, naming_program) 
28924
5c8781b7d6a4
code_funcgr interface includes also sort algebra
haftmann
parents:
28724
diff
changeset

800 
> f thy algebra funcgr name 
28663
bd8438543bf2
code identifier namings are no longer imperative
haftmann
parents:
28423
diff
changeset

801 
> (fn name => fn (_, naming_program) => (name, naming_program))); 
27103  802 

803 

804 
(* program generation *) 

805 

806 
fun consts_program thy cs = 

807 
let 

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

808 
fun project_consts cs (naming, program) = 
27103  809 
let 
810 
val cs_all = Graph.all_succs program cs; 

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

811 
in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end; 
27103  812 
fun generate_consts thy algebra funcgr = 
813 
fold_map (ensure_const thy algebra funcgr); 

814 
in 

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

815 
invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs 
27103  816 
> project_consts 
817 
end; 

818 

819 

820 
(* value evaluation *) 

25969  821 

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

822 
fun ensure_value thy algbr funcgr t = 
24918  823 
let 
824 
val ty = fastype_of t; 

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

826 
o dest_TFree))) t []; 

827 
val stmt_value = 

28688  828 
fold_map (translate_tyvar_sort thy algbr funcgr) vs 
829 
##>> translate_typ thy algbr funcgr ty 

830 
##>> translate_term thy algbr funcgr NONE t 

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

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

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

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

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

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

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

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

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

845 
#> term_value 
26011  846 
end; 
24219  847 

30947  848 
fun base_evaluator thy evaluator algebra funcgr vs t = 
30942
1e246776f876
diagnostic commands now in code_thingol; tuned code of funny continuations
haftmann
parents:
30932
diff
changeset

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

850 
val (((naming, program), (((vs', ty'), t'), deps)), _) = 
88aaab83b6fc
dropped explicit suppport for frees in evaluation conversion stack
haftmann
parents:
31054
diff
changeset

851 
invoke_generation thy (algebra, funcgr) ensure_value t; 
30947  852 
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

853 
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

854 

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

855 
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

856 
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

857 

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

858 

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

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

860 

31036  861 
fun read_const_exprs thy = 
862 
let 

863 
fun consts_of some_thyname = 

864 
let 

865 
val thy' = case some_thyname 

866 
of SOME thyname => ThyInfo.the_theory thyname thy 

867 
 NONE => thy; 

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

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

870 
fun belongs_here c = 

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

872 
in case some_thyname 

873 
of NONE => cs 

874 
 SOME thyname => filter belongs_here cs 

875 
end; 

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

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

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

31156  879 
else ([Code.read_const thy s], []); 
31036  880 
in pairself flat o split_list o map read_const_expr end; 
881 

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

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

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

884 
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

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

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

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

888 
> 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

889 
> 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

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

891 

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

892 
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

893 

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

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

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

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

898 
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

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

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

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

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

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

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

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

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

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

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

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

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

912 

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

913 
local 
27103  914 

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

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

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

917 

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

920 

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

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

922 

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

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

924 
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

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

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

927 
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

928 

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

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

930 
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

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

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

933 
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

934 

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

935 
end; 
27103  936 

24219  937 
end; (*struct*) 
938 

939 

28054  940 
structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol; 