{-# LANGUAGE PatternSynonyms #-}

-- |
-- Module      :  Disco.AST.Desugared
-- Copyright   :  disco team and contributors
-- Maintainer  :  [email protected]
--
-- 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 (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
$cshowsPrec :: Int -> X_DTerm -> ShowS
showsPrec :: Int -> X_DTerm -> ShowS
$cshow :: X_DTerm -> String
show :: X_DTerm -> String
$cshowList :: [X_DTerm] -> ShowS
showList :: [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
$cfrom :: forall x. X_DTerm -> Rep X_DTerm x
from :: forall x. X_DTerm -> Rep X_DTerm x
$cto :: forall x. Rep X_DTerm x -> X_DTerm
to :: forall x. Rep X_DTerm x -> X_DTerm
Generic)

instance Subst Type X_DTerm
instance Alpha X_DTerm

pattern DTVar :: Type -> QName DTerm -> DTerm
pattern $mDTVar :: forall {r}.
DTerm -> (Type -> QName DTerm -> r) -> ((# #) -> r) -> r
$bDTVar :: Type -> QName DTerm -> DTerm
DTVar ty qname = XTerm_ (DTVar_ ty qname)

pattern DTPrim :: Type -> Prim -> DTerm
pattern $mDTPrim :: forall {r}. DTerm -> (Type -> Prim -> r) -> ((# #) -> r) -> r
$bDTPrim :: Type -> Prim -> DTerm
DTPrim ty name = TPrim_ ty name

pattern DTUnit :: DTerm
pattern $mDTUnit :: forall {r}. DTerm -> ((# #) -> r) -> ((# #) -> r) -> r
$bDTUnit :: DTerm
DTUnit = TUnit_ ()

pattern DTBool :: Type -> Bool -> DTerm
pattern $mDTBool :: forall {r}. DTerm -> (Type -> Bool -> r) -> ((# #) -> r) -> r
$bDTBool :: Type -> Bool -> DTerm
DTBool ty bool = TBool_ ty bool

pattern DTNat :: Type -> Integer -> DTerm
pattern $mDTNat :: forall {r}. DTerm -> (Type -> Integer -> r) -> ((# #) -> r) -> r
$bDTNat :: Type -> Integer -> DTerm
DTNat ty int = TNat_ ty int

pattern DTRat :: Rational -> DTerm
pattern $mDTRat :: forall {r}. DTerm -> (Rational -> r) -> ((# #) -> r) -> r
$bDTRat :: Rational -> DTerm
DTRat rat = TRat_ () rat

pattern DTChar :: Char -> DTerm
pattern $mDTChar :: forall {r}. DTerm -> (Char -> r) -> ((# #) -> r) -> r
$bDTChar :: Char -> DTerm
DTChar c = TChar_ () c

pattern DTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
pattern $mDTAbs :: forall {r}.
DTerm
-> (Quantifier -> Type -> Bind (Name DTerm) DTerm -> r)
-> ((# #) -> r)
-> r
$bDTAbs :: Quantifier -> Type -> Bind (Name DTerm) DTerm -> DTerm
DTAbs q ty lam = TAbs_ q ty lam

pattern DTApp :: Type -> DTerm -> DTerm -> DTerm
pattern $mDTApp :: forall {r}.
DTerm -> (Type -> DTerm -> DTerm -> r) -> ((# #) -> r) -> r
$bDTApp :: Type -> DTerm -> DTerm -> DTerm
DTApp ty term1 term2 = TApp_ ty term1 term2

pattern DTPair :: Type -> DTerm -> DTerm -> DTerm
pattern $mDTPair :: forall {r}.
DTerm -> (Type -> DTerm -> DTerm -> r) -> ((# #) -> r) -> r
$bDTPair :: Type -> DTerm -> DTerm -> DTerm
DTPair ty t1 t2 = XTerm_ (DTPair_ ty t1 t2)

pattern DTCase :: Type -> [DBranch] -> DTerm
pattern $mDTCase :: forall {r}. DTerm -> (Type -> [DBranch] -> r) -> ((# #) -> r) -> r
$bDTCase :: Type -> [DBranch] -> DTerm
DTCase ty branch = TCase_ ty branch

pattern DTTyOp :: Type -> TyOp -> Type -> DTerm
pattern $mDTTyOp :: forall {r}.
DTerm -> (Type -> TyOp -> Type -> r) -> ((# #) -> r) -> r
$bDTTyOp :: Type -> TyOp -> Type -> DTerm
DTTyOp ty1 tyop ty2 = TTyOp_ ty1 tyop ty2

pattern DTNil :: Type -> DTerm
pattern $mDTNil :: forall {r}. DTerm -> (Type -> r) -> ((# #) -> r) -> r
$bDTNil :: Type -> DTerm
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 $mDTTest :: forall {r}.
DTerm
-> ([(String, Type, Name DTerm)] -> DTerm -> r)
-> ((# #) -> r)
-> r
$bDTTest :: [(String, Type, Name DTerm)] -> DTerm -> DTerm
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 $mDBinding :: forall {r}.
Binding_ DS
-> (Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> r)
-> ((# #) -> r)
-> r
$bDBinding :: Maybe (Embed PolyType) -> Name DTerm -> Embed DTerm -> Binding_ DS
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 $mDGPat :: forall {r}.
Guard_ DS -> (Embed DTerm -> Pattern_ DS -> r) -> ((# #) -> r) -> r
$bDGPat :: Embed DTerm -> Pattern_ DS -> Guard_ DS
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 $mDPVar :: forall {r}.
Pattern_ DS -> (Type -> Name DTerm -> r) -> ((# #) -> r) -> r
$bDPVar :: Type -> Name DTerm -> Pattern_ DS
DPVar ty name <- PVar_ (unembed -> ty) name
  where
    DPVar Type
ty Name DTerm
name = X_PVar DS -> Name DTerm -> Pattern_ DS
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 $mDPWild :: forall {r}. Pattern_ DS -> (Type -> r) -> ((# #) -> r) -> r
$bDPWild :: Type -> Pattern_ DS
DPWild ty <- PWild_ (unembed -> ty)
  where
    DPWild Type
ty = X_PWild DS -> Pattern_ DS
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 $mDPUnit :: forall {r}. Pattern_ DS -> ((# #) -> r) -> ((# #) -> r) -> r
$bDPUnit :: Pattern_ DS
DPUnit = PUnit_ ()

pattern DPPair :: Type -> Name DTerm -> Name DTerm -> DPattern
pattern $mDPPair :: forall {r}.
Pattern_ DS
-> (Type -> Name DTerm -> Name DTerm -> r) -> ((# #) -> r) -> r
$bDPPair :: Type -> Name DTerm -> Name DTerm -> Pattern_ DS
DPPair ty x1 x2 <- XPattern_ (Left (unembed -> ty, x1, x2))
  where
    DPPair Type
ty Name DTerm
x1 Name DTerm
x2 = X_Pattern DS -> Pattern_ DS
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 $mDPInj :: forall {r}.
Pattern_ DS
-> (Type -> Side -> Name DTerm -> r) -> ((# #) -> r) -> r
$bDPInj :: Type -> Side -> Name DTerm -> Pattern_ DS
DPInj ty s x <- XPattern_ (Right (unembed -> ty, s, x))
  where
    DPInj Type
ty Side
s Name DTerm
x = X_Pattern DS -> Pattern_ DS
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

------------------------------------------------------------
-- getType
------------------------------------------------------------

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 :: Pattern_ DS -> Type
getType (DPVar Type
ty Name DTerm
_) = Type
ty
  getType (DPWild Type
ty) = Type
ty
  getType Pattern_ DS
DPUnit = Type
TyUnit
  getType (DPPair Type
ty Name DTerm
_ Name DTerm
_) = Type
ty
  getType (DPInj Type
ty Side
_ Name DTerm
_) = Type
ty