{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}
{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}

-- |
-- 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.Terms
  (L, D,
   Term(..), lam,
   DTerm(..), Decl(..), Decls(..)
  ) where

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

-- dummy datatypes for distinguishing Decl names from Lam names
data L a
data D a

-- to make a function for RAssign (for pretty)
newtype StringF x = StringF String
unStringF :: StringF x -> String
unStringF (StringF String
str) = String
str


------------------------------------------------------------
-- source terms
------------------------------------------------------------

-- Term datatype; no Ds since there's no declarations yet
data Term :: * -> * where
  Var :: Name (L a) -> Term a
  Lam :: Binding (L b) (Term a) -> Term (b -> a)
  App :: Term (b -> a) -> Term b -> Term a

$(mkNuMatching [t| forall a . Term a |])

instance Show (Term a) where show :: Term a -> String
show = Term a -> String
forall a. Term a -> String
tpretty

-- helps to build terms without explicitly using nu or Var
lam :: (Term a -> Term b) -> Term (a -> b)
lam :: (Term a -> Term b) -> Term (a -> b)
lam Term a -> Term b
f = Binding (L a) (Term b) -> Term (a -> b)
forall b a. Binding (L b) (Term a) -> Term (b -> a)
Lam (Binding (L a) (Term b) -> Term (a -> b))
-> Binding (L a) (Term b) -> Term (a -> b)
forall a b. (a -> b) -> a -> b
$ (Name (L a) -> Term b) -> Binding (L a) (Term b)
forall k1 (a :: k1) b. (Name a -> b) -> Binding a b
nu (Term a -> Term b
f (Term a -> Term b)
-> (Name (L a) -> Term a) -> Name (L a) -> Term b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name (L a) -> Term a
forall a. Name (L a) -> Term a
Var)

-- pretty print terms
tpretty :: Term a -> String
tpretty :: Term a -> String
tpretty Term a
t = Mb 'RNil (Term a) -> RAssign StringF 'RNil -> Int -> String
forall (c :: RList *) a.
Mb c (Term a) -> RAssign StringF c -> Int -> String
pretty' (Term a -> Mb 'RNil (Term a)
forall k a. a -> Mb 'RNil a
emptyMb Term a
t) RAssign StringF 'RNil
forall k (f :: k -> *). RAssign f 'RNil
C.empty Int
0
  where pretty' :: Mb c (Term a) -> RAssign StringF c -> Int -> String
        pretty' :: Mb c (Term a) -> RAssign StringF c -> Int -> String
pretty' Mb c (Term a)
[nuP| Var b |] RAssign StringF c
varnames Int
n =
            case Mb c (Name (L a)) -> Either (Member c (L a)) (Name (L a))
forall k1 k2 (a :: k1) (ctx :: RList k2).
Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP Mb c (Name (L a))
b of
              Left Member c (L a)
pf  -> StringF (L a) -> String
forall x. StringF x -> String
unStringF (Member c (L a) -> RAssign StringF c -> StringF (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)
pf RAssign StringF c
varnames)
              Right Name (L a)
n -> String
"(free-var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name (L a) -> String
forall a. Show a => a -> String
show Name (L a)
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        pretty' Mb c (Term a)
[nuP| Lam b |] RAssign StringF c
varnames Int
n =
            let x :: String
x = String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n in
            String
"(\\" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb (c ':> L b) (Term a)
-> RAssign StringF (c ':> L b) -> Int -> String
forall (c :: RList *) a.
Mb c (Term a) -> RAssign StringF c -> Int -> String
pretty' (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) (RAssign StringF c
varnames RAssign StringF c -> StringF (L b) -> RAssign StringF (c ':> L b)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: (String -> StringF (L b)
forall x. String -> StringF x
StringF String
x)) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        pretty' Mb c (Term a)
[nuP| App b1 b2 |] RAssign StringF c
varnames Int
n =
            String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb c (Term (b -> a)) -> RAssign StringF c -> Int -> String
forall (c :: RList *) a.
Mb c (Term a) -> RAssign StringF c -> Int -> String
pretty' Mb c (Term (b -> a))
b1 RAssign StringF c
varnames Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb c (Term b) -> RAssign StringF c -> Int -> String
forall (c :: RList *) a.
Mb c (Term a) -> RAssign StringF c -> Int -> String
pretty' Mb c (Term b)
b2 RAssign StringF c
varnames Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

------------------------------------------------------------
-- target terms
------------------------------------------------------------

-- terms under declarations
data DTerm :: * -> * where
  TVar :: Name (L a) -> DTerm a
  TDVar :: Name (D a) -> DTerm a
  TApp :: DTerm (a -> b) -> DTerm a -> DTerm b

-- we use this type for a definiens instead of putting lambdas on the front
data Decl :: * -> * where
  Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)
  Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)

-- top-level declarations with a return value
data Decls :: * -> * where
  Decls_Base :: DTerm a -> Decls a
  Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a

$(mkNuMatching [t| forall a . DTerm a |])
$(mkNuMatching [t| forall a . Decl a |])
$(mkNuMatching [t| forall a . Decls a |])

instance Show (DTerm a) where show :: DTerm a -> String
show = DTerm a -> String
forall a. DTerm a -> String
pretty
instance Show (Decls a) where show :: Decls a -> String
show = Decls a -> String
forall a. Decls a -> String
decls_pretty

------------------------------------------------------------
-- pretty printing
------------------------------------------------------------

-- pretty print terms
pretty :: DTerm a -> String
pretty :: DTerm a -> String
pretty DTerm a
t = Mb 'RNil (DTerm a) -> RAssign StringF 'RNil -> String
forall (c :: RList *) a.
Mb c (DTerm a) -> RAssign StringF c -> String
mpretty (DTerm a -> Mb 'RNil (DTerm a)
forall k a. a -> Mb 'RNil a
emptyMb DTerm a
t) RAssign StringF 'RNil
forall k (f :: k -> *). RAssign f 'RNil
C.empty

mpretty :: Mb c (DTerm a) -> RAssign StringF c -> String
mpretty :: Mb c (DTerm a) -> RAssign StringF c -> String
mpretty Mb c (DTerm a)
[nuP| TVar b |] RAssign StringF c
varnames =
    Either (Member c (L a)) (Name (L a)) -> RAssign StringF c -> String
forall a (c :: RList *) x.
Show a =>
Either (Member c x) a -> RAssign StringF c -> String
mprettyName (Mb c (Name (L a)) -> Either (Member c (L a)) (Name (L a))
forall k1 k2 (a :: k1) (ctx :: RList k2).
Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP Mb c (Name (L a))
b) RAssign StringF c
varnames
mpretty Mb c (DTerm a)
[nuP| TDVar b |] RAssign StringF c
varnames =
    Either (Member c (D a)) (Name (D a)) -> RAssign StringF c -> String
forall a (c :: RList *) x.
Show a =>
Either (Member c x) a -> RAssign StringF c -> String
mprettyName (Mb c (Name (D a)) -> Either (Member c (D a)) (Name (D a))
forall k1 k2 (a :: k1) (ctx :: RList k2).
Mb ctx (Name a) -> Either (Member ctx a) (Name a)
mbNameBoundP Mb c (Name (D a))
b) RAssign StringF c
varnames
mpretty Mb c (DTerm a)
[nuP| TApp b1 b2 |] RAssign StringF c
varnames =
    String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb c (DTerm (a -> a)) -> RAssign StringF c -> String
forall (c :: RList *) a.
Mb c (DTerm a) -> RAssign StringF c -> String
mpretty Mb c (DTerm (a -> a))
b1 RAssign StringF c
varnames
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb c (DTerm a) -> RAssign StringF c -> String
forall (c :: RList *) a.
Mb c (DTerm a) -> RAssign StringF c -> String
mpretty Mb c (DTerm a)
b2 RAssign StringF c
varnames String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

mprettyName :: Either (Member c x) a -> RAssign StringF c -> String
mprettyName (Left Member c x
pf) RAssign StringF c
varnames = StringF x -> String
forall x. StringF x -> String
unStringF (Member c x -> RAssign StringF c -> StringF x
forall k (c :: RList k) (a :: k) (f :: k -> *).
Member c a -> RAssign f c -> f a
C.get Member c x
pf RAssign StringF c
varnames)
mprettyName (Right a
n) RAssign StringF c
varnames = String
"(free-var " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (a -> String
forall a. Show a => a -> String
show a
n) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
        

-- pretty print decls
decls_pretty :: Decls a -> String
decls_pretty :: Decls a -> String
decls_pretty Decls a
decls =
    String
"let\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Mb 'RNil (Decls a) -> RAssign StringF 'RNil -> Int -> String
forall (c :: RList *) a.
Mb c (Decls a) -> RAssign StringF c -> Int -> String
mdecls_pretty (Decls a -> Mb 'RNil (Decls a)
forall k a. a -> Mb 'RNil a
emptyMb Decls a
decls) RAssign StringF 'RNil
forall k (f :: k -> *). RAssign f 'RNil
C.empty Int
0)

mdecls_pretty :: Mb c (Decls a) -> RAssign StringF c -> Int -> String
mdecls_pretty :: Mb c (Decls a) -> RAssign StringF c -> Int -> String
mdecls_pretty Mb c (Decls a)
[nuP| Decls_Base t |] RAssign StringF c
varnames Int
n =
    String
"in " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Mb c (DTerm a) -> RAssign StringF c -> String
forall (c :: RList *) a.
Mb c (DTerm a) -> RAssign StringF c -> String
mpretty Mb c (DTerm a)
t RAssign StringF c
varnames)
mdecls_pretty Mb c (Decls a)
[nuP| Decls_Cons decl rest |] RAssign StringF c
varnames Int
n =
    let fname :: String
fname = String
"F" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n in
    String
fname String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Mb c (Decl b) -> RAssign StringF c -> Int -> String
forall (c :: RList *) a.
Mb c (Decl a) -> RAssign StringF c -> Int -> String
mdecl_pretty Mb c (Decl b)
decl RAssign StringF c
varnames Int
0) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n"
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb (c ':> D b) (Decls a)
-> RAssign StringF (c ':> D b) -> Int -> String
forall (c :: RList *) a.
Mb c (Decls a) -> RAssign StringF c -> Int -> String
mdecls_pretty (Mb c (Binding (D b) (Decls a))
-> Mb (c :++: ('RNil ':> D b)) (Decls 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 (D b) (Decls a))
rest) (RAssign StringF c
varnames RAssign StringF c -> StringF (D b) -> RAssign StringF (c ':> D b)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: (String -> StringF (D b)
forall x. String -> StringF x
StringF String
fname)) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

mdecl_pretty :: Mb c (Decl a) -> RAssign StringF c -> Int -> String
mdecl_pretty :: Mb c (Decl a) -> RAssign StringF c -> Int -> String
mdecl_pretty Mb c (Decl a)
[nuP| Decl_One t|] RAssign StringF c
varnames Int
n =
  let vname :: String
vname = String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n in
  String
vname String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb (c ':> L a) (DTerm b) -> RAssign StringF (c ':> L a) -> String
forall (c :: RList *) a.
Mb c (DTerm a) -> RAssign StringF c -> String
mpretty (Mb c (Binding (L a) (DTerm b))
-> Mb (c :++: ('RNil ':> L a)) (DTerm b)
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 a) (DTerm b))
t) (RAssign StringF c
varnames RAssign StringF c -> StringF (L a) -> RAssign StringF (c ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: String -> StringF (L a)
forall x. String -> StringF x
StringF String
vname)
mdecl_pretty Mb c (Decl a)
[nuP| Decl_Cons d|] RAssign StringF c
varnames Int
n =
  let vname :: String
vname = String
"x" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n in
  String
vname String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Mb (c ':> L a) (Decl b)
-> RAssign StringF (c ':> L a) -> Int -> String
forall (c :: RList *) a.
Mb c (Decl a) -> RAssign StringF c -> Int -> String
mdecl_pretty (Mb c (Binding (L a) (Decl b))
-> Mb (c :++: ('RNil ':> L a)) (Decl b)
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 a) (Decl b))
d) (RAssign StringF c
varnames RAssign StringF c -> StringF (L a) -> RAssign StringF (c ':> L a)
forall a (f :: a -> *) (c :: RList a) (a :: a).
RAssign f c -> f a -> RAssign f (c ':> a)
:>: String -> StringF (L a)
forall x. String -> StringF x
StringF String
vname) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)