/******************************************************************
 *  (C) Copyright 1994; dit/upm
 *  Distributed under the conditions stated in the
 *  TOPO General Public License (see file LICENSE)
 ******************************************************************
 *  $Log$
 ******************************************************************/

/******************************************************************
 *  
 *  Francisco Monfort Martin
 *  Santiago Pavon Gomez
 *  David Larrabeiti Lopez
 *
 *  3 May 1990
 *
 *  LOTOS data type expressions rewrite system.
 *
 *  Expressions are rewritten by applying recursively One_Rewrite,
 *  which rewrites the most external operation of an expression.
 *
 *  Every operation has attached a set of rewrite rules in the table
 *  of operations.
 *
 *  An operation is rewritten by applying all possible applicable
 *  rewrite rules to that operation.
 *
 *  The subset of applicable rewrite rules is computed by Pattern Matching
 *  of the left hand sides of the rules into the expression, and
 *  rewriting & checking their premises.
 *
 *  A PMT (Pattern Match Tree) is a data structure that must be 
 *  attached to each rule in the table of operations in order to
 *  perform a fast pattern matching.
 *
 *  A rule is applied by substitution of the rhs of that rule in the
 *  expression.  
 *
 *  COMPILATION FLAGS:
 *     SDEBUG : activate debugging
 *
 *  TYPE DEFINITIONS:
 *     PMatchNodeTyp, *PMatchTreeTyp : pattern matching tree type
 *
 *  FUNCTION DEFINITIONS:
 *     InitPMT         : init this module
 *     MakePMT         : build a pmt
 *     FreePMT : free a pmt
 *     StatPMT        : statistics on pmt nodes usage
 *     StatisticPMT        : statistics of a pmt 
 *     One_Rewrite     : rewrite the most external operation of an expression
 *     Rewrite         : rewrite a expression
 *     Evaluate        : evaluate a predicate
 *     FalseIfConst    : transform an expression into FALSE if it is a constant
 *     OneEvaluate     : rewrite the most external operation of a predicate
 *     Rw_Rules        : rewrite rhs and premises of rewrite rules 
 *     Rw_Spec         : rewrite all expressions in the specification
 *  
 *  LOG:
 *     10/06/93. dlarra.
 *     New pattern matching algorithm and new control functions . 
 *
 ******************************************************************/


#ifndef batyperw_H
#define batyperw_H


#include "baexpr.h"
#include "limisc.h"

/* 
 * Pattern Matching tree node
 *
 */

typedef struct pm_node {
  int             name;          /* pattern operation or variable name */
  struct pm_node *son;           /* ok...next */
  struct pm_node *brother;       /* oops...next try */
  ListTyp         appl_rules;    /* pattern matched...applicable rules */ 
} PMatchNodeTyp, *PMatchTreeTyp; /* (the rules are shared with the OpTable) */


/* InitPMT
 * Init this module
 */
extern void InitPMT();


/* MakePMT
 * Take the rewrite rules of an operation as input and
 * return the corresponding pattern match tree
 */
extern PMatchTreeTyp MakePMT( /* rwl */ );
/*       ListTyp rwl; */


/* FreePMT
 * Free a pmt
 */
extern void FreePMT( /* n */ );
/*     PMatchTreeTyp n; */


/* StatPMT
 * pmn_used, pmn_released : pmt nodes used and released
 */
extern void StatPMT( /* pmn_used, pmn_released */ );
/*     int *pmn_used,*pmn_released; */


/* StatisticPMT
 * Number of pmt nodes and list nodes ( of applicable rules ) in a pmt
 */
extern void StatisticPMT( /* pmt, used_pmt, used_ln */ );
/*     PMatchTreeTyp pmt;
       int          *used_pmt, *used_ln; */


/* flag_Rules
 *  TRUE if the rewrite rules table has been already rewritten.
 *  FALSE otherwise.
 * This flag must be set to FALSE when a new specification is loaded.
 */
extern boolean flag_Rules;


/* flag_Beh
 *  TRUE if the expressions in the specification has been already rewritten.
 *  FALSE otherwise.
 * This flag must be set to FALSE when a new specification is loaded.
 */
extern boolean flag_Beh;


/* One_Rewrite
 * Apply all the possible rewrite rules to the most external operation 
 * of the expression exp.
 */
extern boolean One_Rewrite( /* pexp */ );
/*        ExprTyp *pexp; */


/* Rewrite
 * Return the rewritten expression of the expression exp.
 */
extern ExprTyp Rewrite( /* exp */ );
/* ExprTyp  exp; */


/* Evaluate
 * Evaluate (Rewrite) the predicate p.
 * Return 't' if the result is "true.bool", 'f' if it is "false.bool"
 * and 'i' otherwise.
 */
extern char Evaluate( /* pp */ );
/* PredicateTyp  *pp; */


/* FalseIfConst
 * If e is a constant expression then it is rewritten to false.bool
 */
extern ExprTyp FalseIfConst( /* exp */ );
/* ExprTyp exp; */


/* OneEvaluate
 * Evaluate (One_Rewrite) the predicate p.
 * Return 't' if the result is "true.bool", 'f' if it is "false.bool"
 * and 'i' otherwise.
 */
extern char OneEvaluate( /* p */ );
/*        PredicateTyp  p; */


/* Rw_Rules
 * Rewrite the substitution pattern and the premises of all the
 * rewrite rules of all the operators.
 * This function must be called before any rewrite process can be done.
 */
extern void Rw_Rules();


/* Rw_Spec
 * Rewrite all the data value expression in the current specification.
 * This function must be called before any behaviour processing can be done.
 * Rw_Spec calls Rw_Rules() if it is neccesary.
 */
extern void Rw_Spec();


#endif





