module Agda.Syntax.Internal
( module Agda.Syntax.Internal
, module Agda.Syntax.Abstract.Name
, module Agda.Utils.Pointer
) where
import Prelude hiding (foldr, mapM)
import Control.Arrow ((***))
import Control.Applicative
import Control.Monad.Identity hiding (mapM)
import Control.Monad.State hiding (mapM)
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 hiding (Arg, Dom, NamedArg, ArgInfo)
import qualified Agda.Syntax.Common as Common
import Agda.Syntax.Literal
import Agda.Syntax.Abstract.Name
import Agda.Utils.Geniplate
import Agda.Utils.Size
import Agda.Utils.Permutation
import Agda.Utils.Pointer
import Agda.Utils.List
import Agda.Utils.Functor
#include "../undefined.h"
import Agda.Utils.Impossible
type Color = Term
type ArgInfo = Common.ArgInfo Color
type Arg a = Common.Arg Color a
type Dom a = Common.Dom Color a
type NamedArg a = Common.NamedArg Color a
type Args = [Arg Term]
type NamedArgs = [NamedArg Term]
data ConHead = ConHead
{ conName :: QName
, conFields :: [QName]
} deriving (Typeable)
instance Eq ConHead where
(==) = (==) `on` conName
instance Ord ConHead where
(<=) = (<=) `on` conName
instance Show ConHead where
show (ConHead c fs) = show c ++ show fs
instance HasRange ConHead where
getRange = getRange . conName
instance SetRange ConHead where
setRange r = mapConName (setRange r)
class LensConName a where
getConName :: a -> QName
setConName :: QName -> a -> a
setConName = mapConName . const
mapConName :: (QName -> QName) -> a -> a
mapConName f a = setConName (f (getConName a)) a
instance LensConName ConHead where
getConName = conName
setConName c con = con { conName = c }
data Term = Var !Int Elims
| Lam ArgInfo (Abs Term)
| Lit Literal
| Def QName Elims
| Con ConHead Args
| Pi (Dom Type) (Abs Type)
| Sort Sort
| Level Level
| MetaV !MetaId Elims
| DontCare Term
| Shared !(Ptr Term)
deriving (Typeable, Show)
data Elim' a = Apply (Arg a) | Proj QName
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Elim = Elim' Term
type Elims = [Elim]
data Abs a = Abs { absName :: String, unAbs :: a }
| NoAbs { absName :: String, unAbs :: a }
deriving (Typeable, Functor, Foldable, Traversable)
data Type' a = El { getSort :: Sort, unEl :: a }
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Type = Type' Term
instance Decoration Type' where
traverseF f (El s a) = El s <$> f a
data Tele a = EmptyTel
| ExtendTel a (Abs (Tele a))
deriving (Typeable, Show, Functor, Foldable, Traversable)
type Telescope = Tele (Dom Type)
mapAbsNamesM :: Applicative m => (String -> m String) -> Tele a -> m (Tele a)
mapAbsNamesM f EmptyTel = pure EmptyTel
mapAbsNamesM f (ExtendTel a (Abs x b)) = ExtendTel a <$> (Abs <$> f x <*> mapAbsNamesM f b)
mapAbsNamesM f (ExtendTel a (NoAbs x b)) = ExtendTel a <$> (NoAbs <$> f x <*> mapAbsNamesM f b)
mapAbsNames :: (String -> String) -> Tele a -> Tele a
mapAbsNames f = runIdentity . mapAbsNamesM (Identity . f)
replaceEmptyName :: String -> Tele a -> Tele a
replaceEmptyName x = mapAbsNames repl
where repl "" = x
repl y = y
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 Elims
| BlockedLevel MetaId Term
| NeutralLevel Term
| UnreducedLevel Term
deriving (Show, Typeable)
newtype MetaId = 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
, namedClausePats :: [NamedArg Pattern]
, clauseBody :: ClauseBody
, clauseType :: Maybe (Arg Type)
}
deriving (Typeable, Show)
clausePats :: Clause -> [Arg Pattern]
clausePats = map (fmap namedThing) . namedClausePats
data ClauseBodyF a = Body a
| Bind (Abs (ClauseBodyF a))
| NoBody
deriving (Typeable, Show, Functor, Foldable, Traversable)
type ClauseBody = ClauseBodyF Term
instance HasRange Clause where
getRange = clauseRange
data Pattern
= VarP String
| DotP Term
| ConP ConHead ConPatternInfo [NamedArg Pattern]
| LitP Literal
| ProjP QName
deriving (Typeable, Show)
namedVarP :: String -> Named RString Pattern
namedVarP "_" = Named Nothing (VarP "_")
namedVarP x = Named (Just $ unranged x) (VarP x)
type ConPatternInfo = Maybe (Bool, Arg Type)
patternVars :: Arg Pattern -> [Arg (Either String Term)]
patternVars (Common.Arg i (VarP x) ) = [Common.Arg i $ Left x]
patternVars (Common.Arg i (DotP t) ) = [Common.Arg i $ Right t]
patternVars (Common.Arg i (ConP _ _ ps)) = List.concat $ map (patternVars . fmap namedThing) ps
patternVars (Common.Arg i (LitP l) ) = []
patternVars (Common.Arg i ProjP{} ) = []
properlyMatching :: Pattern -> Bool
properlyMatching VarP{} = False
properlyMatching DotP{} = False
properlyMatching LitP{} = True
properlyMatching (ConP _ mt ps) = List.or $ isNothing mt
: map (properlyMatching . namedArg) ps
properlyMatching ProjP{} = True
absurdBody :: Abs Term
absurdBody = Abs "()" $ Var 0 []
isAbsurdBody :: Abs Term -> Bool
isAbsurdBody (Abs "()" (Var 0 [])) = True
isAbsurdBody _ = False
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 []
dontCare :: Term -> Term
dontCare v =
case ignoreSharing v of
DontCare{} -> v
_ -> DontCare v
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
]
sgTel :: Dom (String, Type) -> Telescope
sgTel (Common.Dom ai (x, t)) = ExtendTel (Common.Dom ai t) $ Abs x EmptyTel
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__
class Suggest a b where
suggest :: a -> b -> String
instance Suggest String String where
suggest "_" y = y
suggest x _ = x
instance Suggest (Abs a) (Abs b) where
suggest b1 b2 = suggest (absName b1) (absName b2)
unSpine :: Term -> Term
unSpine v =
case hasElims v of
Just (h, es) -> unSpine' h [] es
Nothing -> v
where
unSpine' :: (Elims -> Term) -> Elims -> Elims -> Term
unSpine' h res es =
case es of
[] -> v
e@(Apply a) : es' -> unSpine' h (e : res) es'
Proj f : es' -> unSpine' (Def f) [Apply (defaultArg v)] es'
where v = h $ reverse res
hasElims :: Term -> Maybe (Elims -> Term, Elims)
hasElims v =
case ignoreSharing v of
Var i es -> Just (Var i, es)
Def f es -> Just (Def f, es)
MetaV x es -> Just (MetaV x, es)
Con{} -> Nothing
Lit{} -> Nothing
Lam{} -> Nothing
Pi{} -> Nothing
Sort{} -> Nothing
Level{} -> Nothing
DontCare{} -> Nothing
Shared{} -> __IMPOSSIBLE__
argFromElim :: Elim -> Arg Term
argFromElim (Apply u) = u
argFromElim Proj{} = __IMPOSSIBLE__
isApplyElim :: Elim -> Maybe (Arg Term)
isApplyElim (Apply u) = Just u
isApplyElim Proj{} = Nothing
allApplyElims :: Elims -> Maybe Args
allApplyElims = mapM isApplyElim
splitApplyElims :: Elims -> (Args, Elims)
splitApplyElims (Apply u : es) = (u :) *** id $ splitApplyElims es
splitApplyElims es = ([], es)
class IsProjElim e where
isProjElim :: e -> Maybe QName
instance IsProjElim Elim where
isProjElim (Proj d) = Just d
isProjElim Apply{} = Nothing
dropProjElims :: IsProjElim e => [e] -> [e]
dropProjElims = filter (isNothing . isProjElim)
argsFromElims :: Elims -> Args
argsFromElims = map argFromElim . dropProjElims
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 Sized a => Sized (Elim' a) where
size (Apply v) = size v
size Proj{} = 1
instance KillRange ConHead where
killRange (ConHead c fs) = killRange2 ConHead c fs
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 i f -> killRange1 Lam i 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 Pattern where
killRange p =
case p of
VarP{} -> p
DotP v -> killRange1 DotP v
ConP con info ps -> killRange3 ConP con info ps
LitP l -> killRange1 LitP l
ProjP q -> killRange1 ProjP q
instance KillRange Permutation where
killRange = id
instance KillRange Clause where
killRange (Clause r tel perm ps body t) = killRange6 Clause r tel perm ps body t
instance KillRange a => KillRange (ClauseBodyF a) where
killRange = fmap killRange
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
instance KillRange a => KillRange (Elim' a) where
killRange = fmap killRange
instanceUniverseBiT' [] [t| (([Type], [Clause]), Pattern) |]
instanceUniverseBiT' [] [t| (Args, Pattern) |]
instanceUniverseBiT' [] [t| (Elims, Pattern) |]
instanceUniverseBiT' [] [t| (([Type], [Clause]), Term) |]
instanceUniverseBiT' [] [t| (Args, Term) |]
instanceUniverseBiT' [] [t| (Elims, Term) |]
instanceUniverseBiT' [] [t| ([Term], Term) |]