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

« back to all changes in this revision

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

-- | Termination checker, based on

-- \"A Predicative Analysis of Structural Recursion\" by

-- Andreas Abel and Thorsten Altenkirch (JFP'01).

-- and

-- \"The Size-Change Principle for Program Termination\" by

-- Chin Soon Lee, Neil Jones, and Amir Ben-Amram (POPL'01).

-- TODO: Note that we should also check that data type definitions are

-- strictly positive. Furthermore, for inductive-recursive families we

-- may need to do something more clever.

module Agda.Termination.Termination

( terminates

, Agda.Termination.Termination.tests

) where

import Agda.Termination.Lexicographic

import Agda.Termination.CallGraph

import Agda.Termination.Matrix

import Agda.Utils.Either

import Agda.Utils.TestHelpers

import Control.Arrow

import Agda.Utils.QuickCheck

import qualified Data.Set as Set

import qualified Data.Array as Array

import Data.Set (Set)

import qualified Data.Set as Set

import Data.Map (Map)

import qualified Data.Map as Map

import Data.Monoid

import Data.Array (Array)

-- | TODO: This comment seems to be partly out of date.

-- @'terminates' cs@ checks if the functions represented by @cs@

-- terminate. The call graph @cs@ should have one entry ('Call') per

-- recursive function application.

-- @'Right' perms@ is returned if the functions are size-change terminating.

-- If termination can not be established, then @'Left' problems@ is

-- returned instead. Here @problems@ contains an

-- indication of why termination cannot be established. See 'lexOrder'

-- for further details.

-- Note that this function assumes that all data types are strictly

-- positive.

-- The termination criterion is taken from Jones et al.

-- In the completed call graph, each idempotent call-matrix

-- from a function to itself must have a decreasing argument.

-- Idempotency is wrt. matrix multiplication.

-- This criterion is strictly more liberal than searching for a

-- lexicographic order (and easier to implement, but harder to justify).

terminates :: (Ord meta, Monoid meta) => CallGraph meta -> Either meta ()

terminates cs = let ccs = complete cs

checkIdems $ toList ccs

checkIdems :: (Ord meta,Monoid meta) => [(Call,meta)] -> Either meta ()

checkIdems [] = Right ()

checkIdems ((c,m):xs) = if (checkIdem c) then checkIdems xs else Left m

{- Convention (see TermCheck):

Guardedness flag is in position (0,0) of the matrix,

it is always present even if the functions are all recursive.

The examples below do not include the guardedness flag, though.

checkIdem :: Call -> Bool

checkIdem c = let

b = target c == source c

idem = (c >*< c) == c

diag = Array.elems $ diagonal (mat (cm c))

hasDecr = any isDecr $ diag

(not b) || (not idem) || hasDecr

-- | Matrix is decreasing if any diagonal element is 'Lt'.

isDecr :: Order -> Bool

isDecr Lt = True

isDecr (Mat m) = any isDecr $ Array.elems $ diagonal m

isDecr _ = False

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

-- Some examples

-- | The call graph instantiation used by the examples below.

type CG = CallGraph (Set Integer)

-- | Constructs a call graph suitable for use with the 'R' monoid.

buildCallGraph :: [Call] -> CG

buildCallGraph = fromList . flip zip (map Set.singleton [1 ..])

100

-- | The example from the JFP'02 paper.

101

102

example1 :: CG

103

example1 = buildCallGraph [c1, c2, c3]

104

where

105

flat = 1

106

aux = 2

107

c1 = Call { source = flat, target = aux

108

, cm = CallMatrix $ fromLists (Size 2 1) [[Lt], [Lt]]

109

}

110

c2 = Call { source = aux, target = aux

111

, cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown]

112

, [Unknown, Le]]

113

}

114

c3 = Call { source = aux, target = flat

115

, cm = CallMatrix $ fromLists (Size 1 2) [[Unknown, Le]]

116

}

117

118

prop_terminates_example1 = isRight $ terminates example1

119

120

-- | An example which is now handled by this algorithm: argument

121

-- swapping addition.

122

123

-- @S x + y = S (y + x)@

124

125

-- @Z + y = y@

126

127

example2 :: CG

128

example2 = buildCallGraph [c]

129

where

130

plus = 1

131

c = Call { source = plus, target = plus

132

, cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Le]

133

, [Lt, Unknown] ]

134

}

135

136

prop_terminates_example2 = isRight $ terminates example2

137

138

-- | A related example which is anyway handled: argument swapping addition

139

-- using two alternating functions.

140

141

-- @S x + y = S (y +' x)@

142

143

-- @Z + y = y@

144

145

-- @S x +' y = S (y + x)@

146

147

-- @Z +' y = y@

148

149

example3 :: CG

150

example3 = buildCallGraph [c plus plus', c plus' plus]

151

where

152

plus = 1

153

plus' = 2

154

c f g = Call { source = f, target = g

155

, cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Le]

156

, [Lt, Unknown] ]

157

}

158

159

prop_terminates_example3 = isRight $ terminates example3

160

161

-- | A contrived example.

162

163

-- @f (S x) y = f (S x) y + g x y@

164

165

-- @f Z y = y@

166

167

-- @g x y = f x y@

168

169

-- TODO: This example checks that the meta information is reported properly

170

-- when an error is encountered.

171

172

example4 :: CG

173

example4 = buildCallGraph [c1, c2, c3]

174

where

175

f = 1

176

g = 2

177

c1 = Call { source = f, target = f

178

, cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown]

179

, [Unknown, Le] ]

180

}

181

c2 = Call { source = f, target = g

182

, cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown]

183

, [Unknown, Le] ]

184

}

185

c3 = Call { source = g, target = f

186

, cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown]

187

, [Unknown, Le] ]

188

}

189

190

prop_terminates_example4 = isLeft $ terminates example4

191

192

-- | This should terminate.

193

194

-- @f (S x) (S y) = g x (S y) + f (S (S x)) y@

195

196

-- @g (S x) (S y) = f (S x) (S y) + g x (S y)@

197

198

example5 :: CG

199

example5 = buildCallGraph [c1, c2, c3, c4]

200

where

201

f = 1

202

g = 2

203

c1 = Call { source = f, target = g

204

, cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown]

205

, [Unknown, Le] ]

206

}

207

c2 = Call { source = f, target = f

208

, cm = CallMatrix $ fromLists (Size 2 2) [ [Unknown, Unknown]

209

, [Unknown, Lt] ]

210

}

211

c3 = Call { source = g, target = f

212

, cm = CallMatrix $ fromLists (Size 2 2) [ [Le, Unknown]

213

, [Unknown, Le] ]

214

}

215

c4 = Call { source = g, target = g

216

, cm = CallMatrix $ fromLists (Size 2 2) [ [Lt, Unknown]

217

, [Unknown, Le] ]

218

}

219

220

prop_terminates_example5 = isRight $ terminates example5

221

222

-- | Another example which should fail.

223

224

-- @f (S x) = f x + f (S x)@

225

226

-- @f x = f x@

227

228

-- TODO: This example checks that the meta information is reported properly

229

-- when an error is encountered.

230

231

example6 :: CG

232

example6 = buildCallGraph [c1, c2, c3]

233

where

234

f = 1

235

c1 = Call { source = f, target = f

236

, cm = CallMatrix $ fromLists (Size 1 1) [ [Lt] ]

237

}

238

c2 = Call { source = f, target = f

239

, cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ]

240

}

241

c3 = Call { source = f, target = f

242

, cm = CallMatrix $ fromLists (Size 1 1) [ [Le] ]

243

}

244

245

prop_terminates_example6 = isLeft $ terminates example6

246

247

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

248

-- All tests

249

250

tests :: IO Bool

251

tests = runTests "Agda.Termination.Termination"

252

[ quickCheck' prop_terminates_example1

253

, quickCheck' prop_terminates_example2

254

, quickCheck' prop_terminates_example3

255

, quickCheck' prop_terminates_example4

256

, quickCheck' prop_terminates_example5

257

, quickCheck' prop_terminates_example6

258

]

Older »