[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [xsmith-dev] XSmith questions



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@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@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@gmail.com> wrote:
>> >
>> >> As always, thanks! :)
>> >>
>> >> On Fri, Jul 30, 2021 at 5:29 PM William G Hatch <william@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
>> >>>
>> >>
>>