evaluator separating static and dynamic operations
authorhaftmann
Tue Dec 21 08:40:39 2010 +0100 (2010-12-21)
changeset 41344d990badc97a3
parent 41343 71f4f15258a5
child 41345 e284a364f724
child 41346 6673f6fa94ca
evaluator separating static and dynamic operations
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_target.ML	Tue Dec 21 08:40:39 2010 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Tue Dec 21 08:40:39 2010 +0100
     1.3 @@ -28,6 +28,10 @@
     1.4    val check_code: theory -> string list
     1.5      -> ((string * bool) * Token.T list) list -> unit
     1.6  
     1.7 +  val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
     1.8 +    -> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
     1.9 +    -> string * string
    1.10 +
    1.11    type serializer
    1.12    type literals = Code_Printer.literals
    1.13    val add_target: string * { serializer: serializer, literals: literals,
    1.14 @@ -353,7 +357,13 @@
    1.15          class instance tyco const module_name args
    1.16            naming (modify naming program) names
    1.17      val width = the_default default_width some_width;
    1.18 -  in prepared_serializer prepared_program width end;
    1.19 +  in (fn program => prepared_serializer program width, prepared_program) end;
    1.20 +
    1.21 +fun invoke_serializer thy target some_width module_name args naming program names =
    1.22 +  let
    1.23 +    val (mounted_serializer, prepared_program) = mount_serializer thy
    1.24 +      target some_width module_name args naming program names;
    1.25 +  in mounted_serializer prepared_program end;
    1.26  
    1.27  fun assert_module_name "" = error ("Empty module name not allowed.")
    1.28    | assert_module_name module_name = module_name;
    1.29 @@ -361,18 +371,18 @@
    1.30  in
    1.31  
    1.32  fun export_code_for thy some_path target some_width module_name args =
    1.33 -  export some_path ooo mount_serializer thy target some_width module_name args;
    1.34 +  export some_path ooo invoke_serializer thy target some_width module_name args;
    1.35  
    1.36  fun produce_code_for thy target some_width module_name args =
    1.37    let
    1.38 -    val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    1.39 +    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
    1.40    in fn naming => fn program => fn names =>
    1.41      produce (serializer naming program names) |> apsnd (fn deresolve => map deresolve names)
    1.42    end;
    1.43  
    1.44  fun present_code_for thy target some_width module_name args =
    1.45    let
    1.46 -    val serializer = mount_serializer thy target some_width (assert_module_name module_name) args;
    1.47 +    val serializer = invoke_serializer thy target some_width (assert_module_name module_name) args;
    1.48    in fn naming => fn program => fn (names, selects) =>
    1.49      present selects (serializer naming program names)
    1.50    end;
    1.51 @@ -386,7 +396,7 @@
    1.52      fun ext_check env_param p =
    1.53        let 
    1.54          val destination = make_destination p;
    1.55 -        val _ = export (SOME destination) (mount_serializer thy target (SOME 80)
    1.56 +        val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
    1.57            module_name args naming program names_cs);
    1.58          val cmd = make_command env_param module_name;
    1.59        in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.60 @@ -400,6 +410,28 @@
    1.61      else Isabelle_System.with_tmp_dir "Code_Test" (ext_check env_param)
    1.62    end;
    1.63  
    1.64 +fun evaluation mounted_serializer prepared_program deps ((vs, ty), t) =
    1.65 +  let
    1.66 +    val _ = if Code_Thingol.contains_dict_var t then
    1.67 +      error "Term to be evaluated contains free dictionaries" else ();
    1.68 +    val v' = Name.variant (map fst vs) "a";
    1.69 +    val vs' = (v', []) :: vs;
    1.70 +    val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty];
    1.71 +    val value_name = "Value.value.value"
    1.72 +    val program = prepared_program
    1.73 +      |> Graph.new_node (value_name,
    1.74 +          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
    1.75 +      |> fold (curry Graph.add_edge value_name) deps;
    1.76 +    val (program_code, deresolve) = produce (mounted_serializer program);
    1.77 +    val value_name' = the (deresolve value_name);
    1.78 +  in (program_code, value_name') end;
    1.79 +
    1.80 +fun evaluator thy target naming program deps =
    1.81 +  let
    1.82 +    val (mounted_serializer, prepared_program) = mount_serializer thy
    1.83 +      target NONE "Code" [] naming program deps;
    1.84 +  in evaluation mounted_serializer prepared_program deps end;
    1.85 +
    1.86  end; (* local *)
    1.87  
    1.88