From bb4b49b6c36989b98e11f37f28dc13c5aff07277 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 15:40:03 +0200 Subject: [PATCH 1/9] More modal tests --- .../proof/modal/proof/ParseModalAction.java | 11 ++-- .../dan323/uses/modal/ModalProofParser.java | 5 +- .../uses/modal/ModalProofTransformer.java | 2 +- .../uses/modal/test/ModalTransformerTest.java | 56 +++++++++++++++++++ 4 files changed, 67 insertions(+), 7 deletions(-) create mode 100644 domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java diff --git a/domain/proof-structures/implementation.deduction.modal/src/main/java/com/dan323/proof/modal/proof/ParseModalAction.java b/domain/proof-structures/implementation.deduction.modal/src/main/java/com/dan323/proof/modal/proof/ParseModalAction.java index a6fcc5b9..f55235e9 100644 --- a/domain/proof-structures/implementation.deduction.modal/src/main/java/com/dan323/proof/modal/proof/ParseModalAction.java +++ b/domain/proof-structures/implementation.deduction.modal/src/main/java/com/dan323/proof/modal/proof/ParseModalAction.java @@ -147,8 +147,10 @@ private static int[] parseArray(ProofReason proofReason) { private static ModalAssume parseAss(ModalOperation atPos, String state) { if (atPos instanceof RelationOperation operation) { return new ModalAssume(operation); - } else { + } else if (state != null) { return new ModalAssume((ModalLogicalOperation) atPos, state); + } else { + throw new IllegalArgumentException("State provided is invalid."); } } @@ -159,7 +161,7 @@ private static ModalOrE parseOrE(ProofReason reason) { private static int[] parseArray(String proofReason, int reasonLength) { return Arrays.stream(proofReason.substring(reasonLength + 2, proofReason.length() - 1) - .split(",")) + .split(",")) .map(String::trim) .mapToInt(Integer::parseInt) .toArray(); @@ -184,9 +186,10 @@ public static ModalOperation parseExpression(String expression) { return modalParser.evaluate(expression); } - public static AbstractModalAction parseAction(String name, List sources, ModalOperation extraInfo, String state){ + public static AbstractModalAction parseAction(String name, List sources, ModalOperation extraInfo, String state) { return switch (name) { - case "Ass" -> extraInfo instanceof RelationOperation relationOperation ? new ModalAssume(relationOperation): new ModalAssume((ModalLogicalOperation)extraInfo, state); + case "Ass" -> + extraInfo instanceof RelationOperation relationOperation ? new ModalAssume(relationOperation) : new ModalAssume((ModalLogicalOperation) extraInfo, state); case "|I1" -> new ModalOrI1(sources.getFirst(), (ModalLogicalOperation) extraInfo); case "|I2" -> new ModalOrI2(sources.getFirst(), (ModalLogicalOperation) extraInfo); case "|E" -> new ModalOrE(sources.get(0), sources.get(1), sources.get(2)); diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java index b7fd5581..9cc0c43b 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java @@ -63,13 +63,14 @@ private static ProofStepModal parseLine(String line) { var rule = startExpression.substring(lastSpace + 2); return new ProofStepModal(assmsLevel, (RelationOperation) ParseModalAction.parseExpression(expression), ParseModalAction.parseReason(rule)); } else { - var array = line.substring(i).toCharArray(); + var array = line.substring(i + 2).toCharArray(); String state = line.substring(0, i); + i = 0; while (array[i] == ' ') { i++; } int assmsLevel = i / 3; - var startExpression = line.substring(i + 1); + var startExpression = line.substring(i); var firstSpace = startExpression.indexOf(" ".repeat(11)); var lastSpace = startExpression.lastIndexOf(" "); var expression = startExpression.substring(0, firstSpace); diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java index 1e73bb28..b860366a 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java @@ -53,7 +53,7 @@ public ProofDto fromProof(ModalNaturalDeduction proof) { var goal = proof.getGoal().toString(); var steps = new ArrayList(); for (var step : proof.getSteps()) { - steps.add(new StepDto(step.getStep().toString(), step.getProof().toString(), step.getAssumptionLevel(), Map.of("state", step.getState()))); + steps.add(new StepDto(step.getStep().toString(), step.getProof().toString(), step.getAssumptionLevel(), step.getState() != null ? Map.of("state", step.getState()) : Map.of())); } return new ProofDto(steps.stream().toList(), logic, goal); diff --git a/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java new file mode 100644 index 00000000..d7d4cdcb --- /dev/null +++ b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java @@ -0,0 +1,56 @@ +package com.dan323.uses.modal.test; + +import com.dan323.expressions.modal.Always; +import com.dan323.expressions.modal.ImplicationModal; +import com.dan323.expressions.modal.ModalLogicalOperation; +import com.dan323.expressions.modal.VariableModal; +import com.dan323.expressions.relation.LessEqual; +import com.dan323.expressions.relation.RelationOperation; +import com.dan323.proof.modal.ModalAssume; +import com.dan323.proof.modal.ModalBoxE; +import com.dan323.proof.modal.ModalBoxI; +import com.dan323.proof.modal.ModalDeductionTheorem; +import com.dan323.proof.modal.proof.ModalNaturalDeduction; +import com.dan323.uses.modal.ModalProofTransformer; +import org.junit.jupiter.api.Test; + +import java.util.List; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +public class ModalTransformerTest { + + private static final ModalLogicalOperation P = new VariableModal("P"); + private static final ModalLogicalOperation Q = new VariableModal("Q"); + private static final RelationOperation s0LessThans1 = new LessEqual("s0", "s1"); + + + @Test + public void transformSuccessful() { + var nd = new ModalNaturalDeduction(); + nd.initializeProof(List.of(new Always(P)), new Always(new ImplicationModal(Q, P))); + new ModalAssume(s0LessThans1).apply(nd); + new ModalAssume(Q, "s1").apply(nd); + new ModalBoxE(1, 2).apply(nd); + new ModalDeductionTheorem().apply(nd); + new ModalBoxI().apply(nd); + var transformer = new ModalProofTransformer(); + assertTrue(transformer.fromProof(nd).isDone()); + assertEquals(nd.toString(), transformer.from(transformer.fromProof(nd)).toString()); + } + + @Test + public void transformFailed() { + var nd = new ModalNaturalDeduction(); + nd.initializeProof(List.of(new Always(P)), new Always(new ImplicationModal(Q, P))); + new ModalAssume(s0LessThans1).apply(nd); + new ModalAssume(Q, "s1").apply(nd); + new ModalBoxE(1, 2).apply(nd); + new ModalDeductionTheorem().apply(nd); + new ModalBoxI().apply(nd); + var transformer = new ModalProofTransformer(); + assertTrue(transformer.fromProof(nd).isDone()); + assertEquals(nd.toString(), transformer.from(transformer.fromProof(nd)).toString()); + } +} From d8ee1d88d085e4db9e0418a830dd0785455a4202 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 15:50:53 +0200 Subject: [PATCH 2/9] More modal tests --- .../src/main/java/com/dan323/uses/modal/ModalProofParser.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java index 9cc0c43b..63563e89 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java @@ -63,8 +63,9 @@ private static ProofStepModal parseLine(String line) { var rule = startExpression.substring(lastSpace + 2); return new ProofStepModal(assmsLevel, (RelationOperation) ParseModalAction.parseExpression(expression), ParseModalAction.parseReason(rule)); } else { - var array = line.substring(i + 2).toCharArray(); String state = line.substring(0, i); + line = line.substring(i + 2); + var array = line.toCharArray(); i = 0; while (array[i] == ' ') { i++; From 995ac363d9dfbc61a40aeba8ca91bbbd635571c2 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 16:27:38 +0200 Subject: [PATCH 3/9] More modal tests --- .../src/main/java/module-info.java | 1 + .../uses/modal/ModalProofTransformer.java | 5 ++-- .../uses/modal/test/ModalTransformerTest.java | 30 ++++++++++++++----- 3 files changed, 26 insertions(+), 10 deletions(-) diff --git a/domain/proof-structures/implementation.deduction.modal/src/main/java/module-info.java b/domain/proof-structures/implementation.deduction.modal/src/main/java/module-info.java index 7bd5ec8e..73bee4eb 100644 --- a/domain/proof-structures/implementation.deduction.modal/src/main/java/module-info.java +++ b/domain/proof-structures/implementation.deduction.modal/src/main/java/module-info.java @@ -3,6 +3,7 @@ */ module implementation.deduction.modal { exports com.dan323.proof.modal; + exports com.dan323.proof.modal.relational; exports com.dan323.proof.modal.proof; requires framework.deduction; requires language.implementation.modal; diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java index b860366a..fe9cb4fb 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofTransformer.java @@ -44,7 +44,8 @@ public ModalNaturalDeduction from(ProofDto proof) { public AbstractModalAction from(ActionDto action) { var parser = new ModalLogicParser(); - return ParseModalAction.parseAction(action.name(), action.sources(), parser.evaluate(action.extraParameters().get("expression")), action.extraParameters().get("state")); + var expression = action.extraParameters().get("expression"); + return ParseModalAction.parseAction(action.name(), action.sources(), expression == null ? null : parser.evaluate(expression), action.extraParameters().get("state")); } @Override @@ -53,7 +54,7 @@ public ProofDto fromProof(ModalNaturalDeduction proof) { var goal = proof.getGoal().toString(); var steps = new ArrayList(); for (var step : proof.getSteps()) { - steps.add(new StepDto(step.getStep().toString(), step.getProof().toString(), step.getAssumptionLevel(), step.getState() != null ? Map.of("state", step.getState()) : Map.of())); + steps.add(new StepDto(step.getStep().toString(), step.getProof().toString(), step.getAssumptionLevel(), step.getState() != null ? Map.of("state", step.getState()) : Map.of())); } return new ProofDto(steps.stream().toList(), logic, goal); diff --git a/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java index d7d4cdcb..b9453df2 100644 --- a/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java +++ b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java @@ -6,24 +6,24 @@ import com.dan323.expressions.modal.VariableModal; import com.dan323.expressions.relation.LessEqual; import com.dan323.expressions.relation.RelationOperation; -import com.dan323.proof.modal.ModalAssume; -import com.dan323.proof.modal.ModalBoxE; -import com.dan323.proof.modal.ModalBoxI; -import com.dan323.proof.modal.ModalDeductionTheorem; +import com.dan323.model.ActionDto; +import com.dan323.proof.modal.*; import com.dan323.proof.modal.proof.ModalNaturalDeduction; +import com.dan323.proof.modal.relational.Reflexive; import com.dan323.uses.modal.ModalProofTransformer; import org.junit.jupiter.api.Test; import java.util.List; +import java.util.Map; -import static org.junit.jupiter.api.Assertions.assertEquals; -import static org.junit.jupiter.api.Assertions.assertTrue; +import static org.junit.jupiter.api.Assertions.*; public class ModalTransformerTest { private static final ModalLogicalOperation P = new VariableModal("P"); private static final ModalLogicalOperation Q = new VariableModal("Q"); private static final RelationOperation s0LessThans1 = new LessEqual("s0", "s1"); + private static final ModalProofTransformer transformer = new ModalProofTransformer(); @Test @@ -35,7 +35,6 @@ public void transformSuccessful() { new ModalBoxE(1, 2).apply(nd); new ModalDeductionTheorem().apply(nd); new ModalBoxI().apply(nd); - var transformer = new ModalProofTransformer(); assertTrue(transformer.fromProof(nd).isDone()); assertEquals(nd.toString(), transformer.from(transformer.fromProof(nd)).toString()); } @@ -49,8 +48,23 @@ public void transformFailed() { new ModalBoxE(1, 2).apply(nd); new ModalDeductionTheorem().apply(nd); new ModalBoxI().apply(nd); - var transformer = new ModalProofTransformer(); assertTrue(transformer.fromProof(nd).isDone()); assertEquals(nd.toString(), transformer.from(transformer.fromProof(nd)).toString()); } + + @Test + public void transformAction() { + var actionDto = new ActionDto("Ass", List.of(), Map.of("expression", "P", "state", "s0")); + var action = transformer.from(actionDto); + assertInstanceOf(ModalAssume.class, action); + actionDto = new ActionDto("Rep", List.of(1), Map.of()); + action = transformer.from(actionDto); + assertInstanceOf(ModalCopy.class, action); + actionDto = new ActionDto("->I", List.of(), Map.of()); + action = transformer.from(actionDto); + assertInstanceOf(ModalDeductionTheorem.class, action); + actionDto = new ActionDto("Refl", List.of(1), Map.of()); + action = transformer.from(actionDto); + assertInstanceOf(Reflexive.class, action); + } } From f7c83f448648a580ccf10f97aef81eb79dcbbb23 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 16:38:44 +0200 Subject: [PATCH 4/9] Reduce duplication --- .../java/com/dan323/uses/ProofParser.java | 47 ++++++++++++++++++- .../uses/classical/ParseClassicalProof.java | 40 +++------------- .../dan323/uses/modal/ModalProofParser.java | 40 +++------------- 3 files changed, 59 insertions(+), 68 deletions(-) diff --git a/domain/use-cases/base-use-case/src/main/java/com/dan323/uses/ProofParser.java b/domain/use-cases/base-use-case/src/main/java/com/dan323/uses/ProofParser.java index 76cf07f7..31bdaa09 100644 --- a/domain/use-cases/base-use-case/src/main/java/com/dan323/uses/ProofParser.java +++ b/domain/use-cases/base-use-case/src/main/java/com/dan323/uses/ProofParser.java @@ -1,13 +1,56 @@ package com.dan323.uses; import com.dan323.expressions.base.LogicOperation; +import com.dan323.proof.generic.Action; import com.dan323.proof.generic.proof.Proof; import com.dan323.proof.generic.proof.ProofStep; -public interface ProofParser

, T extends LogicOperation, Q extends ProofStep> { +import java.util.List; - P parseProof(String proof); +public interface ProofParser

, T extends LogicOperation, Q extends ProofStep, A extends Action> { + + default P parseProof(String proof) { + P nd = getNewProof(); + var actions = proof.lines().map(this::parseLine).toList(); + var assms = ProofParser.extractAssumptions(actions); + var actualProof = ProofParser.skipInitAssumptions(actions); + if (actions.getLast().getAssumptionLevel() == 0) { + nd.initializeProof(assms, actions.getLast().getStep()); + nd.getSteps().addAll(actualProof); + var parsedActions = (List)nd.parse(); + nd.reset(); + int i = 0; + for (A action : parsedActions) { + if (i < nd.getAssms().size()) { + i++; + } else if (action.isValid(nd)) { + action.apply(nd); + } else { + throw new IllegalArgumentException("The proof is invalid!!"); + } + } + return nd; + } else { + throw new IllegalArgumentException("The proof is invalid!!"); + } + } String logic(); + P getNewProof(); + + Q parseLine(String line); + + private static > List extractAssumptions(List steps) { + return steps.stream() + .takeWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) + .map(ProofStep::getStep) + .toList(); + } + + private static > List skipInitAssumptions(List steps) { + return steps.stream() + .dropWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) + .toList(); + } } diff --git a/domain/use-cases/classical-use-case/src/main/java/com/dan323/uses/classical/ParseClassicalProof.java b/domain/use-cases/classical-use-case/src/main/java/com/dan323/uses/classical/ParseClassicalProof.java index ac72c372..abf40a01 100644 --- a/domain/use-cases/classical-use-case/src/main/java/com/dan323/uses/classical/ParseClassicalProof.java +++ b/domain/use-cases/classical-use-case/src/main/java/com/dan323/uses/classical/ParseClassicalProof.java @@ -4,47 +4,21 @@ import com.dan323.classical.proof.NaturalDeduction; import com.dan323.classical.proof.ParseClassicalAction; import com.dan323.expressions.classical.ClassicalLogicOperation; -import com.dan323.uses.ProofParser; import com.dan323.proof.generic.proof.ProofStep; +import com.dan323.uses.ProofParser; -public class ParseClassicalProof implements ProofParser> { +public class ParseClassicalProof implements ProofParser, ClassicalAction> { - public String logic(){ + public String logic() { return "classical"; } - public NaturalDeduction parseProof(String proof) { - NaturalDeduction nd = new NaturalDeduction(); - var actions = proof.lines().map(ParseClassicalProof::parseLine).toList(); - var assms = actions.stream() - .takeWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) - .map(ProofStep::getStep) - .toList(); - var actualProof = actions.stream() - .dropWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) - .toList(); - if (actions.getLast().getAssumptionLevel() == 0) { - nd.initializeProof(assms, actions.getLast().getStep()); - nd.getSteps().addAll(actualProof); - var parsedActions = nd.parse(); - nd.reset(); - int i = 0; - for (ClassicalAction action : parsedActions) { - if (i < nd.getAssms().size()) { - i++; - } else if (action.isValid(nd)) { - action.apply(nd); - } else { - throw new IllegalArgumentException("The proof is invalid!!"); - } - } - return nd; - } else { - throw new IllegalArgumentException("The proof is invalid!!"); - } + @Override + public NaturalDeduction getNewProof() { + return new NaturalDeduction(); } - private static ProofStep parseLine(String line) { + public ProofStep parseLine(String line) { var array = line.toCharArray(); int i = 0; while (array[i] == ' ') { diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java index 63563e89..6fae3834 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java @@ -3,51 +3,25 @@ import com.dan323.expressions.modal.ModalLogicalOperation; import com.dan323.expressions.modal.ModalOperation; import com.dan323.expressions.relation.RelationOperation; -import com.dan323.proof.generic.proof.ProofStep; -import com.dan323.proof.modal.AbstractModalAction; +import com.dan323.proof.modal.ModalAction; import com.dan323.proof.modal.proof.ModalNaturalDeduction; import com.dan323.proof.modal.proof.ParseModalAction; import com.dan323.proof.modal.proof.ProofStepModal; import com.dan323.uses.ProofParser; -public class ModalProofParser implements ProofParser { +public class ModalProofParser implements ProofParser { public String logic() { return "modal"; } - public ModalNaturalDeduction parseProof(String proof) { - ModalNaturalDeduction nd = new ModalNaturalDeduction(); - var actions = proof.lines().map(ModalProofParser::parseLine).toList(); - var assms = actions.stream() - .takeWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) - .map(ProofStep::getStep) - .toList(); - var actualProof = actions.stream() - .dropWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass")) - .toList(); - if (actions.getLast().getAssumptionLevel() == 0) { - nd.initializeProof(assms, actions.getLast().getStep()); - nd.getSteps().addAll(actualProof); - var parsedActions = nd.parse(); - nd.reset(); - int i = 0; - for (AbstractModalAction action : parsedActions) { - if (i < nd.getAssms().size()) { - i++; - } else if (action.isValid(nd)) { - action.apply(nd); - } else { - throw new IllegalArgumentException("The proof is invalid!!"); - } - } - return nd; - } else { - throw new IllegalArgumentException("The proof is invalid!!"); - } + @Override + public ModalNaturalDeduction getNewProof() { + return new ModalNaturalDeduction(); } - private static ProofStepModal parseLine(String line) { + + public ProofStepModal parseLine(String line) { int i = line.indexOf(':'); if (i == -1) { var array = line.toCharArray(); From 9dfa580a4430640264185f102954ec8b18dcd931 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 16:42:33 +0200 Subject: [PATCH 5/9] Reduce duplication --- .../dan323/uses/modal/ModalProofParser.java | 44 ++++++++----------- 1 file changed, 19 insertions(+), 25 deletions(-) diff --git a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java index 6fae3834..fe8ec4fe 100644 --- a/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java +++ b/domain/use-cases/modal-use-case/src/main/java/com/dan323/uses/modal/ModalProofParser.java @@ -23,33 +23,27 @@ public ModalNaturalDeduction getNewProof() { public ProofStepModal parseLine(String line) { int i = line.indexOf(':'); - if (i == -1) { - var array = line.toCharArray(); - i = 0; - while (array[i] == ' ') { - i++; - } - int assmsLevel = i / 3; - var startExpression = line.substring(i); - var firstSpace = startExpression.indexOf(" ".repeat(11)); - var lastSpace = startExpression.lastIndexOf(" "); - var expression = startExpression.substring(0, firstSpace); - var rule = startExpression.substring(lastSpace + 2); + boolean isRelation = true; + String state = null; + if (i != -1) { + state = line.substring(0, i); + isRelation = false; + line = line.substring(i + 2); + } + var array = line.toCharArray(); + i = 0; + while (array[i] == ' ') { + i++; + } + int assmsLevel = i / 3; + var startExpression = line.substring(i); + var firstSpace = startExpression.indexOf(" ".repeat(11)); + var lastSpace = startExpression.lastIndexOf(" "); + var expression = startExpression.substring(0, firstSpace); + var rule = startExpression.substring(lastSpace + 2); + if (isRelation) { return new ProofStepModal(assmsLevel, (RelationOperation) ParseModalAction.parseExpression(expression), ParseModalAction.parseReason(rule)); } else { - String state = line.substring(0, i); - line = line.substring(i + 2); - var array = line.toCharArray(); - i = 0; - while (array[i] == ' ') { - i++; - } - int assmsLevel = i / 3; - var startExpression = line.substring(i); - var firstSpace = startExpression.indexOf(" ".repeat(11)); - var lastSpace = startExpression.lastIndexOf(" "); - var expression = startExpression.substring(0, firstSpace); - var rule = startExpression.substring(lastSpace + 2); return new ProofStepModal(state, assmsLevel, (ModalLogicalOperation) ParseModalAction.parseExpression(expression), ParseModalAction.parseReason(rule)); } } From 0c526a96f57f6ca68e35743130181185e25062ba Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 16:49:48 +0200 Subject: [PATCH 6/9] Reduce duplication --- .../src/test/java/com/dan323/uses/mock/Parsers.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java index bd7c2a1f..8a8d1cf2 100644 --- a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java +++ b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java @@ -104,6 +104,16 @@ public void initializeProof(List assms, LogicOperation goal) { public String logic() { return logic; } + + @Override + public Proof getNewProof() { + throw new UnsupportedOperationException(); + } + + @Override + public ProofStep parseLine(String line) { + throw new UnsupportedOperationException(); + } }; } From c5523ffced1ab5c04a9742b41efe8b0709148887 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 17:06:59 +0200 Subject: [PATCH 7/9] Reduce duplication --- .../com/dan323/proof/generic/proof/Proof.java | 2 +- .../com/dan323/uses/test/ProofParserTest.java | 68 +++++++++++++++++++ 2 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java diff --git a/domain/proof-structures/framework.deduction/src/main/java/com/dan323/proof/generic/proof/Proof.java b/domain/proof-structures/framework.deduction/src/main/java/com/dan323/proof/generic/proof/Proof.java index a5b8a217..f774039f 100644 --- a/domain/proof-structures/framework.deduction/src/main/java/com/dan323/proof/generic/proof/Proof.java +++ b/domain/proof-structures/framework.deduction/src/main/java/com/dan323/proof/generic/proof/Proof.java @@ -9,7 +9,7 @@ public abstract class Proof> { - private List assms; + private List assms = List.of(); private T goal; private final List steps = new ArrayList<>(); diff --git a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java new file mode 100644 index 00000000..b5a530b5 --- /dev/null +++ b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java @@ -0,0 +1,68 @@ +package com.dan323.uses.test; + +import com.dan323.expressions.base.LogicOperation; +import com.dan323.proof.generic.Action; +import com.dan323.proof.generic.proof.Proof; +import com.dan323.proof.generic.proof.ProofReason; +import com.dan323.proof.generic.proof.ProofStep; +import com.dan323.uses.ProofParser; +import org.junit.jupiter.api.Test; + +import java.util.List; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +public class ProofParserTest { + + @Test + public void proofParserTest() { + var proofParser = new ProofParserStub(); + var proof = proofParser.parseProof("\n".repeat(5)); + assertEquals(5, proof.getSteps().size()); + } + + + private static final class ProofParserStub implements ProofParser>, LogicOperation, ProofStep, Action, Proof>>> { + + @Override + public String logic() { + return "l1"; + } + + @Override + public Proof> getNewProof() { + return new Proof<>() { + @Override + public List, ? extends Proof>>> parse() { + return List.of(); + } + + @Override + protected ProofStep generateAssm(LogicOperation logicexpression) { + return new ProofStep<>(0, logicexpression, new ProofReason("Ass", List.of())); + } + + @Override + public void automate() { + + } + + @Override + public void initializeProof(List assms, LogicOperation goal) { + getSteps().clear(); + setAssms(assms); + } + }; + } + + @Override + public ProofStep parseLine(String line) { + return new ProofStep<>(0, new LogicOperation() { + @Override + public String toString() { + return "P"; + } + }, new ProofReason("Ass", List.of())); + } + } +} From be837da8fe1c9d2fb99cf6639abda4b33b8f4cb9 Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 17:19:24 +0200 Subject: [PATCH 8/9] Reduce duplication --- .../proof/modal/ParseModalActionTest.java | 19 ++++++++++++++++++- .../uses/modal/test/ModalTransformerTest.java | 5 +++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/domain/proof-structures/implementation.deduction.modal/src/test/java/com/dan323/proof/modal/ParseModalActionTest.java b/domain/proof-structures/implementation.deduction.modal/src/test/java/com/dan323/proof/modal/ParseModalActionTest.java index 9e72fe0f..5a7e3847 100644 --- a/domain/proof-structures/implementation.deduction.modal/src/test/java/com/dan323/proof/modal/ParseModalActionTest.java +++ b/domain/proof-structures/implementation.deduction.modal/src/test/java/com/dan323/proof/modal/ParseModalActionTest.java @@ -2,8 +2,8 @@ import com.dan323.expressions.modal.*; import com.dan323.expressions.relation.LessEqual; -import com.dan323.proof.generic.Copy; import com.dan323.proof.modal.proof.ModalNaturalDeduction; +import com.dan323.proof.modal.proof.ParseModalAction; import com.dan323.proof.modal.relational.Reflexive; import com.dan323.proof.modal.relational.Transitive; import org.junit.jupiter.api.Test; @@ -11,6 +11,7 @@ import java.util.List; import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; public class ParseModalActionTest { @@ -192,4 +193,20 @@ public void parseDia() { lst = mnd.parse(); assertEquals(new ModalDiaE(4), lst.get(7)); } + + @Test + public void parseAction() { + var action = ParseModalAction.parseAction("Ass", List.of(), new VariableModal("P"), "s0"); + assertInstanceOf(ModalAssume.class, action); + action = ParseModalAction.parseAction("Refl", List.of(1), null, null); + assertInstanceOf(Reflexive.class, action); + action = ParseModalAction.parseAction("Rep", List.of(2), null, null); + assertInstanceOf(ModalCopy.class, action); + action = ParseModalAction.parseAction("->I", List.of(), null, null); + assertInstanceOf(ModalDeductionTheorem.class, action); + action = ParseModalAction.parseAction("->E", List.of(2,4), null, null); + assertInstanceOf(ModalModusPonens.class, action); + action = ParseModalAction.parseAction("-E", List.of(3), null, null); + assertInstanceOf(ModalNotE.class, action); + } } diff --git a/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java index b9453df2..cec995fd 100644 --- a/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java +++ b/domain/use-cases/modal-use-case/src/test/java/com/dan323/uses/modal/test/ModalTransformerTest.java @@ -66,5 +66,10 @@ public void transformAction() { actionDto = new ActionDto("Refl", List.of(1), Map.of()); action = transformer.from(actionDto); assertInstanceOf(Reflexive.class, action); + actionDto = new ActionDto("->E", List.of(1, 2), Map.of()); + action = transformer.from(actionDto); + assertInstanceOf(ModalModusPonens.class, action); + var actionInError = new ActionDto("->E", List.of(), Map.of()); + assertThrows(IndexOutOfBoundsException.class, () -> transformer.from(actionInError)); } } From ff5b8842a40a1afe67454c0d15ee8338fdd795fa Mon Sep 17 00:00:00 2001 From: dnl232 Date: Sun, 18 Aug 2024 17:25:18 +0200 Subject: [PATCH 9/9] Reduce duplication --- .../src/test/java/com/dan323/uses/mock/Parsers.java | 4 ++-- .../src/test/java/com/dan323/uses/mock/Transformers.java | 4 ++-- .../src/test/java/com/dan323/uses/test/ProofParserTest.java | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java index 8a8d1cf2..0b4916d6 100644 --- a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java +++ b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Parsers.java @@ -90,12 +90,12 @@ protected ProofStep generateAssm(LogicOperation logicexpression) { @Override public void automate() { - + // Do nothing } @Override public void initializeProof(List assms, LogicOperation goal) { - + // Do nothing } }; } diff --git a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Transformers.java b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Transformers.java index 5c799bcf..4d88cce8 100644 --- a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Transformers.java +++ b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/mock/Transformers.java @@ -39,12 +39,12 @@ protected ProofStep generateAssm(LogicOperation logicexpression) { @Override public void automate() { - + // Do nothing } @Override public void initializeProof(List assms, LogicOperation goal) { - + // Do nothing } }; } diff --git a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java index b5a530b5..92a74bf3 100644 --- a/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java +++ b/domain/use-cases/base-use-case/src/test/java/com/dan323/uses/test/ProofParserTest.java @@ -44,7 +44,7 @@ protected ProofStep generateAssm(LogicOperation logicexpression) @Override public void automate() { - + // Do nothing } @Override