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