-- |
-- Module      : Data.Binding.Hobbits.SuperComb
-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner
--
-- License     : BSD3
--
-- Maintainer  : emw4@rice.edu
-- Stability   : experimental
-- Portability : GHC
--

module Data.Binding.Hobbits.Examples.LambdaLifting.Examples where

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

------------------------------------------------------------
-- examples
------------------------------------------------------------

ex1 :: Term ((b1 -> b) -> b1 -> b)
ex1 :: Term ((b1 -> b) -> b1 -> b)
ex1 = (Term (b1 -> b) -> Term (b1 -> b)) -> Term ((b1 -> b) -> b1 -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term (b1 -> b)
f -> ((Term b1 -> Term b) -> Term (b1 -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b1 -> Term b) -> Term (b1 -> b))
-> (Term b1 -> Term b) -> Term (b1 -> b)
forall a b. (a -> b) -> a -> b
$ \Term b1
x -> Term (b1 -> b) -> Term b1 -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b1 -> b)
f Term b1
x))

ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
ex2 = (Term (((b2 -> b1) -> b2 -> b1) -> b) -> Term b)
-> Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term (((b2 -> b1) -> b2 -> b1) -> b)
f1 -> Term (((b2 -> b1) -> b2 -> b1) -> b)
-> Term ((b2 -> b1) -> b2 -> b1) -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term (((b2 -> b1) -> b2 -> b1) -> b)
f1 ((Term (b2 -> b1) -> Term (b2 -> b1))
-> Term ((b2 -> b1) -> b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term (b2 -> b1)
f2 -> (Term b2 -> Term b1) -> Term (b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term b2
x -> Term (b2 -> b1) -> Term b2 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b2 -> b1)
f2 Term b2
x))))

ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
ex3 = (Term b3 -> Term ((((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b))
-> Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term b3
x -> (Term (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> Term b)
-> Term ((((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term (((b3 -> b2 -> b1) -> b2 -> b1) -> b)
f1 -> Term (((b3 -> b2 -> b1) -> b2 -> b1) -> b)
-> Term ((b3 -> b2 -> b1) -> b2 -> b1) -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term (((b3 -> b2 -> b1) -> b2 -> b1) -> b)
f1 ((Term (b3 -> b2 -> b1) -> Term (b2 -> b1))
-> Term ((b3 -> b2 -> b1) -> b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term (b3 -> b2 -> b1)
f2 -> (Term b2 -> Term b1) -> Term (b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term b2
y -> Term (b3 -> b2 -> b1)
f2 Term (b3 -> b2 -> b1) -> Term b3 -> Term (b2 -> b1)
forall b a. Term (b -> a) -> Term b -> Term a
`App` Term b3
x Term (b2 -> b1) -> Term b2 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
`App` Term b2
y)))))

ex4
  :: Term
       (((b1 -> b) -> b2 -> b)
        -> (((b1 -> b) -> b2 -> b) -> b2 -> b1)
        -> b2
        -> b1)
ex4 :: Term
  (((b1 -> b) -> b2 -> b)
   -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
ex4 = (Term ((b1 -> b) -> b2 -> b)
 -> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1))
-> Term
     (((b1 -> b) -> b2 -> b)
      -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term ((b1 -> b) -> b2 -> b)
  -> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1))
 -> Term
      (((b1 -> b) -> b2 -> b)
       -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1))
-> (Term ((b1 -> b) -> b2 -> b)
    -> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1))
-> Term
     (((b1 -> b) -> b2 -> b)
      -> (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
forall a b. (a -> b) -> a -> b
$ \Term ((b1 -> b) -> b2 -> b)
x -> (Term (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> Term (b2 -> b1))
-> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> Term (b2 -> b1))
 -> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1))
-> (Term (((b1 -> b) -> b2 -> b) -> b2 -> b1) -> Term (b2 -> b1))
-> Term ((((b1 -> b) -> b2 -> b) -> b2 -> b1) -> b2 -> b1)
forall a b. (a -> b) -> a -> b
$ \Term (((b1 -> b) -> b2 -> b) -> b2 -> b1)
f1 ->
      Term (((b1 -> b) -> b2 -> b) -> b2 -> b1)
-> Term ((b1 -> b) -> b2 -> b) -> Term (b2 -> b1)
forall b a. Term (b -> a) -> Term b -> Term a
App Term (((b1 -> b) -> b2 -> b) -> b2 -> b1)
f1 ((Term (b1 -> b) -> Term (b2 -> b)) -> Term ((b1 -> b) -> b2 -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term (b1 -> b) -> Term (b2 -> b)) -> Term ((b1 -> b) -> b2 -> b))
-> (Term (b1 -> b) -> Term (b2 -> b))
-> Term ((b1 -> b) -> b2 -> b)
forall a b. (a -> b) -> a -> b
$ \Term (b1 -> b)
f2 -> (Term b2 -> Term b) -> Term (b2 -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b2 -> Term b) -> Term (b2 -> b))
-> (Term b2 -> Term b) -> Term (b2 -> b)
forall a b. (a -> b) -> a -> b
$ \Term b2
y -> Term (b1 -> b)
f2 Term (b1 -> b) -> Term b1 -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
`App` (Term (((b1 -> b) -> b2 -> b) -> b2 -> b1)
f1 Term (((b1 -> b) -> b2 -> b) -> b2 -> b1)
-> Term ((b1 -> b) -> b2 -> b) -> Term (b2 -> b1)
forall b a. Term (b -> a) -> Term b -> Term a
`App` Term ((b1 -> b) -> b2 -> b)
x Term (b2 -> b1) -> Term b2 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
`App` Term b2
y))

ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
ex5 = (Term ((b2 -> b1) -> b) -> Term ((b2 -> b1) -> b))
-> Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam (\Term ((b2 -> b1) -> b)
f1 -> (Term (b2 -> b1) -> Term b) -> Term ((b2 -> b1) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term (b2 -> b1) -> Term b) -> Term ((b2 -> b1) -> b))
-> (Term (b2 -> b1) -> Term b) -> Term ((b2 -> b1) -> b)
forall a b. (a -> b) -> a -> b
$ \Term (b2 -> b1)
f2 -> Term ((b2 -> b1) -> b) -> Term (b2 -> b1) -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term ((b2 -> b1) -> b)
f1 ((Term b2 -> Term b1) -> Term (b2 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b2 -> Term b1) -> Term (b2 -> b1))
-> (Term b2 -> Term b1) -> Term (b2 -> b1)
forall a b. (a -> b) -> a -> b
$ \Term b2
x -> Term (b2 -> b1) -> Term b2 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b2 -> b1)
f2 Term b2
x))

-- lambda-lift with a free variable (use mbLambdaLift)
ex6 :: Binding (L ((b -> b) -> a)) (Term a)
ex6 :: Binding (L ((b -> b) -> a)) (Term a)
ex6 = (Name (L ((b -> b) -> a)) -> Term a)
-> Binding (L ((b -> b) -> a)) (Term a)
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu (\Name (L ((b -> b) -> a))
f -> Term ((b -> b) -> a) -> Term (b -> b) -> Term a
forall b a. Term (b -> a) -> Term b -> Term a
App (Name (L ((b -> b) -> a)) -> Term ((b -> b) -> a)
forall a. Name (L a) -> Term a
Var Name (L ((b -> b) -> a))
f) ((Term b -> Term b) -> Term (b -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b -> Term b) -> Term (b -> b))
-> (Term b -> Term b) -> Term (b -> b)
forall a b. (a -> b) -> a -> b
$ \Term b
x -> Term b
x))

-- lambda-lift with a free variable as part of a lambda's environment
ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
ex7 = (Name (L ((b2 -> b2) -> b1)) -> Term ((b1 -> b) -> b))
-> Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu (\Name (L ((b2 -> b2) -> b1))
f -> (Term (b1 -> b) -> Term b) -> Term ((b1 -> b) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term (b1 -> b) -> Term b) -> Term ((b1 -> b) -> b))
-> (Term (b1 -> b) -> Term b) -> Term ((b1 -> b) -> b)
forall a b. (a -> b) -> a -> b
$ \Term (b1 -> b)
y -> Term (b1 -> b) -> Term b1 -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b1 -> b)
y (Term b1 -> Term b) -> Term b1 -> Term b
forall a b. (a -> b) -> a -> b
$ Term ((b2 -> b2) -> b1) -> Term (b2 -> b2) -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
App (Name (L ((b2 -> b2) -> b1)) -> Term ((b2 -> b2) -> b1)
forall a. Name (L a) -> Term a
Var Name (L ((b2 -> b2) -> b1))
f) ((Term b2 -> Term b2) -> Term (b2 -> b2)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b2 -> Term b2) -> Term (b2 -> b2))
-> (Term b2 -> Term b2) -> Term (b2 -> b2)
forall a b. (a -> b) -> a -> b
$ \Term b2
x -> Term b2
x))

-- example from paper's Section 4
exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
exP = (Term ((b1 -> b1) -> b) -> Term ((b1 -> b1) -> b))
-> Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term ((b1 -> b1) -> b) -> Term ((b1 -> b1) -> b))
 -> Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b))
-> (Term ((b1 -> b1) -> b) -> Term ((b1 -> b1) -> b))
-> Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)
forall a b. (a -> b) -> a -> b
$ \Term ((b1 -> b1) -> b)
f -> (Term (b1 -> b1) -> Term b) -> Term ((b1 -> b1) -> b)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term (b1 -> b1) -> Term b) -> Term ((b1 -> b1) -> b))
-> (Term (b1 -> b1) -> Term b) -> Term ((b1 -> b1) -> b)
forall a b. (a -> b) -> a -> b
$ \Term (b1 -> b1)
g -> Term ((b1 -> b1) -> b) -> Term (b1 -> b1) -> Term b
forall b a. Term (b -> a) -> Term b -> Term a
App Term ((b1 -> b1) -> b)
f (Term (b1 -> b1) -> Term b) -> Term (b1 -> b1) -> Term b
forall a b. (a -> b) -> a -> b
$ (Term b1 -> Term b1) -> Term (b1 -> b1)
forall a b. (Term a -> Term b) -> Term (a -> b)
lam ((Term b1 -> Term b1) -> Term (b1 -> b1))
-> (Term b1 -> Term b1) -> Term (b1 -> b1)
forall a b. (a -> b) -> a -> b
$ \Term b1
x -> Term (b1 -> b1) -> Term b1 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b1 -> b1)
g (Term b1 -> Term b1) -> Term b1 -> Term b1
forall a b. (a -> b) -> a -> b
$ Term (b1 -> b1) -> Term b1 -> Term b1
forall b a. Term (b -> a) -> Term b -> Term a
App Term (b1 -> b1)
g Term b1
x