disco-0.1.0.0: src/Disco/AST/Desugared.hs
{-# LANGUAGE PatternSynonyms #-}
-----------------------------------------------------------------------------
-- |
-- Module : Disco.AST.Desugared
-- Copyright : disco team and contributors
-- Maintainer : byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Typed abstract syntax trees representing the typechecked, desugared
-- Disco language.
--
-----------------------------------------------------------------------------
module Disco.AST.Desugared
( -- * Desugared, type-annotated terms
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
-- * Branches and guards
, 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
-- | A @DTerm@ is a term which has been typechecked and desugared, so
-- it has fewer constructors and complex features than 'ATerm', but
-- still retains typing information.
type DTerm = Term_ DS
type instance X_Binder DS = Name DTerm
type instance X_TVar DS = Void -- names are qualified
type instance X_TPrim DS = Type
type instance X_TLet DS = Void -- Let gets translated to lambda
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 -- For lambas this is the function type but
-- for forall/exists it's the argument type
type instance X_TApp DS = Type
type instance X_TCase DS = Type
type instance X_TChain DS = Void -- Chains are translated into conjunctions of
-- binary comparisons
type instance X_TTyOp DS = Type
type instance X_TContainer DS = Void -- Literal containers are desugared into
-- conversion functions applied to list literals
type instance X_TContainerComp DS = Void -- Container comprehensions are translated
-- into monadic chains
type instance X_TAscr DS = Void -- No type ascriptions
type instance X_TTup DS = Void -- No tuples, only pairs
type instance X_TParens DS = Void -- No explicit parens
-- Extra constructors
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 (Show, Generic)
instance Subst Type X_DTerm
instance Alpha X_DTerm
pattern DTVar :: Type -> QName DTerm -> DTerm
pattern DTVar ty qname = XTerm_ (DTVar_ ty qname)
pattern DTPrim :: Type -> Prim -> DTerm
pattern DTPrim ty name = TPrim_ ty name
pattern DTUnit :: DTerm
pattern DTUnit = TUnit_ ()
pattern DTBool :: Type -> Bool -> DTerm
pattern DTBool ty bool = TBool_ ty bool
pattern DTNat :: Type -> Integer -> DTerm
pattern DTNat ty int = TNat_ ty int
pattern DTRat :: Rational -> DTerm
pattern DTRat rat = TRat_ () rat
pattern DTChar :: Char -> DTerm
pattern DTChar c = TChar_ () c
pattern DTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
pattern DTAbs q ty lam = TAbs_ q ty lam
pattern DTApp :: Type -> DTerm -> DTerm -> DTerm
pattern DTApp ty term1 term2 = TApp_ ty term1 term2
pattern DTPair :: Type -> DTerm -> DTerm -> DTerm
pattern DTPair ty t1 t2 = XTerm_ (DTPair_ ty t1 t2)
pattern DTCase :: Type -> [DBranch] -> DTerm
pattern DTCase ty branch = TCase_ ty branch
pattern DTTyOp :: Type -> TyOp -> Type -> DTerm
pattern DTTyOp ty1 tyop ty2 = TTyOp_ ty1 tyop ty2
pattern DTNil :: Type -> DTerm
pattern DTNil ty = XTerm_ (DTNil_ ty)
-- | A test frame, recording a collection of variables with their types and
-- their original user-facing names. Used for legible reporting of test
-- failures inside the enclosed term.
pattern DTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm
pattern 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 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 -- Boolean guards get desugared to pattern-matching
type instance X_GPat DS = ()
type instance X_GLet DS = Void -- Let gets desugared to 'when' with a variable
pattern DGPat :: Embed DTerm -> DPattern -> DGuard
pattern 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
-- In the desugared language, constructor patterns (DPPair, DPInj) can
-- only contain variables, not nested patterns. This means that the
-- desugaring phase has to make explicit the order of matching by
-- exploding nested patterns into sequential guards, which makes the
-- interpreter simpler.
type instance X_Pattern DS =
Either
(Embed Type, Name DTerm, Name DTerm) -- DPPair
(Embed Type, Side, Name DTerm) -- DPInj
pattern DPVar :: Type -> Name DTerm -> DPattern
pattern DPVar ty name <- PVar_ (unembed -> ty) name
where
DPVar ty name = PVar_ (embed ty) name
pattern DPWild :: Type -> DPattern
pattern DPWild ty <- PWild_ (unembed -> ty)
where
DPWild ty = PWild_ (embed ty)
pattern DPUnit :: DPattern
pattern DPUnit = PUnit_ ()
pattern DPPair :: Type -> Name DTerm -> Name DTerm -> DPattern
pattern DPPair ty x1 x2 <- XPattern_ (Left (unembed -> ty, x1, x2))
where
DPPair ty x1 x2 = XPattern_ (Left (embed ty, x1, x2))
pattern DPInj :: Type -> Side -> Name DTerm -> DPattern
pattern DPInj ty s x <- XPattern_ (Right (unembed -> ty, s, x))
where
DPInj ty s x = XPattern_ (Right (embed ty, s, x))
{-# COMPLETE DPVar, DPWild, DPUnit, DPPair, DPInj #-}
type instance X_QBind DS = Void
type instance X_QGuard DS = Void
------------------------------------------------------------
-- getType
------------------------------------------------------------
instance HasType DTerm where
getType (DTVar ty _) = ty
getType (DTPrim ty _) = ty
getType DTUnit = TyUnit
getType (DTBool ty _) = ty
getType (DTChar _) = TyC
getType (DTNat ty _) = ty
getType (DTRat _) = TyF
getType (DTAbs Lam ty _) = ty
getType DTAbs{} = TyProp
getType (DTApp ty _ _) = ty
getType (DTPair ty _ _) = ty
getType (DTCase ty _) = ty
getType (DTTyOp ty _ _) = ty
getType (DTNil ty) = ty
getType (DTTest _ _) = TyProp
instance HasType DPattern where
getType (DPVar ty _) = ty
getType (DPWild ty) = ty
getType DPUnit = TyUnit
getType (DPPair ty _ _) = ty
getType (DPInj ty _ _) = ty