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

VECTOR_define_inline(char)

typedef long long num;
VECTOR_define_inline(num)

// ===== 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 num curline = 1; // 1-numbered for error messages

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);
  h0 ^= (h1<<5)|(h1>>27);
  h1 += (h0<<7)|(h0>>25);
  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);
  }
}

// ===== type operations

static num numtypes;

typedef struct {
  num pos; // position in type_data_state
} type_ptr;

static inline type_ptr pos2type(num pos) {
  type_ptr result;
  result.pos = pos;
  return result;
}

typedef struct {
  const char *name;
  num subtypes; // -1 for tyvar
  num subtypepos; // position in type_subtype_state
  num hash;
} type_data;

VECTOR_define_inline(type_data)
VECTOR_define_inline(type_ptr)

static vector_type_data type_data_state;
static inline type_data type2data(type_ptr type) {
  return vector_type_data_read(&type_data_state,type.pos);
}
static inline num type2hash(type_ptr type) {
  return type2data(type).hash;
}

static vector_type_ptr type_subtype_state;
static inline type_ptr pos2subtype(num pos) {
  return vector_type_ptr_read(&type_subtype_state,pos);
}

static int type_cmp(type_ptr type,type_ptr TYPE)
{
  if (type.pos == TYPE.pos) return 0;
  type_data t = type2data(type);
  type_data T = type2data(TYPE);
  if (t.subtypes >= 0 && T.subtypes < 0) return 1;
  if (T.subtypes >= 0 && t.subtypes < 0) return -1;
  int result = name_cmp(t.name,T.name);
  if (result) return result;
  if (t.subtypes < 0) return 0;
  know(T.subtypes == t.subtypes);
  for (num i = 0;i < t.subtypes;++i) {
    type_ptr subtype = pos2subtype(t.subtypepos+i);
    type_ptr SUBTYPE = pos2subtype(T.subtypepos+i);
    result = type_cmp(subtype,SUBTYPE);
    if (result) return result;
  }
  return 0;
}

static int type_is(type_ptr type,type_ptr TYPE)
{
  if (type.pos == TYPE.pos) return 1;
  type_data t = type2data(type);
  type_data T = type2data(TYPE);
  if (t.hash != T.hash) return 0;
  if (t.subtypes != T.subtypes) return 0;
  if (!name_is(t.name,T.name)) return 0;
  if (t.subtypes < 0) return 0;
  know(T.subtypes == t.subtypes);
  for (num i = 0;i < t.subtypes;++i) {
    type_ptr subtype = pos2subtype(t.subtypepos+i);
    type_ptr SUBTYPE = pos2subtype(T.subtypepos+i);
    if (!type_is(subtype,SUBTYPE)) return 0;
  }
  return 1;
}

static int type_is_tyvar(type_ptr type)
{
  type_data t = type2data(type);
  return t.subtypes < 0;
}

static int type_is_tyvarnamed(type_ptr type,const char *name,char split)
{
  type_data t = type2data(type);
  if (t.subtypes >= 0) return 0;
  return name_is_withsplit(t.name,name,split);
}

// does not constrain arguments
static int type_is_appnamed(type_ptr type,const char *name,char split)
{
  type_data t = type2data(type);
  if (t.subtypes < 0) return 0;
  return name_is_withsplit(t.name,name,split);
}

static int type_is_bool(type_ptr type)
{
  type_data t = type2data(type);
  if (t.subtypes != 0) return 0;
  return name_is(t.name,"bool\n");
}

static int type_is_fun(type_ptr type,type_ptr *from,type_ptr *to)
{
  type_data t = type2data(type);
  if (t.subtypes != 2) return 0;
  if (!name_is(t.name,"fun\n")) return 0;
  if (from) *from = pos2subtype(t.subtypepos);
  if (to) *to = pos2subtype(t.subtypepos+1);
  return 1;
}

static int type_is_funfromto(type_ptr type,type_ptr from,type_ptr to)
{
  type_data t = type2data(type);
  if (t.subtypes != 2) return 0;
  if (!name_is(t.name,"fun\n")) return 0;
  if (!type_is(from,pos2subtype(t.subtypepos))) return 0;
  if (!type_is(to,pos2subtype(t.subtypepos+1))) return 0;
  return 1;
}

// XXX simplicity: could merge with type_some_subst_is
static int type_is_equality(type_ptr type)
{
  type_ptr 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 type_some_subst_is
static int type_is_choice(type_ptr type)
{
  type_ptr 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);
}

static int type_is_abstype(type_ptr abstype,const char *abstypename,const char *tyvarnames,num numtyvars,char split)
{
  type_data t = type2data(abstype);
  if (t.subtypes != numtyvars) return 0;
  if (!name_is_withsplit(t.name,abstypename,split)) return 0;
  const char *z = tyvarnames;
  for (num i = 0;i < numtyvars;++i) {
    type_ptr subtype = pos2subtype(t.subtypepos+i);
    if (!type_is_tyvarnamed(subtype,z,split)) return 0;
    while (*z != split) ++z;
    ++z;
  }
  return 1;
}

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

  type_data t = type2data(type);
  type_data T = type2data(TYPE);

  if (t.subtypes != T.subtypes) return 0;

  if (t.subtypes >= 0) {
    if (!name_is(t.name,T.name)) return 0;
    for (num i = 0;i < t.subtypes;++i) {
      type_ptr subtype = pos2subtype(t.subtypepos+i);
      type_ptr SUBTYPE = pos2subtype(T.subtypepos+i);
      if (!type_tyvarnames_subst_is(subtype,SUBTYPE,abstype,numtyvars,tyvarnames,split))
        return 0;
    }
    return 1;
  }

  const char *z = tyvarnames;
  for (num i = 0;i < numtyvars;++i) {
    if (type_is_tyvarnamed(type,z,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
      type_data a = type2data(abstype);
      know(a.subtypes == numtyvars);
      type_ptr abstypei = pos2subtype(a.subtypepos+i);
      return type_is(TYPE,abstypei);
    }
    while (*z != split) ++z;
    ++z;
  }

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

static int type_subst_is(vector_type_ptr *from,vector_type_ptr *to,type_ptr type,type_ptr TYPE)
{
  type_data t = type2data(type);
  type_data T = type2data(TYPE);

  if (t.subtypes >= 0) {
    if (T.subtypes != t.subtypes) return 0;
    if (!name_is(t.name,T.name)) return 0;
    for (num i = 0;i < t.subtypes;++i) {
      type_ptr subtype = pos2subtype(t.subtypepos+i);
      type_ptr SUBTYPE = pos2subtype(T.subtypepos+i);
      if (!type_subst_is(from,to,subtype,SUBTYPE))
        return 0;
    }
    return 1;
  }

  num len = vector_type_ptr_len(from);
  know(len == vector_type_ptr_len(to));
  for (num i = 0;i < len;++i)
    if (type_is(type,vector_type_ptr_read(from,i)))
      return type_is(TYPE,vector_type_ptr_read(to,i));

  return type_is(type,TYPE);
}

static int type_substboth_is(vector_type_ptr *from,vector_type_ptr *to,type_ptr type,type_ptr TYPE)
{
  type_data t = type2data(type);
  type_data T = type2data(TYPE);

  if (t.subtypes < 0) {
    num len = vector_type_ptr_len(from);
    know(len == vector_type_ptr_len(to));
    for (num i = 0;i < len;++i)
      if (type_is(type,vector_type_ptr_read(from,i))) {
        type = vector_type_ptr_read(to,i);
        break;
      }
    return type_subst_is(from,to,TYPE,type);
  }

  if (T.subtypes < 0) {
    num len = vector_type_ptr_len(from);
    know(len == vector_type_ptr_len(to));
    for (num i = 0;i < len;++i)
      if (type_is(TYPE,vector_type_ptr_read(from,i))) {
        TYPE = vector_type_ptr_read(to,i);
        break;
      }
    return type_subst_is(from,to,type,TYPE);
  }

  if (T.subtypes != t.subtypes) return 0;
  if (!name_is(t.name,T.name)) return 0;

  for (num i = 0;i < t.subtypes;++i) {
    type_ptr subtype = pos2subtype(t.subtypepos+i);
    type_ptr SUBTYPE = pos2subtype(T.subtypepos+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_type_ptr *from,vector_type_ptr *to,type_ptr type,type_ptr TYPE)
{
  type_data t = type2data(type);
  type_data T = type2data(TYPE);

  if (t.subtypes >= 0) {
    if (T.subtypes != t.subtypes) return 0;
    if (!name_is(t.name,T.name)) return 0;
    for (num i = 0;i < t.subtypes;++i) {
      type_ptr subtype = pos2subtype(t.subtypepos+i);
      type_ptr SUBTYPE = pos2subtype(T.subtypepos+i);
      if (!type_find_subst_append(from,to,subtype,SUBTYPE))
        return 0;
    }
    return 1;
  }

  num len = vector_type_ptr_len(from);
  know(len == vector_type_ptr_len(to));
  for (num i = 0;i < len;++i)
    if (type_is(type,vector_type_ptr_read(from,i)))
      return type_is(TYPE,vector_type_ptr_read(to,i));

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

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

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

  know(type_subst_is(&from,&to,type,TYPE));
  return 1;
}

// 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_type_ptr *result,type_ptr type)
{
  type_data t = type2data(type);

  if (t.subtypes < 0) {
    for (num i = 0;i < vector_type_ptr_len(result);++i)
      if (type_is(vector_type_ptr_read(result,i),type))
        return;
    vector_type_ptr_append(result,type);
    return;
  }

  for (num i = 0;i < t.subtypes;++i)
    type_vars_append(result,pos2subtype(t.subtypepos+i));
}

static void type_vars(vector_type_ptr *result,type_ptr type)
{
  vector_type_ptr_empty(result);
  type_vars_append(result,type);
}

// ===== term operations

static num numterms;

typedef struct {
  num pos; // position in term_data_state
} term_ptr;

static inline term_ptr pos2term(num pos) {
  term_ptr result;
  result.pos = pos;
  return result;
}

typedef struct {
  type_ptr type;
  num hash;
  num frees;
  num freepos;
  union {
    const char *name; // for tag 'c' or 'd'
    struct {
      term_ptr v;
      term_ptr x;
    } terms; // for tag 'e' or 'f'
  } split;
  char tag;
} term_data;

VECTOR_define_inline(term_ptr)
VECTOR_define_inline(term_data)

static vector_term_data term_data_state;
static inline term_data term2data(term_ptr term) {
  return vector_term_data_read(&term_data_state,term.pos);
}
static inline num term2hash(term_ptr term) {
  return term2data(term).hash;
}
static inline char term2tag(term_ptr term) {
  return term2data(term).tag;
}

static vector_term_ptr termfrees_state;

static type_ptr term2type(term_ptr term)
{
  term_data t = term2data(term);
  return t.type;
}

static int term_is_const(term_ptr term,type_ptr *type,const char **name)
{
  term_data t = term2data(term);
  if (t.tag != 'c') return 0;
  if (type) *type = t.type;
  if (name) *name = t.split.name;
  return 1;
}

static int term_is_var(term_ptr term,type_ptr *type,const char **name)
{
  term_data t = term2data(term);
  if (t.tag != 'd') return 0;
  if (type) *type = t.type;
  if (name) *name = t.split.name;
  return 1;
}

static int term_is_comb(term_ptr term,type_ptr *type,term_ptr *funterm,term_ptr *pointterm)
{
  term_data t = term2data(term);
  if (t.tag != 'e') return 0;
  if (type) *type = t.type;
  if (funterm) *funterm = t.split.terms.v;
  if (pointterm) *pointterm = t.split.terms.x;
  return 1;
}

static int term_is_abs(term_ptr term,type_ptr *type,term_ptr *fromterm,term_ptr *toterm)
{
  term_data t = term2data(term);
  if (t.tag != 'f') return 0;
  if (type) *type = t.type;
  if (fromterm) *fromterm = t.split.terms.v;
  if (toterm) *toterm = t.split.terms.x;
  return 1;
}

static int term_is(term_ptr term,term_ptr TERM)
{
  if (term.pos == TERM.pos) return 1;
  term_data t = term2data(term);
  term_data T = term2data(TERM);
  if (t.hash != T.hash) return 0;
  if (t.tag != T.tag) return 0;
  if (!type_is(t.type,T.type)) return 0;
  if (t.tag == 'c' || t.tag == 'd') return name_is(t.split.name,T.split.name);
  if (!term_is(t.split.terms.v,T.split.terms.v)) return 0;
  if (!term_is(t.split.terms.x,T.split.terms.x)) return 0;
  return 1;
}

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

  num lenL = vector_term_ptr_len(L);
  for (num i = 2*(lenL/2)-2;i >= 0;i -= 2) {
    term_ptr var = vector_term_ptr_read(L,i);
    term_ptr VAR = vector_term_ptr_read(L,i+1);
    if (term_is(term,var)) return term_is(TERM,VAR) ? 0 : -1;
    if (term_is(TERM,VAR)) return 1;
  }

  term_data t = term2data(term);
  term_data T = term2data(TERM);
  return name_cmp(t.split.name,T.split.name);
}

// can extend L while running but restores it
static int term_alphaorder_cmp_recursive(term_ptr term,term_ptr TERM,vector_term_ptr *L)
{
  if (term.pos == TERM.pos) return 0;

  term_data t = term2data(term);
  term_data T = term2data(TERM);

  if (t.tag > T.tag) return 1;
  if (t.tag < T.tag) return -1;

  if (t.tag == 'd')
    return term_alphaorder_cmp_vars(term,TERM,L);

  if (t.tag == 'c') {
    int result = name_cmp(t.split.name,T.split.name);
    if (result) return result;
    return type_cmp(t.type,T.type);
  }

  if (t.tag == 'e') {
    int result = term_alphaorder_cmp_recursive(t.split.terms.v,T.split.terms.v,L);
    if (result) return result;
    return term_alphaorder_cmp_recursive(t.split.terms.x,T.split.terms.x,L);
  }

  know(t.tag == 'f');

  int result = type_cmp(term2type(t.split.terms.v),term2type(T.split.terms.v));
  if (result) return result;

  num lenL = vector_term_ptr_len(L);
  vector_term_ptr_append(L,t.split.terms.v);
  vector_term_ptr_append(L,T.split.terms.v);
  result = term_alphaorder_cmp_recursive(t.split.terms.x,T.split.terms.x,L);
  vector_term_ptr_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_type_ptr *result,term_ptr term)
{
  term_data t = term2data(term);

  if (t.tag == 'c' || t.tag == 'd') {
    type_vars_append(result,t.type);
    return;
  }

  know(t.tag == 'e' || t.tag == 'f');
  term_tyvars_append(result,t.split.terms.v);
  term_tyvars_append(result,t.split.terms.x);

  // scanning type would be redundant for both e and f
  // and scanning type by itself is insufficient
  // so skip scanning type
}

static void term_tyvars(vector_type_ptr *result,term_ptr term)
{
  vector_type_ptr_empty(result);
  term_tyvars_append(result,term);
}

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

static int term_is_equality(term_ptr term,term_ptr *left,term_ptr *right)
{
  term_ptr 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(term_ptr term,term_ptr TERM)
{
  static vector_term_ptr tmp;
  know(vector_term_ptr_len(&tmp) == 0);
  return term_alphaorder_cmp_recursive(term,TERM,&tmp);
}

static int term_alphaequivalent(term_ptr term,term_ptr TERM)
{
  return term_alphaorder_cmp(term,TERM) == 0;
}

static void term_freevars_append(vector_term_ptr *result,term_ptr term)
{
  num origlen = vector_term_ptr_len(result);
  term_data t = term2data(term);
  for (num i = 0;i < t.frees;++i) {
    term_ptr v = vector_term_ptr_read(&termfrees_state,t.freepos+i);
    int found = 0;
    for (num j = 0;j < origlen;++j)
      if (term_is(v,vector_term_ptr_read(result,j))) {
        found = 1;
        break;
      }
    if (!found)
      vector_term_ptr_append(result,vector_term_ptr_read(&termfrees_state,t.freepos+i));
  }
}

static void term_freevars(vector_term_ptr *result,term_ptr term)
{
  vector_term_ptr_empty(result);
  term_data t = term2data(term);
  for (num i = 0;i < t.frees;++i)
    vector_term_ptr_append(result,vector_term_ptr_read(&termfrees_state,t.freepos+i));
}

static int term_has_freevars(term_ptr term)
{
  term_data t = term2data(term);
  return t.frees > 0;
}

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

  term_data t = term2data(term);
  for (num i = 0;i < t.frees;++i) {
    term_ptr w = vector_term_ptr_read(&termfrees_state,t.freepos+i);
    type_ptr 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;
}

static int vector_term_contains(vector_term_ptr *list,term_ptr term)
{
  num i = vector_term_ptr_len(list);
  while (i-- > 0)
    if (term_is(term,vector_term_ptr_read(list,i)))
      return 1;
  return 0;
}

// later entries override earlier entries
// return term if not found
static term_ptr term_map_term(vector_term_ptr *from,vector_term_ptr *to,term_ptr term)
{
  num i = vector_term_ptr_len(from);
  while (i-- > 0)
    if (term_is(term,vector_term_ptr_read(from,i)))
      return vector_term_ptr_read(to,i);
  return term;
}

// later entries override earlier entries
// return -1 if not found
static num term_map_num(vector_term_ptr *from,vector_num *to,term_ptr term)
{
  num i = vector_term_ptr_len(from);
  while (i-- > 0)
    if (term_is(term,vector_term_ptr_read(from,i)))
      return vector_num_read(to,i);
  return -1;
}

static int term_subst_obvious_id(term_ptr term,vector_term_ptr *from)
{
  term_data t = term2data(term);
  for (num i = 0;i < t.frees;++i) {
    term_ptr w = vector_term_ptr_read(&termfrees_state,t.freepos+i);
    if (vector_term_contains(from,w)) 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(term_ptr term,vector_term_ptr *from,vector_term_ptr *to,vector_num *primed,term_ptr TERM)
{
  if (term_subst_obvious_id(term,from))
    return term_is(term,TERM);

  term_data t = term2data(term);

  know(t.tag != 'c');
  if (t.tag == 'd') {
    term_ptr m = term_map_term(from,to,term);
    num mprimes = term_map_num(from,primed,term);
    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
    type_ptr TERMtype;
    const char *TERMname;
    if (!term_is_var(TERM,&TERMtype,&TERMname)) return 0;
    type_ptr 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);
  }

  term_data T = term2data(TERM);
  if (T.tag != t.tag) return 0;

  if (t.tag == 'e') {
    if (!term_subst_is(t.split.terms.v,from,to,primed,T.split.terms.v)) return 0;
    if (!term_subst_is(t.split.terms.x,from,to,primed,T.split.terms.x)) return 0;
    return 1;
  }
  know(t.tag == 'f');

  term_ptr v = t.split.terms.v;
  term_ptr x = t.split.terms.x;

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

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

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

    // have v |-> x
    // considering rewriting as subst(v) |-> subst(x)
    // 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 f->m with f!=v has f free in x and v free in m
    // * if problem, move on to larger vprimes
    // * for vprimes>0, define problem as:
    //   v''' free in origsubst(x)
    //   where origsubst is from->to ignoring v

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

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

    term_data xdata = term2data(x);

    num freelen = xdata.frees;
    num freepos = xdata.freepos;

    for (num i = 0;i < freelen;++i) {
      term_ptr f = vector_term_ptr_read(&termfrees_state,freepos+i);
      if (term_is(f,v)) continue;
      term_ptr m = term_map_term(from,to,f);
      num mprimes = term_map_num(from,primed,f);
      if (mprimes < 0) {
        know(m.pos == f.pos); // not just term_is(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);
        type_ptr 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_term_ptr_append(from,v);
      vector_term_ptr_append(to,v);
      vector_num_append(primed,vprimes);

      int result = term_subst_is(x,from,to,primed,T.split.terms.x);

      vector_term_ptr_trunc(from,len);
      vector_term_ptr_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(term_ptr term,vector_type_ptr *tyfrom,vector_type_ptr *tyto,vector_term_ptr *varfrom,vector_term_ptr *varto,term_ptr TERM)
{
  term_data t = term2data(term);
  term_data T = term2data(TERM);

  if (t.tag != T.tag) return 0;

  if (t.tag == 'd')
    if (vector_term_contains(varfrom,term))
      return term_is(term_map_term(varfrom,varto,term),TERM);

  if (t.tag == 'c' || t.tag == 'd') {
    if (!name_is(t.split.name,T.split.name)) return 0;
    return type_subst_is(tyfrom,tyto,t.type,T.type);
  }

  if (t.tag == 'e') {
    term_ptr termfun = t.split.terms.v;
    term_ptr TERMfun = T.split.terms.v;
    if (!term_tyvar_subst_is_recursive(termfun,tyfrom,tyto,varfrom,varto,TERMfun)) return 0;
    term_ptr termpoint = t.split.terms.x;
    term_ptr TERMpoint = T.split.terms.x;
    return term_tyvar_subst_is_recursive(termpoint,tyfrom,tyto,varfrom,varto,TERMpoint);
  }

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

  term_ptr v = t.split.terms.v;
  term_ptr tterm = t.split.terms.x;
  type_ptr vtype;
  const char *vname;
  know(term_is_var(v,&vtype,&vname));

  // do not want to rename v now
  // so be careful to override v in varfrom lookups below

  term_ptr V = T.split.terms.v;
  term_ptr TTERM = T.split.terms.x;
  type_ptr 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

  term_data tdata = term2data(tterm);
  num freelen = tdata.frees;
  num freepos = tdata.freepos;

  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) {
      term_ptr f = vector_term_ptr_read(&termfrees_state,freepos+i);
      if (term_is(f,v)) continue;

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

      if (vector_term_contains(varfrom,f)) {
        term_ptr m = term_map_term(varfrom,varto,f);
        // f is renamed as m
        // now want to know:
        // does subst(v''') match m?
        type_ptr 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
        type_ptr 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_term_ptr_append(varfrom,v);
    vector_term_ptr_append(varto,V);
  }

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

  done:

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

static int term_tyvar_subst_is(term_ptr term,vector_type_ptr *from,vector_type_ptr *to,term_ptr TERM)
{
  static vector_term_ptr varfrom;
  static vector_term_ptr varto;
  know(vector_term_ptr_len(&varfrom) == 0);
  know(vector_term_ptr_len(&varto) == 0);
  return term_tyvar_subst_is_recursive(term,from,to,&varfrom,&varto,TERM);
}

// ===== theorem operations

static num numthms;

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

// see whether thmdata[start:stop] exactly matches h
static int hypotheses_match(num start,num stop,vector_term_ptr *h)
{
  if (vector_term_ptr_len(h) != stop-start) return 0;
  for (num i = start;i < stop;++i) {
    term_ptr hi = vector_term_ptr_read(h,i-start);
    if (!term_is(hi,vector_term_ptr_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_term_ptr *result,num start,num stop,term_ptr skip)
{
  vector_term_ptr_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) {
    term_ptr h = vector_term_ptr_read(&thmdata,i);
    if (skip.pos >= 0 && term_alphaequivalent(h,skip)) continue;
    vector_term_ptr_append(result,h);
  }
}

// same as hypotheses_extract but taking theorem as input
static void hypotheses_extract_th(vector_term_ptr *result,num th,term_ptr 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_term_ptr *result,vector_term_ptr *h,vector_term_ptr *H)
{
  vector_term_ptr_empty(result);

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

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

static int hypotheses_aremerged(num start,num stop,num th,num TH,term_ptr thskip,term_ptr THskip)
{
  static vector_term_ptr h;
  static vector_term_ptr H;
  static vector_term_ptr 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_term_ptr h;
  hypotheses_extract_th(&h,th,pos2term(-1));
  return hypotheses_match(start,stop,&h);
}

// ===== 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 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 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);
}

static dict const2type_state;
static type_ptr const2type(const char *s) {
  return pos2type(dict_lookup(&const2type_state,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_state,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,type_ptr result)
{
  reject_previous_constnames(s,split);
  dict_add(&const2type_state,s,split,result.pos);
}

// ===== typedefs

static num numtypedefs;

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

// ===== type tags

static void tag_a(const char *s) // Tyvar
{
  noteol(s);
  type_data t;
  t.name = s;
  t.subtypes = -1;
  t.subtypepos = -1;
  t.hash = name_hash(s);
  vector_type_data_append(&type_data_state,t);
}

static void tag_b(const char *s) // Tyapp
{
  num arity = subid(&s,-1);
  num hash = hash_mix(7152249725402530200+arity);
  type_data t;
  t.subtypes = arity;
  t.subtypepos = vector_type_ptr_len(&type_subtype_state);

  for (num i = 0;i < arity;++i) {
    type_ptr subtype = pos2type(subid(&s,numtypes));
    vector_type_ptr_append(&type_subtype_state,subtype);
    hash = hash_mix(hash+type2hash(subtype));
  }
  noteol(s);

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

  t.name = s;
  t.hash = hash_mix(hash+name_hash(s));
  vector_type_data_append(&type_data_state,t);
}

// ===== term tags

static void tag_c(const char *s) // Const
{
  type_ptr type = pos2type(subid(&s,numtypes));
  noteol(s);

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

  term_data t;
  t.type = type;
  t.hash = hash;
  t.frees = 0;
  t.freepos = 0;
  t.tag = 'c';
  t.split.name = s;

  vector_term_data_append(&term_data_state,t);

  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;
  }

  type_ptr registeredtype = const2type(s);
  if (registeredtype.pos >= 0) { // XXX
    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) {
    type_ptr from,to;
    if (!type_is_fun(type,&from,&to)) reject("non-function type with typedef name");

    char split = vector_char_read(&typedef2split,registeredtypedef);
    type_ptr reptype = pos2type(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) {
    type_ptr from,to;
    if (!type_is_fun(type,&from,&to)) reject("non-function type with typedef name");

    char split = vector_char_read(&typedef2split,registeredtypedef);
    type_ptr reptype = pos2type(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
{
  type_ptr type = pos2type(subid(&s,numtypes));
  noteol(s);

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

  term_data t;
  t.type = type;
  t.hash = hash;
  t.frees = 1;
  t.freepos = vector_term_ptr_len(&termfrees_state);
  t.tag = 'd';
  t.split.name = s;

  vector_term_ptr_append(&termfrees_state,pos2term(numterms));
  vector_term_data_append(&term_data_state,t);
}

static void tag_e(const char *s) // Comb
{
  type_ptr outputtype = pos2type(subid(&s,numtypes));
  term_ptr funterm = pos2term(subid(&s,numterms));
  term_ptr pointterm = pos2term(subid(&s,numterms));
  eol(s);

  num hash = 3679975592003923231LL;
  hash = hash_mix(hash+term2hash(funterm));
  hash = hash_mix(hash+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
    term_data p = term2data(pointterm);
    pos = p.freepos;
    len = p.frees;
  } else {
    static vector_term_ptr frees;
    term_freevars(&frees,funterm);
    term_freevars_append(&frees,pointterm);
    pos = vector_term_ptr_len(&termfrees_state);
    len = vector_term_ptr_len(&frees);
    for (num i = 0;i < len;++i)
      vector_term_ptr_append(&termfrees_state,vector_term_ptr_read(&frees,i));
  }

  term_data t;
  t.type = outputtype;
  t.hash = hash;
  t.frees = len;
  t.freepos = pos;
  t.tag = 'e';
  t.split.terms.v = funterm;
  t.split.terms.x = pointterm;

  vector_term_data_append(&term_data_state,t);
}

static void tag_f(const char *s) // Abs
{
  type_ptr outputtype = pos2type(subid(&s,numtypes));
  term_ptr fromterm = pos2term(subid(&s,numterms));
  term_ptr toterm = pos2term(subid(&s,numterms));
  eol(s);

  num hash = 4019844455831122549LL;
  hash = hash_mix(hash+term2hash(fromterm));
  hash = hash_mix(hash+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");

  term_data tt = term2data(toterm);
  num pos = tt.freepos;
  num len = tt.frees;

  for (num i = 0;i < len;++i) {
    term_ptr v = vector_term_ptr_read(&termfrees_state,pos+i);
    if (term_is(fromterm,v)) {
      num newpos = vector_term_ptr_len(&termfrees_state);
      num newlen = 0;
      for (num j = 0;j < len;++j)
        if (j != i) {
          vector_term_ptr_append(&termfrees_state,vector_term_ptr_read(&termfrees_state,pos+j));
          ++newlen;
        }
      pos = newpos;
      len = newlen;
      break;
    }
  }
    
  term_data t;
  t.type = outputtype;
  t.hash = hash;
  t.frees = len;
  t.freepos = pos;
  t.tag = 'f';
  t.split.terms.v = fromterm;
  t.split.terms.x = toterm;

  vector_term_data_append(&term_data_state,t);
}

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

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 vector_type_ptr tag_A_tyvars;

static void tag_A(const char *s)
{
  type_ptr reptype = pos2type(subid(&s,numtypes));
  term_ptr repprop = pos2term(subid(&s,numterms));
  num th = subid(&s,numthms);
  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");

  term_ptr thconclusion = vector_term_ptr_read(&thm2conclusion,th);

  term_ptr reppropcheck;
  term_ptr 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_type_ptr_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) {
        type_ptr tyvar = vector_type_ptr_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) {
        type_ptr tyvar = vector_type_ptr_read(&tag_A_tyvars,pos);
        type_ptr prevtyvar = vector_type_ptr_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.pos);
  vector_num_append(&typedef2repprop,repprop.pos);
  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);
}

static void finish_A(num hypstart,num hypstop,term_ptr 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);

  type_ptr reptype = pos2type(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);

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

  type_ptr 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

  term_ptr funterm;
  term_ptr 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

  term_ptr pointfunterm;
  term_ptr 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

  type_ptr 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

  type_ptr 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,numtypedefs);
  eol(s);
}

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

  num typedefpos = tag_D_pos;

  type_ptr reptype = pos2type(vector_num_read(&typedef2reptype,typedefpos));
  term_ptr repprop = pos2term(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);

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

  term_ptr funterm,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

  type_ptr 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

  term_ptr 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

  term_ptr 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

  term_ptr 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

  type_ptr 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

  type_ptr 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

  type_ptr abstype;
  type_ptr 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 term_ptr tag_B_xyx;
static term_ptr tag_B_y;

static void tag_B(const char *s)
{
  term_ptr term = pos2term(subid(&s,numterms));
  eol(s);

  term_ptr 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

  term_ptr 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,term_ptr conclusion)
{
  if (hypstop != hypstart) reject("BETA: hypotheses");
  term_ptr 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_type_ptr tag_C_tyvars;
static vector_type_ptr tag_C_tyvarsright;
static const char *tag_C_name;
static type_ptr tag_C_type;
static term_ptr tag_C_defn;

static void tag_C(const char *s)
{
  term_ptr term = pos2term(subid(&s,numterms));
  noteol(s);

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

  type_ptr 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_type_ptr_len(&tag_C_tyvarsright);++i) {
    type_ptr ty2 = vector_type_ptr_read(&tag_C_tyvarsright,i);
    int found = 0;
    for (num j = 0;j < vector_type_ptr_len(&tag_C_tyvars);++j) {
      type_ptr ty = vector_type_ptr_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,term_ptr conclusion)
{
  if (hypstop != hypstart) reject("DEFINITION: hypotheses");

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

  type_ptr 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 term_ptr tag_E_thleft;
static term_ptr tag_E_thright;
static num tag_E_TH;
static term_ptr tag_E_THleft;
static term_ptr tag_E_THright;

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

  term_ptr thconclusion = vector_term_ptr_read(&thm2conclusion,th);
  term_ptr THconclusion = vector_term_ptr_read(&thm2conclusion,TH);

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

  type_ptr 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,term_ptr conclusion)
{
  term_ptr left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("MK_COMB: operation mismatch");
  // now have: left = right

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

  term_ptr 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,pos2term(-1),pos2term(-1))) reject("MK_COMB: hypothesis mismatch");
}

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

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

static vector_term_ptr tag_F_free;

static void tag_F(const char *s)
{
  term_ptr var = pos2term(subid(&s,numterms));
  num th = subid(&s,numthms);
  eol(s);

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

  term_ptr thconclusion = vector_term_ptr_read(&thm2conclusion,th);
  term_ptr 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) {
    term_ptr h = vector_term_ptr_read(&thmdata,i);

    term_freevars(&tag_F_free,h);

    for (num j = 0;j < vector_term_ptr_len(&tag_F_free);++j)
      if (term_is(var,vector_term_ptr_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,term_ptr conclusion)
{
  term_ptr left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("ABS: operation mismatch");
  // now have: left = right

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

  term_ptr 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 term_ptr tag_P_right;
static num tag_P_th;
static num tag_P_TH;

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

  term_ptr thconclusion = vector_term_ptr_read(&thm2conclusion,th);
  term_ptr THconclusion = vector_term_ptr_read(&thm2conclusion,TH);

  term_ptr 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,term_ptr conclusion)
{
  if (!term_is(conclusion,tag_P_right)) reject("EQ_MP: conclusion mismatch");
  if (!hypotheses_aremerged(hypstart,hypstop,tag_P_th,tag_P_TH,pos2term(-1),pos2term(-1))) reject("EQ_MP: hypothesis mismatch");
}

// ===== R: REFL

static term_ptr tag_R_term;

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

static void finish_R(num hypstart,num hypstop,term_ptr conclusion)
{
  if (hypstop != hypstart) reject("REFL: hypotheses");
  term_ptr 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_term_ptr tag_S_from;
static vector_term_ptr tag_S_to;
static vector_num tag_S_primed;

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

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

    type_ptr 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_term_ptr_len(&tag_S_from);++i)
      if (term_is(from,vector_term_ptr_read(&tag_S_from,i)))
        goto skip;

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

static void finish_S(num hypstart,num hypstop,term_ptr conclusion)
{
  num th = tag_S_th;
  term_ptr thconclusion = vector_term_ptr_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) {
    term_ptr oldh = vector_term_ptr_read(&thmdata,i);
    int found = 0;
    for (num j = hypstart;j < hypstop;++j) {
      term_ptr newh = vector_term_ptr_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_type_ptr tag_T_from;
static vector_type_ptr tag_T_to;

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

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

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

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

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

static void finish_T(num hypstart,num hypstop,term_ptr conclusion)
{
  num th = tag_T_th;
  term_ptr thconclusion = vector_term_ptr_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) {
    term_ptr oldh = vector_term_ptr_read(&thmdata,i);
    int found = 0;
    for (num j = hypstart;j < hypstop;++j) {
      term_ptr newh = vector_term_ptr_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 term_ptr tag_U_term;

static void tag_U(const char *s)
{
  term_ptr term = pos2term(subid(&s,numterms));
  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,term_ptr conclusion)
{
  if (!term_is(conclusion,tag_U_term)) reject("ASSUME: wrong conclusion");
  if (hypstop-hypstart != 1) reject("ASSUME: wrong number of hypotheses");
  term_ptr h = vector_term_ptr_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 term_ptr tag_V_left;
static term_ptr tag_V_right;

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

  term_ptr thconclusion = vector_term_ptr_read(&thm2conclusion,th);
  term_ptr THconclusion = vector_term_ptr_read(&thm2conclusion,TH);

  term_ptr thleft,thright;
  if (!term_is_equality(thconclusion,&thleft,&thright)) reject("TRANS: first operation mismatch");
  term_ptr 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,term_ptr conclusion)
{
  term_ptr 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,pos2term(-1),pos2term(-1))) reject("TRANS: hypothesis mismatch");
}

// ===== X: AXIOM

static term_ptr tag_X_term;

static void tag_X(const char *s)
{
  term_ptr term = pos2term(subid(&s,numterms));
  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,term_ptr 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,numthms);
  tag_Z_TH = subid(&s,numthms);
  eol(s);
}

static void finish_Z(num hypstart,num hypstop,term_ptr conclusion)
{
  num th = tag_Z_th;
  num TH = tag_Z_TH;
  term_ptr left,right;
  if (!term_is_equality(conclusion,&left,&right)) reject("DEDUCT_ANTISYM_RULE: operation mismatch");
  if (!term_is(left,vector_term_ptr_read(&thm2conclusion,th))) reject("DEDUCT_ANTISYM_RULE: left-side mismatch");
  if (!term_is(right,vector_term_ptr_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 char lastinftag;

static void tag_t(const char *s)
{
  know(vector_term_ptr_len(&thm2conclusion) == numthms);
  num hypstart = vector_term_ptr_len(&thmdata);
  if (*s == '\n') reject("theorem with no conclusion");
  term_ptr z = pos2term(subid(&s,numterms));
  num numargs = 1;
  while (*s != '\n') {
    vector_term_ptr_append(&thmdata,z);
    z = pos2term(subid(&s,numterms));
    ++numargs;
  }
  vector_term_ptr_append(&thm2conclusion,z);
  know(vector_term_ptr_len(&thm2conclusion) == numthms+1);

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

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

  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_term_ptr_len(&thmdata),z);
}

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

static num numinfs;
static num numpt;

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

static void tag_comma(const char *s)
{
  subid(&s,numthms);
  subid(&s,numinfs);
  if (*s != '\n') subid(&s,numpt);
  if (*s != '\n') subid(&s,numpt);
  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':
      ++numtypes;
      break;
    case 'c': case 'd': case 'e': case 'f':
      ++numterms;
      break;
    case 't':
      ++numthms;
      vector_num_append(&thm2datapos,vector_term_ptr_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') ++numtypedefs;
      ++numinfs;
      lastinftag = tag;
      break;
    case ',': case ';':
      ++numpt;
      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(&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
    ,numtypes
    ,numterms
    ,numinfs
    ,numthms
    ,numtypedefs
  );

  return 0;
}