-- This program tests whether sharing is correctly implemented
-- The execution of main should give 2 solutions, 0 and 2.
-- Likewise, test should always be True, since main is a
-- double, hence an even value.

-- Sergio Antoy & Michael Hanus
-- Fri Apr  8 09:49:18 PDT 2005

double x = x + x

-- this function non-deterministically returns either 0 or 1
-- when the argument is True.  The value of the argument does
-- not really matter, but it must be evaluated so the term
-- below is cloned.

ndet True = 0 ? 1

-- this function doubles either 0 or 1, the result of ndet, after
-- reducing ndet's argument.  since the argument is
-- non-deterministic, and the term is a non-tree graph, the FLVM
-- must clone a graph preserving the sharing.  

-- The term being cloned is:
--
--                  +
--                 / \
--                 \ /
--                 ndet
--                  |
--                  |
--                  ?
--                 / \
--                /   \
--             False  True

main = double(ndet(False ? True))

test = main `mod` 2 == 0