Added second problem with bombs and pacmans: it works!

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 927cfe6544fb5c6f4adba3157f6cb855e850059f..8f080d57ef4dbc9a8140ee3c16b50d166a73e514 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -147,6 +147,14 @@ let super_simplify ({div; ps; conv} as p) =
     List.hd divs) div in
   {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv}
 
+let cast_to_ps =
+ function
+    #i_num_var as y -> (y : i_num_var)
+  | `Bottom | `Pacman -> raise (Backtrack "foo")
+  | t ->
+    prerr_endline (print (t :> nf));
+    assert false (* algorithm failed *)
+
 let subst_in_problem x inst ({freshno; div; conv; ps; sigma} as p) =
  let len_ps = List.length ps in
 (*(let l = Array.to_list (Array.init (freshno + 1) string_of_var) in
@@ -195,7 +203,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
          match u with
          | `N i -> acc_new_ps,i
          | _ ->
-            let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
+            let ps = List.map (fun t -> cast_to_ps (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
             let super_simplified_ps = super_simplify_ps ps ps in
 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;