mainActivity/src/com/example/furt/myapplication/Node.java

   1 package com.example.furt.myapplication;
   2
   3 import android.graphics.Color;
   4 import android.util.TypedValue;
   5 import android.view.Gravity;
   6 import android.view.View;
   7 import android.view.ViewGroup;
   8 import android.view.ViewTreeObserver;
   9 import android.widget.RelativeLayout;
  10 import android.widget.TextView;
  11
  12 import java.util.ArrayList;
  13 import java.util.List;
  14
  15
  16 public class Node implements Tree {
  17
  18     static int FIELD_UNSET = -1;
  19     static int OPEN=0;
  20     static int FAKE=1;
  21     static int CLOSED=2;
  22     static int FAKE_CLOSED=3;
  23     static int CANCELED=4;
  24     static int FAKE_CANCELED=5;
  25
  26     Formula F; //formula legata al nodo
  27     String ruleName; //nome della regola associata a questo nodo
  28     List<Node> Children = new ArrayList<Node>(); //Nodi figli
  29     List<Hypothesis> NodeHP = new ArrayList<Hypothesis>(); //ipotesi associate
  30     Node Father; //puntatore al padre
  31     View.OnClickListener handler; //touchHandler per far comparire il pop-up delle regole
  32     View.OnLongClickListener longHandler; //touchHandler per far comparire il menu con tutte le regole
  33     boolean hasFocus; //indica se questo nodo è quello selezionato
  34     int status; //stato del nodo (chiuso, aperto,fake...)
  35     RelativeLayout global; //layout in cui si trova l'albero
  36     BorderedTextView view; //view contenente questo oggetto
  37     TextView ruleView; //view contenente l'intestazione della regola
  38
  39     float baseLine; //baseLine del Node: corrisponde alla lunghezza dell'overline
  40     float leftOffset; //leftOffset: corrisponde alla larghezza della porzione di albero a sinistra del nodo
  41     float rightOffset; //rightOffset: porzione di albero a destra del nodo
  42     float maxWidth; //larghezza del sottoalbero di questo nodo (comprensiva del nodo stesso)
  43
  44     Node(Formula F) {
  45         this.F = F;
  46         view = null;
  47         handler = null;
  48         ruleName="";
  49         Father = null;
  50         status=OPEN;
  51         hasFocus = false;
  52         leftOffset = 0;
  53         rightOffset = 0;
  54         baseLine = getBaseWidth();
  55         maxWidth = baseLine;
  56     }
  57
  58     /**************SetView**************+*****/
  59     /*****************************************/
  60     /*******Setta la TextView del node  ******/
  61     /** e il layout in cui deve comparire  ***/
  62     /*****************************************/
  63
  64     public void setView(BorderedTextView t,RelativeLayout r) {
  65         view = t;
  66         ruleView =new TextView(t.getContext());
  67         global=r;
  68     }
  69
  70
  71     /**************Count****************+*****/
  72     /*****************************************/
  73     /*******Restituisce il numero di    ******/
  74     /*************nodi dell'albero ***********/
  75     /*****************************************/
  76
  77     int count()
  78     {
  79         int ris=1;
  80         for (Node n:Children)
  81             ris+=n.count();
  82         return ris;
  83     }
  84     /**************addHP****************+*****/
  85     /*****************************************/
  86     /*******Metodi per aggiungere ipotesi*****/
  87     /*******sotto forma di Hypothesis o di****/
  88     /*************Formula*********************/
  89     /*****************************************/
  90
  91     public void addHPFormula(List<Formula>List,boolean deleted) {
  92         loop:for (Formula newHp:List) {
  93             for (Hypothesis oldHp: NodeHP) {
  94                 if (oldHp.HP.toString().equals(newHp.toString())) { //ipotesi già presente: passo alla prossima
  95                     continue loop;
  96                 }
  97             }
  98             NodeHP.add(new Hypothesis(newHp, deleted));
  99         }
 100     }
 101
 102     public void addHPList(List<Hypothesis>List) {
 103         loop:for (Hypothesis newHp:List) {
 104             for (Hypothesis oldHp: NodeHP) {
 105                 if (oldHp.HP.toString().equals(newHp.HP.toString())) { //ipotesi già presente: passo alla prossima
 106                     continue loop;
 107                 }
 108             }
 109             Hypothesis copyHP=new Hypothesis(newHp.HP, newHp.isDeleted);
 110             copyHP.fromNode=newHp.fromNode;
 111             NodeHP.add(copyHP);
 112         }
 113     }
 114
 115     /*****************************************/
 116     /******* Algoritmo di ricerca del ********/
 117     /******* focus: restituisce false ********/
 118     /******* se la dimostrazione è completa***/
 119
 120     public boolean searchFocus(Node caller)
 121     {
 122         if (Children.size()==0) //caso base: controllo se il focus può essere su di me
 123         {
 124             if (status!=OPEN && status!=FAKE) //nodo chiuso: il focus non può essere su di me
 125                 return false;
 126             hasFocus=true;                             //posso assumere il focus
 127             if (handler!=null)
 128                 handler.onClick(view);
 129             return true;
 130         }
 131         //passo induttivo: vado su tutti i miei figli, poi su mio padre. Termino se il padre è null.
 132         for (Node n:Children) {
 133             if (caller != null)
 134                 if (n == caller) //per ogni figlio diverso dal chiamante
 135                 {
 136                     continue;
 137                 }
 138             if(n.searchFocus(null))
 139                 return true;
 140         }
 141         if (caller==null) //ero stato chiamato da mio padre: è inutile richiamarlo
 142             return false;
 143         else if (Father==null)
 144             return false; //padre null: l'albero è dimostrato e non ci sono nodi a cui dare il focus.
 145         else
 146             return Father.searchFocus(this); //propaga il searchFocus sul padre
 147     }
 148     public void addChild(Node N) {
 149         N.Father = this;
 150         Children.add(N);
 151         Node tmp=Father;
 152         //c'è un nuovo nodo nell'albero: tutti i campi dell'algoritmo di disegno sono da ricalcolare per questo ramo
 153         baseLine=FIELD_UNSET;
 154         maxWidth=FIELD_UNSET;
 155         leftOffset=FIELD_UNSET;
 156         rightOffset=FIELD_UNSET;
 157         while (tmp!=null)
 158         {
 159             tmp.baseLine=FIELD_UNSET;
 160             tmp.leftOffset=FIELD_UNSET;
 161             tmp.rightOffset=FIELD_UNSET;
 162             tmp.maxWidth=FIELD_UNSET;
 163             tmp=tmp.Father;
 164         }
 165     }
 166
 167     public float getBaseWidth() {
 168         return F.size();
 169     }
 170
 171     public float getMaxWidth() //ritorna la larghezza massima del sottoalbero
 172     {
 173         if (maxWidth!=FIELD_UNSET)
 174             return maxWidth;
 175         else
 176             maxWidth=getLeftOffset()+getBaseWidth()+getRightOffset();
 177         return (maxWidth);
 178     }
 179
 180     public float getLineWidth()
 181     {
 182         if (baseLine!=FIELD_UNSET)
 183             return baseLine;
 184         else
 185         {
 186             baseLine=Math.max(getUpLine(),getBaseWidth()); //la baseline è il massimo valore tra la upLine e la baseWidth
 187             return baseLine;
 188         }
 189     }
 190     public float getUpLine() //calcola la upLine, ovvero la dimensione prevista del sottoalbero assumendo il nodo attuale di lunghezza unitaria
 191     {
 192         float spaceSize= DrawActivity.spaceSize;
 193         if (Children.size()==0)
 194             return(getBaseWidth());
 195         int res=0;
 196         for(Node n:Children)
 197             res+=(n.getMaxWidth())+spaceSize;
 198         res-=spaceSize;
 199         res-=Children.get(0).getLeftOffset(); //la linea deve fermarsi all'inizio della formula del primo figlio sinistro
 200         res-=Children.get(Children.size()-1).getRightOffset(); //la linea deve finire alla fine della formula dell'ultimo figlio destro
 201         return res;
 202     }
 203
 204     /**Calcolo del leftOffset
 205      * esso è uguale al leftOffset del primo figlio, a cui aggiungere la porzione di overline a sinistra della formula del nodo
 206      * o rimuovere la mezza differenza tra la baseWidth e la upLine. Se il leftOffset risulterebbe negativo, diventa nullo.
 207      */
 208
 209     public float getLeftOffset() {
 210         if (leftOffset != FIELD_UNSET) {
 211             return leftOffset;
 212         }
 213         else {
 214             if (Children.size() == 0) //foglia
 215                 leftOffset=0;
 216             else
 217                 leftOffset=Math.max(Children.get(0).getLeftOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
 218             return leftOffset;
 219         }
 220     }
 221
 222     public float getRightOffset()
 223     {
 224         if (rightOffset!=FIELD_UNSET)
 225             return rightOffset;
 226         else {
 227             if (Children.size() == 0) //foglia
 228                 rightOffset=0;
 229             else
 230                 rightOffset=Math.max(Children.get(Children.size() - 1).getRightOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
 231             return rightOffset;
 232         }
 233     }
 234
 235     public float getMaxHeight() //calcolo dell'altezza massima dell'albero attuale.
 236     {
 237         float baseRes=F.height();
 238         float res=baseRes;
 239         for (Node n:Children)
 240         {
 241             float tempH=n.getMaxHeight()+baseRes;
 242             if(tempH>res)
 243                 res=tempH;
 244         }
 245         return res;
 246     }
 247
 248     void Refactor() //metodo di supporto: svuota i campi dell'intero sottoalbero che verranno ricalcolati dall'algoritmo alla prossima applicazione
 249     {
 250         baseLine=FIELD_UNSET;
 251         leftOffset=FIELD_UNSET;
 252         rightOffset=FIELD_UNSET;
 253         maxWidth=FIELD_UNSET;
 254         for(Node n:Children)
 255             n.Refactor();
 256     }
 257
 258
 259     public void Clean() //metodo di supporto: rimuove dal layout legato al Node tutte le view presenti
 260     {
 261         global.removeAllViews();
 262     }
 263
 264     public boolean isCorrect() //controlla per l'intero sottoalbero se esso è privo di nodi fake.
 265     {
 266         if (status==FAKE || status==FAKE_CANCELED || status==FAKE_CLOSED)
 267             return false;
 268         else for (Node n:Children)
 269             if (!n.isCorrect())
 270                 return false;
 271         return true;
 272
 273     }
 274
 275     public void Draw()
 276     {
 277         float interval=0; //intervallo di spazio da sommare nella creazione dei figli
 278         float spaceSize= DrawActivity.spaceSize; //dimensione della spaziatura tra i sottoalberi
 279         int childNo=Children.size(); //numero di figli del nodo attuale
 280         if (childNo==0) //foglia: possibile ramo dimostrato
 281
 282         {
 283             view.setBorders(null); //le foglie non hanno overline
 284             if (status!=OPEN && status!=FAKE) { //nodo chiuso
 285                 view.setTextColor(Color.GRAY);
 286                 if (hasFocus) //avevo il focus: provo a darlo ad uno dei miei fratelli
 287                 {
 288                     if (!(Father.searchFocus(this))) { //focus inapplicabile nell'albero: dimostrazione completata.
 289                         DrawActivity.finishedTree(view.getContext());
 290                         return;
 291                     }
 292                     hasFocus = false;
 293                 }
 294                 if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
 295                     view.setWidth((int) F.sizeDeleted());
 296                     view.setText(F.toStringDeleted());
 297                     view.setOnClickListener(null); //rimuove eventuali listener per evitare il proseguimento dell'albero
 298                     /**NOTA: è possibile permettere all'utente di proseguire la dimostrazione
 299                      * di un ramo chiuso commentando la riga precedente e aggiungendo nel touchnodeHandler
 300                      * un'controllo che, in caso di nodo chiuso cliccato, lo riapre e gli riaffida il focus.
 301                      */
 302                 }
 303                 return;
 304             }
 305             if (hasFocus && DrawActivity.selectedNode!=this)
 306                 handler.onClick(view);
 307             else if (hasFocus) //hasFocus: must be colored red anyway
 308                 view.setTextColor(Color.RED);
 309             return;
 310         }
 311
 312         ruleView.setText(ruleName);
 313         ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
 314         RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 315         intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
 316         intlp.addRule(RelativeLayout.ABOVE,view.getId());
 317         ruleView.setLayoutParams(intlp);
 318         global.addView(ruleView);
 319
 320         hasFocus=false; //se sono arrivato a questo punto il nodo non è una foglia e non può avere il focus di default
 321
 322         for (int i=0;i<childNo;i++) {
 323             final Node newChild=Children.get(i); //recupero l'i-esimo figlio
 324             RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 325             final BorderedTextView childView=new BorderedTextView(view.getContext());
 326             childView.setBorders(DrawActivity.b);
 327             lp.addRule(RelativeLayout.ABOVE, view.getId());
 328             if (i==0) //first child
 329             {
 330                 float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0); //il primo figlio è posizionato a sinistra del padre, con un ulteriore offset
 331                                                                                                                // sinistro pari allo scarto della sua overline
 332                 if (getLineWidth()>getUpLine()) //sono più grande dell'overline prevista: aggiungo un ulteriore offset al figlio
 333                     leftPos+=((getLineWidth()-getUpLine())/2);
 334                 lp.setMargins(Math.round(leftPos), 0, 0, 0); //leftPos è il margine sinistro del figlio
 335                 childView.setLeft(Math.round(leftPos));
 336             }
 337             else {
 338                 lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0); //figlio intermedio: basta aggiungere l'interval alla posizione sinistra del padre
 339                 childView.setLeft(Math.round(view.getLeft() + interval));
 340             }
 341             childView.setLayoutParams(lp);
 342             childView.setId(DrawActivity.globalId++);
 343             childView.setText(newChild.F.toString());
 344             childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
 345             childView.setGravity(Gravity.CENTER); //formula al centro della sua overline
 346             childView.setWidth(Math.round(newChild.getLineWidth()));
 347             global.addView(childView);
 348             childView.getViewTreeObserver().addOnGlobalLayoutListener(new ViewTreeObserver.OnGlobalLayoutListener() {
 349                 @Override
 350                 public void onGlobalLayout() {
 351                     newChild.setView(childView,global);
 352                     if(newChild.handler==null)
 353                         newChild.handler=new touchnodeHandler(newChild);
 354                     newChild.longHandler=new longnodeHandler(newChild);
 355                     newChild.view.setOnClickListener(newChild.handler);
 356                     newChild.view.setOnLongClickListener(newChild.longHandler);
 357                     childView.getViewTreeObserver().removeOnGlobalLayoutListener(this);
 358                     newChild.Draw();
 359                 }
 360             });
 361             if (i!=childNo-1) //l'ultimo figlio non ha intervalli
 362             {
 363                 float leftOverflow=Math.max((Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2,0);
 364                 interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow)); //devo aggiungere all'interval la basewidth del figlio attuale, il rightoffset del figlio attuale e il leftOffset del figlio successivo.
 365                 interval+=spaceSize;
 366                 if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
 367                     interval+=newChild.getLeftOffset();
 368             }
 369         }
 370     }
 371     void Resize() //metodo per ridisegnare l'albero dopo un pinch zoom: l'algoritmo applicato è uguale a quello del metodo Draw()
 372     {
 373         int i;
 374         float interval=0; //intervallo di spazio da sommare nella creazione dei figli
 375         float spaceSize= DrawActivity.spaceSize;
 376         int childNo=Children.size();
 377         if (childNo!=0)
 378         {
 379
 380             ruleView.setText(ruleName);
 381             ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
 382             RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 383             intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
 384             int sum=0;
 385             sum+=F.height();
 386             Node tmp=Father;
 387             while (tmp!=null)
 388             {
 389                 sum+=tmp.F.height();
 390                 tmp=tmp.Father;
 391             }
 392             intlp.setMargins(0,0,0,sum);
 393             intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
 394             ruleView.setLayoutParams(intlp);
 395         }
 396         for (i=0;i<childNo;i++) {
 397             Node newChild=Children.get(i);
 398             RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
 399             TextView childView=Children.get(i).view;
 400             lp.addRule(RelativeLayout.ABOVE,view.getId());
 401             if (i==0) //first child
 402             {
 403                 float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
 404                 if (getLineWidth()>getUpLine())
 405                     leftPos+=((getLineWidth()-getUpLine())/2);
 406                 lp.setMargins(Math.round(leftPos), 0, 0, 0);
 407                 childView.setLeft(Math.round(leftPos));
 408             }
 409             else {
 410                 lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
 411                 childView.setLeft(Math.round(view.getLeft() + interval));
 412             }
 413             childView.setLayoutParams(lp);
 414             childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
 415
 416             if(newChild.status==CANCELED || newChild.status==FAKE_CANCELED)
 417                 childView.setWidth((int) ((newChild.F.sizeDeleted())));
 418             else
 419                 childView.setWidth(Math.round(newChild.getLineWidth()));
 420
 421             newChild.Resize();
 422
 423             if (i!=childNo-1) //l'ultimo figlio non ha intervalli
 424             {
 425                 float leftOverflow=(Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2;
 426                 interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
 427                 interval+=spaceSize;
 428                 if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
 429                     interval+=newChild.getLeftOffset();
 430             }
 431
 432         }
 433
 434     }
 435
 436 }