equal
deleted
inserted
replaced
603 (Code_Thingol.dynamic_value thy I |
603 (Code_Thingol.dynamic_value thy I |
604 (K (fn program => eval_term thy program (compile false thy program)))); |
604 (K (fn program => eval_term thy program (compile false thy program)))); |
605 |
605 |
606 fun static_conv thy consts = |
606 fun static_conv thy consts = |
607 lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts |
607 lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts |
608 (K (fn program => fn _ => let val nbe_program = compile true thy program |
608 (K (fn program => fn _ => oracle thy program (compile true thy program)))); |
609 in oracle thy program nbe_program end))); |
|
610 |
609 |
611 fun static_value thy consts = lift_triv_classes_rew thy |
610 fun static_value thy consts = lift_triv_classes_rew thy |
612 (Code_Thingol.static_value thy I consts |
611 (Code_Thingol.static_value thy I consts |
613 (K (fn program => fn _ => let val nbe_program = compile true thy program |
612 (K (fn program => fn _ => eval_term thy program (compile true thy program)))); |
614 in eval_term thy program (compile false thy program) end))); |
|
615 |
613 |
616 |
614 |
617 (** setup **) |
615 (** setup **) |
618 |
616 |
619 val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of); |
617 val setup = Value.add_evaluator ("nbe", dynamic_value o Proof_Context.theory_of); |