-- Example of the non-determinism introduction and elimination pattern
-- Sergio and Michael
-- Fri Mar 11 13:01:12 PST 2011
-- updated Thu Jul  6 12:41:17 PDT 2017

-- Sort using either of two function to compute the minimum of a list
-- The function is selected according to the value of "intro"

{-# OPTIONS_CYMAKE -F --pgmF=currypp #-}

import List

import Test.EasyCheck
-- execute with: curry check min

sort [] mode = []
sort (x:xs) mode = y : sort ys mode
   where y = (if mode then minOfND else minOfD) (x:xs)
         ys = delete y (x:xs)


minOfND :: [a] ->DET a
minOfND l@(x++[min]++y) | (all (min <=) l) = min 

minOfD (x:xs) = aux x xs
   where aux x [] = x
         aux x (y:ys) = aux (min x y) ys

list = [3,1,4,8,1,6] 

prop = sort list True -=- sort list False