src/Tools/code/code_target.ML
changeset 24621 97d403d9ab54
parent 24591 6509626eb2c9
child 24630 351a308ab58d
     1.1 --- a/src/Tools/code/code_target.ML	Tue Sep 18 07:36:11 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Tue Sep 18 07:36:12 2007 +0200
     1.3 @@ -32,12 +32,14 @@
     1.4    type serializer;
     1.5    val add_serializer: string * serializer -> theory -> theory;
     1.6    val get_serializer: theory -> string -> bool -> string option -> string option -> Args.T list
     1.7 -    -> (theory -> string -> string) -> string list option -> CodeThingol.code -> unit;
     1.8 +    -> (theory -> string -> string) -> (string -> bool) -> string list option
     1.9 +    -> CodeThingol.code -> unit;
    1.10    val assert_serializer: theory -> string -> string;
    1.11  
    1.12    val eval_verbose: bool ref;
    1.13 -  val eval_term: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    1.14 -    ->  CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.15 +  val eval_invoke: theory -> (theory -> string -> string) -> (string -> bool)
    1.16 +    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    1.17 +    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.18    val code_width: int ref;
    1.19  
    1.20    val setup: theory -> theory;
    1.21 @@ -300,7 +302,7 @@
    1.22          * ((class * (string * (string * dict list list))) list
    1.23        * (string * const) list));
    1.24  
    1.25 -fun pr_sml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    1.26 +fun pr_sml allows_exception tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    1.27    let
    1.28      val pr_label_classrel = translate_string (fn "." => "__" | c => c) o NameSpace.qualifier;
    1.29      val pr_label_classop = NameSpace.base o NameSpace.qualifier;
    1.30 @@ -569,7 +571,8 @@
    1.31      str ("end; (*struct " ^ name ^ "*)")
    1.32    ]);
    1.33  
    1.34 -fun pr_ocaml tyco_syntax const_syntax labelled_name init_syms deresolv is_cons ml_def =
    1.35 +fun pr_ocaml allows_exception tyco_syntax const_syntax labelled_name
    1.36 +    init_syms deresolv is_cons ml_def =
    1.37    let
    1.38      fun pr_dicts fxy ds =
    1.39        let
    1.40 @@ -858,7 +861,7 @@
    1.41  fun code_output p = Pretty.setmp_margin (!code_width) Pretty.output p ^ "\n";
    1.42  
    1.43  fun seri_ml pr_def pr_modl module output labelled_name reserved_syms raw_module_alias module_prolog
    1.44 -  (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    1.45 +  allows_exception (_ : string -> class_syntax option) tyco_syntax const_syntax code =
    1.46    let
    1.47      val module_alias = if is_some module then K module else raw_module_alias;
    1.48      val is_cons = CodeThingol.is_cons code;
    1.49 @@ -1014,7 +1017,7 @@
    1.50      fun pr_node prefix (Def (_, NONE)) =
    1.51            NONE
    1.52        | pr_node prefix (Def (_, SOME def)) =
    1.53 -          SOME (pr_def tyco_syntax const_syntax labelled_name init_syms
    1.54 +          SOME (pr_def allows_exception tyco_syntax const_syntax labelled_name init_syms
    1.55              (deresolver prefix) is_cons def)
    1.56        | pr_node prefix (Module (dmodlname, (_, nodes))) =
    1.57            SOME (pr_modl dmodlname (the_prolog (NameSpace.implode (prefix @ [dmodlname]))
    1.58 @@ -1064,8 +1067,8 @@
    1.59  
    1.60  in
    1.61  
    1.62 -fun pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
    1.63 -    deresolv_here deresolv is_cons deriving_show def =
    1.64 +fun pr_haskell allows_exception class_syntax tyco_syntax const_syntax labelled_name
    1.65 +    init_syms deresolv_here deresolv is_cons deriving_show def =
    1.66    let
    1.67      fun class_name class = case class_syntax class
    1.68       of NONE => deresolv class
    1.69 @@ -1294,7 +1297,8 @@
    1.70  end; (*local*)
    1.71  
    1.72  fun seri_haskell module_prefix module destination string_classes labelled_name
    1.73 -    reserved_syms raw_module_alias module_prolog class_syntax tyco_syntax const_syntax code =
    1.74 +    reserved_syms raw_module_alias module_prolog
    1.75 +    allows_exception class_syntax tyco_syntax const_syntax code =
    1.76    let
    1.77      val _ = Option.map File.check destination;
    1.78      val is_cons = CodeThingol.is_cons code;
    1.79 @@ -1365,7 +1369,8 @@
    1.80                andalso forall (deriv' tycos) tys
    1.81            | deriv' _ (ITyVar _) = true
    1.82        in deriv [] tyco end;
    1.83 -    fun seri_def qualified = pr_haskell class_syntax tyco_syntax const_syntax labelled_name init_syms
    1.84 +    fun seri_def qualified = pr_haskell allows_exception class_syntax tyco_syntax
    1.85 +      const_syntax labelled_name init_syms
    1.86        deresolv_here (if qualified then deresolv else deresolv_here) is_cons
    1.87        (if string_classes then deriving_show else K false);
    1.88      fun write_module (SOME destination) modlname =
    1.89 @@ -1428,7 +1433,7 @@
    1.90  
    1.91  (** diagnosis serializer **)
    1.92  
    1.93 -fun seri_diagnosis labelled_name _ _ _ _ _ _ code =
    1.94 +fun seri_diagnosis labelled_name _ _ _ _ _ _ _ code =
    1.95    let
    1.96      val init_names = CodeName.make_vars [];
    1.97      fun pr_fun "fun" = SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
    1.98 @@ -1438,7 +1443,7 @@
    1.99              pr_typ (INFX (1, R)) ty2
   1.100            ])
   1.101        | pr_fun _ = NONE
   1.102 -    val pr = pr_haskell (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   1.103 +    val pr = pr_haskell (K true) (K NONE) pr_fun (K NONE) labelled_name init_names I I (K false) (K false);
   1.104    in
   1.105      []
   1.106      |> Graph.fold (fn (name, (def, _)) => case try pr (name, def) of SOME p => cons p | NONE => I) code
   1.107 @@ -1495,6 +1500,7 @@
   1.108    -> string list
   1.109    -> (string -> string option)
   1.110    -> (string -> Pretty.T option)
   1.111 +  -> (string -> bool)
   1.112    -> (string -> class_syntax option)
   1.113    -> (string -> typ_syntax option)
   1.114    -> (string -> term_syntax option)
   1.115 @@ -1570,7 +1576,8 @@
   1.116  val target_Haskell = "Haskell";
   1.117  val target_diag = "diag";
   1.118  
   1.119 -fun get_serializer thy target permissive module file args labelled_name = fn cs =>
   1.120 +fun get_serializer thy target permissive module file args
   1.121 +    labelled_name allows_exception = fn cs =>
   1.122    let
   1.123      val data = case Symtab.lookup (CodeTargetData.get thy) target
   1.124       of SOME data => data
   1.125 @@ -1589,15 +1596,16 @@
   1.126      project
   1.127      #> check_empty_funs
   1.128      #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
   1.129 -      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   1.130 +      allows_exception (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
   1.131    end;
   1.132  
   1.133 -fun eval_term thy (ref_name, reff) code (t, ty) args =
   1.134 +fun eval_invoke thy labelled_name allows_exception (ref_name, reff) code (t, ty) args =
   1.135    let
   1.136      val val_name = "Isabelle_Eval.EVAL.EVAL";
   1.137      val val_name' = "Isabelle_Eval.EVAL";
   1.138      val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
   1.139 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [] CodeName.labelled_name;
   1.140 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
   1.141 +      labelled_name allows_exception;
   1.142      fun eval code = (
   1.143        reff := NONE;
   1.144        seri (SOME [val_name]) code;