author  haftmann 
Wed, 13 May 2009 18:41:40 +0200  
changeset 31138  a51ce445d498 
parent 31092  27a6558e64b6 
child 31142  8f609d1e7002 
permissions  rwrr 
24219  1 
(* Title: Pure/Isar/code_unit.ML 
2 
Author: Florian Haftmann, TU Muenchen 

3 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

4 
Basic notions of code generation. Auxiliary. 
24219  5 
*) 
6 

7 
signature CODE_UNIT = 

8 
sig 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

9 
(*typ instantiations*) 
26970  10 
val typscheme: theory > string * typ > (string * sort) list * typ 
28423  11 
val inst_thm: theory > sort Vartab.table > thm > thm 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

12 

26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

13 
(*constant aliasses*) 
26354  14 
val add_const_alias: thm > theory > theory 
28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

15 
val triv_classes: theory > class list 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

16 
val resubst_alias: theory > string > string 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

17 

f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

18 
(*constants*) 
24219  19 
val string_of_typ: theory > typ > string 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

20 
val string_of_const: theory > string > string 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

21 
val no_args: theory > string > int 
26112  22 
val check_const: theory > term > string 
24219  23 
val read_bare_const: theory > string > string * typ 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

24 
val read_const: theory > string > string 
24219  25 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

26 
(*constructor sets*) 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

27 
val constrset_of_consts: theory > (string * typ) list 
24219  28 
> string * ((string * sort) list * (string * typ list) list) 
29 

30022
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

30 
(*code equations*) 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

31 
val mk_eqn: theory > (string > bool) > thm * bool > thm * bool 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

32 
val mk_eqn_liberal: theory > (string > bool) > thm > (thm * bool) option 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

33 
val assert_eqn: theory > (string > bool) > thm * bool > thm * bool 
31089  34 
val const_eqn: theory > thm > string 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

35 
val const_typ_eqn: thm > string * typ 
31089  36 
val typscheme_eqn: theory > thm > (string * sort) list * typ 
28423  37 
val expand_eta: theory > int > thm > thm 
28368  38 
val rewrite_eqn: simpset > thm > thm 
27582  39 
val rewrite_head: thm list > thm > thm 
28423  40 
val norm_args: theory > thm list > thm list 
31036  41 
val norm_varnames: theory > thm list > thm list 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

42 

98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

43 
(*case certificates*) 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

44 
val case_cert: thm > string * (int * string list) 
24219  45 
end; 
46 

28054  47 
structure Code_Unit: CODE_UNIT = 
24219  48 
struct 
49 

50 

51 
(* auxiliary *) 

52 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26747
diff
changeset

53 
fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy); 
25597
34860182b250
moved instance parameter management from class.ML to axclass.ML
haftmann
parents:
25540
diff
changeset

54 
fun string_of_const thy c = case AxClass.inst_of_param thy c 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

55 
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

56 
 NONE => Sign.extern_const thy c; 
24219  57 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

58 
fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; 
24219  59 

26354  60 

61 
(* utilities *) 

62 

26970  63 
fun typscheme thy (c, ty) = 
64 
let 

30022
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

65 
val ty' = Logic.unvarifyT ty; 
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

66 
fun dest (TFree (v, sort)) = (v, sort) 
26970  67 
 dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); 
30022
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

68 
val vs = map dest (Sign.const_typargs thy (c, ty')); 
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

69 
in (vs, Type.strip_sorts ty') end; 
26970  70 

28423  71 
fun inst_thm thy tvars' thm = 
26354  72 
let 
73 
val tvars = (Term.add_tvars o Thm.prop_of) thm []; 

28310  74 
val inter_sort = Sorts.inter_sort (Sign.classes_of thy); 
75 
fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v 

76 
of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) 

77 
(tvar, (v, inter_sort (sort, sort')))) 

26354  78 
 NONE => NONE; 
79 
val insts = map_filter mk_inst tvars; 

80 
in Thm.instantiate (insts, []) thm end; 

81 

28423  82 
fun expand_eta thy k thm = 
26354  83 
let 
84 
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; 

85 
val (head, args) = strip_comb lhs; 

86 
val l = if k = ~1 

87 
then (length o fst o strip_abs) rhs 

88 
else Int.max (0, k  length args); 

89 
val used = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); 

90 
fun get_name _ 0 = pair [] 

91 
 get_name (Abs (v, ty, t)) k = 

92 
Name.variants [v] 

93 
##>> get_name t (k  1) 

94 
#>> (fn ([v'], vs') => (v', ty) :: vs') 

95 
 get_name t k = 

96 
let 

97 
val (tys, _) = (strip_type o fastype_of) t 

98 
in case tys 

99 
of [] => raise TERM ("expand_eta", [t]) 

100 
 ty :: _ => 

101 
Name.variants [""] 

102 
#> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k  1) 

103 
#>> (fn vs' => (v, ty) :: vs')) 

104 
end; 

105 
val (vs, _) = get_name rhs l used; 

106 
fun expand (v, ty) thm = Drule.fun_cong_rule thm 

107 
(Thm.cterm_of thy (Var ((v, 0), ty))); 

108 
in 

109 
thm 

110 
> fold expand vs 

111 
> Conv.fconv_rule Drule.beta_eta_conversion 

112 
end; 

113 

28368  114 
fun eqn_conv conv = 
26354  115 
let 
116 
fun lhs_conv ct = if can Thm.dest_comb ct 

117 
then (Conv.combination_conv lhs_conv conv) ct 

118 
else Conv.all_conv ct; 

119 
in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; 

120 

121 
fun head_conv conv = 

122 
let 

123 
fun lhs_conv ct = if can Thm.dest_comb ct 

124 
then (Conv.fun_conv lhs_conv) ct 

125 
else conv ct; 

126 
in Conv.fun_conv (Conv.arg_conv lhs_conv) end; 

127 

28368  128 
val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; 
26354  129 
val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; 
130 

28423  131 
fun norm_args thy thms = 
26354  132 
let 
133 
val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; 

28310  134 
val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0; 
26354  135 
in 
136 
thms 

28423  137 
> map (expand_eta thy k) 
26354  138 
> map (Conv.fconv_rule Drule.beta_eta_conversion) 
139 
end; 

140 

31036  141 
fun canonical_tvars thy thm = 
26354  142 
let 
28423  143 
val ctyp = Thm.ctyp_of thy; 
31036  144 
val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'"; 
26354  145 
fun tvars_subst_for thm = (fold_types o fold_atyps) 
146 
(fn TVar (v_i as (v, _), sort) => let 

147 
val v' = purify_tvar v 

148 
in if v = v' then I 

149 
else insert (op =) (v_i, (v', sort)) end 

150 
 _ => I) (prop_of thm) []; 

151 
fun mk_inst (v_i, (v', sort)) (maxidx, acc) = 

152 
let 

153 
val ty = TVar (v_i, sort) 

154 
in 

155 
(maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc) 

156 
end; 

157 
val maxidx = Thm.maxidx_of thm + 1; 

158 
val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []); 

159 
in Thm.instantiate (inst, []) thm end; 

160 

31036  161 
fun canonical_vars thy thm = 
26354  162 
let 
28423  163 
val cterm = Thm.cterm_of thy; 
31036  164 
val purify_var = Name.desymbolize false; 
26354  165 
fun vars_subst_for thm = fold_aterms 
166 
(fn Var (v_i as (v, _), ty) => let 

167 
val v' = purify_var v 

168 
in if v = v' then I 

169 
else insert (op =) (v_i, (v', ty)) end 

170 
 _ => I) (prop_of thm) []; 

171 
fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) = 

172 
let 

173 
val t = Var (v_i, ty) 

174 
in 

175 
(maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc) 

176 
end; 

177 
val maxidx = Thm.maxidx_of thm + 1; 

178 
val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []); 

179 
in Thm.instantiate ([], inst) thm end; 

180 

31036  181 
fun canonical_absvars thm = 
26354  182 
let 
183 
val t = Thm.plain_prop_of thm; 

31036  184 
val purify_var = Name.desymbolize false; 
26354  185 
val t' = Term.map_abs_vars purify_var t; 
186 
in Thm.rename_boundvars t t' thm end; 

187 

31036  188 
fun norm_varnames thy thms = 
26354  189 
let 
190 
fun burrow_thms f [] = [] 

191 
 burrow_thms f thms = 

192 
thms 

193 
> Conjunction.intr_balanced 

194 
> f 

195 
> Conjunction.elim_balanced (length thms) 

196 
in 

197 
thms 

31036  198 
> map (canonical_vars thy) 
199 
> map canonical_absvars 

30739  200 
> map Drule.zero_var_indexes 
31036  201 
> burrow_thms (canonical_tvars thy) 
30688  202 
> Drule.zero_var_indexes_list 
26354  203 
end; 
204 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

205 

26354  206 
(* const aliasses *) 
207 

208 
structure ConstAlias = TheoryDataFun 

209 
( 

26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

210 
type T = ((string * string) * thm) list * class list; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

211 
val empty = ([], []); 
26354  212 
val copy = I; 
26618  213 
val extend = I; 
29288  214 
fun merge _ ((alias1, classes1), (alias2, classes2)) : T = 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

215 
(Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

216 
Library.merge (op =) (classes1, classes2)); 
26354  217 
); 
218 

28423  219 
fun add_const_alias thm thy = 
26354  220 
let 
28423  221 
val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm) 
26354  222 
of SOME lhs_rhs => lhs_rhs 
223 
 _ => error ("Not an equation: " ^ Display.string_of_thm thm); 

224 
val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs 

225 
of SOME c_c' => c_c' 

226 
 _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm); 

26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

227 
val some_class = the_list (AxClass.class_of_param thy (snd c_c')); 
28423  228 
in thy > 
26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

229 
ConstAlias.map (fn (alias, classes) => 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

230 
((c_c', thm) :: alias, fold (insert (op =)) some_class classes)) 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

231 
end; 
26354  232 

26747
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

233 
fun resubst_alias thy = 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

234 
let 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

235 
val alias = fst (ConstAlias.get thy); 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

236 
val subst_inst_param = Option.map fst o AxClass.inst_of_param thy; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

237 
fun subst_alias c = 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

238 
get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

239 
in 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

240 
perhaps subst_inst_param 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

241 
#> perhaps subst_alias 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

242 
end; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

243 

f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

244 
val triv_classes = snd o ConstAlias.get; 
f32fa5f5bdd1
moved 'trivial classes' to foundation of code generator
haftmann
parents:
26618
diff
changeset

245 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

246 

26610  247 
(* reading constants as terms *) 
24219  248 

26112  249 
fun check_bare_const thy t = case try dest_Const t 
250 
of SOME c_ty => c_ty 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26747
diff
changeset

251 
 NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); 
26112  252 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

253 
fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; 
26112  254 

255 
fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; 

24219  256 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

257 
fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; 
24219  258 

259 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

260 
(* constructor sets *) 
24219  261 

24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

262 
fun constrset_of_consts thy cs = 
24219  263 
let 
28704
8703d17c5e68
assert that no class parameter is used as constructor
haftmann
parents:
28423
diff
changeset

264 
val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c 
8703d17c5e68
assert that no class parameter is used as constructor
haftmann
parents:
28423
diff
changeset

265 
then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs; 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

266 
fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

267 
^ " :: " ^ string_of_typ thy ty); 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

268 
fun last_typ c_ty ty = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

269 
let 
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
28708
diff
changeset

270 
val frees = OldTerm.typ_tfrees ty; 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

271 
val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

272 
handle TYPE _ => no_constr c_ty 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

273 
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else (); 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

274 
val _ = if length frees <> length vs then no_constr c_ty else (); 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

275 
in (tyco, vs) end; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

276 
fun ty_sorts (c, ty) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

277 
let 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

278 
val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; 
26970  279 
val (tyco, _) = last_typ (c, ty) ty_decl; 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

280 
val (_, vs) = last_typ (c, ty) ty; 
28015  281 
in ((tyco, map snd vs), (c, (map fst vs, ty))) end; 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

282 
fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

283 
let 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

284 
val _ = if tyco' <> tyco 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

285 
then error "Different type constructors in constructor set" 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

286 
else (); 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

287 
val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

288 
in ((tyco, sorts), c :: cs) end; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

289 
fun inst vs' (c, (vs, ty)) = 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

290 
let 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

291 
val the_v = the o AList.lookup (op =) (vs ~~ vs'); 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

292 
val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

293 
in (c, (fst o strip_type) ty') end; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

294 
val c' :: cs' = map ty_sorts cs; 
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

295 
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c'); 
24848  296 
val vs = Name.names Name.context Name.aT sorts; 
24423
ae9cd0e92423
overloaded definitions accompanied by explicit constants
haftmann
parents:
24219
diff
changeset

297 
val cs''' = map (inst vs) cs''; 
30022
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

298 
in (tyco, (vs, rev cs''')) end; 
24219  299 

300 

30022
1d8b8fa19074
maintain order of constructors in datatypes; clarified conventions for type schemes
haftmann
parents:
29288
diff
changeset

301 
(* code equations *) 
24219  302 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

303 
exception BAD_THM of string; 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

304 
fun bad_thm msg = raise BAD_THM msg; 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

305 
fun error_thm f thm = f thm handle BAD_THM msg => error msg; 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

306 
fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

307 

3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

308 
fun is_linear thm = 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

309 
let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

310 
in not (has_duplicates (op =) ((fold o fold_aterms) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

311 
(fn Var (v, _) => cons v  _ => I) args [])) end; 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

312 

3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

313 
fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) = 
24219  314 
let 
315 
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm 

316 
handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

317 
 THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); 
30766
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

318 
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

319 
 Free _ => bad_thm ("Illegal free variable in equation\n" 
30766
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

320 
^ Display.string_of_thm thm) 
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

321 
 _ => I) t []; 
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

322 
fun tvars_of t = fold_term_types (fn _ => 
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

323 
fold_atyps (fn TVar (v, _) => insert (op =) v 
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

324 
 TFree _ => bad_thm 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

325 
("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t []; 
24219  326 
val lhs_vs = vars_of lhs; 
327 
val rhs_vs = vars_of rhs; 

328 
val lhs_tvs = tvars_of lhs; 

30766
44561a14a4c5
corrected check for additional type variables on rhs of code equations
haftmann
parents:
30739
diff
changeset

329 
val rhs_tvs = tvars_of rhs; 
24219  330 
val _ = if null (subtract (op =) lhs_vs rhs_vs) 
331 
then () 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

332 
else bad_thm ("Free variables on right hand side of equation\n" 
24219  333 
^ Display.string_of_thm thm); 
334 
val _ = if null (subtract (op =) lhs_tvs rhs_tvs) 

335 
then () 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

336 
else bad_thm ("Free type variables on right hand side of equation\n" 
28423  337 
^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

338 
val (c, ty) = case head 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

339 
of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

340 
 _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); 
24219  341 
fun check _ (Abs _) = bad_thm 
342 
("Abstraction on left hand side of equation\n" 

343 
^ Display.string_of_thm thm) 

344 
 check 0 (Var _) = () 

345 
 check _ (Var _) = bad_thm 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

346 
("Variable with application on left hand side of equation\n" 
24219  347 
^ Display.string_of_thm thm) 
348 
 check n (t1 $ t2) = (check (n+1) t1; check 0 t2) 

31092
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

349 
 check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

350 
then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

351 
then () 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

352 
else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

353 
^ Display.string_of_thm thm) 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

354 
else bad_thm 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

355 
("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" 
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

356 
^ Display.string_of_thm thm); 
24219  357 
val _ = map (check 0) args; 
31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

358 
val _ = if not proper orelse is_linear thm then () 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

359 
else bad_thm ("Duplicate variables on left hand side of equation\n" 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

360 
^ Display.string_of_thm thm); 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

361 
val _ = if (is_none o AxClass.class_of_param thy) c 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

362 
then () 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

363 
else bad_thm ("Polymorphic constant as head in equation\n" 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

364 
^ Display.string_of_thm thm) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

365 
val _ = if not (is_constr_head c) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

366 
then () 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

367 
else bad_thm ("Constructor as head in equation\n" 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

368 
^ Display.string_of_thm thm) 
28423  369 
val ty_decl = Sign.the_const_type thy c; 
370 
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) 

371 
then () else bad_thm ("Type\n" ^ string_of_typ thy ty 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

372 
^ "\nof equation\n" 
28423  373 
^ Display.string_of_thm thm 
374 
^ "\nis incompatible with declared function type\n" 

375 
^ string_of_typ thy ty_decl) 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

376 
in (thm, proper) end; 
28423  377 

31092
27a6558e64b6
proper error handling for malformed code equations
haftmann
parents:
31090
diff
changeset

378 
fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); 
28423  379 

31089  380 
val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; 
28423  381 

31089  382 
fun typscheme_eqn thy = typscheme thy o const_typ_eqn; 
28423  383 

31090
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

384 
(*these are permissive wrt. to overloaded constants!*) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

385 
fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

386 
apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

387 

3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

388 
fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

389 
o try_thm (gen_assert_eqn thy is_constr_head (K true)) 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

390 
o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); 
3be41b271023
clarified matter of "proper" flag in code equations
haftmann
parents:
31089
diff
changeset

391 

31089  392 
fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn; 
24219  393 

394 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

395 
(* case cerificates *) 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

396 

24917  397 
fun case_certificate thm = 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

398 
let 
24917  399 
val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals 
400 
o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm; 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

401 
val _ = case head of Free _ => true 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

402 
 Var _ => true 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

403 
 _ => raise TERM ("case_cert", []); 
24917  404 
val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; 
405 
val (Const (case_const, _), raw_params) = strip_comb case_expr; 

406 
val n = find_index (fn Free (v, _) => v = case_var  _ => false) raw_params; 

407 
val _ = if n = ~1 then raise TERM ("case_cert", []) else (); 

408 
val params = map (fst o dest_Var) (nth_drop n raw_params); 

409 
fun dest_case t = 

24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

410 
let 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

411 
val (head' $ t_co, rhs) = Logic.dest_equals t; 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

412 
val _ = if head' = head then () else raise TERM ("case_cert", []); 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

413 
val (Const (co, _), args) = strip_comb t_co; 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

414 
val (Var (param, _), args') = strip_comb rhs; 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

415 
val _ = if args' = args then () else raise TERM ("case_cert", []); 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

416 
in (param, co) end; 
24917  417 
fun analyze_cases cases = 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

418 
let 
24917  419 
val co_list = fold (AList.update (op =) o dest_case) cases []; 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

420 
in map (the o AList.lookup (op =) co_list) params end; 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

421 
fun analyze_let t = 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

422 
let 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

423 
val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

424 
val _ = if head' = head then () else raise TERM ("case_cert", []); 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

425 
val _ = if arg' = arg then () else raise TERM ("case_cert", []); 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

426 
val _ = if [param'] = params then () else raise TERM ("case_cert", []); 
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

427 
in [] end; 
24917  428 
fun analyze (cases as [let_case]) = 
429 
(analyze_cases cases handle Bind => analyze_let let_case) 

430 
 analyze cases = analyze_cases cases; 

431 
in (case_const, (n, analyze cases)) end; 

432 

433 
fun case_cert thm = case_certificate thm 

434 
handle Bind => error "bad case certificate" 

28346
b8390cd56b8f
discontinued special treatment of op = vs. eq_class.eq
haftmann
parents:
28310
diff
changeset

435 
 TERM _ => error "bad case certificate"; 
24844
98c006a30218
certificates for code generator case expressions
haftmann
parents:
24707
diff
changeset

436 

24219  437 
end; 