- add tests for a couple of related rewrites
- accept same range of constants for sign extension in the rewrite as for
  the zero extension version (to make the test simpler)

- additional rewrites (signed extend of subrange@zeros, subrange assignment,
  variants with casts)
- drop # from new top-level type variables (e.g., n_times_8) so that the
  rewriter knows that they're safe to include in casts
- add casts in else-branches when only one possible value for a size is left
- add casts when assertions force a size to be a particular value
- don't use types to detect set constraints in analysis because we won't
  know which part of the assertion should be replaced
- also use non-top-level type variables when simplifying sizes in analysis
  (useful when it can from pattern matching on an ast)
- cope with repeated int('n) in a pattern match (!)

Also handle any type variables from assignments and degrade gracefully
during constant propagation when unification is not possible.

- handle multiple bitvector length variables
- more fine-grained unnecessary cast insertion checks
- add tuple matching support to constant propagation (for the test)

- updates for type checking changes
- handle a little more pattern matching in constant propagation
- fix bug where false positive warnings were produced
- ensure bitvectors in tuples are always monomorphised (to catch the case
  where the bitvectors only appear alone with a constant size)

It now pushes casts into lets and constructor applications, and so
supports the case needed for RISC-V.

Fixes monomorphisation on files using mappings.
Also extended constant propagation to handle pattern matches on
bitvector expressions (because an earlier rewrite replaces the literals).
Also moved L_undef rewriting because monomorphisation can handle them
but not the replacement functions.