Funcons.EDSL

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.

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.

Constructors

FName Name

FApp Name [Funcons]

FSet [Funcons]

FMap [Funcons]

FBinding Funcons [Funcons]

FValue Values

FSortSeq Funcons SeqSortOp

FSortPower Funcons Funcons

FSortUnion Funcons Funcons

FSortInter Funcons Funcons

FSortComplement Funcons

FSortComputes Funcons

FSortComputesFrom Funcons Funcons

Instances

Eq Funcons

Defined in Funcons.Types

Methods

(==) :: Funcons -> Funcons -> Bool

(/=) :: Funcons -> Funcons -> Bool

Ord Funcons

Defined in Funcons.Types

Methods

compare :: Funcons -> Funcons -> Ordering

(<) :: Funcons -> Funcons -> Bool

(<=) :: Funcons -> Funcons -> Bool

(>) :: Funcons -> Funcons -> Bool

(>=) :: Funcons -> Funcons -> Bool

max :: Funcons -> Funcons -> Funcons

min :: Funcons -> Funcons -> Funcons

Read Funcons

Defined in Funcons.Types

Methods

readsPrec :: Int -> ReadS Funcons

readList :: ReadS [Funcons]

readPrec :: ReadPrec Funcons

readListPrec :: ReadPrec [Funcons]

Show Funcons

Defined in Funcons.Types

Methods

showsPrec :: Int -> Funcons -> ShowS

show :: Funcons -> String

showList :: [Funcons] -> ShowS

HasValues Funcons

Defined in Funcons.Types

Methods

project :: Funcons -> Maybe (Values Funcons)

inject :: Values Funcons -> Funcons

type Values = Values Funcons

type Types = Types Funcons

type ComputationTypes = ComputationTypes Funcons

Representation of builtin types.

data SeqSortOp

Postfix operators for specifying sequences.

Constructors

StarOp

PlusOp

QuestionMarkOp

Instances

Eq SeqSortOp

Defined in Funcons.Operations.Values

Methods

(==) :: SeqSortOp -> SeqSortOp -> Bool

(/=) :: SeqSortOp -> SeqSortOp -> Bool

Ord SeqSortOp

Defined in Funcons.Operations.Values

Methods

compare :: SeqSortOp -> SeqSortOp -> Ordering

(<) :: SeqSortOp -> SeqSortOp -> Bool

(<=) :: SeqSortOp -> SeqSortOp -> Bool

(>) :: SeqSortOp -> SeqSortOp -> Bool

(>=) :: SeqSortOp -> SeqSortOp -> Bool

max :: SeqSortOp -> SeqSortOp -> SeqSortOp

min :: SeqSortOp -> SeqSortOp -> SeqSortOp

Read SeqSortOp

Defined in Funcons.Operations.Values

Methods

readsPrec :: Int -> ReadS SeqSortOp

readList :: ReadS [SeqSortOp]

readPrec :: ReadPrec SeqSortOp

readListPrec :: ReadPrec [SeqSortOp]

Show SeqSortOp

Defined in Funcons.Operations.Values

Methods

showsPrec :: Int -> SeqSortOp -> ShowS

show :: SeqSortOp -> String

showList :: [SeqSortOp] -> ShowS

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

app0_ :: ([Funcons] -> Funcons) -> Funcons

app1_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons

app2_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons

app3_ :: ([Funcons] -> Funcons) -> Funcons -> Funcons -> Funcons -> Funcons

Funcon terms

set_ :: [Funcons] -> Funcons

Creates a set of funcon terms.

vec_ :: [Values] -> Funcons

env_fromlist_ :: [(String, Funcons)] -> Funcons

Create an environment from a list of bindings (String to Values) This function has been introduced for easy expression of the semantics of builtin identifiers

null__ :: Values t

Values

int_ :: Int -> Funcons

Creates an integer literal.

bool_ :: Bool -> Funcons

bool__ :: Bool -> Values

list__ :: [Values] -> Values

vector__ :: [Values] -> Values

tuple__ :: [Values] -> Values

char_ :: Char -> Funcons

char__ :: Char -> Values

nat_ :: Int -> Funcons

Creates a natural literal.

float_ :: Double -> Funcons

ieee_float_32_ :: Float -> Funcons

ieee_float_64_ :: Double -> Funcons

string_ :: String -> Funcons

Creates a string literal.

string__ :: String -> Values

atom_ :: String -> Funcons

Creates an atom from a String.

Types

values_ :: Funcons

integers_ :: Funcons

vectors_ :: Types -> Funcons

type_ :: Types -> Funcons

Creates a tuple of funcon terms. tuple_ :: [Funcons] -> Funcons tuple_ = FTuple

ty_star :: Funcons -> Funcons

ty_plus :: Funcons -> Funcons

ty_opt :: Funcons -> Funcons

ty_union :: Funcons -> Funcons -> Funcons

ty_neg :: Funcons -> Funcons

ty_inter :: Funcons -> Funcons -> Funcons

ty_power :: Funcons -> Funcons -> Funcons

Pretty-print funcon terms

showValues :: Values -> String

Pretty-print a Values.

showValuesSeq :: [Values] -> String

Pretty-print a sequence of Values.

showFuncons :: Funcons -> String

Pretty-print a Funcons.

showFunconsSeq :: [Funcons] -> String

Pretty-print a sequence of Funcons.

showTypes :: Types -> String

Pretty-print a Types.

showTerms :: FTerm -> String

showOp :: SeqSortOp -> String

Is a funcon term a certain value?

isVal :: Funcons -> Bool

isInt :: Funcons -> Bool

isNat :: Funcons -> Bool

isList :: Funcons -> Bool

isMap :: Funcons -> Bool

isType :: Funcons -> Bool

isVec :: Funcons -> Bool

isChar :: Funcons -> Bool

isTup :: p -> Bool

isString :: Funcons -> Bool

isString_ :: HasValues t => Values t -> Bool

unString :: HasValues t => Values t -> String

Up and downcasting between funcon terms

downcastValue :: Funcons -> Values

downcastType :: Funcons -> Types

Returns the unicode representation of an assci value. Otherwise it returns the original value.

Attempt to downcast a funcon term to a value.

downcastValueType :: Values t -> Types t

upcastNaturals :: Values t -> Values t

Returns the natural representation of a value if it is a subtype. Otherwise it returns the original value.

upcastIntegers :: Values t -> Values t

Returns the integer representation of a value if it is a subtype. Otherwise it returns the original value.

upcastRationals :: Values t -> Values t

Returns the rational representation of a value if it is a subtype. Otherwise it returns the original value.

upcastCharacter :: HasValues t => Values t -> Maybe Char

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.

Constructors

NonStrictFuncon NonStrictFuncon

Funcons for which arguments are not evaluated.

StrictFuncon StrictFuncon

Strict funcons whose arguments are evaluated.

PartiallyStrictFuncon [Strictness] Strictness NonStrictFuncon

Funcons for which some arguments are evaluated.

ValueOp ValueOp

Synonym for StrictFuncon, for value operations.

NullaryFuncon NullaryFuncon

Funcons without any arguments.

data Strictness

Denotes whether an argument of a funcon should be evaluated or not.

Constructors

Strict

NonStrict

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.

libEmpty :: FunconLibrary

Creates an empty FunconLibrary.

libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary

Unites two FunconLibrarys.

libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary

Right-based union of FunconLibrarys

libUnions :: [FunconLibrary] -> FunconLibrary

Unites a list of FunconLibrarys.

libOverrides :: [FunconLibrary] -> FunconLibrary

Right-based union of list of FunconLibrarys

libFromList :: [(Name, EvalFunction)] -> FunconLibrary

Creates a FunconLibrary from a list.

library :: FunconLibrary

A funcon library with funcons for builtin types.

fromNullaryValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction

fromValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction

fromSeqValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction

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 TypeRelation), 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.

Instances

Monad MSOS

Defined in Funcons.MSOS

Methods

(>>=) :: MSOS a -> (a -> MSOS b) -> MSOS b

(>>) :: MSOS a -> MSOS b -> MSOS b

return :: a -> MSOS a

Functor MSOS

Defined in Funcons.MSOS

Methods

fmap :: (a -> b) -> MSOS a -> MSOS b

(<$) :: a -> MSOS b -> MSOS a

MonadFail MSOS

Defined in Funcons.MSOS

Methods

fail :: String -> MSOS a

Applicative MSOS

Defined in Funcons.MSOS

Methods

pure :: a -> MSOS a

(<*>) :: MSOS (a -> b) -> MSOS a -> MSOS b

liftA2 :: (a -> b -> c) -> MSOS a -> MSOS b -> MSOS c

(*>) :: MSOS a -> MSOS b -> MSOS b

(<*) :: MSOS a -> MSOS b -> MSOS a

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.

Instances

Monad Rewrite

Defined in Funcons.MSOS

Methods

(>>=) :: Rewrite a -> (a -> Rewrite b) -> Rewrite b

(>>) :: Rewrite a -> Rewrite b -> Rewrite b

return :: a -> Rewrite a

Functor Rewrite

Defined in Funcons.MSOS

Methods

fmap :: (a -> b) -> Rewrite a -> Rewrite b

(<$) :: a -> Rewrite b -> Rewrite a

Applicative Rewrite

Defined in Funcons.MSOS

Methods

pure :: a -> Rewrite a

(<*>) :: Rewrite (a -> b) -> Rewrite a -> Rewrite b

liftA2 :: (a -> b -> c) -> Rewrite a -> Rewrite b -> Rewrite c

(*>) :: Rewrite a -> Rewrite b -> Rewrite b

(<*) :: Rewrite a -> Rewrite b -> Rewrite a

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.

Instances

Show Rewritten

Defined in Funcons.MSOS

Methods

showsPrec :: Int -> Rewritten -> ShowS

show :: Rewritten -> String

showList :: [Rewritten] -> ShowS

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.

rewriteSeqTo :: [Funcons] -> Rewrite Rewritten

Yield a sequence of funcon terms as the result of a rewrite. This is only valid when all terms rewrite to a value

stepTo :: Funcons -> MSOS StepRes

Yield a funcon term as the result of an MSOS computation. This function must be used instead of return.

stepSeqTo :: [Funcons] -> MSOS StepRes

Yield a sequence of funcon terms as the result of a computation. This is only valid when all terms rewrite to a value

compstep :: MSOS StepRes -> 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.

rewritten :: Values -> Rewrite Rewritten

Returns a value as a fully rewritten term.

premiseStep :: Funcons -> MSOS StepRes

premiseEval :: ([Values] -> Rewrite Rewritten) -> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten

Execute a premise as either a rewrite or a step. Depending on whether only rewrites are necessary to yield a value, or whether a computational step is necessary, 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   rule1 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

type Inherited = Map Name [Values]

a map storing the values of inherited entities.

getInh :: Name -> MSOS [Values]

Get the value of an inherited entity.

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.

type Mutable = Map Name Values

A map storing the values of mutable entities.

getMut :: Name -> MSOS Values

Get the value of some mutable entity.

putMut :: Name -> Values -> MSOS ()

Set the value of some mutable entity.

type Output = Map Name [Values]

a map storing the values of output entities.

writeOut :: Name -> [Values] -> MSOS ()

Add new values to a certain output entity.

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.

type Control = Map Name (Maybe Values)

a map storing the values of control entities.

raiseSignal :: Name -> Values -> MSOS ()

Signal a value of some control entity.

receiveSignals :: [Name] -> MSOS a -> MSOS (a, [Maybe Values])

Receive the value of a control entity from a given MSOS computation.

type Input m = Map Name ([[Values]], Maybe (m Funcons))

A map storing the values of input entities.

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.

Constructors

TVar MetaVar

TName Name

TApp Name [FTerm]

TSeq [FTerm]

TSet [FTerm]

TMap [FTerm]

TBinding FTerm FTerm

TFuncon Funcons

TSortSeq FTerm SeqSortOp

TSortPower FTerm FTerm

TSortUnion FTerm FTerm

TSortInter FTerm FTerm

TSortComplement FTerm

TSortComputes FTerm

TSortComputesFrom FTerm FTerm

TAny

Instances

Eq FTerm

Defined in Funcons.Types

Methods

(==) :: FTerm -> FTerm -> Bool

(/=) :: FTerm -> FTerm -> Bool

Ord FTerm

Defined in Funcons.Types

Methods

compare :: FTerm -> FTerm -> Ordering

(<) :: FTerm -> FTerm -> Bool

(<=) :: FTerm -> FTerm -> Bool

(>) :: FTerm -> FTerm -> Bool

(>=) :: FTerm -> FTerm -> Bool

max :: FTerm -> FTerm -> FTerm

min :: FTerm -> FTerm -> FTerm

Read FTerm

Defined in Funcons.Types

Methods

readsPrec :: Int -> ReadS FTerm

readList :: ReadS [FTerm]

readPrec :: ReadPrec FTerm

readListPrec :: ReadPrec [FTerm]

Show FTerm

Defined in Funcons.Types

Methods

showsPrec :: Int -> FTerm -> ShowS

show :: FTerm -> String

showList :: [FTerm] -> ShowS

HasTypeVar FTerm

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> FTerm -> FTerm

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FTerm -> FTerm

type Env = Map MetaVar Levelled

An environment mapping meta-variables to funcon terms. This environment is used by a substitution procedure to transform funcon terms from FTerm representation to Funcons.

emptyEnv :: Map k a

The empty substitution environment. Bindings are inserted by pattern-matching.

fvalues :: [Values] -> [Funcons]

Defining rules

rewriteTermTo :: FTerm -> Env -> Rewrite Rewritten

Variant of rewriteTo that applies substitution.

stepTermTo :: FTerm -> Env -> MSOS StepRes

Variant of stepTo that applies substitution.

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.

getInhPatt :: Name -> [VPattern] -> Env -> MSOS Env

Version of getInh that applies pattern-matching.

putMutTerm :: Name -> FTerm -> Env -> MSOS ()

Variant of putMut that applies substitution.

getMutPatt :: Name -> VPattern -> Env -> MSOS Env

Variant of getMut that performs pattern-matching.

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 :: Maybe Values -> Maybe VPattern -> Env -> MSOS Env

Variant of receiveSignal that performs pattern-matching.

raiseTerm :: Name -> FTerm -> Env -> MSOS ()

Variant of raiseSignal that applies substitution.

matchInput :: Name -> VPattern -> Env -> MSOS Env

Variant of consumeInput that matches the given VPattern 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.

withControlTerm :: Name -> Maybe FTerm -> Env -> MSOS a -> MSOS a

getControlPatt :: Name -> Maybe VPattern -> Env -> MSOS Env

Version of getControl that applies pattern-matching.

Backtracking

evalRules :: [Rewrite Rewritten] -> [MSOS StepRes] -> 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.

stepRules :: [IException] -> [MSOS StepRes] -> MSOS StepRes

rewriteRules :: [Rewrite Rewritten] -> Rewrite Rewritten

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).

Constructors

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 Env).

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

data VPattern

Patterns for matching values (Values).

Constructors

PADT Name [VPattern]

VPWildCard

VPMetaVar MetaVar

VPAnnotated VPattern FTerm

VPSeqVar MetaVar SeqSortOp

VPLit Values

VPType TPattern

Instances

Eq VPattern

Defined in Funcons.Patterns

Methods

(==) :: VPattern -> VPattern -> Bool

(/=) :: VPattern -> VPattern -> Bool

Ord VPattern

Defined in Funcons.Patterns

Methods

compare :: VPattern -> VPattern -> Ordering

(<) :: VPattern -> VPattern -> Bool

(<=) :: VPattern -> VPattern -> Bool

(>) :: VPattern -> VPattern -> Bool

(>=) :: VPattern -> VPattern -> Bool

max :: VPattern -> VPattern -> VPattern

min :: VPattern -> VPattern -> VPattern

Read VPattern

Defined in Funcons.Patterns

Methods

readsPrec :: Int -> ReadS VPattern

readList :: ReadS [VPattern]

readPrec :: ReadPrec VPattern

readListPrec :: ReadPrec [VPattern]

Show VPattern

Defined in Funcons.Patterns

Methods

showsPrec :: Int -> VPattern -> ShowS

show :: VPattern -> String

showList :: [VPattern] -> ShowS

HasTypeVar VPattern

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> VPattern -> VPattern

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> VPattern -> VPattern

data FPattern

Patterns for matching funcon terms (FTerm).

Constructors

PValue VPattern

PMetaVar MetaVar

PSeqVar MetaVar SeqSortOp

PAnnotated FPattern FTerm

PWildCard

Instances

Eq FPattern

Defined in Funcons.Patterns

Methods

(==) :: FPattern -> FPattern -> Bool

(/=) :: FPattern -> FPattern -> Bool

Ord FPattern

Defined in Funcons.Patterns

Methods

compare :: FPattern -> FPattern -> Ordering

(<) :: FPattern -> FPattern -> Bool

(<=) :: FPattern -> FPattern -> Bool

(>) :: FPattern -> FPattern -> Bool

(>=) :: FPattern -> FPattern -> Bool

max :: FPattern -> FPattern -> FPattern

min :: FPattern -> FPattern -> FPattern

Read FPattern

Defined in Funcons.Patterns

Methods

readsPrec :: Int -> ReadS FPattern

readList :: ReadS [FPattern]

readPrec :: ReadPrec FPattern

readListPrec :: ReadPrec [FPattern]

Show FPattern

Defined in Funcons.Patterns

Methods

showsPrec :: Int -> FPattern -> ShowS

show :: FPattern -> String

showList :: [FPattern] -> ShowS

HasTypeVar FPattern

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> FPattern -> FPattern

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FPattern -> FPattern

data TPattern

Constructors

TPWildCard

TPVar MetaVar

TPSeqVar MetaVar SeqSortOp

TPLit FTerm

TPComputes TPattern

TPComputesFrom TPattern TPattern

TPADT Name [TPattern]

Instances

Eq TPattern

Defined in Funcons.Types

Methods

(==) :: TPattern -> TPattern -> Bool

(/=) :: TPattern -> TPattern -> Bool

Ord TPattern

Defined in Funcons.Types

Methods

compare :: TPattern -> TPattern -> Ordering

(<) :: TPattern -> TPattern -> Bool

(<=) :: TPattern -> TPattern -> Bool

(>) :: TPattern -> TPattern -> Bool

(>=) :: TPattern -> TPattern -> Bool

max :: TPattern -> TPattern -> TPattern

min :: TPattern -> TPattern -> TPattern

Read TPattern

Defined in Funcons.Types

Methods

readsPrec :: Int -> ReadS TPattern

readList :: ReadS [TPattern]

readPrec :: ReadPrec TPattern

readListPrec :: ReadPrec [TPattern]

Show TPattern

Defined in Funcons.Types

Methods

showsPrec :: Int -> TPattern -> ShowS

show :: TPattern -> String

showList :: [TPattern] -> ShowS

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.

f2vPattern :: FPattern -> VPattern

lifted_vsMatch :: [Values] -> [VPattern] -> Env -> MSOS Env

Variant of vsMatch that is lifted into the MSOS monad.

lifted_fsMatch :: [Funcons] -> [FPattern] -> Env -> MSOS Env

Variant of fsMatch that is lifted into the MSOS monad. If all given terms are values, then vsMatch is used instead.

pat2term :: FPattern -> FTerm

vpat2term :: VPattern -> FTerm

typat2term :: TPattern -> FTerm

Meta-environment

envRewrite :: MetaVar -> Env -> Rewrite Env

Apply as many rewrites as possible to the term bound to the given variable in the meta-environment

envStore :: MetaVar -> FTerm -> Env -> Rewrite Env

lifted_envRewrite :: MetaVar -> Env -> MSOS Env

lifted_envStore :: MetaVar -> FTerm -> Env -> MSOS Env

Type substitution

type TypeEnv = Map MetaVar TyAssoc

Associates types (Terms) with meta-variables

data TyAssoc

Constructors

ElemOf FTerm

SubTyOf FTerm

class HasTypeVar a where

Used for replacing meta-variables T in pattern annotations `P:T` with the type to which T is bound in some type-environment (if any)

Minimal complete definition

subsTypeVarWildcard

Methods

subsTypeVar :: TypeEnv -> a -> a

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> a -> a

Instances

HasTypeVar FTerm

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> FTerm -> FTerm

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FTerm -> FTerm

HasTypeVar VPattern

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> VPattern -> VPattern

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> VPattern -> VPattern

HasTypeVar FPattern

Defined in Funcons.TypeSubstitution

Methods

subsTypeVar :: TypeEnv -> FPattern -> FPattern

subsTypeVarWildcard :: Maybe FTerm -> TypeEnv -> FPattern -> FPattern

limitedSubsTypeVar :: HasTypeVar a => Set MetaVar -> TypeEnv -> a -> a

Version of subsTypeVar that does not replace the meta-variables in the given set

limitedSubsTypeVarWildcard :: HasTypeVar a => Set MetaVar -> Maybe FTerm -> TypeEnv -> a -> a

Version of subsTypeVarWildcard that does not replace the meta-variables in the given set

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 EntityDefaults is used to declare (and possibly initialise) entities.

data EntityDefault

Default values of entities can be specified for inherited and mutable entities.

Constructors

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 TypeRelation = Map Name DataTypeMembers

The typing environment maps datatype names to their definitions.

type TypeParam = (Maybe MetaVar, Maybe SeqSortOp, FTerm)

A type parameter is of the form X:T where the name of the parameter,X, is optional. When present, X can be used to specify the type of constructors. Variable X be a sequence variable.

data DataTypeMembers

A datatype has `zero or more' type parameters and `zero or more' alternatives.

Constructors

DataTypeMemberss Name [TPattern] [DataTypeAltt]

Instances

Show DataTypeMembers

Defined in Funcons.Types

Methods

showsPrec :: Int -> DataTypeMembers -> ShowS

show :: DataTypeMembers -> String

showList :: [DataTypeMembers] -> ShowS

data DataTypeAltt

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.

Constructors

DataTypeInclusionn FTerm

DataTypeMemberConstructor Name [FTerm] (Maybe [TPattern])

Instances

Show DataTypeAltt

Defined in Funcons.Types

Methods

showsPrec :: Int -> DataTypeAltt -> ShowS

show :: DataTypeAltt -> String

showList :: [DataTypeAltt] -> ShowS

typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers

Lookup the definition of a datatype in the typing environment.

typeEnvUnion :: TypeRelation -> TypeRelation -> TypeRelation

Unites two TypeRelations.

typeEnvUnions :: [TypeRelation] -> TypeRelation

Unites a list of TypeRelations.

typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation

Creates a TypeRelation from a list.

emptyTypeRelation :: TypeRelation

The empty TypeRelation.