23 val sortargs: code_graph -> string -> sort list |
23 val sortargs: code_graph -> string -> sort list |
24 val all: code_graph -> string list |
24 val all: code_graph -> string list |
25 val pretty: theory -> code_graph -> Pretty.T |
25 val pretty: theory -> code_graph -> Pretty.T |
26 val obtain: theory -> string list -> term list -> code_algebra * code_graph |
26 val obtain: theory -> string list -> term list -> code_algebra * code_graph |
27 val dynamic_eval_conv: theory |
27 val dynamic_eval_conv: theory |
28 -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm |
28 -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv |
29 val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) |
29 val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a) |
30 -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a |
30 -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a |
31 val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm |
31 val static_eval_conv: theory -> string list |
|
32 -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv |
|
33 val pre_post_conv: theory -> conv -> conv |
32 |
34 |
33 val setup: theory -> theory |
35 val setup: theory -> theory |
34 end |
36 end |
35 |
37 |
36 structure Code_Preproc : CODE_PREPROC = |
38 structure Code_Preproc : CODE_PREPROC = |
419 ); |
421 ); |
420 |
422 |
421 |
423 |
422 (** retrieval and evaluation interfaces **) |
424 (** retrieval and evaluation interfaces **) |
423 |
425 |
424 fun obtain thy cs ts = apsnd snd |
426 fun obtain thy consts ts = apsnd snd |
425 (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts)); |
427 (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts)); |
|
428 |
|
429 fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end; |
426 |
430 |
427 fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct = |
431 fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct = |
428 let |
432 let |
429 val pp = Syntax.pp_global thy; |
433 val pp = Syntax.pp_global thy; |
430 val ct = cterm_of proto_ct; |
434 val ct = cterm_of proto_ct; |
431 val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) |
435 val _ = (Sign.no_frees pp o map_types (K dummyT) o Sign.no_vars pp) |
432 (Thm.term_of ct); |
436 (Thm.term_of ct); |
433 val thm = preprocess_conv thy ct; |
437 val thm = preprocess_conv thy ct; |
434 val ct' = Thm.rhs_of thm; |
438 val ct' = Thm.rhs_of thm; |
435 val t' = Thm.term_of ct'; |
439 val (vs', t') = dest_cterm ct'; |
436 val vs = Term.add_tfrees t' []; |
|
437 val consts = fold_aterms |
440 val consts = fold_aterms |
438 (fn Const (c, _) => insert (op =) c | _ => I) t' []; |
441 (fn Const (c, _) => insert (op =) c | _ => I) t' []; |
439 val (algebra', eqngr') = obtain thy consts [t']; |
442 val (algebra', eqngr') = obtain thy consts [t']; |
440 in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end; |
443 in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end; |
441 |
444 |
442 fun dynamic_eval_conv thy = |
445 fun dynamic_eval_conv thy = |
443 let |
446 let |
444 fun conclude_evaluation thm2 thm1 = |
447 fun conclude_evaluation thm2 thm1 = |
445 let |
448 let |
454 fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy) |
457 fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy) |
455 (K o postproc (postprocess_term thy)) (K oooo evaluator); |
458 (K o postproc (postprocess_term thy)) (K oooo evaluator); |
456 |
459 |
457 fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy); |
460 fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy); |
458 |
461 |
|
462 fun static_eval_conv thy consts conv = |
|
463 let |
|
464 val (algebra, eqngr) = obtain thy consts []; |
|
465 fun conv' ct = |
|
466 let |
|
467 val (vs, t) = dest_cterm ct; |
|
468 in Conv.tap_thy (fn thy => pre_post_conv thy (conv algebra eqngr vs t)) ct end; |
|
469 in conv' end; |
|
470 |
459 |
471 |
460 (** setup **) |
472 (** setup **) |
461 |
473 |
462 val setup = |
474 val setup = |
463 let |
475 let |