clarified evaluation code
authorhaftmann
Tue Sep 18 07:36:12 2007 +0200 (2007-09-18)
changeset 2462197d403d9ab54
parent 24620 40811901b998
child 24622 8116eb022282
clarified evaluation code
src/HOL/Library/Eval.thy
src/Tools/code/code_package.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:11 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Sep 18 07:36:12 2007 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    fun hook specs =
     1.5      DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac [])
     1.6        (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs)
     1.7 -      [TypOf.class_typ_of] mk ((K o K) (fold (Code.add_func true)))
     1.8 +      [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func))
     1.9  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    1.10  *}
    1.11  
    1.12 @@ -176,7 +176,10 @@
    1.13    val _ = (Term.map_types o Term.map_atyps) (fn _ =>
    1.14      error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
    1.15      t0;
    1.16 -in Logic.mk_equals (t0, CodeTarget.eval_term thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) []) end;
    1.17 +in
    1.18 +  Logic.mk_equals (t0,
    1.19 +    CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
    1.20 +end;
    1.21  *}
    1.22  
    1.23  ML {*
     2.1 --- a/src/Tools/code/code_package.ML	Tue Sep 18 07:36:11 2007 +0200
     2.2 +++ b/src/Tools/code/code_package.ML	Tue Sep 18 07:36:12 2007 +0200
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  signature CODE_PACKAGE =
     2.6  sig
     2.7 -  (*interfaces*)
     2.8    val eval_conv: theory
     2.9      -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
    2.10         -> string list -> cterm -> thm)
    2.11 @@ -18,9 +17,10 @@
    2.12      -> cterm -> 'a;
    2.13    val satisfies_ref: (unit -> bool) option ref;
    2.14    val satisfies: theory -> cterm -> string list -> bool;
    2.15 +  val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    2.16 +    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    2.17    val codegen_command: theory -> string -> unit;
    2.18  
    2.19 -  (*axiomatic interfaces*)
    2.20    type appgen;
    2.21    val add_appconst: string * appgen -> theory -> theory;
    2.22    val appgen_let: appgen;
    2.23 @@ -425,7 +425,7 @@
    2.24      val code = Program.get thy;
    2.25      val seris' = map (fn (((target, module), file), args) =>
    2.26        CodeTarget.get_serializer thy target permissive module file args
    2.27 -        CodeName.labelled_name cs) seris;
    2.28 +        CodeName.labelled_name (K false) cs) seris;
    2.29    in (map (fn f => f code) seris' : unit list; ()) end;
    2.30  
    2.31  fun raw_eval f thy g =
    2.32 @@ -461,6 +461,8 @@
    2.33  fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
    2.34  fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
    2.35  
    2.36 +fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name (K false);
    2.37 +
    2.38  val satisfies_ref : (unit -> bool) option ref = ref NONE;
    2.39  
    2.40  fun satisfies thy ct witnesses =
    2.41 @@ -472,7 +474,7 @@
    2.42            error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
    2.43            t0;
    2.44        in
    2.45 -        CodeTarget.eval_term thy ("CodePackage.satisfies_ref", satisfies_ref)
    2.46 +        eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
    2.47            code (t, ty) witnesses
    2.48        end;
    2.49    in eval_term thy evl ct end;
    2.50 @@ -552,7 +554,7 @@
    2.51      |> Sign.sticky_prefix "codeprop"
    2.52      |> lift_name_yield (fold_map add codeprops)
    2.53      ||> Sign.restore_naming thy
    2.54 -    |-> (fn c_thms => fold (Code.add_func true o snd) c_thms #> pair c_thms)
    2.55 +    |-> (fn c_thms => fold (Code.add_func o snd) c_thms #> pair c_thms)
    2.56    end;
    2.57  
    2.58  
     3.1 --- a/src/Tools/code/code_target.ML	Tue Sep 18 07:36:11 2007 +0200
     3.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 18 07:36:12 2007 +0200
     3.3 @@ -32,12 +32,14 @@
     3.4    type serializer;
     3.5    val add_serializer: string * serializer -> theory -> theory;
     3.6    val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
     3.7 -    -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;
     3.8 +    -> (theory -> string -> string) -> (string -> bool) -> string list option
     3.9 +    -> CodeThingol.code -> unit;
    3.10    val assert_serializer: theory -> string -> string;
    3.11  
    3.12    val eval_verbose: bool ref;
    3.13 -  val eval_term: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    3.14 -    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    3.15 +  val eval_invoke: theory -> (theory -> string -> string) -> (string -> bool)
    3.16 +    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    3.17 +    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    3.18    val code_width: int ref;
    3.19  
    3.20    val setup: theory -> theory;
    3.21 @@ -300,7 +302,7 @@
    3.22          * ((class * (string * (string * dict list list))) list
    3.23        * (string * const) list));
    3.24  
    3.25 -fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    3.26 +fun pr_sml allows_exception tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    3.27    let
    3.28      val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
    3.29      val pr_label_classop = NameSpace.base o NameSpace.qualifier;
    3.30 @@ -569,7 +571,8 @@
    3.31      str ("end; (*struct " ^ name ^ "*)")
    3.32    ]);
    3.33  
    3.34 -fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    3.35 +fun pr_ocaml allows_exception tyco_syntax const_syntax labelled_name
    3.36 +    init_syms deresolv is_cons ml_def =
    3.37    let
    3.38      fun pr_dicts fxy ds =
    3.39        let
    3.40 @@ -858,7 +861,7 @@
    3.41  fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
    3.42  
    3.43  fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
    3.44 -  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    3.45 +  allows_exception (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    3.46    let
    3.47      val module_alias = if is_some module then K module else raw_module_alias;
    3.48      val is_cons = CodeThingol.is_cons code;
    3.49 @@ -1014,7 +1017,7 @@
    3.50      fun pr_node prefix (Def (_, NONE)) =
    3.51            NONE
    3.52        | pr_node prefix (Def (_, SOME def)) =
    3.53 -          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
    3.54 +          SOME (pr_def allows_exception tyco_syntax const_syntax labelled_name init_syms
    3.55              (deresolver prefix) is_cons def)
    3.56        | pr_node prefix (Module (dmodlname, (_, nodes))) =
    3.57            SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
    3.58 @@ -1064,8 +1067,8 @@
    3.59  
    3.60  in
    3.61  
    3.62 -fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
    3.63 -    deresolv_here deresolv is_cons deriving_show def =
    3.64 +fun pr_haskell allows_exception class_syntax tyco_syntax const_syntax labelled_name
    3.65 +    init_syms deresolv_here deresolv is_cons deriving_show def =
    3.66    let
    3.67      fun class_name class = case class_syntax class
    3.68       of NONE => deresolv class
    3.69 @@ -1294,7 +1297,8 @@
    3.70  end; (*local*)
    3.71  
    3.72  fun seri_haskell module_prefix module destination string_classes labelled_name
    3.73 -    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
    3.74 +    reserved_syms raw_module_alias module_prolog
    3.75 +    allows_exception class_syntax tyco_syntax const_syntax code =
    3.76    let
    3.77      val _ = Option.map File.check destination;
    3.78      val is_cons = CodeThingol.is_cons code;
    3.79 @@ -1365,7 +1369,8 @@
    3.80                andalso forall (deriv' tycos) tys
    3.81            | deriv' _ (ITyVar _) = true
    3.82        in deriv [] tyco end;
    3.83 -    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
    3.84 +    fun seri_def qualified = pr_haskell allows_exception class_syntax tyco_syntax
    3.85 +      const_syntax labelled_name init_syms
    3.86        deresolv_here (if qualified then deresolv else deresolv_here) is_cons
    3.87        (if string_classes then deriving_show else K false);
    3.88      fun write_module (SOME destination) modlname =
    3.89 @@ -1428,7 +1433,7 @@
    3.90  
    3.91  (** diagnosis serializer **)
    3.92  
    3.93 -fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
    3.94 +fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code =
    3.95    let
    3.96      val init_names = CodeName.make_vars [];
    3.97      fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
    3.98 @@ -1438,7 +1443,7 @@
    3.99              pr_typ (INFX (1, R)) ty2
   3.100            ])
   3.101        | pr_fun _ = NONE
   3.102 -    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   3.103 +    val pr = pr_haskell (K true) (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   3.104    in
   3.105      []
   3.106      |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
   3.107 @@ -1495,6 +1500,7 @@
   3.108    -> string list
   3.109    -> (string -> string option)
   3.110    -> (string -> Pretty.T option)
   3.111 +  -> (string -> bool)
   3.112    -> (string -> class_syntax option)
   3.113    -> (string -> typ_syntax option)
   3.114    -> (string -> term_syntax option)
   3.115 @@ -1570,7 +1576,8 @@
   3.116  val target_Haskell = "Haskell";
   3.117  val target_diag = "diag";
   3.118  
   3.119 -fun get_serializer thy target permissive module file args labelled_name = fn cs =>
   3.120 +fun get_serializer thy target permissive module file args
   3.121 +    labelled_name allows_exception = fn cs =>
   3.122    let
   3.123      val data = case Symtab.lookup (CodeTargetData.get thy) target
   3.124       of SOME data => data
   3.125 @@ -1589,15 +1596,16 @@
   3.126      project
   3.127      #> check_empty_funs
   3.128      #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
   3.129 -      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   3.130 +      allows_exception (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   3.131    end;
   3.132  
   3.133 -fun eval_term thy (ref_name, reff) code (t, ty) args =
   3.134 +fun eval_invoke thy labelled_name allows_exception (ref_name, reff) code (t, ty) args =
   3.135    let
   3.136      val val_name = "Isabelle_Eval.EVAL.EVAL";
   3.137      val val_name' = "Isabelle_Eval.EVAL";
   3.138      val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
   3.139 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
   3.140 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
   3.141 +      labelled_name allows_exception;
   3.142      fun eval code = (
   3.143        reff := NONE;
   3.144        seri (SOME [val_name]) code;