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
data Term = Var Nat Args
| Lam Hiding (Abs Term)
| 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
| Prop
| Lub Sort Sort
| Suc Sort
| MetaS MetaId Args
| Inf
| DLub Sort (Abs Sort)
deriving (Typeable, Data, Eq, Ord, Show)
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 Args = [Arg Term]
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
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
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
deriving (Typeable, Data, Show)
instance HasRange Clause where
getRange = clauseRange
data Pattern = VarP String
| 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
arity :: Type -> Nat
arity t =
case unEl t of
Pi _ (Abs _ b) -> 1 + arity b
Fun _ b -> 1 + arity b
_ -> 0
argName :: Type -> String
argName = argN . unEl
where
argN (Pi _ b) = "." ++ absName b
argN (Fun _ _) = ".x"
argN _ = __IMPOSSIBLE__
data FunView
= FunV (Arg Type) Term
| NoFunV Term
funView :: Term -> FunView
funView t@(Pi arg _) = FunV arg t
funView t@(Fun arg _) = FunV arg t
funView t = NoFunV t
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
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
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
]