unbound 0.4.2 → 0.4.3

raw patch · 4 files changed

+42/−55 lines, 4 filesdep +binary

Dependencies added: binary

Files

• CHANGES +8/−0
• Unbound/LocallyNameless/Types.hs +31/−0
• examples/LCTyped.hs +0/−53
• unbound.cabal +3/−2

@@ -76,3 +76,11 @@    * added unbind variants [l]unbind{23}Plus for conveniently unbinding     in a MonadPlus context.++Version 0.4.3: 29 January 2014++  * Add Binary instances for Name, GenBind, Rebind, and Embed.++    Note that although the PVP requires a major version bump for added+    instances, it was impossible to write these instances outside of+    the package, so there is no danger of breakage.

@@ -39,6 +39,9 @@ import Generics.RepLib import Unbound.LocallyNameless.Name +import Data.Binary+import Control.Applicative (pure, (<$>), (<*>))+ ------------------------------------------------------------ -- Basic types ------------------------------------------------------------@@ -147,3 +150,31 @@  $(derive [''RelaxedOrder, ''StrictOrder, ''RelaxedCard, ''StrictCard]) ++-- Data.Binary instances for Name and Bind+----------------------------------------------------++instance Rep a => Binary (Name a) where+  put (Nm _ (s,i)) = do put (0 :: Word8)+                        put s+                        put i+  put (Bn _ i j)   = do put (1 :: Word8)+                        put i+                        put j+  +  get = do tag <- getWord8+           case tag of+              0 -> Nm <$> pure rep <*> get+              1 -> Bn <$> pure rep <*> get <*> get++instance (Binary p, Binary t) => Binary (GenBind order card p t) where+  put (B p t) = do put p ; put t+  get = B <$> get <*> get++instance (Binary p1, Binary p2) => Binary (Rebind p1 p2) where+  put (R p1 p2) = do put p1 ; put p2+  get = R <$> get <*> get+  +instance (Binary p) => Binary (Embed p) where+  put (Embed p) = put p+  get = Embed <$> get

@@ -1,53 +0,0 @@-{-# LANGUAGE GADTs-           , TemplateHaskell-           , KindSignatures-           , ScopedTypeVariables-           , TypeOperators-  #-}--module LCTyped where--import Unbound.LocallyNameless-import Data.Type.Equality--import Unsafe.Coerce (unsafeCoerce)------------------------------------------------------------------data Res1 c a where-  Result1   :: Rep b => a :=: (c b) -> Res1 c a-  NoResult1 :: Res1 c a--destr1 :: R a -> R (c d) -> Res1 c a-destr1 (Data (DT s1 ((_ :: R b) :+: MNil)) _)-       (Data (DT s2 _) _)-  | s1 == s2  = Result1 (unsafeCoerce Refl :: a :=: (c b))-  | otherwise = NoResult1-destr1 _ _ = NoResult1--data Res2 c2 a where-  Result2   :: (Rep d, Rep e) => a :=: (c2 d e) -> Res2 c2 a-  NoResult2 :: Res2 c2 a--destr2 :: R a -> R (c2 d e) -> Res2 c2 a-destr2 (Data (DT s1 ((_ :: R d) :+: (_ :: R e) :+: MNil)) _)-       (Data (DT s2 _) _)-  | s1 == s2  = Result2 (unsafeCoerce Refl :: a :=: (c2 d e))-  | otherwise = NoResult2-destr2 _ _ = NoResult2-----------------------------------------------------------------data V :: * -> * -> * where-  VZ :: V (a,env) a-  VS :: V env a -> V (b,env) a--data Tm :: * -> * -> * where-  Var :: V env a -> Tm env a-  Lam :: Tm (a,env) b -> Tm env (a -> b)-  App :: Tm env (a -> b) -> Tm env a -> Tm env b--$(derive [''V, ''Tm])

@@ -1,5 +1,5 @@ name:           unbound-version:        0.4.2+version:        0.4.3 license:        BSD3 license-file:   LICENSE build-type:     Simple@@ -32,7 +32,8 @@   build-depends: base >= 4.3 && < 5,                  RepLib >= 0.5.3 && < 0.6,                  mtl >= 2.0 && < 2.2, transformers >= 0.2.2.0 && < 0.4,-                 containers >= 0.3 && < 0.6+                 containers >= 0.3 && < 0.6,+                 binary >= 0.7 && < 0.8   exposed-modules:     Unbound.LocallyNameless,     Unbound.LocallyNameless.Name,