-- editorconfig-checker-disable-file
{-# LANGUAGE AllowAmbiguousTypes    #-}
{-# LANGUAGE ConstraintKinds        #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE OverloadedStrings      #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE TupleSections          #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

module PlutusCore.MkPlc
    ( TermLike (..)
    , UniOf
    , HasTypeLevel
    , HasTermLevel
    , HasTypeAndTermLevel
    , mkTyBuiltinOf
    , mkTyBuiltin
    , mkConstantOf
    , mkConstant
    , VarDecl (..)
    , TyVarDecl (..)
    , TyDecl (..)
    , mkVar
    , mkTyVar
    , tyDeclVar
    , Def (..)
    , embedTerm
    , TermDef
    , TypeDef
    , FunctionType (..)
    , FunctionDef (..)
    , functionTypeToType
    , functionDefToType
    , functionDefVarDecl
    , mkFunctionDef
    , mkImmediateLamAbs
    , mkImmediateTyAbs
    , mkIterTyForall
    , mkIterTyLam
    , mkIterApp
    , mkIterAppNoAnn
    , (@@)
    , mkIterTyFun
    , mkIterLamAbs
    , mkIterInst
    , mkIterInstNoAnn
    , mkIterTyAbs
    , mkIterTyApp
    , mkIterTyAppNoAnn
    , mkIterKindArrow
    , mkFreshTermLet
    , headSpineToTerm
    ) where

import PlutusPrelude
import Prelude hiding (error)

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Name.Unique
import PlutusCore.Quote

import Data.Word
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
    constr   :: ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
    kase     :: ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann

    termLet  :: ann -> TermDef term tyname name uni ann -> term ann -> term ann
    typeLet  :: ann -> TypeDef tyname uni ann -> term ann -> term ann

    termLet = ann -> TermDef term tyname name uni ann -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni 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 :: forall k (a :: k) (uni :: * -> *) tyname ann.
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

-- | 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 :: forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
TermLike term tyname name uni fun =>
ann -> uni (Esc a) -> a -> term ann
mkConstantOf ann
ann uni (Esc a)
uni = ann -> Some (ValueOf uni) -> term ann
forall 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
. 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 `HasTermLevel` a)
    => ann -> a -> term ann
mkConstant :: forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
(TermLike term tyname name uni fun, HasTermLevel uni a) =>
ann -> a -> term ann
mkConstant ann
ann = ann -> Some (ValueOf uni) -> term ann
forall 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 :: * -> *). Contains uni a => a -> Some (ValueOf uni)
someValue

instance TermLike (Term tyname name uni fun) tyname name uni fun where
    var :: forall ann. 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 :: forall ann.
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 :: forall ann.
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 :: forall ann.
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 :: forall ann.
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 :: forall ann. 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 :: forall ann.
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 :: forall ann.
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 :: forall ann.
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 :: forall ann.
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
    constr :: forall ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
constr   = ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
forall tyname name (uni :: * -> *) fun ann.
ann
-> Type tyname uni ann
-> Word64
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Constr
    kase :: forall ann.
ann
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
kase     = ann
-> Type tyname uni 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
-> Type tyname uni ann
-> Term tyname name uni fun ann
-> [Term tyname name uni fun ann]
-> Term tyname name uni fun ann
Case

embedTerm :: TermLike term tyname name uni fun => Term tyname name uni fun ann -> term ann
embedTerm :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
Term tyname name uni fun ann -> term ann
embedTerm = \case
    Var ann
a name
n           -> ann -> name -> term ann
forall ann. 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 ann. 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
embedTerm 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 ann.
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
embedTerm 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 ann. 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
embedTerm 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
embedTerm Term tyname name uni fun ann
t2)
    Constant ann
a Some (ValueOf uni)
c      -> ann -> Some (ValueOf uni) -> term ann
forall 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
a Some (ValueOf uni)
c
    Builtin ann
a fun
bi      -> ann -> fun -> term ann
forall ann. 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 ann. 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
embedTerm 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 ann. 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 ann. 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
embedTerm 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 ann.
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
embedTerm Term tyname name uni fun ann
t)
    Constr ann
a Type tyname uni ann
ty Word64
i [Term tyname name uni fun ann]
es  -> ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
forall ann.
ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
constr ann
a Type tyname uni ann
ty Word64
i ((Term tyname name uni fun ann -> term ann)
-> [Term tyname name uni fun ann] -> [term ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
embedTerm [Term tyname name uni fun ann]
es)
    Case ann
a Type tyname uni ann
ty Term tyname name uni fun ann
arg [Term tyname name uni fun ann]
cs  -> ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
forall ann.
ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
kase ann
a 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
embedTerm Term tyname name uni fun ann
arg) ((Term tyname name uni fun ann -> term ann)
-> [Term tyname name uni fun ann] -> [term ann]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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
embedTerm [Term tyname name uni fun ann]
cs)

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

-- | Make a 'TyVar' referencing the given 'TyVarDecl'.
mkTyVar :: ann -> TyVarDecl tyname ann -> Type tyname uni ann
mkTyVar :: forall ann tyname (uni :: * -> *).
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
    { forall var val. Def var val -> var
defVar :: var
    , forall var val. 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
$cshowsPrec :: forall var val. (Show var, Show val) => Int -> Def var val -> ShowS
showsPrec :: Int -> Def var val -> ShowS
$cshow :: forall var val. (Show var, Show val) => Def var val -> String
show :: Def var val -> String
$cshowList :: forall var val. (Show var, Show val) => [Def var val] -> ShowS
showList :: [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
$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
/= :: 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
$ccompare :: forall var val.
(Ord var, Ord val) =>
Def var val -> Def var val -> Ordering
compare :: Def var val -> Def var val -> Ordering
$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
>= :: Def var val -> Def var val -> Bool
$cmax :: 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
$cmin :: 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
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
$cfrom :: forall var val x. Def var val -> Rep (Def var val) x
from :: forall x. Def var val -> Rep (Def var val) x
$cto :: forall var val x. Rep (Def var val) x -> Def var val
to :: forall x. Rep (Def var val) x -> Def var val
Generic)

-- | A term definition as a variable.
type TermDef term tyname name uni ann = Def (VarDecl tyname name uni 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
    { forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> ann
_functionTypeAnn :: ann                  -- ^ An annotation.
    , forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> Type tyname uni ann
_functionTypeDom :: Type tyname uni ann  -- ^ The domain of a function.
    , forall tyname (uni :: * -> *) ann.
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
    { forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> ann
_functionDefAnn  :: ann                          -- ^ An annotation.
    , forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> name
_functionDefName :: name                         -- ^ The name of a function.
    , forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> FunctionType tyname uni ann
_functionDefType :: FunctionType tyname uni ann  -- ^ The type of the function.
    , forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
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 :: forall tyname (uni :: * -> *) ann.
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 :: forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
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 ann
functionDefVarDecl :: forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni ann
functionDefVarDecl (FunctionDef ann
ann name
name FunctionType tyname uni ann
funTy term ann
_) = ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl ann
ann name
name (Type tyname uni ann -> VarDecl tyname name uni ann)
-> Type tyname uni ann -> VarDecl tyname name uni 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 :: forall {k} ann name tyname (uni :: * -> *) (term :: * -> *)
       (fun :: k).
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 ann
    -> term ann -- ^ The body of the let, possibly referencing the name.
    -> term ann
mkImmediateLamAbs :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni 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 ann. 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 ann.
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 :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
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 ann. 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 ann. 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. Each `apply` node uses the annotation associated with
-- the corresponding argument.
mkIterApp
    :: TermLike term tyname name uni fun
    => term ann
    -> [(ann, term ann)]
    -> term ann
mkIterApp :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp = (term ann -> (ann, term ann) -> term ann)
-> term ann -> [(ann, term ann)] -> term ann
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((term ann -> (ann, term ann) -> term ann)
 -> term ann -> [(ann, term ann)] -> term ann)
-> (term ann -> (ann, term ann) -> term ann)
-> term ann
-> [(ann, term ann)]
-> term ann
forall a b. (a -> b) -> a -> b
$ \term ann
acc (ann
ann, term ann
arg) -> ann -> term ann -> term ann -> term ann
forall ann. 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 term ann
acc term ann
arg

-- | Make an iterated application with no annotation.
mkIterAppNoAnn
    :: TermLike term tyname name uni fun
    => term () -- ^ @f@
    -> [term ()] -- ^ @[ x0 ... xn ]@
    -> term () -- ^ @[f x0 ... xn ]@
mkIterAppNoAnn :: forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn term ()
term = term () -> [((), term ())] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp term ()
term ([((), term ())] -> term ())
-> ([term ()] -> [((), term ())]) -> [term ()] -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (term () -> ((), term ())) -> [term ()] -> [((), term ())]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((),)

-- | An infix synonym for `mkIterAppNoAnn`
(@@) :: TermLike term tyname name uni fun
     => term () -- ^ @f@
     -> [term ()] -- ^ @[ x0 ... xn ]@
     -> term () -- ^ @[f x0 ... xn ]@
@@ :: forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
(@@) = term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn

-- | Make an iterated instantiation. Each `tyInst` node uses the annotation associated with
-- the corresponding argument.
mkIterInst
    :: TermLike term tyname name uni fun
    => term ann -- ^ @a@
    -> [(ann, Type tyname uni ann)] -- ^ @ [ x0 ... xn ] @
    -> term ann -- ^ @{ a x0 ... xn }@
mkIterInst :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInst = (term ann -> (ann, Type tyname uni ann) -> term ann)
-> term ann -> [(ann, Type tyname uni ann)] -> term ann
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((term ann -> (ann, Type tyname uni ann) -> term ann)
 -> term ann -> [(ann, Type tyname uni ann)] -> term ann)
-> (term ann -> (ann, Type tyname uni ann) -> term ann)
-> term ann
-> [(ann, Type tyname uni ann)]
-> term ann
forall a b. (a -> b) -> a -> b
$ \term ann
acc (ann
ann, Type tyname uni ann
arg) -> ann -> term ann -> Type tyname uni ann -> term ann
forall ann. 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 term ann
acc Type tyname uni ann
arg

-- | Make an iterated instantiation with no annotation.
mkIterInstNoAnn
    :: TermLike term tyname name uni fun
    => term () -- ^ @a@
    -> [Type tyname uni ()] -- ^ @ [ x0 ... xn ] @
    -> term () -- ^ @{ a x0 ... xn }@
mkIterInstNoAnn :: forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
term () -> [Type tyname uni ()] -> term ()
mkIterInstNoAnn term ()
term = term () -> [((), Type tyname uni ())] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
mkIterInst term ()
term ([((), Type tyname uni ())] -> term ())
-> ([Type tyname uni ()] -> [((), Type tyname uni ())])
-> [Type tyname uni ()]
-> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni () -> ((), Type tyname uni ()))
-> [Type tyname uni ()] -> [((), Type tyname uni ())]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((),)

-- | Lambda abstract a list of names.
mkIterLamAbs
    :: TermLike term tyname name uni fun
    => [VarDecl tyname name uni ann]
    -> term ann
    -> term ann
mkIterLamAbs :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [VarDecl tyname name uni ann]
args term ann
body =
    (VarDecl tyname name uni ann -> term ann -> term ann)
-> term ann -> [VarDecl tyname name uni ann] -> term ann
forall a b. (a -> b -> b) -> b -> [a] -> b
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 ann.
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 ann]
args

-- | Type abstract a list of names.
mkIterTyAbs
    :: TermLike term tyname name uni fun
    => [TyVarDecl tyname ann]
    -> term ann
    -> term ann
mkIterTyAbs :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[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 a b. (a -> b -> b) -> b -> [a] -> b
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 ann. 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. Each `TyApp` node uses the annotation associated with
-- the corresponding argument.
mkIterTyApp
    :: Type tyname uni ann -- ^ @f@
    -> [(ann, Type tyname uni ann)] -- ^ @[ x0 ... xn ]@
    -> Type tyname uni ann -- ^ @[ f x0 ... xn ]@
mkIterTyApp :: forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyApp = (Type tyname uni ann
 -> (ann, Type tyname uni ann) -> Type tyname uni ann)
-> Type tyname uni ann
-> [(ann, Type tyname uni ann)]
-> Type tyname uni ann
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Type tyname uni ann
  -> (ann, Type tyname uni ann) -> Type tyname uni ann)
 -> Type tyname uni ann
 -> [(ann, Type tyname uni ann)]
 -> Type tyname uni ann)
-> (Type tyname uni ann
    -> (ann, Type tyname uni ann) -> Type tyname uni ann)
-> Type tyname uni ann
-> [(ann, Type tyname uni ann)]
-> Type tyname uni ann
forall a b. (a -> b) -> a -> b
$ \Type tyname uni ann
acc (ann
ann, Type tyname uni ann
arg) -> 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 Type tyname uni ann
acc Type tyname uni ann
arg

-- | Make an iterated type application with no annotation.
mkIterTyAppNoAnn
    :: Type tyname uni () -- ^ @f@
    -> [Type tyname uni ()] -- ^ @[ x0 ... xn ]@
    -> Type tyname uni () -- ^ @[ f x0 ... xn ]@
mkIterTyAppNoAnn :: forall tyname (uni :: * -> *).
Type tyname uni () -> [Type tyname uni ()] -> Type tyname uni ()
mkIterTyAppNoAnn Type tyname uni ()
ty = Type tyname uni ()
-> [((), Type tyname uni ())] -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
Type tyname uni ann
-> [(ann, Type tyname uni ann)] -> Type tyname uni ann
mkIterTyApp Type tyname uni ()
ty ([((), Type tyname uni ())] -> Type tyname uni ())
-> ([Type tyname uni ()] -> [((), Type tyname uni ())])
-> [Type tyname uni ()]
-> Type tyname uni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type tyname uni () -> ((), Type tyname uni ()))
-> [Type tyname uni ()] -> [((), Type tyname uni ())]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((),)

-- | Make an iterated function type.
mkIterTyFun
    :: ann
    -> [Type tyname uni ann]
    -> Type tyname uni ann
    -> Type tyname uni ann
mkIterTyFun :: forall ann tyname (uni :: * -> *).
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 a b. (a -> b -> b) -> b -> [a] -> b
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 :: forall tyname ann (uni :: * -> *).
[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 a b. (a -> b -> b) -> b -> [a] -> b
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 :: forall tyname ann (uni :: * -> *).
[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 a b. (a -> b -> b) -> b -> [a] -> b
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 :: forall ann. 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 a b. (a -> b -> b) -> b -> [a] -> b
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

{- | A helper to create a single, fresh strict binding; It returns the fresh bound `Var`iable and
a function `Term -> Term`, expecting an "in-Term" to form a let-expression.
-}
mkFreshTermLet :: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a)
               => Type tyname uni a -- ^ the type of binding
               -> t a -- ^ the term bound to the fresh variable
               -> m (t a, t a -> t a) -- ^ the fresh Var and a function that takes an "in" term to construct the Let
mkFreshTermLet :: forall (m :: * -> *) (t :: * -> *) tyname (uni :: * -> *) fun a.
(MonadQuote m, TermLike t tyname Name uni fun, Monoid a) =>
Type tyname uni a -> t a -> m (t a, t a -> t a)
mkFreshTermLet Type tyname uni a
aT t a
a = do
    -- I wish this was less constrained to Name
    Name
genName <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"generated"
    (t a, t a -> t a) -> m (t a, t a -> t a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> Name -> t a
forall ann. ann -> Name -> t ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var a
forall a. Monoid a => a
mempty Name
genName, a -> TermDef t tyname Name uni a -> t a -> t a
forall ann. ann -> TermDef t tyname Name uni ann -> t ann -> t ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> TermDef term tyname name uni ann -> term ann -> term ann
termLet a
forall a. Monoid a => a
mempty (VarDecl tyname Name uni a -> t a -> TermDef t tyname Name uni a
forall var val. var -> val -> Def var val
Def (a -> Name -> Type tyname uni a -> VarDecl tyname Name uni a
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl a
forall a. Monoid a => a
mempty Name
genName Type tyname uni a
aT) t a
a))

-- | 'apply' the head of the application to the arguments iteratively.
headSpineToTerm :: TermLike term tyname name uni fun => HeadSpine (term ()) -> term ()
headSpineToTerm :: forall (term :: * -> *) tyname name (uni :: * -> *) fun.
TermLike term tyname name uni fun =>
HeadSpine (term ()) -> term ()
headSpineToTerm = (term () -> term () -> term ()) -> HeadSpine (term ()) -> term ()
forall a. (a -> a -> a) -> HeadSpine a -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 (() -> term () -> term () -> term ()
forall ann. 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 ())