1.1 --- a/src/Tools/code/code_thingol.ML	Tue Jan 29 10:19:58 2008 +0100
     1.2 +++ b/src/Tools/code/code_thingol.ML	Tue Jan 29 10:20:00 2008 +0100
     1.3 @@ -85,11 +85,12 @@
     1.4    val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     1.5      -> CodeFuncgr.T -> string -> transact -> string * transact;
     1.6    val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     1.7 -    -> CodeFuncgr.T -> term -> transact -> string * transact;
     1.8 -  val add_value_stmt: iterm * itype -> code -> code;
     1.9 +    -> CodeFuncgr.T -> term
    1.10 +      -> transact -> (code * ((typscheme * iterm) * string list)) * transact;
    1.11    val transact: theory -> CodeFuncgr.T
    1.12      -> (theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodeFuncgr.T
    1.13        -> transact -> 'a * transact) -> code -> 'a * code;
    1.14 +  val add_value_stmt: iterm * itype -> code -> code;
    1.15  end;
    1.16  
    1.17  structure CodeThingol: CODE_THINGOL =
    1.18 @@ -642,42 +643,20 @@
    1.19        ##>> exprgen_typ thy algbr funcgr ty
    1.20        ##>> exprgen_term thy algbr funcgr t
    1.21        #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
    1.22 +    fun term_value (dep, code1) =
    1.23 +      let
    1.24 +        val Fun ((vs, ty), [(([], t), _)]) =
    1.25 +          Graph.get_node code1 CodeName.value_name;
    1.26 +        val deps = Graph.imm_succs code1 CodeName.value_name;
    1.27 +        val code2 = Graph.del_nodes [CodeName.value_name] code1;
    1.28 +        val code3 = project_code false [] (SOME deps) code2;
    1.29 +      in ((code3, (((vs, ty), t), deps)), (dep, code2)) end;
    1.30    in
    1.31      ensure_stmt stmt_value CodeName.value_name
    1.32 +    #> snd
    1.33 +    #> term_value
    1.34    end;
    1.35  
    1.36 -fun eval evaluate term_of thy g code0 =
    1.37 -  let
    1.38 -    fun result (_, code) =
    1.39 -      let
    1.40 -        val Fun ((vs, ty), [(([], t), _)]) =
    1.41 -          Graph.get_node code CodeName.value_name;
    1.42 -        val deps = Graph.imm_succs code CodeName.value_name;
    1.43 -        val code' = Graph.del_nodes [CodeName.value_name] code;
    1.44 -        val code'' = project_code false [] (SOME deps) code';
    1.45 -      in ((code'', ((vs, ty), t), deps), code') end;
    1.46 -    fun h funcgr ct =
    1.47 -      let
    1.48 -        val ((code, vs_ty_t, deps), _) =
    1.49 -          code0
    1.50 -          |> transact thy funcgr (fn thy => fn algbr => fn funcgr =>
    1.51 -               ensure_value thy algbr funcgr (term_of ct))
    1.52 -          |> result
    1.53 -          ||> `(fn code' => code');
    1.54 -      in g code vs_ty_t deps ct end;
    1.55 -  in evaluate thy h end;
    1.56 -
    1.57 -val _ : (theory -> (CodeFuncgr.T -> 'Z -> 'Y) -> 'X)
    1.58 -                  -> ('Z -> term)
    1.59 -                     -> theory
    1.60 -                        -> (stmt Graph.T
    1.61 -                            -> ((vname * sort) list * itype) * iterm
    1.62 -                               -> Graph.key list -> 'Z -> 'Y)
    1.63 -                           -> stmt Graph.T -> 'X = eval;
    1.64 -
    1.65 -fun eval_conv thy = eval CodeFuncgr.eval_conv Thm.term_of thy;
    1.66 -fun eval_term thy = eval CodeFuncgr.eval_term I thy;
    1.67 -
    1.68  end; (*struct*)
    1.69  
    1.70