{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module PlutusCore.MkPlc
    ( TermLike (..)
    , UniOf
    , mkTyBuiltinOf
    , mkTyBuiltin
    , mkConstantOf
    , mkConstant
    , VarDecl (..)
    , TyVarDecl (..)
    , TyDecl (..)
    , mkVar
    , mkTyVar
    , tyDeclVar
    , Def (..)
    , embed
    , TermDef
    , TypeDef
    , FunctionType (..)
    , FunctionDef (..)
    , functionTypeToType
    , functionDefToType
    , functionDefVarDecl
    , mkFunctionDef
    , mkImmediateLamAbs
    , mkImmediateTyAbs
    , mkIterTyForall
    , mkIterTyLam
    , mkIterApp
    , mkIterTyFun
    , mkIterLamAbs
    , mkIterInst
    , mkIterTyAbs
    , mkIterTyApp
    , mkIterKindArrow
    ) where

import PlutusPrelude
import Prelude hiding (error)

import PlutusCore.Core

import Universe

-- | A final encoding for Term, to allow PLC terms to be used transparently as PIR terms.
class TermLike term tyname name uni fun | term -> tyname name uni fun where
    var      :: ann -> name -> term ann
    tyAbs    :: ann -> tyname -> Kind ann -> term ann -> term ann
    lamAbs   :: ann -> name -> Type tyname uni ann -> term ann -> term ann
    apply    :: ann -> term ann -> term ann -> term ann
    constant :: ann -> Some (ValueOf uni) -> term ann
    builtin  :: ann -> fun -> term ann
    tyInst   :: ann -> term ann -> Type tyname uni ann -> term ann
    unwrap   :: ann -> term ann -> term ann
    iWrap    :: ann -> Type tyname uni ann -> Type tyname uni ann -> term ann -> term ann
    error    :: ann -> Type tyname uni ann -> term ann
    termLet  :: ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
    typeLet  :: ann -> TypeDef tyname uni ann -> term ann -> term ann

    termLet = ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
mkImmediateLamAbs
    typeLet = ann -> TypeDef tyname uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TypeDef tyname uni ann -> term ann -> term ann
mkImmediateTyAbs

-- TODO: make it @forall {k}@ once we have that.
-- (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0099-explicit-specificity.rst)
-- | Embed a type (given its explicit type tag) into a PLC type.
mkTyBuiltinOf :: forall k (a :: k) uni tyname ann. ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf :: ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf ann
ann = ann -> SomeTypeIn uni -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin ann
ann (SomeTypeIn uni -> Type tyname uni ann)
-> (uni (Esc a) -> SomeTypeIn uni)
-> uni (Esc a)
-> Type tyname uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> SomeTypeIn uni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn

-- TODO: make it @forall {k}@ once we have that.
-- (see https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0099-explicit-specificity.rst)
-- | Embed a type (provided it's in the universe) into a PLC type.
mkTyBuiltin
    :: forall k (a :: k) uni tyname ann. uni `Contains` a
    => ann -> Type tyname uni ann
mkTyBuiltin :: ann -> Type tyname uni ann
mkTyBuiltin ann
ann = ann -> uni (Esc a) -> Type tyname uni ann
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf ann
ann (uni (Esc a) -> Type tyname uni ann)
-> uni (Esc a) -> Type tyname uni ann
forall a b. (a -> b) -> a -> b
$ Contains uni a => uni (Esc a)
forall k (uni :: * -> *) (a :: k). Contains uni a => uni (Esc a)
knownUni @_ @uni @a

-- | Embed a Haskell value (given its explicit type tag) into a PLC term.
mkConstantOf
    :: forall a uni fun term tyname name ann. TermLike term tyname name uni fun
    => ann -> uni (Esc a) -> a -> term ann
mkConstantOf :: ann -> uni (Esc a) -> a -> term ann
mkConstantOf ann
ann uni (Esc a)
uni = ann -> Some (ValueOf uni) -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Some (ValueOf uni) -> term ann
constant ann
ann (Some (ValueOf uni) -> term ann)
-> (a -> Some (ValueOf uni)) -> a -> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. uni (Esc a) -> a -> Some (ValueOf uni)
forall a (uni :: * -> *). uni (Esc a) -> a -> Some (ValueOf uni)
someValueOf uni (Esc a)
uni

-- | Embed a Haskell value (provided its type is in the universe) into a PLC term.
mkConstant
    :: forall a uni fun term tyname name ann. (TermLike term tyname name uni fun, uni `Includes` a)
    => ann -> a -> term ann
mkConstant :: ann -> a -> term ann
mkConstant ann
ann = ann -> Some (ValueOf uni) -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Some (ValueOf uni) -> term ann
constant ann
ann (Some (ValueOf uni) -> term ann)
-> (a -> Some (ValueOf uni)) -> a -> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Some (ValueOf uni)
forall a (uni :: * -> *). Includes uni a => a -> Some (ValueOf uni)
someValue

instance TermLike (Term tyname name uni fun) tyname name uni fun where
    var :: ann -> name -> Term tyname name uni fun ann
var      = ann -> name -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> name -> Term tyname name uni fun ann
Var
    tyAbs :: ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
tyAbs    = ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> tyname
-> Kind ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
TyAbs
    lamAbs :: ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
lamAbs   = ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> name
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
LamAbs
    apply :: ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
apply    = ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
Apply
    constant :: ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
constant = ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Some (ValueOf uni) -> Term tyname name uni fun ann
Constant
    builtin :: ann -> fun -> Term tyname name uni fun ann
builtin  = ann -> fun -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> fun -> Term tyname name uni fun ann
Builtin
    tyInst :: ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
tyInst   = ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
TyInst
    unwrap :: ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
unwrap   = ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Term tyname name uni fun ann -> Term tyname name uni fun ann
Unwrap
    iWrap :: ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
iWrap    = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> Term tyname name uni fun ann
IWrap
    error :: ann -> Type tyname uni ann -> Term tyname name uni fun ann
error    = ann -> Type tyname uni ann -> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann -> Type tyname uni ann -> Term tyname name uni fun ann
Error

embed :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
embed :: Term tyname name uni fun ann -> term ann
embed = \case
    Var ann
a name
n           -> ann -> name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
a name
n
    TyAbs ann
a tyname
tn Kind ann
k Term tyname name uni fun ann
t    -> ann -> tyname -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs ann
a tyname
tn Kind ann
k (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t)
    LamAbs ann
a name
n Type tyname uni ann
ty Term tyname name uni fun ann
t   -> ann -> name -> Type tyname uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
a name
n Type tyname uni ann
ty (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t)
    Apply ann
a Term tyname name uni fun ann
t1 Term tyname name uni fun ann
t2     -> ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
a (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t1) (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t2)
    Constant ann
a Some (ValueOf uni)
c      -> ann -> Some (ValueOf uni) -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Some (ValueOf uni) -> term ann
constant ann
a Some (ValueOf uni)
c
    Builtin ann
a fun
bi      -> ann -> fun -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
builtin ann
a fun
bi
    TyInst ann
a Term tyname name uni fun ann
t Type tyname uni ann
ty     -> ann -> term ann -> Type tyname uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst ann
a (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t) Type tyname uni ann
ty
    Error ann
a Type tyname uni ann
ty        -> ann -> Type tyname uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> term ann
error ann
a Type tyname uni ann
ty
    Unwrap ann
a Term tyname name uni fun ann
t        -> ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
unwrap ann
a (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t)
    IWrap ann
a Type tyname uni ann
ty1 Type tyname uni ann
ty2 Term tyname name uni fun ann
t -> ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
iWrap ann
a Type tyname uni ann
ty1 Type tyname uni ann
ty2 (Term tyname name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embed Term tyname name uni fun ann
t)

-- | Make a 'Var' referencing the given 'VarDecl'.
mkVar :: TermLike term tyname name uni fun => ann -> VarDecl tyname name uni fun ann -> term ann
mkVar :: ann -> VarDecl tyname name uni fun ann -> term ann
mkVar ann
ann = ann -> name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann (name -> term ann)
-> (VarDecl tyname name uni fun ann -> name)
-> VarDecl tyname name uni fun ann
-> term ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarDecl tyname name uni fun ann -> name
forall tyname name (uni :: * -> *) k (fun :: k) ann.
VarDecl tyname name uni fun ann -> name
_varDeclName

-- | Make a 'TyVar' referencing the given 'TyVarDecl'.
mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar ann
ann = ann -> tyname -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann (tyname -> Type tyname uni ann)
-> (TyVarDecl tyname ann -> tyname)
-> TyVarDecl tyname ann
-> Type tyname uni ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TyVarDecl tyname ann -> tyname
forall tyname ann. TyVarDecl tyname ann -> tyname
_tyVarDeclName

-- | A definition. Pretty much just a pair with more descriptive names.
data Def var val = Def
    { Def var val -> var
defVar :: var
    , Def var val -> val
defVal :: val
    } deriving stock (Int -> Def var val -> ShowS
[Def var val] -> ShowS
Def var val -> String
(Int -> Def var val -> ShowS)
-> (Def var val -> String)
-> ([Def var val] -> ShowS)
-> Show (Def var val)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall var val. (Show var, Show val) => Int -> Def var val -> ShowS
forall var val. (Show var, Show val) => [Def var val] -> ShowS
forall var val. (Show var, Show val) => Def var val -> String
showList :: [Def var val] -> ShowS
$cshowList :: forall var val. (Show var, Show val) => [Def var val] -> ShowS
show :: Def var val -> String
$cshow :: forall var val. (Show var, Show val) => Def var val -> String
showsPrec :: Int -> Def var val -> ShowS
$cshowsPrec :: forall var val. (Show var, Show val) => Int -> Def var val -> ShowS
Show, Def var val -> Def var val -> Bool
(Def var val -> Def var val -> Bool)
-> (Def var val -> Def var val -> Bool) -> Eq (Def var val)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall var val.
(Eq var, Eq val) =>
Def var val -> Def var val -> Bool
/= :: Def var val -> Def var val -> Bool
$c/= :: forall var val.
(Eq var, Eq val) =>
Def var val -> Def var val -> Bool
== :: Def var val -> Def var val -> Bool
$c== :: forall var val.
(Eq var, Eq val) =>
Def var val -> Def var val -> Bool
Eq, Eq (Def var val)
Eq (Def var val)
-> (Def var val -> Def var val -> Ordering)
-> (Def var val -> Def var val -> Bool)
-> (Def var val -> Def var val -> Bool)
-> (Def var val -> Def var val -> Bool)
-> (Def var val -> Def var val -> Bool)
-> (Def var val -> Def var val -> Def var val)
-> (Def var val -> Def var val -> Def var val)
-> Ord (Def var val)
Def var val -> Def var val -> Bool
Def var val -> Def var val -> Ordering
Def var val -> Def var val -> Def var val
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall var val. (Ord var, Ord val) => Eq (Def var val)
forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Bool
forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Ordering
forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Def var val
min :: Def var val -> Def var val -> Def var val
$cmin :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Def var val
max :: Def var val -> Def var val -> Def var val
$cmax :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Def var val
>= :: Def var val -> Def var val -> Bool
$c>= :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Bool
> :: Def var val -> Def var val -> Bool
$c> :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Bool
<= :: Def var val -> Def var val -> Bool
$c<= :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Bool
< :: Def var val -> Def var val -> Bool
$c< :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Bool
compare :: Def var val -> Def var val -> Ordering
$ccompare :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Ordering
$cp1Ord :: forall var val. (Ord var, Ord val) => Eq (Def var val)
Ord, (forall x. Def var val -> Rep (Def var val) x)
-> (forall x. Rep (Def var val) x -> Def var val)
-> Generic (Def var val)
forall x. Rep (Def var val) x -> Def var val
forall x. Def var val -> Rep (Def var val) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall var val x. Rep (Def var val) x -> Def var val
forall var val x. Def var val -> Rep (Def var val) x
$cto :: forall var val x. Rep (Def var val) x -> Def var val
$cfrom :: forall var val x. Def var val -> Rep (Def var val) x
Generic)

-- | A term definition as a variable.
type TermDef term tyname name uni fun ann = Def (VarDecl tyname name uni fun ann) (term ann)
-- | A type definition as a type variable.
type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann)

-- | The type of a PLC function.
data FunctionType tyname uni ann = FunctionType
    { FunctionType tyname uni ann -> ann
_functionTypeAnn :: ann                  -- ^ An annotation.
    , FunctionType tyname uni ann -> Type tyname uni ann
_functionTypeDom :: Type tyname uni ann  -- ^ The domain of a function.
    , FunctionType tyname uni ann -> Type tyname uni ann
_functionTypeCod :: Type tyname uni ann  -- ^ The codomain of the function.
    }

-- Should we parameterize 'VarDecl' by @ty@ rather than @tyname@, so that we can define
-- 'FunctionDef' as 'TermDef FunctionType tyname name uni fun ann'?
-- Perhaps we even should define general 'Decl' and 'Def' that cover all of the cases?
-- | A PLC function.
data FunctionDef term tyname name uni fun ann = FunctionDef
    { FunctionDef term tyname name uni fun ann -> ann
_functionDefAnn  :: ann                          -- ^ An annotation.
    , FunctionDef term tyname name uni fun ann -> name
_functionDefName :: name                         -- ^ The name of a function.
    , FunctionDef term tyname name uni fun ann
-> FunctionType tyname uni ann
_functionDefType :: FunctionType tyname uni ann  -- ^ The type of the function.
    , FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm :: term ann                     -- ^ The definition of the function.
    }

-- | Convert a 'FunctionType' to the corresponding 'Type'.
functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann
functionTypeToType :: FunctionType tyname uni ann -> Type tyname uni ann
functionTypeToType (FunctionType ann
ann Type tyname uni ann
dom Type tyname uni ann
cod) = ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann Type tyname uni ann
dom Type tyname uni ann
cod

-- | Get the type of a 'FunctionDef'.
functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefToType :: FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefToType (FunctionDef ann
_ name
_ FunctionType tyname uni ann
funTy term ann
_) = FunctionType tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> Type tyname uni ann
functionTypeToType FunctionType tyname uni ann
funTy

-- | Convert a 'FunctionDef' to a 'VarDecl'. I.e. ignore the actual term.
functionDefVarDecl :: FunctionDef term tyname name uni fun ann -> VarDecl tyname name uni fun ann
functionDefVarDecl :: FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni fun ann
functionDefVarDecl (FunctionDef ann
ann name
name FunctionType tyname uni ann
funTy term ann
_) = ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl ann
ann name
name (Type tyname uni ann -> VarDecl tyname name uni fun ann)
-> Type tyname uni ann -> VarDecl tyname name uni fun ann
forall a b. (a -> b) -> a -> b
$ FunctionType tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> Type tyname uni ann
functionTypeToType FunctionType tyname uni ann
funTy

-- | Make a 'FunctionDef'. Return 'Nothing' if the provided type is not functional.
mkFunctionDef
    :: ann
    -> name
    -> Type tyname uni ann
    -> term ann
    -> Maybe (FunctionDef term tyname name uni fun ann)
mkFunctionDef :: ann
-> name
-> Type tyname uni ann
-> term ann
-> Maybe (FunctionDef term tyname name uni fun ann)
mkFunctionDef ann
annName name
name (TyFun ann
annTy Type tyname uni ann
dom Type tyname uni ann
cod) term ann
term =
    FunctionDef term tyname name uni fun ann
-> Maybe (FunctionDef term tyname name uni fun ann)
forall a. a -> Maybe a
Just (FunctionDef term tyname name uni fun ann
 -> Maybe (FunctionDef term tyname name uni fun ann))
-> FunctionDef term tyname name uni fun ann
-> Maybe (FunctionDef term tyname name uni fun ann)
forall a b. (a -> b) -> a -> b
$ ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
forall k (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
ann
-> name
-> FunctionType tyname uni ann
-> term ann
-> FunctionDef term tyname name uni fun ann
FunctionDef ann
annName name
name (ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> FunctionType tyname uni ann
FunctionType ann
annTy Type tyname uni ann
dom Type tyname uni ann
cod) term ann
term
mkFunctionDef ann
_       name
_    Type tyname uni ann
_                     term ann
_    = Maybe (FunctionDef term tyname name uni fun ann)
forall a. Maybe a
Nothing

-- | Make a "let-binding" for a term as an immediately applied lambda abstraction.
mkImmediateLamAbs
    :: TermLike term tyname name uni fun
    => ann
    -> TermDef term tyname name uni fun ann
    -> term ann -- ^ The body of the let, possibly referencing the name.
    -> term ann
mkImmediateLamAbs :: ann -> TermDef term tyname name uni fun ann -> term ann -> term ann
mkImmediateLamAbs ann
ann1 (Def (VarDecl ann
ann2 name
name Type tyname uni ann
ty) term ann
bind) term ann
body =
    ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann1 (ann -> name -> Type tyname uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
ann2 name
name Type tyname uni ann
ty term ann
body) term ann
bind

-- | Make a "let-binding" for a type as an immediately instantiated type abstraction. Note: the body must be a value.
mkImmediateTyAbs
    :: TermLike term tyname name uni fun
    => ann
    -> TypeDef tyname uni ann
    -> term ann -- ^ The body of the let, possibly referencing the name.
    -> term ann
mkImmediateTyAbs :: ann -> TypeDef tyname uni ann -> term ann -> term ann
mkImmediateTyAbs ann
ann1 (Def (TyVarDecl ann
ann2 tyname
name Kind ann
k) Type tyname uni ann
bind) term ann
body =
    ann -> term ann -> Type tyname uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst ann
ann1 (ann -> tyname -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs ann
ann2 tyname
name Kind ann
k term ann
body) Type tyname uni ann
bind

-- | Make an iterated application.
mkIterApp
    :: TermLike term tyname name uni fun
    => ann
    -> term ann -- ^ @f@
    -> [term ann] -- ^@[ x0 ... xn ]@
    -> term ann -- ^ @[f x0 ... xn ]@
mkIterApp :: ann -> term ann -> [term ann] -> term ann
mkIterApp ann
ann = (term ann -> term ann -> term ann)
-> term ann -> [term ann] -> term ann
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (ann -> term ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply ann
ann)

-- | Make an iterated instantiation.
mkIterInst
    :: TermLike term tyname name uni fun
    => ann
    -> term ann -- ^ @a@
    -> [Type tyname uni ann] -- ^ @ [ x0 ... xn ] @
    -> term ann -- ^ @{ a x0 ... xn }@
mkIterInst :: ann -> term ann -> [Type tyname uni ann] -> term ann
mkIterInst ann
ann = (term ann -> Type tyname uni ann -> term ann)
-> term ann -> [Type tyname uni ann] -> term ann
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (ann -> term ann -> Type tyname uni ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst ann
ann)

-- | Lambda abstract a list of names.
mkIterLamAbs
    :: TermLike term tyname name uni fun
    => [VarDecl tyname name uni fun ann]
    -> term ann
    -> term ann
mkIterLamAbs :: [VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [VarDecl tyname name uni fun ann]
args term ann
body =
    (VarDecl tyname name uni fun ann -> term ann -> term ann)
-> term ann -> [VarDecl tyname name uni fun ann] -> term ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(VarDecl ann
ann name
name Type tyname uni ann
ty) term ann
acc -> ann -> name -> Type tyname uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs ann
ann name
name Type tyname uni ann
ty term ann
acc) term ann
body [VarDecl tyname name uni fun ann]
args

-- | Type abstract a list of names.
mkIterTyAbs
    :: TermLike term tyname name uni fun
    => [TyVarDecl tyname ann]
    -> term ann
    -> term ann
mkIterTyAbs :: [TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyAbs [TyVarDecl tyname ann]
args term ann
body =
    (TyVarDecl tyname ann -> term ann -> term ann)
-> term ann -> [TyVarDecl tyname ann] -> term ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(TyVarDecl ann
ann tyname
name Kind ann
kind) term ann
acc -> ann -> tyname -> Kind ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs ann
ann tyname
name Kind ann
kind term ann
acc) term ann
body [TyVarDecl tyname ann]
args

-- | Make an iterated type application.
mkIterTyApp
    :: ann
    -> Type tyname uni ann -- ^ @f@
    -> [Type tyname uni ann] -- ^ @[ x0 ... xn ]@
    -> Type tyname uni ann -- ^ @[ f x0 ... xn ]@
mkIterTyApp :: ann
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
mkIterTyApp ann
ann = (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp ann
ann)

-- | Make an iterated function type.
mkIterTyFun
    :: ann
    -> [Type tyname uni ann]
    -> Type tyname uni ann
    -> Type tyname uni ann
mkIterTyFun :: ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun ann
ann [Type tyname uni ann]
tys Type tyname uni ann
target = (Type tyname uni ann -> Type tyname uni ann -> Type tyname uni ann)
-> Type tyname uni ann
-> [Type tyname uni ann]
-> Type tyname uni ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Type tyname uni ann
ty Type tyname uni ann
acc -> ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun ann
ann Type tyname uni ann
ty Type tyname uni ann
acc) Type tyname uni ann
target [Type tyname uni ann]
tys

-- | Universally quantify a list of names.
mkIterTyForall
    :: [TyVarDecl tyname ann]
    -> Type tyname uni ann
    -> Type tyname uni ann
mkIterTyForall :: [TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyForall [TyVarDecl tyname ann]
args Type tyname uni ann
body =
    (TyVarDecl tyname ann
 -> Type tyname uni ann -> Type tyname uni ann)
-> Type tyname uni ann
-> [TyVarDecl tyname ann]
-> Type tyname uni ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(TyVarDecl ann
ann tyname
name Kind ann
kind) Type tyname uni ann
acc -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall ann
ann tyname
name Kind ann
kind Type tyname uni ann
acc) Type tyname uni ann
body [TyVarDecl tyname ann]
args

-- | Lambda abstract a list of names.
mkIterTyLam
    :: [TyVarDecl tyname ann]
    -> Type tyname uni ann
    -> Type tyname uni ann
mkIterTyLam :: [TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyLam [TyVarDecl tyname ann]
args Type tyname uni ann
body =
    (TyVarDecl tyname ann
 -> Type tyname uni ann -> Type tyname uni ann)
-> Type tyname uni ann
-> [TyVarDecl tyname ann]
-> Type tyname uni ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(TyVarDecl ann
ann tyname
name Kind ann
kind) Type tyname uni ann
acc -> ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam ann
ann tyname
name Kind ann
kind Type tyname uni ann
acc) Type tyname uni ann
body [TyVarDecl tyname ann]
args

-- | Make an iterated function kind.
mkIterKindArrow
    :: ann
    -> [Kind ann]
    -> Kind ann
    -> Kind ann
mkIterKindArrow :: ann -> [Kind ann] -> Kind ann -> Kind ann
mkIterKindArrow ann
ann [Kind ann]
kinds Kind ann
target = (Kind ann -> Kind ann -> Kind ann)
-> Kind ann -> [Kind ann] -> Kind ann
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (ann -> Kind ann -> Kind ann -> Kind ann
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow ann
ann) Kind ann
target [Kind ann]
kinds