-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Feedback services for intelligent tutoring systems -- -- Ideas (Interactive Domain-specific Exercise Assistants) is a joint -- research project between the Open University of the Netherlands and -- Utrecht University. The project's goal is to use software and compiler -- technology to build state-of-the-art components for intelligent -- tutoring systems (ITS) and learning environments. The ideas -- software package provides a generic framework for constructing the -- expert knowledge module (also known as a domain reasoner) for an ITS -- or learning environment. Domain knowledge is offered as a set of -- feedback services that are used by external tools such as the digital -- mathematical environment (DME), MathDox, and the Math-Bridge system. -- We have developed several domain reasoners based on this framework, -- including reasoners for mathematics, linear algebra, logic, learning -- Haskell (the Ask-Elle programming tutor) and evaluating Haskell -- expressions, and for practicing communication skills (the serious game -- Communicate!). @package ideas @version 1.5 -- | 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) prettyXML :: Bool -> XML -> Doc prettyElement :: Bool -> Element -> Doc instance GHC.Show.Show Ideas.Text.XML.Document.Attribute instance GHC.Show.Show Ideas.Text.XML.Document.Reference instance GHC.Show.Show Ideas.Text.XML.Document.Parameter instance GHC.Show.Show Ideas.Text.XML.Document.XML instance GHC.Show.Show Ideas.Text.XML.Document.Element instance Text.PrettyPrint.Leijen.Pretty Ideas.Text.XML.Document.Attribute instance Text.PrettyPrint.Leijen.Pretty Ideas.Text.XML.Document.Reference instance Text.PrettyPrint.Leijen.Pretty Ideas.Text.XML.Document.Parameter instance Text.PrettyPrint.Leijen.Pretty Ideas.Text.XML.Document.XML instance Text.PrettyPrint.Leijen.Pretty Ideas.Text.XML.Document.Element -- | 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 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. -- --
-- >>> show <$> Nothing -- Nothing -- -- >>> show <$> Just 3 -- Just "3" ---- -- Convert from an Either Int Int to -- an Either Int String using -- show: -- --
-- >>> show <$> Left 17 -- Left 17 -- -- >>> show <$> Right 17 -- Right "17" ---- -- Double each element of a list: -- --
-- >>> (*2) <$> [1,2,3] -- [2,4,6] ---- -- Apply even to the second element of a pair: -- --
-- >>> even <$> (2,2) -- (2,True) --(<$>) :: 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 GHC.Show.Show Ideas.Text.Parsing.UnbalancedError -- | A parser for XML documents, directly derived from the specification: -- -- http://www.w3.org/TR/2006/REC-xml-20060816 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 compactXML :: Element -> String children :: Element -> [Element] findAttribute :: Monad m => String -> Element -> m String findChildren :: String -> Element -> [Element] findChild :: Monad m => String -> Element -> m Element getData :: Element -> String instance GHC.Show.Show Ideas.Text.XML.Interface.Element module Ideas.Main.Revision ideasVersion :: String ideasRevision :: String 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 parseXMLFile :: FilePath -> IO XML compactXML :: Element -> 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 findChildren :: String -> Element -> [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 GHC.Base.Monoid Ideas.Text.XML.XMLBuilder instance Ideas.Text.XML.BuildXML Ideas.Text.XML.XMLBuilder -- | A minimal interface for constructing simple HTML pages See -- http://www.w3.org/TR/html4/ 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 Ideas.Text.XML.InXML Ideas.Text.HTML.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 GHC.Classes.Eq Ideas.Text.OpenMath.Object.OMOBJ instance GHC.Show.Show Ideas.Text.OpenMath.Object.OMOBJ instance Ideas.Text.XML.InXML Ideas.Text.OpenMath.Object.OMOBJ instance Data.Generics.Uniplate.Operations.Uniplate Ideas.Text.OpenMath.Object.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 compactJSON :: JSON -> String jsonRPC :: JSON -> RPCHandler -> IO RPCResponse type RPCHandler = String -> JSON -> IO JSON data RPCResponse Response :: JSON -> JSON -> JSON -> RPCResponse [responseResult] :: RPCResponse -> JSON [responseError] :: RPCResponse -> JSON [responseId] :: RPCResponse -> JSON propEncoding :: Property instance GHC.Classes.Eq Ideas.Text.JSON.JSON instance GHC.Classes.Eq Ideas.Text.JSON.Number instance GHC.Show.Show Ideas.Text.JSON.Number instance GHC.Show.Show Ideas.Text.JSON.JSON instance Ideas.Text.JSON.InJSON GHC.Types.Int instance Ideas.Text.JSON.InJSON GHC.Integer.Type.Integer instance Ideas.Text.JSON.InJSON GHC.Types.Double instance Ideas.Text.JSON.InJSON GHC.Types.Char instance Ideas.Text.JSON.InJSON GHC.Types.Bool instance Ideas.Text.JSON.InJSON a => Ideas.Text.JSON.InJSON [a] instance (Ideas.Text.JSON.InJSON a, Ideas.Text.JSON.InJSON b) => Ideas.Text.JSON.InJSON (a, b) instance (Ideas.Text.JSON.InJSON a, Ideas.Text.JSON.InJSON b, Ideas.Text.JSON.InJSON c) => Ideas.Text.JSON.InJSON (a, b, c) instance (Ideas.Text.JSON.InJSON a, Ideas.Text.JSON.InJSON b, Ideas.Text.JSON.InJSON c, Ideas.Text.JSON.InJSON d) => Ideas.Text.JSON.InJSON (a, b, c, d) instance Ideas.Text.JSON.InJSON GHC.IO.Exception.IOException instance GHC.Show.Show Ideas.Text.JSON.RPCRequest instance GHC.Show.Show Ideas.Text.JSON.RPCResponse instance Ideas.Text.JSON.InJSON Ideas.Text.JSON.RPCRequest instance Ideas.Text.JSON.InJSON Ideas.Text.JSON.RPCResponse instance Test.QuickCheck.Arbitrary.Arbitrary Ideas.Text.JSON.JSON instance Test.QuickCheck.Arbitrary.Arbitrary Ideas.Text.JSON.Number -- | A type class for expressing choice, preference, and left-biased -- choice. The Menu datatype implements the type class by keeping -- all the alternatives. module Ideas.Common.Strategy.Choice -- | Laws: .|., ./. |> are all associative, and -- have empty as their unit element. class Choice a where choice xs = if null xs then empty else foldr1 (.|.) xs preference xs = if null xs then empty else foldr1 (./.) xs orelse xs = if null xs then empty else foldr1 (|>) xs -- | Nothing to choose from. empty :: Choice a => a -- | Normal (unbiased) choice. (.|.) :: Choice a => a -> a -> a -- | Left-preference. (./.) :: Choice a => a -> a -> a -- | Left-biased choice. (|>) :: Choice a => a -> a -> a -- | One of the alternatives in a list (unbiased). choice :: Choice a => [a] -> a preference :: Choice a => [a] -> a orelse :: Choice a => [a] -> a -- | A menu offers choices and preferences. It stores singleton bindings -- (thus acting as a finite map) and one special element -- (doneMenu). It is an instance of the Functor and -- Monad type classes. data Menu k a -- | Singleton binding (|->) :: a -> s -> Menu a s -- | Special element for denoting success doneMenu :: Menu k a -- | Equality with a comparison function for the elements eqMenuBy :: (k -> k -> Bool) -> (a -> a -> Bool) -> Menu k a -> Menu k a -> Bool -- | Returns all elements that are in the menu. elems :: Menu k a -> [(k, a)] -- | Returns only the best elements that are in the menu with respect to -- left-biased choices. bests :: Menu k a -> [(k, a)] -- | Returns only the best elements that are in the menu, with a given -- ordering. bestsOrdered :: (k -> k -> Ordering) -> Menu k a -> [(k, a)] -- | Is the menu empty? isEmpty :: Menu k a -> Bool hasDone :: Menu k a -> Bool -- | Get an element from the menu by its index. getByIndex :: Int -> Menu k a -> Maybe (k, a) -- | Only keep the best elements in the menu. cut :: Menu k a -> Menu k a -- | Generalized monadic bind, with the arguments flipped. onMenu :: Choice b => (k -> a -> b) -> b -> Menu k a -> b -- | Maps a function over a menu that also takes the index of an element. onMenuWithIndex :: Choice b => (Int -> k -> a -> b) -> b -> Menu k a -> b instance Ideas.Common.Strategy.Choice.Choice [a] instance Ideas.Common.Strategy.Choice.Choice b => Ideas.Common.Strategy.Choice.Choice (a -> b) instance (GHC.Classes.Eq k, GHC.Classes.Eq a) => GHC.Classes.Eq (Ideas.Common.Strategy.Choice.Menu k a) instance Ideas.Common.Strategy.Choice.Choice (Ideas.Common.Strategy.Choice.Menu k a) instance GHC.Base.Functor (Ideas.Common.Strategy.Choice.Menu k) -- | 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 GHC.Base.Monoid (Ideas.Common.Utils.QuickCheck.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 Data.Data.Data Ideas.Common.Utils.StringRef.StringRef instance GHC.Classes.Ord Ideas.Common.Utils.StringRef.StringRef instance GHC.Classes.Eq Ideas.Common.Utils.StringRef.StringRef -- | A lightweight wrapper for organizing tests (including QuickCheck -- tests). 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 TestSuite is a monoid. module Ideas.Common.Utils.TestSuite data TestSuite -- | Construct a (named) test suite containing test cases and other suites suite :: String -> [TestSuite] -> TestSuite -- | Turn a QuickCheck property into the test suite. The first argument is -- a label for the property useProperty :: Testable prop => String -> prop -> TestSuite -- | Turn a QuickCheck property into the test suite, also providing a test -- configuration (Args) usePropertyWith :: Testable prop => String -> Args -> prop -> 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 assertMessage :: String -> Bool -> String -> TestSuite assertMessageIO :: String -> IO Message -> TestSuite -- | All errors are turned into warnings onlyWarnings :: TestSuite -> TestSuite rateOnError :: Int -> TestSuite -> TestSuite runTestSuite :: Bool -> TestSuite -> IO () runTestSuiteResult :: Bool -> TestSuite -> IO Result data Result subResults :: Result -> [(String, Result)] findSubResult :: String -> Result -> Maybe Result justOneSuite :: Result -> Maybe (String, Result) allMessages :: Result -> [(String, Message)] topMessages :: Result -> [(String, Message)] nrOfTests :: Result -> Int nrOfErrors :: Result -> Int nrOfWarnings :: Result -> Int timeInterval :: Result -> Double makeSummary :: Result -> String printSummary :: Result -> IO () data Message message :: String -> Message warning :: String -> Message messageLines :: Message -> [String] data Status class HasStatus a getStatus :: HasStatus a => a -> Status isError :: HasStatus a => a -> Bool isWarning :: HasStatus a => a -> Bool isOk :: HasStatus a => a -> Bool data Rating class HasRating a rating :: HasRating a => a -> Maybe Int rate :: HasRating a => Int -> a -> a instance GHC.Classes.Eq Ideas.Common.Utils.TestSuite.Message instance GHC.Classes.Ord Ideas.Common.Utils.TestSuite.Rating instance GHC.Classes.Eq Ideas.Common.Utils.TestSuite.Rating instance GHC.Classes.Ord Ideas.Common.Utils.TestSuite.Status instance GHC.Classes.Eq Ideas.Common.Utils.TestSuite.Status instance GHC.Base.Monoid Ideas.Common.Utils.TestSuite.TestSuite instance GHC.Show.Show Ideas.Common.Utils.TestSuite.Result instance GHC.Base.Monoid Ideas.Common.Utils.TestSuite.Result instance Ideas.Common.Utils.TestSuite.HasStatus Ideas.Common.Utils.TestSuite.Result instance Ideas.Common.Utils.TestSuite.HasRating Ideas.Common.Utils.TestSuite.Result instance GHC.Show.Show Ideas.Common.Utils.TestSuite.Message instance GHC.Base.Monoid Ideas.Common.Utils.TestSuite.Message instance Ideas.Common.Utils.TestSuite.HasStatus Ideas.Common.Utils.TestSuite.Message instance Ideas.Common.Utils.TestSuite.HasRating Ideas.Common.Utils.TestSuite.Message instance GHC.Base.Monoid Ideas.Common.Utils.TestSuite.Status instance GHC.Base.Monoid Ideas.Common.Utils.TestSuite.Rating instance Ideas.Common.Utils.TestSuite.HasRating Ideas.Common.Utils.TestSuite.Rating -- | 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 -- | 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) -- | 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, 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]] 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 GHC.Classes.Ord Ideas.Common.Utils.ShowString instance GHC.Classes.Eq Ideas.Common.Utils.ShowString instance GHC.Show.Show Ideas.Common.Utils.ShowString instance GHC.Read.Read Ideas.Common.Utils.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 GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Utils.Mirror a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Utils.Mirror a) instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Utils.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 GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Iterator.ListIterator a) instance Ideas.Common.Traversal.Iterator.Iterator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Utils.Mirror a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Iterator.ListIterator a) instance Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Iterator.ListIterator a) instance Ideas.Common.Traversal.Utils.Focus (Ideas.Common.Traversal.Iterator.ListIterator a) instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Iterator.ListIterator instance Test.QuickCheck.Arbitrary.Arbitrary a => Test.QuickCheck.Arbitrary.Arbitrary (Ideas.Common.Traversal.Iterator.ListIterator a) 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 GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.Leafs a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Navigator.Leafs a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.Horizontal a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Navigator.Horizontal a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.LevelOrder a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Navigator.LevelOrder a) instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.PostOrder a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.PostOrder a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Navigator.PostOrder a) instance GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.PreOrder a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Navigator.PreOrder a) instance GHC.Classes.Ord Ideas.Common.Traversal.Navigator.Location instance GHC.Classes.Eq Ideas.Common.Traversal.Navigator.Location instance GHC.Show.Show Ideas.Common.Traversal.Navigator.Location instance GHC.Base.Monoid Ideas.Common.Traversal.Navigator.Location instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Navigator.Navigator (Ideas.Common.Traversal.Utils.Mirror a) instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Navigator.PreOrder instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.PreOrder instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.PreOrder a) instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Navigator.PostOrder instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.PostOrder instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Navigator.LevelOrder instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.LevelOrder instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.LevelOrder a) instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Navigator.Horizontal instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.Horizontal instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.Horizontal a) instance Ideas.Common.Traversal.Utils.Wrapper Ideas.Common.Traversal.Navigator.Leafs instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.Leafs instance Ideas.Common.Traversal.Navigator.Navigator a => Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.Leafs a) instance Ideas.Common.Traversal.Navigator.Navigator (Ideas.Common.Traversal.Navigator.StrNavigator a) instance Ideas.Common.Traversal.Utils.Focus (Ideas.Common.Traversal.Navigator.StrNavigator a) instance Ideas.Common.Traversal.Iterator.Iterator (Ideas.Common.Traversal.Navigator.StrIterator a) instance Ideas.Common.Traversal.Utils.Focus (Ideas.Common.Traversal.Navigator.StrIterator a) instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.StrIterator instance (GHC.Show.Show a, Data.Generics.Uniplate.Operations.Uniplate a) => GHC.Show.Show (Ideas.Common.Traversal.Navigator.UniplateNavigator a) instance (GHC.Classes.Eq a, Data.Generics.Uniplate.Operations.Uniplate a) => GHC.Classes.Eq (Ideas.Common.Traversal.Navigator.UniplateNavigator a) instance Data.Generics.Uniplate.Operations.Uniplate a => Ideas.Common.Traversal.Navigator.Navigator (Ideas.Common.Traversal.Navigator.UniplateNavigator a) instance Ideas.Common.Traversal.Utils.Update Ideas.Common.Traversal.Navigator.UniplateNavigator instance Data.Generics.Uniplate.Operations.Uniplate a => Ideas.Common.Traversal.Utils.Focus (Ideas.Common.Traversal.Navigator.UniplateNavigator a) instance (Test.QuickCheck.Arbitrary.Arbitrary a, Data.Generics.Uniplate.Operations.Uniplate a) => Test.QuickCheck.Arbitrary.Arbitrary (Ideas.Common.Traversal.Navigator.UniplateNavigator 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 GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Traversal.Tests.T a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Traversal.Tests.T a) instance Data.Generics.Uniplate.Operations.Uniplate (Ideas.Common.Traversal.Tests.T a) instance Test.QuickCheck.Arbitrary.Arbitrary a => Test.QuickCheck.Arbitrary.Arbitrary (Ideas.Common.Traversal.Tests.T 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 Fix a where fix f = let a = f a in a fix :: Fix a => (a -> a) -> a 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 Ideas.Common.Classes.Container [] instance Ideas.Common.Classes.Container Data.Set.Base.Set instance Ideas.Common.Classes.BiFunctor Data.Either.Either instance Ideas.Common.Classes.BiFunctor (,) -- | Many entities of the Ideas framework carry an Id for -- identification. Identifiers have a hierarchical structure of an -- arbitrary depth (e.g. algebra.equation or a.b.c). -- Valid symbols for identifiers are the alpha-numerical characters, -- together with - and _. Each identifier carries a -- description and a hash value for fast comparison. -- -- Functionality for identifiers is provided by means of three type -- classes: -- --
arr id = id
arr (f >>> g) = arr f >>> -- arr g
first (arr f) = arr (first -- f)
first (f >>> g) = first f >>> -- first g
first f >>> arr fst = -- arr fst >>> f
first f >>> arr (id *** g) = -- arr (id *** g) >>> first f
first (first f) >>> arr -- assoc = arr assoc >>> first -- f
-- 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 :: * -> * -> *) -- | Lift a function to an arrow. arr :: Arrow a => (b -> c) -> a b c -- | Send the first component of the input through the argument arrow, and -- copy the rest unchanged to the output. first :: Arrow a => a b c -> a (b, d) (c, d) -- | A mirror image of first. -- -- The default definition may be overridden with a more efficient version -- if desired. second :: Arrow a => a b c -> a (d, b) (d, c) -- | Split the input between the two argument arrows and combine their -- output. Note that this is in general not a functor. -- -- The default definition may be overridden with a more efficient version -- if desired. (***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c') -- | Fanout: send the input to both argument arrows and combine their -- output. -- -- The default definition may be overridden with a more efficient version -- if desired. (&&&) :: 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. -- -- Instances should satisfy the following laws: -- --
left (arr f) = arr (left -- f)
left (f >>> g) = left f >>> -- left g
f >>> arr Left = arr -- Left >>> left f
left f >>> arr (id +++ g) = -- arr (id +++ g) >>> left f
left (left f) >>> arr -- assocsum = arr assocsum >>> -- left f
-- 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 :: * -> * -> *) -- | Feed marked inputs through the argument arrow, passing the rest -- through unchanged to the output. left :: ArrowChoice a => a b c -> a (Either b d) (Either c d) -- | A mirror image of left. -- -- The default definition may be overridden with a more efficient version -- if desired. right :: ArrowChoice a => a b c -> a (Either d b) (Either d c) -- | Split the input between the two argument arrows, retagging and merging -- their outputs. Note that this is in general not a functor. -- -- The default definition may be overridden with a more efficient version -- if desired. (+++) :: ArrowChoice a => a b c -> a b' c' -> a (Either b b') (Either c c') -- | Fanin: Split the input between the two argument arrows and merge their -- outputs. -- -- The default definition may be overridden with a more efficient version -- if desired. (|||) :: 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 :: * -> * -> *) -- | An associative operation with identity zeroArrow. (<+>) :: ArrowPlus a => a b c -> a b c -> a b c -- | Left-to-right composition (>>>) :: Category k cat => cat a b -> cat b c -> cat a c -- | Right-to-left composition (<<<) :: Category k 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 Control.Arrow.ArrowChoice Ideas.Common.View.Matcher instance Control.Arrow.ArrowPlus Ideas.Common.View.Matcher instance Control.Arrow.ArrowZero Ideas.Common.View.Matcher instance Control.Arrow.Arrow Ideas.Common.View.Matcher instance Control.Category.Category Ideas.Common.View.Matcher instance Ideas.Common.View.IsMatcher Ideas.Common.View.Matcher instance Control.Category.Category Ideas.Common.View.View instance Control.Arrow.Arrow Ideas.Common.View.View instance Ideas.Common.Classes.BiArrow Ideas.Common.View.View instance Control.Arrow.ArrowChoice Ideas.Common.View.View instance Ideas.Common.View.IsMatcher Ideas.Common.View.View instance Ideas.Common.View.IsView Ideas.Common.View.View instance Ideas.Common.Id.HasId (Ideas.Common.View.View a b) instance Ideas.Common.Id.Identify (Ideas.Common.View.View a b) instance Control.Category.Category Ideas.Common.View.Isomorphism instance Control.Arrow.Arrow Ideas.Common.View.Isomorphism instance Ideas.Common.Classes.BiArrow Ideas.Common.View.Isomorphism instance Control.Arrow.ArrowChoice Ideas.Common.View.Isomorphism instance Ideas.Common.View.IsMatcher Ideas.Common.View.Isomorphism instance Ideas.Common.View.IsView Ideas.Common.View.Isomorphism instance Ideas.Common.Id.HasId (Ideas.Common.View.Isomorphism a b) instance Ideas.Common.Id.Identify (Ideas.Common.View.Isomorphism a b) instance Ideas.Common.Id.HasId Ideas.Common.View.ViewPackage -- | 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 ternary :: WithFunctions a => Symbol -> a -> 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 GHC.Classes.Ord Ideas.Common.Rewriting.Term.Term instance GHC.Classes.Eq Ideas.Common.Rewriting.Term.Term instance GHC.Read.Read Ideas.Common.Rewriting.Term.Term instance GHC.Show.Show Ideas.Common.Rewriting.Term.Term instance GHC.Classes.Eq Ideas.Common.Rewriting.Term.Symbol instance GHC.Classes.Ord Ideas.Common.Rewriting.Term.Symbol instance GHC.Show.Show Ideas.Common.Rewriting.Term.Symbol instance GHC.Read.Read Ideas.Common.Rewriting.Term.Symbol instance Ideas.Common.Id.HasId Ideas.Common.Rewriting.Term.Symbol instance Data.Generics.Uniplate.Operations.Uniplate Ideas.Common.Rewriting.Term.Term instance Ideas.Common.Rewriting.Term.IsTerm Ideas.Common.Rewriting.Term.Term instance Ideas.Common.Rewriting.Term.IsTerm Ideas.Common.Utils.ShowString instance (Ideas.Common.Rewriting.Term.IsTerm a, Ideas.Common.Rewriting.Term.IsTerm b) => Ideas.Common.Rewriting.Term.IsTerm (a, b) instance (Ideas.Common.Rewriting.Term.IsTerm a, Ideas.Common.Rewriting.Term.IsTerm b) => Ideas.Common.Rewriting.Term.IsTerm (Data.Either.Either a b) instance Ideas.Common.Rewriting.Term.IsTerm GHC.Types.Int instance Ideas.Common.Rewriting.Term.IsTerm GHC.Integer.Type.Integer instance Ideas.Common.Rewriting.Term.IsTerm GHC.Types.Double instance Ideas.Common.Rewriting.Term.IsTerm GHC.Types.Char instance Ideas.Common.Rewriting.Term.IsTerm a => Ideas.Common.Rewriting.Term.IsTerm [a] instance Ideas.Common.Rewriting.Term.WithFunctions Ideas.Common.Rewriting.Term.Term instance Ideas.Common.Rewriting.Term.WithVars Ideas.Common.Rewriting.Term.Term instance Ideas.Common.Rewriting.Term.WithMetaVars Ideas.Common.Rewriting.Term.Term instance Test.QuickCheck.Arbitrary.Arbitrary Ideas.Common.Rewriting.Term.Term -- | 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 GHC.Classes.Eq Ideas.Common.Environment.Environment instance GHC.Show.Show (Ideas.Common.Environment.Ref a) instance GHC.Classes.Eq (Ideas.Common.Environment.Ref a) instance Ideas.Common.Id.HasId (Ideas.Common.Environment.Ref a) instance Ideas.Common.Environment.Reference GHC.Types.Int instance Ideas.Common.Environment.Reference Ideas.Common.Rewriting.Term.Term instance Ideas.Common.Environment.Reference GHC.Types.Char instance Ideas.Common.Environment.Reference Ideas.Common.Utils.ShowString instance Ideas.Common.Environment.Reference a => Ideas.Common.Environment.Reference [a] instance (Ideas.Common.Environment.Reference a, Ideas.Common.Environment.Reference b) => Ideas.Common.Environment.Reference (a, b) instance GHC.Show.Show Ideas.Common.Environment.Binding instance GHC.Classes.Eq Ideas.Common.Environment.Binding instance Ideas.Common.Id.HasId Ideas.Common.Environment.Binding instance GHC.Show.Show Ideas.Common.Environment.Environment instance GHC.Base.Monoid Ideas.Common.Environment.Environment instance Ideas.Common.Environment.HasRefs Ideas.Common.Environment.Environment instance Ideas.Common.Environment.HasEnvironment Ideas.Common.Environment.Environment -- | 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 GHC.Base.Functor Ideas.Common.Rule.EnvironmentMonad.EnvMonad instance GHC.Base.Applicative Ideas.Common.Rule.EnvironmentMonad.EnvMonad instance GHC.Base.Alternative Ideas.Common.Rule.EnvironmentMonad.EnvMonad instance GHC.Base.Monad Ideas.Common.Rule.EnvironmentMonad.EnvMonad instance GHC.Base.MonadPlus Ideas.Common.Rule.EnvironmentMonad.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 GHC.Classes.Eq Ideas.Common.Rewriting.Substitution.Substitution instance GHC.Base.Monoid Ideas.Common.Rewriting.Substitution.Substitution instance GHC.Show.Show Ideas.Common.Rewriting.Substitution.Substitution instance Test.QuickCheck.Arbitrary.Arbitrary Ideas.Common.Rewriting.Substitution.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) module Ideas.Common.CyclicTree data CyclicTree a b node :: a -> [CyclicTree a b] -> CyclicTree a b node0 :: a -> CyclicTree a b node1 :: a -> CyclicTree a b -> CyclicTree a b node2 :: a -> CyclicTree a b -> CyclicTree a b -> CyclicTree a b leaf :: b -> CyclicTree a b label :: IsId n => n -> CyclicTree a b -> CyclicTree a b isNode :: CyclicTree a b -> Maybe (a, [CyclicTree a b]) isLeaf :: CyclicTree a b -> Maybe b isLabel :: CyclicTree a b -> Maybe (Id, CyclicTree a b) replaceNode :: (a -> [CyclicTree a b] -> CyclicTree a b) -> CyclicTree a b -> CyclicTree a b replaceLeaf :: (b -> CyclicTree a c) -> CyclicTree a b -> CyclicTree a c replaceLabel :: (Id -> CyclicTree a b -> CyclicTree a b) -> CyclicTree a b -> CyclicTree a b shrinkTree :: CyclicTree a b -> [CyclicTree a b] fold :: CyclicTreeAlg a b t -> CyclicTree a b -> t foldUnwind :: CyclicTreeAlg a b t -> CyclicTree a b -> t data CyclicTreeAlg a b t fNode :: CyclicTreeAlg a b t -> a -> [t] -> t fLeaf :: CyclicTreeAlg a b t -> b -> t fLabel :: CyclicTreeAlg a b t -> Id -> t -> t fRec :: CyclicTreeAlg a b t -> Int -> t -> t fVar :: CyclicTreeAlg a b t -> Int -> t emptyAlg :: CyclicTreeAlg a b t monoidAlg :: Monoid m => CyclicTreeAlg a b m instance (GHC.Show.Show a, GHC.Show.Show b) => GHC.Show.Show (Ideas.Common.CyclicTree.CyclicTree a b) instance Ideas.Common.Classes.BiFunctor Ideas.Common.CyclicTree.CyclicTree instance GHC.Base.Functor (Ideas.Common.CyclicTree.CyclicTree d) instance GHC.Base.Applicative (Ideas.Common.CyclicTree.CyclicTree d) instance GHC.Base.Monad (Ideas.Common.CyclicTree.CyclicTree d) instance Data.Foldable.Foldable (Ideas.Common.CyclicTree.CyclicTree d) instance Data.Traversable.Traversable (Ideas.Common.CyclicTree.CyclicTree d) instance Ideas.Common.Classes.Fix (Ideas.Common.CyclicTree.CyclicTree a b) instance (Test.QuickCheck.Arbitrary.Arbitrary a, Test.QuickCheck.Arbitrary.Arbitrary b) => Test.QuickCheck.Arbitrary.Arbitrary (Ideas.Common.CyclicTree.CyclicTree a b) -- | 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 (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Ideas.Common.Derivation.Derivation s a) instance GHC.Base.Functor (Ideas.Common.Derivation.Derivation s) instance Ideas.Common.Classes.BiFunctor Ideas.Common.Derivation.Derivation -- | 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 (GHC.Show.Show s, GHC.Show.Show a) => GHC.Show.Show (Ideas.Common.DerivationTree.DerivationTree s a) instance GHC.Base.Functor (Ideas.Common.DerivationTree.DerivationTree s) instance Ideas.Common.Classes.BiFunctor Ideas.Common.DerivationTree.DerivationTree -- | A type class for sequences together with the Firsts type class -- for accessing the firsts set and ready predicate. module Ideas.Common.Strategy.Sequence class Sequence a where type family Sym a single s = s ~> done sequence xs = if null xs then done else foldr1 (.*.) xs -- | The empty sequence. done :: Sequence a => a -- | Prepend a symbol to a sequence. (~>) :: Sequence a => Sym a -> a -> a -- | Append two sequences. (.*.) :: Sequence a => a -> a -> a -- | Singleton sequence. single :: Sequence a => Sym a -> a -- | Sequential composition. sequence :: Sequence a => [a] -> a class Firsts s where type family Elem s -- | The ready predicate (we are done). ready :: Firsts s => s -> Bool -- | The firsts set. firsts :: Firsts s => s -> [(Elem s, s)] firstsTree :: Firsts s => s -> DerivationTree (Elem s) s instance Ideas.Common.Strategy.Sequence.Sequence b => Ideas.Common.Strategy.Sequence.Sequence (a -> b) 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 termRewriteRule :: (IsId n, IsTerm a, Show a) => n -> RuleSpec Term -> 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 GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Rewriting.RewriteRule.RuleSpec a) instance GHC.Base.Functor Ideas.Common.Rewriting.RewriteRule.RuleSpec instance GHC.Show.Show (Ideas.Common.Rewriting.RewriteRule.RewriteRule a) instance Ideas.Common.Id.HasId (Ideas.Common.Rewriting.RewriteRule.RewriteRule a) instance Ideas.Common.Rewriting.RewriteRule.Different a => Ideas.Common.Rewriting.RewriteRule.Different [a] instance Ideas.Common.Rewriting.RewriteRule.Different GHC.Types.Char instance Ideas.Common.Rewriting.RewriteRule.Different Ideas.Common.Rewriting.Term.Term instance (Ideas.Common.Rewriting.Term.IsTerm a, GHC.Show.Show a) => Ideas.Common.Rewriting.RewriteRule.RuleBuilder (Ideas.Common.Rewriting.RewriteRule.RuleSpec a) a instance (Ideas.Common.Rewriting.RewriteRule.Different a, Ideas.Common.Rewriting.RewriteRule.RuleBuilder t b) => Ideas.Common.Rewriting.RewriteRule.RuleBuilder (a -> t) b instance Ideas.Common.Classes.Apply Ideas.Common.Rewriting.RewriteRule.RewriteRule 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 lawAbs :: (Different b, Arbitrary b, Show b) => (b -> LawSpec a) -> LawSpec 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 GHC.Show.Show (Ideas.Common.Algebra.Law.Law a) instance Ideas.Common.Algebra.Law.LawBuilder (Ideas.Common.Algebra.Law.LawSpec a) a instance Ideas.Common.Algebra.Law.LawBuilder (Ideas.Common.Algebra.Law.Law a) a instance Ideas.Common.Algebra.Law.LawBuilder b a => Ideas.Common.Algebra.Law.LawBuilder (a -> b) a instance (GHC.Show.Show a, GHC.Classes.Eq a, Test.QuickCheck.Arbitrary.Arbitrary a) => Test.QuickCheck.Property.Testable (Ideas.Common.Algebra.Law.Law a) instance (Test.QuickCheck.Arbitrary.Arbitrary a, Ideas.Common.Rewriting.Term.IsTerm a, GHC.Show.Show a, Ideas.Common.Rewriting.RewriteRule.Different a) => Ideas.Common.Rewriting.RewriteRule.RuleBuilder (Ideas.Common.Algebra.Law.LawSpec a) a -- | The Context datatype places a value in a context consisting of -- an environment with bindings and a point of focus. The datatype is an -- instance of the HasEnvironment type class (for accessing the -- environment) and the Navigator type class (for traversing the -- term). module Ideas.Common.Context -- | Abstract data type for a context: a context stores an envrionent. data Context a -- | Construct a context newContext :: 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 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 GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Context.Context a) instance GHC.Show.Show a => GHC.Show.Show (Ideas.Common.Context.Context a) instance Ideas.Common.Traversal.Navigator.Navigator (Ideas.Common.Context.Context a) instance Ideas.Common.Environment.HasEnvironment (Ideas.Common.Context.Context 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 -- | 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 Control.Category.Category Ideas.Common.Rule.Transformation.Trans instance Control.Arrow.Arrow Ideas.Common.Rule.Transformation.Trans instance Control.Arrow.ArrowZero Ideas.Common.Rule.Transformation.Trans instance Control.Arrow.ArrowPlus Ideas.Common.Rule.Transformation.Trans instance Control.Arrow.ArrowChoice Ideas.Common.Rule.Transformation.Trans instance Control.Arrow.ArrowApply Ideas.Common.Rule.Transformation.Trans instance GHC.Base.Monoid (Ideas.Common.Rule.Transformation.Trans a b) instance Ideas.Common.Rule.Transformation.MakeTrans GHC.Base.Maybe instance Ideas.Common.Rule.Transformation.MakeTrans [] instance Ideas.Common.Rule.Transformation.MakeTrans Ideas.Common.Rule.EnvironmentMonad.EnvMonad instance Ideas.Common.Environment.HasRefs (Ideas.Common.Rule.Transformation.Trans a b) -- | 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 Ideas.Common.View.LiftView Ideas.Common.Rule.Recognizer.Recognizer instance GHC.Base.Monoid (Ideas.Common.Rule.Recognizer.Recognizer a) instance Ideas.Common.Rule.Recognizer.Recognizable Ideas.Common.Rule.Recognizer.Recognizer instance Ideas.Common.Environment.HasRefs (Ideas.Common.Rule.Recognizer.Recognizer a) -- | 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 GHC.Show.Show (Ideas.Common.Rule.Abstract.Rule a) instance GHC.Classes.Eq (Ideas.Common.Rule.Abstract.Rule a) instance GHC.Classes.Ord (Ideas.Common.Rule.Abstract.Rule a) instance Ideas.Common.Classes.Apply Ideas.Common.Rule.Abstract.Rule instance Ideas.Common.Id.HasId (Ideas.Common.Rule.Abstract.Rule a) instance Ideas.Common.View.LiftView Ideas.Common.Rule.Abstract.Rule instance Ideas.Common.Rule.Recognizer.Recognizable Ideas.Common.Rule.Abstract.Rule instance Ideas.Common.Classes.Buggy (Ideas.Common.Rule.Abstract.Rule a) instance Ideas.Common.Classes.Minor (Ideas.Common.Rule.Abstract.Rule a) instance Ideas.Common.Environment.HasRefs (Ideas.Common.Rule.Abstract.Rule a) module Ideas.Common.Rule -- | This module defines special symbols for labeling and atomicity. module Ideas.Common.Strategy.Symbol class Eq a => AtomicSymbol a atomicOpen :: AtomicSymbol a => a atomicClose :: AtomicSymbol a => a class Eq a => LabelSymbol a isEnterSymbol :: LabelSymbol a => a -> Bool enterRule :: Id -> Rule a exitRule :: Id -> Rule a isEnterRule :: Rule a -> Maybe Id isExitRule :: Rule a -> Maybe Id instance Ideas.Common.Strategy.Symbol.AtomicSymbol (Ideas.Common.Rule.Abstract.Rule a) instance Ideas.Common.Strategy.Symbol.LabelSymbol (Ideas.Common.Rule.Abstract.Rule a) -- | Processes support choices and sequences and are modelled after Hoare's -- CSP calculus. module Ideas.Common.Strategy.Process -- | Process data type with efficient support for sequences data Process a -- | Generalized equality of processes, which takes an equality function -- for the symbols. eqProcessBy :: (a -> a -> Bool) -> Process a -> Process a -> Bool menu :: Process a -> Menu a (Process a) withMenu :: Choice b => (a -> Process a -> b) -> b -> Process a -> b fold :: Choice b => (a -> b -> b) -> b -> Process a -> b runProcess :: Apply f => Process (f a) -> a -> [a] instance GHC.Classes.Eq a => GHC.Classes.Eq (Ideas.Common.Strategy.Process.Process a) instance GHC.Base.Functor Ideas.Common.Strategy.Process.Process instance Ideas.Common.Strategy.Choice.Choice (Ideas.Common.Strategy.Process.Process a) instance Ideas.Common.Strategy.Sequence.Sequence (Ideas.Common.Strategy.Process.Process a) instance Ideas.Common.Classes.Fix (Ideas.Common.Strategy.Process.Process a) instance Ideas.Common.Strategy.Sequence.Firsts (Ideas.Common.Strategy.Process.Process a) -- | Basic machinery for fully executing a strategy expression, or only -- partially. Partial execution results in a prefix that keeps the -- current locations in the strategy (a list of Paths) for -- continuing the execution later on. A path can be used to reconstruct -- the sequence of steps already performed (a so-called trace). Prefixes -- can be merged with the Monoid operation. module Ideas.Common.Strategy.Prefix data Prefix a -- | The error prefix (i.e., without a location in the strategy). noPrefix :: Prefix a -- | Make a prefix from a core strategy and a start term. makePrefix :: Process (Rule a) -> a -> Prefix a firstsOrdered :: (Rule a -> Rule a -> Ordering) -> Prefix a -> [((Rule a, a, Environment), Prefix a)] -- | Construct a prefix by replaying a path in a core strategy: the third -- argument is the current term. replayProcess :: Path -> Process (Rule a) -> ([Rule a], a -> Prefix a) isEmptyPrefix :: Prefix a -> Bool -- | Transforms the prefix such that only major steps are kept in the -- remaining strategy. majorPrefix :: Prefix a -> Prefix a -- | The searchModePrefix transformation changes the process in such a way -- that all intermediate states can only be reached by one path. A -- prerequisite is that symbols are unique (or only used once). searchModePrefix :: Prefix a -> Prefix a -- | Returns the current Path. prefixPaths :: Prefix a -> [Path] -- | A path encodes a location in a strategy. Paths are represented as a -- list of integers. data Path -- | The empty path. emptyPath :: Path readPath :: Monad m => String -> m Path readPaths :: Monad m => String -> m [Path] instance GHC.Classes.Eq Ideas.Common.Strategy.Prefix.Path instance GHC.Show.Show (Ideas.Common.Strategy.Prefix.Prefix a) instance GHC.Base.Monoid (Ideas.Common.Strategy.Prefix.Prefix a) instance Ideas.Common.Strategy.Sequence.Firsts (Ideas.Common.Strategy.Prefix.Prefix a) instance GHC.Show.Show Ideas.Common.Strategy.Prefix.Path -- | Representation of a strategy as a cyclic tree with explicit -- fixed-points. The nodes in the tree are named strategy combinators. -- The leafs are rules. module Ideas.Common.Strategy.StrategyTree type StrategyTree a = CyclicTree (Decl Nary) (Rule a) data Decl f type Combinator f = forall a. f (Process (Rule a)) associative :: Decl f -> Decl f isAssociative :: Decl f -> Bool combinator :: Decl f -> Combinator f (.=.) :: IsId n => n -> Combinator f -> Decl f applyDecl :: Arity f => Decl f -> f (StrategyTree a) class Arity f listify :: Arity f => f a -> [a] -> Maybe a toArity :: Arity f => ([a] -> a) -> f a liftIso :: Arity f => Isomorphism a b -> f a -> f b data Nullary a Nullary :: a -> Nullary a [fromNullary] :: Nullary a -> a data Unary a Unary :: (a -> a) -> Unary a [fromUnary] :: Unary a -> a -> a data Binary a Binary :: (a -> a -> a) -> Binary a [fromBinary] :: Binary a -> a -> a -> a data Nary a Nary :: ([a] -> a) -> Nary a [fromNary] :: Nary a -> [a] -> a instance GHC.Show.Show (Ideas.Common.Strategy.StrategyTree.Decl f) instance GHC.Classes.Eq (Ideas.Common.Strategy.StrategyTree.Decl f) instance Ideas.Common.Id.HasId (Ideas.Common.Strategy.StrategyTree.Decl f) instance Ideas.Common.Strategy.StrategyTree.Arity Ideas.Common.Strategy.StrategyTree.Nullary instance Ideas.Common.Strategy.StrategyTree.Arity Ideas.Common.Strategy.StrategyTree.Unary instance Ideas.Common.Strategy.StrategyTree.Arity Ideas.Common.Strategy.StrategyTree.Binary instance Ideas.Common.Strategy.StrategyTree.Arity Ideas.Common.Strategy.StrategyTree.Nary -- | Abstract data type for a Strategy and a LabeledStrategy. module Ideas.Common.Strategy.Abstract -- | Abstract data type for strategies data Strategy a -- | A strategy which is labeled with an identifier data LabeledStrategy a -- | Labels a strategy with an identifier. Labels are used to identify -- substrategies and to specialize feedback messages. The first argument -- of label can be of type String, in which case the string -- is used as identifier (and not as description). label :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a -- | Removes the label from a strategy unlabel :: LabeledStrategy a -> Strategy a -- | Type class to turn values into strategies class IsStrategy f toStrategy :: IsStrategy f => f a -> Strategy a liftS :: IsStrategy f => (Strategy a -> Strategy a) -> f a -> Strategy a liftS2 :: (IsStrategy f, IsStrategy g) => (Strategy a -> Strategy a -> Strategy a) -> f a -> g a -> Strategy a liftSn :: IsStrategy f => ([Strategy a] -> Strategy a) -> [f a] -> Strategy a -- | Construct the empty prefix for a labeled strategy emptyPrefix :: IsStrategy f => f a -> a -> Prefix a -- | Construct a prefix for a path and a labeled strategy. The third -- argument is the current term. replayPath :: IsStrategy f => Path -> f a -> a -> ([Rule a], Prefix a) -- | Construct a prefix for a list of paths and a labeled strategy. The -- third argument is the current term. replayPaths :: IsStrategy f => [Path] -> f a -> a -> Prefix a -- | Construct a prefix for a path and a labeled strategy. The third -- argument is the initial term. replayStrategy :: (Monad m, IsStrategy f) => Path -> f a -> a -> m (a, Prefix 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 derivationList :: IsStrategy f => (Rule a -> Rule a -> Ordering) -> f a -> a -> [Derivation (Rule a, Environment) a] toStrategyTree :: IsStrategy f => f a -> StrategyTree a onStrategyTree :: IsStrategy f => (StrategyTree a -> StrategyTree a) -> f a -> Strategy a useDecl :: Arity f => Decl f -> f (Strategy a) decl0 :: Decl Nullary -> Strategy a decl1 :: IsStrategy f => Decl Unary -> f a -> Strategy a decl2 :: (IsStrategy f, IsStrategy g) => Decl Binary -> f a -> g a -> Strategy a declN :: IsStrategy f => Decl Nary -> [f a] -> Strategy a instance GHC.Show.Show (Ideas.Common.Strategy.Abstract.Strategy a) instance Ideas.Common.Classes.Apply Ideas.Common.Strategy.Abstract.Strategy instance Ideas.Common.Strategy.Choice.Choice (Ideas.Common.Strategy.Abstract.Strategy a) instance Ideas.Common.Strategy.Sequence.Sequence (Ideas.Common.Strategy.Abstract.Strategy a) instance Ideas.Common.Classes.Fix (Ideas.Common.Strategy.Abstract.Strategy a) instance Ideas.Common.Strategy.Abstract.IsStrategy Ideas.Common.Strategy.Abstract.Strategy instance Ideas.Common.Strategy.Abstract.IsStrategy Ideas.Common.Strategy.Abstract.LabeledStrategy instance Ideas.Common.Strategy.Abstract.IsStrategy Ideas.Common.Rule.Abstract.Rule instance Ideas.Common.Strategy.Abstract.IsStrategy Ideas.Common.Rewriting.RewriteRule.RewriteRule instance GHC.Show.Show (Ideas.Common.Strategy.Abstract.LabeledStrategy a) instance Ideas.Common.Classes.Apply Ideas.Common.Strategy.Abstract.LabeledStrategy instance Ideas.Common.Id.HasId (Ideas.Common.Strategy.Abstract.LabeledStrategy a) instance Ideas.Common.View.LiftView Ideas.Common.Strategy.Abstract.LabeledStrategy instance Ideas.Common.View.LiftView Ideas.Common.Strategy.Abstract.Strategy -- | Locations that correspond to the labels in a strategy module Ideas.Common.Strategy.Location checkLocation :: Id -> LabeledStrategy a -> Bool subTaskLocation :: LabeledStrategy a -> Id -> Id -> Id nextTaskLocation :: LabeledStrategy a -> Id -> Id -> Id -- | Returns a list of all strategy locations, paired with the label strategyLocations :: LabeledStrategy a -> [([Int], Id)] -- | This module defines extra combinators. module Ideas.Common.Strategy.Derived -- | Allows all permutations of the list permute :: (Choice a, Sequence a) => [a] -> a many :: (Sequence a, Fix a, Choice a) => a -> a many1 :: (Sequence a, Fix a, Choice a) => a -> a replicate :: Sequence a => Int -> a -> a -- | Apply a certain strategy or do nothing (non-greedy) option :: (Choice a, Sequence a) => a -> a -- | Apply a certain strategy if this is possible (greedy version of -- option) try :: (Choice a, Sequence a) => a -> a -- | Repeat a strategy zero or more times (greedy version of many) repeat :: (Sequence a, Fix a, Choice a) => a -> a -- | Apply a certain strategy at least once (greedy version of -- many1) repeat1 :: (Sequence a, Fix a, Choice a) => a -> a -- | Apply the strategies from the list exhaustively (until this is no -- longer possible) exhaustive :: (Sequence a, Fix a, Choice a) => [a] -> a atomic :: AtomicSymbol a => Process a -> Process a (<%>) :: (AtomicSymbol a, LabelSymbol a) => Process a -> Process a -> Process a interleave :: (AtomicSymbol a, LabelSymbol a) => [Process a] -> Process a (<@>) :: AtomicSymbol a => Process a -> Process a -> Process a (!*>) :: AtomicSymbol a => Process a -> Process a -> Process a inits :: AtomicSymbol a => Process a -> Process a filterP :: (a -> Bool) -> Process a -> Process a hide :: (a -> Bool) -> Process a -> Process a -- | Strategies can be configured at their labeled positions. Possible -- actions are removereinsert, collapseexpand, and hide/reveal. module Ideas.Common.Strategy.Configuration data StrategyCfg byName :: HasId a => ConfigAction -> a -> StrategyCfg data ConfigAction Remove :: ConfigAction Reinsert :: ConfigAction Collapse :: ConfigAction Expand :: ConfigAction Hide :: ConfigAction Reveal :: ConfigAction configure :: StrategyCfg -> LabeledStrategy a -> LabeledStrategy a configureS :: StrategyCfg -> Strategy a -> Strategy a remove :: IsStrategy f => f a -> Strategy a collapse :: IsStrategy f => f a -> Strategy a hide :: IsStrategy f => f a -> Strategy a -- | Apply a strategy at least once, but collapse into a single step multi :: (IsId l, IsStrategy f) => l -> f a -> Strategy a isConfigId :: HasId a => a -> Bool instance GHC.Classes.Eq Ideas.Common.Strategy.Configuration.ConfigAction instance GHC.Show.Show Ideas.Common.Strategy.Configuration.ConfigAction instance GHC.Show.Show Ideas.Common.Strategy.Configuration.StrategyCfg instance GHC.Base.Monoid Ideas.Common.Strategy.Configuration.StrategyCfg instance GHC.Show.Show Ideas.Common.Strategy.Configuration.ConfigLocation instance GHC.Read.Read Ideas.Common.Strategy.Configuration.ConfigAction -- | Converting a strategy to XML, and the other way around. module Ideas.Encoding.StrategyInfo strategyToXML :: IsStrategy f => f a -> XML -- | 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 -- | Alternate two strategies (.@.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a -- | Prefixing a basic rule to a strategy atomically (!~>) :: IsStrategy f => Rule a -> f a -> Strategy a -- | Initial prefixes (allows the strategy to stop succesfully at any time) inits :: IsStrategy f => f 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 choice :: IsStrategy f => [f a] -> Strategy a -- | Merges a list of strategies (in parallel) interleave :: IsStrategy f => [f a] -> Strategy a noInterleaving :: IsStrategy f => f a -> Strategy a interleaveId :: Id -- | 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 -- | Choose between the two strategies, with a preference for steps from -- the left hand-side strategy. (./.) :: (IsStrategy f, IsStrategy g) => f a -> g 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 the strategies from the list exhaustively (until this is no -- longer possible) exhaustive :: IsStrategy f => [f a] -> Strategy a type DependencyGraph node key = [(node, key, [key])] -- | Create a strategy from a dependency graph with strategies as nodes -- Does not check for cycles dependencyGraph :: (IsStrategy f, Ord key) => DependencyGraph (f a) key -> Strategy a -- | Parameterized traversals based on the strategy language. 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 leftmost :: Option a rightmost :: 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 leftmostbu :: (IsStrategy f, Navigator a) => f a -> Strategy a leftmosttd :: (IsStrategy f, Navigator a) => f a -> Strategy a somewhere :: (IsStrategy f, Navigator a) => f a -> Strategy a somewhereWhen :: (IsStrategy g, Navigator a) => (a -> Bool) -> g a -> Strategy a oncetdPref :: (IsStrategy f, Navigator a) => f a -> Strategy a oncebuPref :: (IsStrategy f, Navigator a) => f a -> Strategy a -- | left-most innermost traversal. innermost :: (IsStrategy f, Navigator a) => f a -> Strategy a -- | left-most outermost traversal. outermost :: (IsStrategy f, Navigator a) => f a -> Strategy a ruleUp :: Navigator a => Rule a ruleDown :: Navigator a => Rule a ruleDownLast :: Navigator a => Rule a ruleLeft :: Navigator a => Rule a ruleRight :: Navigator a => Rule a instance GHC.Base.Monoid (Ideas.Common.Strategy.Traversal.Option a) -- | Legacy strategy combinators (before the Functor-Applicative-Monad -- proposal) module Ideas.Common.Strategy.Legacy (<%>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a (<@>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a (<|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a (>|>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a (<*>) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a alternatives :: IsStrategy f => [f a] -> Strategy a -- | A strategy is a context-free grammar with rules as symbols. Strategies -- can be labeled with strings. The type class IsStrategy is -- introduced to lift functions and combinators that work on strategies -- to also accept rules and labeled strategies. This module re-exports -- the most important functionality of the underlying modules. module Ideas.Common.Strategy -- | Abstract data type for strategies data Strategy a -- | A strategy which is labeled with an identifier data LabeledStrategy a -- | Type class to turn values into strategies class IsStrategy f toStrategy :: IsStrategy f => f a -> Strategy a derivationList :: IsStrategy f => (Rule a -> Rule a -> Ordering) -> f a -> a -> [Derivation (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 -- | Alternate two strategies (.@.) :: (IsStrategy f, IsStrategy g) => f a -> g a -> Strategy a -- | Prefixing a basic rule to a strategy atomically (!~>) :: IsStrategy f => Rule a -> f 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 an identifier. Labels are used to identify -- substrategies and to specialize feedback messages. The first argument -- of label can be of type String, in which case the string -- is used as identifier (and not as description). label :: (IsId l, IsStrategy f) => l -> f a -> LabeledStrategy a -- | Initial prefixes (allows the strategy to stop succesfully at any time) inits :: 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 choice :: IsStrategy f => [f a] -> Strategy a 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 -- | Choose between the two strategies, with a preference for steps from -- the left hand-side 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 type DependencyGraph node key = [(node, key, [key])] -- | Create a strategy from a dependency graph with strategies as nodes -- Does not check for cycles dependencyGraph :: (IsStrategy f, Ord key) => DependencyGraph (f a) key -> Strategy a -- | Returns a list of all strategy locations, paired with the label strategyLocations :: LabeledStrategy a -> [([Int], Id)] checkLocation :: Id -> LabeledStrategy a -> Bool subTaskLocation :: LabeledStrategy a -> Id -> Id -> Id nextTaskLocation :: LabeledStrategy a -> Id -> Id -> Id data Prefix a -- | Construct the empty prefix for a labeled strategy emptyPrefix :: IsStrategy f => f a -> a -> Prefix a -- | The error prefix (i.e., without a location in the strategy). noPrefix :: Prefix a -- | Construct a prefix for a path and a labeled strategy. The third -- argument is the current term. replayPath :: IsStrategy f => Path -> f a -> a -> ([Rule a], Prefix a) -- | Construct a prefix for a list of paths and a labeled strategy. The -- third argument is the current term. replayPaths :: IsStrategy f => [Path] -> f a -> a -> Prefix a -- | Construct a prefix for a path and a labeled strategy. The third -- argument is the initial term. replayStrategy :: (Monad m, IsStrategy f) => Path -> f a -> a -> m (a, Prefix a) -- | A path encodes a location in a strategy. Paths are represented as a -- list of integers. data Path -- | The empty path. emptyPath :: Path readPath :: Monad m => String -> m Path readPaths :: Monad m => String -> m [Path] -- | Returns the current Path. prefixPaths :: Prefix a -> [Path] -- | Transforms the prefix such that only major steps are kept in the -- remaining strategy. majorPrefix :: Prefix a -> Prefix a isEmptyPrefix :: Prefix a -> Bool -- | 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.Algebra.Group -- | The class of monoids (types with an associative binary operation that -- has an identity). Instances should satisfy the following laws: -- --
mappend mempty x = x
mappend x mempty = x
mappend x (mappend y z) = mappend (mappend x y) z
mconcat = foldr mappend mempty