~ubuntu-branches/ubuntu/wily/agda/wily-proposed

« back to all changes in this revision

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

Committer: Package Import Robot
Author(s): Iain Lane, d5cf60f
Date: 2015-05-20 13:08:33 UTC
mfrom: (1.1.7)
Revision ID: package-import@ubuntu.com-20150520130833-cdcmhagwsouna237

Tags: 2.4.2.2-2

[d5cf60f] Depend on ${shlibs:Depends}, to get libc (& maybe other) deps

files added:
README.md

src/data/postprocess-latex.pl

src/full/Agda/TypeChecking/Rewriting.hs

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

src/full/Agda/TypeChecking/Unquote.hs

src/full/Agda/Utils/AssocList.hs

src/full/Agda/Utils/Bag.hs

src/full/Agda/Utils/Empty.hs

src/full/Agda/Utils/Except.hs

src/full/Agda/Utils/IORef.hs

src/full/Agda/Utils/Lens

src/full/Agda/Utils/Lens.hs

src/full/Agda/Utils/Lens/Examples.hs

src/full/Agda/Utils/Permutation

src/full/Agda/Utils/Permutation/Tests.hs

src/full/undefined.h

files removed:
README

src/full/Agda/Utils/Fresh.hs

src/full/Agda/Utils/Unicode.hs

src/full/Agda/undefined.h

files modified:
Agda.cabal

CHANGELOG

debian/changelog

debian/control

debian/rules

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

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

src/data/agda.sty

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

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

src/full/Agda/Auto/Auto.hs

src/full/Agda/Auto/CaseSplit.hs

src/full/Agda/Auto/Convert.hs

src/full/Agda/Auto/NarrowingSearch.hs

src/full/Agda/Auto/SearchControl.hs

src/full/Agda/Auto/Syntax.hs

src/full/Agda/Auto/Typecheck.hs

src/full/Agda/Compiler/CallCompiler.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/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/Interface.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/Case.hs

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

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

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

src/full/Agda/ImpossibleTest.hs

src/full/Agda/Interaction/BasicOps.hs

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

src/full/Agda/Interaction/EmacsCommand.hs

src/full/Agda/Interaction/EmacsTop.hs

src/full/Agda/Interaction/Exceptions.hs

src/full/Agda/Interaction/FindFile.hs

src/full/Agda/Interaction/Highlighting/Dot.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/LaTeX.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/InteractionTop.hs

src/full/Agda/Interaction/MakeCase.hs

src/full/Agda/Interaction/Monad.hs

src/full/Agda/Interaction/Options.hs

src/full/Agda/Interaction/Options/Lenses.hs

src/full/Agda/Interaction/Response.hs

src/full/Agda/Main.hs

src/full/Agda/Syntax/Abstract.hs

src/full/Agda/Syntax/Abstract/Copatterns.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/Generic.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/Defs.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/Notation.hs

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

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

src/full/Agda/Termination/Inlining.hs

src/full/Agda/Termination/Monad.hs

src/full/Agda/Termination/Order.hs

src/full/Agda/Termination/RecCheck.hs

src/full/Agda/Termination/Semiring.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/TheTypeChecker.hs

src/full/Agda/TypeChecking/Abstract.hs

src/full/Agda/TypeChecking/CheckInternal.hs

src/full/Agda/TypeChecking/CompiledClause.hs

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

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/Coverage/SplitTree.hs

src/full/Agda/TypeChecking/Datatypes.hs

src/full/Agda/TypeChecking/DisplayForm.hs

src/full/Agda/TypeChecking/DropArgs.hs

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/InstanceArguments.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/Base.hs

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

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

src/full/Agda/TypeChecking/Monad/Benchmark.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/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/Sharing.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/Abstract.hs

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

src/full/Agda/TypeChecking/Polarity.hs

src/full/Agda/TypeChecking/Positivity.hs

src/full/Agda/TypeChecking/Pretty.hs

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

src/full/Agda/TypeChecking/Primitive.hs

src/full/Agda/TypeChecking/ProjectionLike.hs

src/full/Agda/TypeChecking/Quote.hs

src/full/Agda/TypeChecking/RecordPatterns.hs

src/full/Agda/TypeChecking/Records.hs

src/full/Agda/TypeChecking/Reduce.hs

src/full/Agda/TypeChecking/Reduce/Monad.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/ProblemRest.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/SizedTypes/Solve.hs

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

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

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

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

src/full/Agda/TypeChecking/Substitute.hs

src/full/Agda/TypeChecking/SyntacticEquality.hs

src/full/Agda/TypeChecking/Telescope.hs

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

src/full/Agda/TypeChecking/Tests.hs

src/full/Agda/TypeChecking/With.hs

src/full/Agda/Utils/BiMap.hs

src/full/Agda/Utils/Char.hs

src/full/Agda/Utils/Cluster.hs

src/full/Agda/Utils/Either.hs

src/full/Agda/Utils/Favorites.hs

src/full/Agda/Utils/FileName.hs

src/full/Agda/Utils/Function.hs

src/full/Agda/Utils/Functor.hs

src/full/Agda/Utils/Geniplate.hs

src/full/Agda/Utils/Graph/AdjacencyMap.hs

src/full/Agda/Utils/Graph/AdjacencyMap/Unidirectional.hs

src/full/Agda/Utils/HashMap.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/Maybe/Strict.hs

src/full/Agda/Utils/Monad.hs

src/full/Agda/Utils/Null.hs

src/full/Agda/Utils/PartialOrd.hs

src/full/Agda/Utils/Permutation.hs

src/full/Agda/Utils/Pointer.hs

src/full/Agda/Utils/Pretty.hs

src/full/Agda/Utils/ReadP.hs

src/full/Agda/Utils/SemiRing.hs

src/full/Agda/Utils/Size.hs

src/full/Agda/Utils/String.hs

src/full/Agda/Utils/Suffix.hs

src/full/Agda/Utils/Time.hs

src/full/Agda/Utils/Trie.hs

src/full/Agda/Utils/Tuple.hs

src/full/Agda/Utils/Update.hs

src/full/Agda/Utils/VarSet.hs

src/full/Agda/Utils/Warshall.hs

src/full/Agda/Version.hs

Show diffs side-by-side

added added

removed removed

src/full/Agda/TypeChecking/SizedTypes.hs

{-# LANGUAGE CPP #-}

{-# LANGUAGE PatternGuards #-}

module Agda.TypeChecking.SizedTypes where

import Control.Monad.Error

import Data.Function

import Data.List

import qualified Data.Map as Map

import {-# SOURCE #-} Agda.TypeChecking.Conversion

import {-# SOURCE #-} Agda.TypeChecking.Constraints

import qualified Agda.Utils.Warshall as W

import Agda.Utils.Except ( MonadError(catchError, throwError) )

import Agda.Utils.List

import Agda.Utils.Maybe

import Agda.Utils.Monad

import Agda.Utils.Size

import Agda.Utils.Tuple

#include "../undefined.h"

import qualified Agda.Utils.Warshall as W

#include "undefined.h"

import Agda.Utils.Impossible

------------------------------------------------------------------------

358

(b, m) <- sizeExpr v

359

return $ Just $ Leq a (m - n) b

360

`catchError` \ err -> case err of

361

PatternErr _ -> return Nothing

361

PatternErr{} -> return Nothing

362

_ -> throwError err

363

_ -> __IMPOSSIBLE__

364

506

term (W.SizeVar j n) | j < ar = plus (var $ ar - j - 1) n

507

term _ = __IMPOSSIBLE__

508

509

lam _ v = Lam defaultArgInfo $ Abs "s" v -- hiding does not matter

510

511

-- convert size expression to term and abstract

512

v = flip (foldr lam) [0..ar-1] $ term e

509

tel = replicate ar $ defaultArg "s"

510

-- convert size expression to term

511

v = term e

513

512

514

513

reportSDoc "tc.size.solve" 20 $ sep

515

514

[ text (show m) <+> text ":="

520

519

let isInf (W.SizeConst W.Infinite) = True

521

520

isInf _ = False

522

521

unlessM ((isJust <$> isInteractionMeta m) `and2M` return (isInf e)) $

523

assignTerm m v

522

assignTerm m tel v

524

523

525

524

mapM_ inst $ Map.toList sol

526

525

return True

Older »