From b277f630cb63b40ae983282ea81ffefe288d3e8f Mon Sep 17 00:00:00 2001 From: acondolu Date: Sun, 23 Jul 2017 22:22:41 +0200 Subject: [PATCH] Check for absence of bombs and pacmans --- ocaml/lambda4.ml | 18 +++++++++++------- ocaml/num.ml | 4 ++-- 2 files changed, 13 insertions(+), 9 deletions(-) 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))) -- 2.39.2