← 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/Compiler/Epic/Primitive.hs

Committer: Package Import Robot
Author(s): Iain Lane, Kiwamu Okabe, Iain Lane
Date: 2013-04-10 11:46:43 UTC
mfrom: (4.1.5 experimental)
Revision ID: package-import@ubuntu.com-20130410114643-prunhsz59f0fhrdn

Tags: 2.3.2-1

[ Kiwamu Okabe ]
* New patch: Extend haskell-src-exts dependency and fix type miss.

[ Iain Lane ]
* [dfbca48] Imported Upstream version 2.3.2
* [7746bcc] Remove all patches — all upstream.
* [2cdb691] Update build-deps to match control file
* [868ebf4] agda-mode no longer depends on haskell-mode or GHCi.
Remove dependency and update .el file accordingly
* [9e0ba22] Add agda-bin package here, as the separate package has been
removed
* [75a240f] agda-mode needs to depend on agda-bin
* [d290f95] Allow Quickcheck up to 2.7. Fix haskeline build-dep.
* [79190e6] Add missing geniplate and parallel BDs

files added:
.pc/allow-quickcheck-2.7

.pc/allow-quickcheck-2.7/Agda.cabal

debian/agda-bin.install

debian/patches/allow-quickcheck-2.7

doc/release-notes/2-3-2.txt

src/data/agda.sty

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

src/full/Agda/Compiler/CallCompiler.hs

src/full/Agda/Interaction/GhcTop.hs

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

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

src/full/Agda/Interaction/InteractionTop.hs

src/full/Agda/Interaction/Response.hs

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

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

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

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

src/full/Agda/TypeChecking/DropArgs.hs

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

src/full/Agda/TypeChecking/InstanceArguments.hs

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

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

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

src/full/Agda/TypeChecking/ProjectionLike.hs

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

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

src/full/Agda/Utils/Geniplate.hs

src/full/Agda/Utils/HashMap.hs

src/full/Agda/Utils/Pointed.hs

src/full/Agda/Utils/Time.hs

src/main

src/main/Main.hs

files removed:
.pc/extend-mtl-dependenc

.pc/extend-mtl-dependenc/Agda.cabal

debian/patches/extend-mtl-dependenc

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Syntax/Strict.hs

src/full/Agda/Utils/Generics.hs

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

files modified:
.pc/applied-patches

Agda.cabal

LICENSE

README

debian/50agda.el

debian/changelog

debian/control

debian/patches/series

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/EpicInclude/AgdaPrelude.e

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/Convert.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/ForceConstrs.hs

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

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

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

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

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

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

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

src/full/Agda/Compiler/HaskellTypes.hs

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

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

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

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

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

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

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/FindFile.hs

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

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

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

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

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

src/full/Agda/Interaction/Imports.hs

src/full/Agda/Interaction/MakeCase.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/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/Info.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.hs

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

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/Translation/AbstractToConcrete.hs

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

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

src/full/Agda/Termination/CallGraph.hs

src/full/Agda/Termination/Lexicographic.hs

src/full/Agda/Termination/Matrix.hs

src/full/Agda/Termination/SparseMatrix.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/CompiledClause.hs

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

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

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

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

src/full/Agda/TypeChecking/Coverage.hs

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

src/full/Agda/TypeChecking/Datatypes.hs

src/full/Agda/TypeChecking/DisplayForm.hs

src/full/Agda/TypeChecking/Eliminators.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/Irrelevance.hs

src/full/Agda/TypeChecking/Level.hs

src/full/Agda/TypeChecking/LevelConstraints.hs

src/full/Agda/TypeChecking/MetaVars.hs

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

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

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

src/full/Agda/TypeChecking/Monad.hs

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

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

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

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

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

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

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

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/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/Builtin/Coinduction.hs-boot

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

src/full/Agda/Utils/Either.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/Map.hs

src/full/Agda/Utils/Maybe.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/VarSet.hs

src/full/Agda/Utils/Warshall.hs

Show diffs side-by-side

added added

removed removed

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

15

15

import qualified Agda.Syntax.Internal as T

16

16

import Agda.TypeChecking.Monad hiding (defName)

17

17

import Agda.TypeChecking.Monad.Builtin

18

import Agda.Utils.Monad (andM)

18

19

19

20

import Agda.Compiler.Epic.AuxAST

20

21

import Agda.Compiler.Epic.CompileState

92

93

if all isJust builtins

93

94

then do

94

95

let names = map (defName . fromMaybe __IMPOSSIBLE__) builtins

95

b <- and <$> mapM constrInScope names

96

b <- andM $ map constrInScope names

96

97

if b then return $ Just (transf names) else return Nothing

97

98

else return Nothing

98

99

Older »