From 269932207bd455f64c202ee67014f018c18dd4fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ja=CC=81n=20Kl=CC=8Cuka?= Date: Wed, 17 May 2023 01:54:38 +0200 Subject: [PATCH] Fixed and refactored Leibnitz's rule validation Fixes #43 --- src/Validation/Rules/Leibnitz.elm | 347 ++++++++++--------- tests/TestLeibnitz.elm | 545 +++++++++++++++++++++++------- 2 files changed, 593 insertions(+), 299 deletions(-) diff --git a/src/Validation/Rules/Leibnitz.elm b/src/Validation/Rules/Leibnitz.elm index 3ca7b67..207b246 100644 --- a/src/Validation/Rules/Leibnitz.elm +++ b/src/Validation/Rules/Leibnitz.elm @@ -3,29 +3,54 @@ module Validation.Rules.Leibnitz exposing (checkSubsts, commonSignedTemplate, va import Dict import Formula exposing (Formula(..)) import Formula.Signed exposing (Signed(..)) -import Helpers.Rules exposing (signedMap) import Tableau exposing (..) import Term exposing (Term(..)) import Validation.Common exposing (..) import Zipper exposing (Zipper) +templateVar : Term templateVar = Var "[]" -differentStructureError = - Err "The 2nd referenced formula and current formula have different structure" +differentFormulaStructure : Formula -> Formula -> String +differentFormulaStructure refF currentF = + "The 2nd referenced formula and current formula have different structure (" + ++ Formula.toString refF ++ " vs. " + ++ Formula.toString currentF ++ ")" -differentSignError = - Err "The 2nd referenced formula and current formula have different sign" +differentTermStructure : Term -> Term -> String +differentTermStructure refTerm currentTerm = + "The 2nd referenced formula and current formula contain non-matching subterms at corresponding locations (" + ++ Term.toString refTerm ++ " vs. " + ++ Term.toString currentTerm ++ ")" + + +differentArgsCount : String +differentArgsCount = + "Arguments count mismatch" + + +differentArgsCountTo : String -> String -> String +differentArgsCountTo replacementMsg msg = + if msg == differentArgsCount then + replacementMsg + + else + msg + + +differentSign : String +differentSign = + "The 2nd referenced formula and current formula have different sign" isEquality : Signed Formula -> Bool isEquality f = case f of - T (EqAtom lt rt) -> + T (EqAtom _ _) -> True _ -> @@ -35,7 +60,7 @@ isEquality f = leftEqTerm : Signed Formula -> Term leftEqTerm f = case f of - T (EqAtom lt rt) -> + T (EqAtom lt _) -> lt _ -> @@ -45,211 +70,172 @@ leftEqTerm f = rightEqTerm : Signed Formula -> Term rightEqTerm f = case f of - T (EqAtom lt rt) -> + T (EqAtom _ rt) -> rt _ -> Fun "default" [] -commonTermsTemplate : List Term -> List Term -> List Term -commonTermsTemplate refTerms currentTerms = - case refTerms of - [] -> - case currentTerms of - [] -> - [] - - _ -> - List.map (always templateVar) currentTerms - - refTerm :: rts -> - case currentTerms of - [] -> - List.map (always templateVar) refTerms - - currentTerm :: cts -> - commonTermTemplate refTerm currentTerm - :: commonTermsTemplate rts cts - - -commonTermTemplate : Term -> Term -> Term -commonTermTemplate refTerm currentTerm = - case refTerm of - Var refStr -> - case currentTerm of - Var currentStr -> - if refStr /= currentStr then - templateVar - - else - Var refStr - - Fun _ _ -> - templateVar - - Fun refStr refTerms -> - case currentTerm of - Fun currentStr currentTerms -> - if refStr /= currentStr || List.length refTerms /= List.length currentTerms then - templateVar - - else - Fun refStr (commonTermsTemplate refTerms currentTerms) - - Var _ -> - templateVar - - -commonFormulaTemplate : Formula -> Formula -> Result String Formula -commonFormulaTemplate refF currentF = - case refF of - PredAtom refStr refTerms -> - case currentF of - PredAtom currentStr currentTerms -> - Ok - (PredAtom refStr - (commonTermsTemplate refTerms currentTerms) - ) - - _ -> - differentStructureError - - EqAtom refLt refRt -> - case currentF of - EqAtom currentLt currentRt -> - Ok - (EqAtom - (commonTermTemplate refLt currentLt) - (commonTermTemplate refRt currentRt) - ) - - _ -> - differentStructureError - - Neg refSf -> - case currentF of - Neg currentSf -> - Result.map (\f -> Neg f) - (commonFormulaTemplate refSf currentSf) - - _ -> - differentStructureError - - Conj refSf1 refSf2 -> - case currentF of - Conj currentSf1 currentSf2 -> - Result.map2 (\f1 f2 -> Conj f1 f2) - (commonFormulaTemplate refSf1 currentSf1) - (commonFormulaTemplate refSf2 currentSf2) - - _ -> - differentStructureError - - Disj refSf1 refSf2 -> - case currentF of - Disj currentSf1 currentSf2 -> - Result.map2 (\f1 f2 -> Disj f1 f2) - (commonFormulaTemplate refSf1 currentSf1) - (commonFormulaTemplate refSf2 currentSf2) - - _ -> - differentStructureError - - Impl refSf1 refSf2 -> - case currentF of - Impl currentSf1 currentSf2 -> - Result.map2 (\f1 f2 -> Impl f1 f2) - (commonFormulaTemplate refSf1 currentSf1) - (commonFormulaTemplate refSf2 currentSf2) - - _ -> - differentStructureError - - Equiv refSf1 refSf2 -> - case currentF of - Equiv currentSf1 currentSf2 -> - Result.map2 (\f1 f2 -> Equiv f1 f2) - (commonFormulaTemplate refSf1 currentSf1) - (commonFormulaTemplate refSf2 currentSf2) - - _ -> - differentStructureError - - ForAll refX refSf -> - case currentF of - ForAll currentX currentSf -> - Result.map (\f -> ForAll refX f) - (commonFormulaTemplate refSf currentSf) - - _ -> - differentStructureError - - Exists refX refSf -> - case currentF of - Exists currentX currentSf -> - Result.map (\f -> Exists refX f) - (commonFormulaTemplate refSf currentSf) - - _ -> - differentStructureError +commonTermsTemplate : Term -> Term -> List Term -> List Term -> Result String (List Term) +commonTermsTemplate lTerm rTerm refTerms currentTerms = + case (refTerms, currentTerms) of + (refTerm :: rts, currentTerm :: cts) -> + Result.map2 (::) + (commonTermTemplate lTerm rTerm refTerm currentTerm) + (commonTermsTemplate lTerm rTerm rts cts) + + ([], []) -> + Ok <| [] _ -> - Err "wrong formula type" + Err differentArgsCount + + +commonTermTemplate : Term -> Term -> Term -> Term -> Result String Term +commonTermTemplate lTerm rTerm refTerm currentTerm = + if refTerm == lTerm && currentTerm == rTerm then + Ok templateVar + else + case (refTerm, currentTerm) of + (Var refVSym, Var currentVSym) -> + if refVSym == currentVSym then + Ok <| Var refVSym + + else + Err <| differentTermStructure refTerm currentTerm + + (Fun refFSym refTerms, Fun currentFSym currentTerms) -> + if refFSym == currentFSym + && List.length refTerms == List.length currentTerms then + commonTermsTemplate lTerm rTerm refTerms currentTerms + |> Result.map (Fun refFSym) + |> Result.mapError + (differentArgsCountTo <| + differentTermStructure refTerm currentTerm) + + else + Err <| differentTermStructure refTerm currentTerm + + _ -> + Err <| differentTermStructure refTerm currentTerm + + +commonFormulaTemplate : Term -> Term -> Formula -> Formula -> Result String Formula +commonFormulaTemplate lTerm rTerm refF currentF = + case (refF, currentF) of + (PredAtom refPSym refTerms, PredAtom currentPSym currentTerms) -> + if refPSym == currentPSym + && List.length refTerms == List.length currentTerms then + commonTermsTemplate lTerm rTerm refTerms currentTerms + |> Result.map (PredAtom refPSym) + |> Result.mapError + (differentArgsCountTo <| + differentFormulaStructure refF currentF) + + else + Err <| differentFormulaStructure refF currentF + + (EqAtom refLt refRt, EqAtom currentLt currentRt) -> + Result.map2 EqAtom + (commonTermTemplate lTerm rTerm refLt currentLt) + (commonTermTemplate lTerm rTerm refRt currentRt) + + (Neg refSf, Neg currentSf) -> + Result.map Neg + (commonFormulaTemplate lTerm rTerm refSf currentSf) + + (Conj refSf1 refSf2, Conj currentSf1 currentSf2) -> + Result.map2 Conj + (commonFormulaTemplate lTerm rTerm refSf1 currentSf1) + (commonFormulaTemplate lTerm rTerm refSf2 currentSf2) + + (Disj refSf1 refSf2, Disj currentSf1 currentSf2) -> + Result.map2 Disj + (commonFormulaTemplate lTerm rTerm refSf1 currentSf1) + (commonFormulaTemplate lTerm rTerm refSf2 currentSf2) + + (Impl refSf1 refSf2, Impl currentSf1 currentSf2) -> + Result.map2 Impl + (commonFormulaTemplate lTerm rTerm refSf1 currentSf1) + (commonFormulaTemplate lTerm rTerm refSf2 currentSf2) + + (Equiv refSf1 refSf2, Equiv currentSf1 currentSf2) -> + Result.map2 Equiv + (commonFormulaTemplate lTerm rTerm refSf1 currentSf1) + (commonFormulaTemplate lTerm rTerm refSf2 currentSf2) + + (ForAll refX refSf, ForAll currentX currentSf) -> + if refX == currentX then + Result.map (ForAll refX) + (commonFormulaTemplate lTerm rTerm refSf currentSf) + + else + Err <| differentFormulaStructure refF currentF + + (Exists refX refSf, Exists currentX currentSf) -> + if refX == currentX then + Result.map (Exists refX) + (commonFormulaTemplate lTerm rTerm refSf currentSf) + + else + Err <| differentFormulaStructure refF currentF + _ -> + Err <| differentFormulaStructure refF currentF -commonSignedTemplate : Signed Formula -> Signed Formula -> Result String (Signed Formula) -commonSignedTemplate refF currentF = - case refF of - T f -> - case currentF of - F f1 -> - differentSignError - T f1 -> - commonFormulaTemplate f (Formula.Signed.getFormula currentF) - |> Result.map (\a -> T a) +commonSignedTemplate : Term -> Term -> Signed Formula -> Signed Formula -> Result String (Signed Formula) +commonSignedTemplate lTerm rTerm refSF currentSF = + case (refSF, currentSF) of + (T refF, T currentF) -> + Result.map T + <| commonFormulaTemplate lTerm rTerm refF currentF - F f -> - case currentF of - F f1 -> - commonFormulaTemplate f (Formula.Signed.getFormula currentF) - |> Result.map (\a -> F a) + (F refF, F currentF) -> + Result.map F + <| commonFormulaTemplate lTerm rTerm refF currentF - T f1 -> - differentSignError + _ -> + Err <| differentSign applyFunToSigned : (a -> Result e a) -> Signed a -> Result e (Signed a) applyFunToSigned function sf = case sf of T formula -> - function formula |> Result.map (\f -> T f) + Result.map T <| function formula F formula -> - function formula |> Result.map (\f -> F f) + Result.map F <| function formula -mapNotSubstitutableError : String -> Zipper -> List Problem -mapNotSubstitutableError err z = +mapNotSubstitutableError : Term -> Term -> Term -> Zipper -> String -> List Problem +mapNotSubstitutableError substitutedT lhsT rhsT z err = semanticsProblem z - (String.replace "[]" "[] in 2nd referenced formula" err) + <| String.replace + (Term.toString substitutedT ++ " for []") + (Term.toString lhsT ++ " with " + ++ Term.toString rhsT + ++ " in the 2nd referenced formula") + err checkSubst : Term.Substitution + -> (String -> List Problem) -> Result (List Problem) (Signed Formula) -> Signed Formula -> Zipper -> Result (List Problem) Zipper -checkSubst σ replaced currentF z = +checkSubst σ mapErr replaced currentF z = case replaced of Err problem -> Err problem Ok repl -> applyFunToSigned (Formula.substitute σ) repl - |> Result.mapError (\err -> mapNotSubstitutableError err z) + |> Result.mapError mapErr |> Result.andThen (checkPredicate (\f -> f == currentF) (semanticsProblem z "Substitution invalid") @@ -274,17 +260,24 @@ checkSubsts refEq refF z = (Zipper.zNode z).formula |> Result.withDefault (T (PredAtom "default" [])) replaced = - commonSignedTemplate refF currentF |> Result.mapError (\err -> semanticsProblem z err) + commonSignedTemplate lt rt refF currentF |> Result.mapError (\err -> semanticsProblem z err) σ1 = Dict.fromList [ ( "[]", lt ) ] + mapErr1 = + mapNotSubstitutableError lt lt rt z + σ2 = Dict.fromList [ ( "[]", rt ) ] + + mapErr2 = + mapNotSubstitutableError rt lt rt z + in z - |> checkSubst σ1 replaced refF - |> Result.andThen (checkSubst σ2 replaced currentF) + |> checkSubst σ1 mapErr1 replaced refF + |> Result.andThen (checkSubst σ2 mapErr2 replaced currentF) validate : Zipper -> Result (List Problem) Zipper diff --git a/tests/TestLeibnitz.elm b/tests/TestLeibnitz.elm index 89599b2..54fd4eb 100644 --- a/tests/TestLeibnitz.elm +++ b/tests/TestLeibnitz.elm @@ -12,185 +12,439 @@ import Validation.Rules.Leibnitz exposing (checkSubsts, commonSignedTemplate, va import Zipper exposing (..) -tableauExample = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "" - , gui = defGUI - } - , ext = Open - } - - -zipperExample = - zipper tableauExample - - suiteCommonTemplate : Test suiteCommonTemplate = describe "The commonSignedTemplate function" - [ test "replace in eq atom" + [ test "replace right in eq atom" (\() -> Expect.equal (commonSignedTemplate + (Var "a") + (Var "c") (T (EqAtom (Var "b") (Var "a"))) (T (EqAtom (Var "b") (Var "c"))) ) (Ok (T (EqAtom (Var "b") (Var "[]")))) ) + , test "replace left in eq atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (EqAtom (Var "a") (Var "b"))) + (T (EqAtom (Var "c") (Var "b"))) + ) + (Ok (T (EqAtom (Var "[]") (Var "b")))) + ) + , test "replace both in eq atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (EqAtom (Var "a") (Var "a"))) + (T (EqAtom (Var "c") (Var "c"))) + ) + (Ok (T (EqAtom (Var "[]") (Var "[]")))) + ) + , test "replace none in eq atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (EqAtom (Var "a") (Var "b"))) + (T (EqAtom (Var "a") (Var "b"))) + ) + (Ok (T (EqAtom (Var "a") (Var "b")))) + ) , test "replace in predicate atom" (\() -> Expect.equal (commonSignedTemplate - (T (PredAtom "p" [ Fun "f" [ Var "b" ] ])) - (T (PredAtom "p" [ Fun "f" [ Var "b", Var "x" ] ])) + (Var "a") + (Var "c") + (T (PredAtom "p" [ Var "b", Var "a", Var "x" ])) + (T (PredAtom "p" [ Var "b", Var "c", Var "x" ])) + ) + (Ok (T (PredAtom "p" [ Var "b", Var "[]", Var "x" ]))) + ) + , test "replace all in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Var "a", Var "a", Var "a" ])) + (T (PredAtom "p" [ Var "c", Var "c", Var "c" ])) ) - (Ok (T (PredAtom "p" [ Var "[]" ]))) + (Ok (T (PredAtom "p" [ Var "[]", Var "[]", Var "[]" ]))) ) - , test "replace function with variable in predicate atom 2" + , test "replace none in predicate atom" (\() -> Expect.equal (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Var "a", Var "c", Var "b" ])) + (T (PredAtom "p" [ Var "a", Var "c", Var "b" ])) + ) + (Ok (T (PredAtom "p" [ Var "a", Var "c", Var "b" ]))) + ) + , test "replace in function in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "a" ] ])) + (T (PredAtom "p" [ Fun "f" [ Var "c" ] ])) + ) + (Ok (T (PredAtom "p" [ Fun "f" [ Var "[]" ] ]))) + ) + , test "replace none in function in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "a", Var "b", Var "c" ] ])) + (T (PredAtom "p" [ Fun "f" [ Var "a", Var "b", Var "c" ] ])) + ) + (Ok (T (PredAtom "p" [ Fun "f" [ Var "a", Var "b", Var "c" ] ]))) + ) + , test "replace function with variable in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Fun "f" [ Var "b" ]) + (Var "b") (T (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "b" ], Var "b" ] ])) (T (PredAtom "p" [ Fun "f" [ Var "b", Var "b" ] ])) ) (Ok (T (PredAtom "p" [ Fun "f" [ Var "[]", Var "b" ] ]))) ) + , test "replace variable with function in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "b") + (Fun "f" [ Var "b" ]) + (T (PredAtom "p" [ Fun "f" [ Var "b", Var "b" ] ])) + (T (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "b" ], Var "b" ] ])) + ) + (Ok (T (PredAtom "p" [ Fun "f" [ Var "[]", Var "b" ] ]))) + ) + , test "replace function with different function in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Fun "f" [ Var "b" ]) + (Fun "g" [ Var "b" ]) + (T (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "b" ], Var "b" ] ])) + (T (PredAtom "p" [ Fun "f" [ Fun "g" [ Var "b" ], Var "b" ] ])) + ) + (Ok (T (PredAtom "p" [ Fun "f" [ Var "[]", Var "b" ] ]))) + ) + , test "replace function with the same function with a different argument in predicate atom" + (\() -> + Expect.equal + (commonSignedTemplate + (Fun "f" [ Var "a" ]) + (Fun "f" [ Var "c" ]) + (T (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "a" ], Var "b" ], Fun "f" [ Var "a" ], Fun "f" [ Var "a" ] ])) + (T (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "c" ], Var "b" ], Fun "f" [ Var "c" ], Fun "f" [ Var "a" ] ])) + ) + (Ok (T (PredAtom "p" [ Fun "f" [ Var "[]", Var "b" ], Var "[]", Fun "f" [ Var "a" ] ]))) + ) + , test "replace in predicate atom with non-matching arity" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Var "a" ])) + (T (PredAtom "p" [ Var "c", Var "x" ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "have different structure " + ++ "(p(a) vs. p(c, x))" + ) + ) + , test "replace in non-matching predicate atoms (different preds)" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Var "a" ])) + (T (PredAtom "q" [ Var "c" ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "have different structure " + ++ "(p(a) vs. q(c))" + ) + ) + , test "replace in predicate atom with non-matching argument (arity)" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "a" ] ])) + (T (PredAtom "p" [ Fun "f" [ Var "c", Var "x" ] ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "contain non-matching subterms " + ++ "at corresponding locations " + ++ "(f(a) vs. f(c, x))" + ) + ) + , test "replace in predicate atom with non-matching argument (vars)" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "c" ] ])) + (T (PredAtom "p" [ Fun "f" [ Var "a" ] ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "contain non-matching subterms " + ++ "at corresponding locations " + ++ "(c vs. a)" + ) + ) + , test "replace in predicate atom with non-matching argument (var vs. fun)" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "a" ] ])) + (T (PredAtom "p" [ Var "c" ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "contain non-matching subterms " + ++ "at corresponding locations " + ++ "(f(a) vs. c)" + ) + ) + , test "replace in predicate atom with non-matching argument (different funcs)" + (\() -> + Expect.equal + (commonSignedTemplate + (Var "a") + (Var "c") + (T (PredAtom "p" [ Fun "f" [ Var "a" ] ])) + (T (PredAtom "p" [ Fun "g" [ Var "c" ] ])) + ) + (Err <| + "The 2nd referenced formula and current formula " + ++ "contain non-matching subterms " + ++ "at corresponding locations " + ++ "(f(a) vs. g(c))" + ) + ) , test "no change" (\() -> Expect.equal (commonSignedTemplate - (T (Conj (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) (EqAtom (Fun "f" [ Var "b" ]) (Var "b")))) - (T (Conj (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) (EqAtom (Fun "f" [ Var "b" ]) (Var "b")))) + (Var "a") + (Var "c") + (T + (Conj + (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "a" ]) (Var "c")) + ) + ) + (T + (Conj + (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "a" ]) (Var "c")) + ) + ) + ) + (Ok + (T + (Conj + (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "a" ]) (Var "c")) + ) + ) ) - (Ok (T (Conj (EqAtom (Fun "f" [ Var "b" ]) (Var "x")) (EqAtom (Fun "f" [ Var "b" ]) (Var "b"))))) ) , test "replace in conjunction" (\() -> Expect.equal (commonSignedTemplate - (T (Conj (EqAtom (Fun "f" [ Var "b", Var "c" ]) (Var "x")) (EqAtom (Fun "f" [ Var "c" ]) (Var "b")))) - (T (Conj (EqAtom (Fun "f" [ Var "b", Var "x" ]) (Var "x")) (EqAtom (Fun "f" [ Var "x" ]) (Var "x")))) + (Var "c") + (Var "x") + (T + (Conj + (EqAtom (Fun "f" [ Var "b", Var "c" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "c" ]) (Var "c")) + ) + ) + (T + (Conj + (EqAtom (Fun "f" [ Var "b", Var "x" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "x" ]) (Var "c")) + ) + ) + ) + (Ok + (T + (Conj + (EqAtom (Fun "f" [ Var "b", Var "[]" ]) (Var "x")) + (EqAtom (Fun "f" [ Var "[]" ]) (Var "c")) + ) + ) ) - (Ok (T (Conj (EqAtom (Fun "f" [ Var "b", Var "[]" ]) (Var "x")) (EqAtom (Fun "f" [ Var "[]" ]) (Var "[]"))))) ) , test "replace in for all" (\() -> Expect.equal (commonSignedTemplate - (T (ForAll "x" (Disj (EqAtom (Fun "f" [ Var "x", Var "z" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "a", Var "b", Var "c" ], Fun "g" [ Var "a" ] ])))) - (T (ForAll "x" (Disj (EqAtom (Fun "f" [ Var "x", Var "a" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "o", Var "o", Var "o" ], Fun "h" [ Var "a" ] ])))) + (Var "x") + (Var "c") + (T + (ForAll "x" + (Impl + (EqAtom (Fun "f" [ Var "c", Var "x" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "x", Var "b", Var "x" ] + , Fun "h" [ Var "x" ] + ] + ) + ) + ) + ) + (T + (ForAll "x" + (Impl + (EqAtom (Fun "f" [ Var "c", Var "c" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "c", Var "b", Var "c" ] + , Fun "h" [ Var "x" ] + ] + ) + ) + ) + ) + ) + (Ok + (T + (ForAll "x" + (Impl + (EqAtom (Fun "f" [ Var "c", Var "[]" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "[]", Var "b", Var "[]" ] + , Fun "h" [ Var "x" ] + ] + ) + ) + ) + ) ) - (Ok (T (ForAll "x" (Disj (EqAtom (Fun "f" [ Var "x", Var "[]" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "[]", Var "[]", Var "[]" ], Var "[]" ]))))) ) , test "replace in exists" (\() -> Expect.equal (commonSignedTemplate - (T (Exists "x" (Conj (EqAtom (Fun "f" [ Var "c", Var "z" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "c", Var "z" ], Fun "g" [ Var "a" ] ])))) - (T (Exists "x" (Conj (EqAtom (Fun "f" [ Var "x", Var "z" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "c", Var "z" ], Fun "h" [ Var "a" ] ])))) + (Var "c") + (Var "x") + (T + (Exists "x" + (Disj + (EqAtom (Fun "f" [ Var "c", Var "z" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "c", Var "z" ] + , Fun "g" [ Var "c" ] + ] + ) + ) + ) + ) + (T + (Exists "x" + (Disj + (EqAtom (Fun "f" [ Var "x", Var "z" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "c", Var "z" ] + , Fun "g" [ Var "x" ] + ] + ) + ) + ) + ) + ) + (Ok + (T + (Exists "x" + (Disj + (EqAtom (Fun "f" [ Var "[]", Var "z" ]) (Var "y")) + (PredAtom "p" + [ Fun "f" [ Var "c", Var "z" ] + , Fun "g" [ Var "[]" ] + ] + ) + ) + ) + ) ) - (Ok (T (Exists "x" (Conj (EqAtom (Fun "f" [ Var "[]", Var "z" ]) (Var "y")) (PredAtom "p" [ Fun "f" [ Var "c", Var "z" ], Var "[]" ]))))) ) ] -tableau1 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "T ∀x (p(c) & (x = c))" - , gui = defGUI - } - , ext = Open - } +sfFrom : String -> Signed Formula +sfFrom sfString = + Result.withDefault (F <| PredAtom "ERR" []) <| + Formula.Parser.parseSigned sfString -zipper1 = - zipper tableau1 - - -tableau2 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "T ∀x (p(f(x)) | ∀c(c = c))" - , gui = defGUI +zipperWith : String -> Zipper +zipperWith sfString = + zipper + { node = + { id = 1 + , value = "" + , references = [ { str = "1", up = Just 0 } ] + , formula = Formula.Parser.parseSigned sfString + , gui = defGUI + } + , ext = Open } - , ext = Open - } -zipper2 = - zipper tableau2 +zipper1 = + zipperWith "T ∀x (p(c) & (x = c))" -tableau3 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "F ∃x∃y (∀z p(z) | ∀z(r(z) & f(z,x) != y))" - , gui = defGUI - } - , ext = Open - } +zipper2 = + zipperWith "T ∀x (p(f(x)) | ∀c(c = c))" zipper3 = - zipper tableau3 - - -tableau4 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "T ∃x (p(b) & r(x))" - , gui = defGUI - } - , ext = Open - } + zipperWith "F ∃x∃y (∀z p(z) | ∀z(r(z) & f(z,x) != y))" zipper4 = - zipper tableau4 - - -tableau5 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "T (p(f(f(a))) | ∀c r(c))" - , gui = defGUI - } - , ext = Open - } + zipperWith "T ∃x (p(b) & r(x))" zipper5 = - zipper tableau5 - - -tableau6 = - { node = - { id = 1 - , value = "" - , references = [ { str = "1", up = Just 0 } ] - , formula = Formula.Parser.parseSigned "T ∃x∃y ((r(z) & c = f(a,x)) | p(z))" - , gui = defGUI - } - , ext = Open - } + zipperWith "T (p(f(f(a))) | ∀c r(c))" zipper6 = - zipper tableau6 + zipperWith "T ∃x∃y ((r(z) & c = f(a,x)) | p(z))" suiteCheckSubsts : Test @@ -201,10 +455,17 @@ suiteCheckSubsts = Expect.equal (checkSubsts (T (EqAtom (Fun "f" [ Var "a" ]) (Var "x"))) - (T (ForAll "x" (Conj (PredAtom "p" [ Var "c" ]) (EqAtom (Fun "f" [ Var "a" ]) (Var "c"))))) + (T + (ForAll "x" + (Conj + (PredAtom "p" [ Var "c" ]) + (EqAtom (Fun "f" [ Var "a" ]) (Var "c")) + ) + ) + ) zipper1 ) - (Err (semanticsProblem zipper1 "Cannot substitute x for [] in 2nd referenced formula; variable x is bound")) + (Err (semanticsProblem zipper1 "Cannot substitute f(a) with x in the 2nd referenced formula; variable x is bound")) ) , test "not substitutable 2" (\() -> @@ -214,7 +475,7 @@ suiteCheckSubsts = (T (ForAll "x" (Disj (PredAtom "p" [ Fun "f" [ Var "x" ] ]) (ForAll "c" (EqAtom (Var "y") (Var "c")))))) zipper2 ) - (Err (semanticsProblem zipper2 "Cannot substitute c for [] in 2nd referenced formula; variable c is bound")) + (Err (semanticsProblem zipper2 "Cannot substitute y with c in the 2nd referenced formula; variable c is bound")) ) , test "not substitutable 3" (\() -> @@ -224,7 +485,7 @@ suiteCheckSubsts = (F (Exists "x" (Exists "y" (Disj (ForAll "z" (PredAtom "p" [ Var "z" ])) (ForAll "z" (Conj (PredAtom "r" [ Var "z" ]) (Neg (EqAtom (Fun "f" [ Var "z", Var "y" ]) (Var "y"))))))))) zipper3 ) - (Err (semanticsProblem zipper3 "Cannot substitute y for [] in 2nd referenced formula; variable y is bound")) + (Err (semanticsProblem zipper3 "Cannot substitute y with x in the 2nd referenced formula; variable y is bound")) ) , test "not substitutable 4" (\() -> @@ -234,7 +495,27 @@ suiteCheckSubsts = (F (Exists "x" (Exists "y" (Disj (ForAll "z" (PredAtom "p" [ Var "z" ])) (ForAll "z" (Conj (PredAtom "r" [ Var "z" ]) (Neg (EqAtom (Fun "f" [ Var "z", Var "a" ]) (Var "y"))))))))) zipper3 ) - (Err (semanticsProblem zipper3 "Cannot substitute x for [] in 2nd referenced formula; variable x is bound")) + (Err (semanticsProblem zipper3 "Cannot substitute a with x in the 2nd referenced formula; variable x is bound")) + ) + , test "not substitutable 5" + (\() -> + Expect.equal + (checkSubsts + (T (EqAtom (Fun "f" [ Var "z", Var "a" ]) (Fun "f" [ Var "z", Var "x" ]))) + (F (Exists "x" (Exists "y" (Disj (ForAll "z" (PredAtom "p" [ Var "z" ])) (ForAll "z" (Conj (PredAtom "r" [ Var "z" ]) (Neg (EqAtom (Fun "f" [ Var "z", Var "a" ]) (Var "y"))))))))) + zipper3 + ) + (Err (semanticsProblem zipper3 "Cannot substitute f(z, a) with f(z, x) in the 2nd referenced formula; variable z is bound")) + ) + , test "not substitutable 6" + (\() -> + Expect.equal + (checkSubsts + (T (EqAtom (Var "a") (Fun "f" [ Var "z", Var "x" ]))) + (F (Exists "x" (Exists "y" (Disj (ForAll "z" (PredAtom "p" [ Var "z" ])) (ForAll "z" (Conj (PredAtom "r" [ Var "z" ]) (Neg (EqAtom (Var "a") (Var "y"))))))))) + zipper3 + ) + (Err (semanticsProblem zipper3 "Cannot substitute a with f(z, x) in the 2nd referenced formula; variables x, z are bound")) ) , test "different sign" (\() -> @@ -254,7 +535,7 @@ suiteCheckSubsts = (T (ForAll "x" (Disj (PredAtom "p" [ Var "c" ]) (EqAtom (Fun "f" [ Var "a" ]) (Var "c"))))) zipper1 ) - (Err (semanticsProblem zipper1 "The 2nd referenced formula and current formula have different structure")) + (Err (semanticsProblem zipper1 "The 2nd referenced formula and current formula have different structure (( p(c) ∨ f(a) ≐ c ) vs. ( p(c) ∧ x ≐ c ))")) ) , test "different structure 2" (\() -> @@ -264,7 +545,7 @@ suiteCheckSubsts = (T (ForAll "x" (Disj (PredAtom "p" [ Fun "f" [ Var "x" ] ]) (ForAll "c" (PredAtom "a" [ Var "y" ]))))) zipper2 ) - (Err (semanticsProblem zipper2 "The 2nd referenced formula and current formula have different structure")) + (Err (semanticsProblem zipper2 "The 2nd referenced formula and current formula have different structure (a(y) vs. c ≐ c)")) ) , test "different structure 3" (\() -> @@ -274,9 +555,9 @@ suiteCheckSubsts = (F (Exists "x" (Exists "y" (Disj (ForAll "z" (PredAtom "p" [ Var "z" ])) (Exists "z" (Conj (PredAtom "r" [ Var "z" ]) (Neg (EqAtom (Fun "f" [ Var "z", Var "y" ]) (Var "y"))))))))) zipper3 ) - (Err (semanticsProblem zipper3 "The 2nd referenced formula and current formula have different structure")) + (Err (semanticsProblem zipper3 "The 2nd referenced formula and current formula have different structure (∃z ( r(z) ∧ ¬ f(z, y) ≐ y ) vs. ∀z ( r(z) ∧ ¬ f(z, x) ≐ y ))")) ) - , test "invalid substitution 1" + , test "different structure 4" (\() -> Expect.equal (checkSubsts @@ -284,9 +565,9 @@ suiteCheckSubsts = (T (Exists "x" (Conj (PredAtom "p" [ Var "c" ]) (PredAtom "r" [ Var "x" ])))) zipper4 ) - (Err (semanticsProblem zipper4 "Substitution invalid")) + (Err (semanticsProblem zipper4 "The 2nd referenced formula and current formula contain non-matching subterms at corresponding locations (c vs. b)")) ) - , test "invalid substitution 2" + , test "different structure 5" (\() -> Expect.equal (checkSubsts @@ -294,9 +575,9 @@ suiteCheckSubsts = (T (Disj (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "x" ] ] ]) (ForAll "c" (PredAtom "r" [ Var "c" ])))) zipper5 ) - (Err (semanticsProblem zipper5 "Substitution invalid")) + (Err (semanticsProblem zipper5 "The 2nd referenced formula and current formula contain non-matching subterms at corresponding locations (x vs. a)")) ) - , test "invalid substitution 3" + , test "different structure 6" (\() -> Expect.equal (checkSubsts @@ -304,7 +585,7 @@ suiteCheckSubsts = (T (Exists "x" (Exists "y" (Disj (Conj (PredAtom "r" [ Var "z" ]) (EqAtom (Var "c") (Fun "f" [ Var "z", Var "x" ]))) (PredAtom "p" [ Var "z" ]))))) zipper6 ) - (Err (semanticsProblem zipper6 "Substitution invalid")) + (Err (semanticsProblem zipper6 "The 2nd referenced formula and current formula contain non-matching subterms at corresponding locations (z vs. a)")) ) , test "ok 1" (\() -> @@ -336,6 +617,26 @@ suiteCheckSubsts = ) (Ok zipper6) ) + , test "ok 4" + (\() -> + Expect.equal + (checkSubsts + (T (EqAtom (Fun "f" [ Var "x" ]) (Fun "f" [ Var "a" ]))) + (T (Disj (PredAtom "p" [ Fun "f" [ Fun "f" [ Var "x" ] ] ]) (ForAll "c" (PredAtom "r" [ Var "c" ])))) + zipper5 + ) + (Ok zipper5) + ) + , test "ok 5" + (\() -> + Expect.equal + (checkSubsts + (sfFrom "T g(a) ≐ g(b)") + (sfFrom "T P(g(a))") + (zipperWith "T P(g(b))") + ) + (Ok (zipperWith "T P(g(b))")) + ) ]