view lib/js/urweb.js @ 1218:48d2ca496d2c

Path conditions, used to track implicit flows
author Adam Chlipala <adamc@hcoop.net>
date Sat, 10 Apr 2010 13:02:15 -0400
parents 26fed2c4f5be
children 83b1853d1e58
line wrap: on
line source
// Detect browser quirks that we should be aware of.

function needsDynPrefix() {
  var span = document.createElement("span");
  span.innerHTML = "<script>alert('test');</script>";
  var scripts = span.getElementsByTagName("script");
  return scripts.length == 0;
}

var dynPrefix = needsDynPrefix() ? "<span style=\"display:none\">A</span>" : "";

// Function versions of operators

function not(x) { return !x; }
function neg(x) { return -x; }

function eq(x, y) { return x == y; }
function plus(x, y) { return x + y; }
function minus(x, y) { return x - y; }
function times(x, y) { return x * y; }
function div(x, y) { return x / y; }
function mod(x, y) { return x % y; }
function lt(x, y) { return x < y; }
function le(x, y) { return x <= y; }

// Characters

function isLower(c) { return c >= 'a' && c <= 'z'; }
function isUpper(c) { return c >= 'A' && c <= 'Z'; }
function isAlpha(c) { return isLower(c) || isUpper(c); }
function isDigit(c) { return c >= '0' && c <= '9'; }
function isAlnum(c) { return isAlpha(c) || isDigit(c); }
function isBlank(c) { return c == ' ' || c == '\t'; }
function isSpace(c) { return isBlank(c) || c == '\r' || c == '\n'; }
function isXdigit(c) { return isDigit(c) || (c >= 'a' && c <= 'f') || (c >= 'A' && c <= 'F'); }
function toLower(c) { return c.toLowerCase(); }
function toUpper(c) { return c.toUpperCase(); }


// Lists

function cons(v, ls) {
  return { next : ls, data : v };
}
function rev(ls) {
  var acc = null;
  for (; ls; ls = ls.next)
    acc = cons(ls.data, acc);
  return acc;
}
function concat(ls1, ls2) {
  var acc = ls2;
  ls1 = rev(ls1);
  for (; ls1; ls1 = ls1.next)
    acc = cons(ls1.data, acc);
  return acc;
}
function member(x, ls) {
  for (; ls; ls = ls.next)
    if (ls.data == x)
      return true;
  return false;
}
function remove(x, ls) {
  var acc = null;

  for (; ls; ls = ls.next)
    if (ls.data == x)
      return concat(acc, ls.next);
    else
      acc = cons(ls.data, acc);

  return ls;
}
function union(ls1, ls2) {
  var acc = ls2;

  for (; ls1; ls1 = ls1.next)
    if (!member(ls1.data, ls2))
      acc = cons(ls1.data, acc);

  return acc;
}
function length(ls) {
  var acc = 0;

  for (; ls; ls = ls.next)
    ++acc;

  return acc;
}


// Error handling

function whine(msg) {
  alert(msg);
  throw msg;
}

function pf(loc) {
  throw ("Pattern match failure (" + loc + ")");
}

function runHandlers(kind, ls, arg) {
  if (ls == null)
    alert(kind + ": " + arg);
  for (; ls; ls = ls.next)
    try {
      exec({c:"a", f:{c:"a", f:ls.data, x:{c:"c", v:arg}}, x:{c:"c", v:null}});
    } catch (v) { }
}

var errorHandlers = null;

function onError(f) {
  errorHandlers = cons(f, errorHandlers);
}

function er(s) {
  runHandlers("Error", errorHandlers, s);
  throw {uw_error: s};
}

var failHandlers = null;

function onFail(f) {
  failHandlers = cons(f, failHandlers);
}

function doExn(v) {
  if (v == null || v.uw_error == null) {
    var s = (v == null ? "null" : v.message ? v.message : v.toString());
    if (v != null && v.fileName && v.lineNumber)
      s += " (" + v.fileName + ":" + v.lineNumber + ")";
    runHandlers("Fail", failHandlers, s);
  }
}

var disconnectHandlers = null;

function flift(f) {
  return {env:cons(f,null), body:{c:"v", n:1}};
}

function onDisconnect(f) {
  disconnectHandlers = cons(flift(f), disconnectHandlers);
}

function discon() {
  runHandlers("Disconnect", disconnectHandlers, null);
}

var connectHandlers = null;

function onConnectFail(f) {
  connectHandlers = cons(flift(f), connectHandlers);
}

function conn() {
  runHandlers("Connect", connectHandlers, null);
}

var serverHandlers = null;

function onServerError(f) {
  serverHandlers = cons(f, serverHandlers);
}

function servErr(s) {
  window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0);
}


// Embedding closures in XML strings

function cs(f) {
  return {closure: f};
}

function isWeird(v) {
  return v.closure != null || v.cat1 != null;
}

function cat(s1, s2) {
  if (isWeird(s1) || isWeird(s2))
    return {cat1: s1, cat2: s2};
  else
    return s1 + s2;
}

var closures = [];
var freeClosures = null;

function newClosure(f) {
  var n;
  if (freeClosures == null) {
    n = closures.length;
  } else {
    n = freeClosures.data;
    freeClosures = freeClosures.next;
  }
  closures[n] = f;
  return n;
}

function freeClosure(n) {
  closures[n] = null;
  freeClosures = cons(n, freeClosures);
}

function cr(n) {
  return closures[n];
}

function flatten(cls, tr) {
  if (tr.cat1 != null)
    return flatten(cls, tr.cat1) + flatten(cls, tr.cat2);
  else if (tr.closure != null) {
    var cl = newClosure(tr.closure);
    cls.v = cons(cl, cls.v);
    return "cr(" + cl + ")";
  } else
    return tr;
}

function flattenLocal(s) {
  var cls = {v : null};
  var r = flatten(cls, s);
  for (cl = cls.v; cl != null; cl = cl.next)
    freeClosure(cl.data);
  return r;
}



// Dynamic tree management

function populate(node) {
  var s = node.signal;
  var oldSources = node.sources;
  try {
    var sr = execF(s, null);
    var newSources = sr._sources;

    for (var sp = oldSources; sp; sp = sp.next)
      if (!member(sp.data, newSources))
        sp.data.dyns = remove(node, sp.data.dyns);

    for (var sp = newSources; sp; sp = sp.next)
      if (!member(sp.data, oldSources))
        sp.data.dyns = cons(node, sp.data.dyns);

    node.sources = newSources;
    node.recreate(sr._data);
  } catch (v) {
    doExn(v);
  }
}

function sc(v) {
  return {data : v, dyns : null};
}
function sv(s, v) {
  s.data = v;

  for (var ls = s.dyns; ls; ls = ls.next)
    if (!ls.dead)
      populate(ls.data);
}
function sg(s) {
  return s.data;
}

function ss(s) {
  return {env:cons(s, null), body:{c:"r", l:
    cons({n:"sources", v:{c:"c", v:cons(s, null)}},
      cons({n:"data", v:{c:"f", f:sg, a:cons({c:"v", n:1}, null)}}, null))}};
}
function sr(v) {
  return {env:null, body:{c:"c", v:{_sources : null, _data : v}}};
}
function sb(x,y) {
  return {env:cons(y,cons(x,null)),
    body:{c:"=",
      e1:{c:"a", f:{c:"v", n:2}, x:{c:"c", v:null}},
      e2:{c:"=",
        e1:{c:"a",
          f:{c:"a", f:{c:"v", n:2}, x:{c:".", r:{c:"v", n:0}, f:"data"}},
          x:{c:"c", v:null}},
        e2:{c:"r", l:cons(
          {n:"sources", v:{c:"f", f:union, a:cons({c:".", r:{c:"v", n:1}, f:"sources"},
            cons({c:".", r:{c:"v", n:0}, f:"sources"}, null))}},
          cons({n:"data", v:{c:".", r:{c:"v", n:0}, f:"data"}}, null))}}}};
}
function scur(s) {
  return execF(s, null)._data;
}

function lastParent() {
  var pos = document.body;

  while (pos.lastChild && pos.lastChild.nodeType == 1)
    pos = pos.lastChild;

  pos = pos.parentNode;

  return pos;
}

function parent() {
  return thisScript ? thisScript.parentNode : lastParent();
}

function addNode(node) {
  if (thisScript)
    thisScript.parentNode.replaceChild(node, thisScript);
  else
    lastParent().appendChild(node);
}

var thisScript = null;

function runScripts(node) {
  if (node.getElementsByTagName) {
    var savedScript = thisScript;

    var scripts = node.getElementsByTagName("script"), scriptsCopy = [];
    var len = scripts.length;
    for (var i = 0; i < len; ++i)
      scriptsCopy[i] = scripts[i];
    for (var i = 0; i < len; ++i) {
      thisScript = scriptsCopy[i];

      try {
        eval(thisScript.text);
      } catch (v) {
        doExn(v);
      }
      if (thisScript.parentNode)
        thisScript.parentNode.removeChild(thisScript);
    }

    thisScript = savedScript;
  }
}


// Dynamic tree entry points

function killScript(scr) {
  scr.dead = true;
  for (var ls = scr.sources; ls; ls = ls.next)
    ls.data.dyns = remove(scr, ls.data.dyns);
  for (var ls = scr.closures; ls; ls = ls.next)
    freeClosure(ls.data);
}

function dyn(pnode, s) {
  var x = document.createElement("script");
  x.dead = false;
  x.signal = s;
  x.sources = null;
  x.closures = null;

  var firstChild = null;

  x.recreate = function(v) {
    for (var ls = x.closures; ls; ls = ls.next)
      freeClosure(ls.data);

    var next;
    for (var child = firstChild; child && child != x; child = next) {
      next = child.nextSibling;

      killScript(child);
      if (child.getElementsByTagName) {
        var arr = child.getElementsByTagName("script");
        for (var i = 0; i < arr.length; ++i)
          killScript(arr[i]);
      }

      if (child.parentNode)
        child.parentNode.removeChild(child);
    }

    var cls = {v : null};
    var html = flatten(cls, v);
    if (pnode != "table" && pnode != "tr")
      html = dynPrefix + html;
    x.closures = cls.v;

    if (pnode == "table") {
      var dummy = document.createElement("body");
      dummy.innerHTML = "<table>" + html + "</table>";
      runScripts(dummy);
      var table = x.parentNode;

      if (table) {
        firstChild = null;
        var tbody;

        var arr = dummy.getElementsByTagName("tbody");

        var tbody;
        if (arr.length > 0 && arr[0].parentNode == dummy.firstChild) {
          tbody = arr[0];
          var next;
          for (var node = dummy.firstChild.firstChild; node; node = next) {
            next = node.nextSibling;

            if (node.tagName != "TBODY")
              tbody.appendChild(node);
          }
        } else
          tbody = dummy.firstChild;

        var next;
        firstChild = document.createElement("script");
        table.insertBefore(firstChild, x);
        for (var node = tbody.firstChild; node; node = next) {
          next = node.nextSibling;
          table.insertBefore(node, x);
        }
      }
    } else if (pnode == "tr") {
      var dummy = document.createElement("body");
      dummy.innerHTML = "<table><tr>" + html + "</tr></table>";
      runScripts(dummy);
      var table = x.parentNode;

      if (table) {
        var arr = dummy.getElementsByTagName("tr");
        firstChild = null;
        var tr;
        if (arr.length > 0 && table != null)
          tr = arr[0];
        else
          tr = dummy.firstChild;

        var next;
        firstChild = document.createElement("script");
        table.insertBefore(firstChild, x);
        for (var node = tr.firstChild; node; node = next) {
          next = node.nextSibling;
          table.insertBefore(node, x);
        }
      }
    } else {
      firstChild = document.createElement("span");
      firstChild.innerHTML = html;
      runScripts(firstChild);
      if (x.parentNode)
        x.parentNode.insertBefore(firstChild, x);
    }
  };

  addNode(x);
  populate(x);
}

function input(x, s, recreate, type) {
  if (type) x.type = type;
  x.dead = false;
  x.signal = ss(s);
  x.sources = null;
  x.recreate = recreate(x);
  addNode(x);
  populate(x);

  return x;
}

function inp(s) {
  var x = input(document.createElement("input"), s,
        function(x) { return function(v) { if (x.value != v) x.value = v; }; });
  x.value = s.data;
  x.onkeyup = function() { sv(s, x.value) };

  return x;
}

function sel(s, content) {
  var dummy = document.createElement("span");
  dummy.innerHTML = "<select>" + content + "</select>";
  var x = input(dummy.firstChild, s, function(x) { return function(v) { if (x.value != v) x.value = v; }; });
  x.value = s.data;
  if (x.value != s.data)
    sv(s, x.value);
  x.onchange = function() { sv(s, x.value) };

  return x;
}

function chk(s) {
  var x = input(document.createElement("input"), s,
        function(x) { return function(v) { if (x.checked != v) x.checked = v; }; }, "checkbox");
  x.defaultChecked = x.checked = s.data;
  x.onclick = function() { sv(s, x.checked) };

  return x;
}

function tbx(s) {
  var x = input(document.createElement("textarea"), s,
        function(x) { return function(v) { if (x.innerHTML != v) x.innerHTML = v; }; });
  x.innerHTML = s.data;
  x.onkeyup = function() { sv(s, x.value) };

  return x;
}

function addOnChange(x, f) {
  var old = x.onchange;
  x.onchange = function() { old(); f (); };
}


// Basic string operations

function eh(x) {
  if (x == null)
    return "NULL";
  else
    return x.split("&").join("&amp;").split("<").join("&lt;").split(">").join("&gt;");
}

function ts(x) { return x.toString() }
function bs(b) { return (b ? "True" : "False") }

function id(x) { return x; }
function sub(s, i) { return s.charAt(i); }
function suf(s, i) { return s.substring(i); }
function slen(s) { return s.length; }
function sidx(s, ch) {
  var r = s.indexOf(ch);
  if (r == -1)
    return null;
  else
    return r;
}
function sspn(s, chs) {
  for (var i = 0; i < s.length; ++i)
    if (chs.indexOf(s.charAt(i)) != -1)
      return i;

  return null;
}
function schr(s, ch) {
  var r = s.indexOf(ch);
  if (r == -1)
    return null;
  else
    return s.substring(r);
}
function ssub(s, start, len) {
  return s.substring(start, start+len);
}

function pi(s) {
  var r = parseInt(s);
  if (r.toString() == s)
    return r;
  else
    er("Can't parse int: " + s);
}

function pfl(s) {
  var r = parseFloat(s);
  if (r.toString() == s)
    return r;
  else
    er("Can't parse float: " + s);
}

function pio(s) {
  var r = parseInt(s);
  if (r.toString() == s)
    return r;
  else
    return null;
}

function pflo(s) {
  var r = parseFloat(s);
  if (r.toString() == s)
    return r;
  else
    return null;
}

function uf(s) {
  if (s.length == 0)
    return "_";
  return (s.charAt(0) == '_' ? "_" : "") + encodeURIComponent(s);
}

function uu(s) {
  if (s.length > 0 && s.charAt(0) == '_') {
    s = s.substring(1);
  } else if (s.length >= 3 && s.charAt(0) == '%' && s.charAt(1) == '5' && (s.charAt(2) == 'f' || s.charAt(2) == 'F'))
    s = s.substring(3);
  return decodeURIComponent(s.replace(new RegExp ("\\+", "g"), " "));
}

function atr(s) {
  return s.replace(new RegExp ("\"", "g"), "&quot;").replace(new RegExp ("&", "g"), "&amp;")
}

function ub(b) {
  return b ? "1" : "0";
}

function uul(getToken, getData) {
  var tok = getToken();
  if (tok == "Nil") {
    return null;
  } else if (tok == "Cons") {
    var d = getData();
    var l = uul(getToken, getData);
    return {_1:d, _2:l};
  } else
    whine("Can't unmarshal list (" + tok + ")");
}

function strcmp(str1, str2) {
  return ((str1 == str2) ? 0 : ((str1 > str2) ? 1 : -1));
}


// Remote calls

var client_id = null;
var client_pass = 0;
var url_prefix = "/";
var timeout = 60;

function getXHR(uri)
{
  try {
    return new XMLHttpRequest();
  } catch (e) {
    try {
     return new ActiveXObject("Msxml2.XMLHTTP");
    } catch (e) {
      try {
        return new ActiveXObject("Microsoft.XMLHTTP");
      } catch (e) {
        whine("Your browser doesn't seem to support AJAX.");
      }
    }
  }
}

var sig = null;

var unloading = false, inFlight = null;

function unload() {
  unloading = true;

  for (; inFlight; inFlight = inFlight.next) {
    inFlight.data.abort();
  }
}

function requestUri(xhr, uri, needsSig) {
  if (unloading)
    return;

  xhr.open("POST", uri, true);
  xhr.setRequestHeader("Content-type", "text/plain");
  xhr.setRequestHeader("Content-length", "0");
  xhr.setRequestHeader("Connection", "close");

  if (client_id != null) {
    xhr.setRequestHeader("UrWeb-Client", client_id.toString());
    xhr.setRequestHeader("UrWeb-Pass", client_pass.toString());
  }

  if (needsSig) {
    if (sig == null)
      whine("Missing cookie signature!");

    xhr.setRequestHeader("UrWeb-Sig", sig);
  }

  inFlight = cons(xhr, inFlight);
  xhr.send(null);
}

function xhrFinished(xhr) {
  xhr.abort();
  inFlight = remove(xhr, inFlight);
}

function unurlify(parse, s) {
  return parse(s);
}

function rc(prefix, uri, parse, k, needsSig) {
  uri = cat(prefix, uri);
  uri = flattenLocal(uri);
  var xhr = getXHR();

  xhr.onreadystatechange = function() {
    if (xhr.readyState == 4) {
      var isok = false;

      try {
        if (xhr.status == 200)
          isok = true;
      } catch (e) { }

      if (isok) {
        try {
          k(parse(xhr.responseText));
        } catch (v) {
          doExn(v);
        }
      } else {
        conn();
      }

      xhrFinished(xhr);
    }
  };

  requestUri(xhr, uri, needsSig);
}

function path_join(s1, s2) {
  if (s1.length > 0 && s1.charAt(s1.length-1) == '/')
    return s1 + s2;
  else
    return s1 + "/" + s2;
}

var channels = [];

function newQueue() {
  return { front : null, back : null };
}
function enqueue(q, v) {
  if (q.front == null) {
    q.front = cons(v, null);
    q.back = q.front;
  } else {
    var node = cons(v, null);
    q.back.next = node;
    q.back = node;
  }
}
function dequeue(q) {
  if (q.front == null)
    return null;
  else {
    var r = q.front.data;
    q.front = q.front.next;
    if (q.front == null)
      q.back = null;
    return r;
  }
}

function newChannel() {
  return { msgs : newQueue(), listeners : newQueue() };
}

function listener() {
  var uri = path_join(url_prefix, ".msgs");
  var xhr = getXHR();
  var tid, orsc, onTimeout;

  var connect = function () {
    xhr.onreadystatechange = orsc;
    tid = window.setTimeout(onTimeout, timeout * 500);
    requestUri(xhr, uri, false);
  }

  orsc = function() {
    if (xhr.readyState == 4) {
      window.clearTimeout(tid);

      var isok = false;

      try {
        if (xhr.status == 200)
          isok = true;
      } catch (e) { }

      if (isok) {
        var text = xhr.responseText
        if (text == "")
          return;
        var lines = text.split("\n");

        if (lines.length < 2) {
          discon();
          return;
        }

        for (var i = 0; i+1 < lines.length; i += 2) {
          var chn = lines[i];
          var msg = lines[i+1];

          if (chn < 0)
            whine("Out-of-bounds channel in message from remote server");

          var ch;

          if (chn >= channels.length || channels[chn] == null) {
            ch = newChannel();
            channels[chn] = ch;
          } else
            ch = channels[chn];

          var listener = dequeue(ch.listeners);
          if (listener == null) {
            enqueue(ch.msgs, msg);
          } else {
            try {
              listener(msg);
            } catch (v) {
              doExn(v);
            }
          }
        }

        xhrFinished(xhr);

        connect();
      }
      else {
        try {
          if (xhr.status != 0)
            servErr("Error querying remote server for messages: " + xhr.status);
        } catch (e) { }
      }
    }
  };

  onTimeout = function() {
    xhrFinished(xhr);
    connect();
  };

  connect();
}

function rv(chn, parse, k) {
  if (chn == null)
    return;

  if (chn < 0)
    whine("Out-of-bounds channel receive");

  var ch;

  if (chn >= channels.length || channels[chn] == null) {
    ch = newChannel();
    channels[chn] = ch;
  } else
    ch = channels[chn];

  var msg = dequeue(ch.msgs);
  if (msg == null) {
    enqueue(ch.listeners, function(msg) { k(parse(msg)); });
  } else {
    try {
      k(parse(msg));
    } catch (v) {
      doExn(v);
    }
  }
}

function sl(ms, k) {
  window.setTimeout(function() { k(null); }, ms);
}

function sp(e) {
  execF(e, null);
}


// Key events

var uw_event = null;

function kc() {
  return window.event ? uw_event.keyCode : uw_event.which;
}


// The Ur interpreter

var urfuncs = [];

function lookup(env, n) {
  while (env != null) {
    if (n == 0)
      return env.data;
    else {
      --n;
      env = env.next;
    }
  }

  whine("Out-of-bounds Ur variable reference");
}

function execP(env, p, v) {
  switch (p.c) {
  case "w":
    return env;
  case "v":
    return cons(v, env);
  case "c":
    if (v == p.v)
      return env;
    else
      return false;
  case "s":
    if (v == null)
      return false;
    else
      return execP(env, p.p, p.n ? v.v : v);
  case "1":
    if (v.n != p.n)
      return false;
    else
      return execP(env, p.p, v.v);
  case "r":
    for (var fs = p.l; fs != null; fs = fs.next) {
      env = execP(env, fs.data.p, v["_" + fs.data.n]);
      if (env == false)
        return false;
    }
    return env;
  default:
    whine("Unknown Ur pattern kind" + p.c);
  }
}

function exec0(env, e) {
  return exec1(env, null, e);
}

function exec1(env, stack, e) {
  var stack, usedK = false;

  var saveEnv = function() {
    if (stack.next != null && stack.next.data.c != "<")
      stack = cons({c: "<", env: env}, stack.next);
    else
      stack = stack.next;
  };

  while (true) {
    switch (e.c) {
    case "c":
      var v = e.v;
      if (stack == null)
        return v;
      var fr = stack.data;

      switch (fr.c) {
      case "s":
        e = {c: "c", v: {v: v}};
        stack = stack.next;
        break;
      case "1":
        e = {c: "c", v: {n: fr.n, v: v}};
        stack = stack.next;
        break;
      case "f":
        fr.args[fr.pos++] = v;
        if (fr.a == null) {
          var res;
          stack = stack.next;

          if (fr.f.apply)
            res = fr.f.apply(null, fr.args);
          else if (fr.args.length == 0)
            res = fr.f();
          else if (fr.args.length == 1)
            res = fr.f(fr.args[0]);
          else if (fr.args.length == 2)
            res = fr.f(fr.args[0], fr.args[1]);
          else if (fr.args.length == 3)
            res = fr.f(fr.args[0], fr.args[1], fr.args[2]);
          else if (fr.args.length == 4)
            res = fr.f(fr.args[0], fr.args[1], fr.args[2], fr.args[3]);
          else if (fr.args.length == 5)
            res = fr.f(fr.args[0], fr.args[1], fr.args[2], fr.args[3], fr.args[4]);
          else
            whine("Native function has " + fr.args.length + " args, but there is no special case for that count.");

          e = {c: "c", v: res};
          if (usedK) return null;
        } else {
          e = fr.a.data;
          fr.a = fr.a.next;
        }
        break;
      case "a1":
        e = fr.x;
        stack = cons({c: "a2", f: v}, stack.next);
        break;
      case "a2":
        if (fr.f == null)
          whine("Ur: applying null function");
        else if (fr.f.body) {
          saveEnv();
          env = cons(v, fr.f.env);
          e = fr.f.body;
        } else {
          e = {c: "c", v: fr.f(v)};
          stack = stack.next;
        }
        break;
      case "<":
        env = fr.env;
        stack = stack.next;
        break;
      case "r":
        fr.fs["_" + fr.n] = v;
        if (fr.l == null) {
          e = {c: "c", v: fr.fs};
          stack = stack.next;
        } else {
          fr.n = fr.l.data.n;
          e = fr.l.data.v;
          fr.l = fr.l.next;
        }
        break;
      case ".":
        e = {c: "c", v: v["_" + fr.f]};
        stack = stack.next;
        break;
      case ";":
        e = fr.e2;
        stack = stack.next;
        break;
      case "=":
        saveEnv();
        env = cons(v, env);
        e = fr.e2;
        break;
      case "m":
        var ps;
        for (ps = fr.p; ps != null; ps = ps.next) {
          var r = execP(env, ps.data.p, v);
          if (r != false) {
            saveEnv();
            env = r;
            e = ps.data.b;
            break;
          }
        }
        if (ps == null)
          whine("Match failure in Ur interpretation");
        break;
      default:
        whine("Unknown Ur continuation kind " + fr.c);
      }

      break;
    case "v":
      e = {c: "c", v: lookup(env, e.n)};
      break;
    case "n":
      e = urfuncs[e.n];
      break;
    case "s":
      stack = cons({c: "s"}, stack);
      e = e.v;
      break;
    case "1":
      stack = cons({c: "1", n: e.n}, stack);
      e = e.v;
      break;
    case "f":
      if (e.a == null)
        e = {c: "c", v: (eval(e.f))()};
      else {
        var args = [];
        stack = cons({c: "f", f: eval(e.f), args: args, pos: 0, a: e.a.next}, stack);
        if (!e.a.data.c) alert("[2] fr.f = " + e.f + "; 0 = " + e.a.data);
        e = e.a.data;
      }
      break;
    case "l":
      e = {c: "c", v: {env: env, body: e.b}};
      break;
    case "a":
      stack = cons({c: "a1", x: e.x}, stack);
      e = e.f;
      break;
    case "r":
      if (e.l == null)
        whine("Empty Ur record in interpretation");
      var fs = {};
      stack = cons({c: "r", n: e.l.data.n, fs: fs, l: e.l.next}, stack);
      e = e.l.data.v;
      break;
    case ".":
      stack = cons({c: ".", f: e.f}, stack);
      e = e.r;
      break;
    case ";":
      stack = cons({c: ";", e2: e.e2}, stack);
      e = e.e1;
      break;
    case "=":
      stack = cons({c: "=", e2: e.e2}, stack);
      e = e.e1;
      break;
    case "m":
      stack = cons({c: "m", p: e.p}, stack);
      e = e.e;
      break;
    case "e":
      e = {c: "c", v: cs({c: "wc", env: env, body: e.e})};
      break;
    case "wc":
      env = e.env;
      e = e.body;
      break;
    case "K":
      { var savedStack = stack.next, savedEnv = env;
      e = {c: "c", v: function(v) { return exec1(savedEnv, savedStack, {c: "c", v: v}); } };}
      usedK = true;
      break;      
    default:
      whine("Unknown Ur expression kind " + e.c);
    }
  }
}

function execD(e) {
  return exec0(null, e);
}

function exec(e) {
  var r = exec0(null, e);

  if (r != null && r.body != null)
    return function(v) { return exec0(cons(v, r.env), r.body); };
  else
    return r;
}

function execF(f, x) {
  return exec0(cons(x, f.env), f.body);
}


// App-specific code