Safe Haskell | None |
---|---|
Language | Haskell2010 |
This module provides the types and the functions necessary for defining funcons. The package provides a large collection of predefined funcons in Funcons.Core. Module Funcons.Tools provides functions for creating executables.
- data Funcons
- data Values
- = ADTVal Name [Values]
- | Ascii Int
- | Atom String
- | Bit BitVector
- | Char Char
- | ComputationType ComputationTypes
- | Float Float
- | IEEE_Float_32 Float
- | IEEE_Float_64 Double
- | Int Integer
- | List [Values]
- | Map Map
- | Multiset (MultiSet Values)
- | Nat Integer
- | Rational Rational
- | Set Set
- | String String
- | Thunk Funcons
- | EmptyTuple
- | NonEmptyTuple Values Values [Values]
- | Vector Vectors
- data Types
- = ADTs
- | ADT Name [Types]
- | AsciiCharacters
- | Atoms
- | Bits Int
- | BoundedIntegers Integer Integer
- | ComputationTypes
- | EmptyType
- | IEEEFloats IEEEFormats
- | Integers
- | Lists Types
- | Maps Types Types
- | Multisets Types
- | Naturals
- | Rationals
- | Sets Types
- | Strings
- | Thunks ComputationTypes
- | Tuples [TTParam]
- | Types
- | UnicodeCharacters
- | Union Types Types
- | Values
- | Vectors Types
- data ComputationTypes
- data SeqSortOp
- applyFuncon :: Name -> [Funcons] -> Funcons
- list_ :: [Funcons] -> Funcons
- tuple_ :: [Funcons] -> Funcons
- set_ :: [Funcons] -> Funcons
- map_empty_ :: Funcons
- empty_tuple_ :: Funcons
- int_ :: Int -> Funcons
- nat_ :: Int -> Funcons
- string_ :: String -> Funcons
- values_ :: Funcons
- integers_ :: Funcons
- strings_ :: Funcons
- unicode_characters_ :: Funcons
- showValues :: Values -> String
- showFuncons :: Funcons -> String
- showTypes :: Types -> String
- isVal :: Funcons -> Bool
- isString :: Funcons -> Bool
- isInt :: Funcons -> Bool
- isNat :: Funcons -> Bool
- isList :: Funcons -> Bool
- isMap :: Funcons -> Bool
- isType :: Funcons -> Bool
- isVec :: Funcons -> Bool
- isAscii :: Funcons -> Bool
- isChar :: Funcons -> Bool
- isTup :: Funcons -> Bool
- isId :: Funcons -> Bool
- isThunk :: Funcons -> Bool
- downcastValue :: Funcons -> Values
- downcastType :: Funcons -> Types
- downcastValueType :: Values -> Types
- upcastNaturals :: Values -> Values
- upcastIntegers :: Values -> Values
- upcastRationals :: Values -> Values
- upcastUnicode :: Values -> Values
- data EvalFunction
- data Strictness
- type StrictFuncon = [Values] -> Rewrite Rewritten
- type PartiallyStrictFuncon = NonStrictFuncon
- type NonStrictFuncon = [Funcons] -> Rewrite Rewritten
- type ValueOp = StrictFuncon
- type NullaryFuncon = Rewrite Rewritten
- type FunconLibrary = Map Name EvalFunction
- libEmpty :: FunconLibrary
- libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
- libUnions :: [FunconLibrary] -> FunconLibrary
- libFromList :: [(Name, EvalFunction)] -> FunconLibrary
- library :: FunconLibrary
- data MSOS a
- data Rewrite a
- data Rewritten
- rewriteTo :: Funcons -> Rewrite Rewritten
- stepTo :: Funcons -> MSOS Funcons
- compstep :: MSOS Funcons -> Rewrite Rewritten
- rewritten :: Values -> Rewrite Rewritten
- premiseStep :: Funcons -> MSOS Funcons
- premiseEval :: (Values -> Rewrite Rewritten) -> (MSOS Funcons -> MSOS Funcons) -> Funcons -> Rewrite Rewritten
- norule :: Funcons -> Rewrite a
- sortErr :: Funcons -> String -> Rewrite a
- partialOp :: Funcons -> String -> Rewrite a
- type Inherited = Map Name Values
- getInh :: Name -> MSOS Values
- withInh :: Name -> Values -> MSOS a -> MSOS a
- type Mutable = Map Name Values
- getMut :: Name -> MSOS Values
- putMut :: Name -> Values -> MSOS ()
- type Output = Map Name [Values]
- writeOut :: Name -> [Values] -> MSOS ()
- readOut :: Name -> MSOS a -> MSOS (a, [Values])
- type Control = Map Name (Maybe Values)
- raiseSignal :: Name -> Values -> MSOS ()
- receiveSignal :: Name -> MSOS a -> MSOS (a, Maybe Values)
- type Input m = Map Name ([[Values]], Maybe (m Values))
- consumeInput :: Name -> MSOS Values
- withExtraInput :: Name -> [Values] -> MSOS a -> MSOS a
- withExactInput :: Name -> [Values] -> MSOS a -> MSOS a
- data FTerm
- type Env = Map MetaVar Levelled
- emptyEnv :: Map k a
- rewriteTermTo :: FTerm -> Env -> Rewrite Rewritten
- stepTermTo :: FTerm -> Env -> MSOS Funcons
- premise :: FTerm -> FPattern -> Env -> MSOS Env
- withInhTerm :: Name -> FTerm -> Env -> MSOS a -> MSOS a
- getInhPatt :: Name -> VPattern -> Env -> MSOS Env
- putMutTerm :: Name -> FTerm -> Env -> MSOS ()
- getMutPatt :: Name -> VPattern -> Env -> MSOS Env
- writeOutTerm :: Name -> FTerm -> Env -> MSOS ()
- readOutPatt :: Name -> VPattern -> MSOS Env -> MSOS Env
- receiveSignalPatt :: Name -> Maybe VPattern -> MSOS Env -> MSOS Env
- raiseTerm :: Name -> FTerm -> Env -> MSOS ()
- assignInput :: Name -> MetaVar -> Env -> MSOS Env
- withExtraInputTerms :: Name -> [FTerm] -> Env -> MSOS a -> MSOS a
- withExactInputTerms :: Name -> [FTerm] -> Env -> MSOS a -> MSOS a
- evalRules :: [Rewrite Rewritten] -> [MSOS Funcons] -> Rewrite Rewritten
- data SideCondition
- sideCondition :: SideCondition -> Env -> Rewrite Env
- lifted_sideCondition :: SideCondition -> Env -> MSOS Env
- data VPattern
- data FPattern
- vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env
- fsMatch :: [Funcons] -> [FPattern] -> Env -> Rewrite Env
- lifted_vsMatch :: [Values] -> [VPattern] -> Env -> MSOS Env
- lifted_fsMatch :: [Funcons] -> [FPattern] -> Env -> MSOS Env
- rewriteType :: Name -> [Values] -> Rewrite Rewritten
- type EntityDefaults = [EntityDefault]
- data EntityDefault
- = DefMutable Name Funcons
- | DefInherited Name Funcons
- | DefOutput Name
- | DefControl Name
- | DefInput Name
- type TypeEnv = Map Name DataTypeMembers
- data DataTypeMembers = DataTypeMembers [TypeParam] [DataTypeAlt]
- data DataTypeAlt
- typeLookup :: Name -> TypeEnv -> Maybe DataTypeMembers
- typeEnvUnion :: TypeEnv -> TypeEnv -> TypeEnv
- typeEnvUnions :: [TypeEnv] -> TypeEnv
- typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeEnv
- emptyTypeEnv :: TypeEnv
Funcon representation
data Funcons
Internal representation of funcon terms.
The generic constructors FName
and FApp
use names to represent
nullary funcons and applications of funcons to other terms.
Funcon terms are easily created using applyFuncon
or via
the smart constructors exported by Funcons.Core.
data Values
This datatype provides a number of builtin value types.
Composite values are only built up out of other values.
The only exception is Thunk
which stores a thunked computation
(funcon term).
ADTVal Name [Values] | |
Ascii Int | |
Atom String | |
Bit BitVector | |
Char Char | |
ComputationType ComputationTypes | |
Float Float | |
IEEE_Float_32 Float | |
IEEE_Float_64 Double | |
Int Integer | |
List [Values] | |
Map Map | |
Multiset (MultiSet Values) | |
Nat Integer | |
Rational Rational | |
Set Set | |
String String | |
Thunk Funcons | |
EmptyTuple | |
NonEmptyTuple Values Values [Values] | Tuples are split in |
Vector Vectors |
data Types
Representation of builtin types.
ADTs | |
ADT Name [Types] | |
AsciiCharacters | |
Atoms | |
Bits Int | |
BoundedIntegers Integer Integer | |
ComputationTypes | |
EmptyType | |
IEEEFloats IEEEFormats | |
Integers | |
Lists Types | |
Maps Types Types | |
Multisets Types | |
Naturals | |
Rationals | |
Sets Types | |
Strings | |
Thunks ComputationTypes | |
Tuples [TTParam] | Types optionally attached to |
Types | |
UnicodeCharacters | |
Union Types Types | |
Values | |
Vectors Types |
data ComputationTypes
Computation type S=>T reflects a type of term whose given value is of type S and result is of type T.
data SeqSortOp
Postfix operators for specifying sequences.
applyFuncon :: Name -> [Funcons] -> Funcons
Build funcon terms by applying a funcon name to `zero or more' funcon terms. This function is useful for defining smart constructors, e,g,
handle_thrown_ :: [Funcons] -> Funcons handle_thrown_ = applyFuncon "handle-thrown"
or alternatively,
handle_thrown_ :: Funcons -> Funcons -> Funcons handle_thrown_ x y = applyFuncon "handle-thrown" [x,y]
Smart construction of funcon terms
Funcon terms
The empty map as a Funcons
.
Creates an empty tuple as a Values
.
Values
Types
Pretty-print funcon terms
showValues :: Values -> String
Pretty-print a Values
.
showFuncons :: Funcons -> String
Pretty-print a Funcons
.
Is a funcon term a certain value?
Up and downcasting between funcon terms
downcastValue :: Funcons -> Values
Attempt to downcast a funcon term to a value.
downcastType :: Funcons -> Types
Attempt to downcast a funcon term to a type.
downcastValueType :: Values -> Types
Attempt to downcast a value to a type.
upcastNaturals :: Values -> Values
Returns the natural representation of a value if it is a subtype. Otherwise it returns the original value.
upcastIntegers :: Values -> Values
Returns the integer representation of a value if it is a subtype. Otherwise it returns the original value.
upcastRationals :: Values -> Values
Returns the rational representation of a value if it is a subtype. Otherwise it returns the original value.
upcastUnicode :: Values -> Values
Returns the unicode representation of an assci value. Otherwise it returns the original value.
Evaluation functions
data EvalFunction
Evaluation functions capture the operational behaviour of a funcon.
Evaluation functions come in multiple flavours, each with a different
treatment of the arguments of the funcon.
Before the application of an evaluation funcon, any argument may be
evaluated, depending on the Strictness
of the argument.
NonStrictFuncon NonStrictFuncon | Funcons for which arguments are not evaluated. |
StrictFuncon StrictFuncon | Strict funcons whose arguments are evaluated. |
PartiallyStrictFuncon [Strictness] NonStrictFuncon | Funcons for which some arguments are evaluated. |
ValueOp ValueOp | Synonym for |
NullaryFuncon NullaryFuncon | Funcons without any arguments. |
type StrictFuncon = [Values] -> Rewrite Rewritten
Type synonym for the evaluation function of strict funcons.
The evaluation function of a StrictFuncon
receives fully evaluated arguments.
type PartiallyStrictFuncon = NonStrictFuncon
Type synonym for the evaluation function of non-strict funcons.
type NonStrictFuncon = [Funcons] -> Rewrite Rewritten
Type synonym for the evaluation function of fully non-strict funcons.
type ValueOp = StrictFuncon
Type synonym for value operations.
type NullaryFuncon = Rewrite Rewritten
Type synonym for the evaluation functions of nullary funcons.
Funcon libraries
type FunconLibrary = Map Name EvalFunction
A funcon library maps funcon names to their evaluation functions.
Creates an empty FunconLibrary
.
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
Unites two FunconLibrary
s.
libUnions :: [FunconLibrary] -> FunconLibrary
Unites a list of FunconLibrary
s.
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
Creates a FunconLibrary
from a list.
A funcon library with funcons for builtin types.
Implicit & modular propagation of entities
data MSOS a
Monadic type for the propagation of semantic entities and meta-information
on the evaluation of funcons. The meta-information includes a library
of funcons (see FunconLibrary
), a typing environment (see TypeEnv
),
runtime options, etc.
The semantic entities are divided into five classes:
- inherited entities, propagated similar to values of a reader monad.
- mutable entities, propagated similar to values of a state monad.
- output entities, propagation similar to values of a write monad.
- control entities, similar to output entities except only a single control signal can be emitted at once (signals do not form a monoid).
- input entities, propagated like values of a state monad, but access like
value of a reader monad. This package provides simulated input/outout
and real interaction via the
IO
monad. See Funcons.Tools.
For each entity class a map is propagated, mapping entity names to values. This enables modular access to the entities.
data Rewrite a
Monadic type for the implicit propagation of meta-information on
the evaluation of funcon terms (no semantic entities).
It is separated from MSOS
to ensure
that side-effects (access or modification of semantic entities) can not
occur during syntactic rewrites.
data Rewritten
After a term is fully rewritten it is either a value or a term that requires a computational step to proceed. This types forms the interface between syntactic rewrites and computational steps.
Helpers to create rewrites & step rules
rewriteTo :: Funcons -> Rewrite Rewritten
Yield a funcon term as the result of a syntactic rewrite.
This function must be used instead of return
.
The given term is fully rewritten.
stepTo :: Funcons -> MSOS Funcons
Yield a funcon term as the result of an MSOS
computation.
This function must be used instead of return
.
compstep :: MSOS Funcons -> Rewrite Rewritten
Yield an MSOS
computation as a fully rewritten term.
This function must be used in order to access entities in the definition
of funcons.
premiseStep :: Funcons -> MSOS Funcons
Execute a computational step as a premise. The result of the step is the returned funcon term.
premiseEval :: (Values -> Rewrite Rewritten) -> (MSOS Funcons -> MSOS Funcons) -> Funcons -> Rewrite Rewritten
Execute a premise as either a rewrite or a step. Depending on whether rewrites were performed or a step was performed a different continuation is applied (first and second argument). Example usage:
stepScope :: NonStrictFuncon --strict in first argument stepScope [FValue (Map e1), x] = premiseEval x rule1 step1 where rewrite1 v = rewritten v step1 stepX = do Map e0 <- getInh "environment" x' <- withInh "environment" (Map (union e1 e0)) stepX stepTo (scope_ [FValue e1, x'])
norule :: Funcons -> Rewrite a
Yields an error signaling that no rule is applicable. The funcon term argument may be used to provide a useful error message.
sortErr :: Funcons -> String -> Rewrite a
Yields an error signaling that a sort error was encountered.
These errors render a rule inapplicable and a next rule is attempted
when a backtracking procedure like evalRules
is applied.
The funcon term argument may be used to provide a useful error message.
partialOp :: Funcons -> String -> Rewrite a
Yields an error signaling that a partial operation was applied
to a value outside of its domain (e.g. division by zero).
These errors render a rule inapplicable and a next rule is attempted
when a backtracking procedure like evalRules
is applied.
The funcon term argument may be used to provide a useful error message.
Entities and entity access
withInh :: Name -> Values -> MSOS a -> MSOS a
Set the value of an inherited entity.
The new value is only set for MSOS
computation given as a third argument.
readOut :: Name -> MSOS a -> MSOS (a, [Values])
Read the values of a certain output entity. The output is obtained
from the MSOS
computation given as a second argument.
raiseSignal :: Name -> Values -> MSOS ()
Signal a value of some control entity.
receiveSignal :: Name -> MSOS a -> MSOS (a, Maybe Values)
Receive the value of a control entity from a given MSOS
computation.
consumeInput :: Name -> MSOS Values
Consume a single value from the input stream. | Throws an 'unsufficient input' exception, if not enough input is available.
withExtraInput :: Name -> [Values] -> MSOS a -> MSOS a
Provides extra values to a certain input entity, available
to be consumed by the given MSOS
computation argument.
withExactInput :: Name -> [Values] -> MSOS a -> MSOS a
Provides an exact amount of input for some input entity,
that is to be completely consumed by the given MSOS
computation.
If less output is consumed a 'insufficient input consumed' exception
is thrown.
CBS compilation
This section describes functions that extend the interpreter with backtracking and pattern-matching facilities. These functions are developed for compiling CBS funcon specifications to Haskell. To read about CBS we refer to JLAMP2016. The functions can be used for manual development of funcons, although this is not recommended.
Funcon representation with meta-variables
data FTerm
Funcon term representation identical to Funcons
,
but with meta-variables.
Defining rules
premise :: FTerm -> FPattern -> Env -> MSOS Env
Variant of premiseStep
that applies substitute and pattern-matching.
Entity access
withInhTerm :: Name -> FTerm -> Env -> MSOS a -> MSOS a
Variant of withInh
that performs substitution.
putMutTerm :: Name -> FTerm -> Env -> MSOS ()
Variant of putMut
that applies substitution.
writeOutTerm :: Name -> FTerm -> Env -> MSOS ()
Variant of writeOut
that applies substitution.
readOutPatt :: Name -> VPattern -> MSOS Env -> MSOS Env
Variant of readOut
that performs pattern-matching.
receiveSignalPatt :: Name -> Maybe VPattern -> MSOS Env -> MSOS Env
Variant of receiveSignal
that performs pattern-matching.
raiseTerm :: Name -> FTerm -> Env -> MSOS ()
Variant of raiseSignal
that applies substitution.
assignInput :: Name -> MetaVar -> Env -> MSOS Env
Variant of consumeInput
that binds the given MetaVar
to the consumed
value in the given Env
.
withExtraInputTerms :: Name -> [FTerm] -> Env -> MSOS a -> MSOS a
Variant of withExtraInput
that performs substitution.
withExactInputTerms :: Name -> [FTerm] -> Env -> MSOS a -> MSOS a
Variant of withExactInput
that performs substitution.
Backtracking
evalRules :: [Rewrite Rewritten] -> [MSOS Funcons] -> Rewrite Rewritten
Function evalRules
implements a backtracking procedure.
It receives two lists of alternatives as arguments, the first
containing all rewrite rules of a funcon and the second all step rules.
The first successful rule is the only rule fully executed.
A rule is unsuccessful if it throws an exception. Some of these
exceptions (partial operation, sort error or pattern-match failure)
cause the next alternative to be tried. Other exceptions
(different forms of internal errors) will be propagated further.
All side-effects of attempting a rule are discarded when a rule turns
out not to be applicable.
First all rewrite rules are attempted, therefore avoiding performing a step until it is absolutely necessary. This is a valid strategy as valid (I)MSOS rules can be considered in any order.
When no rules are successfully executed to completetion a 'no rule exception' is thrown.
data SideCondition
CSB supports five kinds of side conditions.
Each of the side conditions are explained below.
When a side condition is not accepted an exception is thrown that
is caught by the backtrackign procedure evalRules
.
A value is a ground value if it is not a thunk (and not composed out of
thunks).
SCEquality FTerm FTerm | T1 == T2. Accepted only when T1 and T2 rewrite to equal ground values. |
SCInequality FTerm FTerm | T1 =/= T2. Accepted only when T1 and T2 rewrite to unequal ground values. |
SCIsInSort FTerm FTerm | T1 : T2. Accepted only when T2 rewrites to a type and T1 rewrites to a value of that type. |
SCNotInSort FTerm FTerm | ~(T1 : T2). Accepted only when T2 rewrites to a type and T1 rewrites to a value not of that type. |
SCPatternMatch FTerm VPattern | T = P. Accepted only when T rewrites to a value that matches the pattern P. (May produce new bindings in |
sideCondition :: SideCondition -> Env -> Rewrite Env
Executes a side condition, given an Env
environment, throwing possible exceptions, and
possibly extending the environment.
lifted_sideCondition :: SideCondition -> Env -> MSOS Env
Variant of sideCondition
that is lifted into the MSOS
monad.
Pattern Matching
vsMatch :: [Values] -> [VPattern] -> Env -> Rewrite Env
Matching values with value patterns patterns.
If the list of patterns is a singleton list, then vsMatch
attempts
to match the values as a tuple against the pattern as well.
fsMatch :: [Funcons] -> [FPattern] -> Env -> Rewrite Env
Match a sequence of terms to a sequence of patterns.
Tools for creating interpreters
Helpers for defining evaluation functions.
rewriteType :: Name -> [Values] -> Rewrite Rewritten
Parameterisable evaluation function function for types.
Default entity values
type EntityDefaults = [EntityDefault]
A list of EntityDefault
s is used to declare (and possibly initialise)
entities.
data EntityDefault
Default values of entities can be specified for inherited and mutable entities.
DefMutable Name Funcons | |
DefInherited Name Funcons | |
DefOutput Name | For the purpose of unit-testing it is advised to notify an interpreter of the existence of control, output and input entities as well. |
DefControl Name | |
DefInput Name |
Type environments
type TypeEnv = Map Name DataTypeMembers
The typing environment maps datatype names to their definitions.
data DataTypeMembers
A datatype has `zero or more' type parameters and `zero or more' alternatives.
data DataTypeAlt
An alternative is either a datatype constructor or the inclusion
of some other type. The types are arbitrary funcon terms (with possible
variables) that may require evaluation to be resolved to a Types
.
typeLookup :: Name -> TypeEnv -> Maybe DataTypeMembers
Lookup the definition of a datatype in the typing environment.
typeEnvUnion :: TypeEnv -> TypeEnv -> TypeEnv
Unites two TypeEnv
s.
typeEnvUnions :: [TypeEnv] -> TypeEnv
Unites a list of TypeEnv
s.
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeEnv
Creates a TypeEnv
from a list.
The empty TypeEnv
.