Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rewrites stop #916

Closed
stahlbauer opened this issue Nov 18, 2019 · 1 comment
Closed

Rewrites stop #916

stahlbauer opened this issue Nov 18, 2019 · 1 comment

Comments

@stahlbauer
Copy link

Problem: Only one rewrite rule is applied. The rewrites stops after this first rule. Any hint?

Here is the K file:

module TEST-SYNTAX
    imports DOMAINS

    syntax App ::=
            "app" Id ModuleDefinitionList 

    syntax ModuleDefinitionList ::=
            List { ModuleDefinition, "" }

    syntax ModuleDefinition ::=
            "unit" Id "begin" FunctionDefinitionList "end"

    syntax FunctionDefinition ::=
            "fun" Id 

    syntax FunctionDefinitionList ::=
            List { FunctionDefinition, "" }

endmodule

module TEST

    imports DOMAINS
    imports TEST-SYNTAX

    syntax KResult ::= Int

    configuration <T>
        <Modules>
            <Module multiplicity="*" type="List">
                <ModuleId> .K </ModuleId>
                <Threads>
                    <Thread multiplicity="*" type="List">
                        <k> $PGM </k>
                    </Thread>
                </Threads>
                <Memory> .Map </Memory>
                <Functions>
                    <Function multiplicity="*" type="List">
                        <FunctionId> .K </FunctionId>
                        <FunctionBody> .K </FunctionBody>
                    </Function>
                </Functions>
            </Module>
        </Modules>
    </T>

    rule <k> app Id DDL:ModuleDefinitionList => DDL ... </k>

    rule <k> .ModuleDefinitionList => . ... </k>
    rule <k> D:ModuleDefinition Dd:ModuleDefinitionList => D ~> Dd ... </k> [structural]
    rule <k> unit I:Id begin FDL:FunctionDefinitionList end => . </k>
        (.Bag
        <Module>
            <ModuleId>I</ModuleId>
            <Threads>
                <Thread><k>FDL</k></Thread>
                ...
            </Threads>
            <Memory> .Map </Memory>
            ...
        </Module>)

    rule <k> .FunctionDefinitionList => . ... </k>
    rule <k> F:FunctionDefinition Ff:FunctionDefinitionList => F ~> Ff ... </k> [structural]
    rule <k> fun I:Id => . ... </k>
        (.Bag <Function>
            <FunctionId> I </FunctionId>
            <FunctionBody> .K </FunctionBody>
        </Function>)

endmodule

A program test-program.src in this language:

app ExampleProgram

unit MD begin
    fun foo
end
@stahlbauer
Copy link
Author

stahlbauer commented Nov 19, 2019

I am working on a smaller example. The way I am using (.Bag ...) seems to be wrong.

Baltoli pushed a commit that referenced this issue Apr 9, 2024
Closes runtimeverification/pyk#885.

Overhauls the way command line argument parsing and parameter passing is
done.
When building a pyk-based command-line tool, for each subcommand of the
tool, extend `class Command` . This subclass should contain all
information about what arguments are accepted by that command (through
providing its own arguments or inheriting from other `Options` classes),
the default values of those arguments, the name of the command, and the
help string for the command, as static fields. The values of those
options for a specific invocation of that command are stored as
non-static fields of a `Command`. The `Command` subclass contains the
code that runs when that command is called in `exec()`. In addition,
default values of arguments inherited from other `Options` classes can
be overridden in the subclass.

The `CLI` class manages the tool's CLI options. It is constructed by
passing in the name of every command subclass to be included in the
tool. It can then build the whole `ArgumentParser` for the tool and
process the arguments to instantiate a new `*Command` of the correct
type and with the correct arguments.

Advantages:
- All information about a subcommand is consolidated into one place
- Default values specified in only one place
- Commands only have to be listed once, when instantiating `CLI`
- Setting up an argument parser with all subcommands is done
automatically.
- Routing of requested command to its associated execution function is
done automatically.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Baltoli pushed a commit that referenced this issue Apr 9, 2024
Closes runtimeverification/pyk#885.

Overhauls the way command line argument parsing and parameter passing is
done.
When building a pyk-based command-line tool, for each subcommand of the
tool, extend `class Command` . This subclass should contain all
information about what arguments are accepted by that command (through
providing its own arguments or inheriting from other `Options` classes),
the default values of those arguments, the name of the command, and the
help string for the command, as static fields. The values of those
options for a specific invocation of that command are stored as
non-static fields of a `Command`. The `Command` subclass contains the
code that runs when that command is called in `exec()`. In addition,
default values of arguments inherited from other `Options` classes can
be overridden in the subclass.

The `CLI` class manages the tool's CLI options. It is constructed by
passing in the name of every command subclass to be included in the
tool. It can then build the whole `ArgumentParser` for the tool and
process the arguments to instantiate a new `*Command` of the correct
type and with the correct arguments.

Advantages:
- All information about a subcommand is consolidated into one place
- Default values specified in only one place
- Commands only have to be listed once, when instantiating `CLI`
- Setting up an argument parser with all subcommands is done
automatically.
- Routing of requested command to its associated execution function is
done automatically.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant