Skip to content

Enumerate Possible Generator Schedules Lazily (use Lazy Lists) #47

@ngernest

Description

@ngernest

Right now, in the dfs function in DeriveSchedules.lean, we enumerate generator schedules eagerly by putting them all in a list. We should change this implementation by using lazy lists instead, either using our hand-rolled lazy lists (in LazyList.lean) or the one from Batteries.

This change should in theory allow us to support all of the Cedar typing rules when deriving a generator for well-typed Cedar terms. Note that if we expose all 41 Cedar typing rules to Chamelean right now, it takes a very long time (> 5 mins) to derive a generator -- see #43 for more details.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions