src/Tools/code/code_target.ML
changeset 24918 22013215eece
parent 24867 e5b55d7be9bb
child 24928 3419943838f5
     1.1 --- a/src/Tools/code/code_target.ML	Mon Oct 08 22:03:30 2007 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Mon Oct 08 22:03:31 2007 +0200
     1.3 @@ -34,14 +34,12 @@
     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
     1.8 -    -> CodeThingol.code -> unit;
     1.9 +    -> string list option -> CodeThingol.code -> unit;
    1.10    val assert_serializer: theory -> string -> string;
    1.11  
    1.12    val eval_verbose: bool ref;
    1.13 -  val eval_invoke: theory -> (theory -> string -> string)
    1.14 -    -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    1.15 -    -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.16 +  val eval_invoke: theory -> (string * (unit -> 'a) option ref)
    1.17 +    -> CodeThingol.code -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    1.18    val code_width: int ref;
    1.19  
    1.20    val setup: theory -> theory;
    1.21 @@ -1632,7 +1630,7 @@
    1.22  val target_diag = "diag";
    1.23  
    1.24  fun get_serializer thy target permissive module file args
    1.25 -    labelled_name = fn cs =>
    1.26 +    = fn cs =>
    1.27    let
    1.28      val (seris, exc) = CodeTargetData.get thy;
    1.29      val data = case Symtab.lookup seris target
    1.30 @@ -1648,28 +1646,26 @@
    1.31      fun check_empty_funs code = case (filter_out (member (op =) exc)
    1.32          (CodeThingol.empty_funs code))
    1.33       of [] => code
    1.34 -      | names => error ("No defining equations for " ^ commas (map (labelled_name thy) names));
    1.35 +      | names => error ("No defining equations for " ^ commas (map (CodeName.labelled_name thy) names));
    1.36    in
    1.37      project
    1.38      #> check_empty_funs
    1.39 -    #> seri module file args (labelled_name thy) reserved (Symtab.lookup alias) (Symtab.lookup prolog)
    1.40 -      (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
    1.41 +    #> seri module file args (CodeName.labelled_name thy) reserved (Symtab.lookup alias)
    1.42 +      (Symtab.lookup prolog) (Symtab.lookup class) (Symtab.lookup tyco) (Symtab.lookup const)
    1.43    end;
    1.44  
    1.45 -fun eval_invoke thy labelled_name (ref_name, reff) code (t, ty) args =
    1.46 +fun eval_invoke thy (ref_name, reff) code (t, ty) args =
    1.47    let
    1.48      val _ = if CodeThingol.contains_dictvar t then
    1.49        error "Term to be evaluated constains free dictionaries" else ();
    1.50 -    val val_name = "Isabelle_Eval.EVAL.EVAL";
    1.51 -    val val_name' = "Isabelle_Eval.EVAL";
    1.52 -    val val_name'_args = space_implode " " (val_name' :: map (enclose "(" ")") args);
    1.53 -    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE []
    1.54 -      labelled_name;
    1.55 +    val val_args = space_implode " "
    1.56 +      (NameSpace.qualifier CodeName.value_name :: map (enclose "(" ")") args);
    1.57 +    val seri = get_serializer thy "SML" false (SOME "Isabelle_Eval") NONE [];
    1.58      fun eval code = (
    1.59        reff := NONE;
    1.60 -      seri (SOME [val_name]) code;
    1.61 +      seri (SOME [CodeName.value_name]) code;
    1.62        use_text "generated code for evaluation" Output.ml_output (!eval_verbose)
    1.63 -        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_name'_args ^ "))");
    1.64 +        ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ val_args ^ "))");
    1.65        case !reff
    1.66         of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name
    1.67              ^ " (reference probably has been shadowed)")
    1.68 @@ -1677,7 +1673,7 @@
    1.69        );
    1.70    in
    1.71      code
    1.72 -    |> CodeThingol.add_eval_def (val_name, (t, ty))
    1.73 +    |> CodeThingol.add_value_stmt (t, ty)
    1.74      |> eval
    1.75    end;
    1.76