← Back to branch summary

~ubuntu-branches/ubuntu/trusty/agda/trusty

~ubuntu-branches/ubuntu/trusty/agda/trusty

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Records.hs-boot

Committer: Package Import Robot
Author(s): Iain Lane
Date: 2011-11-23 10:12:59 UTC
mfrom: (12.1.3 sid)
Revision ID: package-import@ubuntu.com-20111123101259-zhs3e4ynpck20hmu

Tags: 2.3.0-1

* [c0e4746] Imported Upstream version 2.3.0. New/changed features include:
  + New more liberal syntax for mutually recursive definitions
  + Pattern matching on lambdas
  + New syntax for updating (some fields of) records
  + Universe polymorphism is now enabled by default
  + New type of hidden function argument: instance arguments
  + Dependent irrelevant function types and records with irrelevant fields
  + See http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Version-2-3-0
    for a full list
* [369ed3a] Update BDs in line with cabal requirements in new upstream
* [3798aee] Remove all patches. They are all now upstream.

files added:
doc/release-notes/2-3-0.txt

src/full/Agda/Compiler/Epic/CaseOpts.hs

src/full/Agda/Compiler/Epic/ForceConstrs.hs

src/full/Agda/Compiler/Epic/Injection.hs

src/full/Agda/Compiler/Epic/Interface.hs

src/full/Agda/Compiler/Epic/Smashing.hs

src/full/Agda/Compiler/Epic/Static.hs

src/full/Agda/Compiler/JS

src/full/Agda/Compiler/JS/Case.hs

src/full/Agda/Compiler/JS/Compiler.hs

src/full/Agda/Compiler/JS/Parser.hs

src/full/Agda/Compiler/JS/Pretty.hs

src/full/Agda/Compiler/JS/Substitution.hs

src/full/Agda/Compiler/JS/Syntax.hs

src/full/Agda/Interaction/EmacsCommand.hs

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

src/full/Agda/TypeChecking/CompiledClause/Compile.hs

src/full/Agda/TypeChecking/CompiledClause/Compile.hs-boot

src/full/Agda/TypeChecking/Eliminators.hs

src/full/Agda/TypeChecking/Irrelevance.hs

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

src/full/Agda/TypeChecking/LevelConstraints.hs

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

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

src/full/Agda/Utils/VarSet.hs

files removed:
.pc

.pc/.version

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src/full

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src/full/Agda

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src/full/Agda/Syntax

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src/full/Agda/Syntax/Parser

.pc/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch/src/full/Agda/Syntax/Parser/Lexer.x

.pc/0002-Compatibility-with-src-exts-1.11.patch

.pc/0002-Compatibility-with-src-exts-1.11.patch/Agda.cabal

.pc/0003-Compatibility-with-syb-0.4.patch

.pc/0003-Compatibility-with-syb-0.4.patch/Agda.cabal

.pc/0003-Compatibility-with-syb-0.4.patch/src

.pc/0003-Compatibility-with-syb-0.4.patch/src/full

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda/Interaction

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda/Interaction/Highlighting

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda/Interaction/Highlighting/Generate.hs

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda/Utils

.pc/0003-Compatibility-with-syb-0.4.patch/src/full/Agda/Utils/Generics.hs

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/Agda.cabal

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src/full

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src/full/Agda

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src/full/Agda/Syntax

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src/full/Agda/Syntax/Parser

.pc/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch/src/full/Agda/Syntax/Parser/Alex.hs

.pc/applied-patches

debian/patches

debian/patches/0001-Compatibility-with-Alex-2.3.5-and-GHC-7.0.3.patch

debian/patches/0002-Compatibility-with-src-exts-1.11.patch

debian/patches/0003-Compatibility-with-syb-0.4.patch

debian/patches/0004-Add-an-alexGetByte-function-for-alex-3.0-compatibili.patch

debian/patches/series

src/full/Agda/Compiler/Epic/ConstructorIrrelevancy.hs

src/full/Agda/Compiler/Epic/LambdaLift.hs

files modified:
Agda.cabal

README

debian/changelog

debian/control

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

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

src/data/EpicInclude/AgdaPrelude.e

src/data/EpicInclude/stdagda.c

src/data/EpicInclude/stdagda.h

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

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

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

src/data/emacs-mode/annotation.el

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/CaseSplit.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Compiler/Epic/AuxAST.hs

src/full/Agda/Compiler/Epic/CompileState.hs

src/full/Agda/Compiler/Epic/Compiler.hs

src/full/Agda/Compiler/Epic/Epic.hs

src/full/Agda/Compiler/Epic/Erasure.hs

src/full/Agda/Compiler/Epic/Forcing.hs

src/full/Agda/Compiler/Epic/FromAgda.hs

src/full/Agda/Compiler/Epic/NatDetection.hs

src/full/Agda/Compiler/Epic/Primitive.hs

src/full/Agda/Compiler/HaskellTypes.hs

src/full/Agda/Compiler/MAlonzo/Compiler.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/GhciTop.hs

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

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

src/full/Agda/Interaction/Imports.hs

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

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/Abstract/Pretty.hs

src/full/Agda/Syntax/Abstract/Views.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/Operators.hs

src/full/Agda/Syntax/Concrete/Operators/Parser.hs

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

src/full/Agda/Syntax/Fixity.hs

src/full/Agda/Syntax/Internal.hs

src/full/Agda/Syntax/Internal/Generic.hs

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Notation.hs

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

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

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

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

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

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

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Scope/Base.hs

src/full/Agda/Syntax/Scope/Monad.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/SparseMatrix.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/CompiledClause.hs

src/full/Agda/TypeChecking/CompiledClause/Match.hs

src/full/Agda/TypeChecking/CompiledClause/Match.hs-boot

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

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

src/full/Agda/TypeChecking/Coverage.hs

src/full/Agda/TypeChecking/Coverage/Match.hs

src/full/Agda/TypeChecking/Datatypes.hs

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

src/full/Agda/TypeChecking/DisplayForm.hs

src/full/Agda/TypeChecking/Empty.hs

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

src/full/Agda/TypeChecking/Errors.hs

src/full/Agda/TypeChecking/EtaContract.hs

src/full/Agda/TypeChecking/Forcing.hs

src/full/Agda/TypeChecking/Free.hs

src/full/Agda/TypeChecking/Implicit.hs

src/full/Agda/TypeChecking/Injectivity.hs

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/MetaVars.hs

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

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

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

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

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

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

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

src/full/Agda/TypeChecking/Monad/Context.hs-boot

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

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

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

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

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

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

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

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

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/Monad/Statistics.hs

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

src/full/Agda/TypeChecking/Patterns/Match.hs

src/full/Agda/TypeChecking/Patterns/Match.hs-boot

src/full/Agda/TypeChecking/Polarity.hs

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

src/full/Agda/TypeChecking/Positivity.hs

src/full/Agda/TypeChecking/Pretty.hs

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/Quote.hs

src/full/Agda/TypeChecking/Rebind.hs

src/full/Agda/TypeChecking/RecordPatterns.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/Builtin/Coinduction.hs

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

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

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

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

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

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

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

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

src/full/Agda/TypeChecking/Rules/LHS/Problem.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/Rules/Term.hs-boot

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/Tests.hs

src/full/Agda/TypeChecking/UniversePolymorphism.hs

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

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Graph.hs

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

src/full/Agda/Utils/List.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/Size.hs

src/full/Agda/Utils/String.hs

Show diffs side-by-side

added added

removed removed

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

7

7

import qualified Agda.Syntax.Concrete.Name as C

8

8

import Agda.TypeChecking.Monad

9

9

10

isRecord :: MonadTCM tcm => QName -> tcm Bool

11

isEtaRecord :: MonadTCM tcm => QName -> tcm Bool

12

getRecordFieldNames :: MonadTCM tcm => QName -> tcm [Arg C.Name]

13

etaContractRecord :: MonadTCM tcm => QName -> QName -> Args -> tcm Term

14

isGeneratedRecordConstructor :: MonadTCM tcm => QName -> tcm Bool

10

isRecord :: QName -> TCM Bool

11

isEtaRecord :: QName -> TCM Bool

12

getRecordFieldNames :: QName -> TCM [Arg C.Name]

13

etaContractRecord :: QName -> QName -> Args -> TCM Term

14

isGeneratedRecordConstructor :: QName -> TCM Bool

Older »