/*******************************************************************************/
/* Coq Unit Testing project                                                    */
/* Copyright 2017 Catherine Dubois and Alain Giorgetti                         */
/* Samovar - FEMTO-ST institute                                                */
/*******************************************************************************/
/*      This file is distributed under the terms of the                        */
/*       GNU Lesser General Public License Version 2.1                         */
/*******************************************************************************/

/* File: rom.pl

   Contents: Characterization of terms in correspondence with rooted ordinary maps. */

/* in(K,I,J) holds iff K is in the interval [I..J]. */
in(J,I,J) :- J >= I.
in(K,I,J) :- J > I, J1 is J-1, in(K,I,J1).

/* Definition of ROM terms. */

/* romterm(T,E) iff T is a ROM term of size E. */
romterm(mty,0).
romterm(b(T1,T2),E) :- E > 0, Em1 is E-1, in(E1,0,Em1), E2 is Em1-E1,
 romterm(T1,E1), romterm(T2,E2).
romterm(u(K,T),E) :- E > 0, Em1 is E-1, romterm(T,Em1), 
 Kmax is 2*Em1, in(K,0,Kmax).

/* Functions on ROM terms */

/* nbNodes(T,N) iff N is the number of nodes in the term T. */
nbNodes(mty,0).
nbNodes(b(T1,T2),N) :- nbNodes(T1,N1), nbNodes(T2,N2), N is N1+N2+1.
nbNodes(u(_,T),N) :- nbNodes(T,Nm1), N is Nm1+1.
