{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE PatternSynonyms #-}

-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- |
-- Module      :  Disco.AST.Typed
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Typed abstract syntax trees representing the typechecked surface
-- syntax of the Disco language.  Each tree node is annotated with the
-- type of its subtree.
module Disco.AST.Typed (
  -- * Type-annotated terms
  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,

  -- * Branches and guards
  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,

  -- * Utilities
  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

-- | The extension descriptor for Typed specific AST types.
data TY
  deriving (Typeable TY
TY -> DataType
TY -> Constr
(forall b. Data b => b -> b) -> TY -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> TY -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TY -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> TY -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TY -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data)

type AProperty = Property_ TY

------------------------------------------------------------

-- TODO: Should probably really do this with a 2-level/open recursion
-- approach, with a cofree comonad or whatever

-- | An @ATerm@ is a typechecked term where every node in the tree has
--   been annotated with the type of the subterm rooted at that node.
type ATerm = Term_ TY

type instance X_Binder TY = [APattern]

type instance X_TVar TY = Void -- Names are now qualified
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 -- No more type ascriptions in typechecked terms
type instance X_TTup TY = Type
type instance X_TParens TY = Void -- No more explicit parens

-- A test frame for reporting counterexamples in a test. These don't appear
-- in source programs, but because the deugarer manipulates partly-desugared
-- terms it helps to be able to represent these in 'ATerm'.
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) -> ((# #) -> 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) -> ((# #) -> 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)
-> ((# #) -> r)
-> r
ATLet ty bind = TLet_ ty bind

pattern ATUnit :: ATerm
pattern $bATUnit :: ATerm
$mATUnit :: forall {r}. ATerm -> ((# #) -> r) -> ((# #) -> r) -> r
ATUnit = TUnit_ ()

pattern ATBool :: Type -> Bool -> ATerm
pattern $bATBool :: Type -> Bool -> ATerm
$mATBool :: forall {r}. ATerm -> (Type -> Bool -> r) -> ((# #) -> 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) -> ((# #) -> r) -> r
ATNat ty int = TNat_ ty int

pattern ATRat :: Rational -> ATerm
pattern $bATRat :: Rational -> ATerm
$mATRat :: forall {r}. ATerm -> (Rational -> r) -> ((# #) -> r) -> r
ATRat rat = TRat_ () rat

pattern ATChar :: Char -> ATerm
pattern $bATChar :: Char -> ATerm
$mATChar :: forall {r}. ATerm -> (Char -> r) -> ((# #) -> r) -> r
ATChar c = TChar_ () c

pattern ATString :: String -> ATerm
pattern $bATString :: String -> ATerm
$mATString :: forall {r}. ATerm -> (String -> r) -> ((# #) -> 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)
-> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> r) -> r
ATCase ty branch = TCase_ ty branch

pattern ATChain :: Type -> ATerm -> [ALink] -> ATerm
pattern $bATChain :: Type -> ATerm -> [Link_ TY] -> ATerm
$mATChain :: forall {r}.
ATerm -> (Type -> ATerm -> [Link_ TY] -> r) -> ((# #) -> 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) -> ((# #) -> 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)
-> ((# #) -> 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)
-> ((# #) -> 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)
-> ((# #) -> 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)
-> ((# #) -> 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 (forall a b. (a -> b) -> [a] -> [b]
map (,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) -> ((# #) -> 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 -> Link_ TY
$mATLink :: forall {r}. Link_ TY -> (BOp -> ATerm -> r) -> ((# #) -> 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) -> ((# #) -> 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) -> ((# #) -> 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)
-> ((# #) -> 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 = () -- ??? Type?

pattern AGBool :: Embed ATerm -> AGuard
pattern $bAGBool :: Embed ATerm -> AGuard
$mAGBool :: forall {r}. AGuard -> (Embed ATerm -> r) -> ((# #) -> 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) -> ((# #) -> r) -> r
AGPat embedt pat = GPat_ () embedt pat

pattern AGLet :: ABinding -> AGuard
pattern $bAGLet :: ABinding -> AGuard
$mAGLet :: forall {r}. AGuard -> (ABinding -> r) -> ((# #) -> r) -> r
AGLet b = GLet_ () b

{-# COMPLETE AGBool, AGPat, AGLet #-}

type APattern = Pattern_ TY

-- We have to use Embed Type because we don't want any type variables
-- inside the types being treated as binders!

type instance X_PVar TY = Embed Type
type instance X_PWild TY = Embed Type
type instance X_PAscr TY = Void -- No more ascriptions in typechecked patterns.
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) -> ((# #) -> r) -> r
APVar ty name <- PVar_ (unembed -> ty) name
  where
    APVar Type
ty Name ATerm
name = forall e. X_PVar e -> Name (Term_ e) -> Pattern_ e
PVar_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) Name ATerm
name

pattern APWild :: Type -> APattern
pattern $bAPWild :: Type -> APattern
$mAPWild :: forall {r}. APattern -> (Type -> r) -> ((# #) -> r) -> r
APWild ty <- PWild_ (unembed -> ty)
  where
    APWild Type
ty = forall e. X_PWild e -> Pattern_ e
PWild_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty)

pattern APUnit :: APattern
pattern $bAPUnit :: APattern
$mAPUnit :: forall {r}. APattern -> ((# #) -> r) -> ((# #) -> r) -> r
APUnit = PUnit_ ()

pattern APBool :: Bool -> APattern
pattern $bAPBool :: Bool -> APattern
$mAPBool :: forall {r}. APattern -> (Bool -> r) -> ((# #) -> r) -> r
APBool b = PBool_ () b

pattern APChar :: Char -> APattern
pattern $bAPChar :: Char -> APattern
$mAPChar :: forall {r}. APattern -> (Char -> r) -> ((# #) -> r) -> r
APChar c = PChar_ () c

pattern APString :: String -> APattern
pattern $bAPString :: String -> APattern
$mAPString :: forall {r}. APattern -> (String -> r) -> ((# #) -> r) -> r
APString s = PString_ () s

pattern APTup :: Type -> [APattern] -> APattern
pattern $bAPTup :: Type -> [APattern] -> APattern
$mAPTup :: forall {r}.
APattern -> (Type -> [APattern] -> r) -> ((# #) -> r) -> r
APTup ty lp <- PTup_ (unembed -> ty) lp
  where
    APTup Type
ty [APattern]
lp = forall e. X_PTup e -> [Pattern_ e] -> Pattern_ e
PTup_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) [APattern]
lp

pattern APInj :: Type -> Side -> APattern -> APattern
pattern $bAPInj :: Type -> Side -> APattern -> APattern
$mAPInj :: forall {r}.
APattern -> (Type -> Side -> APattern -> r) -> ((# #) -> r) -> r
APInj ty s p <- PInj_ (unembed -> ty) s p
  where
    APInj Type
ty Side
s APattern
p = forall e. X_PInj e -> Side -> Pattern_ e -> Pattern_ e
PInj_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) Side
s APattern
p

pattern APNat :: Type -> Integer -> APattern
pattern $bAPNat :: Type -> Integer -> APattern
$mAPNat :: forall {r}. APattern -> (Type -> Integer -> r) -> ((# #) -> r) -> r
APNat ty n <- PNat_ (unembed -> ty) n
  where
    APNat Type
ty Integer
n = forall e. X_PNat e -> Integer -> Pattern_ e
PNat_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) Integer
n

pattern APCons :: Type -> APattern -> APattern -> APattern
pattern $bAPCons :: Type -> APattern -> APattern -> APattern
$mAPCons :: forall {r}.
APattern
-> (Type -> APattern -> APattern -> r) -> ((# #) -> r) -> r
APCons ty p1 p2 <- PCons_ (unembed -> ty) p1 p2
  where
    APCons Type
ty APattern
p1 APattern
p2 = forall e. X_PCons e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PCons_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) APattern
p1 APattern
p2

pattern APList :: Type -> [APattern] -> APattern
pattern $bAPList :: Type -> [APattern] -> APattern
$mAPList :: forall {r}.
APattern -> (Type -> [APattern] -> r) -> ((# #) -> r) -> r
APList ty lp <- PList_ (unembed -> ty) lp
  where
    APList Type
ty [APattern]
lp = forall e. X_PList e -> [Pattern_ e] -> Pattern_ e
PList_ (forall e. IsEmbed e => Embedded e -> e
embed 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) -> ((# #) -> r) -> r
APAdd ty s p t <- PAdd_ (unembed -> ty) s p t
  where
    APAdd Type
ty Side
s APattern
p ATerm
t = forall e. X_PAdd e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PAdd_ (forall e. IsEmbed e => Embedded e -> e
embed 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) -> ((# #) -> r) -> r
APMul ty s p t <- PMul_ (unembed -> ty) s p t
  where
    APMul Type
ty Side
s APattern
p ATerm
t = forall e. X_PMul e -> Side -> Pattern_ e -> Term_ e -> Pattern_ e
PMul_ (forall e. IsEmbed e => Embedded e -> e
embed 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) -> ((# #) -> r) -> r
APSub ty p t <- PSub_ (unembed -> ty) p t
  where
    APSub Type
ty APattern
p ATerm
t = forall e. X_PSub e -> Pattern_ e -> Term_ e -> Pattern_ e
PSub_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) APattern
p ATerm
t

pattern APNeg :: Type -> APattern -> APattern
pattern $bAPNeg :: Type -> APattern -> APattern
$mAPNeg :: forall {r}.
APattern -> (Type -> APattern -> r) -> ((# #) -> r) -> r
APNeg ty p <- PNeg_ (unembed -> ty) p
  where
    APNeg Type
ty APattern
p = forall e. X_PNeg e -> Pattern_ e -> Pattern_ e
PNeg_ (forall e. IsEmbed e => Embedded e -> e
embed Type
ty) APattern
p

pattern APFrac :: Type -> APattern -> APattern -> APattern
pattern $bAPFrac :: Type -> APattern -> APattern -> APattern
$mAPFrac :: forall {r}.
APattern
-> (Type -> APattern -> APattern -> r) -> ((# #) -> r) -> r
APFrac ty p1 p2 <- PFrac_ (unembed -> ty) p1 p2
  where
    APFrac Type
ty APattern
p1 APattern
p2 = forall e. X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PFrac_ (forall e. IsEmbed e => Embedded e -> e
embed 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 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 forall a. [a] -> [a] -> [a]
++ APattern -> [(Name ATerm, Type)]
varsBound APattern
q
varsBound (APList Type
_ [APattern]
ps) = APattern -> [(Name ATerm, Type)]
varsBound 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 forall a. [a] -> [a] -> [a]
++ APattern -> [(Name ATerm, Type)]
varsBound APattern
q

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

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
_ [Link_ TY]
_) = 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 [Link_ TY]
y) = Type -> ATerm -> [Link_ TY] -> ATerm
ATChain Type
ty ATerm
x [Link_ TY]
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 = forall t. HasType t => t -> Type
getType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind

------------------------------------------------------------
-- subst
------------------------------------------------------------

substQT :: QName ATerm -> ATerm -> ATerm -> ATerm
substQT :: QName ATerm -> ATerm -> ATerm -> ATerm
substQT QName ATerm
x ATerm
s = forall a. Plated a => (a -> a) -> a -> a
transform forall a b. (a -> b) -> a -> b
$ \case
  t :: ATerm
t@(ATVar Type
_ QName ATerm
y)
    | QName ATerm
x forall a. Eq a => a -> a -> Bool
== QName ATerm
y -> ATerm
s
    | Bool
otherwise -> ATerm
t
  ATerm
t -> ATerm
t

------------------------------------------------------------
-- Exploding a typed term into a surface term with annotations
------------------------------------------------------------

instance Pretty ATerm where
  pretty :: forall (r :: EffectRow) ann.
Members '[Reader PA, LFresh] r =>
ATerm -> Sem r (Doc ann)
pretty = forall t (r :: EffectRow) ann.
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r (Doc ann)
pretty 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 (coerce :: forall a b. Coercible a b => a -> b
coerce (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 (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 (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 (forall a b. (a -> b) -> [a] -> [b]
map ABranch -> Branch
explodeBranch [ABranch]
bs)) (Type -> PolyType
toPolyType Type
ty)
  ATChain Type
ty ATerm
t [Link_ TY]
ls -> Term -> PolyType -> Term
TAscr (Term -> [Link_ UD] -> Term
TChain (ATerm -> Term
explode ATerm
t) (forall a b. (a -> b) -> [a] -> [b]
map Link_ TY -> Link_ UD
explodeLink [Link_ TY]
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 (forall a b. (a -> b) -> [a] -> [b]
map (ATerm -> Term
explode forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ATerm -> Term
explode) [(ATerm, Maybe ATerm)]
ts) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 (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 :: forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope a -> b
explodeBinder (forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> (Telescope a
xs, ATerm
at)) = forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (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 (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 (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
b) (forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
n))

explodeAbs :: Bind [APattern] ATerm -> Bind [Pattern] Term
explodeAbs :: Bind [APattern] ATerm -> Bind [Pattern] Term
explodeAbs (forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([APattern]
aps, ATerm
at)) = forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (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 (coerce :: forall a b. Coercible a b => a -> b
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 (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 (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 = forall a b.
(Alpha a, Alpha b) =>
(a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope AGuard -> Guard_ UD
explodeGuard

explodeGuard :: AGuard -> Guard
explodeGuard :: AGuard -> Guard_ UD
explodeGuard (AGBool (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Embed Term -> Guard_ UD
GBool (forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
at))
explodeGuard (AGPat (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at) APattern
ap) = Embed Term -> Pattern -> Guard_ UD
GPat (forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
at)) (APattern -> Pattern
explodePattern APattern
ap)
explodeGuard (AGLet ABinding
ab) = Binding -> Guard_ UD
GLet (ABinding -> Binding
explodeBinding ABinding
ab)

explodeLink :: ALink -> Link
explodeLink :: Link_ TY -> Link_ UD
explodeLink (ATLink BOp
bop ATerm
at) = BOp -> Term -> Link_ UD
TLink BOp
bop (ATerm -> Term
explode ATerm
at)

explodeQual :: AQual -> Qual
explodeQual :: AQual -> Qual
explodeQual (AQBind Name ATerm
x (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Name Term -> Embed Term -> Qual
QBind (coerce :: forall a b. Coercible a b => a -> b
coerce Name ATerm
x) (forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
at))
explodeQual (AQGuard (forall e. IsEmbed e => e -> Embedded e
unembed -> Embedded (Embed ATerm)
at)) = Embed Term -> Qual
QGuard (forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
at))