{-# LANGUAGE QuasiQuotes, ViewPatterns #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators, DataKinds #-}
{-# LANGUAGE GADTs #-}

{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

-- |
-- Module      : Data.Binding.Hobbits.Examples.LambdaLifting
-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--
-- The lambda lifting example from the paper E. Westbrook, N. Frisby,
-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in
-- Functional Programming Languages\".

-------------------------------------------------------------------------
-- lambda lifting for the lambda calculus with top-level declarations
-------------------------------------------------------------------------

module Data.Binding.Hobbits.Examples.LambdaLifting (
  -- * Term data types, using 'Data.Binding.Hobbits.Mb'
  module Data.Binding.Hobbits.Examples.LambdaLifting.Terms,
  -- * The lambda-lifting function
  lambdaLift, mbLambdaLift
  ) where

import Data.Binding.Hobbits
import qualified Data.Type.RList as C

import Data.Binding.Hobbits.Examples.LambdaLifting.Terms

-- imported for ease of use at terminal
import Data.Binding.Hobbits.Examples.LambdaLifting.Examples

import Control.Monad.Cont (Cont, runCont, cont)

------------------------------------------------------------
-- "peeling" lambdas off of a term
------------------------------------------------------------

data LType a where LType :: LType (L a)
type LC c = RAssign LType c

type family AddArrows (c :: RList *) b
type instance AddArrows RNil b = b
type instance AddArrows (c :> L a) b = AddArrows c (a -> b)

data PeelRet c a where
  PeelRet :: lc ~ (lc0 :> b) => LC lc -> Mb (c :++: lc) (Term a) ->
             PeelRet c (AddArrows lc a)

peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
peelLambdas Mb c (Binding (L b) (Term a))
b = LC 'RNil
-> LType (L b)
-> Mb (c :++: ('RNil ':> L b)) (Term a)
-> PeelRet c (AddArrows ('RNil ':> L b) a)
forall (lc :: RList *) (lc0 :: RList *) b (c :: RList *) a.
(lc ~ (lc0 ':> b)) =>
LC lc0
-> LType b -> Mb (c :++: lc) (Term a) -> PeelRet c (AddArrows lc a)
peelLambdasH LC 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil LType (L b)
forall a. LType (L a)
LType (Mb c (Binding (L b) (Term a))
-> Mb (c :++: ('RNil ':> L b)) (Term a)
forall k1 k2 (c1 :: RList k2) (c2 :: RList k2) (a :: k1) b.
Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine Mb c (Binding (L b) (Term a))
b)

peelLambdasH ::
  lc ~ (lc0 :> b) => LC lc0 -> LType b -> Mb (c :++: lc) (Term a) ->
                     PeelRet c (AddArrows lc a)
peelLambdasH :: LC lc0
-> LType b -> Mb (c :++: lc) (Term a) -> PeelRet c (AddArrows lc a)
peelLambdasH LC lc0
lc0 LType b
isl Mb (c :++: lc) (Term a)
[nuP| Lam b |] =
  LC (lc0 ':> b)
-> LType (L b)
-> Mb (c :++: ((lc0 ':> b) ':> L b)) (Term a)
-> PeelRet c (AddArrows ((lc0 ':> b) ':> L b) a)
forall (lc :: RList *) (lc0 :: RList *) b (c :: RList *) a.
(lc ~ (lc0 ':> b)) =>
LC lc0
-> LType b -> Mb (c :++: lc) (Term a) -> PeelRet c (AddArrows lc a)
peelLambdasH (LC lc0
lc0 LC lc0 -> LType b -> LC (lc0 ':> b)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: LType b
isl) LType (L b)
forall a. LType (L a)
LType (Mb ((c :++: lc0) ':> b) (Binding (L b) (Term a))
-> Mb (((c :++: lc0) ':> b) :++: ('RNil ':> L b)) (Term a)
forall k1 k2 (c1 :: RList k2) (c2 :: RList k2) (a :: k1) b.
Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b
mbCombine Mb ((c :++: lc0) ':> b) (Binding (L b) (Term a))
b)
peelLambdasH LC lc0
lc0 LType b
ilt Mb (c :++: lc) (Term a)
t = LC (lc0 ':> b)
-> Mb (c :++: (lc0 ':> b)) (Term a)
-> PeelRet c (AddArrows (lc0 ':> b) a)
forall (lc :: RList *) (lc0 :: RList *) b (c :: RList *) a.
(lc ~ (lc0 ':> b)) =>
LC lc -> Mb (c :++: lc) (Term a) -> PeelRet c (AddArrows lc a)
PeelRet (LC lc0
lc0 LC lc0 -> LType b -> LC (lc0 ':> b)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: LType b
ilt) Mb (c :++: lc) (Term a)
Mb (c :++: (lc0 ':> b)) (Term a)
t




boundParams ::
  lc ~ (lc0 :> b) => LC lc -> (RAssign Name lc -> DTerm a) ->
                     Decl (AddArrows lc a)
boundParams :: LC lc -> (RAssign Name lc -> DTerm a) -> Decl (AddArrows lc a)
boundParams (RAssign LType c
lc0 :>: LType a
LType) RAssign Name lc -> DTerm a
k = -- flagged as non-exhaustive, in spite of type
  RAssign LType c
-> (RAssign Name c -> Decl (a -> a)) -> Decl (AddArrows c (a -> a))
forall (lc :: RList *) a.
LC lc -> (RAssign Name lc -> Decl a) -> Decl (AddArrows lc a)
freeParams RAssign LType c
lc0 (\RAssign Name c
ns -> Binding (L a) (DTerm a) -> Decl (a -> a)
forall a a. Binding (L a) (DTerm a) -> Decl (a -> a)
Decl_One (Binding (L a) (DTerm a) -> Decl (a -> a))
-> Binding (L a) (DTerm a) -> Decl (a -> a)
forall a b. (a -> b) -> a -> b
$ (Name (L a) -> DTerm a) -> Binding (L a) (DTerm a)
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu ((Name (L a) -> DTerm a) -> Binding (L a) (DTerm a))
-> (Name (L a) -> DTerm a) -> Binding (L a) (DTerm a)
forall a b. (a -> b) -> a -> b
$ \Name (L a)
n -> RAssign Name lc -> DTerm a
k (RAssign Name c
ns RAssign Name c -> Name (L a) -> RAssign Name (c ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Name (L a)
n))

freeParams ::
  LC lc -> (RAssign Name lc -> Decl a) -> Decl (AddArrows lc a)
freeParams :: LC lc -> (RAssign Name lc -> Decl a) -> Decl (AddArrows lc a)
freeParams LC lc
MNil RAssign Name lc -> Decl a
k = RAssign Name lc -> Decl a
k RAssign Name lc
forall k (f :: k -> *). RAssign f 'RNil
C.empty
freeParams (RAssign LType c
lc :>: LType a
LType) RAssign Name lc -> Decl a
k =
    RAssign LType c
-> (RAssign Name c -> Decl (a -> a)) -> Decl (AddArrows c (a -> a))
forall (lc :: RList *) a.
LC lc -> (RAssign Name lc -> Decl a) -> Decl (AddArrows lc a)
freeParams RAssign LType c
lc (\RAssign Name c
names -> Binding (L a) (Decl a) -> Decl (a -> a)
forall a b. Binding (L a) (Decl b) -> Decl (a -> b)
Decl_Cons (Binding (L a) (Decl a) -> Decl (a -> a))
-> Binding (L a) (Decl a) -> Decl (a -> a)
forall a b. (a -> b) -> a -> b
$ (Name (L a) -> Decl a) -> Binding (L a) (Decl a)
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu ((Name (L a) -> Decl a) -> Binding (L a) (Decl a))
-> (Name (L a) -> Decl a) -> Binding (L a) (Decl a)
forall a b. (a -> b) -> a -> b
$ \Name (L a)
x -> RAssign Name lc -> Decl a
k (RAssign Name c
names RAssign Name c -> Name (L a) -> RAssign Name (c ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Name (L a)
x))

------------------------------------------------------------
-- sub-contexts
------------------------------------------------------------

-- FIXME: use this type in place of functions
type SubC c' c = RAssign Name c -> RAssign Name c'

------------------------------------------------------------
-- operations on contexts of free variables
------------------------------------------------------------

data MbLName c a where
    MbLName :: Mb c (Name (L a)) -> MbLName c (L a)

type FVList c fvs = RAssign (MbLName c) fvs

-- unioning free variable contexts: the data structure
data FVUnionRet c fvs1 fvs2 where
    FVUnionRet :: FVList c fvs -> SubC fvs1 fvs -> SubC fvs2 fvs ->
                  FVUnionRet c fvs1 fvs2

fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
fvUnion FVList c fvs1
MNil FVList c fvs2
MNil = FVList c 'RNil
-> SubC 'RNil 'RNil -> SubC 'RNil 'RNil -> FVUnionRet c 'RNil 'RNil
forall (c :: RList *) (fvs :: RList *) (fvs1 :: RList *)
       (fvs2 :: RList *).
FVList c fvs
-> SubC fvs1 fvs -> SubC fvs2 fvs -> FVUnionRet c fvs1 fvs2
FVUnionRet FVList c 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil (\RAssign Name 'RNil
_ -> RAssign Name 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil) (\RAssign Name 'RNil
_ -> RAssign Name 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil)
fvUnion FVList c fvs1
MNil (RAssign (MbLName c) c
fvs2 :>: MbLName c a
fv2) = case FVList c 'RNil -> RAssign (MbLName c) c -> FVUnionRet c 'RNil c
forall (c :: RList *) (fvs1 :: RList *) (fvs2 :: RList *).
FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
fvUnion FVList c 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign (MbLName c) c
fvs2 of
  FVUnionRet FVList c fvs
fvs SubC 'RNil fvs
f1 SubC c fvs
f2 -> case MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
forall (c :: RList *) a (fvs :: RList *).
MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
elemMC MbLName c a
fv2 FVList c fvs
fvs of
    Maybe (Member fvs a)
Nothing -> FVList c (fvs ':> a)
-> SubC fvs1 (fvs ':> a)
-> SubC fvs2 (fvs ':> a)
-> FVUnionRet c fvs1 fvs2
forall (c :: RList *) (fvs :: RList *) (fvs1 :: RList *)
       (fvs2 :: RList *).
FVList c fvs
-> SubC fvs1 fvs -> SubC fvs2 fvs -> FVUnionRet c fvs1 fvs2
FVUnionRet (FVList c fvs
fvs FVList c fvs -> MbLName c a -> FVList c (fvs ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: MbLName c a
fv2)
               (\(RAssign Name c
xs :>: Name a
_) -> SubC 'RNil fvs
f1 RAssign Name fvs
RAssign Name c
xs) (\(RAssign Name c
xs :>: Name a
x) -> SubC c fvs
f2 RAssign Name fvs
RAssign Name c
xs RAssign Name c -> Name a -> RAssign Name (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Name a
x)
    Just Member fvs a
idx -> FVList c fvs
-> SubC 'RNil fvs
-> SubC (c ':> a) fvs
-> FVUnionRet c 'RNil (c ':> a)
forall (c :: RList *) (fvs :: RList *) (fvs1 :: RList *)
       (fvs2 :: RList *).
FVList c fvs
-> SubC fvs1 fvs -> SubC fvs2 fvs -> FVUnionRet c fvs1 fvs2
FVUnionRet FVList c fvs
fvs SubC 'RNil fvs
f1 (\RAssign Name fvs
xs -> SubC c fvs
f2 RAssign Name fvs
xs RAssign Name c -> Name a -> RAssign Name (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Member fvs a -> RAssign Name fvs -> Name a
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
C.get Member fvs a
idx RAssign Name fvs
xs)
fvUnion (RAssign (MbLName c) c
fvs1 :>: MbLName c a
fv1) FVList c fvs2
fvs2 = case RAssign (MbLName c) c -> FVList c fvs2 -> FVUnionRet c c fvs2
forall (c :: RList *) (fvs1 :: RList *) (fvs2 :: RList *).
FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
fvUnion RAssign (MbLName c) c
fvs1 FVList c fvs2
fvs2 of
  FVUnionRet FVList c fvs
fvs SubC c fvs
f1 SubC fvs2 fvs
f2 -> case MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
forall (c :: RList *) a (fvs :: RList *).
MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
elemMC MbLName c a
fv1 FVList c fvs
fvs of
    Maybe (Member fvs a)
Nothing -> FVList c (fvs ':> a)
-> SubC fvs1 (fvs ':> a)
-> SubC fvs2 (fvs ':> a)
-> FVUnionRet c fvs1 fvs2
forall (c :: RList *) (fvs :: RList *) (fvs1 :: RList *)
       (fvs2 :: RList *).
FVList c fvs
-> SubC fvs1 fvs -> SubC fvs2 fvs -> FVUnionRet c fvs1 fvs2
FVUnionRet (FVList c fvs
fvs FVList c fvs -> MbLName c a -> FVList c (fvs ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: MbLName c a
fv1)
               (\(RAssign Name c
xs :>: Name a
x) -> SubC c fvs
f1 RAssign Name fvs
RAssign Name c
xs RAssign Name c -> Name a -> RAssign Name (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Name a
x) (\(RAssign Name c
xs :>: Name a
_) -> SubC fvs2 fvs
f2 RAssign Name fvs
RAssign Name c
xs)
    Just Member fvs a
idx -> FVList c fvs
-> SubC (c ':> a) fvs
-> SubC fvs2 fvs
-> FVUnionRet c (c ':> a) fvs2
forall (c :: RList *) (fvs :: RList *) (fvs1 :: RList *)
       (fvs2 :: RList *).
FVList c fvs
-> SubC fvs1 fvs -> SubC fvs2 fvs -> FVUnionRet c fvs1 fvs2
FVUnionRet FVList c fvs
fvs (\RAssign Name fvs
xs -> SubC c fvs
f1 RAssign Name fvs
xs RAssign Name c -> Name a -> RAssign Name (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Member fvs a -> RAssign Name fvs -> Name a
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
C.get Member fvs a
idx RAssign Name fvs
xs) SubC fvs2 fvs
f2

elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
elemMC MbLName c a
_ FVList c fvs
MNil = Maybe (Member fvs a)
forall a. Maybe a
Nothing
elemMC mbLN :: MbLName c a
mbLN@(MbLName Mb c (Name (L a))
n) (RAssign (MbLName c) c
mc :>: MbLName Mb c (Name (L a))
n') = case Mb c (Name (L a)) -> Mb c (Name (L a)) -> Maybe (L a :~: L a)
forall k1 k2 (a :: k1) (b :: k1) (c :: RList k2).
Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)
mbCmpName Mb c (Name (L a))
n Mb c (Name (L a))
n' of
  Just L a :~: L a
Refl -> Member (c ':> a) a -> Maybe (Member (c ':> a) a)
forall a. a -> Maybe a
Just Member (c ':> a) a
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
  Maybe (L a :~: L a)
Nothing -> (Member c a -> Member (c ':> L a) a)
-> Maybe (Member c a) -> Maybe (Member (c ':> L a) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Member c a -> Member (c ':> L a) a
forall k1 k2 (ctx :: RList k1) (a :: k2) (b :: k1).
Member ctx a -> Member (ctx ':> b) a
Member_Step (MbLName c a -> RAssign (MbLName c) c -> Maybe (Member c a)
forall (c :: RList *) a (fvs :: RList *).
MbLName c a -> FVList c fvs -> Maybe (Member fvs a)
elemMC MbLName c a
mbLN RAssign (MbLName c) c
mc)

------------------------------------------------------------
-- deBruijn terms, i.e., closed terms
------------------------------------------------------------

data STerm c a where
    SWeaken :: SubC c1 c -> STerm c1 a -> STerm c a
    SVar :: Member c (L a) -> STerm c a
    SDVar :: Name (D a) -> STerm c a
    SApp :: STerm c (a -> b) -> STerm c a -> STerm c b

skelSubst :: STerm c a -> RAssign Name c -> DTerm a
skelSubst :: STerm c a -> RAssign Name c -> DTerm a
skelSubst (SWeaken SubC c1 c
f STerm c1 a
db) RAssign Name c
names = STerm c1 a -> RAssign Name c1 -> DTerm a
forall (c :: RList *) a. STerm c a -> RAssign Name c -> DTerm a
skelSubst STerm c1 a
db (RAssign Name c1 -> DTerm a) -> RAssign Name c1 -> DTerm a
forall a b. (a -> b) -> a -> b
$ SubC c1 c
f RAssign Name c
names
skelSubst (SVar Member c (L a)
inC) RAssign Name c
names = Name (L a) -> DTerm a
forall a. Name (L a) -> DTerm a
TVar (Name (L a) -> DTerm a) -> Name (L a) -> DTerm a
forall a b. (a -> b) -> a -> b
$ Member c (L a) -> RAssign Name c -> Name (L a)
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
C.get Member c (L a)
inC RAssign Name c
names
skelSubst (SDVar Name (D a)
dTVar) RAssign Name c
_ = Name (D a) -> DTerm a
forall a. Name (D a) -> DTerm a
TDVar Name (D a)
dTVar
skelSubst (SApp STerm c (a -> a)
db1 STerm c a
db2) RAssign Name c
names = DTerm (a -> a) -> DTerm a -> DTerm a
forall a b. DTerm (a -> b) -> DTerm a -> DTerm b
TApp (STerm c (a -> a) -> RAssign Name c -> DTerm (a -> a)
forall (c :: RList *) a. STerm c a -> RAssign Name c -> DTerm a
skelSubst STerm c (a -> a)
db1 RAssign Name c
names) (STerm c a -> RAssign Name c -> DTerm a
forall (c :: RList *) a. STerm c a -> RAssign Name c -> DTerm a
skelSubst STerm c a
db2 RAssign Name c
names)

-- applying a STerm to a context of names
skelAppMultiNames ::
  STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
skelAppMultiNames :: STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
skelAppMultiNames STerm fvs (AddArrows fvs a)
db FVList c fvs
args = STerm fvs (AddArrows fvs a)
-> FVList c fvs -> RAssign (Member fvs) fvs -> STerm fvs a
forall (fvs :: RList *) (args :: RList *) a (c :: RList *).
STerm fvs (AddArrows args a)
-> FVList c args -> RAssign (Member fvs) args -> STerm fvs a
skelAppMultiNamesH STerm fvs (AddArrows fvs a)
db FVList c fvs
args (FVList c fvs -> RAssign (Member fvs) fvs
forall k (f :: k -> *) (c :: RList k).
RAssign f c -> RAssign (Member c) c
C.members FVList c fvs
args) where
  skelAppMultiNamesH ::
    STerm fvs (AddArrows args a) -> FVList c args -> RAssign (Member fvs) args ->
    STerm fvs a
  skelAppMultiNamesH :: STerm fvs (AddArrows args a)
-> FVList c args -> RAssign (Member fvs) args -> STerm fvs a
skelAppMultiNamesH STerm fvs (AddArrows args a)
fvs FVList c args
MNil RAssign (Member fvs) args
_ = STerm fvs a
STerm fvs (AddArrows args a)
fvs
  -- flagged as non-exhaustive, in spite of type
  skelAppMultiNamesH STerm fvs (AddArrows args a)
fvs (RAssign (MbLName c) c
args :>: MbLName Mb c (Name (L a))
_) (RAssign (Member fvs) c
inCs :>: Member fvs a
inC) =
    STerm fvs (a -> a) -> STerm fvs a -> STerm fvs a
forall (c :: RList *) a b.
STerm c (a -> b) -> STerm c a -> STerm c b
SApp (STerm fvs (AddArrows c (a -> a))
-> RAssign (MbLName c) c
-> RAssign (Member fvs) c
-> STerm fvs (a -> a)
forall (fvs :: RList *) (args :: RList *) a (c :: RList *).
STerm fvs (AddArrows args a)
-> FVList c args -> RAssign (Member fvs) args -> STerm fvs a
skelAppMultiNamesH STerm fvs (AddArrows args a)
STerm fvs (AddArrows c (a -> a))
fvs RAssign (MbLName c) c
args RAssign (Member fvs) c
RAssign (Member fvs) c
inCs) (Member fvs (L a) -> STerm fvs a
forall (c :: RList *) a. Member c (L a) -> STerm c a
SVar Member fvs a
Member fvs (L a)
inC)

------------------------------------------------------------
-- STerms combined with their free variables
------------------------------------------------------------

proxyCons :: Proxy r -> f a -> Proxy (r :> a)
proxyCons :: Proxy r -> f a -> Proxy (r ':> a)
proxyCons Proxy r
_ f a
_ = Proxy (r ':> a)
forall k (t :: k). Proxy t
Proxy

data FVSTerm c lc a where
    FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a

fvSSepLTVars ::
  RAssign f lc -> FVSTerm (c :++: lc) RNil a -> FVSTerm c lc a
fvSSepLTVars :: RAssign f lc -> FVSTerm (c :++: lc) 'RNil a -> FVSTerm c lc a
fvSSepLTVars RAssign f lc
lc (FVSTerm FVList (c :++: lc) fvs
fvs STerm (fvs :++: 'RNil) a
db) = case RAssign f lc
-> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
forall (f :: * -> *) (lc :: RList *) (c :: RList *)
       (fvs :: RList *).
RAssign f lc
-> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
fvSSepLTVarsH RAssign f lc
lc Proxy c
forall k (t :: k). Proxy t
Proxy FVList (c :++: lc) fvs
fvs of
  SepRet FVList c fvs'
fvs' SubC fvs (fvs' :++: lc)
f -> FVList c fvs' -> STerm (fvs' :++: lc) a -> FVSTerm c lc a
forall (c :: RList *) (fvs :: RList *) (lc :: RList *) a.
FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
FVSTerm FVList c fvs'
fvs' (SubC fvs (fvs' :++: lc) -> STerm fvs a -> STerm (fvs' :++: lc) a
forall (c1 :: RList *) (c :: RList *) a.
SubC c1 c -> STerm c1 a -> STerm c a
SWeaken SubC fvs (fvs' :++: lc)
f STerm fvs a
STerm (fvs :++: 'RNil) a
db)

data SepRet lc c fvs where
  SepRet :: FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs

-- | Create a 'Proxy' object for the type list of a 'RAssign' vector.
proxyOfRAssign :: RAssign f c -> Proxy c
proxyOfRAssign :: RAssign f c -> Proxy c
proxyOfRAssign RAssign f c
_ = Proxy c
forall k (t :: k). Proxy t
Proxy

fvSSepLTVarsH ::
  RAssign f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
fvSSepLTVarsH :: RAssign f lc
-> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
fvSSepLTVarsH RAssign f lc
_ Proxy c
_ FVList (c :++: lc) fvs
MNil = FVList c 'RNil -> SubC 'RNil ('RNil :++: lc) -> SepRet lc c 'RNil
forall (c :: RList *) (fvs' :: RList *) (fvs :: RList *)
       (lc :: RList *).
FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs
SepRet FVList c 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil (\RAssign Name ('RNil :++: lc)
_ -> RAssign Name 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil)
fvSSepLTVarsH RAssign f lc
lc Proxy c
c (RAssign (MbLName (c :++: lc)) c
fvs :>: fv :: MbLName (c :++: lc) a
fv@(MbLName Mb (c :++: lc) (Name (L a))
n)) = case RAssign f lc
-> Proxy c -> RAssign (MbLName (c :++: lc)) c -> SepRet lc c c
forall (f :: * -> *) (lc :: RList *) (c :: RList *)
       (fvs :: RList *).
RAssign f lc
-> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs
fvSSepLTVarsH RAssign f lc
lc Proxy c
c RAssign (MbLName (c :++: lc)) c
fvs of
  SepRet FVList c fvs'
m SubC c (fvs' :++: lc)
f -> case Append c lc (c :++: lc)
-> Mb (c :++: lc) (Name (L a))
-> Either (Member lc (L a)) (Mb c (Name (L a)))
forall (c1 :: RList *) (c2 :: RList *) a.
Append c1 c2 (c1 :++: c2)
-> Mb (c1 :++: c2) (Name a)
-> Either (Member c2 a) (Mb c1 (Name a))
raiseAppName (Proxy c -> RAssign f lc -> Append c lc (c :++: lc)
forall k (c1 :: RList k) (f :: k -> *) (c2 :: RList k).
Proxy c1 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)
C.mkMonoAppend Proxy c
c RAssign f lc
lc) Mb (c :++: lc) (Name (L a))
n of
    Left Member lc (L a)
idx ->
      FVList c fvs'
-> SubC (c ':> L a) (fvs' :++: lc) -> SepRet lc c (c ':> L a)
forall (c :: RList *) (fvs' :: RList *) (fvs :: RList *)
       (lc :: RList *).
FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs
SepRet FVList c fvs'
m (\RAssign Name (fvs' :++: lc)
xs ->
                 SubC c (fvs' :++: lc)
f RAssign Name (fvs' :++: lc)
xs RAssign Name c -> Name (L a) -> RAssign Name (c ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Member (fvs' :++: lc) (L a)
-> RAssign Name (fvs' :++: lc) -> Name (L a)
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
C.get (Proxy fvs' -> Member lc (L a) -> Member (fvs' :++: lc) (L a)
forall k1 k2 (r1 :: RList k1) (r2 :: RList k1) (a :: k2).
Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a
C.weakenMemberL (FVList c fvs' -> Proxy fvs'
forall (f :: * -> *) (c :: RList *). RAssign f c -> Proxy c
proxyOfRAssign FVList c fvs'
m) Member lc (L a)
idx) RAssign Name (fvs' :++: lc)
xs)
    Right Mb c (Name (L a))
n ->
      FVList c (fvs' ':> L a)
-> SubC fvs ((fvs' ':> L a) :++: lc) -> SepRet lc c fvs
forall (c :: RList *) (fvs' :: RList *) (fvs :: RList *)
       (lc :: RList *).
FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs
SepRet (FVList c fvs'
m FVList c fvs' -> MbLName c (L a) -> FVList c (fvs' ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Mb c (Name (L a)) -> MbLName c (L a)
forall (c :: RList *) a. Mb c (Name (L a)) -> MbLName c (L a)
MbLName Mb c (Name (L a))
n)
      (\RAssign Name ((fvs' ':> L a) :++: lc)
xs -> case Proxy (fvs' ':> a)
-> RAssign f lc
-> RAssign Name ((fvs' ':> L a) :++: lc)
-> (RAssign Name (fvs' ':> a), RAssign Name lc)
forall k (c :: RList k) (c1 :: RList k) (c2 :: RList k)
       (prx :: RList k -> *) (any :: k -> *) (f :: k -> *).
(c ~ (c1 :++: c2)) =>
prx c1
-> RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)
C.split Proxy (fvs' ':> a)
c' RAssign f lc
lc RAssign Name ((fvs' ':> L a) :++: lc)
xs of
          (RAssign Name c
fvs' :>: Name a
fv', RAssign Name lc
lcs) ->
            SubC c (fvs' :++: lc)
f (RAssign Name c -> RAssign Name lc -> RAssign Name (c :++: lc)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
C.append RAssign Name c
fvs' RAssign Name lc
lcs) RAssign Name c -> Name a -> RAssign Name (c ':> a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Name a
fv')
    where c' :: Proxy (fvs' ':> a)
c' = Proxy fvs' -> MbLName (c :++: lc) a -> Proxy (fvs' ':> a)
forall (r :: RList *) (f :: * -> *) a.
Proxy r -> f a -> Proxy (r ':> a)
proxyCons (FVList c fvs' -> Proxy fvs'
forall (f :: * -> *) (c :: RList *). RAssign f c -> Proxy c
proxyOfRAssign FVList c fvs'
m) MbLName (c :++: lc) a
fv

raiseAppName ::
  Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
raiseAppName :: Append c1 c2 (c1 :++: c2)
-> Mb (c1 :++: c2) (Name a)
-> Either (Member c2 a) (Mb c1 (Name a))
raiseAppName Append c1 c2 (c1 :++: c2)
app Mb (c1 :++: c2) (Name a)
n =
  case (Mb c2 (Name a) -> Either (Member c2 a) (Name a))
-> Mb c1 (Mb c2 (Name a)) -> Mb c1 (Either (Member c2 a) (Name a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Mb c2 (Name a) -> Either (Member c2 a) (Name a)
forall k1 k2 (a :: k1) (ctx :: RList k2).
Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP (RAssign Proxy c2
-> Mb (c1 :++: c2) (Name a) -> Mb c1 (Mb c2 (Name a))
forall k (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a.
RAssign any ctx2 -> Mb (ctx1 :++: ctx2) a -> Mb ctx1 (Mb ctx2 a)
mbSeparate (Append c1 c2 (c1 :++: c2) -> RAssign Proxy c2
forall k (c1 :: RList k) (c2 :: RList k) (c :: RList k).
Append c1 c2 c -> RAssign Proxy c2
C.proxiesFromAppend Append c1 c2 (c1 :++: c2)
app) Mb (c1 :++: c2) (Name a)
n) of
    Mb c1 (Either (Member c2 a) (Name a))
[nuP| Left mem |] -> Member c2 a -> Either (Member c2 a) (Mb c1 (Name a))
forall a b. a -> Either a b
Left (Member c2 a -> Either (Member c2 a) (Mb c1 (Name a)))
-> Member c2 a -> Either (Member c2 a) (Mb c1 (Name a))
forall a b. (a -> b) -> a -> b
$ Mb c1 (Member c2 a) -> Member c2 a
forall a k (ctx :: RList k). Liftable a => Mb ctx a -> a
mbLift Mb c1 (Member c2 a)
mem
    Mb c1 (Either (Member c2 a) (Name a))
[nuP| Right n |] -> Mb c1 (Name a) -> Either (Member c2 a) (Mb c1 (Name a))
forall a b. b -> Either a b
Right Mb c1 (Name a)
n

------------------------------------------------------------
-- lambda-lifting, woo hoo!
------------------------------------------------------------

type LLBodyRet b c a = Cont (Decls b) (FVSTerm c RNil a)

llBody :: LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody :: LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody LC c
_ Mb c (Term a)
[nuP| Var v |] =
  FVSTerm c 'RNil a -> LLBodyRet b c a
forall (m :: * -> *) a. Monad m => a -> m a
return (FVSTerm c 'RNil a -> LLBodyRet b c a)
-> FVSTerm c 'RNil a -> LLBodyRet b c a
forall a b. (a -> b) -> a -> b
$ FVList c ('RNil ':> L a)
-> STerm (('RNil ':> L a) :++: 'RNil) a -> FVSTerm c 'RNil a
forall (c :: RList *) (fvs :: RList *) (lc :: RList *) a.
FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
FVSTerm (RAssign (MbLName c) 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil RAssign (MbLName c) 'RNil
-> MbLName c (L a) -> FVList c ('RNil ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: Mb c (Name (L a)) -> MbLName c (L a)
forall (c :: RList *) a. Mb c (Name (L a)) -> MbLName c (L a)
MbLName Mb c (Name (L a))
v) (STerm (('RNil ':> L a) :++: 'RNil) a -> FVSTerm c 'RNil a)
-> STerm (('RNil ':> L a) :++: 'RNil) a -> FVSTerm c 'RNil a
forall a b. (a -> b) -> a -> b
$ Member ('RNil ':> L a) (L a) -> STerm ('RNil ':> L a) a
forall (c :: RList *) a. Member c (L a) -> STerm c a
SVar Member ('RNil ':> L a) (L a)
forall k2 (ctx :: RList k2) (ctx :: k2). Member (ctx ':> ctx) ctx
Member_Base
llBody LC c
c Mb c (Term a)
[nuP| App t1 t2 |] = do
  FVSTerm FVList c fvs
fvs1 STerm (fvs :++: 'RNil) (b -> a)
db1 <- LC c -> Mb c (Term (b -> a)) -> LLBodyRet b c (b -> a)
forall (c :: RList *) a b. LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody LC c
c Mb c (Term (b -> a))
t1
  FVSTerm FVList c fvs
fvs2 STerm (fvs :++: 'RNil) b
db2 <- LC c -> Mb c (Term b) -> LLBodyRet b c b
forall (c :: RList *) a b. LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody LC c
c Mb c (Term b)
t2
  FVUnionRet FVList c fvs
names SubC fvs fvs
sub1 SubC fvs fvs
sub2 <- FVUnionRet c fvs fvs
-> ContT (Decls b) Identity (FVUnionRet c fvs fvs)
forall (m :: * -> *) a. Monad m => a -> m a
return (FVUnionRet c fvs fvs
 -> ContT (Decls b) Identity (FVUnionRet c fvs fvs))
-> FVUnionRet c fvs fvs
-> ContT (Decls b) Identity (FVUnionRet c fvs fvs)
forall a b. (a -> b) -> a -> b
$ FVList c fvs -> FVList c fvs -> FVUnionRet c fvs fvs
forall (c :: RList *) (fvs1 :: RList *) (fvs2 :: RList *).
FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2
fvUnion FVList c fvs
fvs1 FVList c fvs
fvs2
  FVSTerm c 'RNil a -> LLBodyRet b c a
forall (m :: * -> *) a. Monad m => a -> m a
return (FVSTerm c 'RNil a -> LLBodyRet b c a)
-> FVSTerm c 'RNil a -> LLBodyRet b c a
forall a b. (a -> b) -> a -> b
$ FVList c fvs -> STerm (fvs :++: 'RNil) a -> FVSTerm c 'RNil a
forall (c :: RList *) (fvs :: RList *) (lc :: RList *) a.
FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
FVSTerm FVList c fvs
names (STerm (fvs :++: 'RNil) a -> FVSTerm c 'RNil a)
-> STerm (fvs :++: 'RNil) a -> FVSTerm c 'RNil a
forall a b. (a -> b) -> a -> b
$ STerm fvs (b -> a) -> STerm fvs b -> STerm fvs a
forall (c :: RList *) a b.
STerm c (a -> b) -> STerm c a -> STerm c b
SApp (SubC fvs fvs -> STerm fvs (b -> a) -> STerm fvs (b -> a)
forall (c1 :: RList *) (c :: RList *) a.
SubC c1 c -> STerm c1 a -> STerm c a
SWeaken SubC fvs fvs
sub1 STerm fvs (b -> a)
STerm (fvs :++: 'RNil) (b -> a)
db1) (SubC fvs fvs -> STerm fvs b -> STerm fvs b
forall (c1 :: RList *) (c :: RList *) a.
SubC c1 c -> STerm c1 a -> STerm c a
SWeaken SubC fvs fvs
sub2 STerm fvs b
STerm (fvs :++: 'RNil) b
db2)
llBody LC c
c Mb c (Term a)
[nuP| Lam b |] = do
  PeelRet LC lc
lc Mb (c :++: lc) (Term a)
body <- PeelRet c (b -> a) -> ContT (Decls b) Identity (PeelRet c (b -> a))
forall (m :: * -> *) a. Monad m => a -> m a
return (PeelRet c (b -> a)
 -> ContT (Decls b) Identity (PeelRet c (b -> a)))
-> PeelRet c (b -> a)
-> ContT (Decls b) Identity (PeelRet c (b -> a))
forall a b. (a -> b) -> a -> b
$ Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
forall (c :: RList *) b a.
Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)
peelLambdas Mb c (Binding (L b) (Term a))
b
  FVSTerm ((c :++: lc0) ':> b) 'RNil a
llret <- LC ((c :++: lc0) ':> b)
-> Mb ((c :++: lc0) ':> b) (Term a)
-> LLBodyRet b ((c :++: lc0) ':> b) a
forall (c :: RList *) a b. LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody (LC c -> LC lc -> RAssign LType (c :++: lc)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
C.append LC c
c LC lc
lc) Mb (c :++: lc) (Term a)
Mb ((c :++: lc0) ':> b) (Term a)
body
  FVSTerm FVList c fvs
fvs STerm (fvs :++: lc) a
db <- FVSTerm c lc a -> ContT (Decls b) Identity (FVSTerm c lc a)
forall (m :: * -> *) a. Monad m => a -> m a
return (FVSTerm c lc a -> ContT (Decls b) Identity (FVSTerm c lc a))
-> FVSTerm c lc a -> ContT (Decls b) Identity (FVSTerm c lc a)
forall a b. (a -> b) -> a -> b
$ LC lc -> FVSTerm (c :++: lc) 'RNil a -> FVSTerm c lc a
forall (f :: * -> *) (lc :: RList *) (c :: RList *) a.
RAssign f lc -> FVSTerm (c :++: lc) 'RNil a -> FVSTerm c lc a
fvSSepLTVars LC lc
lc FVSTerm (c :++: lc) 'RNil a
FVSTerm ((c :++: lc0) ':> b) 'RNil a
llret
  ((FVSTerm c 'RNil a -> Decls b) -> Decls b) -> LLBodyRet b c a
forall a r. ((a -> r) -> r) -> Cont r a
cont (((FVSTerm c 'RNil a -> Decls b) -> Decls b) -> LLBodyRet b c a)
-> ((FVSTerm c 'RNil a -> Decls b) -> Decls b) -> LLBodyRet b c a
forall a b. (a -> b) -> a -> b
$ \FVSTerm c 'RNil a -> Decls b
k ->
    Decl (AddArrows fvs (b -> a))
-> Binding (D (AddArrows fvs (b -> a))) (Decls b) -> Decls b
forall b a. Decl b -> Binding (D b) (Decls a) -> Decls a
Decls_Cons (LC fvs
-> (RAssign Name fvs -> Decl (b -> a))
-> Decl (AddArrows fvs (b -> a))
forall (lc :: RList *) a.
LC lc -> (RAssign Name lc -> Decl a) -> Decl (AddArrows lc a)
freeParams (FVList c fvs -> LC fvs
forall (c :: RList *) (lc :: RList *). FVList c lc -> LC lc
fvsToLC FVList c fvs
fvs) ((RAssign Name fvs -> Decl (b -> a))
 -> Decl (AddArrows fvs (b -> a)))
-> (RAssign Name fvs -> Decl (b -> a))
-> Decl (AddArrows fvs (b -> a))
forall a b. (a -> b) -> a -> b
$ \RAssign Name fvs
names1 ->
                LC lc -> (RAssign Name lc -> DTerm a) -> Decl (AddArrows lc a)
forall (lc :: RList *) (lc0 :: RList *) b a.
(lc ~ (lc0 ':> b)) =>
LC lc -> (RAssign Name lc -> DTerm a) -> Decl (AddArrows lc a)
boundParams LC lc
lc ((RAssign Name lc -> DTerm a) -> Decl (AddArrows lc a))
-> (RAssign Name lc -> DTerm a) -> Decl (AddArrows lc a)
forall a b. (a -> b) -> a -> b
$ \RAssign Name lc
names2 ->
                STerm ((fvs :++: lc0) ':> b) a
-> RAssign Name ((fvs :++: lc0) ':> b) -> DTerm a
forall (c :: RList *) a. STerm c a -> RAssign Name c -> DTerm a
skelSubst STerm (fvs :++: lc) a
STerm ((fvs :++: lc0) ':> b) a
db (RAssign Name fvs -> RAssign Name lc -> RAssign Name (fvs :++: lc)
forall k (f :: k -> *) (c1 :: RList k) (c2 :: RList k).
RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)
C.append RAssign Name fvs
names1 RAssign Name lc
names2))
      (Binding (D (AddArrows fvs (b -> a))) (Decls b) -> Decls b)
-> Binding (D (AddArrows fvs (b -> a))) (Decls b) -> Decls b
forall a b. (a -> b) -> a -> b
$ (Name (D (AddArrows fvs (b -> a))) -> Decls b)
-> Binding (D (AddArrows fvs (b -> a))) (Decls b)
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu ((Name (D (AddArrows fvs (b -> a))) -> Decls b)
 -> Binding (D (AddArrows fvs (b -> a))) (Decls b))
-> (Name (D (AddArrows fvs (b -> a))) -> Decls b)
-> Binding (D (AddArrows fvs (b -> a))) (Decls b)
forall a b. (a -> b) -> a -> b
$ \Name (D (AddArrows fvs (b -> a)))
d -> FVSTerm c 'RNil a -> Decls b
k (FVSTerm c 'RNil a -> Decls b) -> FVSTerm c 'RNil a -> Decls b
forall a b. (a -> b) -> a -> b
$ FVList c fvs -> STerm (fvs :++: 'RNil) a -> FVSTerm c 'RNil a
forall (c :: RList *) (fvs :: RList *) (lc :: RList *) a.
FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a
FVSTerm FVList c fvs
fvs (STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
forall (fvs :: RList *) a (c :: RList *).
STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a
skelAppMultiNames (Name (D (AddArrows fvs (b -> a)))
-> STerm fvs (AddArrows fvs (b -> a))
forall a (c :: RList *). Name (D a) -> STerm c a
SDVar Name (D (AddArrows fvs (b -> a)))
d) FVList c fvs
fvs)
  where
    fvsToLC :: FVList c lc -> LC lc
    fvsToLC :: FVList c lc -> LC lc
fvsToLC = (forall x. MbLName c x -> LType x) -> FVList c lc -> LC lc
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
C.mapRAssign forall x. MbLName c x -> LType x
forall (c :: RList *) a. MbLName c a -> LType a
mbLNameToProof where
      mbLNameToProof :: MbLName c a -> LType a
      mbLNameToProof :: MbLName c a -> LType a
mbLNameToProof (MbLName Mb c (Name (L a))
_) = LType a
forall a. LType (L a)
LType

-- the top-level lambda-lifting function
lambdaLift :: Term a -> Decls a
lambdaLift :: Term a -> Decls a
lambdaLift Term a
t = Cont (Decls a) (FVSTerm 'RNil 'RNil a)
-> (FVSTerm 'RNil 'RNil a -> Decls a) -> Decls a
forall r a. Cont r a -> (a -> r) -> r
runCont (LC 'RNil
-> Mb 'RNil (Term a) -> Cont (Decls a) (FVSTerm 'RNil 'RNil a)
forall (c :: RList *) a b. LC c -> Mb c (Term a) -> LLBodyRet b c a
llBody LC 'RNil
forall k (f :: k -> *). RAssign f 'RNil
MNil (Term a -> Mb 'RNil (Term a)
forall k a. a -> Mb 'RNil a
emptyMb Term a
t)) ((FVSTerm 'RNil 'RNil a -> Decls a) -> Decls a)
-> (FVSTerm 'RNil 'RNil a -> Decls a) -> Decls a
forall a b. (a -> b) -> a -> b
$ \(FVSTerm FVList 'RNil fvs
fvs STerm (fvs :++: 'RNil) a
db) ->
  DTerm a -> Decls a
forall a. DTerm a -> Decls a
Decls_Base (STerm fvs a -> RAssign Name fvs -> DTerm a
forall (c :: RList *) a. STerm c a -> RAssign Name c -> DTerm a
skelSubst STerm fvs a
STerm (fvs :++: 'RNil) a
db ((forall x. MbLName 'RNil x -> Name x)
-> FVList 'RNil fvs -> RAssign Name fvs
forall k (f :: k -> *) (g :: k -> *) (c :: RList k).
(forall (x :: k). f x -> g x) -> RAssign f c -> RAssign g c
C.mapRAssign (\(MbLName mbn) -> Mb 'RNil (Name (L a)) -> Name (L a)
forall k a. Mb 'RNil a -> a
elimEmptyMb Mb 'RNil (Name (L a))
mbn) FVList 'RNil fvs
fvs))

mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)
mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)
mbLambdaLift = (Term a -> Decls a) -> Mb c (Term a) -> Mb c (Decls a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term a -> Decls a
forall a. Term a -> Decls a
lambdaLift