-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Feedback services for intelligent tutoring systems
--
-- ideas provides feedback services to intelligent tutoring systems such
-- as the digital mathematical environment of the Freudenthal Institute,
-- MathDox, and Activemath.
@package ideas
@version 1.1
-- | Datatype for representing XML documents
module Ideas.Text.XML.Document
type Name = String
type Attributes = [Attribute]
data Attribute
(:=) :: Name -> AttValue -> Attribute
data Reference
CharRef :: Int -> Reference
EntityRef :: String -> Reference
data Parameter
Parameter :: String -> Parameter
data XMLDoc
XMLDoc :: Maybe String -> Maybe String -> Maybe Bool -> Maybe DTD -> [(String, External)] -> Element -> XMLDoc
versionInfo :: XMLDoc -> Maybe String
encoding :: XMLDoc -> Maybe String
standalone :: XMLDoc -> Maybe Bool
dtd :: XMLDoc -> Maybe DTD
externals :: XMLDoc -> [(String, External)]
root :: XMLDoc -> Element
data XML
Tagged :: Element -> XML
CharData :: String -> XML
CDATA :: String -> XML
Reference :: Reference -> XML
data Element
Element :: Name -> Attributes -> Content -> Element
name :: Element -> Name
attributes :: Element -> Attributes
content :: Element -> Content
type Content = [XML]
data DTD
DTD :: Name -> (Maybe ExternalID) -> [DocTypeDecl] -> DTD
data DocTypeDecl
ElementDecl :: Name -> ContentSpec -> DocTypeDecl
AttListDecl :: Name -> [AttDef] -> DocTypeDecl
EntityDecl :: Bool -> Name -> EntityDef -> DocTypeDecl
NotationDecl :: Name -> (Either ExternalID PublicID) -> DocTypeDecl
DTDParameter :: Parameter -> DocTypeDecl
DTDConditional :: Conditional -> DocTypeDecl
data ContentSpec
Empty :: ContentSpec
Any :: ContentSpec
Mixed :: Bool -> [Name] -> ContentSpec
Children :: CP -> ContentSpec
data CP
Choice :: [CP] -> CP
Sequence :: [CP] -> CP
QuestionMark :: CP -> CP
Star :: CP -> CP
Plus :: CP -> CP
CPName :: Name -> CP
data AttType
IdType :: AttType
IdRefType :: AttType
IdRefsType :: AttType
EntityType :: AttType
EntitiesType :: AttType
NmTokenType :: AttType
NmTokensType :: AttType
StringType :: AttType
EnumerationType :: [String] -> AttType
NotationType :: [String] -> AttType
data DefaultDecl
Required :: DefaultDecl
Implied :: DefaultDecl
Value :: AttValue -> DefaultDecl
Fixed :: AttValue -> DefaultDecl
type AttDef = (Name, AttType, DefaultDecl)
type EntityDef = Either EntityValue (ExternalID, Maybe String)
type AttValue = [Either Char Reference]
type EntityValue = [Either Char (Either Parameter Reference)]
data ExternalID
System :: String -> ExternalID
Public :: String -> String -> ExternalID
type PublicID = String
data Conditional
Include :: [DocTypeDecl] -> Conditional
Ignore :: [String] -> Conditional
type TextDecl = (Maybe String, String)
type External = (Maybe TextDecl, Content)
instance Show Parameter
instance Show Reference
instance Show XML
instance Show Element
instance Show Attribute
-- | Support for the UTF8 encoding
module Ideas.Text.UTF8
-- | Encode a string to UTF8 format
encode :: String -> String
-- | Encode a string to UTF8 format (monadic)
encodeM :: Monad m => String -> m String
-- | Decode an UTF8 format string to unicode points
decode :: String -> String
-- | Decode an UTF8 format string to unicode points (monadic)
decodeM :: Monad m => String -> m String
-- | Test whether the argument is a proper UTF8 string
isUTF8 :: String -> Bool
-- | Test whether all characters are in the range 0-255
allBytes :: String -> Bool
-- | QuickCheck internal encoding/decoding functions
propEncoding :: Property
-- | Support for Unicode
module Ideas.Text.XML.Unicode
isExtender :: Char -> Bool
isLetter :: Char -> Bool
isDigit :: Char -> Bool
isCombiningChar :: Char -> Bool
extenderMap :: [(Char, Char)]
letterMap :: [(Char, Char)]
digitMap :: [(Char, Char)]
combiningCharMap :: [(Char, Char)]
decoding :: Monad m => String -> m String
-- | Utility functions for parsing with Parsec library
module Ideas.Text.Parsing
-- | Sequential application.
(<*>) :: Applicative f => forall a b. f (a -> b) -> f a -> f b
-- | Sequence actions, discarding the value of the first argument.
(*>) :: Applicative f => forall a b. f a -> f b -> f b
-- | Sequence actions, discarding the value of the second argument.
(<*) :: Applicative f => forall a b. f a -> f b -> f a
-- | An infix synonym for fmap.
(<$>) :: Functor f => (a -> b) -> f a -> f b
-- | Replace all locations in the input with the same value. The default
-- definition is fmap . const, but this may be
-- overridden with a more efficient version.
(<$) :: Functor f => forall a b. a -> f b -> f a
-- | A variant of <*> with the arguments reversed.
(<**>) :: Applicative f => f a -> f (a -> b) -> f b
parseSimple :: Parser a -> String -> Either String a
complete :: Parser a -> Parser a
skip :: Parser a -> Parser ()
(<..>) :: Char -> Char -> Parser Char
ranges :: [(Char, Char)] -> Parser Char
stopOn :: [String] -> Parser String
naturalOrFloat :: Parser (Either Integer Double)
float :: Parser Double
data UnbalancedError
NotClosed :: SourcePos -> Char -> UnbalancedError
NotOpened :: SourcePos -> Char -> UnbalancedError
balanced :: [(Char, Char)] -> String -> Maybe UnbalancedError
instance Show UnbalancedError
-- | A parser for XML documents, directly derived from the specification:
module Ideas.Text.XML.Parser
document :: Parser XMLDoc
extParsedEnt :: Parser (Maybe TextDecl, Content)
extSubset :: Parser (Maybe TextDecl, [DocTypeDecl])
-- | Collection of common operation on XML documents
module Ideas.Text.XML.Interface
data Element
Element :: Name -> Attributes -> Content -> Element
name :: Element -> Name
attributes :: Element -> Attributes
content :: Element -> Content
type Content = [Either String Element]
data Attribute
(:=) :: Name -> String -> Attribute
type Attributes = [Attribute]
normalize :: XMLDoc -> Element
parseXML :: String -> Either String Element
children :: Element -> [Element]
findAttribute :: Monad m => String -> Element -> m String
findChild :: Monad m => String -> Element -> m Element
getData :: Element -> String
instance Show Element
module Ideas.Main.Revision
ideasVersion :: String
ideasRevision :: Int
ideasLastChanged :: String
module Ideas.Text.OpenMath.Symbol
type Symbol = (Maybe String, String)
makeSymbol :: String -> String -> Symbol
extraSymbol :: String -> Symbol
dictionary :: Symbol -> Maybe String
symbolName :: Symbol -> String
showSymbol :: Symbol -> String
module Ideas.Text.OpenMath.Dictionary.Calculus1
-- | List of symbols defined in calculus1 dictionary
calculus1List :: [Symbol]
-- | This symbol is used to express ordinary differentiation of a unary
-- function. The single argument is the unary function.
diffSymbol :: Symbol
-- | This symbol is used to express the nth-iterated ordinary
-- differentiation of a unary function. The first argument is n, and the
-- second the unary function.
nthdiffSymbol :: Symbol
-- | This symbol is used to express partial differentiation of a function
-- of more than one variable. It has two arguments, the first is a list
-- of integers which index the variables of the function, the second is
-- the function.
partialdiffSymbol :: Symbol
-- | This symbol is used to represent indefinite integration of unary
-- functions. The argument is the unary function.
intSymbol :: Symbol
-- | This symbol is used to represent definite integration of unary
-- functions. It takes two arguments; the first being the range (e.g. a
-- set) of integration, and the second the function.
defintSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Linalg2
-- | List of symbols defined in linalg2 dictionary
linalg2List :: [Symbol]
-- | This symbol represents an n-ary function used to construct (or
-- describe) vectors. Vectors in this CD are considered to be row vectors
-- and must therefore be transposed to be considered as column vectors.
vectorSymbol :: Symbol
-- | This symbol is an n-ary constructor used to represent rows of
-- matrices. Its arguments should be members of a ring.
matrixrowSymbol :: Symbol
-- | This symbol is an n-ary matrix constructor which requires matrixrow's
-- as arguments. It is used to represent matrices.
matrixSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Logic1
-- | List of symbols defined in logic1 dictionary
logic1List :: [Symbol]
-- | This symbol is used to show that two boolean expressions are logically
-- equivalent, that is have the same boolean value for any inputs.
equivalentSymbol :: Symbol
-- | This symbol represents the logical not function which takes one
-- boolean argument, and returns the opposite boolean value.
notSymbol :: Symbol
-- | This symbol represents the logical and function which is an n-ary
-- function taking boolean arguments and returning a boolean value. It is
-- true if all arguments are true or false otherwise.
andSymbol :: Symbol
-- | This symbol represents the logical xor function which is an n-ary
-- function taking boolean arguments and returning a boolean value. It is
-- true if there are an odd number of true arguments or false otherwise.
xorSymbol :: Symbol
-- | This symbol represents the logical or function which is an n-ary
-- function taking boolean arguments and returning a boolean value. It is
-- true if any of the arguments are true or false otherwise.
orSymbol :: Symbol
-- | This symbol represents the logical implies function which takes two
-- boolean expressions as arguments. It evaluates to false if the first
-- argument is true and the second argument is false, otherwise it
-- evaluates to true.
impliesSymbol :: Symbol
-- | This symbol represents the boolean value true.
trueSymbol :: Symbol
-- | This symbol represents the boolean value false.
falseSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Nums1
-- | List of symbols defined in nums1 dictionary
nums1List :: [Symbol]
-- | This symbol represents the constructor function for integers,
-- specifying the base. It takes two arguments, the first is a positive
-- integer to denote the base to which the number is represented, the
-- second argument is a string which contains an optional sign and the
-- digits of the integer, using 0-9a-z (as a consequence of this no radix
-- greater than 35 is supported). Base 16 and base 10 are already covered
-- in the encodings of integers.
basedIntegerSymbol :: Symbol
-- | This symbol represents the constructor function for rational numbers.
-- It takes two arguments, the first is an integer p to denote the
-- numerator and the second a nonzero integer q to denote the denominator
-- of the rational p/q.
rationalSymbol :: Symbol
-- | A symbol to represent the notion of infinity.
infinitySymbol :: Symbol
-- | This symbol represents the base of the natural logarithm,
-- approximately 2.718. See Abramowitz and Stegun, Handbook of
-- Mathematical Functions, section 4.1.
eSymbol :: Symbol
-- | This symbol represents the square root of -1.
iSymbol :: Symbol
-- | A symbol to convey the notion of pi, approximately 3.142. The ratio of
-- the circumference of a circle to its diameter.
piSymbol :: Symbol
-- | A symbol to convey the notion of the gamma constant as defined in
-- Abramowitz and Stegun, Handbook of Mathematical Functions, section
-- 6.1.3. It is the limit of 1 + 12 + 13 + ... + 1/m - ln m as m
-- tends to infinity, this is approximately 0.5772 15664.
gammaSymbol :: Symbol
-- | A symbol to convey the notion of not-a-number. The result of an
-- ill-posed floating computation. See IEEE standard for floating point
-- representations.
naNSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Quant1
-- | List of symbols defined in quant1 dictionary
quant1List :: [Symbol]
-- | This symbol represents the universal (for all) quantifier which
-- takes two arguments. It must be placed within an OMBIND element. The
-- first argument is the bound variables (placed within an OMBVAR
-- element), and the second is an expression.
forallSymbol :: Symbol
-- | This symbol represents the existential (there exists)
-- quantifier which takes two arguments. It must be placed within an
-- OMBIND element. The first argument is the bound variables (placed
-- within an OMBVAR element), and the second is an expression.
existsSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Relation1
-- | List of symbols defined in relation1 dictionary
relation1List :: [Symbol]
-- | This symbol represents the binary equality function.
eqSymbol :: Symbol
-- | This symbol represents the binary less than function which returns
-- true if the first argument is less than the second, it returns false
-- otherwise.
ltSymbol :: Symbol
-- | This symbol represents the binary greater than function which returns
-- true if the first argument is greater than the second, it returns
-- false otherwise.
gtSymbol :: Symbol
-- | This symbol represents the binary inequality function.
neqSymbol :: Symbol
-- | This symbol represents the binary less than or equal to function which
-- returns true if the first argument is less than or equal to the
-- second, it returns false otherwise.
leqSymbol :: Symbol
-- | This symbol represents the binary greater than or equal to function
-- which returns true if the first argument is greater than or equal to
-- the second, it returns false otherwise.
geqSymbol :: Symbol
-- | This symbol is used to denote the approximate equality of its two
-- arguments.
approxSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Transc1
-- | List of symbols defined in transc1 dictionary
transc1List :: [Symbol]
-- | This symbol represents a binary log function; the first argument is
-- the base, to which the second argument is log'ed. It is defined in
-- Abramowitz and Stegun, Handbook of Mathematical Functions, section 4.1
logSymbol :: Symbol
-- | This symbol represents the ln function (natural logarithm) as
-- described in Abramowitz and Stegun, section 4.1. It takes one
-- argument. Note the description in the CMP/FMP of the branch cut. If
-- signed zeros are in use, the inequality needs to be non-strict.
lnSymbol :: Symbol
-- | This symbol represents the exponentiation function as described in
-- Abramowitz and Stegun, section 4.2. It takes one argument.
expSymbol :: Symbol
-- | This symbol represents the sin function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
sinSymbol :: Symbol
-- | This symbol represents the cos function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
cosSymbol :: Symbol
-- | This symbol represents the tan function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
tanSymbol :: Symbol
-- | This symbol represents the sec function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
secSymbol :: Symbol
-- | This symbol represents the csc function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
cscSymbol :: Symbol
-- | This symbol represents the cot function as described in Abramowitz and
-- Stegun, section 4.3. It takes one argument.
cotSymbol :: Symbol
-- | This symbol represents the sinh function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
sinhSymbol :: Symbol
-- | This symbol represents the cosh function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
coshSymbol :: Symbol
-- | This symbol represents the tanh function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
tanhSymbol :: Symbol
-- | This symbol represents the sech function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
sechSymbol :: Symbol
-- | This symbol represents the csch function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
cschSymbol :: Symbol
-- | This symbol represents the coth function as described in Abramowitz
-- and Stegun, section 4.5. It takes one argument.
cothSymbol :: Symbol
-- | This symbol represents the arcsin function. This is the inverse of the
-- sin function as described in Abramowitz and Stegun, section 4.4. It
-- takes one argument.
arcsinSymbol :: Symbol
-- | This symbol represents the arccos function. This is the inverse of the
-- cos function as described in Abramowitz and Stegun, section 4.4. It
-- takes one argument.
arccosSymbol :: Symbol
-- | This symbol represents the arctan function. This is the inverse of the
-- tan function as described in Abramowitz and Stegun, section 4.4. It
-- takes one argument.
arctanSymbol :: Symbol
-- | This symbol represents the arcsec function as described in Abramowitz
-- and Stegun, section 4.4.
arcsecSymbol :: Symbol
-- | This symbol represents the arccsc function as described in Abramowitz
-- and Stegun, section 4.4.
arccscSymbol :: Symbol
-- | This symbol represents the arccot function as described in Abramowitz
-- and Stegun, section 4.4.
arccotSymbol :: Symbol
-- | This symbol represents the arcsinh function as described in Abramowitz
-- and Stegun, section 4.6.
arcsinhSymbol :: Symbol
-- | This symbol represents the arccosh function as described in Abramowitz
-- and Stegun, section 4.6.
arccoshSymbol :: Symbol
-- | This symbol represents the arctanh function as described in Abramowitz
-- and Stegun, section 4.6.
arctanhSymbol :: Symbol
-- | This symbol represents the arcsech function as described in Abramowitz
-- and Stegun, section 4.6.
arcsechSymbol :: Symbol
-- | This symbol represents the arccsch function as described in Abramowitz
-- and Stegun, section 4.6.
arccschSymbol :: Symbol
-- | This symbol represents the arccoth function as described in Abramowitz
-- and Stegun, section 4.6.
arccothSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.List1
-- | List of symbols defined in list1 dictionary
list1List :: [Symbol]
-- | This symbol represents a mapping function which may be used to
-- construct lists, it takes as arguments a function from X to Y and a
-- list over X in that order. The value that is returned is a list of
-- values in Y. The argument list may be a set or an integer_interval.
mapSymbol :: Symbol
-- | This symbol represents the suchthat function which may be used to
-- construct lists, it takes two arguments. The first argument should be
-- the set which contains the elements of the list, the second argument
-- should be a predicate, that is a function from the set to the booleans
-- which describes if an element is to be in the list returned.
suchthatSymbol :: Symbol
-- | This symbol denotes the list construct which is an n-ary function. The
-- list entries must be given explicitly.
listSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Fns1
-- | List of symbols defined in fns1 dictionary
fns1List :: [Symbol]
-- | The domainofapplication element denotes the domain over which a given
-- function is being applied. It is intended in MathML to be a more
-- general alternative to specification of this domain using such
-- quantifier elements as bvar, lowlimit or condition.
domainofapplicationSymbol :: Symbol
-- | This symbol denotes the domain of a given function, which is the set
-- of values it is defined over.
domainSymbol :: Symbol
-- | This symbol denotes the range of a function, that is a set that the
-- function will map to. The single argument should be the function whos
-- range is being queried. It should be noted that this is not
-- necessarily equal to the image, it is merely required to contain the
-- image.
rangeSymbol :: Symbol
-- | This symbol denotes the image of a given function, which is the set of
-- values the domain of the given function maps to.
imageSymbol :: Symbol
-- | The identity function, it takes one argument and returns the same
-- value.
identitySymbol :: Symbol
-- | This symbol is used to describe the left inverse of its argument (a
-- function). This inverse may only be partially defined because the
-- function may not have been surjective. If the function is not
-- surjective the left inverse function is ill-defined without further
-- stipulations. No other assumptions are made on the semantics of this
-- left inverse.
leftInverseSymbol :: Symbol
-- | This symbol is used to describe the right inverse of its argument (a
-- function). This inverse may only be partially defined because the
-- function may not have been surjective. If the function is not
-- surjective the right inverse function is ill-defined without further
-- stipulations. No other assumptions are made on the semantics of this
-- right inverse.
rightInverseSymbol :: Symbol
-- | This symbol is used to describe the inverse of its argument (a
-- function). This inverse may only be partially defined because the
-- function may not have been surjective. If the function is not
-- surjective the inverse function is ill-defined without further
-- stipulations. No assumptions are made on the semantics of this
-- inverse.
inverseSymbol :: Symbol
-- | This symbol represents the function which forms the left-composition
-- of its two (function) arguments.
leftComposeSymbol :: Symbol
-- | This symbol is used to represent anonymous functions as lambda
-- expansions. It is used in a binder that takes two further arguments,
-- the first of which is a list of variables, and the second of which is
-- an expression, and it forms the function which is the lambda
-- extraction of the expression
lambdaSymbol :: Symbol
module Ideas.Text.OpenMath.Dictionary.Arith1
-- | List of symbols defined in arith1 dictionary
arith1List :: [Symbol]
-- | The symbol to represent the n-ary function to return the least common
-- multiple of its arguments.
lcmSymbol :: Symbol
-- | The symbol to represent the n-ary function to return the gcd (greatest
-- common divisor) of its arguments.
gcdSymbol :: Symbol
-- | The symbol representing an n-ary commutative function plus.
plusSymbol :: Symbol
-- | This symbol denotes unary minus, i.e. the additive inverse.
unaryMinusSymbol :: Symbol
-- | The symbol representing a binary minus function. This is equivalent to
-- adding the additive inverse.
minusSymbol :: Symbol
-- | The symbol representing an n-ary multiplication function.
timesSymbol :: Symbol
-- | This symbol represents a (binary) division function denoting the first
-- argument right-divided by the second, i.e. divide(a,b)=a*inverse(b).
-- It is the inverse of the multiplication function defined by the symbol
-- times in this CD.
divideSymbol :: Symbol
-- | This symbol represents a power function. The first argument is raised
-- to the power of the second argument. When the second argument is not
-- an integer, powering is defined in terms of exponentials and
-- logarithms for the complex and real numbers. This operator can
-- represent general powering.
powerSymbol :: Symbol
-- | A unary operator which represents the absolute value of its argument.
-- The argument should be numerically valued. In the complex case this is
-- often referred to as the modulus.
absSymbol :: Symbol
-- | A binary operator which represents its first argument lowered
-- to its n'th root where n is the second argument. This is the inverse
-- of the operation represented by the power symbol defined in this CD.
-- Care should be taken as to the precise meaning of this operator, in
-- particular which root is represented, however it is here to represent
-- the general notion of taking n'th roots. As inferred by the signature
-- relevant to this symbol, the function represented by this symbol is
-- the single valued function, the specific root returned is the one
-- indicated by the first CMP. Note also that the converse of the second
-- CMP is not valid in general.
rootSymbol :: Symbol
-- | An operator taking two arguments, the first being the range of
-- summation, e.g. an integral interval, the second being the function to
-- be summed. Note that the sum may be over an infinite interval.
sumSymbol :: Symbol
-- | An operator taking two arguments, the first being the range of
-- multiplication e.g. an integral interval, the second being the
-- function to be multiplied. Note that the product may be over an
-- infinite interval.
productSymbol :: Symbol
-- | A datatype, parser, and pretty printer for XML documents. Re-exports
-- functions defined elsewhere.
module Ideas.Text.XML
type XML = Element
type Attr = Attribute
type AttrList = Attributes
data Element
Element :: Name -> Attributes -> Content -> Element
name :: Element -> Name
attributes :: Element -> Attributes
content :: Element -> Content
class InXML a where listToXML = Element "list" [] . map (Right . toXML) listFromXML xml | name xml == "list" && null (attributes xml) = mapM fromXML (children xml) | otherwise = fail "expecting a list tag"
toXML :: InXML a => a -> XML
listToXML :: InXML a => [a] -> XML
fromXML :: (InXML a, Monad m) => XML -> m a
listFromXML :: (InXML a, Monad m) => XML -> m [a]
data XMLBuilder
makeXML :: String -> XMLBuilder -> XML
parseXML :: String -> Either String XML
showXML :: XML -> String
compactXML :: XML -> String
findAttribute :: Monad m => String -> Element -> m String
children :: Element -> [Element]
data Attribute
(:=) :: Name -> String -> Attribute
fromBuilder :: XMLBuilder -> Maybe Element
findChild :: Monad m => String -> Element -> m Element
getData :: Element -> String
class Monoid a => BuildXML a where string = unescaped . escape text = string . show element s = tag s . mconcat emptyTag s = tag s mempty
(.=.) :: BuildXML a => String -> String -> a
unescaped :: BuildXML a => String -> a
builder :: BuildXML a => Element -> a
tag :: BuildXML a => String -> a -> a
string :: BuildXML a => String -> a
text :: (BuildXML a, Show s) => s -> a
element :: BuildXML a => String -> [a] -> a
emptyTag :: BuildXML a => String -> a
munless :: Monoid a => Bool -> a -> a
mwhen :: Monoid a => Bool -> a -> a
instance BuildXML XMLBuilder
instance Monoid XMLBuilder
-- | A minimal interface for constructing simple HTML pages See
-- http:www.w3.orgTRhtml4/
module Ideas.Text.HTML
data HTMLPage
type HTMLBuilder = XMLBuilder
addCSS :: FilePath -> HTMLPage -> HTMLPage
addScript :: FilePath -> HTMLPage -> HTMLPage
showHTML :: HTMLPage -> String
string :: BuildXML a => String -> a
text :: (BuildXML a, Show s) => s -> a
htmlPage :: String -> HTMLBuilder -> HTMLPage
link :: BuildXML a => String -> a -> a
h1 :: BuildXML a => String -> a
h2 :: BuildXML a => String -> a
h3 :: BuildXML a => String -> a
h4 :: BuildXML a => String -> a
h5 :: BuildXML a => String -> a
h6 :: BuildXML a => String -> a
preText :: BuildXML a => String -> a
ul :: BuildXML a => [a] -> a
-- | First argument indicates whether the table has a header or not
table :: BuildXML a => Bool -> [[a]] -> a
keyValueTable :: BuildXML a => [(String, a)] -> a
image :: BuildXML a => String -> a
space :: BuildXML a => a
spaces :: BuildXML a => Int -> a
highlightXML :: Bool -> XML -> HTMLBuilder
para :: BuildXML a => a -> a
ttText :: BuildXML a => String -> a
hr :: BuildXML a => a
br :: BuildXML a => a
pre :: BuildXML a => a -> a
bullet :: BuildXML a => a
divClass :: BuildXML a => String -> a -> a
spanClass :: BuildXML a => String -> a -> a
idA :: BuildXML a => String -> a
classA :: BuildXML a => String -> a
styleA :: BuildXML a => String -> a
titleA :: BuildXML a => String -> a
-- | Renders as teletype or monospaced Ideas.Text.
tt :: BuildXML a => a -> a
-- | Renders as italic text style.
italic :: BuildXML a => a -> a
-- | Renders as bold text style.
bold :: BuildXML a => a -> a
big :: BuildXML a => a -> a
small :: BuildXML a => a -> a
instance InXML HTMLPage
module Ideas.Text.OpenMath.Object
data OMOBJ
OMI :: Integer -> OMOBJ
OMF :: Double -> OMOBJ
OMV :: String -> OMOBJ
OMS :: Symbol -> OMOBJ
OMA :: [OMOBJ] -> OMOBJ
OMBIND :: OMOBJ -> [String] -> OMOBJ -> OMOBJ
getOMVs :: OMOBJ -> [String]
xml2omobj :: XML -> Either String OMOBJ
omobj2xml :: OMOBJ -> XML
instance Typeable OMOBJ
instance Show OMOBJ
instance Eq OMOBJ
instance Uniplate OMOBJ
instance InXML OMOBJ
-- | Formal mathematical properties (FMP)
module Ideas.Text.OpenMath.FMP
data FMP
FMP :: Symbol -> [String] -> OMOBJ -> Symbol -> OMOBJ -> FMP
quantor :: FMP -> Symbol
metaVariables :: FMP -> [String]
leftHandSide :: FMP -> OMOBJ
relation :: FMP -> Symbol
rightHandSide :: FMP -> OMOBJ
toObject :: FMP -> OMOBJ
eqFMP :: OMOBJ -> OMOBJ -> FMP
-- | Represents a common misconception. In certain (most) situations, the
-- two objects are not the same.
buggyFMP :: OMOBJ -> OMOBJ -> FMP
module Ideas.Text.OpenMath.Tests
propEncoding :: Property
-- | Support for JavaScript Object Notation (JSON) and remote procedure
-- calls using JSON. JSON is a lightweight alternative for XML.
module Ideas.Text.JSON
data JSON
Number :: Number -> JSON
String :: String -> JSON
Boolean :: Bool -> JSON
Array :: [JSON] -> JSON
Object :: [(Key, JSON)] -> JSON
Null :: JSON
type Key = String
data Number
I :: Integer -> Number
D :: Double -> Number
class InJSON a where listToJSON = Array . map toJSON listFromJSON (Array xs) = mapM fromJSON xs listFromJSON _ = fail "expecting an array"
toJSON :: InJSON a => a -> JSON
listToJSON :: InJSON a => [a] -> JSON
fromJSON :: (InJSON a, Monad m) => JSON -> m a
listFromJSON :: (InJSON a, Monad m) => JSON -> m [a]
lookupM :: Monad m => String -> JSON -> m JSON
parseJSON :: String -> Either String JSON
showCompact :: JSON -> String
showPretty :: JSON -> String
jsonRPC :: (MonadError a m, InJSON a) => JSON -> RPCHandler m -> m RPCResponse
type RPCHandler m = String -> JSON -> m JSON
propEncoding :: Property
instance Eq Number
instance Eq JSON
instance Arbitrary Number
instance Arbitrary JSON
instance InJSON RPCResponse
instance InJSON RPCRequest
instance Show RPCResponse
instance Show RPCRequest
instance InJSON IOException
instance (InJSON a, InJSON b, InJSON c, InJSON d) => InJSON (a, b, c, d)
instance (InJSON a, InJSON b, InJSON c) => InJSON (a, b, c)
instance (InJSON a, InJSON b) => InJSON (a, b)
instance InJSON a => InJSON [a]
instance InJSON Bool
instance InJSON Char
instance InJSON Double
instance InJSON Integer
instance InJSON Int
instance Show Number
instance Show JSON
-- | Extensions to the QuickCheck library
module Ideas.Common.Utils.QuickCheck
data ArbGen a
generator :: ArbGen a -> Gen a
generators :: [ArbGen a] -> Gen a
arbGen :: Arbitrary b => (b -> a) -> ArbGen a
constGen :: a -> ArbGen a
constGens :: [a] -> ArbGen a
unaryGen :: (a -> a) -> ArbGen a
unaryGens :: [a -> a] -> ArbGen a
unaryArbGen :: Arbitrary b => (b -> a -> a) -> ArbGen a
binaryGen :: (a -> a -> a) -> ArbGen a
binaryGens :: [a -> a -> a] -> ArbGen a
toArbGen :: Gen a -> ArbGen a
common :: ArbGen a -> ArbGen a
uncommon :: ArbGen a -> ArbGen a
rare :: ArbGen a -> ArbGen a
changeFrequency :: Rational -> ArbGen a -> ArbGen a
instance Monoid (ArbGen a)
-- | References to Strings, proving a fast comparison implementation (Eq
-- and Ord) that uses a hash function. Code is based on Daan Leijen's
-- Lazy Virutal Machine (LVM) identifiers.
module Ideas.Common.Utils.StringRef
data StringRef
stringRef :: String -> StringRef
toString :: StringRef -> String
tableStatus :: IO String
instance Typeable StringRef
instance Eq StringRef
instance Ord StringRef
instance Data StringRef
-- | A lightweight wrapper around the QuickCheck library. It introduces the
-- notion of a test suite, and it stores the test results for later
-- inspection (e.g., for the generation of a test report). A test suite
-- has a monadic interface.
module Ideas.Common.Utils.TestSuite
type TestSuite = TestSuiteM ()
-- | Monads in which IO computations may be embedded. Any monad
-- built by applying a sequence of monad transformers to the IO
-- monad will be an instance of this class.
--
-- Instances should satisfy the following laws, which state that
-- liftIO is a transformer of monads:
--
--
class Monad m => MonadIO (m :: * -> *)
liftIO :: MonadIO m => IO a -> m a
-- | Construct a (named) test suite containing tests and other suites
suite :: String -> TestSuite -> TestSuite
-- | Add a QuickCheck property to the test suite. The first argument is a
-- label for the property
addProperty :: Testable prop => String -> prop -> TestSuite
-- | Add a QuickCheck property to the test suite, also providing a test
-- configuration (Args)
addPropertyWith :: Testable prop => String -> Args -> prop -> TestSuite
warn :: String -> TestSuite
assertTrue :: String -> Bool -> TestSuite
assertNull :: Show a => String -> [a] -> TestSuite
assertEquals :: (Eq a, Show a) => String -> a -> a -> TestSuite
assertIO :: String -> IO Bool -> TestSuite
runTestSuite :: TestSuite -> IO ()
runTestSuiteResult :: TestSuite -> IO TestSuiteResult
data TestSuiteResult
subResults :: TestSuiteResult -> [(String, TestSuiteResult)]
findSubResult :: String -> TestSuiteResult -> Maybe TestSuiteResult
messages :: TestSuiteResult -> [Message]
topMessages :: TestSuiteResult -> [Message]
numberOfTests :: TestSuiteResult -> Int
makeSummary :: TestSuiteResult -> String
printSummary :: TestSuiteResult -> IO ()
data Message
newMessage :: String -> Message
isError :: Message -> Bool
warning :: Message -> Message
messageLabel :: Message -> Maybe String
instance Show Message
instance Show TestSuiteResult
instance Monoid TestSuiteResult
instance Monoid a => Monoid (TestSuiteM a)
instance MonadIO TestSuiteM
instance Monad TestSuiteM
-- | Exports a subset of Data.Generics.Uniplate.Direct (the
-- Uniplate type class and its utility plus constructor
-- functions)
module Ideas.Common.Utils.Uniplate
-- | The standard Uniplate class, all operations require this. All
-- definitions must define uniplate, while descend and
-- descendM are optional.
class Uniplate on
uniplate :: Uniplate on => on -> (Str on, Str on -> on)
descend :: Uniplate on => (on -> on) -> on -> on
descendM :: (Uniplate on, Monad m) => (on -> m on) -> on -> m on
-- | Get the direct children of a node. Usually using universe is
-- more appropriate.
children :: Uniplate on => on -> [on]
-- | Return all the contexts and holes.
--
--
-- universe x == map fst (contexts x)
-- all (== x) [b a | (a,b) <- contexts x]
--
contexts :: Uniplate on => on -> [(on, on -> on)]
-- | Perform a transformation on all the immediate children, then combine
-- them back. This operation allows additional information to be passed
-- downwards, and can be used to provide a top-down transformation. This
-- function can be defined explicitly, or can be provided by
-- automatically in terms of uniplate.
--
-- For example, on the sample type, we could write:
--
--
-- descend f (Val i ) = Val i
-- descend f (Neg a ) = Neg (f a)
-- descend f (Add a b) = Add (f a) (f b)
--
descend :: Uniplate on => (on -> on) -> on -> on
-- | Monadic variant of descend
descendM :: Uniplate on => forall (m :: * -> *). Monad m => (on -> m on) -> on -> m on
-- | The one depth version of contexts
--
--
-- children x == map fst (holes x)
-- all (== x) [b a | (a,b) <- holes x]
--
holes :: Uniplate on => on -> [(on, on -> on)]
-- | Perform a fold-like computation on each value, technically a
-- paramorphism
para :: Uniplate on => (on -> [r] -> r) -> on -> r
-- | Rewrite by applying a rule everywhere you can. Ensures that the rule
-- cannot be applied anywhere in the result:
--
--
-- propRewrite r x = all (isNothing . r) (universe (rewrite r x))
--
--
-- Usually transform is more appropriate, but rewrite can
-- give better compositionality. Given two single transformations
-- f and g, you can construct f mplus g
-- which performs both rewrites until a fixed point.
rewrite :: Uniplate on => (on -> Maybe on) -> on -> on
-- | Monadic variant of rewrite
rewriteM :: (Monad m, Uniplate on) => (on -> m (Maybe on)) -> on -> m on
-- | Transform every element in the tree, in a bottom-up manner.
--
-- For example, replacing negative literals with literals:
--
--
-- negLits = transform f
-- where f (Neg (Lit i)) = Lit (negate i)
-- f x = x
--
transform :: Uniplate on => (on -> on) -> on -> on
-- | Monadic variant of transform
transformM :: (Monad m, Uniplate on) => (on -> m on) -> on -> m on
-- | The underlying method in the class. Taking a value, the function
-- should return all the immediate children of the same type, and a
-- function to replace them.
--
-- Given uniplate x = (cs, gen)
--
-- cs should be a Str on, constructed of Zero,
-- One and Two, containing all x's direct
-- children of the same type as x. gen should take a
-- Str on with exactly the same structure as cs, and
-- generate a new element with the children replaced.
--
-- Example instance:
--
--
-- instance Uniplate Expr where
-- uniplate (Val i ) = (Zero , \Zero -> Val i )
-- uniplate (Neg a ) = (One a , \(One a) -> Neg a )
-- uniplate (Add a b) = (Two (One a) (One b), \(Two (One a) (One b)) -> Add a b)
--
uniplate :: Uniplate on => on -> (Str on, Str on -> on)
-- | Get all the children of a node, including itself and all children.
--
--
-- universe (Add (Val 1) (Neg (Val 2))) =
-- [Add (Val 1) (Neg (Val 2)), Val 1, Neg (Val 2), Val 2]
--
--
-- This method is often combined with a list comprehension, for example:
--
--
-- vals x = [i | Val i <- universe x]
--
universe :: Uniplate on => on -> [on]
-- | The field to the right does not contain the target.
(|-) :: Type (item -> from) to -> item -> Type from to
-- | The field to the right is the target.
(|*) :: Type (to -> from) to -> to -> Type from to
-- | The field to the right is a list of the type of the target
(||*) :: Type ([to] -> from) to -> [to] -> Type from to
-- | The main combinator used to start the chain.
--
-- The following rule can be used for optimisation:
--
--
-- plate Ctor |- x == plate (Ctor x)
--
plate :: from -> Type from to
-- | A collection of general utility functions
module Ideas.Common.Utils
data Some f
Some :: (f a) -> Some f
data ShowString
ShowString :: String -> ShowString
fromShowString :: ShowString -> String
readInt :: String -> Maybe Int
readM :: (Monad m, Read a) => String -> m a
subsets :: [a] -> [[a]]
isSubsetOf :: Eq a => [a] -> [a] -> Bool
cartesian :: [a] -> [b] -> [(a, b)]
distinct :: Eq a => [a] -> Bool
allsame :: Eq a => [a] -> Bool
fixpoint :: Eq a => (a -> a) -> a -> a
splitAtElem :: Eq a => a -> [a] -> Maybe ([a], [a])
splitsWithElem :: Eq a => a -> [a] -> [[a]]
-- | Use a fixed standard random number generator. This generator is
-- accessible by calling System.Random.getStdGen
useFixedStdGen :: IO ()
timedSeconds :: Int -> IO a -> IO a
fst3 :: (a, b, c) -> a
snd3 :: (a, b, c) -> b
thd3 :: (a, b, c) -> c
headM :: Monad m => [a] -> m a
findIndexM :: Monad m => (a -> Bool) -> [a] -> m Int
elementAt :: Monad m => Int -> [a] -> m a
changeAt :: Monad m => Int -> (a -> a) -> [a] -> m [a]
replaceAt :: Monad m => Int -> a -> [a] -> m [a]
list :: b -> ([a] -> b) -> [a] -> b
instance Eq ShowString
instance Ord ShowString
instance Show ShowString
module Ideas.Common.Traversal.Utils
class Update f
update :: Update f => f a -> (a, a -> f a)
current :: Update f => f a -> a
change :: Update f => (a -> a) -> f a -> f a
replace :: Update f => a -> f a -> f a
changeM :: Update f => (a -> Maybe a) -> f a -> Maybe (f a)
changeG :: (Update f, Monad g) => (a -> g a) -> f a -> g (f a)
class Focus a where type family Unfocus a focus = fromMaybe (error "no focus") . focusM focusM = Just . focus
focus :: Focus a => Unfocus a -> a
focusM :: Focus a => Unfocus a -> Maybe a
unfocus :: Focus a => a -> Unfocus a
liftFocus :: Focus a => (Unfocus a -> Maybe (Unfocus a)) -> a -> Maybe a
unliftFocus :: Focus a => (a -> Maybe a) -> Unfocus a -> Maybe (Unfocus a)
class Wrapper f
wrap :: Wrapper f => a -> f a
unwrap :: Wrapper f => f a -> a
liftWrapper :: (Monad m, Wrapper f) => (a -> m a) -> f a -> m (f a)
unliftWrapper :: (Monad m, Wrapper f) => (f a -> m (f a)) -> a -> m a
mapWrapper :: Wrapper f => (a -> a) -> f a -> f a
data Mirror a
makeMirror :: a -> Mirror a
(>|<) :: (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a
safe :: (a -> Maybe a) -> a -> a
fixp :: (a -> Maybe a) -> a -> a
fixpl :: (a -> Maybe a) -> a -> [a]
-- | an associative operation
mplus :: MonadPlus m => forall a. m a -> m a -> m a
-- | Left-to-right Kleisli composition of monads.
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> a -> m c
instance Show a => Show (Mirror a)
instance Eq a => Eq (Mirror a)
instance Wrapper Mirror
module Ideas.Common.Traversal.Iterator
class Iterator a where first = fixp previous final = fixp next position = pred . length . fixpl previous
next :: Iterator a => a -> Maybe a
previous :: Iterator a => a -> Maybe a
first :: Iterator a => a -> a
final :: Iterator a => a -> a
position :: Iterator a => a -> Int
isFirst :: Iterator a => a -> Bool
isFinal :: Iterator a => a -> Bool
hasNext :: Iterator a => a -> Bool
hasPrevious :: Iterator a => a -> Bool
searchForward :: Iterator a => (a -> Bool) -> a -> Maybe a
searchBackward :: Iterator a => (a -> Bool) -> a -> Maybe a
searchNext :: Iterator a => (a -> Bool) -> a -> Maybe a
searchPrevious :: Iterator a => (a -> Bool) -> a -> Maybe a
searchWith :: (a -> Maybe a) -> (a -> Bool) -> a -> Maybe a
data ListIterator a
instance Eq a => Eq (ListIterator a)
instance Arbitrary a => Arbitrary (ListIterator a)
instance Update ListIterator
instance Focus (ListIterator a)
instance Iterator (ListIterator a)
instance Show a => Show (ListIterator a)
instance Iterator a => Iterator (Mirror a)
-- | Type classes and instances.
module Ideas.Common.Classes
-- | A type class for functors that can be applied to a value.
-- Transformation, Rule, and Strategy are all instances of this type
-- class.
class Apply t
applyAll :: Apply t => t a -> a -> [a]
-- | Returns zero or one results
apply :: Apply t => t a -> a -> Maybe a
-- | Checks whether the functor is applicable (at least one result)
applicable :: Apply t => t a -> a -> Bool
-- | If not applicable, return the current value (as default)
applyD :: Apply t => t a -> a -> a
-- | Same as apply, except that the result (at most one) is returned in
-- some monad
applyM :: (Apply t, Monad m) => t a -> a -> m a
applyList :: Apply t => [t a] -> a -> Maybe a
-- | Instances should satisfy the following law: getSingleton .
-- singleton == Just
class Container f
singleton :: Container f => a -> f a
getSingleton :: Container f => f a -> Maybe a
-- | Type class for bi-directional arrows. - should be used
-- instead of arr from the arrow interface. Minimal complete
-- definition: -.
class Arrow arr => BiArrow arr where !-> f = f <-> errBiArrow <-! f = errBiArrow <-> f
(<->) :: BiArrow arr => (a -> b) -> (b -> a) -> arr a b
(!->) :: BiArrow arr => (a -> b) -> arr a b
(<-!) :: BiArrow arr => (b -> a) -> arr a b
class BiFunctor f where mapFirst = flip biMap id mapSecond = biMap id
biMap :: BiFunctor f => (a -> c) -> (b -> d) -> f a b -> f c d
mapFirst :: BiFunctor f => (a -> b) -> f a c -> f b c
mapSecond :: BiFunctor f => (b -> c) -> f a b -> f a c
mapBoth :: BiFunctor f => (a -> b) -> f a a -> f b b
class Buggy a where buggy = setBuggy True
buggy :: Buggy a => a -> a
setBuggy :: Buggy a => Bool -> a -> a
isBuggy :: Buggy a => a -> Bool
class Minor a where minor = setMinor True isMajor = not . isMinor
minor :: Minor a => a -> a
setMinor :: Minor a => Bool -> a -> a
isMinor :: Minor a => a -> Bool
isMajor :: Minor a => a -> Bool
instance BiFunctor (,)
instance BiFunctor Either
instance Container Set
instance Container []
-- | Identification of entities
module Ideas.Common.Id
data Id
class IsId a where concatId = mconcat . map newId
newId :: IsId a => a -> Id
concatId :: IsId a => [a] -> Id
class HasId a
getId :: HasId a => a -> Id
changeId :: HasId a => (Id -> Id) -> a -> a
class HasId a => Identify a
(@>) :: (Identify a, IsId n) => n -> a -> a
(#) :: (IsId a, IsId b) => a -> b -> Id
sameId :: (IsId a, IsId b) => a -> b -> Bool
unqualified :: HasId a => a -> String
qualifiers :: HasId a => a -> [String]
qualification :: HasId a => a -> String
describe :: HasId a => String -> a -> a
description :: HasId a => a -> String
showId :: HasId a => a -> String
compareId :: HasId a => a -> a -> Ordering
-- | Identity of mappend
mempty :: Monoid a => a
isEmptyId :: Id -> Bool
listQualify :: (IsId a, IsId b) => [a] -> b -> Id
instance Typeable Id
instance Data Id
instance (HasId a, HasId b) => HasId (Either a b)
instance HasId Id
instance (IsId a, IsId b) => IsId (Either a b)
instance IsId a => IsId (Maybe a)
instance (IsId a, IsId b, IsId c) => IsId (a, b, c)
instance (IsId a, IsId b) => IsId (a, b)
instance IsId ()
instance IsId a => IsId [a]
instance IsId Char
instance IsId Id
instance Arbitrary Id
instance Monoid Id
instance Ord Id
instance Eq Id
instance Read Id
instance Show Id
-- | This module defines views on data-types, as described in Canonical
-- Forms in Interactive Exercise Assistants
module Ideas.Common.View
-- | The basic arrow class.
--
-- Minimal complete definition: arr and first, satisfying
-- the laws
--
--
--
-- where
--
--
-- assoc ((a,b),c) = (a,(b,c))
--
--
-- The other combinators have sensible default definitions, which may be
-- overridden for efficiency.
class Category a => Arrow (a :: * -> * -> *)
arr :: Arrow a => (b -> c) -> a b c
first :: Arrow a => a b c -> a (b, d) (c, d)
second :: Arrow a => a b c -> a (d, b) (d, c)
(***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')
(&&&) :: Arrow a => a b c -> a b c' -> a b (c, c')
-- | Choice, for arrows that support it. This class underlies the
-- if and case constructs in arrow notation. Minimal
-- complete definition: left, satisfying the laws
--
--
--
-- where
--
--
-- assocsum (Left (Left x)) = Left x
-- assocsum (Left (Right y)) = Right (Left y)
-- assocsum (Right z) = Right (Right z)
--
--
-- The other combinators have sensible default definitions, which may be
-- overridden for efficiency.
class Arrow a => ArrowChoice (a :: * -> * -> *)
left :: ArrowChoice a => a b c -> a (Either b d) (Either c d)
right :: ArrowChoice a => a b c -> a (Either d b) (Either d c)
(+++) :: ArrowChoice a => a b c -> a b' c' -> a (Either b b') (Either c c')
(|||) :: ArrowChoice a => a b d -> a c d -> a (Either b c) d
class Arrow a => ArrowZero (a :: * -> * -> *)
zeroArrow :: ArrowZero a => a b c
-- | A monoid on arrows.
class ArrowZero a => ArrowPlus (a :: * -> * -> *)
(<+>) :: ArrowPlus a => a b c -> a b c -> a b c
-- | Left-to-right composition
(>>>) :: Category cat => cat a b -> cat b c -> cat a c
-- | Right-to-left composition
(<<<) :: Category cat => cat b c -> cat a b -> cat a c
class IsMatcher f where match = runKleisli . unM . matcher matcher = makeMatcher . match
match :: IsMatcher f => f a b -> a -> Maybe b
matcher :: IsMatcher f => f a b -> Matcher a b
-- | generalized monadic variant of match
matchM :: (Monad m, IsMatcher f) => f a b -> a -> m b
belongsTo :: IsMatcher f => a -> f a b -> Bool
viewEquivalent :: (IsMatcher f, Eq b) => f a b -> a -> a -> Bool
viewEquivalentWith :: IsMatcher f => (b -> b -> Bool) -> f a b -> a -> a -> Bool
data Matcher a b
makeMatcher :: (a -> Maybe b) -> Matcher a b
-- | Minimal complete definition: toView or both match
-- and build.
class IsMatcher f => IsView f where build f = build (toView f) toView f = makeView (match f) (build f)
build :: IsView f => f a b -> b -> a
toView :: IsView f => f a b -> View a b
simplify :: IsView f => f a b -> a -> a
simplifyWith :: IsView f => (b -> b) -> f a b -> a -> a
simplifyWithM :: IsView f => (b -> Maybe b) -> f a b -> a -> a
canonical :: IsView f => f a b -> a -> Maybe a
canonicalWith :: IsView f => (b -> b) -> f a b -> a -> Maybe a
canonicalWithM :: IsView f => (b -> Maybe b) -> f a b -> a -> Maybe a
isCanonical :: (IsView f, Eq a) => f a b -> a -> Bool
isCanonicalWith :: IsView f => (a -> a -> Bool) -> f a b -> a -> Bool
data View a b
identity :: Category f => f a a
makeView :: (a -> Maybe b) -> (b -> a) -> View a b
matcherView :: Matcher a b -> (b -> a) -> View a b
data Isomorphism a b
from :: Isomorphism a b -> a -> b
to :: Isomorphism a b -> b -> a
inverse :: Isomorphism a b -> Isomorphism b a
class LiftView f where liftView v = liftViewIn (v &&& identity)
liftView :: LiftView f => View a b -> f b -> f a
liftViewIn :: LiftView f => View a (b, c) -> f b -> f a
swapView :: Isomorphism (a, b) (b, a)
-- | Specialized version of traverseView
listView :: View a b -> View [a] [b]
traverseView :: Traversable f => View a b -> View (f a) (f b)
($<) :: Traversable f => View a (f b) -> View b c -> View a (f c)
data ViewPackage
ViewPackage :: (String -> Maybe a) -> View a b -> ViewPackage
propIdempotence :: (Show a, Eq a) => Gen a -> View a b -> Property
propSoundness :: Show a => (a -> a -> Bool) -> Gen a -> View a c -> Property
propNormalForm :: (Show a, Eq a) => Gen a -> View a b -> Property
instance Category Matcher
instance Arrow Matcher
instance ArrowZero Matcher
instance ArrowPlus Matcher
instance ArrowChoice Matcher
instance HasId ViewPackage
instance Identify (Isomorphism a b)
instance HasId (Isomorphism a b)
instance IsView Isomorphism
instance IsMatcher Isomorphism
instance ArrowChoice Isomorphism
instance BiArrow Isomorphism
instance Arrow Isomorphism
instance Category Isomorphism
instance Identify (View a b)
instance HasId (View a b)
instance IsView View
instance IsMatcher View
instance ArrowChoice View
instance BiArrow View
instance Arrow View
instance Category View
instance IsMatcher Matcher
-- | A simple data type for term rewriting
module Ideas.Common.Rewriting.Term
data Symbol
newSymbol :: IsId a => a -> Symbol
isAssociative :: Symbol -> Bool
makeAssociative :: Symbol -> Symbol
data Term
TVar :: String -> Term
TCon :: Symbol -> [Term] -> Term
TList :: [Term] -> Term
TNum :: Integer -> Term
TFloat :: Double -> Term
TMeta :: Int -> Term
class IsTerm a
toTerm :: IsTerm a => a -> Term
fromTerm :: (IsTerm a, MonadPlus m) => Term -> m a
termView :: IsTerm a => View Term a
fromTermM :: (Monad m, IsTerm a) => Term -> m a
fromTermWith :: (Monad m, IsTerm a) => (Symbol -> [a] -> m a) -> Term -> m a
class WithFunctions a where symbol s = function s [] getSymbol a = case getFunction a of { Just (t, []) -> return t _ -> fail "Ideas.Common.Term.getSymbol" }
symbol :: WithFunctions a => Symbol -> a
function :: WithFunctions a => Symbol -> [a] -> a
getSymbol :: (WithFunctions a, Monad m) => a -> m Symbol
getFunction :: (WithFunctions a, Monad m) => a -> m (Symbol, [a])
isSymbol :: WithFunctions a => Symbol -> a -> Bool
isFunction :: (WithFunctions a, Monad m) => Symbol -> a -> m [a]
unary :: WithFunctions a => Symbol -> a -> a
binary :: WithFunctions a => Symbol -> a -> a -> a
isUnary :: (WithFunctions a, Monad m) => Symbol -> a -> m a
isBinary :: (WithFunctions a, Monad m) => Symbol -> a -> m (a, a)
class WithVars a
variable :: WithVars a => String -> a
getVariable :: (WithVars a, Monad m) => a -> m String
isVariable :: WithVars a => a -> Bool
vars :: (Uniplate a, WithVars a) => a -> [String]
varSet :: (Uniplate a, WithVars a) => a -> Set String
hasVar :: (Uniplate a, WithVars a) => String -> a -> Bool
withoutVar :: (Uniplate a, WithVars a) => String -> a -> Bool
hasSomeVar :: (Uniplate a, WithVars a) => a -> Bool
hasNoVar :: (Uniplate a, WithVars a) => a -> Bool
variableView :: WithVars a => View a String
class WithMetaVars a
metaVar :: WithMetaVars a => Int -> a
getMetaVar :: (WithMetaVars a, Monad m) => a -> m Int
isMetaVar :: WithMetaVars a => a -> Bool
metaVars :: (Uniplate a, WithMetaVars a) => a -> [Int]
metaVarSet :: (Uniplate a, WithMetaVars a) => a -> IntSet
hasMetaVar :: (Uniplate a, WithMetaVars a) => Int -> a -> Bool
nextMetaVar :: (Uniplate a, WithMetaVars a) => a -> Int
instance Typeable Term
instance Show Term
instance Read Term
instance Eq Term
instance Ord Term
instance Arbitrary Term
instance WithMetaVars Term
instance WithVars Term
instance WithFunctions Term
instance IsTerm a => IsTerm [a]
instance IsTerm Char
instance IsTerm Double
instance IsTerm Integer
instance IsTerm Int
instance (IsTerm a, IsTerm b) => IsTerm (Either a b)
instance (IsTerm a, IsTerm b) => IsTerm (a, b)
instance IsTerm ShowString
instance IsTerm Term
instance Uniplate Term
instance HasId Symbol
instance Read Symbol
instance Show Symbol
instance Ord Symbol
instance Eq Symbol
-- | References, bindings, and heterogenous environments
module Ideas.Common.Environment
-- | A data type for references (without a value)
data Ref a
-- | A type class for types as references
class (IsTerm a, Typeable a, Show a, Read a) => Reference a where makeRef n = Ref (newId n) show readM termView makeRefList n = Ref (newId n) show readM termView
makeRef :: (Reference a, IsId n) => n -> Ref a
makeRefList :: (Reference a, IsId n) => n -> Ref [a]
data Binding
makeBinding :: Typeable a => Ref a -> a -> Binding
fromBinding :: Typeable a => Binding -> Maybe (Ref a, a)
showValue :: Binding -> String
getTermValue :: Binding -> Term
data Environment
makeEnvironment :: [Binding] -> Environment
singleBinding :: Typeable a => Ref a -> a -> Environment
class HasEnvironment env where deleteRef a = changeEnv (Env . delete (getId a) . envMap) insertRef ref = let f b = Env . insert (getId b) b . envMap in changeEnv . f . Binding ref changeRef ref f env = maybe id (insertRef ref . f) (ref ? env) env
environment :: HasEnvironment env => env -> Environment
setEnvironment :: HasEnvironment env => Environment -> env -> env
deleteRef :: HasEnvironment env => Ref a -> env -> env
insertRef :: (HasEnvironment env, Typeable a) => Ref a -> a -> env -> env
changeRef :: (HasEnvironment env, Typeable a) => Ref a -> (a -> a) -> env -> env
class HasRefs a where getRefIds a = [getId r | Some r <- getRefs a] getRefs = sortBy cmp . nubBy eq . allRefs where cmp :: Some Ref -> Some Ref -> Ordering cmp (Some x) (Some y) = compareId (getId x) (getId y) eq a b = cmp a b == EQ
getRefs :: HasRefs a => a -> [Some Ref]
allRefs :: HasRefs a => a -> [Some Ref]
getRefIds :: HasRefs a => a -> [Id]
bindings :: HasEnvironment env => env -> [Binding]
noBindings :: HasEnvironment env => env -> Bool
(?) :: (HasEnvironment env, Typeable a) => Ref a -> env -> Maybe a
instance Eq Environment
instance HasEnvironment Environment
instance HasRefs Environment
instance Monoid Environment
instance Show Environment
instance HasId Binding
instance Eq Binding
instance Show Binding
instance (Reference a, Reference b) => Reference (a, b)
instance Reference a => Reference [a]
instance Reference Char
instance Reference Term
instance Reference Int
instance HasId (Ref a)
instance Eq (Ref a)
instance Show (Ref a)
-- | State monad for environments
module Ideas.Common.Rule.EnvironmentMonad
data EnvMonad a
(:=) :: Ref a -> a -> EnvMonad ()
(:~) :: Ref a -> (a -> a) -> EnvMonad ()
(:?) :: Ref a -> a -> EnvMonad a
getRef :: Typeable a => Ref a -> EnvMonad a
updateRefs :: MonadPlus m => [EnvMonad a] -> Environment -> m Environment
runEnvMonad :: EnvMonad a -> Environment -> [(a, Environment)]
execEnvMonad :: EnvMonad a -> Environment -> [Environment]
evalEnvMonad :: EnvMonad a -> Environment -> [a]
envMonadRefs :: EnvMonad a -> [Some Ref]
envMonadFunctionRefs :: (a -> EnvMonad b) -> [Some Ref]
instance MonadPlus EnvMonad
instance Monad EnvMonad
-- | Substitutions on terms. Substitutions are idempotent, and non-cyclic.
module Ideas.Common.Rewriting.Substitution
-- | Abstract data type for substitutions
data Substitution
-- | Returns the empty substitution
emptySubst :: Substitution
-- | Returns a singleton substitution
singletonSubst :: Int -> Term -> Substitution
-- | Returns the domain of a substitution (as a set)
dom :: Substitution -> IntSet
-- | Lookups a variable in a substitution. Nothing indicates that the
-- variable is not in the domain of the substitution
lookupVar :: Int -> Substitution -> Maybe Term
-- | Combines two substitutions. The left-hand side substitution is first
-- applied to the co-domain of the right-hand side substitution
(@@) :: Substitution -> Substitution -> Substitution
-- | Apply the substitution
(|->) :: Substitution -> Term -> Term
-- | Turns a list into a substitution
listToSubst :: [(Int, Term)] -> Substitution
composable :: Substitution -> Substitution -> Bool
(@+@) :: Substitution -> Substitution -> Maybe Substitution
tests :: TestSuite
instance Eq Substitution
instance Arbitrary Substitution
instance Show Substitution
instance Monoid Substitution
-- | Compute the difference of two terms generically, taking associativity
-- into account.
module Ideas.Common.Rewriting.Difference
difference :: IsTerm a => a -> a -> Maybe (a, a)
-- | This function returns the difference, except that the returned terms
-- should be logically equivalent. Nothing can signal that there is no
-- difference, or that the terms to start with are not equivalent.
differenceEqual :: IsTerm a => (a -> a -> Bool) -> a -> a -> Maybe (a, a)
differenceWith :: View Term a -> a -> a -> Maybe (a, a)
differenceEqualWith :: View Term a -> (a -> a -> Bool) -> a -> a -> Maybe (a, a)
-- | Datatype for representing a derivation (parameterized both in the
-- terms and the steps)
module Ideas.Common.Derivation
data Derivation s a
emptyDerivation :: a -> Derivation s a
prepend :: (a, s) -> Derivation s a -> Derivation s a
extend :: Derivation s a -> (s, a) -> Derivation s a
-- | Tests whether the derivation is empty
isEmpty :: Derivation s a -> Bool
-- | Returns the number of steps in a derivation
derivationLength :: Derivation s a -> Int
-- | All terms in a derivation
terms :: Derivation s a -> [a]
-- | All steps in a derivation
steps :: Derivation s a -> [s]
-- | The triples of a derivation, consisting of the before term, the step,
-- and the after term.
triples :: Derivation s a -> [(a, s, a)]
firstTerm :: Derivation s a -> a
lastTerm :: Derivation s a -> a
lastStep :: Derivation s a -> Maybe s
withoutLast :: Derivation s a -> Derivation s a
updateSteps :: (a -> s -> a -> t) -> Derivation s a -> Derivation t a
-- | Apply a monadic function to each term, and to each step
derivationM :: Monad m => (s -> m ()) -> (a -> m ()) -> Derivation s a -> m ()
instance BiFunctor Derivation
instance Functor (Derivation s)
instance (Show s, Show a) => Show (Derivation s a)
-- | Datatype for representing derivations as a tree. The datatype stores
-- all intermediate results as well as annotations for the steps.
module Ideas.Common.DerivationTree
data DerivationTree s a
-- | Constructs a node without branches; the boolean indicates whether the
-- node is an endpoint or not
singleNode :: a -> Bool -> DerivationTree s a
-- | Branches are attached after the existing ones (order matters)
addBranches :: [(s, DerivationTree s a)] -> DerivationTree s a -> DerivationTree s a
makeTree :: (a -> (Bool, [(s, a)])) -> a -> DerivationTree s a
-- | The root of the tree
root :: DerivationTree s a -> a
-- | Is this node an endpoint?
endpoint :: DerivationTree s a -> Bool
-- | All branches
branches :: DerivationTree s a -> [(s, DerivationTree s a)]
-- | Returns all subtrees at a given node
subtrees :: DerivationTree s a -> [DerivationTree s a]
-- | Returns all leafs, i.e., final results in derivation. Be careful: the
-- returned list may be very long
leafs :: DerivationTree s a -> [a]
-- | The argument supplied is the maximum number of steps; if more steps
-- are needed, Nothing is returned
lengthMax :: Int -> DerivationTree s a -> Maybe Int
-- | Restrict the height of the tree (by cutting off branches at a certain
-- depth). Nodes at this particular depth are turned into endpoints
restrictHeight :: Int -> DerivationTree s a -> DerivationTree s a
-- | Restrict the width of the tree (by cutting off branches).
restrictWidth :: Int -> DerivationTree s a -> DerivationTree s a
updateAnnotations :: (a -> s -> a -> t) -> DerivationTree s a -> DerivationTree t a
cutOnStep :: (s -> Bool) -> DerivationTree s a -> DerivationTree s a
mergeMaybeSteps :: DerivationTree (Maybe s) a -> DerivationTree s a
sortTree :: (l -> l -> Ordering) -> DerivationTree l a -> DerivationTree l a
cutOnTerm :: (a -> Bool) -> DerivationTree s a -> DerivationTree s a
-- | The first derivation (if any)
derivation :: DerivationTree s a -> Maybe (Derivation s a)
-- | Return a random derivation (if any exists at all)
randomDerivation :: RandomGen g => g -> DerivationTree s a -> Maybe (Derivation s a)
-- | All possible derivations (returned in a list)
derivations :: DerivationTree s a -> [Derivation s a]
instance (Show s, Show a) => Show (DerivationTree s a)
instance BiFunctor DerivationTree
instance Functor (DerivationTree s)
module Ideas.Common.Rewriting.AC
type Pairings a = a -> a -> [[(a, a)]]
type PairingsList a b = [a] -> [b] -> [[([a], [b])]]
type PairingsPair a b = (a, a) -> (b, b) -> [[(a, b)]]
pairingsNone :: PairingsPair a b
pairingsA :: Bool -> PairingsList a b
pairingsMatchA :: (a -> [b] -> c) -> [a] -> [b] -> [[c]]
pairingsC :: PairingsPair a b
pairingsAC :: Bool -> PairingsList a b
module Ideas.Common.Rewriting.Unification
unify :: Term -> Term -> Maybe Substitution
match :: MonadPlus m => Term -> Term -> m Substitution
matchExtended :: Map Symbol SymbolMatch -> Term -> Term -> [(Substitution, Maybe Term, Maybe Term)]
matchList :: Match Term -> Match [Term]
type Match a = a -> a -> [Substitution]
type SymbolMatch = Match Term -> [Term] -> Term -> [Substitution]
unificationTests :: TestSuite
module Ideas.Common.Rewriting.RewriteRule
class Different a
different :: Different a => (a, a)
data RewriteRule a
ruleSpecTerm :: RewriteRule a -> RuleSpec Term
data RuleSpec a
(:~>) :: a -> a -> RuleSpec a
makeRewriteRule :: (IsId n, RuleBuilder f a) => n -> f -> RewriteRule a
class (IsTerm a, Show a) => RuleBuilder t a | t -> a
buildRuleSpec :: RuleBuilder t a => Int -> t -> RuleSpec Term
showRewriteRule :: Bool -> RewriteRule a -> Maybe String
metaInRewriteRule :: RewriteRule a -> [Int]
renumberRewriteRule :: Int -> RewriteRule a -> RewriteRule a
symbolMatcher :: Symbol -> SymbolMatch -> RewriteRule a -> RewriteRule a
symbolBuilder :: Symbol -> ([Term] -> Term) -> RewriteRule a -> RewriteRule a
instance Show a => Show (RuleSpec a)
instance Apply RewriteRule
instance (Different a, RuleBuilder t b) => RuleBuilder (a -> t) b
instance (IsTerm a, Show a) => RuleBuilder (RuleSpec a) a
instance Different Char
instance Different a => Different [a]
instance HasId (RewriteRule a)
instance Show (RewriteRule a)
instance Functor RuleSpec
module Ideas.Common.Rewriting
module Ideas.Common.Algebra.Law
data Law a
data LawSpec a
(:==:) :: a -> a -> LawSpec a
law :: LawBuilder l a => String -> l -> Law a
mapLaw :: (b -> a) -> (a -> b) -> Law a -> Law b
propertyLaw :: (Arbitrary a, Show a, Testable b) => (a -> a -> b) -> Law a -> Property
rewriteLaw :: (Different a, IsTerm a, Arbitrary a, Show a) => Law a -> RewriteRule a
instance (Arbitrary a, IsTerm a, Show a, Different a) => RuleBuilder (LawSpec a) a
instance (Show a, Eq a, Arbitrary a) => Testable (Law a)
instance LawBuilder b a => LawBuilder (a -> b) a
instance LawBuilder (LawSpec a) a
instance Show (Law a)
module Ideas.Common.Algebra.Group
-- | The class of monoids (types with an associative binary operation that
-- has an identity). Instances should satisfy the following laws:
--
--
--
-- The method names refer to the monoid of lists under concatenation, but
-- there are many other instances.
--
-- Minimal complete definition: mempty and mappend.
--
-- Some types can be viewed as a monoid in more than one way, e.g. both
-- addition and multiplication on numbers. In such cases we often define
-- newtypes and make those instances of Monoid, e.g.
-- Sum and Product.
class Monoid a
mempty :: Monoid a => a
mappend :: Monoid a => a -> a -> a
mconcat :: Monoid a => [a] -> a
-- | An infix synonym for mappend.
(<>) :: Monoid m => m -> m -> m
-- | Minimal complete definition: inverse or appendInverse
class Monoid a => Group a where inverse = (mempty <>-) appendInv a b = a <> inverse b
inverse :: Group a => a -> a
appendInv :: Group a => a -> a -> a
(<>-) :: Group a => a -> a -> a
class Monoid a => MonoidZero a
mzero :: MonoidZero a => a
data WithZero a
fromWithZero :: WithZero a -> Maybe a
class CoMonoid a
isEmpty :: CoMonoid a => a -> Bool
isAppend :: CoMonoid a => a -> Maybe (a, a)
class CoMonoid a => CoGroup a where isAppendInv = const Nothing
isInverse :: CoGroup a => a -> Maybe a
isAppendInv :: CoGroup a => a -> Maybe (a, a)
class CoMonoid a => CoMonoidZero a
isMonoidZero :: CoMonoidZero a => a -> Bool
associativeList :: CoMonoid a => a -> [a]
instance Eq a => Eq (WithZero a)
instance Ord a => Ord (WithZero a)
instance Functor WithZero
instance Foldable WithZero
instance Traversable WithZero
instance Applicative WithZero
instance CoMonoid a => CoMonoidZero (WithZero a)
instance CoMonoid a => CoMonoid (WithZero a)
instance CoMonoid (Set a)
instance CoMonoid [a]
instance Monoid a => MonoidZero (WithZero a)
instance Monoid a => Monoid (WithZero a)
module Ideas.Common.Algebra.GroupLaws
associative :: Monoid a => Law a
leftIdentity :: Monoid a => Law a
rightIdentity :: Monoid a => Law a
identityLaws :: Monoid a => [Law a]
monoidLaws :: Monoid a => [Law a]
commutativeMonoidLaws :: Monoid a => [Law a]
-- | Not all monoids are idempotent (see: idempotentFor)
idempotent :: Monoid a => Law a
leftInverse :: Group a => Law a
rightInverse :: Group a => Law a
doubleInverse :: Group a => Law a
inverseIdentity :: Group a => Law a
inverseDistrFlipped :: Group a => Law a
inverseLaws :: Group a => [Law a]
groupLaws :: Group a => [Law a]
appendInverseLaws :: Group a => [Law a]
commutative :: Monoid a => Law a
inverseDistr :: Group a => Law a
abelianGroupLaws :: Group a => [Law a]
leftZero :: MonoidZero a => Law a
rightZero :: MonoidZero a => Law a
zeroLaws :: MonoidZero a => [Law a]
monoidZeroLaws :: MonoidZero a => [Law a]
associativeFor :: (a -> a -> a) -> Law a
commutativeFor :: (a -> a -> a) -> Law a
idempotentFor :: (a -> a -> a) -> Law a
leftDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
rightDistributiveFor :: (a -> a -> a) -> (a -> a -> a) -> Law a
module Ideas.Common.Algebra.Field
class SemiRing a where sum [] = zero sum xs = foldl1 (<+>) xs product [] = one product xs = foldl1 (<*>) xs
(<+>) :: SemiRing a => a -> a -> a
zero :: SemiRing a => a
sum :: SemiRing a => [a] -> a
(<*>) :: SemiRing a => a -> a -> a
one :: SemiRing a => a
product :: SemiRing a => [a] -> a
class SemiRing a => Ring a where plusInverse = (zero <->) a <-> b = a <+> plusInverse b
plusInverse :: Ring a => a -> a
(<->) :: Ring a => a -> a -> a
class Ring a => Field a where timesInverse = (one >) a > b = a <*> timesInverse b
timesInverse :: Field a => a -> a
(>) :: Field a => a -> a -> a
newtype Additive a
Additive :: a -> Additive a
fromAdditive :: Additive a -> a
newtype Multiplicative a
Multiplicative :: a -> Multiplicative a
fromMultiplicative :: Multiplicative a -> a
data SafeNum a
safeNum :: SafeNum a -> Either String a
class CoSemiRing a
isPlus :: CoSemiRing a => a -> Maybe (a, a)
isZero :: CoSemiRing a => a -> Bool
isTimes :: CoSemiRing a => a -> Maybe (a, a)
isOne :: CoSemiRing a => a -> Bool
class CoSemiRing a => CoRing a where isMinus _ = Nothing
isNegate :: CoRing a => a -> Maybe a
isMinus :: CoRing a => a -> Maybe (a, a)
class CoRing a => CoField a where isDivision _ = Nothing
isRecip :: CoField a => a -> Maybe a
isDivision :: CoField a => a -> Maybe (a, a)
instance Show a => Show (Additive a)
instance Eq a => Eq (Additive a)
instance Ord a => Ord (Additive a)
instance Arbitrary a => Arbitrary (Additive a)
instance CoArbitrary a => CoArbitrary (Additive a)
instance Show a => Show (Multiplicative a)
instance Eq a => Eq (Multiplicative a)
instance Ord a => Ord (Multiplicative a)
instance Arbitrary a => Arbitrary (Multiplicative a)
instance CoArbitrary a => CoArbitrary (Multiplicative a)
instance CoSemiRing a => CoMonoidZero (Multiplicative a)
instance CoField a => CoGroup (Multiplicative a)
instance CoSemiRing a => CoMonoid (Multiplicative a)
instance CoRing a => CoGroup (Additive a)
instance CoSemiRing a => CoMonoid (Additive a)
instance (Eq a, Fractional a) => Field (SafeNum a)
instance Num a => Ring (SafeNum a)
instance Num a => SemiRing (SafeNum a)
instance (Eq a, Fractional a) => Fractional (SafeNum a)
instance Num a => Num (SafeNum a)
instance Monad SafeNum
instance Functor SafeNum
instance Show a => Show (SafeNum a)
instance Ord a => Ord (SafeNum a)
instance Eq a => Eq (SafeNum a)
instance Arbitrary a => Arbitrary (SafeNum a)
instance SemiRing a => MonoidZero (Multiplicative a)
instance Field a => Group (Multiplicative a)
instance SemiRing a => Monoid (Multiplicative a)
instance Applicative Multiplicative
instance Functor Multiplicative
instance Ring a => Group (Additive a)
instance SemiRing a => Monoid (Additive a)
instance Applicative Additive
instance Functor Additive
module Ideas.Common.Algebra.FieldLaws
leftDistributive :: SemiRing a => Law a
rightDistributive :: SemiRing a => Law a
distributiveLaws :: SemiRing a => [Law a]
semiRingLaws :: SemiRing a => [Law a]
leftNegateTimes :: Ring a => Law a
rightNegateTimes :: Ring a => Law a
negateTimesLaws :: Ring a => [Law a]
ringLaws :: Ring a => [Law a]
commutativeRingLaws :: Ring a => [Law a]
distributiveSubtractionLaws :: Ring a => [Law a]
exchangeInverses :: Field a => Law a
fieldLaws :: Field a => [Law a]
fromAdditiveLaw :: Law (Additive a) -> Law a
fromMultiplicativeLaw :: Law (Multiplicative a) -> Law a
propsField :: [Property]
module Ideas.Common.Traversal.Navigator
data Location
toLocation :: [Int] -> Location
fromLocation :: Location -> [Int]
-- | For a minimal complete definition, provide an implemention for downs
-- or allDowns. All other functions need an implementation as well,
-- except for change. Note that a constructor (a -> f a) is not
-- included in the type class to allow additional type class constraints
-- on type a.
class Navigator a where downLast = liftM (fixp right) . down childnr = pred . length . fixpl left location = toLocation . map childnr . drop 1 . reverse . fixpl up
up :: Navigator a => a -> Maybe a
down :: Navigator a => a -> Maybe a
downLast :: Navigator a => a -> Maybe a
left :: Navigator a => a -> Maybe a
right :: Navigator a => a -> Maybe a
childnr :: Navigator a => a -> Int
location :: Navigator a => a -> Location
isTop :: Navigator a => a -> Bool
isLeaf :: Navigator a => a -> Bool
hasLeft :: Navigator a => a -> Bool
hasRight :: Navigator a => a -> Bool
hasUp :: Navigator a => a -> Bool
hasDown :: Navigator a => a -> Bool
top :: Navigator a => a -> a
leftMost :: Navigator a => a -> a
rightMost :: Navigator a => a -> a
leftMostLeaf :: Navigator a => a -> a
rightMostLeaf :: Navigator a => a -> a
depth :: Navigator a => a -> Int
level :: Navigator a => a -> Int
levelNext :: Navigator a => a -> Maybe a
levelPrevious :: Navigator a => a -> Maybe a
leftMostAt :: Navigator a => Int -> a -> Maybe a
rightMostAt :: Navigator a => Int -> a -> Maybe a
downs :: Navigator a => a -> [a]
downTo :: Navigator a => Int -> a -> Maybe a
arity :: Navigator a => a -> Int
navigateTo :: Navigator a => Location -> a -> Maybe a
navigateTowards :: Navigator a => Location -> a -> a
data PreOrder a
makePreOrder :: a -> PreOrder a
data PostOrder a
makePostOrder :: a -> PostOrder a
data LevelOrder a
makeLevelOrder :: a -> LevelOrder a
data Horizontal a
makeHorizontal :: a -> Horizontal a
data Leafs a
makeLeafs :: Navigator a => a -> Leafs a
data UniplateNavigator a
instance Eq Location
instance Ord Location
instance Show a => Show (PreOrder a)
instance Eq a => Eq (PreOrder a)
instance Show a => Show (PostOrder a)
instance Eq a => Eq (PostOrder a)
instance Navigator a => Iterator (PostOrder a)
instance Show a => Show (LevelOrder a)
instance Eq a => Eq (LevelOrder a)
instance Show a => Show (Horizontal a)
instance Eq a => Eq (Horizontal a)
instance Show a => Show (Leafs a)
instance Eq a => Eq (Leafs a)
instance (Arbitrary a, Uniplate a) => Arbitrary (UniplateNavigator a)
instance Uniplate a => Focus (UniplateNavigator a)
instance Update UniplateNavigator
instance Uniplate a => Navigator (UniplateNavigator a)
instance (Eq a, Uniplate a) => Eq (UniplateNavigator a)
instance (Show a, Uniplate a) => Show (UniplateNavigator a)
instance Update StrIterator
instance Focus (StrIterator a)
instance Iterator (StrIterator a)
instance Focus (StrNavigator a)
instance Navigator (StrNavigator a)
instance Navigator a => Iterator (Leafs a)
instance Update Leafs
instance Wrapper Leafs
instance Navigator a => Iterator (Horizontal a)
instance Update Horizontal
instance Wrapper Horizontal
instance Navigator a => Iterator (LevelOrder a)
instance Update LevelOrder
instance Wrapper LevelOrder
instance Update PostOrder
instance Wrapper PostOrder
instance Navigator a => Iterator (PreOrder a)
instance Update PreOrder
instance Wrapper PreOrder
instance Navigator a => Navigator (Mirror a)
instance Monoid Location
instance Show Location
-- | A context for a term that maintains an environment of key-value pairs.
-- A context is both showable and parsable.
module Ideas.Common.Context
-- | Abstract data type for a context: a context stores an envrionent
-- (key-value pairs) and a value
data Context a
-- | Construct a context
newContext :: Environment -> ContextNavigator a -> Context a
fromContext :: Monad m => Context a -> m a
fromContextWith :: Monad m => (a -> b) -> Context a -> m b
fromContextWith2 :: Monad m => (a -> b -> c) -> Context a -> Context b -> m c
data Location
location :: Navigator a => a -> Location
data ContextNavigator a
noNavigator :: a -> ContextNavigator a
navigator :: Uniplate a => a -> ContextNavigator a
termNavigator :: IsTerm a => a -> ContextNavigator a
-- | Lift a rule to operate on a term in a context
liftToContext :: LiftView f => f a -> f (Context a)
contextView :: View (Context a) (a, Context a)
use :: (LiftView f, IsTerm a, IsTerm b) => f a -> f (Context b)
useC :: (LiftView f, IsTerm a, IsTerm b) => f (Context a) -> f (Context b)
-- | Apply a function at top-level. Afterwards, try to return the focus to
-- the old position
applyTop :: (a -> a) -> Context a -> Context a
currentTerm :: Context a -> Maybe Term
changeTerm :: (Term -> Maybe Term) -> Context a -> Maybe (Context a)
replaceInContext :: a -> Context a -> Context a
currentInContext :: Context a -> Maybe a
changeInContext :: (a -> a) -> Context a -> Context a
instance HasEnvironment (Context a)
instance Navigator (Context a)
instance Show a => Show (Context a)
instance Eq a => Eq (Context a)
-- | This module defines transformations. Given a term, a transformation
-- returns a list of results (often a singleton list or the empty list).
module Ideas.Common.Rule.Transformation
type Transformation a = Trans a a
data Trans a b
-- | A type class for constructing a transformation. If possible,
-- makeTrans should be used. Use specialized constructor
-- functions for disambiguation.
class MakeTrans f
makeTrans :: MakeTrans f => (a -> f b) -> Trans a b
transPure :: (a -> b) -> Trans a b
transMaybe :: (a -> Maybe b) -> Trans a b
transList :: (a -> [b]) -> Trans a b
transEnvMonad :: (a -> EnvMonad b) -> Trans a b
transRewrite :: RewriteRule a -> Trans a a
transRef :: Typeable a => Ref a -> Trans a a
transUseEnvironment :: Trans a b -> Trans (a, Environment) (b, Environment)
transLiftView :: View a b -> Transformation b -> Transformation a
transLiftViewIn :: View a (b, c) -> Transformation b -> Transformation a
transLiftContext :: Transformation a -> Transformation (Context a)
transLiftContextIn :: Transformation (a, Environment) -> Transformation (Context a)
-- | Overloaded variant of transLiftContext
makeTransLiftContext :: MakeTrans f => (a -> f a) -> Transformation (Context a)
-- | Overloaded variant of transLiftContext; ignores result
makeTransLiftContext_ :: MakeTrans f => (a -> f ()) -> Transformation (Context a)
transApply :: Trans a b -> a -> [(b, Environment)]
transApplyWith :: Environment -> Trans a b -> a -> [(b, Environment)]
getRewriteRules :: Trans a b -> [Some RewriteRule]
isZeroTrans :: Trans a b -> Bool
instance HasRefs (Trans a b)
instance MakeTrans EnvMonad
instance MakeTrans []
instance MakeTrans Maybe
instance Monoid (Trans a b)
instance ArrowApply Trans
instance ArrowChoice Trans
instance ArrowPlus Trans
instance ArrowZero Trans
instance Arrow Trans
instance Category Trans
-- | This module defines transformations. Given a term, a transformation
-- returns a list of results (often a singleton list or the empty list).
-- A transformation can be parameterized with one or more Bindables.
-- Transformations rules can be lifted to work on more complex domains
-- with the LiftView type class.
module Ideas.Common.Rule.Parameter
type ParamTrans a b = Trans (a, b) b
supplyParameters :: ParamTrans b a -> (a -> Maybe b) -> Transformation a
supplyContextParameters :: ParamTrans b a -> (a -> EnvMonad b) -> Transformation (Context a)
parameter1 :: (IsId n1, Reference a) => n1 -> (a -> Transformation b) -> ParamTrans a b
parameter2 :: (IsId n1, IsId n2, Reference a, Reference b) => n1 -> n2 -> (a -> b -> Transformation c) -> ParamTrans (a, b) c
parameter3 :: (IsId n1, IsId n2, IsId n3, Reference a, Reference b, Reference c) => n1 -> n2 -> n3 -> (a -> b -> c -> Transformation d) -> ParamTrans (a, b, c) d
module Ideas.Common.Rule.Recognizer
class Recognizable f where recognizeAll r a b = map snd $ transApply (recognizeTrans r) (a, b) recognize r a b = listToMaybe $ recognizeAll r a b recognizeTrans = unR . recognizer
recognizer :: Recognizable f => f a -> Recognizer a
recognizeAll :: Recognizable f => f a -> a -> a -> [Environment]
recognize :: Recognizable f => f a -> a -> a -> Maybe Environment
recognizeTrans :: Recognizable f => f a -> Trans (a, a) ()
data Recognizer a
makeRecognizer :: (a -> a -> Bool) -> Recognizer a
makeRecognizerEnvMonad :: (a -> a -> EnvMonad ()) -> Recognizer a
makeRecognizerTrans :: Trans (a, a) () -> Recognizer a
instance HasRefs (Recognizer a)
instance Recognizable Recognizer
instance Monoid (Recognizer a)
instance LiftView Recognizer
-- | A rule is just a transformation with some meta-information, such as a
-- name (which should be unique) and properties such as buggy or
-- minor. Rules can be lifted with a view using the LiftView type
-- class.
module Ideas.Common.Rule.Abstract
-- | Abstract data type for representing rules
data Rule a
transformation :: Rule a -> Transformation a
recognizer :: Recognizable f => f a -> Recognizer a
checkReferences :: Rule a -> Environment -> Maybe String
makeRule :: (IsId n, MakeTrans f) => n -> (a -> f a) -> Rule a
ruleMaybe :: IsId n => n -> (a -> Maybe a) -> Rule a
ruleList :: IsId n => n -> (a -> [a]) -> Rule a
ruleTrans :: IsId n => n -> Transformation a -> Rule a
ruleRewrite :: RewriteRule a -> Rule a
buggyRule :: (IsId n, MakeTrans f) => n -> (a -> f a) -> Rule a
minorRule :: (IsId n, MakeTrans f) => n -> (a -> f a) -> Rule a
rewriteRule :: (IsId n, RuleBuilder f a) => n -> f -> Rule a
rewriteRules :: (IsId n, RuleBuilder f a) => n -> [f] -> Rule a
-- | A special (minor) rule that always returns the identity
idRule :: IsId n => n -> Rule a
-- | A special (minor) rule that checks a predicate (and returns the
-- identity if the predicate holds)
checkRule :: IsId n => n -> (a -> Bool) -> Rule a
-- | A special (minor) rule that is never applicable (i.e., this rule
-- always fails)
emptyRule :: IsId n => n -> Rule a
ruleSiblings :: Rule a -> [Id]
siblingOf :: HasId b => b -> Rule a -> Rule a
isRewriteRule :: Rule a -> Bool
isRecognizer :: Rule a -> Bool
-- | Perform the function after the rule has been fired
doAfter :: (a -> a) -> Rule a -> Rule a
addRecognizer :: Recognizer a -> Rule a -> Rule a
addRecognizerBool :: (a -> a -> Bool) -> Rule a -> Rule a
addTransRecognizer :: (a -> a -> Bool) -> Rule a -> Rule a
addRecognizerEnvMonad :: (a -> a -> EnvMonad ()) -> Rule a -> Rule a
instance HasRefs (Rule a)
instance (Arbitrary a, CoArbitrary a) => Arbitrary (Rule a)
instance Minor (Rule a)
instance Buggy (Rule a)
instance Recognizable Rule
instance LiftView Rule
instance HasId (Rule a)
instance Apply Rule
instance Ord (Rule a)
instance Eq (Rule a)
instance Show (Rule a)
module Ideas.Common.Rule
-- | The core strategy combinators. This module defines the interal data
-- structure of a strategy, and some utility functions that operate
-- directly on it.
module Ideas.Common.Strategy.Core
-- | A generalized Core expression, not restricted to rules. This makes
-- GCore a (traversable and foldable) functor.
data GCore l a
(:*:) :: GCore l a -> GCore l a -> GCore l a
(:|:) :: GCore l a -> GCore l a -> GCore l a
(:|>:) :: GCore l a -> GCore l a -> GCore l a
(:%:) :: GCore l a -> GCore l a -> GCore l a
(:!%:) :: GCore l a -> GCore l a -> GCore l a
Many :: (GCore l a) -> GCore l a
Repeat :: (GCore l a) -> GCore l a
Not :: (GCore l a) -> GCore l a
Label :: l -> (GCore l a) -> GCore l a
Atomic :: (GCore l a) -> GCore l a
Succeed :: GCore l a
Fail :: GCore l a
-- | Generalized constructor (not restricted to rules)
Rule :: a -> GCore l a
Var :: Int -> GCore l a
Rec :: Int -> (GCore l a) -> GCore l a
-- | Core expression, with rules
type Core l a = GCore l (Rule a)
(.|.) :: GCore l a -> GCore l a -> GCore l a
(.*.) :: GCore l a -> GCore l a -> GCore l a
(.%.) :: GCore l a -> GCore l a -> GCore l a
coreMany :: GCore l a -> GCore l a
coreRepeat :: GCore l a -> GCore l a
coreOrElse :: GCore l a -> GCore l a -> GCore l a
coreFix :: (GCore l a -> GCore l a) -> GCore l a
noLabels :: GCore l a -> GCore l a
substCoreVar :: Int -> GCore l a -> GCore l a -> GCore l a
instance (Show l, Show a) => Show (GCore l a)
instance (Arbitrary l, Arbitrary a) => Arbitrary (GCore l a)
instance Foldable (GCore l)
instance Traversable (GCore l)
instance BiFunctor GCore
instance Uniplate (GCore l a)
instance Functor (GCore l)
-- | Basic machinery for executing a core strategy expression.
module Ideas.Common.Strategy.Parsing
data Step l a
Enter :: l -> Step l a
Exit :: l -> Step l a
RuleStep :: Environment -> (Rule a) -> Step l a
data State l a
makeState :: Core l a -> a -> State l a
stack :: State l a -> Stack l a
choices :: State l a -> [Bool]
trace :: State l a -> [Step l a]
value :: State l a -> a
parseDerivationTree :: Bool -> State l a -> DerivationTree (Step l a) (State l a)
replay :: Monad m => Int -> [Bool] -> Core l a -> m (State l a)
runCore :: Core l a -> a -> [a]
firsts :: Bool -> State l a -> [(Result (Step l a), State l a)]
data Result a
Result :: a -> Result a
Ready :: Result a
isReady :: Result a -> Bool
instance Show l => Show (Step l a)
instance Eq l => Eq (Step l a)
instance Show l => Show (Stack l a)
instance (Show l, Show a) => Show (State l a)
instance Show a => Show (Result a)
instance Functor Result
instance Minor (Step l a)
instance Apply (Step l)
module Ideas.Common.Strategy.Abstract
-- | Abstract data type for strategies
data Strategy a
-- | Type class to turn values into strategies
class IsStrategy f
toStrategy :: IsStrategy f => f a -> Strategy a
-- | A strategy which is labeled with a string
data LabeledStrategy a
-- | Labels a strategy with a string
label :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a
-- | Removes the label from a strategy
unlabel :: LabeledStrategy a -> Strategy a
-- | Returns the derivation tree for a strategy and a term, including all
-- minor rules
fullDerivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Step LabelInfo a) a
-- | Returns the derivation tree for a strategy and a term with only major
-- rules
derivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Rule a, Environment) a
-- | Returns a list of all major rules that are part of a labeled strategy
rulesInStrategy :: IsStrategy f => f a -> [Rule a]
-- | Apply a function to all the rules that make up a labeled strategy
mapRules :: (Rule a -> Rule b) -> LabeledStrategy a -> LabeledStrategy b
mapRulesS :: (Rule a -> Rule b) -> Strategy a -> Strategy b
-- | Use a function as do-after hook for all rules in a labeled strategy,
-- but also use the function beforehand
cleanUpStrategy :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a
-- | Use a function as do-after hook for all rules in a labeled strategy
cleanUpStrategyAfter :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a
toCore :: Strategy a -> Core LabelInfo a
fromCore :: Core LabelInfo a -> Strategy a
liftCore :: IsStrategy f => (Core LabelInfo a -> Core LabelInfo a) -> f a -> Strategy a
liftCore2 :: (IsStrategy f, IsStrategy g) => (Core LabelInfo a -> Core LabelInfo a -> Core LabelInfo a) -> f a -> g a -> Strategy a
makeLabeledStrategy :: IsStrategy f => LabelInfo -> f a -> LabeledStrategy a
toLabeledStrategy :: Monad m => Strategy a -> m (LabeledStrategy a)
data LabelInfo
processLabelInfo :: (l -> LabelInfo) -> Core l a -> Core l a
changeInfo :: IsLabeled f => (LabelInfo -> LabelInfo) -> f a -> LabeledStrategy a
makeInfo :: IsId a => a -> LabelInfo
removed :: LabelInfo -> Bool
collapsed :: LabelInfo -> Bool
hidden :: LabelInfo -> Bool
class IsLabeled f
toLabeled :: IsLabeled f => f a -> LabeledStrategy a
noInterleaving :: IsStrategy f => f a -> Strategy a
instance Eq LabelInfo
instance Ord LabelInfo
instance LiftView Strategy
instance LiftView LabeledStrategy
instance IsLabeled RewriteRule
instance IsLabeled Rule
instance IsLabeled LabeledStrategy
instance HasId (LabeledStrategy a)
instance Apply LabeledStrategy
instance Show (LabeledStrategy a)
instance IsStrategy RewriteRule
instance IsStrategy Rule
instance IsStrategy LabeledStrategy
instance IsStrategy Strategy
instance Arbitrary LabelInfo
instance HasId LabelInfo
instance Show LabelInfo
instance (Arbitrary a, CoArbitrary a) => Arbitrary (Strategy a)
instance Apply Strategy
instance Show (Strategy a)
module Ideas.Common.Strategy.Configuration
data StrategyConfiguration
makeStrategyConfiguration :: [ConfigItem] -> StrategyConfiguration
type ConfigItem = (ConfigLocation, ConfigAction)
data ConfigLocation
byName :: HasId a => a -> ConfigLocation
byGroup :: HasId a => a -> ConfigLocation
data ConfigAction
Remove :: ConfigAction
Reinsert :: ConfigAction
Collapse :: ConfigAction
Expand :: ConfigAction
Hide :: ConfigAction
Reveal :: ConfigAction
configActions :: [ConfigAction]
configure :: StrategyConfiguration -> LabeledStrategy a -> LabeledStrategy a
configureNow :: LabeledStrategy a -> LabeledStrategy a
remove :: IsLabeled f => f a -> LabeledStrategy a
reinsert :: IsLabeled f => f a -> LabeledStrategy a
collapse :: IsLabeled f => f a -> LabeledStrategy a
expand :: IsLabeled f => f a -> LabeledStrategy a
hide :: IsLabeled f => f a -> LabeledStrategy a
reveal :: IsLabeled f => f a -> LabeledStrategy a
instance Show ConfigLocation
instance Show ConfigAction
instance Enum ConfigAction
instance Show StrategyConfiguration
-- | A collection of strategy combinators: all lifted to work on different
-- data types
module Ideas.Common.Strategy.Combinators
-- | Put two strategies in sequence (first do this, then do that)
(<*>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Choose between the two strategies (either do this or do that)
(<|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Interleave two strategies
(<%>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | The strategy that always succeeds (without doing anything)
succeed :: Strategy a
-- | The strategy that always fails
fail :: Strategy a
-- | Makes a strategy atomic (w.r.t. parallel composition)
atomic :: IsStrategy f => f a -> Strategy a
-- | Puts a list of strategies into a sequence
sequence :: IsStrategy f => [f a] -> Strategy a
-- | Combines a list of alternative strategies
alternatives :: IsStrategy f => [f a] -> Strategy a
-- | Merges a list of strategies (in parallel)
interleave :: IsStrategy f => [f a] -> Strategy a
-- | Allows all permutations of the list
permute :: IsStrategy f => [f a] -> Strategy a
-- | Repeat a strategy zero or more times (non-greedy)
many :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy at least once (non-greedy)
many1 :: IsStrategy f => f a -> Strategy a
-- | Apply a strategy a certain number of times
replicate :: IsStrategy f => Int -> f a -> Strategy a
-- | Apply a certain strategy or do nothing (non-greedy)
option :: IsStrategy f => f a -> Strategy a
-- | Checks whether a predicate holds for the current term. The check is
-- considered to be a minor step.
check :: (a -> Bool) -> Strategy a
-- | Check whether or not the argument strategy cannot be applied: the
-- result strategy only succeeds if this is not the case (otherwise it
-- fails).
not :: IsStrategy f => f a -> Strategy a
-- | Repeat a strategy zero or more times (greedy version of many)
repeat :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy at least once (greedy version of
-- many1)
repeat1 :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy if this is possible (greedy version of
-- option)
try :: IsStrategy f => f a -> Strategy a
-- | Left-biased choice: if the left-operand strategy can be applied, do
-- so. Otherwise, try the right-operand strategy
(|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Repeat the strategy as long as the predicate holds
while :: IsStrategy f => (a -> Bool) -> f a -> Strategy a
-- | Repeat the strategy until the predicate holds
until :: IsStrategy f => (a -> Bool) -> f a -> Strategy a
-- | Apply a strategy at least once, but collapse into a single step
multi :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a
-- | Apply the strategies from the list exhaustively (until this is no
-- longer possible)
exhaustive :: IsStrategy f => [f a] -> Strategy a
-- | A fix-point combinator on strategies (to model recursion). Powerful
-- (but dangerous) combinator
fix :: (Strategy a -> Strategy a) -> Strategy a
-- | Locations in a strategy
module Ideas.Common.Strategy.Location
subTaskLocation :: LabeledStrategy a -> Id -> Id -> Id
nextTaskLocation :: LabeledStrategy a -> Id -> Id -> Id
-- | Returns a list of all strategy locations, paired with the labeled
-- substrategy at that location
strategyLocations :: LabeledStrategy a -> [([Int], LabeledStrategy a)]
-- | Returns the substrategy or rule at a strategy location. Nothing
-- indicates that the location is invalid
subStrategy :: Id -> LabeledStrategy a -> Maybe (LabeledStrategy a)
-- | A prefix encodes a sequence of steps already performed (a so-called
-- trace), and allows to continue the derivation at that particular
-- point.
module Ideas.Common.Strategy.Prefix
-- | Abstract data type for a (labeled) strategy with a prefix (a sequence
-- of executed rules). A prefix is still aware of the labels that
-- appear in the strategy. A prefix is encoded as a list of integers (and
-- can be reconstructed from such a list: see makePrefix). The
-- list is stored in reversed order.
data Prefix a
-- | Construct the empty prefix for a labeled strategy
emptyPrefix :: LabeledStrategy a -> Prefix a
-- | Construct a prefix for a given list of integers and a labeled
-- strategy.
makePrefix :: Monad m => [Int] -> LabeledStrategy a -> m (Prefix a)
prefixToSteps :: Prefix a -> [Step LabelInfo a]
-- | Create a derivation tree with a prefix as annotation.
prefixTree :: Bool -> Prefix a -> a -> DerivationTree (Prefix a) a
-- | Retrieves the rules from a list of steps
stepsToRules :: [Step l a] -> [Rule a]
-- | Returns the last rule of a prefix (if such a rule exists)
lastStepInPrefix :: Prefix a -> Maybe (Step LabelInfo a)
-- | Calculate the active labels
activeLabels :: Prefix a -> [LabelInfo]
instance Eq (Prefix a)
instance Show (Prefix a)
module Ideas.Common.Rewriting.Confluence
isConfluent :: [RewriteRule a] -> Bool
checkConfluence :: [RewriteRule a] -> IO ()
checkConfluenceWith :: Config -> [RewriteRule a] -> IO ()
somewhereM :: Uniplate a => (a -> [a]) -> a -> [a]
data Config
defaultConfig :: Config
showTerm :: Config -> Term -> String
complexity :: Config -> Term -> Int
termEquality :: Config -> Term -> Term -> Bool
module Ideas.Common.Strategy.Traversal
layer :: (IsStrategy f, Navigator a) => [Option a] -> f a -> Strategy a
traverse :: (IsStrategy f, Navigator a) => [Option a] -> f a -> Strategy a
data Option a
topdown :: Option a
bottomup :: Option a
leftToRight :: Option a
rightToLeft :: Option a
full :: Option a
spine :: Option a
stop :: Option a
once :: Option a
traversalFilter :: (a -> Bool) -> Option a
parentFilter :: Navigator a => (a -> [Int]) -> Option a
fulltd :: (IsStrategy f, Navigator a) => f a -> Strategy a
fullbu :: (IsStrategy f, Navigator a) => f a -> Strategy a
oncetd :: (IsStrategy f, Navigator a) => f a -> Strategy a
oncebu :: (IsStrategy f, Navigator a) => f a -> Strategy a
somewhere :: (IsStrategy f, Navigator a) => f a -> Strategy a
innermost :: (IsStrategy f, Navigator a) => f a -> Strategy a
outermost :: (IsStrategy f, Navigator a) => f a -> Strategy a
instance Monoid (Option a)
-- | A strategy is a context-free grammar with rules as symbols. Strategies
-- can be labeled with strings. A type class is introduced to lift all
-- the combinators that work on strategies, only to prevent that you have
-- to insert these lifting functions yourself.
module Ideas.Common.Strategy
-- | Abstract data type for strategies
data Strategy a
-- | A strategy which is labeled with a string
data LabeledStrategy a
-- | Type class to turn values into strategies
class IsStrategy f
toStrategy :: IsStrategy f => f a -> Strategy a
-- | Returns the derivation tree for a strategy and a term, including all
-- minor rules
fullDerivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Step LabelInfo a) a
-- | Returns the derivation tree for a strategy and a term with only major
-- rules
derivationTree :: IsStrategy f => Bool -> f a -> a -> DerivationTree (Rule a, Environment) a
-- | Put two strategies in sequence (first do this, then do that)
(<*>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Choose between the two strategies (either do this or do that)
(<|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Interleave two strategies
(<%>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | The strategy that always succeeds (without doing anything)
succeed :: Strategy a
-- | The strategy that always fails
fail :: Strategy a
-- | Makes a strategy atomic (w.r.t. parallel composition)
atomic :: IsStrategy f => f a -> Strategy a
-- | Labels a strategy with a string
label :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a
-- | Puts a list of strategies into a sequence
sequence :: IsStrategy f => [f a] -> Strategy a
-- | Combines a list of alternative strategies
alternatives :: IsStrategy f => [f a] -> Strategy a
-- | Merges a list of strategies (in parallel)
interleave :: IsStrategy f => [f a] -> Strategy a
-- | Allows all permutations of the list
permute :: IsStrategy f => [f a] -> Strategy a
-- | A fix-point combinator on strategies (to model recursion). Powerful
-- (but dangerous) combinator
fix :: (Strategy a -> Strategy a) -> Strategy a
-- | Repeat a strategy zero or more times (non-greedy)
many :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy at least once (non-greedy)
many1 :: IsStrategy f => f a -> Strategy a
-- | Apply a strategy a certain number of times
replicate :: IsStrategy f => Int -> f a -> Strategy a
-- | Apply a certain strategy or do nothing (non-greedy)
option :: IsStrategy f => f a -> Strategy a
-- | Checks whether a predicate holds for the current term. The check is
-- considered to be a minor step.
check :: (a -> Bool) -> Strategy a
-- | Check whether or not the argument strategy cannot be applied: the
-- result strategy only succeeds if this is not the case (otherwise it
-- fails).
not :: IsStrategy f => f a -> Strategy a
-- | Repeat a strategy zero or more times (greedy version of many)
repeat :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy at least once (greedy version of
-- many1)
repeat1 :: IsStrategy f => f a -> Strategy a
-- | Apply a certain strategy if this is possible (greedy version of
-- option)
try :: IsStrategy f => f a -> Strategy a
-- | Left-biased choice: if the left-operand strategy can be applied, do
-- so. Otherwise, try the right-operand strategy
(|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a
-- | Apply the strategies from the list exhaustively (until this is no
-- longer possible)
exhaustive :: IsStrategy f => [f a] -> Strategy a
-- | Repeat the strategy as long as the predicate holds
while :: IsStrategy f => (a -> Bool) -> f a -> Strategy a
-- | Repeat the strategy until the predicate holds
until :: IsStrategy f => (a -> Bool) -> f a -> Strategy a
-- | Apply a strategy at least once, but collapse into a single step
multi :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a
-- | Returns a list of all strategy locations, paired with the labeled
-- substrategy at that location
strategyLocations :: LabeledStrategy a -> [([Int], LabeledStrategy a)]
-- | Returns the substrategy or rule at a strategy location. Nothing
-- indicates that the location is invalid
subStrategy :: Id -> LabeledStrategy a -> Maybe (LabeledStrategy a)
subTaskLocation :: LabeledStrategy a -> Id -> Id -> Id
nextTaskLocation :: LabeledStrategy a -> Id -> Id -> Id
-- | Abstract data type for a (labeled) strategy with a prefix (a sequence
-- of executed rules). A prefix is still aware of the labels that
-- appear in the strategy. A prefix is encoded as a list of integers (and
-- can be reconstructed from such a list: see makePrefix). The
-- list is stored in reversed order.
data Prefix a
-- | Construct the empty prefix for a labeled strategy
emptyPrefix :: LabeledStrategy a -> Prefix a
-- | Construct a prefix for a given list of integers and a labeled
-- strategy.
makePrefix :: Monad m => [Int] -> LabeledStrategy a -> m (Prefix a)
-- | Create a derivation tree with a prefix as annotation.
prefixTree :: Bool -> Prefix a -> a -> DerivationTree (Prefix a) a
data Step l a
Enter :: l -> Step l a
Exit :: l -> Step l a
RuleStep :: Environment -> (Rule a) -> Step l a
prefixToSteps :: Prefix a -> [Step LabelInfo a]
-- | Retrieves the rules from a list of steps
stepsToRules :: [Step l a] -> [Rule a]
-- | Returns the last rule of a prefix (if such a rule exists)
lastStepInPrefix :: Prefix a -> Maybe (Step LabelInfo a)
-- | Use a function as do-after hook for all rules in a labeled strategy,
-- but also use the function beforehand
cleanUpStrategy :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a
-- | Use a function as do-after hook for all rules in a labeled strategy
cleanUpStrategyAfter :: (a -> a) -> LabeledStrategy a -> LabeledStrategy a
-- | Returns a list of all major rules that are part of a labeled strategy
rulesInStrategy :: IsStrategy f => f a -> [Rule a]
module Ideas.Common.Traversal.Tests
testIterator :: (Show a, Eq a, Iterator a) => String -> Gen a -> TestSuite
testNavigator :: (Show a, Eq a, Navigator a) => String -> Gen a -> TestSuite
tests :: TestSuite
uniGen :: Gen (UniplateNavigator (T Int))
listGen :: Gen (ListIterator Int)
instance Show a => Show (T a)
instance Eq a => Eq (T a)
instance Arbitrary a => Arbitrary (T a)
instance Uniplate (T a)
-- | Testing strategy combinator properties
module Ideas.Common.Strategy.Tests
tests :: TestSuite
instance Show Choice
instance Arbitrary Choice
instance Show Sequence
instance Arbitrary Sequence
instance Show Interleave
instance Arbitrary Interleave
instance SemiRing Interleave
instance SemiRing Sequence
instance MonoidZero Interleave
instance Monoid Interleave
instance MonoidZero Sequence
instance Monoid Sequence
instance Monoid Choice
instance Eq Interleave
instance Eq Sequence
instance Eq Choice
module Ideas.Common.Algebra.Boolean
class BoolValue a where true = fromBool True false = fromBool False fromBool b = if b then true else false
true :: BoolValue a => a
false :: BoolValue a => a
fromBool :: BoolValue a => Bool -> a
isTrue :: BoolValue a => a -> Bool
isFalse :: BoolValue a => a -> Bool
class BoolValue a => Boolean a
(<&&>) :: Boolean a => a -> a -> a
(<||>) :: Boolean a => a -> a -> a
complement :: Boolean a => a -> a
ands :: Boolean a => [a] -> a
ors :: Boolean a => [a] -> a
implies :: Boolean a => a -> a -> a
equivalent :: Boolean a => a -> a -> a
class BoolValue a => CoBoolean a
isAnd :: CoBoolean a => a -> Maybe (a, a)
isOr :: CoBoolean a => a -> Maybe (a, a)
isComplement :: CoBoolean a => a -> Maybe a
conjunctions :: CoBoolean a => a -> [a]
disjunctions :: CoBoolean a => a -> [a]
class MonoidZero a => DualMonoid a
(><) :: DualMonoid a => a -> a -> a
dualCompl :: DualMonoid a => a -> a
newtype And a
And :: a -> And a
fromAnd :: And a -> a
newtype Or a
Or :: a -> Or a
fromOr :: Or a -> a
instance Show a => Show (And a)
instance Eq a => Eq (And a)
instance Ord a => Ord (And a)
instance Arbitrary a => Arbitrary (And a)
instance CoArbitrary a => CoArbitrary (And a)
instance Show a => Show (Or a)
instance Eq a => Eq (Or a)
instance Ord a => Ord (Or a)
instance Arbitrary a => Arbitrary (Or a)
instance CoArbitrary a => CoArbitrary (Or a)
instance Boolean a => DualMonoid (Or a)
instance Boolean a => MonoidZero (Or a)
instance Boolean a => Monoid (Or a)
instance Applicative Or
instance Functor Or
instance Boolean a => DualMonoid (And a)
instance Boolean a => MonoidZero (And a)
instance Boolean a => Monoid (And a)
instance Applicative And
instance Functor And
instance CoBoolean a => CoMonoidZero (Or a)
instance CoBoolean a => CoMonoid (Or a)
instance CoBoolean a => CoMonoidZero (And a)
instance CoBoolean a => CoMonoid (And a)
instance Boolean b => Boolean (a -> b)
instance Boolean Bool
instance BoolValue b => BoolValue (a -> b)
instance BoolValue Bool
module Ideas.Common.Algebra.BooleanLaws
andOverOrLaws :: Boolean a => [Law a]
orOverAndLaws :: Boolean a => [Law a]
complementAndLaws :: Boolean a => [Law a]
complementOrLaws :: Boolean a => [Law a]
absorptionAndLaws :: Boolean a => [Law a]
absorptionOrLaws :: Boolean a => [Law a]
deMorganAnd :: Boolean a => Law a
deMorganOr :: Boolean a => Law a
doubleComplement :: Boolean a => Law a
complementTrue :: Boolean a => Law a
complementFalse :: Boolean a => Law a
booleanLaws :: Boolean a => [Law a]
fromAndLaw :: Law (And a) -> Law a
fromOrLaw :: Law (Or a) -> Law a
propsBoolean :: [Property]
module Ideas.Common.Algebra.SmartGroup
newtype Smart a
Smart :: a -> Smart a
fromSmart :: Smart a -> a
newtype SmartZero a
SmartZero :: a -> SmartZero a
fromSmartZero :: SmartZero a -> a
newtype SmartGroup a
SmartGroup :: a -> SmartGroup a
fromSmartGroup :: SmartGroup a -> a
newtype SmartField a
SmartField :: a -> SmartField a
fromSmartField :: SmartField a -> a
(.+.) :: (CoField a, Field a) => a -> a -> a
(.-.) :: (CoField a, Field a) => a -> a -> a
neg :: (CoField a, Field a) => a -> a
(.*.) :: (CoField a, Field a) => a -> a -> a
(./.) :: (CoField a, Field a) => a -> a -> a
(.&&.) :: (Boolean a, CoBoolean a) => a -> a -> a
(.||.) :: (Boolean a, CoBoolean a) => a -> a -> a
instance Show a => Show (Smart a)
instance Eq a => Eq (Smart a)
instance Ord a => Ord (Smart a)
instance CoMonoid a => CoMonoid (Smart a)
instance (CoMonoid a, MonoidZero a) => MonoidZero (Smart a)
instance CoMonoidZero a => CoMonoidZero (Smart a)
instance Show a => Show (SmartZero a)
instance Eq a => Eq (SmartZero a)
instance Ord a => Ord (SmartZero a)
instance (CoMonoidZero a, MonoidZero a) => MonoidZero (SmartZero a)
instance CoMonoid a => CoMonoid (SmartZero a)
instance CoMonoidZero a => CoMonoidZero (SmartZero a)
instance Show a => Show (SmartGroup a)
instance Eq a => Eq (SmartGroup a)
instance Ord a => Ord (SmartGroup a)
instance CoMonoid a => CoMonoid (SmartGroup a)
instance CoGroup a => CoGroup (SmartGroup a)
instance CoMonoidZero a => CoMonoidZero (SmartGroup a)
instance (CoGroup a, MonoidZero a, Group a) => MonoidZero (SmartGroup a)
instance CoSemiRing a => CoSemiRing (SmartField a)
instance CoRing a => CoRing (SmartField a)
instance CoField a => CoField (SmartField a)
instance (Boolean a, CoBoolean a) => Boolean (Smart a)
instance BoolValue a => BoolValue (Smart a)
instance (CoField a, Field a) => Field (SmartField a)
instance (CoField a, Field a) => Ring (SmartField a)
instance (CoField a, Field a) => SemiRing (SmartField a)
instance Applicative SmartField
instance Functor SmartField
instance (CoGroup a, Group a) => Group (SmartGroup a)
instance (CoGroup a, Group a) => Monoid (SmartGroup a)
instance Applicative SmartGroup
instance Functor SmartGroup
instance (CoMonoidZero a, MonoidZero a) => Monoid (SmartZero a)
instance Applicative SmartZero
instance Functor SmartZero
instance (CoMonoid a, Monoid a) => Monoid (Smart a)
instance Applicative Smart
instance Functor Smart
-- | Representation for predicates
module Ideas.Common.Predicate
data Predicate a
predicate :: (a -> Bool) -> Predicate a
predicateView :: View a b -> Predicate a
evalPredicate :: Predicate a -> a -> Bool
class BoolValue a where true = fromBool True false = fromBool False fromBool b = if b then true else false
true :: BoolValue a => a
false :: BoolValue a => a
fromBool :: BoolValue a => Bool -> a
isTrue :: BoolValue a => a -> Bool
isFalse :: BoolValue a => a -> Bool
class BoolValue a => Boolean a
(<&&>) :: Boolean a => a -> a -> a
(<||>) :: Boolean a => a -> a -> a
complement :: Boolean a => a -> a
ands :: Boolean a => [a] -> a
ors :: Boolean a => [a] -> a
implies :: Boolean a => a -> a -> a
equivalent :: Boolean a => a -> a -> a
instance Identify (Predicate a)
instance HasId (Predicate a)
instance Boolean (Predicate a)
instance BoolValue (Predicate a)
-- | This module defines the concept of an exercise
module Ideas.Common.Exercise
data Exercise a
makeExercise :: (Show a, Eq a, IsTerm a) => Exercise a
emptyExercise :: Exercise a
exerciseId :: Exercise a -> Id
status :: Exercise a -> Status
parser :: Exercise a -> String -> Either String a
prettyPrinter :: Exercise a -> a -> String
equivalence :: Exercise a -> Context a -> Context a -> Bool
similarity :: Exercise a -> Context a -> Context a -> Bool
ready :: Exercise a -> Predicate a
suitable :: Exercise a -> Predicate a
isReady :: Exercise a -> a -> Bool
isSuitable :: Exercise a -> a -> Bool
hasTermView :: Exercise a -> Maybe (View Term a)
strategy :: Exercise a -> LabeledStrategy (Context a)
navigation :: Exercise a -> a -> ContextNavigator a
canBeRestarted :: Exercise a -> Bool
extraRules :: Exercise a -> [Rule (Context a)]
ruleOrdering :: Exercise a -> Rule (Context a) -> Rule (Context a) -> Ordering
difference :: Exercise a -> a -> a -> Maybe (a, a)
differenceEqual :: Exercise a -> a -> a -> Maybe (a, a)
testGenerator :: Exercise a -> Maybe (Gen a)
randomExercise :: Exercise a -> Maybe (StdGen -> Maybe Difficulty -> a)
examples :: Exercise a -> [(Difficulty, a)]
getRule :: Monad m => Exercise a -> Id -> m (Rule (Context a))
simpleGenerator :: Gen a -> Maybe (StdGen -> Maybe Difficulty -> a)
useGenerator :: (a -> Bool) -> (Maybe Difficulty -> Gen a) -> Maybe (StdGen -> Maybe Difficulty -> a)
randomTerm :: Exercise a -> Maybe Difficulty -> IO a
randomTermWith :: StdGen -> Exercise a -> Maybe Difficulty -> Maybe a
ruleset :: Exercise a -> [Rule (Context a)]
makeContext :: Exercise a -> Environment -> a -> Context a
-- | Put a value into an empty environment
inContext :: Exercise a -> a -> Context a
recognizeRule :: Exercise a -> Rule (Context a) -> Context a -> Context a -> [(Location, Environment)]
ruleOrderingWith :: [Rule a] -> Rule a -> Rule a -> Ordering
ruleOrderingWithId :: HasId b => [b] -> Rule a -> Rule a -> Ordering
type Examples a = [(Difficulty, a)]
mapExamples :: (a -> b) -> Examples a -> Examples b
examplesContext :: Exercise a -> Examples (Context a)
data Difficulty
VeryEasy :: Difficulty
Easy :: Difficulty
Medium :: Difficulty
Difficult :: Difficulty
VeryDifficult :: Difficulty
readDifficulty :: String -> Maybe Difficulty
level :: Difficulty -> [a] -> Examples a
hasTypeable :: Exercise a -> Maybe (IsTypeable a)
useTypeable :: Typeable a => Maybe (IsTypeable a)
castFrom :: Typeable b => Exercise a -> a -> Maybe b
castTo :: Typeable b => Exercise a -> b -> Maybe a
data Status
-- | A released exercise that has undergone some thorough testing
Stable :: Status
-- | A released exercise, possibly with some deficiencies
Provisional :: Status
-- | An exercise that is under development
Alpha :: Status
-- | An exercise for experimentation purposes only
Experimental :: Status
-- | An exercise with the status Stable or Provisional
isPublic :: Exercise a -> Bool
-- | An exercise that is not public
isPrivate :: Exercise a -> Bool
-- | Function for defining equivalence or similarity without taking the
-- context into account.
withoutContext :: (a -> a -> Bool) -> Context a -> Context a -> Bool
-- | Similarity on terms without a context
simpleSimilarity :: Exercise a -> a -> a -> Bool
-- | Equivalence on terms without a context
simpleEquivalence :: Exercise a -> a -> a -> Bool
prettyPrinterContext :: Exercise a -> Context a -> String
restrictGenerator :: (a -> Bool) -> Gen a -> Gen a
-- | Shows a derivation for a given start term. The specified rule ordering
-- is used for selection.
showDerivation :: Exercise a -> a -> String
printDerivation :: Exercise a -> a -> IO ()
type ExerciseDerivation a = Derivation (Rule (Context a), Environment) (Context a)
defaultDerivation :: Exercise a -> a -> ExerciseDerivation a
derivationDiffEnv :: Derivation s (Context a) -> Derivation (s, Environment) (Context a)
checkExercise :: Exercise a -> IO ()
checkParserPretty :: (a -> a -> Bool) -> (String -> Either String a) -> (a -> String) -> a -> Bool
checkExamples :: Exercise a -> TestSuite
exerciseTestSuite :: Exercise a -> TestSuite
instance Eq Difficulty
instance Ord Difficulty
instance Enum Difficulty
instance Show Status
instance Eq Status
instance Show (ShowAs a)
instance Show Difficulty
instance HasId (Exercise a)
instance Apply Exercise
instance Ord (Exercise a)
instance Eq (Exercise a)
-- | Exports most from package Common
module Ideas.Common.Library
-- | Alias for strategy combinator fail
failS :: Strategy a
-- | Alias for strategy combinator not
notS :: IsStrategy f => f a -> Strategy a
-- | Alias for strategy combinator repeat
repeatS :: IsStrategy f => f a -> Strategy a
-- | Alias for strategy combinator replicate
replicateS :: IsStrategy f => Int -> f a -> Strategy a
-- | Alias for strategy combinator sequence
sequenceS :: IsStrategy f => [f a] -> Strategy a
-- | Alias for strategy combinator until
untilS :: IsStrategy f => (a -> Bool) -> f a -> Strategy a
-- | Abstract syntax for feedback scripts, and pretty-printer (Show
-- instance)
module Ideas.Service.FeedbackScript.Syntax
data Script
makeScript :: [Decl] -> Script
scriptDecls :: Script -> [Decl]
makeText :: String -> Text
textItems :: Text -> [Text]
data Decl
NameSpace :: [Id] -> Decl
Supports :: [Id] -> Decl
Include :: [FilePath] -> Decl
Simple :: DeclType -> [Id] -> Text -> Decl
Guarded :: DeclType -> [Id] -> [(Condition, Text)] -> Decl
data DeclType
TextForId :: DeclType
StringDecl :: DeclType
Feedback :: DeclType
data Text
TextString :: String -> Text
TextTerm :: Term -> Text
TextRef :: Id -> Text
TextEmpty :: Text
(:<>:) :: Text -> Text -> Text
data Condition
RecognizedIs :: Id -> Condition
CondNot :: Condition -> Condition
CondConst :: Bool -> Condition
CondRef :: Id -> Condition
includes :: Script -> [FilePath]
feedbackDecl :: HasId a => a -> Text -> Decl
textForIdDecl :: HasId a => a -> Text -> Decl
instance Uniplate Text
instance Uniplate Condition
instance Monoid Text
instance Monoid Script
instance Show Text
instance Show Condition
instance Show DeclType
instance Show Decl
instance Show Script
-- | Simple parser for feedback scripts
module Ideas.Service.FeedbackScript.Parser
parseScript :: FilePath -> IO Script
parseScriptSafe :: FilePath -> IO Script
data Script
-- | The information maintained for a learner trying to complete a
-- derivation.
module Ideas.Service.State
data State a
makeState :: Exercise a -> [Prefix (Context a)] -> Context a -> State a
makeNoState :: Exercise a -> Context a -> State a
emptyStateContext :: Exercise a -> Context a -> State a
emptyState :: Exercise a -> a -> State a
exercise :: State a -> Exercise a
statePrefixes :: State a -> [Prefix (Context a)]
stateContext :: State a -> Context a
stateTerm :: State a -> a
stateLabels :: State a -> [[LabelInfo]]
instance HasEnvironment (State a)
instance HasId (State a)
instance Show (State a)
module Ideas.Service.Types
data Service
makeService :: String -> String -> (forall a. TypedValue (Type a)) -> Service
deprecate :: Service -> Service
serviceDeprecated :: Service -> Bool
serviceFunction :: Service -> forall a. TypedValue (Type a)
data TypeRep f t
Iso :: Isomorphism t1 t2 -> TypeRep f t1 -> TypeRep f t2
(:->) :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (t1 -> t2)
Tag :: String -> TypeRep f t1 -> TypeRep f t1
List :: TypeRep f t -> TypeRep f [t]
Pair :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (t1, t2)
(:|:) :: TypeRep f t1 -> TypeRep f t2 -> TypeRep f (Either t1 t2)
Unit :: TypeRep f ()
Const :: f t -> TypeRep f t
data Const a t
Service :: Const a Service
Exercise :: Const a (Exercise a)
Strategy :: Const a (Strategy (Context a))
State :: Const a (State a)
Rule :: Const a (Rule (Context a))
Context :: Const a (Context a)
Id :: Const a Id
Location :: Const a Location
Script :: Const a Script
StratCfg :: Const a StrategyConfiguration
Environment :: Const a Environment
Text :: Const a Text
StdGen :: Const a StdGen
SomeExercise :: Const a (Some Exercise)
Bool :: Const a Bool
Int :: Const a Int
String :: Const a String
type Type a = TypeRep (Const a)
data TypedValue f
(:::) :: t -> f t -> TypedValue f
class Typed a t | t -> a where typeOf = const typed typedList = List typed
typeOf :: Typed a t => t -> Type a t
typed :: Typed a t => Type a t
typedList :: Typed a t => Type a [t]
class Equal f
equal :: Equal f => f a -> f b -> Maybe (a -> b)
class ShowF f
showF :: ShowF f => f a -> String
equalM :: Monad m => Type a t1 -> Type a t2 -> m (t1 -> t2)
instance Typed a (Some Exercise)
instance Typed a t => Typed a (Tree t)
instance Typed a t => Typed a [t]
instance (Typed a t1, Typed a t2) => Typed a (Derivation t1 t2)
instance (Typed a t1, Typed a t2) => Typed a (Either t1 t2)
instance Typed a t => Typed a (Maybe t)
instance (Typed a t1, Typed a t2) => Typed a (t1 -> t2)
instance (Typed a t1, Typed a t2, Typed a t3, Typed a t4) => Typed a (t1, t2, t3, t4)
instance (Typed a t1, Typed a t2, Typed a t3) => Typed a (t1, t2, t3)
instance (Typed a t1, Typed a t2) => Typed a (t1, t2)
instance Typed a Text
instance Typed a Script
instance Typed a StrategyConfiguration
instance Typed a (Context a)
instance Typed a (Exercise a)
instance Typed a (State a)
instance Typed a Service
instance Typed a Difficulty
instance Typed a StdGen
instance Typed a Environment
instance Typed a Location
instance Typed a Id
instance Typed a (Strategy (Context a))
instance Typed a (Rule (Context a))
instance Typed a Char
instance Typed a ()
instance Typed a Bool
instance Typed a Int
instance ShowF (Const a)
instance Show (Const a t)
instance Show (TypedValue (Const a))
instance Show (TypedValue f) => Show (TypedValue (TypeRep f))
instance ShowF f => Show (TypeRep f t)
instance ShowF f => ShowF (TypeRep f)
instance Equal (Const a)
instance Equal f => Equal (TypeRep f)
instance HasId Service
instance Show Service
module Ideas.Encoding.Evaluator
data EncoderState st a b
simpleEncoder :: (a -> b) -> EncoderState st a b
maybeEncoder :: (a -> Maybe b) -> EncoderState st a b
eitherEncoder :: (a -> Either String b) -> EncoderState st a b
encoderFor :: (a -> EncoderState st a b) -> EncoderState st a b
encoderStateFor :: (st -> a -> EncoderState st a b) -> EncoderState st a b
encodeTyped :: Typed a t => EncoderState st t b -> EncoderState st (TypedValue (Type a)) b
runEncoderState :: EncoderState st a b -> st -> a -> Either String b
runEncoderStateM :: Monad m => EncoderState st a b -> st -> a -> m b
(//) :: EncoderState st a c -> a -> EncoderState st b c
getState :: EncoderState st a st
withState :: (st -> b) -> EncoderState st a b
-- | Lift a value.
pure :: Applicative f => forall a. a -> f a
-- | An infix synonym for fmap.
(<$>) :: Functor f => (a -> b) -> f a -> f b
-- | A variant of <*> with the arguments reversed.
(<**>) :: Applicative f => f a -> f (a -> b) -> f b
-- | Lift a binary function to actions.
liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
data Evaluator a m b
Evaluator :: (TypedValue (Type a) -> m b) -> (forall t. Type a t -> m t) -> Evaluator a m b
evalService :: Monad m => Evaluator a m b -> Service -> m b
instance BuildXML b => BuildXML (EncoderState st a b)
instance MonadPlus (EncoderState st a)
instance Monad (EncoderState st a)
instance Monoid b => Monoid (EncoderState st a b)
instance Applicative (EncoderState st a)
instance Functor (EncoderState st a)
instance ArrowApply (EncoderState st)
instance ArrowChoice (EncoderState st)
instance ArrowPlus (EncoderState st)
instance ArrowZero (EncoderState st)
instance Arrow (EncoderState st)
instance Category (EncoderState st)
-- | Services using JSON notation
module Ideas.Encoding.DecoderJSON
type JSONDecoder a = EncoderState (JSONDecoderState a) JSON
data JSONDecoderState a
JSONDecoderState :: Exercise a -> Script -> StdGen -> JSONDecoderState a
getExercise :: JSONDecoderState a -> Exercise a
getScript :: JSONDecoderState a -> Script
getStdGen :: JSONDecoderState a -> StdGen
jsonDecoder :: Type a t -> JSONDecoder a t
module Ideas.Encoding.OpenMathSupport
toOpenMath :: Monad m => Exercise a -> a -> m OMOBJ
fromOpenMath :: MonadPlus m => Exercise a -> OMOBJ -> m a
noMixedFractions :: OMOBJ -> OMOBJ
toOMOBJ :: IsTerm a => a -> OMOBJ
fromOMOBJ :: (MonadPlus m, IsTerm a) => OMOBJ -> m a
-- | Services using XML notation
module Ideas.Encoding.DecoderXML
type XMLDecoder a = EncoderState (XMLDecoderState a) XML
data XMLDecoderState a
XMLDecoderState :: Exercise a -> Script -> StdGen -> Bool -> (XML -> Either String a) -> XMLDecoderState a
getExercise :: XMLDecoderState a -> Exercise a
getScript :: XMLDecoderState a -> Script
getStdGen :: XMLDecoderState a -> StdGen
isOpenMath :: XMLDecoderState a -> Bool
decodeTerm :: XMLDecoderState a -> XML -> Either String a
xmlDecoder :: Type a t -> XMLDecoder a t
module Ideas.Encoding.RulePresenter
ruleToHTML :: Some Exercise -> Rule a -> HTMLBuilder
module Ideas.Encoding.RulesInfo
rulesInfoXML :: Exercise a -> (a -> XMLBuilder) -> XMLBuilder
rewriteRuleToFMP :: Bool -> RewriteRule a -> FMP
collectExamples :: Exercise a -> ExampleMap a
type ExampleMap a = Map Id [(a, a)]
-- | Converting a strategy to XML, and the other way around.
module Ideas.Encoding.StrategyInfo
strategyToXML :: IsStrategy f => f a -> XML
xmlToStrategy :: Monad m => (String -> Maybe (Rule a)) -> XML -> m (Strategy a)
module Ideas.Service.BasicServices
stepsremaining :: State a -> Either String Int
findbuggyrules :: State a -> Context a -> [(Rule (Context a), Location, Environment)]
ready :: State a -> Bool
allfirsts :: State a -> Either String [(StepInfo a, State a)]
derivation :: Maybe StrategyConfiguration -> State a -> Either String (Derivation (Rule (Context a), Environment) (Context a))
onefirst :: State a -> Either String (StepInfo a, State a)
applicable :: Location -> State a -> [Rule (Context a)]
allapplications :: State a -> [(Rule (Context a), Location, State a)]
apply :: Rule (Context a) -> Location -> Environment -> State a -> Either String (State a)
generate :: Exercise a -> Maybe Difficulty -> IO (State a)
generateWith :: StdGen -> Exercise a -> Maybe Difficulty -> Either String (State a)
type StepInfo a = (Rule (Context a), Location, Environment)
exampleDerivations :: Exercise a -> Either String [Derivation (Rule (Context a), Environment) (Context a)]
-- | Diagnose a term submitted by a student
module Ideas.Service.Diagnose
data Diagnosis a
Buggy :: Environment -> (Rule (Context a)) -> Diagnosis a
NotEquivalent :: Diagnosis a
Similar :: Bool -> (State a) -> Diagnosis a
Expected :: Bool -> (State a) -> (Rule (Context a)) -> Diagnosis a
Detour :: Bool -> (State a) -> Environment -> (Rule (Context a)) -> Diagnosis a
Correct :: Bool -> (State a) -> Diagnosis a
diagnose :: State a -> Context a -> Diagnosis a
restartIfNeeded :: State a -> State a
newState :: Diagnosis a -> Maybe (State a)
instance Typed a (Diagnosis a)
instance Show (Diagnosis a)
module Ideas.Service.DomainReasoner
data DomainReasoner
DR :: Id -> [Some Exercise] -> [Service] -> [ViewPackage] -> [(Id, Id)] -> [(Id, FilePath)] -> TestSuite -> String -> String -> DomainReasoner
reasonerId :: DomainReasoner -> Id
exercises :: DomainReasoner -> [Some Exercise]
services :: DomainReasoner -> [Service]
views :: DomainReasoner -> [ViewPackage]
aliases :: DomainReasoner -> [(Id, Id)]
scripts :: DomainReasoner -> [(Id, FilePath)]
testSuite :: DomainReasoner -> TestSuite
version :: DomainReasoner -> String
fullVersion :: DomainReasoner -> String
exercisesSorted :: DomainReasoner -> [Some Exercise]
servicesSorted :: DomainReasoner -> [Service]
findExercise :: Monad m => DomainReasoner -> Id -> m (Some Exercise)
findService :: Monad m => DomainReasoner -> Id -> m Service
defaultScript :: DomainReasoner -> Id -> IO Script
instance Typed a DomainReasoner
instance HasId DomainReasoner
instance Monoid DomainReasoner
-- | Diagnose a term submitted by a student. Deprecated (see diagnose
-- service).
module Ideas.Service.Submit
submit :: State a -> Context a -> Result a
data Result a
Buggy :: [Rule (Context a)] -> Result a
NotEquivalent :: Result a
Ok :: [Rule (Context a)] -> (State a) -> Result a
Detour :: [Rule (Context a)] -> (State a) -> Result a
Unknown :: (State a) -> Result a
instance Typed a (Result a)
-- | Services using JSON notation
module Ideas.Encoding.EncoderJSON
jsonEncoder :: JSONEncoder a (TypedValue (Type a))
module Ideas.Service.ProblemDecomposition
problemDecomposition :: Maybe Id -> State a -> Maybe (Answer a) -> Either String (Reply a)
data Reply a
Ok :: Id -> (State a) -> Reply a
Incorrect :: Bool -> Id -> (State a) -> Environment -> Reply a
instance Typed a (Reply a)
instance Typed a (Answer a)
module Ideas.Service.Request
data Request
Request :: String -> Maybe Id -> Maybe String -> DataFormat -> Maybe Encoding -> Request
service :: Request -> String
exerciseId :: Request -> Maybe Id
source :: Request -> Maybe String
dataformat :: Request -> DataFormat
encoding :: Request -> Maybe Encoding
data DataFormat
XML :: DataFormat
JSON :: DataFormat
data Encoding
OpenMath :: Encoding
StringEncoding :: Encoding
HTMLEncoding :: Encoding
discoverDataFormat :: Monad m => String -> m DataFormat
readEncoding :: Monad m => String -> m Encoding
instance Show DataFormat
instance Show Encoding
instance Eq Encoding
-- | Services using JSON notation
module Ideas.Encoding.ModeJSON
processJSON :: Bool -> DomainReasoner -> String -> IO (Request, String, String)
-- | Facilities to create a log database
module Ideas.Main.LoggingDatabase
logMessage :: Request -> String -> String -> String -> UTCTime -> IO ()
logEnabled :: Bool
-- | Options and command-line flags for services
module Ideas.Main.Options
data Flag
Version :: Flag
Help :: Flag
InputFile :: String -> Flag
MakePages :: FilePath -> Flag
Test :: FilePath -> Flag
MakeScriptFor :: String -> Flag
AnalyzeScript :: FilePath -> Flag
getFlags :: IO [Flag]
versionText :: String
helpText :: String
shortVersion :: String
fullVersion :: String
instance Eq Flag
-- | Run a feedbackscript
module Ideas.Service.FeedbackScript.Run
data Script
data Environment a
Env :: Bool -> Maybe (Rule (Context a)) -> Maybe (Rule (Context a)) -> Maybe [LabelInfo] -> Maybe (String, String) -> Maybe Term -> Maybe Term -> Maybe String -> Environment a
oldReady :: Environment a -> Bool
expected :: Environment a -> Maybe (Rule (Context a))
recognized :: Environment a -> Maybe (Rule (Context a))
actives :: Environment a -> Maybe [LabelInfo]
diffPair :: Environment a -> Maybe (String, String)
before :: Environment a -> Maybe Term
after :: Environment a -> Maybe Term
afterText :: Environment a -> Maybe String
newEnvironment :: State a -> Environment a
feedbackDiagnosis :: Diagnosis a -> Environment a -> Script -> Text
feedbackHint :: Id -> Environment a -> Script -> Text
feedbackHints :: Id -> [((Rule (Context a), b, c), State a)] -> State a -> Script -> [Text]
ruleToString :: Environment a -> Script -> Rule b -> String
feedbackIds :: [Id]
attributeIds :: [Id]
conditionIds :: [Id]
eval :: Environment a -> Script -> Either Id Text -> Maybe Text
module Ideas.Service.FeedbackText
data Message
accept :: Message -> Maybe Bool
text :: Message -> Text
onefirsttext :: Script -> State a -> Maybe String -> (Message, Maybe (State a))
submittext :: Script -> State a -> String -> (Message, State a)
derivationtext :: Script -> State a -> Either String (Derivation String (Context a))
feedbacktext :: Script -> State a -> Context a -> (Message, State a)
instance Typed a Message
-- | Services using XML notation
module Ideas.Encoding.EncoderXML
type XMLEncoder a t = EncoderState (XMLEncoderState a) t XMLBuilder
data XMLEncoderState a
XMLEncoderState :: Exercise a -> Bool -> (a -> XMLBuilder) -> XMLEncoderState a
getExercise :: XMLEncoderState a -> Exercise a
isOpenMath :: XMLEncoderState a -> Bool
encodeTerm :: XMLEncoderState a -> a -> XMLBuilder
xmlEncoder :: XMLEncoder a (TypedValue (Type a))
encodeState :: XMLEncoder a (State a)
-- | Manages links to information
module Ideas.Encoding.LinkManager
data LinkManager
LinkManager :: (String -> String) -> String -> Bool -> String -> String -> String -> (Service -> String) -> (forall a. Exercise a -> String) -> (forall a. Exercise a -> String) -> (forall a. Exercise a -> String) -> (forall a. Exercise a -> String) -> (forall a. Exercise a -> String) -> (forall a. Exercise a -> Rule (Context a) -> String) -> (forall a. Exercise a -> Difficulty -> String) -> (forall a. State a -> String) -> (forall a. State a -> String) -> (forall a. State a -> String) -> (forall a. State a -> String) -> LinkManager
urlForResource :: LinkManager -> String -> String
urlForRequest :: LinkManager -> String
isStatic :: LinkManager -> Bool
urlForIndex :: LinkManager -> String
urlForExercises :: LinkManager -> String
urlForServices :: LinkManager -> String
urlForService :: LinkManager -> Service -> String
urlForExercise :: LinkManager -> forall a. Exercise a -> String
urlForStrategy :: LinkManager -> forall a. Exercise a -> String
urlForRules :: LinkManager -> forall a. Exercise a -> String
urlForExamples :: LinkManager -> forall a. Exercise a -> String
urlForDerivations :: LinkManager -> forall a. Exercise a -> String
urlForRule :: LinkManager -> forall a. Exercise a -> Rule (Context a) -> String
urlForRandomExample :: LinkManager -> forall a. Exercise a -> Difficulty -> String
urlForState :: LinkManager -> forall a. State a -> String
urlForFirsts :: LinkManager -> forall a. State a -> String
urlForApplications :: LinkManager -> forall a. State a -> String
urlForDerivation :: LinkManager -> forall a. State a -> String
dynamicLinks :: String -> LinkManager
stateToXML :: State a -> XMLBuilder
staticLinks :: LinkManager
linksUp :: Int -> LinkManager -> LinkManager
pathLevel :: FilePath -> Int
(>) :: String -> FilePath -> FilePath
linkToIndex :: LinkManager -> HTMLBuilder -> HTMLBuilder
linkToExercises :: LinkManager -> HTMLBuilder -> HTMLBuilder
linkToServices :: LinkManager -> HTMLBuilder -> HTMLBuilder
linkToService :: LinkManager -> Service -> HTMLBuilder -> HTMLBuilder
linkToExercise :: LinkManager -> Exercise a -> HTMLBuilder -> HTMLBuilder
linkToStrategy :: LinkManager -> Exercise a -> HTMLBuilder -> HTMLBuilder
linkToRules :: LinkManager -> Exercise a -> HTMLBuilder -> HTMLBuilder
linkToExamples :: LinkManager -> Exercise a -> HTMLBuilder -> HTMLBuilder
linkToDerivations :: LinkManager -> Exercise a -> HTMLBuilder -> HTMLBuilder
linkToRule :: LinkManager -> Exercise a -> Rule (Context a) -> HTMLBuilder -> HTMLBuilder
linkToRandomExample :: LinkManager -> Exercise a -> Difficulty -> HTMLBuilder -> HTMLBuilder
linkToState :: LinkManager -> State a -> HTMLBuilder -> HTMLBuilder
linkToFirsts :: LinkManager -> State a -> HTMLBuilder -> HTMLBuilder
linkToApplications :: LinkManager -> State a -> HTMLBuilder -> HTMLBuilder
linkToDerivation :: LinkManager -> State a -> HTMLBuilder -> HTMLBuilder
-- | Encoding in HTML
module Ideas.Encoding.EncoderHTML
htmlEncoder :: LinkManager -> DomainReasoner -> Exercise a -> TypedValue (Type a) -> HTMLPage
-- | Manages links to information
module Ideas.Main.Documentation
makeDocumentation :: DomainReasoner -> String -> IO ()
-- | Services using XML notation
module Ideas.Encoding.ModeXML
processXML :: DomainReasoner -> Maybe String -> String -> IO (Request, String, String)
module Ideas.Main.BlackBoxTests
blackBoxTests :: DomainReasoner -> String -> IO TestSuite
-- | Analysis of a feedbackscript
module Ideas.Service.FeedbackScript.Analysis
makeScriptFor :: IsId a => DomainReasoner -> a -> IO ()
parseAndAnalyzeScript :: DomainReasoner -> FilePath -> IO ()
analyzeScript :: [Some Exercise] -> Script -> [Message]
data Message
UnknownExercise :: Id -> Message
UnknownFeedback :: Id -> Message
FeedbackUndefined :: Id -> Message
NoTextForRule :: Id -> Id -> Message
UnknownAttribute :: Id -> Message
UnknownCondAttr :: Id -> Message
instance Show Message
-- | Main module for feedback services
module Ideas.Main.Default
defaultMain :: DomainReasoner -> IO ()
newDomainReasoner :: IsId a => a -> DomainReasoner
module Ideas.Service.ServiceList
serviceList :: [Service]
metaServiceList :: DomainReasoner -> [Service]