Check for absence of bombs and pacmans

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9ab675e6b95ab242efc8e138d3c62309a92328e7..2f6a0a0fed506d5c82b4974aa87176268f91a298 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -757,23 +757,27 @@ let solve (p, todo) =
        Backtrack _ -> `Unseparable "backtrack"
 ;;
 
+let no_bombs_pacmans p =
+    not (List.exists (eta_subterm `Bottom) (p.ps@p.conv))
+ && not (List.exists (eta_subterm `Pacman) p.ps)
+ && Util.option_map (eta_subterm `Pacman) p.div <> Some true
+;;
+
 let check p =
- (* TODO check if there are duplicates in p.ps
-     before it was: ps = sort_uniq ~compare:eta_compare (ps :> nf list) *)
- (* FIXME what about initial fragments? *)
  if (let rec f = function
      | [] -> false
      | hd::tl -> List.exists (eta_eq hd) tl || f tl in
-   f p.ps)
+   f p.ps) (* FIXME what about initial fragments of numbers? *)
   then `CompleteUnseparable "ps contains duplicates"
  (* check if div occurs somewhere in ps@conv *)
  else if (match p.div with
   | None -> true
   | Some div -> not (List.exists (eta_subterm div) (p.ps@p.conv))
-  ) && false (* TODO no bombs && pacmans *)
+  ) && no_bombs_pacmans p
   then `CompleteSeparable "no bombs, pacmans and div"
- else if false (* TODO bombs or div fuori da lambda in ps@conv *)
-  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv"
+  (* il check seguente e' spostato nel parser e lancia un ParsingError *)
+ (* else if false (* TODO bombs or div fuori da lambda in ps@conv *)
+  then `CompleteUnseparable "bombs or div fuori da lambda in ps@conv" *)
  else if p.div = None
   then `CompleteSeparable "no div"
  else `Uncomplete

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 1822e387386b87a54c725f8513d3e7de6085ab0f..1e630f4c6f43e24ca3e0c8557a8c59b3185cc0e5 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -295,8 +295,8 @@ let eta_compare x y =
   | `Pacman, `Pacman -> 0
   | `Lam _, `N _ -> -1
   | `N _, `Lam _ -> 1
-  | `Bottom, `Lam _
-  | `Lam _, `Bottom -> assert false (* TO BE UNDERSTOOD *)
+  | `Bottom, `Lam(_,t) -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux `Bottom t
+  | `Lam(_,t), `Bottom -> prerr_endline "(* TO BE UNDERSTOOD *)"; aux t `Bottom
   | `Lam(_,t1), `Lam(_,t2) -> aux t1 t2
   | `Lam(_,t1), t2 -> - aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))
   | t2, `Lam(_,t1) ->   aux t1 (mk_app (lift 1 t2) (`Var(0,-666)))