| Copyright | disco team and contributors |
|---|---|
| License | BSD-3-Clause |
| Maintainer | [email protected] |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Disco.Value
Description
Disco runtime values and environments.
Synopsis
- data Value where
- VNum :: Rational -> Value
- VConst :: Op -> Value
- VInj :: Side -> Value -> Value
- VUnit :: Value
- VPair :: Value -> Value -> Value
- VClo :: Maybe (Int, [Value]) -> 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
- VGen :: StdGen -> Value
- pattern VNil :: Value
- pattern VCons :: Value -> Value -> Value
- pattern VFun :: (Value -> Value) -> Value
- data SimpleValue where
- SNum :: 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
- boolv :: Bool -> Value
- vbool :: Value -> Bool
- 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]
- genv :: StdGen -> Value
- vgen :: Value -> StdGen
- 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
- mergeTestEnv :: TestEnv -> TestEnv -> 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
- resultIsCertain :: TestReason -> Bool
- data LOp
- interpLOp :: LOp -> Bool -> Bool -> Bool
- type Env = Ctx Core Value
- data Cell
- data Mem
- emptyMem :: Mem
- allocate :: Members '[State Mem] r => Env -> Core -> Sem r Int
- allocateValue :: Members '[State Mem] r => Value -> 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)
- memoLookup :: Members '[State Mem] r => Int -> SimpleValue -> Sem r (Maybe Value)
- set :: Members '[State Mem] r => Int -> Cell -> Sem r ()
- memoSet :: Members '[State Mem] r => Int -> SimpleValue -> Value -> Sem r ()
- prettyValue' :: Member (Input TyDefCtx) r => Type -> Value -> Sem r (Doc ann)
- prettyValue :: Members '[Input TyDefCtx, LFresh, Reader PA] r => Type -> Value -> Sem r (Doc ann)
Values
Different types of values which can result from the evaluation process.
Constructors
| VNum :: Rational -> Value | A numeric value. |
| 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 :: Maybe (Int, [Value]) -> 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. |
| VGen :: StdGen -> Value |
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.
Constructors
| SNum :: Rational -> SimpleValue | |
| SUnit :: SimpleValue | |
| SInj :: Side -> SimpleValue -> SimpleValue | |
| SPair :: SimpleValue -> SimpleValue -> SimpleValue | |
| SBag :: [(SimpleValue, Integer)] -> SimpleValue | |
| SType :: Type -> SimpleValue |
Instances
| Show SimpleValue Source # | |
Defined in Disco.Value Methods showsPrec :: Int -> SimpleValue -> ShowS # show :: SimpleValue -> String # showList :: [SimpleValue] -> ShowS # | |
| Eq SimpleValue Source # | |
Defined in Disco.Value | |
| Ord SimpleValue Source # | |
Defined in Disco.Value Methods compare :: SimpleValue -> SimpleValue -> Ordering # (<) :: SimpleValue -> SimpleValue -> Bool # (<=) :: SimpleValue -> SimpleValue -> Bool # (>) :: SimpleValue -> SimpleValue -> Bool # (>=) :: SimpleValue -> SimpleValue -> Bool # max :: SimpleValue -> SimpleValue -> SimpleValue # min :: SimpleValue -> SimpleValue -> SimpleValue # | |
toSimpleValue :: Value -> SimpleValue Source #
fromSimpleValue :: SimpleValue -> Value Source #
Conversion
intv :: Integer -> Value Source #
A convenience function for creating a default VNum value with a
default (Fractional) flag.
Props & testing
A ValProp is the normal form of a Disco value of type Prop.
data TestResult Source #
The possible outcomes of a proposition.
Constructors
| TestResult Bool TestReason TestEnv |
Instances
| Show TestResult Source # | |
Defined in Disco.Value Methods 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.
Constructors
| TestBool | The prop evaluated to a boolean. |
| TestCmp BOp Type a a | The test was a comparison. Records the comparison operator, 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. |
| TestBin LOp TestResult TestResult | A binary logical operator was used to combine the given two results. |
| 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 #
Constructors
| 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 Methods 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.
Constructors
| SearchMotive (Bool, Bool) |
Bundled Patterns
| pattern SMExists :: SearchMotive | |
| pattern SMForall :: SearchMotive |
Instances
| Show SearchMotive Source # | |
Defined in Disco.Value Methods 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 #
resultIsCertain :: TestReason -> Bool Source #
Binary logical operators.
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.