[xsmith-dev] XSmith questions

[William G Hatch]

As hinted in my other reply, the best answer would be that Xsmith type
variables have a list of types that they can't be in addition to their
list of possible types.  Then you could test whether it is possibly,
definitely, or definitely not a given thing, and if you make a choice
that it isn't something you can specify just that without removing
other flexibility later.  But since that feature still doesn't exist,
I don't have a great answer.  Sometimes in situations like this I punt
to concretizing the type.  It removes flexibility for later choices,
but lets me make a clear decision about the type now (without forcing
all unconstrained variables into the same choice).

On Fri, Aug 27, 2021 at 02:25:38PM -0700, Sorawee Porncharoenwase wrote:
>So, this is actually another question that I meant to ask. I have this code
>as a choice method for choice-filters-to-apply:
>
>[VariableReference
>  (λ ()
>    (define t ($xsmith_type (current-hole)))
>    (define method? (can-unify? t (method-type (fresh-type-variable)
>(fresh-type-variable))))
>    (cond
>      [method?
>       (and (parent-node (current-hole))
>            (equal? (ast-node-type (parent-node (current-hole)))
>                    'ProcedureApplicationForMethod))]
>      ;; we are generating default return values.
>      ;; at this point, there's no lifting target, so we can't have
>      ;; variable reference
>      [(and (parent-node (current-hole))
>            (equal? (ast-node-type (parent-node (current-hole)))
>                    'TopLevelMethod))
>       #f]
>      [else #t]))]
>
>I raised a concern earlier that can-unify? is not ideal because
>
>($xsmith_type (current-hole))
>
>is sometimes unconstrained, meaning it rejects more than it should, and you
>agree with that. What’s the right way to do this properly?
>
>
>On Fri, Aug 27, 2021 at 2:10 PM William G Hatch <william at hatch.uno> wrote:
>
>> In Dafny do function expressions not generate closures?
>>
>> My first thought is that you can add a choice filter (with
>> choice-filters-to-apply, defined probably with add-choice-method) that
>> disallows expressions that need an array type unless there is a
>> variable already visible or its in a context where it can lift one.
>>
>> > function expression (which can't have any statement)
>>
>> As an aside, I hate languages that do this...
>>
>> On Fri, Aug 27, 2021 at 02:33:59AM -0700, Sorawee Porncharoenwase wrote:
>> >I feel like this should be easy, but somehow the solution eludes me...
>> >
>> >An array in Dafny must be allocated and then stored in a variable as a
>> part
>> >of the array declaration statement (essentially, there's no array
>> literal).
>> >The variable can then be used freely in any expression position. However,
>> >the fact that the allocation is a statement means that in function
>> >expression (which can't have any statement), the only way to get an array
>> >value in is through parameters. In particular, there is no lifting target
>> >of array type inside function expressions.
>> >
>> >How should I deal with this situation? Is it possible to create a new kind
>> >of variable reference that "tries" the array type, and use stuff like
>> >xsmith_get-reference-for-child! to see if there is a lifting target, and
>> if
>> >there's none, then try other types (say, integer) that are guaranteed to
>> >have a lifting target instead? That doesn't seem possible since the type
>> of
>> >the node seems already predetermined by the time fresh is invoked.
>> >
>> >On Mon, Aug 23, 2021 at 10:06 AM William G Hatch <william at hatch.uno>
>> wrote:
>> >
>> >> I agree this is too bad.  But I'm sorry to say that I'm not going to
>> >> improve this right now.  It would require fairly major work in the
>> >> type unification machinery.  The workaround is maybe not the best, but
>> >> it's at least pretty easy to do.
>> >>
>> >> On Mon, Aug 23, 2021 at 12:12:38AM -0700, Sorawee Porncharoenwase wrote:
>> >> >I want to express a type constraint that it’s either a product type of
>> >> >length 0, 2, or 3. Is there a way to do that? fresh-type-variable with
>> >> >arguments seems like a solution, except that the composite type isn’t
>> >> >allowed to be repeated. Usually, if I have a generic type of the same
>> >> >arity, I can simply push fresh-type-variable in. E.g.,
>> >> >
>> >> >(fresh-type-variable
>> >> > (immutable (array-type ...))
>> >> > (immutable (set-type ...)))
>> >> >
>> >> >=>
>> >> >
>> >> >(immutable (fresh-type-variable (array-type ...) (set-type ...)))
>> >> >
>> >> >The problem is that product-type‘s argument is a list of types of
>> false,
>> >> so
>> >> >fresh-type-variable doesn’t work there.
>> >> >
>> >> >I guess I can create generic types product0, product2, and product3,
>> and
>> >> >put them in fresh-type-variable, but well, I really want to avoid doing
>> >> >this.
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >
>> >> >On Fri, Jul 30, 2021 at 5:35 PM Sorawee Porncharoenwase <
>> >> >sorawee.pwase at gmail.com> wrote:
>> >> >
>> >> >> As always, thanks! :)
>> >> >>
>> >> >> On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <william at hatch.uno>
>> >> wrote:
>> >> >>
>> >> >>> On Fri, Jul 30, 2021 at 03:32:54PM -0700, Sorawee Porncharoenwase
>> >> wrote:
>> >> >>> >> When I've had this situation, as a workaround, I've just made a
>> >> >>> >> function that returns a fresh-type-variable with all of the
>> >> supported
>> >> >>> >> base types and maybe some constructed types.  It's... not great.
>> >> >>> >>
>> >> >>> >
>> >> >>> >My question is, say, I want to disallow a function, a list of
>> >> functions,
>> >> >>> a
>> >> >>> >list of list of functions, a list of list of list of functions,
>> and so
>> >> >>> on.
>> >> >>> >Of course, I can express things positively: it's an int or bool or
>> >> >>> >listof... what? A list of fresh-type-variable runs a risk of
>> choosing
>> >> >>> >function type. So I could do a listof (int or bool or listof ...)
>> for
>> >> >>> >another level, and keep increasing levels. Is this what you have in
>> >> mind?
>> >> >>>
>> >> >>> Yeah, that's the problem with it.  You can realistically only
>> specify
>> >> >>> a small set of the infinite set of constructible types (granted in
>> >> >>> practice the set of types usable by xsmith is bounded as well since
>> it
>> >> >>> bounds the tree depth of constructed types).  But specifying that
>> list
>> >> >>> is a chore and you probably get poor performance if you actually try
>> >> >>> to generate many combinations with constructed types.  So in
>> practice
>> >> >>> when I have this situation so far I just... don't generate as many
>> >> >>> things as I otherwise could.
>> >> >>>
>> >> >>> >> However, that feature just hasn't made it to the top of my
>> >> priorities
>> >> >>> >> yet...  Sorry :(
>> >> >>> >>
>> >> >>> >
>> >> >>> >No worries at all! If there's anything that I can help regarding
>> this
>> >> >>> >feature, let me know. It looks like the representation of a type
>> right
>> >> >>> now
>> >> >>> >consists of a lower bound and an upper bound, and probably this
>> >> feature
>> >> >>> >will require changing the representation, correct?
>> >> >>>
>> >> >>> The upper and lower bounds are about subtyping.  If a type changes
>> >> >>> through unification it can affect the types connected as upper/lower
>> >> >>> bounds.  This feature shouldn't change that, other than being more
>> >> >>> information that will be conveyed to the related type variables.
>> When
>> >> >>> a variable is constrained by unification to remove a type from its
>> >> >>> allowed list, all related types in its upper/lower bounds lists also
>> >> >>> remove that type.  Eg. if variable A is (or string int (-> int int))
>> >> >>> and variable B is (or (subtype-of string) (subtype-of int)
>> (subtype-of
>> >> >>> (-> int int))) and variable A is constrained to definitely not be a
>> >> >>> function, variable B could no longer be a function and still be a
>> >> >>> subtype of A.  If two variables are unified with `unify!` instead of
>> >> >>> `subtype-unify!` (or equivalently by being `subtype-unify!`ed in
>> both
>> >> >>> directions) they are more or less merged into a single variable.
>> (IE
>> >> >>> the object that you get from `fresh-type-variable` can be merged
>> with
>> >> >>> others and they are always canonicalized before doing anything to
>> >> >>> them.)
>> >> >>>
>> >> >>> Right now a type variable has a list of possible types (or #f for
>> >> >>> unconstrained).  The list can have any number of base types and
>> every
>> >> >>> compound type, but it's limited in that it can only have one of each
>> >> >>> compound type (though each compound type may have type variables
>> >> >>> inside and thus represent potentially many types).
>> >> >>>
>> >> >>> I think the needed change would be to add a list of disallowed
>> types.
>> >> >>> I think this list should probably be applied recursively -- IE it
>> >> >>> should be pushed to child types.  So eg. if you disallow function
>> >> >>> types in a type variable it also disallows lists of functions, etc.
>> >> >>> I'm not certain if there are exceptions, though.  Would it make
>> sense
>> >> >>> to have a recursive and non-recursive version of this?
>> >> >>>
>> >> >>> At any rate, when checking if things `can-unify?`, you would use the
>> >> >>> disallowed list as well as the allowed list of both variables to
>> >> >>> determine the outcome.  When variables are unified, they need to
>> >> >>> propagate their disallowed list to related type variables (IE the
>> ones
>> >> >>> in the upper/lower bounds lists).
>> >> >>>
>> >> >>> Another thing that would need to be worked out is what exactly to
>> >> >>> store in the disallowed list.  Constructors for compound types?  Or
>> >> >>> maybe predicates?  Probably base types and predicates is my guess.
>> >> >>>
>> >> >>> At any rate, since we keep emailing about the issue I've thought
>> >> >>> through more of it than before, so now I'm much more likely to
>> >> >>> actually sit down and do it soon. :P
>> >> >>>
>> >> >>
>> >>
>>