(* Lecture 6: Carsten Schuermann
   Signatures and structures 
*)

signature  LIST = 
  sig 
    type 'a list
    
    val empty : 'a list
    val cons  : 'a * 'a list -> 'a list
      
    val append : 'a list -> 'a list -> 'a list 
    val reverse :  'a list -> 'a list
  end



structure List : LIST =
  struct
    datatype 'a list = Empty | Cons  of 'a * 'a list

    val empty = Empty
    val cons = Cons

    (* append L1 L2 = L3 
       Invariant : 
       L3 = L1, L2
    *)
    fun append Empty l2 = l2
      | append (Cons (h, l1')) l2 = Cons (h, append l1' l2)

    (* reverse L1 L2 = L3 
       Invariant : 
       L3 = rev (L1), L2
    *)
    fun reverse' Empty a = a
      | reverse' (Cons (h, l)) a  = reverse' l (Cons (h, a)) 

    (* reverse L = L' 
       Invariant : 
       L' = rev L
    *)
    fun reverse l = reverse' l Empty
  end