unbound 0.5.1 → 0.5.1.1

raw patch · 37 files changed

+2932/−2333 lines, 37 filesdep +semigroupsdep −unbounddep ~QuickCheckPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: semigroups

Dependencies removed: unbound

Dependency ranges changed: QuickCheck

API changes (from Hackage documentation)

Files

• CHANGES +2/−2
• Examples/Abstract.hs +0/−176
• Examples/DepCalc.hs +0/−291
• Examples/F.hs +0/−140
• Examples/Functor.hs +0/−110
• Examples/Functor2.hs +0/−104
• Examples/Issue15.hs +0/−13
• Examples/Issue28.hs +0/−65
• Examples/LC-smallstep.hs +0/−93
• Examples/LCRec.hs +0/−155
• Examples/LF.hs +0/−825
• Examples/Set.hs +0/−69
• Examples/TaggedTerm.hs +0/−59
• Examples/UnifyExp.hs +0/−161
• Examples/Vec.hs +0/−54
• Unbound/LocallyNameless/Alpha.hs +25/−10
• Unbound/LocallyNameless/Types.hs +1/−1
• Unbound/PermM.hs +14/−1
• examples/Abstract.hs +176/−0
• examples/Basic.hs +184/−0
• examples/DepCalc.hs +291/−0
• examples/F.hs +140/−0
• examples/Functor.hs +110/−0
• examples/Functor2.hs +104/−0
• examples/Issue15.hs +13/−0
• examples/Issue28.hs +65/−0
• examples/LC-smallstep.hs +93/−0
• examples/LC.hs +144/−0
• examples/LCRec.hs +155/−0
• examples/LF.hs +825/−0
• examples/Main.hs +32/−0
• examples/STLC.hs +201/−0
• examples/Set.hs +69/−0
• examples/TaggedTerm.hs +59/−0
• examples/UnifyExp.hs +161/−0
• examples/Vec.hs +54/−0
• unbound.cabal +14/−4

@@ -118,5 +118,5 @@ Version 0.5.1: August 2016   * Fix testsuite compilation problem -Planned extensions:-  * Cache free variables at binders+Version 0.5.1.1: October 2016+  * Update to newer GHC/TH

@@ -1,176 +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 Examples.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-

@@ -1,291 +0,0 @@-{-# LANGUAGE PatternGuards-           , MultiParamTypeClasses-           , TemplateHaskell-           , ScopedTypeVariables-           , FlexibleInstances-           , FlexibleContexts-           , UndecidableInstances-  #-}--{- A "simple" core dependent calculus.--term     M ::= x | * | \D. M | M [N] | Pi D. B-             | T | c-             | case M with y of [ c [x] => N ]--tele     D ::= . | x:A, D--ctx      G ::= . | G, x:A--judgement forms:-    G |- D wf         telescope wellformedness-    G |- [ M ] : D    check a list of terms against a telescope-    G |- chk M : A    check that term M has type A-    G |- inf M : A    infer the type of M (which is A)-    G |- A == B       check that A & B are equal--typing rules:--     telescope well formedness   (checkTele)--     G |-chk A : *    G,x:A |- D wf-     ----------------------------- cons-     G |- x:A, D wf--     ------------- nil-     G |- [] wf--     list of terms vs a telescope   (checks)--     G |-chk N : A    (G |- [N] : D)[x |-> N]-     -------------------------------------- cons-     G |- N, [N] : x:A,D--     -------------- nil-     G |- [] : .--     terms (check && infer)--     x:A \in G-     ------------     G |- inf x : A--     G |- D wf        G, D |- chk B : *-     ---------------------------------     G |- inf Pi D.B : *--     G |- D wf        G, D |- inf M : B-     --------------------------------     G |- inf \D.M : Pi D. B--     G |- inf M : Pi D.B      G |- [N] : D-     ----------------------------------------     G |- inf M [N] : B [ D |-> [N] ]-       ** note: simultaneous substitution for the domain **--     -----------     G |- inf * : *--     G |- inf  M : A    G |- A == B-     -----------------------------     G |- chk  M : B--     A = Pi D . *-     T : A \in Sigma-     ----------------------     G |- inf T : A--     c: A \in Sigma-     A = Pi D. Pi D'. T [x]-     dom(D) = [x]-     --------------     G |- inf c : A--     G |- inf M : T [ P ]-     G |- chk A : *-     for each i,-         ci : Pi D. Pi Di. T [x] \in Sigma  where dom(D) = [x]-         G, Di[ D |-> [P] ], y : M = C [w] |- chk N : A-    -------------------------------------------------------     G |-inf case M in A with y of [ c [w] => N ] : A---}--import Unbound.LocallyNameless--import Data.Monoid-import Control.Monad-import Control.Monad.Trans.Error--data TyCon    -- tags for the names of type constructors-data DataCon  -- and data constructors so that we don't get them-              -- confused with variables---- initial context of data and type constructors-sigmaData :: [(Name DataCon, Exp)]-sigmaData = undefined--sigmaTy  :: [(Name TyCon, Exp)]-sigmaTy = undefined--teq :: Name TyCon-teq = string2Name "=="--data Exp = EVar (Name Exp)-         | EStar-         | ELam (Bind Tele Exp)-         | EApp Exp [Exp]-         | EPi (Bind Tele Exp)-         | ETyCon (Name TyCon)-         | ELet (Bind Lets Exp)-         | EDataCon (Name DataCon)-         | ECase Exp Exp (Bind (Name Exp)-                    [(Name DataCon,Bind [Name Exp] Exp)])-  deriving Show--data Tele = Empty-          | Cons (Rebind (Name Exp, Embed Exp) Tele)-  deriving Show--type Ctx  = [ (Name Exp, Exp) ]--$(derive [''TyCon, ''DataCon, ''Exp, ''Tele])--instance Alpha Exp-instance Alpha Tele--instance Subst Exp Exp where-  isvar (EVar v) = Just (SubstName v)-  isvar _        = Nothing--instance Subst Exp Tele------------------------------------------------------ for examples--evar :: String -> Exp-evar = EVar . string2Name--elam :: [(String, Exp)] -> Exp -> Exp-elam t b = ELam (bind (mkTele t) b)--epi :: [(String, Exp)] -> Exp -> Exp-epi t b = EPi (bind (mkTele t) b)--earr :: Exp -> Exp -> Exp-earr t1 t2 = epi [("_", t1)] t2--eapp :: Exp -> Exp -> Exp-eapp a b = EApp a [b]--mkTele :: [(String, Exp)] -> Tele-mkTele []          = Empty-mkTele ((x,e) : t) = Cons (rebind (string2Name x, Embed e) (mkTele t))--{- Polymorphic identity function -}--pid :: Exp-pid = elam [("A", EStar), ("x", evar "A")] (evar "x")--{--ELam (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@1)--}--{- Polymorphic identity type: -}-sid :: Exp-sid = epi [("A", EStar), ("x", evar "A")] (evar "A")--{--EPi (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@0)--}--{- Polymorphic identity type: -}-sid2 :: Exp-sid2 = epi [("B", EStar), ("y", evar "B")] (evar "B")---------------------------------------------------------------- Type checker--type M = ErrorT String FreshM-ok = return ()--runM :: M a -> a-runM m = case (runFreshM (runErrorT m)) of-   Left s  -> error s-   Right a -> a--lookUp :: Name a -> [(Name a, b)] -> M b-lookUp n []     = throwError $ "Not in scope: " ++ show n-lookUp v ((x,a):t') | v == x    = return a-                    | otherwise = lookUp v t'--unPi :: Ctx -> Exp -> M (Bind Tele Exp)-unPi g (EPi bnd) = return bnd-unPi g e         = throwError $ "Expected pi type, got " ++ show e ++ " instead"--unVar :: Exp -> M (Name Exp)-unVar (EVar x) = return x-unVar e        = throwError $ "Expected variable, got " ++ show e ++ " instead"--unTApp :: Ctx -> Exp -> M (Name TyCon, [Exp])-unTApp _ (EApp (ETyCon n) args) = return (n, args)-unTApp _ e = throwError $ "Expected datatype, got " ++ show e++ " instead"---- Check a telescope and push it onto the context-checkTele :: Ctx -> Tele -> M Ctx-checkTele g Empty = return g-checkTele g (Cons rb) = do-  let ((x,Embed t), tele) = unrebind rb-  a <- infer g t-  check g a EStar-  checkTele ((x,t) : g) tele--infer :: Ctx -> Exp -> M Exp-infer g (EVar x)  = lookUp x g-infer _ EStar     = return EStar-infer g (ELam bnd) = do-    (delta, m) <- unbind bnd-    g' <- checkTele g delta-    b <- infer g' m-    return . EPi $ bind delta b-infer g (EApp m ns) = do-    bnd <- (unPi g) =<< infer g m-    (delta, b) <- unbind bnd-    checks g ns delta  --- ensures that the length ns == length (binders delta)-    return $ substs (zip (binders delta) ns) b-infer g (EPi bnd) = do-    (delta, b) <- unbind bnd-    g' <- checkTele g delta-    check g' b EStar-    return EStar-infer g (ETyCon n) = do-    bnd <- (unPi g) =<< lookUp n sigmaTy-    (delta, t) <- unbind bnd-    checkEq g t EStar-    return $ EPi bnd-infer g (EDataCon c) = do-  bnd <- (unPi g) =<< lookUp c sigmaData-  (delta, t) <- unbind bnd-  bnd' <- unPi g t-  (delta', EApp (ETyCon _) vars) <- unbind bnd'-  vs <- mapM unVar vars-  if vs == binders delta then return $ EPi bnd-     else throwError $ "incorrect result type for " ++ show (EDataCon c)-infer g (ECase m a bnd) = do-   check g a EStar-   (y, brs) <- unbind bnd-   t <- infer g m-   (n, ps)  <- unTApp g t-   _ <- mapM (checkBr y ps) brs-   return a-    where-      checkBr y ps (c,bnd) = do-         cbnd <- (unPi g) =<< lookUp c sigmaData-         (delta, rest) <- unbind cbnd-         cbnd' <- unPi g rest-         Just (deltai, _, ws, n) <- unbind2 cbnd' bnd-         g' <- checkTele g (substs (zip (binders delta) ps) deltai)-         let g'' = (y, EApp (ETyCon teq) [m, (EApp (EDataCon c) (map EVar ws))]): g'-         check g' n a--check :: Ctx -> Exp -> Exp -> M ()-check g m a = do-  b <- infer g m-  checkEq g b a--checks :: Ctx -> [Exp] -> Tele -> M ()-checks _ [] Empty = ok-checks g (e:es) (Cons rb) = do-  let ((x, Embed a), t') = unrebind rb-  check g e a-  checks (subst x e g) (subst x e es) (subst x e t')-checks _ _ _ = throwError $ "Unequal number of parameters and arguments"----- A conservative, inexpressive notion of equality, just for the sake--- of the example.-checkEq :: Ctx -> Exp -> Exp -> M ()-checkEq _ e1 e2 = if aeq e1 e2 then return () else throwError $ "Couldn't match: " ++ show e1 ++ " " ++ show e2-

@@ -1,140 +0,0 @@-{-# LANGUAGE TemplateHaskell,-             ScopedTypeVariables,-             FlexibleInstances,-             MultiParamTypeClasses,-             FlexibleContexts,-             UndecidableInstances,-             GADTs #-}--module F where--import Unbound.LocallyNameless--import Control.Monad-import Control.Monad.Trans.Error-import Data.List as List---- System F with type and term variables--type TyName = Name Ty-type TmName = Name Tm--data Ty = TyVar TyName-        | Arr Ty Ty-        | All (Bind TyName Ty)-   deriving Show--data Tm = TmVar TmName-        | Lam (Bind (TmName, Embed Ty) Tm)-        | TLam (Bind TyName Tm)-        | App Tm Tm-        | TApp Tm Ty-   deriving Show--$(derive [''Ty, ''Tm])---------------------------------------------------------instance Alpha Ty where-instance Alpha Tm where--instance Subst Tm Ty where-instance Subst Tm Tm where-  isvar (TmVar x) = Just (SubstName x)-  isvar _  = Nothing-instance Subst Ty Ty where-  isvar (TyVar x) = Just (SubstName x)-  isvar _ = Nothing---------------------------------------------------------- Example terms---------------------------------------------------------x :: Name Tm-y :: Name Tm-z :: Name Tm-(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")--a :: Name Ty-b :: Name Ty-c :: Name Ty-(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")---- /\a. \x:a. x-polyid :: Tm-polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x))))---- All a. a -> a-polyidty :: Ty-polyidty = All (bind a (Arr (TyVar a) (TyVar a)))----------------------------------------------------------------------- Typechecker-------------------------------------------------------------------type Delta = [ TyName ]-type Gamma = [ (TmName, Ty) ]--data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }-emptyCtx = Ctx { getDelta = [], getGamma = [] }--type M = ErrorT String FreshM--runM :: M a -> a-runM m = case (runFreshM (runErrorT m)) of-   Left s  -> error s-   Right a -> a--checkTyVar :: Ctx -> TyName -> M ()-checkTyVar g v = do-    if List.elem v (getDelta g) then-      return ()-    else-      throwError "NotFound"--lookupTmVar :: Ctx -> TmName -> M Ty-lookupTmVar g v = do-    case lookup v (getGamma g) of-      Just s -> return s-      Nothing -> throwError "NotFound"--extendTy :: TyName -> Ctx -> Ctx-extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }--extendTm :: TmName -> Ty -> Ctx -> Ctx-extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }--tcty :: Ctx -> Ty -> M ()-tcty g  (TyVar x) =-   checkTyVar g x-tcty g  (All b) = do-   (x, ty') <- unbind b-   tcty (extendTy x g) ty'-tcty g  (Arr t1 t2) = do-   tcty g  t1-   tcty g  t2--ti :: Ctx -> Tm -> M Ty-ti g (TmVar x) = lookupTmVar g x-ti g (Lam bnd) = do-  ((x, Embed ty1), t) <- unbind bnd-  tcty g ty1-  ty2 <- ti (extendTm x ty1 g) t-  return (Arr ty1 ty2)-ti g (App t1 t2) = do-  ty1 <- ti g t1-  ty2 <- ti g t2-  case ty1 of-    Arr ty11 ty21 | ty2 `aeq` ty11 ->-      return ty21-    _ -> throwError "TypeError"-ti g (TLam bnd) = do-  (x, t) <- unbind bnd-  ty <- ti (extendTy x g) t-  return (All (bind x ty))-ti g (TApp t ty) = do-  tyt <- ti g t-  case tyt of-   (All b) -> do-      tcty g  ty-      (n1, ty1) <- unbind b-      return $ subst n1 ty ty1-

@@ -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)-

@@ -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)-

@@ -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])

@@ -1,65 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}--module Issue28 where--import Unbound.LocallyNameless--type Var = Name Term--data Term-  = V Var-  | Unit-  | Pi (Bind (Var, Embed Term) Term)-  | LetRec (Bind (Rec Decl) Term)-    deriving (Show)--data Decl = -  -- a recursive declaration  x : A = m-  -- where x may occur in m but not in A-  Decl {-    declVar :: Var-    , declClass :: Shift (Embed Term)-    , declVal :: Embed Term-    }-  deriving (Show)--$(derive [''Term, ''Decl])--instance Alpha Term-instance Alpha Decl-instance Subst Term Decl -instance Subst Term Term where-  isvar (V x) = Just (SubstName x)-  isvar _ = Nothing--x :: Var-x = s2n "x"--letrec :: Decl -> Term -> Term-letrec d e = LetRec $ bind (rec d) e--decl :: Var -> Term -> Term -> Decl-decl v klass e = Decl v (Shift (Embed klass)) (embed e)---m0 = letrec (decl x Unit Unit) Unit---- >> show m1---     "LetRec (<[Decl {declVar = x, declClass = {{V x}}, declVal = {V 0@0}}]> V 0@0)"-m1 = letrec (decl x (V x) (V x)) (V x)---- substitution shows that binding is as we expect,--- >> subst x Unit m1---     "LetRec (<[Decl {declVar = x, declClass = {{Unit}}, declVal = {V 0@0}}]> V 0@0)"----- >> show m2---     "Pi (<(x,{Unit})> LetRec (<[Decl {declVar = x, declClass = {{V 0@0}}, declVal = {V 0@0}}]> V 0@0))"------     looks a little strange, but the shift is still there-m2 = Pi (bind (x, embed Unit) m1)-----

@@ -1,93 +0,0 @@--- Untyped lambda calculus, with small-step evaluation and an example parser--{-# LANGUAGE PatternGuards-           , MultiParamTypeClasses-           , TemplateHaskell-           , ScopedTypeVariables-           , FlexibleInstances-           , FlexibleContexts-           , UndecidableInstances-  #-}-import Control.Applicative-import Control.Arrow-import Control.Monad--import Control.Monad.Trans.Maybe--import Text.Parsec hiding ((<|>))-import qualified Text.Parsec.Token as P-import Text.Parsec.Language (haskellDef)--import Unbound.LocallyNameless--data Term = Var (Name Term)-          | App Term Term-          | Lam (Bind (Name Term) Term)-  deriving Show--$(derive [''Term])--instance Alpha Term-instance Subst Term Term where-  isvar (Var v) = Just (SubstName v)-  isvar _       = Nothing--done :: MonadPlus m => m a-done = mzero--step :: Term -> MaybeT FreshM Term-step (Var _) = done-step (Lam _) = done-step (App (Lam b) t2) = do-  (x,t1) <- unbind b-  return $ subst x t2 t1-step (App t1 t2) =-      App <$> step t1 <*> pure t2-  <|> App <$> pure t1 <*> step t2--tc :: Monad m => (a -> MaybeT m a) -> (a -> m a)-tc f a = do-  ma' <- runMaybeT (f a)-  case ma' of-    Just a' -> tc f a'-    Nothing -> return a--eval :: Term -> Term-eval x = runFreshM (tc step x)---- Some example terms--lam :: String -> Term -> Term-lam x t = Lam $ bind (string2Name x) t--var :: String -> Term-var = Var . string2Name--idT = lam "y" (var "y")--foo = lam "z" (var "y")--trueT  = lam "x" (lam "y" (var "x"))-falseT = lam "x" (lam "x" (var "x"))---- A small parser for Terms-lexer = P.makeTokenParser haskellDef-parens   = P.parens lexer-brackets = P.brackets lexer-ident    = P.identifier lexer--parseTerm = parseAtom `chainl1` (pure App)--parseAtom = parens parseTerm-        <|> var <$> ident-        <|> lam <$> (brackets ident) <*> parseTerm--runTerm :: String -> Either ParseError Term-runTerm = (id +++ eval) . parse parseTerm ""--{- example, 2 + 3 = 5:--    *Main> runTerm "([m][n][s][z] m s (n s z)) ([s] [z] s (s z)) ([s][z] s (s (s z))) s z"-    Right (App (Var s) (App (Var s) (App (Var s) (App (Var s) (App (Var s) (Var z))))))---}

@@ -1,155 +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------------------------------------------------------------------------------------------- | A very simple example demonstration of the binding library--- based on the untyped lambda calculus.-module LCRec where--import Unbound.LocallyNameless-import Control.Monad.Reader (Reader, runReader)-import Data.Set as S-import Data.List as L---- | A Simple datatype for the Lambda Calculus-data Exp = Var (Name Exp)-         | Lam (Bind (Name Exp) Exp)-         | App Exp Exp-         | Letrec (Bind (Rec [(Name Exp, Embed Exp)]) Exp)-  deriving Show---- Use RepLib to derive representation types-$(derive [''Exp])---- | With representation types, tbe default implementation of Alpha--- provides alpha-equivalence and free variable calculation.-instance Alpha Exp---- | The subst class uses generic programming to implement capture--- avoiding substitution. It just needs to know where the variables--- are.-instance Subst Exp Exp where-   isvar (Var x) = Just (SubstName x)-   isvar _       = Nothing----- | All new functions should be defined in a monad that can generate--- locally fresh names.--type M a = FreshM a---- | Beta-Eta equivalence for lambda calculus terms.--- If the terms have a normal form--- then the algorithm will terminate. Otherwise, the algorithm may--- loop for certain inputs.-(=~) :: 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 -> do-        (x, e1'') <- unbind bnd-        return $ subst x e2' e1''-    otherwise -> return $ App e1' e2'-red (Lam bnd) = do-   (x, e) <- unbind bnd-   e' <- red e-   case e of-     -- look for an eta-reduction-     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1-     otherwise -> return (Lam (bind x e'))-red (Var x) = return $ (Var x)-red (Letrec bnd) = do-  (r, body) <- unbind bnd-  -- get the variable definitions-  let vars = unrec r-  -- substitute them all (once) throughout the body, iteratively-  let newbody = foldr (\ (x,Embed rhs) body -> subst x rhs body) body vars-  let fvs = fv newbody-  -- garbage collect, if possible-  if (L.any (\ (x,_) -> x `S.member` fvs) vars) then-    return $ Letrec (bind (rec vars) newbody)-  else return newbody-------------------------------------------------------------------------- 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 (runFreshM 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"--lam :: Name Exp -> Exp -> Exp-lam x y = Lam (bind x y)--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)--e = Letrec (bind (rec [(y, Embed(Var x)), (x, Embed (Var z))]) (Var y))--main :: IO ()-main = do-  -- \x.x == \x.y-  assert "a1" $ lam x (Var x) `aeq` lam y (Var y)-  -- \x.x /= \x.y-  assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x))-  -- \x.(\y.x) (\y.y) == \y.y-  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))-  -- \x. f x === 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-

@@ -1,825 +0,0 @@-{- Type checker for LF, based on algorithm in Harper and Pfennig, "On-   Equivalence and Canonical Forms in the LF Type Theory", ACM-   Transactions on Computational Logic, 2000.--}--{-# LANGUAGE TemplateHaskell-           , ScopedTypeVariables-           , FlexibleInstances-           , MultiParamTypeClasses-           , FlexibleContexts-           , UndecidableInstances-           , TypeSynonymInstances-           , TypeFamilies-           , GeneralizedNewtypeDeriving-           , NoMonomorphismRestriction-  #-}--{- TODO:-   1. [ ] Fix parser to deal with infix type operators-   2. [ ] test on contents of qbf/-   3. [ ] tune for speed?--}--module Main where--import Prelude hiding (lookup)--import Unbound.LocallyNameless-import Unbound.LocallyNameless.Fresh (contLFreshM)-import Unbound.LocallyNameless.Ops (unsafeUnbind)--import Text.Parsec hiding ((<|>))-import qualified Text.Parsec.Token as P-import Text.Parsec.Language (haskellDef)-import Text.Parsec.String-import qualified Text.Parsec.Expr as PE--import Text.PrettyPrint (Doc, (<+>), (<>), colon, comma, text, render, empty, integer, nest, vcat, ($+$))-import qualified Text.PrettyPrint as PP--import Control.Monad.Error-import Control.Monad.Reader-import Control.Monad.Identity-import Control.Applicative hiding (many)--import qualified Data.Map as M-import qualified Data.Set as S-import Data.List (sortBy, groupBy)-import Data.Function (on)-import Data.Ord (comparing)--import System.Environment----------------------------------- Syntax ------------------------------------------------------- Kinds-data Kind = KPi (Bind (Name Tm, Embed Ty) Kind) -- {x:ty} k-          | Type                                -- type-  deriving Show---- Types, also called "Families"-data Ty   = TyPi (Bind (Name Tm, Embed Ty) Ty)  -- {x:ty} ty-          | TyApp Ty Tm                         -- ty tm-          | TyConst (Name Ty)                   -- a-  deriving Show---- Terms, also called "Objects"-data Tm   = Lam (Bind (Name Tm, Embed Ty) Tm)   -- [x:ty] tm-          | TmApp Tm Tm                         -- tm tm-          | TmVar (Name Tm)                     -- x-  deriving Show-  -- Harper and Pfennig distinguish between term *variables* and term-  -- *constants*, but for our purposes there is no need to distinguish-  -- between them.--$(derive [''Kind, ''Ty, ''Tm])--instance Alpha Kind-instance Alpha Ty-instance Alpha Tm---- There are no term variables in types or kinds, so we can just--- use the default structural Subst instances.-instance Subst Tm Kind-instance Subst Tm Ty---- For Tm we must implement isvar so the Subst instance knows about--- term variables.-instance Subst Tm Tm where-  isvar (TmVar v) = Just (SubstName v)-  isvar _         = Nothing---- A declaration is either---   * a type constant declaration (a name and a kind),---   * a term constant declaration (with optional type and definition), or---   * a fixity/precedence declaration.-data Decl = DeclTy (Name Ty) Kind-          | DeclTm (Name Tm) (Maybe Ty) (Maybe Tm)-          | DeclInfix Op-  deriving Show--data Op = Op Assoc Integer (Name Tm)-  deriving Show--data Assoc = L | R-  deriving Show---- A program is a sequence of declarations.-type Prog = [Decl]------------------------- Erasure ---------------------------------- Simple kinds and types (no dependency)-data SKind = SKType-           | SKArr STy SKind-  deriving (Eq, Show)-data STy   = STyConst (Name Ty)-           | STyArr STy STy-  deriving (Eq, Show)  -- structural equality is OK here, since there-                       -- are no bound variables.  Otherwise we could-                       -- use 'aeq' from-                       -- Generics.RepLib.Bind.LocallyNameless.--$(derive [''SKind, ''STy])--class Erasable t where-  type Erased t :: *-  erase :: t -> Erased t--instance Erasable Kind where-  type Erased Kind = SKind-  erase Type = SKType-  erase (KPi b) = SKArr (erase ty) (erase k)-    where ((_, Embed ty), k) = unsafeUnbind b-          -- this is actually safe since we ignore the name-          -- and promise to erase it from k.--instance Erasable Ty where-  type Erased Ty = STy-  erase (TyPi b)      = STyArr (erase t1) (erase t2)-    where ((_, Embed t1), t2) = unsafeUnbind b-  erase (TyApp ty _)  = erase ty-  erase (TyConst c)   = STyConst c--instance Erasable Tm where-  type Erased Tm = Tm-  erase t = t--instance (Erasable a, Erasable b) => Erasable (a,b) where-  type Erased (a,b) = (Erased a, Erased b)-  erase (x,y) = (erase x, erase y)----------------------------------- Signatures/contexts ----------------------------------------data Context tm ty = C (M.Map (Name Tm) tm) (M.Map (Name Ty) ty)--emptyCtx :: Context tm ty-emptyCtx = C M.empty M.empty--extendTm :: Name Tm -> tm -> Context tm ty -> Context tm ty-extendTm x t (C tm ty) = C (M.insert x t tm) ty--extendTy :: Name Ty -> ty -> Context tm ty -> Context tm ty-extendTy x k (C tm ty) = C tm (M.insert x k ty)--lookupTm :: Name Tm -> TcM (Context tm ty) tm-lookupTm x = ask >>= \(C tm _) -> embedMaybe (text $ "Not in scope: term variable " ++ show x)-                                  (M.lookup x tm)--lookupTy :: Name Ty -> TcM (Context tm ty) ty-lookupTy x = ask >>= \(C _ ty) -> embedMaybe (text $ "Not in scope: type constant " ++ show x)-                                  (M.lookup x ty)--embedMaybe :: Doc -> Maybe a -> TcM ctx a-embedMaybe errMsg m = case m of-  Just a  -> return a-  Nothing -> err errMsg--addTrace :: Doc -> TcM ctx String-addTrace msg = do-  chks  <- getChkContext-  trace <- vcat <$> mapM ppr chks-  return . PP.render $ msg $+$ trace--embedEither :: (MonadError String m) => Either String a -> m a-embedEither = either throwError return--instance Erasable a => Erasable (M.Map k a) where-  type Erased (M.Map k a) = M.Map k (Erased a)-  erase = M.map erase--instance (Erasable tm, Erasable ty) => Erasable (Context tm ty) where-  type Erased (Context tm ty) = Context (Erased tm) (Erased ty)-  erase (C tm ty) = C (erase tm) (erase ty)--instance (Erasable a) => Erasable (Maybe a) where-  type Erased (Maybe a) = Maybe (Erased a)-  erase = fmap erase--type Ctx  = Context (Ty, Maybe Tm) Kind-type SCtx = Erased Ctx--withTmBinding :: (MonadReader (Context (tm, Maybe Tm) ty) m, LFresh m)-              => Name Tm -> tm -> m r -> m r-withTmBinding x b = do-  avoid [AnyName x] . local (extendTm x (b, Nothing))--withTmDefn :: (MonadReader (Context tm ty) m, LFresh m)-           => Name Tm -> tm -> m r -> m r-withTmDefn x b = do-  avoid [AnyName x] . local (extendTm x b)--withTyBinding :: (MonadReader (Context tm ty) m, LFresh m)-              => Name Ty -> ty -> m r -> m r-withTyBinding x b = do-  avoid [AnyName x] . local (extendTy x b)---------------------------- Error reporting -------------------------------- Keep track of what we're in the middle of checking.-data Check = TyCheck Tm-           | KCheck Ty-           | SCheck Kind-           | TmEq Tm Tm STy-           | TyEq Ty Ty SKind-           | KEq Kind Kind-           | DeclCheck Decl----------------------------------- Typechecking monad -----------------------------------------newtype TcM ctx a = TcM { unTcM :: ErrorT String (ReaderT ctx (ReaderT [Check] LFreshM)) a }-  deriving (Functor, Applicative, Monad, MonadReader ctx, MonadPlus, MonadError String, LFresh)--getTcMAvoids :: TcM ctx (S.Set AnyName)-getTcMAvoids = TcM . lift . lift . lift $ getAvoids--getChkContext :: TcM ctx [Check]-getChkContext = TcM . lift . lift $ ask---- | Continue a TcM computation, given a binding context, a checking---   context, and a set of names to avoid.-contTcM :: TcM ctx a -> ctx -> [Check] -> S.Set AnyName -> Either String a-contTcM (TcM m) c chks nms = flip contLFreshM nms . flip runReaderT chks . flip runReaderT c . runErrorT $ m---- | Run a TcM computation in an empty context.-runTcM :: TcM (Context tm ty) a -> Either String a-runTcM m = contTcM m emptyCtx [] S.empty---- | Run a subcomputation with an erased context.-withErasedCtx :: TcM SCtx a -> TcM Ctx a-withErasedCtx m = do-  c <- ask-  chks <- getChkContext-  nms <- getTcMAvoids-  embedEither $ contTcM m (erase c) chks nms---- | Run a subcomputation with another check pushed on the checking---   context stack.-whileChecking :: Check -> TcM ctx a -> TcM ctx a-whileChecking chk m = do-  c <- ask-  chks <- getChkContext-  nms <- getTcMAvoids-  embedEither $ contTcM m c (chk:chks) nms--ensure errMsg b = if b then return () else errMsg >>= err--err msg = addTrace msg >>= throwError--matchErr :: Pretty a => a -> a -> TcM ctx Doc-matchErr x y = do-  x' <- ppr x-  y' <- ppr y-  return $ text "Cannot match" <+> x' <+> text "with" <+> y'--unTyPi (TyPi bnd) = return bnd-unTyPi t = ppr t >>= \t' -> err $ text "Expected pi type, got" <+> t' <+> text "instead"--unKPi (KPi bnd) = return bnd-unKPi t = ppr t >>= \t' -> err $ text "Expected pi kind, got" <+> t' <+> text "instead"--isType Type = return ()-isType t = ppr t >>= \t' -> err $ text "Expected Type, got" <+> t' <+> text "instead"----------------------------------- Weak head reduction ------------------------------------------ Reduce a term to weak-head normal form, or return it unchanged if--- it is not head-reducible.  Works in erased or unerased contexts.-whr :: Tm -> TcM (Context (t, Maybe Tm) ty) Tm-whr (TmVar a) = (do-  (_, Just defn) <- lookupTm a-  whr defn)-  `mplus`-  return (TmVar a)--whr (TmApp (Lam b) m1) =-  lunbind b $ \((x,_),m2) ->-    whr $ subst x m1 m2--whr (TmApp m1 m2) = do-  m1' <- whr m1-  case m1' of-    Lam _ -> whr (TmApp m1' m2)-    _     -> return $ TmApp m1' m2--whr t = return t----------------------------------- Term equality ------------------------------------------------ Type-directed term equality.  In context Delta, is M <==> N at--- simple type tau?-tmEq :: Tm -> Tm -> STy -> TcM SCtx ()-tmEq m n t = whileChecking (TmEq m n t) $ tmEqWhr m n t--tmEqWhr :: Tm -> Tm -> STy -> TcM SCtx ()-tmEqWhr m n t = do-  m' <- whr m-  n' <- whr n-  whileChecking (TmEq m' n' t) $ tmEq' m' n' t -- XXX--  -- XXX todo: might be nice to have 'lfresh' and 'lfreshen', the-  -- first NOT taking an argument--  -- XXX todo: need nicer way of doing "string2Name"--- Type-directed term equality on terms in WHNF-tmEq' :: Tm -> Tm -> STy -> TcM SCtx ()-tmEq' m n (STyArr t1 t2) = do-  x <- lfresh (string2Name "_x")-  withTmBinding x t1 $-    tmEq (TmApp m (TmVar x)) (TmApp n (TmVar x)) t2-tmEq' m n a@(STyConst {}) = do-  a' <- tmEqS m n-  ensure (matchErr a a') $ a == a'---- Structural term equality.  Check whether two terms in WHNF are--- structurally equal, and return their "approximate type" if so.-tmEqS :: Tm -> Tm -> TcM SCtx STy--tmEqS (TmVar a) (TmVar b) = do-  ensure (matchErr a b) $ a == b-  (tyA,_) <- lookupTm a  -- XXX-  return tyA--tmEqS (TmApp m1 m2) (TmApp n1 n2) = do-  ty <- tmEqS m1 n1-  case ty of-    STyArr t2 t1 -> do-      tmEq m2 n2 t2-      return t1-    _            -> do-      ty' <- ppr ty-      err $-        text "Left-hand side of an application has type" <+> ty' <> text "; expecting an arrow type"--tmEqS t1 t2 = err $ text "Term mismatch"----------------------------------- Type equality ------------------------------------------------ Kind-directed type equality.-tyEq :: Ty -> Ty -> SKind -> TcM SCtx ()-tyEq ty1 ty2 k = whileChecking (TyEq ty1 ty2 k) $ tyEq' ty1 ty2 k--tyEq' (TyPi bnd1) (TyPi bnd2) SKType =  -- XXX-  lunbind2 bnd1 bnd2 $ \(Just ((x, Embed a1), a2, (_, Embed b1), b2)) -> do-    tyEq a1 b1 SKType-    withTmBinding x (erase a1) $ tyEq a2 b2 SKType--tyEq' a b SKType = do-  t <- tyEqS a b-  ensure (matchErr t SKType) $ t == SKType--tyEq' a b (SKArr t k) = do-  x <- lfresh (string2Name "_x")-  withTmBinding x t $ tyEq (TyApp a (TmVar x)) (TyApp b (TmVar x)) k---- Structural type equality.-tyEqS :: Ty -> Ty -> TcM SCtx SKind-tyEqS (TyConst a) (TyConst b) = do-  ensure (matchErr a b) $ a == b-  lookupTy a--tyEqS (TyApp a m) (TyApp b n) = do-  SKArr t k <- tyEqS a b  -- XXX-  tmEq m n t-  return k--tyEqS t1 t2 = do-  t1' <- ppr t1-  t2' <- ppr t2-  err $ text "Types are not equal: " <+> t1' <> comma <+> t2'----------------------------------- Kind equality ------------------------------------------------ Algorithmic kind equality.-kEq :: Kind -> Kind -> TcM SCtx ()--kEq Type Type = return ()--kEq k1@(KPi bnd1) k2@(KPi bnd2) = whileChecking (KEq k1 k2) $-  lunbind bnd1 $ \((x, Embed a), k) ->-  lunbind bnd2 $ \((_, Embed b), l) -> do-    tyEq a b SKType-    withTmBinding x (erase a) $ kEq k l--kEq k1 k2 = do-  k1' <- ppr k1-  k2' <- ppr k2-  err $ text "Kinds are not equal:" <+> k1' <> comma <+> k2'----------------------------------- Type checking ------------------------------------------------ Compute the type of a term.-tyCheck :: Tm -> TcM Ctx Ty-tyCheck tm = whileChecking (TyCheck tm) $ tyCheck' tm--tyCheck' :: Tm -> TcM Ctx Ty-tyCheck' t@(TmVar x)     = liftM fst $ lookupTm x-tyCheck' t@(TmApp m1 m2) = do-  bnd <- unTyPi =<< tyCheck m1-  a2  <- tyCheck m2-  lunbind bnd $ \((x, Embed a2'), a1) -> do-    withErasedCtx $ tyEq a2' a2 SKType-    return $ subst x m2 a1-tyCheck' t@(Lam bnd) =-  lunbind bnd $ \((x, Embed a1), m2) -> do-    isType =<< kCheck a1-    a2   <- withTmBinding x a1 $ tyCheck m2-    return $ TyPi (bind (x, Embed a1) a2)---- Compute the kind of a type.-kCheck :: Ty -> TcM Ctx Kind-kCheck ty = whileChecking (KCheck ty) $ kCheck' ty--kCheck' :: Ty -> TcM Ctx Kind-kCheck' (TyConst a) = lookupTy a-kCheck' (TyApp a m) = do-  bnd <- unKPi =<< kCheck a-  b   <- tyCheck m-  lunbind bnd $ \((x, Embed b'), k) -> do-    withErasedCtx $ tyEq b' b SKType-    return $ subst x m k-kCheck' (TyPi bnd) =-  lunbind bnd $ \((x, Embed a1), a2) -> do-    isType =<< kCheck a1-    isType =<< (withTmBinding x a1 $ kCheck a2)-    return Type---- Check the validity of a kind.-sortCheck :: Kind -> TcM Ctx ()-sortCheck k = whileChecking (SCheck k) $ sortCheck' k--sortCheck' :: Kind -> TcM Ctx ()-sortCheck' Type      = return ()-sortCheck' (KPi bnd) =-  lunbind bnd $ \((x, Embed a), k) -> do-    isType =<< kCheck a-    withTmBinding x a $ sortCheck k-----------------------------------------------------------------  Parser  ---------------------------------------------------------------------------------------------------------------type OpList = [Op]--mkOp :: Op -> PE.Operator String OpList Identity Tm-mkOp (Op a _ nm) = PE.Infix (TmApp . TmApp (TmVar nm) <$ sym (name2String nm))-                            (assoc a)-  where assoc L = PE.AssocLeft-        assoc R = PE.AssocRight--mkOpTable :: OpList -> PE.OperatorTable String OpList Identity Tm-mkOpTable = map (map mkOp) . groupBy ((==) `on` prec) . sortBy (flip $ comparing prec)-  where prec (Op _ n _) = n--type LFParser = Parsec String OpList--lfParseTest :: Show a => LFParser a -> String -> IO ()-lfParseTest p = print . runParser p [] ""----------------------------------- Lexing -----------------------------------------------------startStuff = letter   <|> oneOf "!#$%&*+/<=>?@\\^|-~"-endStuff   = alphaNum <|> oneOf "!#$%&*+/<=>?@\\^|-~"--reservedNames = ["type", "infix", "right", "left"]-             ++ [":", "=", ".", "->", "%", "{", "}", "(", ")"]---langDef = haskellDef { P.reservedNames   = reservedNames-                     , P.reservedOpNames = reservedNames-                     , P.identStart      = startStuff-                     , P.identLetter     = endStuff-                     , P.opStart         = startStuff-                     , P.opLetter        = endStuff-                     }--lexer    = P.makeTokenParser langDef--parens   = P.parens     lexer-braces   = P.braces     lexer-brackets = P.brackets   lexer-sym      = P.symbol     lexer-op       = P.reservedOp lexer-reserved = P.reserved   lexer-natural  = P.natural    lexer--var      = string2Name <$> P.identifier lexer----------------------------------- Terms ------------------------------------------------------parseTm :: LFParser Tm-parseTm = parseTmExpr `chainl1` (pure TmApp)--parseTmExpr :: LFParser Tm-parseTmExpr = do-  ops <- getState-  PE.buildExpressionParser (mkOpTable ops) parseAtom--parseAtom :: LFParser Tm-parseAtom = parens parseTm-        <|> TmVar <$> var-        <|> Lam <$> (-              bind-                <$> brackets ((,) <$> var-                                  <*> (Embed <$> (sym ":" *> parseTy))-                             )-                <*> parseTm-              )----------------------------------- Types ------------------------------------------------------parseTy :: LFParser Ty-parseTy  =-      -- ty ::=--      -- [x:ty] ty-      TyPi <$> (bind-         <$> braces ((,) <$> var-                         <*> (Embed <$> (sym ":" *> parseTy))-                    )-         <*> parseTy)--      -- te -> ty-  <|> try (TyPi <$> (bind-             <$> ((,) (string2Name "_") . Embed <$> parseTyExpr)-             <*> (op "->" *> parseTy)-          ))--      -- te-  <|> parseTyExpr--  -- XXX this does not handle type expressions built using infix type operators!-parseTyExpr :: LFParser Ty-  -- te ::= ta [tm ...]-parseTyExpr = foldl TyApp <$> parseTyAtom <*> many parseAtom--parseTyAtom :: LFParser Ty-parseTyAtom =-      -- ta ::=--      -- (ty)-      parens parseTy--      -- x-  <|> TyConst <$> var----------------------------------- Kinds ------------------------------------------------------parseKind :: LFParser Kind-parseKind =-      -- k ::=--      -- {x:ty} k-      KPi <$> (bind-       <$> braces ((,) <$> var-                       <*> (Embed <$> (sym ":" *> parseTy))-                  )-       <*> parseKind)--      -- ka -> k-  <|> try (KPi <$> (bind-             <$> ((,) (string2Name "_") . Embed <$> parseTyExpr)-             <*> (op "->" *> parseKind)-          ))--      -- ka-  <|> parseKindAtom--parseKindAtom :: LFParser Kind-parseKindAtom =-      -- ka ::=--      -- (k)-      parens parseKind--      -- Type-  <|> try (Type <$ reserved "type")----------------------------------- Declarations -----------------------------------------------parseDecl :: LFParser Decl-parseDecl = declBody <* sym "."- where-  declBody =-        DeclInfix <$> (Op <$> (sym "%" *> reserved "infix" *> rl)-                          <*> natural-                          <*> var)--    <|> try (DeclTy <$> var-                    <*> (sym ":" *> parseKind))--    <|> try (DeclTm <$> var-                    <*> (sym ":" *> (Just <$> parseTy))-                    <*> optionMaybe (sym "=" *> parseTm))--    <|>      DeclTm <$> var-                    <*> pure Nothing-                    <*> (sym "=" *> (Just <$> parseTm))-  rl = (L <$ reserved "left") <|> (R <$ reserved "right")----------------------------------- Programs ---------------------------------------------------parseProg :: LFParser Prog-parseProg =-      -- stop at eof-      [] <$ eof--  <|> do d <- parseDecl  -- parse a single decl-         case d of       -- add fixity declarations to the state-           DeclInfix op -> modifyState (op:)-           _ -> return ()--         (d:) <$> parseProg  -- parse the rest of the program--------------------------------------------- Pretty-printing ----------------------------------------------------------------class Pretty p where-  ppr :: (LFresh m, Functor m) => p -> m Doc--instance Pretty (Name a) where-  ppr = return . text . show--dot = text "."--instance Pretty Decl where-  ppr (DeclTy t k) = do-    t' <- ppr t-    k' <- ppr k-    return $ t' <+> colon <+> k' <> dot-  ppr (DeclTm x mty mdef) = do-    x'   <- ppr x-    tyf  <- case mty of-              Nothing -> return id-              Just ty -> do ty' <- ppr ty-                            return (<+> (colon <+> ty'))-    deff <- case mdef of-              Nothing -> return id-              Just def -> do def' <- ppr def-                             return (<+> (text "=" <+> def'))-    return $ (deff . tyf $ x') <> dot-  ppr (DeclInfix op) = do-    op' <- ppr op-    return $ op' <> dot--instance Pretty Op where-  ppr (Op assoc prec op) = do-    op' <- ppr op-    return $-      text "%infix"-        <+> text (case assoc of L -> "left"; R -> "right")-        <+> integer prec-        <+> op'--instance Pretty Kind where-  ppr Type = return $ text "type"-  ppr (KPi bnd) = lunbind bnd $ \((x, Embed ty), k) -> do-    x'  <- ppr x-    ty' <- ppr ty-    k'  <- ppr k-    if x `S.member` fv k-      then return $ PP.braces (x' <> colon <> ty') <+> k'-      else return $ PP.parens ty' <+> text "->" <+> k'--instance Pretty Ty where-  ppr (TyApp ty tm) = do-    ty' <- ppr ty-    tm' <- ppr tm-    return $ ty' <+> PP.parens tm'-  ppr (TyConst c) = ppr c-  ppr (TyPi bnd) = lunbind bnd $ \((x, Embed ty1), ty2) -> do-    x' <- ppr x-    ty1' <- ppr ty1-    ty2' <- ppr ty2-    if x `S.member` fv ty2-      then return $ PP.braces (x' <> colon <> ty1') <+> ty2'-      else return $ PP.parens ty1' <+> text "->" <+> ty2'--instance Pretty STy where-  ppr sty = ppr (uneraseTy sty)--uneraseTy (STyConst c) = TyConst c-uneraseTy (STyArr t1 t2) = TyPi (bind (string2Name "_", Embed (uneraseTy t1)) (uneraseTy t2))--uneraseK SKType = Type-uneraseK (SKArr sty sk) = KPi (bind (string2Name "_", Embed (uneraseTy sty)) (uneraseK sk))--instance Pretty SKind where-  ppr sk = ppr (uneraseK sk)--instance Pretty Tm where-  ppr (TmVar x) = ppr x-  ppr (TmApp tm1 tm2) = do-    tm1' <- ppr tm1-    tm2' <- ppr tm2-    return $ tm1' <+> PP.parens tm2'-  ppr (Lam bnd) = lunbind bnd $ \((x, Embed ty), tm) -> do-    x' <- ppr x-    ty' <- ppr ty-    tm' <- ppr tm-    return $ PP.brackets (x' <> colon <> ty') <+> tm'--instance Pretty Check where-  ppr (TyCheck tm) =-    (text "While checking the type of:" <+>) <$> ppr tm-  ppr (KCheck ty) =-    (text "While checking the kind of:" <+>) <$> ppr ty-  ppr (SCheck k) =-    (text "While checking the sort of:" <+>) <$> ppr k-  ppr (TmEq m n ty) = do-    m' <- ppr m-    n' <- ppr n-    ty' <- ppr ty-    return $  text "While checking that terms:"-          $+$ nest 4 (m' $+$ n')-          $+$ nest 2 (text "are equal at type")-          $+$ nest 4 ty'-  ppr (TyEq t1 t2 k) = do-    t1' <- ppr t1-    t2' <- ppr t2-    k'  <- ppr k-    return $  text "While checking that types:"-          $+$ nest 4 (t1' $+$ t2')-          $+$ nest 2 (text "are equal at kind")-          $+$ nest 4 k'-  ppr (KEq k1 k2) = do-    k1' <- ppr k1-    k2' <- ppr k2-    return $ text "While checking equality of kinds:"-          $+$ nest 4 (k1' $+$ k2')-  ppr (DeclCheck decl) = do-    d' <- ppr decl-    return $ text "While checking the declaration:" $+$ nest 4 d'----------------------------------- Typechecking programs --------------------------------------checkProg :: Prog -> TcM Ctx ()-checkProg [] = return ()-checkProg (DeclInfix _ : ds) = checkProg ds-checkProg (d@(DeclTy nm k) : ds) = do-  whileChecking (DeclCheck d) $ sortCheck k-  withTyBinding nm k $ checkProg ds-checkProg ((DeclTm nm Nothing Nothing):_) = do-  throwError $ "Term " ++ show nm-    ++ " has no type or definition! (This shouldn't happen.)"-checkProg (d@(DeclTm nm (Just ty) Nothing) : ds) = do-  whileChecking (DeclCheck d) $ isType =<< kCheck ty-  withTmBinding nm ty $ checkProg ds-checkProg (d@(DeclTm nm Nothing (Just def)) : ds) = do-  ty <- whileChecking (DeclCheck d) $ tyCheck def-  withTmDefn nm (ty, Just def) $ checkProg ds-checkProg (d@(DeclTm nm (Just ty) (Just def)) : ds) = do-  whileChecking (DeclCheck d) $ do-    isType =<< kCheck ty-    ty'  <- tyCheck def-    withErasedCtx $ tyEq ty ty' SKType-  withTmDefn nm (ty, Just def) $ checkProg ds--checkLF :: [FilePath] -> IO ()-checkLF fileNames = do-  files <- mapM readFile fileNames-  case runParser parseProg [] "" (concat files) of-    Left err   -> print err-    Right prog -> do-      -- putStrLn . unlines . map render . runLFreshM . mapM ppr $ prog-      putStrLn . either ("Error: "++) (const "OK!") . runTcM . checkProg $ prog--main = do-  fileNames <- getArgs-  checkLF fileNames

@@ -1,69 +0,0 @@-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving- #-}--module Set where--import Unbound.LocallyNameless-import Unbound.LocallyNameless.Types-import Data.List-import Data.Set--data Ty = All (SetPlusBind [Name Ty] Ty)-        | Var (Name Ty)-        | Arr Ty Ty deriving Show--$(derive [''Ty])--instance Alpha Ty--a, b, c :: Rep a => Name a-a = s2n "a"-b = s2n "b"-c = s2n "c"--sall :: [Name Ty] -> Ty -> Ty-sall ns t = All (setbind ns t)--s1 = sall [a, b] (Arr (Var a) (Var b))-s2 = sall [a, b] (Arr (Var b) (Var a))-s3 = sall [b, a] (Arr (Var a) (Var b))-s4 = sall [b, a] (Arr (Var b) (Var a))-s5 = sall [b, a, c] (Arr (Var b) (Var a))-s6 = sall [a, c] (Arr (Var a) (Var c))---data E =-  L (Bind (Name E) E)-  | V (Name E)-  | A E E-  | C Int-  | LR (SetBind (Rec [(Name E,Embed E)]) E)-  deriving Show-           -$(derive [''E])           - -instance Alpha E  -  -letrec :: [(Name E, Embed E)] -> E -> E-letrec ns t = LR (permbind (Rec ns) t)--p1 = letrec [(a, Embed (V a)), (b, Embed (C 2))] (A (V a) (V b))-p2 = letrec [(b, Embed (V 2)), (a, Embed (V a))] (A (V a) (V b))--assert :: String -> Bool -> IO ()-assert s True  = return ()-assert s False = print ("Assertion " ++ s ++ " failed")--main :: IO ()-main = do-  assert "s1" $ s1 `aeq` s2-  assert "s2" $ s1 `aeq` s3-  assert "s3" $ s1 `aeq` s4-  assert "s4" $ s1 `aeq` s5-  assert "s5" $ s1 `aeq` s6--  -- NOTE: this assertion fails. This is a bug. Perm binds don't do what we want. -  assert "a11" $ p1 `aeq` p2-

@@ -1,59 +0,0 @@-{-# LANGUAGE TemplateHaskell-           , UndecidableInstances-           , TypeOperators-           , GADTs-           , FlexibleInstances-           , ScopedTypeVariables-           , MultiParamTypeClasses-           , KindSignatures-           , RankNTypes-           , StandaloneDeriving-           , OverlappingInstances- #-}--------------------------------------------------------------------------------- |--- Module      :  TaggedTerm--- Copyright   :  (c) the Unbound team (see LICENSE)--- License     :  BSD-like (see LICENSE)------ Maintainer  :  byorgey@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable--------------------------------------------------------------------------------module TaggedTerm where--import Unbound.LocallyNameless hiding (Con)--data Term-data Pattern--data Expr :: * -> * where-         -- Note: be very careful here!  Name (Expr a) -> Expr a does-         -- not work since the names in patterns will not get-         -- connected up with names in terms.-  Var :: Name (Expr Term) -> Expr a-  App :: Expr a ->  Expr a -> Expr a-  Lam :: Bind (Expr Pattern) (Expr Term) -> Expr Term-  Con :: String -> [Expr a] -> Expr a--deriving instance Show (Expr a)--$(derive [''Term, ''Pattern, ''Expr])--instance (Rep t) => Alpha (Expr t)--instance Subst (Expr Term) (Expr Term) where-  isvar (Var x) = Just (SubstName x)-  isvar _       = Nothing--instance Subst (Expr Term) (Expr Pattern)--test1 :: Expr Term-test1 = Lam (bind (Con "Pair" [Var $ s2n "y", Var $ s2n "z"]) (Con "Pair" [Var (s2n "y"), Var (s2n "x")]))--test2 :: Expr Term-test2 = subst (s2n "y") (Con "Unit" [] :: Expr Term) test1--test3 :: Expr Term-test3 = subst (s2n "x") (Con "Unit" [] :: Expr Term) test1

@@ -1,161 +0,0 @@-{-# OPTIONS -fglasgow-exts #-}-{-# OPTIONS -fallow-undecidable-instances #-}-{-# OPTIONS -fallow-overlapping-instances #-}-{-# OPTIONS -fth #-}---------------------------------------------------------------------------------- |--- Module      :  UnifyExp--- Copyright   :  (c) Ben Kavanagh 2008--- License     :  BSD------ Maintainer  :  ben.kavanagh@gmail.com--- Stability   :  experimental--- Portability :  non-portable------ A file demonstrating the use of Generics.Replib.Unify-----------------------------------------------------------------------------------module UnifyExp-where--import Generics.RepLib-import Generics.RepLib.Unify-import Test.HUnit-import Control.Monad.Error----data Exp = Var Int-	 | Plus Exp Exp-	 | K String-	 deriving (Show, Eq)-$(derive [''Exp])--instance HasVar Int Exp where-    is_var (Var i) = Just i-    is_var _ = Nothing-    var = Var---- A = "f" ==> [(A, "f")]-test1 :: Maybe [(Int, Exp)]-test1 = solveUnification [(Var 1, K "f")]----- A = "f" + A  ==>   fails occurs check-test2 :: Maybe [(Int, Exp)]-test2 = solveUnification [(Var 1, Plus (K "f") (Var 1))]----- A + B = B + B ==> A = B-test3 :: Maybe [(Int, Exp)]-test3 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 2))]---- A + B = B + C ==> [(A, C), (B, C)]-test4 :: Maybe [(Int, Exp)]-test4 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 3))]-----data Term = TVar Int-	  | K2 String-	  | App Term Term-	 deriving (Show, Eq)-$(derive [''Term])--instance HasVar Int Term where-    is_var (TVar i) = Just i-    is_var _ = Nothing-    var = TVar---- There are two ways to override the unify [Char] [Char] problem. the first is to implement--- unify and only offer the case for K2, defaulting to generic unify in other cases. The other--- is to implement unify for String using equality, overriding the default Cons/Nil case handling----- special instance of unify for String--- Writing an instance for String which leaves 'special' term 'a' abstract has a problem with case a = String,--- which leads to overlap with a a case.. So we can only specialise String for a known 'special' term (here Term)-instance (Eq n, Show n, HasVar n Term) => Unify n Term String where-    unifyStep _ x y = if x == y-		      then return ()-		      else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y)------- f(g(A)) = f(B)  ==>   [(B, g(A))]-test5 :: Maybe [(Int, Term)]-test5 = solveUnification [(App (K2 "f") (App (K2 "g") (TVar 1)), App (K2 "f") (TVar 2))]----- f(g(A), A) = f(B, xyz) ==> [(A, xyz), (B, g(xyz))]-test6 :: Maybe [(Int, Term)]-test6 = solveUnification [(App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1), App (App (K2 "f") (TVar 2)) (K2 "xyz"))]---- f(A) = f(B, C) ==> fail. constructor mismatch. App vs K2. This is in essence an 'arity' failure.--- in a term datatype that had Application as an arity plus list, the arity would not be equal and would call failure.--- I'm not sure the error message would be adequate. Perhaps I could use a typeclass/newtype to get better error messages--- on equality failures.-test7 :: Maybe [(Int, Term)]-test7 = solveUnification [(App (K2 "f") (TVar 1),  App (App (K2 "f") (TVar 2)) (TVar 3))]---- f(A) = f(B) ==> [(A, B)]-test8 :: Maybe [(Int, Term)]-test8 = solveUnification [(App (K2 "f") (TVar 1), App (K2 "f") (TVar 2))]---- A = B, B = abc  ==>  [(B, abc), (A, abc)]-test9 :: Maybe [(Int, Term)]-test9 = solveUnification [(TVar 1, TVar 2), (TVar 2, K2 "abc")]---- A = abc, xyz = X, A = X  ==>  fails with built in equality since we effectively ask abc = xyz-test10 :: Maybe [(Int, Term)]-test10 = solveUnification [(TVar 1, K2 "abc"), (K2 "xyz", TVar 2), (TVar 1, TVar 2)]------ Test that unification works with surrounding term structure (other datatypes) which are closed, i.e. they have no free variables.-data OuterTerm =  K3 String-	       | Inner Term-	       | App3 OuterTerm OuterTerm-	 deriving (Show, Eq)-$(derive [''OuterTerm])----- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer-test11 :: Maybe [(Int, Term)]-test11 = solveUnification'-	   (undefined :: Proxy (Int, Term))-	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),-	     App3 (K3 "H") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]----- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer-test12 :: Maybe [(Int, Term)]-test12 = solveUnification'-	   (undefined :: Proxy (Int, Term))-	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),-	     App3 (K3 "I") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]------- todo. fix tests so that errors are tested properly.-tests = test [ test1 ~?= Just [(1,K "f")],-	       test2 ~?= error "***Exception: occurs check failed",-	       test3 ~?= Just [(1,Var 2)],-	       test4 ~?= Just [(1,Var 3),(2,Var 3)],-	       test5 ~?= Just [(2,App (K2 "g") (TVar 1))],-	       test6 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],-	       test7 ~?= error "*** Exception: constructor mismatch",-	       test8 ~?= Just [(1,TVar 2)],-	       test9 ~?= Just [(2,K2 "abc"),(1,K2 "abc")],-	       test10 ~?= error "*** Exception: unify failed in built in equality",-	       test11 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],-	       test12 ~?= error "*** Exception: unify failed when testing equality for \"H\" = \"I\""]---main = runTestTT tests-

@@ -1,54 +0,0 @@-{-# LANGUAGE TemplateHaskell-           , UndecidableInstances-           , TypeOperators-           , GADTs-           , FlexibleInstances-           , ScopedTypeVariables-           , MultiParamTypeClasses-           , KindSignatures-           , RankNTypes-           , StandaloneDeriving-           , OverlappingInstances- #-}--------------------------------------------------------------------------------- |--- Module      :  Vec--- Copyright   :  (c) the Unbound team (see LICENSE)--- License     :  BSD-like (see LICENSE)------ Maintainer  :  byorgey@cis.upenn.edu--- Stability   :  experimental--- Portability :  non-portable--------------------------------------------------------------------------------module Vec where--import Unbound.LocallyNameless hiding (Nil)--data Z-data S n--data Vec :: * -> * -> * where-  Nil   :: Vec Z a-  Cons  :: a -> Vec n a -> Vec (S n) a--deriving instance Show a => Show (Vec n a)--data Term = Var (Name Term) -          | Lit (Vec (S (S Z)) Int) -          | Pair Term Term-  deriving Show--$(derive [''Z, ''S, ''Vec, ''Term])--instance (Alpha a, Rep n) => Alpha (Vec n a)-instance Alpha Term--instance Subst Term Term where-  isvar (Var x) = Just (SubstName x)-  isvar _       = Nothing--instance (Rep n, Rep a) => Subst Term (Vec n a)--t :: Term-t = Pair (Var (s2n "x")) (Lit (Cons 1 (Cons 2 Nil)))

@@ -1,4 +1,5 @@-{-# LANGUAGE RankNTypes
+{-# LANGUAGE CPP+           , RankNTypes
            , FlexibleContexts
            , GADTs
            , TypeFamilies
@@ -23,7 +24,9 @@ 
 import Data.List (intersect)
 import Data.Maybe (isJust)
-
++import Data.Semigroup (Semigroup)+import qualified Data.Semigroup as Semigroup import Data.Monoid
 
 ------------------------------------------------------------
@@ -228,15 +231,21 @@                                      --   others while looking for it
   deriving (Eq, Ord)
 
++instance Semigroup FindResult where+  NamesSeen i <> NamesSeen j = NamesSeen (i + j)+  NamesSeen i <> Index j     = Index (i + j)+  Index j     <> _           = Index j+ -- | @FindResult@ forms a monoid which combines information from
 --   several 'findpatrec' operations.  @mappend@ takes the leftmost
 --   'Index', and combines the number of names seen to the left of it
 --   so we can correctly compute its global index.
 instance Monoid FindResult where
   mempty = NamesSeen 0
-  NamesSeen i `mappend` NamesSeen j = NamesSeen (i + j)
-  NamesSeen i `mappend` Index j     = Index (i + j)
-  Index j     `mappend` _           = Index j
+#if !MIN_VERSION_base(4,11,0)+  mappend = (Semigroup.<>)+#endif 
 -- | Find the (first) index of the name in the pattern, if it exists.
 findpat :: Alpha a => a -> AnyName -> Maybe Integer
@@ -259,15 +268,21 @@ --   if the end of the pattern was reached too soon.
 newtype NthCont = NthCont { runNthCont :: Integer -> NthResult }
 
++instance Semigroup NthCont where+  (NthCont f) <> (NthCont g)+    = NthCont $ \i -> case f i of+        Found n     -> Found n+        CurIndex i' -> g i'+ -- | @NthCont@ forms a monoid: function composition which
 --   short-circuits once a result is found.
 instance Monoid NthCont where
   mempty = NthCont $ \i -> CurIndex i
-  (NthCont f) `mappend` (NthCont g)
-    = NthCont $ \i -> case f i of
-                        Found n     -> Found n
-                        CurIndex i' -> g i'
-
+#if !MIN_VERSION_base(4,11,0)  +  mappend = (Semigroup.<>)+#endif+ -- | If we see a name, check whether the index is 0: if it is, we've
 --   found the name we're looking for, otherwise continue with a
 --   decremented index.

@@ -89,7 +89,7 @@  instance (Show a, Show b) => Show (GenBind order card a b) where   showsPrec p (B a b) = showParen (p>0)-      (showString "bind " . showsPrec 11 a . showsPrec 11 b)+      (showString "bind " . showsPrec 11 a . showString " " . showsPrec 11 b)  -------------------------------------------------- -- Rebind

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP           #-} {-# LANGUAGE PatternGuards #-} ---------------------------------------------------------------------- -- |@@ -21,6 +22,8 @@ import qualified Data.Set as S import Control.Arrow ((&&&)) import Control.Monad ((>=>))+import Data.Semigroup (Semigroup)+import qualified Data.Semigroup as Semigroup  -- | A /permutation/ is a bijective function from names to names --   which is the identity on all but a finite set of names.  They@@ -64,9 +67,15 @@          ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a]))  -- | Permutations form a monoid under composition.+instance Ord a => Semigroup (Perm a) where+  (<>) = compose++-- | Permutations form a monoid under composition. instance Ord a => Monoid (Perm a) where   mempty  = empty-  mappend = compose+#if !MIN_VERSION_base(4,11,0)  +  mappend = (Semigroup.<>)+#endif  -- | Is this the identity permutation? isid :: Ord a => Perm a -> Bool@@ -79,7 +88,11 @@ join :: Ord a => Perm a -> Perm a -> Maybe (Perm a) join (Perm p1) (Perm p2) =      let overlap = M.intersectionWith (==) p1 p2 in+#if MIN_VERSION_containers(0,5,0)     +     if M.foldr (&&) True overlap then+#else      if M.fold (&&) True overlap then+#endif        Just (Perm (M.union p1 p2))        else Nothing 

@@ -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 Examples.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+

@@ -0,0 +1,184 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) The University of Pennsylvania, 2006+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A file demonstrating the use of RepLib+--+-----------------------------------------------------------------------------++module Examples.Basic where++import Generics.RepLib+--import Language.Haskell.TH+++-- For each datatype that we define, we need to also create its representation.+-- The template Haskell function derive does this automatically for+-- each type.++data Tree a = Leaf a | Node (Tree a) (Tree a)+$(derive [''Tree])++data Day = Monday | Tuesday | Wednesday | Thursday | Friday | Saturday | Sunday++$(derive [''Day])++-- Note, for mutually recursive datatypes, use "derive" and give list+-- of type names.++-- Note also that the functions of RepLib can cooperate with the+-- traditional 'deriving' mechanism+data Company   = C [Dept]                 deriving (Eq, Ord, Show)+data Dept      = D String Manager [CUnit] deriving (Eq, Ord, Show)+data Manager   = M Employee               deriving (Eq, Ord, Show)+data CUnit     = PU Employee | DU Dept    deriving (Eq, Ord, Show)+data Employee  = E Person Salary          deriving (Eq, Ord, Show)+data Person    = P String                 deriving (Eq, Ord, Show)+data Salary    = S Float                  deriving (Eq, Ord, Show)++$(derive+    [''Company,+     ''Dept,+     ''CUnit,+     ''Employee,+          ''Manager,+          ''Person,+          ''Salary])+++--+-- Some sample data for these types+--+t1 :: Tree Int+t1 = Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6))++t2 :: Tree Int+t2 = Node (Node (Leaf 0) (Leaf 7)) (Leaf 20)++s1 :: Company+s1 = C [D "Types" (M (E (P "Stephanie") (S 1000.0)))+            [PU (E (P "Michael") (S 50)),+             PU (E (P "Samuel") (S 50)),+             PU (E (P "Theodore") (S 50))],+        D "Terms" (M (E (P "Stephanie") (S 200)))+            [DU (D "Shipping" (M (E (P "Alice") (S 3000)))+                [])]]+++--+-- Prelude operations.+--+-- Note that we didn't derive Eq, Ord, Bounded or Show for "Day" and "Tree". We can+-- do that now with operations from RepLib.PreludeLib.++-- for Day+instance Eq Day      where+  (==) = eqR1 rep1+instance Ord Day     where+  compare = compareR1 rep1+instance Bounded Day where+  minBound = minBoundR1 rep1+  maxBound = maxBoundR1 rep1+instance Show Day    where+  showsPrec = showsPrecR1 rep1++-- for Tree+instance (Rep a, Eq a) => Eq (Tree a)     where (==) = eqR1 rep1+instance (Rep a, Show a) => Show (Tree a) where showsPrec = showsPrecR1 rep1+instance (Rep a, Ord a) => Ord (Tree a)   where compare = compareR1 rep1++-- Besides the prelude operations, RepLib provides a number of other+-- type-indexed operations.++--+-- Instances for RepLib.Lib operations+--++-- Generate creates arbitrary elements of a type, up to a certain depth.+instance Generate Day+instance Generate a => Generate (Tree a)+instance Generate Company+instance Generate Dept+instance Generate Manager+instance Generate CUnit+instance Generate Employee+instance Generate Person+instance Generate Salary+++-- Sum adds together all of the Ints in a datastructure+instance GSum a => GSum (Tree a)+instance GSum Company+instance GSum Dept+instance GSum Manager+instance GSum CUnit+instance GSum Employee+instance GSum Person+instance GSum Salary++-- Shrink creates smaller versions of a data structure.+instance Shrink a => Shrink (Tree a)++--+-- SYB Style operations+--+-- RepLib also supports many of the combinators from the SYB library. For example,+-- we can include the following code from the "Paradise" benchmark that gives everyone+-- in the company a raise.++-- Increase salary by percentage+increase :: Float -> Company -> Company+increase k = everywhere (mkT (incS k))++-- "interesting" code for increase+incS :: Float -> Salary -> Salary+incS k (S s) = S (s * (1+k))+++--+-- Generalized folds+--+-- finally, we define generalized versions of fold left and+-- fold right for the Tree type constructor.+-- instance Fold Tree where+--   foldRight op = rreduceR1 (rTree1 ( RreduceD { rreduceD = op }+--                                    , RreduceD { rreduceD = foldRight op}))+--   foldLeft  op = lreduceR1 (rTree1 ( LreduceD { lreduceD = op }+--                                    , LreduceD { lreduceD = foldLeft op }))++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")+++main = do+   assert "m1" (minBound == Monday)+   assert "m2" (maxBound == Sunday)++   assert "e1" (t1 == Node (Node (Leaf 3) (Leaf 4)) (Node (Leaf 5) (Leaf 6)))++   assert "o3" (Monday < Tuesday)+   assert "o4" (not (t1 < t2))+--+   assert "g1" (generate 7 == [Monday,Tuesday,Wednesday,Thursday,Friday,Saturday,Sunday])+   assert "g2" ((generate 3 :: [Tree Int]) == [Leaf 0,Leaf 1,Leaf 2,Node (Leaf 0) (Leaf 0),Node (Leaf 0) (Leaf 1),Node (Leaf 0) (Node (Leaf 0) (Leaf 0)),Node (Leaf 1) (Leaf 0),Node (Leaf 1) (Leaf 1),Node (Leaf 1) (Node (Leaf 0) (Leaf 0)),Node (Node (Leaf 0) (Leaf 0)) (Leaf 0),Node (Node (Leaf 0) (Leaf 0)) (Leaf 1),Node (Node (Leaf 0) (Leaf 0)) (Node (Leaf 0) (Leaf 0))])++--+   assert "s1" (subtrees t1 == [Node (Leaf 3) (Leaf 4),Node (Leaf 5) (Leaf 6)])+--   assert "s2" (gsum t1 == 18)+--   assert "s3" (gsum t2 == 27)+--+   assert "i1" (increase 0.1 s1 == C [D "Types" (M (E (P "Stephanie") (S 1100.0))) [PU (E (P "Michael") (S 55.0)),PU (E (P "Samuel") (S 55.0)),PU (E (P "Theodore") (S 55.0))],D "Terms" (M (E (P "Stephanie") (S 220.0))) [DU (D "Shipping" (M (E (P "Alice") (S 3300.0))) [])]])++   assert "i2" (s1 < (increase 0.2 s1))+--+--   assert "f1" (gproduct t1 == 360)+--   assert "f2" (count t1 == 4)+

@@ -0,0 +1,291 @@+{-# LANGUAGE PatternGuards+           , MultiParamTypeClasses+           , TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , FlexibleContexts+           , UndecidableInstances+  #-}++{- A "simple" core dependent calculus.++term     M ::= x | * | \D. M | M [N] | Pi D. B+             | T | c+             | case M with y of [ c [x] => N ]++tele     D ::= . | x:A, D++ctx      G ::= . | G, x:A++judgement forms:+    G |- D wf         telescope wellformedness+    G |- [ M ] : D    check a list of terms against a telescope+    G |- chk M : A    check that term M has type A+    G |- inf M : A    infer the type of M (which is A)+    G |- A == B       check that A & B are equal++typing rules:++     telescope well formedness   (checkTele)++     G |-chk A : *    G,x:A |- D wf+     ----------------------------- cons+     G |- x:A, D wf++     ------------- nil+     G |- [] wf++     list of terms vs a telescope   (checks)++     G |-chk N : A    (G |- [N] : D)[x |-> N]+     -------------------------------------- cons+     G |- N, [N] : x:A,D++     -------------- nil+     G |- [] : .++     terms (check && infer)++     x:A \in G+     -----------+     G |- inf x : A++     G |- D wf        G, D |- chk B : *+     --------------------------------+     G |- inf Pi D.B : *++     G |- D wf        G, D |- inf M : B+     -------------------------------+     G |- inf \D.M : Pi D. B++     G |- inf M : Pi D.B      G |- [N] : D+     ---------------------------------------+     G |- inf M [N] : B [ D |-> [N] ]+       ** note: simultaneous substitution for the domain **++     ----------+     G |- inf * : *++     G |- inf  M : A    G |- A == B+     ----------------------------+     G |- chk  M : B++     A = Pi D . *+     T : A \in Sigma+     ---------------------+     G |- inf T : A++     c: A \in Sigma+     A = Pi D. Pi D'. T [x]+     dom(D) = [x]+     -------------+     G |- inf c : A++     G |- inf M : T [ P ]+     G |- chk A : *+     for each i,+         ci : Pi D. Pi Di. T [x] \in Sigma  where dom(D) = [x]+         G, Di[ D |-> [P] ], y : M = C [w] |- chk N : A+    ------------------------------------------------------+     G |-inf case M in A with y of [ c [w] => N ] : A++-}++import Unbound.LocallyNameless++import Data.Monoid+import Control.Monad+import Control.Monad.Trans.Error++data TyCon    -- tags for the names of type constructors+data DataCon  -- and data constructors so that we don't get them+              -- confused with variables++-- initial context of data and type constructors+sigmaData :: [(Name DataCon, Exp)]+sigmaData = undefined++sigmaTy  :: [(Name TyCon, Exp)]+sigmaTy = undefined++teq :: Name TyCon+teq = string2Name "=="++data Exp = EVar (Name Exp)+         | EStar+         | ELam (Bind Tele Exp)+         | EApp Exp [Exp]+         | EPi (Bind Tele Exp)+         | ETyCon (Name TyCon)+         | ELet (Bind Lets Exp)+         | EDataCon (Name DataCon)+         | ECase Exp Exp (Bind (Name Exp)+                    [(Name DataCon,Bind [Name Exp] Exp)])+  deriving Show++data Tele = Empty+          | Cons (Rebind (Name Exp, Embed Exp) Tele)+  deriving Show++type Ctx  = [ (Name Exp, Exp) ]++$(derive [''TyCon, ''DataCon, ''Exp, ''Tele])++instance Alpha Exp+instance Alpha Tele++instance Subst Exp Exp where+  isvar (EVar v) = Just (SubstName v)+  isvar _        = Nothing++instance Subst Exp Tele++------------------------------------------------++-- for examples++evar :: String -> Exp+evar = EVar . string2Name++elam :: [(String, Exp)] -> Exp -> Exp+elam t b = ELam (bind (mkTele t) b)++epi :: [(String, Exp)] -> Exp -> Exp+epi t b = EPi (bind (mkTele t) b)++earr :: Exp -> Exp -> Exp+earr t1 t2 = epi [("_", t1)] t2++eapp :: Exp -> Exp -> Exp+eapp a b = EApp a [b]++mkTele :: [(String, Exp)] -> Tele+mkTele []          = Empty+mkTele ((x,e) : t) = Cons (rebind (string2Name x, Embed e) (mkTele t))++{- Polymorphic identity function -}++pid :: Exp+pid = elam [("A", EStar), ("x", evar "A")] (evar "x")++{-+ELam (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@1)+-}++{- Polymorphic identity type: -}+sid :: Exp+sid = epi [("A", EStar), ("x", evar "A")] (evar "A")++{-+EPi (<(Cons (<<(A,{EStar})>> Cons (<<(x,{EVar 0@0})>> Empty)))> EVar 0@0)+-}++{- Polymorphic identity type: -}+sid2 :: Exp+sid2 = epi [("B", EStar), ("y", evar "B")] (evar "B")+++----------------------------------------------------------+-- Type checker++type M = ErrorT String FreshM+ok = return ()++runM :: M a -> a+runM m = case (runFreshM (runErrorT m)) of+   Left s  -> error s+   Right a -> a++lookUp :: Name a -> [(Name a, b)] -> M b+lookUp n []     = throwError $ "Not in scope: " ++ show n+lookUp v ((x,a):t') | v == x    = return a+                    | otherwise = lookUp v t'++unPi :: Ctx -> Exp -> M (Bind Tele Exp)+unPi g (EPi bnd) = return bnd+unPi g e         = throwError $ "Expected pi type, got " ++ show e ++ " instead"++unVar :: Exp -> M (Name Exp)+unVar (EVar x) = return x+unVar e        = throwError $ "Expected variable, got " ++ show e ++ " instead"++unTApp :: Ctx -> Exp -> M (Name TyCon, [Exp])+unTApp _ (EApp (ETyCon n) args) = return (n, args)+unTApp _ e = throwError $ "Expected datatype, got " ++ show e++ " instead"++-- Check a telescope and push it onto the context+checkTele :: Ctx -> Tele -> M Ctx+checkTele g Empty = return g+checkTele g (Cons rb) = do+  let ((x,Embed t), tele) = unrebind rb+  a <- infer g t+  check g a EStar+  checkTele ((x,t) : g) tele++infer :: Ctx -> Exp -> M Exp+infer g (EVar x)  = lookUp x g+infer _ EStar     = return EStar+infer g (ELam bnd) = do+    (delta, m) <- unbind bnd+    g' <- checkTele g delta+    b <- infer g' m+    return . EPi $ bind delta b+infer g (EApp m ns) = do+    bnd <- (unPi g) =<< infer g m+    (delta, b) <- unbind bnd+    checks g ns delta  --- ensures that the length ns == length (binders delta)+    return $ substs (zip (binders delta) ns) b+infer g (EPi bnd) = do+    (delta, b) <- unbind bnd+    g' <- checkTele g delta+    check g' b EStar+    return EStar+infer g (ETyCon n) = do+    bnd <- (unPi g) =<< lookUp n sigmaTy+    (delta, t) <- unbind bnd+    checkEq g t EStar+    return $ EPi bnd+infer g (EDataCon c) = do+  bnd <- (unPi g) =<< lookUp c sigmaData+  (delta, t) <- unbind bnd+  bnd' <- unPi g t+  (delta', EApp (ETyCon _) vars) <- unbind bnd'+  vs <- mapM unVar vars+  if vs == binders delta then return $ EPi bnd+     else throwError $ "incorrect result type for " ++ show (EDataCon c)+infer g (ECase m a bnd) = do+   check g a EStar+   (y, brs) <- unbind bnd+   t <- infer g m+   (n, ps)  <- unTApp g t+   _ <- mapM (checkBr y ps) brs+   return a+    where+      checkBr y ps (c,bnd) = do+         cbnd <- (unPi g) =<< lookUp c sigmaData+         (delta, rest) <- unbind cbnd+         cbnd' <- unPi g rest+         Just (deltai, _, ws, n) <- unbind2 cbnd' bnd+         g' <- checkTele g (substs (zip (binders delta) ps) deltai)+         let g'' = (y, EApp (ETyCon teq) [m, (EApp (EDataCon c) (map EVar ws))]): g'+         check g' n a++check :: Ctx -> Exp -> Exp -> M ()+check g m a = do+  b <- infer g m+  checkEq g b a++checks :: Ctx -> [Exp] -> Tele -> M ()+checks _ [] Empty = ok+checks g (e:es) (Cons rb) = do+  let ((x, Embed a), t') = unrebind rb+  check g e a+  checks (subst x e g) (subst x e es) (subst x e t')+checks _ _ _ = throwError $ "Unequal number of parameters and arguments"+++-- A conservative, inexpressive notion of equality, just for the sake+-- of the example.+checkEq :: Ctx -> Exp -> Exp -> M ()+checkEq _ e1 e2 = if aeq e1 e2 then return () else throwError $ "Couldn't match: " ++ show e1 ++ " " ++ show e2+

@@ -0,0 +1,140 @@+{-# LANGUAGE TemplateHaskell,+             ScopedTypeVariables,+             FlexibleInstances,+             MultiParamTypeClasses,+             FlexibleContexts,+             UndecidableInstances,+             GADTs #-}++module F where++import Unbound.LocallyNameless++import Control.Monad+import Control.Monad.Trans.Error+import Data.List as List++-- System F with type and term variables++type TyName = Name Ty+type TmName = Name Tm++data Ty = TyVar TyName+        | Arr Ty Ty+        | All (Bind TyName Ty)+   deriving Show++data Tm = TmVar TmName+        | Lam (Bind (TmName, Embed Ty) Tm)+        | TLam (Bind TyName Tm)+        | App Tm Tm+        | TApp Tm Ty+   deriving Show++$(derive [''Ty, ''Tm])++------------------------------------------------------+instance Alpha Ty where+instance Alpha Tm where++instance Subst Tm Ty where+instance Subst Tm Tm where+  isvar (TmVar x) = Just (SubstName x)+  isvar _  = Nothing+instance Subst Ty Ty where+  isvar (TyVar x) = Just (SubstName x)+  isvar _ = Nothing+------------------------------------------------------+-- Example terms+------------------------------------------------------++x :: Name Tm+y :: Name Tm+z :: Name Tm+(x,y,z) = (string2Name "x", string2Name "y", string2Name "z")++a :: Name Ty+b :: Name Ty+c :: Name Ty+(a,b,c) = (string2Name "a", string2Name "b", string2Name "c")++-- /\a. \x:a. x+polyid :: Tm+polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x))))++-- All a. a -> a+polyidty :: Ty+polyidty = All (bind a (Arr (TyVar a) (TyVar a)))+++-----------------------------------------------------------------+-- Typechecker+-----------------------------------------------------------------+type Delta = [ TyName ]+type Gamma = [ (TmName, Ty) ]++data Ctx = Ctx { getDelta :: Delta , getGamma :: Gamma }+emptyCtx = Ctx { getDelta = [], getGamma = [] }++type M = ErrorT String FreshM++runM :: M a -> a+runM m = case (runFreshM (runErrorT m)) of+   Left s  -> error s+   Right a -> a++checkTyVar :: Ctx -> TyName -> M ()+checkTyVar g v = do+    if List.elem v (getDelta g) then+      return ()+    else+      throwError "NotFound"++lookupTmVar :: Ctx -> TmName -> M Ty+lookupTmVar g v = do+    case lookup v (getGamma g) of+      Just s -> return s+      Nothing -> throwError "NotFound"++extendTy :: TyName -> Ctx -> Ctx+extendTy n ctx = ctx { getDelta =  n : (getDelta ctx) }++extendTm :: TmName -> Ty -> Ctx -> Ctx+extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) }++tcty :: Ctx -> Ty -> M ()+tcty g  (TyVar x) =+   checkTyVar g x+tcty g  (All b) = do+   (x, ty') <- unbind b+   tcty (extendTy x g) ty'+tcty g  (Arr t1 t2) = do+   tcty g  t1+   tcty g  t2++ti :: Ctx -> Tm -> M Ty+ti g (TmVar x) = lookupTmVar g x+ti g (Lam bnd) = do+  ((x, Embed ty1), t) <- unbind bnd+  tcty g ty1+  ty2 <- ti (extendTm x ty1 g) t+  return (Arr ty1 ty2)+ti g (App t1 t2) = do+  ty1 <- ti g t1+  ty2 <- ti g t2+  case ty1 of+    Arr ty11 ty21 | ty2 `aeq` ty11 ->+      return ty21+    _ -> throwError "TypeError"+ti g (TLam bnd) = do+  (x, t) <- unbind bnd+  ty <- ti (extendTy x g) t+  return (All (bind x ty))+ti g (TApp t ty) = do+  tyt <- ti g t+  case tyt of+   (All b) -> do+      tcty g  ty+      (n1, ty1) <- unbind b+      return $ subst n1 ty ty1+

@@ -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)+

@@ -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)+

@@ -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])

@@ -0,0 +1,65 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}++module Issue28 where++import Unbound.LocallyNameless++type Var = Name Term++data Term+  = V Var+  | Unit+  | Pi (Bind (Var, Embed Term) Term)+  | LetRec (Bind (Rec Decl) Term)+    deriving (Show)++data Decl = +  -- a recursive declaration  x : A = m+  -- where x may occur in m but not in A+  Decl {+    declVar :: Var+    , declClass :: Shift (Embed Term)+    , declVal :: Embed Term+    }+  deriving (Show)++$(derive [''Term, ''Decl])++instance Alpha Term+instance Alpha Decl+instance Subst Term Decl +instance Subst Term Term where+  isvar (V x) = Just (SubstName x)+  isvar _ = Nothing++x :: Var+x = s2n "x"++letrec :: Decl -> Term -> Term+letrec d e = LetRec $ bind (rec d) e++decl :: Var -> Term -> Term -> Decl+decl v klass e = Decl v (Shift (Embed klass)) (embed e)+++m0 = letrec (decl x Unit Unit) Unit++-- >> show m1+--     "LetRec (<[Decl {declVar = x, declClass = {{V x}}, declVal = {V 0@0}}]> V 0@0)"+m1 = letrec (decl x (V x) (V x)) (V x)++-- substitution shows that binding is as we expect,+-- >> subst x Unit m1+--     "LetRec (<[Decl {declVar = x, declClass = {{Unit}}, declVal = {V 0@0}}]> V 0@0)"+++-- >> show m2+--     "Pi (<(x,{Unit})> LetRec (<[Decl {declVar = x, declClass = {{V 0@0}}, declVal = {V 0@0}}]> V 0@0))"+--+--     looks a little strange, but the shift is still there+m2 = Pi (bind (x, embed Unit) m1)+++++

@@ -0,0 +1,93 @@+-- Untyped lambda calculus, with small-step evaluation and an example parser++{-# LANGUAGE PatternGuards+           , MultiParamTypeClasses+           , TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , FlexibleContexts+           , UndecidableInstances+  #-}+import Control.Applicative+import Control.Arrow+import Control.Monad++import Control.Monad.Trans.Maybe++import Text.Parsec hiding ((<|>))+import qualified Text.Parsec.Token as P+import Text.Parsec.Language (haskellDef)++import Unbound.LocallyNameless++data Term = Var (Name Term)+          | App Term Term+          | Lam (Bind (Name Term) Term)+  deriving Show++$(derive [''Term])++instance Alpha Term+instance Subst Term Term where+  isvar (Var v) = Just (SubstName v)+  isvar _       = Nothing++done :: MonadPlus m => m a+done = mzero++step :: Term -> MaybeT FreshM Term+step (Var _) = done+step (Lam _) = done+step (App (Lam b) t2) = do+  (x,t1) <- unbind b+  return $ subst x t2 t1+step (App t1 t2) =+      App <$> step t1 <*> pure t2+  <|> App <$> pure t1 <*> step t2++tc :: Monad m => (a -> MaybeT m a) -> (a -> m a)+tc f a = do+  ma' <- runMaybeT (f a)+  case ma' of+    Just a' -> tc f a'+    Nothing -> return a++eval :: Term -> Term+eval x = runFreshM (tc step x)++-- Some example terms++lam :: String -> Term -> Term+lam x t = Lam $ bind (string2Name x) t++var :: String -> Term+var = Var . string2Name++idT = lam "y" (var "y")++foo = lam "z" (var "y")++trueT  = lam "x" (lam "y" (var "x"))+falseT = lam "x" (lam "x" (var "x"))++-- A small parser for Terms+lexer = P.makeTokenParser haskellDef+parens   = P.parens lexer+brackets = P.brackets lexer+ident    = P.identifier lexer++parseTerm = parseAtom `chainl1` (pure App)++parseAtom = parens parseTerm+        <|> var <$> ident+        <|> lam <$> (brackets ident) <*> parseTerm++runTerm :: String -> Either ParseError Term+runTerm = (id +++ eval) . parse parseTerm ""++{- example, 2 + 3 = 5:++    *Main> runTerm "([m][n][s][z] m s (n s z)) ([s] [z] s (s z)) ([s][z] s (s (s z))) s z"+    Right (App (Var s) (App (Var s) (App (Var s) (App (Var s) (App (Var s) (Var z))))))++-}

@@ -0,0 +1,144 @@+{-# 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+--+--+--+-----------------------------------------------------------------------------++-- | A very simple example demonstration of the binding library+-- based on the untyped lambda calculus.+module Examples.LC where++import Unbound.LocallyNameless+import Control.Monad.Reader (Reader, runReader)+import Data.Set as S++import System.Exit (exitFailure)++-- | A Simple datatype for the Lambda Calculus+data Exp = Var (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Exp+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Exp])++-- | With representation types, tbe default implementation of Alpha+-- provides alpha-equivalence and free variable calculation.+instance Alpha Exp++-- | The subst class uses generic programming to implement capture+-- avoiding substitution. It just needs to know where the variables+-- are.+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing+++-- | All new functions should be defined in a monad that can generate+-- locally fresh names.++type M a = FreshM a++-- | Beta-Eta equivalence for lambda calculus terms.+-- If the terms have a normal form+-- then the algorithm will terminate. Otherwise, the algorithm may+-- loop for certain inputs.+(=~) :: 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 -> do+    --    (x, e1'') <- unbind bnd+    --    return $ subst x e2' e1''+      return $ substBind bnd e2'+    otherwise -> return $ App e1' e2'+red (Lam bnd) = do+   (x, e) <- unbind bnd+   e' <- red e+   case e of+     -- look for an eta-reduction+     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return (Lam (bind x e'))+red (Var x) = return $ (Var x)+++---------------------------------------------------------------------+-- Some testing code to demonstrate this library in action.++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed") >> exitFailure++assertM :: String -> M Bool -> IO ()+assertM s c =+  if (runFreshM c) then return ()+  else print ("Assertion " ++ s ++ " failed") >> exitFailure++x :: Name Exp+x = string2Name "x"++y :: Name Exp+y = string2Name "y"++z :: Name Exp+z = string2Name "z"++s :: Name Exp+s = string2Name "s"++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++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 == \x.y+  assert "a1" $ lam x (Var x) `aeq` lam y (Var y)+  -- \x.x /= \x.y+  assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x))+  -- \x.(\y.x) (\y.y) == \y.y+  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))+  -- \x. f x === 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+

@@ -0,0 +1,155 @@+{-# 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+--+--+--+-----------------------------------------------------------------------------++-- | A very simple example demonstration of the binding library+-- based on the untyped lambda calculus.+module LCRec where++import Unbound.LocallyNameless+import Control.Monad.Reader (Reader, runReader)+import Data.Set as S+import Data.List as L++-- | A Simple datatype for the Lambda Calculus+data Exp = Var (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Exp+         | Letrec (Bind (Rec [(Name Exp, Embed Exp)]) Exp)+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Exp])++-- | With representation types, tbe default implementation of Alpha+-- provides alpha-equivalence and free variable calculation.+instance Alpha Exp++-- | The subst class uses generic programming to implement capture+-- avoiding substitution. It just needs to know where the variables+-- are.+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing+++-- | All new functions should be defined in a monad that can generate+-- locally fresh names.++type M a = FreshM a++-- | Beta-Eta equivalence for lambda calculus terms.+-- If the terms have a normal form+-- then the algorithm will terminate. Otherwise, the algorithm may+-- loop for certain inputs.+(=~) :: 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 -> do+        (x, e1'') <- unbind bnd+        return $ subst x e2' e1''+    otherwise -> return $ App e1' e2'+red (Lam bnd) = do+   (x, e) <- unbind bnd+   e' <- red e+   case e of+     -- look for an eta-reduction+     App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return (Lam (bind x e'))+red (Var x) = return $ (Var x)+red (Letrec bnd) = do+  (r, body) <- unbind bnd+  -- get the variable definitions+  let vars = unrec r+  -- substitute them all (once) throughout the body, iteratively+  let newbody = foldr (\ (x,Embed rhs) body -> subst x rhs body) body vars+  let fvs = fv newbody+  -- garbage collect, if possible+  if (L.any (\ (x,_) -> x `S.member` fvs) vars) then+    return $ Letrec (bind (rec vars) newbody)+  else return newbody++---------------------------------------------------------------------+-- 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 (runFreshM 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"++lam :: Name Exp -> Exp -> Exp+lam x y = Lam (bind x y)++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)++e = Letrec (bind (rec [(y, Embed(Var x)), (x, Embed (Var z))]) (Var y))++main :: IO ()+main = do+  -- \x.x == \x.y+  assert "a1" $ lam x (Var x) `aeq` lam y (Var y)+  -- \x.x /= \x.y+  assert "a2" $ not (lam x (Var y) `aeq` lam x (Var x))+  -- \x.(\y.x) (\y.y) == \y.y+  assertM "be1" $ lam x (App (lam y (Var x)) (lam y (Var y))) =~ (lam y (Var y))+  -- \x. f x === 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+

@@ -0,0 +1,825 @@+{- Type checker for LF, based on algorithm in Harper and Pfennig, "On+   Equivalence and Canonical Forms in the LF Type Theory", ACM+   Transactions on Computational Logic, 2000.+-}++{-# LANGUAGE TemplateHaskell+           , ScopedTypeVariables+           , FlexibleInstances+           , MultiParamTypeClasses+           , FlexibleContexts+           , UndecidableInstances+           , TypeSynonymInstances+           , TypeFamilies+           , GeneralizedNewtypeDeriving+           , NoMonomorphismRestriction+  #-}++{- TODO:+   1. [ ] Fix parser to deal with infix type operators+   2. [ ] test on contents of qbf/+   3. [ ] tune for speed?+-}++module Main where++import Prelude hiding (lookup)++import Unbound.LocallyNameless+import Unbound.LocallyNameless.Fresh (contLFreshM)+import Unbound.LocallyNameless.Ops (unsafeUnbind)++import Text.Parsec hiding ((<|>))+import qualified Text.Parsec.Token as P+import Text.Parsec.Language (haskellDef)+import Text.Parsec.String+import qualified Text.Parsec.Expr as PE++import Text.PrettyPrint (Doc, (<+>), (<>), colon, comma, text, render, empty, integer, nest, vcat, ($+$))+import qualified Text.PrettyPrint as PP++import Control.Monad.Error+import Control.Monad.Reader+import Control.Monad.Identity+import Control.Applicative hiding (many)++import qualified Data.Map as M+import qualified Data.Set as S+import Data.List (sortBy, groupBy)+import Data.Function (on)+import Data.Ord (comparing)++import System.Environment++------------------------------+-- Syntax --------------------+------------------------------++-- Kinds+data Kind = KPi (Bind (Name Tm, Embed Ty) Kind) -- {x:ty} k+          | Type                                -- type+  deriving Show++-- Types, also called "Families"+data Ty   = TyPi (Bind (Name Tm, Embed Ty) Ty)  -- {x:ty} ty+          | TyApp Ty Tm                         -- ty tm+          | TyConst (Name Ty)                   -- a+  deriving Show++-- Terms, also called "Objects"+data Tm   = Lam (Bind (Name Tm, Embed Ty) Tm)   -- [x:ty] tm+          | TmApp Tm Tm                         -- tm tm+          | TmVar (Name Tm)                     -- x+  deriving Show+  -- Harper and Pfennig distinguish between term *variables* and term+  -- *constants*, but for our purposes there is no need to distinguish+  -- between them.++$(derive [''Kind, ''Ty, ''Tm])++instance Alpha Kind+instance Alpha Ty+instance Alpha Tm++-- There are no term variables in types or kinds, so we can just+-- use the default structural Subst instances.+instance Subst Tm Kind+instance Subst Tm Ty++-- For Tm we must implement isvar so the Subst instance knows about+-- term variables.+instance Subst Tm Tm where+  isvar (TmVar v) = Just (SubstName v)+  isvar _         = Nothing++-- A declaration is either+--   * a type constant declaration (a name and a kind),+--   * a term constant declaration (with optional type and definition), or+--   * a fixity/precedence declaration.+data Decl = DeclTy (Name Ty) Kind+          | DeclTm (Name Tm) (Maybe Ty) (Maybe Tm)+          | DeclInfix Op+  deriving Show++data Op = Op Assoc Integer (Name Tm)+  deriving Show++data Assoc = L | R+  deriving Show++-- A program is a sequence of declarations.+type Prog = [Decl]++--------------------+-- Erasure ---------+--------------------++-- Simple kinds and types (no dependency)+data SKind = SKType+           | SKArr STy SKind+  deriving (Eq, Show)+data STy   = STyConst (Name Ty)+           | STyArr STy STy+  deriving (Eq, Show)  -- structural equality is OK here, since there+                       -- are no bound variables.  Otherwise we could+                       -- use 'aeq' from+                       -- Generics.RepLib.Bind.LocallyNameless.++$(derive [''SKind, ''STy])++class Erasable t where+  type Erased t :: *+  erase :: t -> Erased t++instance Erasable Kind where+  type Erased Kind = SKind+  erase Type = SKType+  erase (KPi b) = SKArr (erase ty) (erase k)+    where ((_, Embed ty), k) = unsafeUnbind b+          -- this is actually safe since we ignore the name+          -- and promise to erase it from k.++instance Erasable Ty where+  type Erased Ty = STy+  erase (TyPi b)      = STyArr (erase t1) (erase t2)+    where ((_, Embed t1), t2) = unsafeUnbind b+  erase (TyApp ty _)  = erase ty+  erase (TyConst c)   = STyConst c++instance Erasable Tm where+  type Erased Tm = Tm+  erase t = t++instance (Erasable a, Erasable b) => Erasable (a,b) where+  type Erased (a,b) = (Erased a, Erased b)+  erase (x,y) = (erase x, erase y)++------------------------------+-- Signatures/contexts -------+------------------------------++data Context tm ty = C (M.Map (Name Tm) tm) (M.Map (Name Ty) ty)++emptyCtx :: Context tm ty+emptyCtx = C M.empty M.empty++extendTm :: Name Tm -> tm -> Context tm ty -> Context tm ty+extendTm x t (C tm ty) = C (M.insert x t tm) ty++extendTy :: Name Ty -> ty -> Context tm ty -> Context tm ty+extendTy x k (C tm ty) = C tm (M.insert x k ty)++lookupTm :: Name Tm -> TcM (Context tm ty) tm+lookupTm x = ask >>= \(C tm _) -> embedMaybe (text $ "Not in scope: term variable " ++ show x)+                                  (M.lookup x tm)++lookupTy :: Name Ty -> TcM (Context tm ty) ty+lookupTy x = ask >>= \(C _ ty) -> embedMaybe (text $ "Not in scope: type constant " ++ show x)+                                  (M.lookup x ty)++embedMaybe :: Doc -> Maybe a -> TcM ctx a+embedMaybe errMsg m = case m of+  Just a  -> return a+  Nothing -> err errMsg++addTrace :: Doc -> TcM ctx String+addTrace msg = do+  chks  <- getChkContext+  trace <- vcat <$> mapM ppr chks+  return . PP.render $ msg $+$ trace++embedEither :: (MonadError String m) => Either String a -> m a+embedEither = either throwError return++instance Erasable a => Erasable (M.Map k a) where+  type Erased (M.Map k a) = M.Map k (Erased a)+  erase = M.map erase++instance (Erasable tm, Erasable ty) => Erasable (Context tm ty) where+  type Erased (Context tm ty) = Context (Erased tm) (Erased ty)+  erase (C tm ty) = C (erase tm) (erase ty)++instance (Erasable a) => Erasable (Maybe a) where+  type Erased (Maybe a) = Maybe (Erased a)+  erase = fmap erase++type Ctx  = Context (Ty, Maybe Tm) Kind+type SCtx = Erased Ctx++withTmBinding :: (MonadReader (Context (tm, Maybe Tm) ty) m, LFresh m)+              => Name Tm -> tm -> m r -> m r+withTmBinding x b = do+  avoid [AnyName x] . local (extendTm x (b, Nothing))++withTmDefn :: (MonadReader (Context tm ty) m, LFresh m)+           => Name Tm -> tm -> m r -> m r+withTmDefn x b = do+  avoid [AnyName x] . local (extendTm x b)++withTyBinding :: (MonadReader (Context tm ty) m, LFresh m)+              => Name Ty -> ty -> m r -> m r+withTyBinding x b = do+  avoid [AnyName x] . local (extendTy x b)++-----------------------+-- Error reporting ----+-----------------------++-- Keep track of what we're in the middle of checking.+data Check = TyCheck Tm+           | KCheck Ty+           | SCheck Kind+           | TmEq Tm Tm STy+           | TyEq Ty Ty SKind+           | KEq Kind Kind+           | DeclCheck Decl++------------------------------+-- Typechecking monad --------+------------------------------++newtype TcM ctx a = TcM { unTcM :: ErrorT String (ReaderT ctx (ReaderT [Check] LFreshM)) a }+  deriving (Functor, Applicative, Monad, MonadReader ctx, MonadPlus, MonadError String, LFresh)++getTcMAvoids :: TcM ctx (S.Set AnyName)+getTcMAvoids = TcM . lift . lift . lift $ getAvoids++getChkContext :: TcM ctx [Check]+getChkContext = TcM . lift . lift $ ask++-- | Continue a TcM computation, given a binding context, a checking+--   context, and a set of names to avoid.+contTcM :: TcM ctx a -> ctx -> [Check] -> S.Set AnyName -> Either String a+contTcM (TcM m) c chks nms = flip contLFreshM nms . flip runReaderT chks . flip runReaderT c . runErrorT $ m++-- | Run a TcM computation in an empty context.+runTcM :: TcM (Context tm ty) a -> Either String a+runTcM m = contTcM m emptyCtx [] S.empty++-- | Run a subcomputation with an erased context.+withErasedCtx :: TcM SCtx a -> TcM Ctx a+withErasedCtx m = do+  c <- ask+  chks <- getChkContext+  nms <- getTcMAvoids+  embedEither $ contTcM m (erase c) chks nms++-- | Run a subcomputation with another check pushed on the checking+--   context stack.+whileChecking :: Check -> TcM ctx a -> TcM ctx a+whileChecking chk m = do+  c <- ask+  chks <- getChkContext+  nms <- getTcMAvoids+  embedEither $ contTcM m c (chk:chks) nms++ensure errMsg b = if b then return () else errMsg >>= err++err msg = addTrace msg >>= throwError++matchErr :: Pretty a => a -> a -> TcM ctx Doc+matchErr x y = do+  x' <- ppr x+  y' <- ppr y+  return $ text "Cannot match" <+> x' <+> text "with" <+> y'++unTyPi (TyPi bnd) = return bnd+unTyPi t = ppr t >>= \t' -> err $ text "Expected pi type, got" <+> t' <+> text "instead"++unKPi (KPi bnd) = return bnd+unKPi t = ppr t >>= \t' -> err $ text "Expected pi kind, got" <+> t' <+> text "instead"++isType Type = return ()+isType t = ppr t >>= \t' -> err $ text "Expected Type, got" <+> t' <+> text "instead"++------------------------------+-- Weak head reduction -------+------------------------------++-- Reduce a term to weak-head normal form, or return it unchanged if+-- it is not head-reducible.  Works in erased or unerased contexts.+whr :: Tm -> TcM (Context (t, Maybe Tm) ty) Tm+whr (TmVar a) = (do+  (_, Just defn) <- lookupTm a+  whr defn)+  `mplus`+  return (TmVar a)++whr (TmApp (Lam b) m1) =+  lunbind b $ \((x,_),m2) ->+    whr $ subst x m1 m2++whr (TmApp m1 m2) = do+  m1' <- whr m1+  case m1' of+    Lam _ -> whr (TmApp m1' m2)+    _     -> return $ TmApp m1' m2++whr t = return t++------------------------------+-- Term equality -------------+------------------------------++-- Type-directed term equality.  In context Delta, is M <==> N at+-- simple type tau?+tmEq :: Tm -> Tm -> STy -> TcM SCtx ()+tmEq m n t = whileChecking (TmEq m n t) $ tmEqWhr m n t++tmEqWhr :: Tm -> Tm -> STy -> TcM SCtx ()+tmEqWhr m n t = do+  m' <- whr m+  n' <- whr n+  whileChecking (TmEq m' n' t) $ tmEq' m' n' t -- XXX++  -- XXX todo: might be nice to have 'lfresh' and 'lfreshen', the+  -- first NOT taking an argument++  -- XXX todo: need nicer way of doing "string2Name"+-- Type-directed term equality on terms in WHNF+tmEq' :: Tm -> Tm -> STy -> TcM SCtx ()+tmEq' m n (STyArr t1 t2) = do+  x <- lfresh (string2Name "_x")+  withTmBinding x t1 $+    tmEq (TmApp m (TmVar x)) (TmApp n (TmVar x)) t2+tmEq' m n a@(STyConst {}) = do+  a' <- tmEqS m n+  ensure (matchErr a a') $ a == a'++-- Structural term equality.  Check whether two terms in WHNF are+-- structurally equal, and return their "approximate type" if so.+tmEqS :: Tm -> Tm -> TcM SCtx STy++tmEqS (TmVar a) (TmVar b) = do+  ensure (matchErr a b) $ a == b+  (tyA,_) <- lookupTm a  -- XXX+  return tyA++tmEqS (TmApp m1 m2) (TmApp n1 n2) = do+  ty <- tmEqS m1 n1+  case ty of+    STyArr t2 t1 -> do+      tmEq m2 n2 t2+      return t1+    _            -> do+      ty' <- ppr ty+      err $+        text "Left-hand side of an application has type" <+> ty' <> text "; expecting an arrow type"++tmEqS t1 t2 = err $ text "Term mismatch"++------------------------------+-- Type equality -------------+------------------------------++-- Kind-directed type equality.+tyEq :: Ty -> Ty -> SKind -> TcM SCtx ()+tyEq ty1 ty2 k = whileChecking (TyEq ty1 ty2 k) $ tyEq' ty1 ty2 k++tyEq' (TyPi bnd1) (TyPi bnd2) SKType =  -- XXX+  lunbind2 bnd1 bnd2 $ \(Just ((x, Embed a1), a2, (_, Embed b1), b2)) -> do+    tyEq a1 b1 SKType+    withTmBinding x (erase a1) $ tyEq a2 b2 SKType++tyEq' a b SKType = do+  t <- tyEqS a b+  ensure (matchErr t SKType) $ t == SKType++tyEq' a b (SKArr t k) = do+  x <- lfresh (string2Name "_x")+  withTmBinding x t $ tyEq (TyApp a (TmVar x)) (TyApp b (TmVar x)) k++-- Structural type equality.+tyEqS :: Ty -> Ty -> TcM SCtx SKind+tyEqS (TyConst a) (TyConst b) = do+  ensure (matchErr a b) $ a == b+  lookupTy a++tyEqS (TyApp a m) (TyApp b n) = do+  SKArr t k <- tyEqS a b  -- XXX+  tmEq m n t+  return k++tyEqS t1 t2 = do+  t1' <- ppr t1+  t2' <- ppr t2+  err $ text "Types are not equal: " <+> t1' <> comma <+> t2'++------------------------------+-- Kind equality -------------+------------------------------++-- Algorithmic kind equality.+kEq :: Kind -> Kind -> TcM SCtx ()++kEq Type Type = return ()++kEq k1@(KPi bnd1) k2@(KPi bnd2) = whileChecking (KEq k1 k2) $+  lunbind bnd1 $ \((x, Embed a), k) ->+  lunbind bnd2 $ \((_, Embed b), l) -> do+    tyEq a b SKType+    withTmBinding x (erase a) $ kEq k l++kEq k1 k2 = do+  k1' <- ppr k1+  k2' <- ppr k2+  err $ text "Kinds are not equal:" <+> k1' <> comma <+> k2'++------------------------------+-- Type checking -------------+------------------------------++-- Compute the type of a term.+tyCheck :: Tm -> TcM Ctx Ty+tyCheck tm = whileChecking (TyCheck tm) $ tyCheck' tm++tyCheck' :: Tm -> TcM Ctx Ty+tyCheck' t@(TmVar x)     = liftM fst $ lookupTm x+tyCheck' t@(TmApp m1 m2) = do+  bnd <- unTyPi =<< tyCheck m1+  a2  <- tyCheck m2+  lunbind bnd $ \((x, Embed a2'), a1) -> do+    withErasedCtx $ tyEq a2' a2 SKType+    return $ subst x m2 a1+tyCheck' t@(Lam bnd) =+  lunbind bnd $ \((x, Embed a1), m2) -> do+    isType =<< kCheck a1+    a2   <- withTmBinding x a1 $ tyCheck m2+    return $ TyPi (bind (x, Embed a1) a2)++-- Compute the kind of a type.+kCheck :: Ty -> TcM Ctx Kind+kCheck ty = whileChecking (KCheck ty) $ kCheck' ty++kCheck' :: Ty -> TcM Ctx Kind+kCheck' (TyConst a) = lookupTy a+kCheck' (TyApp a m) = do+  bnd <- unKPi =<< kCheck a+  b   <- tyCheck m+  lunbind bnd $ \((x, Embed b'), k) -> do+    withErasedCtx $ tyEq b' b SKType+    return $ subst x m k+kCheck' (TyPi bnd) =+  lunbind bnd $ \((x, Embed a1), a2) -> do+    isType =<< kCheck a1+    isType =<< (withTmBinding x a1 $ kCheck a2)+    return Type++-- Check the validity of a kind.+sortCheck :: Kind -> TcM Ctx ()+sortCheck k = whileChecking (SCheck k) $ sortCheck' k++sortCheck' :: Kind -> TcM Ctx ()+sortCheck' Type      = return ()+sortCheck' (KPi bnd) =+  lunbind bnd $ \((x, Embed a), k) -> do+    isType =<< kCheck a+    withTmBinding x a $ sortCheck k++------------------------------------------------------------+--  Parser  ------------------------------------------------+------------------------------------------------------------++type OpList = [Op]++mkOp :: Op -> PE.Operator String OpList Identity Tm+mkOp (Op a _ nm) = PE.Infix (TmApp . TmApp (TmVar nm) <$ sym (name2String nm))+                            (assoc a)+  where assoc L = PE.AssocLeft+        assoc R = PE.AssocRight++mkOpTable :: OpList -> PE.OperatorTable String OpList Identity Tm+mkOpTable = map (map mkOp) . groupBy ((==) `on` prec) . sortBy (flip $ comparing prec)+  where prec (Op _ n _) = n++type LFParser = Parsec String OpList++lfParseTest :: Show a => LFParser a -> String -> IO ()+lfParseTest p = print . runParser p [] ""++------------------------------+-- Lexing --------------------+------------------------------++startStuff = letter   <|> oneOf "!#$%&*+/<=>?@\\^|-~"+endStuff   = alphaNum <|> oneOf "!#$%&*+/<=>?@\\^|-~"++reservedNames = ["type", "infix", "right", "left"]+             ++ [":", "=", ".", "->", "%", "{", "}", "(", ")"]+++langDef = haskellDef { P.reservedNames   = reservedNames+                     , P.reservedOpNames = reservedNames+                     , P.identStart      = startStuff+                     , P.identLetter     = endStuff+                     , P.opStart         = startStuff+                     , P.opLetter        = endStuff+                     }++lexer    = P.makeTokenParser langDef++parens   = P.parens     lexer+braces   = P.braces     lexer+brackets = P.brackets   lexer+sym      = P.symbol     lexer+op       = P.reservedOp lexer+reserved = P.reserved   lexer+natural  = P.natural    lexer++var      = string2Name <$> P.identifier lexer++------------------------------+-- Terms ---------------------+------------------------------++parseTm :: LFParser Tm+parseTm = parseTmExpr `chainl1` (pure TmApp)++parseTmExpr :: LFParser Tm+parseTmExpr = do+  ops <- getState+  PE.buildExpressionParser (mkOpTable ops) parseAtom++parseAtom :: LFParser Tm+parseAtom = parens parseTm+        <|> TmVar <$> var+        <|> Lam <$> (+              bind+                <$> brackets ((,) <$> var+                                  <*> (Embed <$> (sym ":" *> parseTy))+                             )+                <*> parseTm+              )++------------------------------+-- Types ---------------------+------------------------------++parseTy :: LFParser Ty+parseTy  =+      -- ty ::=++      -- [x:ty] ty+      TyPi <$> (bind+         <$> braces ((,) <$> var+                         <*> (Embed <$> (sym ":" *> parseTy))+                    )+         <*> parseTy)++      -- te -> ty+  <|> try (TyPi <$> (bind+             <$> ((,) (string2Name "_") . Embed <$> parseTyExpr)+             <*> (op "->" *> parseTy)+          ))++      -- te+  <|> parseTyExpr++  -- XXX this does not handle type expressions built using infix type operators!+parseTyExpr :: LFParser Ty+  -- te ::= ta [tm ...]+parseTyExpr = foldl TyApp <$> parseTyAtom <*> many parseAtom++parseTyAtom :: LFParser Ty+parseTyAtom =+      -- ta ::=++      -- (ty)+      parens parseTy++      -- x+  <|> TyConst <$> var++------------------------------+-- Kinds ---------------------+------------------------------++parseKind :: LFParser Kind+parseKind =+      -- k ::=++      -- {x:ty} k+      KPi <$> (bind+       <$> braces ((,) <$> var+                       <*> (Embed <$> (sym ":" *> parseTy))+                  )+       <*> parseKind)++      -- ka -> k+  <|> try (KPi <$> (bind+             <$> ((,) (string2Name "_") . Embed <$> parseTyExpr)+             <*> (op "->" *> parseKind)+          ))++      -- ka+  <|> parseKindAtom++parseKindAtom :: LFParser Kind+parseKindAtom =+      -- ka ::=++      -- (k)+      parens parseKind++      -- Type+  <|> try (Type <$ reserved "type")++------------------------------+-- Declarations --------------+------------------------------++parseDecl :: LFParser Decl+parseDecl = declBody <* sym "."+ where+  declBody =+        DeclInfix <$> (Op <$> (sym "%" *> reserved "infix" *> rl)+                          <*> natural+                          <*> var)++    <|> try (DeclTy <$> var+                    <*> (sym ":" *> parseKind))++    <|> try (DeclTm <$> var+                    <*> (sym ":" *> (Just <$> parseTy))+                    <*> optionMaybe (sym "=" *> parseTm))++    <|>      DeclTm <$> var+                    <*> pure Nothing+                    <*> (sym "=" *> (Just <$> parseTm))+  rl = (L <$ reserved "left") <|> (R <$ reserved "right")++------------------------------+-- Programs ------------------+------------------------------++parseProg :: LFParser Prog+parseProg =+      -- stop at eof+      [] <$ eof++  <|> do d <- parseDecl  -- parse a single decl+         case d of       -- add fixity declarations to the state+           DeclInfix op -> modifyState (op:)+           _ -> return ()++         (d:) <$> parseProg  -- parse the rest of the program++----------------------------------------+-- Pretty-printing ---------------------+----------------------------------------++class Pretty p where+  ppr :: (LFresh m, Functor m) => p -> m Doc++instance Pretty (Name a) where+  ppr = return . text . show++dot = text "."++instance Pretty Decl where+  ppr (DeclTy t k) = do+    t' <- ppr t+    k' <- ppr k+    return $ t' <+> colon <+> k' <> dot+  ppr (DeclTm x mty mdef) = do+    x'   <- ppr x+    tyf  <- case mty of+              Nothing -> return id+              Just ty -> do ty' <- ppr ty+                            return (<+> (colon <+> ty'))+    deff <- case mdef of+              Nothing -> return id+              Just def -> do def' <- ppr def+                             return (<+> (text "=" <+> def'))+    return $ (deff . tyf $ x') <> dot+  ppr (DeclInfix op) = do+    op' <- ppr op+    return $ op' <> dot++instance Pretty Op where+  ppr (Op assoc prec op) = do+    op' <- ppr op+    return $+      text "%infix"+        <+> text (case assoc of L -> "left"; R -> "right")+        <+> integer prec+        <+> op'++instance Pretty Kind where+  ppr Type = return $ text "type"+  ppr (KPi bnd) = lunbind bnd $ \((x, Embed ty), k) -> do+    x'  <- ppr x+    ty' <- ppr ty+    k'  <- ppr k+    if x `S.member` fv k+      then return $ PP.braces (x' <> colon <> ty') <+> k'+      else return $ PP.parens ty' <+> text "->" <+> k'++instance Pretty Ty where+  ppr (TyApp ty tm) = do+    ty' <- ppr ty+    tm' <- ppr tm+    return $ ty' <+> PP.parens tm'+  ppr (TyConst c) = ppr c+  ppr (TyPi bnd) = lunbind bnd $ \((x, Embed ty1), ty2) -> do+    x' <- ppr x+    ty1' <- ppr ty1+    ty2' <- ppr ty2+    if x `S.member` fv ty2+      then return $ PP.braces (x' <> colon <> ty1') <+> ty2'+      else return $ PP.parens ty1' <+> text "->" <+> ty2'++instance Pretty STy where+  ppr sty = ppr (uneraseTy sty)++uneraseTy (STyConst c) = TyConst c+uneraseTy (STyArr t1 t2) = TyPi (bind (string2Name "_", Embed (uneraseTy t1)) (uneraseTy t2))++uneraseK SKType = Type+uneraseK (SKArr sty sk) = KPi (bind (string2Name "_", Embed (uneraseTy sty)) (uneraseK sk))++instance Pretty SKind where+  ppr sk = ppr (uneraseK sk)++instance Pretty Tm where+  ppr (TmVar x) = ppr x+  ppr (TmApp tm1 tm2) = do+    tm1' <- ppr tm1+    tm2' <- ppr tm2+    return $ tm1' <+> PP.parens tm2'+  ppr (Lam bnd) = lunbind bnd $ \((x, Embed ty), tm) -> do+    x' <- ppr x+    ty' <- ppr ty+    tm' <- ppr tm+    return $ PP.brackets (x' <> colon <> ty') <+> tm'++instance Pretty Check where+  ppr (TyCheck tm) =+    (text "While checking the type of:" <+>) <$> ppr tm+  ppr (KCheck ty) =+    (text "While checking the kind of:" <+>) <$> ppr ty+  ppr (SCheck k) =+    (text "While checking the sort of:" <+>) <$> ppr k+  ppr (TmEq m n ty) = do+    m' <- ppr m+    n' <- ppr n+    ty' <- ppr ty+    return $  text "While checking that terms:"+          $+$ nest 4 (m' $+$ n')+          $+$ nest 2 (text "are equal at type")+          $+$ nest 4 ty'+  ppr (TyEq t1 t2 k) = do+    t1' <- ppr t1+    t2' <- ppr t2+    k'  <- ppr k+    return $  text "While checking that types:"+          $+$ nest 4 (t1' $+$ t2')+          $+$ nest 2 (text "are equal at kind")+          $+$ nest 4 k'+  ppr (KEq k1 k2) = do+    k1' <- ppr k1+    k2' <- ppr k2+    return $ text "While checking equality of kinds:"+          $+$ nest 4 (k1' $+$ k2')+  ppr (DeclCheck decl) = do+    d' <- ppr decl+    return $ text "While checking the declaration:" $+$ nest 4 d'++------------------------------+-- Typechecking programs -----+------------------------------++checkProg :: Prog -> TcM Ctx ()+checkProg [] = return ()+checkProg (DeclInfix _ : ds) = checkProg ds+checkProg (d@(DeclTy nm k) : ds) = do+  whileChecking (DeclCheck d) $ sortCheck k+  withTyBinding nm k $ checkProg ds+checkProg ((DeclTm nm Nothing Nothing):_) = do+  throwError $ "Term " ++ show nm+    ++ " has no type or definition! (This shouldn't happen.)"+checkProg (d@(DeclTm nm (Just ty) Nothing) : ds) = do+  whileChecking (DeclCheck d) $ isType =<< kCheck ty+  withTmBinding nm ty $ checkProg ds+checkProg (d@(DeclTm nm Nothing (Just def)) : ds) = do+  ty <- whileChecking (DeclCheck d) $ tyCheck def+  withTmDefn nm (ty, Just def) $ checkProg ds+checkProg (d@(DeclTm nm (Just ty) (Just def)) : ds) = do+  whileChecking (DeclCheck d) $ do+    isType =<< kCheck ty+    ty'  <- tyCheck def+    withErasedCtx $ tyEq ty ty' SKType+  withTmDefn nm (ty, Just def) $ checkProg ds++checkLF :: [FilePath] -> IO ()+checkLF fileNames = do+  files <- mapM readFile fileNames+  case runParser parseProg [] "" (concat files) of+    Left err   -> print err+    Right prog -> do+      -- putStrLn . unlines . map render . runLFreshM . mapM ppr $ prog+      putStrLn . either ("Error: "++) (const "OK!") . runTcM . checkProg $ prog++main = do+  fileNames <- getArgs+  checkLF fileNames

@@ -0,0 +1,32 @@+-- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances +{-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses  #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) The University of Pennsylvania, 2006+-- License     :  BSD+-- +-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+-- Testsuite+--+-----------------------------------------------------------------------------++module Main where++import qualified Examples.Basic as Basic+import qualified Examples.LC as LC+import qualified Examples.STLC as STLC+-- import qualified Examples.Abstract as Abstract+++main = do+     Basic.main+     LC.main+     STLC.main+     -- Abstract.main+     -- F.main+     print "Tests completed"+     

@@ -0,0 +1,201 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  STLC+-- Copyright   :  (c) The University of Pennsylvania, 2010+-- License     :  BSD+--+-- Maintainer  :  sweirich@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+--+--+--+-----------------------------------------------------------------------------++module Examples.STLC where++import Unbound.LocallyNameless+import Data.Set as S++data Ty = TInt | TUnit | Arr Ty Ty+  deriving (Show, Eq)++data Exp = Lit Int+         | Var (Name Exp)+         | Lam (Bind (Name Exp) Exp)+         | App Exp Ty Exp+         | EUnit+  deriving Show++-- Use RepLib to derive representation types+$(derive [''Ty,''Exp])++-- With representation types, default implementations of these+-- classes are available.+instance Alpha Ty where+  +-- aeq :: Alpha a => a -> a -> Bool  +  +instance Alpha Exp where++instance Subst Exp Ty where+instance Subst Exp Exp where+   isvar (Var x) = Just (SubstName x)+   isvar _       = Nothing++-- class Subst a b where+--   subst :: Name b -> a -> b -> a+--   isvar ::++type Ctx = [(Name Exp, Ty)]++type M a = LFreshM a++-- A type checker for STLC terms+tc :: Ctx -> Exp -> Ty -> M Bool+tc g (Var n) ty =+  case lookup n g of+    Just ty' -> return (ty == ty')+    Nothing  -> return False+tc g (Lam bnd) (Arr t1 t2) = do+  lunbind bnd ( \ (x , e) ->+    tc ((x,t1) : g) e t2)+tc g (App e1 t1 e2) t2 = do+  b1 <- tc g e1 (Arr t1 t2)+  b2 <- tc g e2 t1+  return $ b1 && b2+tc g EUnit TUnit = return True+tc g (Lit i) TInt = return True+tc g e t = return False+++-- beta-eta equivalence, from Karl Crary's ATTAPL chapter+-- assumes both terms type check+algeq :: Exp -> Exp -> Ty -> M Bool+algeq e1 e2 TInt  = do+  e1' <- wh e1+  e2' <- wh e2+  patheq e1' e2'+algeq e1 e2 TUnit = return True+algeq e1 e2 (Arr t1 t2) = do+  x <- lfresh (s2n "x")+  algeq (App e1 t1 (Var x)) (App e2 t1 (Var x)) t2++-- path equivalence (for terms in weak-head normal form)+patheq :: Exp -> Exp -> M Bool+patheq (Var x) (Var y) | x == y = return True+patheq (Lit x) (Lit y) | x == y = return True+patheq (App e1 ty e2) (App e1' ty' e2') | ty == ty' = do+ b1 <- patheq e1 e1'+ b2 <- algeq e2 e2' ty+ return $ b1 && b2+patheq _ _ = return False++-- weak-head reduction+wh :: Exp -> M Exp+wh (App e1 ty e2) = do+   e1' <- wh e1+   case e1' of+     Lam bnd ->+       lunbind bnd $ \ (x, e1') ->+       wh (subst x e2 e1')+     _ -> return $ App e1' ty e2+wh e = return e++--- A different equivalence algorithm, based on reduce and compare.+--- (Doesn't support eta equivalences for the unit type.)++-- Parallel beta-eta reduction, prefers beta reductions to+-- eta reductions+red :: Exp -> M Exp+red (App e1 t e2) = do+  e1' <- red e1+  e2' <- red e2+  case e1' of+    Lam bnd ->+      lunbind bnd $ \ (x, e1'') ->+        return $ subst x e2' e1''+    _ -> return $ App e1' t e2'+red (Lam bnd) =+   lunbind bnd $ \ (x, e) -> do+    e' <- red e+    case e of+     -- look for an eta-reduction+     App e1 t (Var y) | y == x && x `S.notMember` fv e1 -> return e1+     otherwise -> return e+red e = return $ e++-- Reduce both sides until you find a match.+redcomp :: Exp -> Exp -> M Bool+redcomp e1 e2 = if e1 `aeq` e2 then return True                                         else do+    e1' <- red e1+    e2' <- red e2+    if e1' `aeq` e1 && e2' `aeq` e2+      then return False+      else redcomp e1' e2'++---------------------------------------------------------------------+-- TDPE ???+{-+data RExp a where+   RVar  :: Name a -> RExp a+   RLam  :: (Bind (Name b) (Exp b)) -> Exp (a -> b)+   RApp  :: RExp (a -> b) -> (RExp a) -> RExp b+   RUnit :: RExp ()++reify   :: (Fresh m, Rep a) => Exp a -> m a+reify e = case rep of+           Unit -> return ()+           (Arr a b) -> do+              e' <- reflect x --here's the rub!+              return $ \ x -> reify (RApp e e')++reflect :: (Fresh m, Rep a) => a -> m (RExp a)+reflect m = case rep of+   Unit -> return RUnit+   (Arr a b) -> do+      x <- fresh "x"+      e' <- reflect (m (reify (RVar x)))+      return $ RLam (bind x e')+-}+---------------------------------------------------------------------++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++assertM :: (a -> Bool) -> String -> M a -> IO ()+assertM f s c =+  if f (runLFreshM c) then return ()+  else print ("Assertion " ++ s ++ " failed")++name1, name2 :: Name Exp+name1 = s2n "x"+name2 = s2n "y"++main :: IO ()+main = do+  -- \x.x === \x.y+  assert "a1" $ Lam (bind name1 (Var name1)) `aeq` Lam (bind name2 (Var name2))+  -- \x.x /= \x.y+  assert "a2" . not $ Lam (bind name1 (Var name2)) `aeq` Lam (bind name1 (Var name1))+  -- [] |- \x. x : () -> ()+  assertM id "tc1" $ tc [] (Lam (bind name1 (Var name1))) (Arr TUnit TUnit)+  -- [] |- \x. x ()  : (Unit -> Int) -> Int+  assertM id "tc2" $ tc []+     (Lam (bind name1+        (App (Var name1) TUnit EUnit))) (Arr (Arr TUnit TInt) TInt)+  -- \x. x  === \x. () :: Unit -> Unit+  assertM id "be1" $+     algeq (Lam (bind name1 (Var name1)))+           (Lam (bind name2 EUnit))+           (Arr TUnit TUnit)+  -- \x. f x === f  :: Int -> Int+  assertM id "be2" $+     algeq (Lam (bind name1 (App (Var name2) TInt (Var name1))))+           (Var name2)+           (Arr TInt TInt)

@@ -0,0 +1,69 @@+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving+ #-}++module Set where++import Unbound.LocallyNameless+import Unbound.LocallyNameless.Types+import Data.List+import Data.Set++data Ty = All (SetPlusBind [Name Ty] Ty)+        | Var (Name Ty)+        | Arr Ty Ty deriving Show++$(derive [''Ty])++instance Alpha Ty++a, b, c :: Rep a => Name a+a = s2n "a"+b = s2n "b"+c = s2n "c"++sall :: [Name Ty] -> Ty -> Ty+sall ns t = All (setbind ns t)++s1 = sall [a, b] (Arr (Var a) (Var b))+s2 = sall [a, b] (Arr (Var b) (Var a))+s3 = sall [b, a] (Arr (Var a) (Var b))+s4 = sall [b, a] (Arr (Var b) (Var a))+s5 = sall [b, a, c] (Arr (Var b) (Var a))+s6 = sall [a, c] (Arr (Var a) (Var c))+++data E =+  L (Bind (Name E) E)+  | V (Name E)+  | A E E+  | C Int+  | LR (SetBind (Rec [(Name E,Embed E)]) E)+  deriving Show+           +$(derive [''E])           + +instance Alpha E  +  +letrec :: [(Name E, Embed E)] -> E -> E+letrec ns t = LR (permbind (Rec ns) t)++p1 = letrec [(a, Embed (V a)), (b, Embed (C 2))] (A (V a) (V b))+p2 = letrec [(b, Embed (V 2)), (a, Embed (V a))] (A (V a) (V b))++assert :: String -> Bool -> IO ()+assert s True  = return ()+assert s False = print ("Assertion " ++ s ++ " failed")++main :: IO ()+main = do+  assert "s1" $ s1 `aeq` s2+  assert "s2" $ s1 `aeq` s3+  assert "s3" $ s1 `aeq` s4+  assert "s4" $ s1 `aeq` s5+  assert "s5" $ s1 `aeq` s6++  -- NOTE: this assertion fails. This is a bug. Perm binds don't do what we want. +  assert "a11" $ p1 `aeq` p2+

@@ -0,0 +1,59 @@+{-# LANGUAGE TemplateHaskell+           , UndecidableInstances+           , TypeOperators+           , GADTs+           , FlexibleInstances+           , ScopedTypeVariables+           , MultiParamTypeClasses+           , KindSignatures+           , RankNTypes+           , StandaloneDeriving+           , OverlappingInstances+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  TaggedTerm+-- Copyright   :  (c) the Unbound team (see LICENSE)+-- License     :  BSD-like (see LICENSE)+--+-- Maintainer  :  byorgey@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------++module TaggedTerm where++import Unbound.LocallyNameless hiding (Con)++data Term+data Pattern++data Expr :: * -> * where+         -- Note: be very careful here!  Name (Expr a) -> Expr a does+         -- not work since the names in patterns will not get+         -- connected up with names in terms.+  Var :: Name (Expr Term) -> Expr a+  App :: Expr a ->  Expr a -> Expr a+  Lam :: Bind (Expr Pattern) (Expr Term) -> Expr Term+  Con :: String -> [Expr a] -> Expr a++deriving instance Show (Expr a)++$(derive [''Term, ''Pattern, ''Expr])++instance (Rep t) => Alpha (Expr t)++instance Subst (Expr Term) (Expr Term) where+  isvar (Var x) = Just (SubstName x)+  isvar _       = Nothing++instance Subst (Expr Term) (Expr Pattern)++test1 :: Expr Term+test1 = Lam (bind (Con "Pair" [Var $ s2n "y", Var $ s2n "z"]) (Con "Pair" [Var (s2n "y"), Var (s2n "x")]))++test2 :: Expr Term+test2 = subst (s2n "y") (Con "Unit" [] :: Expr Term) test1++test3 :: Expr Term+test3 = subst (s2n "x") (Con "Unit" [] :: Expr Term) test1

@@ -0,0 +1,161 @@+{-# OPTIONS -fglasgow-exts #-}+{-# OPTIONS -fallow-undecidable-instances #-}+{-# OPTIONS -fallow-overlapping-instances #-}+{-# OPTIONS -fth #-}++-----------------------------------------------------------------------------+-- |+-- Module      :  UnifyExp+-- Copyright   :  (c) Ben Kavanagh 2008+-- License     :  BSD+--+-- Maintainer  :  ben.kavanagh@gmail.com+-- Stability   :  experimental+-- Portability :  non-portable+--+-- A file demonstrating the use of Generics.Replib.Unify+--+-----------------------------------------------------------------------------++module UnifyExp+where++import Generics.RepLib+import Generics.RepLib.Unify+import Test.HUnit+import Control.Monad.Error++++data Exp = Var Int+	 | Plus Exp Exp+	 | K String+	 deriving (Show, Eq)+$(derive [''Exp])++instance HasVar Int Exp where+    is_var (Var i) = Just i+    is_var _ = Nothing+    var = Var++-- A = "f" ==> [(A, "f")]+test1 :: Maybe [(Int, Exp)]+test1 = solveUnification [(Var 1, K "f")]+++-- A = "f" + A  ==>   fails occurs check+test2 :: Maybe [(Int, Exp)]+test2 = solveUnification [(Var 1, Plus (K "f") (Var 1))]+++-- A + B = B + B ==> A = B+test3 :: Maybe [(Int, Exp)]+test3 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 2))]++-- A + B = B + C ==> [(A, C), (B, C)]+test4 :: Maybe [(Int, Exp)]+test4 = solveUnification [(Plus (Var 1) (Var 2), Plus (Var 2) (Var 3))]+++++data Term = TVar Int+	  | K2 String+	  | App Term Term+	 deriving (Show, Eq)+$(derive [''Term])++instance HasVar Int Term where+    is_var (TVar i) = Just i+    is_var _ = Nothing+    var = TVar++-- There are two ways to override the unify [Char] [Char] problem. the first is to implement+-- unify and only offer the case for K2, defaulting to generic unify in other cases. The other+-- is to implement unify for String using equality, overriding the default Cons/Nil case handling+++-- special instance of unify for String+-- Writing an instance for String which leaves 'special' term 'a' abstract has a problem with case a = String,+-- which leads to overlap with a a case.. So we can only specialise String for a known 'special' term (here Term)+instance (Eq n, Show n, HasVar n Term) => Unify n Term String where+    unifyStep _ x y = if x == y+		      then return ()+		      else throwError $ strMsg ("unify failed when testing equality for " ++ show x ++ " = " ++ show y)+++++-- f(g(A)) = f(B)  ==>   [(B, g(A))]+test5 :: Maybe [(Int, Term)]+test5 = solveUnification [(App (K2 "f") (App (K2 "g") (TVar 1)), App (K2 "f") (TVar 2))]+++-- f(g(A), A) = f(B, xyz) ==> [(A, xyz), (B, g(xyz))]+test6 :: Maybe [(Int, Term)]+test6 = solveUnification [(App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1), App (App (K2 "f") (TVar 2)) (K2 "xyz"))]++-- f(A) = f(B, C) ==> fail. constructor mismatch. App vs K2. This is in essence an 'arity' failure.+-- in a term datatype that had Application as an arity plus list, the arity would not be equal and would call failure.+-- I'm not sure the error message would be adequate. Perhaps I could use a typeclass/newtype to get better error messages+-- on equality failures.+test7 :: Maybe [(Int, Term)]+test7 = solveUnification [(App (K2 "f") (TVar 1),  App (App (K2 "f") (TVar 2)) (TVar 3))]++-- f(A) = f(B) ==> [(A, B)]+test8 :: Maybe [(Int, Term)]+test8 = solveUnification [(App (K2 "f") (TVar 1), App (K2 "f") (TVar 2))]++-- A = B, B = abc  ==>  [(B, abc), (A, abc)]+test9 :: Maybe [(Int, Term)]+test9 = solveUnification [(TVar 1, TVar 2), (TVar 2, K2 "abc")]++-- A = abc, xyz = X, A = X  ==>  fails with built in equality since we effectively ask abc = xyz+test10 :: Maybe [(Int, Term)]+test10 = solveUnification [(TVar 1, K2 "abc"), (K2 "xyz", TVar 2), (TVar 1, TVar 2)]++++-- Test that unification works with surrounding term structure (other datatypes) which are closed, i.e. they have no free variables.+data OuterTerm =  K3 String+	       | Inner Term+	       | App3 OuterTerm OuterTerm+	 deriving (Show, Eq)+$(derive [''OuterTerm])+++-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer+test11 :: Maybe [(Int, Term)]+test11 = solveUnification'+	   (undefined :: Proxy (Int, Term))+	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),+	     App3 (K3 "H") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]+++-- H(f(g(A), A)) = H(f(B, xyz)) ==> [(A, xyz), (B, g(xyz))]  where H is outer+test12 :: Maybe [(Int, Term)]+test12 = solveUnification'+	   (undefined :: Proxy (Int, Term))+	   [(App3 (K3 "H") (Inner $ App (App (K2 "f") (App (K2 "g") (TVar 1))) (TVar 1)),+	     App3 (K3 "I") (Inner $ App (App (K2 "f") (TVar 2)) (K2 "xyz")))]+++++-- todo. fix tests so that errors are tested properly.+tests = test [ test1 ~?= Just [(1,K "f")],+	       test2 ~?= error "***Exception: occurs check failed",+	       test3 ~?= Just [(1,Var 2)],+	       test4 ~?= Just [(1,Var 3),(2,Var 3)],+	       test5 ~?= Just [(2,App (K2 "g") (TVar 1))],+	       test6 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],+	       test7 ~?= error "*** Exception: constructor mismatch",+	       test8 ~?= Just [(1,TVar 2)],+	       test9 ~?= Just [(2,K2 "abc"),(1,K2 "abc")],+	       test10 ~?= error "*** Exception: unify failed in built in equality",+	       test11 ~?= Just [(2,App (K2 "g") (K2 "xyz")),(1,K2 "xyz")],+	       test12 ~?= error "*** Exception: unify failed when testing equality for \"H\" = \"I\""]+++main = runTestTT tests+

@@ -0,0 +1,54 @@+{-# LANGUAGE TemplateHaskell+           , UndecidableInstances+           , TypeOperators+           , GADTs+           , FlexibleInstances+           , ScopedTypeVariables+           , MultiParamTypeClasses+           , KindSignatures+           , RankNTypes+           , StandaloneDeriving+           , OverlappingInstances+ #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  Vec+-- Copyright   :  (c) the Unbound team (see LICENSE)+-- License     :  BSD-like (see LICENSE)+--+-- Maintainer  :  byorgey@cis.upenn.edu+-- Stability   :  experimental+-- Portability :  non-portable+-----------------------------------------------------------------------------++module Vec where++import Unbound.LocallyNameless hiding (Nil)++data Z+data S n++data Vec :: * -> * -> * where+  Nil   :: Vec Z a+  Cons  :: a -> Vec n a -> Vec (S n) a++deriving instance Show a => Show (Vec n a)++data Term = Var (Name Term) +          | Lit (Vec (S (S Z)) Int) +          | Pair Term Term+  deriving Show++$(derive [''Z, ''S, ''Vec, ''Term])++instance (Alpha a, Rep n) => Alpha (Vec n a)+instance Alpha Term++instance Subst Term Term where+  isvar (Var x) = Just (SubstName x)+  isvar _       = Nothing++instance (Rep n, Rep a) => Subst Term (Vec n a)++t :: Term+t = Pair (Var (s2n "x")) (Lit (Cons 1 (Cons 2 Nil)))

@@ -1,10 +1,19 @@ name:           unbound-version:        0.5.1+version:        0.5.1.1 license:        BSD3 license-file:   LICENSE build-type:     Simple cabal-version:  >= 1.10-tested-with:    GHC == 7.0.4, GHC == 7.2.1, GHC == 7.4.1, GHC == 7.6.3, GHC == 7.8.3, GHC == 7.10, GHC == 8.0.1+tested-with:    GHC == 7.0.4,+                GHC == 7.2.1,+                GHC == 7.4.1,+                GHC == 7.6.3,+                GHC == 7.8.3,+                GHC == 7.10,+                GHC == 8.0.1,+                GHC == 8.2.2,+                GHC == 8.4.3,+                GHC == 8.6.1 author:         Stephanie Weirich, Brent Yorgey maintainer:     Stephanie Weirich <sweirich@cis.upenn.edu> homepage:       https://github.com/sweirich/replib@@ -34,6 +43,8 @@                  transformers >= 0.2.2.0 && < 0.6,                  containers >= 0.3 && < 0.6,                  binary >= 0.7 && < 0.9+  if !impl(ghc >= 8.0)+    build-depends: semigroups == 0.18.*   exposed-modules:     Unbound.LocallyNameless,     Unbound.LocallyNameless.Name,@@ -70,11 +81,10 @@                  transformers >= 0.2.2.0 && < 0.6,                  containers >= 0.3 && < 0.6,                  binary >= 0.7 && < 0.9,-                 unbound >= 0.5,                  template-haskell >= 2.11,                  parsec >= 3.1.9 && < 3.2,                  pretty>= 1.1.2 && < 1.2,-                 QuickCheck>=2.8.2 && < 2.10+                 QuickCheck>=2.8.2 && < 2.13       type:       exitcode-stdio-1.0