-- Sergio and Michael
-- Tue Apr 12 17:02:35 PDT 2011
-- updated Thu Jul  6 13:01:24 PDT 2017
-- Test module for the production implementation of
-- of a function computing the minimum of a list.

import SetFunctions

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

testGetMin = outND -=- out
           where input = [3,1,2,4,9,5]  --test data
                 outND = getMinND input
                 out   = getMin   input

-- production implementation
getMin (x:xs) = aux x xs
              where aux x [] = x
                    aux x (y:ys) | x <= y = aux x ys
                                 | otherwise = getMin (y:ys)

--prototypical implementation
getMinND l | exists m (\m -> m =:= elemOf l &>
                not_exists (set1 elemOf l) (\x -> x < m))
           = m
	   where m free

-- accessory functions
withElem e = e:unknown ? unknown:withElem e
elemOf (withElem e) = e


-- Quantification 

exists :: a -> (a -> Bool) -> Bool
exists x f = f x

forall :: Values a -> (a -> Bool) -> Bool
forall s f = foldValues (&&) True (mapValues f s) =:= True

not_exists :: Values a -> (a -> Bool) -> Bool
not_exists s f = foldValues (||) False (mapValues f s) =:= False