diff -upr Agda2.orig/Agda.cabal Agda2/Agda.cabal --- Agda2.orig/Agda.cabal 2007-08-16 23:52:02.000000000 +0900 +++ Agda2/Agda.cabal 2007-11-30 12:28:54.058825600 +0900 @@ -5,7 +5,7 @@ author: Ulf Norell, Catarina Co maintainer: Ulf Norell homepage: category: Theorem Proving -build-depends: base, mtl, QuickCheck >= 1.0 && < 2.0, readline, haskell98, haskell-src, binary >= 0.3, zlib +build-depends: base, mtl, QuickCheck >= 1.0 && < 2.0, haskell98, haskell-src, binary >= 0.3, zlib, containers, pretty, directory, old-time, bytestring, array synopsis: A dependently typed proof checker / programming language. hs-source-dirs: src/full exposed-modules: AgdaMain @@ -127,6 +127,7 @@ exposed-modules: AgdaMain TypeChecking.Telescope TypeChecking.With Utils.Char + Utils.Either Utils.FileName Utils.Fresh Utils.Function diff -upr Agda2.orig/src/full/Interaction/GhciTop.hs Agda2/src/full/Interaction/GhciTop.hs --- Agda2.orig/src/full/Interaction/GhciTop.hs 2007-08-16 23:52:00.000000000 +0900 +++ Agda2/src/full/Interaction/GhciTop.hs 2007-11-30 23:45:20.138792000 +0900 @@ -16,15 +16,15 @@ module Interaction.GhciTop -- , module SI , module Syntax.Scope.Base , module Syntax.Scope.Monad - , module Info +-- , module Info , module Syntax.Translation.ConcreteToAbstract , module Syntax.Translation.AbstractToConcrete , module Syntax.Translation.InternalToAbstract , module Syntax.Abstract.Name , module Interaction.Exceptions - , module B - , module CL +-- , module B +-- , module CL ) where diff -upr Agda2.orig/src/full/Interaction/Highlighting/Precise.hs Agda2/src/full/Interaction/Highlighting/Precise.hs --- Agda2.orig/src/full/Interaction/Highlighting/Precise.hs 2007-08-16 23:52:00.000000000 +0900 +++ Agda2/src/full/Interaction/Highlighting/Precise.hs 2007-11-30 23:45:52.445246400 +0900 @@ -90,7 +90,7 @@ newtype File = File { mapping :: Map Int -- | Returns the smallest position, if any, in the 'File'. smallestPos :: File -> Maybe Integer -smallestPos = fmap (fst . snd) . Map.minView . mapping +smallestPos = fmap (fst . fst) . Map.minViewWithKey . mapping ------------------------------------------------------------------------ -- Creation diff -upr Agda2.orig/src/full/TypeChecking/Rules/Def.hs Agda2/src/full/TypeChecking/Rules/Def.hs --- Agda2.orig/src/full/TypeChecking/Rules/Def.hs 2007-08-16 23:52:01.000000000 +0900 +++ Agda2/src/full/TypeChecking/Rules/Def.hs 2007-11-30 02:47:11.972089600 +0900 @@ -229,7 +229,7 @@ checkWhere n [A.Section _ m tel ds] ret dtel <- mapM prettyA tel dtel' <- prettyTCM =<< lookupSection m liftIO $ putStrLn $ "checking where section " ++ show dx ++ " " ++ show dtel - liftIO $ putStrLn $ " actual tele: " ++ show dtel' + liftIO $ putStrLn $ " actual tele: " ++ show dtel' x <- withCurrentModule m $ checkDecls ds >> ret return x checkWhere _ _ _ = __IMPOSSIBLE__ diff -upr Agda2.orig/src/full/TypeChecking/Rules/LHS.hs Agda2/src/full/TypeChecking/Rules/LHS.hs --- Agda2.orig/src/full/TypeChecking/Rules/LHS.hs 2007-08-16 23:52:01.000000000 +0900 +++ Agda2/src/full/TypeChecking/Rules/LHS.hs 2007-11-30 02:43:21.030011200 +0900 @@ -168,7 +168,7 @@ checkLeftHandSide ps a ret = do , text "tel0 =" <+> prettyTCM tel0 , text "b0 =" <+> prettyTCM b0 , text "gamma =" <+> prettyTCM gamma - , text "b =" <+> addCtxTel gamma (prettyTCM b) + , text "b =" <+> addCtxTel gamma (prettyTCM b) ] ] @@ -183,8 +183,8 @@ checkLeftHandSide ps a ret = do [ text "ps = " <+> fsep (map prettyA ps) , text "perm = " <+> text (show perm) , text "delta = " <+> prettyTCM delta - , text "dpi = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi) - , text "asb = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb) + , text "dpi = " <+> brackets (fsep $ punctuate comma $ map prettyTCM dpi) + , text "asb = " <+> brackets (fsep $ punctuate comma $ map prettyTCM asb) ] ] bindLHSVars ps delta $ bindAsPatterns asb $ do @@ -296,11 +296,11 @@ checkLeftHandSide ps a ret = do reportSDoc "tc.lhs.top" 15 $ addCtxTel delta1 $ sep [ text "preparing to unify" , nest 2 $ vcat - [ text "c =" <+> prettyTCM c <+> text ":" <+> prettyTCM a - , text "d =" <+> prettyTCM d <+> text ":" <+> prettyTCM da + [ text "c =" <+> prettyTCM c <+> text ":" <+> prettyTCM a + , text "d =" <+> prettyTCM d <+> text ":" <+> prettyTCM da , text "gamma =" <+> prettyTCM gamma - , text "vs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs) - , text "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws) + , text "vs =" <+> brackets (fsep $ punctuate comma $ map prettyTCM vs) + , text "ws =" <+> brackets (fsep $ punctuate comma $ map prettyTCM ws) ] ] diff -upr Agda2.orig/src/full/TypeChecking/Serialise.hs Agda2/src/full/TypeChecking/Serialise.hs --- Agda2.orig/src/full/TypeChecking/Serialise.hs 2007-08-16 23:52:01.000000000 +0900 +++ Agda2/src/full/TypeChecking/Serialise.hs 2007-11-30 23:46:18.012009600 +0900 @@ -1,6 +1,6 @@ {-# LANGUAGE OverlappingInstances, GeneralizedNewtypeDeriving #-} -{-# OPTIONS -cpp #-} +{-# OPTIONS -cpp -fglasgow-exts #-} -- | Serialisation of Agda interface files. @@ -32,7 +32,7 @@ import qualified Data.Binary.Get as B import qualified Data.Binary.Builder as B import qualified Data.ByteString.Lazy as L import qualified Data.ByteString.Lazy.Char8 as L8 -import qualified Data.ByteString.Base as BB +import qualified Data.ByteString as BB import Data.Word import qualified Codec.Compression.GZip as G @@ -237,7 +237,7 @@ encode x = B.encode currentInterfaceVers -- L.append is currently (GHC 6.6.1) strict in its second argument, -- and this somehow changes the semantics of encode when this module -- is compiled with optimisations turned on... - append (BB.LPS xs) (BB.LPS ys) = BB.LPS (xs ++ ys) + append = L.append -- | Decodes something encoded by 'encode'. Fails with 'error' if the -- interface version does not match the current interface version. diff -upr Agda2.orig/src/full/Utils/Maybe.hs Agda2/src/full/Utils/Maybe.hs --- Agda2.orig/src/full/Utils/Maybe.hs 2007-08-16 23:52:01.000000000 +0900 +++ Agda2/src/full/Utils/Maybe.hs 2007-11-30 01:34:27.726612800 +0900 @@ -7,10 +7,12 @@ module Utils.Maybe import Data.Monoid import Data.Maybe +{- instance Monoid (Maybe a) where mempty = Nothing mappend (Just x) _ = Just x mappend Nothing m = m +-} fromMaybeM :: Monad m => m a -> m (Maybe a) -> m a fromMaybeM m mm = maybe m return =<< mm