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

Viewing changes to src/full/Agda/TypeChecking/Monad/Signature.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/TypeChecking/Monad/Signature.hs

import qualified Data.Map as Map

import Data.List

import Data.Function

import qualified System.IO.UTF8 as UTF8

import qualified Agda.Utils.IO.Locale as LocIO

import Agda.Syntax.Abstract.Name

import Agda.Syntax.Common

204

oldDef { conPars = np - size ts, conData = copyName d }

205

Datatype{ dataPars = np, dataCons = cs } ->

206

oldDef { dataPars = np - size ts, dataClause = Just cl, dataCons = map copyName cs }

207

Record{ recPars = np, recTel = tel } ->

208

oldDef { recPars = np - size ts, recClause = Just cl, recTel = apply tel ts }

207

Record{ recPars = np, recConType = t, recTel = tel } ->

208

oldDef { recPars = np - size ts, recClause = Just cl

209

, recConType = apply t ts, recTel = apply tel ts

210

}

209

211

_ ->

210

212

Function { funClauses = [cl]

211

213

, funDelayed = NotDelayed

266

268

Constructor{ conInd = i } -> return i

267

269

_ -> __IMPOSSIBLE__

268

270

271

-- | Does the given constructor come from a single-constructor type?

272

273

-- Precondition: The name has to refer to a constructor.

274

singleConstructorType :: QName -> TCM Bool

275

singleConstructorType q = do

276

d <- theDef <$> getConstInfo q

277

case d of

278

Record {} -> return True

279

Constructor { conData = d } -> do

280

di <- theDef <$> getConstInfo d

281

return $ case di of

282

Record {} -> True

283

Datatype { dataCons = cs } -> length cs == 1

284

_ -> __IMPOSSIBLE__

285

_ -> __IMPOSSIBLE__

286

269

287

-- | Lookup the definition of a name. The result is a closed thing, all free

270

288

-- variables have been abstracted over.

271

289

getConstInfo :: MonadTCM tcm => QName -> tcm Definition

272

getConstInfo q = liftTCM $ do

273

ab <- treatAbstractly q

274

defs <- sigDefinitions <$> getSignature

275

idefs <- sigDefinitions <$> getImportedSignature

276

let smash = (++) `on` maybe [] (:[])

277

case smash (Map.lookup q defs) (Map.lookup q idefs) of

278

[] -> fail $ show (getRange q) ++ ": no such name " ++ show q

290

getConstInfo q = liftTCM $ join $ pureTCM $ \st env ->

291

let defs = sigDefinitions $ stSignature st

292

idefs = sigDefinitions $ stImports st

293

ab = treatAbstractly' q env

294

smash = (++) `on` maybe [] (:[])

295

in case smash (Map.lookup q defs) (Map.lookup q idefs) of

296

[] -> fail $ "Unbound name: " ++ show q

279

297

[d] -> mkAbs ab d

280

ds -> fail $ show (getRange q) ++ ": ambiguous name " ++ show q

298

ds -> fail $ "Ambiguous name: " ++ show q

281

299

where

282

300

mkAbs True d =

283

301

case makeAbstract d of

346

364

-- number of parameters if we're currently inside the section and 0 otherwise.

347

365

getSecFreeVars :: MonadTCM tcm => ModuleName -> tcm Nat

348

366

getSecFreeVars m = do

349

sig <- sigSections <$> getSignature

367

sig <- sigSections <$> getSignature

368

isig <- sigSections <$> getImportedSignature

350

369

top <- currentModule

351

370

case top `isSubModuleOf` m || top == m of

352

True -> return $ maybe 0 secFreeVars $ Map.lookup m sig

371

True -> return $ maybe 0 secFreeVars $ Map.lookup m (Map.union sig isig)

353

372

False -> return 0

354

373

355

374

-- | Compute the number of free variables of a module. This is the sum of

376

395

verboseS "tc.sig.inst" 30 $ do

377

396

ctx <- getContext

378

397

m <- currentModule

379

liftIO $ UTF8.putStrLn $ "instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++

398

liftIO $ LocIO.putStrLn $ "instDef in " ++ show m ++ ": " ++ show (defName d) ++ " " ++

380

399

unwords (map show . take (size vs) . reverse . map (fst . unArg) $ ctx)

381

400

return $ d `apply` vs

382

401

Older »