MODULE IndexedNF;

IMPORT JunoAST;

VAR
  avail := NEW(REF ARRAY OF T, 20);
  next := 0;
  (* The available "T"'s are in "avail[0..next-1]". *)

PROCEDURE New(var_cnt, conj_cnt: CARDINAL := 10): T =
  VAR res: T; BEGIN
    IF next > 0 THEN
      DEC(next);
      res := avail[next];
      res.v_cnt := 0; res.c_cnt := 0;
    ELSE
      res := NEW(T, var := NEW(REF JunoAST.Vars, var_cnt),
        conj := NEW(REF JunoAST.Formulas, conj_cnt))
    END;
    RETURN res
  END New;

PROCEDURE Dispose(inf: T) =
  BEGIN
    IF next > LAST(avail^) THEN
      VAR new := NEW(REF ARRAY OF T, 2 * NUMBER(avail^)); BEGIN
        SUBARRAY(new^, 0, NUMBER(avail^)) := avail^;
        avail := new
      END
    END;
    avail[next] := inf;
    INC(next)
  END Dispose;

PROCEDURE ToNF(inf: T): JunoAST.NormalForm =
  VAR res := NEW(JunoAST.NormalForm, bp := inf.bp); BEGIN
    res.var := NEW(REF JunoAST.Vars, inf.v_cnt);
    res.conj := NEW(REF JunoAST.Formulas, inf.c_cnt);
    res.var^ := SUBARRAY(inf.var^,  0, inf.v_cnt);
    res.conj^ := SUBARRAY(inf.conj^, 0, inf.c_cnt);
    RETURN res
  END ToNF;

PROCEDURE FromNF(nf: JunoAST.NormalForm; VAR (*INOUT*) res: T) =
  BEGIN
    res.bp := nf.bp;
    res.v_cnt := NUMBER(nf.var^);
    res.c_cnt := NUMBER(nf.conj^);
    IF NUMBER(res.var^) < res.v_cnt THEN
      res.var := NEW(REF JunoAST.Vars, 2 * res.v_cnt)
    END;
    SUBARRAY(res.var^, 0, res.v_cnt) := nf.var^;
    IF NUMBER(res.conj^) < res.c_cnt THEN
      res.conj := NEW(REF JunoAST.Formulas, 2 * res.c_cnt)
    END;
    SUBARRAY(res.conj^, 0, res.c_cnt) := nf.conj^
  END FromNF;

PROCEDURE AddVar(VAR (*INOUT*) res: T; var: JunoAST.NearVarLink) =
  BEGIN
    IF res.v_cnt > LAST(res.var^) THEN res.var := DoubleVar(res.var) END;
    res.var[res.v_cnt] := var;
    INC(res.v_cnt)
  END AddVar;

PROCEDURE AddConj(VAR (*INOUT*) res: T; conj: JunoAST.Formula) =
  BEGIN
    IF res.c_cnt > LAST(res.conj^) THEN res.conj := DoubleConj(res.conj) END;
    res.conj[res.c_cnt] := conj;
    INC(res.c_cnt)
  END AddConj;

PROCEDURE AddVarList(VAR (*INOUT*) res: T; vars: JunoAST.NearVarList) =
  BEGIN
    VAR tot := res.v_cnt + vars.size; BEGIN
      IF tot > NUMBER(res.var^) THEN
        res.var := DoubleVar(res.var, 1 + ((tot-1) DIV NUMBER(res.var^)));
        <* ASSERT NUMBER(res.var^) >= tot *>
      END
    END;
    VAR curr := vars.head; BEGIN
      WHILE curr # NIL DO
	res.var[res.v_cnt] := curr;
	INC(res.v_cnt);
	curr := curr.next
      END
    END
  END AddVarList;

PROCEDURE AddConjList(VAR (*INOUT*) res: T; forms: JunoAST.ExprList) =
  BEGIN
    VAR tot := res.c_cnt + forms.size; BEGIN
      IF tot > NUMBER(res.conj^) THEN
        res.conj := DoubleConj(res.conj, 1 + ((tot-1) DIV NUMBER(res.conj^)));
        <* ASSERT NUMBER(res.conj^) >= tot *>
      END
    END;
    VAR curr := forms.head; BEGIN
      WHILE curr # NIL DO
	res.conj[res.c_cnt] := curr.expr;
	INC(res.c_cnt);
	curr := curr.next
      END
    END
  END AddConjList;

PROCEDURE AddVarArray(VAR (*INOUT*) res: T; READONLY vars: JunoAST.Vars) =
  BEGIN
    VAR tot := res.v_cnt + NUMBER(vars); BEGIN
      IF tot > NUMBER(res.var^) THEN
        res.var := DoubleVar(res.var, 1 + ((tot-1) DIV NUMBER(res.var^)));
        <* ASSERT NUMBER(res.var^) >= tot *>
      END
    END;
    FOR i := FIRST(vars) TO LAST(vars) DO
      res.var[res.v_cnt] := vars[i];
      INC(res.v_cnt);
    END
  END AddVarArray;

PROCEDURE AddConjArray(VAR (*INOUT*) res: T; READONLY forms: JunoAST.Formulas)=
  BEGIN
    VAR tot := res.c_cnt + NUMBER(forms); BEGIN
      IF tot > NUMBER(res.conj^) THEN
        res.conj := DoubleConj(res.conj, 1 + ((tot-1) DIV NUMBER(res.conj^)));
        <* ASSERT NUMBER(res.conj^) >= tot *>
      END
    END;
    FOR i := FIRST(forms) TO LAST(forms) DO
      res.conj[res.c_cnt] := forms[i];
      INC(res.c_cnt);
    END
  END AddConjArray;

PROCEDURE DoubleVar(vars: REF JunoAST.Vars; factor := 2):REF JunoAST.Vars =
  VAR res := NEW(REF JunoAST.Vars, factor * NUMBER(vars^)); BEGIN
    SUBARRAY(res^, 0, NUMBER(vars^)) := vars^;
    RETURN res
  END DoubleVar;

PROCEDURE DoubleConj(forms: REF JunoAST.Formulas; factor := 2):
    REF JunoAST.Formulas =
  VAR res := NEW(REF JunoAST.Formulas, factor * NUMBER(forms^)); BEGIN
    SUBARRAY(res^, 0, NUMBER(forms^)) := forms^;
    RETURN res
  END DoubleConj;

BEGIN
END IndexedNF.