]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Improved error messages
authoracondolu <andrea.condoluci@unibo.it>
Thu, 13 Jul 2017 16:19:33 +0000 (18:19 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Thu, 13 Jul 2017 16:19:33 +0000 (18:19 +0200)
ocaml/lambda4.ml

index 97a559a1799a604bbbade078e6c1c51d4939ddab..e9aa59dce7094eac40af0f8373cdd7410ecfe570 100644 (file)
@@ -46,7 +46,7 @@ let first bound p var f =
    try
     f p i
    with Backtrack s ->
-prerr_endline ("!!BACKTRACK!! " ^ s);
+prerr_endline (">>>>>> BACKTRACK (reason: " ^ s ^") measure=$ ");
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
 prerr_endline("Now trying var="^string_of_var var^" i="^string_of_int i);
      aux (i+1)
@@ -158,7 +158,7 @@ let super_simplify ({div; ps; conv} as p) =
 let cast_to_ps =
  function
     #i_num_var as y -> (y : i_num_var)
-  | `Bottom | `Pacman -> raise (Backtrack "foo")
+  | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps")
   | t ->
     prerr_endline (print (t :> nf));
     assert false (* algorithm failed *)