More modal tests

domain/proof-structures/framework.deduction/src/main/java/com/dan323/proof/generic/proof/Proof.java

@@ -9,7 +9,7 @@
 
 public abstract class Proof<T extends LogicOperation, Q extends ProofStep<T>> {
 
-    private List<T> assms;
+    private List<T> assms = List.of();
     private T goal;
     private final List<Q> steps = new ArrayList<>();
 

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<Integer> sources, ModalOperation extraInfo, String state){
+    public static AbstractModalAction parseAction(String name, List<Integer> 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));

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;

domain/proof-structures/implementation.deduction.modal/src/test/java/com/dan323/proof/modal/ParseModalActionTest.java

@@ -2,15 +2,16 @@
 
 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;
 
 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);
+    }
 }

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<P extends Proof<T,Q>, T extends LogicOperation, Q extends ProofStep<T>> {
+import java.util.List;
 
-    P parseProof(String proof);
+public interface ProofParser<P extends Proof<T, Q>, T extends LogicOperation, Q extends ProofStep<T>, A extends Action<T, Q, P>> {
+
+    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<A>)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 <T extends LogicOperation, Q extends ProofStep<T>> List<T> extractAssumptions(List<Q> steps) {
+        return steps.stream()
+                .takeWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass"))
+                .map(ProofStep::getStep)
+                .toList();
+    }
+
+    private static <T extends LogicOperation, Q extends ProofStep<T>> List<Q> skipInitAssumptions(List<Q> steps) {
+        return steps.stream()
+                .dropWhile(action -> action.getAssumptionLevel() == 0 && action.getProof().getNameProof().contains("Ass"))
+                .toList();
+    }
 }

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
                     }
                 };
             }
@@ -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();
+            }
         };
     }
 

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
                     }
                 };
             }

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<Proof<LogicOperation, ProofStep<LogicOperation>>, LogicOperation, ProofStep<LogicOperation>, Action<LogicOperation, ProofStep<LogicOperation>, Proof<LogicOperation, ProofStep<LogicOperation>>>> {
+
+        @Override
+        public String logic() {
+            return "l1";
+        }
+
+        @Override
+        public Proof<LogicOperation, ProofStep<LogicOperation>> getNewProof() {
+            return new Proof<>() {
+                @Override
+                public List<? extends Action<LogicOperation, ProofStep<LogicOperation>, ? extends Proof<LogicOperation, ProofStep<LogicOperation>>>> parse() {
+                    return List.of();
+                }
+
+                @Override
+                protected ProofStep<LogicOperation> generateAssm(LogicOperation logicexpression) {
+                    return new ProofStep<>(0, logicexpression, new ProofReason("Ass", List.of()));
+                }
+
+                @Override
+                public void automate() {
+                    // Do nothing
+                }
+
+                @Override
+                public void initializeProof(List<LogicOperation> assms, LogicOperation goal) {
+                    getSteps().clear();
+                    setAssms(assms);
+                }
+            };
+        }
+
+        @Override
+        public ProofStep<LogicOperation> parseLine(String line) {
+            return new ProofStep<>(0, new LogicOperation() {
+                @Override
+                public String toString() {
+                    return "P";
+                }
+            }, new ProofReason("Ass", List.of()));
+        }
+    }
+}

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<NaturalDeduction,ClassicalLogicOperation,ProofStep<ClassicalLogicOperation>> {
+public class ParseClassicalProof implements ProofParser<NaturalDeduction, ClassicalLogicOperation, ProofStep<ClassicalLogicOperation>, 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<ClassicalLogicOperation> parseLine(String line) {
+    public ProofStep<ClassicalLogicOperation> parseLine(String line) {
         var array = line.toCharArray();
         int i = 0;
         while (array[i] == ' ') {