Ported to latest version of Android SDK

[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / FormulaNot.java

diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaNot.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaNot.java
new file mode 100644 (file)
index 0000000..6bd80e5
--- /dev/null
+++ b/mainActivity/app/src/main/java/com/example/furt/myapplication/FormulaNot.java
@@ -0,0 +1,68 @@
+package com.example.furt.myapplication;
+
+import android.graphics.Paint;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class FormulaNot extends GenericFormula implements Formula{
+    Paint p=new Paint();
+    Formula Operand;
+    int priority;
+    int argPriority;
+    FormulaNot(Formula F)
+    {
+        Operand=F;
+        priority=20;
+        argPriority=100;
+    }
+    @Override
+    public String Draw(int p)
+    {
+        if (priority >= p)
+            return "¬"+Operand.Draw(20);
+        else
+            return("¬("+Operand.Draw(20)+")");
+    }
+
+    public List<IntroductionRule> introductionRules(){
+        List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
+
+        //Introduzione del not (NOTA: il not non eredita la regola di riduzione ad assurdo)
+        RuleIntroduction notIntro=new RuleIntroduction("¬i",4);
+        Node notN=new Node(new FormulaBOT());
+        List<Formula> notHP=new ArrayList<Formula>();
+        notHP.add(Operand);
+        notN.addHPFormula(notHP,true);
+        Node thisNode=new Node(this);
+        thisNode.addChild(notN);
+        notIntro.tempRule=thisNode;
+        nodes.add(notIntro);
+        return nodes;
+    }
+    public List<EliminationRule> EliminationRules()
+    {
+        List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+        nodes.add(new RuleNotElimination(this));
+        return nodes;
+    }
+
+    @Override
+    public boolean Fill(Formula Filler) {
+        if(Operand.toString().equals("_")) {
+            Operand = Filler;
+            return true;
+        }
+        return Operand.Fill(Filler);
+    }
+
+    @Override
+    public boolean setCursor() {
+        return Operand.setCursor();
+    }
+
+    @Override
+    public Formula duplicate() {
+        return new FormulaNot(Operand.duplicate());
+    }
+}