21 val eqns: code_graph -> string -> (thm * bool) list |
21 val eqns: code_graph -> string -> (thm * bool) list |
22 val typ: code_graph -> string -> (string * sort) list * typ |
22 val typ: code_graph -> string -> (string * sort) list * typ |
23 val all: code_graph -> string list |
23 val all: code_graph -> string list |
24 val pretty: theory -> code_graph -> Pretty.T |
24 val pretty: theory -> code_graph -> Pretty.T |
25 val obtain: theory -> string list -> term list -> code_algebra * code_graph |
25 val obtain: theory -> string list -> term list -> code_algebra * code_graph |
26 val resubst_triv_consts: theory -> term -> term |
|
27 val eval_conv: theory |
26 val eval_conv: theory |
28 -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm |
27 -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm |
29 val eval: theory -> ((term -> term) -> 'a -> 'a) |
28 val eval: theory -> ((term -> term) -> 'a -> 'a) |
30 -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a |
29 -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a |
31 |
30 |
71 |
70 |
72 fun delete_force msg key xs = |
71 fun delete_force msg key xs = |
73 if AList.defined (op =) xs key then AList.delete (op =) key xs |
72 if AList.defined (op =) xs key then AList.delete (op =) key xs |
74 else error ("No such " ^ msg ^ ": " ^ quote key); |
73 else error ("No such " ^ msg ^ ": " ^ quote key); |
75 |
74 |
76 fun map_data f thy = |
75 fun map_data f = Code.purge_data |
77 thy |
76 #> (Code_Preproc_Data.map o map_thmproc) f; |
78 |> Code.purge_data |
|
79 |> (Code_Preproc_Data.map o map_thmproc) f; |
|
80 |
77 |
81 val map_pre_post = map_data o apfst; |
78 val map_pre_post = map_data o apfst; |
82 val map_pre = map_pre_post o apfst; |
79 val map_pre = map_pre_post o apfst; |
83 val map_post = map_pre_post o apsnd; |
80 val map_post = map_pre_post o apsnd; |
84 |
81 |
161 ct |
158 ct |
162 |> AxClass.overload_conv thy |
159 |> AxClass.overload_conv thy |
163 |> rhs_conv (Simplifier.rewrite post) |
160 |> rhs_conv (Simplifier.rewrite post) |
164 end; |
161 end; |
165 |
162 |
166 fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty) |
163 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); |
167 | t => t); |
|
168 |
|
169 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy; |
|
170 |
164 |
171 fun print_codeproc thy = |
165 fun print_codeproc thy = |
172 let |
166 let |
173 val ctxt = ProofContext.init thy; |
167 val ctxt = ProofContext.init thy; |
174 val pre = (#pre o the_thmproc) thy; |
168 val pre = (#pre o the_thmproc) thy; |
487 (** retrieval and evaluation interfaces **) |
481 (** retrieval and evaluation interfaces **) |
488 |
482 |
489 fun obtain thy cs ts = apsnd snd |
483 fun obtain thy cs ts = apsnd snd |
490 (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); |
484 (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); |
491 |
485 |
492 fun prepare_sorts_typ prep_sort |
|
493 = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort)); |
|
494 |
|
495 fun prepare_sorts prep_sort (Const (c, ty)) = |
|
496 Const (c, prepare_sorts_typ prep_sort ty) |
|
497 | prepare_sorts prep_sort (t1 $ t2) = |
|
498 prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2 |
|
499 | prepare_sorts prep_sort (Abs (v, ty, t)) = |
|
500 Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t) |
|
501 | prepare_sorts _ (t as Bound _) = t; |
|
502 |
|
503 fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = |
486 fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct = |
504 let |
487 let |
505 val pp = Syntax.pp_global thy; |
488 val pp = Syntax.pp_global thy; |
506 val ct = cterm_of proto_ct; |
489 val ct = cterm_of proto_ct; |
507 val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) |
490 val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) |
510 val ct' = Thm.rhs_of thm; |
493 val ct' = Thm.rhs_of thm; |
511 val t' = Thm.term_of ct'; |
494 val t' = Thm.term_of ct'; |
512 val vs = Term.add_tfrees t' []; |
495 val vs = Term.add_tfrees t' []; |
513 val consts = fold_aterms |
496 val consts = fold_aterms |
514 (fn Const (c, _) => insert (op =) c | _ => I) t' []; |
497 (fn Const (c, _) => insert (op =) c | _ => I) t' []; |
515 |
498 val (algebra', eqngr') = obtain thy consts [t']; |
516 val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy)) |
499 in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end; |
517 (Code.triv_classes thy); |
|
518 val t'' = prepare_sorts add_triv_classes t'; |
|
519 val (algebra', eqngr') = obtain thy consts [t'']; |
|
520 in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end; |
|
521 |
500 |
522 fun simple_evaluator evaluator algebra eqngr vs t ct = |
501 fun simple_evaluator evaluator algebra eqngr vs t ct = |
523 evaluator algebra eqngr vs t; |
502 evaluator algebra eqngr vs t; |
524 |
503 |
525 fun eval_conv thy = |
504 fun eval_conv thy = |