packages feed

hobbits 1.1.1 → 1.2

raw patch · 24 files changed

+1296/−1351 lines, 24 filesdep −type-equalitydep ~basedep ~haskell-src-extsdep ~haskell-src-meta

Dependencies removed: type-equality

Dependency ranges changed: base, haskell-src-exts, haskell-src-meta, template-haskell

Files

Data/Binding/Hobbits.hs view
@@ -36,17 +36,20 @@   module Data.Binding.Hobbits.Liftable,    -- * Ancilliary modules-  module Data.Type.List,+  module Data.Proxy, module Data.Type.Equality,+  module Data.Type.HList,   -- | Type lists track the types of bound variables.-  module Data.Binding.Hobbits.NuElim-  -- | The "Data.Binding.Hobbits.NuElim" module allows elimination of-  -- bindings and multi-bindings; NOTE: this module is not covered in-  -- the \"Hobbits for Haskell\" paper.+  module Data.Binding.Hobbits.NuMatching+  -- | The "Data.Binding.Hobbits.NuMatching" module exposes the+  -- | NuMatching class, which allows pattern-matching on (G)ADTs in+  -- | the bodies of multi-bindings                             ) where -import Data.Type.List+import Data.Proxy+import Data.Type.Equality+import Data.Type.HList import Data.Binding.Hobbits.Mb import Data.Binding.Hobbits.Closed import Data.Binding.Hobbits.QQ import Data.Binding.Hobbits.Liftable-import Data.Binding.Hobbits.NuElim+import Data.Binding.Hobbits.NuMatching
Data/Binding/Hobbits/Closed.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TemplateHaskell, ViewPatterns #-}  -- | -- Module      : Data.Binding.Hobbits.Closed--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner -- -- License     : BSD3 --@@ -18,14 +18,15 @@   -- * Abstract types   Cl(),   -- * Operators involving 'Cl'-  cl, clApply, unCl, mbApplyCl, mbLiftClosed, noClosedNames,+  cl, clApply, unCl, noClosedNames,   -- * Synonyms   mkClosed, Closed, unClosed ) where -import Data.Binding.Hobbits.Internal (Name, Mb(..), Cl(..))--import Data.Binding.Hobbits.NuElim+import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Internal.Mb+import Data.Binding.Hobbits.Internal.Closed+import Data.Binding.Hobbits.Mb  import Language.Haskell.TH (Q, Exp(..), Type(..)) import qualified Language.Haskell.TH as TH@@ -35,9 +36,6 @@ import qualified Language.Haskell.TH.Syntax as TH  --- -- | @cl@ is used with Template Haskell quotations to create closed terms of -- type 'Cl'. A quoted expression is closed if all of the names occuring in it -- are@@ -69,36 +67,27 @@   -- -- | Closed terms are closed (sorry) under application. clApply :: Cl (a -> b) -> Cl a -> Cl b -- could be defined with cl were it not for the GHC stage restriction clApply (Cl f) (Cl a) = Cl (f a)  -- | Closed multi-bindings are also closed under application.-clMbApply :: (NuElim a, NuElim b) => Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->+clMbApply :: Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->              Cl (Mb ctx b) clMbApply (Cl f) (Cl a) = Cl (mbApply f a) --- | @mbLiftClosed@ is safe because closed terms don't contain names.-mbLiftClosed :: Mb ctx (Cl a) -> Cl a-mbLiftClosed (MkMb _ a) = a- -- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its -- multi-binding. noClosedNames :: Cl (Name a) -> b-noClosedNames _ = error $ "... Clever girl!" ++-  "The `noClosedNames' invariant has somehow been violated."---- | @mbApplyCl@ @f@ @b@ applies a closed function @f@ to the body of--- multi-binding @b@. For example:------ > mbApplyCl $(cl [| f |]) (nu $ \n -> n)   =   nu f-mbApplyCl :: Cl (a -> b) -> Mb ctx a -> Mb ctx b-mbApplyCl f (MkMb names i) = MkMb names (unCl f i)--+noClosedNames (Cl n) =+  -- We compare n to itself to force evaluation, in case the body of+  -- the closed value is non-terminating...+  case cmpName n n of+    _ ->+      error $+      "... Clever girl!" +++      "The `noClosedNames' invariant has somehow been violated."  -- | @mkClosed = cl@ mkClosed = cl
Data/Binding/Hobbits/Examples/LambdaLifting.hs view
@@ -32,8 +32,7 @@   ) where  import Data.Binding.Hobbits-import qualified Data.Type.List.Map as C-import qualified Data.Type.List.Proof.Member as Mem+import qualified Data.Type.HList as C  import Data.Binding.Hobbits.Examples.LambdaLifting.Terms @@ -47,7 +46,7 @@ ------------------------------------------------------------  data LType a where LType :: LType (L a)-type LC c = MapC LType c+type LC c = HList LType c  type family AddArrows c b type instance AddArrows Nil b = b@@ -71,13 +70,13 @@   boundParams ::-  lc ~ (lc0 :> b) => LC lc -> (MapC Name lc -> DTerm a) ->+  lc ~ (lc0 :> b) => LC lc -> (HList Name lc -> DTerm a) ->                      Decl (AddArrows lc a) boundParams (lc0 :> LType) k = -- flagged as non-exhaustive, in spite of type   freeParams lc0 (\ns -> Decl_One $ nu $ \n -> k (ns :> n))  freeParams ::-  LC lc -> (MapC Name lc -> Decl a) -> Decl (AddArrows lc a)+  LC lc -> (HList Name lc -> Decl a) -> Decl (AddArrows lc a) freeParams Nil k = k C.empty freeParams (lc :> LType) k =     freeParams lc (\names -> Decl_Cons $ nu $ \x -> k (names :> x))@@ -87,7 +86,7 @@ ------------------------------------------------------------  -- FIXME: use this type in place of functions-type SubC c' c = MapC Name c -> MapC Name c'+type SubC c' c = HList Name c -> HList Name c'  ------------------------------------------------------------ -- operations on contexts of free variables@@ -96,7 +95,7 @@ data MbLName c a where     MbLName :: Mb c (Name (L a)) -> MbLName c (L a) -type FVList c fvs = MapC (MbLName c) fvs+type FVList c fvs = HList (MbLName c) fvs  -- unioning free variable contexts: the data structure data FVUnionRet c fvs1 fvs2 where@@ -109,12 +108,12 @@   FVUnionRet fvs f1 f2 -> case elemMC fv2 fvs of     Nothing -> FVUnionRet (fvs :> fv2)                (\(xs :> _) -> f1 xs) (\(xs :> x) -> f2 xs :> x)-    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :> C.lookup idx xs)+    Just idx -> FVUnionRet fvs f1 (\xs -> f2 xs :> C.hlistLookup idx xs) fvUnion (fvs1 :> fv1) fvs2 = case fvUnion fvs1 fvs2 of   FVUnionRet fvs f1 f2 -> case elemMC fv1 fvs of     Nothing -> FVUnionRet (fvs :> fv1)                (\(xs :> x) -> f1 xs :> x) (\(xs :> _) -> f2 xs)-    Just idx -> FVUnionRet fvs (\xs -> f1 xs :> C.lookup idx xs) f2+    Just idx -> FVUnionRet fvs (\xs -> f1 xs :> C.hlistLookup idx xs) f2  elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a) elemMC _ Nil = Nothing@@ -132,9 +131,9 @@     SDVar :: Name (D a) -> STerm c a     SApp :: STerm c (a -> b) -> STerm c a -> STerm c b -skelSubst :: STerm c a -> MapC Name c -> DTerm a+skelSubst :: STerm c a -> HList Name c -> DTerm a skelSubst (SWeaken f db) names = skelSubst db $ f names-skelSubst (SVar inC) names = TVar $ C.lookup inC names+skelSubst (SVar inC) names = TVar $ C.hlistLookup inC names skelSubst (SDVar dTVar) _ = TDVar dTVar skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names) @@ -143,7 +142,7 @@   STerm fvs (AddArrows fvs a) -> FVList c fvs -> STerm fvs a skelAppMultiNames db args = skelAppMultiNamesH db args (C.members args) where   skelAppMultiNamesH ::-    STerm fvs (AddArrows args a) -> FVList c args -> MapC (Member fvs) args ->+    STerm fvs (AddArrows args a) -> FVList c args -> HList (Member fvs) args ->     STerm fvs a   skelAppMultiNamesH fvs Nil _ = fvs   -- flagged as non-exhaustive, in spite of type@@ -158,29 +157,33 @@     FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a  fvSSepLTVars ::-  MapC f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a+  HList f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a fvSSepLTVars lc (FVSTerm fvs db) = case fvSSepLTVarsH lc Proxy fvs of   SepRet fvs' f -> FVSTerm fvs' (SWeaken f db)  data SepRet lc c fvs where   SepRet :: FVList c fvs' -> SubC fvs (fvs' :++: lc) -> SepRet lc c fvs +-- | Create a 'Proxy' object for the type list of a 'HList' vector.+proxyOfHList :: HList f c -> Proxy c+proxyOfHList _ = Proxy+ fvSSepLTVarsH ::-  MapC f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs+  HList f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs fvSSepLTVarsH _ _ Nil = SepRet Nil (\_ -> Nil) fvSSepLTVarsH lc c (fvs :> fv@(MbLName n)) = case fvSSepLTVarsH lc c fvs of   SepRet m f -> case raiseAppName (C.mkMonoAppend c lc) n of-    Left idx -> SepRet m (\xs -> f xs :> C.lookup (Mem.weakenL (C.proxy m) idx) xs)+    Left idx -> SepRet m (\xs -> f xs :> C.hlistLookup (C.weakenMemberL (proxyOfHList m) idx) xs)     Right n -> SepRet (m :> MbLName n)-               (\xs -> case C.split (C.mkMonoAppend c' lc) xs of+               (\xs -> case C.splitHList c' lc xs of                          (fvs' :> fv', lcs) ->-                           f (C.append fvs' lcs) :> fv')-    where c' = proxyCons (C.proxy m) fv+                           f (appendHList fvs' lcs) :> fv')+    where c' = proxyCons (proxyOfHList m) fv  raiseAppName ::-  Append c1 c2 c -> Mb c (Name a) -> Either (Member c2 a) (Mb c1 (Name a))+  Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a)) raiseAppName app n =-  case mbApplyCl $(mkClosed [| mbNameBoundP |]) (mbSeparate app n) of+  case fmap mbNameBoundP (mbSeparate (proxiesFromAppend app) n) of     [nuP| Left mem |] -> Left $ mbLift mem     [nuP| Right n |] -> Right n @@ -200,23 +203,23 @@   return $ FVSTerm names $ SApp (SWeaken sub1 db1) (SWeaken sub2 db2) llBody c [nuP| Lam b |] = do   PeelRet lc body <- return $ peelLambdas b-  llret <- llBody (C.append c lc) body+  llret <- llBody (C.appendHList c lc) body   FVSTerm fvs db <- return $ fvSSepLTVars lc llret   cont $ \k ->     Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->                 boundParams lc $ \names2 ->-                skelSubst db (C.append names1 names2))+                skelSubst db (C.appendHList names1 names2))       $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)   where     fvsToLC :: FVList c lc -> LC lc-    fvsToLC = C.mapC mbLNameToProof where+    fvsToLC = C.mapHList mbLNameToProof where       mbLNameToProof :: MbLName c a -> LType a       mbLNameToProof (MbLName _) = LType  -- the top-level lambda-lifting function lambdaLift :: Term a -> Decls a lambdaLift t = runCont (llBody Nil (emptyMb t)) $ \(FVSTerm fvs db) ->-  Decls_Base (skelSubst db (C.mapC (\(MbLName mbn) -> elimEmptyMb mbn) fvs))+  Decls_Base (skelSubst db (C.mapHList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))  mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)-mbLambdaLift = mbApplyCl $(mkClosed [| lambdaLift |])+mbLambdaLift = fmap lambdaLift
Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE QuasiQuotes, ViewPatterns #-}+{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-} {-# LANGUAGE GADTs, KindSignatures #-}  -- |@@ -20,12 +20,17 @@   ) where  import Data.Binding.Hobbits-import qualified Data.Type.List.Map as C+import qualified Data.Type.HList as C  -- dummy datatypes for distinguishing Decl names from Lam names data L a data D a +-- to make a function for HList (for pretty)+newtype StringF x = StringF String+unStringF (StringF str) = str++ ------------------------------------------------------------ -- source terms ------------------------------------------------------------@@ -36,6 +41,8 @@   Lam :: Binding (L b) (Term a) -> Term (b -> a)   App :: Term (b -> a) -> Term b -> Term a +$(mkNuMatching [t| forall a . Term a |])+ instance Show (Term a) where show = tpretty  -- helps to build terms without explicitly using nu or Var@@ -45,10 +52,10 @@ -- pretty print terms tpretty :: Term a -> String tpretty t = pretty' (emptyMb t) C.empty 0-  where pretty' :: Mb c (Term a) -> MapC StringF c -> Int -> String+  where pretty' :: Mb c (Term a) -> HList StringF c -> Int -> String         pretty' [nuP| Var b |] varnames n =             case mbNameBoundP b of-              Left pf  -> unStringF (C.lookup pf varnames)+              Left pf  -> unStringF (C.hlistLookup pf varnames)               Right n -> "(free-var " ++ show n ++ ")"         pretty' [nuP| Lam b |] varnames n =             let x = "x" ++ show n in@@ -66,8 +73,6 @@   TDVar :: Name (D a) -> DTerm a   TApp :: DTerm (a -> b) -> DTerm a -> DTerm b -instance Show (DTerm a) where show = pretty- -- we use this type for a definiens instead of putting lambdas on the front data Decl :: * -> * where   Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)@@ -78,21 +83,22 @@   Decls_Base :: DTerm a -> Decls a   Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a +$(mkNuMatching [t| forall a . DTerm a |])+$(mkNuMatching [t| forall a . Decl a |])+$(mkNuMatching [t| forall a . Decls a |])++instance Show (DTerm a) where show = pretty instance Show (Decls a) where show = decls_pretty  ------------------------------------------------------------ -- pretty printing ------------------------------------------------------------ --- to make a function for MapC (for pretty)-newtype StringF x = StringF String-unStringF (StringF str) = str- -- pretty print terms pretty :: DTerm a -> String pretty t = mpretty (emptyMb t) C.empty -mpretty :: Mb c (DTerm a) -> MapC StringF c -> String+mpretty :: Mb c (DTerm a) -> HList StringF c -> String mpretty [nuP| TVar b |] varnames =     mprettyName (mbNameBoundP b) varnames mpretty [nuP| TDVar b |] varnames =@@ -101,7 +107,7 @@     "(" ++ mpretty b1 varnames         ++ " " ++ mpretty b2 varnames ++ ")" -mprettyName (Left pf) varnames = unStringF (C.lookup pf varnames)+mprettyName (Left pf) varnames = unStringF (C.hlistLookup pf varnames) mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"          @@ -110,7 +116,7 @@ decls_pretty decls =     "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0) -mdecls_pretty :: Mb c (Decls a) -> MapC StringF c -> Int -> String+mdecls_pretty :: Mb c (Decls a) -> HList StringF c -> Int -> String mdecls_pretty [nuP| Decls_Base t |] varnames n =     "in " ++ (mpretty t varnames) mdecls_pretty [nuP| Decls_Cons decl rest |] varnames n =@@ -118,7 +124,7 @@     fname ++ " " ++ (mdecl_pretty decl varnames 0) ++ "\n"     ++ mdecls_pretty (mbCombine rest) (varnames :> (StringF fname)) (n+1) -mdecl_pretty :: Mb c (Decl a) -> MapC StringF c -> Int -> String+mdecl_pretty :: Mb c (Decl a) -> HList StringF c -> Int -> String mdecl_pretty [nuP| Decl_One t|] varnames n =   let vname = "x" ++ show n in   vname ++ " = " ++ mpretty (mbCombine t) (varnames :> StringF vname)
− Data/Binding/Hobbits/Examples/UnitTests/NuElimTest.hs 
@@ -1,49 +0,0 @@-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables, NoMonomorphismRestriction #-}--module NuElimTest where--import Data.Binding.Hobbits-------- some helpers-----proxies2 = Nil :> Proxy :> Proxy--nu2 :: (Name a1 -> Name a2 -> b) -> Mb (Nil :> a1 :> a2) b-nu2 f = nuMulti proxies2 $ \(Nil :> n1 :> n2) -> f n1 n2-------- test that mbApply works correctly for names in the argument-----test1f :: Mb (Nil :> a :> a) (Name a -> Int)-test1f = nu2 $ \n1 n2 n ->-         case () of-           () | Just Refl <- cmpName n n1 -> 1-           () | Just Refl <- cmpName n n2 -> 2-           _ -> 3--test1a = test1f `mbApply` (nu2 $ \n1 n2 -> n1) -- body should be 1-test1b = test1f `mbApply` (nu2 $ \n1 n2 -> n2) -- body should be 2-test1c = nu (\n -> test1f `mbApply` (nu2 $ \n1 n2 -> n)) -- body should be 3--------- test that mbApply works correctly for names in the argument and the--- return value-----test2f :: Mb (Nil :> a :> a) (Name a -> Name a)-test2f = nu2 $ \n1 n2 n ->-         case () of-           () | Just Refl <- cmpName n n1 -> n2-           () | Just Refl <- cmpName n n2 -> n1-           _ -> n--test2a = test2f `mbApply` (nu2 $ \n1 n2 -> n1) -- should be Nu (n1,n2) n2-test2b = test2f `mbApply` (nu2 $ \n1 n2 -> n2) -- should be Nu (n1,n2) n1-test2c = nu (\n -> test2f `mbApply` (nu2 $ \n1 n2 -> n)) -- should be Nu (n) (Nu (n1,n2) n)
− Data/Binding/Hobbits/Internal.hs 
@@ -1,116 +0,0 @@-{-# LANGUAGE GADTs, DeriveDataTypeable #-}---- |--- Module      : Data.Binding.Hobbits.Internal--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ This module is internal to the Hobbits library, and should not be used--- directly.--module Data.Binding.Hobbits.Internal where--import Data.Typeable-import Data.Type.List-import Unsafe.Coerce (unsafeCoerce)-import Data.IORef (IORef, newIORef, readIORef, writeIORef)-import System.IO.Unsafe (unsafePerformIO)---- | A @Name a@ is a bound name that is associated with type @a@.-newtype Name a = MkName Int deriving (Typeable, Eq)--{-|-  An @Mb ctx b@ is a multi-binding that binds exactly one name for each-  type in @ctx@, where @ctx@ has the form @'Nil' ':>' t1 ':>' ... ':>' tn@.--}-data Mb ctx b  = MkMb (MapC Name ctx) b deriving Typeable--{--instance Typeable a => Typeable (Mb ctx a) where-    typeOf (MkMb _ x) = mkTyConApp (mkTyCon "Mb")-                          [mkTyConApp (mkTyCon "Nil") [], typeOf x]--}---{-|-  The type @Cl a@ represents a closed term of type @a@,-  i.e., an expression of type @a@ with no free (Haskell) variables.-  Since this cannot be checked directly in the Haskell type system,-  the @Cl@ data type is hidden, and the user can only create-  closed terms using Template Haskell, through the 'mkClosed'-  operator.--}-newtype Cl a = Cl { unCl :: a }------ building an arbitrary InCtx proof with a given length--- (this is used internally in HobbitLib)--data ExMember where ExMember :: Member c a -> ExMember---- creating some Member proof of length i-memberFromLen :: Int -> ExMember-memberFromLen 0 = ExMember Member_Base-memberFromLen n = case memberFromLen (n - 1) of-  ExMember mem -> ExMember (Member_Step mem)---- unsafely creating a *specific* member proof from length i;--- this is for when we know the ith element of c must be type a-unsafeLookupC :: Int -> Member c a-unsafeLookupC n = case memberFromLen n of-  ExMember mem -> unsafeCoerce mem----- building a proxy for each type in some unknown context-data ExProxy where ExProxy :: MapC Proxy ctx -> ExProxy-proxyFromLen :: Int -> ExProxy-proxyFromLen 0 = ExProxy Nil-proxyFromLen n = case proxyFromLen (n - 1) of-                   ExProxy proxy -> ExProxy (proxy :> Proxy)---- unsafely building a proxy for each type in ctx from the length n--- of ctx; this is only safe when we know the length of ctx = n-unsafeProxyFromLen :: Int -> MapC Proxy ctx-unsafeProxyFromLen n = case proxyFromLen n of-                         ExProxy proxy -> unsafeCoerce proxy---- unsafely convert a list of Ints, used to represent names, to--- names of certain, given types; note that the first name in the--- list becomes the last name in the output, with the same reversal--- used in the Mb representation (see, e.g., mbCombine)-unsafeNamesFromInts :: [Int] -> MapC Name ctx-unsafeNamesFromInts [] = unsafeCoerce Nil-unsafeNamesFromInts (x:xs) =-    unsafeCoerce $ unsafeNamesFromInts xs :> MkName x------------------------------------------------------------------------------------ encapsulated impurity------------------------------------------------------------------------------------ README: we *cannot* inline counter, because we want all uses--- of counter to be the same IORef-counter :: IORef Int-{-# NOINLINE counter #-}-counter = unsafePerformIO (newIORef 0)---- README: fresh_name takes a dummy argument that is used in a dummy--- way to avoid let-floating its body (and thus getting a fresh name--- exactly once)--- README: it *is* ok to inline fresh_name because we don't care in--- what order fresh names are created-fresh_name :: a -> Int-fresh_name a = unsafePerformIO $ do -    dummyRef <- newIORef a-    x <- readIORef counter-    writeIORef counter (x+1)-    return x--fresh_names :: MapC Name ctx -> MapC Name ctx-fresh_names Nil = Nil-fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
+ Data/Binding/Hobbits/Internal/Closed.hs view
@@ -0,0 +1,28 @@+{-# LANGUAGE TemplateHaskell, ViewPatterns #-}++-- |+-- Module      : Data.Binding.Hobbits.Closed+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines the type @'Cl' a@ of closed objects of type+-- @a@. Note that, in order to ensure adequacy of the Hobbits+-- name-binding approach, this representation is hidden from the user,+-- and so this file should never be imported directly by the user.+--++module Data.Binding.Hobbits.Internal.Closed where++{-|+  The type @Cl a@ represents a closed term of type @a@,+  i.e., an expression of type @a@ with no free (Haskell) variables.+  Since this cannot be checked directly in the Haskell type system,+  the @Cl@ data type is hidden, and the user can only create+  closed terms using Template Haskell, through the 'cl' operator.+-}+newtype Cl a = Cl { unCl :: a }
+ Data/Binding/Hobbits/Internal/Mb.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE GADTs, DeriveDataTypeable, Rank2Types, ViewPatterns #-}++-- |+-- Module      : Data.Binding.Hobbits.Internal.Name+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : westbrook@kestrel.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines the type @'Mb' ctx a@. In order to ensure+-- adequacy of the Hobbits name-binding approach, this representation+-- is hidden, and so this file should never be imported directly by+-- the user.+--++module Data.Binding.Hobbits.Internal.Mb where++import Data.Typeable+import Data.Proxy+import Data.Type.Equality+import Data.Type.HList++import Data.Binding.Hobbits.Internal.Name+++{-|+  An @Mb ctx b@ is a multi-binding that binds one name for each type+  in @ctx@, where @ctx@ has the form @'Nil' ':>' t1 ':>' ... ':>' tn@.+  Internally, multi-bindings are represented either as "fresh+  functions", which are functions that quantify over all fresh names+  that have not been used before and map them to the body of the+  binding, or as "fresh pairs", which are pairs of a list of names+  that are guaranteed to be fresh along with a body. Note that fresh+  pairs must come with an 'MbTypeRepr' for the body type, to ensure+  that the names given in the pair can be relaced by fresher names.+-}+data Mb ctx b+    = MkMbFun (HList Proxy ctx) (HList Name ctx -> b)+    | MkMbPair (MbTypeRepr b) (HList Name ctx) b+    deriving Typeable+++{-|+   This type states that it is possible to replace free names with+   fresh names in an object of type @a@. This type essentially just+   captures a representation of the type a as either a Name type, a+   multi-binding, a function type, or a (G)ADT. In order to be sure+   that only the "right" proofs are used for (G)ADTs, however, this+   type is hidden from the user, and can only be constructed with+   'mkNuMatching'.+-}++data MbTypeRepr a where+    MbTypeReprName :: MbTypeRepr (Name a)+    MbTypeReprMb :: MbTypeRepr a -> MbTypeRepr (Mb ctx a)+    MbTypeReprFun :: MbTypeRepr a -> MbTypeRepr b -> MbTypeRepr (a -> b)+    MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a++data MbTypeReprData a =+    MkMbTypeReprData (forall ctx. HList Name ctx -> HList Name ctx -> a -> a)+++{-|+  The call @mapNamesPf data ns ns' a@ replaces each occurrence of a+  free name in @a@ which is listed in @ns@ by the corresponding name+  listed in @ns'@. This is similar to the name-swapping of Nominal+  Logic, except that the swapping does not go both ways.+-}+mapNamesPf :: MbTypeRepr a -> HList Name ctx -> HList Name ctx -> a -> a+mapNamesPf MbTypeReprName Nil Nil n = n+mapNamesPf MbTypeReprName (names :> m) (names' :> m') n =+    case cmpName m n of+      Just Refl -> m'+      Nothing -> mapNamesPf MbTypeReprName names names' n+mapNamesPf MbTypeReprName _ _ _ = error "Should not be possible! (in mapNamesPf)"+mapNamesPf (MbTypeReprMb tRepr) names1 names2 (ensureFreshFun -> (proxies, f)) =+    -- README: the fresh function created below is *guaranteed* to not+    -- be passed elements of either names1 or names2, since it should+    -- only ever be passed fresh names+    MkMbFun proxies (\ns -> mapNamesPf tRepr names1 names2 (f ns))+mapNamesPf (MbTypeReprFun tReprIn tReprOut) names names' f =+    (mapNamesPf tReprOut names names') . f . (mapNamesPf tReprIn names' names)+mapNamesPf (MbTypeReprData (MkMbTypeReprData mapFun)) names names' x =+    mapFun names names' x+++-- | Ensures a multi-binding is in "fresh function" form+ensureFreshFun :: Mb ctx a -> (HList Proxy ctx, HList Name ctx -> a)+ensureFreshFun (MkMbFun proxies f) = (proxies, f)+ensureFreshFun (MkMbPair tRepr ns body) =+    (mapHList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)++-- | Ensures a multi-binding is in "fresh pair" form+ensureFreshPair :: Mb ctx a -> (HList Name ctx, a)+ensureFreshPair (MkMbPair _ ns body) = (ns, body)+ensureFreshPair (MkMbFun proxies f) =+    let ns = mapHList (MkName . fresh_name) proxies in+    (ns, f ns)
+ Data/Binding/Hobbits/Internal/Name.hs view
@@ -0,0 +1,134 @@+{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}++-- |+-- Module      : Data.Binding.Hobbits.Internal.Name+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : westbrook@kestrel.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines the type @'Name' a@ as a wrapper around a fresh+-- integer. Note that, in order to ensure adequacy of the Hobbits+-- name-binding approach, this representation is hidden from the user,+-- and so this file should never be imported directly by the user.+--++module Data.Binding.Hobbits.Internal.Name where++import Data.List+import Data.Functor.Constant+import Data.Typeable+import Data.Type.Equality ((:~:))+import Unsafe.Coerce (unsafeCoerce)+import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import System.IO.Unsafe (unsafePerformIO)++import Data.Type.HList+++-- | A @Name a@ is a bound name that is associated with type @a@.+newtype Name a = MkName Int deriving (Typeable, Eq)++instance Show (Name a) where+  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'++instance Show (HList Name c) where+    show names = "[" ++ (concat $ intersperse "," $ hlistToList $+                        mapHList (Constant . show) names) ++ "]"+++-------------------------------------------------------------------------------+-- Externally visible operators+-------------------------------------------------------------------------------++{-|+  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,+  respectively. When they are equal, @Some e@ is returned for @e@ a proof+  of type @a :~: b@ that their types are equal. Otherwise, @None@ is returned.++  For example:++> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl+> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None+-}+cmpName :: Name a -> Name b -> Maybe (a :~: b)+cmpName (MkName n1) (MkName n2)+  | n1 == n2 = Just $ unsafeCoerce Refl+  | otherwise = Nothing++++-------------------------------------------------------------------------------+-- Hidden, unsafe operators+-------------------------------------------------------------------------------+++-- building an arbitrary InCtx proof with a given length+-- (this is used internally in HobbitLib)++data ExMember where ExMember :: Member c a -> ExMember++-- creating some Member proof of length i+memberFromLen :: Int -> ExMember+memberFromLen 0 = ExMember Member_Base+memberFromLen n = case memberFromLen (n - 1) of+  ExMember mem -> ExMember (Member_Step mem)++-- unsafely creating a *specific* member proof from length i;+-- this is for when we know the ith element of c must be type a+unsafeLookupC :: Int -> Member c a+unsafeLookupC n = case memberFromLen n of+  ExMember mem -> unsafeCoerce mem+++-- building a proxy for each type in some unknown context+data ExProxy where ExProxy :: HList Proxy ctx -> ExProxy+proxyFromLen :: Int -> ExProxy+proxyFromLen 0 = ExProxy Nil+proxyFromLen n = case proxyFromLen (n - 1) of+                   ExProxy proxy -> ExProxy (proxy :> Proxy)++-- -- unsafely building a proxy for each type in ctx from the length n+-- -- of ctx; this is only safe when we know the length of ctx = n+-- unsafeProxyFromLen :: Int -> MapC Proxy ctx+-- unsafeProxyFromLen n = case proxyFromLen n of+--                          ExProxy proxy -> unsafeCoerce proxy++-- -- unsafely convert a list of Ints, used to represent names, to+-- -- names of certain, given types; note that the first name in the+-- -- list becomes the last name in the output, with the same reversal+-- -- used in the Mb representation (see, e.g., mbCombine)+-- unsafeNamesFromInts :: [Int] -> MapC Name ctx+-- unsafeNamesFromInts [] = unsafeCoerce Nil+-- unsafeNamesFromInts (x:xs) =+--     unsafeCoerce $ unsafeNamesFromInts xs :> MkName x++-------------------------------------------------------------------------------+-- encapsulated impurity+-------------------------------------------------------------------------------++-- README: we *cannot* inline counter, because we want all uses+-- of counter to be the same IORef+counter :: IORef Int+{-# NOINLINE counter #-}+counter = unsafePerformIO (newIORef 0)++-- README: fresh_name takes a dummy argument that is used in a dummy+-- way to avoid let-floating its body (and thus getting a fresh name+-- exactly once)+-- README: it *is* ok to inline fresh_name because we don't care in+-- what order fresh names are created+fresh_name :: a -> Int+fresh_name a = unsafePerformIO $ do +    dummyRef <- newIORef a+    x <- readIORef counter+    writeIORef counter (x+1)+    return x++-- -- make one fresh name for each name in a given input list+-- fresh_names :: MapC Name ctx -> MapC Name ctx+-- fresh_names Nil = Nil+-- fresh_names (names :> n) = fresh_names names :> MkName (fresh_name n)
+ Data/Binding/Hobbits/Internal/Utilities.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE Rank2Types #-}++module Data.Binding.Hobbits.Internal.Utilities where++import qualified Data.Generics as SYB++++everywhereButM :: Monad m =>+  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m+everywhereButM q f x+  | q x       = return x+  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
− Data/Binding/Hobbits/InternalUtilities.hs 
@@ -1,13 +0,0 @@-{-# LANGUAGE Rank2Types #-}--module Data.Binding.Hobbits.InternalUtilities where--import qualified Data.Generics as SYB----everywhereButM :: Monad m =>-  SYB.GenericQ Bool -> SYB.GenericM m -> SYB.GenericM m-everywhereButM q f x-  | q x       = return x-  | otherwise = (SYB.gmapM (everywhereButM q f) x) >>= f
Data/Binding/Hobbits/Liftable.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, OverlappingInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}  -- | -- Module      : Data.Binding.Hobbits.Mb@@ -18,27 +18,41 @@  module Data.Binding.Hobbits.Liftable where -import Data.Type.List.Proof.Member-import Data.Binding.Hobbits.Mb+import Data.Type.HList+import Data.Binding.Hobbits.Internal.Mb import Data.Binding.Hobbits.QQ+import Data.Binding.Hobbits.Closed+import Data.Binding.Hobbits.NuMatching   {-|   The class @Liftable a@ gives a \"lifting function\" for a, which can   take any data of type @a@ out of a multi-binding of type @'Mb' ctx a@. -}-class Liftable a where+class NuMatching a => Liftable a where     mbLift :: Mb ctx a -> a +-------------------------------------------------------------------------------+-- Lifting instances that must be defined inside the library abstraction boundary+-------------------------------------------------------------------------------++instance Liftable Char where+    mbLift (ensureFreshPair -> (_, c)) = c+ instance Liftable Int where-    mbLift = mbLiftInt+    mbLift (ensureFreshPair -> (_, i)) = i  instance Liftable Integer where-    mbLift = mbLiftInteger+    mbLift (ensureFreshPair -> (_, i)) = i -instance Liftable Char where-    mbLift = mbLiftChar+instance Liftable (Closed a) where+    mbLift (ensureFreshPair -> (_, c)) = c ++-------------------------------------------------------------------------------+-- Lifting instances and related functions that could be defined outside the library+-------------------------------------------------------------------------------+ -- README: this requires overlapping instances, because it clashes -- with Liftable2, but this instance is better because it does not -- require c nor a to be liftable@@ -46,6 +60,27 @@     mbLift [nuP| Member_Base |] = Member_Base     mbLift [nuP| Member_Step m |] = Member_Step (mbLift m) +-- | Lift a list (but not its elements) out of a multi-binding+mbList :: NuMatching a => Mb c [a] -> [Mb c a]+mbList [nuP| [] |] = []+mbList [nuP| x : xs |] = x : mbList xs+++-------------------------------------------------------------------------------+-- Liftable1 and Liftable2+-------------------------------------------------------------------------------++instance Liftable a => Liftable [a] where+    mbLift [nuP| [] |] = []+    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)++instance (Liftable a, Liftable b) => Liftable (a,b) where+    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)++-- README: these lead to overlapping instances...++{-+ {-|   The class @Liftable1 f@ gives a lifting function for each type @f a@   when @a@ itself is @Liftable@.@@ -73,7 +108,4 @@ instance (Liftable2 f, Liftable a) => Liftable1 (f a) where     mbLift1 = mbLift2 --- | Lift a list (but not its elements) out of a multi-binding-mbList :: Mb c [a] -> [Mb c a]-mbList [nuP| [] |] = []-mbList [nuP| x : xs |] = x : mbList xs+-}
Data/Binding/Hobbits/Mb.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances #-}+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns #-}  -- | -- Module      : Data.Binding.Hobbits.Mb@@ -21,129 +21,66 @@   Binding(),   -- hides Binding implementation   Mb(),        -- hides MultiBind implementation   -- * Multi-binding constructors-  nu, emptyMb, nuMulti,-  -- * Operations on multi-bindings-  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, --mbRearrange,+  nu, nuMulti, nus, emptyMb,   -- * Queries on names-  cmpName, mbCmpName, mbNameBoundP,-  -- * Special-purpose functions for lifting primitives out of bindings-  mbLiftChar, mbLiftInt, mbLiftInteger,-  -- * Synonyms-  nus+  cmpName, mbNameBoundP, mbCmpName,+  -- * Operations on multi-bindings+  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbApply,+  -- * Eliminators for multi-bindings+  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1 ) where -import Data.Type.List-import Data.Type.List.Map-import qualified Data.Type.List.Proof.Member as Mem---import qualified Data.Type.List.Proof.Append as App-import Data.Binding.Hobbits.Internal---import qualified Data.Binding.Hobbits.Internal as I+import Control.Applicative+import Control.Monad.Identity -import Data.List (intersperse)-import Data.Functor.Constant+import Data.Type.Equality ((:~:)(..))+import Data.Proxy (Proxy(..))  import Unsafe.Coerce (unsafeCoerce) +import Data.Type.HList++import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Internal.Mb+--import qualified Data.Binding.Hobbits.Internal as I+ ---------------------------------------------------------------------------------- bindings+-- creating bindings -------------------------------------------------------------------------------  -- | A @Binding@ is simply a multi-binding that binds one name type Binding a = Mb (Nil :> a) -instance Show (Name a) where-  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'--instance Show (MapC Name c) where-    show mapc = "[" ++ (concat $ intersperse "," $ mapCToList $-                        mapC (Constant . show) mapc) ++ "]"- -- note: we reverse l to show the inner-most bindings last instance Show a => Show (Mb c a) where-  showsPrec p (MkMb names b) = showParen (p > 10) $+  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $     showChar '#' . shows names . showChar '.' . shows b --- README: we pass f to fresh_name to avoid let-floating the results--- of fresh_name (which would always give the same name for each nu)--- README: is *is* ok to do CSE on multiple copies of nu, because--- the programmer cannot tell if two distinct (non-nested) nus get the--- same fresh integer, and two nus that look the same to the CSE engine--- cannot be nested--- README: it *is* ok to inline nu because we don't care in--- what order fresh names are created {-|   @nu f@ creates a binding which binds a fresh name @n@ and whose   body is the result of @f n@. -} nu :: (Name a -> b) -> Binding a b-nu f = let n = fresh_name f in n `seq` MkMb (Nil :> MkName n) (f (MkName n))---- README: inner-most bindings come FIRST--- | Combines a binding inside another binding into a single binding.-mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b-mbCombine (MkMb l1 (MkMb l2 b)) = MkMb (append l1 l2) b--{-|-  Separates a binding into two nested bindings. The first argument, of-  type @'Append' c1 c2 c@, is a \"phantom\" argument to indicate how-  the context @c@ should be split.--}-mbSeparate :: Append c1 c2 c -> Mb c a -> Mb c1 (Mb c2 a)-mbSeparate app (MkMb l a) = MkMb d (MkMb t a) where-  (d, t) = split app l---- | Returns a proxy object that enumerates all the types in ctx.-mbToProxy :: Mb ctx a -> MapC Proxy ctx-mbToProxy (MkMb l _) = mapC (\_ -> Proxy) l--{- README: this is unsafe, because the two bindings could share names-{- |-  Take a multi-binding inside another multi-binding and move the-  outer binding inside the ineer one.--}-mbRearrange :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)-mbRearrange (MkMb l1 (MkMb l2 a)) = MkMb l2 (MkMb l1 a)--}---- | Creates an empty binding that binds 0 names.-emptyMb :: a -> Mb Nil a-emptyMb t = MkMb Nil t+nu f = MkMbFun (Nil :> Proxy) (\(Nil :> n) -> f n)  {-|   The expression @nuMulti p f@ creates a multi-binding of zero or more   names, one for each element of the vector @p@. The bound names are   passed the names to @f@, which returns the body of the-  multi-binding.  The argument @p@, of type @'Mb' f ctx@, acts as a+  multi-binding.  The argument @p@, of type @'HList' f ctx@, acts as a   \"phantom\" argument, used to reify the list of types @ctx@ at the   term level; thus it is unimportant what the type function @f@ is. -}-nuMulti :: MapC f ctx -> (MapC Name ctx -> b) -> Mb ctx b-nuMulti Nil f = emptyMb $ f Nil-nuMulti (proxies :> proxy) f =-    mbCombine $ nuMulti proxies $ \names -> nu $ \n -> f (names :> n)+nuMulti :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b+nuMulti proxies f = MkMbFun (mapHList (const Proxy) proxies) f -{-|-  Eliminates an empty binding, returning its body. Note that-  @elimEmptyMb@ is the inverse of @emptyMb@.--}-elimEmptyMb :: Mb Nil a -> a-elimEmptyMb (MkMb Nil t) = t---elimEmptyMb _ = error "Should not happen! (elimEmptyMb)"+-- | @nus = nuMulti@+nus x = nuMulti x -{-|-  @cmpName n m@ compares names @n@ and @m@ of types @Name a@ and @Name b@,-  respectively. When they are equal, @Some e@ is returned for @e@ a proof-  of type @a :=: b@ that their types are equal. Otherwise, @None@ is returned. -  For example:--> nu $ \n -> nu $ \m -> cmpName n n   ==   nu $ \n -> nu $ \m -> Some Refl-> nu $ \n -> nu $ \m -> cmpName n m   ==   nu $ \n -> nu $ \m -> None--}-cmpName :: Name a -> Name b -> Maybe (a :=: b)-cmpName (MkName n1) (MkName n2)-  | n1 == n2 = Just $ unsafeCoerce Refl-  | otherwise = Nothing+-------------------------------------------------------------------------------+-- Queries on Names+-------------------------------------------------------------------------------  {-|   Checks if a name is bound in a multi-binding, returning @Left mem@@@ -157,8 +94,8 @@ > nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n -} mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)-mbNameBoundP (MkMb names n) = helper names n where-    helper :: MapC Name c -> Name a -> Either (Member c a) (Name a)+mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where+    helper :: HList Name c -> Name a -> Either (Member c a) (Name a)     helper Nil n = Right n     helper (names :> (MkName i)) (MkName j) | i == j = unsafeCoerce $ Left Member_Base     helper (names :> _) n = case helper names n of@@ -180,23 +117,176 @@   @Some Refl@ is returned when the names are equal and @Nothing@ is   returned when they are not. -}-mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :=: b)+mbCmpName :: Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b) mbCmpName b1 b2 = case (mbNameBoundP b1, mbNameBoundP b2) of-  (Left mem1, Left mem2) -> Mem.same mem1 mem2+  (Left mem1, Left mem2) -> membersEq mem1 mem2   (Right n1, Right n2) -> cmpName n1 n2   _ -> Nothing --- | Lifts a @Char@ out of a multi-binding-mbLiftChar :: Mb c Char -> Char-mbLiftChar (MkMb _ c) = c --- | Lifts an @Int@ out of a multi-binding-mbLiftInt :: Mb c Int -> Int-mbLiftInt (MkMb _ c) = c+-------------------------------------------------------------------------------+-- Operations on multi-bindings+------------------------------------------------------------------------------- --- | Lifts an @Integer@ out of a multi-binding-mbLiftInteger :: Mb c Integer -> Integer-mbLiftInteger (MkMb _ c) = c+-- | Creates an empty binding that binds 0 names.+emptyMb :: a -> Mb Nil a+emptyMb body = MkMbFun Nil (\_ -> body) --- | @nus = nuMulti@-nus x = nuMulti x+{-|+  Eliminates an empty binding, returning its body. Note that+  @elimEmptyMb@ is the inverse of @emptyMb@.+-}+elimEmptyMb :: Mb Nil a -> a+elimEmptyMb (ensureFreshPair -> (_, body)) = body+++-- Extract the proxy objects from an Mb inside of a fresh function+freshFunctionProxies :: HList Proxy ctx1 -> (HList Name ctx1 -> Mb ctx2 a) ->+                        HList Proxy ctx2+freshFunctionProxies proxies1 f =+    case f (mapHList (const $ MkName 0) proxies1) of+      MkMbFun proxies2 _ -> proxies2+      MkMbPair _ ns _ -> mapHList (const Proxy) ns+++-- README: inner-most bindings come FIRST+-- | Combines a binding inside another binding into a single binding.+mbCombine :: Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b+mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) = MkMbPair tRepr2 (appendHList l1 l2) b+mbCombine (ensureFreshFun -> (proxies1, f1)) =+    -- README: we pass in Names with integer value 0 here in order to+    -- get out the proxies for the inner-most bindings; this is "safe"+    -- because these proxies should never depend on the names+    -- themselves+    let proxies2 = freshFunctionProxies proxies1 f1 in+    MkMbFun+    (appendHList proxies1 proxies2)+    (\ns ->+         let (ns1, ns2) = splitHList Proxy proxies2 ns in+         let (_, f2) = ensureFreshFun (f1 ns1) in+         f2 ns2)+++{-|+  Separates a binding into two nested bindings. The first argument, of+  type @'HList' any c2@, is a \"phantom\" argument to indicate how+  the context @c@ should be split.+-}+mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a ->+              Mb ctx1 (Mb ctx2 a)+mbSeparate c2 (MkMbPair tRepr ns a) =+    MkMbPair (MbTypeReprMb tRepr) ns1 (MkMbPair tRepr ns2 a) where+        (ns1, ns2) = splitHList Proxy c2 ns+mbSeparate c2 (MkMbFun proxies f) =+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendHList ns1 ns2)))+        where+          (proxies1, proxies2) = splitHList Proxy c2 proxies+++-- | Returns a proxy object that enumerates all the types in ctx.+mbToProxy :: Mb ctx a -> HList Proxy ctx+mbToProxy (MkMbFun proxies _) = proxies+mbToProxy (MkMbPair _ ns _) = mapHList (\_ -> Proxy) ns+++{-|+  Take a multi-binding inside another multi-binding and move the+  outer binding inside the ineer one.+-}+mbSwap :: Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)+mbSwap (ensureFreshFun -> (proxies1, f1)) =+    let proxies2 = freshFunctionProxies proxies1 f1 in+    MkMbFun proxies2+      (\ns2 ->+         MkMbFun proxies1+         (\ns1 ->+            snd (ensureFreshFun (f1 ns1)) ns2))++{-|+  Applies a function in a multi-binding to an argument in a+  multi-binding that binds the same number and types of names.+-}+mbApply :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b+mbApply (ensureFreshFun -> (proxies, f_fun)) (ensureFreshFun -> (_, f_arg)) =+  MkMbFun proxies (\ns -> f_fun ns $ f_arg ns)+++-------------------------------------------------------------------------------+-- Functor and Applicative instances+-------------------------------------------------------------------------------++instance Functor (Mb ctx) where+    fmap f mbArg =+        mbApply (nuMulti (mbToProxy mbArg) (\_ -> f)) mbArg++instance TypeCtx ctx => Applicative (Mb ctx) where+    pure x = nuMulti typeCtxProxies (const x)+    (<*>) = mbApply+++-------------------------------------------------------------------------------+-- Eliminators for multi-bindings+-------------------------------------------------------------------------------++-- FIXME: add more examples!!+{-|+  The expression @nuWithElimMulti args f@ takes a sequence @args@ of+  zero or more multi-bindings, each of type @Mb ctx ai@ for the same+  type context @ctx@ of bound names, and a function @f@ and does the+  following:++  * Creates a multi-binding that binds names @n1,...,nn@, one name for+    each type in @ctx@;++  * Substitutes the names @n1,...,nn@ for the names bound by each+    argument in the @args@ sequence, yielding the bodies of the @args@+    (using the new name @n@); and then++  * Passes the sequence @n1,...,nn@ along with the result of+    substituting into @args@ to the function @f@, which then returns+    the value for the newly created binding.++  Note that the types in @args@ must each have a @NuMatching@ instance;+  this is represented with the @NuMatchingList@ type class.++  Here are some examples:++> (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b+> (<*>) f a =+>     nuWithElimMulti ('Nil' :> f :> a)+>                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')+-}+nuMultiWithElim :: TypeCtx ctx =>+                   (HList Name ctx -> HList Identity args -> b) ->+                   HList (Mb ctx) args -> Mb ctx b+nuMultiWithElim f args =+  MkMbFun typeCtxProxies+          (\ns -> f ns $ mapHList (\arg -> Identity $ snd (ensureFreshFun arg) ns) args)+++{-|+  Similar to 'nuMultiWithElim' but binds only one name.+-}+nuWithElim :: (Name a -> HList Identity args -> b) ->+              HList (Mb (Nil :> a)) args ->+              Binding a b+nuWithElim f args =+    nuMultiWithElim (\(Nil :> n) -> f n) args+++{-|+  Similar to 'nuMultiWithElim' but takes only one argument+-}+nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg ->+                    Mb ctx b+nuMultiWithElim1 f arg =+    nuMultiWithElim (\names (Nil :> Identity arg) -> f names arg) (Nil :> arg)+++{-|+  Similar to 'nuMultiWithElim' but takes only one argument that binds+  a single name.+-}+nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b+nuWithElim1 f arg =+  nuWithElim (\n (Nil :> Identity arg) -> f n arg) (Nil :> arg)
− Data/Binding/Hobbits/NuElim.hs 
@@ -1,585 +0,0 @@-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}--{-|--  This module defines the NuElim typeclass, which allows eliminations-  of (multi-) bindings. The high-level idea is that, when a fresh name-  is created with 'nu', the fresh name can also be substituted for the-  bound name in a binding. See the documentation for 'nuWithElim1' and-  'nuWithElimMulti' for details.--}--module Data.Binding.Hobbits.NuElim (-  mbApply, mbMapAndSwap, mbRearrange,-  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1,-  NuElim(..), mkNuElimData, NuElimList(..), NuElim1(..),-  NuElimProof()-) where----import Data.Data-import Data.Binding.Hobbits.Internal---import Data.Binding.Hobbits.Context-import Data.Binding.Hobbits.Mb-import Data.Type.List-import Data.Type.List.Map-import Language.Haskell.TH hiding (Name)-import qualified Language.Haskell.TH as TH---import Unsafe.Coerce (unsafeCoerce)-import Control.Monad.State-import Control.Monad.Identity---- "proofs" that type a is an allowed type for nu-elimination; i.e.,--- that the multi-binding of an Mb ctx a can be eliminated by nuWithElim-data NuElimProof a where-    NuElimName :: NuElimProof (Name a)-    NuElimMb :: NuElimProof a -> NuElimProof (Mb ctx a)-    NuElimFun :: NuElimProof a -> NuElimProof b -> NuElimProof (a -> b)-    NuElimData :: NuElimDataProof a -> NuElimProof a--data NuElimDataProof a =-    NuElimDataProof (forall ctx. MapC Name ctx -> MapC Name ctx -> a -> a)----- map the names in one MapC to the corresponding ones in another-mapNamesPf :: NuElimProof a -> MapC Name ctx -> MapC Name ctx -> a -> a-mapNamesPf NuElimName Nil Nil n = n-mapNamesPf NuElimName (names :> m) (names' :> m') n =-    case cmpName m n of-      Just Refl -> m'-      Nothing -> mapNamesPf NuElimName names names' n-mapNamesPf NuElimName _ _ _ = error "Should not be possible! (in mapNamesPf)"-mapNamesPf (NuElimMb nuElim) names1 names2 (MkMb ns b) =-    let names2' = fresh_names ns in-    MkMb names2' $ mapNamesPf nuElim (names1 `append` ns) (names2 `append` names2') b-mapNamesPf (NuElimFun nuElimIn nuElimOut) names names' f =-    (mapNamesPf nuElimOut names names') . f . (mapNamesPf nuElimIn names' names)-mapNamesPf (NuElimData (NuElimDataProof mapFun)) names names' x =-    mapFun names names' x----- just like mapNamesPf, except use the NuElim class-mapNames :: NuElim a => MapC Name ctx -> MapC Name ctx -> a -> a-mapNames = mapNamesPf nuElimProof---{-|-  Instances of the @NuElim a@ class allow the type @a@ to be used with-  'nuWithElimMulti' and 'nuWithElim1'. The structure of this class is-  mostly hidden from the user; see 'mkNuElimData' to see how to create-  instances of the @NuElim@ class.--}-class NuElim a where-    nuElimProof :: NuElimProof a--instance NuElim (Name a) where-    nuElimProof = NuElimName--instance (NuElim a, NuElim b) => NuElim (a -> b) where-    nuElimProof = NuElimFun nuElimProof nuElimProof--{--instance NuElim a => NuElim (Mb Nil a) where-    nuElimProof = NuElimMbNil nuElimProof--instance NuElim (Mb ctx a) => NuElim (Mb (ctx :> c) a) where-    nuElimProof = NuElimMbCons nuElimProof--}--instance NuElim a => NuElim (Mb ctx a) where-    nuElimProof = NuElimMb nuElimProof--instance NuElim Int where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))--instance NuElim Char where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> id))--instance (NuElim a, NuElim b) => NuElim (a,b) where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))--instance (NuElim a, NuElim b, NuElim c) => NuElim (a,b,c) where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))--instance (NuElim a, NuElim b, NuElim c, NuElim d) => NuElim (a,b,c,d) where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))--instance (NuElim a, NuElim b) => NuElim (Either a b) where-    nuElimProof = NuElimData-                  (NuElimDataProof-                   $ (\c1 c2 x -> case x of-                                    Left l -> Left (mapNames c1 c2 l)-                                    Right r -> Right (mapNames c1 c2 r)))--instance NuElim a => NuElim [a] where-    nuElimProof = NuElimData (NuElimDataProof $ (\c1 c2 -> map (mapNames c1 c2)))---{--type family NuElimListProof args-type instance NuElimListProof Nil = ()-type instance NuElimListProof (args :> arg) = (NuElimListProof args, NuElimProof arg)---- the NuElimList class, for saying that NuElim holds for a context of types-class NuElimList args where-    nuElimListProof :: NuElimListProof args--instance NuElimList Nil where-    nuElimListProof = ()--instance (NuElimList args, NuElim a) => NuElimList (args :> a) where-    nuElimListProof = (nuElimListProof, nuElimProof)--}--data NuElimObj a = NuElim a => NuElimObj ()---- the NuElimList class, for saying that NuElim holds for a context of types-class NuElimList args where-    nuElimListProof :: MapC NuElimObj args--instance NuElimList Nil where-    nuElimListProof = Nil--instance (NuElimList args, NuElim a) => NuElimList (args :> a) where-    nuElimListProof = nuElimListProof :> NuElimObj ()---class NuElim1 f where-    nuElimProof1 :: NuElim a => NuElimObj (f a)---- README: deriving NuElim from NuElim1 leads to overlapping instances--- for, e.g., Name a-{--instance (NuElim1 f, NuElim a) => NuElim (f a) where-    nuElimProof = nuElimProof1 nuElimProof--}--instance (NuElim1 f, NuElimList ctx) => NuElim (MapC f ctx) where-    nuElimProof = NuElimData $ NuElimDataProof $ helper nuElimListProof where-        helper :: NuElim1 f =>-                  MapC NuElimObj args -> MapC Name ctx1 -> MapC Name ctx1 ->-                  MapC f args -> MapC f args-        helper Nil c1 c2 Nil = Nil-        helper (proofs :> NuElimObj ()) c1 c2 (elems :> (elem :: f a)) =-            case nuElimProof1 :: NuElimObj (f a) of-              NuElimObj () ->-                  (helper proofs c1 c2 elems) :>-                  mapNames c1 c2 elem---- filter out names from a MapC Name-{--data FilterRes where-    FilterRes :: (MapC Name ctx, MapC Name ctx) -> FilterRes--filterName :: Name a -> MapC Name ctx -> MapC Name ctx -> FilterRes-filterName n Nil Nil = Nil-filterName --filterNames :: [Int] -> MapC Name ctx -> MapC Name ctx -> FilterRes-filterNames Nil names1 names2 = FilterRes names1 names2-Nil Nil = FilterRes Nil-filterNames (names1 :> n1)--}--{-|-  Applies a function in a multi-binding to an argument in a-  multi-binding that binds the same number and types of names.--}-mbApply :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b-mbApply (MkMb names f) (MkMb names' a) =-    let names'' = fresh_names names in-    MkMb names'' $ (mapNames names names'' f) (mapNames names' names'' a)--mbMapAndSwap :: NuElim a => (Mb ctx1 a -> b) -> Mb ctx1 (Mb ctx2 a) -> Mb ctx2 b-mbMapAndSwap = undefined-{--mbMapAndSwap (MkMb names f) (MkMb names' a) =-    MkMb names $ f $ mapNames names' names a--}--{-|-  Take a multi-binding inside another multi-binding and move the-  outer binding inside the inner one.--  NOTE: This is not yet implemented.--}-mbRearrange :: NuElim a => Mb ctx1 (Mb ctx2 a) -> Mb ctx2 (Mb ctx1 a)-mbRearrange = mbMapAndSwap id------ FIXME: add more examples!!-{-|-  The expression @nuWithElimMulti args f@ takes a sequence @args@ of-  zero or more multi-bindings, each of type @Mb ctx ai@ for the same-  type context @ctx@ of bound names, and a function @f@ and does the-  following:--  * Creates a multi-binding that binds names @n1,...,nn@, one name for-    each type in @ctx@;--  * Substitutes the names @n1,...,nn@ for the names bound by each-    argument in the @args@ sequence, yielding the bodies of the @args@-    (using the new name @n@); and then--  * Passes the sequence @n1,...,nn@ along with the result of-    substituting into @args@ to the function @f@, which then returns-    the value for the newly created binding.--  Note that the types in @args@ must each have a @NuElim@ instance;-  this is represented with the @NuElimList@ type class.--  Here are some examples:--> commuteFun :: (NuElim a, NuElim b) => Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b-> commuteFun f a =->     nuWithElimMulti ('mbToProxy' f) ('Nil' :> f :> a)->                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')--}-nuMultiWithElim :: (NuElimList args, NuElim b) =>-                   MapC f ctx -> MapC (Mb ctx) args ->-                   (MapC Name ctx -> MapC Identity args -> b) -> Mb ctx b-nuMultiWithElim nameProxies args f =-    mbMultiApply (nuMulti nameProxies-                  (\names -> (mapCToAddArrows args (f names)))) args nuElimListProof where-        mapCToAddArrows :: MapC f args -> (MapC Identity args -> b) ->-                           AddArrows args b-        mapCToAddArrows Nil f = f Nil-        mapCToAddArrows (args :> _) f = mapCToAddArrows args (\args' x -> f (args' :> Identity x))-        mbMultiApply :: NuElim b => Mb ctx (AddArrows args b) ->-                        MapC (Mb ctx) args -> MapC NuElimObj args -> Mb ctx b-        mbMultiApply mbF Nil Nil = mbF-        mbMultiApply mbF (args :> arg) (proofs :> NuElimObj ()) =-            mbApply (mbMultiApply mbF args proofs) arg---type family AddArrows ctx a-type instance AddArrows Nil a = a-type instance AddArrows (ctx :> b) a = AddArrows ctx (b -> a)---- README: old implementation-{--nuMultiWithElim nameProxies args f =-    nuMulti nameProxies $ \names -> f names (mapArgs nuElimListProof args names)-    where-      mapArgs :: MapC NuElimProof args -> MapC (Mb ctx) args ->-                 MapC Name ctx -> MapC Identity args-      mapArgs Nil Nil _ = Nil-      mapArgs (proofs :> proof) (args :> arg) names =-          mapArgs proofs args names :>-                      (Identity $ mapNamesSubst proof names arg)-      mapArgs _ _ _ = error "Should not be possible! (in mapArgs)"--      mapNamesSubst :: NuElimProof arg -> MapC Name ctx -> Mb ctx arg -> arg-      mapNamesSubst proof names (MkMb namesOld arg) =-          mapNamesPf proof namesOld names arg--}--{-|-  Similar to 'nuMultiWithElim' but binds only one name.--}-nuWithElim :: (NuElimList args, NuElim b) => MapC (Mb (Nil :> a)) args ->-              (Name a -> MapC Identity args -> b) -> Binding a b-nuWithElim args f =-    nuMultiWithElim (Nil :> Proxy) args (\(Nil :> n) -> f n)---{-|-  Similar to 'nuMultiWithElim' but takes only one argument--}-nuMultiWithElim1 :: (NuElim arg, NuElim b) => MapC f ctx -> Mb ctx arg ->-                    (MapC Name ctx -> arg -> b) -> Mb ctx b-nuMultiWithElim1 nameProxies arg f =-    nuMultiWithElim nameProxies (Nil :> arg)-                    (\names (Nil :> Identity arg) -> f names arg)---{-|-  Similar to 'nuMultiWithElim' but takes only one argument that binds-  a single name.--}-nuWithElim1 :: (NuElim arg, NuElim b) => Binding a arg ->-               (Name a -> arg -> b) -> Binding a b-nuWithElim1 (MkMb namesOld arg) f =-    nu $ \n -> f n (mapNames namesOld (Nil :> n) arg)-{--nuWithElim1 (MkMb _ arg) f =-    error "Internal error in nuWithElim1"--}----- now we define some TH to create NuElimDataProofs--natsFrom i = i : natsFrom (i+1)--fst3 :: (a,b,c) -> a-fst3 (x,_,_) = x--snd3 :: (a,b,c) -> b-snd3 (_,y,_) = y--thd3 :: (a,b,c) -> c-thd3 (_,_,z) = z---type Names = (TH.Name, TH.Name, TH.Name, TH.Name)--mapNamesType a = [t| forall ctx. MapC Name ctx -> MapC Name ctx -> $a -> $a |]--{-|-  Template Haskell function for creating NuElim instances for (G)ADTs.-  Typical usage is to include the following line in the source file for-  (G)ADT @T@ (here assumed to have two type arguments):--> $(mkNuElimData [t| forall a b . T a b |])--  The 'mkNuElimData' call here will create an instance declaration for-  @'NuElim' (T a b)@. It is also possible to include a context in the-  forall type; for example, if we define the 'ID' data type as follows:--> data ID a = ID a--  then we can create a 'NuElim' instance for it like this:--> $( mkNuElimData [t| NuElim a => ID a |])--  Note that, when a context is included, the Haskell parser will add-  the @forall a@ for you.--}-mkNuElimData :: Q Type -> Q [Dec]-mkNuElimData tQ =-    do t <- tQ-       (cxt, cType, tName, constrs, tyvars) <- getNuElimInfoTop t-       fName <- newName "f"-       x1Name <- newName "x1"-       x2Name <- newName "x2"-       clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs-       mapNamesT <- mapNamesType (return cType)-       return [InstanceD-               cxt (AppT (ConT ''NuElim) cType)-               [ValD (VarP 'nuElimProof)-                (NormalB-                 $ AppE (ConE 'NuElimData)-                   $ AppE (ConE 'NuElimDataProof)-                         $ LetE [SigD fName-                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,-                                 FunD fName clauses]-                               (VarE fName)) []]]--       {--       return (LetE-               [SigD fName-                     (ForallT tyvars reqCxt-                     $ foldl AppT ArrowT-                           [foldl AppT (ConT conName)-                                      (map tyVarToType tyvars)]),-                FunD fname clauses]-               (VarE fname))-        -}-    where-      -- extract the name from a TyVarBndr-      tyBndrToName (PlainTV n) = n-      tyBndrToName (KindedTV n _) = n--      -- fail for getNuElimInfo-      getNuElimInfoFail t extraMsg =-          fail ("mkNuElimData: " ++ show t-                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)--      -- get info for conName (top-level call)-      getNuElimInfoTop t = getNuElimInfo [] [] t t--      -- get info for conName-      getNuElimInfo ctx tyvars topT (ConT tName) =-          do info <- reify tName-             case info of-               TyConI (DataD _ _ tyvarsReq constrs _) ->-                   success tyvarsReq constrs-               TyConI (NewtypeD _ _ tyvarsReq constr _) ->-                   success tyvarsReq [constr]-               _ -> getNuElimInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))-          where-            success tyvarsReq constrs =-                let tyvarsRet = if tyvars == [] && ctx == []-                                then map tyBndrToName tyvarsReq-                                else tyvars in-                return (ctx,-                        foldl AppT (ConT tName) (map VarT tyvars),-                        tName, constrs, tyvarsRet)--      getNuElimInfo ctx tyvars topT (AppT f (VarT argName)) =-          if elem argName tyvars then-              getNuElimInfoFail topT ""-          else-              getNuElimInfo ctx (argName:tyvars) topT f--      getNuElimInfo ctx tyvars topT (ForallT _ ctx' t) =-          getNuElimInfo (ctx ++ ctx') tyvars topT t--      getNuElimInfo ctx tyvars topT t = getNuElimInfoFail topT ""--      -- get the name from a data type-      getTCtor t = getTCtorHelper t t []-      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)-      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =-          getTCtorHelper t1 topT (tyvars ++ [var])-      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars-      getTCtorHelper _ _ _ = Nothing--      -- get a list of Clauses, one for each constructor in constrs-      getClauses :: Names -> [Con] -> Q [Clause]-      getClauses names constrs = mapM (getClause names) constrs--      getClause :: Names -> Con -> Q Clause-      getClause names (NormalC cName cTypes) =-          getClauseHelper names (map snd cTypes)-                          (natsFrom 0)-                          (\l -> ConP cName (map (VarP . fst3) l))-                          (\l -> foldl AppE (ConE cName) (map fst3 l))--      getClause names (RecC cName cVarTypes) =-          getClauseHelper names (map thd3 cVarTypes)-                         (map fst3 cVarTypes)-                         (\l -> RecP cName-                                (map (\(var,_,field) -> (field, VarP var)) l))-                         (\l -> RecConE cName-                                (map (\(exp,_,field) -> (field, exp)) l))--      getClause names (InfixC cType1 cName cType2) =-          undefined -- FIXME--      getClause names (ForallC _ _ con) =  getClause names con--      getClauseHelper :: Names -> [Type] -> [a] ->-                         ([(TH.Name,Type,a)] -> Pat) ->-                         ([(Exp,Type,a)] -> Exp) ->-                         Q Clause-      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =-          do varNames <- mapM (newName . ("x" ++) . show . fst)-                         $ zip (natsFrom 0) cTypes-             let varsTypesData = zip3 varNames cTypes cData-             let expsTypesData = map (mkExpTypeData names) varsTypesData-             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]-                        (NormalB $ eFun expsTypesData) []--      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)-      mkExpTypeData (tName, fName, x1Name, x2Name)-                    (varName, getTCtor -> Just (t, tName', _), cData)-          | tName == tName' =-              -- the type of the arg is the same as the (G)ADT we are-              -- recursing over; apply the recursive function-              (foldl AppE (VarE fName)-                         [(VarE x1Name), (VarE x2Name), (VarE varName)],-               t, cData)-      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =-          -- the type of the arg is not the same as the (G)ADT; call mapNames-          (foldl AppE (VarE 'mapNames)-                     [(VarE x1Name), (VarE x2Name), (VarE varName)],-           t, cData)---- FIXME: old stuff below--type CxtStateQ a = StateT Cxt Q a---- create a NuElimDataProof for a (G)ADT-mkNuElimDataProofOld :: Q TH.Name -> Q Exp-mkNuElimDataProofOld conNameQ =-    do conName <- conNameQ-       (cxt, name, tyvars, constrs) <- getNuElimInfo conName-       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []-       fname <- newName "f"-       return (LetE-               [SigD fname-                     (ForallT tyvars reqCxt-                     $ foldl AppT ArrowT-                           [foldl AppT (ConT conName)-                                      (map tyVarToType tyvars)]),-                FunD fname clauses]-               (VarE fname))-    where-      -- convert a TyVar to a Name-      tyVarToType (PlainTV n) = VarT n-      tyVarToType (KindedTV n _) = VarT n--      -- get info for conName-      getNuElimInfo conName =-          reify conName >>= \info ->-              case info of-                TyConI (DataD cxt name tyvars constrs _) ->-                    return (cxt, name, tyvars, constrs)-                _ -> fail ("mkNuElimDataProof: " ++ show conName-                           ++ " is not a (G)ADT")-      {--      -- report failure-      getNuElimInfoFail t =-          fail ("mkNuElimDataProof: " ++ show t-                ++ " is not a fully applied (G)ADT")--      getNuElimInfo (ConT conName) topT =-          reify conName >>= \info ->-              case info of-                TyConI (DataD cxt name tyvars constrs _) ->-                    return (cxt, name, tyvars, constrs)-                _ -> getNuElimInfoFail topT-      getNuElimInfo (AppT t _) topT = getNuElimInfo t topT-      getNuElimInfo (SigT t _) topT = getNuElimInfo t topT-      getNuElimInfo _ topT = getNuElimInfoFail topT-       -}--      -- get a list of Clauses, one for each constructor in constrs-      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]-      getClauses cxt name tyvars constrs =-          mapM (getClause cxt name tyvars []) constrs--      getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->-                   CxtStateQ Clause-      getClause cxt name tyvars locTyvars (NormalC cName cTypes) =-          getClauseHelper cxt name tyvars locTyvars (map snd cTypes)-                          (natsFrom 0)-                          (\l -> ConP cName (map (VarP . fst3) l))-                          (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))--      getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =-          getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)-                         (map fst3 cVarTypes)-                         (\l -> RecP cName-                                (map (\(var,_,field) -> (field, VarP var)) l))-                         (\l -> RecConE cName-                                (map (\(var,_,field) -> (field, VarE var)) l))--      getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =-          undefined -- FIXME--      getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =-          getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con--      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->-                         [Type] -> [a] ->-                         ([(TH.Name,Type,a)] -> Pat) ->-                         ([(TH.Name,Type,a)] -> Exp) ->-                         CxtStateQ Clause-      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =-          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)-                         $ zip (natsFrom 0) cTypes-             () <- ensureCxt cxt locTyvars cTypes-             let varsTypesData = zip3 varNames cTypes cData-             return $ Clause [(pFun varsTypesData)]-                        (NormalB $ eFun varsTypesData) []--      -- ensure that NuElim a holds for each type a in cTypes-      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()-      ensureCxt cxt locTyvars cTypes =-          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes--      -- FIXME: it is not possible (or, at least, not easy) to determine-      -- if NuElim a is implied from a current Cxt... so we just add-      -- everything we need to the returned Cxt, except for -      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()-      ensureCxt1 cxt locTyvars t = undefined-      {--      ensureCxt1 cxt locTyvars t = do-        curCxt = get-        let fullCxt = cxt ++ curCxt-        isOk <- isNuElim fullCxt --      isNuElim -       -}
+ Data/Binding/Hobbits/NuMatching.hs view
@@ -0,0 +1,426 @@+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}++-- |+-- Module      : Data.Binding.Hobbits.NuMatching+-- Copyright   : (c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : westbrook@kestrel.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines the typeclass @'NuMatching' a@, which allows+-- pattern-matching on the bodies of multi-bindings when their bodies+-- have type a. To ensure adequacy, the actual machinery of how this+-- works is hidden from the user, but, for any given (G)ADT @a@, the+-- user can use the Template Haskell function 'mkNuMatching' to+-- create a 'NuMatching' instance for @a@.+--+++module Data.Binding.Hobbits.NuMatching (+  NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),+  MbTypeRepr()+) where++--import Data.Typeable+import Language.Haskell.TH hiding (Name)+import qualified Language.Haskell.TH as TH+import Control.Monad.State+--import Control.Monad.Identity++import Data.Type.HList+import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Internal.Mb+import Data.Binding.Hobbits.Internal.Closed+++{-| Just like 'mapNamesPf', except uses the NuMatching class. -}+mapNames :: NuMatching a => HList Name ctx -> HList Name ctx -> a -> a+mapNames = mapNamesPf nuMatchingProof+++{-|+  Instances of the @'NuMatching' a@ class allow pattern-matching on+  multi-bindings whose bodies have type @a@, i.e., on multi-bindings+  of type @'Mb' ctx a@. The structure of this class is mostly hidden+  from the user; see 'mkNuMatching' to see how to create instances+  of the @NuMatching@ class.+-}+class NuMatching a where+    nuMatchingProof :: MbTypeRepr a++instance NuMatching (Name a) where+    nuMatchingProof = MbTypeReprName++instance NuMatching (Cl a) where+    -- no need to map free variables in a Closed object+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))++instance (NuMatching a, NuMatching b) => NuMatching (a -> b) where+    nuMatchingProof = MbTypeReprFun nuMatchingProof nuMatchingProof++instance NuMatching a => NuMatching (Mb ctx a) where+    nuMatchingProof = MbTypeReprMb nuMatchingProof++instance NuMatching Int where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))++instance NuMatching Integer where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))++instance NuMatching Char where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))++instance (NuMatching a, NuMatching b) => NuMatching (a,b) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b) -> (mapNames c1 c2 a, mapNames c1 c2 b)))++instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c)))++instance (NuMatching a, NuMatching b, NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 (a,b,c,d) -> (mapNames c1 c2 a, mapNames c1 c2 b, mapNames c1 c2 c, mapNames c1 c2 d)))++instance (NuMatching a, NuMatching b) => NuMatching (Either a b) where+    nuMatchingProof = MbTypeReprData+                  (MkMbTypeReprData+                   $ (\c1 c2 x -> case x of+                                    Left l -> Left (mapNames c1 c2 l)+                                    Right r -> Right (mapNames c1 c2 r)))++instance NuMatching a => NuMatching [a] where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> map (mapNames c1 c2)))++instance NuMatching (Member c a) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id))+++{-+type family NuMatchingListProof args+type instance NuMatchingListProof Nil = ()+type instance NuMatchingListProof (args :> arg) = (NuMatchingListProof args, MbTypeReprData arg)++-- the NuMatchingList class, for saying that NuMatching holds for a context of types+class NuMatchingList args where+    nuMatchingListProof :: NuMatchingListProof args++instance NuMatchingList Nil where+    nuMatchingListProof = ()++instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where+    nuMatchingListProof = (nuMatchingListProof, nuMatchingProof)+-}++data NuMatchingObj a = NuMatching a => NuMatchingObj ()++-- the NuMatchingList class, for saying that NuMatching holds for a context of types+class NuMatchingList args where+    nuMatchingListProof :: HList NuMatchingObj args++instance NuMatchingList Nil where+    nuMatchingListProof = Nil++instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where+    nuMatchingListProof = nuMatchingListProof :> NuMatchingObj ()+++class NuMatching1 f where+    nuMatchingProof1 :: NuMatching a => NuMatchingObj (f a)++-- README: deriving NuMatching from NuMatching1 leads to overlapping instances+-- for, e.g., Name a+{-+instance (NuMatching1 f, NuMatching a) => NuMatching (f a) where+    nuMatchingProof = nuMatchingProof1 nuMatchingProof+-}++instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (HList f ctx) where+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where+        helper :: NuMatching1 f =>+                  HList NuMatchingObj args -> HList Name ctx1 -> HList Name ctx1 ->+                  HList f args -> HList f args+        helper Nil c1 c2 Nil = Nil+        helper (proofs :> NuMatchingObj ()) c1 c2 (elems :> (elem :: f a)) =+            case nuMatchingProof1 :: NuMatchingObj (f a) of+              NuMatchingObj () ->+                  (helper proofs c1 c2 elems) :>+                  mapNames c1 c2 elem+++-- now we define some TH to create NuMatchings++natsFrom i = i : natsFrom (i+1)++fst3 :: (a,b,c) -> a+fst3 (x,_,_) = x++snd3 :: (a,b,c) -> b+snd3 (_,y,_) = y++thd3 :: (a,b,c) -> c+thd3 (_,_,z) = z+++type Names = (TH.Name, TH.Name, TH.Name, TH.Name)++mapNamesType a = [t| forall ctx. HList Name ctx -> HList Name ctx -> $a -> $a |]++{-|+  Template Haskell function for creating NuMatching instances for (G)ADTs.+  Typical usage is to include the following line in the source file for+  (G)ADT @T@ (here assumed to have two type arguments):++> $(mkNuMatching [t| forall a b . T a b |])++  The 'mkNuMatching' call here will create an instance declaration for+  @'NuMatching' (T a b)@. It is also possible to include a context in the+  forall type; for example, if we define the 'ID' data type as follows:++> data ID a = ID a++  then we can create a 'NuMatching' instance for it like this:++> $( mkNuMatching [t| NuMatching a => ID a |])++  Note that, when a context is included, the Haskell parser will add+  the @forall a@ for you.+-}+mkNuMatching :: Q Type -> Q [Dec]+mkNuMatching tQ =+    do t <- tQ+       (cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t+       fName <- newName "f"+       x1Name <- newName "x1"+       x2Name <- newName "x2"+       clauses <- mapM (getClause (tName, fName, x1Name, x2Name)) constrs+       mapNamesT <- mapNamesType (return cType)+       return [InstanceD+               cxt (AppT (ConT ''NuMatching) cType)+               [ValD (VarP 'nuMatchingProof)+                (NormalB+                 $ AppE (ConE 'MbTypeReprData)+                   $ AppE (ConE 'MkMbTypeReprData)+                         $ LetE [SigD fName+                                 $ ForallT (map PlainTV tyvars) cxt mapNamesT,+                                 FunD fName clauses]+                               (VarE fName)) []]]++       {-+       return (LetE+               [SigD fName+                     (ForallT tyvars reqCxt+                     $ foldl AppT ArrowT+                           [foldl AppT (ConT conName)+                                      (map tyVarToType tyvars)]),+                FunD fname clauses]+               (VarE fname))+        -}+    where+      -- extract the name from a TyVarBndr+      tyBndrToName (PlainTV n) = n+      tyBndrToName (KindedTV n _) = n++      -- fail for getMbTypeReprInfo+      getMbTypeReprInfoFail t extraMsg =+          fail ("mkMbTypeRepr: " ++ show t+                ++ " is not a type constructor for a (G)ADT applied to zero or more distinct type variables" ++ extraMsg)++      -- get info for conName (top-level call)+      getMbTypeReprInfoTop t = getMbTypeReprInfo [] [] t t++      -- get info for conName+      getMbTypeReprInfo ctx tyvars topT (ConT tName) =+          do info <- reify tName+             case info of+               TyConI (DataD _ _ tyvarsReq constrs _) ->+                   success tyvarsReq constrs+               TyConI (NewtypeD _ _ tyvarsReq constr _) ->+                   success tyvarsReq [constr]+               _ -> getMbTypeReprInfoFail topT (": info for " ++ (show tName) ++ " = " ++ (show info))+          where+            success tyvarsReq constrs =+                let tyvarsRet = if tyvars == [] && ctx == []+                                then map tyBndrToName tyvarsReq+                                else tyvars in+                return (ctx,+                        foldl AppT (ConT tName) (map VarT tyvars),+                        tName, constrs, tyvarsRet)++      getMbTypeReprInfo ctx tyvars topT (AppT f (VarT argName)) =+          if elem argName tyvars then+              getMbTypeReprInfoFail topT ""+          else+              getMbTypeReprInfo ctx (argName:tyvars) topT f++      getMbTypeReprInfo ctx tyvars topT (ForallT _ ctx' t) =+          getMbTypeReprInfo (ctx ++ ctx') tyvars topT t++      getMbTypeReprInfo ctx tyvars topT t = getMbTypeReprInfoFail topT ""++      -- get the name from a data type+      getTCtor t = getTCtorHelper t t []+      getTCtorHelper (ConT tName) topT tyvars = Just (topT, tName, tyvars)+      getTCtorHelper (AppT t1 (VarT var)) topT tyvars =+          getTCtorHelper t1 topT (tyvars ++ [var])+      getTCtorHelper (SigT t1 _) topT tyvars = getTCtorHelper t1 topT tyvars+      getTCtorHelper _ _ _ = Nothing++      -- get a list of Clauses, one for each constructor in constrs+      getClauses :: Names -> [Con] -> Q [Clause]+      getClauses names constrs = mapM (getClause names) constrs++      getClause :: Names -> Con -> Q Clause+      getClause names (NormalC cName cTypes) =+          getClauseHelper names (map snd cTypes)+                          (natsFrom 0)+                          (\l -> ConP cName (map (VarP . fst3) l))+                          (\l -> foldl AppE (ConE cName) (map fst3 l))++      getClause names (RecC cName cVarTypes) =+          getClauseHelper names (map thd3 cVarTypes)+                         (map fst3 cVarTypes)+                         (\l -> RecP cName+                                (map (\(var,_,field) -> (field, VarP var)) l))+                         (\l -> RecConE cName+                                (map (\(exp,_,field) -> (field, exp)) l))++      getClause names (InfixC cType1 cName cType2) =+          undefined -- FIXME++      getClause names (ForallC _ _ con) =  getClause names con++      getClauseHelper :: Names -> [Type] -> [a] ->+                         ([(TH.Name,Type,a)] -> Pat) ->+                         ([(Exp,Type,a)] -> Exp) ->+                         Q Clause+      getClauseHelper names@(tName, fName, x1Name, x2Name) cTypes cData pFun eFun =+          do varNames <- mapM (newName . ("x" ++) . show . fst)+                         $ zip (natsFrom 0) cTypes+             let varsTypesData = zip3 varNames cTypes cData+             let expsTypesData = map (mkExpTypeData names) varsTypesData+             return $ Clause [(VarP x1Name), (VarP x2Name), (pFun varsTypesData)]+                        (NormalB $ eFun expsTypesData) []++      mkExpTypeData :: Names -> (TH.Name,Type,a) -> (Exp,Type,a)+      mkExpTypeData (tName, fName, x1Name, x2Name)+                    (varName, getTCtor -> Just (t, tName', _), cData)+          | tName == tName' =+              -- the type of the arg is the same as the (G)ADT we are+              -- recursing over; apply the recursive function+              (foldl AppE (VarE fName)+                         [(VarE x1Name), (VarE x2Name), (VarE varName)],+               t, cData)+      mkExpTypeData (tName, fName, x1Name, x2Name) (varName, t, cData) =+          -- the type of the arg is not the same as the (G)ADT; call mapNames+          (foldl AppE (VarE 'mapNames)+                     [(VarE x1Name), (VarE x2Name), (VarE varName)],+           t, cData)++-- FIXME: old stuff below++type CxtStateQ a = StateT Cxt Q a++-- create a MkMbTypeReprData for a (G)ADT+mkMkMbTypeReprDataOld :: Q TH.Name -> Q Exp+mkMkMbTypeReprDataOld conNameQ =+    do conName <- conNameQ+       (cxt, name, tyvars, constrs) <- getMbTypeReprInfo conName+       (clauses, reqCxt) <- runStateT (getClauses cxt name tyvars constrs) []+       fname <- newName "f"+       return (LetE+               [SigD fname+                     (ForallT tyvars reqCxt+                     $ foldl AppT ArrowT+                           [foldl AppT (ConT conName)+                                      (map tyVarToType tyvars)]),+                FunD fname clauses]+               (VarE fname))+    where+      -- convert a TyVar to a Name+      tyVarToType (PlainTV n) = VarT n+      tyVarToType (KindedTV n _) = VarT n++      -- get info for conName+      getMbTypeReprInfo conName =+          reify conName >>= \info ->+              case info of+                TyConI (DataD cxt name tyvars constrs _) ->+                    return (cxt, name, tyvars, constrs)+                _ -> fail ("mkMkMbTypeReprData: " ++ show conName+                           ++ " is not a (G)ADT")+      {-+      -- report failure+      getMbTypeReprInfoFail t =+          fail ("mkMkMbTypeReprData: " ++ show t+                ++ " is not a fully applied (G)ADT")++      getMbTypeReprInfo (ConT conName) topT =+          reify conName >>= \info ->+              case info of+                TyConI (DataD cxt name tyvars constrs _) ->+                    return (cxt, name, tyvars, constrs)+                _ -> getMbTypeReprInfoFail topT+      getMbTypeReprInfo (AppT t _) topT = getMbTypeReprInfo t topT+      getMbTypeReprInfo (SigT t _) topT = getMbTypeReprInfo t topT+      getMbTypeReprInfo _ topT = getMbTypeReprInfoFail topT+       -}++      -- get a list of Clauses, one for each constructor in constrs+      getClauses :: Cxt -> TH.Name -> [TyVarBndr] -> [Con] -> CxtStateQ [Clause]+      getClauses cxt name tyvars constrs =+          mapM (getClause cxt name tyvars []) constrs++      getClause :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] -> Con ->+                   CxtStateQ Clause+      getClause cxt name tyvars locTyvars (NormalC cName cTypes) =+          getClauseHelper cxt name tyvars locTyvars (map snd cTypes)+                          (natsFrom 0)+                          (\l -> ConP cName (map (VarP . fst3) l))+                          (\l -> foldl AppE (ConE cName) (map (VarE . fst3) l))++      getClause cxt name tyvars locTyvars (RecC cName cVarTypes) =+          getClauseHelper cxt name tyvars locTyvars (map thd3 cVarTypes)+                         (map fst3 cVarTypes)+                         (\l -> RecP cName+                                (map (\(var,_,field) -> (field, VarP var)) l))+                         (\l -> RecConE cName+                                (map (\(var,_,field) -> (field, VarE var)) l))++      getClause cxt name tyvars locTyvars (InfixC cType1 cName cType2) =+          undefined -- FIXME++      getClause cxt name tyvars locTyvars (ForallC tyvars2 cxt2 con) =+          getClause (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) con++      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->+                         [Type] -> [a] ->+                         ([(TH.Name,Type,a)] -> Pat) ->+                         ([(TH.Name,Type,a)] -> Exp) ->+                         CxtStateQ Clause+      getClauseHelper cxt name tyvars locTyvars cTypes cData pFun eFun =+          do varNames <- mapM (lift . newName . ("x" ++) . show . fst)+                         $ zip (natsFrom 0) cTypes+             () <- ensureCxt cxt locTyvars cTypes+             let varsTypesData = zip3 varNames cTypes cData+             return $ Clause [(pFun varsTypesData)]+                        (NormalB $ eFun varsTypesData) []++      -- ensure that MbTypeRepr a holds for each type a in cTypes+      ensureCxt :: Cxt -> [TyVarBndr] -> [Type] -> CxtStateQ ()+      ensureCxt cxt locTyvars cTypes =+          foldM (const (ensureCxt1 cxt locTyvars)) () cTypes++      -- FIXME: it is not possible (or, at least, not easy) to determine+      -- if MbTypeRepr a is implied from a current Cxt... so we just add+      -- everything we need to the returned Cxt, except for +      ensureCxt1 :: Cxt -> [TyVarBndr] -> Type -> CxtStateQ ()+      ensureCxt1 cxt locTyvars t = undefined+      {-+      ensureCxt1 cxt locTyvars t = do+        curCxt = get+        let fullCxt = cxt ++ curCxt+        isOk <- isMbTypeRepr fullCxt ++      isMbTypeRepr +       -}
Data/Binding/Hobbits/QQ.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}  -- | -- Module      : Data.Binding.Hobbits.QQ@@ -25,10 +25,6 @@  module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where -import qualified Data.Binding.Hobbits.InternalUtilities as IU-import Data.Binding.Hobbits.Internal (Mb(..), Cl(..))-import Data.Binding.Hobbits.PatternParser (parsePattern)- import Language.Haskell.TH.Syntax as TH import Language.Haskell.TH.Ppr as TH import Language.Haskell.TH.Quote@@ -37,60 +33,79 @@ import Control.Monad.Writer (runWriterT, tell) import Data.Monoid (Any(..)) -+import qualified Data.Binding.Hobbits.Internal.Utilities as IU+import Data.Binding.Hobbits.Internal.Mb+import Data.Binding.Hobbits.Internal.Closed+import Data.Binding.Hobbits.PatternParser (parsePattern)+import Data.Binding.Hobbits.NuMatching  +-- | Helper function to apply an expression to multiple arguments+appEMulti :: Exp -> [Exp] -> Exp+appEMulti = foldl AppE +-- | Helper function to apply the (.) operator on expressions compose :: Exp -> Exp -> Exp compose f g = VarE '(.) `AppE` f `AppE` g +-- | @patQQ str pat@ builds a quasi-quoter named @str@ that parses+-- | patterns with @pat@+patQQ :: String -> (String -> Q Pat) -> QuasiQuoter patQQ n pat = QuasiQuoter (err "Exp") pat (err "Type") (err "Decs")   where err s = error $ "QQ `" ++ n ++ "' is for patterns, not " ++ s ++ "."  ---+-- | A @WrapKit@ specifies a transformation to be applied to variables+-- | in a Template Haskell patterns, as follows:+--+-- * @_varView@ gives an expression for a function to be applied, as a+--   view pattern, to variables before matching them, including to+--   variables bound by @\@@ patterns;+--+-- * @_asXform@ gives a function to transform the bodies of \@+--   patterns, i.e., this function is applied to @p@ in pattern @x\@p@;+--+-- * @_topXform@ gives a function to transform the whole pattern after+--    @_varView@ and/or @_asXform@ have been applied to sub-patterns;+--    as the first argument, @_topXform@ also takes a flag indicating+--    whether any transformations have been applied to sub-patterns.+-- data WrapKit =-  -- _add adds structure just before binding the name (i.e. on VarP)-  -- _rm  removes structure that was added for the @ patterns-  -- _top removes structure at the top of the whole pattern-  WrapKit {_add :: Exp, _rm :: Pat -> Pat, _top :: Bool -> Pat -> Pat}+  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat} -outsideKit (WrapKit {_add = addO, _rm = rmO, _top = topO})-           (WrapKit {_add = addI, _rm = rmI, _top = topI}) =-  WrapKit {_add = addO `compose` addI,-           _rm = rmO . rmI,-           _top = \b -> topO b . topI b}+-- | Combine two WrapKits, composing the individual components+combineWrapKits :: WrapKit -> WrapKit -> WrapKit+combineWrapKits (WrapKit {_varView = varViewO, _asXform = asXformO, _topXform = topXformO})+           (WrapKit {_varView = varViewI, _asXform = asXformI, _topXform = topXformI}) =+  WrapKit {_varView = varViewO `compose` varViewI,+           _asXform = asXformO . asXformI,+           _topXform = \b -> topXformO b . topXformI b} --- wrapVars changes the types of names bound in a pattern+-- | Apply a 'WrapKit' to a pattern wrapVars :: Monad m => WrapKit -> Pat -> m Pat-wrapVars (WrapKit {_add = add, _rm = rm, _top = top}) pat = do-  (pat', Any usedAdd) <- runWriterT m-  return $ top usedAdd pat'+wrapVars (WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform}) pat = do+  (pat', Any usedVarView) <- runWriterT m+  return $ topXform usedVarView pat'   where     m = IU.everywhereButM (SYB.mkQ False isExp) (SYB.mkM w) pat       where isExp :: Exp -> Bool             -- don't recur into the expression part of view patterns             isExp _ = True -    -- this should be called if the 'add' function is ever used+    -- this should be called if the 'varView' function is ever used     hit x = tell (Any True) >> return x      -- wraps up bound names-    w p@VarP{} = hit $ ViewP add p+    w p@VarP{} = hit $ ViewP varView p     -- wraps for the bound name, then immediately unwraps     -- for the rest of the pattern-    w (AsP v p) = hit $ ViewP add $ AsP v $ rm p+    w (AsP v p) = hit $ ViewP varView $ AsP v $ asXform p     -- requires the expression to be closed     w (ViewP (VarE n) p) = return $ ViewP (VarE 'unCl `AppE` VarE n) p     w (ViewP e _) = fail $ "view function must be a single name: `" ++ show (TH.ppr e) ++ "'"     w p = return p ----+-- | Parse a pattern from a string, using 'parsePattern' parseHere :: String -> Q Pat parseHere s = do   fn <- loc_filename `fmap` location@@ -100,45 +115,34 @@     Right p -> return p  ---+-- | A helper function used to ensure two multi-bindings have the same contexts same_ctx :: Mb ctx a -> Mb ctx b -> Mb ctx b same_ctx _ x = x -nuKit mb ln = WrapKit {_add = add, _rm = rm, _top = top} where-  add = (VarE 'same_ctx `AppE` VarE mb) `compose`-        (ConE 'MkMb     `AppE` VarE ln)--  rm p = ConP 'MkMb [WildP, p]--  top b p = if b then AsP mb $ ConP 'MkMb [VarP ln, p] else rm p----+-- | Builds a 'WrapKit' for parsing patterns that match over 'Mb'.+-- | Takes two fresh names as arguments.+nuKit :: TH.Name -> TH.Name -> WrapKit+nuKit topVar namesVar = WrapKit {_varView = varView, _asXform = asXform, _topXform = topXform} where+  varView = (VarE 'same_ctx `AppE` VarE topVar) `compose`+        (appEMulti (ConE 'MkMbPair) [VarE 'nuMatchingProof, VarE namesVar])+  asXform p = ViewP (VarE 'ensureFreshPair) (TupP [WildP, p])+  topXform b p = if b then AsP topVar $ ViewP (VarE 'ensureFreshPair) (TupP [VarP namesVar, p]) else asXform p +-- | Quasi-quoter for patterns that match over 'Mb' nuP = patQQ "nuP" $ \s -> do-  mb <- newName "mb"-  ln <- newName "bs"--  parseHere s >>= wrapVars (nuKit mb ln)----+  topVar <- newName "topMb"+  namesVar <- newName "topNames"+  parseHere s >>= wrapVars (nuKit topVar namesVar) -clKit = WrapKit {_add = ConE 'Cl, _rm = rm, _top = const rm}-  where rm p = ConP 'Cl [p]+-- | Builds a 'WrapKit' for parsing patterns that match over 'Cl'+clKit = WrapKit {_varView = ConE 'Cl, _asXform = asXform, _topXform = const asXform}+  where asXform p = ConP 'Cl [p] +-- | Quasi-quoter for patterns that match over 'Cl', built using 'clKit' clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere ----+-- | Quasi-quoter for patterhs that match over @'Cl' ('Mb' ctx a)@ clNuP = patQQ "clNuP" $ \s -> do-  mb <- newName "mb"-  ln <- newName "bs"--  parseHere s >>= wrapVars (clKit `outsideKit` nuKit mb ln)+  topVar <- newName "topMb"+  namesVar <- newName "topNames"+  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)
+ Data/Type/HList.hs view
@@ -0,0 +1,203 @@+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GADTs #-}++-- |+-- Module      : Data.Type.HList+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- A /type list/ contains types as elements. We use GADT proofs terms to+-- establish membership and append relations. A @Data.Type.HList.HList@ @f@+-- is a vector indexed by a type list, where @f :: * -> *@ is applied to each+-- type element.++module Data.Type.HList where++import Data.Type.Equality ((:~:)(..))+import Data.Proxy (Proxy(..))+import Data.Functor.Constant+import Data.Typeable++-------------------------------------------------------------------------------+-- type-level lists+-------------------------------------------------------------------------------++data Nil deriving Typeable+data r :> a deriving Typeable; infixl 5 :>++type family (r1 :++: r2); infixr 5 :++:+type instance r :++: Nil = r+type instance r1 :++: r2 :> a = (r1 :++: r2) :> a++proxyCons :: Proxy r -> f a -> Proxy (r :> a)+proxyCons _ _ = Proxy+++-------------------------------------------------------------------------------+-- proofs of membership in a type-level list+-------------------------------------------------------------------------------++{-|+  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type+  list @ctx@, meaning that @ctx@ equals++>  t0 ':>' a ':>' t1 ':>' ... ':>' tn++  for some types @t0,t1,...,tn@.+-}+data Member ctx a where+  Member_Base :: Member (ctx :> a) a+  Member_Step :: Member ctx a -> Member (ctx :> b) a+  deriving Typeable++instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)++showsPrecMember :: Bool -> Member ctx a -> ShowS+showsPrecMember _ Member_Base = showString "Member_Base"+showsPrecMember p (Member_Step prf) = showParen p $+  showString "Member_Step" . showsPrec 10 prf++--toEq :: Member (Nil :> a) b -> b :~: a+--toEq Member_Base = Refl+--toEq _ = error "Should not happen! (toEq)"++weakenMemberL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a+weakenMemberL _ Member_Base = Member_Base+weakenMemberL tag (Member_Step mem) = Member_Step (weakenMemberL tag mem)++membersEq :: Member ctx a -> Member ctx b -> Maybe (a :~: b)+membersEq Member_Base Member_Base = Just Refl+membersEq (Member_Step mem1) (Member_Step mem2) = membersEq mem1 mem2+membersEq _ _ = Nothing+++------------------------------------------------------------+-- proofs that one list equals the append of two others+------------------------------------------------------------++{-|+  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.+-}+data Append ctx1 ctx2 ctx where+  Append_Base :: Append ctx Nil ctx+  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)++-- -- | Appends two 'Append' proofs.+-- trans ::+--   Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx+-- trans app Append_Base = app+-- trans app (Append_Step app') = Append_Step (trans app app')++-- -- | Returns a proof that ctx :~: ctx1 :++: ctx2+-- appendPf :: Append ctx1 ctx2 ctx -> (ctx :~: ctx1 :++: ctx2)+-- appendPf Append_Base = Refl+-- appendPf (Append_Step app) = case appendPf app of Refl -> Refl++-- -- | Returns the length of an 'Append' proof.+-- length :: Append ctx1 ctx2 ctx3 -> Int+-- length Append_Base = 0+-- length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app++-------------------------------------------------------------------------------+-- Heterogeneous lists+-------------------------------------------------------------------------------++{-|+  A @HList f c@ is a vector with exactly one element of type @f a@ for+  each type @a@ in the type list @c@.+-}+data HList f c where+  Nil :: HList f Nil -- Creates an empty vector+  (:>) :: HList f c -> f a -> HList f (c :> a) -- Appends an element to the end of a vector++-- | Create an empty 'HList' vector.+empty :: HList f Nil+empty = Nil++-- | Create a singleton 'HList' vector.+singleton :: f a -> HList f (Nil :> a)+singleton x = Nil :> x++-- | Look up an element of a 'HList' vector using a 'Member' proof.+hlistLookup :: Member c a -> HList f c -> f a+hlistLookup Member_Base (_ :> x) = x+hlistLookup (Member_Step mem') (mc :> _) = hlistLookup mem' mc+--hlistLookup _ _ = error "Should not happen! (hlistLookup)"++-- | Map a function on all elements of a 'HList' vector.+mapHList :: (forall x. f x -> g x) -> HList f c -> HList g c+mapHList _ Nil = Nil+mapHList f (mc :> x) = mapHList f mc :> f x++-- | Map a binary function on all pairs of elements of two 'HList' vectors.+mapHList2 :: (forall x. f x -> g x -> h x) -> HList f c -> HList g c -> HList h c+mapHList2 _ Nil Nil = Nil+mapHList2 f (xs :> x) (ys :> y) = mapHList2 f xs ys :> f x y+mapHList2 _ _ _ = error "Something is terribly wrong in mapHList2: this case should not happen!"++-- | Append two 'HList' vectors.+appendHList :: HList f c1 -> HList f c2 -> HList f (c1 :++: c2)+appendHList mc Nil = mc+appendHList mc1 (mc2 :> x) = appendHList mc1 mc2 :> x++-- -- | Append two 'HList' vectors.+-- appendWithPf :: Append c1 c2 c -> HList f c1 -> HList f c2 -> HList f c+-- appendWithPf Append_Base mc Nil = mc+-- appendWithPf (Append_Step app) mc1 (mc2 :> x) = appendWithPf app mc1 mc2 :> x+-- appendWithPf  _ _ _ = error "Something is terribly wrong in appendWithPf: this case should not happen!"++-- | Make an 'Append' proof from any 'HList' vector for the second+-- argument of the append.+mkAppend :: HList f c2 -> Append c1 c2 (c1 :++: c2)+mkAppend Nil = Append_Base+mkAppend (c :> _) = Append_Step (mkAppend c)++-- | A version of 'mkAppend' that takes in a 'Proxy' argument.+mkMonoAppend :: Proxy c1 -> HList f c2 -> Append c1 c2 (c1 :++: c2)+mkMonoAppend _ = mkAppend++-- | The inverse of 'mkAppend', that builds an 'HList' from an 'Append'+proxiesFromAppend :: Append c1 c2 c -> HList Proxy c2+proxiesFromAppend Append_Base = Nil+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :> Proxy++-- | Split an 'HList' vector into two pieces. The first argument is a+-- phantom argument that gives the form of the first list piece.+splitHList :: (c ~ (c1 :++: c2)) => Proxy c1 -> HList any c2 -> HList f c -> (HList f c1, HList f c2)+splitHList _ Nil mc = (mc, Nil)+splitHList _ (any :> _) (mc :> x) = (mc1, mc2 :> x)+  where (mc1, mc2) = splitHList Proxy any mc+--split _ _ = error "Should not happen! (Map.split)"++-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.+members :: HList f c -> HList (Member c) c+members Nil = Nil+members (c :> _) = mapHList Member_Step (members c) :> Member_Base++-- -- | Replace a single element of a 'HList' vector.+-- replace :: HList f c -> Member c a -> f a -> HList f c+-- replace (xs :> _) Member_Base y = xs :> y+-- replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x+-- replace _ _ _ = error "Should not happen! (Map.replace)"++-- | Convert an HList to a list+hlistToList :: HList (Constant a) c -> [a]+hlistToList Nil = []+hlistToList (xs :> Constant x) = hlistToList xs ++ [x]++-- | A type-class which ensures that ctx is a valid context, i.e., has+-- | the form (Nil :> t1 :> ... :> tn) for some types t1 through tn+class TypeCtx ctx where+  typeCtxProxies :: HList Proxy ctx++instance TypeCtx Nil where+  typeCtxProxies = Nil++instance TypeCtx ctx => TypeCtx (ctx :> a) where+  typeCtxProxies = typeCtxProxies :> Proxy
− Data/Type/List.hs 
@@ -1,35 +0,0 @@-{-# LANGUAGE TypeOperators, EmptyDataDecls #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE GADTs #-}---- |--- Module      : Data.Type.List--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ A /type list/ contains types as elements. We use GADT proofs terms to--- establish membership and append relations. A @Data.Type.List.Map.MapC@ @f@--- is a vector indexed by a type list, where @f :: * -> *@ is applied to each--- type element.--module Data.Type.List (-  module Data.Type.List.List, -- | Type-level nil, cons, and ++-  module Data.Type.List.Map, -- | Vectors parameterized by a @* -> *@ and indexed by a type list-  module Data.Type.List.Proof.Member, -- | Membership functions and proofs-  module Data.Type.List.Proof.Append, -- | Append functions and proofs-  module Data.Type.Equality,-  module Data.Proxy-  ) where--import Data.Type.List.List-import Data.Type.List.Map (MapC(..))-import Data.Type.List.Proof.Member (Member(..))-import Data.Type.List.Proof.Append (Append(..))--import Data.Type.Equality ((:=:)(..))-import Data.Proxy (Proxy(..))
− Data/Type/List/List.hs 
@@ -1,35 +0,0 @@-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE DeriveDataTypeable #-}---- |--- Module      : Data.Type.List.List--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ The type-level constructors of type lists.--module Data.Type.List.List where--import Data.Proxy (Proxy(..))-import Data.Typeable------------------------------------------------------------------------------------ type-level lists----------------------------------------------------------------------------------data Nil deriving Typeable-data r :> a deriving Typeable; infixl 5 :>--type family (r1 :++: r2); infixr 5 :++:-type instance r :++: Nil = r-type instance r1 :++: r2 :> a = (r1 :++: r2) :> a--proxyCons :: Proxy r -> f a -> Proxy (r :> a)-proxyCons _ _ = Proxy
− Data/Type/List/Map.hs 
@@ -1,101 +0,0 @@-{-# LANGUAGE GADTs, TypeOperators, RankNTypes #-}---- |--- Module      : Data.Type.List.Map--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ Vectors indexed by a type list--module Data.Type.List.Map where--import Data.Type.List.List-import Data.Type.List.Proof.Append (Append(..))-import Data.Type.List.Proof.Member (Member(..))-import Data.Proxy (Proxy(..))---import Data.Typeable--import Data.Functor.Constant------------------------------------------------------------------------------------ a vector of functor values, indexed by an List----------------------------------------------------------------------------------{-|-  A @MapC f c@ is a vector with exactly one element of type @f a@ for-  each type @a@ in the type list @c@.--}-data MapC f c where-  Nil :: MapC f Nil -- Creates an empty vector-  (:>) :: MapC f c -> f a -> MapC f (c :> a) -- Appends an element to the end of a vector---- | Create an empty 'MapC' vector.-empty :: MapC f Nil-empty = Nil---- | Create a singleton 'MapC' vector.-singleton :: f a -> MapC f (Nil :> a)-singleton x = Nil :> x---- | Look up an element of a 'MapC' vector using a 'Member' proof.-lookup :: Member c a -> MapC f c -> f a-lookup Member_Base (_ :> x) = x-lookup (Member_Step mem') (mc :> _) = Data.Type.List.Map.lookup mem' mc-lookup _ _ = error "Should not happen! (Map.lookup)"---- | Map a function to all elements of a 'MapC' vector.-mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g c-mapC _ Nil = Nil-mapC f (mc :> x) = mapC f mc :> f x---- | Map a binary function to all pairs of elements of two 'MapC' vectors.-mapC2 :: (forall x. f x -> g x -> h x) -> MapC f c -> MapC g c -> MapC h c-mapC2 _ Nil Nil = Nil-mapC2 f (xs :> x) (ys :> y) = mapC2 f xs ys :> f x y---- | Append two 'MapC' vectors.-append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)-append mc Nil = mc-append mc1 (mc2 :> x) = append mc1 mc2 :> x---- | Make an 'Append' proof from any 'MapC' vector for the second--- argument of the append.-mkAppend :: MapC f c2 -> Append c1 c2 (c1 :++: c2)-mkAppend Nil = Append_Base-mkAppend (c :> _) = Append_Step (mkAppend c)---- | A version of 'mkAppend' that takes in a 'Proxy' argument.-mkMonoAppend :: Proxy c1 -> MapC f c2 -> Append c1 c2 (c1 :++: c2)-mkMonoAppend _ = mkAppend---- | Split a 'MapC' vector into two pieces.-split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)-split Append_Base mc = (mc, Nil)-split (Append_Step app) (mc :> x) = (mc1, mc2 :> x)-  where (mc1, mc2) = split app mc-split _ _ = error "Should not happen! (Map.split)"---- | Create a 'Proxy' object for the type list of a 'MapC' vector.-proxy :: MapC f c -> Proxy c-proxy _ = Proxy---- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.-members :: MapC f c -> MapC (Member c) c-members Nil = Nil-members (c :> _) =-  mapC Member_Step (members c) :> Member_Base---- | Replace a single element of a 'MapC' vector.-replace :: MapC f c -> Member c a -> f a -> MapC f c-replace (xs :> _) Member_Base y = xs :> y-replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x---- | Convert a MapC to a list-mapCToList :: MapC (Constant a) c -> [a]-mapCToList Nil = []-mapCToList (xs :> Constant x) = mapCToList xs ++ [x]
− Data/Type/List/Proof/Append.hs 
@@ -1,46 +0,0 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}---- |--- Module      : Data.Type.List.Proof.Append--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ Proofs regarding a type list as an append of two others.--module Data.Type.List.Proof.Append where--import Data.Type.List.List-import Data.Type.Equality ((:=:)(..))----------------------------------------------------------------- proofs about appended lists---------------------------------------------------------------{-|-  An @Append ctx1 ctx2 ctx@ is a \"proof\" that @ctx = ctx1 ':++:' ctx2@.--}-data Append ctx1 ctx2 ctx where-  Append_Base :: Append ctx Nil ctx-  Append_Step :: Append ctx1 ctx2 ctx -> Append ctx1 (ctx2 :> a) (ctx :> a)---- | Appends two 'Append' proofs.-trans ::-  Append ctx1 ctx2 ex_ctx -> Append ex_ctx ctx3 ctx -> Append ctx1 (ctx2 :++: ctx3) ctx-trans app Append_Base = app-trans app (Append_Step app') = Append_Step (trans app app')---- | Returns a proof that ctx :=: ctx1 :++: ctx2-appendPf :: Append ctx1 ctx2 ctx -> (ctx :=: ctx1 :++: ctx2)-appendPf Append_Base = Refl-appendPf (Append_Step app) = case appendPf app of Refl -> Refl---- | Returns the length of an 'Append' proof.-length :: Append ctx1 ctx2 ctx3 -> Int-length Append_Base = 0-length (Append_Step app) = 1 + Data.Type.List.Proof.Append.length app
− Data/Type/List/Proof/Member.hs 
@@ -1,85 +0,0 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE DeriveDataTypeable #-}---- |--- Module      : Data.Type.List.Proof.Member--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ Proofs regarding membership of a type in a type list.--module Data.Type.List.Proof.Member (-  -- * Abstract data types-  Member(..),-  -- * Operators on 'Member' proofs-  toEq, weakenL, same, weakenR, split-  ) where--import Data.Type.List.List-import Data.Type.List.Proof.Append--import Data.Type.Equality ((:=:)(..))-import Data.Proxy (Proxy(..))-import Data.Typeable--import Unsafe.Coerce------------------------------------------------------------------------------------ proof of membership----------------------------------------------------------------------------------{-|-  A @Member ctx a@ is a \"proof\" that the type @a@ is in the type-  list @ctx@, meaning that @ctx@ equals-->  t0 ':>' a ':>' t1 ':>' ... ':>' tn--  for some types @t0,t1,...,tn@.--}-data Member ctx a where-  Member_Base :: Member (ctx :> a) a-  Member_Step :: Member ctx a -> Member (ctx :> b) a-  deriving Typeable--instance Show (Member r a) where showsPrec p = showsPrecMember (p > 10)--showsPrecMember _ Member_Base = showString "Member_Base"-showsPrecMember p (Member_Step prf) = showParen p $-  showString "Member_Step" . showsPrec 10 prf--toEq :: Member (Nil :> a) b -> b :=: a-toEq Member_Base = Refl-toEq _ = error "Should not happen! (toEq)"--weakenL :: Proxy r1 -> Member r2 a -> Member (r1 :++: r2) a-weakenL _    Member_Base = Member_Base-weakenL tag (Member_Step mem) = Member_Step (weakenL tag mem)--same :: Member r a -> Member r b -> Maybe (a :=: b)-same Member_Base Member_Base = Just $ unsafeCoerce Refl-same (Member_Step mem1) (Member_Step mem2) = same mem1 mem2-same _ _ = Nothing------------------------------------------------------------------------------------ relations between Member and Append----------------------------------------------------------------------------------weakenR :: Member r1 a -> Append r1 r2 r -> Member r a-weakenR mem Append_Base = mem-weakenR mem (Append_Step app) = Member_Step (weakenR mem app)--split ::-  Append r1 r2 r -> Member r a -> Either (Member r1 a) (Member r2 a)-split app mem = case app of-  Append_Base -> Left mem-  Append_Step app' -> case mem of-    Member_Base -> Right Member_Base-    Member_Step mem' -> case split app' mem' of-      Left prf -> Left prf-      Right prf -> Right (Member_Step prf)
hobbits.cabal view
@@ -1,5 +1,5 @@ Name:                hobbits-Version:             1.1.1+Version:             1.2 Synopsis:            A library for canonically representing terms with binding  Description: A library for canonically representing terms with binding via a@@ -9,7 +9,7 @@ License:             BSD3 License-file:        LICENSE Author:              Eddy Westbrook, Nicolas Frisby, Paul Brauner-Maintainer:          emw4@rice.edu+Maintainer:          westbrook@galois.com  Category:            Data Structures @@ -17,27 +17,23 @@ Build-Type:    Simple  Library-  Build-Depends: base >= 4 && < 5-  Build-Depends: template-haskell >= 2.5 && < 2.9+  Build-Depends: base >= 4.7 && < 4.9+  Build-Depends: template-haskell >= 2.9 && < 2.11    Build-Depends: syb   Build-Depends: mtl -  Build-Depends: type-equality, tagged+  Build-Depends: tagged   Build-Depends: deepseq -  Build-Depends: haskell-src-meta >= 0.5.1.1, haskell-src-exts,+  Build-Depends: haskell-src-exts >= 1.17.1 && < 1.18, haskell-src-meta,                  th-expand-syns >= 0.3 && < 0.4, transformers    GHC-Options: -fwarn-incomplete-patterns -fwarn-unused-imports    Extensions: CPP -  Exposed-Modules: Data.Type.List,-                   Data.Type.List.List,-                   Data.Type.List.Map,-                   Data.Type.List.Proof.Append,-                   Data.Type.List.Proof.Member,+  Exposed-Modules: Data.Type.HList,                     Data.Binding.Hobbits,                    Data.Binding.Hobbits.Mb,@@ -45,12 +41,14 @@                    Data.Binding.Hobbits.QQ,                    Data.Binding.Hobbits.Liftable, -                   Data.Binding.Hobbits.Internal,                    Data.Binding.Hobbits.PatternParser,-                   Data.Binding.Hobbits.NuElim,+                   Data.Binding.Hobbits.NuMatching,                     Data.Binding.Hobbits.Examples.LambdaLifting,                    Data.Binding.Hobbits.Examples.LambdaLifting.Terms,                    Data.Binding.Hobbits.Examples.LambdaLifting.Examples -  Other-Modules: Data.Binding.Hobbits.InternalUtilities+  Other-Modules: Data.Binding.Hobbits.Internal.Utilities,+                   Data.Binding.Hobbits.Internal.Name+                   Data.Binding.Hobbits.Internal.Mb+                   Data.Binding.Hobbits.Internal.Closed
− output 
@@ -1,20 +0,0 @@-Glasgow Haskell Compiler, Version 7.6.3, stage 2 booted by GHC version 7.4.2-Using binary package database: /Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/package.conf.d/package.cache-Using binary package database: /Users/eddy/.ghc/x86_64-darwin-7.6.3/package.conf.d/package.cache-hiding package Cabal-1.16.0 to avoid conflict with later version Cabal-1.18.1.2-wired-in package ghc-prim mapped to ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd-wired-in package integer-gmp mapped to integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7-wired-in package base mapped to base-4.6.0.1-6c351d70a24d3e96f315cba68f3acf57-wired-in package rts mapped to builtin_rts-wired-in package template-haskell mapped to template-haskell-2.8.0.0-c2c1b21dbbb37ace4b7dc26c966ec664-wired-in package dph-seq not found.-wired-in package dph-par not found.-Hsc static flags: -static-Created temporary directory: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0-*** C pre-processor:-'/usr/bin/clang-wrapper' '-E' '-undef' '-traditional' '-m64' '-fno-stack-protector' '-m64' '-I' '/Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/base-4.6.0.1/include' '-I' '/Library/Frameworks/GHC.framework/Versions/7.6.3-x86_64/usr/lib/ghc-7.6.3/include' '-D__GLASGOW_HASKELL__=706' '-Ddarwin_BUILD_OS=1' '-Dx86_64_BUILD_ARCH=1' '-Ddarwin_HOST_OS=1' '-Dx86_64_HOST_ARCH=1' '-U __PIC__' '-D__PIC__' '-include' 'dist/build/autogen/cabal_macros.h' '-D__GLASGOW_HASKELL__=706' '-Ddarwin_BUILD_OS=1' '-Dx86_64_BUILD_ARCH=1' '-Ddarwin_HOST_OS=1' '-Dx86_64_HOST_ARCH=1' '-x' 'c' 'Data/Type/List.hs' '-o' '/var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp'-*** Copying `/var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp' to `dist/build/tmp-36333/Data/Type/List.hs':-*** Deleting temp files:-Deleting: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0/ghc36361_0.hscpp-*** Deleting temp dirs:-Deleting: /var/folders/st/cjmsx__d5f17m4_1qn0dxkpr0000gn/T/ghc36361_0