{-# OPTIONS_GHC -Wunused-imports #-}
module Mikan.Syntax.Internal.Clause
  ( -- * Clauses
    Clause(..)
  , clausePats
  , clausePerm
  , clauseArgs
  , clauseElims

  -- * Recursivity marks
  , ClauseRecursive(..)
  , decideRecursive, couldBeRecursive
  )
  where

import Prelude hiding (null)

import Control.DeepSeq

import GHC.Generics (Generic)

import Mikan.Syntax.Internal.Telescope
import Mikan.Syntax.Internal.Pattern
import Mikan.Syntax.Internal.Term
import Mikan.Syntax.Common.Pretty
import Mikan.Syntax.Position
import Mikan.Syntax.Common

import Mikan.Utils.Permutation
import Mikan.Utils.Null
import Mikan.Utils.List

---------------------------------------------------------------------------
-- * Definitions
---------------------------------------------------------------------------

-- | Does the clause body contain calls to any of the mutually recursive functions?
data ClauseRecursive
  = YesRecursive
      -- ^ Definitely a call to a mutually recursive function.
  | NotRecursive
      -- ^ Definitely no call to a mutually recursive function.
  | MaybeRecursive
      -- ^ Don't know because the analysis has not run yet.
  deriving (ClauseRecursive
ClauseRecursive -> ClauseRecursive -> Bounded ClauseRecursive
forall a. a -> a -> Bounded a
$cminBound :: ClauseRecursive
minBound :: ClauseRecursive
$cmaxBound :: ClauseRecursive
maxBound :: ClauseRecursive
Bounded, Int -> ClauseRecursive
ClauseRecursive -> Int
ClauseRecursive -> [ClauseRecursive]
ClauseRecursive -> ClauseRecursive
ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
(ClauseRecursive -> ClauseRecursive)
-> (ClauseRecursive -> ClauseRecursive)
-> (Int -> ClauseRecursive)
-> (ClauseRecursive -> Int)
-> (ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> (ClauseRecursive
    -> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive])
-> Enum ClauseRecursive
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: ClauseRecursive -> ClauseRecursive
succ :: ClauseRecursive -> ClauseRecursive
$cpred :: ClauseRecursive -> ClauseRecursive
pred :: ClauseRecursive -> ClauseRecursive
$ctoEnum :: Int -> ClauseRecursive
toEnum :: Int -> ClauseRecursive
$cfromEnum :: ClauseRecursive -> Int
fromEnum :: ClauseRecursive -> Int
$cenumFrom :: ClauseRecursive -> [ClauseRecursive]
enumFrom :: ClauseRecursive -> [ClauseRecursive]
$cenumFromThen :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromThen :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
$cenumFromTo :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromTo :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
$cenumFromThenTo :: ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
enumFromThenTo :: ClauseRecursive
-> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive]
Enum, ClauseRecursive -> ClauseRecursive -> Bool
(ClauseRecursive -> ClauseRecursive -> Bool)
-> (ClauseRecursive -> ClauseRecursive -> Bool)
-> Eq ClauseRecursive
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ClauseRecursive -> ClauseRecursive -> Bool
== :: ClauseRecursive -> ClauseRecursive -> Bool
$c/= :: ClauseRecursive -> ClauseRecursive -> Bool
/= :: ClauseRecursive -> ClauseRecursive -> Bool
Eq, (forall x. ClauseRecursive -> Rep ClauseRecursive x)
-> (forall x. Rep ClauseRecursive x -> ClauseRecursive)
-> Generic ClauseRecursive
forall x. Rep ClauseRecursive x -> ClauseRecursive
forall x. ClauseRecursive -> Rep ClauseRecursive x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ClauseRecursive -> Rep ClauseRecursive x
from :: forall x. ClauseRecursive -> Rep ClauseRecursive x
$cto :: forall x. Rep ClauseRecursive x -> ClauseRecursive
to :: forall x. Rep ClauseRecursive x -> ClauseRecursive
Generic, Int -> ClauseRecursive -> ShowS
[ClauseRecursive] -> ShowS
ClauseRecursive -> String
(Int -> ClauseRecursive -> ShowS)
-> (ClauseRecursive -> String)
-> ([ClauseRecursive] -> ShowS)
-> Show ClauseRecursive
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ClauseRecursive -> ShowS
showsPrec :: Int -> ClauseRecursive -> ShowS
$cshow :: ClauseRecursive -> String
show :: ClauseRecursive -> String
$cshowList :: [ClauseRecursive] -> ShowS
showList :: [ClauseRecursive] -> ShowS
Show)

instance Null ClauseRecursive where
  empty :: ClauseRecursive
empty = ClauseRecursive
MaybeRecursive

instance Pretty ClauseRecursive where
  pretty :: ClauseRecursive -> Doc
pretty = \case
    ClauseRecursive
YesRecursive   -> Doc
"+Rec"
    ClauseRecursive
NotRecursive   -> Doc
"-Rec"
    ClauseRecursive
MaybeRecursive -> Doc
"?Rec"

instance NFData ClauseRecursive

instance KillRange ClauseRecursive where
  killRange :: ClauseRecursive -> ClauseRecursive
killRange = ClauseRecursive -> ClauseRecursive
forall a. a -> a
id


couldBeRecursive :: ClauseRecursive -> Bool
couldBeRecursive :: ClauseRecursive -> Bool
couldBeRecursive = \case
  ClauseRecursive
YesRecursive   -> Bool
True
  ClauseRecursive
NotRecursive   -> Bool
False
  ClauseRecursive
MaybeRecursive -> Bool
True

decideRecursive :: Bool -> ClauseRecursive
decideRecursive :: Bool -> ClauseRecursive
decideRecursive = \case
  Bool
True  -> ClauseRecursive
YesRecursive
  Bool
False -> ClauseRecursive
NotRecursive

-- | A clause is a list of patterns and the clause body.
--
--  The telescope contains the types of the pattern variables and the
--  de Bruijn indices say how to get from the order the variables occur in
--  the patterns to the order they occur in the telescope. The body
--  binds the variables in the order they appear in the telescope.
--
--  @clauseTel ~ permute clausePerm (patternVars namedClausePats)@
--
--  Terms in dot patterns are valid in the clause telescope.
--
--  For the purpose of the permutation and the body dot patterns count
--  as variables. TODO: Change this!
data Clause = Clause
    { Clause -> Range
clauseLHSRange    :: Range
    , Clause -> Range
clauseFullRange   :: Range
    , Clause -> Telescope
clauseTel         :: Telescope
      -- ^ @Δ@: The types of the pattern variables in dependency order.
    , Clause -> NAPs
namedClausePats   :: NAPs
      -- ^ @Δ ⊢ ps@.  The de Bruijn indices refer to @Δ@.
    , Clause -> Maybe Term
clauseBody        :: Maybe Term
      -- ^ @Just v@ with @Δ ⊢ v@ for a regular clause, or @Nothing@ for an
      --   absurd one.
    , Clause -> Maybe (Arg Type)
clauseType        :: Maybe (Arg Type)
      -- ^ @Δ ⊢ t@.  The type of the rhs under @clauseTel@.
      --   Used, e.g., by @TermCheck@.
      --   The @ArgInfo@ remembers whether we are under a copattern for an
      --   instance/tactic field, for example.
    , Clause -> Catchall
clauseCatchall    :: Catchall
      -- ^ Clause has been labelled as CATCHALL.
    , Clause -> ClauseRecursive
clauseRecursive   :: ClauseRecursive
      -- ^ @clauseBody@ contains recursive calls? Computed by termination checker.
    , Clause -> Maybe Bool
clauseUnreachable :: Maybe Bool
      -- ^ Clause has been labelled as unreachable by the coverage checker.
      --   @Nothing@ means coverage checker has not run yet (clause may be unreachable).
      --   @Just False@ means clause is not unreachable.
      --   @Just True@ means clause is unreachable.
    , Clause -> ExpandedEllipsis
clauseEllipsis    :: ExpandedEllipsis
      -- ^ Was this clause created by expansion of an ellipsis?
    , Clause -> Maybe ModuleName
clauseWhereModule :: Maybe ModuleName
      -- ^ Keeps track of the module name associate with the clause's where clause.
    }
  deriving (Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Clause -> ShowS
showsPrec :: Int -> Clause -> ShowS
$cshow :: Clause -> String
show :: Clause -> String
$cshowList :: [Clause] -> ShowS
showList :: [Clause] -> ShowS
Show, (forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Clause -> Rep Clause x
from :: forall x. Clause -> Rep Clause x
$cto :: forall x. Rep Clause x -> Clause
to :: forall x. Rep Clause x -> Clause
Generic)

instance HasRange Clause where
  getRange :: Clause -> Range
getRange = Clause -> Range
clauseLHSRange

-- | A 'null' clause is one with no patterns and no rhs.
--   Should not exist in practice.
instance Null Clause where
  empty :: Clause
empty = Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
forall a. Null a => a
empty Range
forall a. Null a => a
empty Telescope
forall a. Null a => a
empty NAPs
forall a. Null a => a
empty Maybe Term
forall a. Null a => a
empty Maybe (Arg Type)
forall a. Null a => a
empty Catchall
forall a. Null a => a
empty ClauseRecursive
forall a. Null a => a
empty Maybe Bool
forall a. Null a => a
empty ExpandedEllipsis
forall a. Null a => a
empty Maybe ModuleName
forall a. Null a => a
empty
  null :: Clause -> Bool
null (Clause Range
_ Range
_ Telescope
tel NAPs
pats Maybe Term
body Maybe (Arg Type)
_ Catchall
_ ClauseRecursive
_ Maybe Bool
_ ExpandedEllipsis
_ Maybe ModuleName
wm)
    =  Telescope -> Bool
forall a. Null a => a -> Bool
null Telescope
tel
    Bool -> Bool -> Bool
&& NAPs -> Bool
forall a. Null a => a -> Bool
null NAPs
pats
    Bool -> Bool -> Bool
&& Maybe Term -> Bool
forall a. Null a => a -> Bool
null Maybe Term
body
    Bool -> Bool -> Bool
&& Maybe ModuleName -> Bool
forall a. Null a => a -> Bool
null Maybe ModuleName
wm


instance KillRange Clause where
  killRange :: KillRangeT Clause
killRange (Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm) =
    (Range
 -> Range
 -> Telescope
 -> NAPs
 -> Maybe Term
 -> Maybe (Arg Type)
 -> Catchall
 -> ClauseRecursive
 -> Maybe Bool
 -> ExpandedEllipsis
 -> Maybe ModuleName
 -> Clause)
-> Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
forall t (b :: Bool).
(KILLRANGE t b, IsBase t ~ b, All KillRange (Domains t)) =>
t -> t
killRangeN Range
-> Range
-> Telescope
-> NAPs
-> Maybe Term
-> Maybe (Arg Type)
-> Catchall
-> ClauseRecursive
-> Maybe Bool
-> ExpandedEllipsis
-> Maybe ModuleName
-> Clause
Clause Range
rl Range
rf Telescope
tel NAPs
ps Maybe Term
body Maybe (Arg Type)
t Catchall
catchall ClauseRecursive
recursive Maybe Bool
unreachable ExpandedEllipsis
ell Maybe ModuleName
wm

instance Pretty Clause where
  pretty :: Clause -> Doc
pretty Clause{clauseTel :: Clause -> Telescope
clauseTel = Telescope
tel, namedClausePats :: Clause -> NAPs
namedClausePats = NAPs
ps, clauseBody :: Clause -> Maybe Term
clauseBody = Maybe Term
b, clauseType :: Clause -> Maybe (Arg Type)
clauseType = Maybe (Arg Type)
t} =
    [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Telescope -> Doc
forall a. Pretty a => a -> Doc
pretty Telescope
tel Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"|-"
        , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ((Arg (Named_ DeBruijnPattern) -> Doc) -> NAPs -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map' (Int -> Arg (Named_ DeBruijnPattern) -> Doc
forall a. Pretty a => Int -> a -> Doc
prettyPrec Int
10) NAPs
ps) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"="
                       , Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Maybe Term -> Maybe (Arg Type) -> Doc
forall {a} {a}. (Pretty a, Pretty a) => Maybe a -> Maybe a -> Doc
pBody Maybe Term
b Maybe (Arg Type)
t ] ]
    where
      pBody :: Maybe a -> Maybe a -> Doc
pBody Maybe a
Nothing Maybe a
_ = Doc
"(absurd)"
      pBody (Just a
b) Maybe a
Nothing  = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
b
      pBody (Just a
b) (Just a
t) = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
b Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
":", Int -> Doc -> Doc
forall a. Int -> Doc a -> Doc a
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
t ]

instance NFData Clause

-- * Tools for clauses

clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePats = (Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern)
-> NAPs -> [Arg DeBruijnPattern]
forall a b. (a -> b) -> [a] -> [b]
map' ((Named_ DeBruijnPattern -> DeBruijnPattern)
-> Arg (Named_ DeBruijnPattern) -> Arg DeBruijnPattern
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named_ DeBruijnPattern -> DeBruijnPattern
forall name a. Named name a -> a
namedThing) (NAPs -> [Arg DeBruijnPattern])
-> (Clause -> NAPs) -> Clause -> [Arg DeBruijnPattern]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats

-- | Translate the clause patterns to an elimination spine
--   with free variables bound by the clause telescope.
clauseElims :: Clause -> Elims
clauseElims :: Clause -> Elims
clauseElims Clause
cl = NAPs -> Elims
patternsToElims (NAPs -> Elims) -> NAPs -> Elims
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
namedClausePats Clause
cl

-- | Translate the clause patterns to terms with free variables bound by the
--   clause telescope.
--
--   Precondition: no projection patterns.
clauseArgs :: Clause -> Args
clauseArgs :: Clause -> Args
clauseArgs Clause
cl = Elims -> Args
forall a. [Elim' a] -> [Arg a]
mustAllApplyElims (Elims -> Args) -> Elims -> Args
forall a b. (a -> b) -> a -> b
$ Clause -> Elims
clauseElims Clause
cl

-- | Computes the permutation from the clause telescope
--   to the pattern variables.
--
--   Use as @fromMaybe __IMPOSSIBLE__ . clausePerm@ to crash
--   in a controlled way if a de Bruijn index is out of scope here.
clausePerm :: Clause -> Maybe Permutation
clausePerm :: Clause -> Maybe Permutation
clausePerm = NAPs -> Maybe Permutation
dbPatPerm (NAPs -> Maybe Permutation)
-> (Clause -> NAPs) -> Clause -> Maybe Permutation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats

instance HasDefP Clause where
  hasDefP :: Clause -> Bool
hasDefP = NAPs -> Bool
forall a. HasDefP a => a -> Bool
hasDefP (NAPs -> Bool) -> (Clause -> NAPs) -> Clause -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> NAPs
namedClausePats