]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/FormulaNot.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / FormulaNot.java
diff --git a/mainActivity/src/com/example/furt/myapplication/FormulaNot.java b/mainActivity/src/com/example/furt/myapplication/FormulaNot.java
deleted file mode 100755 (executable)
index 6bd80e5..0000000
+++ /dev/null
@@ -1,68 +0,0 @@
-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());
-    }
-}