Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.ADT.Types

Description

An encoding of the simple type-checking via constraints, following https://microsoft.github.io/z3guide/docs/theories/Datatypes/#using-datatypes-for-solving-type-constraints

Synopsis

data M
- = Var {
  - var :: String
  }
- | Lam {
  - bound :: String
  - body :: M
  }
- | App {
  - fn :: M
  - arg :: M
  }
data T
- = TInt
- | TStr
- | TArr {
  - dom :: T
  - rng :: T
  }
cv2M :: String -> [CV] -> M
_undefiner_M :: a
type SM = SBV M
sVar :: SBV [Char] -> SBV M
sLam :: SBV [Char] -> SBV M -> SBV M
sApp :: SBV M -> SBV M -> SBV M
isVar :: SBV M -> SBool
isLam :: SBV M -> SBool
isApp :: SBV M -> SBool
getVar_1 :: SBV M -> SBV [Char]
svar :: SBV M -> SBV [Char]
getLam_1 :: SBV M -> SBV [Char]
sbound :: SBV M -> SBV [Char]
getLam_2 :: SBV M -> SBV M
sbody :: SBV M -> SBV M
getApp_1 :: SBV M -> SBV M
sfn :: SBV M -> SBV M
getApp_2 :: SBV M -> SBV M
sarg :: SBV M -> SBV M
sCaseM :: Mergeable result => SBV M -> (SBV [Char] -> result) -> (SBV [Char] -> SBV M -> result) -> (SBV M -> SBV M -> result) -> result
cv2T :: String -> [CV] -> T
_undefiner_T :: a
type ST = SBV T
sTInt :: SBV T
sTStr :: SBV T
sTArr :: SBV T -> SBV T -> SBV T
isTInt :: SBV T -> SBool
isTStr :: SBV T -> SBool
isTArr :: SBV T -> SBool
getTArr_1 :: SBV T -> SBV T
sdom :: SBV T -> SBV T
getTArr_2 :: SBV T -> SBV T
srng :: SBV T -> SBV T
sCaseT :: Mergeable result => SBV T -> result -> result -> (SBV T -> SBV T -> result) -> result
env :: SString -> ST
typeOf :: SM -> ST
tc :: SM -> ST -> SBool
wellTyped :: SM -> SBool
idWF :: IO SatResult
intFuncAppString :: IO SatResult
selfAppNotWellTyped :: IO SatResult

Documentation

data M Source #

Simple encoding of untyped lambda terms

Constructors

Var	Variables: `x`
Fields var :: String
Lam
Fields bound :: String Abstraction: `x. M` body :: M
App
Fields fn :: M Application: `M M` arg :: M

Instances

Instances details

Arbitrary M Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods arbitrary :: Gen M # shrink :: M -> [M] #
SymVal M Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV M) Source # mkSymValInit :: State -> SBV M -> IO () Source # literal :: M -> SBV M Source # fromCV :: CV -> M Source # isConcretely :: SBV M -> (M -> Bool) -> Bool Source # minMaxBound :: Maybe (M, M) Source # free :: MonadSymbolic m => String -> m (SBV M) Source # free_ :: MonadSymbolic m => m (SBV M) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV M] Source # symbolic :: MonadSymbolic m => String -> m (SBV M) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV M] Source # unliteral :: SBV M -> Maybe M Source # unlitCV :: SBV M -> Maybe (Kind, CVal) Source # isConcrete :: SBV M -> Bool Source # isSymbolic :: SBV M -> Bool Source #
HasKind M Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods kindOf :: M -> Kind Source # hasSign :: M -> Bool Source # intSizeOf :: M -> Int Source # isBoolean :: M -> Bool Source # isBounded :: M -> Bool Source # isReal :: M -> Bool Source # isFloat :: M -> Bool Source # isDouble :: M -> Bool Source # isRational :: M -> Bool Source # isFP :: M -> Bool Source # isUnbounded :: M -> Bool Source # isADT :: M -> Bool Source # isChar :: M -> Bool Source # isString :: M -> Bool Source # isList :: M -> Bool Source # isSet :: M -> Bool Source # isTuple :: M -> Bool Source # isArray :: M -> Bool Source # isRoundingMode :: M -> Bool Source # isUninterpreted :: M -> Bool Source # showType :: M -> String Source #
HasInductionSchema (Forall ta M -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta M -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta M -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

data T Source #

Types.

Constructors

TInt	Integers
TStr	Strings
TArr	Functions: `t -> t`
Fields dom :: T rng :: T

Instances

Instances details

Arbitrary T Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods arbitrary :: Gen T # shrink :: T -> [T] #
SymVal T Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV T) Source # mkSymValInit :: State -> SBV T -> IO () Source # literal :: T -> SBV T Source # fromCV :: CV -> T Source # isConcretely :: SBV T -> (T -> Bool) -> Bool Source # minMaxBound :: Maybe (T, T) Source # free :: MonadSymbolic m => String -> m (SBV T) Source # free_ :: MonadSymbolic m => m (SBV T) Source # mkFreeVars :: MonadSymbolic m => Int -> m [SBV T] Source # symbolic :: MonadSymbolic m => String -> m (SBV T) Source # symbolics :: MonadSymbolic m => [String] -> m [SBV T] Source # unliteral :: SBV T -> Maybe T Source # unlitCV :: SBV T -> Maybe (Kind, CVal) Source # isConcrete :: SBV T -> Bool Source # isSymbolic :: SBV T -> Bool Source #
HasKind T Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods kindOf :: T -> Kind Source # hasSign :: T -> Bool Source # intSizeOf :: T -> Int Source # isBoolean :: T -> Bool Source # isBounded :: T -> Bool Source # isReal :: T -> Bool Source # isFloat :: T -> Bool Source # isDouble :: T -> Bool Source # isRational :: T -> Bool Source # isFP :: T -> Bool Source # isUnbounded :: T -> Bool Source # isADT :: T -> Bool Source # isChar :: T -> Bool Source # isString :: T -> Bool Source # isList :: T -> Bool Source # isSet :: T -> Bool Source # isTuple :: T -> Bool Source # isArray :: T -> Bool Source # isRoundingMode :: T -> Bool Source # isUninterpreted :: T -> Bool Source # showType :: T -> String Source #
HasInductionSchema (Forall ta T -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> SBool) -> ProofObj Source #
SymVal extraT => HasInductionSchema (Forall ta T -> Forall extraS extraT -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> Forall extraS extraT -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #
(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source #
Instance details Defined in Documentation.SBV.Examples.ADT.Types Methods inductionSchema :: (Forall ta T -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2M :: String -> [CV] -> M Source #

Conversion from SMT values to M values.

_undefiner_M :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SM = SBV M Source #

Symbolic version of the type M.

sVar :: SBV [Char] -> SBV M Source #

Symbolic version of the constructor Var.

sLam :: SBV [Char] -> SBV M -> SBV M Source #

Symbolic version of the constructor Lam.

sApp :: SBV M -> SBV M -> SBV M Source #

Symbolic version of the constructor App.

isVar :: SBV M -> SBool Source #

Field recognizer predicate.

isLam :: SBV M -> SBool Source #

Field recognizer predicate.

isApp :: SBV M -> SBool Source #

Field recognizer predicate.

getVar_1 :: SBV M -> SBV [Char] Source #

Field accessor function.

svar :: SBV M -> SBV [Char] Source #

Field accessor function.

getLam_1 :: SBV M -> SBV [Char] Source #

Field accessor function.

sbound :: SBV M -> SBV [Char] Source #

Field accessor function.

getLam_2 :: SBV M -> SBV M Source #

Field accessor function.

sbody :: SBV M -> SBV M Source #

Field accessor function.

getApp_1 :: SBV M -> SBV M Source #

Field accessor function.

sfn :: SBV M -> SBV M Source #

Field accessor function.

getApp_2 :: SBV M -> SBV M Source #

Field accessor function.

sarg :: SBV M -> SBV M Source #

Field accessor function.

sCaseM :: Mergeable result => SBV M -> (SBV [Char] -> result) -> (SBV [Char] -> SBV M -> result) -> (SBV M -> SBV M -> result) -> result Source #

Case analyzer for the type M.

cv2T :: String -> [CV] -> T Source #

Conversion from SMT values to T values.

_undefiner_T :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type ST = SBV T Source #

Symbolic version of the type T.

sTInt :: SBV T Source #

Symbolic version of the constructor TInt.

sTStr :: SBV T Source #

Symbolic version of the constructor TStr.

sTArr :: SBV T -> SBV T -> SBV T Source #

Symbolic version of the constructor TArr.

isTInt :: SBV T -> SBool Source #

Field recognizer predicate.

isTStr :: SBV T -> SBool Source #

Field recognizer predicate.

isTArr :: SBV T -> SBool Source #

Field recognizer predicate.

getTArr_1 :: SBV T -> SBV T Source #

Field accessor function.

sdom :: SBV T -> SBV T Source #

Field accessor function.

getTArr_2 :: SBV T -> SBV T Source #

Field accessor function.

srng :: SBV T -> SBV T Source #

Field accessor function.

sCaseT :: Mergeable result => SBV T -> result -> result -> (SBV T -> SBV T -> result) -> result Source #

Case analyzer for the type T.

env :: SString -> ST Source #

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.

typeOf :: SM -> ST Source #

Use an uninterpreted function to also magically find the type of a term.

tc :: SM -> ST -> SBool Source #

Given a term and a type, check that the term has that type.

wellTyped :: SM -> SBool Source #

Well typedness: If what the typeOf function returns type-checks the term, then a term is well-typed.

idWF :: IO SatResult Source #

Make sure the identity function can be typed.

>>> idWF
Satisfiable. Model:
  env :: String -> T
  env _ = TStr

  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.

intFuncAppString :: IO SatResult Source #

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.

selfAppNotWellTyped :: IO SatResult Source #

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.