moved translation kernel to CodeThingol
authorhaftmann
Mon Oct 08 22:03:31 2007 +0200 (2007-10-08)
changeset 2491822013215eece
parent 24917 8b97a94ab187
child 24919 ad3a8569759c
moved translation kernel to CodeThingol
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
src/Tools/code/code_thingol.ML
     1.1 --- a/src/Tools/code/code_package.ML	Mon Oct 08 22:03:30 2007 +0200
     1.2 +++ b/src/Tools/code/code_package.ML	Mon Oct 08 22:03:31 2007 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      ID:         $Id$
     1.5      Author:     Florian Haftmann, TU Muenchen
     1.6  
     1.7 -Code generator translation kernel.  Code generator Isar setup.
     1.8 +Code generator interfaces and Isar setup.
     1.9  *)
    1.10  
    1.11  signature CODE_PACKAGE =
    1.12 @@ -17,16 +17,12 @@
    1.13      -> term -> 'a;
    1.14    val satisfies_ref: (unit -> bool) option ref;
    1.15    val satisfies: theory -> term -> string list -> bool;
    1.16 -  val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    1.17 -    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.18    val codegen_command: theory -> string -> unit;
    1.19  end;
    1.20  
    1.21  structure CodePackage : CODE_PACKAGE =
    1.22  struct
    1.23  
    1.24 -open BasicCodeThingol;
    1.25 -
    1.26  (** code theorems **)
    1.27  
    1.28  fun code_depgr thy [] = CodeFuncgr.make thy []
    1.29 @@ -57,7 +53,9 @@
    1.30    in Present.display_graph prgr end;
    1.31  
    1.32  
    1.33 -(** code translation **)
    1.34 +(** code generation interfaces **)
    1.35 +
    1.36 +(* code data *)
    1.37  
    1.38  structure Program = CodeDataFun
    1.39  (
    1.40 @@ -77,300 +75,15 @@
    1.41          in Graph.del_nodes dels code end;
    1.42  );
    1.43  
    1.44 -
    1.45 -(* translation kernel *)
    1.46 -
    1.47 -val value_name = "Isabelle_Eval.EVAL.EVAL";
    1.48 -
    1.49 -fun ensure_def thy = CodeThingol.ensure_def
    1.50 -  (fn s => if s = value_name then "<term>" else CodeName.labelled_name thy s);
    1.51 -
    1.52 -exception CONSTRAIN of (string * typ) * typ;
    1.53 +(* generic generation combinators *)
    1.54  
    1.55 -fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr class =
    1.56 -  let
    1.57 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    1.58 -    val (v, cs) = AxClass.params_of_class thy class;
    1.59 -    val class' = CodeName.class thy class;
    1.60 -    val defgen_class =
    1.61 -      fold_map (fn superclass => ensure_def_class thy algbr funcgr superclass
    1.62 -        ##>> ensure_def_classrel thy algbr funcgr (class, superclass)) superclasses
    1.63 -      ##>> fold_map (fn (c, ty) => ensure_def_const thy algbr funcgr c
    1.64 -        ##>> exprgen_typ thy algbr funcgr ty) cs
    1.65 -      #>> (fn info => CodeThingol.Class (unprefix "'" v, info))
    1.66 -  in
    1.67 -    ensure_def thy defgen_class class'
    1.68 -    #> pair class'
    1.69 -  end
    1.70 -and ensure_def_classrel thy algbr funcgr (subclass, superclass) =
    1.71 -  let
    1.72 -    val classrel' = CodeName.classrel thy (subclass, superclass);
    1.73 -    val defgen_classrel =
    1.74 -      ensure_def_class thy algbr funcgr subclass
    1.75 -      ##>> ensure_def_class thy algbr funcgr superclass
    1.76 -      #>> CodeThingol.Classrel;
    1.77 -  in
    1.78 -    ensure_def thy defgen_classrel classrel'
    1.79 -    #> pair classrel'
    1.80 -  end
    1.81 -and ensure_def_tyco thy algbr funcgr "fun" =
    1.82 -      pair "fun"
    1.83 -  | ensure_def_tyco thy algbr funcgr tyco =
    1.84 -      let
    1.85 -        val defgen_datatype =
    1.86 -          let
    1.87 -            val (vs, cos) = Code.get_datatype thy tyco;
    1.88 -          in
    1.89 -            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    1.90 -            ##>> fold_map (fn (c, tys) =>
    1.91 -              ensure_def_const thy algbr funcgr c
    1.92 -              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
    1.93 -            #>> CodeThingol.Datatype
    1.94 -          end;
    1.95 -        val tyco' = CodeName.tyco thy tyco;
    1.96 -      in
    1.97 -        ensure_def thy defgen_datatype tyco'
    1.98 -        #> pair tyco'
    1.99 -      end
   1.100 -and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
   1.101 -  fold_map (ensure_def_class thy algbr funcgr) (proj_sort sort)
   1.102 -  #>> (fn sort => (unprefix "'" v, sort))
   1.103 -and exprgen_typ thy algbr funcgr (TFree vs) =
   1.104 -      exprgen_tyvar_sort thy algbr funcgr vs
   1.105 -      #>> (fn (v, sort) => ITyVar v)
   1.106 -  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
   1.107 -      ensure_def_tyco thy algbr funcgr tyco
   1.108 -      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
   1.109 -      #>> (fn (tyco, tys) => tyco `%% tys)
   1.110 -and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
   1.111 -  let
   1.112 -    val pp = Sign.pp thy;
   1.113 -    datatype typarg =
   1.114 -        Global of (class * string) * typarg list list
   1.115 -      | Local of (class * class) list * (string * (int * sort));
   1.116 -    fun class_relation (Global ((_, tyco), yss), _) class =
   1.117 -          Global ((class, tyco), yss)
   1.118 -      | class_relation (Local (classrels, v), subclass) superclass =
   1.119 -          Local ((subclass, superclass) :: classrels, v);
   1.120 -    fun type_constructor tyco yss class =
   1.121 -      Global ((class, tyco), (map o map) fst yss);
   1.122 -    fun type_variable (TFree (v, sort)) =
   1.123 -      let
   1.124 -        val sort' = proj_sort sort;
   1.125 -      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
   1.126 -    val typargs = Sorts.of_sort_derivation pp algebra
   1.127 -      {class_relation = class_relation, type_constructor = type_constructor,
   1.128 -       type_variable = type_variable}
   1.129 -      (ty_ctxt, proj_sort sort_decl);
   1.130 -    fun mk_dict (Global (inst, yss)) =
   1.131 -          ensure_def_inst thy algbr funcgr inst
   1.132 -          ##>> (fold_map o fold_map) mk_dict yss
   1.133 -          #>> (fn (inst, dss) => DictConst (inst, dss))
   1.134 -      | mk_dict (Local (classrels, (v, (k, sort)))) =
   1.135 -          fold_map (ensure_def_classrel thy algbr funcgr) classrels
   1.136 -          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   1.137 -  in
   1.138 -    fold_map mk_dict typargs
   1.139 -  end
   1.140 -and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
   1.141 -  let
   1.142 -    val ty_decl = Consts.the_declaration consts c;
   1.143 -    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
   1.144 -    val sorts = map (snd o dest_TVar) tys_decl;
   1.145 -  in
   1.146 -    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
   1.147 -  end
   1.148 -and exprgen_eq thy algbr funcgr thm =
   1.149 -  let
   1.150 -    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   1.151 -      o Logic.unvarify o prop_of) thm;
   1.152 -  in
   1.153 -    fold_map (exprgen_term thy algbr funcgr) args
   1.154 -    ##>> exprgen_term thy algbr funcgr rhs
   1.155 -    #>> rpair thm
   1.156 -  end
   1.157 -and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
   1.158 -  let
   1.159 -    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   1.160 -    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
   1.161 -    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   1.162 -    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   1.163 -    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
   1.164 -      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   1.165 -    val arity_typ = Type (tyco, map TFree vs);
   1.166 -    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
   1.167 -    fun exprgen_superarity superclass =
   1.168 -      ensure_def_class thy algbr funcgr superclass
   1.169 -      ##>> ensure_def_classrel thy algbr funcgr (class, superclass)
   1.170 -      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
   1.171 -      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   1.172 -            (superclass, (classrel, (inst, dss))));
   1.173 -    fun exprgen_classparam_inst (c, ty) =
   1.174 -      let
   1.175 -        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   1.176 -        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
   1.177 -        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   1.178 -          o Logic.dest_equals o Thm.prop_of) thm;
   1.179 -      in
   1.180 -        ensure_def_const thy algbr funcgr c
   1.181 -        ##>> exprgen_const thy algbr funcgr c_ty
   1.182 -        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
   1.183 -      end;
   1.184 -    val defgen_inst =
   1.185 -      ensure_def_class thy algbr funcgr class
   1.186 -      ##>> ensure_def_tyco thy algbr funcgr tyco
   1.187 -      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.188 -      ##>> fold_map exprgen_superarity superclasses
   1.189 -      ##>> fold_map exprgen_classparam_inst classparams
   1.190 -      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
   1.191 -             CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classparams)));
   1.192 -    val inst = CodeName.instance thy (class, tyco);
   1.193 -  in
   1.194 -    ensure_def thy defgen_inst inst
   1.195 -    #> pair inst
   1.196 -  end
   1.197 -and ensure_def_const thy (algbr as (_, consts)) funcgr c =
   1.198 -  let
   1.199 -    val c' = CodeName.const thy c;
   1.200 -    fun defgen_datatypecons tyco =
   1.201 -      ensure_def_tyco thy algbr funcgr tyco
   1.202 -      #>> K (CodeThingol.Datatypecons c');
   1.203 -    fun defgen_classparam class =
   1.204 -      ensure_def_class thy algbr funcgr class
   1.205 -      #>> K (CodeThingol.Classparam c');
   1.206 -    fun defgen_fun trns =
   1.207 -      let
   1.208 -        val raw_thms = CodeFuncgr.funcs funcgr c;
   1.209 -        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
   1.210 -        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
   1.211 -        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   1.212 -          then raw_thms
   1.213 -          else map (CodeUnit.expand_eta 1) raw_thms;
   1.214 -      in
   1.215 -        trns
   1.216 -        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.217 -        ||>> exprgen_typ thy algbr funcgr ty
   1.218 -        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
   1.219 -        |>> (fn ((vs, ty), eqs) => CodeThingol.Fun ((vs, ty), eqs))
   1.220 -      end;
   1.221 -    val defgen = case Code.get_datatype_of_constr thy c
   1.222 -     of SOME tyco => defgen_datatypecons tyco
   1.223 -      | NONE => (case AxClass.class_of_param thy c
   1.224 -         of SOME class => defgen_classparam class
   1.225 -          | NONE => defgen_fun)
   1.226 -  in
   1.227 -    ensure_def thy defgen c'
   1.228 -    #> pair c'
   1.229 -  end
   1.230 -and exprgen_term thy algbr funcgr (Const (c, ty)) =
   1.231 -      exprgen_app thy algbr funcgr ((c, ty), [])
   1.232 -  | exprgen_term thy algbr funcgr (Free (v, _)) =
   1.233 -      pair (IVar v)
   1.234 -  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
   1.235 -      let
   1.236 -        val (v, t) = Syntax.variant_abs abs;
   1.237 -      in
   1.238 -        exprgen_typ thy algbr funcgr ty
   1.239 -        ##>> exprgen_term thy algbr funcgr t
   1.240 -        #>> (fn (ty, t) => (v, ty) `|-> t)
   1.241 -      end
   1.242 -  | exprgen_term thy algbr funcgr (t as _ $ _) =
   1.243 -      case strip_comb t
   1.244 -       of (Const (c, ty), ts) =>
   1.245 -            exprgen_app thy algbr funcgr ((c, ty), ts)
   1.246 -        | (t', ts) =>
   1.247 -            exprgen_term thy algbr funcgr t'
   1.248 -            ##>> fold_map (exprgen_term thy algbr funcgr) ts
   1.249 -            #>> (fn (t, ts) => t `$$ ts)
   1.250 -and exprgen_const thy algbr funcgr (c, ty) =
   1.251 -  ensure_def_const thy algbr funcgr c
   1.252 -  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
   1.253 -  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
   1.254 -  (*##>> exprgen_typ thy algbr funcgr ((snd o Term.strip_type) ty)*)
   1.255 -  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   1.256 -and exprgen_app_default thy algbr funcgr (c_ty, ts) =
   1.257 -  exprgen_const thy algbr funcgr c_ty
   1.258 -  ##>> fold_map (exprgen_term thy algbr funcgr) ts
   1.259 -  #>> (fn (t, ts) => t `$$ ts)
   1.260 -and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
   1.261 -  let
   1.262 -    (*FIXME rework this code*)
   1.263 -    val (all_tys, _) = strip_type ty;
   1.264 -    val (tys, _) = chop (1 + (if null cases then 1 else length cases)) all_tys;
   1.265 -    val st = nth ts n;
   1.266 -    val sty = nth tys n;
   1.267 -    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
   1.268 -      | is_undefined _ = false;
   1.269 -    fun mk_case (co, n) t =
   1.270 -      let
   1.271 -        val (vs, body) = Term.strip_abs_eta n t;
   1.272 -        val selector = list_comb (Const (co, map snd vs ---> sty), map Free vs);
   1.273 -      in if is_undefined body then NONE else SOME (selector, body) end;
   1.274 -    val ds = case cases
   1.275 -     of [] => let val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
   1.276 -          in [(Free v_ty, body)] end
   1.277 -      | cases => map_filter (uncurry mk_case) (AList.make (CodeUnit.no_args thy) cases
   1.278 -          ~~ nth_drop n ts);
   1.279 -  in
   1.280 -    exprgen_term thy algbr funcgr st
   1.281 -    ##>> exprgen_typ thy algbr funcgr sty
   1.282 -    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
   1.283 -          ##>> exprgen_term thy algbr funcgr body) ds
   1.284 -    ##>> exprgen_app_default thy algbr funcgr app
   1.285 -    #>> (fn (((st, sty), ds), t0) => ICase (((st, sty), ds), t0))
   1.286 -  end
   1.287 -and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
   1.288 - of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
   1.289 -      if length ts < i then
   1.290 -        let
   1.291 -          val k = length ts;
   1.292 -          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
   1.293 -          val ctxt = (fold o fold_aterms)
   1.294 -            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   1.295 -          val vs = Name.names ctxt "a" tys;
   1.296 -        in
   1.297 -          fold_map (exprgen_typ thy algbr funcgr) tys
   1.298 -          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
   1.299 -          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   1.300 -        end
   1.301 -      else if length ts > i then
   1.302 -        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
   1.303 -        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   1.304 -        #>> (fn (t, ts) => t `$$ ts)
   1.305 -      else
   1.306 -        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
   1.307 -      end
   1.308 -  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
   1.309 +val ensure_const = CodeThingol.ensure_const;
   1.310  
   1.311 -
   1.312 -(* entrance points into translation kernel *)
   1.313 -
   1.314 -fun ensure_def_const' thy algbr funcgr c trns =
   1.315 -  ensure_def_const thy algbr funcgr c trns
   1.316 -  handle CONSTRAIN ((c, ty), ty_decl) => error (
   1.317 -    "Constant " ^ c ^ " with most general type\n"
   1.318 -    ^ CodeUnit.string_of_typ thy ty
   1.319 -    ^ "\noccurs with type\n"
   1.320 -    ^ CodeUnit.string_of_typ thy ty_decl);
   1.321 -
   1.322 -fun perhaps_def_const thy algbr funcgr c trns =
   1.323 -  case try (ensure_def_const thy algbr funcgr c) trns
   1.324 +fun perhaps_const thy algbr funcgr c trns =
   1.325 +  case try (CodeThingol.ensure_const thy algbr funcgr c) trns
   1.326     of SOME (c, trns) => (SOME c, trns)
   1.327      | NONE => (NONE, trns);
   1.328  
   1.329 -fun exprgen_term' thy algbr funcgr t trns =
   1.330 -  exprgen_term thy algbr funcgr t trns
   1.331 -  handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t
   1.332 -    ^ ",\nconstant " ^ c ^ " with most general type\n"
   1.333 -    ^ CodeUnit.string_of_typ thy ty
   1.334 -    ^ "\noccurs with type\n"
   1.335 -    ^ CodeUnit.string_of_typ thy ty_decl);
   1.336 -
   1.337 -
   1.338 -(** code generation interfaces **)
   1.339 -
   1.340 -(* generic generation combinators *)
   1.341 -
   1.342  fun generate thy funcgr gen it =
   1.343    let
   1.344      val naming = NameSpace.qualified_names NameSpace.default_naming;
   1.345 @@ -380,66 +93,51 @@
   1.346      val algbr = (Code.operational_algebra thy, consttab);
   1.347    in   
   1.348      Program.change_yield thy
   1.349 -      (CodeThingol.start_transact (gen thy algbr funcgr it))
   1.350 -    |> fst
   1.351 +      (CodeThingol.transact (gen thy algbr funcgr it))
   1.352    end;
   1.353  
   1.354  fun code thy permissive cs seris =
   1.355    let
   1.356      val code = Program.get thy;
   1.357      val seris' = map (fn (((target, module), file), args) =>
   1.358 -      CodeTarget.get_serializer thy target permissive module file args
   1.359 -        CodeName.labelled_name cs) seris;
   1.360 +      CodeTarget.get_serializer thy target permissive module file args cs) seris;
   1.361    in (map (fn f => f code) seris' : unit list; ()) end;
   1.362  
   1.363  fun raw_eval evaluate term_of thy g =
   1.364    let
   1.365 -    val value_name = "Isabelle_Eval.EVAL.EVAL";
   1.366 -    fun ensure_eval thy algbr funcgr t = 
   1.367 +    fun result (_, code) =
   1.368        let
   1.369 -        val ty = fastype_of t;
   1.370 -        val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   1.371 -          o dest_TFree))) t [];
   1.372 -        val defgen_eval =
   1.373 -          fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   1.374 -          ##>> exprgen_typ thy algbr funcgr ty
   1.375 -          ##>> exprgen_term' thy algbr funcgr t
   1.376 -          #>> (fn ((vs, ty), t) => CodeThingol.Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
   1.377 -        fun result (dep, code) =
   1.378 -          let
   1.379 -            val CodeThingol.Fun ((vs, ty), [(([], t), _)]) = Graph.get_node code value_name;
   1.380 -            val deps = Graph.imm_succs code value_name;
   1.381 -            val code' = Graph.del_nodes [value_name] code;
   1.382 -            val code'' = CodeThingol.project_code false [] (SOME deps) code';
   1.383 -          in ((code'', ((vs, ty), t), deps), (dep, code')) end;
   1.384 -      in
   1.385 -        ensure_def thy defgen_eval value_name
   1.386 -        #> result
   1.387 -      end;
   1.388 +        val CodeThingol.Fun ((vs, ty), [(([], t), _)]) =
   1.389 +          Graph.get_node code CodeName.value_name;
   1.390 +        val deps = Graph.imm_succs code CodeName.value_name;
   1.391 +        val code' = Graph.del_nodes [CodeName.value_name] code;
   1.392 +        val code'' = CodeThingol.project_code false [] (SOME deps) code';
   1.393 +      in ((code'', ((vs, ty), t), deps), code') end;
   1.394      fun h funcgr ct =
   1.395        let
   1.396 -        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
   1.397 +        val ((code, vs_ty_t, deps), _) = term_of ct
   1.398 +          |> generate thy funcgr CodeThingol.ensure_value
   1.399 +          |> result
   1.400 +          ||> `(fn code' => Program.change thy (K code'));
   1.401        in g code vs_ty_t deps ct end;
   1.402    in evaluate thy h end;
   1.403  
   1.404  fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
   1.405  fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
   1.406  
   1.407 -fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
   1.408 -
   1.409  val satisfies_ref : (unit -> bool) option ref = ref NONE;
   1.410  
   1.411  fun satisfies thy t witnesses =
   1.412    let
   1.413      fun evl code ((vs, ty), t) deps ct =
   1.414 -      eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
   1.415 +      CodeTarget.eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
   1.416          code (t, ty) witnesses;
   1.417    in eval_term thy evl t end;
   1.418  
   1.419  fun filter_generatable thy consts =
   1.420    let
   1.421      val (consts', funcgr) = CodeFuncgr.make_consts thy consts;
   1.422 -    val consts'' = generate thy funcgr (fold_map ooo perhaps_def_const) consts';
   1.423 +    val (consts'', _) = generate thy funcgr (fold_map ooo perhaps_const) consts';
   1.424      val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE)
   1.425        (consts' ~~ consts'');
   1.426    in consts''' end;
   1.427 @@ -449,9 +147,9 @@
   1.428      val (perm1, cs) = CodeUnit.read_const_exprs thy
   1.429        (filter_generatable thy) raw_cs;
   1.430      val (perm2, cs') = case generate thy (CodeFuncgr.make thy cs)
   1.431 -      (fold_map ooo ensure_def_const') cs
   1.432 -     of [] => (true, NONE)
   1.433 -      | cs => (false, SOME cs);
   1.434 +      (fold_map ooo ensure_const) cs
   1.435 +     of ([], _) => (true, NONE)
   1.436 +      | (cs, _) => (false, SOME cs);
   1.437    in (perm1 orelse perm2, cs') end;
   1.438  
   1.439  
   1.440 @@ -515,8 +213,7 @@
   1.441    end;
   1.442  
   1.443  
   1.444 -
   1.445 -(** toplevel interface and setup **)
   1.446 +(** interfaces and Isar setup **)
   1.447  
   1.448  local
   1.449  
   1.450 @@ -542,8 +239,8 @@
   1.451      val (c_thms, thy') = add_codeprops (map (the o CodeName.const_rev thy) (these all_cs))
   1.452        (map (the o CodeName.const_rev thy) (these cs)) thy;
   1.453      val prop_cs = (filter_generatable thy' o map fst) c_thms;
   1.454 -    val _ = if null seris then [] else generate thy' (CodeFuncgr.make thy' prop_cs)
   1.455 -      (fold_map ooo ensure_def_const') prop_cs;
   1.456 +    val _ = if null seris then () else (generate thy' (CodeFuncgr.make thy' prop_cs)
   1.457 +      (fold_map ooo ensure_const) prop_cs; ());
   1.458      val _ = if null seris then () else code thy' permissive
   1.459        (SOME (map (CodeName.const thy') prop_cs)) seris;
   1.460    in thy' end;
     2.1 --- a/src/Tools/code/code_target.ML	Mon Oct 08 22:03:30 2007 +0200
     2.2 +++ b/src/Tools/code/code_target.ML	Mon Oct 08 22:03:31 2007 +0200
     2.3 @@ -34,14 +34,12 @@
     2.4    type serializer;
     2.5    val add_serializer: string * serializer -> theory -> theory;
     2.6    val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
     2.7 -    -> (theory -> string -> string) -> string list option
     2.8 -    -> CodeThingol.code -> unit;
     2.9 +    -> string list option -> CodeThingol.code -> unit;
    2.10    val assert_serializer: theory -> string -> string;
    2.11  
    2.12    val eval_verbose: bool ref;
    2.13 -  val eval_invoke: theory -> (theory -> string -> string)
    2.14 -    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    2.15 -    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    2.16 +  val eval_invoke: theory -> (string * (unit -> 'a) option ref)
    2.17 +    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    2.18    val code_width: int ref;
    2.19  
    2.20    val setup: theory -> theory;
    2.21 @@ -1632,7 +1630,7 @@
    2.22  val target_diag = "diag";
    2.23  
    2.24  fun get_serializer thy target permissive module file args
    2.25 -    labelled_name = fn cs =>
    2.26 +    = fn cs =>
    2.27    let
    2.28      val (seris, exc) = CodeTargetData.get thy;
    2.29      val data = case Symtab.lookup seris target
    2.30 @@ -1648,28 +1646,26 @@
    2.31      fun check_empty_funs code = case (filter_out (member (op =) exc)
    2.32          (CodeThingol.empty_funs code))
    2.33       of [] => code
    2.34 -      | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
    2.35 +      | names => error ("No defining equations for " ^ commas (map (CodeName.labelled_name thy) names));
    2.36    in
    2.37      project
    2.38      #> check_empty_funs
    2.39 -    #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
    2.40 -      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
    2.41 +    #> seri module file args (CodeName.labelled_name thy) reserved (Symtab.lookup alias)
    2.42 +      (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
    2.43    end;
    2.44  
    2.45 -fun eval_invoke thy labelled_name (ref_name, reff) code (t, ty) args =
    2.46 +fun eval_invoke thy (ref_name, reff) code (t, ty) args =
    2.47    let
    2.48      val _ = if CodeThingol.contains_dictvar t then
    2.49        error "Term to be evaluated constains free dictionaries" else ();
    2.50 -    val val_name = "Isabelle_Eval.EVAL.EVAL";
    2.51 -    val val_name' = "Isabelle_Eval.EVAL";
    2.52 -    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
    2.53 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
    2.54 -      labelled_name;
    2.55 +    val val_args = space_implode " "
    2.56 +      (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
    2.57 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
    2.58      fun eval code = (
    2.59        reff := NONE;
    2.60 -      seri (SOME [val_name]) code;
    2.61 +      seri (SOME [CodeName.value_name]) code;
    2.62        use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
    2.63 -        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
    2.64 +        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
    2.65        case !reff
    2.66         of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
    2.67              ^ " (reference probably has been shadowed)")
    2.68 @@ -1677,7 +1673,7 @@
    2.69        );
    2.70    in
    2.71      code
    2.72 -    |> CodeThingol.add_eval_def (val_name, (t, ty))
    2.73 +    |> CodeThingol.add_value_stmt (t, ty)
    2.74      |> eval
    2.75    end;
    2.76  
     3.1 --- a/src/Tools/code/code_thingol.ML	Mon Oct 08 22:03:30 2007 +0200
     3.2 +++ b/src/Tools/code/code_thingol.ML	Mon Oct 08 22:03:31 2007 +0200
     3.3 @@ -3,6 +3,7 @@
     3.4      Author:     Florian Haftmann, TU Muenchen
     3.5  
     3.6  Intermediate language ("Thin-gol") representing executable code.
     3.7 +Representation and translation.
     3.8  *)
     3.9  
    3.10  infix 8 `%%;
    3.11 @@ -58,7 +59,7 @@
    3.12    val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    3.13    val fold_unbound_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
    3.14  
    3.15 -  datatype def =
    3.16 +  datatype stmt =
    3.17        Bot
    3.18      | Fun of typscheme * ((iterm list * iterm) * thm) list
    3.19      | Datatype of (vname * sort) list * (string * itype list) list
    3.20 @@ -69,8 +70,7 @@
    3.21      | Classinst of (class * (string * (vname * sort) list))
    3.22            * ((class * (string * (string * dict list list))) list
    3.23          * ((string * const) * thm) list);
    3.24 -  type code = def Graph.T;
    3.25 -  type transact;
    3.26 +  type code = stmt Graph.T;
    3.27    val empty_code: code;
    3.28    val merge_code: code * code -> code;
    3.29    val project_code: bool (*delete empty funs*)
    3.30 @@ -78,11 +78,14 @@
    3.31      -> code -> code;
    3.32    val empty_funs: code -> string list;
    3.33    val is_cons: code -> string -> bool;
    3.34 -  val add_eval_def: string (*bind name*) * (iterm * itype) -> code -> code;
    3.35  
    3.36 -  val ensure_def: (string -> string) -> (transact -> def * transact) -> string
    3.37 -    -> transact -> transact;
    3.38 -  val start_transact: (transact -> 'a * transact) -> code -> 'a * code;
    3.39 +  type transact;
    3.40 +  val ensure_const: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
    3.41 +    -> CodeFuncgr.T -> string -> transact -> string * transact;
    3.42 +  val ensure_value: theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
    3.43 +    -> CodeFuncgr.T -> term -> transact -> string * transact;
    3.44 +  val add_value_stmt: iterm * itype -> code -> code;
    3.45 +  val transact: (transact -> 'a * transact) -> code -> 'a * code;
    3.46  end;
    3.47  
    3.48  structure CodeThingol: CODE_THINGOL =
    3.49 @@ -245,7 +248,7 @@
    3.50  (** definitions, transactions **)
    3.51  
    3.52  type typscheme = (vname * sort) list * itype;
    3.53 -datatype def =
    3.54 +datatype stmt =
    3.55      Bot
    3.56    | Fun of typscheme * ((iterm list * iterm) * thm) list
    3.57    | Datatype of (vname * sort) list * (string * itype list) list
    3.58 @@ -257,7 +260,7 @@
    3.59          * ((class * (string * (string * dict list list))) list
    3.60        * ((string * const) * thm) list);
    3.61  
    3.62 -type code = def Graph.T;
    3.63 +type code = stmt Graph.T;
    3.64  
    3.65  
    3.66  (* abstract code *)
    3.67 @@ -315,12 +318,12 @@
    3.68  
    3.69  type transact = Graph.key option * code;
    3.70  
    3.71 -fun ensure_def labelled_name defgen name (dep, code) =
    3.72 +fun ensure_stmt stmtgen name (dep, code) =
    3.73    let
    3.74      fun add_def false =
    3.75            ensure_bot name
    3.76            #> add_dep (dep, name)
    3.77 -          #> curry defgen (SOME name)
    3.78 +          #> curry stmtgen (SOME name)
    3.79            ##> snd
    3.80            #-> (fn def => add_def_incr (name, def))
    3.81        | add_def true =
    3.82 @@ -329,17 +332,284 @@
    3.83      code
    3.84      |> add_def (can (Graph.get_node code) name)
    3.85      |> pair dep
    3.86 +    |> pair name
    3.87    end;
    3.88  
    3.89 -fun start_transact f code =
    3.90 +fun transact f code =
    3.91    (NONE, code)
    3.92    |> f
    3.93    |-> (fn x => fn (_, code) => (x, code));
    3.94  
    3.95 -fun add_eval_def (name, (t, ty)) code =
    3.96 +
    3.97 +(* translation kernel *)
    3.98 +
    3.99 +fun ensure_class thy (algbr as ((_, algebra), _)) funcgr class =
   3.100 +  let
   3.101 +    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   3.102 +    val (v, cs) = AxClass.params_of_class thy class;
   3.103 +    val class' = CodeName.class thy class;
   3.104 +    val stmt_class =
   3.105 +      fold_map (fn superclass => ensure_class thy algbr funcgr superclass
   3.106 +        ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
   3.107 +      ##>> fold_map (fn (c, ty) => ensure_const thy algbr funcgr c
   3.108 +        ##>> exprgen_typ thy algbr funcgr ty) cs
   3.109 +      #>> (fn info => Class (unprefix "'" v, info))
   3.110 +  in
   3.111 +    ensure_stmt stmt_class class'
   3.112 +  end
   3.113 +and ensure_classrel thy algbr funcgr (subclass, superclass) =
   3.114 +  let
   3.115 +    val classrel' = CodeName.classrel thy (subclass, superclass);
   3.116 +    val stmt_classrel =
   3.117 +      ensure_class thy algbr funcgr subclass
   3.118 +      ##>> ensure_class thy algbr funcgr superclass
   3.119 +      #>> Classrel;
   3.120 +  in
   3.121 +    ensure_stmt stmt_classrel classrel'
   3.122 +  end
   3.123 +and ensure_tyco thy algbr funcgr "fun" =
   3.124 +      pair "fun"
   3.125 +  | ensure_tyco thy algbr funcgr tyco =
   3.126 +      let
   3.127 +        val stmt_datatype =
   3.128 +          let
   3.129 +            val (vs, cos) = Code.get_datatype thy tyco;
   3.130 +          in
   3.131 +            fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   3.132 +            ##>> fold_map (fn (c, tys) =>
   3.133 +              ensure_const thy algbr funcgr c
   3.134 +              ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
   3.135 +            #>> Datatype
   3.136 +          end;
   3.137 +        val tyco' = CodeName.tyco thy tyco;
   3.138 +      in
   3.139 +        ensure_stmt stmt_datatype tyco'
   3.140 +      end
   3.141 +and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr (v, sort) =
   3.142 +  fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
   3.143 +  #>> (fn sort => (unprefix "'" v, sort))
   3.144 +and exprgen_typ thy algbr funcgr (TFree vs) =
   3.145 +      exprgen_tyvar_sort thy algbr funcgr vs
   3.146 +      #>> (fn (v, sort) => ITyVar v)
   3.147 +  | exprgen_typ thy algbr funcgr (Type (tyco, tys)) =
   3.148 +      ensure_tyco thy algbr funcgr tyco
   3.149 +      ##>> fold_map (exprgen_typ thy algbr funcgr) tys
   3.150 +      #>> (fn (tyco, tys) => tyco `%% tys)
   3.151 +and exprgen_dicts thy (algbr as ((proj_sort, algebra), consts)) funcgr (ty_ctxt, sort_decl) =
   3.152 +  let
   3.153 +    val pp = Sign.pp thy;
   3.154 +    datatype typarg =
   3.155 +        Global of (class * string) * typarg list list
   3.156 +      | Local of (class * class) list * (string * (int * sort));
   3.157 +    fun class_relation (Global ((_, tyco), yss), _) class =
   3.158 +          Global ((class, tyco), yss)
   3.159 +      | class_relation (Local (classrels, v), subclass) superclass =
   3.160 +          Local ((subclass, superclass) :: classrels, v);
   3.161 +    fun type_constructor tyco yss class =
   3.162 +      Global ((class, tyco), (map o map) fst yss);
   3.163 +    fun type_variable (TFree (v, sort)) =
   3.164 +      let
   3.165 +        val sort' = proj_sort sort;
   3.166 +      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
   3.167 +    val typargs = Sorts.of_sort_derivation pp algebra
   3.168 +      {class_relation = class_relation, type_constructor = type_constructor,
   3.169 +       type_variable = type_variable}
   3.170 +      (ty_ctxt, proj_sort sort_decl);
   3.171 +    fun mk_dict (Global (inst, yss)) =
   3.172 +          ensure_inst thy algbr funcgr inst
   3.173 +          ##>> (fold_map o fold_map) mk_dict yss
   3.174 +          #>> (fn (inst, dss) => DictConst (inst, dss))
   3.175 +      | mk_dict (Local (classrels, (v, (k, sort)))) =
   3.176 +          fold_map (ensure_classrel thy algbr funcgr) classrels
   3.177 +          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort))))
   3.178 +  in
   3.179 +    fold_map mk_dict typargs
   3.180 +  end
   3.181 +and exprgen_dict_parms thy (algbr as (_, consts)) funcgr (c, ty_ctxt) =
   3.182 +  let
   3.183 +    val ty_decl = Consts.the_declaration consts c;
   3.184 +    val (tys, tys_decl) = pairself (curry (Consts.typargs consts) c) (ty_ctxt, ty_decl);
   3.185 +    val sorts = map (snd o dest_TVar) tys_decl;
   3.186 +  in
   3.187 +    fold_map (exprgen_dicts thy algbr funcgr) (tys ~~ sorts)
   3.188 +  end
   3.189 +and exprgen_eq thy algbr funcgr thm =
   3.190 +  let
   3.191 +    val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
   3.192 +      o Logic.unvarify o prop_of) thm;
   3.193 +  in
   3.194 +    fold_map (exprgen_term thy algbr funcgr) args
   3.195 +    ##>> exprgen_term thy algbr funcgr rhs
   3.196 +    #>> rpair thm
   3.197 +  end
   3.198 +and ensure_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
   3.199 +  let
   3.200 +    val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
   3.201 +    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
   3.202 +    val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
   3.203 +    val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   3.204 +    val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
   3.205 +      Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   3.206 +    val arity_typ = Type (tyco, map TFree vs);
   3.207 +    val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
   3.208 +    fun exprgen_superarity superclass =
   3.209 +      ensure_class thy algbr funcgr superclass
   3.210 +      ##>> ensure_classrel thy algbr funcgr (class, superclass)
   3.211 +      ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
   3.212 +      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   3.213 +            (superclass, (classrel, (inst, dss))));
   3.214 +    fun exprgen_classparam_inst (c, ty) =
   3.215 +      let
   3.216 +        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   3.217 +        val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
   3.218 +        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
   3.219 +          o Logic.dest_equals o Thm.prop_of) thm;
   3.220 +      in
   3.221 +        ensure_const thy algbr funcgr c
   3.222 +        ##>> exprgen_const thy algbr funcgr c_ty
   3.223 +        #>> (fn (c, IConst c_inst) => ((c, c_inst), thm))
   3.224 +      end;
   3.225 +    val stmt_inst =
   3.226 +      ensure_class thy algbr funcgr class
   3.227 +      ##>> ensure_tyco thy algbr funcgr tyco
   3.228 +      ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   3.229 +      ##>> fold_map exprgen_superarity superclasses
   3.230 +      ##>> fold_map exprgen_classparam_inst classparams
   3.231 +      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
   3.232 +             Classinst ((class, (tyco, arity)), (superarities, classparams)));
   3.233 +    val inst = CodeName.instance thy (class, tyco);
   3.234 +  in
   3.235 +    ensure_stmt stmt_inst inst
   3.236 +  end
   3.237 +and ensure_const thy (algbr as (_, consts)) funcgr c =
   3.238 +  let
   3.239 +    val c' = CodeName.const thy c;
   3.240 +    fun stmt_datatypecons tyco =
   3.241 +      ensure_tyco thy algbr funcgr tyco
   3.242 +      #>> K (Datatypecons c');
   3.243 +    fun stmt_classparam class =
   3.244 +      ensure_class thy algbr funcgr class
   3.245 +      #>> K (Classparam c');
   3.246 +    fun stmt_fun trns =
   3.247 +      let
   3.248 +        val raw_thms = CodeFuncgr.funcs funcgr c;
   3.249 +        val ty = (Logic.unvarifyT o CodeFuncgr.typ funcgr) c;
   3.250 +        val vs = (map dest_TFree o Consts.typargs consts) (c, ty);
   3.251 +        val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
   3.252 +          then raw_thms
   3.253 +          else map (CodeUnit.expand_eta 1) raw_thms;
   3.254 +      in
   3.255 +        trns
   3.256 +        |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   3.257 +        ||>> exprgen_typ thy algbr funcgr ty
   3.258 +        ||>> fold_map (exprgen_eq thy algbr funcgr) thms
   3.259 +        |>> (fn ((vs, ty), eqs) => Fun ((vs, ty), eqs))
   3.260 +      end;
   3.261 +    val stmtgen = case Code.get_datatype_of_constr thy c
   3.262 +     of SOME tyco => stmt_datatypecons tyco
   3.263 +      | NONE => (case AxClass.class_of_param thy c
   3.264 +         of SOME class => stmt_classparam class
   3.265 +          | NONE => stmt_fun)
   3.266 +  in
   3.267 +    ensure_stmt stmtgen c'
   3.268 +  end
   3.269 +and exprgen_term thy algbr funcgr (Const (c, ty)) =
   3.270 +      exprgen_app thy algbr funcgr ((c, ty), [])
   3.271 +  | exprgen_term thy algbr funcgr (Free (v, _)) =
   3.272 +      pair (IVar v)
   3.273 +  | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
   3.274 +      let
   3.275 +        val (v, t) = Syntax.variant_abs abs;
   3.276 +      in
   3.277 +        exprgen_typ thy algbr funcgr ty
   3.278 +        ##>> exprgen_term thy algbr funcgr t
   3.279 +        #>> (fn (ty, t) => (v, ty) `|-> t)
   3.280 +      end
   3.281 +  | exprgen_term thy algbr funcgr (t as _ $ _) =
   3.282 +      case strip_comb t
   3.283 +       of (Const (c, ty), ts) =>
   3.284 +            exprgen_app thy algbr funcgr ((c, ty), ts)
   3.285 +        | (t', ts) =>
   3.286 +            exprgen_term thy algbr funcgr t'
   3.287 +            ##>> fold_map (exprgen_term thy algbr funcgr) ts
   3.288 +            #>> (fn (t, ts) => t `$$ ts)
   3.289 +and exprgen_const thy algbr funcgr (c, ty) =
   3.290 +  ensure_const thy algbr funcgr c
   3.291 +  ##>> exprgen_dict_parms thy algbr funcgr (c, ty)
   3.292 +  ##>> fold_map (exprgen_typ thy algbr funcgr) ((fst o Term.strip_type) ty)
   3.293 +  #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
   3.294 +and exprgen_app_default thy algbr funcgr (c_ty, ts) =
   3.295 +  exprgen_const thy algbr funcgr c_ty
   3.296 +  ##>> fold_map (exprgen_term thy algbr funcgr) ts
   3.297 +  #>> (fn (t, ts) => t `$$ ts)
   3.298 +and exprgen_case thy algbr funcgr n cases (app as ((c, ty), ts)) =
   3.299 +  let
   3.300 +    val (tys, _) =
   3.301 +      (chop (1 + (if null cases then 1 else length cases)) o fst o strip_type) ty;
   3.302 +    val dt = nth ts n;
   3.303 +    val dty = nth tys n;
   3.304 +    fun is_undefined (Const (c, _)) = Code.is_undefined thy c
   3.305 +      | is_undefined _ = false;
   3.306 +    fun mk_case (co, n) t =
   3.307 +      let
   3.308 +        val (vs, body) = Term.strip_abs_eta n t;
   3.309 +        val selector = list_comb (Const (co, map snd vs ---> dty), map Free vs);
   3.310 +      in if is_undefined body then NONE else SOME (selector, body) end;
   3.311 +    fun mk_ds [] =
   3.312 +          let
   3.313 +            val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
   3.314 +          in [(Free v_ty, body)] end
   3.315 +      | mk_ds cases = map_filter (uncurry mk_case)
   3.316 +          (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
   3.317 +  in
   3.318 +    exprgen_term thy algbr funcgr dt
   3.319 +    ##>> exprgen_typ thy algbr funcgr dty
   3.320 +    ##>> fold_map (fn (pat, body) => exprgen_term thy algbr funcgr pat
   3.321 +          ##>> exprgen_term thy algbr funcgr body) (mk_ds cases)
   3.322 +    ##>> exprgen_app_default thy algbr funcgr app
   3.323 +    #>> (fn (((dt, dty), ds), t0) => ICase (((dt, dty), ds), t0))
   3.324 +  end
   3.325 +and exprgen_app thy algbr funcgr ((c, ty), ts) = case Code.get_case_data thy c
   3.326 + of SOME (n, cases) => let val i = 1 + (if null cases then 1 else length cases) in
   3.327 +      if length ts < i then
   3.328 +        let
   3.329 +          val k = length ts;
   3.330 +          val tys = (curry Library.take (i - k) o curry Library.drop k o fst o strip_type) ty;
   3.331 +          val ctxt = (fold o fold_aterms)
   3.332 +            (fn Free (v, _) => Name.declare v | _ => I) ts Name.context;
   3.333 +          val vs = Name.names ctxt "a" tys;
   3.334 +        in
   3.335 +          fold_map (exprgen_typ thy algbr funcgr) tys
   3.336 +          ##>> exprgen_case thy algbr funcgr n cases ((c, ty), ts @ map Free vs)
   3.337 +          #>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t)
   3.338 +        end
   3.339 +      else if length ts > i then
   3.340 +        exprgen_case thy algbr funcgr n cases ((c, ty), Library.take (i, ts))
   3.341 +        ##>> fold_map (exprgen_term thy algbr funcgr) (Library.drop (i, ts))
   3.342 +        #>> (fn (t, ts) => t `$$ ts)
   3.343 +      else
   3.344 +        exprgen_case thy algbr funcgr n cases ((c, ty), ts)
   3.345 +      end
   3.346 +  | NONE => exprgen_app_default thy algbr funcgr ((c, ty), ts);
   3.347 +
   3.348 +fun ensure_value thy algbr funcgr t = 
   3.349 +  let
   3.350 +    val ty = fastype_of t;
   3.351 +    val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
   3.352 +      o dest_TFree))) t [];
   3.353 +    val stmt_value =
   3.354 +      fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
   3.355 +      ##>> exprgen_typ thy algbr funcgr ty
   3.356 +      ##>> exprgen_term thy algbr funcgr t
   3.357 +      #>> (fn ((vs, ty), t) => Fun ((vs, ty), [(([], t), Drule.dummy_thm)]));
   3.358 +  in
   3.359 +    ensure_stmt stmt_value CodeName.value_name
   3.360 +  end;
   3.361 +
   3.362 +fun add_value_stmt (t, ty) code =
   3.363    code
   3.364 -  |> Graph.new_node (name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
   3.365 -  |> fold (curry Graph.add_edge name) (Graph.keys code);
   3.366 +  |> Graph.new_node (CodeName.value_name, Fun (([], ty), [(([], t), Drule.dummy_thm)]))
   3.367 +  |> fold (curry Graph.add_edge CodeName.value_name) (Graph.keys code);
   3.368  
   3.369  end; (*struct*)
   3.370