{ Abstract Pascal interactive prover }
{ -------- ------ ----------- ------ }


{ Copyright John T. Latham,
  Department of Computer Science,
  Manchester University. 1987 }



{ Loads a proof state (via dynamic files), interactively works on it via the
  standard input and output, and produces the updated state. }

{

The program is split into modules as follows:

1.  File open close, giving a stack of files for input.

2.  Timing and measurements, giving a virtual clock data type.

3.  Node marking.

4.  Error message generation, noting and producing error messages on the
    standard output.

5.  Manipulation of identifiers, including conversion between integer and 
    string and simple matching.

6.  Output presentation, giving simple routines for the presentation of
    results.

7.  Internal form interface.

8.  Symbol table for OBJ and Pascal variables. Done on variable CURRENTVARS.

9.  OBJect environment, including sorts.

10. Syntax rules, creation, declaration.

11. OBJ loading from internal form.

12. Proof loading and saving.

13. Help procedures.

14. Proof procedures.

15. Initialisation and finalisation.

16. Main program.


}

program prove(input,output);


{*****************************************************************************}
{************* global constants **********************************************}
{*****************************************************************************}

const

#include "VE-prove.i"

#include "dbconsts.i"


        maxerrors=10;
        outputwidth=80;     { width of output for expressions }


{*****************************************************************************}
{*********************** global types ****************************************}
{*****************************************************************************}

type

#include "dbtypes.i"
#include "prove-lexical-types.i"

{** forward reference pointer types}
        exp=^exprec;
        expseq=^expseqrec;
        subsseq=^subsseqrec;
        substseq=^substseqrec;
        ruleid=^rulerec;
        identlist=^identlistrec;

{** 3 state logic}
        boolean3=(dontknow,istrue,isfalse);

{** ordering relation}
        order=(less,equal,greater);

{** timing and measurements}
        timer=record
                start,time,interval:real;
              end;


{** dynamic stack of files}
        filestack=^filerec;
        filerec=record
                  fl:text;
                  last:filestack;
                  lastch:char;
                end;

{** sequence of symbols (as used by expression)}
        symbolseq=^symbolseqrec;
        symbolseqrec=   record
                          sym:symbol;
                          spelling:identifier;
                          sympos,symline:integer;
                          next:symbolseq;
                        end;

{** type (sort) signature}
        typeid=^typerec;
        typerec=record
                    name:identifier;   {name of sort}
                    eq,noteq:ruleid;   {built-in rules for type}
                end;

{** sequence/stack of types}
        typeseq=^typeseqrec;
        typestack=typeseq;
        typeseqrec=     record
                          thistype:typeid;
                          next:typeseq;
                        end;


{** mixfix syntax rules}
{** note: it is possible to mix mixfix and prefix in one rule,
    but restricted only in parse-rule}

        {ruleid=^rulerec;}

        partseq=^partseqrec;                       {each part}
        partseqrec=     record                     {either operator}
                          next:partseq;            {or arg}
                          case isop:boolean of
                          true:(opsym:identifier);
                          false:(argtype:typeid);
                        end;

        rulekind=(normalrule,pasvarrule,eqrule,noteqrule,objidrule,objvarrule);

        BIop=(BInone,BIplus,BIsubs,BImult,BIdiv,BImod,BIneg,
              BIlesseq,BIless,BIgreater,BIgreatereq,BIlast);

        rulerec=record
                  id:integer;            {for ordering}
                  BIstat:BIop;
                  assoc,comm:boolean;    {attributes for infix expressions}
                  precedence:integer;    {binding attribute }
                  ruletype:typeid;       {the type of the instantiated rule}
                  firstop:identifier;    {the first terminal operator}
                  preop:typeseq;         {types of preceding args in reverse}
                  preopcount:integer;    {number of preceding args}
                  rulepart:partseq;      {everything past the firstop}
                  prefixargs:typeseq;    {types of args for prefix rule}
                  postopcount:integer;   {number of all args after firstop}
                  next:ruleid;
                  case rulesort:rulekind of
                    normalrule,pasvarrule,eqrule,noteqrule,objidrule:();
                    objvarrule:(varno:integer);
                end;

{** equations}
        eqn=^eqnrec;
        eqnlist=eqn;

{** OBJect environment}
        object=^objectrec;
        objectrec=record
                    name:identifier;
                    inclusions:identlist;
                    sorts:typeseq;
                    rules:ruleid;
                    eqns:eqnlist;
                  end;

        objectseq=^objectseqrec;
        objectseqrec=record
                       obj:object;
                       next:objectseq;
                     end;

{** list of identifiers}
        {identlist=^identlistrec;}
        identlistrec=record
                       name:identifier;
                       next:identlist;
                     end;

{** proof state}
        blocktype=(programblock,procedureblock,functionblock);

        proofstatus=(unproved,partproved,proved,disproved);

        proofstepkind=(leaf,casestep);

        proofstep=^proofsteprec;
        proofsteprec=record
                       vc:exp;             {the vc at this point}
                       activecases:exp;    {and of all active cases above}
                                           {NB: initially nil, set up when
                                            parent is examined}
                       caseeqns:eqnlist;   {case equations above this point}
                                           {initially nil, set up when
                                            parent is examined}
                       examined:boolean;   {if has been examined}
                       impossible:boolean; {true if activecases=F}
                       status:proofstatus; {status of this proof step}
                       parent:proofstep;   {pointer to parent, or nil if root}
                       case kind:proofstepkind of
                         leaf:();
                         casestep:(truecase:exp;   {the case expression}
                                   case1,case2:proofstep);
                     end;

        vcseq=^vcrec;
        vcrec=record
                line:integer;
                vc:exp;
                vcproof:proofstep;
                next:vcseq;
              end;

        block=^blockrec;
        blockseq=block;
        blockrec=record
                   name:identifier;
                   kind:blocktype;
                   line:integer;
                   environment:objectseq;
                   objlist:identlist;
                   variables:expseq;
                   status:proofstatus;
                   vcs:vcseq;
                   next:blockseq;
                 end;


#include "prove-nodes-types.i"
#include "prove-parseexp-types.i"
#include "prove-simp-types.i"


{*****************************************************************************}
{***************** variables *************************************************}
{*****************************************************************************}


var {separated into modules of ownership}


{-************* file open and close ******************************************}

        ifile,freefiles:filestack;

{-************* timing and measurements **************************************}

{-************* procedures associated with error message generation **********}

        totalerrors,noerrors:integer;
        errors:array[1..maxerrors]of    record
                                          errno:integer;
                                          errid:identifier;
                                          errpos:integer;
                                        end;

{-************* procedures for manipulating and initialising identifiers *****}

{-************* output presentation ******************************************}

        outputpos:integer;

{-************* internal form interface **************************************}

        inch:char;

{-************* symbol table procedures for OBJ and Pascal variables *********}

        currentvars,lastcurrentvars:expseq;

{-************* OBject environment for sorts and eqns ************************}

        anytype,errortype:typeid;
        inttype,booltype,idtype:typeid;
        allobjects,currentenviron,builtinenviron:objectseq;

        currentobject:object; {current for declarations etc.}
                              {head of list in current environment}
                              {during proof, holds only case equations}

        lastequationlevel:integer; {level of last non-case equation declared}

{-************* procedures associated with syntax rules **********************}

        errorrule,subsrule,intrule,
        truerule,falserule,andrule,orrule,imprule,
        notrule,succrule,predrule,zerorule,lessidrule:ruleid;
        objidrules:ruleid;   {global list of ID rules used}
        rulecount:integer;   {for ordering}

{-************* OBJ loading **************************************************}

{-************* loading and saving proof state *******************************}

        proofout:text;

{-************* help procedures **********************************************}

{-************* proof procedures *********************************************}

        proof:blockseq;

{-************* initialisation and finalisation ******************************}

{-************* main program *************************************************}

        sourcename:identifier;
        itemstatus:apstatus;
        proofstate:proofstatus;
        okayinput:boolean;
        errorexp:exp;


#include "options-vars.i"
#include "photo-vars.i"
#include "prove-nodes-vars.i"
#include "prove-simp-vars.i"
#include "prove-lexical-vars.i"


{*****************************************************************************}
{************** forward references *******************************************}
{*****************************************************************************}


#include "options-forward.i"
#include "photo-forward.i"
#include "prove-nodes-forward.i"
#include "prove-expman-forward.i"
#include "prove-simp-forward.i"
#include "prove-parseexp-forward.i"
#include "prove-lexical-forward.i"


procedure error(n:integer); forward;

function matchsym(target,pattern:identifier):boolean; forward;

procedure getnewrule(rsort:rulekind; typ:typeid; first:identifier;
                     pre:typeseq; precount:integer; rule:partseq;
                     prefix:typeseq; postcount:integer; var r:ruleid); forward;

procedure getobjidrule(id:identifier; var r:ruleid); forward;

procedure makeinfixrule(op:identifier; argtyp,optyp:typeid; var rule:ruleid);
                        forward;



#include "dbprocs.i"


{*****************************************************************************}
{*********** file open and close *********************************************}
{*****************************************************************************}


procedure openinput(thisfile:identifier; dir:directory; var opened:boolean);
var f:filestack;
begin
  if freefiles=nil then
    new(f)
  else
  begin
    f:=freefiles;
    freefiles:=freefiles^.last;
  end;

  with f^ do
  begin
    last:=ifile;
    lastch:=inch;
    openfile(fl,thisfile,dir,true,opened);
    if opened then
    begin
      if eof(fl) then
        inch:='.'
      else
        inch:=fl^;
      ifile:=f;
    end;
  end;
end;

procedure closeinputfile;
var temp:filestack; dummy:boolean;
begin
  temp:=ifile;

  inch:=ifile^.lastch;
  ifile:=ifile^.last;

  temp^.last:=freefiles;
  freefiles:=temp;
end;

procedure initfiles;
begin
  freefiles:=nil;
  ifile:=nil;
end;


{****************************************************************************}
{************** timing and measurements *************************************}
{****************************************************************************}


procedure resetclock(var t:timer);
{ set a clock ready for timing }
begin
  t.time:=0;
end;

procedure startclock(var t:timer);
{ start timing after a reset or continue after stop clock }
var clk:real;
begin
  clk:=clock/1000;
  t.start:=clk-t.time;
  t.interval:=clk;
end;

procedure stopclock(var t:timer);
{ .TIME is time in seconds since first startclock,
  .INTERVAL is time in seconds since last startclock }
var clk:real;
begin
  clk:=(clock+0.5)/1000;
  t.interval:=clk-t.interval;
  t.time:=clk-t.start;
end;

{****************************************************************************}
{************** node marking ************************************************}
{****************************************************************************}

procedure markfixed;
var ob:objectseq; bl:blockseq; vl:vcseq;

    procedure markequations(eq:eqnlist);
    begin
      while eq<>nil do
        with eq^ do
        begin
          markexp(lhs);
          markexp(rhs);
          if cond<>nil then
            markexp(cond);
          eq:=next;
        end;
    end;

    procedure markproofstep(p:proofstep);
    begin
      with p^ do
      begin
        markexp(vc);
        if activecases<>nil then
          markexp(activecases);
        markequations(caseeqns);
        if kind=casestep then
        begin
          markexp(truecase);
          markproofstep(case1);
          markproofstep(case2);
        end;
      end;
    end;

begin
  markexp(errorexp);
  bl:=proof;
  while bl<>nil do
    with bl^ do
    begin
      markexpseq(variables);
      vl:=vcs;
      while vl<>nil do
        with vl^ do
        begin
          markexp(vc);
          markproofstep(vcproof);
          vl:=next;
        end;
      bl:=next;
    end;
  ob:=allobjects;
  while ob<>nil do
  begin
    markequations(ob^.obj^.eqns);
    ob:=ob^.next;
 end;
end;


{****************************************************************************}
{*********** procedures associated with error message generation ************}
{****************************************************************************}


procedure outlineerrors;
var i,j,pos:integer;
begin
  if noerrors>0 then
  begin
    write(output,errorprompt);
    write(photo,errorprompt);
    i:=1;
    j:=0;
    while i<=noerrors do
    begin
      if j<errors[i].errpos then
      begin
        while j<errors[i].errpos-1 do
        begin
          j:=j+1;
          write(output,' ');
          write(photo,' ');
        end;
        write(output,'!');
        write(photo,'!');
        j:=j+1;
      end;
      i:=i+1;
    end;
    writeln(output);
    writeln(photo);
    j:=0;
    pos:=0;
    i:=1;
    while i<=noerrors do
    begin
      if errors[i].errpos>pos then
      begin
        j:=j+1;
        pos:=errors[i].errpos;
      end;
      write(output,'  ',j:1,'  ');
      write(photo,'  ',j:1,'  ');
      errormessage(errors[i].errno,errors[i].errid,output);
      errormessage(errors[i].errno,errors[i].errid,photo);
      i:=i+1;
    end;
    noerrors:=0;
  end;
end;

procedure erroratwith(er,erpos,erline:integer; id:identifier);
begin
  totalerrors:=succ(totalerrors);
  if noerrors<maxerrors then
  begin
    noerrors:=succ(noerrors);
    with errors[noerrors]do
    begin
      errno:=er;
      errid:=id;
      if erline=lineno then
        errpos:=erpos
      else
      begin
        errpos:=sympos;
        if errno=300 then
          errno:=301; {modify error syntax-error to syntax-error-before}
      end;
    end;
  end;
end;

procedure errorwith(n:integer; id:identifier);
begin
  erroratwith(n,sympos,lineno,id);
end;

procedure error{n:integer};
begin
  erroratwith(n,sympos,lineno,spaces);
end;

procedure errorat(er,erpos,erline:integer);
begin
  erroratwith(er,erpos,erline,spaces);
end;

procedure syntaxerror(s:symbol);
begin
  errorwith(300,symspell[s]);
end;

procedure initerrors;
begin
  totalerrors:=0;
  noerrors:=0;
end;


{*****************************************************************************}
{*********** procedures for manipulating and initialising identifiers ********}
{*********** (except initialising symbol spellings) **************************}
{*****************************************************************************}


function signedval(spelling:identifier):integer;
{ NB: may be negative }
var h,i,j:integer; overflow:boolean; neg:boolean;
begin
  i:=0;
  j:=0;
  overflow:=false;
  neg:=spelling[1]='-';
  if neg then
    j:=j+1;
  repeat
    j:=j+1;
    if spelling[j]<>' ' then
    begin
      if i>(maxint div 10) then
        overflow:=true
      else
        i:=i*10;
      h:=ord(spelling[j])-ord('0');
      if i>maxint-h then
        overflow:=true
      else
        i:=i+h;
    end;
  until(spelling[j]=' ')or(j=identlength);
  if neg then
    signedval:=-i
  else
    signedval:=i;
  if overflow then
    error(215); {integer overflow}
end;

procedure getintspell(i:integer; var int:identifier);
{NB: may be negative}
var j,k:integer;

    procedure getspell(i:integer);
    begin
      if i>=10 then
        getspell(i div 10);
      if j<=identlength then
      begin
        int[j]:=chr((i mod 10)+ord('0'));
        j:=j+1;
      end;
    end;

begin
  int:=spaces;
  j:=1;
  if i<0 then
  begin
    int[1]:='-';
    i:=-i;
    j:=2;
  end;
  getspell(i);
end;

function matchsym{target,pattern:identifier):boolean};
{target is prefix of pattern, at least up to asterisk }
var matched,star,space:boolean; i:integer;
begin
  i:=1;
  matched:=true;
  star:=false;
  while (i<=identlength) and matched and not star do
  begin
    if pattern[i]='*' then
      star:=true
    else
    if target[i]=pattern[i] then
      i:=succ(i)
    else
      matched:=false;
  end;
  if star then
  begin
    space:=false;
    while (i<identlength) and matched and not space do
    begin
      if target[i]=' ' then
        space:=true
      else
      if target[i]=pattern[succ(i)] then
        i:=succ(i)
      else
        matched:=false;
    end;
  end;
  matchsym:=matched;
end;


{*****************************************************************************}
{*********** procedures for presenting output ********************************}
{*****************************************************************************}


procedure writeline;
begin
  outputpos:=0;
  writeln(output);
  writeln(photo);
end;

procedure outchar(c:char);
begin
  if outputpos>=outputwidth then
    writeline;
  write(output,c);
  write(photo,c);
  outputpos:=succ(outputpos);
end;

procedure outname(n:identifier);
var i,l:integer;
begin
  l:=1;
  while(n[l]<>' ')and(l<identlength)do
    l:=succ(l);
  if n[l]<>' ' then
    l:=succ(l);
  if outputpos>=outputwidth-l then
  begin
    writeln(output);
    writeln(photo);
    outputpos:=0;
  end;
  write(output,' ');
  write(photo,' ');
  for i:=1 to l-1 do
  begin
    write(output,n[i]);
    write(photo,n[i]);
  end;
  outputpos:=outputpos+l;
end;

procedure initoutput;
begin
  writeln(output,'Interactive AP Prover (Version ',VE:3:1,') source= ',sourcename);
  outputpos:=0;
end;


{*****************************************************************************}
{********** internal form interface ******************************************}
{*****************************************************************************}


procedure writechar(var fl:text; ch:char);
begin
  write(fl,ch:1);
end;

procedure writename(var fl:text; name:identifier);
var i:integer;
begin
  i:=1;
  while (i<identlength) and (name[i]<>' ') do
  begin
    write(fl,name[i]:1);
    i:=succ(i);
  end;
  if name[i]<>' ' then
    write(fl,name[i]);
  writeln(fl);
end;

procedure writenumber(var fl:text; n:integer);
var ns:identifier;
begin
  getintspell(n,ns);
  writename(fl,ns);
end;

procedure writeprefixform(var fl:text; rule:ruleid);
var ts:typeseq; ps:partseq;
begin
  with rule^ do
  begin
    writename(fl,firstop);
    writename(fl,ruletype^.name);
    writenumber(fl,preopcount+postopcount);
    if preop<>nil then
      writename(fl,preop^.thistype^.name)
    else
    if rulepart<>nil then
      if rulepart^.isop then
        writename(fl,rulepart^.opsym)
      else
        writename(fl,rulepart^.argtype^.name)
    else
    if prefixargs<>nil then
      writename(fl,prefixargs^.thistype^.name)
    else
      writename(fl,spaces);
  end;
end;

procedure readch;
begin
  with ifile^ do
  begin
    get(fl);
    inch:=fl^;
  end;
end;

procedure readname(var name:identifier);
var i:integer;
begin
  name:=spaces;
  with ifile^ do
  begin
    i:=1;
    while (i<identlength) and not eoln(fl) do
    begin
      name[i]:=fl^;
      get(fl);
      i:=succ(i);
    end;
    if not eoln(fl) then
      name[i]:=fl^;
    readln(fl);
    inch:=fl^;
  end;
end;

procedure readnumber(var n:integer);
var ns:identifier;
begin
  readname(ns);
  n:=signedval(ns);
end;

procedure readprefixform(var rule:ruleid);
var op,typ,second:identifier; srule:ruleid; found,match:boolean;
    argcount:integer; ob:objectseq;

begin
  readname(op);
  readname(typ);
  readnumber(argcount);
  readname(second);
  if op[1]='''' then
    getobjidrule(op,rule)
  else
  begin
    found:=false;
    ob:=currentenviron;
    while ob<>nil do
    begin
      srule:=ob^.obj^.rules;
      while srule<>nil do
      begin
        with srule^ do
        begin
          match:=false;
          if (firstop=op) then
            if (ruletype^.name=typ) then
              if (preopcount+postopcount=argcount) then
                if preop<>nil then
                  match:=preop^.thistype^.name=second
                else
                if rulepart<>nil then
                  if rulepart^.isop then
                    match:=rulepart^.opsym=second
                  else
                    match:=rulepart^.argtype^.name=second
                else
                if prefixargs<>nil then
                  match:=prefixargs^.thistype^.name=second
                else
                  match:=second=spaces;
          if match then
            if found then
            begin
              errorwith(236,op); {ambiguous prefix rule}
              rule:=errorrule;
            end
            else
            begin
              rule:=srule;
              found:=true;
            end;
        end;
        srule:=srule^.next;
      end;
      ob:=ob^.next;
    end;
    if not found then
    begin
      errorwith(237,op); {prefix rule not found}
      rule:=errorrule;
    end;
  end;
end;


{*****************************************************************************}
{************ symmbol table for OBJ and Pascal variables *********************}
{*****************************************************************************}


{using global CURRENTVARS for search and declare}

procedure declareobjvar(vname:identifier; typ:typeid);
{ presume doesn't already exist }
var vr:expseq; varnumber:integer;
begin
  newexpseq(vr);
  with vr^ do
  begin
    if currentvars=nil then
    begin
      currentvars:=vr;
      varnumber:=1;
    end
    else
    begin
      lastcurrentvars^.next:=vr;
      varnumber:=lastcurrentvars^.val^.oprule^.varno+1;
    end;
    lastcurrentvars:=vr;
    next:=nil;
    newexp(val);
    with val^ do
    begin
      getnewrule(objvarrule,typ,vname,nil,0,nil,nil,0,oprule);
      oprule^.varno:=varnumber;
      if varnumber>maxobjvar then
        errorwith(205,vname); {too many obj variables}
      args:=nil;
    end;
  end;
end;

procedure declarevar(vname:identifier; typ:typeid);
{ presume doesn't already exist }
var vr:expseq;
begin
  newexpseq(vr);
  with vr^ do
  begin
    if currentvars=nil then
      currentvars:=vr
    else
      lastcurrentvars^.next:=vr;
    lastcurrentvars:=vr;
    next:=nil;
    newexp(val);
    with val^ do
    begin
      getnewrule(pasvarrule,typ,vname,nil,0,nil,nil,0,oprule);
      args:=nil;
    end;
  end;
end;

procedure findvar(name:identifier; var vexp:exp);
var es:expseq; found:boolean;
begin
  es:=currentvars;
  found:=false;
  while (es<>nil) and not found do
    if name=es^.val^.oprule^.firstop then
    begin
      vexp:=es^.val;
      found:=true;
    end
    else
      es:=es^.next;
  if not found then
  begin
    vexp:=errorexp;
    errorwith(111,name);
  end;
end;


procedure findpossiblevar(name:identifier; var found:boolean; var vexp:exp);
{ require copy for vexp }
var es:expseq;
begin
  es:=currentvars;
  found:=false;
  while (es<>nil) and not found do
    if name=es^.val^.oprule^.firstop then
    begin
      copyexp(es^.val,vexp);
      found:=true;
    end
    else
      es:=es^.next;
end;


{*****************************************************************************}
{************ OBJect environment procedures **********************************}
{*****************************************************************************}


procedure createobject(objname:identifier; var found:boolean; var o:object);
{ create or find object from allobjects. }
{ object called spaces always created, and not chained in }

var ob:objectseq;

begin
  found:=false;
  if objname<>spaces then
  begin
    ob:=allobjects;
    while (ob<>nil) and not found do
      if ob^.obj^.name=objname then
        found:=true
      else
        ob:=ob^.next;
  end;
  if found then
    o:=ob^.obj
  else
  begin
    new(o);
    with o^ do
    begin
      name:=objname;
      sorts:=nil;
      rules:=nil;
      eqns:=nil;
      inclusions:=nil;
    end;
    if objname<>spaces then
    begin
      new(ob);
      with ob^ do
      begin
        obj:=o;
        next:=allobjects;
      end;
      allobjects:=ob;
    end;
  end;      
end;

procedure newobject(obje:object);

var ob:objectseq; objname:identifier; found,incfound:boolean; 
    oid:identlist; inco:object;
begin
  found:=false;
  objname:=obje^.name;
  if objname<>spaces then
  begin
    ob:=currentenviron;
    while not found and (ob<>nil) do
      if ob^.obj^.name=objname then
        found:=true
      else
        ob:=ob^.next;
  end;
  if not found then
  begin
    new(ob);
    with ob^ do
    begin
      obj:=obje;
      next:=currentenviron;
    end;
    currentenviron:=ob;
    oid:=obje^.inclusions;
    while oid<>nil do
    begin
      createobject(oid^.name,incfound,inco);
      newobject(inco);
      oid:=oid^.next;
    end;
  end;
end;

procedure showobjects;
const column=3;
var ob:objectseq;  i:integer;
begin
  writeln(output,'Objects in environment are:');
  writeln(output);
  writeln(photo,'Objects in environment are:');
  writeln(photo);
  i:=0;
  ob:=currentenviron^.next;  {first is spaces}
  while ob<>nil do
  begin
    write(output,ob^.obj^.name);
    write(photo,ob^.obj^.name);
    i:=succ(i) mod column;
    if i=0 then
    begin
      writeln(output);
      writeln(photo);
    end;
    ob:=ob^.next;
  end;
  if i<>0 then
  begin
    writeln(output);
    writeln(photo);
  end;
  writeln(output);
  writeln(photo);
end;

procedure findobject(objectname:identifier; var obj:object);
var ob:objectseq; found:boolean;
begin
  found:=false;
  ob:=currentenviron;
  while not found and (ob<>nil) do
    if ob^.obj^.name=objectname then
      found:=true
    else
      ob:=ob^.next;
  if found then
    obj:=ob^.obj
  else
    obj:=nil;
end;

procedure declareinclusion(obj:object; inc:identifier);
var oid:identlist;
begin
  with obj^ do
  begin
    new(oid);
    oid^.name:=inc;
    oid^.next:=inclusions;
    inclusions:=oid;
  end;
end;

procedure searchsort(name:identifier; var found:boolean; var ts:typeseq);
var ob:objectseq;
begin
  found:=false;
  ob:=currentenviron;
  while (ob<>nil) and not found do
  begin
    ts:=ob^.obj^.sorts;
    while (ts<>nil)and not found do
      if ts^.thistype^.name=name then
        found:=true
      else
        ts:=ts^.next;
    if not found then
      ob:=ob^.next;
  end;
end;

procedure declaresort(sortname:identifier; var typ:typeid);
var found:boolean; ts:typeseq;
    dummy:ruleid;
begin
  found:=false;
  searchsort(sortname,found,ts);
  if found then
    errorwith(150,sortname); {multiple declaration of sort}
  new(typ);
  with typ^ do
  begin
    name:=sortname;
    makeinfixrule(equalsspell,typ,booltype,eq);
    eq^.rulesort:=eqrule;
    makeinfixrule(notequalspell,typ,booltype,noteq);
    noteq^.rulesort:=noteqrule;
    noteq^.comm:=true;
    eq^.comm:=true;
  end;
  new(ts);
  with ts^ do
  begin
    thistype:=typ;
    next:=currentobject^.sorts;
  end;
  currentobject^.sorts:=ts;
end;

procedure findsort(name:identifier; var t:typeid);
var found:boolean; ts:typeseq;
begin
  searchsort(name,found,ts);
  if found then
    t:=ts^.thistype
  else
  begin
    errorwith(151,name); {undefined SORT}
    t:=errortype;
  end;
end;

function compatible(t1,t2:typeid):boolean;
begin
  compatible:=t1=t2;
end;

procedure initenviron;
begin
  currentenviron:=nil;
  allobjects:=nil;
  lastequationlevel:=0;
end;


{*****************************************************************************}
{************** procedures associated with syntax rules **********************}
{*****************************************************************************}


procedure getnewrule{rsort:rulekind; typ:typeid; first:identifier;
                     pre:typeseq; precount:integer; rule:partseq;
                     prefix:typeseq; postcount:integer; var r:ruleid};
begin
  new(r);
  with r^ do
  begin
    rulecount:=rulecount+1;
    id:=rulecount;
    BIstat:=BInone;
    assoc:=false;
    comm:=false;
    precedence:=0;
    rulesort:=rsort;
    ruletype:=typ;
    firstop:=first;
    preop:=pre;
    preopcount:=precount;
    rulepart:=rule;
    prefixargs:=prefix;
    postopcount:=postcount;
    next:=nil;
  end;
end;

procedure makenewrule(rsort:rulekind; typ:typeid; first:identifier;
                      pre:typeseq; precount:integer; rule:partseq;
                      prefix:typeseq; postcount:integer; var r:ruleid);

begin
  getnewrule(rsort,typ,first,pre,precount,rule,prefix,postcount,r);
  r^.next:=currentobject^.rules;
  currentobject^.rules:=r;
end;

function BIstatus(i:integer):BIop;
var b:BIop;
begin
  b:=BInone;
  while i>0 do
  begin
    i:=pred(i);
    if b<BIlast then
      b:=succ(b);
  end;
  BIstatus:=b;
end;

procedure getobjidrule{id:identifier; var r:ruleid};
var found:boolean;
begin
  r:=objidrules;
  found:=false;
  while (r<>nil)and not found do
    if r^.firstop<>id then
      r:=r^.next
    else
      found:=true;
  if not found then
  begin
    getnewrule(objidrule,idtype,id,nil,0,nil,nil,0,r);
    r^.next:=objidrules;
    objidrules:=r;
  end;
end;

procedure makeprefixrule(op:identifier; argtyp,optyp:typeid; var rule:ruleid);
var rulepart:partseq;
begin
  new(rulepart);
  with rulepart^ do
  begin
    next:=nil;
    isop:=false;
    argtype:=argtyp;
  end;
  makenewrule(normalrule,optyp,op,nil,0,rulepart,nil,1,rule);
end;

procedure makeinfixrule{op:identifier; argtyp,optyp:typeid; var rule:ruleid};
var rulepart:partseq; pre:typeseq;
begin
  new(pre);
  with pre^ do
  begin
    thistype:=argtyp;
    next:=nil;
  end;
  new(rulepart);
  with rulepart^ do
  begin
    next:=nil;
    isop:=false;
    argtype:=argtyp;
  end;
  makenewrule(normalrule,optyp,op,pre,1,rulepart,nil,1,rule);
end;

procedure initrules;
begin
  rulecount:=0;
  objidrules:=nil;
end;


{*****************************************************************************}
{*************** OBJ loading procedures **************************************}
{*****************************************************************************}


procedure loadtheorems(objname:identifier);

var vartype:typeid; lhs,rhs,cond:exp;
    varname,vartypename:identifier; found,okay:boolean;

begin
  openinput(objname,thmobjdir,found);
  if found then
  begin
    writeln(output,'Loading theorems ',objname);
    currentvars:=nil;
    while inch='V' do
    begin
      readch;
      readname(varname);
      readname(vartypename);
      findsort(vartypename,vartype);
      declareobjvar(varname,vartype);
    end;

    newrewritelevel;
    startmerge(true);
    while inch in ['E','C'] do
    begin
      if inch='E' then
      begin
        readch;
        loadprefixexpression(lhs);
        loadprefixexpression(rhs);
        cond:=nil;
      end
      else
      begin
        readch;
        loadprefixexpression(lhs);
        loadprefixexpression(rhs);
        loadprefixexpression(cond);
      end;
      mergeequation(lhs,rhs,cond,true,false);
      lastequationlevel:=rewritelevel;
    end;
    endmerge;
    closeinputfile;
  end;
end;

procedure loadrule;
var preopcount,postopcount:integer; firstop:identifier; rule:ruleid;
    rulepart,lastpart,part:partseq; preop,prefix,ts:typestack;
    ruletype:identifier; ruletypeid:typeid;
    argtype:typeid;
    precedence:integer; assoc,comm:boolean; BIstat:BIop; BInum:integer;

    procedure readrevtypeseq(var ts:typeseq; var count:integer);
    var ts1:typeseq; tname:identifier;
    begin
      ts:=nil;
      while inch='T' do
      begin
        count:=count+1;
        readch;
        new(ts1);
        ts1^.next:=ts;
        ts:=ts1;
        readname(tname);
        findsort(tname,ts^.thistype)
      end;
    end;

    procedure readrevpartseq(var rulepart:partseq; var count:integer);
    var rulepart1:partseq; argtype:identifier;
    begin
      rulepart:=nil;
      while inch in ['O','A'] do
      begin
        new(rulepart1);
        rulepart1^.next:=rulepart;
        rulepart:=rulepart1;
        if inch='O' then
        begin
          rulepart^.isop:=true;
          readch;
          readname(rulepart^.opsym);
        end
        else
        begin
          count:=count+1;
          rulepart^.isop:=false;
          readch;
          readname(argtype);
          findsort(argtype,rulepart^.argtype);
        end;
      end;
    end;

begin
  readch;
  if inch='B' then
  begin
    readch;
    readnumber(BInum);
    BIstat:=BIstatus(BInum);
  end
  else
    BIstat:=BInone;
  assoc:=inch='T';
  readch;
  comm:=inch='T';
  readch;
  readnumber(precedence);
  readname(ruletype);
  findsort(ruletype,ruletypeid);
  readname(firstop);
  preopcount:=0;
  readrevtypeseq(preop,preopcount);
  postopcount:=0;
  readrevpartseq(rulepart,postopcount);
  if inch='P' then
    readch;
  readrevtypeseq(prefix,postopcount);
  makenewrule(normalrule,ruletypeid,firstop,preop,preopcount,rulepart,prefix,
              postopcount,rule);
  rule^.BIstat:=BIstat;
  rule^.comm:=comm;
  rule^.assoc:=assoc;
  rule^.precedence:=precedence;
end;

procedure loadobject(objname:identifier);

var sortname,incobjname:identifier; dummy,vartype:typeid; lhs,rhs,cond:exp;
    varname,vartypename:identifier; okay:boolean;
    created:boolean; obj:object;

begin
  createobject(objname,created,obj);
  if not created then
  begin
    newobject(obj);
    openinput(objname,objobjdir,okay);
    if not okay then
      errorwith(240,objname)
    else
    begin
      while inch='I' do
      begin
        readch;
        readname(incobjname);
        declareinclusion(obj,incobjname);
        loadobject(incobjname);
      end;
      currentobject:=obj;
      writeln(output,'Loading object ',objname);
      while inch='S' do
      begin
        readch;
        readname(sortname);
        declaresort(sortname,dummy);
      end;
      while inch='R' do
      loadrule;
  
      currentvars:=nil;
      while inch='V' do
      begin
        readch;
        readname(varname);
        readname(vartypename);
        findsort(vartypename,vartype);
        declareobjvar(varname,vartype);
      end;

      newrewritelevel;
      while inch in ['E','C'] do
      begin
        if inch='E' then
        begin
          readch;
          loadprefixexpression(lhs);
          loadprefixexpression(rhs);
          cond:=nil;
        end
        else
        begin
          readch;
          loadprefixexpression(lhs);
          loadprefixexpression(rhs);
          loadprefixexpression(cond);
        end;
        declareequation(lhs,rhs,cond,false,false);
        lastequationlevel:=rewritelevel;
      end;      
      closeinputfile;
      loadtheorems(objname);
    end;
  end
  else
    newobject(obj);
end;

procedure updatetheorems(obj:object);
var oldcurrent:object; oldvars:expseq;
begin
  oldcurrent:=currentobject;
  currentobject:=obj;
  oldvars:=currentvars;
  loadtheorems(obj^.name);
  currentvars:=oldvars;
  currentobject:=oldcurrent;
end;


{*****************************************************************************}
{*************** proof loading and saving ************************************}
{*****************************************************************************}


{to and from variable PROOF}

procedure readblocktype(var kind:blocktype);
begin
  if inch='M' then
    kind:=programblock
  else
  if inch='P' then
    kind:=procedureblock
  else
    kind:=functionblock;
  readch;
end;

procedure readobjectseq(var il:identlist);
begin
  if inch<>'I' then
    il:=nil
  else
  begin
    readch;
    new(il);
    with il^ do
    begin
      readname(name);
      loadobject(name);
      readobjectseq(next);
    end;
  end;
end;

procedure readvariables(var vars:expseq);
var varname,sortname:identifier; sort:typeid;
begin
  currentvars:=nil;
  while inch='V' do
  begin
    readch;
    readname(varname);
    readname(sortname);
    findsort(sortname,sort);
    declarevar(varname,sort);
  end;
  vars:=currentvars;
end;

procedure readproofstatus(var status:proofstatus);
begin
  if inch='U' then
    status:=unproved
  else
  if inch='W' then
    status:=partproved
  else
  if inch='P' then
    status:=proved
  else
    status:=disproved;
  readch;
end;

procedure readproofstep(var p:proofstep; parentptr:proofstep);
begin
  new(p);
  with p^ do
  begin
    loadprefixexpression(vc);
    examined:=false;
    impossible:=false;
    caseeqns:=nil;
    activecases:=nil;
    parent:=parentptr;
    readproofstatus(status);
    if inch='N' then
    begin
      readch;
      kind:=leaf;
    end
    else
    begin
      readch; {C}
      kind:=casestep;
      loadprefixexpression(truecase);
      readproofstep(case1,p);
      readproofstep(case2,p);
    end;
  end;
end;

procedure readvcseq(var vcs:vcseq);
begin
  if inch<>'C' then
    vcs:=nil
  else
  begin
    readch;
    new(vcs);
    with vcs^ do
    begin
      readnumber(line);
      loadprefixexpression(vc);
      readproofstep(vcproof,nil);
      with vcproof^ do
      begin
        newexp(activecases);
        activecases^.args:=nil;
        activecases^.oprule:=truerule;
      end;
      readvcseq(next);
    end;
  end;
end;

procedure readblockseq(var bs:blockseq);
var found:boolean; obj:object;
begin
  if inch<>'B' then
    bs:=nil
  else
  begin
    currentenviron:=builtinenviron;
    readch;
    new(bs);
    with bs^ do
    begin
      readname(name);
      readblocktype(kind);
      readnumber(line);
      readobjectseq(objlist);
      createobject(spaces,found,obj);
      newobject(obj); {for case equations}
      environment:=currentenviron;
      writeln(output,'Loading block ',name);
      readvariables(variables);
      readproofstatus(status);
      readvcseq(vcs);
      readblockseq(next);
    end;
  end;
end;

procedure readproof(var okay:boolean);
var bl:block; ch:char;
begin
  openinput(sourcename,approofdir,okay);
  if not okay then
  begin
    writeln(output,'Can''t open proof file');
    writeln(photo,'Can''t open proof file');
    proof:=nil;
  end
  else
  begin
    writeln(output,'Loading proof ...');
    readblockseq(proof);
    closeinputfile;
    outlineerrors;
  end;
end;


procedure writeblocktype(var kind:blocktype);
begin
  if kind=programblock then
    writechar(proofout,'M')
  else
  if kind=procedureblock then
    writechar(proofout,'P')
  else
    writechar(proofout,'F');
end;

procedure writeidentlist(il:identlist);
begin
  while il<>nil do
  begin
    writechar(proofout,'I');
    writename(proofout,il^.name);
    il:=il^.next;
  end;
end;

procedure writevariables(vars:expseq);
begin
  while vars<>nil do
  begin
    writechar(proofout,'V');
    writename(proofout,vars^.val^.oprule^.firstop);
    writename(proofout,vars^.val^.oprule^.ruletype^.name);
    vars:=vars^.next;
  end;
end;

procedure writeproofstatus(status:proofstatus);
begin
  if status=unproved then
    writechar(proofout,'U')
  else
  if status=partproved then
    writechar(proofout,'W')
  else
  if status=proved then
    writechar(proofout,'P')
  else
    writechar(proofout,'D');
end;

procedure writeproofstep(p:proofstep);
begin
  with p^ do
  begin
    writeprefixexpression(proofout,vc);
    writeproofstatus(status);
    if kind=leaf then
      writechar(proofout,'N')
    else
    begin
      writechar(proofout,'C');
      writeprefixexpression(proofout,truecase);
      writeproofstep(case1);
      writeproofstep(case2);
    end;
  end;
end;

procedure writevcseq(vcs:vcseq);
begin
  while vcs<>nil do
  begin
    writechar(proofout,'C');
    with vcs^ do
    begin
      writenumber(proofout,line);
      writeprefixexpression(proofout,vc);
      writeproofstep(vcproof);
      vcs:=vcs^.next;
    end;
  end;
end;

procedure writeblockseq(bs:blockseq);
begin
  while bs<>nil do
  begin
    writechar(proofout,'B');
    with bs^ do
    begin
      writename(proofout,name);
      writeblocktype(kind);
      writenumber(proofout,line);
      writeidentlist(objlist);
      writevariables(variables);
      writeproofstatus(status);
      writevcseq(vcs);
      bs:=next;
    end;
  end;
  writechar(proofout,'N');
end;

procedure writeproof;
var dummy:boolean;
begin
  writeln(output,'Please wait- proof write in progress');
  openfile(proofout,sourcename,approofdir,false,dummy);
  writeblockseq(proof);
  writeln(output,'Proof state written');
  reset(proofout);
end;


{*****************************************************************************}
{*************** help procedures *********************************************}
{*****************************************************************************}


procedure helpproofstepshow;
begin
writeln(output,'PROOF STEP show: sub commands are (all lower case)');
writeln(output);
writeln(output,'cases                List all active cases');
writeln(output,'equations <op_sym>   List all equations for given outer LHS op');
writeln(output,'help                 Give this information');
writeln(output,'vars                 List all program variables in scope');
writeln(output);
end;

procedure helpproofstep;
begin
writeln(output,'PROOF STEP: commands available are (all lower case)');
writeln(output);
writeln(output,'auto                 Attempt to prove this VC automatically');
writeln(output,'case                 Make this step a proof tree case analysis');
writeln(output,'false                Consider the false case of this case analysis');
writeln(output,'help                 Give this information');
writeln(output,'leaf                 Make this step a proof tree leaf');
writeln(output,'options              Change options');
writeln(output,'quit                 Exit this proof step');
writeln(output,'save                 Save proof state (done on exit anyway)');
writeln(output,'show                 Show variables, cases or equations');
writeln(output,'structure            Give summary of structure of proof of this step');
writeln(output,'theorems             Extend theorems for an OBJ object');
writeln(output,'true                 Consider the true case of this case analysis');
writeln(output,'zap                  quit back to top level');
writeln(output);
end;

procedure helpblock;
begin
writeln(output);
writeln(output,'PROVE BLOCK: commands available are (all lower case)');
writeln(output);
writeln(output,'<number>             Prove the corresponding VC');
writeln(output,'auto                 Attempt to prove this block automatically');
writeln(output,'help                 Give this information');
writeln(output,'options              Change options');
writeln(output,'quit                 Exit this block');
writeln(output,'save                 Save proof state (done on exit anyway)');
writeln(output,'structure            Give summary of structure of proof of block');
writeln(output,'rerun                Re-run proof of block, to update it with new spec');
writeln(output,'zap                  quit back to top level');
writeln(output);
end;

procedure helpblockseq;
begin
writeln(output);
writeln(output,'PROVE BLOCK SEQUENCE: commands available are (all lower case)');
writeln(output);
writeln(output,'<number>             Prove the corresponding block');
writeln(output,'auto                 Attempt to prove all blocks automatically');
writeln(output,'edit                 Edit current program or module');
writeln(output,'help                 Give this information');
writeln(output,'options              Change options');
writeln(output,'quit                 Exit the prover');
writeln(output,'save                 Save proof state (done on exit anyway)');
writeln(output,'structure            Give summary of structure of proof');
writeln(output,'rerun                Re-run proof so far, to update it with new spec');
writeln(output);
end;


{*****************************************************************************}
{*************** proof procedures ********************************************}
{*****************************************************************************}


procedure findblockstatus(b:block);
var v:vcseq; var state:proofstatus;
begin
  v:=b^.vcs;
  if v=nil then
    state:=proved
  else
  begin
    state:=v^.vcproof^.status;
    v:=v^.next;
    while v<>nil do
    begin
      if state<>disproved then
        if v^.vcproof^.status in [proved,unproved] then
        begin
          if v^.vcproof^.status<>state then
            state:=partproved;
        end
        else
          state:=v^.vcproof^.status;
      v:=v^.next;
    end;
  end;
  b^.status:=state;
end;

procedure findproofstatus(var state:proofstatus);
var bl:blockseq;
begin
  bl:=proof;
  if bl=nil then
    state:=proved
  else
  begin
    state:=bl^.status;
    bl:=bl^.next;
    while bl<>nil do
    begin
      if state<>disproved then
        if bl^.status in [proved,unproved] then
        begin
          if bl^.status<>state then
            state:=partproved;
        end
        else
          state:=bl^.status;
      bl:=bl^.next;
    end;
  end;
end;

procedure setstatus(var s:proofstatus; c1,c2:proofstatus);
begin
  if (c1=disproved) or (c2=disproved) then
    s:=disproved
  else
  if (c1=proved) and (c2=proved) then
    s:=proved
  else
    s:=partproved;
end;

procedure outproofstatus(st:proofstatus);
begin
  if st=unproved then
  begin
    write(output,'unproved  ');
    write(photo,'unproved  ')
  end
  else
  if st=partproved then
  begin
    write(output,'part      ');
    write(photo,'part      ')
  end
  else
  if st=proved then
  begin
    write(output,'proved    ');
    write(photo,'proved    ')
  end
  else
  if st=disproved then
  begin
    write(output,'disproved ');
    write(photo,'disproved ');
  end;
end;

procedure addcaseequations(p:proofstep; var continue:boolean);
{assumes p is a case step. 
 declares the case equations for the children. Also creates active case
 expressions for children}

var copytruecase,copyactivecases:exp;

    procedure addtruecaseequation;
    var l,r:exp; eq:boolean;
    begin
      with p^ do
      begin
        make2argexp(andrule,copyactivecases,copytruecase,case1^.activecases);
        eq:=false;
        if truecase^.oprule^.rulesort=eqrule then
          if truecase^.args^.next^.next=nil then
          begin
            copyexp(truecase^.args^.val,l);
            copyexp(truecase^.args^.next^.val,r);
            currentobject^.eqns:=caseeqns; {ie: of parent}
            declareequation(l,r,nil,false,true);
            case1^.caseeqns:=currentobject^.eqns;
            substitute(case1^.vc,l,r);
            eq:=true;
          end;
        if not eq then
        begin
          copyexp(copytruecase,l);
          newexp(r);
          r^.oprule:=truerule;
          r^.args:=nil;
          currentobject^.eqns:=caseeqns; {ie: of parent}
          declareequation(l,r,nil,false,true);
          case1^.caseeqns:=currentobject^.eqns;
          substitute(case1^.vc,l,r);
        end;
      end;
    end;

    procedure addfalsecaseequation;
    var l,r,nottruecase:exp;
    begin
      with p^ do
      begin
        make1argexp(notrule,copytruecase,nottruecase);
        make2argexp(andrule,copyactivecases,nottruecase,case2^.activecases);
        copyexp(copytruecase,l);
        newexp(r);
        r^.oprule:=falserule;
        r^.args:=nil;
        currentobject^.eqns:=caseeqns; {ie: of parent}
        declareequation(l,r,nil,false,true);
        case2^.caseeqns:=currentobject^.eqns;
        substitute(case2^.vc,l,r);
      end;
    end;

begin {addcaseequations}
  with p^ do
  begin
    currentobject^.eqns:=caseeqns;
    copyexp(activecases,copyactivecases);
    copyexp(truecase,copytruecase);
    newrewritelevel;
    addtruecaseequation;
    addfalsecaseequation;
  end;
end;

procedure makenewproofstep(var p:proofstep; e:exp; parentptr:proofstep);
begin
  new(p);
  with p^ do
  begin
    copyexp(e,vc);
    examined:=false;
    impossible:=false;
    caseeqns:=nil;
    activecases:=nil;
    status:=unproved;
    parent:=parentptr;
    kind:=leaf;
  end;
end;

procedure updatestate(p:proofstep; var continue:boolean);

{ To be applied whenever proofstep not previously examined, (eg: on rerun..)
  or if new rewrites may have been added since last examined. }

var completed:boolean; oldseerewrite:boolean; 

begin
  with p^ do
  begin
    if (parent<>nil) then
    begin
      writeln(output,'Simplifying comprehensive case condition ...');
      writeln(photo,'Simplifying comprehensive case condition ...');
      oldseerewrite:=seerewrite;
      seerewrite:=false;
      {NB: simplification must be done in right environment:}
      currentobject^.eqns:=nil; {no case equations}
      simplify(activecases,completed);
      seerewrite:=oldseerewrite;
    end;
    if activecases^.oprule=falserule then
    begin
      impossible:=true;
      status:=proved;
    end
    else
    begin
      writeln(output,'Simplifying proof step VC ...');
      writeln(photo,'Simplifying proof step VC ...');
      currentobject^.eqns:=caseeqns;
      simplify(vc,continue);
      if (vc^.oprule=truerule) then
        status:=proved
      else
      if vc^.oprule=falserule then
        status:=disproved
      else
        status:=partproved;
    end;
    if kind=casestep then
    begin
      if not examined then
        addcaseequations(p,continue);
      if not impossible then
        setstatus(status,case1^.status,case2^.status);
    end;
    examined:=true;
  end;
end;

procedure autoproveproofstep(var p:proofstep; var continue:boolean);
 
    procedure automakecase;
    var casefound:boolean; eqarg,orarg,andarg:expseq; caseexp:exp;
        smallestsize,thissize:integer; thiscase:exp;
    begin
      with p^ do
      begin
        casefound:=false;

        if vc^.oprule=orrule then
        begin

          {first look for a disjunct with no substitutions,
           and which is not a conjunction}
          orarg:=vc^.args;
          while (orarg<>nil) and not casefound do
          begin
            if orarg^.val^.oprule<>andrule then
              if containsvarsandnosubs(orarg^.val) then
              begin
                casefound:=true;
                caseexp:=orarg^.val;
              end;
            orarg:=orarg^.next;
          end;

          {if not found look for disjunct with least number >0, of
           substitution-free conjuncts. Pick one of the conjuncts.}
          if not casefound then
          begin
            orarg:=vc^.args;
            smallestsize:=maxint;
            while (orarg<>nil) do
            begin
              if orarg^.val^.oprule=andrule then
              begin
                andarg:=orarg^.val^.args;
                thissize:=0;
                while (andarg<>nil) do
                begin
                  if containsvarsandnosubs(andarg^.val) then
                  begin
                    thissize:=thissize+1;
                    thiscase:=andarg^.val;
                  end;
                  andarg:=andarg^.next;
                end;
                if (thissize<smallestsize) and (thissize>0) then
                begin
                  casefound:=true;
                  caseexp:=thiscase;
                  smallestsize:=thissize;
                end
              end;
              orarg:=orarg^.next;
            end;
          end;
        end;

      
        if casefound then  {caseexp is pointer to it}
        begin
          kind:=casestep;

          {take " e " if caseexp is: " not(e) "}
          if caseexp^.oprule=notrule then
            caseexp:=caseexp^.args^.val;
          copyexp(caseexp,truecase);

          {swap args if 2 argument equality and lhs is constant}
          with truecase^ do
            if oprule^.rulesort=eqrule then
              if args^.next^.next=nil then
                if constantexpression(args^.val) then {swap over}
                begin
                  ordered:=false;
                  eqarg:=args^.next;
                  args^.next:=eqarg^.next; {nil}
                  eqarg^.next:=args;
                  args:=eqarg;
                end;

          {now add the proof steps}
          writeln(output,'Making case:');
          writeexpression(truecase,0,false);
          writeline;
          makenewproofstep(case1,vc,p);
          makenewproofstep(case2,vc,p);
          addcaseequations(p,continue);
          setstatus(status,case1^.status,case2^.status);
        end;
      end;
    end;
    

begin
  with p^ do
    if status<>proved then
    begin
      updatestate(p,continue);

      if (kind=leaf) and (status=partproved) then
        automakecase;

      if kind=casestep then
      begin
        autoproveproofstep(case1,continue);
        if continue then
          autoproveproofstep(case2,continue);
        setstatus(status,case1^.status,case2^.status);
      end;
    end;
end;

procedure caseshowproofstep(p:proofstep);

const maxcaselevel = 100;

type branchposition=(first,middle,last);

var branchset : set of 1 .. maxcaselevel;

    procedure caseshowproofstep(p:proofstep; level:integer; pos:branchposition);
    var j:integer;

        procedure spacing(level:integer);
        var i,j:integer;
        begin
          for i:= 1 to level do
          begin
            if i>maxcaselevel then
              outchar('|')
            else
            if i in branchset then
              outchar('|')
            else
              outchar(' ');
            for j:=1 to 3 do
              outchar(' ');
          end;
        end;

    begin
      with p^ do
      begin
        if kind=casestep then
          caseshowproofstep(case1,level+1,first);
        if pos=first then
          if level<=maxcaselevel+1 then
            branchset:=branchset+[level];
        spacing(level-1);
        outchar('+');
        for j:=1 to 3 do
          outchar('-');
        if kind=casestep then
        begin
          writeexpression(truecase,0,false);
          writeline;
        end
        else
        begin
          write(output,'Leaf');
          write(photo,'Leaf');
          writeline;
        end;
        if pos=last then
          if level<=maxcaselevel+1 then
            branchset:=branchset-[level];
        spacing(level+1);
        writeline;
        if kind=casestep then
          caseshowproofstep(case2,level+1,last);
      end;
    end;

begin
  branchset:=[];
  caseshowproofstep(p,1,middle);
end;

procedure showstep(p:proofstep);
begin
  with p^ do
  begin
    writeexpression(vc,0,prettyprint);
    writeline;
    writeln(output);
    writeln(photo);
    if kind=casestep then
    begin
      writeln(output,'Case: ');
      writeln(photo,'Case: ');
      writeexpression(truecase,0,false);
      writeline;
      write(output,'True case status: ');
      write(photo,'True case status: ');
      outproofstatus(case1^.status);
      write(output,'      False case status: ');
      write(photo,'      False case status: ');
      outproofstatus(case2^.status);
      writeln(output);
      writeln(output);
      writeln(photo);
      writeln(photo);
    end;
    if impossible then
    begin
      writeln(output,'This case is impossible');
      writeln(photo,'This case is impossible');
    end;
  end;
end;


procedure rerunproofstep(var p:proofstep; outervc:exp; var continue:boolean);
 
begin
  with p^ do
  begin
    copyexp(outervc,vc);
    examined:=false;
    showstep(p);
    updatestate(p,continue);
    if kind=casestep then
    begin
      rerunproofstep(case1,vc,continue);
      if continue then
        rerunproofstep(case2,vc,continue);
      setstatus(status,case1^.status,case2^.status);
    end;
  end;
  writeln(output);
  writeln(photo);
end;

procedure proveproofstep(var p:proofstep; level:integer; var zap:boolean);
var exit:boolean; continue:boolean;

    procedure showcommand;

    const varspell         ='v*ars               ';
          casesspell       ='c*ases              ';
          equationsspell   ='e*quations          ';
          helpspell        ='h*elp               ';

    var what:identifier; eq:eqnlist; vr:expseq;

    begin
      commandprompt:=showwhatprompt;
      getsym;
      while sym=eolnsym do
      begin
        getsym;
        if sym=eolnsym then
          helpproofstepshow;
      end;
      acceptident(what);
      if matchsym(what,varspell) then
      begin
        accepttoeoln;
        vr:=currentvars;
        while vr<>nil do
        begin
          writeln(output,vr^.val^.oprule^.firstop,vr^.val^.oprule^.ruletype^.name);
          writeln(photo,vr^.val^.oprule^.firstop,vr^.val^.oprule^.ruletype^.name);
          vr:=vr^.next;
        end;
      end
      else
      if matchsym(what,casesspell) then
      begin
        accepttoeoln;
        writeln(output,'Case equations:');
        writeln(photo,'Case equations:');
        eq:=currentobject^.eqns;
        while eq<>nil do
        begin
          writeequation(eq);
          eq:=eq^.next;
        end;
        writeln(output,'Comprehensive case condition:');
        writeln(photo,'Comprehensive case condition:');
        writeexpression(p^.activecases,0,false);
        writeline;
      end
      else
      if matchsym(what,equationsspell) then
      begin
        commandprompt:=operatorprompt;
        while sym=eolnsym do
          getsym;
        acceptident(what);
        accepttoeoln;
        writeallequations(what);
      end
      else
      if matchsym(what,helpspell) then
      begin
        accepttoeoln;
        helpproofstepshow;
      end
      else
      begin
        error(243);
        skiptoeoln;
        helpproofstepshow;
      end;
    end;

    procedure makeleaf;
    var discard:boolean;
    begin
      with p^ do
      begin
        getsym;
        accepttoeoln;
        if kind=casestep then
        begin
          writeln(output,'Discard current cases: Are you sure?');
          writeln(photo,'Discard current cases: Are you sure?');
          getyesorno(false,discard);
          if discard then
          begin
            kind:=leaf;
            status:=partproved;
          end;
        end;
      end;
    end;

    procedure makecase;
    var caseexp:exp; newcases:boolean;
    begin
      with p^ do
      begin
        commandprompt:=caseprompt;
        repeat
          getsym;
        until sym<>eolnsym;
        commandprompt:=moreprompt;
        expression1(booltype,caseexp);
        accepttoeoln;
        if not partofexp(errorexp,caseexp) then
        begin
          if kind=casestep then
          begin
            writeln(output,'Discard current cases: Are you sure? (n)');
            writeln(photo,'Discard current cases: Are you sure? (n)');
            getyesorno(false,newcases);
          end
          else
            newcases:=true;
          if newcases then
          begin
            kind:=casestep;
            truecase:=caseexp;
            makenewproofstep(case1,vc,p);
            makenewproofstep(case2,vc,p);
            addcaseequations(p,continue);
            writeln(output,'Simplifying True Case ...');
            updatestate(case1,continue);
            writeln(output,'Simplifying False Case ...');
            updatestate(case2,continue);
            setstatus(status,case1^.status,case2^.status);
            showstep(p);
          end;
        end;
      end;
    end;

    procedure doproofcommand;
    {NB: assume current symbol is end of line, and leave as end of line }

    const
          autospell      ='a*uto               ';
          casespell      ='c*ase               ';
          falsespell     ='f*alse              ';
          helpspell      ='h*elp               ';
          leafspell      ='l*eaf               ';
          optionsspell   ='o*ptions            ';
          photospell     ='p*hoto              ';
          quitspell      ='q*uit               ';
          savespell      ='sa*ve               ';
          structurespell ='st*ructure          ';
          showspell      ='sh*ow               ';
          theoremsspell  ='th*eorems           ';
          truespell      ='tr*ue               ';
          zapspell       ='z*ap                ';


    var   objectname:identifier; obj:object;

    begin
      with p^ do
      begin
        commandprompt:=proveprompt;
        getsym;
        if sym=eofsym then
          exit:=true
        else
        if sym=eolnsym then
          showstep(p)
        else
        if sym<>ident then
        begin
          error(241);
          skiptoeoln;
          helpproofstep;
        end
        else
        begin
          if matchsym(spelling,helpspell) then
          begin
            getsym;
            accepttoeoln;
            helpproofstep;
          end
          else
          if matchsym(spelling,autospell) then
          begin
            getsym;
            accepttoeoln;
            autoproveproofstep(p,continue);
          end
          else
          if matchsym(spelling,casespell) then
            makecase
          else
          if matchsym(spelling,falsespell) then
          begin
            getsym;
            accepttoeoln;
            if kind=casestep then
            begin
              proveproofstep(case2,level+1,zap);
              updatestate(p,continue);
              writeln(output,'Case level: ',level:1);
              writeln(photo,'Case level: ',level:1);
            end;
          end
          else
          if matchsym(spelling,leafspell) then
            makeleaf
          else
          if matchsym(spelling,optionsspell) then
             optionsset
          else
          if matchsym(spelling,photospell) then
            photocommand
          else
          if matchsym(spelling,quitspell) then
          begin
            getsym;
            exit:=true;
            accepttoeoln;
          end
          else
          if matchsym(spelling,savespell) then
          begin
            getsym;
            accepttoeoln;
            writeproof;
          end
          else
          if matchsym(spelling,showspell) then
            showcommand
          else
          if matchsym(spelling,structurespell) then
          begin
            getsym;
            accepttoeoln;
            caseshowproofstep(p);
          end
          else
          if matchsym(spelling,theoremsspell) then
          begin
            commandprompt:=objectprompt;
            getsym;
            while sym=eolnsym do
            begin
              getsym;
              if sym=eolnsym then
                showobjects;
            end;
            acceptident(objectname);
            findobject(objectname,obj);
            accepttoeoln;
            if obj<>nil then
            begin
              DBtheoremsedit(objectname);
              DBtheoremsaccept(objectname);
              updatetheorems(obj);
              updatestate(p,continue);
            end
            else
              errorwith(240,objectname);
          end
          else
          if matchsym(spelling,truespell) then
          begin
            getsym;
            accepttoeoln;
            if kind=casestep then
            begin
              proveproofstep(case1,level+1,zap);
              updatestate(p,continue);
              writeln(output,'Case level: ',level:1);
              writeln(photo,'Case level: ',level:1);
            end;
          end
          else
          if matchsym(spelling,zapspell) then
          begin
            getsym;
            accepttoeoln;
            zap:=true;
          end
          else
          begin
            error(241); {command expected}
            skiptoeoln;
            helpproofstep;
          end;
        end;
      end;
    end;

begin {of proveproofstep }
  with p^ do
  begin
    writeln(output,'Case level: ',level:1);
    writeln(photo,'Case level: ',level:1);
    updatestate(p,continue);
    showstep(p);
    exit:=false;
    while not (exit or zap) do
      doproofcommand;
  end;
end;

procedure caseshowblock(bs:block; var continue:boolean);
var v:vcseq; blockproved:boolean; i:integer; status:proofstatus;
begin
  currentenviron:=bs^.environment;
  currentobject:=currentenviron^.obj; {case equations object}
  currentvars:=bs^.variables;
  v:=bs^.vcs;
  i:=0;
  while (v<>nil) and continue do
  begin
    i:=succ(i);
    writeln(output,'cases of VC ',i:1,' of ',bs^.name);
    writeln(photo,'cases of VC ',i:1,' of ',bs^.name);
    caseshowproofstep(v^.vcproof);
    writeln(output);
    writeln(output,'Continue? (y)');
    writeln(photo);
    writeln(photo,'Continue? (y)');
    getyesorno(true,continue);
    v:=v^.next;
  end;
end;

procedure autoproveblock(bs:block; var continue:boolean);
var v:vcseq; blockproved:boolean; i:integer; status:proofstatus;

begin
  if bs^.status<>proved then
  begin
    currentenviron:=bs^.environment;
    currentobject:=currentenviron^.obj; {case equations object}
    currentvars:=bs^.variables;
    if bs^.status=unproved then
      bs^.status:=partproved;
    v:=bs^.vcs;
    i:=0;
    while continue and (v<>nil) do
    begin
      i:=succ(i);
      writeln(output,'proving VC ',i:1,' of ',bs^.name);
      autoproveproofstep(v^.vcproof,continue);
      write(output,'VC ',i:1,' of ',bs^.name,' ');
      write(photo,'VC ',i:1,' of ',bs^.name,' ');
      outproofstatus(v^.vcproof^.status);
      writeln(output);
      writeln(photo);
      v:=v^.next;
    end;
    v:=bs^.vcs;
    status:=proved;
    while (status<>disproved) and (v<>nil) do
    begin
      if v^.vcproof^.status<>proved then
        status:=v^.vcproof^.status;
      v:=v^.next;
    end;
    bs^.status:=status;
  end;
end;

procedure rerunblock(bs:block; var continue:boolean);
var v:vcseq; blockproved:boolean; i:integer; status:proofstatus;

begin
  currentenviron:=bs^.environment;
  currentobject:=currentenviron^.obj; {case equations object}
  currentvars:=bs^.variables;
  if bs^.status=unproved then
    bs^.status:=partproved;
  v:=bs^.vcs;
  i:=0;
  while continue and (v<>nil) do
  begin
    i:=succ(i);
    writeln(output,'re-running proof of VC ',i:1,' of ',bs^.name);
    writeln(photo,'re-running proof of VC ',i:1,' of ',bs^.name);
    rerunproofstep(v^.vcproof,v^.vc,continue);
    write(output,'VC ',i:1,' of ',bs^.name,' ');
    write(photo,'VC ',i:1,' of ',bs^.name,' ');
    outproofstatus(v^.vcproof^.status);
    writeln(output);
    writeln(photo);
    v:=v^.next;
  end;
  v:=bs^.vcs;
  status:=proved;
  while (status<>disproved) and (v<>nil) do
  begin
    if v^.vcproof^.status<>proved then
      status:=v^.vcproof^.status;
    v:=v^.next;
  end;
  bs^.status:=status;
end;

procedure proveblock(bs:block);
var v:vcseq; i,max,choice:integer; exit:boolean;
    continue:boolean;

    procedure docommand;
    { sym = ident }
    const
          autospell      ='a*uto               ';
          helpspell      ='h*elp               ';
          optionsspell   ='o*ptions            ';
          photospell     ='p*hoto              ';
          quitspell      ='q*uit               ';
          rerunspell     ='r*erun              ';
          savespell      ='sa*ve               ';
          structurespell ='st*ructure          ';
          zapspell       ='z*ap                ';

    var dummy:boolean;

    begin
      if matchsym(spelling,autospell) then
      begin
        getsym;
        accepttoeoln;
        continue:=true;
        autoproveblock(bs,continue);
      end
      else
      if matchsym(spelling,helpspell) then
      begin
        getsym;
        accepttoeoln;
        helpblock;
      end
      else
      if matchsym(spelling,optionsspell) then
        optionsset
      else
      if matchsym(spelling,photospell) then
        photocommand
      else
      if matchsym(spelling,quitspell) then
      begin
        exit:=true;
        getsym;
        accepttoeoln;
      end
      else
      if matchsym(spelling,savespell) then
      begin
        getsym;
        accepttoeoln;
        writeproof;
      end
      else
      if matchsym(spelling,structurespell) then
      begin
        getsym;
        accepttoeoln;
        caseshowblock(bs,dummy);
      end
      else
      if matchsym(spelling,rerunspell) then
      begin
        getsym;
        accepttoeoln;
        continue:=true;
        rerunblock(bs,continue);
      end
      else
      if matchsym(spelling,zapspell) then
      begin
        getsym;
        accepttoeoln;
        exit:=true;
      end
      else
      begin
        error(241);
        skiptoeoln;
        helpblock;
      end;
    end;

begin
  exit:=false;
  currentenviron:=bs^.environment;
  currentobject:=currentenviron^.obj; {case equations}
  currentvars:=bs^.variables;
  repeat
    writeln(output,'VC selection for ',bs^.name);
    writeln(output);
    writeln(photo,'VC selection for ',bs^.name);
    writeln(photo);
    max:=0;
    v:=bs^.vcs;
    if v<>nil then
    begin
      writeln(output,'          Line   Status    ');
      writeln(output);
      writeln(photo,'          Line   Status    ');
      writeln(photo);
    end;
    while v<>nil do
    begin
      max:=succ(max);
      with v^ do
      begin
        write(output,max:3,' ',line:10,'   ');
        write(photo,max:3,' ',line:10,'   ');
        outproofstatus(v^.vcproof^.status);
        writeln(output);
        writeln(photo);
        v:=next;
      end;
    end;
    writeln(output);
    writeln(photo);
    commandprompt:=proveprompt;
    getsym;
    if not (sym in [eofsym,eolnsym]) then
    begin
      if sym=int then
      begin
        choice:=signedval(spelling);
        getsym;
        accepttoeoln;
        if (choice>0) and (choice<=max) then
        begin
          v:=bs^.vcs;
          for i:=1 to choice-1 do
            v:=v^.next;
          proveproofstep(v^.vcproof,0,exit);
          findblockstatus(bs);
        end;
      end
      else
      if sym=ident then
        docommand
      else
      begin
        error(241);
        skiptoeoln;
        helpblock;
      end;
    end;
  until exit or (sym=eofsym);
end;

procedure caseshowblockseq;
var bs:blockseq; continue:boolean;
begin
  continue:=true;
  bs:=proof;
  while (bs<>nil) and continue do
  begin
    writeln(output,'cases of block ',bs^.name);
    writeln(photo,'cases of block ',bs^.name);
    caseshowblock(bs,continue);
    writeln(output);
    writeln(photo);
    bs:=bs^.next;
  end;
end;

procedure autoproveblockseq;
var bs:blockseq; continue:boolean;
begin
  continue:=true;
  bs:=proof;
  while continue and (bs<>nil) do
  begin
    writeln(output,'proving ',bs^.name);
    autoproveblock(bs,continue);
    write(output,'block ',bs^.name);
    write(photo,'block ',bs^.name);
    outproofstatus(bs^.status);
    writeln(output);
    writeln(photo);
    bs:=bs^.next;
  end;
end;

procedure rerunblockseq;
var bs:blockseq; var continue:boolean;
begin
  continue:=true;
  bs:=proof;
  while continue and (bs<>nil) do
  begin
    writeln(output,'re-running proof of ',bs^.name);
    writeln(photo,'re-running proof of ',bs^.name);
    rerunblock(bs,continue);
    write(output,'block ',bs^.name);
    write(photo,'block ',bs^.name);
    outproofstatus(bs^.status);
    writeln(output);
    writeln(photo);
    bs:=bs^.next;
  end;
end;

procedure proveblockseq;
var bs:blockseq; i,max,choice:integer; exit,reedit:boolean;

    procedure docommand;
    { sym = ident }
    const autospell      ='a*uto               ';
          editspell      ='e*dit               ';
          helpspell      ='h*elp               ';
          optionsspell   ='o*ptions            ';
          photospell     ='p*hoto              ';
          quitspell      ='q*uit               ';
          rerunspell     ='r*erun              ';
          savespell      ='sa*ve               ';
          structurespell ='st*ructure        ';

    begin
      if matchsym(spelling,autospell) then
      begin
        getsym;
        accepttoeoln;
        autoproveblockseq;
      end
      else
      if matchsym(spelling,structurespell) then
      begin
        getsym;
        accepttoeoln;
        caseshowblockseq;
      end
      else
      if matchsym(spelling,editspell) then
      begin
        getsym;
        accepttoeoln;
        writeproof;
        repeat
          DBapedit(sourcename);
          DBapaccept(sourcename);
          readproof(okayinput);
          if not okayinput then
          begin
            writeln(output,'No current proof now: re-edit? (y)');
            writeln(photo,'No current proof now: re-edit? (y)');
            getyesorno(true,reedit);
            exit:=not reedit;
          end;
        until okayinput or exit or (sym=eofsym);
      end
      else
      if matchsym(spelling,helpspell) then
      begin
        getsym;
        accepttoeoln;
        helpblockseq;
      end
      else
      if matchsym(spelling,optionsspell) then
        optionsset
      else
      if matchsym(spelling,photospell) then
        photocommand
      else
      if matchsym(spelling,quitspell) then
      begin
        exit:=true;
        getsym;
        accepttoeoln;
      end
      else
      if matchsym(spelling,savespell) then
      begin
        getsym;
        accepttoeoln;
        writeproof;
      end
      else
      if matchsym(spelling,rerunspell) then
      begin
        getsym;
        accepttoeoln;
        rerunblockseq;
      end
      else
      begin
        error(241);
        skiptoeoln;
        helpblockseq;
      end;
    end;

begin {of proveblockseq}
  exit:=false;
  repeat
    writeln(output,'Main menu (block selection)');
    writeln(output);
    writeln(photo,'Main menu (block selection)');
    writeln(photo);
    max:=0;
    bs:=proof;
    if bs<>nil then
    begin
      writeln(output,'    Name                 Type            Line   Status    ');
      writeln(output);
      writeln(photo,'    Name                 Type            Line   Status    ');
      writeln(photo);
    end;
    while bs<>nil do
    begin
      max:=succ(max);
      with bs^ do
      begin
        write(output,max:3,' ',name,' ');
        write(photo,max:3,' ',name,' ');
        if kind=programblock then
        begin
          write(output,'program   ');
          write(photo,'program   ')
        end
        else
        if kind=procedureblock then
        begin
          write(output,'procedure ');
          write(photo,'procedure ')
        end
        else
        begin
          write(output,'function  ');
          write(photo,'function  ');
        end;
        write(output,line:10,'   ');
        write(photo,line:10,'   ');
        outproofstatus(status);
        writeln(output);
        writeln(photo);
        bs:=next;
      end;
    end;
    writeln(output);
    writeln(photo);
    commandprompt:=proveprompt;
    getsym;
    if not (sym in [eofsym,eolnsym]) then
    begin
      if sym=int then
      begin
        choice:=signedval(spelling);
        getsym;
        accepttoeoln;
        if (choice>0) and (choice<=max) then
        begin
          bs:=proof;
          for i:=1 to choice-1 do
            bs:=bs^.next;
          proveblock(bs);
        end;
      end
      else
      if sym=ident then
        docommand
      else
      begin
        error(241);
        skiptoeoln;
        helpblockseq;
      end;
    end;
  until exit or (sym=eofsym);
end;


{*****************************************************************************}
{*************** initialisation and finalisation *****************************}
{*****************************************************************************}


procedure initbuiltins;
var vexp:exp; dummy:boolean;

begin
  newrewritelevel;

{BOOL}

  createobject(boolspell,dummy,currentobject);
  newobject(currentobject);
  declaresort(boolspell,booltype);
  declaresort(errortypespell,errortype);
  declaresort(anytypespell,anytype);

  getnewrule(normalrule,errortype,errorexpspell,nil,0,nil,nil,0,errorrule);

  booltype^.eq^.assoc:=true;
  booltype^.noteq^.assoc:=true;

  getnewrule(normalrule,booltype,subsrulespell,nil,0,nil,nil,0,subsrule);
  {for use with substitutions on general pred }

  makenewrule(normalrule,booltype,tspell,nil,0,nil,nil,0,truerule);
  makenewrule(normalrule,booltype,fspell,nil,0,nil,nil,0,falserule);
  makeprefixrule(notspell,booltype,booltype,notrule);
  notrule^.precedence:=100;
  makeinfixrule(andspell,booltype,booltype,andrule);
  with andrule^ do
  begin
    precedence:=90;
    assoc:=true;
    comm:=true;
  end;
  makeinfixrule(orspell,booltype,booltype,orrule);
  with orrule^ do
  begin
    precedence:=80;
    assoc:=true;
    comm:=true;
  end;
  makeinfixrule(impliesspell,booltype,booltype,imprule);
  imprule^.precedence:=70;

  loadtheorems(boolspell);

  
{INT}

  createobject(intspell,dummy,currentobject);
  newobject(currentobject);
  declaresort(intspell,inttype);
  getnewrule(normalrule,inttype,intrulespell,nil,0,nil,nil,0,intrule);
  { integer constant expression rule }

  makenewrule(normalrule,inttype,zerospell,nil,0,nil,nil,0,zerorule);
  makeprefixrule(succspell,inttype,inttype,succrule);
  succrule^.precedence:=100;
  makeprefixrule(predspell,inttype,inttype,predrule);
  predrule^.precedence:=100;

  loadtheorems(intspell);


{ID}

  createobject(idspell,dummy,currentobject);
  newobject(currentobject);
  declaresort(idspell,idtype);
  makeinfixrule(lessthanspell,idtype,booltype,lessidrule);
  lessidrule^.precedence:=50;

  loadtheorems(idspell);


{OTHERS}

  newexp(errorexp);
  errorexp^.oprule:=errorrule;
  errorexp^.args:=nil;

  builtinenviron:=currentenviron;
end;

procedure initialise;
var ch:char;
begin
  getparam(sourcename);
  initphoto(false);
  initoptions;
  initoutput;
  initissue;
  initlexical;
  initerrors;
  initrecovery;
  initenviron;
  initfiles;
  initrules;
  initbuiltins;
  initsimp;
end;

procedure finalise;
begin
  finalissue;
  finalphoto;
end;


{*****************************************************************************}
{*********** main program ****************************************************}
{*****************************************************************************}


#include "options-procs.i"
#include "photo-procs.i"
#include "prove-nodes-procs.i"
#include "prove-expman-procs.i"
#include "prove-simp-procs.i"
#include "prove-parseexp-procs.i"
#include "prove-lexical-procs.i"


begin
  initialise;  
  readproof(okayinput);
  if okayinput then
  begin
    readapstatus(sourcename,itemstatus);
    proveblockseq;
    if okayinput then {after edit of ap item, it might not be!!}
    begin
      writeproof;
      findproofstatus(proofstate);
      with itemstatus^ do
        case proofstate of
          proved:proof:=provedproof;
          unproved:proof:=vcgproof;
          partproved:proof:=partproof;
          disproved:proof:=disprovedproof;
        end;
      writeapstatus(sourcename,itemstatus);
    end;
  end;
  finalise;
end.