(* Lists of distinct atoms -- an implementation of sets of atoms. *)

type atomlist =
  | ANil
  | ACons of hd: atom * tl: atomlist where free(hd) # free(tl)

(* Membership test. *)

fun mem accepts x, s produces b
where b -> free(x) <= free(s)
      not b -> free(x) # free(s)
=
  case s of
  | ANil ->
      false
  | ACons (hd, tl) ->
      if x == hd then true else mem(x, tl) end
  end

(* Insertion. *)

fun insert accepts x, s produces t where free(t) == free(x) U free(s) =
  case s of
  | ANil ->
      ACons (x, ANil)
  | ACons (hd, tl) ->
      if x == hd then s else ACons (hd, insert (x, tl)) end
  end

(* Union. *)

fun union accepts s1, s2 produces t where free(t) == free(s1) U free(s2) =
  case s1 of
  | ANil ->
      s2
  | ACons (hd, tl) ->
      union (tl, insert (hd, s2))
  end

(* Removal. *)

fun remove accepts x, s produces t where free(t) == free(s) \ free(x) =
  case s of
  | ANil ->
      ANil
  | ACons (hd, tl) ->
      if x == hd then tl else ACons (hd, remove (x, tl)) end
  end

(* Difference. *)

fun diff accepts s1, s2 produces t where free(t) == free(s1) \ free(s2) =
  case s2 of
  | ANil ->
      s1
  | ACons (hd, tl) ->
      diff (remove (hd, s1), tl)
  end

(* Intersection. *)

fun intersection accepts s1, s2 produces t where free(t) == free(s1) @ free(s2) =
  case s1 of
  | ANil ->
      ANil
  | ACons (hd, tl) ->
      if mem(hd, s2) then
	insert (hd, intersection(tl, s2))
      else
	intersection(tl, s2)
      end
  end

(* Emptiness test. *)

fun is_empty accepts s produces b where b <-> free(s) == empty =
  case s of
  | ANil ->
      true
  | ACons (_, _) ->
      false
  end

(* Choice. *)

fun choice
  accepts s
    where free(s) != empty
  produces x, t
    where free(x) U free(t) == free(s)
      and free(x) # free(t)
=
  case s of
  | ANil ->
      absurd
  | ACons (hd, tl) ->
      hd, tl
  end

(* Terms. *)

type term =
  | Var of atom
  | Abs of < atom * inner term >
  | App of term * term

(* Free variables. *)

fun fv accepts t produces xs where free(xs) == free(t) =
  case t of
  | Var (x) ->
      ACons (x, ANil)
  | Abs (x, t) ->
      remove (x, fv (t))
  | App (t1, t2) ->
      union (fv (t1), fv (t2))
  end

(* A sample loop. *)

fun abstract accepts xs, t produces u where free(u) == free(t) \ free(xs) =
  if is_empty (xs) then
    t
  else
    let x, xs = choice (xs) in
    abstract (xs, Abs (x, t))
  end

fun closeup accepts t produces u where free(u) == empty =
  abstract (fv (t), t)