1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:51:32 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:51:32 2010 +0200
     1.3 @@ -93,11 +93,16 @@
     1.4    val read_const_exprs: theory -> string list -> string list * string list
     1.5    val consts_program: theory -> bool -> string list -> string list * (naming * program)
     1.6    val dynamic_eval_conv: theory
     1.7 -    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     1.8 -    -> cterm -> thm
     1.9 +    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    1.10 +    -> conv
    1.11    val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
    1.12      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    1.13      -> term -> 'a
    1.14 +  val static_eval_conv: theory -> string list
    1.15 +    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    1.16 +    -> conv
    1.17 +  val static_eval_conv_simple: theory -> string list
    1.18 +    -> (program -> conv) -> conv
    1.19  end;
    1.20  
    1.21  structure Code_Thingol: CODE_THINGOL =
    1.22 @@ -846,7 +851,7 @@
    1.23  
    1.24  fun consts_program thy permissive cs =
    1.25    let
    1.26 -    fun project_consts cs (naming, program) =
    1.27 +    fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*)
    1.28        let
    1.29          val cs_all = Graph.all_succs program cs;
    1.30        in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
    1.31 @@ -898,6 +903,15 @@
    1.32  fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
    1.33  fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
    1.34  
    1.35 +fun static_eval_conv thy consts conv =
    1.36 +  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
    1.37 +
    1.38 +fun static_eval_conv_simple thy consts conv =
    1.39 +  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
    1.40 +    conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
    1.41 +      |> fold_map (ensure_const thy algebra eqngr false) consts
    1.42 +      |> (snd o snd o snd)) ct);
    1.43 +
    1.44  
    1.45  (** diagnostic commands **)
    1.46