----------------------------------------------------------------------------- -- Copyright 2019, Advise-Me project team. This file is distributed under -- the terms of the Apache License 2.0. For more information, see the files -- "LICENSE.txt" and "NOTICE.txt", which are included in the distribution. ----------------------------------------------------------------------------- -- | -- Maintainer : bastiaan.heeren@ou.nl -- Stability : provisional -- Portability : portable (depends on ghc) -- ----------------------------------------------------------------------------- module Recognize.Parsing.Interpretation ( InterpretationParser, toStep, interpret, addWildcardConstraint , pStepEq, (>/<), (>*<), (>-<), (>+<), (>^<) , (>>*<<), (>>+<<), (>>/<<), withModulo , pNamedStep, inLiberalEquationMode, Interpretation , getMatchEnvironment, getWildcard, pStepIneq, pStep , clearWildcard, pStepStrongIneq', defaultModulo, squared , sum'', sum', initialState ) where import Control.Applicative import Control.Arrow import Control.Monad import Control.Monad.Identity import Control.Monad.State import Data.Function import Data.List import Domain.Math.Data.MultivariatePolynomial import Domain.Math.Data.Relation import Domain.Math.Expr import Domain.Math.Numeric.Views import Ideas.Common.Id import Ideas.Common.Rewriting import Ideas.Common.View import Ideas.Utils.Uniplate import Recognize.Data.Attribute import Recognize.Data.Math import Recognize.Data.Diagnosis import Recognize.Data.Step import Recognize.Data.Definition import Recognize.Expr.Functions import Recognize.Expr.Normalform import Recognize.Expr.Symbols hiding (wildcard) import Recognize.Parsing.Derived import Recognize.Parsing.Parse import Recognize.Parsing.MathParser import Recognize.Data.MathParserOptions import Recognize.Parsing.Parser import Util.Expr import Util.List import qualified Data.Map as M data ExprParseState = ExprParseState { getEnvironment :: M.Map String Expr -- ^ The environment contains variables the user defined , getMatchEnvironment :: M.Map String Expr -- ^ the match environment contains matches for wildcards , getPredicateEnvironment :: M.Map String (Expr -> Bool) -- ^ the predicate environment contains predicates for wildcards , getEquality :: Expr -> Expr -> State (M.Map String Expr, M.Map String (Expr -> Bool)) Bool -- ^ The equality function used. We can actually think of this as a unification function due to the wildcards , isInLiberalEquationMode :: Bool -- ^ liberal equation mode allows you to parse any equation a = b as long as b - a is equivalent to what you expect , isInLiberalParenthesesMode :: Bool , isNormalized :: Expr -> Bool -- ^ a function to determine whether an expression is normalized } initialState :: ExprParseState initialState = ExprParseState { getEnvironment = mempty , getMatchEnvironment = mempty , getPredicateEnvironment = mempty , getEquality = moduloToEquality defaultModulo , isInLiberalEquationMode = False , isInLiberalParenthesesMode = True , isNormalized = defaultIsNormalized } -- The interpretation parser is a state monad transformer over a regular parser. -- It contains an environment for the user to define variables and keeps an equality function -- that specifies how liberal matching on expressions should be. type InterpretationParser = ParserT ExprParseState Math Identity -- we model possible inputs a student might have for a given concept as an interpretation. -- We can assign attributes to such interpretation (e.g. erroneous, misconception, common, far-fetched) type Interpretation = [(Expr,[Attribute])] -- | @interpret e@ represents the correct interpretation of @e@ without any attributes assigned interpret :: Expr -> Interpretation interpret e = [(e,[])] -------------------------------------------------------------------------------- -- Equality -------------------------------------------------------------------------------- --Parses with the given Equality function. withEquality :: (Expr -> Expr -> State (M.Map String Expr, M.Map String (Expr -> Bool)) Bool) -> InterpretationParser a -> InterpretationParser a withEquality e p = do oldEq <- state $ \st -> (getEquality st, st { getEquality = e }) x <- p modify $ \st -> st { getEquality = oldEq } return x --Turns a Expr -> Expr function f (called a modulo) into an Equality function. --What this means is that the Equality function generated will treat two expressions that are equal under the effect of the function f as equal. moduloToEquality :: (Expr -> Expr) -> Expr -> Expr -> State (M.Map String Expr, M.Map String (Expr -> Bool)) Bool moduloToEquality f x y = do r <- eqComAssoc f x y -- same problem here with normalization of wildcards.... if r then return r else eqComAssoc f (f x) (f y) --Takes a function Expr -> Expr f and parses with the added condition that two expressions are equal if they are equal under the effect of f. withModulo :: (Expr -> Expr) -> InterpretationParser a -> InterpretationParser a withModulo = withEquality . moduloToEquality --The default modulo function. defaultModulo :: Expr -> Expr defaultModulo = restoreWildcards . simplify (multivariatePolynomialViewWith rationalApproxView) . normalizePow . normalizeSqrt . wildcardsToVars where normalizeSqrt = transform f f (Sym s [Sqrt e, Nat 2]) | isPowerSymbol s = e f (Sym s [Sym w [e, Nat 1 :/: Nat 2], Nat 2]) | isPowerSymbol s , isPowerSymbol w = e f (Sqrt a :*: Sqrt b) | a == b = a -- werkt nu natuurlijk niet in product view.. (sqrt(2)*3*sqrt(2)) f e = e normalizePow = transform h h (Sym s [e, Nat i]) | isPowerSymbol s , i > 0 && i < 5 = foldr1 (.*.) (replicate (fromInteger i) e) h e = e -------------------------------------------------------------------------------- -- Normalization -------------------------------------------------------------------------------- --The default normailization function. (Notice that this is the only normalization function used in the InterpretationParser as of now.) defaultIsNormalized :: Expr -> Bool defaultIsNormalized p = sumEqual (sumList p) (sumList n) where n = simplify (multivariatePolynomialViewWith rationalView) (nf p) sumList (a1 :+: a2) = sumList a1 ++ sumList a2 sumList (a1 :-: a2) = sumList a1 ++ map Negate (sumList a2) sumList a = [a] sumEqual (x : xs) ys = sumEqual xs (removeFirst x [] ys) sumEqual [] [] = True sumEqual [] _ = False removeFirst x as (b:bs) | eqNorm x b = as ++ bs | otherwise = removeFirst x (as++[b]) bs removeFirst _ as [] = as eqNorm (Sym s1 _) (Sym s2 _) | isWildcardSymbol s1 && isWildcardSymbol s2 = False eqNorm (Nat a) (Nat b) = a == b eqNorm (Number a) (Number b) = a == b eqNorm (Nat a1 :/: Nat a2) (Number b) = fromIntegral a1 / fromIntegral a2 == b eqNorm (Number a) (Nat b1 :/: Nat b2) = fromIntegral b1 / fromIntegral b2 == a eqNorm (Var a) (Var b) = a == b eqNorm (a1 :*: a2) (b1 :*: b2) = (eqNorm a1 b1 && eqNorm a2 b2) || (eqNorm a1 b2 && eqNorm a2 b1) eqNorm a@(_ :+: _) b@(_ :+: _) = sumEqual (sumList a) (sumList b) eqNorm a@(_ :-: _) b@(_ :-: _) = sumEqual (sumList a) (sumList b) eqNorm a@(_ :-: _) b@(_ :+: _) = sumEqual (sumList a) (sumList b) eqNorm a@(_ :+: _) b@(_ :-: _) = sumEqual (sumList a) (sumList b) eqNorm (a1 :/: a2) (b1 :/: b2) = eqNorm a1 b1 && eqNorm a2 b2 eqNorm (Sqrt a) (Sqrt b) = eqNorm a b eqNorm (Negate a) (Negate b) = eqNorm a b eqNorm (Sym sa as) (Sym sb bs) | sa == sb = as == bs eqNorm _ _ = False -------------------------------------------------------------------------------- -- Liberal equation mode -------------------------------------------------------------------------------- -- Liberal equation mode interprets an equation a = b as an expression by subtracting the rhs from the lhs: a - b (=0). -- This allows to parse a broad set of equations from a single expression (e.g. 7). inLiberalEquationMode :: InterpretationParser a -> InterpretationParser a inLiberalEquationMode p = do st <- get let old = isInLiberalEquationMode st put st { isInLiberalEquationMode = True } x <- p put st { isInLiberalEquationMode = old } return x -------------------------------------------------------------------------------- -- Wildcards -------------------------------------------------------------------------------- clearWildcard :: String -> InterpretationParser () clearWildcard s = modify $ \st -> st { getMatchEnvironment = M.delete s (getMatchEnvironment st) } getWildcard :: String -> InterpretationParser (Maybe Expr) getWildcard s = gets (M.lookup s . getMatchEnvironment) setWildcards :: M.Map String Expr -> InterpretationParser () setWildcards me = state (\s -> ((), s {getMatchEnvironment = me})) addWildcardConstraint :: String -> (Expr -> Bool) -> InterpretationParser () addWildcardConstraint v p = state (\s -> ((), s {getPredicateEnvironment = M.insert v (p . toExpr) (getPredicateEnvironment s)})) -------------------------------------------------------------------------------- -- Definitions -------------------------------------------------------------------------------- addDefinition :: Definition Expr -> InterpretationParser () addDefinition (v, x) = state (\e@ExprParseState {getEnvironment = env} -> ((), e { getEnvironment = M.insert v x env })) filterParenthesis :: String -> String filterParenthesis = filter (`notElem` " {}()[]") ----------------------------------------------------- -- Parsing of Interpretations of expressions and equations ----------------------------------------------------- -- | @toStep p@ parses @p@ and captures @Math@ and returns a @Step@ toStep :: Id -> InterpretationParser [Attribute] -> InterpretationParser Step toStep i p = pWithMath $ \m -> p >>= \ats -> pure $ smallStep i (m,nub ats) toBigStep :: InterpretationParser [Step] -> InterpretationParser Step toBigStep p = do steps <- p case safeHead steps of Nothing -> empty Just s@(Step i (v,_) _) -> if length steps == 1 then return s else return (bigStep i (v,sort $ nub $ concatMap (\(Step _ (_,ats) _) -> ats) steps) steps) -- | @pNamedStep n a@ represents an Interpretation that can be named (L = ..), but still requires the concept -- to be explicitly written down. (e.g. @pNamedStep (interpret (Var "L")) (interpret (3+1)) succeeds on "3+1", "L=3+1", "L=4" but not on "L" pNamedStep :: Id -> Interpretation -> Interpretation -> InterpretationParser Step pNamedStep i a xs = pStepEq i a xs |> pStepEq i xs a |> pStep i xs -- | @pStep a i@ parses interpretation @i@ and assigns attribute @a@ (as identifier) -- We first try to see if we can match an equation e = e -- then we try to see if we can match a single expression e -- otherwise we try to see if we can match an equation * = e, or e = * where * is a wildcard pStep :: Id -> Interpretation -> InterpretationParser Step pStep i xs = toBigStep $ many1' ( toStep i (pSingleEquation xs xs) |> toStep i (snd <$> pSingleExpression xs) |> toStep i (matchEquation (interpret $ wildcard "_step") xs) |> toStep i (matchEquation xs (interpret $ wildcard "_step")) ) where matchEquation as bs = do x <- pSingleEquation as bs mExpr <- getWildcard "_step" clearWildcard "_step" case mExpr of Just e -> return (PartialMatch e : x) _ -> return x -- | @pStepRel i1 i2 xs ys@ parses an (in)equality @xs@ is assumed to be at most as big as @ys@. -- if we match on an equality we use @i1@ as step id, otherwise @i2@ pStepRel :: Id -> Id -> Interpretation -> Interpretation -> InterpretationParser Step pStepRel i1 i2 xs ys = pStepEq i1 xs ys |> pStepWeakIneq i2 xs ys |> pStepStrongIneq i2 xs ys -- | @pStepEq@ parses a (chained) equation. pStepEq :: Id -> Interpretation -> Interpretation -> InterpretationParser Step pStepEq i xs ys = toBigStep $ (:) <$> toStep i (pSingleEquation xs ys) <*> many' (toStep i (pSingleEquation ys ys)) |> (:) <$> toStep i (pSingleEquation ys xs) <*> many' (toStep i (pSingleEquation xs xs)) pStepWeakIneq :: Id -> Interpretation -> Interpretation -> InterpretationParser Step pStepWeakIneq i = stepIneq i pSingleWeakInequation pStepStrongIneq :: Id -> Interpretation -> Interpretation -> InterpretationParser Step pStepStrongIneq i = stepIneq i pSingleStrongInequation pStepStrongIneq' :: Id -> Interpretation -> Interpretation -> InterpretationParser Step pStepStrongIneq' i = stepIneq i pSingleStrongInequation' pStepIneq :: Id -> Interpretation -> Interpretation -> InterpretationParser (RelationType, Step) pStepIneq i xs ys = (,) LessThanOrEqualTo <$> pStepWeakIneq i xs ys |> (,) GreaterThanOrEqualTo <$> pStepWeakIneq i ys xs |> (,) LessThan <$> pStepStrongIneq i xs ys |> (,) GreaterThan <$> pStepStrongIneq i ys xs -- TODO Hier gaat iets niet goed! xs == xs < ys == ys |> ys == ys < xs == xs -- Wat gaat niet goed: Als we relatie x < y willen herkennen -- we herkennen dan als juist: x < y -- dan herkennen we ook x = x' < y' = y -- we herkennen ook y < x als incorrect -- maar we herkennen niet y = y' < x' = x als incorrect. -- Komt verder niet echt in data set voor dus voor nu laten zitten. stepIneq :: Id -> (Interpretation -> Interpretation -> InterpretationParser [Attribute]) -> Interpretation -> Interpretation -> InterpretationParser Step stepIneq i pSingleIneq xs ys = toBigStep (combine xs ys {- TODO HIER BUG: |> combine ys xs) -}) where combine :: Interpretation -> Interpretation -> InterpretationParser [Step] combine xs ys = do as <- many' (toStep i (pSingleEquation xs xs)) b <- toStep i (pSingleIneq xs ys) cs <- many' (toStep i (pSingleEquation ys ys)) return (as ++ [b] ++ cs) pSingleStrongInequation :: Interpretation -> Interpretation -> InterpretationParser [Attribute] pSingleStrongInequation xs ys = snd <$> ( pExplicitRel [(LessThan,[],xs,ys)] |> pExplicitRel [(GreaterThan,[],ys,xs)]) -- todo: make nicer (Have Interpretation (Relation Expr)) pSingleStrongInequation' :: Interpretation -> Interpretation -> InterpretationParser [Attribute] pSingleStrongInequation' xs ys = snd <$> ( pExplicitRel [(LessThan,[],xs,ys)] |> pExplicitRel [(GreaterThan,[],ys,xs)] |> pExplicitRel [(LessThan,[AsymmetricRelation],ys,xs)] |> pExplicitRel [(GreaterThan,[AsymmetricRelation],xs,ys)] |> pExplicitRel [(LessThanOrEqualTo,[InequalityStrictness],xs,ys)] |> pExplicitRel [(GreaterThanOrEqualTo,[InequalityStrictness],ys,xs)] |> pExplicitRel [(LessThanOrEqualTo,[InequalityStrictness,AsymmetricRelation],ys,xs)] |> pExplicitRel [(GreaterThanOrEqualTo,[InequalityStrictness,AsymmetricRelation],xs,ys)] ) pSingleWeakInequation :: Interpretation -> Interpretation -> InterpretationParser [Attribute] pSingleWeakInequation xs ys = snd <$> ( pExplicitRel [(LessThanOrEqualTo,[],xs,ys)] |> pExplicitRel [(GreaterThanOrEqualTo,[],ys,xs)]) pSingleExpression :: Interpretation -> InterpretationParser (Expr, [Attribute]) pSingleExpression xs = do st <- get choice' [ pExprWithWildcard e ats |> do d@(_,p) <- pDefinition' e addDefinition d return (p, [ Normalized | isNormalized st p ] ++ ats) | (e,ats) <- xs ] pSingleEquation :: Interpretation -> Interpretation -> InterpretationParser [Attribute] pSingleEquation a b = snd <$> pExplicitRel [(EqualTo,[],a,b)] pDefinition' :: Expr -> InterpretationParser (Definition Expr) pDefinition' x = do st <- get (d,me) <- satisfyWith (\m -> case getEq m of Just (d :==: y) -> do let (b,(me,_)) = runState ((getEquality st `on` substitute (getEnvironment st)) x y) (getMatchEnvironment st, getPredicateEnvironment st) guard b case getVariable d of Just v -> return ((v, y),me) _ -> Nothing Nothing -> Nothing) setWildcards me return d pExplicitRel :: [(RelationType,[Attribute],Interpretation,Interpretation)] -> InterpretationParser (Relation Expr, [Attribute]) pExplicitRel rs = choice' [ do st <- get mE <- safePeek m <- return $ do e <- mE r <- getRelation e guard (relationType r == rT) if isInLiberalEquationMode st && relationType r == EqualTo then do ((_,(me2,_)),as) <- find (fst.fst) $ map (first (flip runState (getMatchEnvironment st,getPredicateEnvironment st) . (getEquality st `on` substitute (getEnvironment st)) (leftHandSide r :-: rightHandSide r))) (xs >-< ys <|> interpret (Negate 1) >*< (xs >-< ys)) let me3 = M.map toExpr me2 return (r , [ Normalized | checkNormalized st r ] ++ rAts ++ as, me3) else do ((_,(me2,_)),as) <- find (fst.fst) $ map (first (flip runState (getMatchEnvironment st, getPredicateEnvironment st) . (getEquality st `on` substitute (getEnvironment st)) (leftHandSide r))) xs ((_,(me3,_)),bs) <- find (fst.fst) $ map (first (flip runState (me2, getPredicateEnvironment st) . (getEquality st `on` substitute (getEnvironment st)) (rightHandSide r))) ys return (r , [ Normalized | checkNormalized st r ] ++ rAts ++ as ++ bs, me3) case m of Just (r,ats,me) -> do _ <- skip setWildcards me when (relationType r == EqualTo) (mapM_ addDefinition (match definitionView r)) return (r, ats) _ -> empty | (rT,rAts,xs,ys) <- rs ] where checkNormalized st r | nf (rightHandSide r) == nf (leftHandSide r) = isNormalized st (rightHandSide r) || isNormalized st (leftHandSide r) | isFunctionDefinition (leftHandSide r) = isNormalized st (rightHandSide r) | isFunctionDefinition (rightHandSide r) = isNormalized st (leftHandSide r) | isVar (leftHandSide r) = isNormalized st (rightHandSide r) | isVar (rightHandSide r) = isNormalized st (leftHandSide r) | otherwise = isNormalized st (rightHandSide r :-: leftHandSide r) pExprWithWildcard :: Expr -> [Attribute] -> InterpretationParser (Expr,[Attribute]) pExprWithWildcard x as = do mE <- safePeek st <- get let m = do e <- mE case getResult e of Left _ -> do guard $ isInLiberalParenthesesMode st e' <- safeSingleton (snd $ parseMath mathParserOptions (filterParenthesis (getString e))) x' <- safeSingleton (snd $ parseMath mathParserOptions (filterParenthesis (show x))) x'' <- getExpr x' y <- getExpr e' let stn = (getEquality st `on` substitute (getEnvironment st)) x'' y (b,(me2,_)) = runState stn (getMatchEnvironment st,getPredicateEnvironment st) guard b return (y,me2,NonMatchingParentheses : as) Right y -> let stn = (getEquality st `on` substitute (getEnvironment st)) x y (b,(me2,_)) = runState stn (getMatchEnvironment st,getPredicateEnvironment st) in guard b >> return (y,me2,as) case m of Just (y,me3,ats) -> do _ <- skip setWildcards me3 return (y, [ Normalized | isNormalized st y] ++ ats) _ -> empty pWithMath :: (Math -> InterpretationParser a) -> InterpretationParser a pWithMath = (peek >>=) ----------------------------------------------------- -- Common interpretations for expressions and equations ----------------------------------------------------- -- | @binaryop f x y@ applies binary function @f@ for each interpretation of @x@ and @y@. binaryOp :: (Expr -> Expr -> Expr) -> Interpretation -> Interpretation -> Interpretation binaryOp f xs ys = [ (f x y, xa ++ ya) | (x, xa) <- xs , (y, ya) <- ys] -- | @>+<@ represents the correct interpretation of @+@ regardless of mistakes in the arguments infixl 5 >+< (>+<) :: Interpretation -> Interpretation -> Interpretation (>+<) = binaryOp (+) -- | @>*<@ represents the correct representation of @*@ infixl 7 >*< (>*<) :: Interpretation -> Interpretation -> Interpretation (>*<) = binaryOp (*) infixl 6 >-< (>-<) :: Interpretation -> Interpretation -> Interpretation (>-<) = binaryOp (-) infixl 7 >/< (>/<) :: Interpretation -> Interpretation -> Interpretation (>/<) = binaryOp (/) infixr 8 >^< (>^<) :: Interpretation -> Interpretation -> Interpretation (>^<) = binaryOp (**) -- | @x >>*<< y@ generates possible interpretations (correct and erroneous) for multiplying an interpretation of x with an interpretation of y, -- for now we assume the interpretations x and y are monomial or binomial (because specific to Rectangle Area exercise) infixl 7 >>*<< (>>*<<) :: Interpretation -> Interpretation -> Interpretation xs >>*<< ys = xs >*< ys <|> concat [ [ (e + to sumView (delete e zs) * y, xa ++ ya ++ [IncorrectDistribution]) | let zs = from sumView x , length zs > 1 , e <- zs] ++ [ (x * to sumView (delete e zs) + e, xa ++ ya ++ [IncorrectDistribution]) | let zs = from sumView y , length zs > 1 , e <- zs ] ++ [ (a + to sumView (delete a zs) * to sumView (delete b ws) + b, xa ++ ya ++ [IncorrectDistribution]) | let zs = from sumView x , length zs > 1 , a <- zs , let ws = from sumView y , length ws > 1 , b <- ws ] | (x, xa) <- xs , (y, ya) <- ys ] -- | @x >>/<< y@ generates possible interpretations (correct and erroneous) for division -- the erroneous interpretation consists of distributing division over multiplication, eg: (a*b/2 <-> a/2*b/2) infixl 7 >>/<< (>>/<<) :: Interpretation -> Interpretation -> Interpretation xs >>/<< ys = xs >/< ys <|> [ (to productView (n, [ a / y | a <- zs ]), xa ++ ya ++ [IncorrectDistribution]) | (x, xa) <- xs , (y, ya) <- ys , let (n,zs) = from productView x , length zs > 1 ] -- | @x >>+<< y@ represents the correct and erroneous interpretation of @+@. infixl 5 >>+<< (>>+<<) :: Interpretation -> Interpretation -> Interpretation xs >>+<< ys = xs >+< ys <|> xs >*< ys Interpretation sum' [] = [] sum' xs = foldr1 (>+<) xs -- | @sum'' xs@ represents the correct and incorrect representation of sum sum'' :: [Interpretation] -> Interpretation sum'' [] = [] sum'' xs = foldr1 (>>+<<) xs squared :: Interpretation -> Interpretation squared square = concat [ [(s ** 2 , ss) {- ,(s * s, ss)-} ,(4 * s, Misconception Perimeter Area : ss) ] | (s,ss) <- square]