# HG changeset patch
# User haftmann
# Date 1190093772 -7200
# Node ID 97d403d9ab5414881ffc9214e6a2558fcd69c4f8
# Parent  40811901b998dbe054be98871375d156681713da
clarified evaluation code

diff -r 40811901b998 -r 97d403d9ab54 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:11 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:12 2007 +0200
@@ -55,7 +55,7 @@
   fun hook specs =
     DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
       (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
-      [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
+      [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
 *}
 
@@ -176,7 +176,10 @@
   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, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end;
+in
+  Logic.mk_equals (t0,
+    CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
+end;
 *}
 
 ML {*
diff -r 40811901b998 -r 97d403d9ab54 src/Tools/code/code_package.ML
--- a/src/Tools/code/code_package.ML	Tue Sep 18 07:36:11 2007 +0200
+++ b/src/Tools/code/code_package.ML	Tue Sep 18 07:36:12 2007 +0200
@@ -7,7 +7,6 @@
 
 signature CODE_PACKAGE =
 sig
-  (*interfaces*)
   val eval_conv: theory
     -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
        -> string list -> cterm -> thm)
@@ -18,9 +17,10 @@
     -> cterm -> 'a;
   val satisfies_ref: (unit -> bool) option ref;
   val satisfies: theory -> cterm -> 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;
 
-  (*axiomatic interfaces*)
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
   val appgen_let: appgen;
@@ -425,7 +425,7 @@
     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;
+        CodeName.labelled_name (K false) cs) seris;
   in (map (fn f => f code) seris' : unit list; ()) end;
 
 fun raw_eval f thy g =
@@ -461,6 +461,8 @@
 fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
 fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
 
+fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name (K false);
+
 val satisfies_ref : (unit -> bool) option ref = ref NONE;
 
 fun satisfies thy ct witnesses =
@@ -472,7 +474,7 @@
           error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
           t0;
       in
-        CodeTarget.eval_term thy ("CodePackage.satisfies_ref", satisfies_ref)
+        eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
           code (t, ty) witnesses
       end;
   in eval_term thy evl ct end;
@@ -552,7 +554,7 @@
     |> Sign.sticky_prefix "codeprop"
     |> lift_name_yield (fold_map add codeprops)
     ||> Sign.restore_naming thy
-    |-> (fn c_thms => fold (Code.add_func true o snd) c_thms #> pair c_thms)
+    |-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms)
   end;
 
 
diff -r 40811901b998 -r 97d403d9ab54 src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Tue Sep 18 07:36:11 2007 +0200
+++ b/src/Tools/code/code_target.ML	Tue Sep 18 07:36:12 2007 +0200
@@ -32,12 +32,14 @@
   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;
+    -> (theory -> string -> string) -> (string -> bool) -> string list option
+    -> CodeThingol.code -> unit;
   val assert_serializer: theory -> string -> string;
 
   val eval_verbose: bool ref;
-  val eval_term: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
-    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
+  val eval_invoke: theory -> (theory -> string -> string) -> (string -> bool)
+    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
+    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
   val code_width: int ref;
 
   val setup: theory -> theory;
@@ -300,7 +302,7 @@
         * ((class * (string * (string * dict list list))) list
       * (string * const) list));
 
-fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
+fun pr_sml allows_exception tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
   let
     val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
     val pr_label_classop = NameSpace.base o NameSpace.qualifier;
@@ -569,7 +571,8 @@
     str ("end; (*struct " ^ name ^ "*)")
   ]);
 
-fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
+fun pr_ocaml allows_exception tyco_syntax const_syntax labelled_name
+    init_syms deresolv is_cons ml_def =
   let
     fun pr_dicts fxy ds =
       let
@@ -858,7 +861,7 @@
 fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
 
 fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
-  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
+  allows_exception (_ : string -> class_syntax option) tyco_syntax const_syntax code =
   let
     val module_alias = if is_some module then K module else raw_module_alias;
     val is_cons = CodeThingol.is_cons code;
@@ -1014,7 +1017,7 @@
     fun pr_node prefix (Def (_, NONE)) =
           NONE
       | pr_node prefix (Def (_, SOME def)) =
-          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
+          SOME (pr_def allows_exception tyco_syntax const_syntax labelled_name init_syms
             (deresolver prefix) is_cons def)
       | pr_node prefix (Module (dmodlname, (_, nodes))) =
           SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
@@ -1064,8 +1067,8 @@
 
 in
 
-fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
-    deresolv_here deresolv is_cons deriving_show def =
+fun pr_haskell allows_exception class_syntax tyco_syntax const_syntax labelled_name
+    init_syms deresolv_here deresolv is_cons deriving_show def =
   let
     fun class_name class = case class_syntax class
      of NONE => deresolv class
@@ -1294,7 +1297,8 @@
 end; (*local*)
 
 fun seri_haskell module_prefix module destination string_classes labelled_name
-    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
+    reserved_syms raw_module_alias module_prolog
+    allows_exception class_syntax tyco_syntax const_syntax code =
   let
     val _ = Option.map File.check destination;
     val is_cons = CodeThingol.is_cons code;
@@ -1365,7 +1369,8 @@
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
       in deriv [] tyco end;
-    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
+    fun seri_def qualified = pr_haskell allows_exception class_syntax tyco_syntax
+      const_syntax labelled_name init_syms
       deresolv_here (if qualified then deresolv else deresolv_here) is_cons
       (if string_classes then deriving_show else K false);
     fun write_module (SOME destination) modlname =
@@ -1428,7 +1433,7 @@
 
 (** diagnosis serializer **)
 
-fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
+fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code =
   let
     val init_names = CodeName.make_vars [];
     fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
@@ -1438,7 +1443,7 @@
             pr_typ (INFX (1, R)) ty2
           ])
       | pr_fun _ = NONE
-    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
+    val pr = pr_haskell (K true) (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   in
     []
     |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
@@ -1495,6 +1500,7 @@
   -> string list
   -> (string -> string option)
   -> (string -> Pretty.T option)
+  -> (string -> bool)
   -> (string -> class_syntax option)
   -> (string -> typ_syntax option)
   -> (string -> term_syntax option)
@@ -1570,7 +1576,8 @@
 val target_Haskell = "Haskell";
 val target_diag = "diag";
 
-fun get_serializer thy target permissive module file args labelled_name = fn cs =>
+fun get_serializer thy target permissive module file args
+    labelled_name allows_exception = fn cs =>
   let
     val data = case Symtab.lookup (CodeTargetData.get thy) target
      of SOME data => data
@@ -1589,15 +1596,16 @@
     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)
+      allows_exception (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   end;
 
-fun eval_term thy (ref_name, reff) code (t, ty) args =
+fun eval_invoke thy labelled_name allows_exception (ref_name, reff) code (t, ty) args =
   let
     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 [] CodeName.labelled_name;
+    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
+      labelled_name allows_exception;
     fun eval code = (
       reff := NONE;
       seri (SOME [val_name]) code;