{-# LANGUAGE CPP, PatternGuards, ImplicitParams #-}

{- Checking for Structural recursion
   Authors: Andreas Abel, Nils Anders Danielsson, Ulf Norell,
              Karl Mehltretter and others
   Created: 2007-05-28
   Source : TypeCheck.Rules.Decl
 -}

module Agda.Termination.TermCheck
    ( termDecls
    , Result, DeBruijnPat
    ) where

import Control.Applicative
import Control.Monad.Error
import Data.List as List
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Maybe as Maybe
import qualified Data.Set as Set
import Data.Set (Set)

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Internal
import qualified Agda.Syntax.Info as Info
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal (Literal(LitString))

import Agda.Termination.CallGraph   as Term
import qualified Agda.Termination.SparseMatrix as Term
import qualified Agda.Termination.Termination  as Term

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce (reduce, normalise, instantiate, instantiateFull)
import Agda.TypeChecking.Records (isRecordConstructor)
import Agda.TypeChecking.Rules.Builtin.Coinduction
import Agda.TypeChecking.Rules.Term (isType_)
import Agda.TypeChecking.Substitute (abstract,raise,substs)
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Signature (isProjection)
import Agda.TypeChecking.Primitive (constructorForm)
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Substitute

import qualified Agda.Interaction.Highlighting.Range as R
import Agda.Interaction.Options

import Agda.Utils.Size
import Agda.Utils.Monad (thread, (<$>), ifM)

#include "../undefined.h"
import Agda.Utils.Impossible

type Calls = Term.CallGraph (Set CallInfo)
type MutualNames = [QName]

-- | The result of termination checking a module.

type Result = [TerminationError]

-- | Termination check a sequence of declarations.
termDecls :: [A.Declaration] -> TCM Result
termDecls ds = fmap concat $ mapM termDecl ds

-- | Termination check a single declaration.
termDecl :: A.Declaration -> TCM Result
termDecl (A.ScopedDecl scope ds) = do
  setScope scope
  termDecls ds
termDecl d = case d of
    A.Axiom {}            -> return []
    A.Field {}            -> return []
    A.Primitive {}        -> return []
    A.Mutual _ ds
      | [A.RecSig{}, A.RecDef _ r _ _ _ rds] <- unscopeDefs ds
                          -> do
        let m = mnameFromList $ qnameToList r
        setScopeFromDefs ds
        termSection m rds
    A.Mutual i ds  -> termMutual i ds
    A.Section _ x _ ds    -> termSection x ds
    A.Apply {}            -> return []
    A.Import {}           -> return []
    A.Pragma {}           -> return []
    A.Open {}             -> return []
        -- open is just an artifact from the concrete syntax
    A.ScopedDecl{}        -> __IMPOSSIBLE__
        -- taken care of above
    -- These should all be wrapped in mutual blocks
    A.FunDef{}  -> __IMPOSSIBLE__
    A.DataSig{} -> __IMPOSSIBLE__
    A.DataDef{} -> __IMPOSSIBLE__
    A.RecSig{}  -> __IMPOSSIBLE__
    A.RecDef{}  -> __IMPOSSIBLE__
  where
    setScopeFromDefs = mapM_ setScopeFromDef
    setScopeFromDef (A.ScopedDecl scope d) = setScope scope
    setScopeFromDef _ = return ()

    unscopeDefs = concatMap unscopeDef

    unscopeDef (A.ScopedDecl _ ds) = unscopeDefs ds
    unscopeDef d = [d]

collectCalls :: (a -> TCM Calls) -> [a] -> TCM Calls
collectCalls f [] = return Term.empty
collectCalls f (a : as) = do c1 <- f a
                             c2 <- collectCalls f as
                             return (c1 `Term.union` c2)

-- | Termination check a bunch of mutually inductive recursive definitions.
termMutual :: Info.DeclInfo -> [A.Declaration] -> TCM Result
termMutual i ds = if names == [] then return [] else
  do -- get list of sets of mutually defined names from the TCM
     -- this includes local and auxiliary functions introduced
     -- during type-checking

     cutoff <- optTerminationDepth <$> pragmaOptions
     let ?cutoff = cutoff

     reportSLn "term.top" 10 $ "Termination checking " ++ show names ++
       " with cutoff=" ++ show cutoff ++ "..."
     mutualBlock <- findMutualBlock (head names)
     let allNames = Set.elems mutualBlock

     -- collect all recursive calls in the block
     let collect use = collectCalls (termDef use allNames) allNames

     -- Get the name of size suc (if sized types are enabled)
     suc <- sizeSuc

     -- The name of sharp (if available).
     sharp <- fmap nameOfSharp <$> coinductionKit

     guardingTypeConstructors <-
       optGuardingTypeConstructors <$> pragmaOptions

     -- first try to termination check ignoring the dot patterns
     let conf = DBPConf
           { useDotPatterns           = False
           , guardingTypeConstructors = guardingTypeConstructors
           , withSizeSuc              = suc
           , sharp                    = sharp
           }
     calls1 <- collect conf{ useDotPatterns = False }
     reportS "term.lex" 20 $ unlines
       [ "Calls (no dot patterns): " ++ show calls1
       ]
     reportSDoc "term.behaviours" 20 $ vcat
       [ text "Recursion behaviours (no dot patterns):"
       , nest 2 $ return $ Term.prettyBehaviour (Term.complete calls1)
       ]
     reportSDoc "term.matrices" 30 $ vcat
       [ text "Call matrices (no dot patterns):"
       , nest 2 $ pretty $ Term.complete calls1
       ]
     r <- do let r = Term.terminates calls1
             case r of
               Right _ -> return r
               Left _  -> do
                 -- Try again, but include the dot patterns this time.
                 calls2 <- collect conf{ useDotPatterns = True }
                 reportS "term.lex" 20 $ unlines
                   [ "Calls (dot patterns): " ++ show calls2
                   ]
                 reportSDoc "term.behaviours" 20 $ vcat
                   [ text "Recursion behaviours (dot patterns):"
                   , nest 2 $ return $
                       Term.prettyBehaviour (Term.complete calls2)
                   ]
                 reportSDoc "term.matrices" 30 $ vcat
                   [ text "Call matrices (dot patterns):"
                   , nest 2 $ pretty $ Term.complete calls2
                   ]
                 return $ Term.terminates calls2
     case r of
       Left calls -> do
         return [TerminationError
                   { termErrFunctions = names
                     -- TODO: This could be changed to allNames.
                   , termErrCalls     = Set.toList calls
                   }
                ]
       Right _ -> do
         reportSLn "term.warn.yes" 2
                     (show (names) ++ " does termination check")
         return []
  where
  getName (A.FunDef i x cs)       = [x]
  getName (A.RecDef _ _ _ _ _ ds) = concatMap getName ds
  getName (A.Mutual _ ds)       = concatMap getName ds
  getName (A.Section _ _ _ ds)  = concatMap getName ds
  getName (A.ScopedDecl _ ds)   = concatMap getName ds
  getName _                     = []

  -- the mutual names mentioned in the abstract syntax
  names = concatMap getName ds

  concat' :: Ord a => [Set a] -> [a]
  concat' = Set.toList . Set.unions

-- | Termination check a module.
termSection :: ModuleName -> [A.Declaration] -> TCM Result
termSection x ds = do
  tel <- lookupSection x
  reportSDoc "term.section" 10 $
    sep [ text "termination checking section"
          , prettyTCM x
          , prettyTCM tel
          ]
  withCurrentModule x $ addCtxTel tel $ termDecls ds


-- | Termination check a definition by pattern matching.
termDef :: DBPConf -> MutualNames -> QName -> TCM Calls
termDef use names name = do
	-- Retrieve definition
        def <- getConstInfo name
        -- returns a TC.Monad.Base.Definition

	reportSDoc "term.def.fun" 5 $
	  sep [ text "termination checking body of" <+> prettyTCM name
	      , nest 2 $ text ":" <+> (prettyTCM $ defType def)
	      ]
        case (theDef def) of
          Function{ funClauses = cls } ->
            collectCalls (termClause use names name) cls
          _ -> return Term.empty


-- | Termination check clauses
{- Precondition: Each clause headed by the same number of patterns

   For instance

   f x (cons y nil) = g x y

   Clause
     [VarP "x", ConP "List.cons" [VarP "y", ConP "List.nil" []]]
     Bind (Abs { absName = "x"
               , absBody = Bind (Abs { absName = "y"
                                     , absBody = Def "g" [ Var 1 []
                                                         , Var 0 []]})})

   Outline:
   - create "De Bruijn pattern"
   - collect recursive calls
   - going under a binder, lift de Bruijn pattern
   - compare arguments of recursive call to pattern

-}

data DeBruijnPat = VarDBP Nat  -- de Bruijn Index
	         | ConDBP QName [DeBruijnPat]
                   -- ^ The name refers to either an ordinary
                   --   constructor or the successor function on sized
                   --   types.
	         | LitDBP Literal

instance PrettyTCM DeBruijnPat where
  prettyTCM (VarDBP i)    = text $ show i
  prettyTCM (ConDBP c ps) = parens (prettyTCM c <+> hsep (map prettyTCM ps))
  prettyTCM (LitDBP l)    = prettyTCM l

unusedVar :: DeBruijnPat
unusedVar = LitDBP (LitString noRange "term.unused.pat.var")

adjIndexDBP :: (Nat -> Nat) -> DeBruijnPat -> DeBruijnPat
adjIndexDBP f (VarDBP i)      = VarDBP (f i)
adjIndexDBP f (ConDBP c args) = ConDBP c (map (adjIndexDBP f) args)
adjIndexDBP f (LitDBP l)      = LitDBP l

{- | liftDeBruijnPat p n

     increases each de Bruijn index in p by n.
     Needed when going under a binder during analysis of a term.
-}

liftDBP :: DeBruijnPat -> DeBruijnPat
liftDBP = adjIndexDBP (1+)

{- | Configuration parameters to termination checker.
-}
data DBPConf = DBPConf { useDotPatterns           :: Bool
                       , guardingTypeConstructors :: Bool
                         -- ^ Do we assume that record and data type
                         --   constructors preserve guardedness?
                       , withSizeSuc              :: Maybe QName
                       , sharp                    :: Maybe QName
                         -- ^ The name of the sharp constructor, if
                         --   any.
                       }

{- | Convert a term (from a dot pattern) to a DeBruijn pattern.
-}

termToDBP :: DBPConf -> Term -> TCM DeBruijnPat
termToDBP conf t
  | not $ useDotPatterns conf = return $ unusedVar
  | otherwise                 = do
    t <- stripProjections =<< constructorForm t
    case t of
      Var i []    -> return $ VarDBP i
      Con c args  -> ConDBP c <$> mapM (termToDBP conf . unArg) args
      Def s [arg]
        | Just s == withSizeSuc conf -> ConDBP s . (:[]) <$> termToDBP conf (unArg arg)
      Lit l       -> return $ LitDBP l
      _   -> return unusedVar

-- | Removes coconstructors from a deBruijn pattern.
stripCoConstructors :: DBPConf -> DeBruijnPat -> TCM DeBruijnPat
stripCoConstructors conf p = case p of
  VarDBP _  -> return p
  LitDBP _ -> return p
  ConDBP c args -> do
    ind <- if withSizeSuc conf == Just c then
             return Inductive
            else
             whatInduction c
    case ind of
      Inductive   -> ConDBP c <$> mapM (stripCoConstructors conf) args
      CoInductive -> return unusedVar

{- | stripBind i p b = Just (i', dbp, b')

  converts a pattern into a de Bruijn pattern

  i  is the next free de Bruijn level before consumption of p
  i' is the next free de Bruijn level after  consumption of p

  if the clause has no body (b = NoBody), Nothing is returned

-}
stripBind :: DBPConf -> Nat -> Pattern -> ClauseBody -> TCM (Maybe (Nat, DeBruijnPat, ClauseBody))
stripBind _ _ _ NoBody            = return Nothing
stripBind conf i (VarP x) (Bind b)   = return $ Just (i - 1, VarDBP i, absBody b)
stripBind conf i (VarP x) (Body b)   = __IMPOSSIBLE__
stripBind conf i (DotP t) (Bind b)   = do
  t <- termToDBP conf t
  return $ Just (i - 1, t, absBody b)
stripBind conf i (DotP _) (Body b)   = __IMPOSSIBLE__
stripBind conf i (LitP l) b          = return $ Just (i, LitDBP l, b)
stripBind conf i (ConP c _ args) b   = do
    r <- stripBinds conf i (map unArg args) b
    case r of
      Just (i', dbps, b') -> return $ Just (i', ConDBP c dbps, b')
      _                   -> return Nothing

{- | stripBinds i ps b = Just (i', dbps, b')

  i  is the next free de Bruijn level before consumption of ps
  i' is the next free de Bruijn level after  consumption of ps
-}
stripBinds :: DBPConf -> Nat -> [Pattern] -> ClauseBody -> TCM (Maybe (Nat, [DeBruijnPat], ClauseBody))
stripBinds use i [] b     = return $ Just (i, [], b)
stripBinds use i (p:ps) b = do
  r1 <- stripBind use i p b
  case r1 of
    Just (i1, dbp, b1) -> do
      r2 <- stripBinds use i1 ps b1
      case r2 of
        Just (i2, dbps, b2) -> return $ Just (i2, dbp:dbps, b2)
        Nothing -> return Nothing
    Nothing -> return Nothing

-- | Extract recursive calls from one clause.
termClause :: DBPConf -> MutualNames -> QName -> Clause -> TCM Calls
termClause use names name (Clause { clauseTel  = tel
                                  , clausePerm = perm
                                  , clausePats = argPats'
                                  , clauseBody = body }) =
  addCtxTel tel $ do
    argPats' <- normalise argPats'
    -- The termination checker doesn't know about reordered telescopes
    let argPats = substs (renamingR perm) argPats'
    dbs <- stripBinds use (nVars - 1) (map unArg argPats) body
    case dbs of
       Nothing -> return Term.empty
       Just (-1, dbpats, Body t) -> do
          dbpats <- mapM (stripCoConstructors use) dbpats
          termTerm use names name dbpats t
          -- note: convert dB levels into dB indices
       Just (n, dbpats, Body t) -> internalError $ "termClause: misscalculated number of vars: guess=" ++ show nVars ++ ", real=" ++ show (nVars - 1 - n)
       Just (n, dbpats, b)  -> internalError $ "termClause: not a Body" -- ++ show b
  where
    nVars = boundVars body
    boundVars (Bind b)   = 1 + boundVars (absBody b)
    boundVars NoBody     = 0
    boundVars (Body _)   = 0

-- | Extract recursive calls from a term.
termTerm :: DBPConf -> MutualNames -> QName -> [DeBruijnPat] -> Term -> TCM Calls
termTerm conf names f pats0 t0 = do
 cutoff <- optTerminationDepth <$> pragmaOptions
 let ?cutoff = cutoff
 do
  reportSDoc "term.check.clause" 6
    (sep [ text "termination checking clause of" <+> prettyTCM f
         , nest 2 $ text "lhs:" <+> hsep (map prettyTCM pats0)
         , nest 2 $ text "rhs:" <+> prettyTCM t0
         ])
  loop pats0 Term.le t0
  where
       Just fInd = toInteger <$> List.elemIndex f names

       -- sorts can contain arb. terms of type Nat,
       -- so look for recursive calls also
       -- in sorts.  Ideally, Sort would not be its own datatype but just
       -- a subgrammar of Term, then we would not need this boilerplate.
       loopSort :: (?cutoff :: Int) => [DeBruijnPat] -> Sort -> TCM Calls
       loopSort pats s = do
         case s of
           Type (Max [])              -> return Term.empty
           Type (Max [ClosedLevel _]) -> return Term.empty
           Type t -> loop pats Term.unknown (Level t)
           Prop   -> return Term.empty
           Inf    -> return Term.empty
           DLub s1 (NoAbs x s2) -> Term.union <$> loopSort pats s1 <*> loopSort pats s2
           DLub s1 (Abs x s2)   -> liftM2 Term.union
             (loopSort pats s1)
             (addCtxString x __IMPOSSIBLE__ $ loopSort (map liftDBP pats) s2)

       loopType :: (?cutoff :: Int) => [DeBruijnPat] -> Order -> Type -> TCM Calls
       loopType pats guarded (El s t) = liftM2 Term.union
         (loopSort pats s)
         (loop pats guarded t)

       loop
         :: (?cutoff :: Int)
         => [DeBruijnPat] -- ^ Parameters of calling function as patterns.
         -> Order         -- ^ Guardedness status of @Term@.
         -> Term          -- ^ Part of function body from which calls are to be extracted.
         -> TCM Calls
       loop pats guarded t = do
         t <- instantiate t          -- instantiate top-level MetaVar
         suc <- sizeSuc

             -- Handles constructor applications.
         let constructor
               :: QName
                  -- ^ Constructor name.
               -> Induction
                  -- ^ Should the constructor be treated as
                  --   inductive or coinductive?
               -> [(Arg Term, Bool)]
                  -- ^ All the arguments, and for every
                  --   argument a boolean which is 'True' iff the
                  --   argument should be viewed as preserving
                  --   guardedness.
               -> TCM Calls
             constructor c ind args = collectCalls loopArg args
               where
               loopArg (arg , preserves) = do
                 loop pats g' (unArg arg)
                 where g' = case (preserves, ind) of
                              (True,  Inductive)   -> guarded
                              (True,  CoInductive) -> Term.lt .*. guarded
                              (False, _)           -> Term.unknown

             -- Handles function applications @g args0@.
             function :: QName -> [Arg Term] -> TCM Calls
             function g args0 = do
               let args1 = map unArg args0
               args2 <- mapM instantiateFull args1

               -- We have to reduce constructors in case they're reexported.
               let reduceCon (Con c vs) = (`apply` vs) <$> reduce (Con c [])  -- make sure we don't reduce the arguments
                   reduceCon t          = return t
               args2 <- mapM reduceCon args2
               args  <- mapM etaContract args2

               -- If the function is a projection, then preserve guardedness
               -- for its principal argument.
               isProj <- isProjection g
               let unguards = repeat Term.unknown
               let guards = maybe unguards -- not a proj. ==> unguarded
                              (\ _ -> guarded : unguards)
                                -- proj. => preserve g. of princ. arg. (counting starts with 1)
                              isProj
               -- collect calls in the arguments of this call
               calls <- collectCalls (uncurry (loop pats)) (zip guards args)
               -- calls <- collectCalls (loop pats Term.unknown) args


               reportSDoc "term.found.call" 20
                       (sep [ text "found call from" <+> prettyTCM f
                            , nest 2 $ text "to" <+> prettyTCM g
                            ])

               -- insert this call into the call list
               case List.elemIndex g names of

                  -- call leads outside the mutual block and can be ignored
                  Nothing   -> return calls

                  -- call is to one of the mutally recursive functions
                  Just gInd' -> do

                     matrix <- compareArgs suc pats args
                     let (nrows, ncols, matrix') = addGuardedness guarded
                            (genericLength args) -- number of rows
                            (genericLength pats) -- number of cols
                            matrix


                     reportSDoc "term.kept.call" 5
                       (sep [ text "kept call from" <+> prettyTCM f
                               <+> hsep (map prettyTCM pats)
                            , nest 2 $ text "to" <+> prettyTCM g <+>
                                        hsep (map (parens . prettyTCM) args)
                            , nest 2 $ text ("call matrix (with guardedness): " ++ show matrix')
                            ])

                     doc <- prettyTCM (Def g args0)
                     return
                       (Term.insert
                         (Term.Call { Term.source = fInd
                                    , Term.target = toInteger gInd'
                                    , Term.cm     = makeCM ncols nrows matrix'
                                    })
                         (Set.singleton
                            (CallInfo { callInfoRange = getRange g
                                      , callInfoCall  = show doc
                                      }))
                         calls)


         case t of

            -- Constructed value.
            Con c args
              | Just c == sharp conf ->
                constructor c CoInductive $ zip args (repeat True)
              | otherwise ->
                constructor c Inductive $ zip args (repeat True)

            Def g args0
              | guardingTypeConstructors conf -> do
                gDef <- theDef <$> getConstInfo g
                case gDef of
                  Datatype {dataArgOccurrences = occs} -> con occs
                  Record   {recArgOccurrences  = occs} -> con occs
                  _                                    -> fun
              | otherwise -> fun
              where
              -- Data or record type constructor.
              con occs =
                constructor g Inductive $   -- guardedness preserving
                -- constructor g CoInductive $ -- guarding! (Andreas, 2011-04-10) -- does not work, might lead to infinite unfolding in eq. checking (Ripley!)
                  zip args0 (map preserves occs ++ repeat False)
                where
                preserves Positive = True
                preserves Negative = False
                preserves Unused   = True

              -- Call to defined function.
              fun = function g args0

            -- Abstraction. Preserves guardedness.
            Lam h (Abs x t) -> addCtxString x (Arg { argHiding    = h
                                                   , argRelevance = __IMPOSSIBLE__
                                                   , unArg        = __IMPOSSIBLE__
                                                   }) $
              loop (map liftDBP pats) guarded t
            Lam h (NoAbs _ t) -> loop pats guarded t

            -- Neutral term. Destroys guardedness.
            Var i args -> collectCalls (loop pats Term.unknown) (map unArg args)

            -- Dependent function space.
            Pi a (Abs x b) ->
               do g1 <- loopType pats Term.unknown (unArg a)
                  g2 <- addCtxString x a $
                        loopType (map liftDBP pats) piArgumentGuarded b
                  return $ g1 `Term.union` g2

            -- Non-dependent function space.
            Pi a (NoAbs _ b) ->
               do g1 <- loopType pats Term.unknown (unArg a)
                  g2 <- loopType pats piArgumentGuarded b
                  return $ g1 `Term.union` g2

            -- Literal.
            Lit l -> return Term.empty

            -- Sort.
            Sort s -> loopSort pats s

	    -- Unsolved metas are not considered termination problems, there
	    -- will be a warning for them anyway.
            MetaV x args -> return Term.empty

            -- Erased and not-yet-erased proof.
            DontCare t -> loop pats guarded t

            -- Level.
            Level l -> loop pats guarded =<< reallyUnLevelView l

         where
         -- Should function and Π type constructors be treated as
         -- preserving guardedness in their right arguments?
         piArgumentGuarded =
           if guardingTypeConstructors conf then
             guarded   -- preserving guardedness
             -- Term.lt      -- guarding! (Andreas, 2011-04-10)  -- SEE ABOVE
            else
             Term.unknown

{- | compareArgs suc pats ts

     compare a list of de Bruijn patterns (=parameters) @pats@
     with a list of arguments @ts@ and create a call maxtrix
     with |ts| rows and |pats| columns.

     If sized types are enabled, @suc@ is the name of the size successor.
 -}
compareArgs ::  (?cutoff :: Int) => Maybe QName -> [DeBruijnPat] -> [Term] -> TCM [[Term.Order]]
compareArgs suc pats ts = mapM (\t -> mapM (compareTerm suc t) pats) ts

-- | 'makeCM' turns the result of 'compareArgs' into a proper call matrix
makeCM :: Index -> Index -> [[Term.Order]] -> Term.CallMatrix
makeCM ncols nrows matrix = Term.CallMatrix $
  Term.fromLists (Term.Size { Term.rows = nrows
                            , Term.cols = ncols
                            })
                 matrix

{- To turn off guardedness, restore this code.
-- | 'addGuardedness' does nothing.
addGuardedness :: Integral n => Order -> n -> n -> [[Term.Order]] -> (n, n, [[Term.Order]])
addGuardedness g nrows ncols m = (nrows, ncols, m)
-}

-- | 'addGuardedness' adds guardedness flag in the upper left corner (0,0).
addGuardedness :: Integral n => Order -> n -> n -> [[Term.Order]] -> (n, n, [[Term.Order]])
addGuardedness g nrows ncols m =
  (nrows + 1, ncols + 1,
   (g : genericReplicate ncols Term.unknown) : map (Term.unknown :) m)

-- | Stripping off a record constructor is not counted as decrease, in
--   contrast to a data constructor.
decreaseFromConstructor :: QName -> TCM Order
decreaseFromConstructor c = do
  isRC <- isRecordConstructor c
  return $ if isRC then Term.le else Term.lt

increaseFromConstructor :: (?cutoff :: Int) => QName -> TCM Order
increaseFromConstructor c = do
  isRC <- isRecordConstructor c
  return $ if isRC then Term.le else Term.decr (-1)

{-
increaseFromConstructor c = negateOrder <$> decreaseFromConstructor c
  where negateOrder (Decr k) = Decr (- k)
        negateOrder _ = __IMPOSSIBLE__
-}

-- | Compute the sub patterns of a 'DeBruijnPat'.
subPatterns :: DeBruijnPat -> [DeBruijnPat]
subPatterns p = case p of
  VarDBP _    -> []
  ConDBP c ps -> ps ++ concatMap subPatterns ps
  LitDBP _    -> []

compareTerm :: (?cutoff :: Int) => Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm suc t p = do
  t <- stripAllProjections t
  compareTerm' suc t p

{-
compareTerm t p = Term.supremum $ compareTerm' t p : map cmp (subPatterns p)
  where
    cmp p' = (Term..*.) Term.lt (compareTerm' t p')
-}

-- | Remove projections until a term is no longer a projection.
--   Also, remove 'DontCare's.
stripProjections :: Term -> TCM Term
stripProjections (DontCare t) = stripProjections t
stripProjections t@(Def qn ts@(~(r : _))) = do
  isProj <- isProjection qn
  case isProj of
    Just{} | not (null ts) -> stripProjections $ unArg r
    _ -> return t
stripProjections t = return t

-- | Remove all projections from an algebraic term (not going under binders).
class StripAllProjections a where
  stripAllProjections :: a -> TCM a

instance StripAllProjections a => StripAllProjections (Arg a) where
  stripAllProjections (Arg h r a) = Arg h r <$> stripAllProjections a

instance StripAllProjections a => StripAllProjections [a] where
  stripAllProjections = mapM stripAllProjections

instance StripAllProjections Term where
  stripAllProjections t = do
    t <- stripProjections t
    case t of
      Con c ts -> Con c <$> stripAllProjections ts
      Def d ts -> Def d <$> stripAllProjections ts
      _ -> return t

{-
-- | Remove all projections from an algebraic term (not going under binders).
stripAllProjections :: Term -> TCM Term
stripAllProjections t = do
  t <- stripProjections t
  case t of
    Con c ts -> Con c <$> mapM stripAllProjections ts
    Def d ts -> Def d <$> mapM stripAllProjections ts
    _ -> return t
-}

-- | compareTerm t dbpat
--   Precondition: top meta variable resolved
compareTerm' :: (?cutoff :: Int) => Maybe QName -> Term -> DeBruijnPat -> TCM Term.Order
compareTerm' _ (Var i _)      p = compareVar i p
compareTerm' suc (DontCare t) p = compareTerm' suc t p
compareTerm' _ (Lit l)    (LitDBP l')
  | l == l'   = return Term.le
  | otherwise = return Term.unknown
compareTerm' suc (Lit l) p = do
  t <- constructorForm (Lit l)
  case t of
    Lit _ -> return Term.unknown
    _     -> compareTerm' suc t p
-- Andreas, 2011-04-19 give subterm priority over matrix order
compareTerm' _ t@Con{} (ConDBP c ps)
  | any (isSubTerm t) ps = decreaseFromConstructor c
compareTerm' suc (Con c ts) (ConDBP c' ps)
  | c == c' = compareConArgs suc ts ps
compareTerm' suc (Def s ts) (ConDBP s' ps)
  | s == s' && Just s == suc = compareConArgs suc ts ps
-- new cases for counting constructors / projections
-- register also increase
compareTerm' suc (Def s ts) p | Just s == suc = do
    os <- mapM (\ t -> compareTerm' suc (unArg t) p) ts
    return $ decr (-1) .*. infimum os
{- Andreas 2011-07-07 Projections are now being removed in a preprocess
-- projections are size preserving
compareTerm' suc (Def qn ts) p = do
    isProj <- isProjection qn
    case isProj of
      -- strip off projection (n is the number of the record argument, counting starts with 1)
      Just n | length ts >= n && n >= 1 ->
        compareTerm' suc (unArg (ts !! (n - 1))) p
      -- not a projection or underapplied:
      _ -> return Term.unknown
-}
compareTerm' suc (Con c ts) p = do
    os <- mapM (\ t -> compareTerm' suc (unArg t) p) ts
    oc <- increaseFromConstructor c
    return $ if (null os) then Term.unknown else oc .*. infimum os
compareTerm' suc t p | isSubTerm t p = return Term.le
compareTerm' _ _ _ = return Term.unknown

-- TODO: isSubTerm should compute a size difference (Term.Order)
isSubTerm :: Term -> DeBruijnPat -> Bool
isSubTerm t p = equal t p || properSubTerm t p
  where
    equal (Con c ts) (ConDBP c' ps) =
      and $ (c == c')
          : (length ts == length ps)
          : zipWith equal (map unArg ts) ps
    equal (Var i []) (VarDBP j) = i == j
    equal (Lit l) (LitDBP l') = l == l'
    equal _ _ = False

    properSubTerm t (ConDBP _ ps) = any (isSubTerm t) ps
    properSubTerm _ _ = False

compareConArgs :: (?cutoff :: Int) => Maybe QName -> Args -> [DeBruijnPat] -> TCM Term.Order
compareConArgs suc ts ps =
  -- we may assume |ps| >= |ts|, otherwise c ps would be of functional type
  -- which is impossible
      case (length ts, length ps) of
        (0,0) -> return Term.le        -- c <= c
        (0,1) -> return Term.unknown   -- c not<= c x
        (1,0) -> __IMPOSSIBLE__
        (1,1) -> compareTerm' suc (unArg (head ts)) (head ps)
        (_,_) -> do -- build "call matrix"
          m <- mapM (\t -> mapM (compareTerm' suc (unArg t)) ps) ts
          let m2 = makeCM (genericLength ps) (genericLength ts) m
          return $ Term.orderMat (Term.mat m2)
{-
--    if null ts then Term.Le
--               else Term.infimum (zipWith compareTerm' (map unArg ts) ps)
     foldl (Term..*.) Term.Le (zipWith compareTerm' (map unArg ts) ps)
       -- corresponds to taking the size, not the height
       -- allows examples like (x, y) < (Succ x, y)
-}

compareVar :: (?cutoff :: Int) => Nat -> DeBruijnPat -> TCM Term.Order
compareVar i (VarDBP j)    = return $ if i == j then Term.le else Term.unknown
compareVar i (LitDBP _)    = return $ Term.unknown
compareVar i (ConDBP c ps) = do
  os <- mapM (compareVar i) ps
  let o = Term.supremum os
  oc <- decreaseFromConstructor c
  return $ (Term..*.) oc o