]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaOr.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / FormulaOr.java
diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaOr.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaOr.java
new file mode 100644 (file)
index 0000000..83531cc
--- /dev/null
@@ -0,0 +1,84 @@
+package com.example.furt.myapplication;
+
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class FormulaOr extends GenericFormula implements Formula
+{
+    Formula leftF;
+    Formula rightF;
+    int leftPriority;
+    int rightPriority;
+    FormulaOr(Formula F1,Formula F2)
+    {
+        priority=13;
+        leftF=F1;
+        rightF=F2;
+        leftPriority=13;
+        rightPriority=14;
+    }
+
+    @Override
+    public String Draw(int p)
+    {
+        if (priority >= p)
+            return leftF.Draw(leftPriority)+"∨"+rightF.Draw(rightPriority);
+        else
+            return("(")+leftF.Draw(leftPriority)+"∨"+rightF.Draw(rightPriority)+")";
+    }
+
+    public List<IntroductionRule> introductionRules(){
+        List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
+        nodes.addAll(super.introductionRules()); //eredita la R.A.A.
+
+        //Introduzione sinistra dell'or
+        RuleIntroduction orIntroductionLeft=new RuleIntroduction("∨i(L)",6);
+        Node orLeft=new Node(leftF);
+        Node thisNodeL=new Node(this);
+        thisNodeL.addChild(orLeft);
+        orIntroductionLeft.tempRule=thisNodeL;
+        nodes.add(orIntroductionLeft);
+
+        //Introduzione destra dell'or
+        RuleIntroduction orIntroductionRight=new RuleIntroduction("∨i(R)",5);
+        Node orRight=new Node(rightF);
+        Node thisNodeR=new Node(this);
+        thisNodeR.addChild(orRight);
+        orIntroductionRight.tempRule=thisNodeR;
+        nodes.add(orIntroductionRight);
+
+        return nodes;
+    }
+
+    public List<EliminationRule> EliminationRules()
+    {
+        List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+        nodes.add(new RuleOrElimination(this));
+        return nodes;
+    }
+
+    @Override
+    public boolean Fill(Formula Filler) {
+        if(leftF.toString().equals("_")) {
+            this.leftF = Filler;
+            return true;
+        }
+        else if(rightF.toString().equals("_")) {
+            this.rightF = Filler;
+            return true;
+        }
+        return leftF.Fill(Filler) || rightF.Fill(Filler);
+    }
+
+    @Override
+    public boolean setCursor() {
+        return leftF.setCursor() || rightF.setCursor();
+    }
+
+    @Override
+    public Formula duplicate() {
+        return new FormulaOr(leftF.duplicate(),rightF.duplicate());
+    }
+}
+