hobbits 1.2.4 → 1.3

raw patch · 36 files changed

+2915/−2225 lines, 36 filesdep +containersdep +vectordep ~haskell-src-extsdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: containers, vector

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

API changes (from Hackage documentation)

Files

• Data/Binding/Hobbits.hs +0/−55
• Data/Binding/Hobbits/Closed.hs +0/−64
• Data/Binding/Hobbits/Examples/LambdaLifting.hs +0/−228
• Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs +0/−52
• Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs +0/−133
• Data/Binding/Hobbits/Internal/Closed.hs +0/−78
• Data/Binding/Hobbits/Internal/Mb.hs +0/−101
• Data/Binding/Hobbits/Internal/Name.hs +0/−134
• Data/Binding/Hobbits/Internal/Utilities.hs +0/−13
• Data/Binding/Hobbits/Liftable.hs +0/−131
• Data/Binding/Hobbits/Mb.hs +0/−298
• Data/Binding/Hobbits/NuMatching.hs +0/−525
• Data/Binding/Hobbits/PatternParser.hs +0/−42
• Data/Binding/Hobbits/QQ.hs +0/−148
• Data/Type/RList.hs +0/−208
• LICENSE +1/−1
• hobbits.cabal +22/−14
• src/Data/Binding/Hobbits.hs +60/−0
• src/Data/Binding/Hobbits/Closed.hs +121/−0
• src/Data/Binding/Hobbits/Examples/LambdaLifting.hs +231/−0
• src/Data/Binding/Hobbits/Examples/LambdaLifting/Examples.hs +52/−0
• src/Data/Binding/Hobbits/Examples/LambdaLifting/Terms.hs +133/−0
• src/Data/Binding/Hobbits/Internal/Closed.hs +73/−0
• src/Data/Binding/Hobbits/Internal/Mb.hs +97/−0
• src/Data/Binding/Hobbits/Internal/Name.hs +167/−0
• src/Data/Binding/Hobbits/Internal/Utilities.hs +13/−0
• src/Data/Binding/Hobbits/Liftable.hs +154/−0
• src/Data/Binding/Hobbits/Mb.hs +324/−0
• src/Data/Binding/Hobbits/MonadBind.hs +102/−0
• src/Data/Binding/Hobbits/NameMap.hs +197/−0
• src/Data/Binding/Hobbits/NameSet.hs +135/−0
• src/Data/Binding/Hobbits/NuMatching.hs +579/−0
• src/Data/Binding/Hobbits/NuMatchingInstances.hs +40/−0
• src/Data/Binding/Hobbits/PatternParser.hs +34/−0
• src/Data/Binding/Hobbits/QQ.hs +148/−0
• src/Data/Type/RList.hs +232/−0

@@ -1,55 +0,0 @@-{-# LANGUAGE TypeOperators #-}---- |--- Module      : Data.Binding.Hobbits--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ This library implements multi-bindings as described in the paper--- E. Westbrook, N. Frisby, P. Brauner, \"Hobbits for Haskell: A Library for--- Higher-Order Encodings in Functional Programming Languages\".--module Data.Binding.Hobbits (-  -- * Values under multi-bindings-  module Data.Binding.Hobbits.Mb,-  -- | The 'Data.Binding.Hobbits.Mb.Mb' type modeling multi-bindings is the-  -- central abstract type of the library--  -- * Closed terms-  module Data.Binding.Hobbits.Closed,-  -- | The 'Data.Binding.Hobbits.Closed.Cl' type models-  -- super-combinators, which are safe functions to apply under-  -- 'Data.Binding.Hobbits.Mb.Mb'.--  -- * Pattern-matching multi-bindings and closed terms-  module Data.Binding.Hobbits.QQ,-  -- | The 'Data.Binding.Hobbits.QQ.nuP' quasiquoter allows safe pattern-  -- matching on 'Data.Binding.Hobbits.Mb.Mb'-  -- values. 'Data.Binding.Hobbits.QQ.superCombP' is similar.--  -- * Lifting values out of multi-bindings-  module Data.Binding.Hobbits.Liftable,--  -- * Ancilliary modules-  module Data.Proxy, module Data.Type.Equality,-  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-  -- | NuMatching class, which allows pattern-matching on (G)ADTs in-  -- | the bodies of multi-bindings-                            ) where--import Data.Proxy-import Data.Type.Equality-import Data.Type.RList-import Data.Binding.Hobbits.Mb-import Data.Binding.Hobbits.Closed-import Data.Binding.Hobbits.QQ-import Data.Binding.Hobbits.Liftable-import Data.Binding.Hobbits.NuMatching

@@ -1,64 +0,0 @@-{-# 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 uses Template Haskell to distinguish closed terms, so that the--- library can trust such functions to not contain any @Name@ values in their--- closure.--module Data.Binding.Hobbits.Closed (-  -- * Abstract types-  Closed(),-  -- * Operators involving 'Closed'-  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl,-  -- * Typeclass for inherently closed types-  Closable(..)-) where--import Data.Binding.Hobbits.Internal.Name-import Data.Binding.Hobbits.Internal.Mb-import Data.Binding.Hobbits.Internal.Closed-import Data.Binding.Hobbits.Mb---- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its--- multi-binding.-noClosedNames :: Closed (Name a) -> b-noClosedNames (Closed 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."---- | Closed terms are closed (sorry) under application.-clApply :: Closed (a -> b) -> Closed a -> Closed b--- could be defined with cl were it not for the GHC stage restriction-clApply (Closed f) (Closed a) = Closed (f a)---- | Closed multi-bindings are also closed under application.-clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) ->-             Closed (Mb ctx b)-clMbApply (Closed f) (Closed a) = Closed (mbApply f a)---- | When applying a closed function, the argument can be viewed as locally--- closed-clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b-clApplyCl (Closed f) a = Closed (f a)---- | FIXME: this should not be possible!!-closeBug :: a -> Closed a-closeBug = $([| \x -> $(mkClosed [| x |]) |])---- | Typeclass for inherently closed types-class Closable a where-  toClosed :: a -> Closed a

@@ -1,228 +0,0 @@-{-# LANGUAGE QuasiQuotes, ViewPatterns #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE TypeOperators, DataKinds #-}-{-# LANGUAGE GADTs #-}--{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}---- |--- Module      : Data.Binding.Hobbits.Examples.LambdaLifting--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ The lambda lifting example from the paper E. Westbrook, N. Frisby,--- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in--- Functional Programming Languages\".------------------------------------------------------------------------------ lambda lifting for the lambda calculus with top-level declarations----------------------------------------------------------------------------module Data.Binding.Hobbits.Examples.LambdaLifting (-  -- * Term data types, using 'Data.Binding.Hobbits.Mb'-  module Data.Binding.Hobbits.Examples.LambdaLifting.Terms,-  -- * The lambda-lifting function-  lambdaLift, mbLambdaLift-  ) where--import Data.Binding.Hobbits-import qualified Data.Type.RList as C--import Data.Binding.Hobbits.Examples.LambdaLifting.Terms---- imported for ease of use at terminal-import Data.Binding.Hobbits.Examples.LambdaLifting.Examples--import Control.Monad.Cont (Cont, runCont, cont)----------------------------------------------------------------- "peeling" lambdas off of a term---------------------------------------------------------------data LType a where LType :: LType (L a)-type LC c = MapRList LType c--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-  PeelRet :: lc ~ (lc0 :> b) => LC lc -> Mb (c :++: lc) (Term a) ->-             PeelRet c (AddArrows lc a)--peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)-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-----boundParams ::-  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))--freeParams ::-  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 = MapRList Name c -> MapRList Name c'----------------------------------------------------------------- operations on contexts of free variables---------------------------------------------------------------data MbLName c a where-    MbLName :: Mb c (Name (L a)) -> MbLName c (L a)--type FVList c fvs = MapRList (MbLName c) fvs---- unioning free variable contexts: the data structure-data FVUnionRet c fvs1 fvs2 where-    FVUnionRet :: FVList c fvs -> SubC fvs1 fvs -> SubC fvs2 fvs ->-                  FVUnionRet c fvs1 fvs2--fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2-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.mapRListLookup 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.mapRListLookup idx xs) f2--elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)-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)----------------------------------------------------------------- deBruijn terms, i.e., closed terms---------------------------------------------------------------data STerm c a where-    SWeaken :: SubC c1 c -> STerm c1 a -> STerm c a-    SVar :: Member c (L a) -> STerm c a-    SDVar :: Name (D a) -> STerm c a-    SApp :: STerm c (a -> b) -> STerm c a -> STerm c b--skelSubst :: STerm c a -> MapRList Name c -> DTerm a-skelSubst (SWeaken f db) names = skelSubst db $ f names-skelSubst (SVar inC) names = TVar $ C.mapRListLookup inC names-skelSubst (SDVar dTVar) _ = TDVar dTVar-skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names)---- applying a STerm to a context of names-skelAppMultiNames ::-  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 -> MapRList (Member fvs) args ->-    STerm fvs a-  skelAppMultiNamesH fvs MNil _ = fvs-  -- flagged as non-exhaustive, in spite of type-  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =-    SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)----------------------------------------------------------------- STerms combined with their free variables---------------------------------------------------------------data FVSTerm c lc a where-    FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a--fvSSepLTVars ::-  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 'MapRList' vector.-proxyOfMapRList :: MapRList f c -> Proxy c-proxyOfMapRList _ = Proxy--fvSSepLTVarsH ::-  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.mapRListLookup (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))-raiseAppName app n =-  case fmap mbNameBoundP (mbSeparate (proxiesFromAppend app) n) of-    [nuP| Left mem |] -> Left $ mbLift mem-    [nuP| Right n |] -> Right n----------------------------------------------------------------- lambda-lifting, woo hoo!---------------------------------------------------------------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 (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-  FVUnionRet names sub1 sub2 <- return $ fvUnion fvs1 fvs2-  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.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.appendMapRList names1 names2))-      $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)-  where-    fvsToLC :: FVList c lc -> LC lc-    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 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,52 +0,0 @@--- |--- Module      : Data.Binding.Hobbits.SuperComb--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC-----module Data.Binding.Hobbits.Examples.LambdaLifting.Examples where--import Data.Binding.Hobbits.Examples.LambdaLifting.Terms-import Data.Binding.Hobbits----------------------------------------------------------------- examples---------------------------------------------------------------ex1 :: Term ((b1 -> b) -> b1 -> b)-ex1 = lam (\f -> (lam $ \x -> App f x))--ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)-ex2 = lam (\f1 -> App f1 (lam (\f2 -> lam (\x -> App f2 x))))--ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)-ex3 = lam (\x -> lam (\f1 -> App f1 (lam (\f2 -> lam (\y -> f2 `App` x `App` y)))))--ex4-  :: Term-       (((b1 -> b) -> b2 -> b)-        -> (((b1 -> b) -> b2 -> b) -> b2 -> b1)-        -> b2-        -> b1)-ex4 = lam $ \x -> lam $ \f1 ->-      App f1 (lam $ \f2 -> lam $ \y -> f2 `App` (f1 `App` x `App` y))--ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)-ex5 = lam (\f1 -> lam $ \f2 -> App f1 (lam $ \x -> App f2 x))---- lambda-lift with a free variable (use mbLambdaLift)-ex6 :: Binding (L ((b -> b) -> a)) (Term a)-ex6 = nu (\f -> App (Var f) (lam $ \x -> x))---- lambda-lift with a free variable as part of a lambda's environment-ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))-ex7 = nu (\f -> lam $ \y -> App y $ App (Var f) (lam $ \x -> x))---- example from paper's Section 4-exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)-exP = lam $ \f -> lam $ \g -> App f $ lam $ \x -> App g $ App g x

@@ -1,133 +0,0 @@-{-# LANGUAGE EmptyDataDecls #-}-{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}-{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}---- |--- Module      : Data.Binding.Hobbits.SuperComb--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC-----module Data.Binding.Hobbits.Examples.LambdaLifting.Terms-  (L, D,-   Term(..), lam,-   DTerm(..), Decl(..), Decls(..)-  ) where--import Data.Binding.Hobbits-import qualified Data.Type.RList as C---- dummy datatypes for distinguishing Decl names from Lam names-data L a-data D a---- to make a function for MapRList (for pretty)-newtype StringF x = StringF String-unStringF (StringF str) = str------------------------------------------------------------------ source terms----------------------------------------------------------------- Term datatype; no Ds since there's no declarations yet-data Term :: * -> * where-  Var :: Name (L a) -> Term a-  Lam :: Binding (L b) (Term a) -> Term (b -> a)-  App :: Term (b -> a) -> Term b -> Term a--$(mkNuMatching [t| forall a . Term a |])--instance Show (Term a) where show = tpretty---- helps to build terms without explicitly using nu or Var-lam :: (Term a -> Term b) -> Term (a -> b)-lam f = Lam $ nu (f . Var)---- pretty print terms-tpretty :: Term a -> String-tpretty t = pretty' (emptyMb t) C.empty 0-  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.mapRListLookup 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) ++ ")"-        pretty' [nuP| App b1 b2 |] varnames n =-            "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")"----------------------------------------------------------------- target terms----------------------------------------------------------------- terms under declarations-data DTerm :: * -> * where-  TVar :: Name (L a) -> DTerm a-  TDVar :: Name (D a) -> DTerm a-  TApp :: DTerm (a -> b) -> DTerm a -> DTerm b---- we use this type for a definiens instead of putting lambdas on the front-data Decl :: * -> * where-  Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)-  Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)---- top-level declarations with a return value-data Decls :: * -> * where-  Decls_Base :: DTerm a -> Decls a-  Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a--$(mkNuMatching [t| forall a . DTerm a |])-$(mkNuMatching [t| forall a . Decl a |])-$(mkNuMatching [t| forall a . Decls a |])--instance Show (DTerm a) where show = pretty-instance Show (Decls a) where show = decls_pretty----------------------------------------------------------------- pretty printing----------------------------------------------------------------- pretty print terms-pretty :: DTerm a -> String-pretty t = mpretty (emptyMb t) C.empty--mpretty :: Mb c (DTerm a) -> MapRList StringF c -> String-mpretty [nuP| TVar b |] varnames =-    mprettyName (mbNameBoundP b) varnames-mpretty [nuP| TDVar b |] varnames =-    mprettyName (mbNameBoundP b) varnames-mpretty [nuP| TApp b1 b2 |] varnames =-    "(" ++ mpretty b1 varnames-        ++ " " ++ mpretty b2 varnames ++ ")"--mprettyName (Left pf) varnames = unStringF (C.mapRListLookup pf varnames)-mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"-        ---- pretty print decls-decls_pretty :: Decls a -> String-decls_pretty decls =-    "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)--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)--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)-mdecl_pretty [nuP| Decl_Cons d|] varnames n =-  let vname = "x" ++ show n in-  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)

@@ -1,78 +0,0 @@-{-# 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--import Language.Haskell.TH (Q, Exp(..), Type(..))-import qualified Language.Haskell.TH as TH-import qualified Language.Haskell.TH.ExpandSyns as TH--import qualified Data.Generics as SYB-import qualified Language.Haskell.TH.Syntax as TH--{-| The type @Closed 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 @Closed@ data type is hidden, and the-user can only create closed terms using Template Haskell, through the 'mkClosed'-operator. -}-newtype Closed a = Closed { unClosed :: a }---- | Extract the type of an 'Info' object-#if MIN_VERSION_template_haskell(2,11,0)-reifyNameType :: TH.Name -> Q Type-reifyNameType n =-  TH.reify n >>= \i ->-  case i of-    TH.VarI _ ty _ -> return ty-    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."-#else-reifyNameType :: TH.Name -> Q Type-reifyNameType n =-  TH.reify n >>= \i ->-  case i of-    TH.VarI _ ty _ _ -> return ty-    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."-#endif---- | @mkClosed@ is used with Template Haskell quotations to create closed terms--- of type 'Closed'. A quoted expression is closed if all of the names occuring in--- it are either:------   1) bound globally or---   2) bound within the quotation or---   3) also of type 'Closed'.-mkClosed :: Q Exp -> Q Exp-mkClosed e = AppE (ConE 'Closed) `fmap` e >>= SYB.everywhereM (SYB.mkM w) where-  w e@(VarE n@(TH.Name _ flav)) = case flav of-    TH.NameG {} -> return e -- bound globally-    TH.NameU {} -> return e -- bound locally within this quotation-    TH.NameL {} -> closed n >> return e -- bound locally outside this quotation-    _ -> fail $ "`mkClosed' does not allow dynamically bound names: `"-      ++ show n ++ "'."-  w e = return e--  closed n = do-    ty <- reifyNameType n-    TH.expandSyns ty >>= w ty-      where-        w _ (AppT (ConT m) _) | m == ''Closed = return ()-        w top_ty (ForallT _ _ ty') = w top_ty ty'-        w top_ty _ =-          fail $ "`mkClosed` requires non-global variables to have type `Closed'.\n\t`"-          ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"-          ++ show (TH.ppr top_ty) ++ "'."

@@ -1,101 +0,0 @@-{-# 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.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 @'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-  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 (MapRList Proxy ctx) (MapRList Name ctx -> b)-    | MkMbPair (MbTypeRepr b) (MapRList 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. MapRList Name ctx -> MapRList 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 -> 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-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 -> (MapRList Proxy ctx, MapRList Name ctx -> a)-ensureFreshFun (MkMbFun proxies f) = (proxies, f)-ensureFreshFun (MkMbPair tRepr ns body) =-    (mapMapRList (\_ -> Proxy) ns, \ns' -> mapNamesPf tRepr ns ns' body)---- | Ensures a multi-binding is in "fresh pair" form-ensureFreshPair :: Mb ctx a -> (MapRList Name ctx, a)-ensureFreshPair (MkMbPair _ ns body) = (ns, body)-ensureFreshPair (MkMbFun proxies f) =-    let ns = mapMapRList (MkName . fresh_name) proxies in-    (ns, f ns)

@@ -1,134 +0,0 @@-{-# 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.RList----- | 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 (MapRList Name c) where-    show names = "[" ++ (concat $ intersperse "," $ mapRListToList $-                        mapMapRList (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 :: MapRList Proxy ctx -> ExProxy-proxyFromLen :: Int -> ExProxy-proxyFromLen 0 = ExProxy MNil-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)

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

@@ -1,131 +0,0 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}-{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds #-}---- |--- Module      : Data.Binding.Hobbits.Mb--- Copyright   : (c) 2014 Edwin Westbrook------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ This module defines the type-class Liftable for lifting--- non-binding-related data out of name-bindings. Note that this code--- is not "trusted", i.e., it is not part of the name-binding--- abstraction: instead, it is all written using the primitives--- exported by the Mb--module Data.Binding.Hobbits.Liftable where--import Data.Type.RList-import Data.Binding.Hobbits.Internal.Mb-import Data.Binding.Hobbits.QQ-import Data.Binding.Hobbits.Closed-import Data.Binding.Hobbits.NuMatching--import Data.Ratio---{-|-  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 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 (ensureFreshPair -> (_, i)) = i--instance Liftable Integer where-    mbLift (ensureFreshPair -> (_, i)) = i--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-instance Liftable (Member c a) where-    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--instance (Integral a, NuMatching a) => NuMatching (Ratio a) where-  nuMatchingProof =-    isoMbTypeRepr (\r -> (numerator r, denominator r)) (\(n,d) -> n%d)-instance (Integral a, Liftable a) => Liftable (Ratio a) where-  mbLift mb_r =-    (\(n,d) -> n%d) $ mbLift $ fmap (\r -> (numerator r, denominator r)) mb_r--instance Liftable a => Liftable [a] where-    mbLift [nuP| [] |] = []-    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)--instance Liftable () where-    mbLift [nuP| () |] = ()--instance (Liftable a, Liftable b) => Liftable (a,b) where-    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)--instance Liftable Bool where-  mbLift [nuP| True |] = True-  mbLift [nuP| False |] = False--instance Liftable a => Liftable (Maybe a) where-  mbLift [nuP| Nothing |] = Nothing-  mbLift [nuP| Just mb_a |] = Just $ mbLift mb_a--instance (Liftable a, Liftable b) => Liftable (Either a b) where-  mbLift [nuP| Left mb_a |] = Left $ mbLift mb_a-  mbLift [nuP| Right mb_b |] = Right $ mbLift mb_b---- README: these lead to overlapping instances...--{---{-|-  The class @Liftable1 f@ gives a lifting function for each type @f a@-  when @a@ itself is @Liftable@.--}-class Liftable1 f where-    mbLift1 :: Liftable a => Mb ctx (f a) -> f a--instance (Liftable1 f, Liftable a) => Liftable (f a) where-    mbLift = mbLift1--instance Liftable1 [] where-    mbLift1 [nuP| [] |] = []-    mbLift1 [nuP| x : xs |] = (mbLift x) : (mbLift1 xs)--{-|-  The class @Liftable2 f@ gives a lifting function for each type @f a b@-  when @a@ and @b@ are @Liftable@.--}-class Liftable2 f where-    mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b--instance Liftable2 (,) where-    mbLift2 [nuP| (x,y) |] = (mbLift x, mbLift y)--instance (Liftable2 f, Liftable a) => Liftable1 (f a) where-    mbLift1 = mbLift2---}

@@ -1,298 +0,0 @@-{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}---- |--- Module      : Data.Binding.Hobbits.Mb--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ This module defines multi-bindings as the type 'Mb', as well as a number of--- operations on multi-bindings. See the paper E. Westbrook, N. Frisby,--- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in--- Functional Programming Languages\" for more information.--module Data.Binding.Hobbits.Mb (-  -- * Abstract types-  Name(),      -- hides Name implementation-  Binding(),   -- hides Binding implementation-  Mb(),        -- hides MultiBind implementation-  -- * Multi-binding constructors-  nu, nuMulti, nus, emptyMb,-  -- * Queries on names-  cmpName, mbNameBoundP, mbCmpName,-  -- * Operations on multi-bindings-  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbApply,-  -- * Eliminators for multi-bindings-  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1-) where--import Control.Applicative-import Control.Monad.Identity--import Data.Type.Equality ((:~:)(..))-import Data.Proxy (Proxy(..))--import Unsafe.Coerce (unsafeCoerce)--import Data.Type.RList--import Data.Binding.Hobbits.Internal.Name-import Data.Binding.Hobbits.Internal.Mb---import qualified Data.Binding.Hobbits.Internal as I------------------------------------------------------------------------------------ creating bindings------------------------------------------------------------------------------------ | A @Binding@ is simply a multi-binding that binds one name-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-  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $-    showChar '#' . shows names . showChar '.' . shows b--{-|-  @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 = 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 @'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 :: 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------------------------------------------------------------------------------------- Queries on Names----------------------------------------------------------------------------------{-|-  Checks if a name is bound in a multi-binding, returning @Left mem@-  when the name is bound, where @mem@ is a proof that the type of the-  name is in the type list for the multi-binding, and returning-  @Right n@ when the name is not bound, where @n@ is the name.--  For example:--> nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base-> nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n--}-mbNameBoundP :: Mb ctx (Name a) -> Either (Member ctx a) (Name a)-mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where-    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-  Nothing -> Right (MkName n)-  Just i -> Left (I.unsafeLookupC i)--}---{-|-  Compares two names inside bindings, taking alpha-equivalence into-  account; i.e., if both are the @i@th name, or both are the same name-  not bound in their respective multi-bindings, then they compare as-  equal. The return values are the same as for 'cmpName', so that-  @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 b1 b2 = case (mbNameBoundP b1, mbNameBoundP b2) of-  (Left mem1, Left mem2) -> membersEq mem1 mem2-  (Right n1, Right n2) -> cmpName n1 n2-  _ -> Nothing------------------------------------------------------------------------------------- Operations on multi-bindings------------------------------------------------------------------------------------ | Creates an empty binding that binds 0 names.-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 RNil a -> a-elimEmptyMb (ensureFreshPair -> (_, body)) = body----- Extract the proxy objects from an Mb inside of a fresh function-freshFunctionProxies :: MapRList Proxy ctx1 -> (MapRList Name ctx1 -> Mb ctx2 a) ->-                        MapRList Proxy ctx2-freshFunctionProxies proxies1 f =-    case f (mapMapRList (const $ MkName 0) proxies1) of-      MkMbFun proxies2 _ -> proxies2-      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 (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"-    -- because these proxies should never depend on the names-    -- themselves-    let proxies2 = freshFunctionProxies proxies1 f1 in-    MkMbFun-    (appendMapRList proxies1 proxies2)-    (\ns ->-         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 @'MapRList' any c2@, is a \"phantom\" argument to indicate how-  the context @c@ should be split.--}-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) = splitMapRList Proxy c2 ns-mbSeparate c2 (MkMbFun proxies f) =-    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (appendMapRList ns1 ns2)))-        where-          (proxies1, proxies2) = splitMapRList Proxy c2 proxies----- | Returns a proxy object that enumerates all the types in ctx.-mbToProxy :: Mb ctx a -> MapRList Proxy ctx-mbToProxy (MkMbFun proxies _) = proxies-mbToProxy (MkMbPair _ ns _) = mapMapRList (\_ -> 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 ('MNil' :>: f :>: a)->                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')--}-nuMultiWithElim :: TypeCtx ctx =>-                   (MapRList Name ctx -> MapRList Identity args -> b) ->-                   MapRList (Mb ctx) args -> Mb ctx b-nuMultiWithElim f args =-  MkMbFun typeCtxProxies-          (\ns ->-            f ns $ mapMapRList (\arg ->-                                 Identity $ snd (ensureFreshFun arg) ns) args)---{-|-  Similar to 'nuMultiWithElim' but binds only one name.--}-nuWithElim :: (Name a -> MapRList Identity args -> b) ->-              MapRList (Mb (RNil :> a)) args ->-              Binding a b-nuWithElim f args =-    nuMultiWithElim (\(MNil :>: n) -> f n) args---{-|-  Similar to 'nuMultiWithElim' but takes only one argument--}-nuMultiWithElim1 :: TypeCtx ctx => (MapRList Name ctx -> arg -> b) -> Mb ctx arg ->-                    Mb ctx b-nuMultiWithElim1 f arg =-    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg) (MNil :>: 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 (MNil :>: Identity arg) -> f n arg) (MNil :>: arg)

@@ -1,525 +0,0 @@-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ViewPatterns, TypeFamilies #-}-{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances #-}-{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, DataKinds #-}---- |--- 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(), isoMbTypeRepr, NuMatchingObj(..)-) 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.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 => MapRList Name ctx -> MapRList Name ctx -> a -> a-mapNames = mapNamesPf nuMatchingProof---- | Helper to match a data declaration in a TH version-insensitive way-#if MIN_VERSION_template_haskell(2,11,0)-matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])-matchDataDecl (DataD cxt name tyvars _ constrs _) =-  Just (cxt, name, tyvars, constrs)-matchDataDecl (NewtypeD cxt name tyvars _ constr _) =-  Just (cxt, name, tyvars, [constr])-matchDataDecl _ = Nothing-#else-matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])-matchDataDecl (DataD cxt name tyvars constrs _) =-  Just (cxt, name, tyvars, constrs)-matchDataDecl (NewtypeD cxt name tyvars constr _) =-  Just (cxt, name, tyvars, [constr])-matchDataDecl _ = Nothing-#endif---- | Helper to build an instance declaration in a TH version-insensitive way-#if MIN_VERSION_template_haskell(2,11,0)-mkInstanceD :: Cxt -> Type -> [Dec] -> Dec-mkInstanceD = InstanceD Nothing-#else-mkInstanceD :: Cxt -> Type -> [Dec] -> Dec-mkInstanceD = InstanceD-#endif---{-|-  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 (Closed 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 Bool where-    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ _ -> id))--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 () 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 (Maybe a) where-    nuMatchingProof = MbTypeReprData-                  (MkMbTypeReprData-                   $ (\c1 c2 x -> case x of-                                    Just x -> Just (mapNames c1 c2 x)-                                    Nothing -> Nothing))--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 :: MapRList NuMatchingObj args--instance NuMatchingList RNil where-    nuMatchingListProof = MNil--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 (MapRList f ctx) where-    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where-        helper :: NuMatching1 f =>-                  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) :>:-                  mapNames c1 c2 elem----- | Build an 'MbTypeRepr' for type @a@ by using an isomorphism with an--- already-representable type @b@. This is useful for building 'NuMatching'--- instances for, e.g., 'Integral' types, by mapping to and from 'Integer',--- without having to define instances for each one in this module.-isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a-isoMbTypeRepr f_to f_from =-  MbTypeReprData $ MkMbTypeReprData $ \names1 names2 a ->-  f_from $ mapNames names1 names2 (f_to a)----- 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. MapRList Name ctx -> MapRList 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 <- getClauses (tName, fName, x1Name, x2Name) constrs-       mapNamesT <- mapNamesType (return cType)-       return [mkInstanceD-               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 (matchDataDecl -> Just (_, _, tyvarsReq, constrs)) ->-                 success tyvarsReq constrs-               _ -> 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 _ [] = return []--      getClauses names (NormalC cName cTypes : constrs) =-        do clause <--             getClauseHelper names (map snd cTypes) (natsFrom 0)-             (\l -> ConP cName (map (VarP . fst3) l))-             (\l -> foldl AppE (ConE cName) (map fst3 l))-           clauses <- getClauses names constrs-           return $ clause : clauses--      getClauses names (RecC cName cVarTypes : constrs) =-        do clause <--             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))-           clauses <- getClauses names constrs-           return $ clause : clauses--      getClauses names (InfixC cType1 cName cType2 : constrs) =-        undefined -- FIXME--#if MIN_VERSION_template_haskell(2,11,0)-      getClauses names (GadtC cNames cTypes _ : constrs) =-        do clauses1 <--             forM cNames $ \cName ->-             getClauseHelper names (map snd cTypes) (natsFrom 0)-             (\l -> ConP cName (map (VarP . fst3) l))-             (\l -> foldl AppE (ConE cName) (map fst3 l))-           clauses2 <- getClauses names constrs-           return (clauses1 ++ clauses2)--      getClauses names (RecGadtC cNames cVarTypes _ : constrs) =-        do clauses1 <--             forM cNames $ \cName ->-             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))-           clauses2 <- getClauses names constrs-           return (clauses1 ++ clauses2)-#endif--      getClauses names (ForallC _ _ constr : constrs) =-        getClauses names (constr : constrs)--      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 (matchDataDecl -> Just (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] -> [TyVarBndr] -> [Con] ->-                    CxtStateQ [Clause]-      getClauses cxt name tyvars locTyvars [] = return []--      getClauses cxt name tyvars locTyvars (NormalC cName cTypes : constrs) =-        do clause <--             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))-           clauses <- getClauses cxt name tyvars locTyvars constrs-           return (clause : clauses)--      getClauses cxt name tyvars locTyvars (RecC cName cVarTypes : constrs) =-        do clause <--             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))-           clauses <- getClauses cxt name tyvars locTyvars constrs-           return (clause : clauses)--      getClauses cxt name tyvars locTyvars (InfixC cType1 cName cType2 : _) =-        undefined -- FIXME--      getClauses cxt name tyvars locTyvars (ForallC tyvars2 cxt2 constr-                                            : constrs) =-        do clauses1 <--             getClauses (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) [constr]-           clauses2 <- getClauses cxt name tyvars locTyvars constrs-           return (clauses1 ++ clauses2)--#if MIN_VERSION_template_haskell(2,11,0)-      getClauses cxt name tyvars locTyvars (GadtC cNames cTypes _ : constrs) =-        do clauses1 <--             forM cNames $ \cName ->-             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))-           clauses2 <- getClauses cxt name tyvars locTyvars constrs-           return (clauses1 ++ clauses2)--      getClauses cxt name tyvars locTyvars (RecGadtC cNames cVarTypes _-                                            : constrs) =-        do clauses1 <--             forM cNames $ \cName ->-             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))-           clauses2 <- getClauses cxt name tyvars locTyvars constrs-           return (clauses1 ++ clauses2)-#endif--      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 -       -}

@@ -1,42 +0,0 @@--- |--- Module      : Data.Binding.Hobbits.PatternParser--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ Using the haskell-src-meta package to parse Haskell patterns.--module Data.Binding.Hobbits.PatternParser (parsePattern) where--import Language.Haskell.TH--import qualified Language.Haskell.Exts.Parser as Meta--import qualified Language.Haskell.Meta.Parse as Meta--import qualified Language.Haskell.Meta.Parse as Sloppy-import qualified Language.Haskell.Meta.Syntax.Translate as Translate--import qualified Language.Haskell.Exts.Extension as Exts--#if MIN_VERSION_haskell_src_exts(1,14,0)-parsePatternExtensions =-  map Exts.EnableExtension $ Exts.ViewPatterns : Sloppy.myDefaultExtensions-#else-parsePatternExtensions = Exts.ViewPatterns : Sloppy.myDefaultExtensions-#endif------parsePattern :: String -> String -> Either String Pat-parsePattern fn =-  fmap Translate.toPat . Meta.parseResultToEither .-  Meta.parsePatWithMode (Sloppy.myDefaultParseMode-                    {Meta.parseFilename = fn,-                     Meta.extensions = parsePatternExtensions })

@@ -1,148 +0,0 @@-{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}---- |--- Module      : Data.Binding.Hobbits.QQ--- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner------ License     : BSD3------ Maintainer  : emw4@rice.edu--- Stability   : experimental--- Portability : GHC------ Defines a quasi-quoter for writing patterns that match the bodies of 'Mb'--- multi-bindings. Uses the haskell-src-exts parser. @[nuP| P ]@ defines a--- pattern that will match a multi-binding whose body matches @P@. Any--- variables matched by @P@ will remain inside the binding; thus, for example,--- in the pattern @[nuP| x |]@, @x@ matches the entire multi-binding.------ Examples:------ > case (nu Left) of [nuP| Left x |] -> x  ==  nu id------ @[clP| P |]@ does the same for the 'Closed' type, and @[clNuP| P |]@ works--- for both simultaneously: @'Closed' ('Mb' ctx a)@.--module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where--import Language.Haskell.TH.Syntax as TH-import Language.Haskell.TH.Ppr as TH-import Language.Haskell.TH.Quote--import qualified Data.Generics as SYB-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 =-  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat}---- | 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}---- | Apply a 'WrapKit' to a pattern-wrapVars :: Monad m => WrapKit -> Pat -> m 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 'varView' function is ever used-    hit x = tell (Any True) >> return x--    -- wraps up bound names-    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 varView $ AsP v $ asXform p-    -- requires the expression to be closed-    w (ViewP (VarE n) p) = return $ ViewP (VarE 'unClosed `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-  case parsePattern fn s of-    Left e -> error $ "Parse error: `" ++ e ++-      "'\n\n\t when parsing pattern: `" ++ s ++ "'."-    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---- | 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-  topVar <- newName "topMb"-  namesVar <- newName "topNames"-  parseHere s >>= wrapVars (nuKit topVar namesVar)---- | Builds a 'WrapKit' for parsing patterns that match over 'Closed'-clKit = WrapKit {_varView = ConE 'Closed, _asXform = asXform, _topXform = const asXform}-  where asXform p = ConP 'Closed [p]---- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit'-clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere---- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@-clNuP = patQQ "clNuP" $ \s -> do-  topVar <- newName "topMb"-  namesVar <- newName "topNames"-  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)

@@ -1,208 +0,0 @@-{-# 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.-mapRListLookup :: Member c a -> MapRList f c -> f a-mapRListLookup Member_Base (_ :>: x) = x-mapRListLookup (Member_Step mem') (mc :>: _) = mapRListLookup mem' mc---mapRListLookup _ _ = error "Should not happen! (mapRListLookup)"---- | 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,4 +1,4 @@-Copyright (c) 2014, Eddy Westbrook, Nicolas Frisby, Paul Brauner+Copyright (c) 2014, Eddy Westbrook All rights reserved.  Redistribution and use in source and binary forms, with or without modification,

@@ -1,5 +1,5 @@ Name:                hobbits-Version:             1.2.4+Version:             1.3 Synopsis:            A library for canonically representing terms with binding  Description: A library for canonically representing terms with binding via a@@ -13,28 +13,32 @@  Category:            Data Structures -Cabal-version: >= 1.6.0.1+Cabal-version: >= 1.10 Build-Type:    Simple  extra-source-files: CHANGELOG  Library-  Build-Depends: base >= 4.7 && < 5-  Build-Depends: template-haskell >= 2.9 && < 2.13--  Build-Depends: syb-  Build-Depends: mtl--  Build-Depends: tagged-  Build-Depends: deepseq--  Build-Depends: haskell-src-exts >= 1.17.1 && < 1.20, haskell-src-meta,-                 th-expand-syns >= 0.3 && < 0.5, transformers+  build-depends:+      base >= 4.7 && < 5+    , template-haskell >= 2.11 && < 3+    , syb+    , mtl+    , tagged+    , deepseq+    , haskell-src-exts >= 1.17.1 && < 2+    , haskell-src-meta+    , th-expand-syns >= 0.3 && < 0.5+    , transformers+    , containers+    , vector    GHC-Options: -fwarn-incomplete-patterns -fwarn-unused-imports -  Extensions: CPP+  hs-source-dirs: src +  default-language: Haskell2010+   Exposed-Modules: Data.Type.RList,                     Data.Binding.Hobbits,@@ -42,9 +46,13 @@                    Data.Binding.Hobbits.Closed,                    Data.Binding.Hobbits.QQ,                    Data.Binding.Hobbits.Liftable,+                   Data.Binding.Hobbits.MonadBind,+                   Data.Binding.Hobbits.NameMap,+                   Data.Binding.Hobbits.NameSet,                     Data.Binding.Hobbits.PatternParser,                    Data.Binding.Hobbits.NuMatching,+                   Data.Binding.Hobbits.NuMatchingInstances,                     Data.Binding.Hobbits.Examples.LambdaLifting,                    Data.Binding.Hobbits.Examples.LambdaLifting.Terms,

@@ -0,0 +1,60 @@+{-# LANGUAGE TypeOperators #-}++-- |+-- Module      : Data.Binding.Hobbits+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This library implements multi-bindings as described in the paper+-- E. Westbrook, N. Frisby, P. Brauner, \"Hobbits for Haskell: A Library for+-- Higher-Order Encodings in Functional Programming Languages\".++module Data.Binding.Hobbits (+  -- * Values under multi-bindings+  module Data.Binding.Hobbits.Mb,+  -- | The 'Data.Binding.Hobbits.Mb.Mb' type modeling multi-bindings is the+  -- central abstract type of the library++  -- * Closed terms+  module Data.Binding.Hobbits.Closed,+  -- | The 'Data.Binding.Hobbits.Closed.Cl' type models+  -- super-combinators, which are safe functions to apply under+  -- 'Data.Binding.Hobbits.Mb.Mb'.++  -- * Pattern-matching multi-bindings and closed terms+  module Data.Binding.Hobbits.QQ,+  -- | The 'Data.Binding.Hobbits.QQ.nuP' quasiquoter allows safe pattern+  -- matching on 'Data.Binding.Hobbits.Mb.Mb'+  -- values. 'Data.Binding.Hobbits.QQ.superCombP' is similar.++  -- * Lifting values out of multi-bindings+  module Data.Binding.Hobbits.Liftable,++  -- * Ancilliary modules+  module Data.Proxy, module Data.Type.Equality,+  -- | Type lists track the types of bound variables.++  --module Data.Type.RList,+  RList(..), RAssign(..), Member(..), (:++:), Append(..),+  -- | The "Data.Binding.Hobbits.NuMatching" module exposes the NuMatching+  -- class, which allows pattern-matching on (G)ADTs in the bodies of+  -- multi-bindings+  module Data.Binding.Hobbits.NuMatching,+  module Data.Binding.Hobbits.NuMatchingInstances++                            ) where++import Data.Proxy+import Data.Type.Equality+import Data.Type.RList (RList(..), RAssign(..), Member(..), (:++:), Append(..))+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.Closed+import Data.Binding.Hobbits.QQ+import Data.Binding.Hobbits.Liftable+import Data.Binding.Hobbits.NuMatching+import Data.Binding.Hobbits.NuMatchingInstances()

@@ -0,0 +1,121 @@+{-# LANGUAGE TemplateHaskell, ViewPatterns, PolyKinds, GADTs, PatternGuards #-}++-- |+-- 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 uses Template Haskell to distinguish closed terms, so that the+-- library can trust such functions to not contain any @Name@ values in their+-- closure.++module Data.Binding.Hobbits.Closed (+  -- * Abstract types+  Closed(),+  -- * Operators involving 'Closed'+  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl, unsafeClose,+  -- * Typeclass for inherently closed types+  Closable(..)+) where++import Data.Proxy+import Data.Type.RList+import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Internal.Mb+import Data.Binding.Hobbits.Internal.Closed+import Data.Binding.Hobbits.Mb++-- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its+-- multi-binding.+noClosedNames :: Closed (Name a) -> b+noClosedNames (Closed 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."++-- | Closed terms are closed (sorry) under application.+clApply :: Closed (a -> b) -> Closed a -> Closed b+-- could be defined with cl were it not for the GHC stage restriction+clApply (Closed f) (Closed a) = Closed (f a)++-- | Closed multi-bindings are also closed under application.+clMbApply :: Closed (Mb ctx (a -> b)) -> Closed (Mb ctx a) ->+             Closed (Mb ctx b)+clMbApply (Closed f) (Closed a) = Closed (mbApply f a)++-- | When applying a closed function, the argument can be viewed as locally+-- closed+clApplyCl :: Closed (Closed a -> b) -> Closed a -> Closed b+clApplyCl (Closed f) a = Closed (f a)++-- | FIXME: this should not be possible!!+closeBug :: a -> Closed a+closeBug = $([| \x -> $(mkClosed [| x |]) |])++-- | Mark an object as closed without actually traversing it. This is unsafe if+-- the object does in fact contain any names.+unsafeClose :: a -> Closed a+unsafeClose = Closed++-- | Typeclass for inherently closed types+class Closable a where+  toClosed :: a -> Closed a++instance Closable Integer where+  toClosed i = Closed i++instance Closable (Member ctx a) where+  -- NOTE: this is actually definable with mkClosed, but this is more efficient+  toClosed memb = Closed memb++instance Closable (Proxy a) where+  toClosed Proxy = $(mkClosed [| Proxy |])++instance Closable (Closed a) where+  toClosed = clApplyCl $(mkClosed [| id |])++instance Closable Bool where+  toClosed True = $(mkClosed [| True |])+  toClosed False = $(mkClosed [| False |])++instance Closable Char where+  toClosed = unsafeClose++instance Closable Int where+  toClosed = unsafeClose++instance Closable a => Closable [a] where+  toClosed [] = $(mkClosed [| [] |])+  toClosed (a:as) =+    $(mkClosed [| (:) |]) `clApply` toClosed a `clApply` toClosed as++-- | Object-level reification of the 'Closable' typeclass+data IsClosable a where IsClosable :: Closable a => IsClosable a++-- | Type functors @f@ where @f a@ is always 'Closable' for any @a@+class ClosableAny1 f where+  closableAny1 :: f a -> IsClosable (f a)++-- | Helper function to use the proof returned by 'closableAny1'+toClosedAny1 :: ClosableAny1 f => f a -> Closed (f a)+toClosedAny1 x | IsClosable <- closableAny1 x = toClosed x++instance ClosableAny1 Proxy where+  closableAny1 _ = IsClosable++instance ClosableAny1 (Member ctx) where+  closableAny1 _ = IsClosable++instance ClosableAny1 f => Closable (RAssign f ctx) where+  toClosed MNil = $(mkClosed [| MNil |])+  toClosed (xs :>: x) =+    $(mkClosed [| (:>:) |]) `clApply` toClosed xs `clApply` toClosedAny1 x

@@ -0,0 +1,231 @@+{-# LANGUAGE QuasiQuotes, ViewPatterns #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators, DataKinds #-}+{-# LANGUAGE GADTs #-}++{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}++-- |+-- Module      : Data.Binding.Hobbits.Examples.LambdaLifting+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- The lambda lifting example from the paper E. Westbrook, N. Frisby,+-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in+-- Functional Programming Languages\".++-------------------------------------------------------------------------+-- lambda lifting for the lambda calculus with top-level declarations+-------------------------------------------------------------------------++module Data.Binding.Hobbits.Examples.LambdaLifting (+  -- * Term data types, using 'Data.Binding.Hobbits.Mb'+  module Data.Binding.Hobbits.Examples.LambdaLifting.Terms,+  -- * The lambda-lifting function+  lambdaLift, mbLambdaLift+  ) where++import Data.Binding.Hobbits+import qualified Data.Type.RList as C++import Data.Binding.Hobbits.Examples.LambdaLifting.Terms++-- imported for ease of use at terminal+import Data.Binding.Hobbits.Examples.LambdaLifting.Examples++import Control.Monad.Cont (Cont, runCont, cont)++------------------------------------------------------------+-- "peeling" lambdas off of a term+------------------------------------------------------------++data LType a where LType :: LType (L a)+type LC c = RAssign LType c++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+  PeelRet :: lc ~ (lc0 :> b) => LC lc -> Mb (c :++: lc) (Term a) ->+             PeelRet c (AddArrows lc a)++peelLambdas :: Mb c (Binding (L b) (Term a)) -> PeelRet c (b -> a)+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+++++boundParams ::+  lc ~ (lc0 :> b) => LC lc -> (RAssign 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 -> (RAssign 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 = RAssign Name c -> RAssign Name c'++------------------------------------------------------------+-- operations on contexts of free variables+------------------------------------------------------------++data MbLName c a where+    MbLName :: Mb c (Name (L a)) -> MbLName c (L a)++type FVList c fvs = RAssign (MbLName c) fvs++-- unioning free variable contexts: the data structure+data FVUnionRet c fvs1 fvs2 where+    FVUnionRet :: FVList c fvs -> SubC fvs1 fvs -> SubC fvs2 fvs ->+                  FVUnionRet c fvs1 fvs2++fvUnion :: FVList c fvs1 -> FVList c fvs2 -> FVUnionRet c fvs1 fvs2+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.get 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.get idx xs) f2++elemMC :: MbLName c a -> FVList c fvs -> Maybe (Member fvs a)+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)++------------------------------------------------------------+-- deBruijn terms, i.e., closed terms+------------------------------------------------------------++data STerm c a where+    SWeaken :: SubC c1 c -> STerm c1 a -> STerm c a+    SVar :: Member c (L a) -> STerm c a+    SDVar :: Name (D a) -> STerm c a+    SApp :: STerm c (a -> b) -> STerm c a -> STerm c b++skelSubst :: STerm c a -> RAssign Name c -> DTerm a+skelSubst (SWeaken f db) names = skelSubst db $ f names+skelSubst (SVar inC) names = TVar $ C.get inC names+skelSubst (SDVar dTVar) _ = TDVar dTVar+skelSubst (SApp db1 db2) names = TApp (skelSubst db1 names) (skelSubst db2 names)++-- applying a STerm to a context of names+skelAppMultiNames ::+  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 -> RAssign (Member fvs) args ->+    STerm fvs a+  skelAppMultiNamesH fvs MNil _ = fvs+  -- flagged as non-exhaustive, in spite of type+  skelAppMultiNamesH fvs (args :>: MbLName _) (inCs :>: inC) =+    SApp (skelAppMultiNamesH fvs args inCs) (SVar inC)++------------------------------------------------------------+-- STerms combined with their free variables+------------------------------------------------------------++proxyCons :: Proxy r -> f a -> Proxy (r :> a)+proxyCons _ _ = Proxy++data FVSTerm c lc a where+    FVSTerm :: FVList c fvs -> STerm (fvs :++: lc) a -> FVSTerm c lc a++fvSSepLTVars ::+  RAssign 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 'RAssign' vector.+proxyOfRAssign :: RAssign f c -> Proxy c+proxyOfRAssign _ = Proxy++fvSSepLTVarsH ::+  RAssign 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.get (C.weakenMemberL (proxyOfRAssign m) idx) xs)+    Right n ->+      SepRet (m :>: MbLName n)+      (\xs -> case C.split c' lc xs of+          (fvs' :>: fv', lcs) ->+            f (C.append fvs' lcs) :>: fv')+    where c' = proxyCons (proxyOfRAssign m) fv++raiseAppName ::+  Append c1 c2 (c1 :++: c2) -> Mb (c1 :++: c2) (Name a) -> Either (Member c2 a) (Mb c1 (Name a))+raiseAppName app n =+  case fmap mbNameBoundP (mbSeparate (C.proxiesFromAppend app) n) of+    [nuP| Left mem |] -> Left $ mbLift mem+    [nuP| Right n |] -> Right n++------------------------------------------------------------+-- lambda-lifting, woo hoo!+------------------------------------------------------------++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 (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+  FVUnionRet names sub1 sub2 <- return $ fvUnion fvs1 fvs2+  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+  FVSTerm fvs db <- return $ fvSSepLTVars lc llret+  cont $ \k ->+    Decls_Cons (freeParams (fvsToLC fvs) $ \names1 ->+                boundParams lc $ \names2 ->+                skelSubst db (C.append names1 names2))+      $ nu $ \d -> k $ FVSTerm fvs (skelAppMultiNames (SDVar d) fvs)+  where+    fvsToLC :: FVList c lc -> LC lc+    fvsToLC = C.mapRAssign 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 MNil (emptyMb t)) $ \(FVSTerm fvs db) ->+  Decls_Base (skelSubst db (C.mapRAssign (\(MbLName mbn) -> elimEmptyMb mbn) fvs))++mbLambdaLift :: Mb c (Term a) -> Mb c (Decls a)+mbLambdaLift = fmap lambdaLift

@@ -0,0 +1,52 @@+-- |+-- Module      : Data.Binding.Hobbits.SuperComb+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--++module Data.Binding.Hobbits.Examples.LambdaLifting.Examples where++import Data.Binding.Hobbits.Examples.LambdaLifting.Terms+import Data.Binding.Hobbits++------------------------------------------------------------+-- examples+------------------------------------------------------------++ex1 :: Term ((b1 -> b) -> b1 -> b)+ex1 = lam (\f -> (lam $ \x -> App f x))++ex2 :: Term ((((b2 -> b1) -> b2 -> b1) -> b) -> b)+ex2 = lam (\f1 -> App f1 (lam (\f2 -> lam (\x -> App f2 x))))++ex3 :: Term (b3 -> (((b3 -> b2 -> b1) -> b2 -> b1) -> b) -> b)+ex3 = lam (\x -> lam (\f1 -> App f1 (lam (\f2 -> lam (\y -> f2 `App` x `App` y)))))++ex4+  :: Term+       (((b1 -> b) -> b2 -> b)+        -> (((b1 -> b) -> b2 -> b) -> b2 -> b1)+        -> b2+        -> b1)+ex4 = lam $ \x -> lam $ \f1 ->+      App f1 (lam $ \f2 -> lam $ \y -> f2 `App` (f1 `App` x `App` y))++ex5 :: Term (((b2 -> b1) -> b) -> (b2 -> b1) -> b)+ex5 = lam (\f1 -> lam $ \f2 -> App f1 (lam $ \x -> App f2 x))++-- lambda-lift with a free variable (use mbLambdaLift)+ex6 :: Binding (L ((b -> b) -> a)) (Term a)+ex6 = nu (\f -> App (Var f) (lam $ \x -> x))++-- lambda-lift with a free variable as part of a lambda's environment+ex7 :: Binding (L ((b2 -> b2) -> b1)) (Term ((b1 -> b) -> b))+ex7 = nu (\f -> lam $ \y -> App y $ App (Var f) (lam $ \x -> x))++-- example from paper's Section 4+exP :: Term (((b1 -> b1) -> b) -> (b1 -> b1) -> b)+exP = lam $ \f -> lam $ \g -> App f $ lam $ \x -> App g $ App g x

@@ -0,0 +1,133 @@+{-# LANGUAGE EmptyDataDecls #-}+{-# LANGUAGE TemplateHaskell, Rank2Types, QuasiQuotes, ViewPatterns #-}+{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}++-- |+-- Module      : Data.Binding.Hobbits.SuperComb+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--++module Data.Binding.Hobbits.Examples.LambdaLifting.Terms+  (L, D,+   Term(..), lam,+   DTerm(..), Decl(..), Decls(..)+  ) where++import Data.Binding.Hobbits+import qualified Data.Type.RList as C++-- dummy datatypes for distinguishing Decl names from Lam names+data L a+data D a++-- to make a function for RAssign (for pretty)+newtype StringF x = StringF String+unStringF (StringF str) = str+++------------------------------------------------------------+-- source terms+------------------------------------------------------------++-- Term datatype; no Ds since there's no declarations yet+data Term :: * -> * where+  Var :: Name (L a) -> Term a+  Lam :: Binding (L b) (Term a) -> Term (b -> a)+  App :: Term (b -> a) -> Term b -> Term a++$(mkNuMatching [t| forall a . Term a |])++instance Show (Term a) where show = tpretty++-- helps to build terms without explicitly using nu or Var+lam :: (Term a -> Term b) -> Term (a -> b)+lam f = Lam $ nu (f . Var)++-- pretty print terms+tpretty :: Term a -> String+tpretty t = pretty' (emptyMb t) C.empty 0+  where pretty' :: Mb c (Term a) -> RAssign StringF c -> Int -> String+        pretty' [nuP| Var b |] varnames n =+            case mbNameBoundP b of+              Left pf  -> unStringF (C.get 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) ++ ")"+        pretty' [nuP| App b1 b2 |] varnames n =+            "(" ++ pretty' b1 varnames n ++ " " ++ pretty' b2 varnames n ++ ")"++------------------------------------------------------------+-- target terms+------------------------------------------------------------++-- terms under declarations+data DTerm :: * -> * where+  TVar :: Name (L a) -> DTerm a+  TDVar :: Name (D a) -> DTerm a+  TApp :: DTerm (a -> b) -> DTerm a -> DTerm b++-- we use this type for a definiens instead of putting lambdas on the front+data Decl :: * -> * where+  Decl_One :: Binding (L a) (DTerm b) -> Decl (a -> b)+  Decl_Cons :: Binding (L a) (Decl b) -> Decl (a -> b)++-- top-level declarations with a return value+data Decls :: * -> * where+  Decls_Base :: DTerm a -> Decls a+  Decls_Cons :: Decl b -> Binding (D b) (Decls a) -> Decls a++$(mkNuMatching [t| forall a . DTerm a |])+$(mkNuMatching [t| forall a . Decl a |])+$(mkNuMatching [t| forall a . Decls a |])++instance Show (DTerm a) where show = pretty+instance Show (Decls a) where show = decls_pretty++------------------------------------------------------------+-- pretty printing+------------------------------------------------------------++-- pretty print terms+pretty :: DTerm a -> String+pretty t = mpretty (emptyMb t) C.empty++mpretty :: Mb c (DTerm a) -> RAssign StringF c -> String+mpretty [nuP| TVar b |] varnames =+    mprettyName (mbNameBoundP b) varnames+mpretty [nuP| TDVar b |] varnames =+    mprettyName (mbNameBoundP b) varnames+mpretty [nuP| TApp b1 b2 |] varnames =+    "(" ++ mpretty b1 varnames+        ++ " " ++ mpretty b2 varnames ++ ")"++mprettyName (Left pf) varnames = unStringF (C.get pf varnames)+mprettyName (Right n) varnames = "(free-var " ++ (show n) ++ ")"+        ++-- pretty print decls+decls_pretty :: Decls a -> String+decls_pretty decls =+    "let\n" ++ (mdecls_pretty (emptyMb decls) C.empty 0)++mdecls_pretty :: Mb c (Decls a) -> RAssign 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)++mdecl_pretty :: Mb c (Decl a) -> RAssign 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)+mdecl_pretty [nuP| Decl_Cons d|] varnames n =+  let vname = "x" ++ show n in+  vname ++ " " ++ mdecl_pretty (mbCombine d) (varnames :>: StringF vname) (n+1)

@@ -0,0 +1,73 @@+{-# 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++import Language.Haskell.TH (Q, Exp(..), Type(..))+import qualified Language.Haskell.TH as TH+import qualified Language.Haskell.TH.ExpandSyns as TH++import qualified Data.Generics as SYB+import qualified Language.Haskell.TH.Syntax as TH++{-| The type @Closed 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 @Closed@ data type is hidden, and the+user can only create closed terms using Template Haskell, through the 'mkClosed'+operator. -}+newtype Closed a =+  Closed {+  -- | Extract the value of a 'Closed' object+  unClosed :: a+  }++-- | Extract the type of an 'Info' object+reifyNameType :: TH.Name -> Q Type+reifyNameType n =+  TH.reify n >>= \i ->+  case i of+    TH.VarI _ ty _ -> return ty+    _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."++-- | @mkClosed@ is used with Template Haskell quotations to create closed terms+-- of type 'Closed'. A quoted expression is closed if all of the names occuring in+-- it are either:+--+--   1) bound globally or+--   2) bound within the quotation or+--   3) also of type 'Closed'.+mkClosed :: Q Exp -> Q Exp+mkClosed e = AppE (ConE 'Closed) `fmap` e >>= SYB.everywhereM (SYB.mkM w) where+  w e@(VarE n@(TH.Name _ flav)) = case flav of+    TH.NameG {} -> return e -- bound globally+    TH.NameU {} -> return e -- bound locally within this quotation+    TH.NameL {} -> closed n >> return e -- bound locally outside this quotation+    _ -> fail $ "`mkClosed' does not allow dynamically bound names: `"+      ++ show n ++ "'."+  w e = return e++  closed n = do+    ty <- reifyNameType n+    TH.expandSyns ty >>= w ty+      where+        w _ (AppT (ConT m) _) | m == ''Closed = return ()+        w top_ty (ForallT _ _ ty') = w top_ty ty'+        w top_ty _ =+          fail $ "`mkClosed` requires non-global variables to have type `Closed'.\n\t`"+          ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"+          ++ show (TH.ppr top_ty) ++ "'."

@@ -0,0 +1,97 @@+{-# LANGUAGE GADTs, DeriveDataTypeable, ViewPatterns #-}+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}++-- |+-- 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.RList hiding (map)++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 @'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+  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 :: RList k) b+    = MkMbFun (RAssign Proxy ctx) (RAssign Name ctx -> b)+    | MkMbPair (MbTypeRepr b) (RAssign 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. NameRefresher -> 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 -> NameRefresher -> a -> a+mapNamesPf MbTypeReprName refresher n = refreshName refresher n+mapNamesPf (MbTypeReprMb tRepr) refresher (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 refresher (f ns))+mapNamesPf (MbTypeReprFun tReprIn tReprOut) refresher f =+    (mapNamesPf tReprOut refresher) . f . (mapNamesPf tReprIn refresher)+mapNamesPf (MbTypeReprData (MkMbTypeReprData mapFun)) refresher x =+    mapFun refresher x+++-- | Ensures a multi-binding is in "fresh function" form+ensureFreshFun :: Mb ctx a -> (RAssign Proxy ctx, RAssign Name ctx -> a)+ensureFreshFun (MkMbFun proxies f) = (proxies, f)+ensureFreshFun (MkMbPair tRepr ns body) =+    (mapRAssign (\_ -> Proxy) ns, \ns' ->+      mapNamesPf tRepr (mkRefresher ns ns') body)++-- | Ensures a multi-binding is in "fresh pair" form+ensureFreshPair :: Mb ctx a -> (RAssign Name ctx, a)+ensureFreshPair (MkMbPair _ ns body) = (ns, body)+ensureFreshPair (MkMbFun proxies f) =+    let ns = mapRAssign (MkName . fresh_name) proxies in+    (ns, f ns)

@@ -0,0 +1,167 @@+{-# LANGUAGE GADTs, DeriveDataTypeable, FlexibleInstances, TypeOperators #-}+{-# LANGUAGE RankNTypes, DataKinds, PolyKinds #-}++-- |+-- 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.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Data.Type.Equality+import Unsafe.Coerce (unsafeCoerce)+import Data.IORef (IORef, newIORef, readIORef, writeIORef)+import System.IO.Unsafe (unsafePerformIO)++import Data.Type.RList+++-- | A @Name a@ is a bound name that is associated with type @a@.+newtype Name (a :: k) = MkName Int deriving (Typeable, Eq, Ord)++instance Show (Name a) where+  showsPrec _ (MkName n) = showChar '#' . shows n . showChar '#'++instance Show (RAssign Name c) where+    show names = "[" ++ (concat $ intersperse "," $ mapToList 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++instance TestEquality Name where+  testEquality = cmpName++-- | Heterogeneous comparison of names, that could be at different kinds+hcmpName :: forall (a :: k1) (b :: k2). Name a -> Name b -> Maybe (a :~~: b)+hcmpName (MkName n1) (MkName n2)+  | n1 == n2 = Just $ unsafeCoerce HRefl+  | otherwise = Nothing++-- | A name refresher gives new fresh indices to names+newtype NameRefresher = NameRefresher { unNameRefresher :: IntMap Int }++-- | Apply a 'NameRefresher' to a 'Name'+refreshName :: NameRefresher -> Name a -> Name a+refreshName (NameRefresher nmap) (MkName i) =+  MkName $ IntMap.findWithDefault i i nmap++-- | Build a 'NameRefresher' that maps one sequence of names to another+mkRefresher :: forall (ctx :: RList k) .+               RAssign Name ctx -> RAssign Name ctx -> NameRefresher+mkRefresher ns1 ns2 =+  NameRefresher $ IntMap.fromList $ toList $+  map2 (\(MkName i) (MkName j) -> Constant (i,j)) ns1 ns2++-- | Extend a 'NameRefresher' with one more name mapping+extRefresher :: forall (a :: k). NameRefresher -> Name a -> Name a ->+                NameRefresher+extRefresher (NameRefresher nmap) (MkName n1) (MkName n2) =+  NameRefresher $+  IntMap.insertWith (\_ _ -> error "Hobbit name already in NameRefresher!")+  n1 n2 nmap+++-------------------------------------------------------------------------------+-- 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 :: RAssign Proxy ctx -> ExProxy+proxyFromLen :: Int -> ExProxy+proxyFromLen 0 = ExProxy MNil+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)

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

@@ -0,0 +1,154 @@+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, TemplateHaskell #-}+{-# LANGUAGE ViewPatterns, QuasiQuotes, DataKinds, PolyKinds #-}++-- |+-- Module      : Data.Binding.Hobbits.Mb+-- Copyright   : (c) 2014 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines the type-class Liftable for lifting+-- non-binding-related data out of name-bindings. Note that this code+-- is not "trusted", i.e., it is not part of the name-binding+-- abstraction: instead, it is all written using the primitives+-- exported by the Mb++module Data.Binding.Hobbits.Liftable where++import Data.Type.RList+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.Internal.Mb+import Data.Binding.Hobbits.QQ+import Data.Binding.Hobbits.Closed+import Data.Binding.Hobbits.NuMatching+import Data.Binding.Hobbits.NuMatchingInstances++import Data.Ratio+import Data.Proxy+import Numeric.Natural+import Data.Type.Equality+++{-|+  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 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 (ensureFreshPair -> (_, i)) = i++instance Liftable Integer where+    mbLift (ensureFreshPair -> (_, i)) = i++instance Liftable (Closed a) where+    mbLift (ensureFreshPair -> (_, c)) = c++instance Liftable Natural where+    mbLift (ensureFreshPair -> (_, i)) = i+++-------------------------------------------------------------------------------+-- * 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+instance Liftable (Member c a) where+    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++instance (Integral a, NuMatching a) => NuMatching (Ratio a) where+  nuMatchingProof =+    isoMbTypeRepr (\r -> (numerator r, denominator r)) (\(n,d) -> n%d)+instance (Integral a, Liftable a) => Liftable (Ratio a) where+  mbLift mb_r =+    (\(n,d) -> n%d) $ mbLift $ fmap (\r -> (numerator r, denominator r)) mb_r++instance Liftable a => Liftable [a] where+    mbLift [nuP| [] |] = []+    mbLift [nuP| x : xs |] = (mbLift x) : (mbLift xs)++instance Liftable () where+    mbLift [nuP| () |] = ()++instance (Liftable a, Liftable b) => Liftable (a,b) where+    mbLift [nuP| (x,y) |] = (mbLift x, mbLift y)++instance Liftable Bool where+  mbLift [nuP| True |] = True+  mbLift [nuP| False |] = False++instance Liftable a => Liftable (Maybe a) where+  mbLift [nuP| Nothing |] = Nothing+  mbLift [nuP| Just mb_a |] = Just $ mbLift mb_a++instance (Liftable a, Liftable b) => Liftable (Either a b) where+  mbLift [nuP| Left mb_a |] = Left $ mbLift mb_a+  mbLift [nuP| Right mb_b |] = Right $ mbLift mb_b++instance Liftable (a :~: b) where+  mbLift [nuP| Refl |] = Refl++instance Liftable (Proxy (a :: k)) where+  mbLift [nuP| Proxy |] = Proxy++-- Ideally this would be in the Mb module, but that ends up producing a circular+-- include due to needing `mbLift`+instance Eq a => Eq (Mb ctx a) where+  mb1 == mb2 =+    mbLift $ nuMultiWithElim (\_ (_ :>: a1 :>: a2) ->+                               a1 == a2) (MNil :>: mb1 :>: mb2)++++-- README: these lead to overlapping instances...++{-++{-|+  The class @Liftable1 f@ gives a lifting function for each type @f a@+  when @a@ itself is @Liftable@.+-}+class Liftable1 f where+    mbLift1 :: Liftable a => Mb ctx (f a) -> f a++instance (Liftable1 f, Liftable a) => Liftable (f a) where+    mbLift = mbLift1++instance Liftable1 [] where+    mbLift1 [nuP| [] |] = []+    mbLift1 [nuP| x : xs |] = (mbLift x) : (mbLift1 xs)++{-|+  The class @Liftable2 f@ gives a lifting function for each type @f a b@+  when @a@ and @b@ are @Liftable@.+-}+class Liftable2 f where+    mbLift2 :: (Liftable a, Liftable b) => Mb ctx (f a b) -> f a b++instance Liftable2 (,) where+    mbLift2 [nuP| (x,y) |] = (mbLift x, mbLift y)++instance (Liftable2 f, Liftable a) => Liftable1 (f a) where+    mbLift1 = mbLift2++-}

@@ -0,0 +1,324 @@+{-# LANGUAGE GADTs, TypeOperators, FlexibleInstances, ViewPatterns, DataKinds #-}+{-# LANGUAGE RankNTypes, PolyKinds #-}++-- |+-- Module      : Data.Binding.Hobbits.Mb+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines multi-bindings as the type 'Mb', as well as a number of+-- operations on multi-bindings. See the paper E. Westbrook, N. Frisby,+-- P. Brauner, \"Hobbits for Haskell: A Library for Higher-Order Encodings in+-- Functional Programming Languages\" for more information.++module Data.Binding.Hobbits.Mb (+  -- * Abstract types+  Name(),      -- hides Name implementation+  Binding(),   -- hides Binding implementation+  Mb(),        -- hides MultiBind implementation+  -- * Multi-binding constructors+  nu, nuMulti, nus, emptyMb, extMb, extMbMulti,+  -- * Queries on names+  cmpName, hcmpName, mbNameBoundP, mbCmpName,+  -- * Operations on multi-bindings+  elimEmptyMb, mbCombine, mbSeparate, mbToProxy, mbSwap, mbPure, mbApply,+  mbMap2,+  -- * Eliminators for multi-bindings+  nuMultiWithElim, nuWithElim, nuMultiWithElim1, nuWithElim1+) where++import Control.Applicative+import Control.Monad.Identity++import Data.Type.Equality ((:~:)(..))+import Data.Proxy (Proxy(..))++import Unsafe.Coerce (unsafeCoerce)++import Data.Type.RList++import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Internal.Mb+--import qualified Data.Binding.Hobbits.Internal as I++-------------------------------------------------------------------------------+-- creating bindings+-------------------------------------------------------------------------------++-- | A @Binding@ is simply a multi-binding that binds one name+type Binding (a :: k) = Mb (RNil :> a)++-- note: we reverse l to show the inner-most bindings last+instance Show a => Show (Mb c a) where+  showsPrec p (ensureFreshPair -> (names, b)) = showParen (p > 10) $+    showChar '#' . shows names . showChar '.' . shows b++{-|+  @nu f@ creates a binding which binds a fresh name @n@ and whose+  body is the result of @f n@.+-}+nu :: forall (a :: k1) (b :: *) . (Name a -> b) -> Binding a b+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 @'RAssign' 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 :: RAssign f ctx -> (RAssign Name ctx -> b) -> Mb ctx b+nuMulti proxies f = MkMbFun (mapRAssign (const Proxy) proxies) f++-- | @nus = nuMulti@+nus x = nuMulti x++-- | Extend the context of a name-binding by adding a single type+extMb :: Mb ctx a -> Mb (ctx :> tp) a+extMb = mbCombine . fmap (nu . const)++-- | Extend the context of a name-binding with multiple types+extMbMulti :: RAssign f ctx2 -> Mb ctx1 a -> Mb (ctx1 :++: ctx2) a+extMbMulti ns mb = mbCombine $ fmap (nuMulti ns . const) mb+++-------------------------------------------------------------------------------+-- Queries on Names+-------------------------------------------------------------------------------++{-|+  Checks if a name is bound in a multi-binding, returning @Left mem@+  when the name is bound, where @mem@ is a proof that the type of the+  name is in the type list for the multi-binding, and returning+  @Right n@ when the name is not bound, where @n@ is the name.++  For example:++> nu $ \n -> mbNameBoundP (nu $ \m -> m)  ==  nu $ \n -> Left Member_Base+> nu $ \n -> mbNameBoundP (nu $ \m -> n)  ==  nu $ \n -> Right n+-}+mbNameBoundP :: forall (a :: k1) (ctx :: RList k2).+                Mb ctx (Name a) -> Either (Member ctx a) (Name a)+mbNameBoundP (ensureFreshPair -> (names, n)) = helper names n where+    helper :: RAssign 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+  Nothing -> Right (MkName n)+  Just i -> Left (I.unsafeLookupC i)+-}+++{-|+  Compares two names inside bindings, taking alpha-equivalence into+  account; i.e., if both are the @i@th name, or both are the same name+  not bound in their respective multi-bindings, then they compare as+  equal. The return values are the same as for 'cmpName', so that+  @Some Refl@ is returned when the names are equal and @Nothing@ is+  returned when they are not.+-}+mbCmpName :: forall (a :: k1) (b :: k1) (c :: RList k2).+             Mb c (Name a) -> Mb c (Name b) -> Maybe (a :~: b)+mbCmpName (ensureFreshPair -> (names, n1)) (ensureFreshFun -> (_, f2)) =+  cmpName n1 (f2 names)+++-------------------------------------------------------------------------------+-- Operations on multi-bindings+-------------------------------------------------------------------------------++-- | Creates an empty binding that binds 0 names.+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 RNil a -> a+elimEmptyMb (ensureFreshPair -> (_, body)) = body+++-- Extract the proxy objects from an Mb inside of a fresh function+freshFunctionProxies :: RAssign Proxy ctx1 -> (RAssign Name ctx1 -> Mb ctx2 a) ->+                        RAssign Proxy ctx2+freshFunctionProxies proxies1 f =+    case f (mapRAssign (const $ MkName 0) proxies1) of+      MkMbFun proxies2 _ -> proxies2+      MkMbPair _ ns _ -> mapRAssign (const Proxy) ns+++-- README: inner-most bindings come FIRST+-- | Combines a binding inside another binding into a single binding.+mbCombine :: forall (c1 :: RList k) (c2 :: RList k) a b.+             Mb c1 (Mb c2 b) -> Mb (c1 :++: c2) b+mbCombine (MkMbPair tRepr1 l1 (MkMbPair tRepr2 l2 b)) =+  MkMbPair tRepr2 (append 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+    (append proxies1 proxies2)+    (\ns ->+         let (ns1, ns2) = split Proxy proxies2 ns in+         let (_, f2) = ensureFreshFun (f1 ns1) in+         f2 ns2)+++{-|+  Separates a binding into two nested bindings. The first argument, of+  type @'RAssign' any c2@, is a \"phantom\" argument to indicate how+  the context @c@ should be split.+-}+mbSeparate :: forall (ctx1 :: RList k) (ctx2 :: RList k) (any :: k -> *) a.+              RAssign 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) = split Proxy c2 ns+mbSeparate c2 (MkMbFun proxies f) =+    MkMbFun proxies1 (\ns1 -> MkMbFun proxies2 (\ns2 -> f (append ns1 ns2)))+        where+          (proxies1, proxies2) = split Proxy c2 proxies+++-- | Returns a proxy object that enumerates all the types in ctx.+mbToProxy :: forall (ctx :: RList k) (a :: *) .+             Mb ctx a -> RAssign Proxy ctx+mbToProxy (MkMbFun proxies _) = proxies+mbToProxy (MkMbPair _ ns _) = mapRAssign (\_ -> 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))++-- | Put a value inside a multi-binding+mbPure :: RAssign f ctx -> a -> Mb ctx a+mbPure prxs = nuMulti prxs . const++{-|+  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)+++-- | Lift a binary function function to `Mb`s+mbMap2 :: (a -> b -> c) -> Mb ctx a -> Mb ctx b -> Mb ctx c+mbMap2 f mb1 mb2 = fmap f mb1 `mbApply` mb2++-------------------------------------------------------------------------------+-- 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!!+{-|++  asdfasdf++  The expression @nuWithElimMulti args f@ takes a sequence @args@ of one or more+  multi-bindings (it is a runtime error to pass an empty sequence of arguments),+  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.++  For example, here is an alternate way to implement 'mbApply':++> mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b+> mbApply' f a =+>     nuWithElimMulti ('MNil' :>: f :>: a)+>                     (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')+-}+nuMultiWithElim :: (RAssign Name ctx -> RAssign Identity args -> b) ->+                   RAssign (Mb ctx) args -> Mb ctx b+nuMultiWithElim f args =+  let proxies =+        case args of+          MNil -> error "nuMultiWithElim"+          (_ :>: arg1) -> mbToProxy arg1 in+  MkMbFun proxies+          (\ns ->+            f ns $ mapRAssign (\arg ->+                                Identity $ snd (ensureFreshFun arg) ns) args)+++{-|+  Similar to 'nuMultiWithElim' but binds only one name. Note that the argument+  list here is allowed to be empty.+-}+nuWithElim :: (Name a -> RAssign Identity args -> b) ->+              RAssign (Mb (RNil :> a)) args ->+              Binding a b+nuWithElim f MNil = nu $ \n -> f n MNil+nuWithElim f args =+    nuMultiWithElim (\(MNil :>: n) -> f n) args+++{-|+  Similar to 'nuMultiWithElim' but takes only one argument+-}+nuMultiWithElim1 :: (RAssign Name ctx -> arg -> b) -> Mb ctx arg -> Mb ctx b+nuMultiWithElim1 f arg =+    nuMultiWithElim (\names (MNil :>: Identity arg) -> f names arg)+    (MNil :>: 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 (MNil :>: Identity arg) -> f n arg) (MNil :>: arg)

@@ -0,0 +1,102 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module      : Data.Binding.Hobbits.MonadBind+-- Copyright   : (c) 2020 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- This module defines monads that are compatible with the notion of+-- name-binding, where a monad is compatible with name-binding iff it can+-- intuitively run computations that are inside name-bindings. More formally, a+-- /binding monad/ is a monad with an operation 'mbM' that commutes name-binding+-- with the monadic operations, meaning:+--+-- > 'mbM' ('nuMulti' $ \ns -> 'return' a) == 'return' ('nuMulti' $ \ns -> a)+-- > 'mbM' ('nuMulti' $ \ns -> m >>= f)+-- >   == 'mbM' ('nuMulti' $ \ns -> m) >>= \mb_x ->+-- >      'mbM' (('nuMulti' $ \ns x -> f x) `'mbApply'` mb_x)++module Data.Binding.Hobbits.MonadBind (MonadBind(..), MonadStrongBind(..)) where++import Data.Binding.Hobbits.Closed+import Data.Binding.Hobbits.Liftable (mbLift)+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.NuMatching+import Data.Binding.Hobbits.QQ++import Control.Monad.Identity (Identity(..))+import Control.Monad.Reader (ReaderT(..))+import Control.Monad.State (StateT(..), get, lift, put, runStateT)++-- | The class of name-binding monads+class Monad m => MonadBind m where+  mbM :: NuMatching a => Mb ctx (m a) -> m (Mb ctx a)++-- | Bind a name inside a computation and return the name-binding whose body was+-- returned by the computation+nuM :: (MonadBind m, NuMatching b) => (Name a -> m b) -> m (Binding a b)+nuM = mbM . nu++instance MonadBind Identity where+  mbM = Identity . fmap runIdentity++instance MonadBind Maybe where+  mbM [nuP| Just x |] = return x+  mbM [nuP| Nothing |] = Nothing++instance MonadBind m => MonadBind (ReaderT r m) where+  mbM mb = ReaderT $ \r -> mbM $ fmap (flip runReaderT r) mb++-- | A version of 'MonadBind' that does not require a 'NuMatching' instance on+-- the element type of the multi-binding in the monad+class MonadBind m => MonadStrongBind m where+  strongMbM :: Mb ctx (m a) -> m (Mb ctx a)++instance MonadStrongBind Identity where+  strongMbM = Identity . fmap runIdentity++instance MonadStrongBind m => MonadStrongBind (ReaderT r m) where+  strongMbM mb = ReaderT $ \r -> strongMbM $ fmap (flip runReaderT r) mb++-- | State types that can incorporate name-bindings+class NuMatching s => BindState s where+  bindState :: Mb ctx s -> s++instance BindState (Closed s) where+  bindState = mbLift++instance (MonadBind m, BindState s) => MonadBind (StateT s m) where+  mbM mb_m = StateT $ \s ->+    mbM (fmap (\m -> runStateT m s) mb_m) >>= \mb_as ->+    return (fmap fst mb_as, bindState (fmap snd mb_as))++instance (MonadStrongBind m, BindState s) => MonadStrongBind (StateT s m) where+  strongMbM mb_m = StateT $ \s ->+    strongMbM (fmap (\m -> runStateT m s) mb_m) >>= \mb_as ->+    return (fmap fst mb_as, bindState (fmap snd mb_as))+++-- | A monad whose effects are closed+class Monad m => MonadClosed m where+  closedM :: Closed (m a) -> m (Closed a)++instance MonadClosed Identity where+  closedM = Identity . clApply $(mkClosed [| runIdentity |])++instance (MonadClosed m, Closable s) => MonadClosed (StateT s m) where+  closedM clm =+    do s <- get+       cl_a_s <- lift $ closedM ($(mkClosed [| runStateT |]) `clApply` clm+                                 `clApply` toClosed s)+       put (snd $ unClosed cl_a_s)+       return ($(mkClosed [| fst |]) `clApply` cl_a_s)

@@ -0,0 +1,197 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module      : Data.Binding.Hobbits.Mb+-- Copyright   : (c) 2019 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- Implements mappings from 'Name's to some associated data, using+-- 'Data.IntMap.Strict'. Note that these mappings are strict.+--+-- All of the functions in this module operate in an identical manner as those+-- of the same name in the 'Data.IntMap.Strict' module.++module Data.Binding.Hobbits.NameMap (+  NameMap(), NameAndElem(..)+  , empty, singleton, fromList+  , insert, delete, adjust, update, alter+  , lookup, (!), member, null, size+  , union, difference, (\\), intersection+  , map, foldr, foldl+  , assocs+  , liftNameMap+  ) where++import Prelude hiding (lookup, null, map, foldr, foldl)+import qualified Prelude as Prelude (map)+import Data.IntMap.Strict (IntMap)+import qualified Data.IntMap.Strict as IntMap+import Unsafe.Coerce++import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.NuMatching+import Data.Binding.Hobbits.NuMatchingInstances+import Data.Binding.Hobbits.QQ++-- | An element of a 'NameMap', where the name type @a@ is existentially+-- quantified+data NMElem (f :: k -> *) where+  NMElem :: f a -> NMElem f++-- | Coerce an @'NMElem' f@ to an @f a@ for a specific type @a@. This assumes we+-- know that this is the proper type to coerce it to, i.e., it is unsafe.+coerceNMElem :: NMElem f -> f a+coerceNMElem (NMElem x) = unsafeCoerce x++-- | A heterogeneous map from 'Name's of arbitrary type @a@ to elements of @f a@+newtype NameMap (f :: k -> *) =+  NameMap { unNameMap :: IntMap (NMElem f) }++-- | Internal-only helper function for mapping a unary function on 'IntMap's to+-- a 'NameMap'+mapNMap1 :: (IntMap (NMElem f) -> IntMap (NMElem f)) -> NameMap f -> NameMap f+mapNMap1 f (NameMap m) = NameMap $ f m++-- | Internal-only helper function for mapping a binary function on 'IntMap's to+-- 'NameMap's+mapNMap2 :: (IntMap (NMElem f) -> IntMap (NMElem f) -> IntMap (NMElem f)) ->+            NameMap f -> NameMap f -> NameMap f+mapNMap2 f (NameMap m1) (NameMap m2) = NameMap $ f m1 m2++-- | The empty 'NameMap'+empty :: NameMap f+empty = NameMap IntMap.empty++-- | The singleton 'NameMap' with precisely one 'Name' and corresponding value+singleton :: Name a -> f a -> NameMap f+singleton (MkName i) x = NameMap $ IntMap.singleton i $ NMElem x++-- | A pair of a 'Name' of some type @a@ along with an element of type @f a@+data NameAndElem f where+  NameAndElem :: Name a -> f a -> NameAndElem f++-- | Build a 'NameMap' from a list of pairs of names and values they map to+fromList :: [NameAndElem f] -> NameMap f+fromList =+  NameMap . IntMap.fromList .+  Prelude.map (\ne ->+                case ne of+                  NameAndElem (MkName i) f -> (i, NMElem f))++-- | Insert a 'Name' and a value it maps to into a 'NameMap'+insert :: Name a -> f a -> NameMap f -> NameMap f+insert (MkName i) f = mapNMap1 $ IntMap.insert i (NMElem f)++-- | Delete a 'Name' and the value it maps to from a 'NameMap'+delete :: Name a -> NameMap f -> NameMap f+delete (MkName i) = mapNMap1 $ IntMap.delete i++-- | Apply a function to the value mapped to by a 'Name'+adjust :: (f a -> f a) -> Name a -> NameMap f -> NameMap f+adjust f (MkName i) = mapNMap1 $ IntMap.adjust (NMElem . f . coerceNMElem) i++-- | Update the value mapped to by a 'Name', possibly deleting it+update :: (f a -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f+update f (MkName i) = mapNMap1 $ IntMap.update (fmap NMElem . f . coerceNMElem) i++-- | Apply a function to the optional value associated with a 'Name', where+-- 'Nothing' represents the 'Name' not being present in the 'NameMap'+alter :: (Maybe (f a) -> Maybe (f a)) -> Name a -> NameMap f -> NameMap f+alter f (MkName i) =+  mapNMap1 $ IntMap.alter (fmap NMElem . f . fmap coerceNMElem) i++-- | Look up the value associated with a 'Name', returning 'Nothing' if there is+-- none+lookup :: Name a -> NameMap f -> Maybe (f a)+lookup (MkName i) (NameMap m) = fmap coerceNMElem $ IntMap.lookup i m++-- | Synonym for 'lookup' with the argument order reversed+(!) :: NameMap f -> Name a -> f a+(NameMap m) ! (MkName i) = coerceNMElem $ m IntMap.! i++-- | Test if a 'Name' has a value in a 'NameMap'+member :: Name a -> NameMap f -> Bool+member (MkName i) (NameMap m) = IntMap.member i m++-- | Test if a 'NameMap' is empty+null :: NameMap f -> Bool+null (NameMap m) = IntMap.null m++-- | Return the number of 'Name's in a 'NameMap'+size :: NameMap f -> Int+size (NameMap m) = IntMap.size m++-- | Union two 'NameMap's+union :: NameMap f -> NameMap f -> NameMap f+union = mapNMap2 IntMap.union++-- | Remove all bindings in the first 'NameMap' for 'Name's in the second+difference :: NameMap f -> NameMap f -> NameMap f+difference = mapNMap2 IntMap.difference++-- | Infix synonym for 'difference'+(\\) :: NameMap f -> NameMap f -> NameMap f+(\\) = difference++-- | Intersect two 'NameMap's+intersection :: NameMap f -> NameMap f -> NameMap f+intersection = mapNMap2 IntMap.intersection++-- | Map a function across the values associated with each 'Name'+map :: (forall a. f a -> g a) -> NameMap f -> NameMap g+map f (NameMap m) =+  NameMap $ IntMap.map (\e -> case e of+                           NMElem x -> NMElem $ f x) m++-- | Perform a right fold across all values in a 'NameMap'+foldr :: (forall a. f a -> b -> b) -> b -> NameMap f -> b+foldr f b (NameMap m) =+  IntMap.foldr (\e -> case e of+                   NMElem x -> f x) b m++-- | Perform a left fold across all values in a 'NameMap'+foldl :: (forall b. a -> f b -> a) -> a -> NameMap f -> a+foldl f a (NameMap m) =+  IntMap.foldl (\a e -> case e of+                   NMElem x -> f a x) a m++-- | Return all 'Name's in a 'NameMap' with their associated values+assocs :: NameMap f -> [NameAndElem f]+assocs (NameMap m) =+  Prelude.map (\(i, e) -> case e of+                  NMElem f -> NameAndElem (MkName i) f) $+  IntMap.assocs m++$(mkNuMatching [t| forall f. NuMatchingAny1 f => NameAndElem f |])++-- | Lift a 'NameMap' out of a name-binding using a "partial lifting function"+-- that can lift some values in the 'NameMap' out of the binding. The resulting+-- 'NameMap' contains those names and associated values where the names were not+-- bound by the name-binding and the partial lifting function was able to lift+-- their associated values.+liftNameMap :: forall ctx f a. NuMatchingAny1 f =>+               (forall a. Mb ctx (f a) -> Maybe (f a)) ->+               Mb ctx (NameMap f) -> NameMap f+liftNameMap lifter = helper . fmap assocs where+  helper :: Mb ctx [NameAndElem f] -> NameMap f+  helper [nuP| [] |] = empty+  helper [nuP| (NameAndElem mb_n mb_f):mb_elems |]+    | Right n <- mbNameBoundP mb_n+    , Just f <- lifter mb_f+    = insert n f (helper mb_elems)+  helper [nuP| _:mb_elems |] = helper mb_elems

@@ -0,0 +1,135 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE PatternGuards #-}++-- |+-- Module      : Data.Binding.Hobbits.NameSet+-- Copyright   : (c) 2020 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- Implements sets of 'Name's using 'Data.IntSet.Strict'. Note that these+-- mappings are strict.++module Data.Binding.Hobbits.NameSet (+  NameSet(), SomeName(..)+  , empty, singleton, fromList, toList+  , insert, delete, member, null, size+  , union, unions, difference, (\\), intersection+  , map, foldr, foldl+  , liftNameSet+  ) where++import Prelude hiding (lookup, null, map, foldr, foldl)+import qualified Prelude as Prelude (map)+import Data.Maybe+import Data.IntSet (IntSet)+import qualified Data.IntSet as IntSet+import Data.Kind+import qualified Data.Foldable as Foldable++import Data.Binding.Hobbits.Internal.Name+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.NuMatching+import Data.Binding.Hobbits.QQ+import Data.Binding.Hobbits.Liftable++-- | A set of 'Name's whose types all have kind @k@+newtype NameSet k = NameSet { unNameSet :: IntSet }++-- | A 'Name' of some unknown type of kind @k@+data SomeName k = forall (a :: k). SomeName (Name a)++$(mkNuMatching [t| forall k. SomeName k |])++-- | The empty 'NameSet'+empty :: NameSet k+empty = NameSet $ IntSet.empty++-- | The singleton 'NameSet'+singleton :: Name (a::k) -> NameSet k+singleton (MkName i) = NameSet $ IntSet.singleton $ i++-- | Convert a list of names to a 'NameSet'+fromList :: [SomeName k] -> NameSet k+fromList =+  NameSet . IntSet.fromList . Prelude.map (\(SomeName (MkName i)) -> i)++-- | Convert a 'NameSet' to a list+toList :: NameSet k -> [SomeName k]+toList (NameSet s) = Prelude.map (SomeName . MkName) (IntSet.toList s)++-- | Insert a name into a 'NameSet'+insert :: Name (a::k) -> NameSet k -> NameSet k+insert (MkName i) (NameSet s) = NameSet $ IntSet.insert i s++-- | Delete a name from a 'NameSet'+delete :: Name (a::k) -> NameSet k -> NameSet k+delete (MkName i) (NameSet s) = NameSet $ IntSet.delete i s++-- | Test if a name is in a 'NameSet'+member :: Name (a::k) -> NameSet k -> Bool+member (MkName i) (NameSet s) = IntSet.member i s++-- | Test if a 'NameSet' is empty+null :: NameSet k -> Bool+null (NameSet s) = IntSet.null s++-- | Compute the cardinality of a 'NameSet'+size :: NameSet k -> Int+size (NameSet s) = IntSet.size s++-- | Take the union of two 'NameSet's+union :: NameSet k -> NameSet k -> NameSet k+union (NameSet s1) (NameSet s2) = NameSet $ IntSet.union s1 s2++-- | Take the union of a list of 'NameSet's+unions :: Foldable f => f (NameSet k) -> NameSet k+unions = Foldable.foldl' union empty++-- | Take the set of all elements of the first 'NameSet' not in the second+difference :: NameSet k -> NameSet k -> NameSet k+difference (NameSet s1) (NameSet s2) = NameSet $ IntSet.difference s1 s2++-- | Another name for 'difference'+(\\) :: NameSet k -> NameSet k -> NameSet k+(\\) = difference++-- | Take the intersection of two 'NameSet's+intersection :: NameSet k -> NameSet k -> NameSet k+intersection (NameSet s1) (NameSet s2) = NameSet $ IntSet.intersection s1 s2++-- | Map a function across all elements of a 'NameSet'+map :: (forall (a::k). Name a -> Name a) -> NameSet k -> NameSet k+map f (NameSet s) =+  NameSet $ IntSet.map (\i -> let (MkName j) = f (MkName i) in j) s++-- | Perform a right fold of a function across all elements of a 'NameSet'+foldr :: (forall (a::k). Name a -> r -> r) -> r -> NameSet k -> r+foldr f r (NameSet s) = IntSet.foldr (f . MkName) r s++-- | Perform a left fold of a function across all elements of a 'NameSet'+foldl :: (forall (a::k). r -> Name a -> r) -> r -> NameSet k -> r+foldl f r (NameSet s) = IntSet.foldl (\r -> f r . MkName) r s++-- | Lift a 'NameSet' out of a name-binding by lifting all names not bound by+-- the name-binding and then forming a 'NameSet' from those lifted names+liftNameSet :: Mb ctx (NameSet (k :: Type)) -> NameSet k+liftNameSet mb_s = fromList $ mapMaybe helper $ mbList $ fmap toList mb_s+  where+    helper :: forall ctx' k'. Mb ctx' (SomeName k') -> Maybe (SomeName k')+    helper [nuP| SomeName mb_n |]+      | Right n <- mbNameBoundP mb_n = Just (SomeName n)+    helper _ = Nothing

@@ -0,0 +1,579 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- 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,+  MbTypeRepr(), isoMbTypeRepr, unsafeMbTypeRepr,+  NuMatchingAny1(..)+) where++import Data.Vector (Vector)+import qualified Data.Vector as Vector+--import Data.Typeable+import Language.Haskell.TH hiding (Name, Type(..))+import qualified Language.Haskell.TH as TH+import Control.Monad.State+import Numeric.Natural+import Data.Functor.Constant+import Data.Kind as DK+import Data.Word+import Data.Proxy+import Data.Type.Equality+--import Control.Monad.Identity++import Data.Type.RList hiding (map)+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 => NameRefresher -> a -> a+mapNames = mapNamesPf nuMatchingProof++matchDataDecl :: Dec -> Maybe (Cxt, TH.Name, [TyVarBndr], [Con])+matchDataDecl (DataD cxt name tyvars _ constrs _) =+  Just (cxt, name, tyvars, constrs)+matchDataDecl (NewtypeD cxt name tyvars _ constr _) =+  Just (cxt, name, tyvars, [constr])+matchDataDecl _ = Nothing+++mkInstanceD :: Cxt -> TH.Type -> [Dec] -> Dec+mkInstanceD = InstanceD Nothing++{-|+  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++-- | Build an 'MbTypeRepr' for type @a@ by using an isomorphism with an+-- already-representable type @b@. This is useful for building 'NuMatching'+-- instances for, e.g., 'Integral' types, by mapping to and from 'Integer',+-- without having to define instances for each one in this module.+isoMbTypeRepr :: NuMatching b => (a -> b) -> (b -> a) -> MbTypeRepr a+isoMbTypeRepr f_to f_from =+  MbTypeReprData $ MkMbTypeReprData $ \refresher a ->+  f_from $ mapNames refresher (f_to a)++-- | Builds an 'MbTypeRepr' proof for use in a 'NuMatching' instance. This proof+-- is unsafe because it does no renaming of fresh names, so should only be used+-- for types that are guaranteed not to contain any 'Name' or 'Mb' values.+unsafeMbTypeRepr :: MbTypeRepr a+unsafeMbTypeRepr = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching (Name a) where+    nuMatchingProof = MbTypeReprName++instance NuMatching (Closed a) where+    -- no need to map free variables in a Closed object+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\refresher -> 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 Bool where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Int where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Integer where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Char where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Natural where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Float where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Double where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Word where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Word8 where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Word16 where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Word32 where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching Word64 where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance NuMatching () where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\_ -> id))++instance (NuMatching a, NuMatching b) => NuMatching (a,b) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b) ->+                                       (mapNames r a, mapNames r b))++instance (NuMatching a, NuMatching b, NuMatching c) => NuMatching (a,b,c) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b,c) ->+                                       (mapNames r a, mapNames r b, mapNames r c))++instance (NuMatching a, NuMatching b,+          NuMatching c, NuMatching d) => NuMatching (a,b,c,d) where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ \r (a,b,c,d) ->+                                       (mapNames r a, mapNames r b,+                                        mapNames r c, mapNames r d))++instance NuMatching a => NuMatching [a] where+    nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\r -> map (mapNames r)))++instance NuMatching a => NuMatching (Vector a) where+    nuMatchingProof =+      MbTypeReprData (MkMbTypeReprData $ (\r -> Vector.map (mapNames r)))+++{-+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)+-}++{-+-- | An object-level reification of the 'NuMatching' class+data NuMatchingObj a = NuMatching a => NuMatchingObj ()++class NuMatchingList args where+    nuMatchingListProof :: RAssign NuMatchingObj args++instance NuMatchingList RNil where+    nuMatchingListProof = MNil++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 {-# OVERLAPPABLE #-} (NuMatching1 f, NuMatchingList ctx) =>+                              NuMatching (RAssign f ctx) where+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData $ helper nuMatchingListProof where+        helper :: NuMatching1 f =>+                  RAssign NuMatchingObj args -> NameRefresher ->+                  RAssign f args -> RAssign f args+        helper MNil r MNil = MNil+        helper (proofs :>: NuMatchingObj ()) r (elems :>: (elem :: f a)) =+            case nuMatchingProof1 :: NuMatchingObj (f a) of+              NuMatchingObj () ->+                  (helper proofs r elems) :>:+                  mapNames r elem+-}++-- | Typeclass for lifting the 'NuMatching' constraint to functors on arbitrary+-- kinds that do not require any constraints on their input types+class NuMatchingAny1 (f :: k -> Type) where+  nuMatchingAny1Proof :: MbTypeRepr (f a)++instance {-# INCOHERENT #-} NuMatchingAny1 f => NuMatching (f a) where+  nuMatchingProof = nuMatchingAny1Proof++instance NuMatchingAny1 Name where+  nuMatchingAny1Proof = nuMatchingProof++instance NuMatchingAny1 ((:~:) a) where+  nuMatchingAny1Proof = nuMatchingProof++instance NuMatching a => NuMatchingAny1 (Constant a) where+  nuMatchingAny1Proof = nuMatchingProof++instance {-# OVERLAPPABLE #-} NuMatchingAny1 f => NuMatching (RAssign f ctx) where+    nuMatchingProof = MbTypeReprData $ MkMbTypeReprData helper where+        helper :: NuMatchingAny1 f => NameRefresher -> RAssign f args ->+                  RAssign f args+        helper r MNil = MNil+        helper r (elems :>: elem) = helper r elems :>: mapNames r 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)++mapNamesType a = [t| forall ctx. NameRefresher -> $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 TH.Type -> Q [Dec]+mkNuMatching tQ =+    do t <- tQ+       (cxt, cType, tName, constrs, tyvars) <- getMbTypeReprInfoTop t+       fName <- newName "f"+       refrName <- newName "refresher"+       clauses <- getClauses (tName, fName, refrName) constrs+       mapNamesT <- mapNamesType (return cType)+       return [mkInstanceD+               cxt (TH.AppT (TH.ConT ''NuMatching) cType)+               [ValD (VarP 'nuMatchingProof)+                (NormalB+                 $ AppE (ConE 'MbTypeReprData)+                   $ AppE (ConE 'MkMbTypeReprData)+                         $ LetE [SigD fName+                                 $ TH.ForallT (map PlainTV tyvars) cxt mapNamesT,+                                 FunD fName clauses]+                               (VarE fName)) []]]++       {-+       return (LetE+               [SigD fName+                     (TH.ForallT tyvars reqCxt+                     $ foldl TH.AppT TH.ArrowT+                           [foldl TH.AppT (TH.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 (TH.ConT tName) =+          do info <- reify tName+             case info of+               TyConI (matchDataDecl -> Just (_, _, tyvarsReq, constrs)) ->+                 success tyvarsReq constrs+               _ -> 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 TH.AppT (TH.ConT tName) (map TH.VarT tyvars),+                        tName, constrs, tyvarsRet)++      getMbTypeReprInfo ctx tyvars topT (TH.AppT f (TH.VarT argName)) =+          if elem argName tyvars then+              getMbTypeReprInfoFail topT ""+          else+              getMbTypeReprInfo ctx (argName:tyvars) topT f++      getMbTypeReprInfo ctx tyvars topT (TH.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 (TH.ConT tName) topT tyvars = Just (topT, tName, tyvars)+      getTCtorHelper (TH.AppT t1 (TH.VarT var)) topT tyvars =+          getTCtorHelper t1 topT (tyvars ++ [var])+      getTCtorHelper (TH.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 _ [] = return []++      getClauses names (NormalC cName cTypes : constrs) =+        do clause <-+             getClauseHelper names (map snd cTypes) (natsFrom 0)+             (\l -> ConP cName (map (VarP . fst3) l))+             (\l -> foldl AppE (ConE cName) (map fst3 l))+           clauses <- getClauses names constrs+           return $ clause : clauses++      getClauses names (RecC cName cVarTypes : constrs) =+        do clause <-+             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))+           clauses <- getClauses names constrs+           return $ clause : clauses++      getClauses names (InfixC cType1 cName cType2 : constrs) =+        do clause <-+             getClauseHelper names (map snd [cType1, cType2]) (natsFrom 0)+             (\l -> ConP cName (map (VarP . fst3) l))+             (\l -> foldl AppE (ConE cName) (map fst3 l))+           clauses <- getClauses names constrs+           return $ clause : clauses++      getClauses names (GadtC cNames cTypes _ : constrs) =+        do clauses1 <-+             forM cNames $ \cName ->+             getClauseHelper names (map snd cTypes) (natsFrom 0)+             (\l -> ConP cName (map (VarP . fst3) l))+             (\l -> foldl AppE (ConE cName) (map fst3 l))+           clauses2 <- getClauses names constrs+           return (clauses1 ++ clauses2)++      getClauses names (RecGadtC cNames cVarTypes _ : constrs) =+        do clauses1 <-+             forM cNames $ \cName ->+             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))+           clauses2 <- getClauses names constrs+           return (clauses1 ++ clauses2)++      getClauses names (ForallC _ _ constr : constrs) =+        getClauses names (constr : constrs)++      getClauseHelper :: Names -> [TH.Type] -> [a] ->+                         ([(TH.Name,TH.Type,a)] -> Pat) ->+                         ([(Exp,TH.Type,a)] -> Exp) ->+                         Q Clause+      getClauseHelper names@(tName, fName, refrName) 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 refrName), (pFun varsTypesData)]+                        (NormalB $ eFun expsTypesData) []++      mkExpTypeData :: Names -> (TH.Name,TH.Type,a) -> (Exp,TH.Type,a)+      mkExpTypeData (tName, fName, refrName)+                    (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 refrName), (VarE varName)],+               t, cData)+      mkExpTypeData (tName, fName, refrName) (varName, t, cData) =+          -- the type of the arg is not the same as the (G)ADT; call mapNames+          (foldl AppE (VarE 'mapNames)+                     [(VarE refrName), (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+                     (TH.ForallT tyvars reqCxt+                     $ foldl TH.AppT TH.ArrowT+                           [foldl TH.AppT (TH.ConT conName)+                                      (map tyVarToType tyvars)]),+                FunD fname clauses]+               (VarE fname))+    where+      -- convert a TyVar to a Name+      tyVarToType (PlainTV n) = TH.VarT n+      tyVarToType (KindedTV n _) = TH.VarT n++      -- get info for conName+      getMbTypeReprInfo conName =+          reify conName >>= \info ->+              case info of+                TyConI (matchDataDecl -> Just (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 (TH.ConT conName) topT =+          reify conName >>= \info ->+              case info of+                TyConI (DataD cxt name tyvars constrs _) ->+                    return (cxt, name, tyvars, constrs)+                _ -> getMbTypeReprInfoFail topT+      getMbTypeReprInfo (TH.AppT t _) topT = getMbTypeReprInfo t topT+      getMbTypeReprInfo (TH.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] -> [TyVarBndr] -> [Con] ->+                    CxtStateQ [Clause]+      getClauses cxt name tyvars locTyvars [] = return []++      getClauses cxt name tyvars locTyvars (NormalC cName cTypes : constrs) =+        do clause <-+             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))+           clauses <- getClauses cxt name tyvars locTyvars constrs+           return (clause : clauses)++      getClauses cxt name tyvars locTyvars (RecC cName cVarTypes : constrs) =+        do clause <-+             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))+           clauses <- getClauses cxt name tyvars locTyvars constrs+           return (clause : clauses)++      getClauses cxt name tyvars locTyvars (InfixC cType1 cName cType2 : _) =+        undefined -- FIXME++      getClauses cxt name tyvars locTyvars (ForallC tyvars2 cxt2 constr+                                            : constrs) =+        do clauses1 <-+             getClauses (cxt ++ cxt2) name tyvars (locTyvars ++ tyvars2) [constr]+           clauses2 <- getClauses cxt name tyvars locTyvars constrs+           return (clauses1 ++ clauses2)++      getClauses cxt name tyvars locTyvars (GadtC cNames cTypes _ : constrs) =+        do clauses1 <-+             forM cNames $ \cName ->+             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))+           clauses2 <- getClauses cxt name tyvars locTyvars constrs+           return (clauses1 ++ clauses2)++      getClauses cxt name tyvars locTyvars (RecGadtC cNames cVarTypes _+                                            : constrs) =+        do clauses1 <-+             forM cNames $ \cName ->+             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))+           clauses2 <- getClauses cxt name tyvars locTyvars constrs+           return (clauses1 ++ clauses2)++      getClauseHelper :: Cxt -> TH.Name -> [TyVarBndr] -> [TyVarBndr] ->+                         [TH.Type] -> [a] ->+                         ([(TH.Name,TH.Type,a)] -> Pat) ->+                         ([(TH.Name,TH.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] -> [TH.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] -> TH.Type -> CxtStateQ ()+      ensureCxt1 cxt locTyvars t = undefined+      {-+      ensureCxt1 cxt locTyvars t = do+        curCxt = get+        let fullCxt = cxt ++ curCxt+        isOk <- isMbTypeRepr fullCxt ++      isMbTypeRepr +       -}

@@ -0,0 +1,40 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE QuasiQuotes #-}++-- |+-- Module      : Data.Binding.Hobbits.NuMatchingInstances+-- Copyright   : (c) 2020 Edwin Westbrook+--+-- License     : BSD3+--+-- Maintainer  : westbrook@galois.com+-- Stability   : experimental+-- Portability : GHC+--+-- Provides a set of instances of 'NuMatching' for standard types using the+-- template Haskell 'mkNuMatching' function++module Data.Binding.Hobbits.NuMatchingInstances where++import Data.Proxy+import Data.Type.Equality+import Data.Functor.Constant++import Data.Type.RList+import Data.Binding.Hobbits.Mb+import Data.Binding.Hobbits.NuMatching (NuMatching, NuMatchingAny1, mkNuMatching)+import Data.Binding.Hobbits.QQ (nuP)++$(mkNuMatching [t| forall a. NuMatching a => Maybe a |])+$(mkNuMatching [t| forall a b. (NuMatching a, NuMatching b) => Either a b |])+$(mkNuMatching [t| forall ctx a. Member ctx a |])+$(mkNuMatching [t| forall a. Proxy a |])+$(mkNuMatching [t| forall a b. a :~: b |])+$(mkNuMatching [t| forall a b. NuMatching a => Constant a b |])

@@ -0,0 +1,34 @@+-- |+-- Module      : Data.Binding.Hobbits.PatternParser+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- Using the haskell-src-meta package to parse Haskell patterns.++module Data.Binding.Hobbits.PatternParser (parsePattern) where++import Language.Haskell.TH++import qualified Language.Haskell.Exts.Parser as Meta++import qualified Language.Haskell.Meta.Parse as Meta++import qualified Language.Haskell.Meta.Parse as Sloppy+import qualified Language.Haskell.Meta.Syntax.Translate as Translate++import qualified Language.Haskell.Exts.Extension as Exts++parsePatternExtensions =+  map Exts.EnableExtension $ Exts.ViewPatterns : Sloppy.myDefaultExtensions++parsePattern :: String -> String -> Either String Pat+parsePattern fn =+  fmap Translate.toPat . Meta.parseResultToEither .+  Meta.parsePatWithMode (Sloppy.myDefaultParseMode+                    {Meta.parseFilename = fn,+                     Meta.extensions = parsePatternExtensions })

@@ -0,0 +1,148 @@+{-# LANGUAGE TemplateHaskell, FlexibleContexts, PolyKinds #-}++-- |+-- Module      : Data.Binding.Hobbits.QQ+-- Copyright   : (c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul Brauner+--+-- License     : BSD3+--+-- Maintainer  : emw4@rice.edu+-- Stability   : experimental+-- Portability : GHC+--+-- Defines a quasi-quoter for writing patterns that match the bodies of 'Mb'+-- multi-bindings. Uses the haskell-src-exts parser. @[nuP| P ]@ defines a+-- pattern that will match a multi-binding whose body matches @P@. Any+-- variables matched by @P@ will remain inside the binding; thus, for example,+-- in the pattern @[nuP| x |]@, @x@ matches the entire multi-binding.+--+-- Examples:+--+-- > case (nu Left) of [nuP| Left x |] -> x  ==  nu id+--+-- @[clP| P |]@ does the same for the 'Closed' type, and @[clNuP| P |]@ works+-- for both simultaneously: @'Closed' ('Mb' ctx a)@.++module Data.Binding.Hobbits.QQ (nuP, clP, clNuP) where++import Language.Haskell.TH.Syntax as TH+import Language.Haskell.TH.Ppr as TH+import Language.Haskell.TH.Quote++import qualified Data.Generics as SYB+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 =+  WrapKit {_varView :: Exp, _asXform :: Pat -> Pat, _topXform :: Bool -> Pat -> Pat}++-- | 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}++-- | Apply a 'WrapKit' to a pattern+wrapVars :: Monad m => WrapKit -> Pat -> m 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 'varView' function is ever used+    hit x = tell (Any True) >> return x++    -- wraps up bound names+    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 varView $ AsP v $ asXform p+    -- requires the expression to be closed+    w (ViewP (VarE n) p) = return $ ViewP (VarE 'unClosed `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+  case parsePattern fn s of+    Left e -> error $ "Parse error: `" ++ e +++      "'\n\n\t when parsing pattern: `" ++ s ++ "'."+    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++-- | 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+  topVar <- newName "topMb"+  namesVar <- newName "topNames"+  parseHere s >>= wrapVars (nuKit topVar namesVar)++-- | Builds a 'WrapKit' for parsing patterns that match over 'Closed'+clKit = WrapKit {_varView = ConE 'Closed, _asXform = asXform, _topXform = const asXform}+  where asXform p = ConP 'Closed [p]++-- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit'+clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere++-- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@+clNuP = patQQ "clNuP" $ \s -> do+  topVar <- newName "topMb"+  namesVar <- newName "topNames"+  parseHere s >>= wrapVars (clKit `combineWrapKits` nuKit topVar namesVar)

@@ -0,0 +1,232 @@+{-# LANGUAGE TypeOperators, EmptyDataDecls, RankNTypes #-}+{-# LANGUAGE TypeFamilies, DataKinds, PolyKinds, KindSignatures #-}+{-# LANGUAGE GADTs, TypeInType, PatternGuards #-}++-- |+-- 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 Prelude hiding (map, foldr)+import Data.Kind+import Data.Type.Equality+import Data.Proxy (Proxy(..))+import Data.Functor.Constant+import Data.Typeable++-------------------------------------------------------------------------------+-- * Right-lists as a datatype+-------------------------------------------------------------------------------++-- | A form of lists where elements are added to the right instead of the left+data RList a+  = RNil+  | (RList a) :> a++-- | Append two 'RList's at the type level+type family ((r1 :: RList k) :++: (r2 :: RList k)) :: RList k+infixr 5 :++:+type instance (r :++: 'RNil) = r+type instance (r1 :++: (r2 ':> a)) = (r1 :++: r2) ':> a++-------------------------------------------------------------------------------+-- * 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 :: RList k1) (a :: k2) 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) where+    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++instance TestEquality (Member ctx) where+  testEquality Member_Base Member_Base = Just Refl+  testEquality (Member_Step memb1) (Member_Step memb2)+    | Just Refl <- testEquality memb1 memb2+    = Just Refl+  testEquality _ _ = Nothing++instance Eq (Member ctx a) where+  Member_Base == Member_Base = True+  (Member_Step memb1) == (Member_Step memb2) = memb1 == memb2+  _ == _ = False++--toEq :: Member (Nil :> a) b -> b :~: a+--toEq Member_Base = Refl+--toEq _ = error "Should not happen! (toEq)"++-- | Weaken a 'Member' proof by prepending another context to the context it+-- proves membership in+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)+++------------------------------------------------------------+-- * 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)++-- | Make an 'Append' proof from any 'RAssign' vector for the second+-- argument of the append.+mkAppend :: RAssign 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 -> RAssign f c2 -> Append c1 c2 (c1 :++: c2)+mkMonoAppend _ = mkAppend++-- | The inverse of 'mkAppend', that builds an 'RAssign' from an 'Append'+proxiesFromAppend :: Append c1 c2 c -> RAssign Proxy c2+proxiesFromAppend Append_Base = MNil+proxiesFromAppend (Append_Step a) = proxiesFromAppend a :>: Proxy+++-------------------------------------------------------------------------------+-- * Contexts+-------------------------------------------------------------------------------++{-|+  An @RAssign f r@ an assignment of an @f a@ for each @a@ in the 'RList' @r@+-}+data RAssign (f :: k -> *) (c :: RList k) where+  MNil :: RAssign f RNil+  (:>:) :: RAssign f c -> f a -> RAssign f (c :> a)++-- | Create an empty 'RAssign' vector.+empty :: RAssign f RNil+empty = MNil++-- | Create a singleton 'RAssign' vector.+singleton :: f a -> RAssign f (RNil :> a)+singleton x = MNil :>: x++-- | Look up an element of an 'RAssign' vector using a 'Member' proof+get :: Member c a -> RAssign f c -> f a+get Member_Base (_ :>: x) = x+get (Member_Step mem') (mc :>: _) = get mem' mc++-- | Heterogeneous type application, including a proof that the input kind of+-- the function equals the kind of the type argument+data HApply (f :: k1 -> Type) (a :: k2) where+  HApply :: forall (f :: k -> Type) (a :: k). f a -> HApply f a++-- | Look up an element of an 'RAssign' vector using a 'Member' proof at what+-- GHC thinks might be a different kind, i.e., heterogeneously+hget :: forall (f :: k1 -> Type) (c :: RList k1) (a :: k2).+        Member c a -> RAssign f c -> HApply f a+hget Member_Base (_ :>: x) = HApply x+hget (Member_Step mem') (mc :>: _) = hget mem' mc++-- | Modify an element of an 'RAssign' vector using a 'Member' proof.+modify :: Member c a -> (f a -> f a) -> RAssign f c -> RAssign f c+modify Member_Base f (xs :>: x) = xs :>: f x+modify (Member_Step mem') f (xs :>: x) = modify mem' f xs :>: x++-- | Set an element of an 'RAssign' vector using a 'Member' proof.+set :: Member c a -> f a -> RAssign f c -> RAssign f c+set memb x = modify memb (const x)++-- | Test if an object is in an 'RAssign', returning a 'Member' proof if it is+memberElem :: TestEquality f => f a -> RAssign f ctx -> Maybe (Member ctx a)+memberElem _ MNil = Nothing+memberElem x (_ :>: y) | Just Refl <- testEquality x y = Just Member_Base+memberElem x (xs :>: _) = fmap Member_Step $ memberElem x xs++-- | Map a function on all elements of an 'RAssign' vector.+map :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c+map _ MNil = MNil+map f (mc :>: x) = map f mc :>: f x++-- | An alternate name for 'map' that does not clash with the prelude+mapRAssign :: (forall x. f x -> g x) -> RAssign f c -> RAssign g c+mapRAssign = map++-- | Map a binary function on all pairs of elements of two 'RAssign' vectors.+map2 :: (forall x. f x -> g x -> h x) ->+                RAssign f c -> RAssign g c -> RAssign h c+map2 _ MNil MNil = MNil+map2 f (xs :>: x) (ys :>: y) = map2 f xs ys :>: f x y++-- | Take the tail of an 'RAssign'+tail :: RAssign f (ctx :> a) -> RAssign f ctx+tail (xs :>: _) = xs++-- | Convert a monomorphic 'RAssign' to a list+toList :: RAssign (Constant a) c -> [a]+toList = mapToList getConstant++-- | Map a function with monomorphic output type across an 'RAssign' to create a+-- standard list:+--+-- > mapToList f = toList . map (Constant . f)+mapToList :: (forall a. f a -> b) -> RAssign f ctx -> [b]+mapToList _ MNil = []+mapToList f (xs :>: x) = mapToList f xs ++ [f x]++-- | Append two 'RAssign' vectors.+append :: RAssign f c1 -> RAssign f c2 -> RAssign f (c1 :++: c2)+append mc MNil = mc+append mc1 (mc2 :>: x) = append mc1 mc2 :>: x++-- | Perform a right fold across an 'RAssign'+foldr :: (forall a. f a -> r -> r) -> r -> RAssign f ctx -> r+foldr _ r MNil = r+foldr f r (xs :>: x) = f x $ foldr f r xs++-- | Split an 'RAssign' vector into two pieces. The first argument is a+-- phantom argument that gives the form of the first list piece.+split :: (c ~ (c1 :++: c2)) => prx c1 ->+                 RAssign any c2 -> RAssign f c -> (RAssign f c1, RAssign f c2)+split _ MNil mc = (mc, MNil)+split _ (any :>: _) (mc :>: x) = (mc1, mc2 :>: x)+  where (mc1, mc2) = split Proxy any mc++-- | Create a vector of proofs that each type in @c@ is a 'Member' of @c@.+members :: RAssign f c -> RAssign (Member c) c+members MNil = MNil+members (c :>: _) = map Member_Step (members c) :>: Member_Base++-- | 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 :: RAssign Proxy ctx++instance TypeCtx RNil where+  typeCtxProxies = MNil++instance TypeCtx ctx => TypeCtx (ctx :> a) where+  typeCtxProxies = typeCtxProxies :>: Proxy