module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Abstract.Name
, module Agda.Utils.Pointer
) where
import Prelude hiding (foldr)
import Control.Applicative
import Control.Parallel
import Data.Typeable (Typeable)
import Data.Foldable
import Data.Traversable
import Data.Function
import Data.Maybe
import qualified Data.List as List
import Agda.Syntax.Position
import Agda.Syntax.Common
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
import Agda.Utils.Geniplate
import Agda.Utils.Monad
import Agda.Utils.Size
import Agda.Utils.Permutation
import Agda.Utils.Pointer
#include "../undefined.h"
import Agda.Utils.Impossible
data Term = Var !Int Args
| Lam Hiding (Abs Term)
| Lit Literal
| Def QName Args
| Con QName Args
| Pi (Dom Type) (Abs Type)
| Sort Sort
| Level Level
| MetaV !MetaId Args
| DontCare Term
| Shared !(Ptr Term)
deriving (Typeable, Show)
type Args = [Arg Term]
data Elim = Apply (Arg Term) | Proj QName
deriving (Show)
data Abs a = Abs { absName :: String, unAbs :: a }
| NoAbs { absName :: String, unAbs :: a }
deriving (Typeable, Functor, Foldable, Traversable)
data Type = El { getSort :: Sort, unEl :: Term }
deriving (Typeable, Show)
data Tele a = EmptyTel
| ExtendTel a (Abs (Tele a))
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Telescope = Tele (Dom Type)
data Sort = Type Level
| Prop
| Inf
| DLub Sort (Abs Sort)
deriving (Typeable, Show)
newtype Level = Max [PlusLevel]
deriving (Show, Typeable)
data PlusLevel = ClosedLevel Integer
| Plus Integer LevelAtom
deriving (Show, Typeable)
data LevelAtom = MetaLevel MetaId Args
| BlockedLevel MetaId Term
| NeutralLevel Term
| UnreducedLevel Term
deriving (Show, Typeable)
newtype MetaId = MetaId Nat
deriving (Eq, Ord, Num, Real, Enum, Integral, Typeable)
data Blocked t = Blocked MetaId t
| NotBlocked t
deriving (Typeable, Eq, Ord, Functor, Foldable, Traversable)
instance Applicative Blocked where
pure = notBlocked
Blocked x f <*> e = Blocked x $ f (ignoreBlocking e)
NotBlocked f <*> e = f <$> e
data Clause = Clause
{ clauseRange :: Range
, clauseTel :: Telescope
, clausePerm :: Permutation
, clausePats :: [Arg Pattern]
, clauseBody :: ClauseBody
}
deriving (Typeable, Show)
data ClauseBody = Body Term
| Bind (Abs ClauseBody)
| NoBody
deriving (Typeable, Show)
instance HasRange Clause where
getRange = clauseRange
data Pattern = VarP String
| DotP Term
| ConP QName (Maybe (Arg Type)) [Arg Pattern]
| LitP Literal
deriving (Typeable, Show)
patternVars :: Arg Pattern -> [Arg (Either String Term)]
patternVars (Arg h r (VarP x) ) = [Arg h r $ Left x]
patternVars (Arg h r (DotP t) ) = [Arg h r $ Right t]
patternVars (Arg h r (ConP _ _ ps)) = List.concat $ map patternVars ps
patternVars (Arg h r (LitP l) ) = []
properlyMatching :: Pattern -> Bool
properlyMatching VarP{} = False
properlyMatching DotP{} = False
properlyMatching LitP{} = True
properlyMatching (ConP _ mt ps) = List.or $ isNothing mt
: map (properlyMatching . unArg) ps
ignoreSharing :: Term -> Term
ignoreSharing v = v
ignoreSharingType :: Type -> Type
ignoreSharingType v = v
shared :: Term -> Term
shared v = v
sharedType :: Type -> Type
sharedType v = v
updateSharedFM :: (Monad m, Applicative m, Traversable f) => (Term -> m (f Term)) -> Term -> m (f Term)
updateSharedFM f v0@(Shared p) = do
fv <- f (derefPtr p)
flip traverse fv $ \v ->
case derefPtr (setPtr v p) of
Var _ [] -> return v
_ -> compressPointerChain v0 `pseq` return v0
updateSharedFM f v = f v
updateSharedM :: Monad m => (Term -> m Term) -> Term -> m Term
updateSharedM f v0@(Shared p) = do
v <- f (derefPtr p)
case derefPtr (setPtr v p) of
Var _ [] -> return v
_ -> compressPointerChain v0 `pseq` return v0
updateSharedM f v = f v
updateShared :: (Term -> Term) -> Term -> Term
updateShared f v0@(Shared p) =
case derefPtr (setPtr (f $ derefPtr p) p) of
v@(Var _ []) -> v
_ -> compressPointerChain v0 `pseq` v0
updateShared f v = f v
pointerChain :: Term -> [Ptr Term]
pointerChain (Shared p) = p : pointerChain (derefPtr p)
pointerChain _ = []
compressPointerChain :: Term -> Term
compressPointerChain v =
case reverse $ pointerChain v of
p:_:ps@(_:_) -> setPointers (Shared p) ps
_ -> v
where
setPointers _ [] = v
setPointers u (p : ps) =
setPtr u p `seq` setPointers u ps
var :: Nat -> Term
var i = Var i []
typeDontCare :: Type
typeDontCare = El Prop (Sort Prop)
topSort :: Type
topSort = El Inf (Sort Inf)
set0 = set 0
set n = sort $ mkType n
prop = sort Prop
sort s = El (sSuc s) $ Sort s
varSort n = Type $ Max [Plus 0 $ NeutralLevel $ Var n []]
sSuc :: Sort -> Sort
sSuc Prop = mkType 1
sSuc Inf = Inf
sSuc (DLub a b) = DLub (sSuc a) (fmap sSuc b)
sSuc (Type l) = Type $ levelSuc l
levelSuc (Max []) = Max [ClosedLevel 1]
levelSuc (Max as) = Max $ map inc as
where inc (ClosedLevel n) = ClosedLevel (n + 1)
inc (Plus n l) = Plus (n + 1) l
mkType n = Type $ Max [ClosedLevel n | n > 0]
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
]
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
stripDontCare :: Term -> Term
stripDontCare v = case ignoreSharing v of
DontCare v -> v
_ -> v
arity :: Type -> Nat
arity t = case ignoreSharing $ unEl t of
Pi _ b -> 1 + arity (unAbs b)
_ -> 0
argName :: Type -> String
argName = argN . ignoreSharing . unEl
where
argN (Pi _ b) = "." ++ absName b
argN _ = __IMPOSSIBLE__
instance Show a => Show (Abs a) where
showsPrec p (Abs x a) = showParen (p > 0) $
showString "Abs " . shows x . showString " " . showsPrec 10 a
showsPrec p (NoAbs x a) = showParen (p > 0) $
showString "NoAbs " . shows x . showString " " . showsPrec 10 a
instance Show MetaId where
show (MetaId n) = "_" ++ show n
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 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)
Level l -> size l
Lam _ f -> 1 + size f
Lit _ -> 1
Pi a b -> 1 + size a + size b
Sort s -> 1
DontCare mv -> size mv
Shared p -> size (derefPtr p)
instance Sized Type where
size = size . unEl
instance Sized Level where
size (Max as) = 1 + Prelude.sum (map size as)
instance Sized PlusLevel where
size (ClosedLevel _) = 1
size (Plus _ a) = size a
instance Sized LevelAtom where
size (MetaLevel _ vs) = 1 + Prelude.sum (map size vs)
size (BlockedLevel _ v) = size v
size (NeutralLevel v) = size v
size (UnreducedLevel v) = size v
instance Sized (Tele a) where
size EmptyTel = 0
size (ExtendTel _ tel) = 1 + size tel
instance Sized a => Sized (Abs a) where
size = size . unAbs
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
Level l -> killRange1 Level l
Pi a b -> killRange2 Pi a b
Sort s -> killRange1 Sort s
DontCare mv -> killRange1 DontCare mv
Shared p -> Shared $ updatePtr killRange p
instance KillRange Level where
killRange (Max as) = killRange1 Max as
instance KillRange PlusLevel where
killRange l@ClosedLevel{} = l
killRange (Plus n l) = killRange1 (Plus n) l
instance KillRange LevelAtom where
killRange (MetaLevel n as) = killRange1 (MetaLevel n) as
killRange (BlockedLevel m v) = killRange1 (BlockedLevel m) v
killRange (NeutralLevel v) = killRange1 NeutralLevel v
killRange (UnreducedLevel v) = killRange1 UnreducedLevel v
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
DLub s1 s2 -> killRange2 DLub s1 s2
instance KillRange a => KillRange (Tele a) where
killRange = fmap killRange
instance KillRange a => KillRange (Blocked a) where
killRange = fmap killRange
instance KillRange a => KillRange (Abs a) where
killRange = fmap killRange
instanceUniverseBiT' [] [t| (([Type], [Clause]), Pattern) |]
instanceUniverseBiT' [] [t| (Args, Pattern) |]
instanceUniverseBiT' [] [t| (([Type], [Clause]), Term) |]
instanceUniverseBiT' [] [t| (Args, Term) |]
instanceUniverseBiT' [] [t| ([Term], Term) |]