module INT-STACK {

  imports {
    using(INT)
  }
  
  signature {
  
    [ IntStack ]                                 ** piles d'entiers
 
        op new-stack : -> IntStack               ** pile vide
        op push     : Int IntStack -> IntStack   ** empile un entier
	
        op pop      : IntStack     -> IntStack   ** depile 
        op top      : IntStack     -> Int        ** sommet d'une pile

  }
  axioms {

        var s : IntStack                
	var i : Int
	
        eq pop(push(i,s)) = s .
        eq top(push(i,s)) = i .
  }
}



module SYMB-LIST {

  imports {
    using(INT-STACK)
  }
  
  signature {  
  
    [ Symb SymbList ]                            ** symboles et listes de symboles  
    
        op <_>    : Int -> Symb                  ** représentation d'un entier
        ops + - * :     -> Symb                  ** opérateurs arithmétiques

        op []     : -> SymbList                  ** les constructeurs  
        op _::_   : Symb SymbList -> SymbList    ** de listes de symboles

        op eval   : SymbList -> Int                ** évalue une liste de symboles

        op stack-eval : SymbList IntStack -> Int   ** évaluation à l'aide d'une pile 

    }
    axioms {

        var  l    : SymbList        
	vars i j  : Int
        var  p    : IntStack


        eq eval(l) = stack-eval(l, new-stack) .

        eq stack-eval([], p) = top(p) .
	
        eq stack-eval(< i > :: l, p ) = stack-eval(l, push(i,p)) .
	
        eq stack-eval(+ :: l, p )     = stack-eval(l, push(top(p) + top(pop(p)), pop(pop(p)))) .
	
        eq stack-eval(- :: l, p )     = stack-eval(l, push(top(pop(p)) - top(p), pop(pop(p)))) .
	
        eq stack-eval(* :: l, p )     = stack-eval(l, push(top(p) * top(pop(p)), pop(pop(p)))) .



**      une autre façon de spécifier stack-eval :
	
**      eq stack-eval([], push(i,new-stack)) = i .

**      eq stack-eval(< i > :: l, p ) = stack-eval(l, push(i,p)) .
	
**      eq stack-eval(+ :: l, push(i,push(j,p)) )     = stack-eval(l, push(i + j, p)) .
	
**      eq stack-eval(- :: l, push(i,push(j,p)) )     = stack-eval(l, push(j - i, p)) .
	
**      eq stack-eval(* :: l, push(i,push(j,p)) )     = stack-eval(l, push(i * j, p)) .
 	
    }
}


select SYMB-LIST

red eval( < 2 > :: < 3 > :: + :: < 4 > :: * :: < 6 > :: - :: []) .