Testable.icl 16.6 KB
Newer Older
1
implementation module Gast.Testable
Bas Lijnse's avatar
Bas Lijnse committed
2 3 4 5

/*
	GAST: A Generic Automatic Software Test-system
	
6
	testable: the test algorithm for logical properties
Bas Lijnse's avatar
Bas Lijnse committed
7

8
	Pieter Koopman, 2002-2010
Bas Lijnse's avatar
Bas Lijnse committed
9 10 11 12 13
	Radboud Universty, Nijmegen
	The Netherlands
	pieter@cs.ru.nl
*/

Camil Staps's avatar
Camil Staps committed
14 15
import StdEnv

16
from Data.Func import $
Camil Staps's avatar
Camil Staps committed
17
import Data.Functor
18
from Data.List import instance Functor [], concatMap
19
import qualified Data.Map
Camil Staps's avatar
Camil Staps committed
20
import Data.Maybe
Camil Staps's avatar
Camil Staps committed
21 22 23
import Math.Random
import Testing.TestEvents
import Text
Camil Staps's avatar
Camil Staps committed
24
import Text.GenJSON
25
import Text.GenPrint
Camil Staps's avatar
Camil Staps committed
26 27 28 29 30
import Text.Language

import Gast.Gen
import Gast.GenLibTest
import Gast.ThunkNames
Bas Lijnse's avatar
Bas Lijnse committed
31 32 33 34 35

derive gLess Result
instance == Result where (==) x y = x===y

newAdmin :: Admin
36
newAdmin = { res=Undef, labels=[], args=[], argsRepresentation = [], failedAssertions = []
37
           , namePath = []
38
           , recFieldValueNrLimits = 'Data.Map'.newMap
39
           }
Bas Lijnse's avatar
Bas Lijnse committed
40

41
instance Testable Bool where
42 43
    evaluate b genState result=:{Admin| args, argsRepresentation} =
        [{result & args = reverse args, argsRepresentation = reverse argsRepresentation, res = if b OK CE}]
Camil Staps's avatar
Camil Staps committed
44
	testname b = "Bool"
Bas Lijnse's avatar
Bas Lijnse committed
45

46
instance Testable Result where
47 48
    evaluate r genState result=:{Admin| args, argsRepresentation} =
        [{result & args = reverse args, argsRepresentation = reverse argsRepresentation, res = r}]
Camil Staps's avatar
Camil Staps committed
49
	testname r = "Result"
Bas Lijnse's avatar
Bas Lijnse committed
50 51

instance Testable Property
Camil Staps's avatar
Camil Staps committed
52
where
Camil Staps's avatar
Camil Staps committed
53 54 55
	evaluate (Prop _ _ p) genState result = p genState result
	testname (Prop n _ _) = n
	testmodule (Prop _ m _) = m
Bas Lijnse's avatar
Bas Lijnse committed
56

57
instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a & TestArg a  
58
where
Camil Staps's avatar
Camil Staps committed
59 60 61 62
	evaluate f genState admin = forAll f (generateAll genState`) genState` admin
	where
		genState` = {GenState| genState & recFieldValueNrLimits = admin.Admin.recFieldValueNrLimits}
	testname f = thunk_name_to_string f
Camil Staps's avatar
Camil Staps committed
63
	testmodule f = Just (thunk_to_module_name_string f)
Bas Lijnse's avatar
Bas Lijnse committed
64 65 66

instance Testable [a] | Testable a  
where
67
	evaluate list genState admin = diagonal [ evaluate x genState admin \\ x<-list ] // copy the genState
Camil Staps's avatar
Camil Staps committed
68
	testname xs = "[" +++ join "," (map testname xs) +++ "]"
Camil Staps's avatar
Camil Staps committed
69 70 71
	testmodule xs = case removeDup [testmodule x \\ x <- xs] of
		[m] -> m
		_   -> Nothing
Bas Lijnse's avatar
Bas Lijnse committed
72 73

prop :: a -> Property | Testable a
Camil Staps's avatar
Camil Staps committed
74
prop p = Prop (testname p) (testmodule p) (evaluate p)
Bas Lijnse's avatar
Bas Lijnse committed
75

76
forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
77
forAll f []   genState r=:{Admin| args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values
78
forAll f list genState r = diagonal [apply f a genState r \\ a<-list ] // copy the genState
Bas Lijnse's avatar
Bas Lijnse committed
79

80
apply :: !(a->b) a GenState !Admin -> [Admin] | Testable b & TestArg a
81
apply f a genState r =
82
    evaluate (f a) genState {Admin| r & args = [show1 a:r.Admin.args], argsRepresentation = [printToString a : r.Admin.argsRepresentation]}
Bas Lijnse's avatar
Bas Lijnse committed
83

84
diagonal :: ![[a]] -> [a]
Bas Lijnse's avatar
Bas Lijnse committed
85 86 87 88 89 90 91 92 93 94 95
diagonal list = f 1 2 list []
where
	f n m [] [] = []
	f 0 m xs ys = f m (m+1) (rev ys xs) []
	f n m [] ys = f m (m+1) (rev ys []) []
	f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
	f n m [[]:xs] ys = f (n-1) m xs ys
	
	rev []    accu = accu
	rev [x:r] accu = rev r [x:accu]

96 97
generateAll :: !GenState -> [a] | ggen{|*|} a // & genType{|*|} a
generateAll genState = l where l = ggen{|*|} genState // {genState & currType = hd (genType{|*|} [] [] l) }
Bas Lijnse's avatar
Bas Lijnse committed
98 99 100 101 102 103

derive gEq Result
derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)

//--- testing ---//

104 105 106 107 108 109
:: Config =
	{ maxTests :: Int
	, maxArgs  :: Int
	, fails    :: Int
	, randoms  :: [Int]
	, genState :: GenState
Bas Lijnse's avatar
Bas Lijnse committed
110 111
	}

112 113 114 115 116 117
printEvents :: PrintConfig [GastEvent] -> [String]
printEvents pc [ge:ges] = case s of
	"" -> printEvents pc ges
	s  -> [s:printEvents pc ges]
where
	s = case ge of
Camil Staps's avatar
Camil Staps committed
118 119 120 121
		GE_TestStarted m n               -> pc.beforeStartOutput m n
		GE_TestFinished m n r ces labels -> pc.resultOutput m n r ces labels
		GE_CounterExample ce             -> pc.counterExampleOutput ce
		GE_Tick n adm                    -> pc.everyOutput n adm
122 123
printEvents _ [] = []

124 125 126 127
defaultTestConfig =
	{ maxTests = 1000
	, maxArgs  = 2000
	, fails    = 1
128 129 130
	, randoms  = aStream
	, genState = genState
	}
131

132 133
verbosePrintConfig =
	{ everyOutput          = verboseEvery
Camil Staps's avatar
Camil Staps committed
134
	, counterExampleOutput = humanReadableCEOutput True False
135 136 137 138
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
	}
verboseEvery n r = blank <+ n <+ ":" <+ join " " r.Admin.args
139

140 141
tracePrintConfig =
	{ everyOutput          = traceEvery
Camil Staps's avatar
Camil Staps committed
142
	, counterExampleOutput = humanReadableCEOutput False False
143 144
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
Bas Lijnse's avatar
Bas Lijnse committed
145
	}
146
traceEvery n r = n <+ ":" <+ join " " r.Admin.args <+ "\n"
Bas Lijnse's avatar
Bas Lijnse committed
147 148 149 150

blank :: String
blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81

Camil Staps's avatar
Camil Staps committed
151 152 153
countPrintConfig n =
	{ everyOutput          = countEvery n
	, counterExampleOutput = humanReadableCEOutput True True
154 155
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
156
	}
157 158 159 160 161 162 163
countEvery :: !Int !Int Admin -> String
countEvery steps n r
| n rem steps == 0 = toString n +++ "\r"
| otherwise        = ""

quietPrintConfig =
	{ everyOutput          = noEveryOutput
Camil Staps's avatar
Camil Staps committed
164
	, counterExampleOutput = noCounterExampleOutput
165
	, beforeStartOutput    = noBeforeOutput
Camil Staps's avatar
Camil Staps committed
166
	, resultOutput         = humanReadableResOutput False
Bas Lijnse's avatar
Bas Lijnse committed
167 168
	}

169 170 171 172 173 174
testEventsPrintConfig =
	{ everyOutput          = noEveryOutput
	, counterExampleOutput = noCounterExampleOutput
	, beforeStartOutput    = jsonEventStart
	, resultOutput         = jsonEventEnd
	}
175

176 177 178
noCounterExampleOutput :: CounterExampleRes -> String
noCounterExampleOutput _ = ""

Camil Staps's avatar
Camil Staps committed
179 180
noBeforeOutput :: !(Maybe String) !String -> String
noBeforeOutput _ _ = ""
181 182 183 184

noEveryOutput :: !Int Admin -> String
noEveryOutput n _ = ""

Camil Staps's avatar
Camil Staps committed
185 186 187 188 189
humanReadableCEOutput :: Bool Bool CounterExampleRes -> String
humanReadableCEOutput newLine showArgs {maxTests, nTests, nE, args, name, failedAssertions} = concat $
	if showArgs [(maxTests-nTests+1) <+ ":" <+ join " " args] [] ++
	if newLine ["\n"] [] ++
	[ showName True name
190 191 192 193
	, "Counterexample "
	, toString (nE+1)
	, " found after "
	, pluralisen English (maxTests-nTests+1) "test"
Camil Staps's avatar
Camil Staps committed
194
	, ": "
195
	, join " " args
Camil Staps's avatar
Camil Staps committed
196
	, "\n"
197 198
	: concatMap showFailedAssertion failedAssertions
	]
199
where
200
	showFailedAssertion :: !(!FailedAssertion, !String, !String) -> [String]
Camil Staps's avatar
Camil Staps committed
201
	showFailedAssertion (ExpectedRelation _ rel _, x, y) = ["not (", x, " ", toString rel, " ", y, ")\n"]
202

Camil Staps's avatar
Camil Staps committed
203 204
humanReadableResOutput :: Bool (Maybe String) String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite _ name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
205
where
206
	resStr = case resultType of
Camil Staps's avatar
Camil Staps committed
207
		Proof nTests -> "Proof: " +++ msgStr +++ conclude nTests 0 labels
208 209
		with
			msgStr = if (nRej == 0) "success for all arguments" "success for all non-rejected arguments"
Camil Staps's avatar
Camil Staps committed
210
		PassedTest maxArgs nTests nUnd allArgsGenerated -> msgStr +++ conclude nTests nUnd labels
211 212 213 214 215
		with
			msgStr
			| allArgsGenerated = "Passed: success for arguments"
			| nTests == 0      = "Passed"
			| otherwise        = "Passed: maximum number of arguments (" <+ maxArgs <+ ") generated"
Camil Staps's avatar
Camil Staps committed
216 217 218
		CounterExpls nTests nUnd nE -> pluralisen English nE "counterexample" +++ " found" +++ conclude nTests nUnd labels
		Undefined nUnd -> "Undefined: no success nor counterexample found, all tests rejected or undefined" +++ conclude maxTests nUnd labels
		NoTests maxArgs nTests nUnd -> "No tests performed, maximum number of arguments (" <+ maxArgs <+ ") generated" +++ conclude nTests nUnd labels
219 220 221 222 223

	withBlank x
	| addWhite  = blank +++ x
	| otherwise = x

Camil Staps's avatar
Camil Staps committed
224 225
	conclude :: Int Int [(String, Int)] -> String
	conclude ntests nund labels
226
		# n    = maxTests-ntests
Camil Staps's avatar
Camil Staps committed
227
		# rest = showLabels n (sort labels)
228 229 230 231 232 233 234 235 236 237
		# rest = case nRej of
			0 -> rest
			n -> [", ", pluralisen English n "case", " rejected": rest]
		# rest = case nund of
			0 -> rest
			n -> [", ", pluralisen English n "case", " undefined": rest]
		| n==0
			= concat rest
			= concat [" after ",pluralisen English n "test":rest]

Camil Staps's avatar
Camil Staps committed
238 239 240 241
	showLabels :: !Int ![(String,Int)] -> [String]
	showLabels ntests [] = ["\n"]
	showLabels 0      [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]
	showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]
242

Camil Staps's avatar
Camil Staps committed
243 244
jsonEventStart :: !(Maybe String) !String -> String
jsonEventStart mod name = toString (toJSON {StartEvent | name=name, module_name=mod}) +++ "\n"
245

Camil Staps's avatar
Camil Staps committed
246 247
jsonEventEnd :: !(Maybe String) !String !TestsResult ![CounterExampleRes] ![(String, Int)] -> String
jsonEventEnd mod name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
248
where
249
	endEvent =
Camil Staps's avatar
Camil Staps committed
250 251 252 253 254
		{ name        = showName False name
		, module_name = mod
		, event       = eventType
		, message     = concat
			[ humanReadableResOutput False mod name res counterExamples labels
Camil Staps's avatar
Camil Staps committed
255
			: map (humanReadableCEOutput False False) counterExamples
256 257 258 259 260 261 262 263
			]
		}

	eventType = case res.resultType of
		Proof _            -> Passed
		PassedTest _ _ _ _ -> Passed
		CounterExpls _ _ _ -> Failed $ Just $ CounterExamples $
			(\ce ->
Camil Staps's avatar
Camil Staps committed
264
				{ counterExample   = map GPrint ce.CounterExampleRes.argsRepresentation
265 266 267 268 269 270 271 272
				, failedAssertions = fst3 <$> ce.CounterExampleRes.failedAssertions
				}
			) <$> counterExamples
		Undefined _        -> Failed Nothing
		NoTests _ _ _      -> Failed Nothing

showName :: Bool String -> String
showName quoteName l = if quoteName ("\"" <+ l <+ "\" ") l
273

274 275
toPrintConfig :: ([PrintOption] -> PrintConfig)
toPrintConfig = foldl handleOption verbosePrintConfig
276
where
Camil Staps's avatar
Camil Staps committed
277 278 279 280
	handleOption pc Verbose          = verbosePrintConfig
	handleOption pc Trace            = tracePrintConfig
	handleOption pc (Concise n)      = countPrintConfig n
	handleOption pc Quiet            = quietPrintConfig
281
	handleOption pc OutputTestEvents =
282 283 284 285 286
		{ pc
		& everyOutput          = noEveryOutput
		, counterExampleOutput = noCounterExampleOutput
		, resultOutput         = jsonEventEnd
		, beforeStartOutput    = jsonEventStart
287
		}
288 289

derive genShow Testoption, GenType
290 291 292 293

Test :: ![Testoption] !p -> [GastEvent] | Testable p
Test options p = testConfig config.randoms {config & randoms = []} p
where
294
	config = foldl handleOption defaultTestConfig options
295 296 297 298 299 300 301 302

	handleOption c (Tests i)      = {c & maxTests = i, maxArgs = 2*i}
	handleOption c (Fails i)      = {c & fails = i}
	handleOption c (Args i)       = {c & maxArgs = i}
	handleOption c (RandomSeed i) = {c & randoms = genRandInt i}
	handleOption c (RandomList r) = {c & randoms = r}
	handleOption c (MaxDepth i)   = {c & genState = {c.genState & maxDepth = i}}
	handleOption c (Skew s)
303 304 305 306
	| s > 0     = {c & genState = {c.genState & mode = SkewGeneration {skewl = 1, skewr = s}}}
	| s < 0     = {c & genState = {c.genState & mode = SkewGeneration {skewl = ~s, skewr = 1}}}
	| otherwise = {c & genState = {c.genState & mode = SkewGeneration {skewl = 1, skewr = 1}}}
	handleOption c Bent = {c & genState = {c.genState & mode = BentGeneration}}
307 308 309
	handleOption _ o = abort ("Test: unknown option \"" +++ show1 o +++ "\"\n")

TestList :: ![Testoption] ![p] -> [GastEvent] | Testable p
310 311
TestList options ps = flatten (map (Test options) ps)

Bas Lijnse's avatar
Bas Lijnse committed
312
test :: !p -> [String] | Testable p
313
test p = testn 1000 p
Bas Lijnse's avatar
Bas Lijnse committed
314 315 316 317 318

testn :: !Int !p -> [String] | Testable p
testn n p = verbosen n aStream p

testnm :: !Int !Int !p -> [String] | Testable p
319
testnm n m p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
320 321

ttestn :: !Int !p -> [String] | Testable p
322
ttestn n p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
323 324

ttestnm :: !Int !Int !p -> [String] | Testable p
325
ttestnm n m p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
326 327

verbose  :: !RandomStream !p -> [String] | Testable p
328
verbose rs p = printEvents verbosePrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
329 330

verbosen :: !Int !RandomStream !p -> [String] | Testable p
331
verbosen n rs p = printEvents verbosePrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
332 333

concise :: !RandomStream !p -> [String] | Testable p
Camil Staps's avatar
Camil Staps committed
334
concise rs p = printEvents (countPrintConfig 100) $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
335 336

concisen   :: !Int !RandomStream !p -> [String] | Testable p
Camil Staps's avatar
Camil Staps committed
337
concisen n rs p = printEvents (countPrintConfig 100) $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
338 339

quiet :: !RandomStream !p -> [String] | Testable p
340
quiet rs p = printEvents quietPrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
341 342

quietn   :: !Int !RandomStream !p -> [String] | Testable p
343
quietn n rs p = printEvents quietPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
344 345

quietnm   :: !Int !Int !RandomStream !p -> [String] | Testable p
346
quietnm n m rs p = printEvents quietPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
347

348
testEvents :: !RandomStream !p -> [String] | Testable p
349
testEvents rs p = printEvents testEventsPrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
350

351
testEventsn :: !Int !RandomStream !p -> [String] | Testable p
352
testEventsn n rs p = printEvents testEventsPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
353

354 355 356
testConfig :: RandomStream Config p -> [GastEvent] | Testable p
testConfig rs {maxTests,maxArgs,fails,genState} p
	# res = evaluate p genState newAdmin
Camil Staps's avatar
Camil Staps committed
357
	= [GE_TestStarted (testmodule p) (testname p):analyse res maxTests maxArgs 0 0 0 [] []]
Bas Lijnse's avatar
Bas Lijnse committed
358
where
359 360 361 362 363
	analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExampleRes] ![(String,Int)] -> [GastEvent]
	analyse results nTests nArgs nRej nUnd nE counterExamples labels =
		case analyse` results nTests nArgs nRej nUnd nE of
			// testing of property finished
			Just resType -> [GE_TestFinished
Camil Staps's avatar
Camil Staps committed
364
				(testmodule p) (testname p)
365 366 367 368 369 370 371 372 373 374 375 376
				{maxTests = maxTests, nRej = nRej, resultType = resType}
				counterExamples
				labels]
			// continue with testing property
			Nothing ->
				let [res:rest] = results in
				[GE_Tick (maxTests-nTests+1) res:case res.res of
					OK   -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels)
					Pass -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels) // NOT YET CORRECT ?
					CE   -> [GE_CounterExample counterExample:more]
					with
						counterExample =
377 378 379 380 381 382 383
							{ maxTests           = maxTests
							, nTests             = nTests
							, nE                 = nE
							, args               = res.Admin.args
							, argsRepresentation = res.Admin.argsRepresentation
							, name               = let n = testname p in join "." [n:dropWhile ((==) n) (reverse res.namePath)]
							, failedAssertions   = res.Admin.failedAssertions
384 385 386 387
							}
						more | nE+1<fails
							= analyse rest (nTests-1) (nArgs-1) nRej nUnd (nE+1) [counterExample: counterExamples] (admin res.labels labels)
							= [GE_TestFinished
Camil Staps's avatar
Camil Staps committed
388
								(testmodule p) (testname p)
389 390 391 392 393 394 395 396 397 398 399 400
								{ maxTests   = maxTests
								, nRej       = nRej
								, resultType = CounterExpls (nTests - 1) nUnd (nE + 1)
								}
								[counterExample: counterExamples]
								(admin res.labels labels)]
					Rej   -> analyse rest nTests (nArgs-1) (nRej+1) nUnd     nE counterExamples labels
					Undef -> analyse rest nTests (nArgs-1) nRej     (nUnd+1) nE counterExamples labels
					_     -> abort "Error in Gast: analyse; missing case for result\n"
				]

	// there should always be a result for empty result lists!
401 402 403
	analyse` :: ![.Admin] !Int !Int !Int !Int !Int -> Maybe ResultType
	analyse` [] ntests nargs nrej 0    0  = Just $ Proof ntests
	analyse` [] ntests nargs nrej nund 0
404 405
	| ntests==maxTests                    = Just $ Undefined nund
	| otherwise                           = Just $ PassedTest maxArgs ntests nund True
406 407 408
	analyse` [] ntests nargs nrej nund ne = Just $ CounterExpls ntests nund ne
	analyse` _  0      nargs nrej nund 0  = Just $ PassedTest maxArgs 0 nund False
	analyse` _  0      nargs nrej nund ne = Just $ CounterExpls 0 nund ne
409 410 411
	analyse` _  ntests 0     nrej nund 0
	| ntests == maxTests                  = Just $ NoTests maxArgs ntests nund
	| otherwise                           = Just $ PassedTest maxArgs ntests nund False
412
	analyse` _  ntests 0     nrej nund ne = Just $ CounterExpls ntests nund ne
413
	analyse` _  _      _     _    _    _  = Nothing
Bas Lijnse's avatar
Bas Lijnse committed
414 415 416 417 418 419 420 421 422 423 424

	admin :: ![String] ![(String,Int)] -> [(String,Int)]
	admin [] accu = accu
	admin [label:rest] accu = admin rest (insert label accu)

	insert :: !String ![(String,Int)] -> [(String,Int)]
	insert label [] = [(label,1)]
	insert label [this=:(old,n):rest]
	 | label==old
		= [(old,n+1):rest]
		= [this:insert label rest]