funcons-tools-0.1.0.0: A modular interpreter for executing funcons

Safe HaskellNone
LanguageHaskell2010

Funcons.EDSL

Contents

Description

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.

Synopsis

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

Constructors

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 EmptyTuple and NonEmptyTuple to avoid singleton tuples. Tuples should be constructed by applications of tuple_.

Vector Vectors 

Instances

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.

Constructors

StarOp 
PlusOp 
QuestionMarkOp 

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

list_ :: [Funcons] -> Funcons

Creates a list of funcon terms.

tuple_ :: [Funcons] -> Funcons

Creates a tuple of funcon terms.

set_ :: [Funcons] -> Funcons

Creates a set of funcon terms.

map_empty_ :: Funcons

The empty map as a Funcons.

empty_tuple_ :: Funcons

Creates an empty tuple as a Values.

Values

int_ :: Int -> Funcons

Creates an integer literal.

nat_ :: Int -> Funcons

Creates a natural literal.

string_ :: String -> Funcons

Creates a string literal.

Types

Pretty-print funcon terms

showValues :: Values -> String

Pretty-print a Values.

showFuncons :: Funcons -> String

Pretty-print a Funcons.

showTypes :: Types -> String

Pretty-print a Types.

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.

Constructors

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

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

Creates a FunconLibrary from a list.

library :: FunconLibrary

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.

Instances

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.

rewritten :: Values -> Rewrite Rewritten

Returns a value as a fully rewritten term.

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

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.

receiveSignal :: 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 Values))

A map storing the values of input entities.

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.

Instances

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.

Defining rules

rewriteTermTo :: FTerm -> Env -> Rewrite Rewritten

Variant of rewriteTo that applies substitution.

stepTermTo :: FTerm -> Env -> MSOS Funcons

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

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

data FPattern

Patterns for matching funcon terms (FTerm).

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.

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.

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

typeEnvUnions :: [TypeEnv] -> TypeEnv

Unites a list of TypeEnvs.

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

Creates a TypeEnv from a list.