118 | prove_row [] = no_tac; |
118 | prove_row [] = no_tac; |
119 |
119 |
120 |
120 |
121 (** Error reporting **) |
121 (** Error reporting **) |
122 |
122 |
123 fun pr_goals ctxt st = |
|
124 Pretty.string_of |
|
125 (Goal_Display.pretty_goal |
|
126 {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st) |
|
127 |
|
128 fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *) |
123 fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *) |
129 fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *) |
124 fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *) |
130 |
125 |
131 fun pr_unprovable_cell _ ((i,j), Less _) = [] |
126 fun pr_unprovable_cell _ ((i,j), Less _) = [] |
132 | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = |
127 | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = |
133 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st] |
128 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
|
129 Goal_Display.string_of_goal ctxt st] |
134 | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = |
130 | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = |
135 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^ |
131 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
136 "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq] |
132 Goal_Display.string_of_goal ctxt st_less ^ |
|
133 "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ |
|
134 Goal_Display.string_of_goal ctxt st_leq] |
137 | pr_unprovable_cell ctxt ((i,j), False st) = |
135 | pr_unprovable_cell ctxt ((i,j), False st) = |
138 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st] |
136 ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ |
|
137 Goal_Display.string_of_goal ctxt st] |
139 |
138 |
140 fun pr_unprovable_subgoals ctxt table = |
139 fun pr_unprovable_subgoals ctxt table = |
141 table |
140 table |
142 |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) |
141 |> map_index (fn (i,cs) => map_index (fn (j,x) => ((i,j), x)) cs) |
143 |> flat |
142 |> flat |