unbound-generics 0.3.4 → 0.4.0

raw patch · 10 files changed

+326/−15 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Changelog.md +89/−0
• examples/Prof.hs +42/−0
• src/Unbound/Generics/LocallyNameless.hs +2/−0
• src/Unbound/Generics/LocallyNameless/Ignore.hs +47/−0
• src/Unbound/Generics/LocallyNameless/Operations.hs +13/−0
• src/Unbound/Generics/LocallyNameless/Subst.hs +13/−14
• test/TestIgnore.hs +52/−0
• test/TestRefine.hs +60/−0
• test/test-main.hs +4/−0
• unbound-generics.cabal +4/−1

@@ -1,3 +1,92 @@+# NEXT++# 0.4.0++* New binding specification type `Ignore`.++  Any two `Ignore T` terms will always be alpha-equivalent to each other, will+  be considered to contain no variables, and will not have any substitution+  apply beneath `Ignore`.  Useful for attaching annotation terms to your AST.++  ```haskell+    import Text.Parsec.Pos (SourcePos)+    +	data Expr =+	   ...+	   | Lambda (Ignore SourcePos) (Bind (Name Expr) Expr)+  ```++  As expected, any two `Lambda` expressions will be considered alpha-equivalent+  even if they differ in source position.++  Note that the `Ignore` will block operations on `Name a` for all `a`, which can be a little unexpected:++  ```haskell+    data Ty =+	  TyVar (Name Ty)+      | TyArr Ty Ty+    +    instance Subst Ty Ty where+	  ...++	data Expr =+	  ...+	  | Var (Name Expr)+	  | Lambda (Ignore Ty) (Bind (Name Expr) Expr)+    +     instance Subst Ty Expr+  ```++  Applying a substitution of a type for a free type variable to a `Lambda` will+  not descend into the `Ignore Ty`.++  Thanks Reed Mullanix (TOTWBF) for the new operation.++* Fix an issue in substitution where traversal would not continue in+  an AST node for which `isvar` or `isCoerceVar` is defined to return+  non-`Nothing` but which had additional structure.++  For example, in a language with meta variables and explicit substitutions:+  ```haskell+     data Expr =+	   ...+         -- normal variables that stand for expressions+       | Var (Name Expr)+          -- a meta variable occurrence and an explicit substitution+		  -- of expressions to substitute in for the free variables+	   | MetaVar (Name Meta) [(Name Expr, Expr)]+     -- a meta variable stands for an expression with some free term vars+	 data Meta = MetaVar Expr++     -- substitution for a meta in an expression+	 instance Subst Expr Meta where+	   isCoerceVar (MetaVar u sub) = Just (SubstCoerce u (Just . applyExplicitSubst sub))+	 applyExplicitSubst :: [(Name Expr, Expr)] -> Meta -> Expr+	 applyExplicitSubst s (MetaVar e) = substs s e+  ```++  Given an expression `e1` defined as `MetaVar "u" [("x", 10)]`, we may want to+  substitute a `Meta ("x" + "x")` for `"u"`  to get `10 + 10` (that is,+  we replace `"u"` by the expression `"x" + "x"` and immediately apply+  the substitution `10` for `"x"`).++  Now suppose we have an expression `e2` defined as `MetaVar "v" [("y",+  e1)]` (that is, an occurrence of meta var "v" together with a+  substitution of `e1` from above for `"y"`).  If we again try to+  substitute `Meta ("x" + "x")` for `"u"` in `e2`, we would expect to+  get `MetaVar "v" [("y", 10 + 10)]` (that is, since "v" is not equal to+  "u", we leave the meta var alone, but substitute for any occurrences+  of "u" in the explicit substitution, so `e1` becomes `10 + 10` as+  before).++  The bug in previous versions of `unbound-generics` was that we would+  incorrectly leave `MetaVar "v" [("y", e1)]` unchanged as soon as we+  saw that `isCoerceVar (MetaVar "v" [("y", e1)])` returned+  `Just (SubstCoerce "u" ...)` where `"u" /= "v"`.++  Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue.+  https://github.com/lambdageek/unbound-generics/issues/26+ # 0.3.4  * Bump `containers` upper bound to support `0.6`.

@@ -0,0 +1,42 @@+{-# language GADTs, RankNTypes #-}+module Prof where++import Data.Profunctor++data Shop a b s t where+  Shop :: (s -> a) -> (s -> b -> t) -> Shop a b s t++type Optic p s t a b  = p a b -> p s t+type Lens s t a b = forall p . (Strong p) => Optic p s t a b++lens :: (s -> a) -> (s -> b -> t) -> Lens s t a b+lens get set pab = dimap (\s -> (s, get s)) (uncurry set) (second' pab)++instance Profunctor (Shop a b) where+  dimap f g (Shop get set) = Shop (get . f) (\s -> g . set (f s))++instance Strong (Shop a b) where+   first' (Shop get set) = Shop (get . fst) (\(s,c) b -> (set s b, c))++withLens :: Lens s t a b -> ((s -> a) -> (s -> b -> t) -> r) -> r+withLens l k = case l (Shop id (const id)) of+                 Shop getter setter -> k getter setter+++type Prism s t a b = forall p . (Choice p) => Optic p s t a b++prism :: (s -> Either t a) -> (b -> t) -> Prism s t a b+prism view review pab = dimap view (either id review) (right' pab)++data Market a b s t where+  Market :: (s -> Either t a) -> (b -> t) -> Market a b s t++instance Profunctor (Market a b) where+  dimap f g (Market view review) = Market (either (Left . g) Right . (view . f)) (g . review)++instance Choice (Market a b) where+  left' (Market view review) = Market (either (either (Left . Left) Right . view) (Left . Right)) (Left . review)++withPrism :: Prism s t a b -> ((s -> Either t a) -> (b -> t) -> r) -> r+withPrism l k = case l (Market Right id) of+                  Market view review -> k view review

@@ -20,6 +20,7 @@   module Unbound.Generics.LocallyNameless.Name,   module Unbound.Generics.LocallyNameless.Operations,   module Unbound.Generics.LocallyNameless.Bind,+  module Unbound.Generics.LocallyNameless.Ignore,   module Unbound.Generics.LocallyNameless.Embed,   module Unbound.Generics.LocallyNameless.Shift,   module Unbound.Generics.LocallyNameless.Rebind,@@ -32,6 +33,7 @@ import Unbound.Generics.LocallyNameless.Alpha import Unbound.Generics.LocallyNameless.Name hiding (Bn, Fn) import Unbound.Generics.LocallyNameless.Bind hiding (B)+import Unbound.Generics.LocallyNameless.Ignore hiding (I) import Unbound.Generics.LocallyNameless.Embed import Unbound.Generics.LocallyNameless.Shift import Unbound.Generics.LocallyNameless.Rebind hiding (Rebnd)

@@ -0,0 +1,47 @@+-- |+-- Module     : Unbound.Generics.LocallyNameless.Ignore+-- Copyright  : (c) 2018, Reed Mullanix+-- License    : BSD3 (See LICENSE)+-- Maintainer : Reed Mullanix+-- Stability  : experimental+--+-- Ignores a term for the purposes of alpha-equality and substitution+{-# LANGUAGE DeriveGeneric #-}+module Unbound.Generics.LocallyNameless.Ignore (+    Ignore(..)+    ) where++import Control.DeepSeq (NFData(..))+import Control.Applicative+import Data.Monoid ++import GHC.Generics (Generic)++import Unbound.Generics.LocallyNameless.Alpha++-- | Ignores a term 't' for the purpose of alpha-equality and substitution+data Ignore t = I !t+        deriving (Generic)++instance (NFData t) => NFData (Ignore t) where+    rnf (I t) = rnf t `seq` ()++instance (Show t) => Show (Ignore t) where+    showsPrec prec (I t) = +        showParen (prec > 0) (showString "<-" +                              . showsPrec prec t+                              . showString "->")++instance (Show t) => Alpha (Ignore t) where+    aeq' _ _ _ = True+    fvAny' _ _ = pure+    isPat _ = inconsistentDisjointSet+    isTerm _ = mempty+    close _ _ = id+    open _ _ = id+    namePatFind  _ = NamePatFind $ const $ Left 0+    nthPatFind _ = NthPatFind Left+    swaps' _ _ = id+    lfreshen' _ i cont = cont i mempty+    freshen' _ i = return (i, mempty)+    acompare' _ _ _ = EQ

@@ -40,6 +40,10 @@        , trec        , untrec        , luntrec+         -- * Opaque terms+       , Ignore+       , ignore+       , unignore        ) where  import Control.Applicative (Applicative)@@ -55,6 +59,7 @@ import Unbound.Generics.LocallyNameless.Embed (Embed(..), IsEmbed(..)) import Unbound.Generics.LocallyNameless.Rebind import Unbound.Generics.LocallyNameless.Rec+import Unbound.Generics.LocallyNameless.Ignore import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf, justFiltered) import Unbound.Generics.LocallyNameless.Internal.Lens (view) import Unbound.Generics.LocallyNameless.Internal.Iso (from)@@ -213,3 +218,11 @@ luntrec :: (Alpha p, LFresh m) => TRec p -> m p luntrec (TRec b) =   lunbind b $ \(p, ()) -> return (unrec p)++-- | Constructor for ignoring a term for the purposes of alpha-equality and substs+ignore :: t -> Ignore t+ignore t = I t++-- | Destructor for ignored terms+unignore :: Ignore t -> t+unignore (I t) = t

@@ -56,6 +56,7 @@ import Unbound.Generics.LocallyNameless.Alpha import Unbound.Generics.LocallyNameless.Embed import Unbound.Generics.LocallyNameless.Shift+import Unbound.Generics.LocallyNameless.Ignore import Unbound.Generics.LocallyNameless.Bind import Unbound.Generics.LocallyNameless.Rebind import Unbound.Generics.LocallyNameless.Rec@@ -90,10 +91,10 @@   subst n u x =     if (isFreeName n)     then case (isvar x :: Maybe (SubstName a b)) of-      Just (SubstName m) -> if m == n then u else x-      Nothing -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of-        Just (SubstCoerce m f) -> if m == n then maybe x id (f u) else x-        Nothing -> to $ gsubst n u (from x)+      Just (SubstName m) | m == n -> u+      _ -> case (isCoerceVar x :: Maybe (SubstCoerce a b)) of+        Just (SubstCoerce m f) | m == n -> maybe x id (f u)+        _ -> to $ gsubst n u (from x)     else error $ "Cannot substitute for bound variable " ++ show n    substs :: [(Name b, b)] -> a -> a@@ -101,16 +102,10 @@   substs ss x     | all (isFreeName . fst) ss =       case (isvar x :: Maybe (SubstName a b)) of-        Just (SubstName m) ->-          case find ((==m) . fst) ss of-            Just (_, u) -> u-            Nothing     -> x-        Nothing -> case isCoerceVar x :: Maybe (SubstCoerce a b) of -            Just (SubstCoerce m f) ->-              case find ((==m) . fst) ss of -                  Just (_, u) -> maybe x id (f u)-                  Nothing -> x-            Nothing -> to $ gsubsts ss (from x)+        Just (SubstName m) | Just (_, u) <- find ((==m) . fst) ss -> u+        _ -> case isCoerceVar x :: Maybe (SubstCoerce a b) of +            Just (SubstCoerce m f) | Just (_, u) <- find ((==m) . fst) ss -> maybe x id (f u)+            _ -> to $ gsubsts ss (from x)     | otherwise =       error $ "Cannot substitute for bound variable in: " ++ show (map fst ss) @@ -185,3 +180,7 @@ instance (Subst c p) => Subst c (Rec p)  instance (Alpha p, Subst c p) => Subst c (TRec p)++instance Subst a (Ignore b) where+  subst _ _ = id+  substs _ = id

@@ -0,0 +1,52 @@+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}+module TestIgnore (test_ignore) where++import Data.Typeable(Typeable)+import GHC.Generics (Generic)+import Unbound.Generics.LocallyNameless++import AlphaAssertions++import Test.Tasty+import Test.Tasty.HUnit++type Var = Name Term++type SourcePos = (Int, Int)+data SourceSpan = SourceSpan +    { start :: SourcePos+    , end :: SourcePos+    }+    deriving (Show)++data Term+    = Var Var+    | Lam (Bind Var Term)+    | App Term Term+    | Ann (Ignore SourceSpan) Term+    | NoSubst (Ignore Term)+    deriving (Show, Typeable, Generic)++instance Alpha Term+instance Subst Term Term where+    isvar (Var x) = Just $ SubstName x+    isvar _ = Nothing++lam :: Var -> Term -> Term+lam x t = Lam (bind x t)++x :: Var+x = s2n "x"++y :: Var+y = s2n "y"++t1 :: Term+t1 = Ann (ignore (SourceSpan (0,0) (0,1))) (Var x)++t2 :: Term+t2 = Ann (ignore (SourceSpan (1,0) (1,10))) (Var x)++test_ignore :: TestTree+test_ignore =+    testCase "<-(0,0) (0,1)-> x = <-(1,0) (1,10)-> x" $ assertAeq t1 t2

@@ -0,0 +1,60 @@+{-# LANGUAGE DeriveGeneric, DeriveDataTypeable, MultiParamTypeClasses #-}+module TestRefine (test_refine) where++import Data.Typeable (Typeable)+import GHC.Generics (Generic)+import Unbound.Generics.LocallyNameless++import AlphaAssertions++import Test.Tasty+import Test.Tasty.HUnit++-- Regular variables range over terms+type Var = Name Term++-- Metavariables range over extracts+type MetaVar = Name Extract++data Term +    = Var Var+    | Hole MetaSubst MetaVar -- Every occurance of a metavariable must subst away fvs of extract+    | Lam (Bind Var Term)+    | App Term Term+    deriving (Generic, Typeable, Show)++-- Extracts represent code extracted via refinement+newtype Extract = Extract { extractTerm :: Term }+    deriving (Generic, Typeable, Show)++newtype MetaSubst = MetaSubst { unMetaSubst :: [(Var, Term)] }+    deriving (Generic, Typeable, Show)++instance Alpha Term+instance Alpha Extract+instance Alpha MetaSubst++instance Subst Term Term where+    isvar (Var x) = Just $ SubstName x+    isvar _ = Nothing++instance Subst Extract Term where+    isCoerceVar (Hole ms x) = Just $ SubstCoerce x (Just . applyMetaSubst ms)+    isCoerceVar _ = Nothing++applyMetaSubst :: MetaSubst -> Extract -> Term+applyMetaSubst (MetaSubst ms) e = substs ms $ extractTerm e++instance Subst Term MetaSubst+instance Subst Extract MetaSubst++test_refine :: TestTree+test_refine =+    testCase "subst ?1 x <a/?1>?0 = <a/x>?0"+    $ let h0 = s2n "0" :: MetaVar+          h1 = s2n "1" :: MetaVar+          a = s2n "a" :: Var+          x = s2n "x" :: Var+          e1 = Hole (MetaSubst [(a, Hole (MetaSubst []) h1)]) h0+          e2 = Hole (MetaSubst [(a, Var x)]) h0+      in assertAeq (subst h1 (Extract $ Var x) e1) e2

@@ -7,6 +7,8 @@ import PropOpenClose import TinyLam import TestACompare+import TestRefine+import TestIgnore import TestShiftEmbed import TestTH @@ -16,6 +18,8 @@          test_calc        , test_parallelReduction        , test_openClose+       , test_refine+       , test_ignore        , test_tinyLam        , test_acompare        , test_shiftEmbed

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                unbound-generics-version:             0.3.4+version:             0.4.0 synopsis:            Support for programming with names and binders using GHC Generics description:         Specify the binding structure of your data type with an                      expressive set of type combinators, and unbound-generics@@ -38,6 +38,7 @@                        Unbound.Generics.LocallyNameless.LFresh                        Unbound.Generics.LocallyNameless.Alpha                        Unbound.Generics.LocallyNameless.Bind+                       Unbound.Generics.LocallyNameless.Ignore                        Unbound.Generics.LocallyNameless.Rebind                        Unbound.Generics.LocallyNameless.Embed                        Unbound.Generics.LocallyNameless.Shift@@ -81,6 +82,8 @@                        TestParallelReduction                        PropOpenClose                        TinyLam+                       TestRefine+                       TestIgnore                        TestACompare                        TestShiftEmbed                        TestTH