DataTypes.hs

{-# LANGUAGE ScopedTypeVariables #-}

module Example.Monad.DataTypes where

import Z3.Monad
import Control.Monad.IO.Class (liftIO)

run :: IO ()
run = evalZ3 datatypeScript

mkCellDatatype :: Z3 Sort
mkCellDatatype = do
  -- Create a cell data type of the form:
  -- data Cell = Nil | Cons {car :: Cell, cdr :: Cell}

  -- Nil constructor
  nil <- mkStringSymbol "Nil"
  isNil <- mkStringSymbol "is_Nil"
  nilConst <- mkConstructor nil isNil []

  -- Cons constructor
  car <- mkStringSymbol "car"
  cdr <- mkStringSymbol "cdr"
  cons <- mkStringSymbol "Cons"
  isCons <- mkStringSymbol "is_Cons"
  -- In the following, car and cdr are the field names. The second argument,
  -- their sort, is Nothing, since this is a recursive sort. The third argument is
  -- 0, since the type is not mutually recursive.
  consConst <- mkConstructor cons isCons [(car,Nothing,0),(cdr,Nothing,0)]

  -- Cell datatype
  cell <- mkStringSymbol "Cell"
  mkDatatype cell [nilConst, consConst]

datatypeScript :: Z3 ()
datatypeScript = do
  cell <- mkCellDatatype
  liftIO $ putStrLn "Cell constructors are:"
  [nilConst, consConst] <- getDatatypeSortConstructors cell
  mapM_ (\c -> getDeclName c >>= getSymbolString >>= liftIO . putStrLn) [nilConst, consConst]

  nil <- mkApp nilConst []
  -- t1 = Cons (Nil,Nil)
  t1 <- mkApp consConst [nil, nil]

  liftIO $ putStrLn "prove (nil != cons (nil,nil)) //Expect Unsat"
  p <- (mkEq nil t1 >>= mkNot)
  push
  mkNot p >>= assert
  check >>= liftIO . print
  pop 1

  liftIO $ putStrLn "prove (cons (x,u) = cons(y,v) => x = y && u = v) //Expect Unsat"
  [u,v,x,y] <- mapM (flip mkFreshConst cell) ["u","v","x","y"]
  t1 <- mkApp consConst [x,u]
  t2 <- mkApp consConst [y,v]
  p1 <- mkEq t1 t2
  p2 <- mkEq x y
  p3 <- mkEq u v
  p4 <- mkAnd [p2, p3]
  p5 <- mkImplies p1 p4
  push
  mkNot p5 >>= assert
  check >>= liftIO . print
  pop 1

  liftIO $ putStrLn "we expect a = cons(x, cons(y, nil)), x = y != Nil"

  [isNil, isCons] <- getDatatypeSortRecognizers cell
  [[], [car, cdr]] <- getDatatypeSortConstructorAccessors cell

  a <- mkFreshConst "a" cell
  b <- mkApp cdr [a]
  c <- mkApp cdr [b]

  carA <- mkApp car [a]
  carB <- mkApp car [b]

  push
  mkApp isCons [a] >>= assert
  mkApp isCons [b] >>= assert
  mkApp isNil [c] >>= assert

  mkApp isCons [carA] >>= assert
  mkEq carA carB >>= assert

  (ch, m) <- getModel

  case m of Just m' -> showModel m' >>= liftIO . putStrLn
            otherwise -> liftIO . print $ ch
  pop 1