{-# 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
DataType
Typeable TY
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> TY -> c TY)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c TY)
-> (TY -> Constr)
-> (TY -> DataType)
-> (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))
-> ((forall b. Data b => b -> b) -> TY -> TY)
-> (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 u. (forall d. Data d => d -> u) -> TY -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> TY -> u)
-> (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 (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> TY -> m TY)
-> Data TY
TY -> DataType
TY -> Constr
(forall b. Data b => b -> b) -> TY -> TY
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> TY -> c TY
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c 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)
$tTY :: DataType
gmapMo :: (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 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 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 :: Int -> (forall d. Data d => d -> u) -> TY -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> TY -> u
gmapQ :: (forall d. Data d => d -> u) -> TY -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> TY -> [u]
gmapQr :: (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 :: (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 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 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 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 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
$cp1Data :: Typeable 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) -> (Void# -> 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) -> (Void# -> 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)
-> (Void# -> r)
-> r
ATLet ty bind = TLet_ ty bind

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

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

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

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

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

pattern ATChain :: Type -> ATerm -> [ALink] -> ATerm
pattern $bATChain :: Type -> ATerm -> [ALink] -> ATerm
$mATChain :: forall r.
ATerm -> (Type -> ATerm -> [ALink] -> r) -> (Void# -> 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) -> (Void# -> 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)
-> (Void# -> 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)
-> (Void# -> 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)
-> (Void# -> 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)
-> (Void# -> 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 ((ATerm -> (ATerm, Maybe ATerm))
-> [ATerm] -> [(ATerm, Maybe ATerm)]
forall a b. (a -> b) -> [a] -> [b]
map (,Maybe ATerm
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) -> (Void# -> 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 -> ALink
$mATLink :: forall r. ALink -> (BOp -> ATerm -> r) -> (Void# -> 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) -> (Void# -> 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) -> (Void# -> 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)
-> (Void# -> 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) -> (Void# -> 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) -> (Void# -> r) -> r
AGPat embedt pat = GPat_ () embedt pat

pattern AGLet :: ABinding -> AGuard
pattern $bAGLet :: ABinding -> AGuard
$mAGLet :: forall r. AGuard -> (ABinding -> r) -> (Void# -> 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) -> (Void# -> r) -> r
APVar ty name <- PVar_ (unembed -> ty) name
  where
    APVar Type
ty Name ATerm
name = X_PVar TY -> Name ATerm -> APattern
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 ATerm
name

pattern APWild :: Type -> APattern
pattern $bAPWild :: Type -> APattern
$mAPWild :: forall r. APattern -> (Type -> r) -> (Void# -> r) -> r
APWild ty <- PWild_ (unembed -> ty)
  where
    APWild Type
ty = X_PWild TY -> APattern
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 APUnit :: APattern
pattern $bAPUnit :: APattern
$mAPUnit :: forall r. APattern -> (Void# -> r) -> (Void# -> r) -> r
APUnit = PUnit_ ()

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

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

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

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

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

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

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

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

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

pattern APFrac :: Type -> APattern -> APattern -> APattern
pattern $bAPFrac :: Type -> APattern -> APattern -> APattern
$mAPFrac :: forall r.
APattern
-> (Type -> APattern -> APattern -> r) -> (Void# -> r) -> r
APFrac ty p1 p2 <- PFrac_ (unembed -> ty) p1 p2
  where
    APFrac Type
ty APattern
p1 APattern
p2 = X_PFrac TY -> APattern -> APattern -> APattern
forall e. X_PFrac e -> Pattern_ e -> Pattern_ e -> Pattern_ e
PFrac_ (Embedded (Embed Type) -> Embed Type
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Type)
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 (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
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 [(Name ATerm, Type)]
-> [(Name ATerm, Type)] -> [(Name ATerm, Type)]
forall a. [a] -> [a] -> [a]
++ APattern -> [(Name ATerm, Type)]
varsBound APattern
q
varsBound (APList Type
_ [APattern]
ps)   = APattern -> [(Name ATerm, Type)]
varsBound (APattern -> [(Name ATerm, Type)])
-> [APattern] -> [(Name ATerm, Type)]
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 [(Name ATerm, Type)]
-> [(Name ATerm, Type)] -> [(Name ATerm, Type)]
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
_ [ALink]
_)         = 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 [ALink]
y  )       = Type -> ATerm -> [ALink] -> ATerm
ATChain Type
ty ATerm
x [ALink]
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 = ATerm -> Type
forall t. HasType t => t -> Type
getType (ATerm -> Type) -> (ABranch -> ATerm) -> ABranch -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Telescope AGuard, ATerm) -> ATerm
forall a b. (a, b) -> b
snd ((Telescope AGuard, ATerm) -> ATerm)
-> (ABranch -> (Telescope AGuard, ATerm)) -> ABranch -> ATerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ABranch -> (Telescope AGuard, ATerm)
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 = (ATerm -> ATerm) -> ATerm -> ATerm
forall a. Plated a => (a -> a) -> a -> a
transform ((ATerm -> ATerm) -> ATerm -> ATerm)
-> (ATerm -> ATerm) -> ATerm -> ATerm
forall a b. (a -> b) -> a -> b
$ \case
  t :: ATerm
t@(ATVar Type
_ QName ATerm
y)
    | QName ATerm
x QName ATerm -> QName ATerm -> Bool
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 :: ATerm -> Sem r Doc
pretty = Term -> Sem r Doc
forall t (r :: EffectRow).
(Pretty t, Members '[Reader PA, LFresh] r) =>
t -> Sem r Doc
pretty (Term -> Sem r Doc) -> (ATerm -> Term) -> ATerm -> Sem r Doc
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 (Name ATerm -> Name Term
coerce (QName ATerm -> Name ATerm
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 ((ABinding -> Binding)
-> Bind (Telescope ABinding) ATerm -> Bind (Telescope Binding) Term
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 ((ATerm -> Term) -> [ATerm] -> [Term]
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 ((ABranch -> Branch) -> [ABranch] -> [Branch]
forall a b. (a -> b) -> [a] -> [b]
map ABranch -> Branch
explodeBranch [ABranch]
bs)) (Type -> PolyType
toPolyType Type
ty)
  ATChain Type
ty ATerm
t [ALink]
ls        -> Term -> PolyType -> Term
TAscr (Term -> [Link] -> Term
TChain (ATerm -> Term
explode ATerm
t) ((ALink -> Link) -> [ALink] -> [Link]
forall a b. (a -> b) -> [a] -> [b]
map ALink -> Link
explodeLink [ALink]
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 (((ATerm, Maybe ATerm) -> (Term, Maybe Term))
-> [(ATerm, Maybe ATerm)] -> [(Term, Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map (ATerm -> Term
explode (ATerm -> Term)
-> (Maybe ATerm -> Maybe Term)
-> (ATerm, Maybe ATerm)
-> (Term, Maybe Term)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (ATerm -> Term) -> Maybe ATerm -> Maybe Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ATerm -> Term
explode) [(ATerm, Maybe ATerm)]
ts) ((Ellipsis ATerm -> Ellipsis Term)
-> Maybe (Ellipsis ATerm) -> Maybe (Ellipsis Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ATerm -> Term) -> Ellipsis ATerm -> Ellipsis Term
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 ((AQual -> Qual)
-> Bind (Telescope AQual) ATerm -> Bind (Telescope Qual) Term
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 :: (a -> b) -> Bind (Telescope a) ATerm -> Bind (Telescope b) Term
explodeTelescope a -> b
explodeBinder (Bind (Telescope a) ATerm -> (Telescope a, ATerm)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> (Telescope a
xs,ATerm
at)) = Telescope b -> Term -> Bind (Telescope b) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ((a -> b) -> Telescope a -> Telescope b
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 (Embed ATerm -> Embedded (Embed ATerm)
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 (Name ATerm -> Name Term
coerce Name ATerm
b) (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (ATerm -> Term
explode Embedded (Embed ATerm)
ATerm
n))

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

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

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

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