Systematically use WithDefault for PragmaOptions

[andreasabel]

In this PR:

• add opposites to most boolean flags via a generic pragmaFlag method and the WithDefault type
• compute option implications at use site; e.g. --flat-split implies --cohesion; rather than implementing this as a side effect of --flat-split, we include optFlatSplit as disjunctive component in optCohesion; thus --flat-split --no-flat-split will not turn on --cohesion
• --exact-split is now synonym of -WCoverageNoExactSplit
• everything cubical is left untouched by this PR
• --count-clusters is now on by default
• CHANGELOG and docs have been updated

Also: closes #6573, closes #6574.

• Check on presence of --erasure in --erase-record-parameters comes too early #6573
• Sort out --exact-split vs. -WCoverageNoExactSplit #6574

[jespercockx]

Also related: #5265 and #5264. I was working on these last year but unfortunately got stalled and ran out of steam.

[nad]

@andreasabel, you changed some options so that activation of "option X that only makes sense together with option Y" now implies activation of "option Y". Is this a good idea? It can lead to less typing, but one could also argue that it is more clear if certain options always have to be declared.

Currently some options are treated in this way, while others are not. For instance, --erase-record-parameters implies --erasure, but --erased-matches does not. I think --erase-record-parameters and --erased-matches should be handled in the same way, but I have not decided which variant I prefer. Should we strive for clarity or brevity?

[andreasabel]

@andreasabel, you changed some options so that activation of "option X that only makes sense together with option Y" now implies activation of "option Y". Is this a good idea?

I think if option X is "Y with additional features" then X should imply Y, rather than explicitly require Y. For the "erasure family" of options in particular, since these have "erase" already in the name.

It is a bit like in a restaurant, where you can order a beer but also just a glass, but the order of a beer will imply the order of a glass... ;-) Meaning to say that I expect from a tool some common sense (as far as possible).

Currently some options are treated in this way, while others are not. For instance, --erase-record-parameters implies --erasure, but --erased-matches does not. I think --erase-record-parameters and --erased-matches should be handled in the same way

I agree. Somehow I didn't do anything for --erased-matches because it was possible to supply it without --erasure without getting an error (unlike --erase-record-parameters which would error without --erasure). I guess this was an oversight in case of --erased-matches. I will conform it to --erase-record-parameters so that it implies --erasure.

--erased-matches is on by default, so it cannot imply --erasure, which is off by default. What can be done about it that it will internally report to be off unless --erasure is also on. (Edit: the latter does not seem helpful.)

[nad]

--erased-matches is on by default, so it cannot imply --erasure, which is off by default.

Well, --erased-matches is on by default if you use --with-K (which is on by default), but not if you use --without-K/--cubical-compatible/--erased-cubical/--cubical:

agda/src/full/Agda/Interaction/Options/Base.hs

Lines 1254 to 1265 in b673c46

	withKFlag :: Flag PragmaOptions
	withKFlag o = return $ o
	{ _optWithoutK = Value False
	, _optErasedMatches = Value True
	}
	withoutKFlag :: Flag PragmaOptions
	withoutKFlag o = return $ o
	{ _optWithoutK = Value True
	, _optFlatSplit = setDefault False (_optFlatSplit o)
	, _optErasedMatches = setDefault False (_optErasedMatches o)
	}

agda/src/full/Agda/Interaction/Options/Base.hs

Lines 1270 to 1290 in b673c46

	cubicalCompatibleFlag :: Flag PragmaOptions
	cubicalCompatibleFlag o =
	return $ o
	{ _optCubicalCompatible = Value True
	, _optWithoutK = setDefault True $ _optWithoutK o
	, _optFlatSplit = setDefault False $ _optFlatSplit o
	, _optErasedMatches = setDefault False $ _optErasedMatches o
	}
	cubicalFlag
	:: Cubical -- ^ Which variant of Cubical Agda?
	-> Flag PragmaOptions
	cubicalFlag variant o =
	return $ o
	{ _optCubical = Just variant
	, _optCubicalCompatible = setDefault True $ _optCubicalCompatible o
	, _optWithoutK = setDefault True $ _optWithoutK o
	, _optTwoLevel = setDefault True $ _optTwoLevel o
	, _optFlatSplit = setDefault False $ _optFlatSplit o
	, _optErasedMatches = setDefault False $ _optErasedMatches o
	}

[andreasabel]

Ok, I haven't looked at the without-K/cubical family in this PR.
Basically, --erasure should be implied if _optErasedMatches has Value True, meaning it has been explicitly set by the user. This is easy to facilitate.

Just for the record, agda --without-K --erased-matches is neither an error right now (requesting --erasure) nor does it imply --erasure:

{-# OPTIONS --without-K --erased-matches #-}

foo : (@0 A : Set) (x : A) → A
foo A x = x

Erasure attributes have not been enabled (use --erasure to enable them): 0

PR:

• Fixup PR #6556 II: explicit --erased-matches implies --erasure #6613

[andreasabel]

Fixed this unwords (case null info) by bd4f880