Added second problem with bombs and pacmans: it works!

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;

diff --git a/ocaml/problems.ml b/ocaml/problems.ml
index 15fe980880a155791384577cac5cda70f52d3cba..b604231c89bae9fb0be52c3b78abe940720953d7 100644 (file)
--- a/ocaml/problems.ml
+++ b/ocaml/problems.ml
@@ -336,13 +336,10 @@ let n3 () = magic_conv
 
 (* ************************************************************************** *)
 
-(* let o1 () = magic_conv (Some"BOT") [] [] ["*"];; *)
-
-let o1 () = magic_conv None [] ["x BOT"] ["*"];;
-
 let o1 () = magic_conv None [] ["x a b"; "x (_. BOT) c"] ["*"];;
+let o2 () = magic_conv None [] ["x (y (_. BOT) a) c"; "x (y a PAC) d"] ["*"];;
 
-main [o1() ];;
+main [o1() ; o2() ];;
 
 (* main ([
  p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ;