-rw-r--r-- 76692 holtrace-20250617/holtrace-verify.c raw
#include <stdio.h>
#include <stdlib.h>
#include <inttypes.h>
#include "vector.h"
#include "in.h"

typedef long long num;

VECTOR_define_inline(char);
VECTOR_define_inline(num);

// ===== state

static num curline = 1; // 1-numbered for error messages
static num typeid;
static num termid;
static num thmid;
static num infid;
static num typedefid;
static num ptid;

static vector_char type2tag_vec;
static num type2tag(num type) { return vector_char_read(&type2tag_vec,type); }

static vector_char term2tag_vec;
static char term2tag(num term) { return vector_char_read(&term2tag_vec,term); }

static vector_num typedata;
static vector_num type2datapos;
static vector_num type2hash;

static vector_num termdata;
static vector_num term2datapos;
static vector_num termfrees;
static vector_num term2freepos;
static vector_num term2freelen;
static vector_num term2hash;

static vector_num thmdata;
static vector_num thm2datapos;
static vector_num thm2conclusion;

static vector_char typedef2split;
static vector_num typedef2reptype;
static vector_num typedef2repprop;
static vector_num typedef2numtyvars;
static vector_num typedef2infid;
static vector_num typedef2abstypename;
static vector_num typedef2absname;
static vector_num typedef2repname;
static vector_num typedef2tyvarnames;

static char lastinftag;

// ===== general constraints

#define CUTOFF 288230376151711743LL
// but likely to abort before that from running out of heap space
// also, could abort from running out of stack space for recursion

// want this in production, ignoring NDEBUG, always having side effects
#define know(property) ((property) ? 0 : (fprintf(stderr,"code line %d: internal error: failed %s\n",__LINE__,#property), exit(100)))

static void reject(const char *err)
{
  fprintf(stderr,"line %lld: %s\n",curline,err);
  exit(100);
}

// ===== general parsing

// some allowed variations:
// will accept leading zeros
// will not require, e.g., id-1 to be !
// will accept space even when not needed
static num subid_core(const char **s,num id)
{
  const char *t = *s;
  if (*t == '\n') reject("missing numeric argument");
  if (*t == '!') { *s = t+1; return id-1; }
  if (*t == '@') { *s = t+1; return id-2; }
  if (*t == '#') { *s = t+1; return id-3; }
  if (*t == '$') { *s = t+1; return id-4; }
  if (*t == '%') { *s = t+1; return id-5; }
  if (*t == '^') { *s = t+1; return id-6; }
  if (*t == '&') { *s = t+1; return id-7; }
  if (*t == '*') { *s = t+1; return id-8; }
  if (*t == '(') { *s = t+1; return id-9; }
  if (*t == ')') { *s = t+1; return id-10; }

  int negate = 0;
  if (*t == '-') { ++t; negate = 1; }
  num result = 0;
  for (;;) {
    char c = *t;
    if (result >= CUTOFF) {
      fprintf(stderr,"line %lld: refusing to handle number %lld\n",curline,result);
      exit(100);
    }
    if (c >= '0' && c <= '9')
      result = 32*result+(c-'0');
    else if (c >= 'A' && c <= 'V')
      result = 32*result+(c-'7');
    else break;
    ++t;
  }
  if (*t == ' ') ++t;
  if (t == *s) reject("non-numeric argument where numeric is expected");
  *s = t;
  return negate ? id-result : result;
}

static num subid(const char **s,num id)
{
  num result = subid_core(s,id);
  if (result < 0 || (result >= id && id >= 0)) {
    fprintf(stderr,"line %lld: result %lld out of range\n",curline,result);
    exit(100);
  }
  return result;
}

static void noteol(const char *s)
{
  if (*s == '\n') reject("empty name");
}

static void eol(const char *s)
{
  if (*s != '\n') reject("extra arguments");
}

// ===== name operations

static int name_cmp(const char *s,const char *t)
{
  for (;;) {
    char a = *s++;
    char b = *t++;
    if (a > b) return 1;
    if (a < b) return -1;
    if (a == '\n') return 0;
  }
}

static int name_is(const char *s,const char *t)
{
  for (;;) {
    char a = *s++;
    char b = *t++;
    if (a != b) return 0;
    if (a == '\n') return 1;
  }
}

static int name_is_withsplit(const char *s,const char *t,char split)
{
  for (;;) {
    char a = *s++;
    char b = *t++;
    if (a == '\n') return b == split;
    if (b == split) return 0;
    if (a != b) return 0;
  }
}

static int nameprimes_is(const char *s,num sprimes,const char *t,num tprimes)
{
  for (;;) {
    char a = *s;
    if (a != '\n') ++s; else if (sprimes) { a = '\''; --sprimes; }
    char b = *t;
    if (b != '\n') ++t; else if (tprimes) { b = '\''; --tprimes; }
    if (a != b) return 0;
    if (a == '\n') return 1;
  }
}

static num hash_mix(num h)
{
  uint32_t h0 = h;
  uint32_t h1 = h>>32;
  h0 ^= (h1<<5)|(h1>>27);
  h1 += (h0<<7)|(h0>>25);
  h0 ^= (h1<<11)|(h1>>21);
  h1 ^= (h0<<16)|(h0>>16);
  h = h1;
  h <<= 32;
  h |= h0;
  return h;
}

static num name_hash(const char *s)
{
  num result = 632422315470652589LL;
  for (;;) {
    char c = *s++;
    if (c == '\n') return result;
    result = hash_mix(result+c);
  }
}

// ===== name->num dictionaries
// XXX speed: maybe use faster associative array

typedef struct {
  // for one->3, two->1, three->4, four->1:
  vector_char names; // one\ntwo\nthree\nfour\n
  vector_num index2pos; // 0 3 6 11
  vector_num index2result; // 3 1 4 1
} dict;

static int dict_namematch(dict *d,const char *s,char split,num pos)
{
  for (;;) {
    char a = *s++;
    char b = vector_char_read(&d->names,pos++);
    if (a == split) return b == '\n';
    if (b == '\n') return 0;
    if (a != b) return 0;
  }
}

static num dict_lookup(dict *d,const char *s,char split,int *flag)
{
  num len = vector_num_len(&d->index2pos);
  for (num i = 0;i < len;++i) {
    num pos = vector_num_read(&d->index2pos,i);
    if (dict_namematch(d,s,split,pos)) {
      if (flag) *flag = 1;
      return vector_num_read(&d->index2result,i);
    }
  }
  if (flag) *flag = 0;
  return -1;
}

static void dict_add(dict *d,const char *s,char split,num result)
{
  vector_num_append(&d->index2result,result);
  num pos = vector_char_len(&d->names);
  vector_num_append(&d->index2pos,pos);
  while (*s != split)
    vector_char_append(&d->names,*s++);
  vector_char_append(&d->names,'\n');
}

static dict const2type_dict;
static num const2type(const char *s) { return dict_lookup(&const2type_dict,s,'\n',0); }

static dict absname2typedef_dict;
static num absname2typedef(const char *s) { return dict_lookup(&absname2typedef_dict,s,'\n',0); }

static dict repname2typedef_dict;
static num repname2typedef(const char *s) { return dict_lookup(&repname2typedef_dict,s,'\n',0); }

static void reject_previous_constnames(const char *s,char split)
{
  if (name_is_withsplit("=\n",s,split)) reject("const name =");
  if (name_is_withsplit("@\n",s,split)) reject("const name @");
  if (dict_lookup(&const2type_dict,s,split,0) >= 0) reject("colliding const name");
  if (dict_lookup(&absname2typedef_dict,s,split,0) >= 0) reject("colliding const name");
  if (dict_lookup(&repname2typedef_dict,s,split,0) >= 0) reject("colliding const name");
}

static void const2type_add(const char *s,char split,num result)
{
  reject_previous_constnames(s,split);
  dict_add(&const2type_dict,s,split,result);
}

static void absname2typedef_add(const char *s,char split,num result)
{
  reject_previous_constnames(s,split);
  dict_add(&absname2typedef_dict,s,split,result);
}

static void repname2typedef_add(const char *s,char split,num result)
{
  reject_previous_constnames(s,split);
  dict_add(&repname2typedef_dict,s,split,result);
}

static dict app2arity_dict;

static num app2arity(const char *s)
{
  if (name_is(s,"fun\n")) return 2;
  if (name_is(s,"bool\n")) return 0;
  if (name_is(s,"ind\n")) return 0;
  return dict_lookup(&app2arity_dict,s,'\n',0);
}

// trying to match new_type in fusion.ml
static void app2arity_add(const char *s,char split,num arity)
{
  if (name_is_withsplit("fun\n",s,split)) reject("colliding tyapp name");
  if (name_is_withsplit("bool\n",s,split)) reject("colliding tyapp name");
  if (name_is_withsplit("ind\n",s,split)) reject("colliding tyapp name");
  if (dict_lookup(&app2arity_dict,s,split,0) >= 0) reject("colliding tyapp name");
  dict_add(&app2arity_dict,s,split,arity);
}

// ===== type operations

static int type_cmp(num type,num TYPE)
{
  if (type == TYPE) return 0;
  char tag = type2tag(type);
  char TAG = type2tag(TYPE);
  if (tag > TAG) return 1;
  if (tag < TAG) return -1;
  num pos1 = vector_num_read(&type2datapos,type+1);
  num POS1 = vector_num_read(&type2datapos,TYPE+1);
  char *s = in_buf+vector_num_read(&typedata,pos1-1);
  char *S = in_buf+vector_num_read(&typedata,POS1-1);
  int result = name_cmp(s,S);
  if (result) return result;
  if (tag == 'a') return 0;
  know(tag == 'b');
  num pos0 = vector_num_read(&type2datapos,type);
  num POS0 = vector_num_read(&type2datapos,TYPE);
  know(POS1-POS0 == pos1-pos0);
  for (num i = 0;i < pos1-1-pos0;++i) {
    num subtype = vector_num_read(&typedata,pos0+i);
    num SUBTYPE = vector_num_read(&typedata,POS0+i);
    result = type_cmp(subtype,SUBTYPE);
    if (result) return result;
  }
  return 0;
}

static int type_is(num type,num TYPE)
{
  if (type == TYPE) return 1;
  if (vector_num_read(&type2hash,type) != vector_num_read(&type2hash,TYPE)) return 0;
  return type_cmp(type,TYPE) == 0;
}

static int type_is_tyvarnamed(num type,const char *name,char split)
{
  if (type2tag(type) != 'a') return 0;
  num pos0 = vector_num_read(&type2datapos,type);
  num pos1 = vector_num_read(&type2datapos,type+1);
  if (pos1-pos0 != 1) return 0;
  const char *typename = in_buf+vector_num_read(&typedata,pos0);
  return name_is_withsplit(typename,name,split);
}

// does not constrain arguments
static int type_is_appnamed(num type,const char *name,char split)
{
  if (type2tag(type) != 'b') return 0;
  num pos1 = vector_num_read(&type2datapos,type+1);
  const char *typename = in_buf+vector_num_read(&typedata,pos1-1);
  return name_is_withsplit(typename,name,split);
}

static int type_is_bool(num type)
{
  if (type2tag(type) != 'b') return 0;
  num pos0 = vector_num_read(&type2datapos,type);
  num pos1 = vector_num_read(&type2datapos,type+1);
  if (pos1-pos0 != 1) return 0;
  return name_is(in_buf+vector_num_read(&typedata,pos0),"bool\n");
}

static int type_is_fun(num type,num *from,num *to)
{
  if (type2tag(type) != 'b') return 0;
  num pos0 = vector_num_read(&type2datapos,type);
  num pos1 = vector_num_read(&type2datapos,type+1);
  if (pos1-pos0 != 3) return 0;
  if (!name_is(in_buf+vector_num_read(&typedata,pos0+2),"fun\n")) return 0;
  if (from) *from = vector_num_read(&typedata,pos0);
  if (to) *to = vector_num_read(&typedata,pos0+1);
  return 1;
}

static int type_is_funfromto(num type,num from,num to)
{
  num frommatch,tomatch;
  if (!type_is_fun(type,&frommatch,&tomatch)) return 0;
  if (!type_is(from,frommatch)) return 0;
  if (!type_is(to,tomatch)) return 0;
  return 1;
}

static int type_is_abstype(num abstype,const char *abstypename,const char *tyvarnames,num numtyvars,char split)
{
  if (type2tag(abstype) != 'b') return 0;
  num pos0 = vector_num_read(&type2datapos,abstype);
  num pos1 = vector_num_read(&type2datapos,abstype+1);
  if (pos1-pos0 != numtyvars+1) return 0;
  if (!name_is_withsplit(in_buf+vector_num_read(&typedata,pos1-1),abstypename,split)) return 0;
  const char *s = tyvarnames;
  for (num i = 0;i < numtyvars;++i) {
    num subtype = vector_num_read(&typedata,pos0+i);
    if (!type_is_tyvarnamed(subtype,s,split)) return 0;
    while (*s != split) ++s;
    ++s;
  }
  return 1;
}

// 1 if TYPE is result of tyvarnames->abstype substitution into type
static int type_tyvarnames_subst_is(num type,num TYPE,num abstype,num numtyvars,const char *tyvarnames,char split)
{
  if (!numtyvars) return type_is(type,TYPE);

  char tag = type2tag(type);

  if (tag == 'b') {
    if (type2tag(TYPE) != 'b') return 0;
    num pos1 = vector_num_read(&type2datapos,type+1);
    num POS1 = vector_num_read(&type2datapos,TYPE+1);
    char *s = in_buf+vector_num_read(&typedata,pos1-1);
    char *S = in_buf+vector_num_read(&typedata,POS1-1);
    if (!name_is(s,S)) return 0;
    num pos0 = vector_num_read(&type2datapos,type);
    num POS0 = vector_num_read(&type2datapos,TYPE);
    know(POS1-POS0 == pos1-pos0);
    for (num i = 0;i < pos1-1-pos0;++i) {
      num subtype = vector_num_read(&typedata,pos0+i);
      num SUBTYPE = vector_num_read(&typedata,POS0+i);
      if (!type_tyvarnames_subst_is(subtype,SUBTYPE,abstype,numtyvars,tyvarnames,split))
        return 0;
    }
    return 1;
  }

  know(tag == 'a');
  const char *t = tyvarnames;
  for (num i = 0;i < numtyvars;++i) {
    if (type_is_tyvarnamed(type,t,split)) {
      // e.g. tyvars are A B C
      // and we've found that type matches B
      // so now want to check that TYPE matches second position in abstype
      know(type2tag(abstype) == 'b');
      num pos0 = vector_num_read(&type2datapos,abstype);
      num pos1 = vector_num_read(&type2datapos,abstype+1);
      know(pos1-pos0 == numtyvars+1);
      num abstypei = vector_num_read(&typedata,pos0+i);
      return type_is(TYPE,abstypei);
    }
    while (*t != split) ++t;
    ++t;
  }

  // type is tyvar not in tyvars
  // so look for exact match
  return type_is(type,TYPE);
}

static int type_subst_is(vector_num *from,vector_num *to,num type,num TYPE)
{
  char tag = type2tag(type);

  if (tag == 'b') {
    if (type2tag(TYPE) != 'b') return 0;
    num pos1 = vector_num_read(&type2datapos,type+1);
    num POS1 = vector_num_read(&type2datapos,TYPE+1);
    char *s = in_buf+vector_num_read(&typedata,pos1-1);
    char *S = in_buf+vector_num_read(&typedata,POS1-1);
    if (!name_is(s,S)) return 0;
    num pos0 = vector_num_read(&type2datapos,type);
    num POS0 = vector_num_read(&type2datapos,TYPE);
    know(POS1-POS0 == pos1-pos0);
    for (num i = 0;i < pos1-1-pos0;++i) {
      num subtype = vector_num_read(&typedata,pos0+i);
      num SUBTYPE = vector_num_read(&typedata,POS0+i);
      if (!type_subst_is(from,to,subtype,SUBTYPE))
        return 0;
    }
    return 1;
  }

  know(tag == 'a');
  num len = vector_num_len(from);
  know(len == vector_num_len(to));
  for (num i = 0;i < len;++i)
    if (type_is(type,vector_num_read(from,i)))
      return type_is(TYPE,vector_num_read(to,i));

  return type_is(type,TYPE);
}

static int type_substboth_is(vector_num *from,vector_num *to,num type,num TYPE)
{
  char tag = type2tag(type);
  char TAG = type2tag(TYPE);

  if (tag == 'a') {
    num len = vector_num_len(from);
    know(len == vector_num_len(to));
    for (num i = 0;i < len;++i)
      if (type_is(type,vector_num_read(from,i))) {
        type = vector_num_read(to,i);
        break;
      }
    return type_subst_is(from,to,TYPE,type);
  }
  if (TAG == 'a') {
    num len = vector_num_len(from);
    know(len == vector_num_len(to));
    for (num i = 0;i < len;++i)
      if (type_is(TYPE,vector_num_read(from,i))) {
        TYPE = vector_num_read(to,i);
        break;
      }
    return type_subst_is(from,to,type,TYPE);
  }

  know(tag == 'b');
  know(TAG == 'b');

  num pos1 = vector_num_read(&type2datapos,type+1);
  num POS1 = vector_num_read(&type2datapos,TYPE+1);
  char *s = in_buf+vector_num_read(&typedata,pos1-1);
  char *S = in_buf+vector_num_read(&typedata,POS1-1);
  if (!name_is(s,S)) return 0;
  num pos0 = vector_num_read(&type2datapos,type);
  num POS0 = vector_num_read(&type2datapos,TYPE);
  know(POS1-POS0 == pos1-pos0);
  for (num i = 0;i < pos1-1-pos0;++i) {
    num subtype = vector_num_read(&typedata,pos0+i);
    num SUBTYPE = vector_num_read(&typedata,POS0+i);
    if (!type_substboth_is(from,to,subtype,SUBTYPE))
      return 0;
  }
  return 1;
}

// XXX simplicity: maybe merge with type_subst_is
static int type_find_subst_append(vector_num *from,vector_num *to,num type,num TYPE)
{
  char tag = type2tag(type);

  if (tag == 'b') {
    if (type2tag(TYPE) != 'b') return 0;
    num pos1 = vector_num_read(&type2datapos,type+1);
    num POS1 = vector_num_read(&type2datapos,TYPE+1);
    char *s = in_buf+vector_num_read(&typedata,pos1-1);
    char *S = in_buf+vector_num_read(&typedata,POS1-1);
    if (!name_is(s,S)) return 0;
    num pos0 = vector_num_read(&type2datapos,type);
    num POS0 = vector_num_read(&type2datapos,TYPE);
    know(POS1-POS0 == pos1-pos0);
    for (num i = 0;i < pos1-1-pos0;++i) {
      num subtype = vector_num_read(&typedata,pos0+i);
      num SUBTYPE = vector_num_read(&typedata,POS0+i);
      if (!type_find_subst_append(from,to,subtype,SUBTYPE))
        return 0;
    }
    return 1;
  }

  know(tag == 'a');
  num len = vector_num_len(from);
  know(len == vector_num_len(to));
  for (num i = 0;i < len;++i)
    if (type_is(type,vector_num_read(from,i)))
      return type_is(TYPE,vector_num_read(to,i));

  vector_num_append(from,type);
  vector_num_append(to,TYPE);
  return 1;
}

// 1 if TYPE is result of some substitution into type
static int type_some_subst_is(num type,num TYPE)
{
  static vector_num from;
  static vector_num to;

  vector_num_empty(&from);
  vector_num_empty(&to);
  if (!type_find_subst_append(&from,&to,type,TYPE)) return 0;

  num len = vector_num_len(&from);
  know(type_find_subst_append(&from,&to,type,TYPE));
  know(len == vector_num_len(&from));
  return 1;
}

// XXX simplicity: could merge with general const pattern matching
static int type_is_equality(num type)
{
  num from,to,tofrom,toto;
  if (!type_is_fun(type,&from,&to)) return 0;
  if (!type_is_fun(to,&tofrom,&toto)) return 0;
  if (!type_is(from,tofrom)) return 0;
  return type_is_bool(toto);
}

// XXX simplicity: could merge with general const pattern matching
static int type_is_choice(num type)
{
  num from,to,fromfrom,fromto;
  if (!type_is_fun(type,&from,&to)) return 0;
  if (!type_is_fun(from,&fromfrom,&fromto)) return 0;
  if (!type_is(fromfrom,to)) return 0;
  return type_is_bool(fromto);
}

// accumulates unique tyvars in result (not necessarily sorted)
// on top of any existing tyvars
// each tyvar represented as an index within in_buf
// and uniqueness being determined by type_is
static void type_vars_append(vector_num *result,num type)
{
  char tag = type2tag(type);

  if (tag == 'a') {
    for (num i = 0;i < vector_num_len(result);++i)
      if (type_is(vector_num_read(result,i),type))
        return;
    vector_num_append(result,type);
    return;
  }
  
  know(tag == 'b');
  num pos0 = vector_num_read(&type2datapos,type);
  num pos1 = vector_num_read(&type2datapos,type+1);
  for (num i = pos0;i < pos1-1;++i)
    type_vars_append(result,vector_num_read(&typedata,i));
}

static void type_vars(vector_num *result,num type)
{
  vector_num_empty(result);
  type_vars_append(result,type);
}

// ===== term operations

static num term2type(num term)
{
  return vector_num_read(&termdata,vector_num_read(&term2datapos,term));
}

static int term_is_const(num term,num *type,const char **name)
{
  if (term2tag(term) != 'c') return 0;
  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 2);
  if (type) *type = vector_num_read(&termdata,pos0);
  if (name) *name = in_buf+vector_num_read(&termdata,pos0+1);
  return 1;
}

static int term_is_var(num term,num *type,const char **name)
{
  if (term2tag(term) != 'd') return 0;
  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 2);
  if (type) *type = vector_num_read(&termdata,pos0);
  if (name) *name = in_buf+vector_num_read(&termdata,pos0+1);
  return 1;
}

static int term_is_comb(num term,num *type,num *funterm,num *valueterm)
{
  if (term2tag(term) != 'e') return 0;
  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 3);
  if (type) *type = vector_num_read(&termdata,pos0);
  if (funterm) *funterm = vector_num_read(&termdata,pos0+1);
  if (valueterm) *valueterm = vector_num_read(&termdata,pos0+2);
  return 1;
}

static int term_is_abs(num term,num *type,num *fromterm,num *toterm)
{
  if (term2tag(term) != 'f') return 0;
  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 3);
  if (type) *type = vector_num_read(&termdata,pos0);
  if (fromterm) *fromterm = vector_num_read(&termdata,pos0+1);
  if (toterm) *toterm = vector_num_read(&termdata,pos0+2);
  return 1;
}

static int term_is(num term,num TERM)
{
  if (term == TERM) return 1;
  if (vector_num_read(&term2hash,term) != vector_num_read(&term2hash,TERM)) return 0;
  char tag = term2tag(term);
  char TAG = term2tag(TERM);
  if (TAG != tag) return 0;
  num pos0 = vector_num_read(&term2datapos,term);
  num POS0 = vector_num_read(&term2datapos,TERM);
  num type = vector_num_read(&termdata,pos0);
  num TYPE = vector_num_read(&termdata,POS0);
  if (TYPE != type) return 0;
  num pos1 = vector_num_read(&term2datapos,term+1);
  num POS1 = vector_num_read(&term2datapos,TERM+1);
  if (tag == 'c' || tag == 'd') {
    know(pos1-pos0 == 2);
    know(POS1-POS0 == 2);
    const char *name = in_buf+vector_num_read(&termdata,pos0+1);
    const char *NAME = in_buf+vector_num_read(&termdata,POS0+1);
    return name_is(name,NAME);
  }
  know(pos1-pos0 == 3);
  num subterm0 = vector_num_read(&termdata,pos0+1);
  num SUBTERM0 = vector_num_read(&termdata,POS0+1);
  if (!term_is(subterm0,SUBTERM0)) return 0;
  num subterm1 = vector_num_read(&termdata,pos0+2);
  num SUBTERM1 = vector_num_read(&termdata,POS0+2);
  if (!term_is(subterm1,SUBTERM1)) return 0;
  return 1;
}

// should match ordav in hol-light/fusion.ml
// which is orda when t,u are each variables
// caller here guarantees that t,u are variables
static int term_alphaorder_cmp_vars(num t,num u,vector_num *L)
{
  if (t == u) return 0;

  num lenL = vector_num_len(L);
  for (num i = 2*(lenL/2)-2;i >= 0;i -= 2) {
    num v = vector_num_read(L,i);
    num w = vector_num_read(L,i+1);
    if (term_is(t,v)) return term_is(u,w) ? 0 : -1;
    if (term_is(u,w)) return 1;
  }

  num tpos = vector_num_read(&term2datapos,t);
  const char *tname = in_buf+vector_num_read(&termdata,tpos+1);
  num upos = vector_num_read(&term2datapos,u);
  const char *uname = in_buf+vector_num_read(&termdata,upos+1);

  return name_cmp(tname,uname);
}

// can adjust L while running but restores it
static int term_alphaorder_cmp_recursive(num t,num u,vector_num *L)
{
  if (t == u) return 0;

  char ttag = term2tag(t);
  char utag = term2tag(u);

  if (ttag > utag) return 1;
  if (ttag < utag) return -1;

  if (ttag == 'd')
    return term_alphaorder_cmp_vars(t,u,L);
  if (ttag == 'c') {
    num tpos = vector_num_read(&term2datapos,t);
    num upos = vector_num_read(&term2datapos,u);
    const char *tname = in_buf+vector_num_read(&termdata,tpos+1);
    const char *uname = in_buf+vector_num_read(&termdata,upos+1);
    int result = name_cmp(tname,uname);
    if (result) return result;
    num ttype = vector_num_read(&termdata,tpos);
    num utype = vector_num_read(&termdata,upos);
    return type_cmp(ttype,utype);
  }
  if (ttag == 'e') {
    num tpos = vector_num_read(&term2datapos,t);
    num upos = vector_num_read(&term2datapos,u);
    num tfun = vector_num_read(&termdata,tpos+1);
    num ufun = vector_num_read(&termdata,upos+1);
    int result = term_alphaorder_cmp_recursive(tfun,ufun,L);
    if (result) return result;
    num tpoint = vector_num_read(&termdata,tpos+2);
    num upoint = vector_num_read(&termdata,upos+2);
    return term_alphaorder_cmp_recursive(tpoint,upoint,L);
  }

  num tfrom,tto;
  num ufrom,uto;
  know(term_is_abs(t,0,&tfrom,&tto));
  know(term_is_abs(u,0,&ufrom,&uto));

  num tfromtype,ufromtype;
  know(term_is_var(tfrom,&tfromtype,0));
  know(term_is_var(ufrom,&ufromtype,0));
  int result = type_cmp(tfromtype,ufromtype);
  if (result) return result;

  num lenL = vector_num_len(L);
  vector_num_append(L,tfrom);
  vector_num_append(L,ufrom);
  result = term_alphaorder_cmp_recursive(tto,uto,L);
  vector_num_trunc(L,lenL);
  return result;
}

// accumulates unique tyvars in result (not necessarily sorted)
// on top of any existing tyvars
static void term_tyvars_append(vector_num *result,num term)
{
  char tag = term2tag(term);

  if (tag == 'c' || tag == 'd') {
    num pos0 = vector_num_read(&term2datapos,term);
    num pos1 = vector_num_read(&term2datapos,term+1);
    know(pos1-pos0 == 2);
    type_vars_append(result,vector_num_read(&termdata,pos0));
    return;
  }

  know(tag == 'e' || tag == 'f');
  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 3);
  num term0 = vector_num_read(&termdata,pos0+1);
  num term1 = vector_num_read(&termdata,pos0+2);
  term_tyvars_append(result,term0);
  term_tyvars_append(result,term1);
  // note: could also scan type
  // but this would be redundant for both e and f
}

static void term_tyvars(vector_num *result,num term)
{
  vector_num_empty(result);
  term_tyvars_append(result,term);
}

static int term_is_eqsymbol(num term)
{
  const char *name;
  if (!term_is_const(term,0,&name)) return 0;
  return name_is(name,"=\n");
}

static int term_is_equality(num term,num *left,num *right)
{
  num funterm,funfunterm;
  if (!term_is_comb(term,0,&funterm,right)) return 0;
  if (!term_is_comb(funterm,0,&funfunterm,left)) return 0;
  if (!term_is_eqsymbol(funfunterm)) return 0;
  return 1;
}

static int term_alphaorder_cmp(num t,num u)
{
  static vector_num tmp;
  know(vector_num_len(&tmp) == 0);
  return term_alphaorder_cmp_recursive(t,u,&tmp);
}

static int term_alphaequivalent(num t,num u)
{
  static vector_num tmp;
  know(vector_num_len(&tmp) == 0);
  return term_alphaorder_cmp_recursive(t,u,&tmp) == 0;
}

static void term_freevars_append(vector_num *result,num term)
{
  num origlen = vector_num_len(result);
  num len = vector_num_read(&term2freelen,term);
  num pos = vector_num_read(&term2freepos,term);
  for (num i = 0;i < len;++i) {
    num v = vector_num_read(&termfrees,pos+i);
    int found = 0;
    for (num j = 0;j < origlen;++j)
      if (term_is(v,vector_num_read(result,j))) {
        found = 1;
        break;
      }
    if (!found)
      vector_num_append(result,vector_num_read(&termfrees,pos+i));
  }
}

static void term_freevars(vector_num *result,num term)
{
  vector_num_empty(result);
  num len = vector_num_read(&term2freelen,term);
  num pos = vector_num_read(&term2freepos,term);
  for (num i = 0;i < len;++i)
    vector_num_append(result,vector_num_read(&termfrees,pos+i));
}

static int term_has_freevars(num term)
{
  return vector_num_read(&term2freelen,term) > 0;
}

// 1 if v''' is a free variable in term
static int term_has_free(num term,num v,num primes)
{
  num vtype;
  const char *vname;
  if (!term_is_var(v,&vtype,&vname)) return 0;

  num len = vector_num_read(&term2freelen,term);
  num pos = vector_num_read(&term2freepos,term);
  for (num i = 0;i < len;++i) {
    num w = vector_num_read(&termfrees,pos+i);
    num wtype;
    const char *wname;
    know(term_is_var(w,&wtype,&wname));
    if (type_is(wtype,vtype))
      if (nameprimes_is(wname,0,vname,primes))
        return 1;
  }
  return 0;
}

// later entries override earlier entries
// return value -1 means not found _or_ found -1
static int term_map(vector_num *from,vector_num *to,num term)
{
  num i = vector_num_len(from);
  while (i-- > 0) {
    num fromi = vector_num_read(from,i);
    if (term_is(fromi,term))
      return vector_num_read(to,i);
  }
  return -1;
}

static int term_subst_obvious_id(num term,vector_num *from,vector_num *to)
{
  num len = vector_num_read(&term2freelen,term);
  num pos = vector_num_read(&term2freepos,term);
  for (num i = 0;i < len;++i) {
    num w = vector_num_read(&termfrees,pos+i);
    if (term_map(from,to,w) >= 0) return 0;
  }
  return 1;
}

// 1 if substituting from->to+primed in term gives TERM
// should match subst in fusion.ml (but algorithm is different)
// primed[j]!=0 implies primed[j]>=0 and to[j] is a variable
static int term_subst_is(num term,vector_num *from,vector_num *to,vector_num *primed,num TERM)
{
  if (term_subst_obvious_id(term,from,to))
    return term_is(term,TERM);

  char tag = term2tag(term);

  know(tag != 'c');

  if (tag == 'd') {
    num m = term_map(from,to,term);
    num mprimes = term_map(from,primed,term);
    know(m >= 0);
    know(mprimes >= 0);
    if (mprimes == 0) return term_is(m,TERM);
    // now m+mprimes is a variable
    // want to check if same variable as TERM
    num TERMtype;
    const char *TERMname;
    if (!term_is_var(TERM,&TERMtype,&TERMname)) return 0;
    num mtype;
    const char *mname;
    know(term_is_var(m,&mtype,&mname));
    if (!type_is(TERMtype,mtype)) return 0;
    return nameprimes_is(TERMname,0,mname,mprimes);
  }

  if (term2tag(TERM) != tag) return 0;

  num pos0 = vector_num_read(&term2datapos,term);
  num pos1 = vector_num_read(&term2datapos,term+1);
  know(pos1-pos0 == 3);
  num term0 = vector_num_read(&termdata,pos0+1);
  num term1 = vector_num_read(&termdata,pos0+2);

  if (tag == 'e') {
    num POS0 = vector_num_read(&term2datapos,TERM);
    num POS1 = vector_num_read(&term2datapos,TERM+1);
    know(POS1-POS0 == 3);
    num TERM0 = vector_num_read(&termdata,POS0+1);
    num TERM1 = vector_num_read(&termdata,POS0+2);
    if (!term_subst_is(term0,from,to,primed,TERM0)) return 0;
    if (!term_subst_is(term1,from,to,primed,TERM1)) return 0;
    return 1;
  }

  know(tag == 'f');

  num v = term0;

  num vtype;
  const char *vname;
  know(term_is_var(v,&vtype,&vname));

  num len = vector_num_len(from);
  know(len == vector_num_len(to));
  know(len == vector_num_len(primed));

  for (num vprimes = 0;;++vprimes) {
    if (vprimes >= CUTOFF) reject("too many primes");

    // have v |-> term1
    // considering rewriting as subst(v) |-> subst(term1)
    // where subst replaces v with v'''
    // where number of primes is vprimes
    // and subst replaces other vars as per from->to

    int ok = 1;
    // goal: set ok to 0 if v''' has a problem

    // original algorithm determines problem as follows:
    // * first try vprimes = 0
    //   problem is then: some subst x->m with x!=v has x free in term1 and v free in m
    // * if problem, move on to larger vprimes
    // * for vprimes>0, define problem as:
    //   v''' free in origsubst(term1)
    //   where origsubst is from->to ignoring v

    // there are really three cases for the v''' problem:
    // * if v is free in term1: stays as v
    //   so no match for vprimes>0
    //   (and this also can be ignored for vprimes=0)
    // * if x!=v is free in term1 and x->m:
    //   frees(origsubst(term1)) includes frees(m)
    //   so problem if v''' free in m
    //   (which is also a test we want for vprimes=0)
    // * if f!=v is free in term1 and f not mapped from->to:
    //   frees(origsubst(term1)) includes f
    //   so problem if v''' free in f (i.e., v''' = f)

    // in other words, for each f free in term1:
    // * if f=v: no problem
    // * else if f->m: problem if v''' free in m
    // * else: problem if v''' free in f

    num freelen = vector_num_read(&term2freelen,term1);
    num freepos = vector_num_read(&term2freepos,term1);

    for (num i = 0;i < freelen;++i) {
      num f = vector_num_read(&termfrees,freepos+i);
      if (term_is(f,v)) continue;
      num m = term_map(from,to,f);
      num mprimes = term_map(from,primed,f);
      if (m < 0) { m = f; mprimes = 0; }
      // is v+vprimes free in m+mprimes?
      if (mprimes == 0) {
        if (!term_has_free(m,v,vprimes)) continue;
      } else { // both v and m are now variables
        know(mprimes > 0);
        num mtype;
        const char *mname;
        know(term_is_var(m,&mtype,&mname));
        if (!type_is(vtype,mtype)) continue;
        if (!nameprimes_is(vname,vprimes,mname,mprimes)) continue;
      }
      ok = 0;
      break;
    }
    if (ok) {
      vector_num_append(from,v);
      vector_num_append(to,v);
      vector_num_append(primed,vprimes);

      num POS0 = vector_num_read(&term2datapos,TERM);
      num POS1 = vector_num_read(&term2datapos,TERM+1);
      know(POS1-POS0 == 3);
      num TERM1 = vector_num_read(&termdata,POS0+2);
      int result = term_subst_is(term1,from,to,primed,TERM1);

      vector_num_trunc(from,len);
      vector_num_trunc(to,len);
      vector_num_trunc(primed,len);
      return result;
    }
  }
}

// 1 if substituting tyfrom->tyto and varfrom->varto in term gives TERM
// note: if variable is handled by varfrom->varto, ignore tyfrom->tyto
// should match inst in fusion.ml (but algorithm is different)
static int term_tyvar_subst_is_recursive(num term,vector_num *tyfrom,vector_num *tyto,vector_num *varfrom,vector_num *varto,num TERM)
{
  char tag = term2tag(term);
  if (term2tag(TERM) != tag) return 0;

  if (tag == 'c') {
    num termtype;
    num TERMtype;
    const char *termname;
    const char *TERMname;
    know(term_is_const(term,&termtype,&termname));
    know(term_is_const(TERM,&TERMtype,&TERMname));
    if (!name_is(termname,TERMname)) return 0;
    return type_subst_is(tyfrom,tyto,termtype,TERMtype);
  }

  if (tag == 'd') {
    num m = term_map(varfrom,varto,term);
    if (m >= 0) return term_is(m,TERM);

    num termtype;
    num TERMtype;
    const char *termname;
    const char *TERMname;
    know(term_is_var(term,&termtype,&termname));
    know(term_is_var(TERM,&TERMtype,&TERMname));
    if (!name_is(termname,TERMname)) return 0;
    return type_subst_is(tyfrom,tyto,termtype,TERMtype);
  }

  if (tag == 'e') {
    num termfun,termpoint;
    know(term_is_comb(term,0,&termfun,&termpoint));
    num TERMfun,TERMpoint;
    know(term_is_comb(TERM,0,&TERMfun,&TERMpoint));
    if (!term_tyvar_subst_is_recursive(termfun,tyfrom,tyto,varfrom,varto,TERMfun)) return 0;
    return term_tyvar_subst_is_recursive(termpoint,tyfrom,tyto,varfrom,varto,TERMpoint);
  }

  num varlen = vector_num_len(varfrom);
  know(varlen == vector_num_len(varto));
  int result = 0;

  num v,tterm;
  know(term_is_abs(term,0,&v,&tterm));
  num vtype;
  const char *vname;
  know(term_is_var(v,&vtype,&vname));

  // at this point v is no longer renamed
  // so could mark (v,-1) in (varfrom,varto) at this point
  // (if v is already in varfrom)
  // instead: be careful to override v in varfrom lookups below

  num V,TTERM;
  know(term_is_abs(TERM,0,&V,&TTERM));
  num Vtype;
  const char *Vname;
  know(term_is_var(V,&Vtype,&Vname));

  // variable capture at this level means:
  //   subst(v) matches subst(f) for some f free in tterm
  //   without f being v
  // then have to rename v as v''' for some number of primes

  num freelen = vector_num_read(&term2freelen,tterm);
  num freepos = vector_num_read(&term2freepos,tterm);

  num wprimes;
  for (wprimes = 0;;++wprimes) {
    if (wprimes >= CUTOFF) reject("too many primes");

    // considering v''' as replacement for v
    // (or no replacement if wprimes == 0)
    // does subst(v''') match subst(f) for some free f != v?

    int collision = 0;
    for (num i = 0;i < freelen;++i) {
      num f = vector_num_read(&termfrees,freepos+i);
      if (term_is(f,v)) continue;

      // does subst(v''') match subst(f)?

      num m = term_map(varfrom,varto,f);
      if (m >= 0) {
        // f is in varfrom, so being renamed
        // now want to know:
        // does subst(v''') match m?
        num mtype;
        const char *mname;
        know(term_is_var(m,&mtype,&mname));
        if (nameprimes_is(mname,0,vname,wprimes))
          if (type_subst_is(tyfrom,tyto,vtype,mtype)) {
            collision = 1;
            break;
          }
      } else {
        // f is not in varfrom, so just do tyfrom->tyto
        num ftype;
        const char *fname;
        know(term_is_var(f,&ftype,&fname));
        if (nameprimes_is(fname,0,vname,wprimes))
          if (type_substboth_is(tyfrom,tyto,vtype,ftype)) {
            collision = 1;
            break;
          }
      }
    }
    if (!collision) break;
  }

  if (!nameprimes_is(Vname,0,vname,wprimes)) goto done;
  if (!type_subst_is(tyfrom,tyto,vtype,Vtype)) goto done;

  if (wprimes > 0) {
    vector_num_append(varfrom,v);
    vector_num_append(varto,V);
  }

  result = term_tyvar_subst_is_recursive(tterm,tyfrom,tyto,varfrom,varto,TTERM);

  done:

  vector_num_trunc(varfrom,varlen);
  vector_num_trunc(varto,varlen);
  return result;
}

static int term_tyvar_subst_is(num term,vector_num *from,vector_num *to,num TERM)
{
  static vector_num varfrom;
  static vector_num varto;
  know(vector_num_len(&varfrom) == 0);
  know(vector_num_len(&varto) == 0);
  return term_tyvar_subst_is_recursive(term,from,to,&varfrom,&varto,TERM);
}

// ===== theorem operations

// see whether thmdata[start:stop] exactly matches h
static int hypotheses_match(num start,num stop,vector_num *h)
{
  if (vector_num_len(h) != stop-start) return 0;
  for (num i = start;i < stop;++i) {
    num hi = vector_num_read(h,i-start);
    if (!term_is(hi,vector_num_read(&thmdata,i))) return 0;
  }
  return 1;
}

// extract hypotheses from thmdata[start:stop]
// skipping terms alpha-equivalent to skip if skip>=0
static void hypotheses_extract(vector_num *result,num start,num stop,num skip)
{
  vector_num_empty(result);

  // XXX speed: can usually speed up alpha test with first-pass equality test
  // since we know thmdata[start:stop] are alpha-inequivalent

  for (num i = start;i < stop;++i) {
    num h = vector_num_read(&thmdata,i);
    if (skip >= 0 && term_alphaequivalent(h,skip)) continue;
    vector_num_append(result,h);
  }
}

// same as hypotheses_extract but taking theorem as input
static void hypotheses_extract_th(vector_num *result,num th,num skip)
{
  num start = vector_num_read(&thm2datapos,th);
  num stop = vector_num_read(&thm2datapos,th+1);
  hypotheses_extract(result,start,stop,skip);
}

// merge modulo alpha-equivalence
static void hypotheses_merge(vector_num *result,vector_num *h,vector_num *H)
{
  vector_num_empty(result);

  num hlen = vector_num_len(h);
  num Hlen = vector_num_len(H);
  num i = 0;
  num I = 0;

  for (;;) {
    if (i == hlen) {
      while (I < Hlen) vector_num_append(result,vector_num_read(H,I++));
      return;
    }
    if (I == Hlen) {
      while (i < hlen) vector_num_append(result,vector_num_read(h,i++));
      return;
    }
    num hi = vector_num_read(h,i);
    num HI = vector_num_read(H,I);
    int order = term_alphaorder_cmp(hi,HI);
    vector_num_append(result,(order <= 0 ? hi : HI));
    i += (order <= 0);
    I += (order >= 0);
  }
}

static int hypotheses_aremerged(num start,num stop,num th,num TH,num thskip,num THskip)
{
  static vector_num h;
  static vector_num H;
  static vector_num result;
  hypotheses_extract_th(&h,th,thskip);
  hypotheses_extract_th(&H,TH,THskip);
  hypotheses_merge(&result,&h,&H);
  return hypotheses_match(start,stop,&result);
}

static int hypotheses_arecopied(num start,num stop,num th)
{
  static vector_num h;
  hypotheses_extract_th(&h,th,-1);
  return hypotheses_match(start,stop,&h);
}

// ===== type tags

static void tag_a(const char *s) // Tyvar
{
  noteol(s);
  vector_num_append(&typedata,s-in_buf);
  vector_num_append(&type2hash,name_hash(s));
}

static void tag_b(const char *s) // Tyapp
{
  num arity = subid(&s,-1);
  num hash = hash_mix(7152249725402530200+arity);
  for (num i = 0;i < arity;++i) {
    num subtype = subid(&s,typeid);
    vector_num_append(&typedata,subtype);
    hash = hash_mix(hash+vector_num_read(&type2hash,subtype));
  }
  noteol(s);
  hash = hash_mix(hash+name_hash(s));
  vector_num_append(&typedata,s-in_buf);
  vector_num_append(&type2hash,hash);

  num expectedarity = app2arity(s);
  if (expectedarity < 0) reject("undefined app name");
  if (expectedarity != arity) reject("wrong number of app arguments");
}

// ===== term tags

static void tag_c(const char *s) // Const
{
  num type = subid(&s,typeid);
  noteol(s);

  num hash = 1260898140613410013LL;
  hash = hash_mix(hash+vector_num_read(&type2hash,type));
  hash = hash_mix(hash+name_hash(s));

  vector_num_append(&termdata,type);
  vector_num_append(&termdata,s-in_buf);
  vector_num_append(&term2freelen,0);
  vector_num_append(&term2freepos,0);
  vector_num_append(&term2hash,hash);

  if (name_is(s,"=\n")) {
    if (!type_is_equality(type)) reject("non-equality type");
    return;
  }

  if (name_is(s,"@\n")) {
    if (!type_is_choice(type)) reject("non-choice type");
    return;
  }

  num registeredtype = const2type(s);
  if (registeredtype >= 0) {
    if (!type_some_subst_is(registeredtype,type)) reject("const type mismatch");
    return;
  }

  // XXX simplicity: merge the absname/repname code segments

  num registeredtypedef = absname2typedef(s);
  if (registeredtypedef >= 0) {
    num from,to;
    if (!type_is_fun(type,&from,&to)) reject("non-function type with typedef name");

    char split = vector_char_read(&typedef2split,registeredtypedef);
    num reptype = vector_num_read(&typedef2reptype,registeredtypedef);
    num numtyvars = vector_num_read(&typedef2numtyvars,registeredtypedef);
    const char *abstypename = in_buf+vector_num_read(&typedef2abstypename,registeredtypedef);
    const char *absname = in_buf+vector_num_read(&typedef2absname,registeredtypedef);
    const char *tyvarnames = in_buf+vector_num_read(&typedef2tyvarnames,registeredtypedef);

    know(name_is_withsplit(s,absname,split));

    // expecting: absname:reptype->abstype
    // modulo substitution for tyvars
    if (!type_is_appnamed(to,abstypename,split)) reject("typedef absname-abstype mismatch");

    if (!type_tyvarnames_subst_is(reptype,from,to,numtyvars,tyvarnames,split)) reject("typedef absname-reptype mismatch");
    return;
  }

  registeredtypedef = repname2typedef(s);
  if (registeredtypedef >= 0) {
    num from,to;
    if (!type_is_fun(type,&from,&to)) reject("non-function type with typedef name");

    char split = vector_char_read(&typedef2split,registeredtypedef);
    num reptype = vector_num_read(&typedef2reptype,registeredtypedef);
    num numtyvars = vector_num_read(&typedef2numtyvars,registeredtypedef);
    const char *abstypename = in_buf+vector_num_read(&typedef2abstypename,registeredtypedef);
    const char *repname = in_buf+vector_num_read(&typedef2repname,registeredtypedef);
    const char *tyvarnames = in_buf+vector_num_read(&typedef2tyvarnames,registeredtypedef);

    know(name_is_withsplit(s,repname,split));

    // expecting: repname:abstype->reptype
    // modulo substitution for tyvars
    if (!type_is_appnamed(from,abstypename,split)) reject("typedef repname-abstype mismatch");

    if (!type_tyvarnames_subst_is(reptype,to,from,numtyvars,tyvarnames,split)) reject("typedef repname-reptype mismatch");
    return;
  }

  reject("undefined constant");
}

static void tag_d(const char *s) // Var
{
  num type = subid(&s,typeid);
  noteol(s);

  num hash = 5725918395758143510LL;
  hash = hash_mix(hash+vector_num_read(&type2hash,type));
  hash = hash_mix(hash+name_hash(s));

  vector_num_append(&termdata,type);
  vector_num_append(&termdata,s-in_buf);
  vector_num_append(&term2freepos,vector_num_len(&termfrees));
  vector_num_append(&termfrees,termid);
  vector_num_append(&term2freelen,1);
  vector_num_append(&term2hash,hash);
}

static void tag_e(const char *s) // Comb
{
  num outputtype = subid(&s,typeid);
  num funterm = subid(&s,termid);
  num pointterm = subid(&s,termid);
  eol(s);

  vector_num_append(&termdata,outputtype);
  vector_num_append(&termdata,funterm);
  vector_num_append(&termdata,pointterm);

  num hash = 3679975592003923231LL;
  hash = hash_mix(hash+vector_num_read(&term2hash,funterm));
  hash = hash_mix(hash+vector_num_read(&term2hash,pointterm));

  if (!type_is_funfromto(term2type(funterm),term2type(pointterm),outputtype)) reject("combination mismatch");

  num pos,len;
  if (!term_has_freevars(funterm)) {
    // closed function; common case
    pos = vector_num_read(&term2freepos,pointterm);
    len = vector_num_read(&term2freelen,pointterm);
  } else {
    static vector_num frees;
    term_freevars(&frees,funterm);
    term_freevars_append(&frees,pointterm);
    pos = vector_num_len(&termfrees);
    len = vector_num_len(&frees);
    for (num i = 0;i < len;++i)
      vector_num_append(&termfrees,vector_num_read(&frees,i));
  }
  vector_num_append(&term2freepos,pos);
  vector_num_append(&term2freelen,len);
  vector_num_append(&term2hash,hash);
}

static void tag_f(const char *s) // Abs
{
  num outputtype = subid(&s,typeid);
  num fromterm = subid(&s,termid);
  num toterm = subid(&s,termid);
  eol(s);

  vector_num_append(&termdata,outputtype);
  vector_num_append(&termdata,fromterm);
  vector_num_append(&termdata,toterm);

  num hash = 4019844455831122549LL;
  hash = hash_mix(hash+vector_num_read(&term2hash,fromterm));
  hash = hash_mix(hash+vector_num_read(&term2hash,toterm));

  if (!term_is_var(fromterm,0,0)) reject("non-variable lambda");
  if (!type_is_funfromto(outputtype,term2type(fromterm),term2type(toterm))) reject("lambda mismatch");

  num pos = vector_num_read(&term2freepos,toterm);
  num len = vector_num_read(&term2freelen,toterm);

  for (num i = 0;i < len;++i) {
    num v = vector_num_read(&termfrees,pos+i);
    if (term_is(fromterm,v)) {
      num newpos = vector_num_len(&termfrees);
      num newlen = 0;
      for (num j = 0;j < len;++j)
        if (j != i) {
          vector_num_append(&termfrees,vector_num_read(&termfrees,pos+j));
          ++newlen;
        }
      pos = newpos;
      len = newlen;
      break;
    }
  }
    
  vector_num_append(&term2freepos,pos);
  vector_num_append(&term2freelen,len);
  vector_num_append(&term2hash,hash);
}

// ===== A: TYPE_DEFINITION
// (plus D for followup)

static vector_num tag_A_tyvars;

static void tag_A(const char *s)
{
  num reptype = subid(&s,typeid);
  num repprop = subid(&s,termid);
  num th = subid(&s,thmid);
  noteol(s);

  int state = 0;
  char split = 0;
  const char *abstypename = 0;
  const char *absname = 0;
  const char *repname = 0;
  const char *tyvarnames = 0;
  for (;*s != '\n';++s)
    switch(state) {
      case 0: split = *s; ++state; break;
      case 1: abstypename = s; ++state; // fall through
      case 2: if (*s == split) ++state; break;
      case 3: absname = s; ++state; // fall through
      case 4: if (*s == split) ++state; break;
      case 5: repname = s; ++state; // fall through
      case 6: if (*s == split) { ++state; tyvarnames = s+1; }
    }
  if (state != 7) reject("TYPE_DEFINITION: misformatted");
  if (split != ']') reject("TYPE_DEFINITION: refusing non-bracket");
  know(abstypename);
  know(absname);
  know(repname);
  know(tyvarnames);
  num numtyvarnames = 0;
  for (s = tyvarnames;*s != '\n';++s)
    if (*s == split)
      ++numtyvarnames;
  if (s[-1] != split) reject("TYPE_DEFINITION: partial final component");

  num thstart = vector_num_read(&thm2datapos,th);
  num thstop = vector_num_read(&thm2datapos,th+1);
  if (thstart != thstop) reject("TYPE_DEFINITION: input theorem has hypotheses");

  num thconclusion = vector_num_read(&thm2conclusion,th);

  num reppropcheck;
  num reppoint;
  if (!term_is_comb(thconclusion,0,&reppropcheck,&reppoint)) reject("TYPE_DEFINITION: input theorem is not a combination");
  if (!term_is(repprop,reppropcheck)) reject("TYPE_DEFINITION: repprop mismatch");
  if (!type_is(reptype,term2type(reppoint))) reject("TYPE_DEFINITION: reptype mismatch");

  if (term_has_freevars(repprop)) reject("TYPE_DEFINITION: free variables in repprop");

  term_tyvars(&tag_A_tyvars,repprop);
  if (vector_num_len(&tag_A_tyvars) != numtyvarnames) reject("TYPE_DEFINITION: wrong number of tyvars");

  const char *tyvarname = tyvarnames;
  num prevpos = -1;
  for (s = tyvarnames;*s != '\n';++s)
    if (*s == split) {
      num pos;
      for (pos = 0;pos < numtyvarnames;++pos) {
        num tyvar = vector_num_read(&tag_A_tyvars,pos);
        if (type_is_tyvarnamed(tyvar,tyvarname,split)) break;
      }
      if (pos >= numtyvarnames) reject("TYPE_DEFINITION: tyvar not in repprop");

      if (prevpos >= 0) {
        num tyvar = vector_num_read(&tag_A_tyvars,pos);
        num prevtyvar = vector_num_read(&tag_A_tyvars,prevpos);
        if (type_cmp(tyvar,prevtyvar) != 1) reject("TYPE_DEFINITION: tyvars not in increasing order");
      }

      prevpos = pos;
      tyvarname = s+1;
    }

  num typedefpos = vector_num_len(&typedef2reptype);

  app2arity_add(abstypename,split,numtyvarnames);
  absname2typedef_add(absname,split,typedefpos);
  repname2typedef_add(repname,split,typedefpos);

  vector_num_append(&typedef2reptype,reptype);
  vector_num_append(&typedef2repprop,repprop);
  vector_num_append(&typedef2numtyvars,numtyvarnames);
  vector_num_append(&typedef2abstypename,abstypename-in_buf);
  vector_num_append(&typedef2absname,absname-in_buf);
  vector_num_append(&typedef2repname,repname-in_buf);
  vector_num_append(&typedef2tyvarnames,tyvarnames-in_buf);
  vector_char_append(&typedef2split,split);
  vector_num_append(&typedef2infid,infid);
}

static void finish_A(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("TYPE_DEFINITION: hypotheses");

  num typedefpos = vector_num_len(&typedef2reptype)-1;
  know(typedefpos >= 0);
  know(typedefpos == vector_num_len(&typedef2numtyvars)-1);
  know(typedefpos == vector_num_len(&typedef2abstypename)-1);
  know(typedefpos == vector_num_len(&typedef2absname)-1);
  know(typedefpos == vector_num_len(&typedef2repname)-1);
  know(typedefpos == vector_num_len(&typedef2tyvarnames)-1);
  know(typedefpos == vector_char_len(&typedef2split)-1);

  num reptype = vector_num_read(&typedef2reptype,typedefpos);
  num numtyvars = vector_num_read(&typedef2numtyvars,typedefpos);
  const char *abstypename = in_buf+vector_num_read(&typedef2abstypename,typedefpos);
  const char *absname = in_buf+vector_num_read(&typedef2absname,typedefpos);
  const char *repname = in_buf+vector_num_read(&typedef2repname,typedefpos);
  const char *tyvarnames = in_buf+vector_num_read(&typedef2tyvarnames,typedefpos);
  char split = vector_char_read(&typedef2split,typedefpos);

  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("TYPE_DEFINITION: conclusion has operation mismatch");

  num abstype;
  const char *name;
  if (!term_is_var(right,&abstype,&name)) reject("TYPE_DEFINITION: right side of conclusion is not variable");

  if (!name_is(name,"a\n")) reject("TYPE_DEFINITION: refusing non-a variable name in conclusion");
  // now have: left = a; a:abstype

  num funterm;
  num pointterm;
  if (!term_is_comb(left,0,&funterm,&pointterm)) reject("TYPE_DEFINITION: left side of conclusion is not combination");
  // now have: funterm(pointterm) = a; a:abstype

  num pointfunterm;
  num pointpointterm;
  if (!term_is_comb(pointterm,0,&pointfunterm,&pointpointterm)) reject("TYPE_DEFINITION: left side of conclusion is not evaluation at combination");
  // now have: funterm(pointfunterm(pointpointterm)) = a; a:abstype

  if (!term_is(pointpointterm,right)) reject("TYPE_DEFINITION: variable mismatch");
  // now have: funterm(pointfunterm(a)) = a; a:abstype

  num funtype;
  const char *funname;
  if (!term_is_const(funterm,&funtype,&funname)) reject("TYPE_DEFINITION: outer function is not constant");
  if (!name_is_withsplit(funname,absname,split)) reject("TYPE_DEFINITION: absname mismatch");
  // now have: absname(pointfunterm(a)) = a; absname:funtype; a:abstype

  num pointfuntype;
  const char *pointfunname;
  if (!term_is_const(pointfunterm,&pointfuntype,&pointfunname)) reject("TYPE_DEFINITION: inner function is not constant");
  if (!name_is_withsplit(pointfunname,repname,split)) reject("TYPE_DEFINITION: repname mismatch");
  // now have: absname(repname(a)) = a; absname:funtype; repname:pointfuntype; a:abstype

  know(type_is_funfromto(funtype,reptype,abstype));
  know(type_is_funfromto(pointfuntype,abstype,reptype));
  // now have: absname(repname(a)) = a; absname:reptype->abstype; repname:abstype->reptype; a:abstype

  if (!type_is_abstype(abstype,abstypename,tyvarnames,numtyvars,split)) reject("TYPE_DEFINITION: abstype mismatch");
}

static num tag_D_pos;

static void tag_D(const char *s)
{
  tag_D_pos = subid(&s,typedefid);
  eol(s);
}

static void finish_D(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("TYPE_DEFINITION followup: hypotheses");

  num typedefpos = tag_D_pos;

  num reptype = vector_num_read(&typedef2reptype,typedefpos);
  num repprop = vector_num_read(&typedef2repprop,typedefpos);
  num numtyvars = vector_num_read(&typedef2numtyvars,typedefpos);
  const char *abstypename = in_buf+vector_num_read(&typedef2abstypename,typedefpos);
  const char *absname = in_buf+vector_num_read(&typedef2absname,typedefpos);
  const char *repname = in_buf+vector_num_read(&typedef2repname,typedefpos);
  const char *tyvarnames = in_buf+vector_num_read(&typedef2tyvarnames,typedefpos);
  char split = vector_char_read(&typedef2split,typedefpos);

  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("TYPE_DEFINITION followup: conclusion has operation mismatch");

  num funterm;
  num pointterm;
  if (!term_is_comb(left,0,&funterm,&pointterm)) reject("TYPE_DEFINITION followup: left side of conclusion is not combination");
  // now have: funterm(pointterm) = right

  if (!term_is(funterm,repprop)) reject("TYPE_DEFINITION followup: left side of conclusion is not repprop combination");
  // now have: repterm(pointterm) = right

  num reptypecheck;
  const char *name;
  if (!term_is_var(pointterm,&reptypecheck,&name)) reject("TYPE_DEFINITION followup: left side of conclusion is not repprop of variable");

  if (!name_is(name,"r\n")) reject("TYPE_DEFINITION followup: refusing non-r variable name in conclusion");
  if (!type_is(reptypecheck,reptype)) reject("TYPE_DEFINITION followup: reptype mismatch");
  // now have: repterm(r) = right; r:reptype

  num rightleft,rightright;
  if (!term_is_equality(right,&rightleft,&rightright)) reject("TYPE_DEFINITION followup: second-level operation mismatch");
  // now have: repterm(r) = (rightleft = rightright); r:reptype

  if (!term_is(rightright,pointterm)) reject("TYPE_DEFINITION followup: variable mismatch");
  // now have: repterm(r) = (rightleft = r); r:reptype

  num rightfun,rightpoint;
  if (!term_is_comb(rightleft,0,&rightfun,&rightpoint)) reject("TYPE_DEFINITION followup: second level is not combination");
  // now have: repterm(r) = (rightfun(rightpoint) = r); r:reptype

  num rightpointfun,rightpointpoint;
  if (!term_is_comb(rightpoint,0,&rightpointfun,&rightpointpoint)) reject("TYPE_DEFINITION followup: third level is not combination");
  // now have: repterm(r) = (rightfun(rightpointfun(rightpointpoint)) = r); r:reptype

  if (!term_is(rightpointpoint,pointterm)) reject("TYPE_DEFINITION followup: bottom-level variable mismatch");
  // now have: repterm(r) = (rightfun(rightpointfun(r)) = r); r:reptype

  num rightfuntype;
  const char *rightfunname;
  if (!term_is_const(rightfun,&rightfuntype,&rightfunname)) reject("TYPE_DEFINITION followup: outer function is not constant");
  if (!name_is_withsplit(rightfunname,repname,split)) reject("TYPE_DEFINITION followup: repname mismatch");
  // now have: repterm(r) = (repname(rightpointfun(r)) = r); r:reptype; repname:rightfuntype

  num rightpointfuntype;
  const char *rightpointfunname;
  if (!term_is_const(rightpointfun,&rightpointfuntype,&rightpointfunname)) reject("TYPE_DEFINITION followup: inner function is not constant");
  if (!name_is_withsplit(rightpointfunname,absname,split)) reject("TYPE_DEFINITION followup: absname mismatch");
  // now have: repterm(r) = (repname(absname(r)) = r); r:reptype; repname:rightfuntype; absname:rightpointfuntype

  num abstype,rightfunto;
  know(type_is_fun(rightfuntype,&abstype,&rightfunto));
  know(type_is(rightfunto,reptype));
  know(type_is_funfromto(rightpointfuntype,reptype,abstype));
  // now have: repterm(r) = (repname(absname(r)) = r); r:reptype; repname:abstype->reptype; absname:reptype->abstype

  if (!type_is_abstype(abstype,abstypename,tyvarnames,numtyvars,split)) reject("TYPE_DEFINITION followup: abstype mismatch");
}

// ==== B: BETA
// input: (x|->y)(x)
// output: (x|->y)(x) = y
static num tag_B_xyx;
static num tag_B_y;

static void tag_B(const char *s)
{
  num term = subid(&s,termid);
  eol(s);

  num funterm,pointterm;
  if (!term_is_comb(term,0,&funterm,&pointterm)) reject("BETA: operation mismatch");
  // now have: funterm(pointterm)

  if (!term_is_var(pointterm,0,0)) reject("BETA: combination is not with variable");
  // redundant given abs restrictions below, but keep for clarity

  num fromterm,toterm;
  if (!term_is_abs(funterm,0,&fromterm,&toterm)) reject("BETA: combination is not of abstraction");
  // now have: (fromterm|->toterm)(pointterm)

  if (!term_is(fromterm,pointterm)) reject("BETA: combination is not of same variable");
  // now have: (fromterm|->toterm)(fromterm)

  tag_B_xyx = term;
  tag_B_y = toterm;
}

static void finish_B(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("BETA: hypotheses");
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("BETA: operation mismatch");
  if (!term_is(left,tag_B_xyx)) reject("BETA: left-side mismatch");
  if (!term_is(right,tag_B_y)) reject("BETA: right-side mismatch");
}

// ===== C: DEFINITION

static vector_num tag_C_tyvars;
static vector_num tag_C_tyvarsright;
static const char *tag_C_name;
static num tag_C_type;
static num tag_C_defn;

static void tag_C(const char *s)
{
  num term = subid(&s,termid);
  noteol(s);

  num left,right;
  if (!term_is_equality(term,&left,&right)) reject("DEFINITION: operation mismatch");

  num type;
  const char *name;
  if (!term_is_var(left,&type,&name)) reject("DEFINITION: not a variable");
  if (!name_is(name,s)) reject("DEFINITION: name mismatch");

  if (term_has_freevars(right)) reject("DEFINITION: free variables on right side");

  type_vars(&tag_C_tyvars,type);

  term_tyvars(&tag_C_tyvarsright,right);

  for (num i = 0;i < vector_num_len(&tag_C_tyvarsright);++i) {
    num ty2 = vector_num_read(&tag_C_tyvarsright,i);
    int found = 0;
    for (num j = 0;j < vector_num_len(&tag_C_tyvars);++j) {
      num ty = vector_num_read(&tag_C_tyvars,j);
      if (type_is(ty,ty2)) {
        found = 1;
        break;
      }
    }
    if (!found) reject("DEFINITION: type variables on right side not included in constant");
  }

  const2type_add(name,'\n',type);

  tag_C_name = name;
  tag_C_type = type;
  tag_C_defn = right;
}

static void finish_C(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("DEFINITION: hypotheses");

  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("DEFINITION: operation mismatch");
  // now have: left = right

  num type;
  const char *name;
  if (!term_is_const(left,&type,&name)) reject("DEFINITION: left side is not constant");
  if (!name_is(name,tag_C_name)) reject("DEFINITION: name mismatch");
  if (!type_is(type,tag_C_type)) reject("DEFINITION: type mismatch");
  // now have: Const(tag_C_name,tag_C_type) = right

  if (!term_is(right,tag_C_defn)) reject("DEFINITION: right-side mismatch");
}

// ===== E: MK_COMB
// input: theorem thleft = thright
// input: theorem THleft = THright
// output: theorem thleft(THleft) = thright(THright)

static num tag_E_th;
static num tag_E_thleft;
static num tag_E_thright;
static num tag_E_TH;
static num tag_E_THleft;
static num tag_E_THright;

static void tag_E(const char *s)
{
  num th = subid(&s,thmid);
  num TH = subid(&s,thmid);
  eol(s);

  num thconclusion = vector_num_read(&thm2conclusion,th);
  num THconclusion = vector_num_read(&thm2conclusion,TH);

  num thleft,thright;
  if (!term_is_equality(thconclusion,&thleft,&thright)) reject("MK_COMB: first theorem is not equality");
  num THleft,THright;
  if (!term_is_equality(THconclusion,&THleft,&THright)) reject("MK_COMB: second theorem is not equality");

  num from;
  if (!type_is_fun(term2type(thleft),&from,0)) reject("first MK_COMB: type is not function");
  if (!type_is(term2type(THleft),from)) reject("MK_COMB: combination mismatch");

  tag_E_th = th;
  tag_E_thleft = thleft;
  tag_E_thright = thright;
  tag_E_TH = TH;
  tag_E_THleft = THleft;
  tag_E_THright = THright;
}

static void finish_E(num hypstart,num hypstop,num conclusion)
{
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("MK_COMB: operation mismatch");
  // now have: left = right

  num leftfun,leftpoint;
  if (!term_is_comb(left,0,&leftfun,&leftpoint)) reject("MK_COMB: left-side operation mismatch");
  // now have: leftfun(leftpoint) = right

  num rightfun,rightpoint;
  if (!term_is_comb(right,0,&rightfun,&rightpoint)) reject("MK_COMB: right-side operation mismatch");
  // now have: leftfun(leftpoint) = rightfun(rightpoint)

  if (!term_is(leftfun,tag_E_thleft)) reject("MK_COMB: left-outer mismatch");
  if (!term_is(leftpoint,tag_E_THleft)) reject("MK_COMB: left-inner mismatch");
  if (!term_is(rightfun,tag_E_thright)) reject("MK_COMB: right-outer mismatch");
  if (!term_is(rightpoint,tag_E_THright)) reject("MK_COMB: right-inner mismatch");

  if (!hypotheses_aremerged(hypstart,hypstop,tag_E_th,tag_E_TH,-1,-1)) reject("MK_COMB: hypothesis mismatch");
}

// ===== F: ABS
// input: variable v
// input: theorem l = r
// output: (v|->l) = (v|->r)

static num tag_F_var;
static num tag_F_th;
static num tag_F_left;
static num tag_F_right;

static vector_num tag_F_free;

static void tag_F(const char *s)
{
  num var = subid(&s,termid);
  num th = subid(&s,thmid);
  eol(s);

  if (!term_is_var(var,0,0)) reject("ABS: first input is not a variable");

  num thconclusion = vector_num_read(&thm2conclusion,th);
  num left,right;
  if (!term_is_equality(thconclusion,&left,&right)) reject("ABS: second input is not an equality");

  num thstart = vector_num_read(&thm2datapos,th);
  num thstop = vector_num_read(&thm2datapos,th+1);

  for (num i = thstart;i < thstop;++i) {
    num h = vector_num_read(&thmdata,i);

    term_freevars(&tag_F_free,h);

    for (num j = 0;j < vector_num_len(&tag_F_free);++j)
      if (term_is(var,vector_num_read(&tag_F_free,j)))
        reject("ABS variable is free in hypothesis");
  }

  tag_F_var = var;
  tag_F_th = th;
  tag_F_left = left;
  tag_F_right = right;
}

static void finish_F(num hypstart,num hypstop,num conclusion)
{
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("ABS: operation mismatch");
  // now have: left = right

  num leftv,leftt;
  if (!term_is_abs(left,0,&leftv,&leftt)) reject("ABS: left-side operation mismatch");
  // now have: (leftv|->leftt) = right

  num rightv,rightt;
  if (!term_is_abs(right,0,&rightv,&rightt)) reject("ABS: right-side operation mismatch");
  // now have: (leftv|->leftt) = (rightv|->rightt)

  if (!term_is(leftv,tag_F_var)) reject("ABS: left-side variable mismatch");
  if (!term_is(rightv,tag_F_var)) reject("ABS: right-side variable mismatch");
  if (!term_is(leftt,tag_F_left)) reject("ABS: left-side output mismatch");
  if (!term_is(rightt,tag_F_right)) reject("ABS: right-side output mismatch");
  // now have: (tag_F_var|->tag_F_left) = (tag_F_var|->tag_F_right)

  if (!hypotheses_arecopied(hypstart,hypstop,tag_F_th)) reject("ABS: hypothesis mismatch");
}

// ===== P: EQ_MP
// input: theorem L = R
// input: theorem L (modulo alpha-equivalence)
// output: theorem R

static num tag_P_right;
static num tag_P_th;
static num tag_P_TH;

static void tag_P(const char *s)
{
  num th = subid(&s,thmid);
  num TH = subid(&s,thmid);
  eol(s);

  num thconclusion = vector_num_read(&thm2conclusion,th);
  num THconclusion = vector_num_read(&thm2conclusion,TH);

  num left,right;
  if (!term_is_equality(thconclusion,&left,&right)) reject("EQ_MP: operation mismatch");

  if (!term_alphaequivalent(left,THconclusion)) reject("EQ_MP: left-side mismatch");
   
  tag_P_th = th;
  tag_P_TH = TH;
  tag_P_right = right;
}

static void finish_P(num hypstart,num hypstop,num conclusion)
{
  if (!term_is(conclusion,tag_P_right)) reject("EQ_MP: conclusion mismatch");
  if (!hypotheses_aremerged(hypstart,hypstop,tag_P_th,tag_P_TH,-1,-1)) reject("EQ_MP: hypothesis mismatch");
}

// ===== R: REFL

static num tag_R_term;

static void tag_R(const char *s)
{
  tag_R_term = subid(&s,termid);
  eol(s);
}

static void finish_R(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("REFL: hypotheses");
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("REFL: conclusion mismatch");
  if (!term_is(left,tag_R_term)) reject("REFL: left-side mismatch");
  if (!term_is(right,tag_R_term)) reject("REFL: right-side mismatch");
}

// ===== S: INST

static num tag_S_th;
static vector_num tag_S_from;
static vector_num tag_S_to;
static vector_num tag_S_primed;

static void tag_S(const char *s)
{
  tag_S_th = subid(&s,thmid);

  vector_num_empty(&tag_S_from);
  vector_num_empty(&tag_S_to);
  vector_num_empty(&tag_S_primed);
  for (;;) {
    if (*s == '\n') break;
    num from = subid(&s,termid);
    if (*s == '\n') reject("INST: odd number of term arguments");
    num to = subid(&s,termid);

    num fromtype;
    if (!term_is_var(from,&fromtype,0)) reject("INST: substituting for non-variable (note: S th from to, not S th to from)");
    if (!type_is(fromtype,term2type(to))) reject("INST: type mismatch");

    for (num i = 0;i < vector_num_len(&tag_S_from);++i)
      if (term_is(from,vector_num_read(&tag_S_from,i)))
        goto skip;

    vector_num_append(&tag_S_from,from);
    vector_num_append(&tag_S_to,to);
    vector_num_append(&tag_S_primed,0);
    skip: ;
  }
}

static num finish_S_hyptotal;

static void finish_S(num hypstart,num hypstop,num conclusion)
{
  finish_S_hyptotal += hypstop-hypstart;

  num th = tag_S_th;
  num thconclusion = vector_num_read(&thm2conclusion,th);

  if (!term_subst_is(thconclusion,&tag_S_from,&tag_S_to,&tag_S_primed,conclusion))
    reject("INST: conclusion mismatch");

  num thstart = vector_num_read(&thm2datapos,th);
  num thstop = vector_num_read(&thm2datapos,th+1);

  static vector_num hypused;
  vector_num_empty(&hypused);

  // XXX speed: maybe better to compute the map and sort
  // XXX completeness: also need this in case of alpha squeeze
  for (num i = thstart;i < thstop;++i) {
    num oldh = vector_num_read(&thmdata,i);
    int found = 0;
    for (num j = hypstart;j < hypstop;++j) {
      num newh = vector_num_read(&thmdata,j);
      if (term_subst_is(oldh,&tag_S_from,&tag_S_to,&tag_S_primed,newh)) {
        vector_num_write(&hypused,j-hypstart,1);
        found = 1;
        break;
      }
    }
    if (!found) reject("INST: hypothesis mismatch (maybe alpha squeeze?)");
  }

  if (vector_num_len(&hypused) != hypstop-hypstart) reject("INST: extra hypotheses");
  for (num j = hypstart;j < hypstop;++j)
    if (vector_num_read(&hypused,j-hypstart) != 1) reject("INST: extra hypotheses");
}

// ===== T: INST_TYPE

static num tag_T_th;
static vector_num tag_T_from;
static vector_num tag_T_to;

static void tag_T(const char *s)
{
  tag_T_th = subid(&s,thmid);

  vector_num_empty(&tag_T_from);
  vector_num_empty(&tag_T_to);
  for (;;) {
    if (*s == '\n') break;
    num from = subid(&s,typeid);
    if (*s == '\n') reject("INST_TYPE: odd number of type arguments");
    num to = subid(&s,typeid);

    if (type2tag(from) != 'a') reject("INST_TYPE: substituting for non-tyvar (note: T th from to, not T th to from)");

    for (num i = 0;i < vector_num_len(&tag_T_from);++i)
      if (type_is(from,vector_num_read(&tag_T_from,i)))
        goto skip;

    vector_num_append(&tag_T_from,from);
    vector_num_append(&tag_T_to,to);
    skip: ;
  }
}

num finish_T_hyptotal;

static void finish_T(num hypstart,num hypstop,num conclusion)
{
  finish_T_hyptotal += hypstop-hypstart;

  num th = tag_T_th;
  num thconclusion = vector_num_read(&thm2conclusion,th);

  if (!term_tyvar_subst_is(thconclusion,&tag_T_from,&tag_T_to,conclusion))
    reject("INST_TYPE: conclusion mismatch");

  num thstart = vector_num_read(&thm2datapos,th);
  num thstop = vector_num_read(&thm2datapos,th+1);

  static vector_num hypused;
  vector_num_empty(&hypused);

  // XXX speed: maybe better to compute the map and sort
  // XXX completeness: also need this in case of alpha squeeze
  for (num i = thstart;i < thstop;++i) {
    num oldh = vector_num_read(&thmdata,i);
    int found = 0;
    for (num j = hypstart;j < hypstop;++j) {
      num newh = vector_num_read(&thmdata,j);
      if (term_tyvar_subst_is(oldh,&tag_T_from,&tag_T_to,newh)) {
        vector_num_write(&hypused,j-hypstart,1);
        found = 1;
        break;
      }
    }
    if (!found) reject("INST_TYPE: hypothesis mismatch (maybe alpha squeeze?)");
  }

  if (vector_num_len(&hypused) != hypstop-hypstart) reject("INST_TYPE: extra hypotheses");
  for (num j = hypstart;j < hypstop;++j)
    if (vector_num_read(&hypused,j-hypstart) != 1) reject("INST_TYPE: extra hypotheses");
}

// ===== U: ASSUME

static num tag_U_term;

static void tag_U(const char *s)
{
  num term = subid(&s,termid);
  eol(s);

  if (!type_is_bool(term2type(term))) reject("ASSUME: non-bool input");

  tag_U_term = term;
}

static void finish_U(num hypstart,num hypstop,num conclusion)
{
  if (!term_is(conclusion,tag_U_term)) reject("ASSUME: wrong conclusion");
  if (hypstop-hypstart != 1) reject("ASSUME: wrong number of hypotheses");
  num h = vector_num_read(&thmdata,hypstart);
  if (!term_is(h,tag_U_term)) reject("ASSUME: wrong hypothesis");
}

// ===== V: TRANS

static num tag_V_th;
static num tag_V_TH;
static num tag_V_left;
static num tag_V_right;

static void tag_V(const char *s)
{
  num th = subid(&s,thmid);
  num TH = subid(&s,thmid);
  eol(s);

  num thconclusion = vector_num_read(&thm2conclusion,th);
  num THconclusion = vector_num_read(&thm2conclusion,TH);

  num thleft,thright;
  if (!term_is_equality(thconclusion,&thleft,&thright)) reject("TRANS: first operation mismatch");
  num THleft,THright;
  if (!term_is_equality(THconclusion,&THleft,&THright)) reject("TRANS: second operation mismatch");

  if (!term_alphaequivalent(thright,THleft)) reject("TRANS: input mismatch");

  tag_V_th = th;
  tag_V_TH = TH;
  tag_V_left = thleft;
  tag_V_right = THright;
}

static void finish_V(num hypstart,num hypstop,num conclusion)
{
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("TRANS: output operation mismatch");
  if (!term_is(left,tag_V_left)) reject("TRANS: output left-side mismatch");
  if (!term_is(right,tag_V_right)) reject("TRANS: output right-side mismatch");

  if (!hypotheses_aremerged(hypstart,hypstop,tag_V_th,tag_V_TH,-1,-1)) reject("TRANS: hypothesis mismatch");
}

// ===== X: AXIOM

static num tag_X_term;

static void tag_X(const char *s)
{
  num term = subid(&s,termid);
  eol(s);

  if (!type_is_bool(term2type(term))) reject("AXIOM: non-bool input");

  tag_X_term = term;
}

static void finish_X(num hypstart,num hypstop,num conclusion)
{
  if (hypstop != hypstart) reject("AXIOM: hypotheses");
  if (!term_is(conclusion,tag_X_term)) reject("AXIOM: wrong conclusion");
}

// ===== Z: DEDUCT_ANTISYM_RULE
// if q entails p and p entails q then p = q

static num tag_Z_th;
static num tag_Z_TH;

static void tag_Z(const char *s)
{
  tag_Z_th = subid(&s,thmid);
  tag_Z_TH = subid(&s,thmid);
  eol(s);
}

static void finish_Z(num hypstart,num hypstop,num conclusion)
{
  num th = tag_Z_th;
  num TH = tag_Z_TH;
  num left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("DEDUCT_ANTISYM_RULE: operation mismatch");
  if (!term_is(left,vector_num_read(&thm2conclusion,th))) reject("DEDUCT_ANTISYM_RULE: left-side mismatch");
  if (!term_is(right,vector_num_read(&thm2conclusion,TH))) reject("DEDUCT_ANTISYM_RULE: right-side mismatch");

  if (!hypotheses_aremerged(hypstart,hypstop,tag_Z_th,tag_Z_TH,right,left)) reject("DEDUCT_ANTISYM_RULE: hypothesis mismatch");
}

// ===== theorems

static void tag_t(const char *s)
{
  know(vector_num_len(&thm2conclusion) == thmid);
  num hypstart = vector_num_len(&thmdata);
  num numargs = 0;
  num z = 0;
  while (*s != '\n') {
    z = subid(&s,termid);
    ++numargs;
    if (*s == '\n')
      vector_num_append(&thm2conclusion,z);
    else
      vector_num_append(&thmdata,z);
  }
  if (numargs < 1) reject("theorem with no conclusion");
  know(vector_num_len(&thm2conclusion) == thmid+1);

  for (num i = hypstart;i+1 < vector_num_len(&thmdata);++i) {
    num hthis = vector_num_read(&thmdata,i);
    num hnext = vector_num_read(&thmdata,i+1);
    if (term_alphaorder_cmp(hthis,hnext) != -1)
      reject("refusing out-of-order hypotheses");
  }

  void (*finish)(num,num,num);

  switch(lastinftag) {
    case 'A': finish = finish_A; break;
    case 'B': finish = finish_B; break;
    case 'C': finish = finish_C; break;
    case 'D': finish = finish_D; break;
    case 'E': finish = finish_E; break;
    case 'F': finish = finish_F; break;
    case 'P': finish = finish_P; break;
    case 'R': finish = finish_R; break;
    case 'S': finish = finish_S; break;
    case 'T': finish = finish_T; break;
    case 'U': finish = finish_U; break;
    case 'V': finish = finish_V; break;
    case 'X': finish = finish_X; break;
    case 'Z': finish = finish_Z; break;
    default:
      reject("theorem without preceding inference");
  }
  finish(hypstart,vector_num_len(&thmdata),z);
}

// ===== tags not relevant to logic; just check topology

static void tag_slash(const char *s)
{
  subid(&s,thmid);
  noteol(s);
}

static void tag_comma(const char *s)
{
  subid(&s,thmid);
  subid(&s,infid);
  if (*s != '\n') subid(&s,ptid);
  if (*s != '\n') subid(&s,ptid);
  eol(s);
}

// ===== dispatcher

static void handleline(num start,num stop)
{
  know(0 <= start);
  know(start <= stop);
  know(stop < in_bytes);
  know(in_buf[stop] == '\n');

  ++curline;
  if (stop <= start) {
    fprintf(stderr,"blank line %lld prohibited\n",curline);
    exit(100);
  }
  
  char tag = in_buf[start];
  const char *s = in_buf+start+1;

  switch(tag) {
    case 'a': tag_a(s); break;
    case 'b': tag_b(s); break;
    case 'c': tag_c(s); break;
    case 'd': tag_d(s); break;
    case 'e': tag_e(s); break;
    case 'f': tag_f(s); break;
    case 't': tag_t(s); break;
    case 'A': tag_A(s); break;
    case 'B': tag_B(s); break;
    case 'C': tag_C(s); break;
    case 'D': tag_D(s); break;
    case 'E': tag_E(s); break;
    case 'F': tag_F(s); break;
    case 'P': tag_P(s); break;
    case 'R': tag_R(s); break;
    case 'S': tag_S(s); break;
    case 'T': tag_T(s); break;
    case 'U': tag_U(s); break;
    case 'V': tag_V(s); break;
    case 'X': tag_X(s); break;
    case 'Z': tag_Z(s); break;
    case '/': tag_slash(s); break;
    case ',': tag_comma(s); break;
    case ';': break;
    default:
      fprintf(stderr,"line %lld: unrecognized tag %c\n",curline,tag);
      exit(100);
  }

  switch(tag) {
    case 'a': case 'b':
      ++typeid;
      vector_char_append(&type2tag_vec,tag);
      vector_num_append(&type2datapos,vector_num_len(&typedata));
      break;
    case 'c': case 'd': case 'e': case 'f':
      ++termid;
      vector_char_append(&term2tag_vec,tag);
      vector_num_append(&term2datapos,vector_num_len(&termdata));
      break;
    case 't':
      ++thmid;
      vector_num_append(&thm2datapos,vector_num_len(&thmdata));
      break;
    case 'A': case 'B': case 'C': case 'D':
    case 'E': case 'F': case 'P': case 'R':
    case 'S': case 'T': case 'U': case 'V':
    case 'X': case 'Z':
      if (tag == 'A') ++typedefid;
      ++infid;
      lastinftag = tag;
      break;
    case ',': case ';':
      ++ptid;
      break;
    case '/':
      break;
    default:
      fprintf(stderr,"line %lld: unrecognized tag %c\n",curline,tag);
      exit(100);
  }
}

// ===== overall driver

static void verify(void)
{
  if (in_bytes < 0) {
    fprintf(stderr,"internal error: negative length\n");
    exit(100);
  }
  if (in_bytes > CUTOFF) {
    fprintf(stderr,"refusing to handle more than %lld bytes\n",CUTOFF);
    exit(100);
  }

  vector_num_append(&type2datapos,0);
  vector_num_append(&term2datapos,0);
  vector_num_append(&thm2datapos,0);

  num start = 0;
  for (num i = 0;i < in_bytes;++i) {
    char c = in_buf[i];
    if (c == '\n') {
      if (start) handleline(start,i);
      start = i+1;
      continue;
    }
    if (c < 32 || c > 126) {
      fprintf(stderr,"byte %d is not printable ASCII\n",(int) c);
      exit(100);
    }
  }
  if (start != in_bytes) reject("subsequent partial final line");
}

int main()
{
  in_init();
  if (in_bytes < 11 || memcmp(in_buf,"HOLTrace 1\n",11)) {
    fprintf(stderr,"input does not start with HOLTrace 1\n");
    exit(100);
  }

  verify();
  fprintf(stderr,"verified %lld bytes, %lld lines, %lld types, %lld terms, %lld infs, %lld thms, %lld typedefs\n"
    ,in_bytes,curline
    ,typeid
    ,termid
    ,infid
    ,thmid
    ,typedefid
  );

  return 0;
}