-----------------------------------------------------------------------------
-- 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)
--
-- This module defines the subexpression recognizer.
-- If you wish to extend the language that the subexpression recognizer accepts, see "Recognize.SubExpr.Symbols"
-- Common functions can be found in "Recognize.SubExpr.Functions"
-- If you wish to make use of the parameters of the recognizer see "Recognize.SubExpr.SEParser"
-- Finally, if you want to change/view the comparison functions see "Recognize.SubExpr.Compare"
-- Throughout the code you may find log statements. Logging is only visible if debug mode is on.
-- The algorithm is still a WIP and doesn't look very polished. It is however in a usable state (see exercises theatrerate, pattern, vpattern and matryoshka).
-- 
-----------------------------------------------------------------------------

module Recognize.SubExpr.Recognizer
   ( pMatchSubSteps
   ) where

import           Control.Applicative (empty, (<|>))
import           Control.Arrow
import           Control.Monad
import           Data.Maybe
import qualified Data.Map as M
import           Domain.Math.Data.Relation
import           Domain.Math.Expr
import           Ideas.Common.Id        (newId)
import           Ideas.Common.Rewriting
import           Ideas.Common.View (from)
import Ideas.Utils.Prelude
import Recognize.Parsing.Parse
import Recognize.Data.Math
import Recognize.Parsing.Derived
import Recognize.SubExpr.SEParser
import Recognize.Expr.Functions as F
import Recognize.Expr.Normalform
import Recognize.SubExpr.Compare
import Recognize.SubExpr.Symbols
import Recognize.SubExpr.Functions as SF
import Recognize.Data.Attribute
import Recognize.Data.Diagnosis
import Recognize.Data.Step
import Util.List
import Util.Monad

-- | Accepts an expression for matching with input expressions
--
-- The algorithm parses an input as long as it matches against the given expression.
-- Input can be matched in 4 different ways.
--
-- * Input matches exactly (module commutativity, associativity)
-- * Input matches simplified
-- * Input matches exactly (..) against a subexpression
-- * Input matches simplified against a subexpression
--
-- A small example: Given an expression 1 + 2, we can match against several different combinations of input:
-- [1,2,1+2,3,3] [3,3,3] [2,1,3] etc
--
-- Note that we can no longer match an input if we had already parsed an simplified form of this input, unless
-- the
pMatchSubSteps :: Expr -> SEParser (Expr, [Step])
pMatchSubSteps m = do
  pLog $ "pMatchSubSteps: " ++ show m

  b_iter <- gets optIterate
  stop_pred <- gets matchPredicate

  -- Iterates over input matching them to an expression until no more expression matches.
  -- if we were unable to match the whole expression to some input we will fail.
  (e,st) <- pFoldAlt b_iter (\(m2,steps) -> do
    pLog ("Iteration: " ++ show m2 ++ " " ++ show steps)
    math <- peek
    pLog ("Math: " ++ show math)
    -- If we have a matched expression, then check whether we have to stop or not
    when (isMatched m2) $ pLog "stopping" >> guard (stop_pred m2)

    -- If we can't match against @math@ then we may try to skip it
    choice' [successStep (m2,steps) math, failStep (m2,steps)]
    ) (m,[]) -- initial to be matched expression

  pLog ("Can we exit pMatchSubSteps? " ++ show e ++ " | " ++ show (isMatched e))
  -- If @e@ is not matched then fail
  unless (isMatched e) empty

  -- Remove any expression constructors related to the subexpression recognizer
  -- However, this is not always possible: match 5 <&> match 6. In this case we must
  -- return 5 <$> 6.
  e2 <- pSubstituteVars e
  e3 <- maybeToParse $ getMatched e2
  let e4 = cleanExpr e3
  pLog ("Exit pMatchSubSteps: " ++ show (e4, st))
  return (e4, st)
  where
    successStep (m2,steps) math = do
      -- We take the input type specified by a parameter and attempt to parse/recognize
      -- @math@ according to that input type
      (m3, attr2) <- gets inputType >>= pMatchSubInputType m2 math
      -- If successful we can skip
      _ <- skip
      return (m3, steps ++ [Step (newId "subexpr") (math, attr2) []])
    -- Sometimes unrelated expressions can be mixed in with ones that we wish to recognize
    -- In that case we would like to skip over these and continue until we find a new expression
    -- that we can recognize
    failStep mst = do
      guardBy optSkipOnce -- Check if we can skip an expression
      modify $ \st -> st { optSkipOnce = False }
      _ <- skip
      pLog "Skip an expression"
      math <- peek
      successStep mst math

-- | Parses a @Math@ type according to the given allowed input types.
pMatchSubInputType :: Expr -> Math -> Maybe [InputType] -> SEParser (Expr, [Attribute])
pMatchSubInputType m math Nothing = do -- if none specified we try to figure out its inputtype on our own
  e <- getExpr math
  pLog ("pMatchSubInputType: " ++ show e ++ " : " ++ show (determineInputType e))
  pMatchSubInputType' m math (determineInputType e)
pMatchSubInputType m math (Just its) = do
  e <- getExpr math
  pLog ("pMatchSubInputType: " ++ show e ++ " : " ++ show (determineInputType e) ++ " " ++ show its)
  let e_inputType = determineInputType e

  guard $ any (doesTypeConform e e_inputType) its --Make sure the expression conforms to any of the input types.
  pMatchSubInputType' m math e_inputType
  where
    doesTypeConform e Linear lwt@(LinearWithType t) = e `conformsTo` lwt
    doesTypeConform _ eit it = eit == it

-- | Calls the recognizer function that corresponds to the inputtype
pMatchSubInputType' :: Expr -> Math -> InputType -> SEParser (Expr, [Attribute])
pMatchSubInputType' m math Expr = getExpr math >>= pMatchSubExpr m
pMatchSubInputType' m math Definition = getEq math >>= pMatchSubDef m
pMatchSubInputType' m math Equation = do
  che <- gets chainedEquations
  rel <- getRelation math
  pMatchSubEq che m (leftHandSide rel :==: rightHandSide rel)
pMatchSubInputType' m math Linear = do
  rel <- getRelation math
  pMatchSubLin m rel
pMatchSubInputType' m math (LinearWithType _) = pMatchSubInputType' m math Linear

-- | Match two expressions
pMatchSubExpr :: Expr -> Expr -> SEParser (Expr, [Attribute])
pMatchSubExpr m e = do
  pLog ("pMatchSubExpr: " ++ show m ++ " | " ++ show e)
  res <- pMatchSubInput (\x -> addMatching x >> return (matchExpr x)) m e
  pLog ("MatchedExpr: " ++ show m ++ " " ++ show e ++ " " ++ show res)
  return res

-- | Match an expression to an equation
--
-- First we see if we can match the two expression of the input equation. This tells us whether the equation is equal or unequal.
--
-- Next we match the expression to the left side of the equation.
--
-- Assuming everything matches we return the expression, but anything that was matched is replaced by the right side of the equation.
-- This could be the entire expression or some subterm.
pMatchSubEq :: Bool -> Expr -> Equation Expr -> SEParser (Expr, [Attribute])
pMatchSubEq _ m (x :==: y) = do
    pLog ("pMatchSubEq: " ++ show m ++ " | " ++ show x ++ " .==. " ++ show y)
    us <- resetSEState
    mxy <- option $ choice' [ (\(a,b) -> (a,b,y)) <$> pMatchSubInput return x y
                            -- , do
                            --   pLog ("CHE attempt: " ++ show (che, not (isAtom y)))
                            --   guard (che && not (isAtom y))
                            --   l <- maybeToParse $ getMostLeft y
                            --   (\(a,b) -> (a,b,l)) <$> pMatchSubInput (return . id) x l
                            ]
    put us
    -- If y is not a (simplified) subexpression of x then
    -- clearly the equation must be invalid
    let attr1 = maybe [InvalidEquation x y] (\t -> MatchedBy x y : snd3 t) mxy
    -- regardless of whether x is a subexpression of m
    -- we must continue with y
    when (isJust mxy) $ pLog ("Found Valid equation match: " ++ show mxy)
    when (isNothing mxy) $ pLog "Found Invalid equation"
    (m2,attr2) <- pMatchSubInput (\_ -> addMatching y >> return (matchExpr $ maybe y thd3 mxy)) m x

    pLog ("Matched: " ++ show m ++ " | " ++ show (x .==. y) ++ " | " ++ show m2 ++ " | " ++ show mxy)
    return (m2, filter (\a -> isLabelAttr a || isCommonMistake a) attr2 ++ attr1)

-- | Matches an expression to an equation (definition).
--
-- We only consider the right side of the equation for matching.
--
-- Since the left side of the equation may be used in further input we continue with both the left side and right side of the equation.
pMatchSubDef :: Expr -> Equation Expr -> SEParser (Expr, [Attribute])
pMatchSubDef m e@(x :==: y) = do
  pLog ("pMatchSubDef: " ++ show m ++ " | " ++ show e)
  (m2,rw) <- pMatchSubInput (\_ -> addMatching x >> addMatching y >> matchExpr <$> (return y <|> return x)) m y
  pLog ("MatchedDef: " ++ show m ++ " " ++ show e ++ " " ++ show m2)
  return (m2, rw)

-- | Match an expression to a relation
--
-- Both sides of the relation must match the expression.
pMatchSubLin :: Expr -> Relation Expr -> SEParser (Expr, [Attribute])
pMatchSubLin m rel = do
  let x = leftHandSide rel
  let y = rightHandSide rel
  pLog ("pMatchSubLin: " ++ show m ++ " | " ++ show x ++ " .==. " ++ show y)
  (m2,attrx) <- pMatchSubInput (\_ -> addMatching x >> matchExpr <$> return x) m x
  (m3,attry) <- pMatchSubInput (\_ -> addMatching y >> matchExpr <$> return y) m2 y
  return (m3,attrx++attry)

pMatchSubInput :: (Expr -> SEParser Expr) -> Expr -> Expr -> SEParser (Expr, [Attribute])
pMatchSubInput c m e =
  choice'
    [ pFindSubExpr c m e
    , do
      guardBy optGrow -- Only if we are allowed to grow can we call pMatchSubGrow
      guard (not $ hasMatch m)
      f <- gets growF
      -- pMatchSubGrow must match the entire motherexpression. Hence,
      -- if it succeeds we can simply the function c to the returned expression.
      -- This allows us to avoid c messing with the growing of the motherexpression
      applyFirstM c $ pMatchSubGrow f (\x -> addMatching x >> return (matchExpr x)) m e
    ]

-- | Using some growth function we grow the first expression if the first expression is a subexpression of the second expression.
pMatchSubGrow :: (Expr -> Expr) -> (Expr -> SEParser Expr) -> Expr -> Expr -> SEParser (Expr, [Attribute])
pMatchSubGrow f c m e = do
  pLog ("pMatchSubGrow " ++ show e ++ " " ++ show m)
  let alts = alternativesExpr m
  let findAlts = map (\(m2,rw) -> pFindSubExpr c e m2 >>= \(e2,_) -> return (e2,rw,m2)) alts
  (e2,rw,m2) <- choice' findAlts
  pLog $ "Matching in Grow: " ++ show e2 ++ " | " ++ show m2
  if isMatch e2
    then (\x -> (x,rw)) <$> c e
    else second (rw++) <$> pMatchSubGrow f c e2 (f (matchExpr m2))

-- | Interpreter for the subexpression recognizer language.
pFindSubExpr :: (Expr -> SEParser Expr) -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubExpr c m e = do
  pLog ("pFindSubExpr: " ++ show m ++ " " ++ show e)
  mres <- option pFindSubExpr'
  maybeToParse mres
  where
    -- Call the corresponding interpreting function
    pFindSubExpr' =
      case getFunction m of
        Nothing -> pFindSubNullary c m e
        Just (s,[])
          | isMagicNumberSymbol s -> pFindSubMagicNumber c e
          | isMagicNatSymbol s -> pFindSubMagicNat c e
          | isMagicVarSymbol s -> pFindSubMagicVar c e
        Just (s,[x])
          | isStopSymbol s     -> empty
          | isMatchSymbol s    -> pFindSubMatch c s x e
          | isSimSymbol s      -> pFindSubSim c s x e
          | isNoSimSymbol s    -> pFindSubNoSim c s x e
          | isSubSymbol s      -> pFindSubSub c s x e
          | isVarSymbol s      -> pFindSubVar c x e
          | otherwise          -> pFindSubUnary c s x e
        Just (s,[x,y])
          | isBuggySymbol s    -> pFindSubBuggy c x y e
          | isOrSymbol s       -> pFindSubOr c s x y e
          | isAndSymbol s      -> pFindSubAnd c s x y e
          | isLabelSymbol s    -> pFindSubLabel c s x y e
          | timesSymbol  == s  -> pFindSubAssoc c s (snd $ from productView m) e
          | plusSymbol   == s  -> pFindSubAssoc c s (from sumView m) e
          | divideSymbol == s  -> pFindSubDivision c s x y e
          | otherwise          -> pFindSubBinary c s x y e
        Just (s,[x,y,z])
          | isLtSymbol s       -> pFindSubLt c x y z e
        _ -> pLog ("Empty in pFindSubExpr: " ++ show m ++ " " ++ show e) >> empty

-- | Match if e is a number
pFindSubMagicNumber :: (Expr -> SEParser Expr) -> Expr -> SEParser (Expr, [Attribute])
pFindSubMagicNumber c e = do
  guard (isNumber e)
  (\x -> (x,[])) <$> c e

-- | Match if e is a natural number
pFindSubMagicNat :: (Expr -> SEParser Expr) -> Expr -> SEParser (Expr, [Attribute])
pFindSubMagicNat c e = do
  guard (isNat e)
  (\x -> (x,[])) <$> c e

-- | Match if e is a magic variable
pFindSubMagicVar :: (Expr -> SEParser Expr) -> Expr -> SEParser (Expr, [Attribute])
pFindSubMagicVar c e = do
  guard (F.isVar e)
  (\x -> (x,[])) <$> c e

-- | Compare two atoms
pFindSubNullary :: (Expr -> SEParser Expr) -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubNullary c e1 e2 = do
  pLog ("pFindSubNullary: " ++ show e1 ++ " " ++ show e2)
  precision <- gets precision
  b <- pCompare (roundNumber precision e1) (roundNumber precision e2)
  guard b
  (\x -> (x,[])) <$> c e1

-- | If an expression has been matched then we do not allow a subexpression of that expression to be matched.
--
-- Instead the expression may only be simplified
pFindSubMatch :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubMatch c s m e = do
  (e,attrs) <- pMatchAlts (function s [m]) e
  let mattr = MatchedBy m e
  e' <- c e
  return (e',mattr : attrs)

-- |  The second expression must be a simplification of the first expression
pFindSubSim :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubSim c s m e = do
  b <- gets optTraverse
  dic <- gets usedVariables
  modify $ \st -> st { optTraverse = False }
  m' <- maybeToParse $ substituteAllIf SF.isVar dic m
  (m2, attrs) <- pFindSubExpr c (nf $ cleanExpr m') e
  modify $ \st -> st { optTraverse = b }
  pLog $ "pFindSubSim " ++ show m' ++ " | " ++ show m2 ++ " | " ++ show e
  if isMatched m2 && isSimplified m2
    then return (m2, attrs)
    else return (function s [m2], attrs)

-- | No simplification allowed
pFindSubNoSim :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubNoSim c s m e = do
  pLog $ "pFindSubNoSim: " ++ show m ++ " " ++ show e
  modify $ \st -> st { optSimplify = False }
  (m2, attrs) <- pFindSubExpr c m e
  modify $ \st -> st { optSimplify = True }
  return (function s [m2], attrs)

-- | First a normalized matching only after we have a matching may we match simplifications.
pFindSubSub :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubSub c s m e = do
  pLog ("pFindSubSub: " ++ show m ++ " " ++ show e)
  guardBy optTraverse
  if isMatched m
    then do
      (m2,attrs) <- pFindSubExpr c m e
      if nfComAssoc m2 == nf m2
        then return (m2,attrs)
        else return (function s [m2],attrs)
    else do
      -- If m has yet to be matched then we do not allow m to match to its simplification (an atom)
      -- e.g. m : a + b
      -- first (a + b) must be matched, and only after that may some c = a + b, match with m
      -- This does mean that sub a, where a is an atom will never succeed
      guard (hasSub m || not (isAtom e))
      sim <- gets optSimplify
      modify $ \st -> st { optSimplify = False }
      (m2, attrs) <- pFindSubExpr c m e
      modify $ \st -> st { optSimplify = sim }
      pLog ("pFindSubSub: " ++ show m2)
      if isMatched m2 && nfComAssoc m2 == nf m2
        then return (m2, attrs)
        else return (function s [m2], attrs)

pFindSubVar :: (Expr -> SEParser Expr) -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubVar c (Var v) e = do
  pLog ("pFindSubVar: " ++ show v ++ " " ++ show e)
  vars <- gets usedVariables
  -- Look up the variable in the dictionary
  let mx = M.lookup v vars
  -- If the variable doesn't exist we fail parsing
  x <- maybeToParse mx

  -- For now we don't traverse into the found expression
  -- It is likely that we only bind variables to magic numbers,
  -- whose value change after matching it to some input
  (x2, attrs) <- applyFirstM c $ pMatchAlts x e
  -- Update the variable in the dictionary
  modify $ \st -> st { usedVariables = M.insert v x2 vars }
  pLog ("End of pFindSubVar: " ++ show x2)
  return (x2,attrs)
pFindSubVar _ _ _ = empty

-- | Match something that has a single parameter
pFindSubUnary :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubUnary c s m e =
  choice [ do
    guardBy optTraverse -- Are we allowed to traverse?
    (m2,rw) <- pFindSubExpr c m e
    return (function s [m2], rw)
         ,
    applyFirstM c $ pMatchAlts (function s [m]) e
  ]

-- | Match 'correct' left or 'incorrect' right
pFindSubBuggy :: (Expr -> SEParser Expr) -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubBuggy c x y e = do
  pLog ("pFindSubBuggy: " ++ show x ++ "  " ++ show y ++ " " ++ show e)
  choice
    [ do
      pLog "Go in Left"
      pFindSubExpr c x e
    , do
      pLog "Go in Right"
      second (CommonMistake:) <$> pFindSubExpr c y e
    ]

-- | Match left or right
pFindSubOr :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubOr c s x y e = do
  pLog ("pFindSubOr: " ++ show x ++ " " ++ show y ++ " " ++ show e)
  (eth, attr) <- choice
    [ first Left <$> pFindSubExpr c x e
    , first Right <$> pFindSubExpr c y e
    ]

  case eth of
    Left x' -> return (function s [x',y], attr)
    Right y' -> return (function s [x,y'],attr)

-- | Match left and right
pFindSubAnd :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubAnd c s x y e = do
  pLog ("pFindSubAnd: " ++ show x ++ " " ++ show y ++ " " ++ show e)
  (eth, attr) <- choice
    [ first Left <$> pFindSubExpr c x e
    , first Right <$> pFindSubExpr c y e
    ]

  case eth of
    Left x' -> return (function s [x',y], attr)
    Right y' -> return (function s [x,y'],attr)

-- | Make a label attribute if the expression matches
pFindSubLabel :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubLabel c s lbl@(Var l) x e = do
  pLog ("pFindSubLabel: " ++ show lbl ++ " " ++ show x ++ " " ++ show e)
  (m,attr) <- pFindSubExpr c x e

  return $
    if isMatched m
      then (m, Label l : attr)
      -- Make sure to not throw away the label if we do not yet want to use it
      else (function s [lbl, m], attr)
pFindSubLabel _ _ _ _ _ = empty -- Shouldn't be possible, but we don't statically enforce it


-- | For division we need to be careful in that there can be many different subexpression of a division.
--
-- For example if we have (5+6)/8, then 5/8,6/8,5+6,8 are all subexpressions. The third case of the choice deals with this.
pFindSubDivision :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubDivision c s x y e = do
  pLog ("pFindSubDivision: " ++ show s ++ "  " ++ show x ++ "  " ++ show y ++ " " ++ show e)
  choice [ do
    -- Go into the left branch
    guardBy optTraverse
    (x2,rw) <- pFindSubExpr c x e
    return (function s [x2,y], rw)
         , do
    -- Go into the right branch
    guardBy optTraverse
    (y2, rw) <- pFindSubExpr c y e
    return (function s [x,y2], rw)
         , do
    -- determine whether the top side of the division is a sum or a product.
    (opS, xs) <- choice'
      [ succeedIf (\xs -> length xs > 1) (plusSymbol, from sumView x)
      , succeedIf (\xs -> length xs > 1) (timesSymbol, snd $ from productView x)
      ]
    choice [ do
      -- For (a * b * c / d)
      -- try [a/d,b/d,c/d]
      guardBy optTraverse
      ((z,rw),zs) <- choiceFor' (selections xs) $ \(x,xs) -> pFindSubExpr c (x/y) e >>= \res -> return (res,xs)
      return (function s (z:zs), rw)
           , do
      -- For (a * b * c / d) and e
      -- Try to find a sub match of (a * b * c) in e * d
      (x2,attr) <- pFindSubAssoc c opS xs (e*y)
      return (function s [x2,y], attr)
      ]  ,
    applyFirstM c $ pMatchAlts (function s [x,y]) e
    ]

-- | Match an expression to one or both of the arguments of some binary expression.
pFindSubBinary :: (Expr -> SEParser Expr) -> Symbol -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubBinary c s x y e = do
  pLog ("pFindSubBinary:" ++ show s ++ " " ++ show x ++ "  "  ++ show y ++ "  " ++ show e)
  choice
    [ do
      guardBy optTraverse
      (x2,rw) <- pFindSubExpr c x e
      return (function s [x2,y], rw)
    , do
      guardBy optTraverse
      (y2, rw) <- pFindSubExpr c y e
      return (function s [x,y2], rw)
    , applyFirstM c $ pMatchAlts (function s [x,y]) e
    ]

-- | For expressions that are associative we need to take special consideration.
--
-- For example if we have 5 + 6 + 7 then possible subexpressions are: 5,6,7,5+6,5+7,6+7.
pFindSubAssoc :: (Expr -> SEParser Expr) -> Symbol -> [Expr] -> Expr -> SEParser (Expr, [Attribute])
pFindSubAssoc c s xs e = do
  pLog ("pFindSubAssoc : " ++ show s ++ " " ++ show xs ++ " | " ++ show e)
  -- Given a list [1 , 2<!>3 , 4]
  -- selections = [(4,[1,2<!>3]) , (2<!>3,[1,4]) , (1,[2<!>3,4])] -- pick each component one time
  -- map second subExprCombs = [(4,[([1,2],[]) , ([1,3],[common mistake])]), ...] -- produce all combinations  of the remaining components for each picked component
  -- map first (:[]) = [([4],[([1,2],[]),([1,3],[common mistake])]), ...]
  -- concatMap uncurry cartProd = [(4,([1,2],[])) , (4,([1,3],[common mistake])), ...]
  let subCombsCartProd = concatMap (uncurry cartProd . first (: []) . second subExprsCombs) $ selections xs
  pLog $ "Assoc tempts: " ++ show subCombsCartProd
  choice
    [ choiceFor subCombsCartProd $ \(y,(ys,attr)) -> do
        pLog ("Assoc attempt: " ++ show y ++ " " ++ show ys ++ " | " ++ show e)
        (ys',attr2) <- pFindSubExpr c (function s ys) e
        return (function s [y,ys'],attr ++ attr2)
    , do
      (e,attr) <- pMatchAlts (function s xs) e
      e' <- c e
      return (e',attr)
    ]

-- | Introduce a subexpression variable and add it to the mapping in the user state
pFindSubLt :: (Expr -> SEParser Expr) -> Expr -> Expr -> Expr -> Expr -> SEParser (Expr, [Attribute])
pFindSubLt c (Var v) x y e = do
  pLog ("pFindSubLt: " ++ show v ++ " " ++ show x ++ " " ++ show y ++ " " ++ show e)
  modify $ \st -> st { usedVariables = M.insert v x (usedVariables st) }
  pFindSubExpr c y e
pFindSubLt _ _ _ _ _ = empty

-- | We use this function to generate all possible expressions and then have each expression be compared to the second expression.
--
-- see `alternativesExpr` to see how these expression are generated.
pMatchAlts :: Expr -> Expr -> SEParser (Expr, [Attribute])
pMatchAlts m e = do
  pLog $ "pMatchAlts: " ++ show m ++ " | " ++ show e
  pLog $ "pMatch alts: " ++ show alts
  choiceFor alts $ \(m1,attrs) -> do
    pLog ("pMatchAlt: " ++ show m1 ++ " | " ++ show e)
    choice'
      [ do
        guardBy optSimplify
        guard (not $ hasSub m1)
        (_, _, z) <- pCompareBySimplify m1 e
        pLog "Simplified equal"
        -- If some subexpression has a label then we wish to generate it now
        attrs' <- pGatherLabels m1
        return (e, attrs' ++ attrs ++ z)
      , do
        pLog "Compare normalized"
        -- guard (hasMagicNat m || SF.hasVar m)
        (_, y) <- pCompareByNormalize m1 e
        pLog "Normalized equal"
        attrs' <- pGatherLabels m1
        return (e, attrs' ++ attrs ++ y)
      ]
  where
    alts = alternativesExpr m

-- | Gather all labels that we can find in the subexpression
pGatherLabels :: Expr -> SEParser [Attribute]
pGatherLabels m = case getFunction m of
  Nothing -> return []
  Just (s,[Var l,y])
    | isLabelSymbol s -> (Label l:) <$> pGatherLabels y
  Just (s,[Var l, e,y])
    | isLabelSymbol s -> do
      e' <- pSubstituteVars e
      (LabelE l e':) <$> pGatherLabels y
  Just (_,xs) -> concat <$> mapM pGatherLabels xs