Prototype of GHC.Generics-based declaration of ADTs in Z3

GenericZ3.hs

{-# LANGUAGE DeriveGeneric
           , DefaultSignatures
           , FlexibleInstances
           , FlexibleContexts
           , KindSignatures
           , DataKinds
           , TypeOperators
           , DeriveAnyClass
           , ScopedTypeVariables #-}

module GenericZ3 where

import          GHC.Generics
import          Data.Proxy (Proxy(..))
import          Control.Monad (forM_)
import          Control.Monad.IO.Class (liftIO)

import           Z3.Monad (Z3)
import qualified Z3.Monad as Z3

data IntList
  = Cons { head :: Int, tail :: IntList }
  | Nil
  deriving (Generic)

data Pair a b = First a | Second b
  deriving (Generic)

instance (ToZ3Sort a, ToZ3Sort b) => ToZ3Sort (Pair a b)
instance ToZ3Sort IntList

class ToZ3Sort a where
  toZ3Sort :: Proxy a -> Z3 Z3.Sort

  default toZ3Sort :: (Generic a, GToZ3Sort (Rep a)) => Proxy a -> Z3 Z3.Sort
  toZ3Sort _ = gtoZ3Sort (from (undefined :: a))

instance ToZ3Sort Int where
  toZ3Sort _ = Z3.mkIntSort

instance ToZ3Sort Bool where
  toZ3Sort _ = Z3.mkBoolSort

class GToZ3Sort f where
  gtoZ3Sort :: f a -> Z3 Z3.Sort

instance ToZ3Sort t => GToZ3Sort (Rec0 t) where
  gtoZ3Sort _ = toZ3Sort (Proxy :: Proxy t)

instance (Datatype d, GZ3Constructor f) => GToZ3Sort (D1 d f) where
  gtoZ3Sort m = do
    name <- Z3.mkStringSymbol (datatypeName m)
    cons <- gtoZ3Constructor (undefined :: f a)
    Z3.mkDatatype name cons

class GZ3Constructor f where
  gtoZ3Constructor :: f a -> Z3 [Z3.Constructor]

instance (GZ3Constructor a, GZ3Constructor b) => GZ3Constructor (a :+: b) where
  gtoZ3Constructor _ = (++) <$> gtoZ3Constructor (undefined :: a x) <*> gtoZ3Constructor (undefined :: b x)

instance (Constructor c, GZ3Selector f) => GZ3Constructor (C1 c f) where
  gtoZ3Constructor m = do
    name    <- Z3.mkStringSymbol (conName m)
    recName <- Z3.mkStringSymbol ("is-" ++ conName m)
    sels    <- gtoZ3Selector (undefined :: f a)
    cons    <- Z3.mkConstructor name recName sels
    pure [cons]

class GZ3Selector f where
  gtoZ3Selector :: f a -> Z3 [(Z3.Symbol, Maybe Z3.Sort, Int)]

instance GZ3Selector U1 where
  gtoZ3Selector _ = pure []

instance (GZ3Selector a, GZ3Selector b) => GZ3Selector (a :*: b) where
  gtoZ3Selector _ = (++) <$> gtoZ3Selector (undefined :: a x)
                         <*> gtoZ3Selector (undefined :: b x)

instance (GToZ3Sort f, Selector s) => GZ3Selector (S1 s f) where
  gtoZ3Selector m = do
    name <- Z3.mkStringSymbol (selName m)
    sort <- gtoZ3Sort (undefined :: f a)
    pure [(name, Just sort, 0)]

declareADT :: ToZ3Sort a => Proxy a -> Z3 ()
declareADT proxy = do
  sort <- toZ3Sort proxy
  cons <- Z3.getDatatypeSortConstructors sort
  reco <- Z3.getDatatypeSortRecognizers sort

  sortStr <- Z3.sortToString sort
  consStr <- traverse Z3.funcDeclToString cons
  recoStr <- traverse Z3.funcDeclToString reco

  liftIO $ putStrLn sortStr
  forM_ consStr (liftIO . putStrLn)
  forM_ recoStr (liftIO . putStrLn)

main :: IO ()
main = do
  Z3.evalZ3 $ declareADT (Proxy :: Proxy (Pair Int Bool))