(* 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)