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

« back to all changes in this revision

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

{-# LANGUAGE DeriveDataTypeable #-}

module Agda.Utils.Trace where

import Control.Monad

import Data.Monoid

import Data.Generics (Typeable, Data)

type Trace = CurrentCall

type SiblingCall = ChildCall

data CurrentCall a

= Current a (ParentCall a) [SiblingCall a] [ChildCall a]

| TopLevel [ChildCall a]

deriving (Typeable, Data)

data ParentCall a

= Parent a (ParentCall a) [SiblingCall a]

| NoParent

deriving (Typeable, Data)

data ChildCall a = Child a [ChildCall a]

deriving (Typeable, Data)

newCall :: a -> Trace a -> Trace a

newCall c (TopLevel cs) = Current c NoParent cs []

newCall c (Current c' p ss cs) = Current c (Parent c' p ss) cs []

updateCall :: a -> Trace a -> Trace a

updateCall c (TopLevel _) = error $ "updateCall: no a in progress"

updateCall c (Current _ p ss cs) = case p of

NoParent -> TopLevel $ Child c cs : ss

Parent c' p' ss' -> Current c' p' ss' $ Child c cs : ss

matchCall :: (call -> Maybe a) -> Trace call -> Maybe a

matchCall f tr = case matchTrace f' tr of

[] -> Nothing

x : _ -> Just x

where

f' (Child c _) = maybe [] (:[]) $ f c

matchCalls :: (call -> Maybe a) -> Trace call -> [a]

matchCalls f = matchTrace f'

where

f' (Child c _) = maybe [] (:[]) $ f c

matchTrace :: Monoid m => (ChildCall call -> m) -> Trace call -> m

matchTrace f (TopLevel _) = mempty

matchTrace f t@(Current c _ _ cs) =

f (Child c cs) `mappend` matchTrace f (updateCall c t)

Older »