disco-0.1.5: Functional programming language for teaching discrete math.
Copyrightdisco team and contributors
LicenseBSD-3-Clause
Maintainerbyorgey@gmail.com
Safe HaskellNone
LanguageHaskell2010

Disco.Value

Description

Disco runtime values and environments.

Synopsis

Values

data Value where Source #

Different types of values which can result from the evaluation process.

Constructors

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 enumerate or count).

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. VFun is only used when enumerating function values in order to decide comparisons at higher-order function types. For example, in order to compare two values of type (Bool -> Bool) -> Bool for equality, we have to enumerate all functions of type Bool -> Bool as VFun values.

We assume that all VFun values are strict, that is, their arguments should be fully evaluated to RNF before being passed to the function.

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.

Bundled Patterns

pattern VNil :: Value

Convenient pattern for the empty list.

pattern VCons :: Value -> Value -> Value

Convenient pattern for list cons.

pattern VFun :: (Value -> Value) -> Value 

Instances

Instances details
Show Value Source # 
Instance details

Defined in Disco.Value

Methods

showsPrec :: Int -> Value -> ShowS #

show :: Value -> String #

showList :: [Value] -> ShowS #

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.

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.

pairv :: (a -> Value) -> (b -> Value) -> (a, b) -> Value Source #

vpair :: (Value -> a) -> (Value -> b) -> Value -> (a, b) Source #

listv :: (a -> Value) -> [a] -> Value Source #

vlist :: (Value -> a) -> Value -> [a] Source #

Props & testing

data ValProp Source #

A ValProp is the normal form of a Disco value of type Prop.

Constructors

VPDone TestResult

A prop that has already either succeeded or failed.

VPSearch SearchMotive [Type] Value TestEnv

A pending search.

Instances

Instances details
Show ValProp Source # 
Instance details

Defined in Disco.Value

data TestResult Source #

The possible outcomes of a proposition.

Instances

Instances details
Show TestResult Source # 
Instance details

Defined in Disco.Value

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.

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

Instances details
Functor TestReason_ Source # 
Instance details

Defined in Disco.Value

Methods

fmap :: (a -> b) -> TestReason_ a -> TestReason_ b #

(<$) :: a -> TestReason_ b -> TestReason_ a #

Foldable TestReason_ Source # 
Instance details

Defined in Disco.Value

Methods

fold :: Monoid m => TestReason_ m -> m #

foldMap :: Monoid m => (a -> m) -> TestReason_ a -> m #

foldMap' :: Monoid m => (a -> m) -> TestReason_ a -> m #

foldr :: (a -> b -> b) -> b -> TestReason_ a -> b #

foldr' :: (a -> b -> b) -> b -> TestReason_ a -> b #

foldl :: (b -> a -> b) -> b -> TestReason_ a -> b #

foldl' :: (b -> a -> b) -> b -> TestReason_ a -> b #

foldr1 :: (a -> a -> a) -> TestReason_ a -> a #

foldl1 :: (a -> a -> a) -> TestReason_ a -> a #

toList :: TestReason_ a -> [a] #

null :: TestReason_ a -> Bool #

length :: TestReason_ a -> Int #

elem :: Eq a => a -> TestReason_ a -> Bool #

maximum :: Ord a => TestReason_ a -> a #

minimum :: Ord a => TestReason_ a -> a #

sum :: Num a => TestReason_ a -> a #

product :: Num a => TestReason_ a -> a #

Traversable TestReason_ Source # 
Instance details

Defined in Disco.Value

Methods

traverse :: Applicative f => (a -> f b) -> TestReason_ a -> f (TestReason_ b) #

sequenceA :: Applicative f => TestReason_ (f a) -> f (TestReason_ a) #

mapM :: Monad m => (a -> m b) -> TestReason_ a -> m (TestReason_ b) #

sequence :: Monad m => TestReason_ (m a) -> m (TestReason_ a) #

Show a => Show (TestReason_ a) Source # 
Instance details

Defined in Disco.Value

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

Instances details
Show SearchType Source # 
Instance details

Defined in Disco.Value

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

Instances details
Show SearchMotive Source # 
Instance details

Defined in Disco.Value

newtype TestVars Source #

A collection of variables that might need to be reported for a test, along with their types and user-legible names.

Constructors

TestVars [(String, Type, Name Core)] 

Instances

Instances details
Show TestVars Source # 
Instance details

Defined in Disco.Value

Semigroup TestVars Source # 
Instance details

Defined in Disco.Value

Monoid TestVars Source # 
Instance details

Defined in Disco.Value

newtype TestEnv Source #

A variable assignment found during a test.

Constructors

TestEnv [(String, Type, Value)] 

Instances

Instances details
Show TestEnv Source # 
Instance details

Defined in Disco.Value

Semigroup TestEnv Source # 
Instance details

Defined in Disco.Value

Monoid TestEnv Source # 
Instance details

Defined in Disco.Value

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.

Environments

type Env = Ctx Core Value Source #

An environment is a mapping from names to values.

Memory

data Cell Source #

Constructors

Blackhole 
E Env Core 
V Value 

Instances

Instances details
Show Cell Source # 
Instance details

Defined in Disco.Value

Methods

showsPrec :: Int -> Cell -> ShowS #

show :: Cell -> String #

showList :: [Cell] -> ShowS #

data Mem Source #

Mem represents a memory, containing Cells

Instances

Instances details
Show Mem Source # 
Instance details

Defined in Disco.Value

Methods

showsPrec :: Int -> Mem -> ShowS #

show :: Mem -> String #

showList :: [Mem] -> ShowS #

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.

set :: Members '[State Mem] r => Int -> Cell -> Sem r () Source #

Set the cell at a given index.

Pretty-printing