{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
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.Unique
import PlutusCore.Quote
import PlutusCore.StdLib.Meta.Data.Tuple
import PlutusCore.StdLib.Type
import Control.Lens.Indexed (ifor)
import Control.Monad
idFun :: TermLike term TyName Name uni fun => term ()
idFun :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 a. a -> QuoteT Identity a
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 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 () 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 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 () 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 ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
const :: TermLike term TyName Name uni fun => term ()
const :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 a. a -> QuoteT Identity a
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 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 () 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 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 () 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 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 () 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 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 () 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 ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x
applyFun :: TermLike term TyName Name uni fun => term ()
applyFun :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 a. a -> QuoteT Identity a
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 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 () 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 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 () 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 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 () 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 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 () 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 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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)
selfData :: RecursiveType uni fun ()
selfData :: forall (uni :: * -> *) fun. 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 :: TermLike term TyName Name uni fun => term ()
unroll :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 a. a -> QuoteT Identity a
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 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 () 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 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 () 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 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 () -> term ()
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 () (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$ () -> Name -> term ()
forall ann. ann -> Name -> term ann
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 ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s
fix :: TermLike term TyName Name uni fun => term ()
fix :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(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 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 () 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 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 () 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 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 () 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 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 () 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 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 ()
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 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 () 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
. () -> 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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
f)
(term () -> term ()) -> (term () -> term ()) -> term () -> term ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> Name -> Type TyName uni () -> term () -> term ()
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 () 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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn term ()
unrollFunAB
[ () -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
s
, () -> Name -> term ()
forall ann. ann -> Name -> term ann
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 a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixTerm, Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fixType)
trans :: Type tyname uni () -> Type tyname uni () -> Type tyname uni () -> Quote (Type tyname uni ())
trans :: forall tyname (uni :: * -> *).
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 () -> QuoteT Identity (Type tyname uni ())
forall a. a -> QuoteT Identity a
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 () -> 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)
natTrans :: Type TyName uni () -> Type TyName uni () -> Quote (Type TyName uni ())
natTrans :: forall (uni :: * -> *).
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 -> QuoteT Identity (Type TyName uni ()))
-> QuoteT Identity (Type TyName uni ())
forall a b.
QuoteT Identity a -> (a -> QuoteT Identity b) -> QuoteT Identity b
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 ())
-> QuoteT Identity (Type TyName uni ())
-> QuoteT Identity (Type TyName uni ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type TyName uni ()
-> Type TyName uni ()
-> Type TyName uni ()
-> QuoteT Identity (Type TyName uni ())
forall tyname (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)
natTransId :: Type TyName uni () -> Quote (Type TyName uni ())
natTransId :: forall (uni :: * -> *).
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 a. a -> QuoteT Identity a
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))
fixBy :: TermLike term TyName Name uni fun => term ()
fixBy :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
(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"
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 a. a -> QuoteT Identity a
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 a. a -> QuoteT Identity a
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
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 a. a -> QuoteT Identity a
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 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 () (() -> term () -> Type TyName uni () -> term ()
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 () term ()
forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
term ()
fix Type TyName uni ()
nt1) Type TyName uni ()
nt2
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 a. a -> QuoteT Identity a
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
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)
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)
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)
let inner :: term ()
inner =
() -> 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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 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 () 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 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 () 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 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 () -> Type TyName uni () -> term ()
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 () (() -> 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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
recc) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 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 () -> Type TyName uni () -> term ()
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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 ann. ann -> Name -> term ann
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 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 () 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 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 () Name
by Type TyName uni ()
byTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> 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 ()
instantiatedFix (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> Name -> Type TyName uni () -> term () -> term ()
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 () Name
recc Type TyName uni ()
reccTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> Name -> Type TyName uni () -> term () -> term ()
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 () Name
h Type TyName uni ()
hty (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> TyName -> Kind () -> term () -> term ()
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 () 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 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 () 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 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 () -> Type TyName uni () -> term ()
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 () term ()
inner (() -> TyName -> Type TyName uni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
r)) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixByTerm, Type TyName uni ()
fixByType)
fixN :: TermLike term TyName Name uni fun => Integer -> term () -> term ()
fixN :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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 :: forall (term :: * -> *) (uni :: * -> *) fun.
TermLike term TyName Name uni fun =>
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
[(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 a. a -> QuoteT Identity a
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 a b. (a -> b) -> [a] -> [b]
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
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
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 a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type TyName uni ()
forall {uni :: * -> *}. Type TyName uni ()
fullTy
term ()
instantiatedFix <- do
TyName
x <- Text -> QuoteT Identity TyName
forall (m :: * -> *). MonadQuote m => Text -> m TyName
freshTyName Text
"X"
term () -> QuoteT Identity (term ())
forall a. a -> QuoteT Identity a
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 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 () 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)))
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 a. a -> QuoteT Identity a
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))
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 a. a -> QuoteT Identity a
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"
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)
let branch :: (TyName, TyName) -> Int -> m (term ())
branch (TyName
a, TyName
b) Int
i = do
[VarDecl TyName Name uni ()]
fs <- [(TyName, TyName)]
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni ()))
-> m [VarDecl TyName Name uni ()]
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 ()))
-> m [VarDecl TyName Name uni ()])
-> (Int -> (TyName, TyName) -> m (VarDecl TyName Name uni ()))
-> m [VarDecl TyName Name uni ()]
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 () -> m (VarDecl TyName Name uni ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarDecl TyName Name uni () -> m (VarDecl TyName Name uni ()))
-> VarDecl TyName Name uni () -> m (VarDecl TyName Name uni ())
forall a b. (a -> b) -> a -> b
$ () -> Name -> Type TyName uni () -> VarDecl TyName Name uni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni 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 a. a -> m a
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 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 () 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 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 () -> Type TyName uni () -> term ()
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 () (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 ()] -> term () -> term ()
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 ()]
fs (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> 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 () (() -> VarDecl TyName Name uni () -> term ()
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> VarDecl tyname name uni ann -> term ann
mkVar () ([VarDecl TyName Name uni ()]
fs [VarDecl TyName Name uni ()] -> Int -> VarDecl TyName Name uni ()
forall a. HasCallStack => [a] -> Int -> a
!! Int
i)) (() -> Name -> term ()
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var () Name
x)
[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
let allAsBs :: [TyName]
allAsBs = ((TyName, TyName) -> [TyName]) -> [(TyName, TyName)] -> [TyName]
forall m a. Monoid m => (a -> m) -> [a] -> m
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 =
[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 a b. (a -> b) -> [a] -> [b]
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 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 () 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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn term ()
instantiatedFix
[ () -> Name -> Type TyName uni () -> term () -> term ()
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 () Name
k Type TyName uni ()
kTy (term () -> term ()) -> term () -> term ()
forall a b. (a -> b) -> a -> b
$
() -> TyName -> Kind () -> term () -> term ()
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 () 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 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 () 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.
TermLike term tyname name uni fun =>
term () -> [term ()] -> term ()
mkIterAppNoAnn (() -> Name -> term ()
forall ann. ann -> Name -> term ann
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 ann. ann -> Name -> term ann
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 a. a -> QuoteT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (term ()
fixNTerm, Type TyName uni ()
fixNType)
getSingleFixOf
:: (TermLike term TyName Name uni fun)
=> ann -> term ann -> FunctionDef term TyName Name uni fun ann -> term ann
getSingleFixOf :: forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
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 {k} (term :: * -> *) tyname name (uni :: * -> *) (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 = term ann -> [(ann, Type TyName uni ann)] -> term ann
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
fix1 [(ann
ann, Type TyName uni ann
dom), (ann
ann, Type TyName uni ann
cod)]
abstractedBody :: term ann
abstractedBody = [VarDecl TyName Name uni ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs [FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni 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 {k} (term :: * -> *) tyname name (uni :: * -> *) (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 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
instantiatedFix term ann
abstractedBody
getMutualFixOf
:: (TermLike term TyName Name uni fun)
=> ann -> term ann -> [FunctionDef term TyName Name uni fun ann] -> Quote (Tuple term uni ann)
getMutualFixOf :: forall (term :: * -> *) (uni :: * -> *) fun ann.
TermLike term TyName Name uni fun =>
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 a. Quote a -> Quote a
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"
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)
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 {k} (term :: * -> *) tyname name (uni :: * -> *) (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 = term ann -> [(ann, term ann)] -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
mkIterApp (ann -> Name -> term ann
forall ann. ann -> Name -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> term ann
var ann
ann Name
choose) ((ann
ann,) (term ann -> (ann, term ann)) -> [term ann] -> [(ann, term ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [term ann]
rhss)
vsLam :: term ann
vsLam = [VarDecl TyName Name uni ann] -> term ann -> term ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
[VarDecl tyname name uni ann] -> term ann -> term ann
mkIterLamAbs ((FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni ann)
-> [FunctionDef term TyName Name uni fun ann]
-> [VarDecl TyName Name uni ann]
forall a b. (a -> b) -> [a] -> [b]
map FunctionDef term TyName Name uni fun ann
-> VarDecl TyName Name uni ann
forall {k} (term :: * -> *) tyname name (uni :: * -> *) (fun :: k)
ann.
FunctionDef term tyname name uni fun ann
-> VarDecl tyname name uni ann
functionDefVarDecl [FunctionDef term TyName Name uni fun ann]
funs) term ann
chosen
let cLam :: term ann
cLam = 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
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 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
choose Type TyName uni ann
chooseTy term ann
vsLam
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 m a. Monoid m => (a -> m) -> [a] -> m
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 a. a -> QuoteT Identity a
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
$ term ann -> [(ann, Type TyName uni ann)] -> term ann
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
fixn ((ann
ann,) (Type TyName uni ann -> (ann, Type TyName uni ann))
-> [Type TyName uni ann] -> [(ann, Type TyName uni ann)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type TyName uni ann]
domCods)
let term :: term ann
term = 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
instantiatedFix term ann
cLam
Tuple term uni ann -> Quote (Tuple term uni ann)
forall a. a -> QuoteT Identity a
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 :: * -> *) ann.
[Type TyName uni ann] -> term ann -> Tuple term uni ann
Tuple [Type TyName uni ann]
funTys term ann
term