Add cv_eval_pat to cv_transLib (and an example)

[myreen]

No description provided.

[xrchz]

What's the difference between Some p and Tuple [p]?

[myreen]

This comment makes me realise that it's unclear what the pattern means. I wrote a long comment in the file, see:

HOL/examples/cv_compute/cv_eval_exampleScript.sml

Lines 15 to 24 in e211611

	(* The following example demonstrates that the given pattern,
	Some (Tuple ...), instructs cv_eval_pat what to do with the
	result of evaluation. In this example, we can see that the
	result must be a SOME containing a tuple and the elements
	of the tuple are handled as follows.
	- The first is just directly evaluated.
	- The second is left untouched after the raw cv computation.
	- The third is stored in a new constant, big_replicate, that
	can be used in subsequent calls to cv_trans, cv_eval, etc.
	*)

[xrchz]

So is Tuple [Some (Tuple [])] just not really supposed to be used? Or does that also make sense?

[myreen]

cv_eval_pat will raise an exception if users write Tuple [] in their pattern.

Writing Tuple [x] will mean the same as a single-element tuple in HOL, i.e. it's not a tuple. What's the difference between (2) and 2 in HOL? No difference.

[tanyongkiam]

Some additional context: the constructor Tuple was originally Pair (which avoids some of the above issues). However, the Pair constructor would need to be disambiguated because it is also used elsewhere in CV.