534 in of_univ 0 t 0 |> fst end; |
534 in of_univ 0 t 0 |> fst end; |
535 |
535 |
536 |
536 |
537 (* evaluation with type reconstruction *) |
537 (* evaluation with type reconstruction *) |
538 |
538 |
539 fun eval_term raw_ctxt (nbe_program, idx_tab) t_original ((vs, ty), t) deps = |
539 fun eval_term (nbe_program, idx_tab) raw_ctxt t_original ((vs, ty), t) deps = |
540 let |
540 let |
541 val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); |
541 val ctxt = Syntax.init_pretty_global (Proof_Context.theory_of raw_ctxt); |
542 val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); |
542 val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt); |
543 fun type_infer t' = |
543 fun type_infer t' = |
544 Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) |
544 Syntax.check_term (Config.put Type_Infer_Context.const_sorts false ctxt) |
583 val rhs = Thm.cterm_of thy raw_rhs; |
583 val rhs = Thm.cterm_of thy raw_rhs; |
584 in Thm.mk_binop eq lhs rhs end; |
584 in Thm.mk_binop eq lhs rhs end; |
585 |
585 |
586 val (_, raw_oracle) = Context.>>> (Context.map_theory_result |
586 val (_, raw_oracle) = Context.>>> (Context.map_theory_result |
587 (Thm.add_oracle (@{binding normalization_by_evaluation}, |
587 (Thm.add_oracle (@{binding normalization_by_evaluation}, |
588 fn (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct) => |
588 fn (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct) => |
589 mk_equals ctxt ct (eval_term ctxt nbe_program_idx_tab (term_of ct) vs_ty_t deps)))); |
589 mk_equals ctxt ct (eval_term nbe_program_idx_tab ctxt (term_of ct) vs_ty_t deps)))); |
590 |
590 |
591 fun oracle ctxt nbe_program_idx_tab vs_ty_t deps ct = |
591 fun oracle nbe_program_idx_tab ctxt vs_ty_t deps ct = |
592 raw_oracle (ctxt, nbe_program_idx_tab, vs_ty_t, deps, ct); |
592 raw_oracle (nbe_program_idx_tab, ctxt, vs_ty_t, deps, ct); |
593 |
593 |
594 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt |
594 fun dynamic_conv ctxt = lift_triv_classes_conv ctxt |
595 (Code_Thingol.dynamic_conv ctxt (oracle ctxt o compile false ctxt)); |
595 (Code_Thingol.dynamic_conv ctxt (fn program => oracle (compile false ctxt program) ctxt)); |
596 |
596 |
597 fun dynamic_value ctxt = lift_triv_classes_rew ctxt |
597 fun dynamic_value ctxt = lift_triv_classes_rew ctxt |
598 (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt)); |
598 (Code_Thingol.dynamic_value ctxt I (fn program => eval_term (compile false ctxt program) ctxt)); |
599 |
599 |
600 fun static_conv (ctxt_consts as { ctxt, ... }) = |
600 fun static_conv (ctxt_consts as { ctxt, ... }) = |
601 let |
601 let |
602 val evaluator = Code_Thingol.static_conv ctxt_consts |
602 val evaluator = Code_Thingol.static_conv ctxt_consts |
603 (fn { program, ... } => fn ctxt' => oracle ctxt' (compile true ctxt program)); |
603 (fn { program, ... } => oracle (compile true ctxt program)); |
604 in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end; |
604 in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end; |
605 |
605 |
606 fun static_value { ctxt, consts } = |
606 fun static_value { ctxt, consts } = |
607 let |
607 let |
608 val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts } |
608 val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts } |
609 (fn { program, ... } => fn ctxt' => eval_term ctxt' (compile false ctxt program)); |
609 (fn { program, ... } => eval_term (compile false ctxt program)); |
610 in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end; |
610 in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end; |
611 |
611 |
612 end; |
612 end; |