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

« back to all changes in this revision

Viewing changes to src/full/Agda/Syntax/Strict.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/Syntax/Strict.hs

{-# LANGUAGE CPP #-}

module Agda.Syntax.Strict where

import Data.Generics

import Agda.Syntax.Common

import Agda.Syntax.Internal

import Agda.Syntax.Parser.Tokens

import qualified Agda.Syntax.Concrete as C

import qualified Agda.Syntax.Concrete.Definitions as C

#include "../undefined.h"

import Agda.Utils.Impossible

class Strict a where

force :: a -> Int

instance Strict Term where

force t = case t of

Var _ ts -> force ts

Def _ ts -> force ts

Con _ ts -> force ts

Lam _ t -> force t

Lit _ -> 0

Pi a b -> force (a,b)

Fun a b -> force (a,b)

Sort s -> force s

MetaV _ ts -> force ts

instance Strict Type where

force (El s t) = force (s,t)

instance Strict Sort where

force s = case s of

Type n -> fromIntegral n

Prop -> 0

Lub s1 s2 -> force (s1,s2)

Suc s -> force s

MetaS _ -> 0

instance Strict ClauseBody where

force (Body t) = force t

force (Bind b) = force b

force (NoBind b) = force b

force NoBody = 0

instance Strict C.Expr where

force e = everything (+) (const 1) e

instance Strict C.Declaration where

force e = everything (+) (const 1) e

instance Strict C.Pragma where

force e = everything (+) (const 1) e

instance Strict C.NiceDeclaration where

force d = everything (+) (const 1) d

instance (Strict a, Strict b) => Strict (a,b) where

force (x,y) = force x + force y

instance Strict a => Strict (Arg a) where

force = force . unArg

instance Strict a => Strict [a] where

force = sum . map force

instance Strict a => Strict (Abs a) where

force = force . absBody

instance Strict Token where

-- TODO: This is just a dummy instance. Why can't we just use the

-- NFData derivation provided by Drift?

force = (`seq` 0)

infixr 0 $!!

($!!) :: Strict a => (a -> b) -> a -> b

f $!! x = force x `seq` f x

strict :: Strict a => a -> a

strict x = id $!! x

Older »