# HG changeset patch
# User haftmann
# Date 1191519709 -7200
# Node ID 8c26128f8997bf13a61d0038e4d57b164f61f09a
# Parent  5684cbf8c89569231ba3568ff7b9ec80cf507462
clarified relationship of code generator conversions and evaluations

diff -r 5684cbf8c895 -r 8c26128f8997 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:41:49 2007 +0200
@@ -136,7 +136,7 @@
 subsection {* Evaluation oracle *}
 
 oracle eval_oracle ("term") = {* fn thy => fn t => 
-  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
+  if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
   then t
   else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
 *}
@@ -156,7 +156,7 @@
 
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
+    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
       THEN' resolve_tac [TrueI, refl]))
 *} "solve goal by normalization"
 
diff -r 5684cbf8c895 -r 8c26128f8997 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Thu Oct 04 19:41:49 2007 +0200
@@ -157,9 +157,10 @@
 signature EVAL =
 sig
   val eval_ref: (unit -> term) option ref
-  val eval_conv: cterm -> thm
-  val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
-  val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
+  val eval_term: theory -> term -> term
+  val evaluate: Proof.context -> term -> unit
+  val evaluate': string -> Proof.context -> term -> unit
+  val evaluate_cmd: string option -> Toplevel.state -> unit
 end;
 
 structure Eval =
@@ -167,61 +168,46 @@
 
 val eval_ref = ref (NONE : (unit -> term) option);
 
-end;
-*}
+fun eval_invoke thy code ((_, ty), t) deps _ =
+  CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
 
-oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
-{* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
-let
-  val _ = (Term.map_types o Term.map_atyps) (fn _ =>
-    error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
-    t0;
-in
-  Logic.mk_equals (t0,
-    CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
-end;
-*}
+fun eval_term thy =
+  TermOf.mk_term_of
+  #> CodePackage.eval_term thy (eval_invoke thy)
+  #> Code.postprocess_term thy;
 
-ML {*
-structure Eval : EVAL =
-struct
-
-open Eval;
-
-fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
+val evaluators = [
+  ("code", eval_term),
+  ("SML", Codegen.eval_term),
+  ("normal_form", Nbe.norm_term)
+];
 
-fun eval_conv ct =
-  let
-    val thy = Thm.theory_of_cterm ct;
-    val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;
-  in
-    CodePackage.eval_term thy
-      (eval_invoke thy (Thm.term_of ct)) ct'
-  end;
-
-fun eval_print conv ctxt t =
+fun gen_evaluate evaluators ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val ct = Thm.cterm_of thy t;
-    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
-    val ty = Term.type_of t';
-    val p = 
-      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
+    val (evls, evl) = split_last evaluators;
+    val t' = case get_first (fn f => try (f thy) t) evls
+     of SOME t' => t'
+      | NONE => evl thy t;
+    val ty' = Term.type_of t';
+    val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
+      Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
+      Pretty.quote (ProofContext.pretty_typ ctxt ty')];
   in Pretty.writeln p end;
 
-fun eval_print_cmd conv raw_t state =
+val evaluate = gen_evaluate (map snd evaluators);
+
+fun evaluate' name = gen_evaluate
+  [(the o AList.lookup (op =) evaluators) name];
+
+fun evaluate_cmd some_name raw_t state =
   let
     val ctxt = Toplevel.context_of state;
     val t = Syntax.read_term ctxt raw_t;
-    val thy = ProofContext.theory_of ctxt;
-    val ct = Thm.cterm_of thy t;
-    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
-    val ty = Term.type_of t';
-    val p = 
-      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
-  in Pretty.writeln p end;
+  in case some_name
+   of NONE => evaluate ctxt t
+    | SOME name => evaluate' name ctxt t
+  end;
 
 end;
 *}
@@ -229,11 +215,10 @@
 ML {*
 val valueP =
   OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
-    (OuterParse.term
-      >> (fn t => Toplevel.no_timing o Toplevel.keep
-           (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
-     of SOME thm => thm
-      | NONE => Codegen.evaluation_conv ct) t)));
+    (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
+    -- OuterParse.term
+      >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
+           (Eval.evaluate_cmd some_name t)));
 
 val _ = OuterSyntax.add_parsers [valueP];
 *}
diff -r 5684cbf8c895 -r 8c26128f8997 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/Library/Eval_Witness.thy	Thu Oct 04 19:41:49 2007 +0200
@@ -57,12 +57,11 @@
     | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
       Abs (v, check_type T, dest_exs (n - 1) b)
     | dest_exs _ _ = sys_error "dest_exs";
-
-  val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal))
+  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
 in
-  if CodePackage.satisfies thy ct ws
+  if CodePackage.satisfies thy t ws
   then goal
-  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
+  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
 end
 *}
 
diff -r 5684cbf8c895 -r 8c26128f8997 src/HOL/ex/Eval_Examples.thy
--- a/src/HOL/ex/Eval_Examples.thy	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/HOL/ex/Eval_Examples.thy	Thu Oct 04 19:41:49 2007 +0200
@@ -27,14 +27,44 @@
 text {* term evaluation *}
 
 value "(Suc 2 + 1) * 4"
-value "(Suc 2 + 1) * 4"
+value (code) "(Suc 2 + 1) * 4"
+value (SML) "(Suc 2 + 1) * 4"
+value ("normal_form") "(Suc 2 + 1) * 4"
+
 value "(Suc 2 + Suc 0) * Suc 3"
+value (code) "(Suc 2 + Suc 0) * Suc 3"
+value (SML) "(Suc 2 + Suc 0) * Suc 3"
+value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
+
 value "nat 100"
+value (code) "nat 100"
+value (SML) "nat 100"
+value ("normal_form") "nat 100"
+
 value "(10\<Colon>int) \<le> 12"
+value (code) "(10\<Colon>int) \<le> 12"
+value (SML) "(10\<Colon>int) \<le> 12"
+value ("normal_form") "(10\<Colon>int) \<le> 12"
+
+value "max (2::int) 4"
+value (code) "max (2::int) 4"
+value (SML) "max (2::int) 4"
+value ("normal_form") "max (2::int) 4"
+
+value "of_int 2 / of_int 4 * (1::rat)"
+(*value (code) "of_int 2 / of_int 4 * (1::rat)" FIXME*)
+value (SML) "of_int 2 / of_int 4 * (1::rat)"
+value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
+
 value "[]::nat list"
+value (code) "[]::nat list"
+(*value (SML) "[]::nat list" FIXME*)
+value ("normal_form") "[]::nat list"
+
 value "[(nat 100, ())]"
-value "max (2::int) 4"
-value "of_int 2 / of_int 4 * (1::rat)"
+value (code) "[(nat 100, ())]"
+(*value (SML) "[(nat 100, ())]" FIXME*)
+value ("normal_form") "[(nat 100, ())]"
 
 
 text {* a fancy datatype *}
@@ -47,5 +77,8 @@
     Cair 'a 'b
 
 value "Shift (Cair (4::nat) [Suc 0])"
+value (code) "Shift (Cair (4::nat) [Suc 0])"
+value (SML) "Shift (Cair (4::nat) [Suc 0])"
+value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
 
 end
diff -r 5684cbf8c895 -r 8c26128f8997 src/Tools/code/code_funcgr.ML
--- a/src/Tools/code/code_funcgr.ML	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML	Thu Oct 04 19:41:49 2007 +0200
@@ -17,7 +17,7 @@
   val make: theory -> string list -> T
   val make_consts: theory -> string list -> string list * T
   val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
-  val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
+  val eval_term: theory -> (T -> term -> 'a) -> term -> 'a
 end
 
 structure CodeFuncgr : CODE_FUNCGR =
@@ -155,7 +155,7 @@
 fun instances_of thy algebra insts =
   let
     val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
-    fun all_classops tyco class =
+    fun all_classparams tyco class =
       try (AxClass.params_of_class thy) class
       |> Option.map snd
       |> these
@@ -164,7 +164,7 @@
     Symtab.empty
     |> fold (fn (tyco, class) =>
         Symtab.map_default (tyco, []) (insert (op =) class)) insts
-    |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco)
+    |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
          (Graph.all_succs thy_classes classes))) tab [])
   end;
 
@@ -320,10 +320,10 @@
       end;
   in raw_eval thy conv' end;
 
-fun raw_eval_term thy f =
+fun raw_eval_term thy f t =
   let
-    fun f' _ _ funcgr ct = f funcgr ct;
-  in raw_eval thy f' end;
+    fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct);
+  in raw_eval thy f' (Thm.cterm_of thy t) end;
 
 end; (*local*)
 
diff -r 5684cbf8c895 -r 8c26128f8997 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Thu Oct 04 16:59:30 2007 +0200
+++ b/src/Tools/code/code_package.ML	Thu Oct 04 19:41:49 2007 +0200
@@ -13,10 +13,10 @@
     -> cterm -> thm;
   val eval_term: theory
     -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
-       -> string list -> cterm -> 'a)
-    -> cterm -> 'a;
+       -> string list -> term -> 'a)
+    -> term -> 'a;
   val satisfies_ref: (unit -> bool) option ref;
-  val satisfies: theory -> cterm -> string list -> bool;
+  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;
@@ -213,20 +213,20 @@
 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, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
+    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 gen_superarity superclass =
+    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 gen_classop_def (c, ty) =
+    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);
@@ -241,10 +241,10 @@
       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 gen_superarity superclasses
-      ##>> fold_map gen_classop_def classops
-      #>> (fn ((((class, tyco), arity), superarities), classops) =>
-             CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classops)));
+      ##>> 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
@@ -256,9 +256,9 @@
     fun defgen_datatypecons tyco =
       ensure_def_tyco thy algbr funcgr tyco
       #>> K (CodeThingol.Datatypecons c');
-    fun defgen_classop class =
+    fun defgen_classparam class =
       ensure_def_class thy algbr funcgr class
-      #>> K (CodeThingol.Classop c');
+      #>> K (CodeThingol.Classparam c');
     fun defgen_fun trns =
       let
         val raw_thms = CodeFuncgr.funcs funcgr c;
@@ -277,14 +277,14 @@
     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_classop class
+         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)) =
-      select_appgen thy algbr funcgr ((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, _))) =
@@ -298,7 +298,7 @@
   | exprgen_term thy algbr funcgr (t as _ $ _) =
       case strip_comb t
        of (Const (c, ty), ts) =>
-            select_appgen thy algbr funcgr ((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
@@ -313,7 +313,7 @@
   exprgen_const thy algbr funcgr c_ty
   ##>> fold_map (exprgen_term thy algbr funcgr) ts
   #>> (fn (t, ts) => t `$$ ts)
-and select_appgen thy algbr funcgr ((c, ty), ts) =
+and exprgen_app thy algbr funcgr ((c, ty), ts) =
   case Symtab.lookup (Appgens.get thy) c
    of SOME (i, (appgen, _)) =>
         if length ts < i then
@@ -430,10 +430,10 @@
     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 (K false) cs) seris;
+        CodeName.labelled_name cs) seris;
   in (map (fn f => f code) seris' : unit list; ()) end;
 
-fun raw_eval f thy g =
+fun raw_eval evaluate term_of thy g =
   let
     val value_name = "Isabelle_Eval.EVAL.EVAL";
     fun ensure_eval thy algbr funcgr t = 
@@ -459,23 +459,23 @@
       end;
     fun h funcgr ct =
       let
-        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
+        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
       in g code vs_ty_t deps ct end;
-  in f thy h end;
+  in evaluate thy h end;
 
-fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
-fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
+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 (K false);
+fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
 
 val satisfies_ref : (unit -> bool) option ref = ref NONE;
 
-fun satisfies thy ct witnesses =
+fun satisfies thy t witnesses =
   let
     fun evl code ((vs, ty), t) deps ct =
       eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
         code (t, ty) witnesses;
-  in eval_term thy evl ct end;
+  in eval_term thy evl t end;
 
 fun filter_generatable thy consts =
   let