make pi-forall work on both: ghc 7.8.4 and 7.10.3, intial commit

Author: reuleaux

full/README renamed to full/README.md

@@ -25,11 +25,11 @@ Features
   - bidirectional type checking
   - erased arguments (forall)
   - propositional equality 
-  - inductive & indexed datatypes 
+  - indexed datatypes 
 
 Not covered (Future work!)
 --------------------------
-  - nontermination
+  - termination & inductive datatypes
   - effects
   - co-induction
   - type inference & unification

full/pi-forall.cabal

@@ -8,7 +8,7 @@ Author: Stephanie Weirich <[email protected]>, based on code by Trellys Tea
 Maintainer: Stephanie Weirich <[email protected]>
 Cabal-Version: >= 1.2
 Build-type: Simple
-tested-with: GHC == 7.6.3
+tested-with: GHC == 7.8.4, GHC == 7.10.3
 
 library
   hs-source-dirs: src/
@@ -22,20 +22,17 @@ executable pi-forall
   hs-source-dirs: src/
   Main-is: Main.hs
   Build-depends: base >=4,
-                 parsec >= 3.1 && < 3.1.5,
+                 parsec (>= 3.1 && < 3.1.5) || (>= 3.1.8 && < 3.2),
                  pretty >= 1.0.1.0,
-                 RepLib >= 0.5.3 && < 0.6, 
-                 unbound >= 0.4.2 && < 0.5,
-                 mtl,
-                 -- 0.2.2.0, 0.3.0.0
+                 unbound-generics >= 0.2,
+                 mtl >= 2.2.1,
                  transformers,
                  array >= 0.3.0.2 && < 0.6,
                  containers,
                  directory,
                  filepath,
                  HUnit,
-                 QuickCheck,
-                 bimap == 0.2.4
+                 QuickCheck
   Ghc-Options:  -Wall -fno-warn-unused-matches
 
 

full/src/Environment.hs

@@ -1,6 +1,6 @@
 {- OPLSS -}
 
-{-# LANGUAGE GADTs, NamedFieldPuns, FlexibleContexts, ViewPatterns, RankNTypes #-}
+{-# LANGUAGE GADTs, NamedFieldPuns, FlexibleContexts, ViewPatterns, RankNTypes, CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-matches #-}
 
 -- | Utilities for managing a typechecking context.
@@ -21,13 +21,29 @@ module Environment
 import Syntax
 import PrettyPrint
 
-import Unbound.LocallyNameless hiding (Data)
+import Unbound.Generics.LocallyNameless
 
 import Text.PrettyPrint.HughesPJ
 import Text.ParserCombinators.Parsec.Pos(SourcePos)
 import Control.Monad.Reader
 import Control.Monad.Except
+
+
+
+#ifdef MIN_VERSION_GLASGOW_HASKELL
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
+-- ghc >= 7.10.3
+#else
+-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
+#endif
+#else
+-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
 import Data.Monoid 
+#endif
+
+
+
+
 
 import Data.List
 import Data.Maybe (listToMaybe, catMaybes)

full/src/Equal.hs

@@ -1,6 +1,6 @@
 {- PiForall language, OPLSS -}
 
-{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE ViewPatterns, FlexibleContexts, CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-matches #-}
 
 -- | Compare two terms for equality
@@ -12,9 +12,22 @@ module Equal (whnf, equate, ensurePi,
 import Syntax
 import Environment
 
-import Unbound.LocallyNameless hiding (Data, Refl)
+import Unbound.Generics.LocallyNameless
 import Control.Monad.Except (catchError, zipWithM, zipWithM_)
+
+
+#ifdef MIN_VERSION_GLASGOW_HASKELL
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
+-- ghc >= 7.10.3
+#else
+-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
+#endif
+#else
+-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
 import Control.Applicative ((<$>))
+#endif
+
+
 
 
 -- | compare two expressions for equality

full/src/LayoutToken.hs

@@ -18,7 +18,7 @@
 -- 
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE PolymorphicComponents, NoMonomorphismRestriction, KindSignatures  #-}
+{-# LANGUAGE PolymorphicComponents, NoMonomorphismRestriction, KindSignatures, FlexibleContexts  #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-unused-do-bind -fno-warn-unused-matches #-}
 
 module LayoutToken
@@ -744,20 +744,20 @@ makeTokenParser languageDef open sep close
     layoutBegin = (symbol open)  <?> ("layout opening symbol ("++open++")")
 
     layout p stop =
-	   (do { try layoutBegin; xs <- sepBy p (symbol ";") 
-	       ; layoutEnd <?> "explicit layout closing brace"
-	       ; stop; return (xs)}) <|>
+           (do { try layoutBegin; xs <- sepBy p (symbol ";") 
+               ; layoutEnd <?> "explicit layout closing brace"
+               ; stop; return (xs)}) <|>
            (do { indent; xs <- align p stop; return xs})
 
     align p stop = ormore <|> zero
       where zero = do { stop; option "" layoutSep; undent; return []}
-	    ormore = do { x <- p
-	                ; whiteSpace
-	                ; (do { try layoutSep; xs <- align p stop; return (x:xs)}) <|>
-	                  (do { try layoutEnd; stop; return([x])}) <|>
-	                     -- removing indentation happens automatically
-	                     -- in function whiteSpace
-	                  (do { stop; undent; return ([x])})}
+            ormore = do { x <- p
+                        ; whiteSpace
+                        ; (do { try layoutSep; xs <- align p stop; return (x:xs)}) <|>
+                          (do { try layoutEnd; stop; return([x])}) <|>
+                             -- removing indentation happens automatically
+                             -- in function whiteSpace
+                          (do { stop; undent; return ([x])})}
 
     whiteSpace =
        do { (col1,_,_) <- getInfo
@@ -779,7 +779,7 @@ makeTokenParser languageDef open sep close
                                     rev (s:ss) xs = rev ss (s++xs)
                                 in adjust (col2,p:ps,[])
               (cs,p:ps,_,GT) -> return ()
-          }    	             
+          }                  
 getInfo :: forall (m :: * -> *) t t1.
                  Monad m =>
                  ParsecT t1 t m (Column, t, t1)

full/src/Modules.hs

@@ -1,6 +1,6 @@
 {- PiForall language, OPLSS -}
 
-{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleContexts, CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-orphans #-}
 
 -- | Tools for working with multiple source files
@@ -10,7 +10,23 @@ import Syntax
 import Parser(parseModuleFile, parseModuleImports)
 
 import Text.ParserCombinators.Parsec.Error
+
+
+#ifdef MIN_VERSION_GLASGOW_HASKELL
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
+-- ghc >= 7.10.3
+#else
+-- older ghc versions
 import Control.Applicative 
+#endif
+#else
+-- MIN_VERSION_GLASGOW_HASKELL not even defined yet
+import Control.Applicative
+#endif
+
+
+
+
 import Control.Monad.Except
 import Control.Monad.State.Lazy
 import System.FilePath

full/src/Parser.hs

@@ -1,6 +1,6 @@
 {- PiForall language, OPLSS -}
 
-{-# LANGUAGE PatternGuards, FlexibleInstances, FlexibleContexts, TupleSections, ExplicitForAll #-}
+{-# LANGUAGE PatternGuards, FlexibleInstances, FlexibleContexts, TupleSections, ExplicitForAll, CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-orphans #-}
 
 -- | A parsec-based parser for the concrete syntax.
@@ -15,16 +15,35 @@ module Parser
 
 import Syntax hiding (moduleImports)
 
-import Unbound.LocallyNameless hiding (Data,Refl,Infix,join,name)
+import Unbound.Generics.LocallyNameless
 
 import Text.Parsec hiding (State,Empty)
 import Text.Parsec.Expr(Operator(..),Assoc(..),buildExpressionParser)
 import qualified LayoutToken as Token
 
 import Control.Monad.State.Lazy hiding (join)
+
+
+#ifdef MIN_VERSION_GLASGOW_HASKELL
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
+-- ghc >= 7.10.3
+#else
+-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
+#endif
+#else
+-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
 import Control.Applicative ( (<$>), (<*>))
+#endif
+
+
+
+
+
 import Control.Monad.Except hiding (join)
 
+
+
+
 import Data.List
 import qualified Data.Set as S
 
@@ -158,7 +177,7 @@ trellysStyle = Token.LanguageDef
                 , Token.nestedComments = True
                 , Token.identStart     = letter
                 , Token.identLetter    = alphaNum <|> oneOf "_'"
-                , Token.opStart	       = oneOf ":!#$%&*+.,/<=>?@\\^|-"
+                , Token.opStart        = oneOf ":!#$%&*+.,/<=>?@\\^|-"
                 , Token.opLetter       = oneOf ":!#$%&*+.,/<=>?@\\^|-"
                 , Token.caseSensitive  = True
                 , Token.reservedNames =

full/src/PrettyPrint.hs

@@ -1,22 +1,40 @@
 {- PiForall language, OPLSS -}
 
-{-# LANGUAGE TypeSynonymInstances,ExistentialQuantification,FlexibleInstances, UndecidableInstances, FlexibleContexts,
-             ViewPatterns, DefaultSignatures
- #-}
+{-# LANGUAGE TypeSynonymInstances,ExistentialQuantification,FlexibleInstances, UndecidableInstances, ViewPatterns, DefaultSignatures, GeneralizedNewtypeDeriving, FlexibleContexts, CPP #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-matches -fno-warn-name-shadowing #-}
 
 -- | A Pretty Printer. 
 module PrettyPrint(Disp(..), D(..))  where
 
+import Data.Typeable (Typeable)
+
 import Syntax
-import Unbound.LocallyNameless hiding (empty,Data,Refl)
+import Unbound.Generics.LocallyNameless
+import Unbound.Generics.LocallyNameless.Internal.Fold (toListOf)
 
 import Control.Monad.Identity
 import Control.Monad.Reader
 import Text.PrettyPrint as PP
 import Text.ParserCombinators.Parsec.Pos (SourcePos, sourceName, sourceLine, sourceColumn)
 import Text.ParserCombinators.Parsec.Error (ParseError)
-import Control.Applicative ((<$>), (<*>))
+
+
+#ifdef MIN_VERSION_GLASGOW_HASKELL
+#if MIN_VERSION_GLASGOW_HASKELL(7,10,3,0)
+-- ghc >= 7.10.3
+#else
+-- older ghc versions, but MIN_VERSION_GLASGOW_HASKELL defined
+#endif
+#else
+-- MIN_VERSION_GLASGOW_HASKELL not even defined yet (ghc <= 7.8.x)
+import Control.Applicative (Applicative(..), (<$>), (<*>))
+#endif
+
+
+
+
+
+
 import qualified Data.Set as S
 
 -- | The 'Disp' class governs types which can be turned into 'Doc's
@@ -32,11 +50,11 @@ class Disp d where
 
 cleverDisp :: (Display d, Alpha d) => d -> Doc
 cleverDisp d =
-  runIdentity (runReaderT (display d) initDI)
+  runReaderDispInfo (display d) initDI
 
 
 instance Disp Term 
-instance Rep a => Disp (Name a) 
+instance Typeable a => Disp (Name a) 
 instance Disp Telescope 
 instance Disp Pattern 
 instance Disp Match 
@@ -132,12 +150,12 @@ instance Disp ConstructorDef where
 -- 
 data DispInfo = DI
   {
-  showAnnots :: Bool,           -- ^ should we show the annotations?  
+  showAnnots :: Bool,         -- ^ should we show the annotations?  
   dispAvoid  :: S.Set AnyName   -- ^ names that have been used
   }
 
 
-instance LFresh (Reader DispInfo) where
+instance LFresh (ReaderDispInfo) where
   lfresh nm = do
       let s = name2String nm
       di <- ask;
@@ -152,7 +170,13 @@ instance LFresh (Reader DispInfo) where
 initDI :: DispInfo
 initDI = DI False S.empty
 
-type M a = (ReaderT DispInfo Identity) a
+newtype ReaderDispInfo a = ReaderDispInfo (ReaderT DispInfo Identity a)
+                         deriving (Functor, Applicative, Monad, MonadReader DispInfo)
+
+runReaderDispInfo :: ReaderDispInfo a -> DispInfo -> a
+runReaderDispInfo (ReaderDispInfo comp) = runReader comp
+
+type M a = ReaderDispInfo a
 
 -- | The 'Display' class is like the 'Disp' class. It qualifies
 --   types that can be turned into 'Doc'.  The difference is that the
@@ -294,7 +318,7 @@ instance Display Term where
         da <- display (unembed a)
         dn <- display n
         db <- display b
-        let lhs = if (n `elem` fv b) then
+        let lhs = if (n `elem` toListOf fv b) then
                 parens (dn <+> colon <+> da)
               else 
                 wraparg (unembed a) da
@@ -362,7 +386,7 @@ instance Display Term where
         dn <- display n
         db <- display b
         let lhs = mandatoryBindParens Erased  $
-              if (n `elem` fv b) then
+              if (n `elem` toListOf fv b) then
                 (dn <+> colon <+> da)
               else 
                 da
@@ -470,7 +494,7 @@ gatherBinders body = do
   return ([], db)
 
 -- Assumes that all terms were opened safely earlier.
-instance Rep a => Display (Name a) where
+instance Typeable a => Display (Name a) where
   display n = return $ (text . name2String) n
 
 instance Disp [Term] where