-- choose is the basic non-deterministic choice function
choose x  _ = x
choose _  y = y

-- Non-deterministic insertion in a list
insert x []     = [x]
insert x (y:ys) = choose (x:y:ys) (y:insert x ys)

-- Non-deterministic generation of permutations
permut []     = []
permut (x:xs) = insert x (permut xs)

-- In the following definition, 'ys' (i.e. 'permut xs')  
-- is lazily generated, as much as the  filter 'sorted' demands it.
-- The filter may reject 'ys' without fully constructing it.

sort xs = rId sorted (permut xs)

-- restricted identity: rId p x is x if x satisfies (p x)=True
rId :: (a -> Bool) -> a -> a
rId p x | p x = x

-- this version of sort looks simpler but its behavior is not so
-- clear due to the interpretation of where (sharing or not sharing?)
wheresort xs | sorted ys = ys
                      where ys = permut xs


strictsort xs | ys =:= permut xs & sorted ys =:= True  = ys  where ys free

sorted []  = True
sorted [_] = True
sorted (x:y:ys) | x<=y = sorted (y:ys)

goal1 = sort [4,3,2,1]
goal2 = wheresort [4,3,2,1]
goal3 = strictsort [4,3,2,1]



data Nat = o | s Nat

coin = o
coin = s(o)

add o     n = n
add (s m) n = s(add m n)

double x = add x x


goal4 = double coin