-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.ADT.Types
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- An encoding of the simple type-checking via constraints, following
-- <https://microsoft.github.io/z3guide/docs/theories/Datatypes/#using-datatypes-for-solving-type-constraints>
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE QuasiQuotes       #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeApplications  #-}

module Documentation.SBV.Examples.ADT.Types where

import Data.SBV

-- | Simple encoding of untyped lambda terms
data M = Var { M -> String
var   :: String }     -- ^ Variables: @x@
       | Lam { M -> String
bound :: String       -- ^ Abstraction: @\x. M@
             , M -> M
body :: M
             }
       | App { M -> M
fn  :: M              -- ^ Application: @M M@
             , M -> M
arg :: M
             }

-- | Types.
data T = TInt                        -- ^ Integers
       | TStr                        -- ^ Strings
       | TArr { T -> T
dom :: T, T -> T
rng :: T } -- ^ Functions: @t -> t@

-- | Make terms and types symbolic
mkSymbolic [''M]
mkSymbolic [''T]

-- | Instead of modeling environments for mapping variables to their
-- types, we'll simply use an uninterpreted function. Note that
-- this also implies we consider all terms to be given so that variables
-- do not shadow each other; i.e., all variables are unique. This is
-- a simplification, but it is not without justification: One can 
-- always alpha-rename bound variables so all bound variables are unique.
env :: SString -> ST
env :: SBV String -> ST
env = String -> SBV String -> ST
forall a. SMTDefinable a => String -> a
uninterpret String
"env"

-- | Use an uninterpreted function to also magically find the type of a term.
typeOf :: SM -> ST
typeOf :: SBV M -> ST
typeOf = String -> SBV M -> ST
forall a. SMTDefinable a => String -> a
uninterpret String
"typeOf"

-- | Given a term and a type, check that the term has that type.
tc :: SM -> ST -> SBool
tc :: SBV M -> ST -> SBool
tc = String -> (SBV M -> ST -> SBool) -> SBV M -> ST -> SBool
forall a.
(SMTDefinable a, Typeable a, Lambda Symbolic a) =>
String -> a -> a
smtFunction String
"constraints" ((SBV M -> ST -> SBool) -> SBV M -> ST -> SBool)
-> (SBV M -> ST -> SBool) -> SBV M -> ST -> SBool
forall a b. (a -> b) -> a -> b
$ \SBV M
m ST
t ->
        [sCase|M m of

          -- Var case. The environment must match the type we expect.
          Var s -> env s .== t

          -- Abstraction case. Type must be a function, whose domain matches the variable.
          -- And body much match the range. Note that we can't do a nested scase
          -- here, unfortunately, since custom quasi-quoters do not nest.
          Lam v b
            | isTArr t .&& env v .== sdom t
            -> tc b (srng t)

          -- Application case. In this case, we ask the solver to give us the type of the
          -- function, and then ensure the whole thing is well-formedvx
          App f a -> let tf = typeOf f
                     in   isTArr tf      -- f must have an arrow type
                      .&& tc f tf        -- The function must type-check with that type
                      .&& tc a (sdom tf) -- Argument must have the type of this function
                      .&& t .== srng tf  -- Final result must match the type we're looking for

          -- Otherwise, ill-typed.
          _ -> sFalse
        |]

-- | Well typedness: If what the 'typeOf' function returns type-checks the term,
-- then a term is well-typed.
wellTyped :: SM -> SBool
wellTyped :: SBV M -> SBool
wellTyped SBV M
m = SBV M -> ST -> SBool
tc SBV M
m (SBV M -> ST
typeOf SBV M
m)

-- | Make sure the identity function can be typed.
--
-- >>> idWF
-- Satisfiable. Model:
--   env :: String -> T
--   env _ = TStr
-- <BLANKLINE>
--   typeOf :: M -> T
--   typeOf _ = TArr TStr TStr
--
-- The model is rather uninteresting, but it shows that identity can have the type String to String, where
-- all variables are mapped to Strings.
idWF :: IO SatResult
idWF :: IO SatResult
idWF = SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SBool -> IO SatResult) -> SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ SBV M -> SBool
wellTyped (SBV M -> SBool) -> SBV M -> SBool
forall a b. (a -> b) -> a -> b
$ SBV String -> SBV M -> SBV M
sLam SBV String
x SBV M
vx
  where x :: SBV String
x  = String -> SBV String
forall a. SymVal a => a -> SBV a
literal String
"x"
        vx :: SBV M
vx = SBV String -> SBV M
sVar SBV String
x

-- | Check that if we apply a function that takes n integer to a string is not well-typed.
--
-- >>> intFuncAppString
-- Unsatisfiable
--
-- As expected, the solver says that there's no way to type-check such an expression.
intFuncAppString :: IO SatResult
intFuncAppString :: IO SatResult
intFuncAppString = SymbolicT IO SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
        -- Introduce the constant @plus1 :: Int -> Int@
        SBV M
plus1 <- String -> Symbolic (SBV M)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"plus1"
        SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV M -> ST -> SBool
tc SBV M
plus1 (T -> ST
forall a. SymVal a => a -> SBV a
literal (T
TInt T -> T -> T
`TArr` T
TInt))

        -- Introduce the constant @str :: String@
        SBV M
str <- String -> Symbolic (SBV M)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"str"
        SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SBV M -> ST -> SBool
tc SBV M
str ST
sTStr

        -- Check if the application of plus1 to str can be well-typed
        SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV M -> SBool
wellTyped (SBV M -> SBool) -> SBV M -> SBool
forall a b. (a -> b) -> a -> b
$ SBV M -> SBV M -> SBV M
sApp SBV M
plus1 SBV M
str

-- | Make sure self-application cannot be typed.
--
-- >>> selfAppNotWellTyped
-- Unsatisfiable
--
-- We get unsatisfiable, indicating there's no way to come up with an environment that will
-- successfully assign a type to the term @\x -> x x@.
selfAppNotWellTyped :: IO SatResult
selfAppNotWellTyped :: IO SatResult
selfAppNotWellTyped = SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SBool -> IO SatResult) -> SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ SBV M -> SBool
wellTyped (SBV M -> SBool) -> SBV M -> SBool
forall a b. (a -> b) -> a -> b
$ SBV String -> SBV M -> SBV M
sLam SBV String
x (SBV M -> SBV M -> SBV M
sApp SBV M
vx SBV M
vx)
  where x :: SBV String
x  = String -> SBV String
forall a. SymVal a => a -> SBV a
literal String
"x"
        vx :: SBV M
vx = SBV String -> SBV M
sVar SBV String
x