When needed, add type parameters and variant check to field access

[Chris-Hawblitzel]

(fixes #1366 )

As proposed in #1366 , this adds type parameters and an is-variant check to field accessors when the datatype has type parameters and has at least two variants. For example, for Option<V>, we used to just have:

(declare-fun core!option.Option./Some/0 (core!option.Option.) Poly)

(axiom (forall ((x core!option.Option.)) (!
   (= (core!option.Option./Some/0 x) (core!option.Option./Some/?0 x))
   :pattern ((core!option.Option./Some/0 x))
   :qid internal_core!option.Option./Some/0_accessor_definition
   :skolemid skolem_internal_core!option.Option./Some/0_accessor_definition
)))

With the pull request, we now have:

(declare-fun core!option.Option./Some/0 (Dcr Type core!option.Option.) Poly)

(axiom (forall ((V&. Dcr) (V& Type) (x core!option.Option.)) (!
   (=>
    (is-core!option.Option./Some x)
    (= (core!option.Option./Some/0 V&. V& x) (core!option.Option./Some/?0 x))
   )
   :pattern ((core!option.Option./Some/0 V&. V& x))
   :qid internal_core!option.Option./Some/0_accessor_definition
   :skolemid skolem_internal_core!option.Option./Some/0_accessor_definition
)))

I don't have any tests to add for this, because I don't yet know of any way to actually trigger the unsoundness reported in #1366 .

I checked veritas, and all tests pass with one rlimit needing an increase in ironsht.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.