{-# 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 (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)

-- | 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 $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   -- 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 $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

-- 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 $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

------------------------------------------------------------
-- 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 :: 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