{-# LANGUAGE CPP, DeriveDataTypeable, GeneralizedNewtypeDeriving #-}

module Agda.Syntax.Internal
    ( module Agda.Syntax.Internal
    , module Agda.Syntax.Abstract.Name
    ) where

import Prelude hiding (foldr)
import Control.Applicative
import Data.Generics
import Data.Foldable
import Data.Traversable
import Data.Function

import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name

import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Permutation

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

-- | Raw values.
--
--   @Def@ is used for both defined and undefined constants.
--   Assume there is a type declaration and a definition for
--     every constant, even if the definition is an empty
--     list of clauses.
--
data Term = Var Nat Args
	  | Lam Hiding (Abs Term)   -- ^ terms are beta normal
	  | Lit Literal
	  | Def QName Args
	  | Con QName Args
	  | Pi (Arg Type) (Abs Type)
	  | Fun (Arg Type) Type
	  | Sort Sort
	  | MetaV MetaId Args
  deriving (Typeable, Data, Eq, Ord, Show)

data Type = El Sort Term
  deriving (Typeable, Data, Eq, Ord, Show)

data Sort = Type Term   -- A term of type Nat
	  | Prop
	  | Lub Sort Sort
	  | Suc Sort
	  | MetaS MetaId Args
          | Inf
          | DLub Sort (Abs Sort)
            -- ^ if the free variable occurs in the second sort
            --   the whole thing should reduce to Inf, otherwise
            --   it's the normal Lub
  deriving (Typeable, Data, Eq, Ord, Show)

-- | Something where a meta variable may block reduction.
data Blocked t = Blocked MetaId t
               | NotBlocked t
    deriving (Typeable, Data, Eq, Ord)

instance Show t => Show (Blocked t) where
  showsPrec p (Blocked m x) = showParen (p > 0) $
    showString "Blocked " . shows m . showString " " . showsPrec 10 x
  showsPrec p (NotBlocked x) = showsPrec p x

instance Functor Blocked where
  fmap f (Blocked m t) = Blocked m $ f t
  fmap f (NotBlocked t) = NotBlocked $ f t

instance Foldable Blocked where
  foldr f z (Blocked _ x) = f x z
  foldr f z (NotBlocked x) = f x z

instance Traversable Blocked where
  traverse f (Blocked m t)  = Blocked m <$> f t
  traverse f (NotBlocked t) = NotBlocked <$> f t

instance Applicative Blocked where
  pure = notBlocked
  Blocked x f  <*> e = Blocked x $ f (ignoreBlocking e)
  NotBlocked f <*> e = f <$> e

instance Sized Term where
  size v = case v of
    Var _ vs   -> 1 + Prelude.sum (map size vs)
    Def _ vs   -> 1 + Prelude.sum (map size vs)
    Con _ vs   -> 1 + Prelude.sum (map size vs)
    MetaV _ vs -> 1 + Prelude.sum (map size vs)
    Lam _ f    -> 1 + size f
    Lit _      -> 1
    Pi a b     -> 1 + size a + size b
    Fun a b    -> 1 + size a + size b
    Sort s     -> 1

instance Sized Type where
  size = size . unEl

instance KillRange Term where
  killRange v = case v of
    Var i vs   -> killRange1 (Var i) vs
    Def c vs   -> killRange2 Def c vs
    Con c vs   -> killRange2 Con c vs
    MetaV m vs -> killRange1 (MetaV m) vs
    Lam h f    -> killRange2 Lam h f
    Lit l      -> killRange1 Lit l
    Pi a b     -> killRange2 Pi a b
    Fun a b    -> killRange2 Fun a b
    Sort s     -> killRange1 Sort s

instance KillRange Type where
  killRange (El s v) = killRange2 El s v

instance KillRange Sort where
  killRange s = case s of
    Prop       -> Prop
    Inf        -> Inf
    Type a     -> killRange1 Type a
    Suc s      -> killRange1 Suc s
    Lub s1 s2  -> killRange2 Lub s1 s2
    DLub s1 s2 -> killRange2 DLub s1 s2
    MetaS x as -> killRange1 (MetaS x) as

instance KillRange Telescope where
  killRange EmptyTel = EmptyTel
  killRange (ExtendTel a tel) = killRange2 ExtendTel a tel

instance KillRange a => KillRange (Blocked a) where
  killRange = fmap killRange

instance KillRange a => KillRange (Abs a) where
  killRange = fmap killRange

-- | Type of argument lists.
--
type Args = [Arg Term]

-- | Sequence of types. An argument of the first type is bound in later types
--   and so on.
data Telescope = EmptyTel
	       | ExtendTel (Arg Type) (Abs Telescope)
  deriving (Typeable, Data, Show, Eq, Ord)

instance Sized Telescope where
  size  EmptyTel	 = 0
  size (ExtendTel _ tel) = 1 + size tel

-- | The body has (at least) one free variable.
data Abs a = Abs { absName :: String
		 , absBody :: a
		 }
  deriving (Typeable, Data)

instance Eq a => Eq (Abs a) where
  (==) = (==) `on` absBody

instance Ord a => Ord (Abs a) where
  compare = compare `on` absBody

instance Show a => Show (Abs a) where
  showsPrec p (Abs x a) = showParen (p > 0) $
    showString "Abs " . shows x . showString " " . showsPrec 10 a

instance Functor Abs where
  fmap f (Abs x t) = Abs x $ f t

instance Foldable Abs where
  foldr f z (Abs _ t) = f t z

instance Traversable Abs where
  traverse f (Abs x t) = Abs x <$> f t

instance Sized a => Sized (Abs a) where
  size = size . absBody

telFromList :: [Arg (String, Type)] -> Telescope
telFromList = foldr (\(Arg h (x, a)) -> ExtendTel (Arg h a) . Abs x) EmptyTel

telToList :: Telescope -> [Arg (String, Type)]
telToList EmptyTel = []
telToList (ExtendTel arg (Abs x tel)) = fmap ((,) x) arg : telToList tel

--
-- Definitions
--

-- | A clause is a list of patterns and the clause body should @Bind@ or
-- @NoBind@ in the order the variables occur in the patterns. The @NoBind@
-- constructor is an optimisation to avoid substituting for variables that
-- aren't used.
--
--  The telescope contains the types of the pattern variables and the
--  permutation is how to get from the order the variables occur in the
--  patterns to the order they occur in the telescope.  For the purpose of the
--  permutation dot patterns counts as variables.
--  TODO: change this!
data Clause = Clause
    { clauseRange     :: Range
    , clauseTel       :: Telescope
    , clausePerm      :: Permutation
    , clausePats      :: [Arg Pattern]
    , clauseBody      :: ClauseBody
    }
  deriving (Typeable, Data, Show)
data ClauseBody = Body Term
		| Bind (Abs ClauseBody)
		| NoBind ClauseBody
		| NoBody    -- for absurd clauses
  deriving (Typeable, Data, Show)

instance HasRange Clause where
  getRange = clauseRange

-- | Patterns are variables, constructors, or wildcards.
--   @QName@ is used in @ConP@ rather than @Name@ since
--     a constructor might come from a particular namespace.
--     This also meshes well with the fact that values (i.e.
--     the arguments we are matching with) use @QName@.
--
data Pattern = VarP String  -- name suggestion
             | DotP Term
	     | ConP QName [Arg Pattern]
	     | LitP Literal
  deriving (Typeable, Data, Show)

newtype MetaId = MetaId Nat
    deriving (Eq, Ord, Num, Real, Enum, Integral, Typeable, Data)

instance Show MetaId where
    show (MetaId n) = "_" ++ show n

-- | Doesn't do any reduction.
arity :: Type -> Nat
arity t =
    case unEl t of
	Pi  _ (Abs _ b) -> 1 + arity b
	Fun _	     b	-> 1 + arity b
	_		-> 0

-- | Suggest a name for the first argument of a function of the given type.
argName :: Type -> String
argName = argN . unEl
    where
	argN (Pi _ b)  = "." ++ absName b
	argN (Fun _ _) = ".x"
	argN _	  = __IMPOSSIBLE__


---------------------------------------------------------------------------
-- * Views
---------------------------------------------------------------------------

data FunView
	= FunV (Arg Type) Term	-- ^ second arg is the entire type ('Pi' or 'Fun').
	| NoFunV Term

funView :: Term -> FunView
funView t@(Pi  arg _) = FunV arg t
funView t@(Fun arg _) = FunV arg t
funView t	      = NoFunV t

---------------------------------------------------------------------------
-- * Smart constructors
---------------------------------------------------------------------------

blockingMeta :: Blocked t -> Maybe MetaId
blockingMeta (Blocked m _) = Just m
blockingMeta (NotBlocked _) = Nothing

blocked :: MetaId -> a -> Blocked a
blocked x = Blocked x

notBlocked :: a -> Blocked a
notBlocked = NotBlocked

ignoreBlocking :: Blocked a -> a
ignoreBlocking (Blocked _ x) = x
ignoreBlocking (NotBlocked x) = x

set0   = set 0
set n  = sort $ mkType n
prop   = sort Prop
sort s = El (sSuc s) $ Sort s

mkType n = Type $ Lit $ LitLevel noRange n

teleLam :: Telescope -> Term -> Term
teleLam  EmptyTel	  t = t
teleLam (ExtendTel u tel) t = Lam (argHiding u) $ flip teleLam t <$> tel

getSort :: Type -> Sort
getSort (El s _) = s

unEl :: Type -> Term
unEl (El _ t) = t

-- | Get the next higher sort.
sSuc :: Sort -> Sort
sSuc Prop                      = mkType 1
sSuc (Type (Lit (LitLevel _ n))) = mkType (n + 1)
sSuc Inf                       = Inf
sSuc s                         = Suc s

sLub :: Sort -> Sort -> Sort
sLub (Type (Lit (LitLevel _ 0))) Prop                      = Prop   -- (x:A) -> B prop if A type0, B prop [x:A]
sLub (Type (Lit (LitLevel _ n))) Prop                      = mkType n
sLub Prop (Type (Lit (LitLevel _ n)))                      = mkType n
sLub (Type (Lit (LitLevel _ n))) (Type (Lit (LitLevel _ m))) = mkType $ max n m
sLub (Suc a) (Suc b) = Suc (sLub a b)
sLub (Type (Lit (LitLevel _ n))) (Suc a)
  | n > 0     = sSuc (mkType (n - 1) `sLub` a)
  | otherwise = Suc a
sLub (Suc a) (Type (Lit (LitLevel _ n)))
  | n > 0     = sSuc (a `sLub` mkType (n - 1))
  | otherwise = Suc a
sLub Inf _ = Inf
sLub _ Inf = Inf
sLub s1 s2
    | s1 == s2	= s1
    | otherwise	= Lub s1 s2

impossibleTerm :: String -> Int -> Term
impossibleTerm file line = Lit $ LitString noRange $ unlines
  [ "An internal error has occurred. Please report this as a bug."
  , "Location of the error: " ++ file ++ ":" ++ show line
  ]