# HG changeset patch
# User immler
# Date 1474473385 -7200
# Node ID 867ca0d92ea21719bcf2d8dad053987ca5e08a20
# Parent  b673e7221b1650bcae71160e55ffa7fb0679182f
provide more information on error

diff -r b673e7221b16 -r 867ca0d92ea2 src/HOL/Decision_Procs/approximation.ML
--- a/src/HOL/Decision_Procs/approximation.ML	Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML	Wed Sep 21 17:56:25 2016 +0200
@@ -56,10 +56,11 @@
   THEN' resolve_tac ctxt [TrueI]
 
 fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
-    fun lookup_splitting (Free (name, _))
-      = case AList.lookup (op =) splitting name
-        of SOME s => HOLogic.mk_number @{typ nat} s
-         | NONE => @{term "0 :: nat"}
+    fun lookup_splitting (Free (name, _)) =
+        (case AList.lookup (op =) splitting name
+          of SOME s => HOLogic.mk_number @{typ nat} s
+           | NONE => @{term "0 :: nat"})
+      | lookup_splitting t = raise TERM ("lookup_splitting", [t])
     val vs = nth (Thm.prems_of st) (i - 1)
              |> Logic.strip_imp_concl
              |> HOLogic.dest_Trueprop
@@ -116,9 +117,13 @@
 fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
 
+fun dest_interpret_env (@{const "interpret_form"} $ _ $ xs) = xs
+  | dest_interpret_env (@{const "interpret_floatarith"} $ _ $ xs) = xs
+  | dest_interpret_env t = raise TERM ("dest_interpret_env", [t])
 
-fun dest_float (@{const "Float"} $ m $ e) =
-  (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+  | dest_float t = raise TERM ("dest_float", [t])
+
 
 fun dest_ivl (Const (@{const_name "Some"}, _) $
               (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
@@ -137,8 +142,8 @@
   let
     val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0))
 
-    fun frac c p 0 digits cnt = (digits, cnt, 0)
-      | frac c 0 r digits cnt = (digits, cnt, r)
+    fun frac _ _ 0 digits cnt = (digits, cnt, 0)
+      | frac _ 0 r digits cnt = (digits, cnt, r)
       | frac c p r digits cnt = (let
         val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2)
       in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r
@@ -194,8 +199,21 @@
    (put_simpset HOL_basic_ss ctxt addsimps
      (Named_Theorems.get ctxt @{named_theorems approximation_preproc}))
 
-fun reify_form_conv ctxt =
-  (Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps})
+fun reify_form_conv ctxt ct =
+  let
+    val thm =
+       Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps} ct
+       handle ERROR msg =>
+        cat_error ("Reification failed: " ^ msg)
+          ("Approximation does not support " ^
+            quote (Syntax.string_of_term ctxt (Thm.term_of ct)))
+    fun check_env (Free _) = ()
+      | check_env (Var _) = ()
+      | check_env t =
+          cat_error "Term not supported by approximation:" (Syntax.string_of_term ctxt t)
+    val _ = Thm.rhs_of thm |> Thm.term_of |> dest_interpret_env |> HOLogic.dest_list |> map check_env
+  in thm end
+
 
 fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i