/*
	Arbol
*/

data type ArbolTAD

	type Item      = Integer(int) | MAS | MENOS | POR | ENTRE
	type Arbol     = Vacio | Nodo(Item,Arbol,Arbol)
	type Secuencia = Vacia | Termino(Item,Secuencia)

|[
	var root : Arbol

{inv true}

    fun length : (l : Secuencia) -> int
    { bound l }
    = if l matches
         Vacia         -> 0
       | Termino(i, r) -> 1 + length(r)
      fi

    fun length : (l : Arbol) -> int
    { bound l }
    = if l matches
         Vacio           -> 0
       | Nodo(i, hi, hd) -> 1 + length(hi) max length(hd) 
      fi

	fun concat: (in p:Secuencia, in q:Secuencia) -> Secuencia  {pre true}  {post true} {bound p} 
		= if p matches
			 Vacia         -> q
		   | Termino(i, r) -> Termino(i, concat(r, q))
		  fi

	fun crear: (in it:Item) -> Arbol  {pre true}  {post true}
		= Nodo(it,Vacio,Vacio)

	fun crear: (in it:Item, in lb:Arbol, in rb:Arbol) -> Arbol  {pre true}  {post true}
		= Nodo(it,lb,rb)

	fun esHoja: (in a:Arbol) -> boolean  {pre true}  {post true}
		= if a matches
		     Nodo(_,L,R)         -> L=Vacio /\ R=Vacio 
		   | Vacio               -> false
		  fi
		  
	fun esVacio: (in a:Arbol) -> boolean  {pre true}  {post true}
		= if a matches
			 Nodo(_,_,_) -> false
		   | Vacio       -> true
		  fi

	fun obtRamaIzq: (in a:Arbol) -> Arbol  {pre true}  {post true}
		= if a matches
			 Nodo(_,L,R) -> L
		  fi

	fun obtRamaDer: (in a:Arbol) -> Arbol  {pre true}  {post true}
		= if a matches
			 Nodo(_,L,R) -> R
		  fi

	proc ponRamaIzq: (in left: Arbol, in out a:Arbol)   {pre true}  {post true}
		|[
			if a matches
				Nodo(i,_,R) -> a := Nodo(i,left,R)
			 |	Vacio       -> skip
			fi
		]|

	proc ponRamaDer: (in right: Arbol, in out a:Arbol)   {pre true}  {post true}
		|[
			if a matches
				Nodo(i,L,_) -> a := Nodo(i,L, right)
			 |  Vacio       -> skip
			fi
		]|

	proc writeArbol: (in a:Arbol)   {pre true}  {post true} {bound a }
		|[
			if a matches
				Nodo(i,L,R) -> write("+" + i); writeArbol(L); writeArbol(R)
			 |  Vacio       -> write(".")
			fi
		]|
		
	proc writeSecuencia: (in s:Secuencia)   {pre true}  {post true} {bound s }
		|[
			if s matches
				Termino(i,T) -> write("#" + i); writeSecuencia(T)
			 |  Vacia        -> write(".")
			fi
		]|
		
	fun espejo: (in a:Arbol) -> Arbol   {pre true}  {post true} {bound a }
	= if a matches
			Vacio       -> Vacio
		|	Nodo(i,L,R) -> Nodo(i,espejo(R),espejo(L))
	  fi
		
	fun sonIguales: (in x:Arbol, in y:Arbol) -> boolean   {pre true}  {post true} {bound x }
	= if x matches
			Vacio         -> y = Vacio
		|	Nodo(i,Lx,Rx) -> 
							 if y matches
								Nodo(j,Ly,Ry) -> sonIguales(Lx,Ly) /\ sonIguales(Rx,Ry)
							  | Vacio         -> false
							 fi
	  fi
	  
    fun crearArbolTAD : () -> ArbolTAD = ArbolTAD(Vacio)

	//meth insertar : (in x: int) |[ root := crearArbol(ins(x, arbol)) ]|

	var mytree := crearArbolTAD() : ArbolTAD
	;var A:=Vacio:Arbol
	;var B:=Vacio:Arbol
	;var C:=Vacio:Arbol
	;var D:=Vacio:Arbol
	;var E:=Termino(Integer(1),Termino(Integer(2),Vacia)):Secuencia
	;var F:=Termino(Integer(3),Termino(Integer(4),Termino(Integer(5),Vacia))):Secuencia
	;write(esVacio(C))
	;C := crear(Integer(4))
	;write(esVacio(C))
	;ponRamaIzq(A, C)
	;write(esVacio(C))
	;ponRamaDer(B, C)
	;write(esVacio(C))
	; D := Nodo(Integer(1), Nodo(Integer(2),Nodo(Integer(3),Vacio,Vacio),Vacio),Nodo(Integer(4),Vacio,Nodo(Integer(5),Vacio,Vacio)))
	;write(D)
	;writeArbol(espejo(D))
	;write(sonIguales(A,B))
	;write(sonIguales(C,D))
	;var G:=Vacia:Secuencia
	;G := concat(Vacia,Vacia)
	;writeSecuencia(G)
	;G := concat(F,Vacia)
	;writeSecuencia(F)
	;G := concat(Vacia,F)
	;writeSecuencia(F)
	;G := concat(E,F)
	;writeSecuencia(G)
]|