unbound 0.2.2 → 0.2.3
raw patch · 12 files changed
+429/−411 lines, 12 files
Files
- CHANGES +21/−0
- examples/Abstract.hs +176/−0
- examples/Functor.hs +110/−0
- examples/Functor2.hs +104/−0
- examples/Issue15.hs +13/−0
- examples/STLC.hs +2/−4
- examples/abstract.hs +0/−178
- examples/functor.hs +0/−110
- examples/functor2.hs +0/−104
- examples/issue15.hs +0/−13
- tutorial/Tutorial.lhs +1/−1
- unbound.cabal +2/−1
+ CHANGES view
@@ -0,0 +1,21 @@+Version 0.2: 24 March 2011++ * Initial release to go along with submission of "Binders Unbound".++Version 0.2.1: 28 March 2011++ * Massive update to documentation.++Version 0.2.2: 29 March 2011++ * Add MonadFix instances for FreshM and LFreshM. Thanks to Job+ Vranish for the suggestion.++Version 0.2.3: 20 April 2011++ * Fix minor bugs in+ - tutorial/Tutorial.lhs+ - examples/Abstract.hs+ - examples/STLC.hs++ Thanks to Ki Yung Ahn for the reports.
+ examples/Abstract.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+ TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+ ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module : LC+-- Copyright : (c) The University of Pennsylvania, 2010+-- License : BSD+--+-- Maintainer : sweirich@cis.upenn.edu+-- Stability : experimental+-- Portability : non-portable+--+--+--+-----------------------------------------------------------------------------++-- | This example demonstrates how to use abstract types as part of+-- the syntax of the untyped lambda calculus+--+-- Suppose we wish to include Source positions in our Abstract Syntax+--+module Abstract where++import Generics.RepLib+import Unbound.LocallyNameless++import qualified Data.Set as S+++-- We import the type SourcePos, but it is an abstract data type+-- all we know about it is that it is an instance of the Eq, Show and Ord classes.+import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)++-- Since we don't know the structure of the type, we create an "abstract"+-- representation for it. This defines rSourcePos :: R SourcePos and makes+-- SourcePos an instance of the Rep and Rep1 type classes.+--+-- Right now, this line triggers a warning because the TemplateHaskell code+-- does not work well with type abbreviations. The warning is safe to ignore.+$(derive_abstract [''SourcePos])++-- | A Simple datatype for the Lambda Calculus that includes source position+-- information+data Exp = Var SourcePos (Name Exp)+ | Lam (Bind (Name Exp) Exp)+ | App Exp Exp+ deriving Show++$(derive [''Exp])++-- To make Exp an instance of Alpha, we also need SourcePos to be an+-- instance of Alpha, because it appears inside the Exp type. When we+-- do so, we override the default definition of aeq'. There are a+-- few reasonable choices for this:+--+-- (1) match no source positions together --- default definition+-- aeq' c s1 s2 = False+-- (2) match all source positions together+-- aeq' c s1 s2 = True+-- (3) only match equal source positions together+-- aeq' c s1 s2 = s1 == s2+--+--+-- Below, we choose option (2) because we would like+-- (alpha-)equivalence for Exp to ignore the source position+-- information. Two free variables with the same name but with+-- different source positions should be equal.+--+-- The other defaults for Alpha are fine.+instance Alpha SourcePos where+ aeq' c s1 s2 = True+ acompare' c s1 s2 = EQ++instance Alpha Exp where++instance Subst Exp SourcePos where+instance Subst Exp Exp where+ isvar (Var _ x) = Just (SubstName x)+ isvar _ = Nothing++type M a = LFreshM a++-- | Beta-Eta equivalence for lambda calculus terms.+(=~) :: Exp -> Exp -> M Bool+e1 =~ e2 | e1 `aeq` e2 = return True+e1 =~ e2 = do+ e1' <- red e1+ e2' <- red e2+ if e1' `aeq` e1 && e2' `aeq` e2+ then return False+ else e1' =~ e2'+++-- | Parallel beta-eta reduction for lambda calculus terms.+-- Do as many reductions as possible in one step, while still ensuring+-- termination.+red :: Exp -> M Exp+red (App e1 e2) = do+ e1' <- red e1+ e2' <- red e2+ case e1' of+ -- look for a beta-reduction+ Lam bnd ->+ lunbind bnd $ \ (x, e1'') ->+ return $ subst x e2' e1''+ otherwise -> return $ App e1' e2'+red (Lam bnd) = lunbind bnd $ \ (x, e) -> do+ e' <- red e+ case e of+ -- look for an eta-reduction+ App e1 (Var _ y) | y `aeq` x && x `S.notMember` fv e1 -> return e1+ otherwise -> return (Lam (bind x e'))+red v = return $ v++++---------------------------------------------------------------------+-- Some testing code to demonstrate this library in action.++assert :: String -> Bool -> IO ()+assert s True = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: String -> M Bool -> IO ()+assertM s c =+ if (runLFreshM c) then return ()+ else print ("Assertion " ++ s ++ " failed")++x :: Name Exp+x = string2Name "x"++y :: Name Exp+y = string2Name "y"++z :: Name Exp+z = string2Name "z"++s :: Name Exp+s = string2Name "s"++sp = newPos "Foo" 1 2+sp2 = newPos "Bar" 3 4++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++var :: Name Exp -> Exp+var n = Var sp n++zero = lam s (lam z (var z))+one = lam s (lam z (App (var s) (var z)))+two = lam s (lam z (App (var s) (App (var s) (var z))))+three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))++plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))++true = lam x (lam y (var x))+false = lam x (lam y (var y))+if_ x y z = (App (App x y) z)++main :: IO ()+main = do+ -- \x.x `aeq` \x.y, no matter what the source positions are+ assert "a1" $ lam x (var x) `aeq` lam y (Var sp2 y)+ -- \x.x /= \x.y+ assert "a2" $ not(lam x (var y) `aeq` lam x (var x))+ -- \x.(\y.x) (\y.y) `aeq` \y.y+ assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))+ -- \x. f x `aeq` f+ assertM "be2" $ lam x (App (var y) (var x)) =~ var y+ assertM "be3" $ if_ true (var x) (var y) =~ var x+ assertM "be4" $ if_ false (var x) (var y) =~ var y+ assertM "be5" $ App (App plus one) two =~ three+
+ examples/Functor.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module Functor where++import Unbound.LocallyNameless hiding (Int)+import Control.Monad+import Control.Monad.Trans.Error+import Data.List as List++{- So we can't actually do modules like I was thinking of.+ Substitution in modules only "delays" capture not avoids it.+ -}++type TyName = Name Type+type ModName = Name Module++data Type = TyVar TyName+ | Int+ | Bool+ | Path Module TyName+ deriving Show++data ModDef = TyDef TyName (Maybe (Embed Type))+ | ModDef ModName Module+ -- here is the question. For submodules should+ -- it be Embed Module or just Module? For the+ -- former, then the "binding" names of the submodule+ -- could be bound by the outer module. For the latter+ -- a submodule can't use the same name as the outer+ -- module.+ deriving Show+data Module = Struct (Rec [ModDef])+ | Functor (Bind TyName Module)+ | ModApp Module Type+ | ModVar (Name Module)+ deriving Show++$(derive [''Type, ''ModDef, ''Module])++------------------------------------------------------+instance Alpha Type where+instance Alpha Module where+instance Alpha ModDef where++instance Subst Module Type where++instance Subst Module ModDef+instance Subst Module Module where+ isvar (ModVar x) = Just (SubstName x)+ isvar _ = Nothing++instance Subst Type Module where+instance Subst Type ModDef where+instance Subst Type Type where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing++t :: TyName+t = string2Name "t"++u :: TyName+u = string2Name "u"++x :: TyName+x = string2Name "x"++g :: ModName+g = string2Name "G"++f :: Module+f = Functor (bind x+ (Struct (rec [TyDef t (Just (Embed Bool)),+ TyDef u (Just (Embed (TyVar x)))])))++m :: Module+m = Struct (rec [TyDef t (Just (Embed Int)),+ ModDef g (ModApp f (TyVar t))])+++red :: Fresh m => Module -> m Module+red (ModApp m1 t) = do+ m1' <- red m1+ case m1' of+ Functor bnd -> do+ (x, m1'') <- unbind bnd+ red (subst x t m1'')+ _ -> return (ModApp m1 t)+red (Struct s) = do+ defs <- mapM redDef (unrec s)+ return (Struct (rec defs))+red m = return m++redDef :: Fresh m => ModDef -> m ModDef+redDef (ModDef f m) = do+ m' <- red m+ return (ModDef f m')+redDef d = return d++m3 = Struct (rec [TyDef t Nothing,+ TyDef u (Just (Embed (TyVar t)))])++m2 :: Module+m2 = runFreshM (red m)+
+ examples/Functor2.hs view
@@ -0,0 +1,104 @@+{-# LANGUAGE TemplateHaskell,+ ScopedTypeVariables,+ FlexibleInstances,+ MultiParamTypeClasses,+ FlexibleContexts,+ UndecidableInstances,+ GADTs #-}++module Functor2 where++import Unbound.LocallyNameless hiding (Int)+import Control.Monad+import Control.Monad.Trans.Error+import Data.List as List++{- This is the right way to formalize modules and functors+ -}++type TyName = Name Type+type ModName = Name Module++data Type = TyVar TyName+ | Int+ | Bool+ | Path Module String+ deriving Show++data ModDef = TyDef TyName (Maybe (Embed Type))+ | ModDef ModName (Embed Module)++ deriving Show+data Module = Struct (Bind (Rec [(String,ModDef)]) ())+ | Functor (Bind TyName Module)+ | ModApp Module Type+ | ModVar (Name Module)+ deriving Show++$(derive [''Type, ''ModDef, ''Module])++------------------------------------------------------+instance Alpha Type where+instance Alpha Module where+instance Alpha ModDef where++instance Subst Module Type where++instance Subst Module ModDef+instance Subst Module Module where+ isvar (ModVar x) = Just (SubstName x)+ isvar _ = Nothing++instance Subst Type Module where+instance Subst Type ModDef where+instance Subst Type Type where+ isvar (TyVar x) = Just (SubstName x)+ isvar _ = Nothing+++t :: TyName+t = string2Name "t"++u :: TyName+u = string2Name "u"++x :: TyName+x = string2Name "x"++g :: ModName+g = string2Name "G"++f :: Module+f = Functor (bind x+ (Struct (bind (rec+ [("t", TyDef t (Just (Embed Bool))),+ ("u", TyDef u (Just (Embed (TyVar x))))]) ())))++m :: Module+m = Struct (bind (rec [("t", TyDef t (Just (Embed Int))),+ ("g", ModDef g (Embed (ModApp f (TyVar t))))]) ())+++red :: Fresh m => Module -> m Module+red (ModApp m1 t) = do+ m1' <- red m1+ case m1' of+ Functor bnd -> do+ (x, m1'') <- unbind bnd+ red (subst x t m1'')+ _ -> return (ModApp m1 t)+red (Struct s) = do+ (r,()) <- unbind s+ defs <- mapM redDef (unrec r)+ return (Struct (bind (rec defs) ()))+red m = return m++redDef :: Fresh m => (String,ModDef) -> m (String,ModDef)+redDef (s,ModDef f (Embed m)) = do+ m' <- red m+ return (s,ModDef f (Embed m'))+redDef d = return d++m2 :: Module+m2 = runFreshM (red m)+
+ examples/Issue15.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+ TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+ ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}++module Issue15 where++import Generics.RepLib+import qualified Unbound.LocallyNameless as LN++data Foo = Foo (LN.Name Foo)++$(derive [''Foo])
examples/STLC.hs view
@@ -19,7 +19,6 @@ module STLC where import Unbound.LocallyNameless-import Control.Monad.Reader import Data.Set as S data Ty = TInt | TUnit | Arr Ty Ty@@ -47,8 +46,7 @@ type Ctx = [(Name Exp, Ty)] --- A monad that can generate locally fresh names-type M a = Reader Integer a+type M a = LFreshM a -- A type checker for STLC terms tc :: Ctx -> Exp -> Ty -> M Bool@@ -165,7 +163,7 @@ assertM :: (a -> Bool) -> String -> M a -> IO () assertM f s c =- if f (runReader c (0 :: Integer)) then return ()+ if f (runLFreshM c) then return () else print ("Assertion " ++ s ++ " failed") name1, name2 :: Name Exp
− examples/abstract.hs
@@ -1,178 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,- TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,- ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--------------------------------------------------------------------------------- |--- Module : LC--- Copyright : (c) The University of Pennsylvania, 2010--- License : BSD------ Maintainer : sweirich@cis.upenn.edu--- Stability : experimental--- Portability : non-portable------------------------------------------------------------------------------------------- | This example demonstrates how to use abstract types as part of--- the syntax of the untyped lambda calculus------ Suppose we wish to include Source positions in our Abstract Syntax----module Abstract where--import Generics.RepLib-import Unbound.LocallyNameless--import qualified Data.Set as S--import Control.Monad.Reader (Reader, runReader)----- We import the type SourcePos, but it is an abstract data type--- all we know about it is that it is an instance of the Eq, Show and Ord classes.-import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)---- Since we don't know the structure of the type, we create an "abstract"--- representation for it. This defines rSourcePos :: R SourcePos and makes--- SourcePos an instance of the Rep and Rep1 type classes.------ Right now, this line triggers a warning because the TemplateHaskell code--- does not work well with type abbreviations. The warning is safe to ignore.-$(derive_abstract [''SourcePos])---- | A Simple datatype for the Lambda Calculus that includes source position--- information-data Exp = Var SourcePos (Name Exp)- | Lam (Bind (Name Exp) Exp)- | App Exp Exp- deriving Show--$(derive [''Exp])---- To make Exp an instance of Alpha, we also need SourcePos to be an--- instance of Alpha, because it appears inside the Exp type. When we--- do so, we override the default definition of aeq'. There are a--- few reasonable choices for this:------ (1) match no source positions together --- default definition--- aeq' c s1 s2 = False--- (2) match all source positions together--- aeq' c s1 s2 = True--- (3) only match equal source positions together--- aeq' c s1 s2 = s1 == s2--------- Below, we choose option (2) because we would like--- (alpha-)equivalence for Exp to ignore the source position--- information. Two free variables with the same name but with--- different source positions should be equal.------ The other defaults for Alpha are fine.-instance Alpha SourcePos where- aeq' c s1 s2 = True- acompare' c s1 s2 = EQ--instance Alpha Exp where--instance Subst Exp SourcePos where-instance Subst Exp Exp where- isvar (Var _ x) = Just (SubstName x)- isvar _ = Nothing--type M a = Reader Integer a---- | Beta-Eta equivalence for lambda calculus terms.-(=~) :: Exp -> Exp -> M Bool-e1 =~ e2 | e1 `aeq` e2 = return True-e1 =~ e2 = do- e1' <- red e1- e2' <- red e2- if e1' `aeq` e1 && e2' `aeq` e2- then return False- else e1' =~ e2'----- | Parallel beta-eta reduction for lambda calculus terms.--- Do as many reductions as possible in one step, while still ensuring--- termination.-red :: Exp -> M Exp-red (App e1 e2) = do- e1' <- red e1- e2' <- red e2- case e1' of- -- look for a beta-reduction- Lam bnd ->- lunbind bnd $ \ (x, e1'') ->- return $ subst x e2' e1''- otherwise -> return $ App e1' e2'-red (Lam bnd) = lunbind bnd $ \ (x, e) -> do- e' <- red e- case e of- -- look for an eta-reduction- App e1 (Var _ y) | y `aeq` x && x `S.notMember` fv e1 -> return e1- otherwise -> return (Lam (bind x e'))-red v = return $ v---------------------------------------------------------------------------- Some testing code to demonstrate this library in action.--assert :: String -> Bool -> IO ()-assert s True = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--assertM :: String -> M Bool -> IO ()-assertM s c =- if (runReader c (0 :: Integer)) then return ()- else print ("Assertion " ++ s ++ " failed")--x :: Name Exp-x = string2Name "x"--y :: Name Exp-y = string2Name "y"--z :: Name Exp-z = string2Name "z"--s :: Name Exp-s = string2Name "s"--sp = newPos "Foo" 1 2-sp2 = newPos "Bar" 3 4--lam :: Name Exp -> Exp -> Exp-lam x y = Lam (bind x y)--var :: Name Exp -> Exp-var n = Var sp n--zero = lam s (lam z (var z))-one = lam s (lam z (App (var s) (var z)))-two = lam s (lam z (App (var s) (App (var s) (var z))))-three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))--plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))--true = lam x (lam y (var x))-false = lam x (lam y (var y))-if_ x y z = (App (App x y) z)--main :: IO ()-main = do- -- \x.x `aeq` \x.y, no matter what the source positions are- assert "a1" $ lam x (var x) `aeq` lam y (Var sp2 y)- -- \x.x /= \x.y- assert "a2" $ not(lam x (var y) `aeq` lam x (var x))- -- \x.(\y.x) (\y.y) `aeq` \y.y- assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))- -- \x. f x `aeq` f- assertM "be2" $ lam x (App (var y) (var x)) =~ var y- assertM "be3" $ if_ true (var x) (var y) =~ var x- assertM "be4" $ if_ false (var x) (var y) =~ var y- assertM "be5" $ App (App plus one) two =~ three-
− examples/functor.hs
@@ -1,110 +0,0 @@-{-# LANGUAGE TemplateHaskell,- ScopedTypeVariables,- FlexibleInstances,- MultiParamTypeClasses,- FlexibleContexts,- UndecidableInstances,- GADTs #-}--module Functor where--import Unbound.LocallyNameless hiding (Int)-import Control.Monad-import Control.Monad.Trans.Error-import Data.List as List--{- So we can't actually do modules like I was thinking of.- Substitution in modules only "delays" capture not avoids it.- -}--type TyName = Name Type-type ModName = Name Module--data Type = TyVar TyName- | Int- | Bool- | Path Module TyName- deriving Show--data ModDef = TyDef TyName (Maybe (Embed Type))- | ModDef ModName Module- -- here is the question. For submodules should- -- it be Embed Module or just Module? For the- -- former, then the "binding" names of the submodule- -- could be bound by the outer module. For the latter- -- a submodule can't use the same name as the outer- -- module.- deriving Show-data Module = Struct (Rec [ModDef])- | Functor (Bind TyName Module)- | ModApp Module Type- | ModVar (Name Module)- deriving Show--$(derive [''Type, ''ModDef, ''Module])---------------------------------------------------------instance Alpha Type where-instance Alpha Module where-instance Alpha ModDef where--instance Subst Module Type where--instance Subst Module ModDef-instance Subst Module Module where- isvar (ModVar x) = Just (SubstName x)- isvar _ = Nothing--instance Subst Type Module where-instance Subst Type ModDef where-instance Subst Type Type where- isvar (TyVar x) = Just (SubstName x)- isvar _ = Nothing--t :: TyName-t = string2Name "t"--u :: TyName-u = string2Name "u"--x :: TyName-x = string2Name "x"--g :: ModName-g = string2Name "G"--f :: Module-f = Functor (bind x- (Struct (rec [TyDef t (Just (Embed Bool)),- TyDef u (Just (Embed (TyVar x)))])))--m :: Module-m = Struct (rec [TyDef t (Just (Embed Int)),- ModDef g (ModApp f (TyVar t))])---red :: Fresh m => Module -> m Module-red (ModApp m1 t) = do- m1' <- red m1- case m1' of- Functor bnd -> do- (x, m1'') <- unbind bnd- red (subst x t m1'')- _ -> return (ModApp m1 t)-red (Struct s) = do- defs <- mapM redDef (unrec s)- return (Struct (rec defs))-red m = return m--redDef :: Fresh m => ModDef -> m ModDef-redDef (ModDef f m) = do- m' <- red m- return (ModDef f m')-redDef d = return d--m3 = Struct (rec [TyDef t Nothing,- TyDef u (Just (Embed (TyVar t)))])--m2 :: Module-m2 = runFreshM (red m)-
− examples/functor2.hs
@@ -1,104 +0,0 @@-{-# LANGUAGE TemplateHaskell,- ScopedTypeVariables,- FlexibleInstances,- MultiParamTypeClasses,- FlexibleContexts,- UndecidableInstances,- GADTs #-}--module Functor2 where--import Unbound.LocallyNameless hiding (Int)-import Control.Monad-import Control.Monad.Trans.Error-import Data.List as List--{- This is the right way to formalize modules and functors- -}--type TyName = Name Type-type ModName = Name Module--data Type = TyVar TyName- | Int- | Bool- | Path Module String- deriving Show--data ModDef = TyDef TyName (Maybe (Embed Type))- | ModDef ModName (Embed Module)-- deriving Show-data Module = Struct (Bind (Rec [(String,ModDef)]) ())- | Functor (Bind TyName Module)- | ModApp Module Type- | ModVar (Name Module)- deriving Show--$(derive [''Type, ''ModDef, ''Module])---------------------------------------------------------instance Alpha Type where-instance Alpha Module where-instance Alpha ModDef where--instance Subst Module Type where--instance Subst Module ModDef-instance Subst Module Module where- isvar (ModVar x) = Just (SubstName x)- isvar _ = Nothing--instance Subst Type Module where-instance Subst Type ModDef where-instance Subst Type Type where- isvar (TyVar x) = Just (SubstName x)- isvar _ = Nothing---t :: TyName-t = string2Name "t"--u :: TyName-u = string2Name "u"--x :: TyName-x = string2Name "x"--g :: ModName-g = string2Name "G"--f :: Module-f = Functor (bind x- (Struct (bind (rec- [("t", TyDef t (Just (Embed Bool))),- ("u", TyDef u (Just (Embed (TyVar x))))]) ())))--m :: Module-m = Struct (bind (rec [("t", TyDef t (Just (Embed Int))),- ("g", ModDef g (Embed (ModApp f (TyVar t))))]) ())---red :: Fresh m => Module -> m Module-red (ModApp m1 t) = do- m1' <- red m1- case m1' of- Functor bnd -> do- (x, m1'') <- unbind bnd- red (subst x t m1'')- _ -> return (ModApp m1 t)-red (Struct s) = do- (r,()) <- unbind s- defs <- mapM redDef (unrec r)- return (Struct (bind (rec defs) ()))-red m = return m--redDef :: Fresh m => (String,ModDef) -> m (String,ModDef)-redDef (s,ModDef f (Embed m)) = do- m' <- red m- return (s,ModDef f (Embed m'))-redDef d = return d--m2 :: Module-m2 = runFreshM (red m)-
− examples/issue15.hs
@@ -1,13 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,- TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,- ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--module Issue15 where--import Generics.RepLib-import qualified Unbound.LocallyNameless as LN--data Foo = Foo (LN.Name Foo)--$(derive [''Foo])
tutorial/Tutorial.lhs view
@@ -581,7 +581,7 @@ > checkEq b a > > checkList :: Tele -> [Exp] -> Tele -> M ()-> checkList _ [] Empty = ok+> checkList _ [] Empty = return () > checkList g (e:es) (Cons rb) = do > let ((x, Embed a), t') = unrebind rb > check g e a
unbound.cabal view
@@ -1,5 +1,5 @@ name: unbound-version: 0.2.2+version: 0.2.3 license: BSD3 license-file: LICENSE build-type: Simple@@ -11,6 +11,7 @@ homepage: http://code.google.com/p/replib/ category: Language, Generics, Compilers/Interpreters extra-source-files: README, + CHANGES, examples/*.hs, tutorial/Makefile, tutorial/Tutorial.lhs,