packages feed

hobbits 1.2.2 → 1.2.3

raw patch · 6 files changed

+97/−81 lines, 6 filesdep ~basedep ~template-haskelldep ~th-expand-syns

Dependency ranges changed: base, template-haskell, th-expand-syns

Files

CHANGELOG view
@@ -1,4 +1,11 @@ +1.2.2 -> 1.2.3+- Renamed Cl and unCl to Closed and unClosed, respectively+- Moved mkClosed to Internal/Closed.hs+- Added the Closable typeclass+- Added clApplyCl++ 1.2.1 -> 1.2.2 - Added NuMatching and Liftable instances for the unit type
Data/Binding/Hobbits/Closed.hs view
@@ -16,11 +16,11 @@  module Data.Binding.Hobbits.Closed (   -- * Abstract types-  Cl(),-  -- * Operators involving 'Cl'-  cl, clApply, unCl, noClosedNames,-  -- * Synonyms-  mkClosed, Closed, unClosed+  Closed(),+  -- * Operators involving 'Closed'+  unClosed, mkClosed, noClosedNames, clApply, clMbApply, clApplyCl,+  -- * Typeclass for inherently closed types+  Closable(..) ) where  import Data.Binding.Hobbits.Internal.Name@@ -28,59 +28,10 @@ import Data.Binding.Hobbits.Internal.Closed import Data.Binding.Hobbits.Mb -import Language.Haskell.TH (Q, Exp(..), Type(..))-import qualified Language.Haskell.TH as TH-import qualified Language.Haskell.TH.ExpandSyns as TH--import qualified Data.Generics as SYB-import qualified Language.Haskell.TH.Syntax as TH----- | @cl@ is used with Template Haskell quotations to create closed terms of--- type 'Cl'. A quoted expression is closed if all of the names occuring in it--- are------   1) bound globally or---   2) bound within the quotation or---   3) also of type 'Cl'.-cl :: Q Exp -> Q Exp-cl e = AppE (ConE 'Cl) `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 $ "`cl' does not allow dynamically bound names: `"-      ++ show n ++ "'."-  w e = return e--  closed n = do-    i <- TH.reify n-    case i of-      TH.VarI _ ty _ _ -> TH.expandSyns ty >>= w-        where-          w (AppT (ConT m) _) | m == ''Cl = return ()-          w (ForallT _ _ ty) = w ty-          w _ = fail $ "`cl` requires non-global variables to have type `Cl'.\n\t`"-            ++ show (TH.ppr n) ++ "' does not. It's type is:\n\t `"-            ++ show (TH.ppr ty) ++ "'."-      _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."------ | Closed terms are closed (sorry) under application.-clApply :: Cl (a -> b) -> Cl a -> Cl b--- could be defined with cl were it not for the GHC stage restriction-clApply (Cl f) (Cl a) = Cl (f a)---- | Closed multi-bindings are also closed under application.-clMbApply :: Cl (Mb ctx (a -> b)) -> Cl (Mb ctx a) ->-             Cl (Mb ctx b)-clMbApply (Cl f) (Cl a) = Cl (mbApply f a)- -- | @noClosedNames@ encodes the hobbits guarantee that no name can escape its -- multi-binding.-noClosedNames :: Cl (Name a) -> b-noClosedNames (Cl n) =+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@@ -89,11 +40,25 @@       "... Clever girl!" ++       "The `noClosedNames' invariant has somehow been violated." --- | @mkClosed = cl@-mkClosed = cl+-- | 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 = Cl@-type Closed = Cl+-- | 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) --- | @unClosed = unCl@-unClosed x = unCl x+-- | 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
Data/Binding/Hobbits/Internal/Closed.hs view
@@ -18,11 +18,45 @@  module Data.Binding.Hobbits.Internal.Closed where -{-|-  The type @Cl a@ represents a closed term of type @a@,-  i.e., an expression of type @a@ with no free (Haskell) variables.-  Since this cannot be checked directly in the Haskell type system,-  the @Cl@ data type is hidden, and the user can only create-  closed terms using Template Haskell, through the 'cl' operator.--}-newtype Cl a = Cl { unCl :: a }+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 }++-- | @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+    i <- TH.reify n+    case i of+      TH.VarI _ ty _ _ -> TH.expandSyns ty >>= w+        where+          w (AppT (ConT m) _) | m == ''Closed = return ()+          w (ForallT _ _ ty) = w ty+          w _ = 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 ty) ++ "'."+      _ -> fail $ "hobbits Panic -- could not reify `" ++ show n ++ "'."
Data/Binding/Hobbits/NuMatching.hs view
@@ -23,7 +23,7 @@  module Data.Binding.Hobbits.NuMatching (   NuMatching(..), mkNuMatching, NuMatchingList(..), NuMatching1(..),-  MbTypeRepr()+  MbTypeRepr(), isoMbTypeRepr ) where  --import Data.Typeable@@ -56,7 +56,7 @@ instance NuMatching (Name a) where     nuMatchingProof = MbTypeReprName -instance NuMatching (Cl a) where+instance NuMatching (Closed a) where     -- no need to map free variables in a Closed object     nuMatchingProof = MbTypeReprData (MkMbTypeReprData $ (\c1 c2 -> id)) @@ -151,6 +151,16 @@               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
Data/Binding/Hobbits/QQ.hs view
@@ -20,8 +20,8 @@ -- -- > case (nu Left) of [nuP| Left x |] -> x  ==  nu id ----- [clP| P |] does the same for the Cl type, and [clNuP| P |] works for--- both simultaneously: Cl (Mb ctx a).+-- @[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 @@ -101,7 +101,7 @@     -- 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 'unCl `AppE` VarE n) p+    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 @@ -134,14 +134,14 @@   namesVar <- newName "topNames"   parseHere s >>= wrapVars (nuKit topVar namesVar) --- | Builds a 'WrapKit' for parsing patterns that match over 'Cl'-clKit = WrapKit {_varView = ConE 'Cl, _asXform = asXform, _topXform = const asXform}-  where asXform p = ConP 'Cl [p]+-- | 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 'Cl', built using 'clKit'+-- | Quasi-quoter for patterns that match over 'Closed', built using 'clKit' clP = patQQ "clP" $ (>>= wrapVars clKit) . parseHere --- | Quasi-quoter for patterhs that match over @'Cl' ('Mb' ctx a)@+-- | Quasi-quoter for patterns that match over @'Closed' ('Mb' ctx a)@ clNuP = patQQ "clNuP" $ \s -> do   topVar <- newName "topMb"   namesVar <- newName "topNames"
hobbits.cabal view
@@ -1,5 +1,5 @@ Name:                hobbits-Version:             1.2.2+Version:             1.2.3 Synopsis:            A library for canonically representing terms with binding  Description: A library for canonically representing terms with binding via a