tuned
authorhaftmann
Wed Aug 15 08:57:42 2007 +0200 (2007-08-15)
changeset 242838ca96f4e49cd
parent 24282 9b64aa297524
child 24284 f5afd33f5d02
tuned
src/Pure/Isar/code.ML
src/Tools/code/code_funcgr.ML
src/Tools/code/code_package.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Pure/Isar/code.ML	Wed Aug 15 08:57:41 2007 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Aug 15 08:57:42 2007 +0200
     1.3 @@ -638,10 +638,8 @@
     1.4          | NONE => check_typ_fun (const, thm);
     1.5    in check_typ (fst (CodeUnit.head_func thm), thm) end;
     1.6  
     1.7 -val mk_func = CodeUnit.error_thm
     1.8 -  (assert_func_typ o CodeUnit.mk_func);
     1.9 -val mk_func_liberal = CodeUnit.warning_thm
    1.10 -  (assert_func_typ o CodeUnit.mk_func);
    1.11 +val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
    1.12 +val mk_func_liberal = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
    1.13  
    1.14  end;
    1.15  
     2.1 --- a/src/Tools/code/code_funcgr.ML	Wed Aug 15 08:57:41 2007 +0200
     2.2 +++ b/src/Tools/code/code_funcgr.ML	Wed Aug 15 08:57:42 2007 +0200
     2.3 @@ -12,25 +12,18 @@
     2.4    val timing: bool ref
     2.5    val funcs: T -> CodeUnit.const -> thm list
     2.6    val typ: T -> CodeUnit.const -> typ
     2.7 -  val deps: T -> CodeUnit.const list -> CodeUnit.const list list
     2.8    val all: T -> CodeUnit.const list
     2.9    val pretty: theory -> T -> Pretty.T
    2.10 +  val make: theory -> CodeUnit.const list -> T
    2.11 +  val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
    2.12 +  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
    2.13 +  val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
    2.14 +  val intervene: theory -> T -> T
    2.15 +    (*FIXME drop intervene as soon as possible*)
    2.16    structure Constgraph : GRAPH
    2.17  end
    2.18  
    2.19 -signature CODE_FUNCGR_RETRIEVAL =
    2.20 -sig
    2.21 -  type T (* = CODE_FUNCGR.T *)
    2.22 -  val make: theory -> CodeUnit.const list -> T
    2.23 -  val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
    2.24 -  val make_term: theory -> (T -> (thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
    2.25 -    (*FIXME drop make_term as soon as possible*)
    2.26 -  val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
    2.27 -  val intervene: theory -> T -> T
    2.28 -    (*FIXME drop intervene as soon as possible*)
    2.29 -end;
    2.30 -
    2.31 -structure CodeFuncgr = (*signature is added later*)
    2.32 +structure CodeFuncgr : CODE_FUNCGR =
    2.33  struct
    2.34  
    2.35  (** the graph type **)
    2.36 @@ -48,15 +41,6 @@
    2.37  fun typ funcgr =
    2.38    fst o Constgraph.get_node funcgr;
    2.39  
    2.40 -fun deps funcgr cs =
    2.41 -  let
    2.42 -    val conn = Constgraph.strong_conn funcgr;
    2.43 -    val order = rev conn;
    2.44 -  in
    2.45 -    (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order
    2.46 -    |> filter_out null
    2.47 -  end;
    2.48 -
    2.49  fun all funcgr = Constgraph.keys funcgr;
    2.50  
    2.51  fun pretty thy funcgr =
    2.52 @@ -208,7 +192,7 @@
    2.53      |> instances_of thy algebra
    2.54    end;
    2.55  
    2.56 -fun ensure_const' rewrites thy algebra funcgr const auxgr =
    2.57 +fun ensure_const' thy algebra funcgr const auxgr =
    2.58    if can (Constgraph.get_node funcgr) const
    2.59      then (NONE, auxgr)
    2.60    else if can (Constgraph.get_node auxgr) const
    2.61 @@ -219,26 +203,25 @@
    2.62      |> pair (SOME const)
    2.63    else let
    2.64      val thms = Code.these_funcs thy const
    2.65 -      |> map (CodeUnit.rewrite_func (rewrites thy))
    2.66        |> CodeUnit.norm_args
    2.67        |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var;
    2.68      val rhs = consts_of (const, thms);
    2.69    in
    2.70      auxgr
    2.71      |> Constgraph.new_node (const, thms)
    2.72 -    |> fold_map (ensure_const rewrites thy algebra funcgr) rhs
    2.73 +    |> fold_map (ensure_const thy algebra funcgr) rhs
    2.74      |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
    2.75                             | NONE => I) rhs')
    2.76      |> pair (SOME const)
    2.77    end
    2.78 -and ensure_const rewrites thy algebra funcgr const =
    2.79 +and ensure_const thy algebra funcgr const =
    2.80    let
    2.81      val timeap = if !timing
    2.82        then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const)
    2.83        else I;
    2.84 -  in timeap (ensure_const' rewrites thy algebra funcgr const) end;
    2.85 +  in timeap (ensure_const' thy algebra funcgr const) end;
    2.86  
    2.87 -fun merge_funcss rewrites thy algebra raw_funcss funcgr =
    2.88 +fun merge_funcss thy algebra raw_funcss funcgr =
    2.89    let
    2.90      val funcss = raw_funcss
    2.91        |> resort_funcss thy algebra funcgr
    2.92 @@ -267,7 +250,7 @@
    2.93            (fold_consts (insert (op =)) thms []);
    2.94        in
    2.95          funcgr
    2.96 -        |> ensure_consts' rewrites thy algebra insts
    2.97 +        |> ensure_consts' thy algebra insts
    2.98          |> fold (curry Constgraph.add_edge const) deps
    2.99          |> fold (curry Constgraph.add_edge const) insts
   2.100         end;
   2.101 @@ -276,22 +259,22 @@
   2.102      |> fold add_funcs funcss
   2.103      |> fold add_deps funcss
   2.104    end
   2.105 -and ensure_consts' rewrites thy algebra cs funcgr =
   2.106 +and ensure_consts' thy algebra cs funcgr =
   2.107    let
   2.108      val auxgr = Constgraph.empty
   2.109 -      |> fold (snd oo ensure_const rewrites thy algebra funcgr) cs;
   2.110 +      |> fold (snd oo ensure_const thy algebra funcgr) cs;
   2.111    in
   2.112      funcgr
   2.113 -    |> fold (merge_funcss rewrites thy algebra)
   2.114 +    |> fold (merge_funcss thy algebra)
   2.115           (map (AList.make (Constgraph.get_node auxgr))
   2.116           (rev (Constgraph.strong_conn auxgr)))
   2.117    end handle INVALID (cs', msg)
   2.118      => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg);
   2.119  
   2.120 -fun ensure_consts rewrites thy consts funcgr =
   2.121 +fun ensure_consts thy consts funcgr =
   2.122    let
   2.123      val algebra = Code.coregular_algebra thy
   2.124 -  in ensure_consts' rewrites thy algebra consts funcgr
   2.125 +  in ensure_consts' thy algebra consts funcgr
   2.126      handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
   2.127      ^ commas (map (CodeUnit.string_of_const thy) cs'))
   2.128    end;
   2.129 @@ -302,16 +285,16 @@
   2.130  
   2.131  val ensure_consts = ensure_consts;
   2.132  
   2.133 -fun check_consts rewrites thy consts funcgr =
   2.134 +fun check_consts thy consts funcgr =
   2.135    let
   2.136      val algebra = Code.coregular_algebra thy;
   2.137      fun try_const const funcgr =
   2.138 -      (SOME const, ensure_consts' rewrites thy algebra [const] funcgr)
   2.139 +      (SOME const, ensure_consts' thy algebra [const] funcgr)
   2.140        handle INVALID (cs', msg) => (NONE, funcgr);
   2.141      val (consts', funcgr') = fold_map try_const consts funcgr;
   2.142    in (map_filter I consts', funcgr') end;
   2.143  
   2.144 -fun ensure_consts_term rewrites thy f ct funcgr =
   2.145 +fun ensure_consts_term_proto thy f ct funcgr =
   2.146    let
   2.147      fun consts_of thy t =
   2.148        fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
   2.149 @@ -321,11 +304,10 @@
   2.150        in Thm.transitive thm thm' end
   2.151      val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
   2.152      val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
   2.153 -    val thm1 = Code.preprocess_conv ct
   2.154 -      |> fold (rhs_conv o MetaSimplifier.rewrite false o single) (rewrites thy);
   2.155 +    val thm1 = Code.preprocess_conv ct;
   2.156      val ct' = Thm.rhs_of thm1;
   2.157      val consts = consts_of thy (Thm.term_of ct');
   2.158 -    val funcgr' = ensure_consts rewrites thy consts funcgr;
   2.159 +    val funcgr' = ensure_consts thy consts funcgr;
   2.160      val algebra = Code.coregular_algebra thy;
   2.161      val (_, thm2) = Thm.varifyT' [] thm1;
   2.162      val thm3 = Thm.reflexive (Thm.rhs_of thm2);
   2.163 @@ -344,10 +326,10 @@
   2.164      val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
   2.165      val drop = drop_classes thy tfrees;
   2.166      val instdefs = instances_of_consts thy algebra funcgr' cs;
   2.167 -    val funcgr'' = ensure_consts rewrites thy instdefs funcgr';
   2.168 +    val funcgr'' = ensure_consts thy instdefs funcgr';
   2.169    in (f funcgr'' drop ct'' thm5, funcgr'') end;
   2.170  
   2.171 -fun ensure_consts_eval rewrites thy conv =
   2.172 +fun ensure_consts_eval thy conv =
   2.173    let
   2.174      fun conv' funcgr drop_classes ct thm1 =
   2.175        let
   2.176 @@ -359,49 +341,38 @@
   2.177            error ("eval_conv - could not construct proof:\n"
   2.178            ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
   2.179        end;
   2.180 -  in ensure_consts_term rewrites thy conv' end;
   2.181 +  in ensure_consts_term_proto thy conv' end;
   2.182 +
   2.183 +fun ensure_consts_term thy f =
   2.184 +  let
   2.185 +    fun f' funcgr drop_classes ct thm1 = f funcgr ct;
   2.186 +  in ensure_consts_term_proto thy f' end;
   2.187  
   2.188  end; (*local*)
   2.189  
   2.190 -end; (*struct*)
   2.191 -
   2.192 -functor CodeFuncgrRetrieval (val rewrites: theory -> thm list) : CODE_FUNCGR_RETRIEVAL =
   2.193 -struct
   2.194 -
   2.195 -(** code data **)
   2.196 -
   2.197 -type T = CodeFuncgr.T;
   2.198 -
   2.199  structure Funcgr = CodeDataFun
   2.200  (struct
   2.201    type T = T;
   2.202 -  val empty = CodeFuncgr.Constgraph.empty;
   2.203 -  fun merge _ _ = CodeFuncgr.Constgraph.empty;
   2.204 -  fun purge _ NONE _ = CodeFuncgr.Constgraph.empty
   2.205 +  val empty = Constgraph.empty;
   2.206 +  fun merge _ _ = Constgraph.empty;
   2.207 +  fun purge _ NONE _ = Constgraph.empty
   2.208      | purge _ (SOME cs) funcgr =
   2.209 -        CodeFuncgr.Constgraph.del_nodes ((CodeFuncgr.Constgraph.all_preds funcgr 
   2.210 -          o filter (can (CodeFuncgr.Constgraph.get_node funcgr))) cs) funcgr;
   2.211 +        Constgraph.del_nodes ((Constgraph.all_preds funcgr 
   2.212 +          o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
   2.213  end);
   2.214  
   2.215  fun make thy =
   2.216 -  Funcgr.change thy o CodeFuncgr.ensure_consts rewrites thy;
   2.217 +  Funcgr.change thy o ensure_consts thy;
   2.218  
   2.219  fun make_consts thy =
   2.220 -  Funcgr.change_yield thy o CodeFuncgr.check_consts rewrites thy;
   2.221 -
   2.222 -fun make_term thy f =
   2.223 -  Funcgr.change_yield thy o CodeFuncgr.ensure_consts_term rewrites thy f;
   2.224 +  Funcgr.change_yield thy o check_consts thy;
   2.225  
   2.226  fun eval_conv thy f =
   2.227 -  fst o Funcgr.change_yield thy o CodeFuncgr.ensure_consts_eval rewrites thy f;
   2.228 +  fst o Funcgr.change_yield thy o ensure_consts_eval thy f;
   2.229 +
   2.230 +fun eval_term thy f =
   2.231 +  fst o Funcgr.change_yield thy o ensure_consts_term thy f;
   2.232  
   2.233  fun intervene thy funcgr = Funcgr.change thy (K funcgr);
   2.234  
   2.235 -end; (*functor*)
   2.236 -
   2.237 -structure CodeFuncgr : CODE_FUNCGR =
   2.238 -struct
   2.239 -
   2.240 -open CodeFuncgr;
   2.241 -
   2.242  end; (*struct*)
     3.1 --- a/src/Tools/code/code_package.ML	Wed Aug 15 08:57:41 2007 +0200
     3.2 +++ b/src/Tools/code/code_package.ML	Wed Aug 15 08:57:42 2007 +0200
     3.3 @@ -9,14 +9,15 @@
     3.4  sig
     3.5    (* interfaces *)
     3.6    val eval_conv: theory
     3.7 -    -> (CodeThingol.code -> CodeThingol.iterm -> cterm -> thm) -> cterm -> thm;
     3.8 +    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> thm)
     3.9 +    -> cterm -> thm;
    3.10 +  val eval_term: theory
    3.11 +    -> (CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> cterm -> 'a)
    3.12 +    -> cterm -> 'a;
    3.13 +  val satisfies_ref: bool option ref;
    3.14 +  val satisfies: theory -> cterm -> string list -> bool;
    3.15    val codegen_command: theory -> string -> unit;
    3.16  
    3.17 -  (* primitive interfaces *)
    3.18 -  val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a;
    3.19 -  val satisfies_ref: bool option ref;
    3.20 -  val satisfies: theory -> term -> string list -> bool;
    3.21 -
    3.22    (* axiomatic interfaces *)
    3.23    type appgen;
    3.24    val add_appconst: string * appgen -> theory -> theory;
    3.25 @@ -63,12 +64,10 @@
    3.26      (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
    3.27  );
    3.28  
    3.29 -structure Funcgr = CodeFuncgrRetrieval (fun rewrites thy = []);
    3.30 -
    3.31 -fun code_depgr thy [] = Funcgr.make thy []
    3.32 +fun code_depgr thy [] = CodeFuncgr.make thy []
    3.33    | code_depgr thy consts =
    3.34        let
    3.35 -        val gr = Funcgr.make thy consts;
    3.36 +        val gr = CodeFuncgr.make thy consts;
    3.37          val select = CodeFuncgr.Constgraph.all_succs gr consts;
    3.38        in
    3.39          CodeFuncgr.Constgraph.subgraph
    3.40 @@ -116,7 +115,10 @@
    3.41   of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
    3.42    | NONE => NONE;
    3.43  
    3.44 -fun ensure_def thy = CodeThingol.ensure_def (CodeName.labelled_name thy);
    3.45 +val value_name = "Isabelle_Eval.EVAL.EVAL";
    3.46 +
    3.47 +fun ensure_def thy = CodeThingol.ensure_def
    3.48 +  (fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
    3.49  
    3.50  fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
    3.51    let
    3.52 @@ -442,7 +444,7 @@
    3.53          orelse is_some (Code.get_datatype_of_constr thy c2)
    3.54        then error ("Not a function: " ^ CodeUnit.string_of_const thy c2)
    3.55        else ();
    3.56 -    val funcgr = Funcgr.make thy [c1, c2];
    3.57 +    val funcgr = CodeFuncgr.make thy [c1, c2];
    3.58      val ty1 = (f o CodeFuncgr.typ funcgr) c1;
    3.59      val ty2 = CodeFuncgr.typ funcgr c2;
    3.60      val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
    3.61 @@ -513,75 +515,23 @@
    3.62  fun generate thy funcgr gen it =
    3.63    let
    3.64      (*FIXME*)
    3.65 -    val _ = Funcgr.intervene thy funcgr;
    3.66 +    val _ = CodeFuncgr.intervene thy funcgr;
    3.67      val cs = map_filter (Consttab.lookup ((snd o snd o Translation.get) thy))
    3.68        (CodeFuncgr.all funcgr);
    3.69 -    val funcgr' = Funcgr.make thy cs;
    3.70 +    val CodeFuncgr' = CodeFuncgr.make thy cs;
    3.71      val naming = NameSpace.qualified_names NameSpace.default_naming;
    3.72      val consttab = Consts.empty
    3.73        |> fold (fn c => Consts.declare naming
    3.74 -           ((CodeName.const thy c, CodeFuncgr.typ funcgr' c), true))
    3.75 -           (CodeFuncgr.all funcgr');
    3.76 +           ((CodeName.const thy c, CodeFuncgr.typ CodeFuncgr' c), true))
    3.77 +           (CodeFuncgr.all CodeFuncgr');
    3.78      val algbr = (Code.operational_algebra thy, consttab);
    3.79    in   
    3.80      Program.change_yield thy
    3.81 -      (CodeThingol.start_transact (gen thy algbr funcgr' it))
    3.82 +      (CodeThingol.start_transact (gen thy algbr CodeFuncgr' it))
    3.83 +    |> fst
    3.84    end;
    3.85  
    3.86 -    (*val val_name = "Isabelle_Eval.EVAL.EVAL";
    3.87 -    val val_name' = "Isabelle_Eval.EVAL";
    3.88 -    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
    3.89 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] labelled_name;
    3.90 -    fun eval code = (
    3.91 -      reff := NONE;
    3.92 -      seri (SOME [val_name]) code;
    3.93 -      use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
    3.94 -        ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name'_args ^ "))");
    3.95 -      case !reff
    3.96 -       of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
    3.97 -            ^ " (reference probably has been shadowed)")
    3.98 -        | SOME value => value
    3.99 -      );
   3.100 -
   3.101 -    fun defgen_fun trns =
   3.102 -      let
   3.103 -        val const' = perhaps (Consttab.lookup ((snd o snd o Translation.get) thy)) const;
   3.104 -        val raw_thms = CodeFuncgr.funcs funcgr const';
   3.105 -        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) const';
   3.106 -        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   3.107 -          then raw_thms
   3.108 -          else map (CodeUnit.expand_eta 1) raw_thms;
   3.109 -        val timeap = if !timing then Output.timeap_msg ("time for " ^ c')
   3.110 -          else I;
   3.111 -        val msg = cat_lines ("generating code for theorems " :: map string_of_thm thms);
   3.112 -        val vs = (map dest_TFree o Consts.typargs consts) (c', ty);
   3.113 -        val dest_eqthm =
   3.114 -          apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of;
   3.115 -        fun exprgen_eq (args, rhs) trns =
   3.116 -          trns
   3.117 -          |> fold_map (exprgen_term thy algbr funcgr) args
   3.118 -          ||>> exprgen_term thy algbr funcgr rhs;
   3.119 -      in
   3.120 -        trns
   3.121 -        |> CodeThingol.message msg (fn trns => trns
   3.122 -        |> timeap (fold_map (exprgen_eq o dest_eqthm) thms)
   3.123 -        ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   3.124 -        ||>> exprgen_typ thy algbr funcgr ty
   3.125 -        |-> (fn ((eqs, vs), ty) => succeed (CodeThingol.Fun (eqs, (vs, ty)))))
   3.126 -      end;
   3.127 -    val defgen = if (is_some o Code.get_datatype_of_constr thy) const
   3.128 -      then defgen_datatypecons
   3.129 -      else if is_some opt_tyco
   3.130 -        orelse (not o is_some o AxClass.class_of_param thy) c
   3.131 -      then defgen_fun
   3.132 -      else defgen_classop
   3.133 -  in
   3.134 -    trns
   3.135 -    |> ensure_def thy defgen ("generating constant " ^ CodeUnit.string_of_const thy const) c'
   3.136 -
   3.137 -*)
   3.138 -
   3.139 -(*fun eval_conv thy conv =
   3.140 +fun raw_eval f thy g =
   3.141    let
   3.142      val value_name = "Isabelle_Eval.EVAL.EVAL";
   3.143      fun ensure_eval thy algbr funcgr t = 
   3.144 @@ -590,58 +540,46 @@
   3.145            exprgen_term' thy algbr funcgr t
   3.146            ##>> exprgen_typ thy algbr funcgr (fastype_of t)
   3.147            #>> (fn (t, ty) => CodeThingol.Fun ([([], t)], ([], ty)));
   3.148 +        fun result (dep, code) =
   3.149 +          let
   3.150 +            val CodeThingol.Fun ([([], t)], ([], ty)) = Graph.get_node code value_name;
   3.151 +            val deps = Graph.imm_succs code value_name;
   3.152 +            val code' = Graph.del_nodes [value_name] code;
   3.153 +            val code'' = CodeThingol.project_code false [] (SOME deps) code';
   3.154 +          in ((code'', (t, ty), deps), (dep, code')) end;
   3.155        in
   3.156          ensure_def thy defgen_eval "evaluation" value_name
   3.157 -        #> pair value_name
   3.158 +        #> result
   3.159        end;
   3.160 -    fun conv' funcgr ct =
   3.161 -      let
   3.162 -        val (_, code) = generate thy funcgr ensure_eval (Thm.term_of ct);
   3.163 -        val consts = CodeThingol.fold_constnames (insert (op =)) t [];
   3.164 -        val code = Program.get thy
   3.165 -          |> CodeThingol.project_code true [] (SOME consts)
   3.166 -      in conv code t ct end;
   3.167 -  in Funcgr.eval_conv thy conv' end;*)
   3.168 -
   3.169 -fun eval_conv thy conv =
   3.170 -  let
   3.171 -    fun conv' funcgr ct =
   3.172 +    fun h funcgr ct =
   3.173        let
   3.174 -        val (t, _) = generate thy funcgr exprgen_term' (Thm.term_of ct);
   3.175 -        val consts = CodeThingol.fold_constnames (insert (op =)) t [];
   3.176 -        val code = Program.get thy
   3.177 -          |> CodeThingol.project_code true [] (SOME consts)
   3.178 -      in conv code t ct end;
   3.179 -  in Funcgr.eval_conv thy conv' end;
   3.180 +        val (code, (t, ty), deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
   3.181 +      in g code (t, ty) deps ct end;
   3.182 +  in f thy h end;
   3.183  
   3.184 -fun codegen_term thy t =
   3.185 -  let
   3.186 -    val ct = Thm.cterm_of thy t;
   3.187 -    val (ct', funcgr) = Funcgr.make_term thy (K (K K)) ct;
   3.188 -    val t' = Thm.term_of ct';
   3.189 -  in generate thy funcgr exprgen_term' t' |> fst end;
   3.190 -
   3.191 -fun raw_eval_term thy (ref_spec, t) args =
   3.192 -  let
   3.193 -    val _ = (Term.map_types o Term.map_atyps) (fn _ =>
   3.194 -      error ("Term " ^ Sign.string_of_term thy t ^ " contains polymorphic type"))
   3.195 -      t;
   3.196 -    val t' = codegen_term thy t;
   3.197 -  in
   3.198 -    CodeTarget.eval_term thy CodeName.labelled_name
   3.199 -      (Program.get thy) (ref_spec, t') args
   3.200 -  end;
   3.201 +fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
   3.202 +fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
   3.203  
   3.204  val satisfies_ref : bool option ref = ref NONE;
   3.205  
   3.206 -fun eval_term thy t = raw_eval_term thy t [];
   3.207 -fun satisfies thy t witnesses = raw_eval_term thy
   3.208 -  (("CodePackage.satisfies_ref", satisfies_ref), t) witnesses;
   3.209 +fun satisfies thy ct witnesses =
   3.210 +  let
   3.211 +    fun evl code (t, ty) deps ct =
   3.212 +      let
   3.213 +        val t0 = Thm.term_of ct
   3.214 +        val _ = (Term.map_types o Term.map_atyps) (fn _ =>
   3.215 +          error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
   3.216 +          t0;
   3.217 +      in
   3.218 +        CodeTarget.eval_term thy ("CodePackage.satisfies_ref", satisfies_ref)
   3.219 +          code (t, ty) witnesses
   3.220 +      end;
   3.221 +  in eval_term thy evl ct end;
   3.222  
   3.223  fun filter_generatable thy consts =
   3.224    let
   3.225 -    val (consts', funcgr) = Funcgr.make_consts thy consts;
   3.226 -    val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
   3.227 +    val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
   3.228 +    val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
   3.229      val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
   3.230        (consts' ~~ consts'');
   3.231    in consts''' end;
   3.232 @@ -658,9 +596,9 @@
   3.233    let
   3.234      val (perm1, cs) = CodeUnit.read_const_exprs thy
   3.235        (filter_generatable thy) raw_cs;
   3.236 -    val (perm2, cs') = case generate thy (Funcgr.make thy cs) (fold_map ooo ensure_def_const') cs
   3.237 -     of ([], _) => (true, NONE)
   3.238 -      | (cs, _) => (false, SOME cs);
   3.239 +    val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs) (fold_map ooo ensure_def_const') cs
   3.240 +     of [] => (true, NONE)
   3.241 +      | cs => (false, SOME cs);
   3.242      val code = Program.get thy;
   3.243      val seris' = map (fn (((target, module), file), args) =>
   3.244        CodeTarget.get_serializer thy target (perm1 orelse perm2) module file args
   3.245 @@ -670,10 +608,10 @@
   3.246    end;
   3.247  
   3.248  fun code_thms_cmd thy =
   3.249 -  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy);
   3.250 +  code_thms thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
   3.251  
   3.252  fun code_deps_cmd thy =
   3.253 -  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o Funcgr.make_consts thy);
   3.254 +  code_deps thy o snd o CodeUnit.read_const_exprs thy (fst o CodeFuncgr.make_consts thy);
   3.255  
   3.256  val (inK, module_nameK, fileK) = ("in", "module_name", "file");
   3.257  
     4.1 --- a/src/Tools/code/code_thingol.ML	Wed Aug 15 08:57:41 2007 +0200
     4.2 +++ b/src/Tools/code/code_thingol.ML	Wed Aug 15 08:57:42 2007 +0200
     4.3 @@ -76,7 +76,7 @@
     4.4      -> code -> code;
     4.5    val empty_funs: code -> string list;
     4.6    val is_cons: code -> string -> bool;
     4.7 -  val add_eval_def: string (*bind name*) * iterm -> code -> code;
     4.8 +  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
     4.9  
    4.10    val ensure_def: (string -> string) -> (transact -> def * transact) -> string
    4.11      -> string -> transact -> transact;
    4.12 @@ -247,7 +247,6 @@
    4.13        * (string * iterm) list);
    4.14  
    4.15  type code = def Graph.T;
    4.16 -type transact = Graph.key option * code;
    4.17  
    4.18  
    4.19  (* abstract code *)
    4.20 @@ -372,6 +371,8 @@
    4.21  
    4.22  (* transaction protocol *)
    4.23  
    4.24 +type transact = Graph.key option * code;
    4.25 +
    4.26  fun ensure_def labelled_name defgen msg name (dep, code) =
    4.27    let
    4.28      val msg' = (case dep
    4.29 @@ -402,9 +403,9 @@
    4.30    |> f
    4.31    |-> (fn x => fn (_, code) => (x, code));
    4.32  
    4.33 -fun add_eval_def (name, t) code =
    4.34 +fun add_eval_def (name, (t, ty)) code =
    4.35    code
    4.36 -  |> Graph.new_node (name, Fun ([([], t)], ([("_", [])], ITyVar "_")))
    4.37 +  |> Graph.new_node (name, Fun ([([], t)], ([], ty)))
    4.38    |> fold (curry Graph.add_edge name) (Graph.keys code);
    4.39  
    4.40  end; (*struct*)
     5.1 --- a/src/Tools/nbe.ML	Wed Aug 15 08:57:41 2007 +0200
     5.2 +++ b/src/Tools/nbe.ML	Wed Aug 15 08:57:42 2007 +0200
     5.3 @@ -60,11 +60,6 @@
     5.4     Moreover, to handle functions that are still waiting for some
     5.5     arguments we have additionally a list of arguments collected to far
     5.6     and the number of arguments we're still waiting for.
     5.7 -
     5.8 -   (?) Finally, it might happen, that a function does not get all the
     5.9 -   arguments it needs.  In this case the function must provide means to
    5.10 -   present itself as a string. As this might be a heavy-wight
    5.11 -   operation, we delay it. (?) 
    5.12  *)
    5.13  
    5.14  datatype Univ = 
    5.15 @@ -233,7 +228,7 @@
    5.16          val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
    5.17        in (cs, ml_Let (bind_funs @ [bind_locals]) result) end;
    5.18  
    5.19 -fun assemble_eval thy is_fun t =
    5.20 +fun assemble_eval thy is_fun (t, deps) =
    5.21    let
    5.22      val funs = CodeThingol.fold_constnames (insert (op =)) t [];
    5.23      val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t [];
    5.24 @@ -314,7 +309,7 @@
    5.25  
    5.26  (* evaluation with type reconstruction *)
    5.27  
    5.28 -fun eval thy code t t' =
    5.29 +fun eval thy code t t' deps =
    5.30    let
    5.31      fun subst_Frees [] = I
    5.32        | subst_Frees inst =
    5.33 @@ -330,7 +325,7 @@
    5.34      fun constrain t =
    5.35        singleton (ProofContext.infer_types_pats (ProofContext.init thy)) (TypeInfer.constrain t ty);
    5.36    in
    5.37 -    t'
    5.38 +    (t', deps)
    5.39      |> eval_term thy (Symtab.defined (ensure_funs thy code))
    5.40      |> term_of_univ thy
    5.41      |> tracing (fn t => "Normalized:\n" ^ setmp show_types true Display.raw_string_of_term t)
    5.42 @@ -345,22 +340,22 @@
    5.43  
    5.44  (* evaluation oracle *)
    5.45  
    5.46 -exception Normalization of CodeThingol.code * term * CodeThingol.iterm;
    5.47 +exception Normalization of CodeThingol.code * term * CodeThingol.iterm * string list;
    5.48  
    5.49 -fun normalization_oracle (thy, Normalization (code, t, t')) =
    5.50 -  Logic.mk_equals (t, eval thy code t t');
    5.51 +fun normalization_oracle (thy, Normalization (code, t, t', deps)) =
    5.52 +  Logic.mk_equals (t, eval thy code t t' deps);
    5.53  
    5.54 -fun normalization_invoke thy code t t' =
    5.55 -  Thm.invoke_oracle_i thy "HOL.normalization" (thy, Normalization (code, t, t'));
    5.56 -  (*FIXME get rid of hardwired theory name "HOL"*)
    5.57 +fun normalization_invoke thy code t t' deps =
    5.58 +  Thm.invoke_oracle_i thy "Code_Setup.normalization" (thy, Normalization (code, t, t', deps));
    5.59 +  (*FIXME get rid of hardwired theory name*)
    5.60  
    5.61  fun normalization_conv ct =
    5.62    let
    5.63      val thy = Thm.theory_of_cterm ct;
    5.64 -    fun conv code t' ct =
    5.65 +    fun conv code (t', ty') deps ct =
    5.66        let
    5.67          val t = Thm.term_of ct;
    5.68 -      in normalization_invoke thy code t t' end;
    5.69 +      in normalization_invoke thy code t t' deps end;
    5.70    in CodePackage.eval_conv thy conv ct end;
    5.71  
    5.72  (* evaluation command *)