src/Tools/Code/code_target.ML
changeset 37745 6315b6426200
parent 37528 42804fb5dd92
child 37748 0af0d45257be
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Thu Jul 08 16:19:24 2010 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Tools/code/code_target.ML
     1.5 +(*  Title:      Tools/Code/code_target.ML
     1.6      Author:     Florian Haftmann, TU Muenchen
     1.7  
     1.8  Serializer from intermediate language ("Thin-gol") to target languages.
     1.9 @@ -36,6 +36,8 @@
    1.10    val string: string list -> serialization -> string
    1.11    val code_of: theory -> string -> int option -> string
    1.12      -> string list -> (Code_Thingol.naming -> string list) -> string
    1.13 +  val external_check: theory -> string -> string
    1.14 +    -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> Path.T -> unit
    1.15    val set_default_code_width: int -> theory -> theory
    1.16    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.17  
    1.18 @@ -355,6 +357,27 @@
    1.19        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    1.20    in union (op =) cs3 cs1 end;
    1.21  
    1.22 +fun external_check thy target env_var make_destination make_command p =
    1.23 +  let
    1.24 +    val env_param = getenv env_var;
    1.25 +    fun ext_check env_param =
    1.26 +      let 
    1.27 +        val module_name = "Code_Test";
    1.28 +        val (cs, (naming, program)) =
    1.29 +          Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]);
    1.30 +        val destination = make_destination p;
    1.31 +        val _ = file destination (serialize thy target (SOME 80)
    1.32 +          (SOME module_name) [] naming program cs);
    1.33 +        val cmd = make_command env_param destination module_name;
    1.34 +      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd) <> 0
    1.35 +        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.36 +        else ()
    1.37 +      end;
    1.38 +  in if env_param = ""
    1.39 +    then warning (env_var ^ " not set; skipped code check for " ^ target)
    1.40 +    else ext_check env_param
    1.41 +  end;
    1.42 +
    1.43  fun export_code thy cs seris =
    1.44    let
    1.45      val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;