unbound 0.3 → 0.3.1

raw patch · 6 files changed

+71/−10 lines, 6 filesdep ~RepLib

Dependency ranges changed: RepLib

Files

• CHANGES +5/−1
• Unbound/LocallyNameless/Alpha.hs +4/−5
• Unbound/LocallyNameless/Ops.hs +3/−1
• Unbound/Util.hs +3/−0
• examples/LCTyped.hs +53/−0
• unbound.cabal +3/−3

@@ -29,7 +29,7 @@    * Clean up some compiler warnings. -Version 0.2.6: 24 August 2011+Version 0.3: 24 August 2011    * New permutation- and set-binding functions, for creating binders     which don't care about the order of multiple bound names, and/or@@ -37,3 +37,7 @@    * Bump RepLib dependency to 0.5, which now has support for GADTs     without existential type variables.++Version 0.3.1: 25 August 2011++  * Update to build on GHC 7.2.1

@@ -340,17 +340,16 @@   freshenD  :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName),
   lfreshenD :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b,
   aeqD      :: AlphaCtx -> a -> a -> Bool,
-  -- matchD    :: AlphaCtx -> a -> a -> Maybe (Perm AnyName),
+  acompareD :: AlphaCtx -> a -> a -> Ordering,
   closeD    :: Alpha b => AlphaCtx -> b -> a -> a,
   openD     :: Alpha b => AlphaCtx -> b -> a -> a,
   findpatD  :: a -> AnyName -> FindResult,
-  nthpatD   :: a -> NthCont,
-  acompareD :: AlphaCtx -> a -> a -> Ordering
+  nthpatD   :: a -> NthCont
   }
 
 instance Alpha a => Sat (AlphaD a) where
   dict = AlphaD isPat isTerm isEmbed swaps' fv' freshen' lfreshen' aeq' -- match'
-           close open findpatrec nthpatrec acompare'
+          acompare' close open findpatrec nthpatrec 
 
 ----------------------------------------------------------------------
 -- Generic definitions for 'Alpha' methods.  (Note that all functions
@@ -773,7 +772,7 @@ 
 -- note: for Embeds, when the mode is "term" then we are
 -- implementing the "binding" version of the function
--- and we generally should treat the annots as constants
+-- and we generally should treat the embeds as constants
 instance Alpha t => Alpha (Embed t) where
    isPat (Embed t)   = if (isTerm t) then Just [] else Nothing
    isTerm _          = False

@@ -1,4 +1,6 @@-{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE TypeSynonymInstances+           , FlexibleInstances+  #-} {-# OPTIONS_GHC -fno-warn-orphans #-} ---------------------------------------------------------------------- -- |

@@ -91,3 +91,6 @@   union     = S.union   cmap      = S.map +disjoint :: Ord a => S.Set a -> S.Set a -> Bool+disjoint s1 s2 = S.null( S.intersection s1 s2 )+

@@ -0,0 +1,53 @@+{-# 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,10 +1,10 @@ name:           unbound-version:        0.3+version:        0.3.1 license:        BSD3 license-file:   LICENSE build-type:     Simple cabal-version:  >= 1.6-tested-with:    GHC == 7.0.1, GHC == 7.0.3+tested-with:    GHC == 7.0.1, GHC == 7.0.3, GHC == 7.0.4, GHC == 7.2.1 author:         Stephanie Weirich maintainer:     Brent Yorgey <byorgey@cis.upenn.edu>                 Stephanie Weirich <sweirich@cis.upenn.edu>@@ -30,7 +30,7 @@  Library   build-depends: base >= 4.3 && < 5,-                 RepLib >= 0.5,+                 RepLib >= 0.5.1 && < 0.6,                  mtl >= 2.0 && < 2.1, transformers >= 0.2.2.0 && < 0.2.3,                  containers >= 0.3 && < 0.5   exposed-modules: