1.1 --- a/src/Tools/code/code_package.ML	Fri Jan 25 14:54:48 2008 +0100
     1.2 +++ b/src/Tools/code/code_package.ML	Fri Jan 25 14:54:49 2008 +0100
     1.3 @@ -84,17 +84,9 @@
     1.4     of SOME (c, trns) => (SOME c, trns)
     1.5      | NONE => (NONE, trns);
     1.6  
     1.7 -fun generate thy funcgr gen it =
     1.8 -  let
     1.9 -    val naming = NameSpace.qualified_names NameSpace.default_naming;
    1.10 -    val consttab = Consts.empty
    1.11 -      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
    1.12 -           (CodeFuncgr.all funcgr);
    1.13 -    val algbr = (Code.operational_algebra thy, consttab);
    1.14 -  in   
    1.15 -    Program.change_yield thy
    1.16 -      (CodeThingol.transact (gen thy algbr funcgr it))
    1.17 -  end;
    1.18 +fun generate thy funcgr f x =
    1.19 +  Program.change_yield thy (CodeThingol.transact thy funcgr
    1.20 +    (fn thy => fn funcgr => fn algbr => f thy funcgr algbr x));
    1.21  
    1.22  fun code thy permissive cs seris =
    1.23    let

     2.1 --- a/src/Tools/code/code_target.ML	Fri Jan 25 14:54:48 2008 +0100
     2.2 +++ b/src/Tools/code/code_target.ML	Fri Jan 25 14:54:49 2008 +0100
     2.3 @@ -243,12 +243,12 @@
     2.4      fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
     2.5            else if c = c_min then
     2.6              if negative then SOME ~1 else NONE
     2.7 -          else error "Illegal numeral expression"
     2.8 +          else error "Illegal numeral expression: illegal leading digit"
     2.9        | dest_numeral (IConst (c, _) `$ t1 `$ t2) =
    2.10            if c = c_bit then let val (n, b) = (dest_numeral t1, dest_bit t2)
    2.11              in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    2.12 -          else error "Illegal numeral expression"
    2.13 -      | dest_numeral _ = error "Illegal numeral expression";
    2.14 +          else error "Illegal numeral expression: illegal bit shift operator"
    2.15 +      | dest_numeral _ = error "Illegal numeral expression: illegal constant";
    2.16    in dest_numeral #> the_default 0 end;
    2.17  
    2.18  fun implode_monad c_bind t =

     3.1 --- a/src/Tools/code/code_thingol.ML	Fri Jan 25 14:54:48 2008 +0100
     3.2 +++ b/src/Tools/code/code_thingol.ML	Fri Jan 25 14:54:49 2008 +0100
     3.3 @@ -87,7 +87,9 @@
     3.4    val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
     3.5      -> CodeFuncgr.T -> term -> transact -> string * transact;
     3.6    val add_value_stmt: iterm * itype -> code -> code;
     3.7 -  val transact: (transact -> 'a * transact) -> code -> 'a * code;
     3.8 +  val transact: theory -> CodeFuncgr.T
     3.9 +    -> (theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodeFuncgr.T
    3.10 +      -> transact -> 'a * transact) -> code -> 'a * code;
    3.11  end;
    3.12  
    3.13  structure CodeThingol: CODE_THINGOL =
    3.14 @@ -357,10 +359,18 @@
    3.15      |> pair name
    3.16    end;
    3.17  
    3.18 -fun transact f code =
    3.19 -  (NONE, code)
    3.20 -  |> f
    3.21 -  |-> (fn x => fn (_, code) => (x, code));
    3.22 +fun transact thy funcgr f code =
    3.23 +  let
    3.24 +    val naming = NameSpace.qualified_names NameSpace.default_naming;
    3.25 +    val consttab = Consts.empty
    3.26 +      |> fold (fn c => Consts.declare true naming [] (c, CodeFuncgr.typ funcgr c))
    3.27 +           (CodeFuncgr.all funcgr);
    3.28 +    val algbr = (Code.operational_algebra thy, consttab);
    3.29 +  in
    3.30 +    (NONE, code)
    3.31 +    |> f thy algbr funcgr
    3.32 +    |-> (fn x => fn (_, code) => (x, code))
    3.33 +  end;
    3.34  
    3.35  
    3.36  (* translation kernel *)
    3.37 @@ -614,6 +624,14 @@
    3.38        end
    3.39    | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
    3.40  
    3.41 +
    3.42 +(** evaluation **)
    3.43 +
    3.44 +fun add_value_stmt (t, ty) code =
    3.45 +  code
    3.46 +  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
    3.47 +  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
    3.48 +
    3.49  fun ensure_value thy algbr funcgr t = 
    3.50    let
    3.51      val ty = fastype_of t;
    3.52 @@ -628,10 +646,37 @@
    3.53      ensure_stmt stmt_value CodeName.value_name
    3.54    end;
    3.55  
    3.56 -fun add_value_stmt (t, ty) code =
    3.57 -  code
    3.58 -  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
    3.59 -  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
    3.60 +fun eval evaluate term_of thy g code0 =
    3.61 +  let
    3.62 +    fun result (_, code) =
    3.63 +      let
    3.64 +        val Fun ((vs, ty), [(([], t), _)]) =
    3.65 +          Graph.get_node code CodeName.value_name;
    3.66 +        val deps = Graph.imm_succs code CodeName.value_name;
    3.67 +        val code' = Graph.del_nodes [CodeName.value_name] code;
    3.68 +        val code'' = project_code false [] (SOME deps) code';
    3.69 +      in ((code'', ((vs, ty), t), deps), code') end;
    3.70 +    fun h funcgr ct =
    3.71 +      let
    3.72 +        val ((code, vs_ty_t, deps), _) =
    3.73 +          code0
    3.74 +          |> transact thy funcgr (fn thy => fn algbr => fn funcgr =>
    3.75 +               ensure_value thy algbr funcgr (term_of ct))
    3.76 +          |> result
    3.77 +          ||> `(fn code' => code');
    3.78 +      in g code vs_ty_t deps ct end;
    3.79 +  in evaluate thy h end;
    3.80 +
    3.81 +val _ : (theory -> (CodeFuncgr.T -> 'Z -> 'Y) -> 'X)
    3.82 +                  -> ('Z -> term)
    3.83 +                     -> theory
    3.84 +                        -> (stmt Graph.T
    3.85 +                            -> ((vname * sort) list * itype) * iterm
    3.86 +                               -> Graph.key list -> 'Z -> 'Y)
    3.87 +                           -> stmt Graph.T -> 'X = eval;
    3.88 +
    3.89 +fun eval_conv thy = eval CodeFuncgr.eval_conv Thm.term_of thy;
    3.90 +fun eval_term thy = eval CodeFuncgr.eval_term I thy;
    3.91  
    3.92  end; (*struct*)
    3.93