19 val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms) |
17 val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms) |
20 -> theory -> theory |
18 -> theory -> theory |
21 val del_datatype: string -> theory -> theory |
19 val del_datatype: string -> theory -> theory |
22 val add_inline: thm -> theory -> theory |
20 val add_inline: thm -> theory -> theory |
23 val del_inline: thm -> theory -> theory |
21 val del_inline: thm -> theory -> theory |
|
22 val add_inline_proc: (theory -> cterm list -> thm list) -> theory -> theory |
|
23 val add_constrains: (theory -> term list -> (indexname * sort) list) -> theory -> theory |
24 val add_preproc: (theory -> thm list -> thm list) -> theory -> theory |
24 val add_preproc: (theory -> thm list -> thm list) -> theory -> theory |
25 val these_funcs: theory -> CodegenConsts.const -> thm list |
25 val these_funcs: theory -> CodegenConsts.const -> thm list |
26 val get_datatype: theory -> string |
26 val get_datatype: theory -> string |
27 -> ((string * sort) list * (string * typ list) list) option |
27 -> ((string * sort) list * (string * typ list) list) option |
28 val get_datatype_of_constr: theory -> CodegenConsts.const -> string option |
28 val get_datatype_of_constr: theory -> CodegenConsts.const -> string option |
29 |
29 |
30 val print_thms: theory -> unit |
30 val print_thms: theory -> unit |
31 |
31 |
32 val typ_func: theory -> thm -> typ |
32 val typ_func: theory -> thm -> typ |
33 val rewrite_func: thm list -> thm -> thm |
33 val rewrite_func: thm list -> thm -> thm |
34 val preprocess_cterm: theory -> cterm -> thm |
34 val preprocess_cterm: theory -> (string * typ -> typ) -> cterm -> thm * cterm |
35 val preprocess: theory -> thm list -> thm list |
35 |
36 |
36 val trace: bool ref |
37 val debug: bool ref |
|
38 val strict_functyp: bool ref |
37 val strict_functyp: bool ref |
39 end; |
38 end; |
40 |
39 |
41 signature PRIVATE_CODEGEN_DATA = |
40 signature PRIVATE_CODEGEN_DATA = |
42 sig |
41 sig |
105 |
105 |
106 |
106 |
107 |
107 |
108 (** code theorems **) |
108 (** code theorems **) |
109 |
109 |
110 (* making function theorems *) |
110 (* making rewrite theorems *) |
111 |
111 |
112 fun bad_thm msg thm = |
112 fun bad_thm msg thm = |
113 error (msg ^ ": " ^ string_of_thm thm); |
113 error (msg ^ ": " ^ string_of_thm thm); |
114 |
114 |
|
115 fun check_rew thy thm = |
|
116 let |
|
117 val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm; |
|
118 fun vars_of t = fold_aterms |
|
119 (fn Var (v, _) => insert (op =) v |
|
120 | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm |
|
121 | _ => I) t []; |
|
122 fun tvars_of t = fold_term_types |
|
123 (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v |
|
124 | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t []; |
|
125 val lhs_vs = vars_of lhs; |
|
126 val rhs_vs = vars_of rhs; |
|
127 val lhs_tvs = tvars_of lhs; |
|
128 val rhs_tvs = tvars_of lhs; |
|
129 val _ = if null (subtract (op =) lhs_vs rhs_vs) |
|
130 then () |
|
131 else bad_thm "Free variables on right hand side of rewrite theorems" thm |
|
132 val _ = if null (subtract (op =) lhs_tvs rhs_tvs) |
|
133 then () |
|
134 else bad_thm "Free type variables on right hand side of rewrite theorems" thm |
|
135 in thm end; |
|
136 |
|
137 fun mk_rew thy thm = |
|
138 let |
|
139 val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm; |
|
140 in |
|
141 map (check_rew thy) thms |
|
142 end; |
|
143 |
|
144 |
|
145 (* making function theorems *) |
|
146 |
115 fun typ_func thy = snd o dest_Const o fst o strip_comb o fst |
147 fun typ_func thy = snd o dest_Const o fst o strip_comb o fst |
116 o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; |
148 o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; |
117 |
149 |
118 val mk_rew = |
|
119 #mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of; |
|
120 |
|
121 val strict_functyp = ref true; |
150 val strict_functyp = ref true; |
122 |
151 |
|
152 fun dest_func thy = apfst dest_Const o strip_comb o Envir.beta_eta_contract |
|
153 o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; |
|
154 |
|
155 fun mk_head thy thm = |
|
156 ((CodegenConsts.norm_of_typ thy o fst o dest_func thy) thm, thm); |
|
157 |
|
158 fun check_func verbose thy thm = case try (dest_func thy) thm |
|
159 of SOME (c_ty as (c, ty), args) => |
|
160 let |
|
161 val _ = |
|
162 if has_duplicates (op =) |
|
163 ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []) |
|
164 then bad_thm "Repeated variables on left hand side of function equation" thm |
|
165 else () |
|
166 val is_classop = (is_some o AxClass.class_of_param thy) c; |
|
167 val const = CodegenConsts.norm_of_typ thy c_ty; |
|
168 val ty_decl = CodegenConsts.disc_typ_of_const thy |
|
169 (snd o CodegenConsts.typ_of_inst thy) const; |
|
170 val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); |
|
171 in if Sign.typ_equiv thy (ty_decl, ty) |
|
172 then (const, thm) |
|
173 else (if is_classop orelse (!strict_functyp andalso not |
|
174 (Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty))) |
|
175 then error else (if verbose then warning else K ()) #> K (const, thm)) |
|
176 ("Type\n" ^ string_of_typ ty |
|
177 ^ "\nof function theorem\n" |
|
178 ^ string_of_thm thm |
|
179 ^ "\nis strictly less general than declared function type\n" |
|
180 ^ string_of_typ ty_decl) |
|
181 end |
|
182 | NONE => bad_thm "Not a function equation" thm; |
|
183 |
|
184 fun check_typ_classop thy thm = |
|
185 let |
|
186 val (c_ty as (c, ty), _) = dest_func thy thm; |
|
187 in case AxClass.class_of_param thy c |
|
188 of SOME class => let |
|
189 val const = CodegenConsts.norm_of_typ thy c_ty; |
|
190 val ty_decl = CodegenConsts.disc_typ_of_const thy |
|
191 (snd o CodegenConsts.typ_of_inst thy) const; |
|
192 val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); |
|
193 in if Sign.typ_equiv thy (ty_decl, ty) |
|
194 then thm |
|
195 else error |
|
196 ("Type\n" ^ string_of_typ ty |
|
197 ^ "\nof function theorem\n" |
|
198 ^ string_of_thm thm |
|
199 ^ "\nis strictly less general than declared function type\n" |
|
200 ^ string_of_typ ty_decl) |
|
201 end |
|
202 | NONE => thm |
|
203 end; |
|
204 |
123 fun mk_func thy raw_thm = |
205 fun mk_func thy raw_thm = |
124 let |
206 mk_rew thy raw_thm |
125 fun dest_func thy = dest_Const o fst o strip_comb o Envir.beta_eta_contract |
207 |> map (check_func true thy); |
126 o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; |
|
127 fun mk_head thm = case try (dest_func thy) thm |
|
128 of SOME (c_ty as (c, ty)) => |
|
129 let |
|
130 val is_classop = (is_some o AxClass.class_of_param thy) c; |
|
131 val const = CodegenConsts.norm_of_typ thy c_ty; |
|
132 val ty_decl = CodegenConsts.disc_typ_of_const thy |
|
133 (snd o CodegenConsts.typ_of_inst thy) const; |
|
134 val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); |
|
135 in if Sign.typ_equiv thy (ty_decl, ty) |
|
136 then (const, thm) |
|
137 else ((if is_classop orelse !strict_functyp then error else warning) |
|
138 ("Type\n" ^ string_of_typ ty |
|
139 ^ "\nof function theorem\n" |
|
140 ^ string_of_thm thm |
|
141 ^ "\nis strictly less general than declared function type\n" |
|
142 ^ string_of_typ ty_decl); (const, thm)) |
|
143 end |
|
144 | NONE => bad_thm "Not a function equation" thm; |
|
145 in |
|
146 mk_rew thy raw_thm |
|
147 |> map mk_head |
|
148 end; |
|
149 |
208 |
150 fun get_prim_def_funcs thy c = |
209 fun get_prim_def_funcs thy c = |
151 let |
210 let |
152 fun constrain thm0 thm = case AxClass.class_of_param thy (fst c) |
211 fun constrain thm0 thm = case AxClass.class_of_param thy (fst c) |
153 of SOME _ => |
212 of SOME _ => |
220 |
277 |
221 structure Consttab = CodegenConsts.Consttab; |
278 structure Consttab = CodegenConsts.Consttab; |
222 |
279 |
223 datatype preproc = Preproc of { |
280 datatype preproc = Preproc of { |
224 inlines: thm list, |
281 inlines: thm list, |
|
282 inline_procs: (serial * (theory -> cterm list -> thm list)) list, |
|
283 constrains: (serial * (theory -> term list -> (indexname * sort) list)) list, |
225 preprocs: (serial * (theory -> thm list -> thm list)) list |
284 preprocs: (serial * (theory -> thm list -> thm list)) list |
226 }; |
285 }; |
227 |
286 |
228 fun mk_preproc (inlines, preprocs) = |
287 fun mk_preproc ((inlines, inline_procs), (constrains, preprocs)) = |
229 Preproc { inlines = inlines, preprocs = preprocs }; |
288 Preproc { inlines = inlines, inline_procs = inline_procs, constrains = constrains, preprocs = preprocs }; |
230 fun map_preproc f (Preproc { inlines, preprocs }) = |
289 fun map_preproc f (Preproc { inlines, inline_procs, constrains, preprocs }) = |
231 mk_preproc (f (inlines, preprocs)); |
290 mk_preproc (f ((inlines, inline_procs), (constrains, preprocs))); |
232 fun merge_preproc (Preproc { inlines = inlines1, preprocs = preprocs1 }, |
291 fun merge_preproc (Preproc { inlines = inlines1, inline_procs = inline_procs1, constrains = constrains1 , preprocs = preprocs1 }, |
233 Preproc { inlines = inlines2, preprocs = preprocs2 }) = |
292 Preproc { inlines = inlines2, inline_procs = inline_procs2, constrains = constrains2 , preprocs = preprocs2 }) = |
234 let |
293 let |
235 val (touched1, inlines) = merge_thms (inlines1, inlines2); |
294 val (touched1, inlines) = merge_thms (inlines1, inlines2); |
236 val (touched2, preprocs) = merge_alist (op =) (K true) (preprocs1, preprocs2); |
295 val (touched2, inline_procs) = merge_alist (op =) (K true) (inline_procs1, inline_procs2); |
237 in (touched1 orelse touched2, mk_preproc (inlines, preprocs)) end; |
296 val (touched3, constrains) = merge_alist (op =) (K true) (constrains1, constrains2); |
|
297 val (touched4, preprocs) = merge_alist (op =) (K true) (preprocs1, preprocs2); |
|
298 in (touched1 orelse touched2 orelse touched3 orelse touched4, |
|
299 mk_preproc ((inlines, inline_procs), (constrains, preprocs))) end; |
238 |
300 |
239 fun join_func_thms (tabs as (tab1, tab2)) = |
301 fun join_func_thms (tabs as (tab1, tab2)) = |
240 let |
302 let |
241 val cs1 = Consttab.keys tab1; |
303 val cs1 = Consttab.keys tab1; |
242 val cs2 = Consttab.keys tab2; |
304 val cs2 = Consttab.keys tab2; |
255 fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) = |
317 fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) = |
256 gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) |
318 gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) |
257 andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2); |
319 andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2); |
258 fun merge_dtyps (tabs as (tab1, tab2)) = |
320 fun merge_dtyps (tabs as (tab1, tab2)) = |
259 let |
321 let |
260 (*EXTEND: could be more clever with respect to constructors*) |
|
261 val tycos1 = Symtab.keys tab1; |
322 val tycos1 = Symtab.keys tab1; |
262 val tycos2 = Symtab.keys tab2; |
323 val tycos2 = Symtab.keys tab2; |
263 val tycos' = filter (member eq_string tycos2) tycos1; |
324 val tycos' = filter (member eq_string tycos2) tycos1; |
264 val touched = gen_eq_set (eq_pair (op =) (eq_dtyp)) |
325 val touched = not (gen_eq_set (op =) (tycos1, tycos2) andalso |
|
326 gen_eq_set (eq_pair (op =) (eq_dtyp)) |
265 (AList.make (the o Symtab.lookup tab1) tycos', |
327 (AList.make (the o Symtab.lookup tab1) tycos', |
266 AList.make (the o Symtab.lookup tab2) tycos'); |
328 AList.make (the o Symtab.lookup tab2) tycos')); |
267 in (touched, Symtab.merge (K true) tabs) end; |
329 in (touched, Symtab.merge (K true) tabs) end; |
268 |
330 |
269 datatype spec = Spec of { |
331 datatype spec = Spec of { |
270 funcs: sdthms Consttab.table, |
332 funcs: sdthms Consttab.table, |
271 dconstrs: string Consttab.table, |
333 dconstrs: string Consttab.table, |
299 let |
361 let |
300 val (touched', preproc) = merge_preproc (preproc1, preproc2); |
362 val (touched', preproc) = merge_preproc (preproc1, preproc2); |
301 val (touched_cs, spec) = merge_spec (spec1, spec2); |
363 val (touched_cs, spec) = merge_spec (spec1, spec2); |
302 val touched = if touched' then NONE else touched_cs; |
364 val touched = if touched' then NONE else touched_cs; |
303 in (touched, mk_exec (preproc, spec)) end; |
365 in (touched, mk_exec (preproc, spec)) end; |
304 val empty_exec = mk_exec (mk_preproc ([], []), |
366 val empty_exec = mk_exec (mk_preproc (([], []), ([], [])), |
305 mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty)); |
367 mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty)); |
306 |
368 |
307 fun the_preproc (Exec { preproc = Preproc x, ...}) = x; |
369 fun the_preproc (Exec { preproc = Preproc x, ...}) = x; |
308 fun the_spec (Exec { spec = Spec x, ...}) = x; |
370 fun the_spec (Exec { spec = Spec x, ...}) = x; |
309 val the_funcs = #funcs o the_spec; |
371 val the_funcs = #funcs o the_spec; |
482 val (env, _) = fold unify tys (Vartab.empty, maxidx) |
544 val (env, _) = fold unify tys (Vartab.empty, maxidx) |
483 val instT = Vartab.fold (fn (x_i, (sort, ty)) => |
545 val instT = Vartab.fold (fn (x_i, (sort, ty)) => |
484 cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; |
546 cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; |
485 in map (Thm.instantiate (instT, [])) thms end; |
547 in map (Thm.instantiate (instT, [])) thms end; |
486 |
548 |
487 fun certify_const thy c thms = |
549 fun certify_const thy c c_thms = |
488 let |
550 let |
489 fun cert (c', thm) = if CodegenConsts.eq_const (c, c') |
551 fun cert (c', thm) = if CodegenConsts.eq_const (c, c') |
490 then thm else bad_thm ("Wrong head of function equation,\nexpected constant " |
552 then thm else bad_thm ("Wrong head of function equation,\nexpected constant " |
491 ^ CodegenConsts.string_of_const thy c) thm |
553 ^ CodegenConsts.string_of_const thy c) thm |
492 in (map cert o maps (mk_func thy)) thms end; |
554 in map cert c_thms end; |
493 |
555 |
494 fun mk_cos tyco vs cos = |
556 fun mk_cos tyco vs cos = |
495 let |
557 let |
496 val dty = Type (tyco, map TFree vs); |
558 val dty = Type (tyco, map TFree vs); |
497 fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys); |
559 fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys); |
614 map_dtyps (Symtab.delete tyco) |
676 map_dtyps (Symtab.delete tyco) |
615 #> map_dconstrs (fold Consttab.delete consts) |
677 #> map_dconstrs (fold Consttab.delete consts) |
616 in map_exec_purge (SOME consts) del thy end; |
678 in map_exec_purge (SOME consts) del thy end; |
617 |
679 |
618 fun add_inline thm thy = |
680 fun add_inline thm thy = |
619 map_exec_purge NONE (map_preproc (apfst (fold (insert eq_thm) (mk_rew thy thm)))) thy; |
681 (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (insert eq_thm) (mk_rew thy thm)) thy; |
620 |
682 |
621 fun del_inline thm thy = |
683 fun del_inline thm thy = |
622 map_exec_purge NONE (map_preproc (apfst (fold (remove eq_thm) (mk_rew thy thm)))) thy ; |
684 (map_exec_purge NONE o map_preproc o apfst o apfst) (fold (remove eq_thm) (mk_rew thy thm)) thy ; |
|
685 |
|
686 fun add_inline_proc f = |
|
687 (map_exec_purge NONE o map_preproc o apfst o apsnd) (cons (serial (), f)); |
|
688 |
|
689 fun add_constrains f = |
|
690 (map_exec_purge NONE o map_preproc o apsnd o apfst) (cons (serial (), f)); |
623 |
691 |
624 fun add_preproc f = |
692 fun add_preproc f = |
625 map_exec_purge NONE (map_preproc (apsnd (cons (serial (), f)))); |
693 (map_exec_purge NONE o map_preproc o apsnd o apsnd) (cons (serial (), f)); |
626 |
694 |
627 fun getf_first [] _ = NONE |
695 local |
628 | getf_first (f::fs) x = case f x |
696 |
629 of NONE => getf_first fs x |
697 fun gen_apply_constrain prep post const_typ thy fs x = |
630 | y as SOME x => y; |
698 let |
631 |
699 val ts = prep x; |
632 fun getf_first_list [] x = [] |
700 val tvars = (fold o fold_aterms) Term.add_tvars ts []; |
633 | getf_first_list (f::fs) x = case f x |
701 val consts = (fold o fold_aterms) (fn Const c => cons c | _ => I) ts []; |
634 of [] => getf_first_list fs x |
702 fun insts_of const_typ (c, ty) = |
635 | xs => xs; |
703 let |
|
704 val ty_decl = const_typ (c, ty); |
|
705 val env = Vartab.dest (Type.raw_match (ty_decl, ty) Vartab.empty); |
|
706 val insts = map_filter |
|
707 (fn (v, (sort, TVar (_, sort'))) => |
|
708 if Sorts.sort_le (Sign.classes_of thy) (sort, sort') |
|
709 then NONE else SOME (v, sort) |
|
710 | _ => NONE) env |
|
711 in |
|
712 insts |
|
713 end |
|
714 val const_insts = case const_typ |
|
715 of NONE => [] |
|
716 | SOME const_typ => maps (insts_of const_typ) consts; |
|
717 fun add_inst (v, sort') = |
|
718 let |
|
719 val sort = (the o AList.lookup (op =) tvars) v |
|
720 in |
|
721 AList.map_default (op =) (v, (sort, sort)) |
|
722 (apsnd (fn sort => Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) |
|
723 end; |
|
724 val inst = |
|
725 [] |
|
726 |> fold (fn f => fold add_inst (f thy ts)) fs |
|
727 |> fold add_inst const_insts; |
|
728 in |
|
729 post thy inst x |
|
730 end; |
|
731 |
|
732 val apply_constrain = gen_apply_constrain (maps |
|
733 ((fn (args, rhs) => rhs :: (snd o strip_comb) args) o Logic.dest_equals o Thm.prop_of)) |
|
734 (fn thy => fn inst => map (check_typ_classop thy o Thm.instantiate (map (fn (v, (sort, sort')) => |
|
735 (Thm.ctyp_of thy (TVar (v, sort)), Thm.ctyp_of thy (TVar (v, sort'))) |
|
736 ) inst, []))) NONE; |
|
737 fun apply_constrain_cterm thy const_typ = gen_apply_constrain (single o Thm.term_of) |
|
738 (fn thy => fn inst => pair inst o Thm.cterm_of thy o map_types |
|
739 (TermSubst.instantiateT (map (fn (v, (sort, sort')) => ((v, sort), TVar (v, sort'))) inst)) o Thm.term_of) (SOME const_typ) thy; |
|
740 |
|
741 fun gen_apply_inline_proc prep post thy f x = |
|
742 let |
|
743 val cts = prep x; |
|
744 val rews = map (check_rew thy) (f thy cts); |
|
745 in post rews x end; |
|
746 |
|
747 val apply_inline_proc = gen_apply_inline_proc (maps |
|
748 ((fn [args, rhs] => rhs :: (snd o Drule.strip_comb) args) o snd o Drule.strip_comb o Thm.cprop_of)) |
|
749 (fn rews => map (rewrite_func rews)); |
|
750 val apply_inline_proc_cterm = gen_apply_inline_proc single |
|
751 (Tactic.rewrite false); |
|
752 |
|
753 fun apply_preproc thy f [] = [] |
|
754 | apply_preproc thy f (thms as (thm :: _)) = |
|
755 let |
|
756 val thms' = f thy thms; |
|
757 val c = (CodegenConsts.norm_of_typ thy o fst o dest_func thy) thm; |
|
758 in (certify_const thy c o map (mk_head thy)) thms' end; |
|
759 |
|
760 fun cmp_thms thy = |
|
761 make_ord (fn (thm1, thm2) => not (Sign.typ_instance thy (typ_func thy thm1, typ_func thy thm2))); |
|
762 |
|
763 fun rhs_conv conv thm = |
|
764 let |
|
765 val thm' = (conv o snd o Drule.dest_equals o Thm.cprop_of) thm; |
|
766 in Thm.transitive thm thm' end |
|
767 |
|
768 fun drop_classes thy inst thm = |
|
769 let |
|
770 val unconstr = map (fn (v, (_, sort')) => |
|
771 (Thm.ctyp_of thy o TVar) (v, sort')) inst; |
|
772 val instmap = map (fn (v, (sort, _)) => |
|
773 pairself (Thm.ctyp_of thy o TVar) ((v, []), (v, sort))) inst; |
|
774 in |
|
775 thm |
|
776 |> fold Thm.unconstrainT unconstr |
|
777 |> Thm.instantiate (instmap, []) |
|
778 |> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy)) |
|
779 end; |
|
780 |
|
781 in |
636 |
782 |
637 fun preprocess thy thms = |
783 fun preprocess thy thms = |
638 let |
784 thms |
639 fun cmp_thms (thm1, thm2) = |
785 |> fold (fn (_, f) => apply_preproc thy f) ((#preprocs o the_preproc o get_exec) thy) |
640 not (Sign.typ_instance thy (typ_func thy thm1, typ_func thy thm2)); |
786 |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) |
641 in |
787 |> apply_constrain thy ((map snd o #constrains o the_preproc o get_exec) thy) |
642 thms |
788 |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) |
643 |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) |
789 |> fold (fn (_, f) => apply_inline_proc thy f) ((#inline_procs o the_preproc o get_exec) thy) |
644 |> fold (fn (_, f) => f thy) ((#preprocs o the_preproc o get_exec) thy) |
790 |> map (snd o check_func false thy) |
645 |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) |
791 |> sort (cmp_thms thy) |
646 |> sort (make_ord cmp_thms) |
792 |> common_typ_funcs thy; |
647 |> common_typ_funcs thy |
793 |
648 end; |
794 fun preprocess_cterm thy const_typ ct = |
649 |
795 ct |
650 fun preprocess_cterm thy = |
796 |> apply_constrain_cterm thy const_typ ((map snd o #constrains o the_preproc o get_exec) thy) |
651 Tactic.rewrite false ((#inlines o the_preproc o get_exec) thy); |
797 |-> (fn inst => |
|
798 Thm.reflexive |
|
799 #> fold (rhs_conv o Tactic.rewrite false o single) ((#inlines o the_preproc o get_exec) thy) |
|
800 #> fold (fn (_, f) => rhs_conv (apply_inline_proc_cterm thy f)) ((#inline_procs o the_preproc o get_exec) thy) |
|
801 #> (fn thm => (drop_classes thy inst thm, ((fn xs => nth xs 1) o snd o Drule.strip_comb o Thm.cprop_of) thm)) |
|
802 ); |
|
803 |
|
804 end; (*local*) |
652 |
805 |
653 fun these_funcs thy c = |
806 fun these_funcs thy c = |
654 let |
807 let |
655 fun test_funcs c = |
808 val funcs_1 = |
656 Consttab.lookup ((the_funcs o get_exec) thy) c |
809 Consttab.lookup ((the_funcs o get_exec) thy) c |
657 |> Option.map (Susp.force o fst) |
810 |> Option.map (Susp.force o fst) |
658 |> these |
811 |> these |
659 |> map (Thm.transfer thy); |
812 |> map (Thm.transfer thy); |
660 val test_defs = get_prim_def_funcs thy; |
813 val funcs_2 = case funcs_1 |
|
814 of [] => get_prim_def_funcs thy c |
|
815 | xs => xs; |
661 fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals |
816 fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals |
662 o ObjectLogic.drop_judgment thy o Drule.plain_prop_of); |
817 o ObjectLogic.drop_judgment thy o Drule.plain_prop_of); |
663 in |
818 in |
664 getf_first_list [test_funcs, test_defs] c |
819 funcs_2 |
665 |> preprocess thy |
820 |> preprocess thy |
666 |> drop_refl thy |
821 |> drop_refl thy |
667 end; |
822 end; |
668 |
823 |
669 fun get_datatype thy tyco = |
824 fun get_datatype thy tyco = |