(* Author: Carsten Schuermann *)
(* Lecture 8. Lists *)


(* rev : 'a list -> 'a list -> 'a list *)
(* rev (L1, L2) = L3

   Invariant:
   If  L1 is a list
   and L2 is a list
   and L1' is the reverse list of L1
   then L1', L2 = L3
*)

fun rev [] L2 = L2
  | rev (x::L1) L2 = rev L1 (x::L2)

(* append : 'a list -> 'a list -> 'a list *)
(* append (L1, L2) = L3

   Invariant:
   If   L1 is a list
   and  L2 is a list
   the  L3 = L1, L2
*)
fun append [] L2 = L2
  | append (x::L1) L2 = x::(append L1 L2)

(* rev : 'a list -> 'a list *)
(* rev L1 = L2

   Invariant:
   If  L1 is a list
   then L1' = reverse L1
*)
fun rev' [] = []
  | rev' (x::L) =
    let
      val L' = rev' L
    in
      append L' [x]
    end


(* Example:  Trace a function call   rev [1,2,3,4] [] *)


val s1 = rev [1,2,3,4] []
val s2 = rev' [1,2,3,4]