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
, getMatchEnvironment :: M.Map String Expr
, getPredicateEnvironment :: M.Map String (Expr -> Bool)
, getEquality :: Expr -> Expr -> State (M.Map String Expr, M.Map String (Expr -> Bool)) Bool
, isInLiberalEquationMode :: Bool
, isInLiberalParenthesesMode :: Bool
, isNormalized :: Expr -> Bool
}
initialState :: ExprParseState
initialState =
ExprParseState
{ getEnvironment = mempty
, getMatchEnvironment = mempty
, getPredicateEnvironment = mempty
, getEquality = moduloToEquality defaultModulo
, isInLiberalEquationMode = False
, isInLiberalParenthesesMode = True
, isNormalized = defaultIsNormalized
}
type InterpretationParser = ParserT ExprParseState Math Identity
type Interpretation = [(Expr,[Attribute])]
interpret :: Expr -> Interpretation
interpret e = [(e,[])]
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
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
if r then return r
else eqComAssoc f (f x) (f y)
withModulo :: (Expr -> Expr) -> InterpretationParser a -> InterpretationParser a
withModulo = withEquality . moduloToEquality
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
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
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
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
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)}))
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` " {}()[]")
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 :: Id -> Interpretation -> Interpretation -> InterpretationParser Step
pNamedStep i a xs = pStepEq i a xs
|> pStepEq i xs a
|> pStep i xs
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 :: Id -> Id -> Interpretation -> Interpretation -> InterpretationParser Step
pStepRel i1 i2 xs ys = pStepEq i1 xs ys
|> pStepWeakIneq i2 xs ys
|> pStepStrongIneq i2 xs ys
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
stepIneq :: Id -> (Interpretation -> Interpretation -> InterpretationParser [Attribute]) -> Interpretation -> Interpretation -> InterpretationParser Step
stepIneq i pSingleIneq xs ys = toBigStep (combine xs ys )
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)])
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 >>=)
binaryOp :: (Expr -> Expr -> Expr) -> Interpretation -> Interpretation -> Interpretation
binaryOp f xs ys = [ (f x y, xa ++ ya)
| (x, xa) <- xs
, (y, ya) <- ys]
infixl 5 >+<
(>+<) :: Interpretation -> Interpretation -> Interpretation
(>+<) = binaryOp (+)
infixl 7 >*<
(>*<) :: Interpretation -> Interpretation -> Interpretation
(>*<) = binaryOp (*)
infixl 6 >-<
(>-<) :: Interpretation -> Interpretation -> Interpretation
(>-<) = binaryOp (-)
infixl 7 >/<
(>/<) :: Interpretation -> Interpretation -> Interpretation
(>/<) = binaryOp (/)
infixr 8 >^<
(>^<) :: Interpretation -> Interpretation -> Interpretation
(>^<) = binaryOp (**)
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
]
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
]
infixl 5 >>+<<
(>>+<<) :: Interpretation -> Interpretation -> Interpretation
xs >>+<< ys = xs >+< ys
<|> xs >*< ys <! OperatorMixedUp timesSymbol plusSymbol
sum' :: [Interpretation] -> Interpretation
sum' [] = []
sum' xs = foldr1 (>+<) xs
sum'' :: [Interpretation] -> Interpretation
sum'' [] = []
sum'' xs = foldr1 (>>+<<) xs
squared :: Interpretation -> Interpretation
squared square = concat [ [(s ** 2 , ss)
,(4 * s, Misconception Perimeter Area : ss)
]
| (s,ss) <- square]