/* Feature wish list:

 * Allow to highlight rectangular area in BinopEditor
 * Add the capability to define new constants for closed terms
 * Make binop draw routine more efficient: calculate grid, colors, and
 *  status in a seperate thread and only when needed.

 */

import java.applet.*;
import java.awt.*;
import java.awt.event.*;
import java.util.Vector;

// -----------------------------------------------------------------

/** 
 * This applet allows the user to edit a finite lambda model, and to
 * calculate the denotations of untyped lambda terms therein. See <a
 * href=" http://www.math.lsa.umich.edu/~selinger/finmod/">
 * http://www.math.lsa.umich.edu/~selinger/finmod/</a>.
 *
 * @author Peter Selinger 
 * @version 1.3, March 30, 1998
 */

public class FiniteLambdaModel extends Applet
{
  MainPanel mainpanel;
  TermManagerPanel termmanagerpanel;
  Button morebutton, lessbutton;
  FinMod finmod;

  GridBagLayout gridbag;

  static String BUGFIX_PARAM="bugfix";
  static String INITTERMS_PARAM="initterms";
  static String POSETDIM_PARAM="posetdim";
  static String FINMODINIT_PARAM="finmodinit";

  static String[] initterms_default 
              = {"\\x.xx", "\\xyz.x(yz)", "(\\x.xxx)(\\x.xxx)"};
  static Dimension posetdim_default = new Dimension(200,150);

  /** applet info support */
  public String getAppletInfo() 
  {
    return "Name: FiniteLambdaModel\r\n" + "Author: Peter Selinger\r\n"; 
  }
  
  /** applet parameter information */
  public String[][] getParameterInfo()  
  {
    String[][] info = {
      { BUGFIX_PARAM, "String", "if present, we work around a scrollbar bug in "+
	"appletviewer for Solaris JDK 1.1.5" },
      { INITTERMS_PARAM, "String[]", 
	"terms to display initially, separated by ';'" },
      { FINMODINIT_PARAM, "String", 
	"a string of instructions to initialize the finite model" },
      { POSETDIM_PARAM, "int x int", "dimension of poset editor canvas" },
    };
    return info;		
  }
  
  /** called by the AWT when an applet is first loaded or reloaded */ 
  public void init()
  {
    String param;

    // read posetdim parameter
    param = getParameter(POSETDIM_PARAM);
    Boss.posetdim = posetdim_default;
    if (param!=null) {
      int i=param.indexOf('x');
      if (i>=0) {
	Boss.posetdim=new Dimension(Integer.parseInt(param.substring(0,i)),
        	Integer.parseInt(param.substring(i+1,param.length())));
      }
    }

    // read other parameters
    Boss.bugfix = getParameter(BUGFIX_PARAM);
    Boss.finmodinit = getParameter(FINMODINIT_PARAM);
    param = getParameter(INITTERMS_PARAM);
    Boss.initterms = initterms_default;
    if (param!=null) {
      Vector v = new Vector();
      int i=0;
      int j;
      while ((j=param.indexOf(';',i))>=0) {
	v.addElement(param.substring(i,j));
	i=j+1;
      }
      v.addElement(param.substring(i,param.length()));
      Boss.initterms=new String[v.size()];
      v.copyInto(Boss.initterms);
    }

    // create finmod  need to move this earlier???
    finmod = new FinMod(Boss.posetdim, Boss.finmodinit);

    // create components
    mainpanel = new MainPanel(finmod);
    termmanagerpanel = new TermManagerPanel(finmod);
    morebutton = new Button("More Terms");
    lessbutton = new Button("Fewer Terms");

    Boss.flm = this;
    Boss.morebutton = morebutton;
    Boss.lessbutton = lessbutton;

    // prepare layout
    gridbag = new GridBagLayout();
    GridBagConstraints c = new GridBagConstraints();
    setLayout(gridbag);

    // add mainpanel
    c.fill      = GridBagConstraints.BOTH;
    c.gridwidth = 1;
    c.gridheight= 2;
    c.weighty   = 1.0;
    c.weightx   = 1.0;
    gridbag.setConstraints(mainpanel,c);
    add(mainpanel);

    // add termmanagerpanel
    c.fill      = GridBagConstraints.BOTH;
    c.insets    = new Insets(0,5,0,0);
    c.weighty   = 1.0;
    c.gridheight= 1;
    c.gridwidth = GridBagConstraints.REMAINDER;
    gridbag.setConstraints(termmanagerpanel,c);
    add(termmanagerpanel);

    // add buttons
    c.fill      = GridBagConstraints.NONE;
    c.weighty   = 0.0;
    c.weightx   = 0.5;
    c.anchor    = GridBagConstraints.EAST;
    c.gridwidth = 1;
    c.insets    = new Insets(5,5,0,5);
    gridbag.setConstraints(morebutton,c);
    add(morebutton);
    c.anchor    = GridBagConstraints.WEST;
    c.gridwidth = GridBagConstraints.REMAINDER;
    gridbag.setConstraints(lessbutton,c);
    add(lessbutton);
    
    validate();

    Boss.bs.adjustscrollbars();
  }

  /** draws a box around this panel. */
  public void paint(Graphics g) {
    Dimension d = size();
    g.setColor(getBackground());
    g.draw3DRect(2,2, d.width-5, d.height-5,false);
  }

  /** creates a little breathing space */
  public Insets insets() {
    return new Insets(8,8,8,8);
  }

  /** handles events from the More and Less buttons */
  public boolean action(Event e, Object arg) {
    Object target = e.target;
    
    if (target == morebutton) { 
      Boss.tmp.moreevent();
      return true;
    }
    if (target == lessbutton) { 
      Boss.tmp.lessevent();
      return true;
    }
    return false;
  }
}

// -----------------------------------------------------------------

/** a panel to display a PosetEditor together with a scrollable
 *  BinopEditor, a statusline and a few buttons. */

class MainPanel extends Panel
{
  PosetEditor poseteditor;
  Button deletebutton, labelbutton;
  BinopScroller binopscroller;
  Label statusline;
  
  MainPanel(FinMod finmod)
  {
    Label text;

    // create components
    poseteditor = new PosetEditor(finmod); 
    deletebutton=new Button("Delete");
    deletebutton.disable();
    labelbutton=new Button("Hide Labels");
    binopscroller = new BinopScroller(finmod);
    statusline = new Label("");
    
    Boss.deletebutton = deletebutton;
    Boss.labelbutton = labelbutton;
    Boss.statusline = statusline;

    // prepare layout
    GridBagLayout gridbag = new GridBagLayout();
    GridBagConstraints c = new GridBagConstraints();
    setLayout(gridbag);

    // add text
    c.fill      = GridBagConstraints.BOTH;
    c.gridwidth = GridBagConstraints.REMAINDER;
    c.weighty   = 0.0;
    c.weightx   = 1.0;
    text = new Label("Edit a poset:");
    gridbag.setConstraints(text,c);
    add(text);

    // add poseteditor
    c.anchor    = GridBagConstraints.CENTER;
    c.fill      = GridBagConstraints.NONE;
    gridbag.setConstraints(poseteditor, c);
    add(poseteditor);

    // add a few buttons
    c.fill      = GridBagConstraints.NONE;
    c.gridwidth = 1;
    c.insets    = new Insets(5,5,5,5);
    c.weighty   = 0.0;
    c.anchor    = GridBagConstraints.EAST;
    gridbag.setConstraints(deletebutton, c);
    add(deletebutton);
    c.anchor    = GridBagConstraints.WEST;
    c.gridwidth = GridBagConstraints.REMAINDER;
    gridbag.setConstraints(labelbutton, c);
    add(labelbutton);

    // add text
    c.fill      = GridBagConstraints.BOTH;
    c.insets    = new Insets(5,0,0,0);
    text = new Label("Edit a binary operation:");
    gridbag.setConstraints(text,c);
    add(text);

    // add binopscroller
    c.insets    = new Insets(5,0,0,0);
    c.weighty   = 1.0;
    gridbag.setConstraints(binopscroller, c);
    add(binopscroller);

    // add a status line
    c.weighty   = 0.0;
    gridbag.setConstraints(statusline, c);
    add(statusline);

    // do not need to validate here: this is done from top down.
  }

  /** draws a box around this panel. */
  public void paint(Graphics g) {
    Dimension d = size();
    g.setColor(getBackground());
    g.draw3DRect(0,0, d.width - 1, d.height - 1,true);
  }

  /** breathing space */  
  public Insets insets() {
    return new Insets(5,5,5,5);
  }
  
  /** handles events from the Label and Delete buttons */
  public boolean action(Event e, Object arg) {
    Object target = e.target;
    
    if (target == deletebutton) { 
      return poseteditor.deleteaction();
    }
    if (target == labelbutton) { 
      return poseteditor.labelsaction();
    }
    return false;
  }
}

// -----------------------------------------------------------------

/** a PosetEditor sits on top of a FinMod, and provides methods for
 * painting, as well as event handling of user editing moves.<p>
 *
 * Definition of event state:<p>
 * 
 * <pre>
 *   button = UP: 
 *     focus = NONE
 *     focus = NODE(current)
 *     focus = EDGE(from_node,to_node)   
 *   button = DOWN: 
 *     action = NONE
 *     action = EDGE(from_node,to_node)
 *     action = MOVE(current,newfocus) 
 *     action = DRAW(current,newfocus): 
 *       showline = NONE
 *	 showline = EXISTING(to_node)
 *	 showline = NEW(to_x,to_y)<p>
 *
 *   moveframe is null if not set.<p>
 *				
 *   kbfocus = true/false: do we have keyboard focus?
 *     
 * </pre>
 * button==UP or DOWN, reflecting what this class has seen of the mouse
 * button. The environment should guarantee that the sequence of events
 * is (Down Drag* Up or Move)* interleaved with key-events. If button
 * is UP, there may be a focus node or none. If button is DOWN, action
 * can be NONE (do nothing), MOVE (current node is highlighted for
 * moving; newfocus is NONE or NODE), DRAW (current node is highlighted
 * for drawing an edge from it, newfocus is NONE or NODE). In the last
 * case, showline is NONE if no outlined edge is being shown, EXISTING
 * if edge from current node to existing to_node is being shown, and
 * NEW if edge from current node to outlined node at x,y is being
 * shown.<p>
 *
 * At any time, the moveframe, if not null, determines an area within
 * which the current node may be moved. It is only calculated on
 * demand, i.e. when an actual drag occurs.
 */

class PosetEditor extends Canvas 
{
  int width, height;
  FinMod finmod;

  // event state
  int button, focus, action, showline;
  final int UP=0, DOWN=1, NONE=2, NODE=3, MOVE=4, YES=5, DRAW=6,
    EXISTING=7, NEW=8, EDGE=9;
  int current, newfocus, to_node, to_x, to_y;
  int from_node;
  MoveFrame moveframe;

  boolean kbfocus=false;
  boolean displaylabels=true;

  // semantically constants; maybe later parameters
  Color nodecolor=Color.black;  // color of normal node
  Color movenodecolor=Color.red; // color of moveable node
  Color drawnodecolor=Color.blue; // color of snap node drawing edge
  Color edgecolor=Color.black;    // color of normal edge
  Color drawedgecolor=Color.blue; // color of edge being drawn
  Color focusedgecolor=Color.red; // color of edge being drawn
  Color framecolor=Color.black;   // frame
  Color bgcolor=Color.white;      // background
  Color textcolor=Color.black;    // text

  // for double-buffering
  Image offImage;
  Graphics og;
  Dimension offDimension;

  /** Initialize */
  PosetEditor(FinMod finmod)
  {
    Boss.pe = this;    // and register with it
    this.width = finmod.width;
    this.height = finmod.height;
    this.finmod = finmod;

    button = UP;
    focus = NONE;
    requestFocus();
  }

  // size stuff 
  public Dimension preferredSize() {
    return minimumSize();
  }
  
  public synchronized Dimension minimumSize() {
    return new Dimension(width,height);
  }
  
  // -------------------------------------------------------------------------
  // Paint current state

  public void update(Graphics g)  //paint yourself in g
  {
    int n = finmod.size();
    Point c;

    //need to create offscreen buffer?
    if (og==null || width != offDimension.width 
	|| height != offDimension.height) {
      offDimension = new Dimension(width,height);
      offImage = createImage(width, height);
      og = offImage.getGraphics();
    }

    //clear the background
    og.setColor(bgcolor);
    og.fillRect(0, 0, width, height);

    // paint frame
    og.setColor(Color.gray);
    og.draw3DRect(1,1,width-2,height-2,false);
    if (kbfocus) {
      og.setColor(Color.black);
      og.drawRect(0,0,width-1,height-1);
    } else {
      og.draw3DRect(0,0,width-1,height-1,false);
    }

    // paint nodes
    n=finmod.size();   
    for (int i=0; i<n; i++) {
      c=finmod.coord(i);
      og.setColor(nodecolor);
      paintnode(og,c.x,c.y,displaylabels,finmod.label(i));
    }

    // paint edges
    og.setColor(edgecolor);       
    for (int i=0; i<n; i++)   
      for (int j=i+1; j<n; j++) 
	if (finmod.minrel(i,j) || finmod.minrel(j,i)) { // edge betw. i and j
	  paintedge(og,i,j);
	}
  
    // paint highlighted edge
    if ((button==UP && focus==EDGE) || (button==DOWN && action==EDGE)) {
      og.setColor(focusedgecolor);
      paintedge(og,from_node,to_node);
    }

    // paint highlighted nodes and outlined edges
    if ((button==UP && focus==NODE) || (button==DOWN && action==MOVE)) {
      og.setColor(movenodecolor);
      c=finmod.coord(current);
      paintnode(og,c.x,c.y,displaylabels,finmod.label(current));
    }
    if (button==DOWN && action==DRAW) {
      og.setColor(drawnodecolor);
      c=finmod.coord(current);
      paintnode(og,c.x,c.y,displaylabels,finmod.label(current));
      if (showline==EXISTING || showline==NEW) {
	if (showline==EXISTING) {
	  c=finmod.coord(to_node);
	  to_x=c.x;
	  to_y=c.y;
	paintnode(og,to_x,to_y,displaylabels,finmod.label(to_node));
	} else {
	paintnode(og,to_x,to_y,false,null);
	}

	// paint outlined edge
	og.setColor(drawedgecolor);
	c=finmod.coord(current);
	paintedge(og,c.x,c.y,to_x,to_y);
      }
    }

    // repaint existing image with off-screen image
    if (offImage != null) {
      g.drawImage(offImage, 0, 0, null);
    }
  }

  public void paint(Graphics g) 
  {
    update(g);
  }
   
  
  // -------------------------------------------------------------------------
  // private helper methods
  
  /** paints node at x,y with label if labelflag */

  private void paintnode(Graphics g, int x, int y, boolean labelflag, 
			 String label)
  {
    int rad=finmod.rad;
    g.drawOval(x-rad,y-rad,2*rad,2*rad);
    if (labelflag) {
      g.drawString(label,x+2*rad,y);
    }
  }

  /** paints edge from node i to j in Graphics g, taking into account
   * the radius of the circles representing nodes */

  private void paintedge(Graphics g, int i0, int i1) 
  {
    Point c0=finmod.coord(i0);
    Point c1=finmod.coord(i1);
    paintedge(g,c0.x,c0.y,c1.x,c1.y);
  }

  /** paints edge from point x0/y0 to x1/y1 in Graphics g, taking into
   * account the radius of the circles representing nodes */
  private void paintedge(Graphics g, int x0, int y0, int x1, int y1) 
  {
    int rad=finmod.rad;
    Point cc0=finmod.intercept(x0,y0,x1,y1,rad+1);
    Point cc1=finmod.intercept(x1,y1,x0,y0,rad+1);
    g.drawLine(cc0.x,cc0.y,cc1.x,cc1.y);
  }

  // -------------------------------------------------------------------------
  // Event handling
  
  public boolean mouseDown(Event evt, int x, int y)
  {
    if (button!=UP) {            // this shouldn't normally happen.
      button=DOWN;
      action=NONE;
      repaint();
      return true;
    }
    button=DOWN;
    int node=finmod.closest(x,y,finmod.rad);  // the clicked node
    if (node<0) {                     // clicked on no node
      Point edge=finmod.closest_edge(x,y);  // clicked on edge?
      if (edge.x>=0) {
	action=EDGE;
	from_node=edge.x;
	to_node=edge.y;
	repaint();
	return true;
      }
      if (evt.shiftDown() || evt.clickCount>1) {  // double-click or shift?
	focus=NONE;                               // forget old focus
      }
      switch (focus) {
      case NODE: case EDGE:           // if there is a focus node
	action = NONE;
	repaint();
	return true;
      case NONE: default:                     
	try {                         // else, try to create a node
	  Point c = finmod.place(-1,x,y);
	  current = finmod.add_element(c.x,c.y);  // found room for it  
	  if (evt.shiftDown() || evt.clickCount>1) {  // double-click or shift
	    action = MOVE;
	    newfocus = NODE;
	    moveframe = null;
	  } else {
	    action = DRAW;
	    newfocus = NONE;
	    showline = NONE;
	  }
	  repaint();
	  reset_peers();
	  return true;
	} catch (NoSpaceException e) {  // not enough room to create node
	  action = NONE;
	  repaint();
	  return true;
	}
      }
    } else if (evt.shiftDown() || evt.clickCount>1) {       
      // mouse shift-click or double-click on a node
      action = MOVE;
      current = node;
      newfocus = NODE;
      moveframe = null;
      repaint();
      return true;
    } else if (focus==NODE && node==current) { // mouse down on current node
      action = MOVE;
      newfocus = NONE;
      moveframe = null;
      repaint();
      return true;
    } else {                           // mouse down on non-current node
      action = DRAW;
      current = node;
      newfocus = NODE;
      showline = NONE;
      repaint();
      return true;
    }
  }

  public boolean mouseDrag(Event evt, int x, int y)
  {
    if (button!=DOWN) {                // shouldn't happen
      button=DOWN;
      action=NONE;
      repaint();
      return true;
    }
    switch (action) {
    case NONE: case EDGE: default:
      return true;
    case MOVE:                       // move the current node
      newfocus = NODE;
      if (moveframe==null) {
	moveframe=finmod.determine_moveframe(current);
      }
      try {                          // try to find a place for it near x,y
	Point c=finmod.place_with_moveframe(current,x,y,moveframe);
	finmod.set_coord(current,c.x,c.y);
	repaint();
	return true;
      } catch (NoSpaceException e) { // couldn't find a place, do nothing
	return true;
      }
    case DRAW:
      newfocus = NONE;
      showline = NONE;   // default setting.
      int node=finmod.closest(x,y,2*finmod.rad);   // are we on a node?
      if (node<0) {                      // not on a node
	try {                            // try to create temporary one
	  Point c=finmod.place(-1,x,y);
	  if (finmod.drawableslope(c,finmod.coord(current))) {  // found one
	    showline = NEW;               
	    to_x = c.x;
	    to_y = c.y;
	  }
	} catch (NoSpaceException e) {}  // didn't have room for a node
      } else if (node!=current) {        // or we are on an existing node
	if (finmod.drawableslope(finmod.coord(node),finmod.coord(current))) {
	  showline = EXISTING;
	  to_node=node;
	} 
      }
      repaint();
      return true;
    }
  }

  public boolean mouseUp(Event evt, int x, int y)
  {
    if (button!=DOWN) {             // shouldn't happen
      button=UP;
      focus=NONE;
      repaint();
      return true;
    }
    button = UP;

    boolean must_reset_peers=false;

    // have to create a line?
    if (action==DRAW) {
      if (showline==NEW) {        // create node first?
	to_node=finmod.add_element(to_x,to_y);
	must_reset_peers=true;
      }
      if (showline!=NONE) {         // draw edge?
	if (finmod.coord(current).y>finmod.coord(to_node).y) 
	  finmod.set(current,to_node,true);
	else
	  finmod.set(to_node,current,true);
	must_reset_peers=true;
      } 	
    }
    if (action==MOVE || action==DRAW) {
      focus = newfocus;
    } else if (action==EDGE) {
      focus = EDGE;
    } else {
      focus = NONE;
    }
    if (focus==NONE) {
      Boss.deletebutton.disable();
      Boss.be.unhighlight();
    } else {
      Boss.deletebutton.enable();
      if (focus==NODE) {
	Boss.be.highlight(current);
      }
    }
    repaint();
    if (must_reset_peers)
      reset_peers();
    return true;
  }
  
  public boolean mouseMove(Event evt, int x, int y)
  {
    requestFocus();
    return true;
  }
  
  public boolean mouseEnter(Event evt, int x, int y)
  {
    requestFocus();
    return true;
  }
  
  public boolean gotFocus(Event evt, Object arg) 
  {
    kbfocus=true;
    repaint();
    return true;
  }

  public boolean lostFocus(Event evt, Object arg) 
  {
    kbfocus=false;
    repaint();
    return true;
  }

  public boolean keyDown(Event evt, int nKey)
  {
    switch (nKey) {
    case Event.BACK_SPACE:
    case Event.DELETE:
    case 'd':
      return deleteaction();
    case 'p':
      return printaction();
    case 'l':
      return labelsaction();
    default:
      return false;
    }
  }

  boolean clearaction() {
    finmod.clear();
    button = UP;
    focus = NONE;
    Boss.deletebutton.disable();
    repaint();
    reset_peers();
    return true;
  }

  boolean labelsaction() {
    if (displaylabels) {
      displaylabels=false;
      Boss.labelbutton.setLabel("Show Labels");
    } else {
      displaylabels=true;
      Boss.labelbutton.setLabel("Hide Labels");
    }
    repaint();
    return true;
  }

  boolean printaction() {
    finmod.print();
    return true;
  }    
  
  boolean deleteaction() {
    if (button==UP && focus==NODE) {  // remove current node
      finmod.delete_element(current);
      if (finmod.size()==0) {
	focus=NONE;
	Boss.deletebutton.disable();
	Boss.be.unhighlight();
      } else {
	focus=NODE;
	if (current>=finmod.size())
	  current=finmod.size()-1;
	Boss.be.highlight(current);
      }
      repaint();
      reset_peers();
      return true;
    }
    if (button==UP && focus==EDGE) {  // remove current edge
      if (finmod.rel(from_node,to_node))
	finmod.delete_edge(from_node,to_node);
      else
	finmod.delete_edge(to_node,from_node);
      focus=NONE;
      Boss.deletebutton.disable();
      repaint();
      reset_peers();
      return true;
    }
    return false;
  } 

  private void reset_peers() {
    Boss.be.cursor=false;
    Boss.be.repaint();
    Boss.tmp.recalculate();
  }
}

// -----------------------------------------------------------------

/** displays a scrollable BinopEditor */

class BinopScroller extends Panel {
  Scrollbar vert;
  Scrollbar horz;
  int tx, ty; // the values of the two scrollbars
  BinopEditor be;
  Dimension preferredImageSize = new Dimension(300, 100);
  boolean bugfix;                     // if this is true we have to 
                                      // work around an appletviever bug
  
  BinopScroller(FinMod finmod) {
    be = new BinopEditor(finmod);
    Boss.bs=this;
    bugfix=(Boss.bugfix!=null);

    //Create horizontal scrollbar.
    horz = new Scrollbar(Scrollbar.HORIZONTAL);
    
    //Create vertical scrollbar.
    vert = new Scrollbar(Scrollbar.VERTICAL);
    
    //Add Components
    setLayout(new BorderLayout());
    add("Center", be);
    add("East", vert);
    add("South", horz);
  }

  public boolean handleEvent(Event evt) {
    switch (evt.id) {
    case Event.SCROLL_LINE_UP:
    case Event.SCROLL_LINE_DOWN:
    case Event.SCROLL_PAGE_UP:
    case Event.SCROLL_PAGE_DOWN:
    case Event.SCROLL_ABSOLUTE:
      if (evt.target == vert) {
	ty = ((Integer)evt.arg).intValue();
	be.set_ddy(ty);
	be.repaint();
      }
      if (evt.target == horz) {
	tx = ((Integer)evt.arg).intValue();
	be.set_ddx(tx);
	be.repaint();
      }
    }
    return super.handleEvent(evt);
  }
  
  void adjustscrollbars() {
    resizeHorz();
    resizeVert();
  }

  void resizeHorz() {
    int visibleWidth = be.size().width;   // width of visible area
    int virtualWidth=be.width;         // width of whole table

    // in case we're not yet visible, visibleWidth could be corrupt.
    if (virtualWidth<=0 || visibleWidth<=0) {
      horz.setValues(0,1,0,0);
      return;
    }
    
    //Shift everything to the right if we're displaying empty space
    //on the right side.
    if ((tx + visibleWidth) > virtualWidth) {
      tx = virtualWidth - visibleWidth;
      if (tx < 0) 
	tx = 0;
    }
    
    int visible=(int)(visibleWidth*0.9);
    int max=virtualWidth - visibleWidth + (bugfix ? visible : 0);

    horz.setValues(tx, visible, 0, max);

    //"visible" arg to setValues() has no effect after scrollbar is visible.
    horz.setPageIncrement(visible);
    be.set_ddx(tx);
    return;
  }
  
  void resizeVert() {
    int visibleHeight = be.size().height;
    int virtualHeight = be.height;

    // in case we're not yet visible, visibleHeight could be corrupt.
    if (virtualHeight<=0 || visibleHeight <= 0) {
      vert.setValues(0,1,0,0);
      return;
    }
    
    //Shift everything downward if we're displaying empty space
    //on the bottom.
    if ((ty + visibleHeight) > virtualHeight) {
      ty = virtualHeight - visibleHeight;
      if (ty < 0) 
	ty = 0;
    }
    
    int visible=(int)(visibleHeight*0.9);
    int max=virtualHeight - visibleHeight + (bugfix ? visible : 0);

    vert.setValues(ty, visible, 0, max);

    //"visible" arg to setValues() has no effect after scrollbar is visible.
    vert.setPageIncrement(visible);
    be.set_ddy(ty);
    return;
  }
  
  public void paint(Graphics g) {
    //This method probably was called due to applet being resized.
    adjustscrollbars();
    
    return;
  }
  
  /** adjusts the scrollbars so that the given rectangle (in virtual
   * coordinates) is completely visible, if possible. Does the least
   * amount of movement.  */

  public void shiftintoview(int x0, int y0, int x1, int y1) {
    int visibleWidth = be.size().width;
    int visibleHeight = be.size().height; 
    int virtualWidth = be.width;
    int virtualHeight = be.height;
    int c;

    if (x0<0) 
      x0=0;
    if (x1>virtualWidth) 
      x1=virtualWidth;
    c=Math.min(x0,x1-visibleWidth);
    if (tx<c)
      tx=c;
    c=Math.max(x0,x1-visibleWidth);
    if (tx>c)
      tx=c;
    c=Math.min(y0,y1-visibleHeight);

    if (y0<0) 
      y0=0;
    if (y1>virtualHeight) 
      y1=virtualHeight;
    if (ty<c)
      ty=c;
    c=Math.max(y0,y1-visibleHeight);
    if (ty>c)
      ty=c;
    be.set_ddx(tx);
    be.set_ddy(ty);
  }
}

// -----------------------------------------------------------------

/** edits a binary operation */

class BinopEditor extends Canvas  // this is a scrollable canvas
{
  // canvas's physical properties
  /** coordinates of origin of virtual area within visible area */
  int ddx = 0, ddy = 0;

  /** current dimension of the multiplication table.
   * Note that the size of the visible area is in size() */
  int width, height; 

  FinMod finmod;

  // event state
  boolean kbfocus;
  int highlighted=-1;
  /** after drawing, contains coordinates of rows/columns */
  int[] xpos, ypos;    
  int cursorx, cursory;
  boolean cursor=false;
  boolean editing;
  String editstring;

  // semantic constants: colors
  Color bgcolor = Color.white;
  Color tablecolor = Color.black;
  Color highlightcolor = Color.red;
  Color culpitcolor = new Color(204,204,255);
  Color rulecolor = Color.black;
  Color cursorcolor = Color.black;

  /** padding around mult. table */
  int ux=5, uy=5;  
  /** normal space between rows/columns */
  int nx=3, ny=0;  
  /** extra space after 1st row/column */
  int xx=5, xy=5;  

  /** for double-buffering */
  Image offImage;
  /** offscreen Buffer */
  Graphics og; 
  /** dimension of offscreen Buffer */
  Dimension offDimension; 

  /** initialize */
  BinopEditor(FinMod finmod)
  {
    Boss.be = this;
    this.finmod = finmod;

    // create bogus graphics context so we can get the fontmetrics, to 
    // calculate the size of the graphics context we need. This is annoying.

    /*    offDimension = new Dimension(10,10);
    offImage = createImage(10,10);  // I have no idea why this returns null???.
    if (offImage==null)
      System.err.println("offImage==null");
    else {
      og = offImage.getGraphics();
      calculate_grid(og.getFontMetrics());
    } */

    width=100; height=100;  // make do. is this ever needed???

    requestFocus();
  }

  // Size stuff

  public Dimension minimumSize() {
    return new Dimension(10,10);
  }
  
  public Dimension preferredSize() {
    return new Dimension(width,height);
  }
 
  /** calculates where the virtual image should be located inside the
   * visible image. tx/ty are the positions of the scrollbars, but
   * it the virtual image is smaller than the visible one, we want
   * to center it. ddx/ddy is the coordinate of the upper left corner
   * of the virtual image w.r.t. the visible image */

  public void set_ddx(int tx) { 
    if (size().width<width) 
      ddx=-tx;
    else  
      ddx=(size().width-width)/2;
  }

  public void set_ddy(int ty) { 
    if (size().height<height) 
      ddy=-ty;
    else
      ddy=(size().height-height)/2;
  }

  // -------------------------------------------------------------------------
  // Paint current state

  public void update(Graphics g)  //paint yourself in g
  {
    int n = finmod.size();
    String message;
    FontMetrics fontmetrics;
    int fontheight;
    int ascent;
    int displayWidth=size().width;
    int displayHeight=size().height;
    String entry;
    boolean notmonotone=false, notstronglyext=false;

    // display status message: are we: not monotone, not strongly extensional
    if (!finmod.is_monotone()) {
      message="Not monotone.";
      notmonotone=true;
    } else if (!finmod.is_strongly_extensional()) {
      message="Not strongly extensional.";
      notstronglyext=true;
    } else if (!finmod.is_order_extensional()) {
      message="Okay.";
    } else { 
      message="Okay + order-extensional.";
    }
    Boss.statusline.setText("Status: "+message);

    if (displayWidth<0 || displayHeight<0)
      return; // we probably haven't been validated yet, or we are invisible

    //need to create offscreen buffer?
    if (og==null || displayWidth != offDimension.width 
	|| displayHeight != offDimension.height) {
      offDimension = new Dimension(displayWidth,displayHeight);
      offImage = createImage(displayWidth, displayHeight);
      og = offImage.getGraphics();
    }

    // set up some info about fontmetrics

    fontmetrics = og.getFontMetrics();
    fontheight = fontmetrics.getHeight();
    ascent = fontmetrics.getAscent();
    
    // clear the background
    og.setColor(bgcolor);
    og.fillRect(0,0,displayWidth,displayHeight);

    // to do the following centering correctly, we first need to calculate
    // our current virtual size. ??? This should be moved somewhere so that it 
    // only gets recalculated whenever it changes.

    calculate_grid(og.getFontMetrics());

    og.translate(ddx,ddy);  // below, we need to translate this back!

    // this is just a shortcut
    Point c1=finmod.culpit1;
    Point c2=finmod.culpit2;

    // draw multiplication table entries
    for (int i=-1; i<n; i++)
      for (int j=-1; j<n; j++) {
	entry=display_entry(j,i);
	// determine foreground and background color
	Color fg=tablecolor;
	Color bg=bgcolor;
	if (notmonotone && 
	    ((c1.x==j && c1.y==i) || (c2.x==j && c2.y==i)))
	  bg=culpitcolor;
	if (notstronglyext && (c1.x==j || c2.x==j))
	  bg=culpitcolor;
	if (cursor && cursorx==i && cursory==j) {
	  fg=bg;
	  bg=cursorcolor;
	}
	if ((i==-1 && j==highlighted) || (j==-1 && i==highlighted))
	  fg=highlightcolor;
	
	// paint background
	og.setColor(bg);
	og.fillRect(xpos[i+1],ypos[j+1],xpos[i+2]-xpos[i+1],
		    ypos[j+2]-ypos[j+1]);
	
	// paint entry
	if (entry!=null) {
	  og.setColor(fg);
	  og.drawString(entry,xpos[i+1],ypos[j+1]+ascent);
	}
      }
    
    // draw multl. table rulers
    og.setColor(rulecolor);
    og.drawLine(ux,ypos[1]-(xy+ny)/2,xpos[n+1],ypos[1]-(xy+ny)/2);
    og.drawLine(xpos[1]-(xx+nx)/2,uy,xpos[1]-(xx+nx)/2,ypos[n+1]);
    
    /*    // draw cursor, if any
    if (cursor) {
      og.setColor(Color.white);
      og.setXORMode(Color.black);
      og.fillRect(xpos[cursorx+1],ypos[cursory+1],
		  xpos[cursorx+2]-xpos[cursorx+1],
		  ypos[cursory+2]-ypos[cursory+1]);
      og.setPaintMode();
    }*/

    og.translate(-ddx,-ddy);  // translate back to original origin.

    // paint frame
    og.setColor(Color.gray);
    og.draw3DRect(1,1,displayWidth-2,displayHeight-2,false);
    if (kbfocus) {
      og.setColor(Color.black);
      og.drawRect(0,0,displayWidth-1,displayHeight-1);
    } else {
      og.draw3DRect(0,0,displayWidth-1,displayHeight-1,false);
    }

    // repaint existing image with off-screen image

    if (offImage != null) {
      g.drawImage(offImage, 0, 0, null);
    }
  }

  public void paint(Graphics g) {
    update(g);
  }

  // ---------------------------------------------------------------
  // Helpers for update

  /** determines the width of the longest string in the given string
   * array with respect to the given fontmetrics */

  private int find_widest(String[] column, FontMetrics fontmetrics)
  {
    int len=column.length;
    
    int dx = fontmetrics.stringWidth("0");
    for (int i=0; i<len; i++) {
      if (column[i]!=null) {
	int thislabel=fontmetrics.stringWidth(column[i]);
	if (thislabel>dx)
	  dx=thislabel;
      }
    }
    
    return dx;

  }

  /** calculates the x and y coordinates of the multiplication table
   * also calculates width and height */

  private void calculate_grid(FontMetrics fontmetrics) {
    int n = finmod.size();
    Point p = new Point(ux,uy);
    String[] column = new String[n+1];
    int fontheight = fontmetrics.getHeight();
    int dy = fontheight+ny;
    int dx;

    // create new vector only if size increased
    if (xpos==null || xpos.length < n+2) {
      xpos = new int[n+2];
      ypos = new int[n+2];
    }
    
    // calculate ypos
    for (int j=0; j<n+2; j++) 
      ypos[j]=uy+j*dy+(j>0?xy:0);
    
    // calculate xpos
    xpos[0]=p.x;
    column[0]=null;
    for (int j=0; j<n; j++)
      column[j+1]=finmod.label(j);
    if (cursor && editing && cursorx==-1)
      column[cursory+1]=editstring;
    dx = find_widest(column, fontmetrics);
    p.translate(dx+nx+xx,0);
    for (int i=0; i<n; i++) {
      xpos[i+1]=p.x;
      column[0]=finmod.label(i);
      if (cursor && editing && cursorx==i && cursory==-1)
	column[0]=editstring;
      for (int j=0; j<n; j++) {
	if (cursor && editing && cursorx==i && cursory==j) {
	  column[j+1]=editstring;
	} else {
	  Integer prod = finmod.app(j,i);
	  if (prod==null)
	    column[j+1]=null;
	  else
	    column[j+1]=finmod.label(prod.intValue());
	}
      }
      dx = find_widest(column, fontmetrics);
      p.translate(dx+nx,0);
    }
    xpos[n+1]=p.x;

    width=xpos[n+1]+ux;
    height=ypos[n+1]+uy;
    Boss.bs.adjustscrollbars();
  }

  /** returns the string that should currently be displayed at
   * position (j,i) of the multiplication table, where i and j can be
   * -1, or 0..n-1. Any string currently being edited is taken into
   * account. If the position (j,i) is empty, returns null. */

  String display_entry(int j, int i) {
    if (cursor && editing && cursorx==i && cursory==j) {
      return editstring;
    }
    if (i==-1) {
      if (j==-1) {
	return null;
      } else {
	return finmod.label(j);
      }
    } else {
      if (j==-1) {
	return finmod.label(i);
      }	else {
	  Integer prod = finmod.app(j,i);
	  if (prod==null)
	    return null;
	  else
	    return finmod.label(prod.intValue());
      }
    }
  }

  // ------------------------------------------------------------------------
  // helpers for event handling

  /** updates the cursor state so that cursor is on the point (x,y),
   * if any. If we were currently editing, then first finalize the
   * current edit. Note: x and y are coordinates relative to visible,
   * not virtual, area */

  private void setcursor(int x, int y)
  {
    if (cursor && editing)
      finish_edit();
    x-=ddx;
    y-=ddy;
    if (xpos!=null) {
      // determine x and y-position of click
      int n=finmod.size();
      cursorx=cursory=-2;
      for (int i=0; i<n+1; i++) {
	if (xpos[i]<=x && x<xpos[i+1])
	  cursorx=i-1;
	if (ypos[i]<=y && y<ypos[i+1])
	  cursory=i-1;
      }
      cursor=(cursorx!=-2 && cursory!=-2 && (cursorx!=-1 || cursory!=-1));
      // scroll if necessary
      if (cursor) 
	shifttocursor();
      else
	Boss.bs.shiftintoview(x,y,x,y);
    }
  }
  
  /** causes scollbars to shift so that current cursor is visible */
  private void shifttocursor() {
      if (cursor && xpos!=null && xpos.length>=finmod.size()) {
	Boss.bs.shiftintoview(xpos[cursorx+1]-ux,ypos[cursory+1]-uy,
			      xpos[cursorx+2]+ux,ypos[cursory+2]+uy);
      }
  }    

  /** finalizes the current editing operation. This is invoked, for
   * instance, when the user presses an action key, clicks the mouse,
   * or when we lose focus */

  private boolean finish_edit()  // call only if cursor && editing.
  {
    boolean succ=true;
    int n=finmod.size();

    if (cursorx==-1 && 0<=cursory && cursory<n) {
      succ=finmod.rename(cursory,editstring);
    } else if (cursory==-1 && 0<=cursorx && cursorx<n) {
      succ=finmod.rename(cursorx,editstring);
    } else if (cursorx>=0 && cursorx<n && cursory>=0 && cursory<n) {
      succ=finmod.set_app(cursory,cursorx,editstring);
    }
    editing=false;
    if (succ)
      reset_peers();
    else
      alert();
    return succ;
  }

  /** signalize to the PosetEditor and to the TermManagerPanel that
   * the current Binop has changed, so that they can update their
   * state and repaint themselves */

  private void reset_peers() {
    Boss.pe.repaint();
    Boss.tmp.recalculate();
  }

  /** alerts the user, for instance by beeping */

  void alert()  
  {
    // Toolkit.getDefaultToolkit().beep(); // neither works in Netscape
    System.err.print((char)7);             // but the Toolkit never returns
  }

  // ------------------------------------------------------------------------
  // Event handling

  // event state: if cursor=true, then cursorx, cursory is the current
  // cursor, (-1,a) is the ath header column.
  // editing is true if the entry under the cursor is currently being
  // edited. In that case, editstring contains the edited string.

  public boolean keyDown(Event evt, int nKey)
  {
    switch (nKey) {
    case Event.RIGHT:
      if (cursor && editing)
	finish_edit();
      if (cursorx+1<finmod.size()) {
	cursorx++;
      } else {
	cursorx=0;
      }	
      shifttocursor();
      repaint();
      return true;
    case Event.LEFT:
      if (cursor && editing)
	finish_edit();
      if (cursorx>0) {
	cursorx--;
      } else {
	cursorx=finmod.size()-1;
      }
      shifttocursor();
      repaint();
      return true;
    case Event.DOWN:
      if (cursor && editing)
	finish_edit();
      if (cursory+1<finmod.size()) {
	cursory++;
      } else {
	cursory=0;
      }
      shifttocursor();
      repaint();
      return true;
    case Event.UP:
      if (cursor && editing)
	finish_edit();
      if (cursory>0) {
	cursory--;
      } else {
	cursory=finmod.size()-1;
      }
      shifttocursor();
      repaint();
      return true;
    case Event.ENTER:
      if (cursor && editing)
	finish_edit();
      cursorx=0;
      cursory++;
      if (cursory>=finmod.size()) 
	cursory=0;
      shifttocursor();
      repaint();
      return true;
    case Event.TAB:
      if (cursor && editing)
	finish_edit();
      if (cursorx==-1) {
	cursorx=cursory;
	cursory=-1;
      } else if (cursory==-1) {
	cursory=cursorx;
	cursorx=-1;
      } else {
	cursorx=-1;
      }
      shifttocursor();
      repaint();
      return true;
    case Event.DELETE: 
    case Event.BACK_SPACE:
    case ' ':
      if (cursor) {
	editing=true;
	editstring="";
	repaint();
      }
      return true;
    default:
      char c=(char)nKey;
      if (FinMod.legal_labelchar(c)) {
	if (cursor) {
	  if (editing) {
	    editstring=editstring+(new Character(c).toString());
	    repaint();
	    return true;
	  } else {
	    editing=true;
	    editstring=new Character(c).toString();
	    repaint();
	    return true;
	  }
	}
      }
      return false;
    }
  }      

  public boolean mouseDown(Event evt, int x, int y)
  {
    setcursor(x,y);
    requestFocus();
    repaint();
    return true;
  }

  public boolean mouseDrag(Event evt, int x, int y)
  {
    setcursor(x,y);
    requestFocus();
    repaint();
    return true;
  }

  public boolean mouseMove(Event evt, int x, int y) 
  {
    requestFocus();
    return true;
  }

  public boolean mouseEnter(Event evt, int x, int y) 
  {
    requestFocus();
    return true;
  }

  public boolean gotFocus(Event evt, Object arg) 
  {
    kbfocus=true;
    repaint();
    return true;
  }

  public boolean lostFocus(Event evt, Object arg) 
  {
    kbfocus=false;
    if (cursor && editing)
      finish_edit();
    cursor=false;
    repaint();
    return true;
  }

  //----------------------------------------------------------------------
  // other helpers for specific events

  void unhighlight() 
  {
    highlighted=-1;
    repaint();
  }

  void highlight(int a)
  {
    highlighted=a;
    repaint();
  }

}

// -----------------------------------------------------------------

/** a Panel that contains zero or more TermManagers. Via the
 * moreevent() and lessevent() methods, the number of TermManagers can
 * be changed. */

class TermManagerPanel extends Panel
{
  Vector tmvector;
  Button morebutton, lessbutton;
  FinMod finmod;
  GridBagLayout gridbag;
  GridBagConstraints c;
  Label space;

  TermManagerPanel(FinMod finmod)
  {
    Label text;

    Boss.tmp = this;    // and register with it
    this.finmod = finmod;

    // prepare layout
    gridbag = new GridBagLayout();
    c = new GridBagConstraints();
    setLayout(gridbag);

    // add text
    c.fill      = GridBagConstraints.BOTH;
    c.gridwidth = GridBagConstraints.REMAINDER;
    c.weighty   = 0.0;
    c.weightx   = 1.0;
    text = new Label("Edit lambda terms:");
    gridbag.setConstraints(text,c);
    add(text);

    // create a space
    space = new Label();
    c.weighty   = 1.0;
    gridbag.setConstraints(space,c);
    add(space);

    // create a few TermManagers and add them
    int n=Boss.initterms.length;
    tmvector = new Vector(n+10,10);
    for (int i=0; i<n; i++) {
      addTermManager(Boss.initterms[i]);
    }
  }

  // -----------------------------------------------------------------
  // Private helpers

  /** adds a TermManager to the panel and initialize it to string s. We
   * do not validate here because this is called during initialization. */

  TermManager addTermManager(String s) 
  {
    TermManager tm = new TermManager(finmod, s);
    tmvector.addElement(tm);
    c.fill      = GridBagConstraints.BOTH;
    c.gridwidth = GridBagConstraints.REMAINDER;
    c.weightx   = 1.0;
    c.weighty   = 0.0;
    gridbag.setConstraints(tm,c);
    remove(space);
    add(tm);
    add(space);  // always keep space at the end
    return tm;
  }

  TermManager addTermManager() 
  {
    return addTermManager("");
  }

  /** deletes the last TermManager. Does not validate */

  void deleteTermManager() 
  {
    int n=tmvector.size();
    if (n>0) {
      TermManager tm=(TermManager) tmvector.elementAt(n-1);
      tmvector.removeElementAt(n-1);
      remove(tm);
    }
  }

  // ---------------------------------------------------------------
  // public paint-related methods

  /** draws a box around this panel. */
  public void paint(Graphics g) {
    Dimension d = size();
    g.setColor(getBackground());
    g.draw3DRect(0,0, d.width - 1, d.height - 1,true);
  }

  /** breathing space */
  public Insets insets() {
    return new Insets(5,5,5,5);
  }
  
  // ---------------------------------------------------------------
  // event handline

  /** add a TermManager, request focus and validate */
  public void moreevent() {
    TermManager tm=addTermManager();
    validate();
    tm.requestFocus();
  }
   
  /** delete a TermManager and validate */
  public void lessevent() {
    deleteTermManager();
    validate();
  }    

  /** cause all TermManagers to update their state and redisplay */
  public void recalculate () {
    int n=tmvector.size();
    for (int i=0; i<n; i++) {
      ((TermManager)tmvector.elementAt(i)).recalculate();
    }
  }
}

// -----------------------------------------------------------------

/** displays an editable lambda term and its current denotation */

class TermManager extends Panel
{
  FinMod finmod;
  TextField textfield;
  Label output;
  LambdaTerm term;
  boolean validterm=false;

  TermManager(FinMod finmod, String s)
  {
    this.finmod = finmod;

    // create components
    textfield = new TextField(s,15);
    output = new Label("");

    // add them 
    setLayout(new GridLayout(1,2));
    add(textfield);
    add(output);

    recalculate();
  }

  /** event handling: has the term changed? */

  public boolean action(Event Evt, Object arg) {
    Object target = Evt.target;

    if (target == textfield) {
      recalculate();
      Boss.tmp.validate();
      return true;
    }
    return false;
  }

  public boolean lostFocus(Event evt, Object arg)
  {
    recalculate();
    Boss.tmp.validate();
    return true;
  }

  /** updates display for the current term, reevaluating it in the
   *  current model */

  public void recalculate() {
    try {
      String text=textfield.getText();
      if (text.equals("")) {
	output.setText("");
	validterm=false;
	return;
      }
      term=LambdaParser.parse(textfield.getText());
    } catch (ParseException e) {
      output.setText("? "+e.getMessage()+".");
      textfield.select(e.first, e.last);
      validterm=false;
      return;
    }
    validterm=true;
    output.setText(evaluate()); 
  }

  /** evaluates the current term in the current finmod and returns a
   * string to be displayed */

  private String evaluate() {
    if (!validterm)
      return "Invalid term";
    if (!finmod.is_monotone())
      return ". . . ?";
    if (!finmod.is_strongly_extensional())
      return ". . . ?";
    try {
      term.prepare_evaluation(finmod);
    } catch (UnknownConstantException e) {
      return e.getMessage();
    }
    int a=term.evaluate(finmod);
    if (a==-1)
      return "= Undefined";
    else
      return "= "+finmod.label(a);
  }

}

// -----------------------------------------------------------------

/** a drawable poset with one binary operation. */

class FinMod
{
  // state is private; thus invariants (e.g. transitivity) are guaranteed.
  // we don't guarantee that the binary operation in monotone.
  // note: internal representation of poset is antireflexive!

  private int n;           // number of nodes
  private boolean[][] r;   // binary relation
  private boolean[][] edge;// edge relation: a edge b iff arb and no c. arc,crb
  private boolean[][] comp;// compatibility relation: exists c. a,b<=c
  private Node[] node;     // holds properties of nodes, e.g. coordinates, name
  private Integer[][] op;  // app is a (partial) binary operation; null=undef.

  public Point culpit1, culpit2;

  // semantically constants; maybe later parameters
  // pertaining to geometric appearances:

  int rad=5; // radius of Venn diagram circles
  int edgerad=3; // distance from edge sensitive for clicks
  int maxslope=5; // maximum slope dx/dy of Venn diagram edges
  int minygap=1; // minimum dy of Venn diagram edges

  // we also have a dimension:
  int width, height;

  // -----------------------------------------------------------------
  // constructors
  
  FinMod(Dimension dim) {
    n=0;
    width=dim.width;
    height=dim.height;
  }

  /** parse poset constructors from a ';'-separated constructor string */

  FinMod(Dimension dim, String params) {
    this(dim);
    if (params==null)
      return;
    int i=0;           
    try {
      while (i<params.length()) {
	int j=params.indexOf(';', i);
	if (j<0)
	  j=params.length();
	parseconstructor(params.substring(i,j));
	i=j+1;
      }
    } catch (StringIndexOutOfBoundsException e) {
    }
  }    

  // -----------------------------------------------------------------
  // FinMod Parser

  /** parses finmod constructor from String param of the form
   * "nodelist*nodelist=node" or "nodelist [ < nodelist ] ...". Treats
   * whitespace properly. No errors are generated, but the found
   * constructors are directly applied to the current finmod. Note
   * that _<_ forces all relations that are geometrically possible. */

  private void parseconstructor(String param) {
    if (param.indexOf('=')<0) {    // parse chain of inequalities
      Vector v=new Vector();
      int i=parsenodelist(param,0,v);
      while (i<param.length() && param.charAt(i)=='<') {
	Vector w=new Vector();
	i=parsenodelist(param,i+1,w);
	for (int x=0; x<v.size(); x++) {
	  for (int y=0; y<w.size(); y++) {
	    safe_setrel(((Integer)v.elementAt(x)).intValue(),
		       ((Integer)w.elementAt(y)).intValue());
	  }
	}
	v=w;
      }
    } else {                       // parse multiplication table
      Vector u=new Vector();
      Vector v=new Vector();
      Vector w=new Vector();
      parsenodelist(param,0,v);
      int i=param.indexOf('*'); if (i<0) i=param.length();
      parsenodelist(param,i+1,w);
      int j=param.indexOf('=', i); if (j<0) j=param.length();
      parsenode(param,j+1,u);
      if (u.size()==0)
	return;
      int a=((Integer)u.elementAt(0)).intValue();
      for (int x=0; x<v.size(); x++) {
	for (int y=0; y<w.size(); y++) {
	  set_app(((Integer)v.elementAt(x)).intValue(),
		       ((Integer)w.elementAt(y)).intValue(), a);
	}
      }
    }
  }

  /** in the string param, begins parsing a node of the form "label"
   * or "label(int,int)". Treats whitespace properly; returns the
   * index of the next unused non-whitespace character. Performs an
   * action: if just a label is given, looks for that label in the
   * finmod and adds its index to v. If label and coordinates are
   * given, tries to add such a node to the finmod and adds its index
   * to v. No errors are generated - upon failure, no action takes
   * place. */

  private int parsenode(String param, int i, Vector v) {
    int len=param.length();
    Point coords=null;
    int j,k;
    Double x,y;
    int a;

    i=skipwhitespace(param, i);

    // parse label
    j=i;
    while (j<len && FinMod.legal_labelchar(param.charAt(j))) {
      j++;
    }
    if (j==i)
      return i+1; // illegal character, ignore.
    String label=param.substring(i,j);
    i=skipwhitespace(param, j);

    // parse coordinates, if any
    if (i<len && param.charAt(i)=='(') {
      j=param.indexOf(',',i); if (j<0) j=len;
      k=param.indexOf(')',j); if (k<0) k=len;
      try {
	x=new Double(param.substring(i+1,j));
	y=new Double(param.substring(j+1,k));
	coords=new Point((int)(x.doubleValue()*Boss.posetdim.width),
			 (int)((1-y.doubleValue())*Boss.posetdim.height));
      } catch (NumberFormatException e) {}
      i=skipwhitespace(param, k+1);
    }

    // attempt to add node to finmod only if coords are given and it
    // doesn't already exist, and there is space for it

    a=findlabel(label,-1);
    if (coords!=null && a<0) {     
      try {
	coords=place(-1,coords.x,coords.y); // snap to a free space
	a=add_element(coords,label); 
      } catch (NoSpaceException e) {
      }
    }                       
    if (a>=0)
      v.addElement(new Integer(a));
    return i;
  }
					 
  /** parses a list of nodes from param at index i; returns index of
   * next unused non-whitespace charater. Nodes that do not yet exist are
   * created. The indices of the nodes are appended to v. No errors
   * are generated. A nodelist is either "_" (wildcard stands for all
   * currently existing nodes) or "node [ , node ]...". */

  private int parsenodelist(String param, int i, Vector v) {
    int len=param.length();

    i=skipwhitespace(param,i);

    if (i<len && param.charAt(i)=='_') { // wildcard: add all current nodes
      for (int j=0; j<n; j++)
	v.addElement(new Integer(j));
      i=skipwhitespace(param,i+1);
      return i;
    }
    i = parsenode(param,i,v);
    while (i<len && param.charAt(i)==',') 
      i = parsenode(param,i+1,v);
    return i;
  }

  /** returns next index in string s, beginning at i, that is not a
   * whitespace, or else s.length() */
  private int skipwhitespace(String s, int i) {
    int len=s.length();
    while (i<len && Character.isSpace(s.charAt(i))) {
      i++;
    }
    return i;
  }

  public static boolean legal_labelchar(char c) {
    if ("!@#$%^&+-|/\\`~'\":.?[]".indexOf(c)>=0)
      return true;
    return Character.isLetterOrDigit(c);
  }

  // -----------------------------------------------------------------
  // accessors
  
  int size() {
    return n;
  }

  boolean rel(int a, int b) {
    return r[a][b];
  }

  boolean releq(int a, int b) {
    return a==b || r[a][b];
  }

  boolean releq(Integer a, Integer b) {
    if (a==null)
      return true;  // null is treated implicitly as bottom
    else if (b==null)
      return false;
    else
      return a.equals(b) || r[a.intValue()][b.intValue()];
  }

  boolean releqlift(int a, int b) {   // -1 is the index of bottom
    if (a==-1)
      return true;
    else if (b==-1) 
      return false;
    else 
      return a==b || r[a][b];
  }

  /** true if there is a shortest edge from a to b */
  boolean minrel(int a, int b) {
    return edge[a][b];
  }

  boolean compatible(int a, int b) {
    return comp[a][b];
  }

  boolean compatible(Integer a, Integer b) {
    if (a==null || b==null)
      return true;  // null is treated implicitly as bottom
    else
      return comp[a.intValue()][b.intValue()];
  }

  Point coord(int a) {
    return node[a].c;
  }

  String label(int a) {
    return node[a].label;
  }

  /** looks up index of label s, ignoring index 'ignore'. returns -1
   * if not found */

  int findlabel(String s, int ignore) 
  {
    for (int i=0; i<n; i++) {
      if (i!=ignore && label(i).equals(s)) {
	return i;
      }
    }
    return -1;
  }

  private Node getnode(int a) {   // eliminate this?
    return node[a];
  }

  Integer app(int a, int b) {
    return op[a][b];
  }

  int applift(int a, int b) {
    if (op[a][b]==null)
      return -1;
    return op[a][b].intValue();
  }

  /** returns true if binary operation is monotone. Otherwise, culpit1
   * and culpit2 are set to the first point where monotonicity fails */

  boolean is_monotone() { 
    for (int a=0; a<n; a++)   // check monotonicity of a'th row + column
      for (int b=0; b<n; b++) 
	for (int c=0; c<n; c++) 
	  if (minrel(b,c)) {
	    if (!releq(app(a,b),app(a,c))) {
	      culpit1=new Point(a,b);
	      culpit2=new Point(a,c);
	      return false;
	    }
	    if (!releq(app(b,a),app(c,a))) {
	      culpit1=new Point(b,a);
	      culpit2=new Point(c,a);
	      return false;
	    }
	  }
    return true;
  }

  boolean is_strongly_extensional() {
    for (int a=0; a<n; a++)   
      for (int b=a+1; b<n; b++)
	if (!compatible(a,b)) {
	  int c=0;
	  while (c<n && compatible(app(a,c),app(b,c)))
	    c++;
	  if (c==n) {
	    culpit1=new Point(a,-1);
	    culpit2=new Point(b,-1);
	    return false;
	  }
	}
    return true;
  }

  boolean is_order_extensional() {
    for (int a=0; a<n; a++)
      for (int b=0; b<n; b++)
	if (!releq(a,b)) {
	  int c=0;
	  while (c<n && releq(app(a,c),app(b,c)))
	    c++;
	  if (c==n) {
	    return false;
	  }
	}
    return true;
  }

  int largestbelow(int array[]) {
    int best=-1;
    for (int i=0; i<n; i++) {
      if (releqlift(best,i)) {
	int j=0;  // is the i'th row below array?
	while (j<n && releqlift(applift(i,j),array[j]))
	  j++;
	if (j==n) {  // yes
	  best=i;
	}
      }
    }
    return best;
  }
	  
  // -----------------------------------------------------------------
  // exporting and printing

  public void print() {
    System.out.print(toString()+"\n");
  }

  public String toString() {
    StringBuffer s=new StringBuffer(100);
    boolean ticklist[] = new boolean[n];

    // The order of the following three parts can be changed; the
    // ticklist will ensure that the first time a node gets mentioned,
    // its coordinates are given.

    // Give coordinates for each node, so that they are listed in
    // correct order.
    for (int a=0; a<n; a++) {
      if (!ticklist[a])
	s.append(issuelabel(a,ticklist)+"; ");
    }

    // Create a representation of the poset
    for (int a=0; a<n; a++) {
      boolean first=true;
      for (int b=0; b<n; b++) {
	if (minrel(a,b)) {
	  if (first) {
	    first=false;
	    s.append(issuelabel(a,ticklist)+"<"+issuelabel(b,ticklist));
	  } else {
	    s.append(","+issuelabel(b,ticklist));
	  }
	}
      }
      if (!first) {
	s.append("; ");
      }
    }

    // Create a representation of the binary operation
    boolean done[][] = new boolean[n][n];
    boolean row[]=new boolean[n];
    boolean column[]=new boolean[n];
    for (int a=0; a<n; a++)
      for (int b=0; b<n; b++)
	if (app(a,b)==null)
	  done[a][b]=true;

    for (int a=0; a<n; a++) 
      for (int b=0; b<n; b++) 
	if (!done[a][b]) {
	  reset(row);
	  reset(column);
	  row[a]=true;
	  column[b]=true;
	  int ab=applift(a,b);
	  find_max_square(row,column,done,ab);
	  s.append(issuelist(row,ticklist)+"*");
	  s.append(issuelist(column,ticklist)+"=");
	  s.append(issuelabel(ab,ticklist)+"; ");
	  for (int i=0; i<n; i++)
	    for (int j=0; j<n; j++)
	      if (row[i] && column[j] && applift(i,j)==ab)
		done[i][j]=true;
	}
    
    return s.toString();
  }

  /** we are given an nxn matrix with three kinds of entries:
   * desirable, redundant, and off-limit. We are also given a square
   * row x column. We are interested in squares that 1) contain the
   * given one, 2) contain no off-limit entries, 3) contain as many
   * desirable entries as possible, and 4) contain no rows or columns
   * that are completely redundant. This implementation is not
   * optimal, but correct. Off-limit are "done" entries whose value is
   * different from a. Desirable are "not-done" entries whose value is
   * a.  All other entries are redundant. Admissible means desirable
   * or redundant */

  private void find_max_square(boolean[] row, boolean[] column, 
			       boolean[][] done, int a) {
    boolean more;
    do {
      more=false;
      
      // Add any columns that are admissible but not redundant for the
      // current row
      for (int j=0; j<n; j++) 
	if (!column[j]) {
	  boolean admissible=true;
	  boolean redundant=true;
	  for (int i=0; i<n; i++) 
	    if (row[i]) {
	      if (done[i][j] && applift(i,j)!=a)  // off-limit?
		admissible=false;
	      if (!done[i][j] && applift(i,j)==a) // desirable?
		redundant=false;
	    }
	  if (admissible && !redundant) {
	    column[j]=true;
	    more=true;
	  }
	}

      // Add any rows that are admissible but not redundant for the
      // current column
      for (int i=0; i<n; i++) 
	if (!row[i]) {
	  boolean admissible=true;
	  boolean redundant=true;
	  for (int j=0; j<n; j++) 
	    if (column[j]) {
	      if (done[i][j] && applift(i,j)!=a)  // off-limit?
		admissible=false;
	      if (!done[i][j] && applift(i,j)==a) // desirable?
		redundant=false;
	    }
	  if (admissible && !redundant) {
	    row[i]=true;
	    more=true;
	  }
	}
    } while (more);
  }

  private String issuelist(boolean[] list, boolean[] ticklist) {
    StringBuffer s=new StringBuffer();
    boolean first=true;

    for (int i=0; i<n; i++) 
      if (list[i]) {
	if (first) 
	  first=false;
	else 
	  s.append(",");
	s.append(issuelabel(i,ticklist));
      }
    return s.toString();
  }

  private String issuelabel(int a, boolean[] ticklist) {
    if (ticklist[a])
      return label(a);
    ticklist[a]=true;
    Point c=coord(a);
    String x=format((double)c.x/width);
    String y=format(1-((double)c.y/height));
    return label(a)+"("+x+","+y+")";
  }

  private String format(double d) {
    String s=Double.toString(d);
    int dot=s.indexOf('.');
    if (dot>=0 && dot+4<=s.length())
      s=s.substring(0,dot+4);
    return s;
  }

  private void reset(boolean[] b) {
    for (int i=0; i<b.length; i++) 
      b[i]=false;
  }

  // -----------------------------------------------------------------
  // changers
  
  void clear() {
    n=0;
  }

  void set(int a, int b, boolean value) 
  {
    r[a][b] = value;
    transitivize();
  }

  void safe_setrel(int a, int b) 
  {
    if (a==b || !drawableslope(coord(a),coord(b)) || coord(a).y<coord(b).y)
      return;                 // geometry doesn't allow a<=b
    r[a][b] = true;
    transitivize();
  }

  void delete_edge(int a, int b) 
  {
    r=edge;
    edge=new boolean[n][n];
    r[a][b]=false;
    transitivize();
  }

  int add_element() 
  {
    boolean[][] r1 = new boolean[n+1][n+1];
    boolean[][] edge1=new boolean[n+1][n+1];
    boolean[][] comp1=new boolean[n+1][n+1];
    Node[] node1=new Node[n+1];
    Integer[][] op1=new Integer[n+1][n+1];
    for (int i=0; i<n; i++) {
      node1[i]=node[i];
      for (int j=0; j<n; j++) {
	r1[i][j] = r[i][j];
	edge1[i][j] = edge[i][j];
	comp1[i][j] = comp[i][j];
	op1[i][j] = op[i][j];
      }
    }
    r=r1;
    edge=edge1;
    comp=comp1;
    node=node1;
    op=op1;
    node[n]=new Node(new Point(0,0), freshlabel());
    comp[n][n]=true;
    return n++;  // return index of new element
    // note: we are still transitive, and edge and comp didn't change.
  }

  int add_element(Point c, String label) { 
    int a = add_element();
    node[a] = new Node(c,label);
    return a;
  }

  int add_element(Point c) {
    int a = add_element();
    getnode(a).c=c;
    return a;
  }

  int add_element(int x, int y) {
    return add_element(new Point(x,y));
  }

  void delete_element(int a) 
  {
    if (a<0 || a>=n)
      throw new ArrayIndexOutOfBoundsException("delete_element");
    for (int i=0; i<n-1; i++)
      for (int j=0; j<n-1; j++) {
	r[i][j] = r[i<a ? i : i+1][j<a ? j : j+1];
	op[i][j] = op[i<a ? i : i+1][j<a ? j : j+1];
	if (op[i][j]!=null) {
	  int ij=op[i][j].intValue();
	  if (ij==a) 
	    op[i][j] = null;
	  else if (ij>a)
	    op[i][j]=new Integer(ij-1);
	}
      }
    for (int i=a; i<n-1; i++)
      node[i]=node[i+1];
    n--;
    // note: we are still transitive!
    compute_edges();
    compute_compatibility();
  }

  void set_coord(int a, Point c) 
  {
    getnode(a).c=c;
  }

  void set_coord(int a, int x, int y) 
  {
    set_coord(a, new Point(x,y));
  }

  boolean rename(int a, String s)
  {
    if (s.equals("") || findlabel(s,a)>=0)
      return false;
    getnode(a).label=s;
    return true;
  }

  boolean set_app(int a, int b, String s)
  {
    if (s.equals("")) {
      op[a][b]=null;
      return true;
    }
    int c=findlabel(s,-1);
    if (c<0)
      return false;
    set_app(a,b,c);
    return true;
  }

  void set_app(int a, int b, int c)
  {
    op[a][b]=new Integer(c);
  }

  // -----------------------------------------------------------------
  // private helpers for state updates

  private String freshlabel()
  {
    String s;
    for (int i=0; i<n+1; i++) {
      s=genericstring(i);
      if (findlabel(s,-1)<0)
	return s;
    }
    return "?";  // this never happens, since there are only n labels in use
  }

  private String genericstring(int i) {
    char[] c=new char[8];
    if (i<26) {
      c[0]=(char)(i+'a');
      return new String(c,0,1);
    }
    c[0]=(char)(i%26+'a');
    c[1]=(char)(i/26-1+'a');
    return new String(c,0,2);
  }

  private void transitivize() 
  // note: internal representation of poset is antireflexive!
  {
    boolean cont;
    do 
      {
	cont = false;
	for (int a=0; a<n; a++)
	  for (int b=0; b<n; b++) 
	    if (r[a][b]) 
	      for (int c=0; c<n; c++) 
		if (r[b][c] && !r[a][c])  
		  r[a][c] = cont = true;
      } while (cont==true);
    compute_edges();
    compute_compatibility();
  }

  private void compute_edges()    // ab is edge iff aRb and for no c, aRcRb.
  {
    for (int a=0; a<n; a++) 
      for (int b=0; b<n; b++) 
	if (!r[a][b]) {
	  edge[a][b]=false;
	} else {
	  edge[a][b]=true;
	  for (int c=0; c<n; c++) 
	    if (r[a][c] && r[c][b]) {
	      edge[a][b]=false;
	      break;
	    }
	}
  }

  private void compute_compatibility()  // a~b iff exists c. a,b<=c.
  {
    for (int a=0; a<n; a++) 
      for (int b=0; b<n; b++) {
	int c=0;
	while (c<n && !(releq(a,c) && releq(b,c)))
	  c++;
	comp[a][b]=(c<n);
      }
  }	

  // -----------------------------------------------------------------
  // Helpers for geometry.

  private int distancesq(int a, int x, int y) 
  {
    int dx=getnode(a).c.x-x;
    int dy=getnode(a).c.y-y;
    return dx*dx+dy*dy;
  }

  private int closest_but(int a, int x, int y, int rad)
  {
    int bestdist=rad*rad+1;
    int dist;
    int bestindex=-1;
    for (int i=0; i<n; i++) 
      if (i!=a) {
	dist=distancesq(i,x,y);
	if (dist<bestdist) {
	  bestdist=dist;
	  bestindex=i;
	}
      }
    return bestindex;
  }

  public int closest(int x, int y, int rad)
  {
    return closest_but(-1,x,y,rad);
  }

  public Point closest_edge(int x, int y)
  {
    for (int i=0; i<n; i++)
      for (int j=0; j<n; j++) 
	if (near_edge(x,y,i,j)) 
	  if (minrel(i,j))
	    return new Point(i,j);
    return new Point(-1,-1);
  }

  private boolean near_edge(int x, int y, int i, int j) 
  {
    Point ci=coord(i);
    Point cj=coord(j);
    int cx=ci.x-cj.x;
    int cy=ci.y-cj.y;
    int dx=x-cj.x;
    int dy=y-cj.y;
    int innerprod=cx*dx+cy*dy;
    int csq=cx*cx+cy*cy;
    if (innerprod<0 || innerprod>csq)
      return false;
    int lhs=(cx*dy-cy*dx);
    lhs=lhs*lhs;
    int rhs=edgerad*edgerad*csq;
    return lhs<=rhs;
  }

  // -----------------------------------------------------------------
  // more methods for geometry, calculating with slopes in Venn diagrams

  /** calculates the sup of two points with respect to the order given
   * by maxslope */

  private Point strangemax(Point a, Point b)
  {
    int A0=Math.max(a.x+maxslope*a.y,b.x+maxslope*b.y);
    int B0=Math.max(-a.x+maxslope*a.y,-b.x+maxslope*b.y);
    return new Point((A0-B0)/2,(A0+B0)/(2*maxslope));
  }

  /** calculates the inf of two points with respect to the order given
   * by maxslope */

  private Point strangemin(Point a, Point b)
  {
    int A0=Math.min(a.x+maxslope*a.y,b.x+maxslope*b.y);
    int B0=Math.min(-a.x+maxslope*a.y,-b.x+maxslope*b.y);
    return new Point((A0-B0)/2,(A0+B0)/(2*maxslope));
  }

  private Point strangeright(Point a, Point b)
  {
    int A0=Math.max(a.x+maxslope*a.y,b.x+maxslope*b.y);
    int B0=Math.min(-a.x+maxslope*a.y,-b.x+maxslope*b.y);
    return new Point((A0-B0)/2,(A0+B0)/(2*maxslope));
  }

  private Point strangeleft(Point a, Point b)
  {
    int A0=Math.min(a.x+maxslope*a.y,b.x+maxslope*b.y);
    int B0=Math.max(-a.x+maxslope*a.y,-b.x+maxslope*b.y);
    return new Point((A0-B0)/2,(A0+B0)/(2*maxslope));
  }

  /** checks if the slope between two nodes is steep enough to draw an
   * edge between them. */

  boolean drawableslope(Point a, Point b) 
  {
    int dx=a.x-b.x;
    int dy=a.y-b.y;
    return (Math.abs(dy)>=minygap && Math.abs(dx)<=maxslope*Math.abs(dy));
  }

  /** calculates, for a given node, where it can legally be moved in
   * relation to the other nodes. The result is a MoveFrame. */

  MoveFrame determine_moveframe(int node) {
    MoveFrame mf=new MoveFrame();

    for (int i=0; i<n; i++) {
      if (rel(i,node)) {
	Point c=coord(i);
	if (mf.top==null)                
	  mf.top=c;
	else 
	  mf.top=strangemin(c,mf.top);
      }
      if (rel(node,i)) {
	Point c=coord(i);
	if (mf.bot==null) 
	  mf.bot=c;
	else
	  mf.bot=strangemax(c,mf.bot);
      }
      if (mf.top!=null && mf.bot!=null) {
	mf.left=strangeleft(mf.bot,mf.top);
	mf.right=strangeright(mf.top,mf.bot);
      }
    }
    return mf;
  }

  /** finds an empty space in the current poset near x,y; ignoring the
   * element ignore. Possible to set ignore=-1.  raises
   * NoSpaceException if no good spot found.*/

  Point place(int ignore, int x, int y)
       throws NoSpaceException
  {
    return place_with_moveframe(ignore, x, y, null);
  }

  /** finds an empty space in the current poset near x,y; ignoring the
   * element ignore, and taking the MoveFrame mf into account.
   * Possible to set ignore=-1.  raises NoSpaceException if no good
   * spot found.*/

  Point place_with_moveframe(int ignore, int x, int y, MoveFrame mf) 
       throws NoSpaceException 
  {
    int a;
    Point c;
    double dist;
    boolean more;
    int count=0;
    int tmp;
    do {
      more=false;

      if (x<rad) x=rad;    // constrict to display size
      if (x>=width-rad-1) x=width-rad-1;
      if (y<rad) y=rad;
      if (y>=height-rad-1) y=height-rad-1;

      if (mf!=null) {     // constrict to current moveframe
	if (mf.top!=null && mf.bot!=null && x<mf.left.x) {
	  x=mf.left.x;
	  y=mf.left.y;
	} else if (mf.top!=null && mf.bot!=null && x>mf.right.x) {
	  x=mf.right.x;
	  y=mf.right.y;
	} else if (mf.top!=null && 
		   maxslope*(mf.top.y-y)<(tmp=Math.abs(mf.top.x-x))) {
	  y=mf.top.y-tmp/maxslope;
	} else if (mf.bot!=null && 
		   maxslope*(y-mf.bot.y)<(tmp=Math.abs(mf.bot.x-x))) {
	  y=mf.bot.y+tmp/maxslope;
	}
      }

      a=closest_but(ignore,x,y,2*rad);  // find a spot that's not taken
      if (a>=0) {
	c=coord(a);
	c=intercept(c.x,c.y,x,y,2*rad+2);
	x=c.x;
	y=c.y;
	more=true;
      }
    } while (more && count++<10);
    if (more)
      throw new NoSpaceException();
    return new Point(x,y);
  }

  /** finds the point of distance epsilon from x0y0 along the line
   * x0y0-x1y1. */

  public Point intercept(int x0, int y0, int x1, int y1, int epsilon)
  {
    double length=Math.sqrt((double)((x1-x0)*(x1-x0)+(y1-y0)*(y1-y0)));
    return new Point(x0+(int)(0.5+((x1-x0)*epsilon)/length),
			  y0+(int)(0.5+((y1-y0)*epsilon)/length));
  }
}

// -----------------------------------------------------------------

/** contains a set of constraints to determine an area within the
 * coordinate space of a poset. The shape of this area is roughly like
 * <>, with the slope of the sides given by finmod.maxslope. If top is
 * non-null, then it is the top point of the constrained area, similar
 * for bot, left, and right.  Note: top and bottom are with respect to
 * COORDINATES of points, which are displayed upside down on the
 * screen. That is, top.y>=bot.y */

class MoveFrame 
{
  Point top, bot, left, right;
  MoveFrame() {}
}

// -----------------------------------------------------------------

/** holds properties of a node of a finite model, such as coordinates,
 * label.  */

class Node
{
  Point c;
  String label;
  
  Node(Point c, String label) {
    this.c=c;
    this.label=label;
  }

  public String toString() {
    return "("+c.x+","+c.y+") "+label;
  }
}

// -----------------------------------------------------------------
// Lambda terms

/** an abstract representation up untyped lambda terms - this is not
 * designed for substitution; therefore rather static. */

class LambdaTerm 
{
  final static int VAR=1, APP=2, ABS=3, CONST=4;      // what are we?          
  int top;                            
  LambdaVar x;                        // if top=ABS, we are (lam x.M)
  int idx;       // our deBruijn index: if top=VAR, we are free[idx]
  LambdaTerm M,N;                     // if top=APP, we are (M N)
  String cst;                         // if top=CONST, we are a constant
  LambdaVar[] free; // a list of variables that are bound in our environment.

  // these are not permanent part of the term, but initialized at the
  // begin of evaluation w.r.t. a given finmod. (for efficiency).

  int cstvalue; // if top=CONST, index of than cst in finmod.
  int n;        // size of the finmod
  int valarray[]; // if top=ABS, use this array to store fn values

  LambdaTerm() {}

  void setfree(Vector v) {
    int n=v.size();
    free = new LambdaVar[n];
    for (int i=0; i<n; i++)
      free[i]=(LambdaVar)v.elementAt(i);
  }  

  void setequal(LambdaTerm t) {
    top = t.top;
    x = t.x;
    idx = t.idx;
    M = t.M;
    N = t.N;
    cst = t.cst;
    free = t.free;
  }

  /** set the non-permanent variables */

  void prepare_evaluation(FinMod finmod) 
    throws UnknownConstantException
  {
    n=finmod.size();
    switch (top) {
    case CONST: 
      cstvalue=finmod.findlabel(cst,-1);
      if (cstvalue==-1)
	throw new UnknownConstantException("? Unknown: "+cst);
    case VAR:
      return;
    case APP:
      M.prepare_evaluation(finmod);
      N.prepare_evaluation(finmod);
      return;
    case ABS:
      M.prepare_evaluation(finmod);
      valarray = new int[n];
      return;
    }
  }

  /** evaluate myself in finmod. -1 indicates the value is
   * undefined, i.e. a presumed bottom element. The values of the free
   * variables are assumed to be stored in the .value-fields of those
   * variables. Note, evaluate will run concurrently. It is the
   * thread's creator's responsibility to stop it before finmod is
   * changed. */

  public int evaluate(FinMod finmod) {
    switch (top) {
    case VAR:
      return free[idx].value;
    case CONST:
      return cstvalue;
    case APP: {
      int a,b;
      Integer result;
      a=M.evaluate(finmod);
      if (a==-1) 
	return -1;
      b=N.evaluate(finmod);
      if (b==-1)
	return -1;
      result=finmod.app(a,b);
      if (result==null)
	return -1;
      return result.intValue();
    }
    case ABS:
      for (int i=0; i<n; i++) {
	x.value=i;
	valarray[i]=M.evaluate(finmod);
      }
      return finmod.largestbelow(valarray);
    }
    return -1;
  }
  
  public String toString() {
    return toString(0);
  }

  public String toString(int context) {
    // context = 0: top level, and (12) for application, \x3 for abstraction.
    switch (top) {
    case VAR:
      return (context==3 ? "." : "")+free[idx].name;
    case CONST: 
      String prefix=(context==3 ? "." : "");
      if (cst.length()==1) {
	char ch=cst.charAt(0);
	for (int i=0; i<free.length; i++)
	  if (free[i].name==ch)
	    return prefix+"<"+cst+">";
	return prefix+cst;
      }
      return prefix+"<"+cst+">";
    case APP:
      switch (context) {
      case 0: case 1: default:
	return M.toString(1)+N.toString(2);
      case 2: 
	return "("+M.toString(1)+N.toString(2)+")";
      case 3: 
	return "."+M.toString(1)+N.toString(2);
      }
    case ABS:
      switch (context) {
      case 0: default:
	return "\\"+x.name+M.toString(3);
      case 1: case 2:
	return "(\\"+x.name+M.toString(3)+")";
      case 3:
	return x.name+M.toString(3);
      }
    default:
      return "(Bad Term)";
    }
  }
}

// -----------------------------------------------------------------

class LambdaVar 
{
  char name;
  int value;

  LambdaVar(char name) {
    this.name = name;
  }
}

// -----------------------------------------------------------------

/** provides one public method for parsing a lambda term from a
 * string. This class is effectively static - an instance is never
 * created. */

class LambdaParser
{
  public static LambdaTerm parse(String s) 
       throws ParseException
  {
    if (s.length()==0)
      throw new ParseException("Empty Term",0,0);
    LambdaTerm result = new LambdaTerm();
    int end=parse(s, 0, result, new Vector());
    if (end!=s.length())
      throw new ParseException("Bad character",end,end+1);
    return result;
  }

  /** find the longest substring of s starting at i which is a
   * syntactically correct lambda term. Return the parsed term in
   * global variable result. Return the index of the next character
   * after the term. bound is a vector of bound variables in the current
   * environment. */

  private static int parse(String s, int i, LambdaTerm result, Vector bound) 
       throws ParseException
  {
    Vector acc=new Vector();  // to accumulate subterms
    LambdaTerm t, t2;      // temporary.

    int j=i;

    try {
      do {
	i=j;
	switch (s.charAt(i)) {
	case '(': 
	  t = new LambdaTerm();
	  j=parse(s, i+1, t, bound);
	  if (s.charAt(j)!=')')
	    throw new ParseException("Bad character",j,j+1);
	  acc.addElement(t);
	  j=j+1;
	  break;
	case '\\': {
	  char ch=s.charAt(i+1);
	  int oldboundsize = bound.size();
	  if (!legalvariable(ch)) 
	    throw new ParseException("Need variable",i+1,i+2);
	  t=new LambdaTerm();
	  acc.addElement(t);
	  int k=i+1;
	  while (legalvariable(ch)) {
	    t.top=LambdaTerm.ABS;
	    t.x = new LambdaVar(ch);
	    t.M = new LambdaTerm();
	    t.setfree(bound);
	    bound.addElement(t.x);
	    t=t.M;
	    k++;
	    ch=s.charAt(k);
	  }
	  if (ch=='.') 
	    k++;
	  j=parse(s, k, t, bound);
	  for (int l=bound.size()-1; l>=oldboundsize; l--)
	    bound.removeElementAt(l);
	  break;
	}
	case '{':
	  j=s.indexOf("}",i+1);
	  if (j<=i)
	    throw new ParseException("missing }",i+1,i+2);
	  t=new LambdaTerm();
	  acc.addElement(t);
	  t.top=LambdaTerm.CONST;
	  t.cst=s.substring(i+1,j);
	  t.setfree(bound);
	  j++;
	  break;
	default:
	  char ch;
	  if (legalvariable(ch=s.charAt(i))) {
	    t=new LambdaTerm();
	    int idx=lastindex(bound, ch);
	    if (idx<0) {    // this is a constant
	      t.top=LambdaTerm.CONST;
	      t.cst=""+ch;
	    } else {        // it's a bound variable  
	      t.top=LambdaTerm.VAR;
	      t.idx = idx;
	    }
	    t.setfree(bound);
	    acc.addElement(t);
	    j=i+1;
	    break;
	  }
	}
      } while (j>i && j<s.length());
    } catch (StringIndexOutOfBoundsException e) {
      throw new ParseException("Term ends early",s.length(),s.length());
    } 

    // collect terms
    int n=acc.size();
    if (n<1)
      throw new ParseException("Bad character",i,i+1);
    t=(LambdaTerm) acc.elementAt(0);
    for (int k=1; k<n; k++) {
      t2=new LambdaTerm();
      t2.top=LambdaTerm.APP;
      t2.M=t;
      t2.N=(LambdaTerm) acc.elementAt(k);
      t2.setfree(bound);
      t=t2;
    }
    
    // clone the resulting term into "result"
    result.setequal(t);
    
    return j;
  }

  private static int lastindex(Vector lvv, char ch)
  {
    for (int j=lvv.size()-1; j>=0; j--) 
      if (((LambdaVar)lvv.elementAt(j)).name==ch)
	return j;
    return -1;
  }

  /** true if c is an allowed character for a variable name */
  private static boolean legalvariable(char c)
  {
    return Character.isLetterOrDigit(c);
  }
}

// ------------------------------------------------------------------
// Exceptions

/** an Exception holding the first and last character of where a parse
 * error occurred */

class ParseException extends Exception {
  int first;
  int last;
  ParseException(String s, int first, int last) {
    super(s);
    this.first = first;
    this.last = last;
  }
}

class UnknownConstantException extends Exception {
  UnknownConstantException(String s) {
    super(s);
  }
}

class NoSpaceException extends Exception {
}

// -----------------------------------------------------------------
// Global variables

/** holds the global variables. Holds references to the relevant
 * components so that they can conveniently access each other's
 * methods. It also holds the parsed applet parameters from the applet
 * tag. */

class Boss {
  // components
  static PosetEditor pe;
  static BinopScroller bs;
  static BinopEditor be;
  static TermManagerPanel tmp;
  static Button deletebutton, labelbutton, morebutton, lessbutton;
  static Label statusline;
  static FiniteLambdaModel flm;

  // parsed applet parameters
  static String bugfix;
  static Dimension posetdim;
  static String[] initterms;
  static String finmodinit;
}