{-# 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
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
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
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
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)
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
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
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)
type TermDef term tyname name uni ann = Def (VarDecl tyname name uni ann) (term ann)
type TypeDef tyname uni ann = Def (TyVarDecl tyname ann) (Type tyname uni ann)
data FunctionType tyname uni ann = FunctionType
{ forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> ann
_functionTypeAnn :: ann
, forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> Type tyname uni ann
_functionTypeDom :: Type tyname uni ann
, forall tyname (uni :: * -> *) ann.
FunctionType tyname uni ann -> Type tyname uni ann
_functionTypeCod :: Type tyname uni ann
}
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
, forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
ann.
FunctionDef term tyname name uni fun ann -> name
_functionDefName :: name
, 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
, forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
ann.
FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm :: term ann
}
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
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
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
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
mkImmediateLamAbs
:: TermLike term tyname name uni fun
=> ann
-> TermDef term tyname name uni ann
-> term ann
-> 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
mkImmediateTyAbs
:: TermLike term tyname name uni fun
=> ann
-> TypeDef tyname uni ann
-> term ann
-> 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
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
mkIterAppNoAnn
:: TermLike term tyname name uni fun
=> term ()
-> [term ()]
-> term ()
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 ((),)
(@@) :: TermLike term tyname name uni fun
=> term ()
-> [term ()]
-> term ()
@@ :: 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
mkIterInst
:: TermLike term tyname name uni fun
=> term ann
-> [(ann, Type tyname uni ann)]
-> term ann
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
mkIterInstNoAnn
:: TermLike term tyname name uni fun
=> term ()
-> [Type tyname uni ()]
-> term ()
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 ((),)
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
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
mkIterTyApp
:: Type tyname uni ann
-> [(ann, Type tyname uni ann)]
-> Type tyname uni ann
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
mkIterTyAppNoAnn
:: Type tyname uni ()
-> [Type tyname uni ()]
-> Type tyname uni ()
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 ((),)
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
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
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
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
mkFreshTermLet :: (MonadQuote m, TermLike t tyname Name uni fun, Monoid a)
=> Type tyname uni a
-> t a
-> m (t a, t a -> t a)
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
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))
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 ())