/* 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
* http://www.math.lsa.umich.edu/~selinger/finmod/.
*
* @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.
*
* Definition of event state:
*
*
* 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)
*
* moveframe is null if not set.
*
* kbfocus = true/false: do we have keyboard focus?
*
*
* 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.
*
* 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=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 (txc)
tx=c;
c=Math.min(y0,y1-visibleHeight);
if (y0<0)
y0=0;
if (y1>virtualHeight)
y1=virtualHeight;
if (tyc)
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().widthdx)
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; j0?xy:0);
// calculate xpos
xpos[0]=p.x;
column[0]=null;
for (int j=0; j=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=0 && cursorx=0 && cursory0) {
cursorx--;
} else {
cursorx=finmod.size()-1;
}
shifttocursor();
repaint();
return true;
case Event.DOWN:
if (cursor && editing)
finish_edit();
if (cursory+10) {
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; i0) {
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=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=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=0 && dot+4<=s.length())
s=s.substring(0,dot+4);
return s;
}
private void reset(boolean[] b) {
for (int i=0; i=n)
throw new ArrayIndexOutOfBoundsException("delete_element");
for (int i=0; ia)
op[i][j]=new Integer(ij-1);
}
}
for (int i=a; i=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; icsq)
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=width-rad-1) x=width-rad-1;
if (y=height-rad-1) y=height-rad-1;
if (mf!=null) { // constrict to current moveframe
if (mf.top!=null && mf.bot!=null && xmf.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";
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=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;
}