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.