# HG changeset patch
# User krauss
# Date 1182351777 -7200
# Node ID 4a44fcc9dba931619dab1dbd09c0e11a0fd2f4fc
# Parent  343e84195e2cbf4b3718626da8515358cb13ce76
tuned error msg

diff -r 343e84195e2c -r 4a44fcc9dba9 src/HOL/Tools/function_package/lexicographic_order.ML
--- a/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Jun 20 15:10:34 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML	Wed Jun 20 17:02:57 2007 +0200
@@ -36,7 +36,7 @@
 
 (** Matrix cell datatype **)
 
-datatype cell = Less of thm | LessEq of thm | None of thm | False of thm;
+datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
          
 fun is_Less (Less _) = true
   | is_Less _ = false
@@ -45,14 +45,14 @@
   | is_LessEq _ = false
                                                             
 fun thm_of_cell (Less thm) = thm 
-  | thm_of_cell (LessEq thm) = thm 
+  | thm_of_cell (LessEq (thm, _)) = thm 
   | thm_of_cell (False thm) = thm 
-  | thm_of_cell (None thm) = thm 
+  | thm_of_cell (None (thm, _)) = thm 
                   
-fun pr_cell (Less _ ) = " <  "
-  | pr_cell (LessEq _) = " <= " 
-  | pr_cell (None _) = " N  "
-  | pr_cell (False _) = " F  "
+fun pr_cell (Less _ ) = " < "
+  | pr_cell (LessEq _) = " <=" 
+  | pr_cell (None _) = " ? "
+  | pr_cell (False _) = " F "
 
 
 (** Generating Measure Functions **)
@@ -139,10 +139,10 @@
           val lesseq_thm = goals "Orderings.ord_class.less_eq" |> prove thy solve_tac
         in
           if Thm.no_prems lesseq_thm then
-            LessEq (Goal.finish lesseq_thm)
+            LessEq (Goal.finish lesseq_thm, less_thm)
           else 
             if prems_of lesseq_thm = [HOLogic.Trueprop $ HOLogic.false_const] then False lesseq_thm
-            else None lesseq_thm
+            else None (lesseq_thm, less_thm)
         end
     end
 
@@ -211,7 +211,7 @@
 fun prove_row (Less less_thm :: _) =
     (rtac @{thm "measures_less"} 1)
     THEN PRIMITIVE (flip implies_elim less_thm)
-  | prove_row (LessEq lesseq_thm :: tail) =
+  | prove_row (LessEq (lesseq_thm, _) :: tail) =
     (rtac @{thm "measures_lesseq"} 1)
     THEN PRIMITIVE (flip implies_elim lesseq_thm)
     THEN prove_row tail
@@ -222,10 +222,28 @@
 
 fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
        
+fun my_pr_goals st  =
+    Display.pretty_goals_aux (Sign.pp (Thm.theory_of_thm st)) "" (true, false) (Thm.nprems_of st) st
+     |> Pretty.chunks
+     |> Pretty.string_of
+
+fun row_index i = chr (i + 97)
+fun col_index j = string_of_int (j + 1)
+
+fun pr_unprovable_cell ((i,j), Less _) = ""
+  | pr_unprovable_cell ((i,j), LessEq (_, st)) = "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st
+  | pr_unprovable_cell ((i,j), None (st_less, st_leq)) = 
+    "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st_less
+    ^ "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ my_pr_goals st_leq
+  | pr_unprovable_cell ((i,j), False st) = 
+    "(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ my_pr_goals st
+
 fun pr_unprovable_subgoals table =
-    filter_out (fn x => is_Less x orelse is_LessEq x) (flat table)
-    |> map ((fn th => Pretty.string_of (Pretty.chunks (Display.pretty_goals (Thm.nprems_of th) th))) o thm_of_cell)
-    
+    table
+     |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs)
+     |> flat
+     |> map pr_unprovable_cell
+
 fun no_order_msg table thy tl measure_funs =  
     let 
       fun pr_fun t i = string_of_int i ^ ") " ^ string_of_cterm (cterm_of thy t)
@@ -240,13 +258,13 @@
 
       val gc = map (fn i => chr (i + 96)) (1 upto length table)
       val mc = 1 upto length measure_funs
-      val tstr = "   " ^ concat (map (enclose " " " " o string_of_int) mc)
+      val tstr = "Result matrix:" ::  "   " ^ concat (map (enclose " " " " o string_of_int) mc)
                  :: map2 (fn r => fn i => i ^ ": " ^ concat (map pr_cell r)) table gc
-      val gstr = "Calls:" :: map2 pr_goal tl gc
-      val mstr = "Measures:" :: map2 pr_fun measure_funs mc
+      val gstr = "Calls:" :: map2 (prefix "  " oo pr_goal) tl gc
+      val mstr = "Measures:" :: map2 (prefix "  " oo pr_fun) measure_funs mc
       val ustr = "Unfinished subgoals:" :: pr_unprovable_subgoals table
     in
-      cat_lines ("Could not find lexicographic termination order:" :: tstr @ gstr @ mstr @ ustr)
+      cat_lines (ustr @ gstr @ mstr @ tstr @ ["", "Could not find lexicographic termination order."])
     end
       
 (** The Main Function **)