-- 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
  , headSpineToTermNoAnn
  ) 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'.
The @ann@ is propagated from the 'VarDecl' to the 'Var'. -}
mkVar :: TermLike term tyname name uni fun => VarDecl tyname name uni ann -> term ann
mkVar :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
VarDecl tyname name uni ann -> term ann
mkVar VarDecl tyname name uni ann
v = 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 (VarDecl tyname name uni ann -> ann
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> ann
_varDeclAnn VarDecl tyname name uni ann
v) (VarDecl tyname name uni ann -> name
forall tyname name (uni :: * -> *) ann.
VarDecl tyname name uni ann -> name
_varDeclName VarDecl tyname name uni ann
v)

-- TODO: also propagate @ann@ for 'mkTyVar', and UPLC's 'mkVar'.

-- | 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 => ann -> MonoHeadSpine err (term ann) -> Either err (term ann)
headSpineToTerm :: forall (term :: * -> *) tyname name (uni :: * -> *) fun ann err.
TermLike term tyname name uni fun =>
ann -> MonoHeadSpine err (term ann) -> Either err (term ann)
headSpineToTerm ann
_ (HeadError err
e) = err -> Either err (term ann)
forall a b. a -> Either a b
Left err
e
headSpineToTerm ann
_ (HeadOnly term ann
t) = term ann -> Either err (term ann)
forall a b. b -> Either a b
Right term ann
t
headSpineToTerm ann
ann (HeadSpine term ann
t Spine (term ann)
ts) = term ann -> Either err (term ann)
forall a b. b -> Either a b
Right (term ann -> Either err (term ann))
-> term ann -> Either err (term ann)
forall a b. (a -> b) -> a -> b
$ (term ann -> term ann -> term ann)
-> term ann -> Spine (term ann) -> term ann
forall b a. (b -> a -> b) -> b -> Spine a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (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
t Spine (term ann)
ts

-- | @headSpineToTerm@ but without annotation.
headSpineToTermNoAnn :: TermLike term tyname name uni fun => MonoHeadSpine err (term ()) -> Either err (term ())
headSpineToTermNoAnn :: forall (term :: * -> *) tyname name (uni :: * -> *) fun err.
TermLike term tyname name uni fun =>
MonoHeadSpine err (term ()) -> Either err (term ())
headSpineToTermNoAnn (HeadError err
e) = err -> Either err (term ())
forall a b. a -> Either a b
Left err
e
headSpineToTermNoAnn (HeadOnly term ()
t) = term () -> Either err (term ())
forall a b. b -> Either a b
Right term ()
t
headSpineToTermNoAnn (HeadSpine term ()
t Spine (term ())
ts) = term () -> Either err (term ())
forall a b. b -> Either a b
Right (term () -> Either err (term ()))
-> term () -> Either err (term ())
forall a b. (a -> b) -> a -> b
$ (term () -> term () -> term ())
-> term () -> Spine (term ()) -> term ()
forall b a. (b -> a -> b) -> b -> Spine a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (() -> 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 ()) term ()
t Spine (term ())
ts