src/HOL/Decision_Procs/approximation_generator.ML
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64519 51be997d0698
child 69597 ff784d5a5bfb
permissions -rw-r--r--
executable domain membership checks
     1 (*  Title:      HOL/Decision_Procs/approximation_generator.ML
     2     Author:     Fabian Immler, TU Muenchen
     3 *)
     4 
     5 signature APPROXIMATION_GENERATOR =
     6 sig
     7   val custom_seed: int Config.T
     8   val precision: int Config.T
     9   val epsilon: real Config.T
    10   val approximation_generator:
    11     Proof.context ->
    12     (term * term list) list ->
    13     bool -> int list -> (bool * term list) option * Quickcheck.report option
    14   val setup: theory -> theory
    15 end;
    16 
    17 structure Approximation_Generator : APPROXIMATION_GENERATOR =
    18 struct
    19 
    20 val custom_seed = Attrib.setup_config_int @{binding quickcheck_approximation_custom_seed} (K ~1)
    21 
    22 val precision = Attrib.setup_config_int @{binding quickcheck_approximation_precision} (K 30)
    23 
    24 val epsilon = Attrib.setup_config_real @{binding quickcheck_approximation_epsilon} (K 0.0)
    25 
    26 val random_float = @{code "random_class.random::_ \<Rightarrow> _ \<Rightarrow> (float \<times> (unit \<Rightarrow> term)) \<times> _"}
    27 
    28 fun nat_of_term t =
    29   (HOLogic.dest_nat t handle TERM _ => snd (HOLogic.dest_number t)
    30     handle TERM _ => raise TERM ("nat_of_term", [t]));
    31 
    32 fun int_of_term t = snd (HOLogic.dest_number t) handle TERM _ => raise TERM ("int_of_term", [t]);
    33 
    34 fun real_of_man_exp m e = Real.fromManExp {man = Real.fromInt m, exp = e}
    35 
    36 fun mapprox_float (@{term Float} $ m $ e) = real_of_man_exp (int_of_term m) (int_of_term e)
    37   | mapprox_float t = Real.fromInt (snd (HOLogic.dest_number t))
    38       handle TERM _ => raise TERM ("mapprox_float", [t]);
    39 
    40 (* TODO: define using compiled terms? *)
    41 fun mapprox_floatarith (@{term Add} $ a $ b) xs = mapprox_floatarith a xs + mapprox_floatarith b xs
    42   | mapprox_floatarith (@{term Minus} $ a) xs = ~ (mapprox_floatarith a xs)
    43   | mapprox_floatarith (@{term Mult} $ a $ b) xs = mapprox_floatarith a xs * mapprox_floatarith b xs
    44   | mapprox_floatarith (@{term Inverse} $ a) xs = 1.0 / mapprox_floatarith a xs
    45   | mapprox_floatarith (@{term Cos} $ a) xs = Math.cos (mapprox_floatarith a xs)
    46   | mapprox_floatarith (@{term Arctan} $ a) xs = Math.atan (mapprox_floatarith a xs)
    47   | mapprox_floatarith (@{term Abs} $ a) xs = abs (mapprox_floatarith a xs)
    48   | mapprox_floatarith (@{term Max} $ a $ b) xs =
    49       Real.max (mapprox_floatarith a xs, mapprox_floatarith b xs)
    50   | mapprox_floatarith (@{term Min} $ a $ b) xs =
    51       Real.min (mapprox_floatarith a xs, mapprox_floatarith b xs)
    52   | mapprox_floatarith @{term Pi} _ = Math.pi
    53   | mapprox_floatarith (@{term Sqrt} $ a) xs = Math.sqrt (mapprox_floatarith a xs)
    54   | mapprox_floatarith (@{term Exp} $ a) xs = Math.exp (mapprox_floatarith a xs)
    55   | mapprox_floatarith (@{term Powr} $ a $ b) xs =
    56       Math.pow (mapprox_floatarith a xs, mapprox_floatarith b xs)
    57   | mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
    58   | mapprox_floatarith (@{term Power} $ a $ n) xs =
    59       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
    60   | mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
    61   | mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n)
    62   | mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m
    63   | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
    64 
    65 fun mapprox_atLeastAtMost eps x a b xs =
    66     let
    67       val x' = mapprox_floatarith x xs
    68     in
    69       mapprox_floatarith a xs + eps <= x' andalso x' + eps <= mapprox_floatarith b xs
    70     end
    71 
    72 fun mapprox_form eps (@{term Bound} $ x $ a $ b $ f) xs =
    73     (not (mapprox_atLeastAtMost eps x a b xs)) orelse mapprox_form eps f xs
    74 | mapprox_form eps (@{term Assign} $ x $ a $ f) xs =
    75     (Real.!= (mapprox_floatarith x xs, mapprox_floatarith a xs)) orelse mapprox_form eps f xs
    76 | mapprox_form eps (@{term Less} $ a $ b) xs = mapprox_floatarith a xs + eps < mapprox_floatarith b xs
    77 | mapprox_form eps (@{term LessEqual} $ a $ b) xs = mapprox_floatarith a xs + eps <= mapprox_floatarith b xs
    78 | mapprox_form eps (@{term AtLeastAtMost} $ x $ a $ b) xs = mapprox_atLeastAtMost eps x a b xs
    79 | mapprox_form eps (@{term Conj} $ f $ g) xs = mapprox_form eps f xs andalso mapprox_form eps g xs
    80 | mapprox_form eps (@{term Disj} $ f $ g) xs = mapprox_form eps f xs orelse mapprox_form eps g xs
    81 | mapprox_form _ t _ = raise TERM ("mapprox_form", [t])
    82 
    83 fun dest_interpret_form (@{const "interpret_form"} $ b $ xs) = (b, xs)
    84   | dest_interpret_form t = raise TERM ("dest_interpret_form", [t])
    85 
    86 fun optionT t = Type (@{type_name "option"}, [t])
    87 fun mk_Some t = Const (@{const_name "Some"}, t --> optionT t)
    88 
    89 fun random_float_list size xs seed =
    90   fold (K (apsnd (random_float size) #-> (fn c => apfst (fn b => b::c)))) xs ([],seed)
    91 
    92 fun real_of_Float (@{code Float} (m, e)) =
    93     real_of_man_exp (@{code integer_of_int} m) (@{code integer_of_int} e)
    94 
    95 fun is_True @{term True} = true
    96   | is_True _ = false
    97 
    98 val postproc_form_eqs =
    99   @{lemma
   100     "real_of_float (Float 0 a) = 0"
   101     "real_of_float (Float (numeral m) 0) = numeral m"
   102     "real_of_float (Float 1 0) = 1"
   103     "real_of_float (Float (- 1) 0) = - 1"
   104     "real_of_float (Float 1 (numeral e)) = 2 ^ numeral e"
   105     "real_of_float (Float 1 (- numeral e)) = 1 / 2 ^ numeral e"
   106     "real_of_float (Float a 1) = a * 2"
   107     "real_of_float (Float a (-1)) = a / 2"
   108     "real_of_float (Float (- a) b) = - real_of_float (Float a b)"
   109     "real_of_float (Float (numeral m) (numeral e)) = numeral m * 2 ^ (numeral e)"
   110     "real_of_float (Float (numeral m) (- numeral e)) = numeral m / 2 ^ (numeral e)"
   111     "- (c * d::real) = -c * d"
   112     "- (c / d::real) = -c / d"
   113     "- (0::real) = 0"
   114     "int_of_integer (numeral k) = numeral k"
   115     "int_of_integer (- numeral k) = - numeral k"
   116     "int_of_integer 0 = 0"
   117     "int_of_integer 1 = 1"
   118     "int_of_integer (- 1) = - 1"
   119     by auto
   120   }
   121 
   122 fun rewrite_with ctxt thms = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps thms)
   123 fun conv_term ctxt conv r = Thm.cterm_of ctxt r |> conv |> Thm.prop_of |> Logic.dest_equals |> snd
   124 
   125 fun approx_random ctxt prec eps frees e xs genuine_only size seed =
   126   let
   127     val (rs, seed') = random_float_list size xs seed
   128     fun mk_approx_form e ts =
   129       @{const "approx_form"} $
   130         HOLogic.mk_number @{typ nat} prec $
   131         e $
   132         (HOLogic.mk_list @{typ "(float * float) option"}
   133           (map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $
   134         @{term "[] :: nat list"}
   135   in
   136     (if
   137       mapprox_form eps e (map (real_of_Float o fst) rs)
   138       handle
   139         General.Overflow => false
   140       | General.Domain => false
   141       | General.Div => false
   142       | IEEEReal.Unordered => false
   143     then
   144       let
   145         val ts = map (fn x => snd x ()) rs
   146         val ts' = map
   147           (AList.lookup op = (map dest_Free xs ~~ ts)
   148             #> the_default Term.dummy
   149             #> curry op $ @{term "real_of_float::float\<Rightarrow>_"}
   150             #> conv_term ctxt (rewrite_with ctxt postproc_form_eqs))
   151           frees
   152       in
   153         if Approximation.approximate ctxt (mk_approx_form e ts) |> is_True
   154         then SOME (true, ts')
   155         else (if genuine_only then NONE else SOME (false, ts'))
   156       end
   157     else NONE, seed')
   158   end
   159 
   160 val preproc_form_eqs =
   161   @{lemma
   162     "(a::real) \<in> {b .. c} \<longleftrightarrow> b \<le> a \<and> a \<le> c"
   163     "a = b \<longleftrightarrow> a \<le> b \<and> b \<le> a"
   164     "(p \<longrightarrow> q) \<longleftrightarrow> \<not>p \<or> q"
   165     "(p \<longleftrightarrow> q) \<longleftrightarrow> (p \<longrightarrow> q) \<and> (q \<longrightarrow> p)"
   166     by auto}
   167 
   168 fun reify_goal ctxt t =
   169   HOLogic.mk_not t
   170     |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs)
   171     |> Approximation.reify_form ctxt
   172     |> dest_interpret_form
   173     ||> HOLogic.dest_list
   174 
   175 fun approximation_generator_raw ctxt t =
   176   let
   177     val iterations = Config.get ctxt Quickcheck.iterations
   178     val prec = Config.get ctxt precision
   179     val eps = Config.get ctxt epsilon
   180     val cs = Config.get ctxt custom_seed
   181     val seed = (Code_Numeral.natural_of_integer (cs + 1), Code_Numeral.natural_of_integer 1)
   182     val run = if cs < 0
   183       then (fn f => fn seed => (Random_Engine.run f, seed))
   184       else (fn f => fn seed => f seed)
   185     val frees = Term.add_frees t []
   186     val (e, xs) = reify_goal ctxt t
   187     fun single_tester b s =
   188       approx_random ctxt prec eps frees e xs b s |> run
   189     fun iterate _ _ 0 _ = NONE
   190       | iterate genuine_only size j seed =
   191         case single_tester genuine_only size seed of
   192           (NONE, seed') => iterate genuine_only size (j - 1) seed'
   193         | (SOME q, _) => SOME q
   194   in
   195     fn genuine_only => fn size => (iterate genuine_only size iterations seed, NONE)
   196   end
   197 
   198 fun approximation_generator ctxt [(t, _)] =
   199   (fn genuine_only =>
   200     fn [_, size] =>
   201       approximation_generator_raw ctxt t genuine_only
   202         (Code_Numeral.natural_of_integer size))
   203   | approximation_generator _ _ =
   204       error "Quickcheck-approximation does not support type variables (or finite instantiations)"
   205 
   206 val test_goals =
   207   Quickcheck_Common.generator_test_goal_terms
   208     ("approximation", (fn _ => fn _ => false, approximation_generator))
   209 
   210 val active = Attrib.setup_config_bool @{binding quickcheck_approximation_active} (K false)
   211 
   212 val setup = Context.theory_map (Quickcheck.add_tester ("approximation", (active, test_goals)))
   213 
   214 end