# HG changeset patch
# User haftmann
# Date 1191873811 -7200
# Node ID 22013215eece30c47843d73a5d0fd9fa08086d24
# Parent  8b97a94ab187ff4704e35d760e573408a7855a31
moved translation kernel to CodeThingol

diff -r 8b97a94ab187 -r 22013215eece src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_package.ML	Mon Oct 08 22:03:31 2007 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Code generator translation kernel.  Code generator Isar setup.
+Code generator interfaces and Isar setup.
 *)
 
 signature CODE_PACKAGE =
@@ -17,16 +17,12 @@
     -> term -> 'a;
   val satisfies_ref: (unit -> bool) option ref;
   val satisfies: theory -> term -> string list -> bool;
-  val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
-    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val codegen_command: theory -> string -> unit;
 end;
 
 structure CodePackage : CODE_PACKAGE =
 struct
 
-open BasicCodeThingol;
-
 (** code theorems **)
 
 fun code_depgr thy [] = CodeFuncgr.make thy []
@@ -57,7 +53,9 @@
   in Present.display_graph prgr end;
 
 
-(** code translation **)
+(** code generation interfaces **)
+
+(* code data *)
 
 structure Program = CodeDataFun
 (
@@ -77,300 +75,15 @@
         in Graph.del_nodes dels code end;
 );
 
-
-(* translation kernel *)
-
-val value_name = "Isabelle_Eval.EVAL.EVAL";
-
-fun ensure_def thy = CodeThingol.ensure_def
-  (fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
-
-exception CONSTRAIN of (string * typ) * typ;
+(* generic generation combinators *)
 
-fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
-  let
-    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
-    val (v, cs) = AxClass.params_of_class thy class;
-    val class' = CodeName.class thy class;
-    val defgen_class =
-      fold_map (fn superclass => ensure_def_class thy algbr funcgr superclass
-        ##>> ensure_def_classrel thy algbr funcgr (class, superclass)) superclasses
-      ##>> fold_map (fn (c, ty) => ensure_def_const thy algbr funcgr c
-        ##>> exprgen_typ thy algbr funcgr ty) cs
-      #>> (fn info => CodeThingol.Class (unprefix "'" v, info))
-  in
-    ensure_def thy defgen_class class'
-    #> pair class'
-  end
-and ensure_def_classrel thy algbr funcgr (subclass, superclass) =
-  let
-    val classrel' = CodeName.classrel thy (subclass, superclass);
-    val defgen_classrel =
-      ensure_def_class thy algbr funcgr subclass
-      ##>> ensure_def_class thy algbr funcgr superclass
-      #>> CodeThingol.Classrel;
-  in
-    ensure_def thy defgen_classrel classrel'
-    #> pair classrel'
-  end
-and ensure_def_tyco thy algbr funcgr "fun" =
-      pair "fun"
-  | ensure_def_tyco thy algbr funcgr tyco =
-      let
-        val defgen_datatype =
-          let
-            val (vs, cos) = Code.get_datatype thy tyco;
-          in
-            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-            ##>> fold_map (fn (c, tys) =>
-              ensure_def_const thy algbr funcgr c
-              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
-            #>> CodeThingol.Datatype
-          end;
-        val tyco' = CodeName.tyco thy tyco;
-      in
-        ensure_def thy defgen_datatype tyco'
-        #> pair tyco'
-      end
-and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
-  fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
-  #>> (fn sort => (unprefix "'" v, sort))
-and exprgen_typ thy algbr funcgr (TFree vs) =
-      exprgen_tyvar_sort thy algbr funcgr vs
-      #>> (fn (v, sort) => ITyVar v)
-  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
-      ensure_def_tyco thy algbr funcgr tyco
-      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
-      #>> (fn (tyco, tys) => tyco `%% tys)
-and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
-  let
-    val pp = Sign.pp thy;
-    datatype typarg =
-        Global of (class * string) * typarg list list
-      | Local of (class * class) list * (string * (int * sort));
-    fun class_relation (Global ((_, tyco), yss), _) class =
-          Global ((class, tyco), yss)
-      | class_relation (Local (classrels, v), subclass) superclass =
-          Local ((subclass, superclass) :: classrels, v);
-    fun type_constructor tyco yss class =
-      Global ((class, tyco), (map o map) fst yss);
-    fun type_variable (TFree (v, sort)) =
-      let
-        val sort' = proj_sort sort;
-      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
-    val typargs = Sorts.of_sort_derivation pp algebra
-      {class_relation = class_relation, type_constructor = type_constructor,
-       type_variable = type_variable}
-      (ty_ctxt, proj_sort sort_decl);
-    fun mk_dict (Global (inst, yss)) =
-          ensure_def_inst thy algbr funcgr inst
-          ##>> (fold_map o fold_map) mk_dict yss
-          #>> (fn (inst, dss) => DictConst (inst, dss))
-      | mk_dict (Local (classrels, (v, (k, sort)))) =
-          fold_map (ensure_def_classrel thy algbr funcgr) classrels
-          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
-  in
-    fold_map mk_dict typargs
-  end
-and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
-  let
-    val ty_decl = Consts.the_declaration consts c;
-    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
-    val sorts = map (snd o dest_TVar) tys_decl;
-  in
-    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
-  end
-and exprgen_eq thy algbr funcgr thm =
-  let
-    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
-      o Logic.unvarify o prop_of) thm;
-  in
-    fold_map (exprgen_term thy algbr funcgr) args
-    ##>> exprgen_term thy algbr funcgr rhs
-    #>> rpair thm
-  end
-and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
-  let
-    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
-    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
-    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
-    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
-    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
-      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
-    val arity_typ = Type (tyco, map TFree vs);
-    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
-    fun exprgen_superarity superclass =
-      ensure_def_class thy algbr funcgr superclass
-      ##>> ensure_def_classrel thy algbr funcgr (class, superclass)
-      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
-      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
-            (superclass, (classrel, (inst, dss))));
-    fun exprgen_classparam_inst (c, ty) =
-      let
-        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
-        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
-        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
-          o Logic.dest_equals o Thm.prop_of) thm;
-      in
-        ensure_def_const thy algbr funcgr c
-        ##>> exprgen_const thy algbr funcgr c_ty
-        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
-      end;
-    val defgen_inst =
-      ensure_def_class thy algbr funcgr class
-      ##>> ensure_def_tyco thy algbr funcgr tyco
-      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-      ##>> fold_map exprgen_superarity superclasses
-      ##>> fold_map exprgen_classparam_inst classparams
-      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
-             CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classparams)));
-    val inst = CodeName.instance thy (class, tyco);
-  in
-    ensure_def thy defgen_inst inst
-    #> pair inst
-  end
-and ensure_def_const thy (algbr as (_, consts)) funcgr c =
-  let
-    val c' = CodeName.const thy c;
-    fun defgen_datatypecons tyco =
-      ensure_def_tyco thy algbr funcgr tyco
-      #>> K (CodeThingol.Datatypecons c');
-    fun defgen_classparam class =
-      ensure_def_class thy algbr funcgr class
-      #>> K (CodeThingol.Classparam c');
-    fun defgen_fun trns =
-      let
-        val raw_thms = CodeFuncgr.funcs funcgr c;
-        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
-        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
-        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
-          then raw_thms
-          else map (CodeUnit.expand_eta 1) raw_thms;
-      in
-        trns
-        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-        ||>> exprgen_typ thy algbr funcgr ty
-        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
-        |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
-      end;
-    val defgen = case Code.get_datatype_of_constr thy c
-     of SOME tyco => defgen_datatypecons tyco
-      | NONE => (case AxClass.class_of_param thy c
-         of SOME class => defgen_classparam class
-          | NONE => defgen_fun)
-  in
-    ensure_def thy defgen c'
-    #> pair c'
-  end
-and exprgen_term thy algbr funcgr (Const (c, ty)) =
-      exprgen_app thy algbr funcgr ((c, ty), [])
-  | exprgen_term thy algbr funcgr (Free (v, _)) =
-      pair (IVar v)
-  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
-      let
-        val (v, t) = Syntax.variant_abs abs;
-      in
-        exprgen_typ thy algbr funcgr ty
-        ##>> exprgen_term thy algbr funcgr t
-        #>> (fn (ty, t) => (v, ty) `|-> t)
-      end
-  | exprgen_term thy algbr funcgr (t as _ $ _) =
-      case strip_comb t
-       of (Const (c, ty), ts) =>
-            exprgen_app thy algbr funcgr ((c, ty), ts)
-        | (t', ts) =>
-            exprgen_term thy algbr funcgr t'
-            ##>> fold_map (exprgen_term thy algbr funcgr) ts
-            #>> (fn (t, ts) => t `$$ ts)
-and exprgen_const thy algbr funcgr (c, ty) =
-  ensure_def_const thy algbr funcgr c
-  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
-  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
-  (*##>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)*)
-  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
-and exprgen_app_default thy algbr funcgr (c_ty, ts) =
-  exprgen_const thy algbr funcgr c_ty
-  ##>> fold_map (exprgen_term thy algbr funcgr) ts
-  #>> (fn (t, ts) => t `$$ ts)
-and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
-  let
-    (*FIXME rework this code*)
-    val (all_tys, _) = strip_type ty;
-    val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys;
-    val st = nth ts n;
-    val sty = nth tys n;
-    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
-      | is_undefined _ = false;
-    fun mk_case (co, n) t =
-      let
-        val (vs, body) = Term.strip_abs_eta n t;
-        val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs);
-      in if is_undefined body then NONE else SOME (selector, body) end;
-    val ds = case cases
-     of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
-          in [(Free v_ty, body)] end
-      | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases
-          ~~ nth_drop n ts);
-  in
-    exprgen_term thy algbr funcgr st
-    ##>> exprgen_typ thy algbr funcgr sty
-    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
-          ##>> exprgen_term thy algbr funcgr body) ds
-    ##>> exprgen_app_default thy algbr funcgr app
-    #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0))
-  end
-and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
- of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
-      if length ts < i then
-        let
-          val k = length ts;
-          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
-          val ctxt = (fold o fold_aterms)
-            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
-          val vs = Name.names ctxt "a" tys;
-        in
-          fold_map (exprgen_typ thy algbr funcgr) tys
-          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
-          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
-        end
-      else if length ts > i then
-        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
-        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
-        #>> (fn (t, ts) => t `$$ ts)
-      else
-        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
-      end
-  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
+val ensure_const = CodeThingol.ensure_const;
 
-
-(* entrance points into translation kernel *)
-
-fun ensure_def_const' thy algbr funcgr c trns =
-  ensure_def_const thy algbr funcgr c trns
-  handle CONSTRAIN ((c, ty), ty_decl) => error (
-    "Constant " ^ c ^ " with most general type\n"
-    ^ CodeUnit.string_of_typ thy ty
-    ^ "\noccurs with type\n"
-    ^ CodeUnit.string_of_typ thy ty_decl);
-
-fun perhaps_def_const thy algbr funcgr c trns =
-  case try (ensure_def_const thy algbr funcgr c) trns
+fun perhaps_const thy algbr funcgr c trns =
+  case try (CodeThingol.ensure_const thy algbr funcgr c) trns
    of SOME (c, trns) => (SOME c, trns)
     | NONE => (NONE, trns);
 
-fun exprgen_term' thy algbr funcgr t trns =
-  exprgen_term thy algbr funcgr t trns
-  handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
-    ^ ",\nconstant " ^ c ^ " with most general type\n"
-    ^ CodeUnit.string_of_typ thy ty
-    ^ "\noccurs with type\n"
-    ^ CodeUnit.string_of_typ thy ty_decl);
-
-
-(** code generation interfaces **)
-
-(* generic generation combinators *)
-
 fun generate thy funcgr gen it =
   let
     val naming = NameSpace.qualified_names NameSpace.default_naming;
@@ -380,66 +93,51 @@
     val algbr = (Code.operational_algebra thy, consttab);
   in   
     Program.change_yield thy
-      (CodeThingol.start_transact (gen thy algbr funcgr it))
-    |> fst
+      (CodeThingol.transact (gen thy algbr funcgr it))
   end;
 
 fun code thy permissive cs seris =
   let
     val code = Program.get thy;
     val seris' = map (fn (((target, module), file), args) =>
-      CodeTarget.get_serializer thy target permissive module file args
-        CodeName.labelled_name cs) seris;
+      CodeTarget.get_serializer thy target permissive module file args cs) seris;
   in (map (fn f => f code) seris' : unit list; ()) end;
 
 fun raw_eval evaluate term_of thy g =
   let
-    val value_name = "Isabelle_Eval.EVAL.EVAL";
-    fun ensure_eval thy algbr funcgr t = 
+    fun result (_, code) =
       let
-        val ty = fastype_of t;
-        val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
-          o dest_TFree))) t [];
-        val defgen_eval =
-          fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
-          ##>> exprgen_typ thy algbr funcgr ty
-          ##>> exprgen_term' thy algbr funcgr t
-          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
-        fun result (dep, code) =
-          let
-            val CodeThingol.Fun ((vs, ty), [(([], t), _)]) = Graph.get_node code value_name;
-            val deps = Graph.imm_succs code value_name;
-            val code' = Graph.del_nodes [value_name] code;
-            val code'' = CodeThingol.project_code false [] (SOME deps) code';
-          in ((code'', ((vs, ty), t), deps), (dep, code')) end;
-      in
-        ensure_def thy defgen_eval value_name
-        #> result
-      end;
+        val CodeThingol.Fun ((vs, ty), [(([], t), _)]) =
+          Graph.get_node code CodeName.value_name;
+        val deps = Graph.imm_succs code CodeName.value_name;
+        val code' = Graph.del_nodes [CodeName.value_name] code;
+        val code'' = CodeThingol.project_code false [] (SOME deps) code';
+      in ((code'', ((vs, ty), t), deps), code') end;
     fun h funcgr ct =
       let
-        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
+        val ((code, vs_ty_t, deps), _) = term_of ct
+          |> generate thy funcgr CodeThingol.ensure_value
+          |> result
+          ||> `(fn code' => Program.change thy (K code'));
       in g code vs_ty_t deps ct end;
   in evaluate thy h end;
 
 fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
 fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
 
-fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
-
 val satisfies_ref : (unit -> bool) option ref = ref NONE;
 
 fun satisfies thy t witnesses =
   let
     fun evl code ((vs, ty), t) deps ct =
-      eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
+      CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
         code (t, ty) witnesses;
   in eval_term thy evl t end;
 
 fun filter_generatable thy consts =
   let
     val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
-    val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
+    val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
     val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
       (consts' ~~ consts'');
   in consts''' end;
@@ -449,9 +147,9 @@
     val (perm1, cs) = CodeUnit.read_const_exprs thy
       (filter_generatable thy) raw_cs;
     val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
-      (fold_map ooo ensure_def_const') cs
-     of [] => (true, NONE)
-      | cs => (false, SOME cs);
+      (fold_map ooo ensure_const) cs
+     of ([], _) => (true, NONE)
+      | (cs, _) => (false, SOME cs);
   in (perm1 orelse perm2, cs') end;
 
 
@@ -515,8 +213,7 @@
   end;
 
 
-
-(** toplevel interface and setup **)
+(** interfaces and Isar setup **)
 
 local
 
@@ -542,8 +239,8 @@
     val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
       (map (the o CodeName.const_rev thy) (these cs)) thy;
     val prop_cs = (filter_generatable thy' o map fst) c_thms;
-    val _ = if null seris then [] else generate thy' (CodeFuncgr.make thy' prop_cs)
-      (fold_map ooo ensure_def_const') prop_cs;
+    val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs)
+      (fold_map ooo ensure_const) prop_cs; ());
     val _ = if null seris then () else code thy' permissive
       (SOME (map (CodeName.const thy') prop_cs)) seris;
   in thy' end;
diff -r 8b97a94ab187 -r 22013215eece src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_target.ML	Mon Oct 08 22:03:31 2007 +0200
@@ -34,14 +34,12 @@
   type serializer;
   val add_serializer: string * serializer -> theory -> theory;
   val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
-    -> (theory -> string -> string) -> string list option
-    -> CodeThingol.code -> unit;
+    -> string list option -> CodeThingol.code -> unit;
   val assert_serializer: theory -> string -> string;
 
   val eval_verbose: bool ref;
-  val eval_invoke: theory -> (theory -> string -> string)
-    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
-    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
+  val eval_invoke: theory -> (string * (unit -> 'a) option ref)
+    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val code_width: int ref;
 
   val setup: theory -> theory;
@@ -1632,7 +1630,7 @@
 val target_diag = "diag";
 
 fun get_serializer thy target permissive module file args
-    labelled_name = fn cs =>
+    = fn cs =>
   let
     val (seris, exc) = CodeTargetData.get thy;
     val data = case Symtab.lookup seris target
@@ -1648,28 +1646,26 @@
     fun check_empty_funs code = case (filter_out (member (op =) exc)
         (CodeThingol.empty_funs code))
      of [] => code
-      | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
+      | names => error ("No defining equations for " ^ commas (map (CodeName.labelled_name thy) names));
   in
     project
     #> check_empty_funs
-    #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
-      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
+    #> seri module file args (CodeName.labelled_name thy) reserved (Symtab.lookup alias)
+      (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   end;
 
-fun eval_invoke thy labelled_name (ref_name, reff) code (t, ty) args =
+fun eval_invoke thy (ref_name, reff) code (t, ty) args =
   let
     val _ = if CodeThingol.contains_dictvar t then
       error "Term to be evaluated constains free dictionaries" else ();
-    val val_name = "Isabelle_Eval.EVAL.EVAL";
-    val val_name' = "Isabelle_Eval.EVAL";
-    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
-    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
-      labelled_name;
+    val val_args = space_implode " "
+      (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
+    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
     fun eval code = (
       reff := NONE;
-      seri (SOME [val_name]) code;
+      seri (SOME [CodeName.value_name]) code;
       use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
-        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
+        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
       case !reff
        of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
             ^ " (reference probably has been shadowed)")
@@ -1677,7 +1673,7 @@
       );
   in
     code
-    |> CodeThingol.add_eval_def (val_name, (t, ty))
+    |> CodeThingol.add_value_stmt (t, ty)
     |> eval
   end;
 
diff -r 8b97a94ab187 -r 22013215eece src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Mon Oct 08 22:03:30 2007 +0200
+++ b/src/Tools/code/code_thingol.ML	Mon Oct 08 22:03:31 2007 +0200
@@ -3,6 +3,7 @@
     Author:     Florian Haftmann, TU Muenchen
 
 Intermediate language ("Thin-gol") representing executable code.
+Representation and translation.
 *)
 
 infix 8 `%%;
@@ -58,7 +59,7 @@
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
 
-  datatype def =
+  datatype stmt =
       Bot
     | Fun of typscheme * ((iterm list * iterm) * thm) list
     | Datatype of (vname * sort) list * (string * itype list) list
@@ -69,8 +70,7 @@
     | Classinst of (class * (string * (vname * sort) list))
           * ((class * (string * (string * dict list list))) list
         * ((string * const) * thm) list);
-  type code = def Graph.T;
-  type transact;
+  type code = stmt Graph.T;
   val empty_code: code;
   val merge_code: code * code -> code;
   val project_code: bool (*delete empty funs*)
@@ -78,11 +78,14 @@
     -> code -> code;
   val empty_funs: code -> string list;
   val is_cons: code -> string -> bool;
-  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
 
-  val ensure_def: (string -> string) -> (transact -> def * transact) -> string
-    -> transact -> transact;
-  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
+  type transact;
+  val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
+    -> CodeFuncgr.T -> string -> transact -> string * transact;
+  val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
+    -> CodeFuncgr.T -> term -> transact -> string * transact;
+  val add_value_stmt: iterm * itype -> code -> code;
+  val transact: (transact -> 'a * transact) -> code -> 'a * code;
 end;
 
 structure CodeThingol: CODE_THINGOL =
@@ -245,7 +248,7 @@
 (** definitions, transactions **)
 
 type typscheme = (vname * sort) list * itype;
-datatype def =
+datatype stmt =
     Bot
   | Fun of typscheme * ((iterm list * iterm) * thm) list
   | Datatype of (vname * sort) list * (string * itype list) list
@@ -257,7 +260,7 @@
         * ((class * (string * (string * dict list list))) list
       * ((string * const) * thm) list);
 
-type code = def Graph.T;
+type code = stmt Graph.T;
 
 
 (* abstract code *)
@@ -315,12 +318,12 @@
 
 type transact = Graph.key option * code;
 
-fun ensure_def labelled_name defgen name (dep, code) =
+fun ensure_stmt stmtgen name (dep, code) =
   let
     fun add_def false =
           ensure_bot name
           #> add_dep (dep, name)
-          #> curry defgen (SOME name)
+          #> curry stmtgen (SOME name)
           ##> snd
           #-> (fn def => add_def_incr (name, def))
       | add_def true =
@@ -329,17 +332,284 @@
     code
     |> add_def (can (Graph.get_node code) name)
     |> pair dep
+    |> pair name
   end;
 
-fun start_transact f code =
+fun transact f code =
   (NONE, code)
   |> f
   |-> (fn x => fn (_, code) => (x, code));
 
-fun add_eval_def (name, (t, ty)) code =
+
+(* translation kernel *)
+
+fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
+  let
+    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+    val (v, cs) = AxClass.params_of_class thy class;
+    val class' = CodeName.class thy class;
+    val stmt_class =
+      fold_map (fn superclass => ensure_class thy algbr funcgr superclass
+        ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
+      ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
+        ##>> exprgen_typ thy algbr funcgr ty) cs
+      #>> (fn info => Class (unprefix "'" v, info))
+  in
+    ensure_stmt stmt_class class'
+  end
+and ensure_classrel thy algbr funcgr (subclass, superclass) =
+  let
+    val classrel' = CodeName.classrel thy (subclass, superclass);
+    val stmt_classrel =
+      ensure_class thy algbr funcgr subclass
+      ##>> ensure_class thy algbr funcgr superclass
+      #>> Classrel;
+  in
+    ensure_stmt stmt_classrel classrel'
+  end
+and ensure_tyco thy algbr funcgr "fun" =
+      pair "fun"
+  | ensure_tyco thy algbr funcgr tyco =
+      let
+        val stmt_datatype =
+          let
+            val (vs, cos) = Code.get_datatype thy tyco;
+          in
+            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+            ##>> fold_map (fn (c, tys) =>
+              ensure_const thy algbr funcgr c
+              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
+            #>> Datatype
+          end;
+        val tyco' = CodeName.tyco thy tyco;
+      in
+        ensure_stmt stmt_datatype tyco'
+      end
+and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
+  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
+  #>> (fn sort => (unprefix "'" v, sort))
+and exprgen_typ thy algbr funcgr (TFree vs) =
+      exprgen_tyvar_sort thy algbr funcgr vs
+      #>> (fn (v, sort) => ITyVar v)
+  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
+      ensure_tyco thy algbr funcgr tyco
+      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
+      #>> (fn (tyco, tys) => tyco `%% tys)
+and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
+  let
+    val pp = Sign.pp thy;
+    datatype typarg =
+        Global of (class * string) * typarg list list
+      | Local of (class * class) list * (string * (int * sort));
+    fun class_relation (Global ((_, tyco), yss), _) class =
+          Global ((class, tyco), yss)
+      | class_relation (Local (classrels, v), subclass) superclass =
+          Local ((subclass, superclass) :: classrels, v);
+    fun type_constructor tyco yss class =
+      Global ((class, tyco), (map o map) fst yss);
+    fun type_variable (TFree (v, sort)) =
+      let
+        val sort' = proj_sort sort;
+      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
+    val typargs = Sorts.of_sort_derivation pp algebra
+      {class_relation = class_relation, type_constructor = type_constructor,
+       type_variable = type_variable}
+      (ty_ctxt, proj_sort sort_decl);
+    fun mk_dict (Global (inst, yss)) =
+          ensure_inst thy algbr funcgr inst
+          ##>> (fold_map o fold_map) mk_dict yss
+          #>> (fn (inst, dss) => DictConst (inst, dss))
+      | mk_dict (Local (classrels, (v, (k, sort)))) =
+          fold_map (ensure_classrel thy algbr funcgr) classrels
+          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
+  in
+    fold_map mk_dict typargs
+  end
+and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
+  let
+    val ty_decl = Consts.the_declaration consts c;
+    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
+    val sorts = map (snd o dest_TVar) tys_decl;
+  in
+    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
+  end
+and exprgen_eq thy algbr funcgr thm =
+  let
+    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
+      o Logic.unvarify o prop_of) thm;
+  in
+    fold_map (exprgen_term thy algbr funcgr) args
+    ##>> exprgen_term thy algbr funcgr rhs
+    #>> rpair thm
+  end
+and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
+  let
+    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
+    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
+    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
+    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
+      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
+    val arity_typ = Type (tyco, map TFree vs);
+    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
+    fun exprgen_superarity superclass =
+      ensure_class thy algbr funcgr superclass
+      ##>> ensure_classrel thy algbr funcgr (class, superclass)
+      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
+      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
+            (superclass, (classrel, (inst, dss))));
+    fun exprgen_classparam_inst (c, ty) =
+      let
+        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
+        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
+        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
+          o Logic.dest_equals o Thm.prop_of) thm;
+      in
+        ensure_const thy algbr funcgr c
+        ##>> exprgen_const thy algbr funcgr c_ty
+        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
+      end;
+    val stmt_inst =
+      ensure_class thy algbr funcgr class
+      ##>> ensure_tyco thy algbr funcgr tyco
+      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+      ##>> fold_map exprgen_superarity superclasses
+      ##>> fold_map exprgen_classparam_inst classparams
+      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
+             Classinst ((class, (tyco, arity)), (superarities, classparams)));
+    val inst = CodeName.instance thy (class, tyco);
+  in
+    ensure_stmt stmt_inst inst
+  end
+and ensure_const thy (algbr as (_, consts)) funcgr c =
+  let
+    val c' = CodeName.const thy c;
+    fun stmt_datatypecons tyco =
+      ensure_tyco thy algbr funcgr tyco
+      #>> K (Datatypecons c');
+    fun stmt_classparam class =
+      ensure_class thy algbr funcgr class
+      #>> K (Classparam c');
+    fun stmt_fun trns =
+      let
+        val raw_thms = CodeFuncgr.funcs funcgr c;
+        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
+        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
+        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
+          then raw_thms
+          else map (CodeUnit.expand_eta 1) raw_thms;
+      in
+        trns
+        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+        ||>> exprgen_typ thy algbr funcgr ty
+        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
+        |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
+      end;
+    val stmtgen = case Code.get_datatype_of_constr thy c
+     of SOME tyco => stmt_datatypecons tyco
+      | NONE => (case AxClass.class_of_param thy c
+         of SOME class => stmt_classparam class
+          | NONE => stmt_fun)
+  in
+    ensure_stmt stmtgen c'
+  end
+and exprgen_term thy algbr funcgr (Const (c, ty)) =
+      exprgen_app thy algbr funcgr ((c, ty), [])
+  | exprgen_term thy algbr funcgr (Free (v, _)) =
+      pair (IVar v)
+  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
+      let
+        val (v, t) = Syntax.variant_abs abs;
+      in
+        exprgen_typ thy algbr funcgr ty
+        ##>> exprgen_term thy algbr funcgr t
+        #>> (fn (ty, t) => (v, ty) `|-> t)
+      end
+  | exprgen_term thy algbr funcgr (t as _ $ _) =
+      case strip_comb t
+       of (Const (c, ty), ts) =>
+            exprgen_app thy algbr funcgr ((c, ty), ts)
+        | (t', ts) =>
+            exprgen_term thy algbr funcgr t'
+            ##>> fold_map (exprgen_term thy algbr funcgr) ts
+            #>> (fn (t, ts) => t `$$ ts)
+and exprgen_const thy algbr funcgr (c, ty) =
+  ensure_const thy algbr funcgr c
+  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
+  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
+  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
+and exprgen_app_default thy algbr funcgr (c_ty, ts) =
+  exprgen_const thy algbr funcgr c_ty
+  ##>> fold_map (exprgen_term thy algbr funcgr) ts
+  #>> (fn (t, ts) => t `$$ ts)
+and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
+  let
+    val (tys, _) =
+      (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
+    val dt = nth ts n;
+    val dty = nth tys n;
+    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
+      | is_undefined _ = false;
+    fun mk_case (co, n) t =
+      let
+        val (vs, body) = Term.strip_abs_eta n t;
+        val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
+      in if is_undefined body then NONE else SOME (selector, body) end;
+    fun mk_ds [] =
+          let
+            val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
+          in [(Free v_ty, body)] end
+      | mk_ds cases = map_filter (uncurry mk_case)
+          (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
+  in
+    exprgen_term thy algbr funcgr dt
+    ##>> exprgen_typ thy algbr funcgr dty
+    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
+          ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
+    ##>> exprgen_app_default thy algbr funcgr app
+    #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
+  end
+and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
+ of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
+      if length ts < i then
+        let
+          val k = length ts;
+          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
+          val ctxt = (fold o fold_aterms)
+            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
+          val vs = Name.names ctxt "a" tys;
+        in
+          fold_map (exprgen_typ thy algbr funcgr) tys
+          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
+          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
+        end
+      else if length ts > i then
+        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
+        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
+        #>> (fn (t, ts) => t `$$ ts)
+      else
+        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
+      end
+  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
+
+fun ensure_value thy algbr funcgr t = 
+  let
+    val ty = fastype_of t;
+    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
+      o dest_TFree))) t [];
+    val stmt_value =
+      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
+      ##>> exprgen_typ thy algbr funcgr ty
+      ##>> exprgen_term thy algbr funcgr t
+      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
+  in
+    ensure_stmt stmt_value CodeName.value_name
+  end;
+
+fun add_value_stmt (t, ty) code =
   code
-  |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
-  |> fold (curry Graph.add_edge name) (Graph.keys code);
+  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
+  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
 
 end; (*struct*)