mmveri.h

/*****************************************************************************/
/*        Copyright (C) 2005  NORMAN MEGILL  nm at alum.mit.edu              */
/*            License terms:  GNU General Public License                     */
/*****************************************************************************/
/*34567890123456 (79-character line to adjust editor window) 2345678901234567*/

#ifndef METAMATH_MMVERI_H_
#define METAMATH_MMVERI_H_

#include "mmdata.h"

char verifyProof(long statemNum);

/* assignVar() finds an assignment to substScheme variables that match
   the assumptions specified in the reason string */
nmbrString *assignVar(nmbrString *bigSubstSchemeAss,
  nmbrString *bigSubstInstAss, long substScheme,
    /* For error messages: */
  long statementNum, long step, flag unkHypFlag);

/* Deallocate the math symbol strings assigned in wrkProof structure during
   proof verification.  This should be called after verifyProof() and after the
   math symbol strings have been used for proof printouts, etc. */
/* Note that this does NOT free the other allocations in wrkProof.  The
   ERASE command will do this. */
void cleanWrkProof(void);

/* Structure for getting info about a step for SHOW PROOF/STEP command */
/* If getStep.stepNum is nonzero, we should get info about that step. */
/* This structure should be deallocated after use. */
struct getStep_struct {
  long stepNum; /* Step # to get info about */
  long sourceStmt; /* Right side of = in proof display */
  long targetStmt; /* Left side of = in proof display */
  long targetParentStep; /* Step # of target's parent */
  long targetParentStmt; /* Statement # of target's parent */
  nmbrString *sourceHyps; /* List of step #'s */
  nmbrString *sourceSubstsNmbr; /* List of vars w/ ptr to subst math tokens */
  pntrString *sourceSubstsPntr; /* List of vars w/ ptr to subst math tokens */
  nmbrString *targetSubstsNmbr; /* List of vars w/ ptr to subst math tokens */
  pntrString *targetSubstsPntr; /* List of vars w/ ptr to subst math tokens */
};
extern struct getStep_struct getStep;

#endif /* METAMATH_MMVERI_H_ */