~ubuntu-branches/ubuntu/raring/agda/raring-proposed

Viewing changes to src/full/Agda/Syntax/Concrete/Name.hs

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2010-01-05 23:43:20 UTC
mfrom: (1.1.1 upstream)
Revision ID: james.westby@ubuntu.com-20100105234320-6ksc0sdsfhtweknu

Tags: 2.2.6-1

http://bugs.debian.org/559197

* New upstream release 2.2.6, for headlines please see:
  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-2-6
* debian/control
  + Bump standards-version to 3.8.3, no changes
  + Fix Vcs-Git to point to correct URL
  + Update build-depends for new upstream release
  + Undo arch/indep split per current pkg-haskell practice
  + Add Homepage field
* debian/copyright: Fix encoding to UTF-8 (thanks Lintian)
* debian/README.source: Remove, no repacking so not necessary any more
* debian/50agda.el:
  + Only load file if it exists, prevents a non-intrusive emacs warning
    where 50agda.el is left on system when package is removed.
    (Closes: #559197).
  + Do not load file on XEmacs — agda-mode is not compatible with XEmacs.

files added:
doc/release-notes/2-2-6.txt

src/full/Agda/Auto

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/NarrowingSearch.hs

src/full/Agda/Auto/Print.hs

src/full/Agda/Auto/SearchControl.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Auto/Typecheck.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs-boot

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/FindFile.hs-boot

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/MetaVars

src/full/Agda/TypeChecking/MetaVars/Occurs.hs

src/full/Agda/Utils/IO

src/full/Agda/Utils/IO/Binary.hs

src/full/Agda/Utils/IO/Locale.hs

src/full/Agda/Utils/IO/UTF8.hs

files removed:
debian/README.source

src/full/Agda/Utils/IO.hs

src/full/Agda/Utils/Monad

src/full/Agda/Utils/Monad/Undo.hs

src/full/Agda/Utils/Serialise.hs

files modified:
Agda.cabal

README

debian/50agda.el

debian/changelog

debian/control

debian/copyright

dist/build/Agda/Syntax/Parser/Lexer.hs

dist/build/Agda/Syntax/Parser/Parser.hs

src/agda-mode/Main.hs

src/data/Agda.css

src/data/emacs-mode/agda-input.el

src/data/emacs-mode/agda2-abbrevs.el

src/data/emacs-mode/agda2-highlight.el

src/data/emacs-mode/agda2-mode.el

src/data/emacs-mode/annotation.el

src/full/Agda/Compiler/Agate/Common.hs

src/full/Agda/Compiler/Agate/OptimizedPrinter.hs

src/full/Agda/Compiler/Alonzo/Main.hs

src/full/Agda/Compiler/MAlonzo/Compiler.hs

src/full/Agda/Compiler/MAlonzo/Encode.hs

src/full/Agda/Compiler/MAlonzo/Misc.hs

src/full/Agda/Compiler/MAlonzo/Primitives.hs

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine/CommandLine.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Interaction/Highlighting/Emacs.hs

src/full/Agda/Interaction/Highlighting/Generate.hs

src/full/Agda/Interaction/Highlighting/HTML.hs

src/full/Agda/Interaction/Highlighting/Precise.hs

src/full/Agda/Interaction/Highlighting/Vim.hs

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Name.hs

src/full/Agda/Syntax/Common.hs

src/full/Agda/Syntax/Concrete.hs

src/full/Agda/Syntax/Concrete/Definitions.hs

src/full/Agda/Syntax/Concrete/Name.hs

src/full/Agda/Syntax/Concrete/Pretty.hs

src/full/Agda/Syntax/Info.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Parser.hs

src/full/Agda/Syntax/Parser/LexActions.hs

src/full/Agda/Syntax/Parser/Lexer.x

src/full/Agda/Syntax/Parser/Monad.hs

src/full/Agda/Syntax/Parser/Parser.y

src/full/Agda/Syntax/Parser/Tokens.hs

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Syntax/Translation/AbstractToConcrete.hs

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Conversion.hs-boot

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/MetaVars.hs

src/full/Agda/TypeChecking/MetaVars.hs-boot

src/full/Agda/TypeChecking/Monad/Base.hs

src/full/Agda/TypeChecking/Monad/Builtin.hs

src/full/Agda/TypeChecking/Monad/Debug.hs

src/full/Agda/TypeChecking/Monad/Imports.hs

src/full/Agda/TypeChecking/Monad/MetaVars.hs

src/full/Agda/TypeChecking/Monad/Options.hs

src/full/Agda/TypeChecking/Monad/Signature.hs

src/full/Agda/TypeChecking/Monad/SizedTypes.hs

src/full/Agda/TypeChecking/Monad/State.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Records.hs-boot

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Rules/Builtin.hs

src/full/Agda/TypeChecking/Rules/Data.hs

src/full/Agda/TypeChecking/Rules/Decl.hs

src/full/Agda/TypeChecking/Rules/Def.hs

src/full/Agda/TypeChecking/Rules/LHS.hs

src/full/Agda/TypeChecking/Rules/LHS/Instantiate.hs

src/full/Agda/TypeChecking/Rules/LHS/Split.hs

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

src/full/Agda/TypeChecking/Rules/Record.hs

src/full/Agda/TypeChecking/Rules/Term.hs

src/full/Agda/TypeChecking/Serialise.hs

src/full/Agda/TypeChecking/SizedTypes.hs

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/Telescope.hs

src/full/Agda/TypeChecking/Test/Generators.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Impossible.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/QuickCheck.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/undefined.h

Show diffs side-by-side

added added

removed removed

src/full/Agda/Syntax/Concrete/Name.hs

module Agda.Syntax.Concrete.Name where

import Control.Applicative

import Data.List

import Data.Maybe

import Data.Generics (Typeable, Data)

import System.FilePath

import Test.QuickCheck

import Agda.Syntax.Common

import Agda.Syntax.Position

import Agda.Utils.FileName

import Agda.Utils.TestHelpers

import Agda.Utils.Pretty

#include "../../undefined.h"

import Agda.Utils.Impossible

115

122

| QName Name

116

123

deriving (Typeable, Data, Eq, Ord)

117

124

125

-- | Top-level module names.

126

127

-- Invariant: The list must not be empty.

128

129

newtype TopLevelModuleName

130

= TopLevelModuleName { moduleNameParts :: [String] }

131

deriving (Show, Eq, Ord, Typeable, Data)

132

133

-- | Turns a qualified name into a 'TopLevelModuleName'. The qualified

134

-- name is assumed to represent a top-level module name.

135

136

toTopLevelModuleName :: QName -> TopLevelModuleName

137

toTopLevelModuleName = TopLevelModuleName . map show . qnameParts

138

139

-- | Turns a top-level module name into a file name with the given

140

-- suffix.

141

142

moduleNameToFileName :: TopLevelModuleName -> String -> FilePath

143

moduleNameToFileName (TopLevelModuleName []) ext = __IMPOSSIBLE__

144

moduleNameToFileName (TopLevelModuleName ms) ext =

145

joinPath (init ms) </> last ms <.> ext

146

147

-- | Finds the current project's \"root\" directory, given a project

148

-- file and the corresponding top-level module name.

149

150

-- Example: If the module \"A.B.C\" is located in the file

151

-- \"/foo/A/B/C.agda\", then the root is \"/foo/\".

152

153

-- Precondition: The module name must be well-formed.

154

155

projectRoot :: AbsolutePath -> TopLevelModuleName -> AbsolutePath

156

projectRoot file (TopLevelModuleName m) =

157

mkAbsolute $

158

foldr (.) id (replicate (length m - 1) takeDirectory) $

159

takeDirectory $

160

filePath file

161

118

162

isHole :: NamePart -> Bool

119

163

isHole Hole = True

120

164

isHole _ = False

125

169

isInfix x = isHole (head xs) && isHole (last xs) where xs = nameParts x

126

170

isNonfix x = not (isHole (head xs)) && not (isHole (last xs)) where xs = nameParts x

127

171

128

type Suffix = String

129

130

131

moduleNameToFileName :: QName -> Suffix -> FilePath

132

moduleNameToFileName (QName x) ext = show x ++ ext

133

moduleNameToFileName (Qual m x) ext = show m ++ [slash] ++ moduleNameToFileName x ext

134

135

172

instance Show Name where

136

173

show (Name _ xs) = concatMap show xs

137

174

show (NoName _ _) = "_"

145

181

show (Qual m x) = show m ++ "." ++ show x

146

182

show (QName x) = show x

147

183

184

instance Pretty TopLevelModuleName where

185

pretty (TopLevelModuleName ms) = text $ intercalate "." ms

186

187

instance Arbitrary TopLevelModuleName where

188

arbitrary = TopLevelModuleName <$> listOf1 (listOf1 $ elements "AB")

189

190

instance CoArbitrary TopLevelModuleName where

191

coarbitrary (TopLevelModuleName m) = coarbitrary m

192

148

193

instance HasRange Name where

149

194

getRange (Name r ps) = r

150

195

getRange (NoName r _) = r

164

209

instance KillRange Name where

165

210

killRange (Name r ps) = Name (killRange r) ps

166

211

killRange (NoName r i) = NoName (killRange r) i

167

Older »