hobbits 1.2 → 1.2.1

raw patch · 12 files changed

+373/−346 lines, 12 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG +8/−0
• Data/Binding/Hobbits.hs +2/−2
• Data/Binding/Hobbits/Examples/LambdaLifting.hs +55/−52
• Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs +11/−11
• Data/Binding/Hobbits/Internal/Mb.hs +12/−12
• Data/Binding/Hobbits/Internal/Name.hs +7/−7
• Data/Binding/Hobbits/Liftable.hs +3/−2
• Data/Binding/Hobbits/Mb.hs +47/−41
• Data/Binding/Hobbits/NuMatching.hs +16/−14
• Data/Type/HList.hs +0/−203
• Data/Type/RList.hs +208/−0
• hobbits.cabal +4/−2

@@ -0,0 +1,8 @@++1.2 -> 1.2.1+- Renamed Data.Type.HList to Data.Type.RList+- Now using DataKinds to represent right-lists of types++1.1.1 -> 1.2+- Added Closed type+- Updated to work with stack and also ghc-7.10

@@ -37,7 +37,7 @@    -- * Ancilliary modules   module Data.Proxy, module Data.Type.Equality,-  module Data.Type.HList,+  module Data.Type.RList,   -- | Type lists track the types of bound variables.   module Data.Binding.Hobbits.NuMatching   -- | The "Data.Binding.Hobbits.NuMatching" module exposes the@@ -47,7 +47,7 @@  import Data.Proxy import Data.Type.Equality-import Data.Type.HList+import Data.Type.RList import Data.Binding.Hobbits.Mb import Data.Binding.Hobbits.Closed import Data.Binding.Hobbits.QQ

@@ -1,7 +1,7 @@ {-# LANGUAGE QuasiQuotes, ViewPatterns #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeOperators, DataKinds #-} {-# LANGUAGE GADTs #-}  {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}@@ -32,7 +32,7 @@   ) where  import Data.Binding.Hobbits-import qualified Data.Type.HList as C+import qualified Data.Type.RList as C  import Data.Binding.Hobbits.Examples.LambdaLifting.Terms @@ -46,10 +46,10 @@ ------------------------------------------------------------  data LType a where LType :: LType (L a)-type LC c = HList LType c+type LC c = MapRList LType c -type family AddArrows c b-type instance AddArrows Nil b = b+type family AddArrows (c :: RList *) b+type instance AddArrows RNil b = b type instance AddArrows (c :> L a) b = AddArrows c (a -> b)  data PeelRet c a where@@ -57,36 +57,36 @@              PeelRet c (AddArrows lc a)  peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)-peelLambdas b = peelLambdasH Nil LType (mbCombine b)+peelLambdas b = peelLambdasH MNil LType (mbCombine b)  peelLambdasH ::   lc ~ (lc0 :> b) => LC lc0 -> LType b -> Mb (c :++: lc) (Term a) ->                      PeelRet c (AddArrows lc a) peelLambdasH lc0 isl [nuP| Lam b |] =-  peelLambdasH (lc0 :> isl) LType (mbCombine b)-peelLambdasH lc0 ilt t = PeelRet (lc0 :> ilt) t+  peelLambdasH (lc0 :>: isl) LType (mbCombine b)+peelLambdasH lc0 ilt t = PeelRet (lc0 :>: ilt) t     boundParams ::-  lc ~ (lc0 :> b) => LC lc -> (HList Name lc -> DTerm a) ->+  lc ~ (lc0 :> b) => LC lc -> (MapRList 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))+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 -> (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))+  LC lc -> (MapRList Name lc -> Decl a) -> Decl (AddArrows lc a)+freeParams MNil k = k C.empty+freeParams (lc :>: LType) k =+    freeParams lc (\names -> Decl_Cons $ nu $ \x -> k (names :>: x))  ------------------------------------------------------------ -- sub-contexts ------------------------------------------------------------  -- FIXME: use this type in place of functions-type SubC c' c = HList Name c -> HList Name c'+type SubC c' c = MapRList Name c -> MapRList Name c'  ------------------------------------------------------------ -- operations on contexts of free variables@@ -95,7 +95,7 @@ data MbLName c a where     MbLName :: Mb c (Name (L a)) -> MbLName c (L a) -type FVList c fvs = HList (MbLName c) fvs+type FVList c fvs = MapRList (MbLName c) fvs  -- unioning free variable contexts: the data structure data FVUnionRet c fvs1 fvs2 where@@ -103,21 +103,21 @@                   FVUnionRet c fvs1 fvs2  fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2-fvUnion Nil Nil = FVUnionRet Nil (\_ -> Nil) (\_ -> Nil)-fvUnion Nil (fvs2 :> fv2) = case fvUnion Nil fvs2 of+fvUnion MNil MNil = FVUnionRet MNil (\_ -> MNil) (\_ -> MNil)+fvUnion MNil (fvs2 :>: fv2) = case fvUnion MNil fvs2 of   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.hlistLookup idx xs)-fvUnion (fvs1 :> fv1) fvs2 = case fvUnion fvs1 fvs2 of+    Nothing -> FVUnionRet (fvs :>: fv2)+               (\(xs :>: _) -> f1 xs) (\(xs :>: x) -> f2 xs :>: x)+    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.hlistLookup idx xs) f2+    Nothing -> FVUnionRet (fvs :>: fv1)+               (\(xs :>: x) -> f1 xs :>: x) (\(xs :>: _) -> f2 xs)+    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-elemMC mbLN@(MbLName n) (mc :> MbLName n') = case mbCmpName n n' of+elemMC _ MNil = Nothing+elemMC mbLN@(MbLName n) (mc :>: MbLName n') = case mbCmpName n n' of   Just Refl -> Just Member_Base   Nothing -> fmap Member_Step (elemMC mbLN mc) @@ -131,7 +131,7 @@     SDVar :: Name (D a) -> STerm c a     SApp :: STerm c (a -> b) -> STerm c a -> STerm c b -skelSubst :: STerm c a -> HList Name c -> DTerm a+skelSubst :: STerm c a -> MapRList Name c -> DTerm a skelSubst (SWeaken f db) names = skelSubst db $ f names skelSubst (SVar inC) names = TVar $ C.hlistLookup inC names skelSubst (SDVar dTVar) _ = TDVar dTVar@@ -142,11 +142,11 @@   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 -> HList (Member fvs) args ->+    STerm fvs (AddArrows args a) -> FVList c args -> MapRList (Member fvs) args ->     STerm fvs a-  skelAppMultiNamesH fvs Nil _ = fvs+  skelAppMultiNamesH fvs MNil _ = fvs   -- flagged as non-exhaustive, in spite of type-  skelAppMultiNamesH fvs (args :> MbLName _) (inCs :> inC) =+  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =     SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)  ------------------------------------------------------------@@ -157,28 +157,31 @@     FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a  fvSSepLTVars ::-  HList f lc -> FVSTerm (c :++: lc) Nil a -> FVSTerm c lc a+  MapRList f lc -> FVSTerm (c :++: lc) RNil 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+-- | Create a 'Proxy' object for the type list of a 'MapRList' vector.+proxyOfMapRList :: MapRList f c -> Proxy c+proxyOfMapRList _ = Proxy  fvSSepLTVarsH ::-  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+  MapRList f lc -> Proxy c -> FVList (c :++: lc) fvs -> SepRet lc c fvs+fvSSepLTVarsH _ _ MNil = SepRet MNil (\_ -> MNil)+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.hlistLookup (C.weakenMemberL (proxyOfHList m) idx) xs)-    Right n -> SepRet (m :> MbLName n)-               (\xs -> case C.splitHList c' lc xs of-                         (fvs' :> fv', lcs) ->-                           f (appendHList fvs' lcs) :> fv')-    where c' = proxyCons (proxyOfHList m) fv+    Left idx ->+      SepRet m (\xs ->+                 f xs :>: C.hlistLookup (C.weakenMemberL (proxyOfMapRList m) idx) xs)+    Right n ->+      SepRet (m :>: MbLName n)+      (\xs -> case C.splitMapRList c' lc xs of+          (fvs' :>: fv', lcs) ->+            f (appendMapRList fvs' lcs) :>: fv')+    where c' = proxyCons (proxyOfMapRList m) fv  raiseAppName ::   Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))@@ -191,11 +194,11 @@ -- lambda-lifting, woo hoo! ------------------------------------------------------------ -type LLBodyRet b c a = Cont (Decls b) (FVSTerm c Nil a)+type LLBodyRet b c a = Cont (Decls b) (FVSTerm c RNil a)  llBody :: LC c -> Mb c (Term a) -> LLBodyRet b c a llBody _ [nuP| Var v |] =-  return $ FVSTerm (Nil :> MbLName v) $ SVar Member_Base+  return $ FVSTerm (MNil :>: MbLName v) $ SVar Member_Base llBody c [nuP| App t1 t2 |] = do   FVSTerm fvs1 db1 <- llBody c t1   FVSTerm fvs2 db2 <- llBody c t2@@ -203,23 +206,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.appendHList c lc) body+  llret <- llBody (C.appendMapRList c lc) body   FVSTerm fvs db <- return $ fvSSepLTVars lc llret   cont $ \k ->     Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->                 boundParams lc $ \names2 ->-                skelSubst db (C.appendHList names1 names2))+                skelSubst db (C.appendMapRList names1 names2))       $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)   where     fvsToLC :: FVList c lc -> LC lc-    fvsToLC = C.mapHList mbLNameToProof where+    fvsToLC = C.mapMapRList 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.mapHList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))+lambdaLift t = runCont (llBody MNil (emptyMb t)) $ \(FVSTerm fvs db) ->+  Decls_Base (skelSubst db (C.mapMapRList (\(MbLName mbn) -> elimEmptyMb mbn) fvs))  mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a) mbLambdaLift = fmap lambdaLift

@@ -1,6 +1,6 @@ {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}-{-# LANGUAGE GADTs, KindSignatures #-}+{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}  -- | -- Module      : Data.Binding.Hobbits.SuperComb@@ -20,13 +20,13 @@   ) where  import Data.Binding.Hobbits-import qualified Data.Type.HList as C+import qualified Data.Type.RList as C  -- dummy datatypes for distinguishing Decl names from Lam names data L a data D a --- to make a function for HList (for pretty)+-- to make a function for MapRList (for pretty) newtype StringF x = StringF String unStringF (StringF str) = str @@ -52,14 +52,14 @@ -- pretty print terms tpretty :: Term a -> String tpretty t = pretty' (emptyMb t) C.empty 0-  where pretty' :: Mb c (Term a) -> HList StringF c -> Int -> String+  where pretty' :: Mb c (Term a) -> MapRList StringF c -> Int -> String         pretty' [nuP| Var b |] varnames n =             case mbNameBoundP b of               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-            "(\\" ++ x ++ "." ++ pretty' (mbCombine b) (varnames :> (StringF x)) (n+1) ++ ")"+            "(\\" ++ x ++ "." ++ pretty' (mbCombine b) (varnames :>: (StringF x)) (n+1) ++ ")"         pretty' [nuP| App b1 b2 |] varnames n =             "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")" @@ -98,7 +98,7 @@ pretty :: DTerm a -> String pretty t = mpretty (emptyMb t) C.empty -mpretty :: Mb c (DTerm a) -> HList StringF c -> String+mpretty :: Mb c (DTerm a) -> MapRList StringF c -> String mpretty [nuP| TVar b |] varnames =     mprettyName (mbNameBoundP b) varnames mpretty [nuP| TDVar b |] varnames =@@ -116,18 +116,18 @@ decls_pretty decls =     "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0) -mdecls_pretty :: Mb c (Decls a) -> HList StringF c -> Int -> String+mdecls_pretty :: Mb c (Decls a) -> MapRList 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 =     let fname = "F" ++ show n in     fname ++ " " ++ (mdecl_pretty decl varnames 0) ++ "\n"-    ++ mdecls_pretty (mbCombine rest) (varnames :> (StringF fname)) (n+1)+    ++ mdecls_pretty (mbCombine rest) (varnames :>: (StringF fname)) (n+1) -mdecl_pretty :: Mb c (Decl a) -> HList StringF c -> Int -> String+mdecl_pretty :: Mb c (Decl a) -> MapRList 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)+  vname ++ " = " ++ mpretty (mbCombine t) (varnames :>: StringF vname) mdecl_pretty [nuP| Decl_Cons d|] varnames n =   let vname = "x" ++ show n in-  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :> StringF vname) (n+1)+  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)

@@ -21,14 +21,14 @@ import Data.Typeable import Data.Proxy import Data.Type.Equality-import Data.Type.HList+import Data.Type.RList  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@.+  in @ctx@, where @ctx@ has the form @'RNil' ':>' 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@@ -38,8 +38,8 @@   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+    = MkMbFun (MapRList Proxy ctx) (MapRList Name ctx -> b)+    | MkMbPair (MbTypeRepr b) (MapRList Name ctx) b     deriving Typeable  @@ -60,7 +60,7 @@     MbTypeReprData :: MbTypeReprData a -> MbTypeRepr a  data MbTypeReprData a =-    MkMbTypeReprData (forall ctx. HList Name ctx -> HList Name ctx -> a -> a)+    MkMbTypeReprData (forall ctx. MapRList Name ctx -> MapRList Name ctx -> a -> a)   {-|@@ -69,9 +69,9 @@   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 =+mapNamesPf :: MbTypeRepr a -> MapRList Name ctx -> MapRList Name ctx -> a -> a+mapNamesPf MbTypeReprName MNil MNil n = n+mapNamesPf MbTypeReprName (names :>: m) (names' :>: m') n =     case cmpName m n of       Just Refl -> m'       Nothing -> mapNamesPf MbTypeReprName names names' n@@ -88,14 +88,14 @@   -- | Ensures a multi-binding is in "fresh function" form-ensureFreshFun :: Mb ctx a -> (HList Proxy ctx, HList Name ctx -> a)+ensureFreshFun :: Mb ctx a -> (MapRList Proxy ctx, MapRList Name ctx -> a) ensureFreshFun (MkMbFun proxies f) = (proxies, f) ensureFreshFun (MkMbPair tRepr ns body) =-    (mapHList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)+    (mapMapRList (\_ -> 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 :: Mb ctx a -> (MapRList Name ctx, a) ensureFreshPair (MkMbPair _ ns body) = (ns, body) ensureFreshPair (MkMbFun proxies f) =-    let ns = mapHList (MkName . fresh_name) proxies in+    let ns = mapMapRList (MkName . fresh_name) proxies in     (ns, f ns)

@@ -26,7 +26,7 @@ import Data.IORef (IORef, newIORef, readIORef, writeIORef) import System.IO.Unsafe (unsafePerformIO) -import Data.Type.HList+import Data.Type.RList   -- | A @Name a@ is a bound name that is associated with type @a@.@@ -35,9 +35,9 @@ 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) ++ "]"+instance Show (MapRList Name c) where+    show names = "[" ++ (concat $ intersperse "," $ mapRListToList $+                        mapMapRList (Constant . show) names) ++ "]"   -------------------------------------------------------------------------------@@ -85,11 +85,11 @@   -- building a proxy for each type in some unknown context-data ExProxy where ExProxy :: HList Proxy ctx -> ExProxy+data ExProxy where ExProxy :: MapRList Proxy ctx -> ExProxy proxyFromLen :: Int -> ExProxy-proxyFromLen 0 = ExProxy Nil+proxyFromLen 0 = ExProxy MNil proxyFromLen n = case proxyFromLen (n - 1) of-                   ExProxy proxy -> ExProxy (proxy :> Proxy)+                   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

@@ -1,4 +1,5 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell, ViewPatterns, QuasiQuotes #-}+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}+{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds #-}  -- | -- Module      : Data.Binding.Hobbits.Mb@@ -18,7 +19,7 @@  module Data.Binding.Hobbits.Liftable where -import Data.Type.HList+import Data.Type.RList import Data.Binding.Hobbits.Internal.Mb import Data.Binding.Hobbits.QQ import Data.Binding.Hobbits.Closed

@@ -1,4 +1,4 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns #-}+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}  -- | -- Module      : Data.Binding.Hobbits.Mb@@ -38,7 +38,7 @@  import Unsafe.Coerce (unsafeCoerce) -import Data.Type.HList+import Data.Type.RList  import Data.Binding.Hobbits.Internal.Name import Data.Binding.Hobbits.Internal.Mb@@ -49,7 +49,7 @@ -------------------------------------------------------------------------------  -- | A @Binding@ is simply a multi-binding that binds one name-type Binding a = Mb (Nil :> a)+type Binding a = Mb (RNil :> a)  -- note: we reverse l to show the inner-most bindings last instance Show a => Show (Mb c a) where@@ -61,18 +61,18 @@   body is the result of @f n@. -} nu :: (Name a -> b) -> Binding a b-nu f = MkMbFun (Nil :> Proxy) (\(Nil :> n) -> f n)+nu f = MkMbFun (MNil :>: Proxy) (\(MNil :>: 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 @'HList' f ctx@, acts as a+  multi-binding.  The argument @p@, of type @'MapRList' 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 :: HList f ctx -> (HList Name ctx -> b) -> Mb ctx b-nuMulti proxies f = MkMbFun (mapHList (const Proxy) proxies) f+nuMulti :: MapRList f ctx -> (MapRList Name ctx -> b) -> Mb ctx b+nuMulti proxies f = MkMbFun (mapMapRList (const Proxy) proxies) f  -- | @nus = nuMulti@ nus x = nuMulti x@@ -95,12 +95,15 @@ -} mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx 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-                              Left memb -> Left (Member_Step memb)-                              Right n -> Right n+    helper :: MapRList Name c -> Name a -> Either (Member c a) (Name a)+    helper MNil n = Right n+    helper (names :>: (MkName i)) (MkName j)+      | i == j =+        unsafeCoerce $ Left Member_Base+    helper (names :>: _) n =+      case helper names n of+        Left memb -> Left (Member_Step memb)+        Right n -> Right n -- old implementation with lists {- case elemIndex n names of@@ -129,30 +132,31 @@ -------------------------------------------------------------------------------  -- | Creates an empty binding that binds 0 names.-emptyMb :: a -> Mb Nil a-emptyMb body = MkMbFun Nil (\_ -> body)+emptyMb :: a -> Mb RNil a+emptyMb body = MkMbFun MNil (\_ -> body)  {-|   Eliminates an empty binding, returning its body. Note that   @elimEmptyMb@ is the inverse of @emptyMb@. -}-elimEmptyMb :: Mb Nil a -> a+elimEmptyMb :: Mb RNil 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 :: MapRList Proxy ctx1 -> (MapRList Name ctx1 -> Mb ctx2 a) ->+                        MapRList Proxy ctx2 freshFunctionProxies proxies1 f =-    case f (mapHList (const $ MkName 0) proxies1) of+    case f (mapMapRList (const $ MkName 0) proxies1) of       MkMbFun proxies2 _ -> proxies2-      MkMbPair _ ns _ -> mapHList (const Proxy) ns+      MkMbPair _ ns _ -> mapMapRList (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 (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) =+  MkMbPair tRepr2 (appendMapRList 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"@@ -160,33 +164,33 @@     -- themselves     let proxies2 = freshFunctionProxies proxies1 f1 in     MkMbFun-    (appendHList proxies1 proxies2)+    (appendMapRList proxies1 proxies2)     (\ns ->-         let (ns1, ns2) = splitHList Proxy proxies2 ns in+         let (ns1, ns2) = splitMapRList 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+  type @'MapRList' any c2@, is a \"phantom\" argument to indicate how   the context @c@ should be split. -}-mbSeparate :: HList any ctx2 -> Mb (ctx1 :++: ctx2) a ->+mbSeparate :: MapRList 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+        (ns1, ns2) = splitMapRList Proxy c2 ns mbSeparate c2 (MkMbFun proxies f) =-    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendHList ns1 ns2)))+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendMapRList ns1 ns2)))         where-          (proxies1, proxies2) = splitHList Proxy c2 proxies+          (proxies1, proxies2) = splitMapRList Proxy c2 proxies   -- | Returns a proxy object that enumerates all the types in ctx.-mbToProxy :: Mb ctx a -> HList Proxy ctx+mbToProxy :: Mb ctx a -> MapRList Proxy ctx mbToProxy (MkMbFun proxies _) = proxies-mbToProxy (MkMbPair _ ns _) = mapHList (\_ -> Proxy) ns+mbToProxy (MkMbPair _ ns _) = mapMapRList (\_ -> Proxy) ns   {-|@@ -253,34 +257,36 @@  > (<*>) :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b > (<*>) f a =->     nuWithElimMulti ('Nil' :> f :> a)->                     (\_ ('Nil' :> 'Identity' f' :> 'Identity' a') -> f' a')+>     nuWithElimMulti ('MNil' :>: f :>: a)+>                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a') -} nuMultiWithElim :: TypeCtx ctx =>-                   (HList Name ctx -> HList Identity args -> b) ->-                   HList (Mb ctx) args -> Mb ctx b+                   (MapRList Name ctx -> MapRList Identity args -> b) ->+                   MapRList (Mb ctx) args -> Mb ctx b nuMultiWithElim f args =   MkMbFun typeCtxProxies-          (\ns -> f ns $ mapHList (\arg -> Identity $ snd (ensureFreshFun arg) ns) args)+          (\ns ->+            f ns $ mapMapRList (\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 ->+nuWithElim :: (Name a -> MapRList Identity args -> b) ->+              MapRList (Mb (RNil :> a)) args ->               Binding a b nuWithElim f args =-    nuMultiWithElim (\(Nil :> n) -> f n) args+    nuMultiWithElim (\(MNil :>: n) -> f n) args   {-|   Similar to 'nuMultiWithElim' but takes only one argument -}-nuMultiWithElim1 :: TypeCtx ctx => (HList Name ctx -> arg -> b) -> Mb ctx arg ->+nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg ->                     Mb ctx b nuMultiWithElim1 f arg =-    nuMultiWithElim (\names (Nil :> Identity arg) -> f names arg) (Nil :> arg)+    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg) (MNil :>: arg)   {-|@@ -289,4 +295,4 @@ -} nuWithElim1 :: (Name a -> arg -> b) -> Binding a arg -> Binding a b nuWithElim1 f arg =-  nuWithElim (\n (Nil :> Identity arg) -> f n arg) (Nil :> arg)+  nuWithElim (\n (MNil :>: Identity arg) -> f n arg) (MNil :>: arg)

@@ -1,4 +1,6 @@-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies, FlexibleInstances, FlexibleContexts, TemplateHaskell, UndecidableInstances, ScopedTypeVariables #-}+{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies #-}+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}+{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds #-}  -- | -- Module      : Data.Binding.Hobbits.NuMatching@@ -30,14 +32,14 @@ import Control.Monad.State --import Control.Monad.Identity -import Data.Type.HList+import Data.Type.RList 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 :: NuMatching a => MapRList Name ctx -> MapRList Name ctx -> a -> a mapNames = mapNamesPf nuMatchingProof  @@ -116,13 +118,13 @@  -- the NuMatchingList class, for saying that NuMatching holds for a context of types class NuMatchingList args where-    nuMatchingListProof :: HList NuMatchingObj args+    nuMatchingListProof :: MapRList NuMatchingObj args -instance NuMatchingList Nil where-    nuMatchingListProof = Nil+instance NuMatchingList RNil where+    nuMatchingListProof = MNil  instance (NuMatchingList args, NuMatching a) => NuMatchingList (args :> a) where-    nuMatchingListProof = nuMatchingListProof :> NuMatchingObj ()+    nuMatchingListProof = nuMatchingListProof :>: NuMatchingObj ()   class NuMatching1 f where@@ -135,16 +137,16 @@     nuMatchingProof = nuMatchingProof1 nuMatchingProof -} -instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (HList f ctx) where+instance (NuMatching1 f, NuMatchingList ctx) => NuMatching (MapRList 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)) =+                  MapRList NuMatchingObj args -> MapRList Name ctx1 ->+                  MapRList Name ctx1 -> MapRList f args -> MapRList f args+        helper MNil c1 c2 MNil = MNil+        helper (proofs :>: NuMatchingObj ()) c1 c2 (elems :>: (elem :: f a)) =             case nuMatchingProof1 :: NuMatchingObj (f a) of               NuMatchingObj () ->-                  (helper proofs c1 c2 elems) :>+                  (helper proofs c1 c2 elems) :>:                   mapNames c1 c2 elem  @@ -164,7 +166,7 @@  type Names = (TH.Name, TH.Name, TH.Name, TH.Name) -mapNamesType a = [t| forall ctx. HList Name ctx -> HList Name ctx -> $a -> $a |]+mapNamesType a = [t| forall ctx. MapRList Name ctx -> MapRList Name ctx -> $a -> $a |]  {-|   Template Haskell function for creating NuMatching instances for (G)ADTs.

@@ -1,203 +0,0 @@-{-# 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

@@ -0,0 +1,208 @@+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}+{-# LANGUAGE TypeFamilies, DataKinds, KindSignatures #-}+{-# LANGUAGE GADTs #-}++-- |+-- Module      : Data.Type.RList+-- Copyright   : (c) 2016 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- A /right list/, or 'RList', is a list where cons adds to the end, or the+-- right-hand side, of a list. This is useful conceptually for contexts of+-- name-bindings, where the most recent name-binding is intuitively at the end+-- of the context.++module Data.Type.RList where++import Data.Type.Equality ((:~:)(..))+import Data.Proxy (Proxy(..))+import Data.Functor.Constant+import Data.Typeable++-------------------------------------------------------------------------------+-- Right-lists as a datatype+-------------------------------------------------------------------------------++data RList a+  = RNil+  | (RList a) :> a++type family ((r1 :: RList *) :++: (r2 :: RList *)) :: RList *+infixr 5 :++:+type instance r :++: RNil = 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 RNil 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 @MapRList f r@ is a vector with exactly one element of type @f a@ for+  each type @a@ in the type 'RList' @r@.+-}+data MapRList f c where+  MNil :: MapRList f RNil+  (:>:) :: MapRList f c -> f a -> MapRList f (c :> a)++-- | Create an empty 'MapRList' vector.+empty :: MapRList f RNil+empty = MNil++-- | Create a singleton 'MapRList' vector.+singleton :: f a -> MapRList f (RNil :> a)+singleton x = MNil :>: x++-- | Look up an element of a 'MapRList' vector using a 'Member' proof.+hlistLookup :: Member c a -> MapRList 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 'MapRList' vector.+mapMapRList :: (forall x. f x -> g x) -> MapRList f c -> MapRList g c+mapMapRList _ MNil = MNil+mapMapRList f (mc :>: x) = mapMapRList f mc :>: f x++-- | Map a binary function on all pairs of elements of two 'MapRList' vectors.+mapMapRList2 :: (forall x. f x -> g x -> h x) ->+                MapRList f c -> MapRList g c -> MapRList h c+mapMapRList2 _ MNil MNil = MNil+mapMapRList2 f (xs :>: x) (ys :>: y) = mapMapRList2 f xs ys :>: f x y+mapMapRList2 _ _ _ =+  error "Something is terribly wrong in mapMapRList2: this case should not happen!"++-- | Append two 'MapRList' vectors.+appendMapRList :: MapRList f c1 -> MapRList f c2 -> MapRList f (c1 :++: c2)+appendMapRList mc MNil = mc+appendMapRList mc1 (mc2 :>: x) = appendMapRList mc1 mc2 :>: x++-- -- | Append two 'MapRList' vectors.+-- appendWithPf :: Append c1 c2 c -> MapRList f c1 -> MapRList f c2 -> MapRList 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 'MapRList' vector for the second+-- argument of the append.+mkAppend :: MapRList f c2 -> Append c1 c2 (c1 :++: c2)+mkAppend MNil = Append_Base+mkAppend (c :>: _) = Append_Step (mkAppend c)++-- | A version of 'mkAppend' that takes in a 'Proxy' argument.+mkMonoAppend :: Proxy c1 -> MapRList f c2 -> Append c1 c2 (c1 :++: c2)+mkMonoAppend _ = mkAppend++-- | The inverse of 'mkAppend', that builds an 'MapRList' from an 'Append'+proxiesFromAppend :: Append c1 c2 c -> MapRList Proxy c2+proxiesFromAppend Append_Base = MNil+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :>: Proxy++-- | Split an 'MapRList' vector into two pieces. The first argument is a+-- phantom argument that gives the form of the first list piece.+splitMapRList :: (c ~ (c1 :++: c2)) => Proxy c1 ->+                 MapRList any c2 -> MapRList f c -> (MapRList f c1, MapRList f c2)+splitMapRList _ MNil mc = (mc, MNil)+splitMapRList _ (any :>: _) (mc :>: x) = (mc1, mc2 :>: x)+  where (mc1, mc2) = splitMapRList 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 :: MapRList f c -> MapRList (Member c) c+members MNil = MNil+members (c :>: _) = mapMapRList Member_Step (members c) :>: Member_Base++-- -- | Replace a single element of a 'MapRList' vector.+-- replace :: MapRList f c -> Member c a -> f a -> MapRList 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 MapRList to a list+mapRListToList :: MapRList (Constant a) c -> [a]+mapRListToList MNil = []+mapRListToList (xs :>: Constant x) = mapRListToList xs ++ [x]++-- | A type-class which ensures that ctx is a valid context, i.e., has+-- | the form (RNil :> t1 :> ... :> tn) for some types t1 through tn+class TypeCtx ctx where+  typeCtxProxies :: MapRList Proxy ctx++instance TypeCtx RNil where+  typeCtxProxies = MNil++instance TypeCtx ctx => TypeCtx (ctx :> a) where+  typeCtxProxies = typeCtxProxies :>: Proxy

@@ -1,5 +1,5 @@ Name:                hobbits-Version:             1.2+Version:             1.2.1 Synopsis:            A library for canonically representing terms with binding  Description: A library for canonically representing terms with binding via a@@ -16,6 +16,8 @@ Cabal-version: >= 1.6.0.1 Build-Type:    Simple +extra-source-files: CHANGELOG+ Library   Build-Depends: base >= 4.7 && < 4.9   Build-Depends: template-haskell >= 2.9 && < 2.11@@ -33,7 +35,7 @@    Extensions: CPP -  Exposed-Modules: Data.Type.HList,+  Exposed-Modules: Data.Type.RList,                     Data.Binding.Hobbits,                    Data.Binding.Hobbits.Mb,