added Isar syntax for code checking
authorhaftmann
Wed Jul 14 15:49:29 2010 +0200 (2010-07-14)
changeset 37824365e37fe93f3
parent 37823 194a7d543a70
child 37825 adc1143bc1a8
added Isar syntax for code checking
etc/isar-keywords.el
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/Tools/Code/code_target.ML
     1.1 --- a/etc/isar-keywords.el	Wed Jul 14 15:49:29 2010 +0200
     1.2 +++ b/etc/isar-keywords.el	Wed Jul 14 15:49:29 2010 +0200
     1.3 @@ -285,6 +285,7 @@
     1.4      "avoids"
     1.5      "begin"
     1.6      "binder"
     1.7 +    "checking"
     1.8      "congs"
     1.9      "constrains"
    1.10      "contains"
     2.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 15:49:29 2010 +0200
     2.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Wed Jul 14 15:49:29 2010 +0200
     2.3 @@ -10,20 +10,10 @@
     2.4  subsection {* Check whether generated code compiles *}
     2.5  
     2.6  text {*
     2.7 -  If any of the @{text ML} ... check fails, inspect the code generated
     2.8 -  by the previous @{text export_code} command.
     2.9 +  If any of the checks fails, inspect the code generated
    2.10 +  by a corresponding @{text export_code} command.
    2.11  *}
    2.12  
    2.13 -export_code "*" in SML module_name Code_Test file -
    2.14 -ML {* Code_ML.check_SML @{theory} *}
    2.15 -
    2.16 -export_code "*" in OCaml module_name Code_Test file -
    2.17 -ML {* Code_ML.check_OCaml @{theory} *}
    2.18 -
    2.19 -export_code "*" in Haskell module_name Code_Test file -
    2.20 -ML {* Code_Haskell.check @{theory} *}
    2.21 -
    2.22 -export_code "*" in Scala module_name Code_Test file -
    2.23 -ML {* Code_Scala.check @{theory} *}
    2.24 +export_code "*" checking SML OCaml Haskell Scala
    2.25  
    2.26  end
     3.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 15:49:29 2010 +0200
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Wed Jul 14 15:49:29 2010 +0200
     3.3 @@ -15,20 +15,10 @@
     3.4  subsection {* Check whether generated code compiles *}
     3.5  
     3.6  text {*
     3.7 -  If any of the @{text ML} ... check fails, inspect the code generated
     3.8 -  by the previous @{text export_code} command.
     3.9 +  If any of the checks fails, inspect the code generated
    3.10 +  by a corresponding @{text export_code} command.
    3.11  *}
    3.12  
    3.13 -export_code "*" in SML module_name Code_Test file -
    3.14 -ML {* Code_ML.check_SML @{theory} *}
    3.15 -
    3.16 -export_code "*" in OCaml module_name Code_Test file -
    3.17 -ML {* Code_ML.check_OCaml @{theory} *}
    3.18 -
    3.19 -export_code "*" in Haskell module_name Code_Test file -
    3.20 -ML {* Code_Haskell.check @{theory} *}
    3.21 -
    3.22 -export_code "*" in Scala module_name Code_Test file -
    3.23 -ML {* Code_Scala.check @{theory} *}
    3.24 +export_code "*" checking SML OCaml Haskell Scala
    3.25  
    3.26  end
     4.1 --- a/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
     4.2 +++ b/src/Tools/Code/code_target.ML	Wed Jul 14 15:49:29 2010 +0200
     4.3 @@ -36,7 +36,6 @@
     4.4    val string: string list -> serialization -> string
     4.5    val code_of: theory -> string -> int option -> string
     4.6      -> string list -> (Code_Thingol.naming -> string list) -> string
     4.7 -  val check: theory -> string -> unit
     4.8    val set_default_code_width: int -> theory -> theory
     4.9    val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
    4.10  
    4.11 @@ -322,6 +321,27 @@
    4.12  
    4.13  fun serialize thy = mount_serializer thy NONE;
    4.14  
    4.15 +fun check thy names_cs naming program target args =
    4.16 +  let
    4.17 +    val module_name = "Code_Test";
    4.18 +    val { env_var, make_destination, make_command } =
    4.19 +      (#check o the_fundamental thy) target;
    4.20 +    val env_param = getenv env_var;
    4.21 +    fun ext_check env_param p =
    4.22 +      let 
    4.23 +        val destination = make_destination p;
    4.24 +        val _ = file destination (serialize thy target (SOME 80)
    4.25 +          (SOME module_name) args naming program names_cs);
    4.26 +        val cmd = make_command env_param destination module_name;
    4.27 +      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    4.28 +        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    4.29 +        else ()
    4.30 +      end;
    4.31 +  in if env_param = ""
    4.32 +    then warning (env_var ^ " not set; skipped code check for " ^ target)
    4.33 +    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    4.34 +  end;
    4.35 +
    4.36  fun serialize_custom thy (target_name, seri) naming program names =
    4.37    mount_serializer thy (SOME seri) target_name NONE NONE [] naming program names (String [])
    4.38    |> the;
    4.39 @@ -357,41 +377,25 @@
    4.40        if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
    4.41    in union (op =) cs3 cs1 end;
    4.42  
    4.43 -fun check thy target =
    4.44 -  let
    4.45 -    val { env_var, make_destination, make_command } =
    4.46 -      (#check o the_fundamental thy) target;
    4.47 -    val env_param = getenv env_var;
    4.48 -    fun ext_check env_param p =
    4.49 -      let 
    4.50 -        val module_name = "Code_Test";
    4.51 -        val (cs, (naming, program)) =
    4.52 -          Code_Thingol.consts_program thy false (read_const_exprs thy ["*"]);
    4.53 -        val destination = make_destination p;
    4.54 -        val _ = file destination (serialize thy target (SOME 80)
    4.55 -          (SOME module_name) [] naming program cs);
    4.56 -        val cmd = make_command env_param destination module_name;
    4.57 -      in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
    4.58 -        then error ("Code check failed for " ^ target ^ ": " ^ cmd)
    4.59 -        else ()
    4.60 -      end;
    4.61 -  in if env_param = ""
    4.62 -    then warning (env_var ^ " not set; skipped code check for " ^ target)
    4.63 -    else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
    4.64 -  end;
    4.65 -
    4.66 -
    4.67  fun export_code thy cs seris =
    4.68    let
    4.69 -    val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;
    4.70 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    4.71      fun mk_seri_dest dest = if dest = "" orelse dest = "-" then export
    4.72        else file (Path.explode dest);
    4.73      val _ = map (fn (((target, module), dest), args) =>
    4.74 -      (mk_seri_dest dest (serialize thy target NONE module args naming program cs'))) seris;
    4.75 +      (mk_seri_dest dest (serialize thy target NONE module args naming program names_cs))) seris;
    4.76    in () end;
    4.77  
    4.78  fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
    4.79  
    4.80 +fun check_code thy cs seris =
    4.81 +  let
    4.82 +    val (names_cs, (naming, program)) = Code_Thingol.consts_program thy false cs;
    4.83 +    val _ = map (fn (target, args) => check thy names_cs naming program target args) seris;
    4.84 +  in () end;
    4.85 +
    4.86 +fun check_code_cmd raw_cs seris thy = check_code thy (read_const_exprs thy raw_cs) seris;
    4.87 +
    4.88  
    4.89  (** serializer configuration **)
    4.90  
    4.91 @@ -525,17 +529,20 @@
    4.92  
    4.93  (** Isar setup **)
    4.94  
    4.95 -val (inK, module_nameK, fileK) = ("in", "module_name", "file");
    4.96 +val (inK, module_nameK, fileK, checkingK) = ("in", "module_name", "file", "checking");
    4.97 +
    4.98 +val code_expr_argsP = Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") [];
    4.99  
   4.100  val code_exprP =
   4.101 -  (Scan.repeat1 Parse.term_group
   4.102 -  -- Scan.repeat (Parse.$$$ inK |-- Parse.name
   4.103 -     -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   4.104 -     -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   4.105 -     -- Scan.optional (Parse.$$$ "(" |-- Args.parse --| Parse.$$$ ")") []
   4.106 -  ) >> (fn (raw_cs, seris) => export_code_cmd raw_cs seris));
   4.107 +  Scan.repeat1 Parse.term_group :|-- (fn raw_cs =>
   4.108 +    ((Parse.$$$ checkingK |-- Scan.repeat (Parse.name -- code_expr_argsP))
   4.109 +      >> (fn seris => check_code_cmd raw_cs seris)
   4.110 +    || Scan.repeat (Parse.$$$ inK |-- Parse.name
   4.111 +       -- Scan.option (Parse.$$$ module_nameK |-- Parse.name)
   4.112 +       -- Scan.optional (Parse.$$$ fileK |-- Parse.name) ""
   4.113 +       -- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
   4.114  
   4.115 -val _ = List.app Keyword.keyword [inK, module_nameK, fileK];
   4.116 +val _ = List.app Keyword.keyword [inK, module_nameK, fileK, checkingK];
   4.117  
   4.118  val _ =
   4.119    Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (