juno-compiler/src/IndexedNF.i3

 Copyright (C) 1993, Digital Equipment Corporation                         
 All rights reserved.                                                      
 See the file COPYRIGHT for a full description.                            
                                                                           
 Last modified on Mon Oct 31 09:37:44 PST 1994 by heydon                   


INTERFACE IndexedNF;

IMPORT JunoAST;

TYPE
  T = JunoAST.NormalForm BRANDED "IndexedNF.T" OBJECT
    v_cnt, c_cnt: CARDINAL := 0
  END;

 An IndexNF.T is like a JunoAST.NormalForm, except that the var and
   conj fields may be arrays that are larger than the valid number of
   existential variables and conjuncts stored in it.


   In particular, if nf is a T (indexed normal form), then the valid
   existential variables are stored in nf.var[0..nf.v_cnt-1], and the valid
   conjuncts are stored in nf.conj[0..nf.c_cnt-1]. 


PROCEDURE New(var_cnt, conj_cnt: CARDINAL := 10): T;

 Return a new T from a global avail list. The values var_cnt and
   conj_cnt are hints for the sizes of the existential variable and conjunct
   arrays; the arrays of the result may be smaller or larger than the hints. 

PROCEDURE Dispose(inf: T);

 Return inf to the global avail list. 

PROCEDURE ToNF(inf: T): JunoAST.NormalForm;

 Return a JunoAST.NormalForm equivalent to inf. 

PROCEDURE FromNF(nf: JunoAST.NormalForm; VAR (*INOUT*) res: T);

 Set res to an indexed normal form equivalent to nf. 

PROCEDURE AddVar(VAR (*INOUT*) res: T; var: JunoAST.NearVarLink);

 Append the variable var to the variable list of res. 

PROCEDURE AddConj(VAR (*INOUT*) res: T; conj: JunoAST.Formula);

 Append the formula conj to the conjunction list of res. 

PROCEDURE AddVarList(VAR (*INOUT*) res: T; vars: JunoAST.NearVarList);

 Append the variables vars to the variable list of res. 

PROCEDURE AddConjList(VAR (*INOUT*) res: T; forms: JunoAST.ExprList);

 Append the formulas forms to the conjunction list of res. 

PROCEDURE AddVarArray(VAR (*INOUT*) res: T; READONLY vars: JunoAST.Vars);

 Append the variables vars to the variable list of res. 

PROCEDURE AddConjArray(VAR (*INOUT*) res: T; READONLY forms: JunoAST.Formulas);

 Append the formulas forms to the conjunction list of res. 

END IndexedNF.