{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PatternSynonyms #-}
module Disco.AST.Typed
(
ATerm
, pattern ATVar
, pattern ATPrim
, pattern ATLet
, pattern ATUnit
, pattern ATBool
, pattern ATNat
, pattern ATRat
, pattern ATChar
, pattern ATString
, pattern ATAbs
, pattern ATApp
, pattern ATTup
, pattern ATCase
, pattern ATChain
, pattern ATTyOp
, pattern ATContainer
, pattern ATContainerComp
, pattern ATList
, pattern ATListComp
, pattern ATTest
, ALink
, pattern ATLink
, Container(..)
, ABinding
, ABranch
, AGuard
, pattern AGBool
, pattern AGPat
, pattern AGLet
, AQual
, pattern AQBind
, pattern AQGuard
, APattern
, pattern APVar
, pattern APWild
, pattern APUnit
, pattern APBool
, pattern APTup
, pattern APInj
, pattern APNat
, pattern APChar
, pattern APString
, pattern APCons
, pattern APList
, pattern APAdd
, pattern APMul
, pattern APSub
, pattern APNeg
, pattern APFrac
, pattern ABinding
, varsBound
, getType
, setType
, substQT
, AProperty
)
where
import Unbound.Generics.LocallyNameless
import Unbound.Generics.LocallyNameless.Unsafe
import Control.Arrow ((***))
import Data.Coerce (coerce)
import Data.Data (Data)
import Data.Void
import Control.Lens.Plated (transform)
import Disco.AST.Generic
import Disco.AST.Surface
import Disco.Names
import Disco.Pretty
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
data TY
deriving Typeable TY
DataType
Typeable TY
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TY)
-> (TY -> Constr)
-> (TY -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TY))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TY))
-> ((forall b. Data b => b -> b) -> TY -> TY)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r)
-> (forall u. (forall d. Data d => d -> u) -> TY -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TY -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TY -> m TY)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TY -> m TY)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TY -> m TY)
-> Data TY
TY -> DataType
TY -> Constr
(forall b. Data b => b -> b) -> TY -> TY
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TY
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> TY -> u
forall u. (forall d. Data d => d -> u) -> TY -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TY -> m TY
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TY -> m TY
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TY
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TY)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TY)
$tTY :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> TY -> m TY
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TY -> m TY
gmapMp :: (forall d. Data d => d -> m d) -> TY -> m TY
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> TY -> m TY
gmapM :: (forall d. Data d => d -> m d) -> TY -> m TY
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> TY -> m TY
gmapQi :: Int -> (forall d. Data d => d -> u) -> TY -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TY -> u
gmapQ :: (forall d. Data d => d -> u) -> TY -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TY -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TY -> r
gmapT :: (forall b. Data b => b -> b) -> TY -> TY
$cgmapT :: (forall b. Data b => b -> b) -> TY -> TY
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TY)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TY)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c TY)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c TY)
dataTypeOf :: TY -> DataType
$cdataTypeOf :: TY -> DataType
toConstr :: TY -> Constr
$ctoConstr :: TY -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TY
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c TY
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY
$cp1Data :: Typeable TY
Data
type AProperty = Property_ TY
type ATerm = Term_ TY
type instance X_Binder TY = [APattern]
type instance X_TVar TY = Void
type instance X_TPrim TY = Type
type instance X_TLet TY = Type
type instance X_TUnit TY = ()
type instance X_TBool TY = Type
type instance X_TNat TY = Type
type instance X_TRat TY = ()
type instance X_TChar TY = ()
type instance X_TString TY = ()
type instance X_TAbs TY = Type
type instance X_TApp TY = Type
type instance X_TCase TY = Type
type instance X_TChain TY = Type
type instance X_TTyOp TY = Type
type instance X_TContainer TY = Type
type instance X_TContainerComp TY = Type
type instance X_TAscr TY = Void
type instance X_TTup TY = Type
type instance X_TParens TY = Void
type instance X_Term TY = Either ([(String, Type, Name ATerm)], ATerm) (Type, QName ATerm)
pattern ATVar :: Type -> QName ATerm -> ATerm
pattern $bATVar :: Type -> QName ATerm -> ATerm
$mATVar :: forall r. ATerm -> (Type -> QName ATerm -> r) -> (Void# -> r) -> r
ATVar ty qname = XTerm_ (Right (ty, qname))
pattern ATPrim :: Type -> Prim -> ATerm
pattern $bATPrim :: Type -> Prim -> ATerm
$mATPrim :: forall r. ATerm -> (Type -> Prim -> r) -> (Void# -> r) -> r
ATPrim ty name = TPrim_ ty name
pattern ATLet :: Type -> Bind (Telescope ABinding) ATerm -> ATerm
pattern $bATLet :: Type -> Bind (Telescope ABinding) ATerm -> ATerm
$mATLet :: forall r.
ATerm
-> (Type -> Bind (Telescope ABinding) ATerm -> r)
-> (Void# -> r)
-> r
ATLet ty bind = TLet_ ty bind
pattern ATUnit :: ATerm
pattern $bATUnit :: ATerm
$mATUnit :: forall r. ATerm -> (Void# -> r) -> (Void# -> r) -> r
ATUnit = TUnit_ ()
pattern ATBool :: Type -> Bool -> ATerm
pattern $bATBool :: Type -> Bool -> ATerm
$mATBool :: forall r. ATerm -> (Type -> Bool -> r) -> (Void# -> r) -> r
ATBool ty bool = TBool_ ty bool
pattern ATNat :: Type -> Integer -> ATerm
pattern $bATNat :: Type -> Integer -> ATerm
$mATNat :: forall r. ATerm -> (Type -> Integer -> r) -> (Void# -> r) -> r
ATNat ty int = TNat_ ty int
pattern ATRat :: Rational -> ATerm
pattern $bATRat :: Rational -> ATerm
$mATRat :: forall r. ATerm -> (Rational -> r) -> (Void# -> r) -> r
ATRat rat = TRat_ () rat
pattern ATChar :: Char -> ATerm
pattern $bATChar :: Char -> ATerm
$mATChar :: forall r. ATerm -> (Char -> r) -> (Void# -> r) -> r
ATChar c = TChar_ () c
pattern ATString :: String -> ATerm
pattern $bATString :: String -> ATerm
$mATString :: forall r. ATerm -> (String -> r) -> (Void# -> r) -> r
ATString s = TString_ () s
pattern ATAbs :: Quantifier -> Type -> Bind [APattern] ATerm -> ATerm
pattern $bATAbs :: Quantifier -> Type -> Bind [APattern] ATerm -> ATerm
$mATAbs :: forall r.
ATerm
-> (Quantifier -> Type -> Bind [APattern] ATerm -> r)
-> (Void# -> r)
-> r
ATAbs q ty bind = TAbs_ q ty bind
pattern ATApp :: Type -> ATerm -> ATerm -> ATerm
pattern $bATApp :: Type -> ATerm -> ATerm -> ATerm
$mATApp :: forall r.
ATerm -> (Type -> ATerm -> ATerm -> r) -> (Void# -> r) -> r
ATApp ty term1 term2 = TApp_ ty term1 term2
pattern ATTup :: Type -> [ATerm] -> ATerm
pattern $bATTup :: Type -> [ATerm] -> ATerm
$mATTup :: forall r. ATerm -> (Type -> [ATerm] -> r) -> (Void# -> r) -> r
ATTup ty termlist = TTup_ ty termlist
pattern ATCase :: Type -> [ABranch] -> ATerm
pattern $bATCase :: Type -> [ABranch] -> ATerm
$mATCase :: forall r. ATerm -> (Type -> [ABranch] -> r) -> (Void# -> r) -> r
ATCase ty branch = TCase_ ty branch
pattern ATChain :: Type -> ATerm -> [ALink] -> ATerm
pattern $bATChain :: Type -> ATerm -> [ALink] -> ATerm
$mATChain :: forall r.
ATerm -> (Type -> ATerm -> [ALink] -> r) -> (Void# -> r) -> r
ATChain ty term linklist = TChain_ ty term linklist
pattern ATTyOp :: Type -> TyOp -> Type -> ATerm
pattern $bATTyOp :: Type -> TyOp -> Type -> ATerm
$mATTyOp :: forall r. ATerm -> (Type -> TyOp -> Type -> r) -> (Void# -> r) -> r
ATTyOp ty1 tyop ty2 = TTyOp_ ty1 tyop ty2
pattern ATContainer :: Type -> Container -> [(ATerm, Maybe ATerm)] -> Maybe (Ellipsis ATerm) -> ATerm
pattern $bATContainer :: Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
$mATContainer :: forall r.
ATerm
-> (Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> r)
-> (Void# -> r)
-> r
ATContainer ty c tl mets = TContainer_ ty c tl mets
pattern ATContainerComp :: Type -> Container -> Bind (Telescope AQual) ATerm -> ATerm
pattern $bATContainerComp :: Type -> Container -> Bind (Telescope AQual) ATerm -> ATerm
$mATContainerComp :: forall r.
ATerm
-> (Type -> Container -> Bind (Telescope AQual) ATerm -> r)
-> (Void# -> r)
-> r
ATContainerComp ty c b = TContainerComp_ ty c b
pattern ATTest :: [(String, Type, Name ATerm)] -> ATerm -> ATerm
pattern $bATTest :: [(String, Type, Name ATerm)] -> ATerm -> ATerm
$mATTest :: forall r.
ATerm
-> ([(String, Type, Name ATerm)] -> ATerm -> r)
-> (Void# -> r)
-> r
ATTest ns t = XTerm_ (Left (ns, t))
{-# COMPLETE ATVar, ATPrim, ATLet, ATUnit, ATBool, ATNat, ATRat, ATChar,
ATString, ATAbs, ATApp, ATTup, ATCase, ATChain, ATTyOp,
ATContainer, ATContainerComp, ATTest #-}
pattern ATList :: Type -> [ATerm] -> Maybe (Ellipsis ATerm) -> ATerm
pattern $bATList :: Type -> [ATerm] -> Maybe (Ellipsis ATerm) -> ATerm
$mATList :: forall r.
ATerm
-> (Type -> [ATerm] -> Maybe (Ellipsis ATerm) -> r)
-> (Void# -> r)
-> r
ATList t xs e <- ATContainer t ListContainer (map fst -> xs) e
where
ATList Type
t [ATerm]
xs Maybe (Ellipsis ATerm)
e = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer Type
t Container
ListContainer ((ATerm -> (ATerm, Maybe ATerm))
-> [ATerm] -> [(ATerm, Maybe ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (,Maybe ATerm
forall a. Maybe a
Nothing) [ATerm]
xs) Maybe (Ellipsis ATerm)
e
pattern ATListComp :: Type -> Bind (Telescope AQual) ATerm -> ATerm
pattern $bATListComp :: Type -> Bind (Telescope AQual) ATerm -> ATerm
$mATListComp :: forall r.
ATerm
-> (Type -> Bind (Telescope AQual) ATerm -> r) -> (Void# -> r) -> r
ATListComp t b = ATContainerComp t ListContainer b
type ALink = Link_ TY
type instance X_TLink TY = ()
pattern ATLink :: BOp -> ATerm -> ALink
pattern $bATLink :: BOp -> ATerm -> ALink
$mATLink :: forall r. ALink -> (BOp -> ATerm -> r) -> (Void# -> r) -> r
ATLink bop term = TLink_ () bop term
{-# COMPLETE ATLink #-}
type AQual = Qual_ TY
type instance X_QBind TY = ()
type instance X_QGuard TY = ()
pattern AQBind :: Name ATerm -> Embed ATerm -> AQual
pattern $bAQBind :: Name ATerm -> Embed ATerm -> AQual
$mAQBind :: forall r.
AQual -> (Name ATerm -> Embed ATerm -> r) -> (Void# -> r) -> r
AQBind namet embedt = QBind_ () namet embedt
pattern AQGuard :: Embed ATerm -> AQual
pattern $bAQGuard :: Embed ATerm -> AQual
$mAQGuard :: forall r. AQual -> (Embed ATerm -> r) -> (Void# -> r) -> r
AQGuard embedt = QGuard_ () embedt
{-# COMPLETE AQBind, AQGuard #-}
type ABinding = Binding_ TY
pattern ABinding :: Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> ABinding
pattern $bABinding :: Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> ABinding
$mABinding :: forall r.
ABinding
-> (Maybe (Embed PolyType) -> Name ATerm -> Embed ATerm -> r)
-> (Void# -> r)
-> r
ABinding m b n = Binding_ m b n
{-# COMPLETE ABinding #-}
type ABranch = Bind (Telescope AGuard) ATerm
type AGuard = Guard_ TY
type instance X_GBool TY = ()
type instance X_GPat TY = ()
type instance X_GLet TY = ()
pattern AGBool :: Embed ATerm -> AGuard
pattern $bAGBool :: Embed ATerm -> AGuard
$mAGBool :: forall r. AGuard -> (Embed ATerm -> r) -> (Void# -> r) -> r
AGBool embedt = GBool_ () embedt
pattern AGPat :: Embed ATerm -> APattern -> AGuard
pattern $bAGPat :: Embed ATerm -> APattern -> AGuard
$mAGPat :: forall r.
AGuard -> (Embed ATerm -> APattern -> r) -> (Void# -> r) -> r
AGPat embedt pat = GPat_ () embedt pat
pattern AGLet :: ABinding -> AGuard
pattern $bAGLet :: ABinding -> AGuard
$mAGLet :: forall r. AGuard -> (ABinding -> r) -> (Void# -> r) -> r
AGLet b = GLet_ () b
{-# COMPLETE AGBool, AGPat, AGLet #-}
type APattern = Pattern_ TY
type instance X_PVar TY = Embed Type
type instance X_PWild TY = Embed Type
type instance X_PAscr TY = Void
type instance X_PUnit TY = ()
type instance X_PBool TY = ()
type instance X_PChar TY = ()
type instance X_PString TY = ()
type instance X_PTup TY = Embed Type
type instance X_PInj TY = Embed Type
type instance X_PNat TY = Embed Type
type instance X_PCons TY = Embed Type
type instance X_PList TY = Embed Type
type instance X_PAdd TY = Embed Type
type instance X_PMul TY = Embed Type
type instance X_PSub TY = Embed Type
type instance X_PNeg TY = Embed Type
type instance X_PFrac TY = Embed Type
type instance X_Pattern TY = ()
pattern APVar :: Type -> Name ATerm -> APattern
pattern $bAPVar :: Type -> Name ATerm -> APattern
$mAPVar :: forall r.
APattern -> (Type -> Name ATerm -> r) -> (Void# -> r) -> r
APVar ty name <- PVar_ (unembed -> ty) name
where
APVar Type
ty Name ATerm
name = X_PVar TY -> Name ATerm -> APattern
forall e. X_PVar e -> Name (Term_ e) -> Pattern_ e
PVar_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) Name ATerm
name
pattern APWild :: Type -> APattern
pattern $bAPWild :: Type -> APattern
$mAPWild :: forall r. APattern -> (Type -> r) -> (Void# -> r) -> r
APWild ty <- PWild_ (unembed -> ty)
where
APWild Type
ty = X_PWild TY -> APattern
forall e. X_PWild e -> Pattern_ e
PWild_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty)
pattern APUnit :: APattern
pattern $bAPUnit :: APattern
$mAPUnit :: forall r. APattern -> (Void# -> r) -> (Void# -> r) -> r
APUnit = PUnit_ ()
pattern APBool :: Bool -> APattern
pattern $bAPBool :: Bool -> APattern
$mAPBool :: forall r. APattern -> (Bool -> r) -> (Void# -> r) -> r
APBool b = PBool_ () b
pattern APChar :: Char -> APattern
pattern $bAPChar :: Char -> APattern
$mAPChar :: forall r. APattern -> (Char -> r) -> (Void# -> r) -> r
APChar c = PChar_ () c
pattern APString :: String -> APattern
pattern $bAPString :: String -> APattern
$mAPString :: forall r. APattern -> (String -> r) -> (Void# -> r) -> r
APString s = PString_ () s
pattern APTup :: Type -> [APattern] -> APattern
pattern $bAPTup :: Type -> [APattern] -> APattern
$mAPTup :: forall r.
APattern -> (Type -> [APattern] -> r) -> (Void# -> r) -> r
APTup ty lp <- PTup_ (unembed -> ty) lp
where
APTup Type
ty [APattern]
lp = X_PTup TY -> [APattern] -> APattern
forall e. X_PTup e -> [Pattern_ e] -> Pattern_ e
PTup_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) [APattern]
lp
pattern APInj :: Type -> Side -> APattern -> APattern
pattern $bAPInj :: Type -> Side -> APattern -> APattern
$mAPInj :: forall r.
APattern -> (Type -> Side -> APattern -> r) -> (Void# -> r) -> r
APInj ty s p <- PInj_ (unembed -> ty) s p
where
APInj Type
ty Side
s APattern
p = X_PInj TY -> Side -> APattern -> APattern
forall e. X_PInj e -> Side -> Pattern_ e -> Pattern_ e
PInj_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) Side
s APattern
p
pattern APNat :: Type -> Integer -> APattern
pattern $bAPNat :: Type -> Integer -> APattern
$mAPNat :: forall r. APattern -> (Type -> Integer -> r) -> (Void# -> r) -> r
APNat ty n <- PNat_ (unembed -> ty) n
where
APNat Type
ty Integer
n = X_PNat TY -> Integer -> APattern
forall e. X_PNat e -> Integer -> Pattern_ e
PNat_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) Integer
n
pattern APCons :: Type -> APattern -> APattern -> APattern
pattern $bAPCons :: Type -> APattern -> APattern -> APattern
$mAPCons :: forall r.
APattern
-> (Type -> APattern -> APattern -> r) -> (Void# -> r) -> r
APCons ty p1 p2 <- PCons_ (unembed -> ty) p1 p2
where
APCons Type
ty APattern
p1 APattern
p2 = X_PCons TY -> APattern -> APattern -> APattern
forall e. X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PCons_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) APattern
p1 APattern
p2
pattern APList :: Type -> [APattern] -> APattern
pattern $bAPList :: Type -> [APattern] -> APattern
$mAPList :: forall r.
APattern -> (Type -> [APattern] -> r) -> (Void# -> r) -> r
APList ty lp <- PList_ (unembed -> ty) lp
where
APList Type
ty [APattern]
lp = X_PList TY -> [APattern] -> APattern
forall e. X_PList e -> [Pattern_ e] -> Pattern_ e
PList_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) [APattern]
lp
pattern APAdd :: Type -> Side -> APattern -> ATerm -> APattern
pattern $bAPAdd :: Type -> Side -> APattern -> ATerm -> APattern
$mAPAdd :: forall r.
APattern
-> (Type -> Side -> APattern -> ATerm -> r) -> (Void# -> r) -> r
APAdd ty s p t <- PAdd_ (unembed -> ty) s p t
where
APAdd Type
ty Side
s APattern
p ATerm
t = X_PAdd TY -> Side -> APattern -> ATerm -> APattern
forall e. X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PAdd_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) Side
s APattern
p ATerm
t
pattern APMul :: Type -> Side -> APattern -> ATerm -> APattern
pattern $bAPMul :: Type -> Side -> APattern -> ATerm -> APattern
$mAPMul :: forall r.
APattern
-> (Type -> Side -> APattern -> ATerm -> r) -> (Void# -> r) -> r
APMul ty s p t <- PMul_ (unembed -> ty) s p t
where
APMul Type
ty Side
s APattern
p ATerm
t = X_PMul TY -> Side -> APattern -> ATerm -> APattern
forall e. X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PMul_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) Side
s APattern
p ATerm
t
pattern APSub :: Type -> APattern -> ATerm -> APattern
pattern $bAPSub :: Type -> APattern -> ATerm -> APattern
$mAPSub :: forall r.
APattern -> (Type -> APattern -> ATerm -> r) -> (Void# -> r) -> r
APSub ty p t <- PSub_ (unembed -> ty) p t
where
APSub Type
ty APattern
p ATerm
t = X_PSub TY -> APattern -> ATerm -> APattern
forall e. X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e
PSub_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) APattern
p ATerm
t
pattern APNeg :: Type -> APattern -> APattern
pattern $bAPNeg :: Type -> APattern -> APattern
$mAPNeg :: forall r. APattern -> (Type -> APattern -> r) -> (Void# -> r) -> r
APNeg ty p <- PNeg_ (unembed -> ty) p
where
APNeg Type
ty APattern
p = X_PNeg TY -> APattern -> APattern
forall e. X_PNeg e -> Pattern_ e -> Pattern_ e
PNeg_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) APattern
p
pattern APFrac :: Type -> APattern -> APattern -> APattern
pattern $bAPFrac :: Type -> APattern -> APattern -> APattern
$mAPFrac :: forall r.
APattern
-> (Type -> APattern -> APattern -> r) -> (Void# -> r) -> r
APFrac ty p1 p2 <- PFrac_ (unembed -> ty) p1 p2
where
APFrac Type
ty APattern
p1 APattern
p2 = X_PFrac TY -> APattern -> APattern -> APattern
forall e. X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PFrac_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty) APattern
p1 APattern
p2
{-# COMPLETE APVar, APWild, APUnit, APBool, APChar, APString,
APTup, APInj, APNat, APCons, APList, APAdd, APMul, APSub, APNeg, APFrac #-}
varsBound :: APattern -> [(Name ATerm, Type)]
varsBound :: APattern -> [(Name ATerm, Type)]
varsBound (APVar Type
ty Name ATerm
n) = [(Name ATerm
n, Type
ty)]
varsBound (APWild Type
_) = []
varsBound APattern
APUnit = []
varsBound (APBool Bool
_) = []
varsBound (APChar Char
_) = []
varsBound (APString String
_) = []
varsBound (APTup Type
_ [APattern]
ps) = APattern -> [(Name ATerm, Type)]
varsBound (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [APattern]
ps
varsBound (APInj Type
_ Side
_ APattern
p) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p
varsBound (APNat Type
_ Integer
_) = []
varsBound (APCons Type
_ APattern
p APattern
q) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p [(Name ATerm, Type)]
-> [(Name ATerm, Type)] -> [(Name ATerm, Type)]
forall a. [a] -> [a] -> [a]
++ APattern -> [(Name ATerm, Type)]
varsBound APattern
q
varsBound (APList Type
_ [APattern]
ps) = APattern -> [(Name ATerm, Type)]
varsBound (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< [APattern]
ps
varsBound (APAdd Type
_ Side
_ APattern
p ATerm
_) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p
varsBound (APMul Type
_ Side
_ APattern
p ATerm
_) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p
varsBound (APSub Type
_ APattern
p ATerm
_) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p
varsBound (APNeg Type
_ APattern
p) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p
varsBound (APFrac Type
_ APattern
p APattern
q) = APattern -> [(Name ATerm, Type)]
varsBound APattern
p [(Name ATerm, Type)]
-> [(Name ATerm, Type)] -> [(Name ATerm, Type)]
forall a. [a] -> [a] -> [a]
++ APattern -> [(Name ATerm, Type)]
varsBound APattern
q
instance HasType ATerm where
getType :: ATerm -> Type
getType (ATVar Type
ty QName ATerm
_) = Type
ty
getType (ATPrim Type
ty Prim
_) = Type
ty
getType ATerm
ATUnit = Type
TyUnit
getType (ATBool Type
ty Bool
_) = Type
ty
getType (ATNat Type
ty Integer
_) = Type
ty
getType (ATRat Rational
_) = Type
TyF
getType (ATChar Char
_) = Type
TyC
getType (ATString String
_) = Type -> Type
TyList Type
TyC
getType (ATAbs Quantifier
_ Type
ty Bind [APattern] ATerm
_) = Type
ty
getType (ATApp Type
ty ATerm
_ ATerm
_) = Type
ty
getType (ATTup Type
ty [ATerm]
_) = Type
ty
getType (ATTyOp Type
ty TyOp
_ Type
_) = Type
ty
getType (ATChain Type
ty ATerm
_ [ALink]
_) = Type
ty
getType (ATContainer Type
ty Container
_ [(ATerm, Maybe ATerm)]
_ Maybe (Ellipsis ATerm)
_) = Type
ty
getType (ATContainerComp Type
ty Container
_ Bind (Telescope AQual) ATerm
_) = Type
ty
getType (ATLet Type
ty Bind (Telescope ABinding) ATerm
_) = Type
ty
getType (ATCase Type
ty [ABranch]
_) = Type
ty
getType (ATTest [(String, Type, Name ATerm)]
_ ATerm
_ ) = Type
TyProp
setType :: Type -> ATerm -> ATerm
setType Type
ty (ATVar Type
_ QName ATerm
x ) = Type -> QName ATerm -> ATerm
ATVar Type
ty QName ATerm
x
setType Type
ty (ATPrim Type
_ Prim
x ) = Type -> Prim -> ATerm
ATPrim Type
ty Prim
x
setType Type
_ ATerm
ATUnit = ATerm
ATUnit
setType Type
ty (ATBool Type
_ Bool
b) = Type -> Bool -> ATerm
ATBool Type
ty Bool
b
setType Type
ty (ATNat Type
_ Integer
x ) = Type -> Integer -> ATerm
ATNat Type
ty Integer
x
setType Type
_ (ATRat Rational
r) = Rational -> ATerm
ATRat Rational
r
setType Type
_ (ATChar Char
c) = Char -> ATerm
ATChar Char
c
setType Type
_ (ATString String
cs) = String -> ATerm
ATString String
cs
setType Type
ty (ATAbs Quantifier
q Type
_ Bind [APattern] ATerm
x ) = Quantifier -> Type -> Bind [APattern] ATerm -> ATerm
ATAbs Quantifier
q Type
ty Bind [APattern] ATerm
x
setType Type
ty (ATApp Type
_ ATerm
x ATerm
y ) = Type -> ATerm -> ATerm -> ATerm
ATApp Type
ty ATerm
x ATerm
y
setType Type
ty (ATTup Type
_ [ATerm]
x ) = Type -> [ATerm] -> ATerm
ATTup Type
ty [ATerm]
x
setType Type
ty (ATTyOp Type
_ TyOp
x Type
y ) = Type -> TyOp -> Type -> ATerm
ATTyOp Type
ty TyOp
x Type
y
setType Type
ty (ATChain Type
_ ATerm
x [ALink]
y ) = Type -> ATerm -> [ALink] -> ATerm
ATChain Type
ty ATerm
x [ALink]
y
setType Type
ty (ATContainer Type
_ Container
x [(ATerm, Maybe ATerm)]
y Maybe (Ellipsis ATerm)
z) = Type
-> Container
-> [(ATerm, Maybe ATerm)]
-> Maybe (Ellipsis ATerm)
-> ATerm
ATContainer Type
ty Container
x [(ATerm, Maybe ATerm)]
y Maybe (Ellipsis ATerm)
z
setType Type
ty (ATContainerComp Type
_ Container
x Bind (Telescope AQual) ATerm
y) = Type -> Container -> Bind (Telescope AQual) ATerm -> ATerm
ATContainerComp Type
ty Container
x Bind (Telescope AQual) ATerm
y
setType Type
ty (ATLet Type
_ Bind (Telescope ABinding) ATerm
x ) = Type -> Bind (Telescope ABinding) ATerm -> ATerm
ATLet Type
ty Bind (Telescope ABinding) ATerm
x
setType Type
ty (ATCase Type
_ [ABranch]
x ) = Type -> [ABranch] -> ATerm
ATCase Type
ty [ABranch]
x
setType Type
_ (ATTest [(String, Type, Name ATerm)]
vs ATerm
x) = [(String, Type, Name ATerm)] -> ATerm -> ATerm
ATTest [(String, Type, Name ATerm)]
vs ATerm
x
instance HasType APattern where
getType :: APattern -> Type
getType (APVar Type
ty Name ATerm
_) = Type
ty
getType (APWild Type
ty) = Type
ty
getType APattern
APUnit = Type
TyUnit
getType (APBool Bool
_) = Type
TyBool
getType (APChar Char
_) = Type
TyC
getType (APString String
_) = Type -> Type
TyList Type
TyC
getType (APTup Type
ty [APattern]
_) = Type
ty
getType (APInj Type
ty Side
_ APattern
_) = Type
ty
getType (APNat Type
ty Integer
_) = Type
ty
getType (APCons Type
ty APattern
_ APattern
_) = Type
ty
getType (APList Type
ty [APattern]
_) = Type
ty
getType (APAdd Type
ty Side
_ APattern
_ ATerm
_) = Type
ty
getType (APMul Type
ty Side
_ APattern
_ ATerm
_) = Type
ty
getType (APSub Type
ty APattern
_ ATerm
_) = Type
ty
getType (APNeg Type
ty APattern
_) = Type
ty
getType (APFrac Type
ty APattern
_ APattern
_) = Type
ty
instance HasType ABranch where
getType :: ABranch -> Type
getType = ATerm -> Type
forall t. HasType t => t -> Type
getType (ATerm -> Type) -> (ABranch -> ATerm) -> ABranch -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Telescope AGuard, ATerm) -> ATerm
forall a b. (a, b) -> b
snd ((Telescope AGuard, ATerm) -> ATerm)
-> (ABranch -> (Telescope AGuard, ATerm)) -> ABranch -> ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ABranch -> (Telescope AGuard, ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind
substQT :: QName ATerm -> ATerm -> ATerm -> ATerm
substQT :: QName ATerm -> ATerm -> ATerm -> ATerm
substQT QName ATerm
x ATerm
s = (ATerm -> ATerm) -> ATerm -> ATerm
forall a. Plated a => (a -> a) -> a -> a
transform ((ATerm -> ATerm) -> ATerm -> ATerm)
-> (ATerm -> ATerm) -> ATerm -> ATerm
forall a b. (a -> b) -> a -> b
$ \case
t :: ATerm
t@(ATVar Type
_ QName ATerm
y)
| QName ATerm
x QName ATerm -> QName ATerm -> Bool
forall a. Eq a => a -> a -> Bool
== QName ATerm
y -> ATerm
s
| Bool
otherwise -> ATerm
t
ATerm
t -> ATerm
t
instance Pretty ATerm where
pretty :: ATerm -> Sem r Doc
pretty = Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Term -> Sem r Doc) -> (ATerm -> Term) -> ATerm -> Sem r Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ATerm -> Term
explode
explode :: ATerm -> Term
explode :: ATerm -> Term
explode = \case
ATVar Type
ty QName ATerm
x -> Term -> PolyType -> Term
TAscr (Name Term -> Term
TVar (Name ATerm -> Name Term
coerce (QName ATerm -> Name ATerm
forall a. QName a -> Name a
qname QName ATerm
x))) (Type -> PolyType
toPolyType Type
ty)
ATPrim Type
ty Prim
x -> Term -> PolyType -> Term
TAscr (Prim -> Term
TPrim Prim
x) (Type -> PolyType
toPolyType Type
ty)
ATLet Type
ty Bind (Telescope ABinding) ATerm
tel -> Term -> PolyType -> Term
TAscr (Bind (Telescope Binding) Term -> Term
TLet ((ABinding -> Binding)
-> Bind (Telescope ABinding) ATerm -> Bind (Telescope Binding) Term
forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope ABinding -> Binding
explodeBinding Bind (Telescope ABinding) ATerm
tel)) (Type -> PolyType
toPolyType Type
ty)
ATerm
ATUnit -> Term
TUnit
ATBool Type
_ty Bool
b -> Bool -> Term
TBool Bool
b
ATNat Type
ty Integer
x -> Term -> PolyType -> Term
TAscr (Integer -> Term
TNat Integer
x) (Type -> PolyType
toPolyType Type
ty)
ATRat Rational
r -> Rational -> Term
TRat Rational
r
ATChar Char
c -> Char -> Term
TChar Char
c
ATString String
cs -> String -> Term
TString String
cs
ATAbs Quantifier
q Type
ty Bind [APattern] ATerm
a -> Term -> PolyType -> Term
TAscr (Quantifier -> Bind [Pattern] Term -> Term
TAbs Quantifier
q (Bind [APattern] ATerm -> Bind [Pattern] Term
explodeAbs Bind [APattern] ATerm
a)) (Type -> PolyType
toPolyType Type
ty)
ATApp Type
ty ATerm
x ATerm
y -> Term -> PolyType -> Term
TAscr (Term -> Term -> Term
TApp (ATerm -> Term
explode ATerm
x) (ATerm -> Term
explode ATerm
y)) (Type -> PolyType
toPolyType Type
ty)
ATTup Type
ty [ATerm]
xs -> Term -> PolyType -> Term
TAscr ([Term] -> Term
TTup ((ATerm -> Term) -> [ATerm] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ATerm -> Term
explode [ATerm]
xs)) (Type -> PolyType
toPolyType Type
ty)
ATCase Type
ty [ABranch]
bs -> Term -> PolyType -> Term
TAscr ([Branch] -> Term
TCase ((ABranch -> Branch) -> [ABranch] -> [Branch]
forall a b. (a -> b) -> [a] -> [b]
map ABranch -> Branch
explodeBranch [ABranch]
bs)) (Type -> PolyType
toPolyType Type
ty)
ATChain Type
ty ATerm
t [ALink]
ls -> Term -> PolyType -> Term
TAscr (Term -> [Link] -> Term
TChain (ATerm -> Term
explode ATerm
t) ((ALink -> Link) -> [ALink] -> [Link]
forall a b. (a -> b) -> [a] -> [b]
map ALink -> Link
explodeLink [ALink]
ls)) (Type -> PolyType
toPolyType Type
ty)
ATTyOp Type
ty TyOp
x Type
y -> Term -> PolyType -> Term
TAscr (TyOp -> Type -> Term
TTyOp TyOp
x Type
y) (Type -> PolyType
toPolyType Type
ty)
ATContainer Type
ty Container
c [(ATerm, Maybe ATerm)]
ts Maybe (Ellipsis ATerm)
el ->
Term -> PolyType -> Term
TAscr
(Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c (((ATerm, Maybe ATerm) -> (Term, Maybe Term))
-> [(ATerm, Maybe ATerm)] -> [(Term, Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map (ATerm -> Term
explode (ATerm -> Term)
-> (Maybe ATerm -> Maybe Term)
-> (ATerm, Maybe ATerm)
-> (Term, Maybe Term)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (ATerm -> Term) -> Maybe ATerm -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ATerm -> Term
explode) [(ATerm, Maybe ATerm)]
ts) ((Ellipsis ATerm -> Ellipsis Term)
-> Maybe (Ellipsis ATerm) -> Maybe (Ellipsis Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ATerm -> Term) -> Ellipsis ATerm -> Ellipsis Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ATerm -> Term
explode) Maybe (Ellipsis ATerm)
el))
(Type -> PolyType
toPolyType Type
ty)
ATContainerComp Type
ty Container
c Bind (Telescope AQual) ATerm
b -> Term -> PolyType -> Term
TAscr (Container -> Bind (Telescope Qual) Term -> Term
TContainerComp Container
c ((AQual -> Qual)
-> Bind (Telescope AQual) ATerm -> Bind (Telescope Qual) Term
forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope AQual -> Qual
explodeQual Bind (Telescope AQual) ATerm
b)) (Type -> PolyType
toPolyType Type
ty)
ATTest [(String, Type, Name ATerm)]
_vs ATerm
x -> Term -> PolyType -> Term
TAscr (ATerm -> Term
explode ATerm
x) (Type -> PolyType
toPolyType Type
TyProp)
explodeTelescope
:: (Alpha a, Alpha b)
=> (a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope :: (a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope a -> b
explodeBinder (Bind (Telescope a) ATerm -> (Telescope a, ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> (Telescope a
xs,ATerm
at)) = Telescope b -> Term -> Bind (Telescope b) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((a -> b) -> Telescope a -> Telescope b
forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Telescope a -> Telescope b
mapTelescope a -> b
explodeBinder Telescope a
xs) (ATerm -> Term
explode ATerm
at)
explodeBinding :: ABinding -> Binding
explodeBinding :: ABinding -> Binding
explodeBinding (ABinding Maybe (Embed PolyType)
m Name ATerm
b (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
n)) = Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
Binding Maybe (Embed PolyType)
m (Name ATerm -> Name Term
coerce Name ATerm
b) (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
n))
explodeAbs :: Bind [APattern] ATerm -> Bind [Pattern] Term
explodeAbs :: Bind [APattern] ATerm -> Bind [Pattern] Term
explodeAbs (Bind [APattern] ATerm -> ([APattern], ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([APattern]
aps, ATerm
at)) = [Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((APattern -> Pattern) -> [APattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Pattern
explodePattern [APattern]
aps) (ATerm -> Term
explode ATerm
at)
explodePattern :: APattern -> Pattern
explodePattern :: APattern -> Pattern
explodePattern = \case
APVar Type
ty Name ATerm
x -> Pattern -> Type -> Pattern
PAscr (Name Term -> Pattern
PVar (Name ATerm -> Name Term
coerce Name ATerm
x)) Type
ty
APWild Type
ty -> Pattern -> Type -> Pattern
PAscr Pattern
PWild Type
ty
APattern
APUnit -> Pattern
PUnit
APBool Bool
b -> Bool -> Pattern
PBool Bool
b
APChar Char
c -> Char -> Pattern
PChar Char
c
APString String
s -> String -> Pattern
PString String
s
APTup Type
ty [APattern]
ps -> Pattern -> Type -> Pattern
PAscr ([Pattern] -> Pattern
PTup ((APattern -> Pattern) -> [APattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Pattern
explodePattern [APattern]
ps)) Type
ty
APInj Type
ty Side
s APattern
p -> Pattern -> Type -> Pattern
PAscr (Side -> Pattern -> Pattern
PInj Side
s (APattern -> Pattern
explodePattern APattern
p)) Type
ty
APNat Type
ty Integer
n -> Pattern -> Type -> Pattern
PAscr (Integer -> Pattern
PNat Integer
n) Type
ty
APCons Type
ty APattern
p1 APattern
p2 -> Pattern -> Type -> Pattern
PAscr (Pattern -> Pattern -> Pattern
PCons (APattern -> Pattern
explodePattern APattern
p1) (APattern -> Pattern
explodePattern APattern
p2)) Type
ty
APList Type
ty [APattern]
ps -> Pattern -> Type -> Pattern
PAscr ([Pattern] -> Pattern
PList ((APattern -> Pattern) -> [APattern] -> [Pattern]
forall a b. (a -> b) -> [a] -> [b]
map APattern -> Pattern
explodePattern [APattern]
ps)) Type
ty
APAdd Type
ty Side
s APattern
p ATerm
t -> Pattern -> Type -> Pattern
PAscr (Side -> Pattern -> Term -> Pattern
PAdd Side
s (APattern -> Pattern
explodePattern APattern
p) (ATerm -> Term
explode ATerm
t)) Type
ty
APMul Type
ty Side
s APattern
p ATerm
t -> Pattern -> Type -> Pattern
PAscr (Side -> Pattern -> Term -> Pattern
PMul Side
s (APattern -> Pattern
explodePattern APattern
p) (ATerm -> Term
explode ATerm
t)) Type
ty
APSub Type
ty APattern
p ATerm
t -> Pattern -> Type -> Pattern
PAscr (Pattern -> Term -> Pattern
PSub (APattern -> Pattern
explodePattern APattern
p) (ATerm -> Term
explode ATerm
t)) Type
ty
APNeg Type
ty APattern
p -> Pattern -> Type -> Pattern
PAscr (Pattern -> Pattern
PNeg (APattern -> Pattern
explodePattern APattern
p)) Type
ty
APFrac Type
ty APattern
p APattern
q -> Pattern -> Type -> Pattern
PAscr (Pattern -> Pattern -> Pattern
PFrac (APattern -> Pattern
explodePattern APattern
p) (APattern -> Pattern
explodePattern APattern
q)) Type
ty
explodeBranch :: ABranch -> Branch
explodeBranch :: ABranch -> Branch
explodeBranch = (AGuard -> Guard) -> ABranch -> Branch
forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope AGuard -> Guard
explodeGuard
explodeGuard :: AGuard -> Guard
explodeGuard :: AGuard -> Guard
explodeGuard (AGBool (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Embed Term -> Guard
GBool (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
at))
explodeGuard (AGPat (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at) APattern
ap) = Embed Term -> Pattern -> Guard
GPat (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
at)) (APattern -> Pattern
explodePattern APattern
ap)
explodeGuard (AGLet ABinding
ab) = Binding -> Guard
GLet (ABinding -> Binding
explodeBinding ABinding
ab)
explodeLink :: ALink -> Link
explodeLink :: ALink -> Link
explodeLink (ATLink BOp
bop ATerm
at) = BOp -> Term -> Link
TLink BOp
bop (ATerm -> Term
explode ATerm
at)
explodeQual :: AQual -> Qual
explodeQual :: AQual -> Qual
explodeQual (AQBind Name ATerm
x (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Name Term -> Embed Term -> Qual
QBind (Name ATerm -> Name Term
coerce Name ATerm
x) (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
at))
explodeQual (AQGuard (Embed ATerm -> Embedded (Embed ATerm)
forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Embed Term -> Qual
QGuard (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
at))