{-# LANGUAGE PatternSynonyms #-}
module Disco.AST.Desugared
(
DTerm
, pattern DTVar
, pattern DTPrim
, pattern DTUnit
, pattern DTBool
, pattern DTChar
, pattern DTNat
, pattern DTRat
, pattern DTAbs
, pattern DTApp
, pattern DTPair
, pattern DTCase
, pattern DTTyOp
, pattern DTNil
, pattern DTTest
, Container(..)
, DBinding
, pattern DBinding
, DBranch
, DGuard
, pattern DGPat
, DPattern
, pattern DPVar
, pattern DPWild
, pattern DPUnit
, pattern DPPair
, pattern DPInj
, DProperty
)
where
import GHC.Generics
import Data.Void
import Unbound.Generics.LocallyNameless
import Disco.AST.Generic
import Disco.Names (QName (..))
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
data DS
type DProperty = Property_ DS
type DTerm = Term_ DS
type instance X_Binder DS = Name DTerm
type instance X_TVar DS = Void
type instance X_TPrim DS = Type
type instance X_TLet DS = Void
type instance X_TUnit DS = ()
type instance X_TBool DS = Type
type instance X_TChar DS = ()
type instance X_TString DS = Void
type instance X_TNat DS = Type
type instance X_TRat DS = ()
type instance X_TAbs DS = Type
type instance X_TApp DS = Type
type instance X_TCase DS = Type
type instance X_TChain DS = Void
type instance X_TTyOp DS = Type
type instance X_TContainer DS = Void
type instance X_TContainerComp DS = Void
type instance X_TAscr DS = Void
type instance X_TTup DS = Void
type instance X_TParens DS = Void
type instance X_Term DS = X_DTerm
data X_DTerm
= DTPair_ Type DTerm DTerm
| DTNil_ Type
| DTTest_ [(String, Type, Name DTerm)] DTerm
| DTVar_ Type (QName DTerm)
deriving (Int -> X_DTerm -> ShowS
[X_DTerm] -> ShowS
X_DTerm -> String
(Int -> X_DTerm -> ShowS)
-> (X_DTerm -> String) -> ([X_DTerm] -> ShowS) -> Show X_DTerm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [X_DTerm] -> ShowS
$cshowList :: [X_DTerm] -> ShowS
show :: X_DTerm -> String
$cshow :: X_DTerm -> String
showsPrec :: Int -> X_DTerm -> ShowS
$cshowsPrec :: Int -> X_DTerm -> ShowS
Show, (forall x. X_DTerm -> Rep X_DTerm x)
-> (forall x. Rep X_DTerm x -> X_DTerm) -> Generic X_DTerm
forall x. Rep X_DTerm x -> X_DTerm
forall x. X_DTerm -> Rep X_DTerm x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep X_DTerm x -> X_DTerm
$cfrom :: forall x. X_DTerm -> Rep X_DTerm x
Generic)
instance Subst Type X_DTerm
instance Alpha X_DTerm
pattern DTVar :: Type -> QName DTerm -> DTerm
pattern $bDTVar :: Type -> QName DTerm -> DTerm
$mDTVar :: forall r. DTerm -> (Type -> QName DTerm -> r) -> (Void# -> r) -> r
DTVar ty qname = XTerm_ (DTVar_ ty qname)
pattern DTPrim :: Type -> Prim -> DTerm
pattern $bDTPrim :: Type -> Prim -> DTerm
$mDTPrim :: forall r. DTerm -> (Type -> Prim -> r) -> (Void# -> r) -> r
DTPrim ty name = TPrim_ ty name
pattern DTUnit :: DTerm
pattern $bDTUnit :: DTerm
$mDTUnit :: forall r. DTerm -> (Void# -> r) -> (Void# -> r) -> r
DTUnit = TUnit_ ()
pattern DTBool :: Type -> Bool -> DTerm
pattern $bDTBool :: Type -> Bool -> DTerm
$mDTBool :: forall r. DTerm -> (Type -> Bool -> r) -> (Void# -> r) -> r
DTBool ty bool = TBool_ ty bool
pattern DTNat :: Type -> Integer -> DTerm
pattern $bDTNat :: Type -> Integer -> DTerm
$mDTNat :: forall r. DTerm -> (Type -> Integer -> r) -> (Void# -> r) -> r
DTNat ty int = TNat_ ty int
pattern DTRat :: Rational -> DTerm
pattern $bDTRat :: Rational -> DTerm
$mDTRat :: forall r. DTerm -> (Rational -> r) -> (Void# -> r) -> r
DTRat rat = TRat_ () rat
pattern DTChar :: Char -> DTerm
pattern $bDTChar :: Char -> DTerm
$mDTChar :: forall r. DTerm -> (Char -> r) -> (Void# -> r) -> r
DTChar c = TChar_ () c
pattern DTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
pattern $bDTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
$mDTAbs :: forall r.
DTerm
-> (Quantifier -> Type -> Bind (Name DTerm) DTerm -> r)
-> (Void# -> r)
-> r
DTAbs q ty lam = TAbs_ q ty lam
pattern DTApp :: Type -> DTerm -> DTerm -> DTerm
pattern $bDTApp :: Type -> DTerm -> DTerm -> DTerm
$mDTApp :: forall r.
DTerm -> (Type -> DTerm -> DTerm -> r) -> (Void# -> r) -> r
DTApp ty term1 term2 = TApp_ ty term1 term2
pattern DTPair :: Type -> DTerm -> DTerm -> DTerm
pattern $bDTPair :: Type -> DTerm -> DTerm -> DTerm
$mDTPair :: forall r.
DTerm -> (Type -> DTerm -> DTerm -> r) -> (Void# -> r) -> r
DTPair ty t1 t2 = XTerm_ (DTPair_ ty t1 t2)
pattern DTCase :: Type -> [DBranch] -> DTerm
pattern $bDTCase :: Type -> [DBranch] -> DTerm
$mDTCase :: forall r. DTerm -> (Type -> [DBranch] -> r) -> (Void# -> r) -> r
DTCase ty branch = TCase_ ty branch
pattern DTTyOp :: Type -> TyOp -> Type -> DTerm
pattern $bDTTyOp :: Type -> TyOp -> Type -> DTerm
$mDTTyOp :: forall r. DTerm -> (Type -> TyOp -> Type -> r) -> (Void# -> r) -> r
DTTyOp ty1 tyop ty2 = TTyOp_ ty1 tyop ty2
pattern DTNil :: Type -> DTerm
pattern $bDTNil :: Type -> DTerm
$mDTNil :: forall r. DTerm -> (Type -> r) -> (Void# -> r) -> r
DTNil ty = XTerm_ (DTNil_ ty)
pattern DTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm
pattern $bDTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm
$mDTTest :: forall r.
DTerm
-> ([(String, Type, Name DTerm)] -> DTerm -> r)
-> (Void# -> r)
-> r
DTTest ns t = XTerm_ (DTTest_ ns t)
{-# COMPLETE DTVar, DTPrim, DTUnit, DTBool, DTChar, DTNat, DTRat,
DTAbs, DTApp, DTPair, DTCase, DTTyOp,
DTNil, DTTest #-}
type instance X_TLink DS = Void
type DBinding = Binding_ DS
pattern DBinding :: Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> DBinding
pattern $bDBinding :: Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> DBinding
$mDBinding :: forall r.
DBinding
-> (Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> r)
-> (Void# -> r)
-> r
DBinding m b n = Binding_ m b n
{-# COMPLETE DBinding #-}
type DBranch = Bind (Telescope DGuard) DTerm
type DGuard = Guard_ DS
type instance X_GBool DS = Void
type instance X_GPat DS = ()
type instance X_GLet DS = Void
pattern DGPat :: Embed DTerm -> DPattern -> DGuard
pattern $bDGPat :: Embed DTerm -> DPattern -> DGuard
$mDGPat :: forall r.
DGuard -> (Embed DTerm -> DPattern -> r) -> (Void# -> r) -> r
DGPat embedt pat = GPat_ () embedt pat
{-# COMPLETE DGPat #-}
type DPattern = Pattern_ DS
type instance X_PVar DS = Embed Type
type instance X_PWild DS = Embed Type
type instance X_PAscr DS = Void
type instance X_PUnit DS = ()
type instance X_PBool DS = Void
type instance X_PChar DS = Void
type instance X_PString DS = Void
type instance X_PTup DS = Void
type instance X_PInj DS = Void
type instance X_PNat DS = Void
type instance X_PCons DS = Void
type instance X_PList DS = Void
type instance X_PAdd DS = Void
type instance X_PMul DS = Void
type instance X_PSub DS = Void
type instance X_PNeg DS = Void
type instance X_PFrac DS = Void
type instance X_Pattern DS =
Either
(Embed Type, Name DTerm, Name DTerm)
(Embed Type, Side, Name DTerm)
pattern DPVar :: Type -> Name DTerm -> DPattern
pattern $bDPVar :: Type -> Name DTerm -> DPattern
$mDPVar :: forall r.
DPattern -> (Type -> Name DTerm -> r) -> (Void# -> r) -> r
DPVar ty name <- PVar_ (unembed -> ty) name
where
DPVar Type
ty Name DTerm
name = X_PVar DS -> Name DTerm -> DPattern
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 DTerm
name
pattern DPWild :: Type -> DPattern
pattern $bDPWild :: Type -> DPattern
$mDPWild :: forall r. DPattern -> (Type -> r) -> (Void# -> r) -> r
DPWild ty <- PWild_ (unembed -> ty)
where
DPWild Type
ty = X_PWild DS -> DPattern
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 DPUnit :: DPattern
pattern $bDPUnit :: DPattern
$mDPUnit :: forall r. DPattern -> (Void# -> r) -> (Void# -> r) -> r
DPUnit = PUnit_ ()
pattern DPPair :: Type -> Name DTerm -> Name DTerm -> DPattern
pattern $bDPPair :: Type -> Name DTerm -> Name DTerm -> DPattern
$mDPPair :: forall r.
DPattern
-> (Type -> Name DTerm -> Name DTerm -> r) -> (Void# -> r) -> r
DPPair ty x1 x2 <- XPattern_ (Left (unembed -> ty, x1, x2))
where
DPPair Type
ty Name DTerm
x1 Name DTerm
x2 = X_Pattern DS -> DPattern
forall e. X_Pattern e -> Pattern_ e
XPattern_ ((Embed Type, Name DTerm, Name DTerm)
-> Either
(Embed Type, Name DTerm, Name DTerm) (Embed Type, Side, Name DTerm)
forall a b. a -> Either a b
Left (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty, Name DTerm
x1, Name DTerm
x2))
pattern DPInj :: Type -> Side -> Name DTerm -> DPattern
pattern $bDPInj :: Type -> Side -> Name DTerm -> DPattern
$mDPInj :: forall r.
DPattern -> (Type -> Side -> Name DTerm -> r) -> (Void# -> r) -> r
DPInj ty s x <- XPattern_ (Right (unembed -> ty, s, x))
where
DPInj Type
ty Side
s Name DTerm
x = X_Pattern DS -> DPattern
forall e. X_Pattern e -> Pattern_ e
XPattern_ ((Embed Type, Side, Name DTerm)
-> Either
(Embed Type, Name DTerm, Name DTerm) (Embed Type, Side, Name DTerm)
forall a b. b -> Either a b
Right (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
Type
ty, Side
s, Name DTerm
x))
{-# COMPLETE DPVar, DPWild, DPUnit, DPPair, DPInj #-}
type instance X_QBind DS = Void
type instance X_QGuard DS = Void
instance HasType DTerm where
getType :: DTerm -> Type
getType (DTVar Type
ty QName DTerm
_) = Type
ty
getType (DTPrim Type
ty Prim
_) = Type
ty
getType DTerm
DTUnit = Type
TyUnit
getType (DTBool Type
ty Bool
_) = Type
ty
getType (DTChar Char
_) = Type
TyC
getType (DTNat Type
ty Integer
_) = Type
ty
getType (DTRat Rational
_) = Type
TyF
getType (DTAbs Quantifier
Lam Type
ty Bind (Name DTerm) DTerm
_) = Type
ty
getType DTAbs{} = Type
TyProp
getType (DTApp Type
ty DTerm
_ DTerm
_) = Type
ty
getType (DTPair Type
ty DTerm
_ DTerm
_) = Type
ty
getType (DTCase Type
ty [DBranch]
_) = Type
ty
getType (DTTyOp Type
ty TyOp
_ Type
_) = Type
ty
getType (DTNil Type
ty) = Type
ty
getType (DTTest [(String, Type, Name DTerm)]
_ DTerm
_) = Type
TyProp
instance HasType DPattern where
getType :: DPattern -> Type
getType (DPVar Type
ty Name DTerm
_) = Type
ty
getType (DPWild Type
ty) = Type
ty
getType DPattern
DPUnit = Type
TyUnit
getType (DPPair Type
ty Name DTerm
_ Name DTerm
_) = Type
ty
getType (DPInj Type
ty Side
_ Name DTerm
_) = Type
ty