src/Tools/Code/code_target.ML
changeset 37824 365e37fe93f3
parent 37822 cf3588177676
child 37825 adc1143bc1a8
     1.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
     1.3 @@ -36,7 +36,6 @@
     1.4    val string: string list -> serialization -> string
     1.5    val code_of: theory -> string -> int option -> string
     1.6      -> string list -> (Code_Thingol.naming -> string list) -> string
     1.7 -  val check: theory -> string -> unit
     1.8    val set_default_code_width: int -> theory -> theory
     1.9    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    1.10  
    1.11 @@ -322,6 +321,27 @@
    1.12  
    1.13  fun serialize thy = mount_serializer thy NONE;
    1.14  
    1.15 +fun check thy names_cs naming program target args =
    1.16 +  let
    1.17 +    val module_name = "Code_Test";
    1.18 +    val { env_var, make_destination, make_command } =
    1.19 +      (#check o the_fundamental thy) target;
    1.20 +    val env_param = getenv env_var;
    1.21 +    fun ext_check env_param p =
    1.22 +      let 
    1.23 +        val destination = make_destination p;
    1.24 +        val _ = file destination (serialize thy target (SOME 80)
    1.25 +          (SOME module_name) args naming program names_cs);
    1.26 +        val cmd = make_command env_param destination module_name;
    1.27 +      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.28 +        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.29 +        else ()
    1.30 +      end;
    1.31 +  in if env_param = ""
    1.32 +    then warning (env_var ^ " not set; skipped code check for " ^ target)
    1.33 +    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    1.34 +  end;
    1.35 +
    1.36  fun serialize_custom thy (target_name, seri) naming program names =
    1.37    mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
    1.38    |> the;
    1.39 @@ -357,41 +377,25 @@
    1.40        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    1.41    in union (op =) cs3 cs1 end;
    1.42  
    1.43 -fun check thy target =
    1.44 -  let
    1.45 -    val { env_var, make_destination, make_command } =
    1.46 -      (#check o the_fundamental thy) target;
    1.47 -    val env_param = getenv env_var;
    1.48 -    fun ext_check env_param p =
    1.49 -      let 
    1.50 -        val module_name = "Code_Test";
    1.51 -        val (cs, (naming, program)) =
    1.52 -          Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]);
    1.53 -        val destination = make_destination p;
    1.54 -        val _ = file destination (serialize thy target (SOME 80)
    1.55 -          (SOME module_name) [] naming program cs);
    1.56 -        val cmd = make_command env_param destination module_name;
    1.57 -      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    1.58 -        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    1.59 -        else ()
    1.60 -      end;
    1.61 -  in if env_param = ""
    1.62 -    then warning (env_var ^ " not set; skipped code check for " ^ target)
    1.63 -    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    1.64 -  end;
    1.65 -
    1.66 -
    1.67  fun export_code thy cs seris =
    1.68    let
    1.69 -    val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.70 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.71      fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
    1.72        else file (Path.explode dest);
    1.73      val _ = map (fn (((target, module), dest), args) =>
    1.74 -      (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
    1.75 +      (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris;
    1.76    in () end;
    1.77  
    1.78  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
    1.79  
    1.80 +fun check_code thy cs seris =
    1.81 +  let
    1.82 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    1.83 +    val _ = map (fn (target, args) => check thy names_cs naming program target args) seris;
    1.84 +  in () end;
    1.85 +
    1.86 +fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
    1.87 +
    1.88  
    1.89  (** serializer configuration **)
    1.90  
    1.91 @@ -525,17 +529,20 @@
    1.92  
    1.93  (** Isar setup **)
    1.94  
    1.95 -val (inK, module_nameK, fileK) = ("in", "module_name", "file");
    1.96 +val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
    1.97 +
    1.98 +val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
    1.99  
   1.100  val code_exprP =
   1.101 -  (Scan.repeat1 Parse.term_group
   1.102 -  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
   1.103 -     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   1.104 -     -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   1.105 -     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   1.106 -  ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   1.107 +  Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
   1.108 +    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name -- code_expr_argsP))
   1.109 +      >> (fn seris => check_code_cmd raw_cs seris)
   1.110 +    || Scan.repeat (Parse.$$$ inK |-- Parse.name
   1.111 +       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   1.112 +       -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   1.113 +       -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   1.114  
   1.115 -val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
   1.116 +val _ = List.app Keyword.keyword [inK, module_nameK, fileK, checkingK];
   1.117  
   1.118  val _ =
   1.119    Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (