tuned;
authorwenzelm
Sat Dec 17 13:42:25 2016 +0100 (2016-12-17)
changeset 645787b20f9f94f4e
parent 64577 0288a566c966
child 64579 38a1d8b41189
tuned;
src/HOL/Library/Code_Test.thy
src/HOL/Library/code_test.ML
     1.1 --- a/src/HOL/Library/Code_Test.thy	Sat Dec 17 12:24:13 2016 +0100
     1.2 +++ b/src/HOL/Library/Code_Test.thy	Sat Dec 17 13:42:25 2016 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Library/Code_Test.thy
     1.5 -    Author:     Andreas Lochbihler, ETH Zurich
     1.6 +    Author:     Andreas Lochbihler, ETH Z├╝rich
     1.7  
     1.8 -Test infrastructure for the code generator
     1.9 +Test infrastructure for the code generator.
    1.10  *)
    1.11  
    1.12  theory Code_Test
    1.13 @@ -100,7 +100,7 @@
    1.14    "yxml_string_of_xml_tree (xml.Elem name atts ts) rest =
    1.15     yot_append xml.XY (
    1.16     yot_append (yot_literal name) (
    1.17 -   foldr (\<lambda>(a, x) rest. 
    1.18 +   foldr (\<lambda>(a, x) rest.
    1.19       yot_append xml.Y (
    1.20       yot_append (yot_literal a) (
    1.21       yot_append (yot_literal (STR ''='')) (
     2.1 --- a/src/HOL/Library/code_test.ML	Sat Dec 17 12:24:13 2016 +0100
     2.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 13:42:25 2016 +0100
     2.3 @@ -17,7 +17,7 @@
     2.4    val start_markerN: string
     2.5    val end_markerN: string
     2.6    val test_terms: Proof.context -> term list -> string -> unit
     2.7 -  val test_targets: Proof.context -> term list -> string list -> unit list
     2.8 +  val test_targets: Proof.context -> term list -> string list -> unit
     2.9    val test_code_cmd: string list -> string list -> Toplevel.state -> unit
    2.10  
    2.11    val eval_term: string -> Proof.context -> term -> term
    2.12 @@ -69,9 +69,6 @@
    2.13    | dest_tuples t = [t]
    2.14  
    2.15  
    2.16 -fun map_option _ NONE = NONE
    2.17 -  | map_option f (SOME x) = SOME (f x)
    2.18 -
    2.19  fun last_field sep str =
    2.20    let
    2.21      val n = size sep
    2.22 @@ -191,7 +188,7 @@
    2.23      fun evaluator program _ vs_ty deps =
    2.24        Exn.interruptible_capture evaluate
    2.25          (Code_Target.computation_text ctxt target program deps true vs_ty)
    2.26 -    fun postproc f = map (apsnd (map_option (map f)))
    2.27 +    fun postproc f = map (apsnd (Option.map (map f)))
    2.28    in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
    2.29  
    2.30  
    2.31 @@ -233,15 +230,14 @@
    2.32          @{typ bool} => ()
    2.33        | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)))
    2.34  
    2.35 -    val _ = map ensure_bool ts
    2.36 +    val _ = List.app ensure_bool ts
    2.37  
    2.38      val evals = map (fn t => filter term_of (add_eval t [])) ts
    2.39      val eval = map mk_term_of evals
    2.40  
    2.41 -    val T =
    2.42 -      HOLogic.mk_prodT (@{typ bool},
    2.43 -        Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
    2.44 -    val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
    2.45 +    val t =
    2.46 +      HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
    2.47 +        (map HOLogic.mk_prod (ts ~~ eval))
    2.48  
    2.49      val result = dynamic_value_strict ctxt t target
    2.50  
    2.51 @@ -249,42 +245,44 @@
    2.52        filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
    2.53        handle ListPair.UnequalLengths =>
    2.54          error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
    2.55 -    val _ = case failed of [] => ()
    2.56 -      | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
    2.57    in
    2.58 -    ()
    2.59 +    (case failed of [] =>
    2.60 +      ()
    2.61 +    | _ => error (Pretty.string_of (pretty_failures ctxt target failed)))
    2.62    end
    2.63  
    2.64 -fun test_targets ctxt = map o test_terms ctxt
    2.65 +fun test_targets ctxt = List.app o test_terms ctxt
    2.66  
    2.67  fun test_code_cmd raw_ts targets state =
    2.68    let
    2.69      val ctxt = Toplevel.context_of state
    2.70      val ts = Syntax.read_terms ctxt raw_ts
    2.71      val frees = fold Term.add_free_names ts []
    2.72 -    val _ = if frees = [] then () else
    2.73 -      error ("Terms contain free variables: " ^
    2.74 -      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    2.75 -  in
    2.76 -    test_targets ctxt ts targets; ()
    2.77 -  end
    2.78 +    val _ =
    2.79 +      if null frees then ()
    2.80 +      else error ("Terms contain free variables: " ^
    2.81 +        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    2.82 +  in test_targets ctxt ts targets end
    2.83  
    2.84  fun eval_term target ctxt t =
    2.85    let
    2.86      val frees = Term.add_free_names t []
    2.87 -    val _ = if frees = [] then () else
    2.88 -      error ("Term contains free variables: " ^
    2.89 -      Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    2.90 +    val _ =
    2.91 +      if null frees then ()
    2.92 +      else error ("Term contains free variables: " ^
    2.93 +        Pretty.string_of (Pretty.block (Pretty.commas (map Pretty.str frees))))
    2.94  
    2.95      val thy = Proof_Context.theory_of ctxt
    2.96  
    2.97      val T_t = fastype_of t
    2.98 -    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error
    2.99 -      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
   2.100 +    val _ =
   2.101 +      if Sign.of_sort thy (T_t, @{sort term_of}) then ()
   2.102 +      else error ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
   2.103         " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
   2.104  
   2.105 -    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   2.106 -    val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   2.107 +    val t' =
   2.108 +      HOLogic.mk_list @{typ "bool \<times> (unit \<Rightarrow> yxml_of_term) option"}
   2.109 +        [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   2.110  
   2.111      val result = dynamic_value_strict ctxt t' target
   2.112    in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
   2.113 @@ -298,16 +296,16 @@
   2.114      val _ =
   2.115        if compiler <> "" then ()
   2.116        else error (Pretty.string_of (Pretty.para
   2.117 -         ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   2.118 -         compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
   2.119 +        ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   2.120 +          compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
   2.121  
   2.122      fun compile NONE = ()
   2.123        | compile (SOME cmd) =
   2.124            let
   2.125              val (out, ret) = Isabelle_System.bash_output cmd
   2.126            in
   2.127 -            if ret = 0 then () else error
   2.128 -              ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   2.129 +            if ret = 0 then ()
   2.130 +            else error ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   2.131            end
   2.132  
   2.133      fun run path =
   2.134 @@ -315,15 +313,16 @@
   2.135          val modules = map fst code_files
   2.136          val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
   2.137  
   2.138 -        val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
   2.139 -        val _ = map (fn (name, content) => File.write name content) files
   2.140 +        val _ = List.app (fn (name, code) => File.write (mk_code_file name) code) code_files
   2.141 +        val _ = List.app (fn (name, content) => File.write name content) files
   2.142  
   2.143          val _ = compile compile_cmd
   2.144  
   2.145          val (out, res) = Isabelle_System.bash_output run_cmd
   2.146 -        val _ = if res = 0 then () else error
   2.147 -          ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
   2.148 -           "\nBash output:\n" ^ out)
   2.149 +        val _ =
   2.150 +          if res = 0 then ()
   2.151 +          else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^
   2.152 +            Int.toString res ^ "\nBash output:\n" ^ out)
   2.153        in out end
   2.154    in run end
   2.155