-- | run tests like this: "solve test2"

import Prelude hiding ( not )

import Satchmo.Boolean hiding ( constant )
import Satchmo.Code

import Satchmo.Binary.Op.Fixed
-- import Satchmo.Binary.Op.Flexible

import Satchmo.Solve


assert_positive x = do 
    n <- constant 0 
    e <- equals n x 
    assert [ not e ]

assert_equals x y = do 
    e <- equals x y 
    assert [ e ]

assert_lt x y = do 
    d <- number $ width y
    assert_positive d
    xd <- add x d
    assert_equals xd y

test1 = do 
    x <- number 4 
    y <- constant 12 
    assert_equals x y
    return $ decode (x,y)

test2 = do 
    x <- constant 3
    y <- constant 9
    z <- add x y
    return $ decode [x,y,z]

test3 = do 
    x <- number 5 
    xx <- add x x
    xxx <- add xx x
    y <- constant 15 
    assert_equals xxx y 
    return $ decode [ x, y ]

test4 = do 
    x <- number  8
    y <- number  8
    xy <- times x y
    z <- constant 63
    assert_equals xy z
    return $ decode [x, y, z]

test5 = do 
    x <- number  10
    y <- number  10
    xy <- times x y
    z <- constant 1001
    assert_equals xy z
    return $ decode [x, y, z]

ramanujan = do
    let bits = 11
    a <- number  bits
    b <- number  bits
    c <- number  bits
    d <- number  bits

    assert_lt a c ; assert_lt c d ; assert_lt d b

    let cube x = do x2 <- times x x ; times x2 x
    a3 <- cube a; b3 <- cube b; ab <- add a3 b3
    c3 <- cube c; d3 <- cube d; cd <- add c3 d3
    assert_equals ab cd

    return $ decode [a,b,c,d]