From: acondolu <andrea.condoluci@unibo.it>
Date: Sun, 23 Jul 2017 20:22:41 +0000 (+0200)
Subject: Check for absence of bombs and pacmans
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b277f630cb63b40ae983282ea81ffefe288d3e8f;p=fireball-separation.git

Check for absence of bombs and pacmans
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 9ab675e..2f6a0a0 100644
--- 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 1822e38..1e630f4 100644
--- 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)))