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

« back to all changes in this revision

Viewing changes to src/full/Agda/TypeChecking/Empty.hs

Committer: Bazaar Package Importer
Author(s): Iain Lane
Date: 2009-07-20 19:49:41 UTC
Revision ID: james.westby@ubuntu.com-20090720194941-hcjy91vrn16csh7d

Tags: upstream-2.2.4+dfsg

Import upstream version 2.2.4+dfsg

files added:

Agda.cabal

LICENSE

README

Setup.hs

dist

dist/build

dist/build/Agda

dist/build/Agda/Syntax

dist/build/Agda/Syntax/Parser

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

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

doc/release-notes

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

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

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

src/agda-mode

src/agda-mode/Main.hs

src/data

src/data/Agda.css

src/data/emacs-mode

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/agda2.el

src/data/emacs-mode/annotation.el

src/data/emacs-mode/eri.el

src/full

src/full/Agda

src/full/Agda/Compiler

src/full/Agda/Compiler/Agate

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

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

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

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

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

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

src/full/Agda/Compiler/Alonzo

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

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

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

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

src/full/Agda/Compiler/HaskellTypes.hs

src/full/Agda/Compiler/MAlonzo

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

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

src/full/Agda/Interaction

src/full/Agda/Interaction/BasicOps.hs

src/full/Agda/Interaction/CommandLine

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

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/GhciTop.hs

src/full/Agda/Interaction/Highlighting

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

src/full/Agda/Interaction/Highlighting/Vim.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

src/full/Agda/Syntax/Abstract

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

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

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

src/full/Agda/Syntax/Internal.hs

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

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

src/full/Agda/Syntax/Literal.hs

src/full/Agda/Syntax/Parser

src/full/Agda/Syntax/Parser.hs

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

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

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

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

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

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

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

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

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

src/full/Agda/Syntax/Position.hs

src/full/Agda/Syntax/Scope

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

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

src/full/Agda/Termination/CallGraph.hs

src/full/Agda/Termination/Lexicographic.hs

src/full/Agda/Termination/Matrix.hs

src/full/Agda/Termination/Semiring.hs

src/full/Agda/Termination/TermCheck.hs

src/full/Agda/Termination/Termination.hs

src/full/Agda/Tests.hs

src/full/Agda/TypeChecker.hs

src/full/Agda/TypeChecking

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/Constraints.hs

src/full/Agda/TypeChecking/Conversion.hs

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

src/full/Agda/TypeChecking/Coverage

src/full/Agda/TypeChecking/Coverage.hs

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

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

src/full/Agda/TypeChecking/Implicit.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

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

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

src/full/Agda/TypeChecking/Patterns

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/Rebind.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

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

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

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

src/full/Agda/TypeChecking/Rules/LHS

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

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

src/full/Agda/TypeChecking/Tests.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils

src/full/Agda/Utils/Char.hs

src/full/Agda/Utils/Either.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Fresh.hs

src/full/Agda/Utils/Function.hs

src/full/Agda/Utils/Generics.hs

src/full/Agda/Utils/Graph.hs

src/full/Agda/Utils/Hash.hs

src/full/Agda/Utils/IO.hs

src/full/Agda/Utils/Impossible.hs

src/full/Agda/Utils/List.hs

src/full/Agda/Utils/Map.hs

src/full/Agda/Utils/Maybe.hs

src/full/Agda/Utils/Monad

src/full/Agda/Utils/Monad.hs

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

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/Pretty.hs

src/full/Agda/Utils/QuickCheck.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/SemiRing.hs

src/full/Agda/Utils/Serialise.hs

src/full/Agda/Utils/Size.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/TestHelpers.hs

src/full/Agda/Utils/Trace.hs

src/full/Agda/Utils/Trie.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/Unicode.hs

src/full/Agda/Utils/Warshall.hs

src/full/Agda/Version.hs

src/full/Agda/undefined.h

Show diffs side-by-side

added added

removed removed

src/full/Agda/TypeChecking/Empty.hs

module Agda.TypeChecking.Empty where

import Control.Applicative

import Agda.Syntax.Common

import Agda.Syntax.Internal

import Agda.TypeChecking.Monad

import Agda.TypeChecking.Coverage

import Agda.TypeChecking.Constraints

import Agda.TypeChecking.Reduce

import Agda.Utils.Permutation

import Agda.Utils.Size

-- | Make sure that a type is empty.

isEmptyType :: MonadTCM tcm => Type -> tcm ()

isEmptyType t = noConstraints $ isEmptyTypeC t

isEmptyTypeC :: MonadTCM tcm => Type -> tcm Constraints

isEmptyTypeC t = do

tb <- reduceB t

let t = ignoreBlocking tb

case unEl <$> tb of

NotBlocked MetaV{} -> buildConstraint (IsEmpty t)

Blocked{} -> buildConstraint (IsEmpty t)

_ -> do

tel0 <- getContextTelescope

let tel = telFromList $ telToList tel0 ++ [Arg NotHidden ("_", t)]

ps = [ Arg h $ VarP x | Arg h (x, _) <- telToList tel ]

r <- split tel (idP $ size tel) ps 0

case r of

Left err -> typeError $ ShouldBeEmpty t []

Right [] -> return []

Right cs -> typeError $ ShouldBeEmpty t $ map (unArg . last . scPats) cs

Older »