# HG changeset patch # User haftmann # Date 1292940955 -3600 # Node ID 54dfe5c584e8e068900b1bf46d4a486caef12298 # Parent aaf5968c67efda6bfc5e8179a72da27a09d86524 proper static closures diff -r aaf5968c67ef -r 54dfe5c584e8 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Tue Dec 21 15:15:55 2010 +0100 +++ b/src/Tools/Code/code_thingol.ML Tue Dec 21 15:15:55 2010 +0100 @@ -912,31 +912,37 @@ fun dynamic_value thy postproc evaluator = Code_Preproc.dynamic_value thy postproc (dynamic_evaluator thy evaluator); -fun provide_program thy consts f algebra eqngr = - let - fun generate_consts thy algebra eqngr = - fold_map (ensure_const thy algebra eqngr false); - val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr) - generate_consts consts; - in f algebra eqngr naming program consts' end; - -fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t = +fun lift_evaluation thy evaluation' algebra eqngr naming program vs t = let val (((_, program'), (((vs', ty'), t'), deps)), _) = ensure_value thy algebra eqngr t (NONE, (naming, program)); - in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end; + in evaluation' ((original_sorts vs vs', (vs', ty')), t') deps end; + +fun lift_evaluator thy evaluator' consts algebra eqngr = + let + fun generate_consts thy algebra eqngr = + fold_map (ensure_const thy algebra eqngr false); + val (consts', (naming, program)) = + invoke_generation true thy (algebra, eqngr) generate_consts consts; + val evaluation' = evaluator' naming program consts'; + in lift_evaluation thy evaluation' algebra eqngr naming program end; + +fun lift_evaluator_simple thy evaluator' consts algebra eqngr = + let + fun generate_consts thy algebra eqngr = + fold_map (ensure_const thy algebra eqngr false); + val (consts', (naming, program)) = + invoke_generation true thy (algebra, eqngr) generate_consts consts; + in evaluator' program end; fun static_conv thy consts conv = - Code_Preproc.static_conv thy consts - (provide_program thy consts (static_evaluation thy conv)); + Code_Preproc.static_conv thy consts (lift_evaluator thy conv consts); fun static_conv_simple thy consts conv = - Code_Preproc.static_conv thy consts - (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program)); + Code_Preproc.static_conv thy consts (lift_evaluator_simple thy conv consts); fun static_value thy postproc consts evaluator = - Code_Preproc.static_value thy postproc consts - (provide_program thy consts (static_evaluation thy evaluator)); + Code_Preproc.static_value thy postproc consts (lift_evaluator thy evaluator consts); (** diagnostic commands **)