Copyright | disco team and contributors |
---|---|
License | BSD-3-Clause |
Maintainer | byorgey@gmail.com |
Safe Haskell | None |
Language | Haskell2010 |
Disco runtime values and environments.
Synopsis
- data Value where
- VNum :: RationalDisplay -> Rational -> Value
- VConst :: Op -> Value
- VInj :: Side -> Value -> Value
- VUnit :: Value
- VPair :: Value -> Value -> Value
- VClo :: Env -> [Name Core] -> Core -> Value
- VType :: Type -> Value
- VRef :: Int -> Value
- VFun_ :: ValFun -> Value
- VProp :: ValProp -> Value
- VBag :: [(Value, Integer)] -> Value
- VGraph :: Graph SimpleValue -> Value
- VMap :: Map SimpleValue Value -> Value
- pattern VNil :: Value
- pattern VCons :: Value -> Value -> Value
- pattern VFun :: (Value -> Value) -> Value
- data SimpleValue where
- SNum :: RationalDisplay -> Rational -> SimpleValue
- SUnit :: SimpleValue
- SInj :: Side -> SimpleValue -> SimpleValue
- SPair :: SimpleValue -> SimpleValue -> SimpleValue
- SBag :: [(SimpleValue, Integer)] -> SimpleValue
- SType :: Type -> SimpleValue
- toSimpleValue :: Value -> SimpleValue
- fromSimpleValue :: SimpleValue -> Value
- ratv :: Rational -> Value
- vrat :: Value -> Rational
- intv :: Integer -> Value
- vint :: Value -> Integer
- charv :: Char -> Value
- vchar :: Value -> Char
- enumv :: Enum e => e -> Value
- pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value
- vpair :: (Value -> a) -> (Value -> b) -> Value -> (a, b)
- listv :: (a -> Value) -> [a] -> Value
- vlist :: (Value -> a) -> Value -> [a]
- data ValProp
- data TestResult = TestResult Bool TestReason TestEnv
- data TestReason_ a
- type TestReason = TestReason_ Value
- data SearchType
- newtype SearchMotive where
- SearchMotive (Bool, Bool)
- pattern SMExists :: SearchMotive
- pattern SMForall :: SearchMotive
- newtype TestVars = TestVars [(String, Type, Name Core)]
- newtype TestEnv = TestEnv [(String, Type, Value)]
- emptyTestEnv :: TestEnv
- getTestEnv :: TestVars -> Env -> Either EvalError TestEnv
- extendPropEnv :: TestEnv -> ValProp -> ValProp
- extendResultEnv :: TestEnv -> TestResult -> TestResult
- testIsOk :: TestResult -> Bool
- testIsError :: TestResult -> Bool
- testReason :: TestResult -> TestReason
- testEnv :: TestResult -> TestEnv
- type Env = Ctx Core Value
- data Cell
- data Mem
- emptyMem :: Mem
- allocate :: Members '[State Mem] r => Env -> Core -> Sem r Int
- allocateRec :: Members '[State Mem] r => Env -> [(QName Core, Core)] -> Sem r [Int]
- lkup :: Members '[State Mem] r => Int -> Sem r (Maybe Cell)
- set :: Members '[State Mem] r => Int -> Cell -> Sem r ()
- prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r Doc
- prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc
- prettyTestFailure :: Members '[Input TyDefCtx, LFresh, Reader PA] r => AProperty -> TestResult -> Sem r Doc
- prettyTestResult :: Members '[Input TyDefCtx, LFresh, Reader PA] r => AProperty -> TestResult -> Sem r Doc
Values
Different types of values which can result from the evaluation process.
VNum :: RationalDisplay -> Rational -> Value | A numeric value, which also carries a flag saying how fractional values should be diplayed. |
VConst :: Op -> Value | A built-in function constant. |
VInj :: Side -> Value -> Value | An injection into a sum type. |
VUnit :: Value | The unit value. |
VPair :: Value -> Value -> Value | A pair of values. |
VClo :: Env -> [Name Core] -> Core -> Value | A closure, i.e. a function body together with its environment. |
VType :: Type -> Value | A disco type can be a value. For now, there are only a very
limited number of places this could ever show up (in
particular, as an argument to |
VRef :: Int -> Value | A reference, i.e. a pointer to a memory cell. This is used to implement (optional, user-requested) laziness as well as recursion. |
VFun_ :: ValFun -> Value | A literal function value. We assume that all |
VProp :: ValProp -> Value | A proposition. |
VBag :: [(Value, Integer)] -> Value | A literal bag, containing a finite list of (perhaps only partially evaluated) values, each paired with a count. This is also used to represent sets (with the invariant that all counts are equal to 1). |
VGraph :: Graph SimpleValue -> Value | A graph, stored using an algebraic repesentation. |
VMap :: Map SimpleValue Value -> Value | A map from keys to values. Differs from functions because we can actually construct the set of entries, while functions only have this property when the key type is finite. |
data SimpleValue where Source #
Values which can be used as keys in a map, i.e. those for which a Haskell Ord instance can be easily created. These should always be of a type for which the QSimple qualifier can be constructed. At the moment these are always fully evaluated (containing no indirections) and thus don't need memory management. At some point in the future constructors for simple graphs and simple maps could be created, if the value type is also QSimple. The only reason for actually doing this would be constructing graphs of graphs or maps of maps, or the like.
SNum :: RationalDisplay -> Rational -> SimpleValue | |
SUnit :: SimpleValue | |
SInj :: Side -> SimpleValue -> SimpleValue | |
SPair :: SimpleValue -> SimpleValue -> SimpleValue | |
SBag :: [(SimpleValue, Integer)] -> SimpleValue | |
SType :: Type -> SimpleValue |
Instances
Eq SimpleValue Source # | |
Defined in Disco.Value (==) :: SimpleValue -> SimpleValue -> Bool # (/=) :: SimpleValue -> SimpleValue -> Bool # | |
Ord SimpleValue Source # | |
Defined in Disco.Value compare :: SimpleValue -> SimpleValue -> Ordering # (<) :: SimpleValue -> SimpleValue -> Bool # (<=) :: SimpleValue -> SimpleValue -> Bool # (>) :: SimpleValue -> SimpleValue -> Bool # (>=) :: SimpleValue -> SimpleValue -> Bool # max :: SimpleValue -> SimpleValue -> SimpleValue # min :: SimpleValue -> SimpleValue -> SimpleValue # | |
Show SimpleValue Source # | |
Defined in Disco.Value showsPrec :: Int -> SimpleValue -> ShowS # show :: SimpleValue -> String # showList :: [SimpleValue] -> ShowS # |
toSimpleValue :: Value -> SimpleValue Source #
fromSimpleValue :: SimpleValue -> Value Source #
Conversion
ratv :: Rational -> Value Source #
A convenience function for creating a default VNum
value with a
default (Fractional
) flag.
intv :: Integer -> Value Source #
A convenience function for creating a default VNum
value with a
default (Fractional
) flag.
enumv :: Enum e => e -> Value Source #
Turn any instance of Enum
into a Value
, by creating a
constructor with an index corresponding to the enum value.
Props & testing
A ValProp
is the normal form of a Disco value of type Prop
.
VPDone TestResult | A prop that has already either succeeded or failed. |
VPSearch SearchMotive [Type] Value TestEnv | A pending search. |
data TestResult Source #
The possible outcomes of a proposition.
Instances
Show TestResult Source # | |
Defined in Disco.Value showsPrec :: Int -> TestResult -> ShowS # show :: TestResult -> String # showList :: [TestResult] -> ShowS # |
data TestReason_ a Source #
The possible outcomes of a property test, parametrized over
the type of values. A TestReason
explains why a proposition
succeeded or failed.
TestBool | The prop evaluated to a boolean. |
TestEqual Type a a | The test was an equality test. Records the values being compared and also their type (which is needed for printing). |
TestNotFound SearchType | The search didn't find any examples/counterexamples. |
TestFound TestResult | The search found an example/counterexample. |
TestRuntimeError EvalError | The prop failed at runtime. This is always a failure, no matter which quantifiers or negations it's under. |
Instances
type TestReason = TestReason_ Value Source #
data SearchType Source #
Exhaustive | All possibilities were checked. |
Randomized Integer Integer | A number of small cases were checked exhaustively and then a number of additional cases were checked at random. |
Instances
Show SearchType Source # | |
Defined in Disco.Value showsPrec :: Int -> SearchType -> ShowS # show :: SearchType -> String # showList :: [SearchType] -> ShowS # |
newtype SearchMotive Source #
The answer (success or failure) we're searching for, and
the result (success or failure) we return when we find it.
The motive (False, False)
corresponds to a "forall" quantifier
(look for a counterexample, fail if you find it) and the motive
(True, True)
corresponds to "exists". The other values
arise from negations.
SearchMotive (Bool, Bool) |
pattern SMExists :: SearchMotive | |
pattern SMForall :: SearchMotive |
Instances
Show SearchMotive Source # | |
Defined in Disco.Value showsPrec :: Int -> SearchMotive -> ShowS # show :: SearchMotive -> String # showList :: [SearchMotive] -> ShowS # |
A collection of variables that might need to be reported for a test, along with their types and user-legible names.
A variable assignment found during a test.
extendResultEnv :: TestEnv -> TestResult -> TestResult Source #
testIsOk :: TestResult -> Bool Source #
Whether the property test resulted in success.
testIsError :: TestResult -> Bool Source #
Whether the property test resulted in a runtime error.
testReason :: TestResult -> TestReason Source #
The reason the property test had this result.
testEnv :: TestResult -> TestEnv Source #
Environments
Memory
allocate :: Members '[State Mem] r => Env -> Core -> Sem r Int Source #
Allocate a new memory cell containing an unevaluated expression with the current environment. Return the index of the allocated cell.
allocateRec :: Members '[State Mem] r => Env -> [(QName Core, Core)] -> Sem r [Int] Source #
Allocate new memory cells for a group of mutually recursive bindings, and return the indices of the allocate cells.
lkup :: Members '[State Mem] r => Int -> Sem r (Maybe Cell) Source #
Look up the cell at a given index.
Pretty-printing
prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r Doc Source #