-- | Combinators.

{-# LANGUAGE OverloadedStrings #-}

module PlutusCore.StdLib.Data.Function
    ( const
    , idFun
    , applyFun
    , selfData
    , unroll
    , fix
    , fixAndType
    , fixBy
    , fixByAndType
    , fixN
    , fixNAndType
    , FunctionDef (..)
    , getMutualFixOf
    , getSingleFixOf
    ) where

import PlutusPrelude
import Prelude hiding (const)

import PlutusCore.Core
import PlutusCore.MkPlc
import PlutusCore.Name
import PlutusCore.Quote

import PlutusCore.StdLib.Meta.Data.Tuple
import PlutusCore.StdLib.Type

import Control.Lens.Indexed (ifor)
import Control.Monad

-- | 'id' as a PLC term.
--
-- > /\(A :: *) -> \(x : A) -> x
idFun :: TermLike term TyName Name uni fun => term ()
idFun :: term ()
idFun = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    term () -> Quote (term ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x

-- | 'const' as a PLC term.
--
-- > /\(A B :: *) -> \(x : A) (y : B) -> x
const :: TermLike term TyName Name uni fun => term ()
const :: term ()
const = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    Name
y <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"y"
    term () -> Quote (term ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
y (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x

-- | '($)' as a PLC term.
--
-- > /\(A B :: *) -> \(f : A -> B) (x : A) -> f x
applyFun :: TermLike term TyName Name uni fun => term ()
applyFun :: term ()
applyFun = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    term () -> Quote (term ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)

-- | @Self@ as a PLC type.
--
-- > fix \(self :: * -> *) (a :: *) -> self a -> a
selfData :: RecursiveType uni fun ()
selfData :: RecursiveType uni fun ()
selfData = Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
forall a. Quote a -> a
runQuote (Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ())
-> Quote (RecursiveType uni fun ()) -> RecursiveType uni fun ()
forall a b. (a -> b) -> a -> b
$ do
    TyName
self <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"self"
    TyName
a    <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    FromDataPieces uni () (RecursiveType uni fun ())
forall (uni :: * -> *) ann fun.
FromDataPieces uni ann (RecursiveType uni fun ann)
makeRecursiveType () TyName
self [() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (Kind () -> TyVarDecl TyName ()) -> Kind () -> TyVarDecl TyName ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()]
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni ()
-> Quote (RecursiveType uni fun ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
self) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a))
        (Type TyName uni () -> Quote (RecursiveType uni fun ()))
-> Type TyName uni () -> Quote (RecursiveType uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a

-- | @unroll@ as a PLC term.
--
-- > /\(a :: *) -> \(s : self a) -> unwrap s s
unroll :: TermLike term TyName Name uni fun => term ()
unroll :: term ()
unroll = Quote (term ()) -> term ()
forall a. Quote a -> a
runQuote (Quote (term ()) -> term ()) -> Quote (term ()) -> term ()
forall a b. (a -> b) -> a -> b
$ do
    let self :: Type TyName uni ()
self = RecursiveType uni Any () -> Type TyName uni ()
forall (uni :: * -> *) fun ann.
RecursiveType uni fun ann -> Type TyName uni ann
_recursiveType RecursiveType uni Any ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
selfData
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    Name
s <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"s"
    term () -> Quote (term ())
forall (m :: * -> *) a. Monad m => a -> m a
return
        (term () -> Quote (term ()))
-> (term () -> term ()) -> term () -> Quote (term ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
s (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
self (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
        (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
unwrap () (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s)
        (term () -> Quote (term ())) -> term () -> Quote (term ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s

-- | 'fix' as a PLC term.
--
-- > /\(a b :: *) -> \(f : (a -> b) -> a -> b) ->
-- >    unroll {a -> b} (iwrap selfF (a -> b) \(s : self (a -> b)) \(x : a) -> f (unroll {a -> b} s) x)
--
-- See @plutus/runQuote $ docs/fomega/z-combinator-benchmarks@ for details.
fix :: TermLike term TyName Name uni fun => term ()
fix :: term ()
fix = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixAndType

fixAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixAndType :: (term (), Type TyName uni ())
fixAndType = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    let RecursiveType Type TyName uni ()
self forall (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapSelf = RecursiveType uni fun ()
forall (uni :: * -> *) fun. RecursiveType uni fun ()
selfData
    TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
    TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Name
s <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"s"
    Name
x <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"
    let funAB :: Type TyName uni ()
funAB = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b
        unrollFunAB :: term ()
unrollFunAB = () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
unroll Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB
    let selfFunAB :: Type TyName uni ()
selfFunAB = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
self Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB
    let fixTerm :: term ()
fixTerm =
            () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB)
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
unrollFunAB
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type TyName uni ()] -> term () -> term ()
forall (uni :: * -> *) fun (term :: * -> *).
TermLike term TyName Name uni fun =>
[Type TyName uni ()] -> term () -> term ()
wrapSelf [Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB]
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
s Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
selfFunAB
            (term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a)
            (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
            [ () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
unrollFunAB (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s
            , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
            ]
    let fixType :: Type TyName uni ()
fixType =
            () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (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
. () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())
            (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB) Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
funAB
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixTerm, Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
fixType)


-- | A type that looks like a transformation.
--
-- > trans F G Q : F Q -> G Q
trans :: Type TyName uni () -> Type TyName uni () -> Type TyName uni () -> Quote (Type TyName uni ())
trans :: Type TyName uni ()
-> Type TyName uni ()
-> Type TyName uni ()
-> Quote (Type TyName uni ())
trans Type TyName uni ()
f Type TyName uni ()
g Type TyName uni ()
q = Type TyName uni () -> Quote (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
f Type TyName uni ()
q) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
g Type TyName uni ()
q)

-- | A type that looks like a natural transformation, sometimes written 'F ~> G'.
--
-- > natTrans F G : forall Q :: * . F Q -> G Q
natTrans :: Type TyName uni () -> Type TyName uni () -> Quote (Type TyName uni ())
natTrans :: Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans Type TyName uni ()
f Type TyName uni ()
g = Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q" QuoteT Identity TyName
-> (TyName -> Quote (Type TyName uni ()))
-> Quote (Type TyName uni ())
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \TyName
q -> () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Quote (Type TyName uni ()) -> Quote (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ()
-> Type TyName uni ()
-> Type TyName uni ()
-> Quote (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni ()
-> Type TyName uni ()
-> Quote (Type TyName uni ())
trans Type TyName uni ()
f Type TyName uni ()
g (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

-- | A type that looks like a natural transformation to Id.
--
-- > natTransId F : forall Q :: * . F Q -> Q
natTransId :: Type TyName uni () -> Quote (Type TyName uni ())
natTransId :: Type TyName uni () -> Quote (Type TyName uni ())
natTransId Type TyName uni ()
f = do
    TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    Type TyName uni () -> Quote (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> Quote (Type TyName uni ()))
-> Type TyName uni () -> Quote (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () Type TyName uni ()
f (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q))

-- | The 'fixBy' combinator.
--
-- > fixBy :
-- >     forall (F :: * -> *) .
-- >     ((F ~> Id) -> (F ~> Id)) ->
-- >     ((F ~> F) -> (F ~> Id))
fixBy :: TermLike term TyName Name uni fun => term ()
fixBy :: term ()
fixBy = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(term (), Type TyName uni ())
fixByAndType

fixByAndType :: TermLike term TyName Name uni fun => (term (), Type TyName uni ())
fixByAndType :: (term (), Type TyName uni ())
fixByAndType = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    TyName
f <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"F"

    -- by : (F ~> Id) -> (F ~> Id)
    Name
by <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"by"
    Type TyName uni ()
byTy <- do
        Type TyName uni ()
nt1 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
nt1 Type TyName uni ()
nt2

    Type TyName uni ()
resTy <- do
        Type TyName uni ()
nt1 <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
nt1 Type TyName uni ()
nt2

    -- instantiatedFix = fix {F ~> F} {F ~> Id}
    term ()
instantiatedFix <- do
        Type TyName uni ()
nt1 <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
        term () -> QuoteT Identity (term ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> QuoteT Identity (term ()))
-> term () -> QuoteT Identity (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix Type TyName uni ()
nt1) Type TyName uni ()
nt2

    -- rec : (F ~> F) -> (F ~> Id)
    Name
recc <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"rec"
    Type TyName uni ()
reccTy <- do
      Type TyName uni ()
nt <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
      Type TyName uni ()
nt2 <- Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni () -> Quote (Type TyName uni ())
natTransId (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)
      Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
nt Type TyName uni ()
nt2

    -- h : F ~> F
    Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"h"
    Type TyName uni ()
hty <- Type TyName uni ()
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (uni :: * -> *).
Type TyName uni ()
-> Type TyName uni () -> Quote (Type TyName uni ())
natTrans (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f)

    -- R :: *
    -- fr : F R
    TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"R"
    Name
fr <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fr"
    let frTy :: Type TyName uni ()
frTy = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)

    -- Q :: *
    -- fq : F Q
    TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    Name
fq <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"fq"
    let fqTy :: Type TyName uni ()
fqTy = ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyApp () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
f) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

    -- inner = (/\ (Q :: *) -> \ q : F Q -> rec h {Q} (h {Q} q))
    let inner :: term ()
inner =
            () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
by) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fq Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
fqTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
recc) (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fq)
    let fixByTerm :: term ()
fixByTerm =
            () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
f (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
by Type TyName uni ()
byTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () term ()
instantiatedFix (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
recc Type TyName uni ()
reccTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
h Type TyName uni ()
hty (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
fr Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
frTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
            () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
inner (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)) (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
fr)
    let fixByType :: Type TyName uni ()
fixByType =
            () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
f (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$
            ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
byTy Type TyName uni ()
resTy
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixByTerm, Type TyName uni ()
fixByType)


-- | Make a @n@-ary fixpoint combinator.
--
-- > FixN n :
-- >     forall A1 B1 ... An Bn :: * .
-- >     (forall Q :: * .
-- >         ((A1 -> B1) -> ... -> (An -> Bn) -> Q) ->
-- >         (A1 -> B1) ->
-- >         ... ->
-- >         (An -> Bn) ->
-- >         Q) ->
-- >     (forall R :: * . ((A1 -> B1) -> ... (An -> Bn) -> R) -> R)
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term ()
fixN :: Integer -> term () -> term ()
fixN Integer
n term ()
fixByTerm = (term (), Type TyName uni ()) -> term ()
forall a b. (a, b) -> a
fst (Integer -> term () -> (term (), Type TyName uni ())
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
Integer -> term () -> (term (), Type TyName uni ())
fixNAndType Integer
n term ()
fixByTerm)

fixNAndType :: TermLike term TyName Name uni fun => Integer -> term () -> (term (), Type TyName uni ())
fixNAndType :: Integer -> term () -> (term (), Type TyName uni ())
fixNAndType Integer
n term ()
fixByTerm = Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a. Quote a -> a
runQuote (Quote (term (), Type TyName uni ())
 -> (term (), Type TyName uni ()))
-> Quote (term (), Type TyName uni ())
-> (term (), Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ do
    -- the list of pairs of A and B types
    [(TyName, TyName)]
asbs <- Int
-> QuoteT Identity (TyName, TyName)
-> QuoteT Identity [(TyName, TyName)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n) (QuoteT Identity (TyName, TyName)
 -> QuoteT Identity [(TyName, TyName)])
-> QuoteT Identity (TyName, TyName)
-> QuoteT Identity [(TyName, TyName)]
forall a b. (a -> b) -> a -> b
$ do
        TyName
a <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"a"
        TyName
b <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"b"
        (TyName, TyName) -> QuoteT Identity (TyName, TyName)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TyName
a, TyName
b)

    let abFuns :: [Type TyName uni ()]
abFuns = ((TyName, TyName) -> Type TyName uni ())
-> [(TyName, TyName)] -> [Type TyName uni ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(TyName
a, TyName
b) -> ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)) [(TyName, TyName)]
asbs
    let abTyVars :: [TyVarDecl TyName ()]
abTyVars = ((TyName, TyName) -> [TyVarDecl TyName ()])
-> [(TyName, TyName)] -> [TyVarDecl TyName ()]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TyName
a, TyName
b) -> [ () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a (() -> Kind ()
forall ann. ann -> Kind ann
Type ()), () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
b (() -> Kind ()
forall ann. ann -> Kind ann
Type ())]) [(TyName, TyName)]
asbs

    -- funTysTo X = (A1 -> B1) -> ... -> (An -> Bn) -> X
    let funTysTo :: Type TyName uni () -> Type TyName uni ()
funTysTo = ()
-> [Type TyName uni ()] -> Type TyName uni () -> Type TyName uni ()
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun () [Type TyName uni ()]
forall (uni :: * -> *). [Type TyName uni ()]
abFuns

    -- the type of fixN, as in the header comment
    Type TyName uni ()
fixNType <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        let qvar :: Type TyName uni ()
qvar = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q
        let argTy :: Type TyName uni ()
argTy = () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
qvar) (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
qvar))
        TyName
r <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"R"
        let rvar :: Type TyName uni ()
rvar = () -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r
        let resTy :: Type TyName uni ()
resTy = () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
r (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
rvar) Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
rvar)
        let fullTy :: Type TyName uni ()
fullTy = [TyVarDecl TyName ()] -> Type TyName uni () -> Type TyName uni ()
forall tyname ann (uni :: * -> *).
[TyVarDecl tyname ann]
-> Type tyname uni ann -> Type tyname uni ann
mkIterTyForall [TyVarDecl TyName ()]
abTyVars (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
argTy Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
resTy
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
fullTy

    -- instantiatedFix = fixBy { \X :: * -> (A1 -> B1) -> ... -> (An -> Bn) -> X }
    term ()
instantiatedFix <- do
        TyName
x <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"X"
        term () -> QuoteT Identity (term ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> QuoteT Identity (term ()))
-> term () -> QuoteT Identity (term ())
forall a b. (a -> b) -> a -> b
$ () -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () term ()
fixByTerm (() -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
x)))

    -- f : forall Q :: * . ((A1 -> B1) -> ... -> (An -> Bn) -> Q) -> (A1 -> B1) -> ... -> (An -> Bn) -> Q)
    Name
f <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"f"
    Type TyName uni ()
fTy <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q))

    -- k : forall Q :: * . ((A1 -> B1) -> ... -> (An -> Bn) -> Q) -> Q)
    Name
k <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"k"
    Type TyName uni ()
kTy <- do
        TyName
q <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
        Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Type TyName uni () -> QuoteT Identity (Type TyName uni ()))
-> Type TyName uni () -> QuoteT Identity (Type TyName uni ())
forall a b. (a -> b) -> a -> b
$ () -> TyName -> Kind () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
q (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (Type TyName uni () -> Type TyName uni ())
-> Type TyName uni () -> Type TyName uni ()
forall a b. (a -> b) -> a -> b
$ ()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
q)

    TyName
s <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"S"

    -- h : (A1 -> B1) -> ... -> (An -> Bn) -> S
    Name
h <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"h"
    let hTy :: Type TyName uni ()
hTy = Type TyName uni () -> Type TyName uni ()
forall (uni :: * -> *). Type TyName uni () -> Type TyName uni ()
funTysTo (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
s)

    -- branch (ai, bi) i = \x : ai -> k { bi } \(f1 : A1 -> B1) ... (fn : An -> Bn) . fi x
    let branch :: (TyName, TyName) -> Int -> m (term ())
branch (TyName
a, TyName
b) Int
i = do
            -- names and types for the f arguments
            [VarDecl TyName Name uni fun ()]
fs <- [(TyName, TyName)]
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni fun ()))
-> m [VarDecl TyName Name uni fun ()]
forall i (t :: * -> *) (f :: * -> *) a b.
(TraversableWithIndex i t, Applicative f) =>
t a -> (i -> a -> f b) -> f (t b)
ifor [(TyName, TyName)]
asbs ((Int -> (TyName, TyName) -> m (VarDecl TyName Name uni fun ()))
 -> m [VarDecl TyName Name uni fun ()])
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni fun ()))
-> m [VarDecl TyName Name uni fun ()]
forall a b. (a -> b) -> a -> b
$ \Int
j (TyName
a',TyName
b') -> do
                Name
f_j <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName (Text -> m Name) -> Text -> m Name
forall a b. (a -> b) -> a -> b
$ Text
"f_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall a. Show a => a -> Text
showText Int
j
                VarDecl TyName Name uni fun ()
-> m (VarDecl TyName Name uni fun ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni fun ()
 -> m (VarDecl TyName Name uni fun ()))
-> VarDecl TyName Name uni fun ()
-> m (VarDecl TyName Name uni fun ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni fun ()
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl () Name
f_j (()
-> Type TyName uni () -> Type TyName uni () -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a') (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b'))

            Name
x <- Text -> m Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"x"

            term () -> m (term ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term () -> m (term ())) -> term () -> m (term ())
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
x (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
a) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> term () -> Type TyName uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> Type tyname uni ann -> term ann
tyInst () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
k) (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
b)) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                [VarDecl TyName Name uni fun ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [VarDecl TyName Name uni fun ()]
fs (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                -- this is an ugly but straightforward way of getting the right fi
                () -> term () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann -> term ann
apply () (() -> VarDecl TyName Name uni fun () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni fun ann -> term ann
mkVar () ([VarDecl TyName Name uni fun ()]
fs [VarDecl TyName Name uni fun ()]
-> Int -> VarDecl TyName Name uni fun ()
forall a. [a] -> Int -> a
!! Int
i)) (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)

    -- a list of all the branches
    [term ()]
branches <- [((TyName, TyName), Int)]
-> (((TyName, TyName), Int) -> QuoteT Identity (term ()))
-> QuoteT Identity [term ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([(TyName, TyName)] -> [Int] -> [((TyName, TyName), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(TyName, TyName)]
asbs [Int
0..]) ((((TyName, TyName), Int) -> QuoteT Identity (term ()))
 -> QuoteT Identity [term ()])
-> (((TyName, TyName), Int) -> QuoteT Identity (term ()))
-> QuoteT Identity [term ()]
forall a b. (a -> b) -> a -> b
$ ((TyName, TyName) -> Int -> QuoteT Identity (term ()))
-> ((TyName, TyName), Int) -> QuoteT Identity (term ())
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TyName, TyName) -> Int -> QuoteT Identity (term ())
forall (m :: * -> *) (term :: * -> *) (uni :: * -> *) fun.
(MonadQuote m, TermLike term TyName Name uni fun) =>
(TyName, TyName) -> Int -> m (term ())
branch

    -- [A1, B1, ..., An, Bn]
    let allAsBs :: [TyName]
allAsBs = ((TyName, TyName) -> [TyName]) -> [(TyName, TyName)] -> [TyName]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(TyName
a, TyName
b) -> [TyName
a, TyName
b]) [(TyName, TyName)]
asbs
    let fixNTerm :: term ()
fixNTerm =
          -- abstract out all the As and Bs
          [TyVarDecl TyName ()] -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[TyVarDecl tyname ann] -> term ann -> term ann
mkIterTyAbs ((TyName -> TyVarDecl TyName ())
-> [TyName] -> [TyVarDecl TyName ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\TyName
tn -> () -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
tn (() -> Kind ()
forall ann. ann -> Kind ann
Type ())) [TyName]
allAsBs) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
          () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
f Type TyName uni ()
fTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
          () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () term ()
instantiatedFix
              [ () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
k Type TyName uni ()
kTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> TyName -> Kind () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
tyAbs () TyName
s (() -> Kind ()
forall ann. ann -> Kind ann
Type ()) (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> Name -> Type TyName uni () -> term () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
lamAbs () Name
h Type TyName uni ()
forall (uni :: * -> *). Type TyName uni ()
hTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
                () -> term () -> [term ()] -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
mkIterApp () (() -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
h) [term ()]
branches
              , () -> Name -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f
              ]
    (term (), Type TyName uni ())
-> Quote (term (), Type TyName uni ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixNTerm, Type TyName uni ()
fixNType)

-- | Get the fixed-point of a single recursive function.
getSingleFixOf
    :: (TermLike term TyName Name uni fun)
    => ann -> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
getSingleFixOf :: ann
-> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
getSingleFixOf ann
ann term ann
fix1 fun :: FunctionDef term TyName Name uni fun ann
fun@FunctionDef{_functionDefType :: forall (term :: * -> *) tyname name (uni :: * -> *) k (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> FunctionType tyname uni ann
_functionDefType=(FunctionType ann
_ Type TyName uni ann
dom Type TyName uni ann
cod)} =
    let instantiatedFix :: term ann
instantiatedFix = 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
mkIterInst ann
ann term ann
fix1 [Type TyName uni ann
dom, Type TyName uni ann
cod]
        abstractedBody :: term ann
abstractedBody = [VarDecl TyName Name uni fun ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs [FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni fun ann
forall k (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni fun ann
functionDefVarDecl FunctionDef term TyName Name uni fun ann
fun] (term ann -> term ann) -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ FunctionDef term TyName Name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) k (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm FunctionDef term TyName Name uni fun ann
fun
    in 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
instantiatedFix term ann
abstractedBody

-- | Get the fixed-point of a list of mutually recursive functions.
--
-- > MutualFixOf _ fixN [ FunctionDef _ fN1 (FunctionType _ a1 b1) f1
-- >                    , ...
-- >                    , FunctionDef _ fNn (FunctionType _ an bn) fn
-- >                    ] =
-- >     Tuple [(a1 -> b1) ... (an -> bn)] $
-- >         fixN {a1} {b1} ... {an} {bn}
-- >             /\(q :: *) -> \(choose : (a1 -> b1) -> ... -> (an -> bn) -> q) ->
-- >                 \(fN1 : a1 -> b1) ... (fNn : an -> bn) -> choose f1 ... fn
getMutualFixOf
    :: (TermLike term TyName Name uni fun)
    => ann -> term ann -> [FunctionDef term TyName Name uni fun ann] -> Quote (Tuple term uni ann)
getMutualFixOf :: ann
-> term ann
-> [FunctionDef term TyName Name uni fun ann]
-> Quote (Tuple term uni ann)
getMutualFixOf ann
ann term ann
fixn [FunctionDef term TyName Name uni fun ann]
funs = do
    let funTys :: [Type TyName uni ann]
funTys = (FunctionDef term TyName Name uni fun ann -> Type TyName uni ann)
-> [FunctionDef term TyName Name uni fun ann]
-> [Type TyName uni ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann -> Type TyName uni ann
forall k (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> Type tyname uni ann
functionDefToType [FunctionDef term TyName Name uni fun ann]
funs

    TyName
q <- QuoteT Identity TyName -> QuoteT Identity TyName
forall (m :: * -> *) a. MonadQuote m => Quote a -> m a
liftQuote (QuoteT Identity TyName -> QuoteT Identity TyName)
-> QuoteT Identity TyName -> QuoteT Identity TyName
forall a b. (a -> b) -> a -> b
$ Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"Q"
    -- TODO: It was 'safeFreshName' previously. Should we perhaps have @freshName = safeFreshName@?
    Name
choose <- Text -> QuoteT Identity Name
forall (m :: * -> *). MonadQuote m => Text -> m Name
freshName Text
"choose"
    let chooseTy :: Type TyName uni ann
chooseTy = ann
-> [Type TyName uni ann]
-> Type TyName uni ann
-> Type TyName uni ann
forall ann tyname (uni :: * -> *).
ann
-> [Type tyname uni ann]
-> Type tyname uni ann
-> Type tyname uni ann
mkIterTyFun ann
ann [Type TyName uni ann]
funTys (ann -> TyName -> Type TyName uni ann
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar ann
ann TyName
q)

    -- \v1 ... vn -> choose f1 ... fn
    let rhss :: [term ann]
rhss    = (FunctionDef term TyName Name uni fun ann -> term ann)
-> [FunctionDef term TyName Name uni fun ann] -> [term ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) k (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann -> term ann
_functionDefTerm [FunctionDef term TyName Name uni fun ann]
funs
        chosen :: term ann
chosen  = 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
mkIterApp ann
ann (ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann Name
choose) [term ann]
rhss
        vsLam :: term ann
vsLam   = [VarDecl TyName Name uni fun ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni fun ann] -> term ann -> term ann
mkIterLamAbs ((FunctionDef term TyName Name uni fun ann
 -> VarDecl TyName Name uni fun ann)
-> [FunctionDef term TyName Name uni fun ann]
-> [VarDecl TyName Name uni fun ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni fun ann
forall k (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
       ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni fun ann
functionDefVarDecl [FunctionDef term TyName Name uni fun ann]
funs) term ann
chosen

    -- abstract out Q and choose
    let cLam :: term ann
cLam = 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
q (ann -> Kind ann
forall ann. ann -> Kind ann
Type ann
ann) (term ann -> term ann) -> term ann -> term ann
forall a b. (a -> b) -> a -> b
$ 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
choose Type TyName uni ann
chooseTy term ann
vsLam

    -- fixN {A1} {B1} ... {An} {Bn}
    term ann
instantiatedFix <- do
        let domCods :: [Type TyName uni ann]
domCods = (FunctionDef term TyName Name uni fun ann -> [Type TyName uni ann])
-> [FunctionDef term TyName Name uni fun ann]
-> [Type TyName uni ann]
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(FunctionDef ann
_ Name
_ (FunctionType ann
_ Type TyName uni ann
dom Type TyName uni ann
cod) term ann
_) -> [Type TyName uni ann
dom, Type TyName uni ann
cod]) [FunctionDef term TyName Name uni fun ann]
funs
        term ann -> QuoteT Identity (term ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ann -> QuoteT Identity (term ann))
-> term ann -> QuoteT Identity (term ann)
forall a b. (a -> b) -> a -> b
$ 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
mkIterInst ann
ann term ann
fixn [Type TyName uni ann]
domCods

    let term :: term ann
term = 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
instantiatedFix term ann
cLam

    Tuple term uni ann -> Quote (Tuple term uni ann)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Tuple term uni ann -> Quote (Tuple term uni ann))
-> Tuple term uni ann -> Quote (Tuple term uni ann)
forall a b. (a -> b) -> a -> b
$ [Type TyName uni ann] -> term ann -> Tuple term uni ann
forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
[Type TyName uni ann] -> term ann -> Tuple term uni ann
Tuple [Type TyName uni ann]
funTys term ann
term