kframework / k-legacy Goto Github PK

Can we change the naming of the binary releases to k-stable.zip and k-nightly.zip, as discussed? The name k-latest-stable.zip is rather confusing.

So in my work on the streams IO stuff, I end up creating the following term to put in the stdin cell in the initial configuration:

MyListItem(#buffer("")) $noIO:MyList MyListItem(#istream(0))

Then I use a CopyOnWriteTransformer to replace $noIO:MyList with .MyList. Of course this all happens after CompileDataStructures so we are working with a ListBuiltin object.

Unfortunately, the behavior of CopyOnWriteTransformer in this case is to put one ListBuiltin object inside the other as a base term, rather than the more reasonable behavior to distribute the elements of the inner ListBuiltin into the outer ListBuiltin. I have not tried it with Maps, Bags, or Sets, but it's possible something similar happens there as well.

This is a problem as you can imagine because then the base terms aren't the empty list and aren't a variable, and so the term is rejected when it is being converted to the java backend kil. I need this to work in order to be able to substitute the configuration parameters into the initial configuration in order to execute programs that use streams.

This is a quite urgent issue. Technically today is my last day and I am under no obligation to finish the diff I am working on for streams at all. However, I would like to use some of my own personal time to do so in the next couple days so that when I leave it will be with everything nice and tidy. But this can only happen if this bug and any others I run into afterwards are resolved immediately. So I am marking this priority_critical.

while trying to fix some other bug I realized that -xml parameter fails at runtime with the following error:

➜  lesson_1 git:(master) ✗ rm -rf lambda-kompiled .k
➜  lesson_1 git:(master) ✗ kompile -xml lambda.k
Exception in thread "main" java.lang.NoClassDefFoundError: org/xmlpull/v1/XmlPullParserException
        at com.thoughtworks.xstream.XStream.<init>(XStream.java:336)
        at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:96)
        at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:282)
        at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:250)
        at org.kframework.main.Main.main(Main.java:68)
Caused by: java.lang.ClassNotFoundException: org.xmlpull.v1.XmlPullParserException
        at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
        at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
        at java.security.AccessController.doPrivileged(Native Method)
        at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
        at java.lang.ClassLoader.loadClass(ClassLoader.java:423)
        at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
        at java.lang.ClassLoader.loadClass(ClassLoader.java:356)
        ... 5 more
➜  lesson_1 git:(master) ✗ 

maybe some classes are missing in jar files?

Trying to kompile this module

module BUG
syntax S ::= right :
| "prod"
endmodule

with version
K-framework nightly build.
Git Revision: v3.2.1-208-g8e533f5

produces an error beginning

[Error] Parser: org.kframework.parser.basic.ParseException: Encountered " "|" "| "" at line 3, column 6.

There's only a single bar in the input file! Also, the escaping is excessive.

I was experimenting with kompile and got the following error. Is there a Jar missing from the distribution?

$ cat test.k
module TEST

endmodule

$ ../../../../../../../dist/bin/kompile -xml test.k
Exception in thread "main" java.lang.NoClassDefFoundError: org/xmlpull/v1/XmlPullParserException
    at com.thoughtworks.xstream.XStream.<init>(XStream.java:336)
    at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:95)
    at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:284)
    at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:252)
    at org.kframework.main.Main.main(Main.java:68)
Caused by: java.lang.ClassNotFoundException: org.xmlpull.v1.XmlPullParserException
    at java.net.URLClassLoader$1.run(URLClassLoader.java:366)
    at java.net.URLClassLoader$1.run(URLClassLoader.java:355)
    at java.security.AccessController.doPrivileged(Native Method)
    at java.net.URLClassLoader.findClass(URLClassLoader.java:354)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:424)
    at sun.misc.Launcher$AppClassLoader.loadClass(Launcher.java:308)
    at java.lang.ClassLoader.loadClass(ClassLoader.java:357)
    ... 5 more

fslwork$ krun -abc
Error while parsing commandline:Unrecognized option: -abc
Exception in thread "main" java.lang.NullPointerException
at org.kframework.krun.Main.execute_Krun(Main.java:802)
at org.kframework.main.Main.main(Main.java:78)
fslwork$

For uniformity with other errors, I think it should only say:

fslwork$ krun -abc
[Error] Unrecognized option: -abc
fslwork$

krun fails to run user programs that have a module named same as one of the built-in modules. This can be a problem for a name like "builtins" because IMO it's a very generic name and some users may want to use in their K programs.

Warning: Compiled definition file name (builtins) and the extension of the program () aren't the same. Maybe you should use --syntax-module or --main-module options of krun
Warning: Maude produced warnings or errors.
Advisory: redefining module BUILTINS.

There are two options in ktest which always require folders: -programs and -results. By default, both of these are set to the current directory ".". Many users will likely hold the results in the same folder with the programs, either as separate subfolders or even just flat in the same directory.

To save the user from writing the same folder twice in most cases, e.g.

ktest ... -programs FOLDER -results FOLDER

it would be nice to have the -results folder be by default equal to the -programs folder, so one would only write

ktest ... -programs FOLDER

Right now when we execute something with the command:
krun --search-final

the generated file maude_in.maude contains the line:
show search graph .

This line causes performance problems with more complex programs. I use option --search-final to test multithreading in java semantics. Most tests fail with OutOfMemoryError, even with 20GB of heap space. If I try to run maude directly it get stuch in an unending execution, while writing tens of gygabytes on hard disk.

However if I run the same command without the aforementioned line it displays the final configurations correctly in about 5 min.

Please add the option to execute search without search graph, for someone interested in seeing just the output configurations. Also, I suggest search without the graph to be default. And "show search graph" should require an extra option.

➜  lesson_4 git:(master) ✗ rm -rf imp-kompiled
➜  lesson_4 git:(master) ✗ kompile imp.k
➜  lesson_4 git:(master) ✗ kast imp.k
[Error] Critical: Parse error: Syntax error near unexpected character 'I'
        File: /home/omer/K/k/dist/tutorial/2_imp/lesson_4/imp.k
        Location: (1,8,1,8)
➜  lesson_4 git:(master) ✗ kast -fastKast imp.k
[Error] Critical: Parse error: character 'I' unexpected
        File: /home/omer/K/k/dist/tutorial/2_imp/lesson_4/imp.k
        Location: (1,8,1,8)

(also, can anyone explain me what does kast do? if I understand correctly it prints KIL AST in a user-readable format, is that correct?)

The following definitions works fine:

module CTXABS

configuration
$PGM:K

.Map

""

""
0
0

.List



.List

""
.K
.Bag


.List

rule I:Int => . ...

... (. => ListItem(I))
...

endmodule

Bu if we replace the configuration with the following one

configuration

.Map

""

""
0
0

.List




$PGM:K
.List




""
.K
.Bag


.List

the we get the following error:

Exception in thread "main" java.lang.AssertionError
at org.kframework.compile.transformers.ResolveContextAbstraction.transform(ResolveContextAbstraction.java:139)
at org.kframework.kil.Cell.accept(Cell.java:266)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:365)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:390)
at org.kframework.kil.Bag.accept(Bag.java:55)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:112)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:171)
at org.kframework.compile.transformers.ResolveContextAbstraction.transform(ResolveContextAbstraction.java:59)
at org.kframework.kil.Rule.accept(Rule.java:72)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:75)
at org.kframework.compile.transformers.ResolveContextAbstraction.transform(ResolveContextAbstraction.java:35)
at org.kframework.kil.Module.accept(Module.java:102)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:42)
at org.kframework.kil.Definition.accept(Definition.java:121)
at org.kframework.compile.utils.CompilerTransformerStep.compile(CompilerTransformerStep.java:24)
at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:37)
at org.kframework.compile.ResolveConfigurationAbstraction.compile(ResolveConfigurationAbstraction.java:28)
at org.kframework.compile.ResolveConfigurationAbstraction.compile(ResolveConfigurationAbstraction.java:18)
at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:37)
at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:294)
at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:250)
at org.kframework.main.Main.main(Main.java:69)

Note that this example worked some time ago (in July) and I presented it as a strong feature of K.

We want to allow the same program to have multiple tests, as we used to have with ant test in the past (or maybe it still works?). Something like this:

sum.imp
sum.imp.in.1
sum.imp.out.1
sum.imp.in.2
sum.imp.out.2
...

Now that we have ktest, we can either deprecate "ant test" or change it into a simple call to ktest.

Although it is done similar to that of simple-untyped.

More precisely, the rule for reading is the following:

rule [scanner-nextInt]:

invokeImpl(
methodClosure(,,,,,, 'NoMethodBody(_))::methodType(sig(MethodName:Id, ),), _,
'ListWrap(.KList)
) => I :: int
...

ListItem(I:Int) => . ...
when
Id2String(MethodName) ==String "nextInt"
[read]

If i run a program taht should read two numbers and print them, It just hangs.

How to test it:

1. Download java semantics
2. cd java-semantics-semantics
3. chmod +x ../tools/*
4. kompile java
5. add ../tools to $PATH
6. kjrun.sh ../programs/01_smoke_tests/read.java

Consider the following definition:

module TEST

syntax Foo ::= foo(Int, Int)

rule foo(I, I) => .

endmodule

When you kompile this definition and run:

krun -cPGM="foo(5, 6)"

it should not perform any rewrites. However, it rewrites to .K.

Consider the following simple definition:

module CFGP
  syntax Exp ::= Id "=" Int
  configuration 
    <k> $PGM:Exp </k>
    <st> $ST:Map </st>

  rule <k> X:Id = I:Int => . </k>
       <st>... X |-> (_ => I) ...</st>
endmodule

and the program ex.cfgp including "a = 2"
If we run this program with the following comand
$krun ex.cfgp -cST "a |-> 0"

then we get the following error:

[Error] Critical: Parse error: Syntax error near unexpected character ' '
File: a |-> 0
Location: (1,2,1,2)

This is due to the fact the parser does not know how to parse "a". Kasting the program we get

$ kast ex.cfgp
_`(_`)('_=_, _`,`,_(_`(_`)(#token("Id", "a"), .KList), _`(_`)(#_(2), .KList)))

Then trying to replace "a" with its builtin form "#token("Id", "a")(.Klist)" we get a different error:

$ krun ex.cfgp -cST "#token("Id","a")(.KList) |-> 0"
[Error] Critical: Parse error: Syntax error near unexpected character '"'
File: #token("Id","a")(.KList) |-> 0
Location: (1,13,1,13)

I think this should work, even if it is not a perfect solution.

A hack is to add the syntax declaration
syntax Id ::= "a"
to the definition, as we used to do it four years ago. Obviously, this is an unacceptable solution.

We have to urgently find a solution for it. It breaks the definition for the algorithmic language that I want to use for teaching.

https://github.com/kframework/k/blob/master/javasources/KTool/src/org/kframework/compile/transformers/StrictnessToContexts.java#L45 this assertion fails when a syntax have both strict and seqstrict annotations. The compiler doesn't print any errors, it just fails with java.lang.AssertionError.

If you decide on a default behavior to do when this happens or a way to tell this error to the user, I can implement it.

Execution of helloworld.java hangs with the following content at the beginning of :

'packageId(_)(#token("#Id", "")(.KList))
~> #freezer 'CompilationUnit('Some('PackageDec(.K,,HOLE)),,'ListWrap(.KList),,'ListWrap('ClassDec('ClassDecHead('ListWrap('Public(.KList)),,#token("#Id", "helloWorld")(.KList),,'None(.KList),,'None(.KList),,'None(.KList)),,'ClassBody('ListWrap('MethodDec('MethodDecHead('ListWrap('Public(.KList),,'Static(.KList)),,'None(.KList),,'void(.KList),,#token("#Id", "main")(.KList),,'ListWrap('Param('ListWrap(.KList),,'ArrayType('ClassOrInterfaceType('TypeName(#token("#Id", "String")(.KList)),,'None(.KList))),,#token("#Id", "args")(.KList))),,'None(.KList)),,'Block('ListWrap('ExprStm('Invoke('MethodName('AmbName('AmbName(#token("#Id", "System")(.KList)),,#token("#Id", "out")(.KList)),,#token("#Id", "println")(.KList)),,'ListWrap('Lit('String('ListWrap('Chars(# "Hello World!"(.KList)))))))),,'ExprStm('Invoke('MethodName('AmbName('AmbName(#token("#Id", "System")(.KList)),,#token("#Id", "out")(.KList)),,#token("#Id", "println")(.KList)),,'ListWrap('Lit('String('ListWrap('Chars(# "Done!"(.KList))))))))))))))))(.KList) ~> ...

Since packageId(...) is KResult (see core.k), it should be cooled at this step.

K version: 3.2.1-108. Worked fine with 3.2.1-63.

To avoid exhausting the computing resources, it would be good for ktest to take an option saying how many parallel processes, or threads, or however is best to call them, we want it to execute in parallel.

For working on K, it would help to have command line options we could use to skip PDF generation and/or kompile without editing the config.xml

steps to reproduce:

cd \k\dist\examples\simple\untyped
kompile simple-untyped
kast programs/diverse/collatz.simple > collatz.kast
krun --parser=cat collatz.kast
10

Expected:
Testing Collatz' ...

Actual:
computation get stuck at the term "read ( )"

This issue is linked to stdin problems in java semantics.

BuiltinList is implemented using ArrayDeque, which makes equality checks and hash code computation to fail due to ArrayDeque not override said methods. The easiest fix is probably to extend ArrayDeque and implement equality and hash code. This only requires changes in the existing code where new instances of ArrayDeque are created.

I would like to not let this thread die. Michael, Radu, do you think is going to be possible in the new parser/front-end? Basically all it takes is to detect the sort of the argument which contains a ... in it, and that must be a collection sort (i.e., List, Set, Map, etc.), and in that case to replace the ... with the corresponding constructor and an anonymous variable. It looks quite simple (provided we have a good parser). I'm going to move this into an issue, to make sure we keep track of it.

Grigore

From: [email protected] [[email protected]] on behalf of Rosu, Grigore [[email protected]]
Sent: Friday, September 20, 2013 12:55 PM
To: Andrei Arusoaie
Cc: [email protected]
Subject: Re: [k-list] on ... in rules

You are right. That's what we are doing now. But that limiation was admitted mostly because of our previously limited parsing capabilities. There is hope that we can now work with associative lists in general, where the rewrite engine will optimize matching if it only happens in a heat/tail style.

However, the discussion is sort of orthogonal to this issue. Even if we decide to keep cons-lists, for whatever reasons, we can still use the ... wherever zero, one or more elements can be found. For example,

syntax Exps ::= ConsList{Exp}

syntax Exp ::= head(Exps)

rule head(E...) => E

would desugar to

rule head(E,_) => E

and

rule head(...E) => whatever

would give an error.

Grigore

From: Andrei Arusoaie [[email protected]]
Sent: Friday, September 20, 2013 12:48 PM
To: Rosu, Grigore
Cc: Radu Mereuta; [email protected]
Subject: Re: [k-list] on ... in rules

Maybe this is more related to "how to do it" rather than "what we want", but aren't we currently support cons lists when declaring List{Id, ","}? Do we allow them to match inside a cons list?

Just saying...

Andrei A.

2013/9/20 Rosu, Grigore [email protected]

The idea here is that the collection argument of f tells immediately what kind of collection is there, so K should know how to desugar the ... (modulo, as usual, parsing complications).

Grigore

From: [email protected] [[email protected]] on behalf of Rosu, Grigore [[email protected]]
Sent: Friday, September 20, 2013 12:41 PM
To: Radu Mereuta

Cc: [email protected]
Subject: Re: [k-list] on ... in rules

First, you don't need to do it yourself alone. For now, the idea is to understand WHAT we want. We will worry later about HOW to do it.

By "collection" I mean everything holding more elements of a certain sort, ordered or not. So far only lists, sets, maps, multisets. But we may add more in the future, such sorted maps, sets, etc. For simplicity, let us assume such a collection sort for a collection of elements of sort Sort, say CollectionSort, whose grouping construct is "@". If Collection is, for example, "List{Sort}{","}, then "@" is ",". Here for simplicity I'm assuming that soon we will have only one kind of lists, which will be associative, and which will be defined with the notation above, and NOT the current one List{Sort,","}.

By "operation" I mean anything which can be defined with the K keyword syntax as a production, be it buiitin, predifed, or user defined, as well as an operation that serves as a cell in configurations, for example '_'. By an operation f taking an argument of sort collection, I mean something like this (I only show the case with one argument and prefix notation, but the same applies with multi-argument operations with any syntax):

syntax Sort ::= f(CollectionSort)

or

configuration ..... ..... .....

where ..... means stuff we don't care about.

Now, suppose that in some rule I write f(.....c1...c2.....), where c1 and c2 are terms of sort CollectionSort and there ..... represent again stuff that we do not care about. What I want is to immediately desugar it to f(.....c1 @ _ @ c2.....).

Examples:

rule halt... => .

desugares to

rule halt ~> _ => .

syntax Exps ::= List{Exp}

syntax Bool ::= Exp "in Exps [function]

rule E in ...E... => true

desugares to

rule E in ,E, => true

syntax Bool ::= palindrome(Exps)

rule palindrome((E => .) ... (E => .))

desugares to

rule palindrome((E => .), _, (E => .))

You want more? :)

Grigore

From: Radu Mereuta [[email protected]]
Sent: Friday, September 20, 2013 12:18 PM
To: Rosu, Grigore
Cc: [email protected]
Subject: Re: [k-list] on ... in rules

Ok, my complaint is:

Can you be more specific? I don't really understand what you want me to do. I have a hint, but I want the full extent.
Providing more examples to emphasize what you mean by collection would be great. When I think of a collection I have quite a few variants in mind, all derived from the SDF grammar and the KIL classes, but somehow I think that those don't fully apply to your scenarios.

Radu

On Fri, Sep 20, 2013 at 6:26 PM, Rosu, Grigore [email protected] wrote:

How difficult would it be to simply allow ... anywhere a collection is expected? Many people ask that and they get confused when they see that we do not support ... everywhere.

Suppose that we have an operation/constuct f which expects a collection sort as argument (i.e., list, set, map, etc.). Also, suppose that the construct of the collection is "@" (could be whitespace, or comma, or ~>, or anything user defined using List{Sort}{"@"}). Then what I think we should do in the frontend is to automatically convert

f(stuff1...stuff2)

into

f(stuff1 @ _:CollectionSort @ stuff2)

In particular, I'd also like to write the semantics of halt this way:

rule halt... => .

In every single iteration of cs422 students asked me why not write it like above instead of

rule halt ~> _ => .

So? Radu, your turn, please complain :-)

Grigore

k-list mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/k-list

k-list mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/k-list

module TEST

rule A:KItem ::Int ~> A ::Int => .

endmodule

This should compile no problem, but instead it gives the following error:

[Error] Critical: Variable 'A' declared with two different sorts: Int and KItem
File: /home/dguth2/ktest/test.k
Location: (3,23,3,24)
Compilation Phase: Variable type inference

I need this fixed right away so I can tag a release of the K framework that the Python semantics works with.

I need the following rule to compile:

rule MyListItem(1) (MyListItem(3) => .MyList) _:MyList

It currently gives me an assertion error because it finds a ListUpdate in the base terms and it expects either an empty base terms or a variable.

Since we often test new functionalities of kompile or krun, such as a new parser, which can be activated using command line arguments to these tool, it would be nice to allow ktest to be passed these options without having to modify each test entry in the config.xml. So to have a way to list these options at the beginning of the config.xml file. Or even better, to allow them as command line arguments to ktest, so one would not even need to modify config.xml.

We already allow users to pass default values for attributes in config.xml, such as for programs, results, etc., so why not do the same for attributes such as "kompile-option" and "krun-option".

require "builtins/list.k"

module TEST
  imports LIST

  configuration <k> $PGM:K </k><l> .MyList </l>

  rule <l> .MyList (MyListItem(5) (L:MyList MyListItem(6))) => . </l>



endmodule

This should work. But instead I get:

Exception in thread "main" java.lang.AssertionError
at org.kframework.kil.DataStructureBuiltin.of(DataStructureBuiltin.java:134)
at org.kframework.compile.utils.CompileDataStructures.transform(CompileDataStructures.java:122)
at org.kframework.kil.KApp.accept(KApp.java:148)
at org.kframework.compile.utils.CompileDataStructures.transform(CompileDataStructures.java:118)
at org.kframework.kil.KApp.accept(KApp.java:148)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:345)
at org.kframework.kil.Cell.accept(Cell.java:266)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:365)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:390)
at org.kframework.kil.Bag.accept(Bag.java:55)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:345)
at org.kframework.kil.Cell.accept(Cell.java:266)
at org.kframework.compile.utils.CompileDataStructures.transform(CompileDataStructures.java:56)
at org.kframework.kil.Rule.accept(Rule.java:68)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:75)
at org.kframework.kil.Module.accept(Module.java:136)
at org.kframework.kil.visitors.CopyOnWriteTransformer.transform(CopyOnWriteTransformer.java:42)
at org.kframework.kil.Definition.accept(Definition.java:121)
at org.kframework.compile.utils.CompilerTransformerStep.compile(CompilerTransformerStep.java:24)
at org.kframework.compile.utils.CompilerSteps.compile(CompilerSteps.java:37)
at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:296)
at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:252)
at org.kframework.main.Main.main(Main.java:68)

rule T => #if T ==K . #then . #else T::Int #fi

This rule kompiles to something that checks isInt. Radu?

Example:

module TEST-CONTEXT-WITH-LABEL
syntax KLabel ::= "'L" | "'A"
syntax KResult ::= "res" "(" Id ")"
context 'L(HOLE)
rule 'A(_) => res(String2Id("X"))
endmodule

program:
'L('A(.KList))

Expected:
'L(res)

Actual:
res ( X ) ~> 'L(HOLE)

K version: 3.2.1-141. Also 3.2.1-128.
See the directory in k/issues.

So it turns out my big problem was I wasn't running it on 32 bits. Which, you know, is rather embarassing. But in any event, I finally managed to run Python with the C parser, and it didn't crash. But it didn't work, either.

Here is what I got at first:

[Error] Critical: Parse error: Unexpected end of rule
File: /home/dguth2/k/dist/include/builtins/bool.k
Location: (23,7,23,7)

Turns out the problem here is that we are asking for rules to be a CondSentence1 and we get back a CondSentence. CondSentence1 doesn't include ensures so I am pretty sure that's wrong. So I changed it and moved forward and got this:

Colon{[pos-info,area-in-file("/home/dguth2/python-semantics/python-semantics-logic.k",area(1,8,1,9,8,1))]} <<< - unimplemented yet: org.kframework.kil.loader.JavaClassesFactory
Colon{[pos-info,area-in-file("/home/dguth2/python-semantics/python-semantics-logic.k",area(1,16,1,17,16,1))]} <<< - unimplemented yet: org.kframework.kil.loader.JavaClassesFactory
Colon{[pos-info,area-in-file("/home/dguth2/python-semantics/python-semantics-logic.k",area(1,8,1,9,8,1))]} <<< - unimplemented yet: org.kframework.kil.loader.JavaClassesFactory
Colon{[pos-info,area-in-file("/home/dguth2/python-semantics/python-semantics-logic.k",area(1,16,1,17,16,1))]} <<< - unimplemented yet: org.kframework.kil.loader.JavaClassesFactory
java.lang.NullPointerException
at org.kframework.kil.visitors.BasicVisitor.visit(BasicVisitor.java:595)
at org.kframework.kil.TermCons.accept(TermCons.java:144)
at org.kframework.kil.visitors.BasicVisitor.visit(BasicVisitor.java:585)
at org.kframework.kil.Rewrite.accept(Rewrite.java:98)
at org.kframework.kil.visitors.BasicVisitor.visit(BasicVisitor.java:268)
at org.kframework.kil.visitors.BasicVisitor.visit(BasicVisitor.java:277)
at org.kframework.kil.Ambiguity.accept(Ambiguity.java:48)
at org.kframework.kil.visitors.BasicVisitor.visit(BasicVisitor.java:114)
at org.kframework.kil.Sentence.accept(Sentence.java:105)
at org.kframework.parser.generator.ParseRulesFilter.transform(ParseRulesFilter.java:97)
at org.kframework.kil.StringSentence.accept(StringSentence.java:63)
at org.kframework.kil.visitors.BasicTransformer.transform(BasicTransformer.java:57)
at org.kframework.parser.generator.ParseRulesFilter.transform(ParseRulesFilter.java:80)
at org.kframework.kil.Module.accept(Module.java:136)
at org.kframework.kil.visitors.BasicTransformer.transform(BasicTransformer.java:39)
at org.kframework.kil.Definition.accept(Definition.java:121)
at org.kframework.parser.DefinitionLoader.parseDefinition(DefinitionLoader.java:241)
at org.kframework.parser.DefinitionLoader.loadDefinition(DefinitionLoader.java:90)
at org.kframework.kompile.KompileFrontEnd.genericCompile(KompileFrontEnd.java:284)
at org.kframework.kompile.KompileFrontEnd.kompile(KompileFrontEnd.java:252)
at org.kframework.main.Main.main(Main.java:68)

TermCons is trying to turn Colon into a term when it's a terminal, so it fails. I made a fix for this too. Now I get this:

[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: ExceptClauses ::= NeList{ExceptClause,""}
(list ( _:List ((ListItem((K:K : K2:K) ::KeyDatum) => .List)) )) _
2: Comps ::= List{Comp,""}
(list ( _:List ((ListItem((K:K : K2:K) ::KeyDatum) => .List)) )) _
File: /home/dguth2/python-semantics/python-semantics-common.k
Location: (219,64,219,109)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Comps ::= List{Comp,""}
(list ( _:List ((ListItem(K:K) => .List)) )) _
2: ExceptClauses ::= NeList{ExceptClause,""}
(list ( _:List ((ListItem(K:K) => .List)) )) _
File: /home/dguth2/python-semantics/python-semantics-common.k
Location: (224,64,224,92)
Compilation Phase: Ambiguity filter
[Error] Critical: Could not infer a unique sort for variable 'String'. Possible sorts: KLabel, Map, K
File: /home/dguth2/python-semantics/python-semantics-common.k
Location: (264,37,264,43)

All three of these seem to be the result of failing to prefer K syntax over user syntax. The third of these fails with an error because VariableTypeInferenceFilter is not designed to prune branches that fail from the ambiguity tree and proceed with what remains.

I also took the liberty of attempting to replace the code Radu had written with similar code that compiled under the latest version of SDF that Jurgen pointed us to on Github. We do not have a repository for the dependencies that I can commit to anymore so I can't check it in right now but if someone creates a dependencies repository on Github I can check it in, or I can email the code to anyone who requests it.

This was quite an involved task and used a decent amount of trial and error, but eventually I got something that parsed Python. This actually revealed some bugs in my definition in which I had failed to declare follow restrictions appropriately and only the fact that the old version of SDF had bugs limiting the full generality of the parse tree prevented the code from working improperly.

This eventually gave me an execution of kompile that was significantly slower than the Java parser. I haven't timed the two SglrJNI implementations side by side because they're not really comparable when they give different results, so it's possible Radu's code is fast and mine is slow for reasons we may eventually be able to debug. Or it's possible the old version of SGLR is faster. Or it's possible that they're both slow and the problem is that I have some rules with very large ambiguity trees that the Java parser handles more efficiently than the C parser. I'm not sure.

In any event, it still didn't compile, but it gave me this result:

[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: ExceptClauses ::= NeList{ExceptClause,""}
(list ( _:List ((ListItem((K:K : K2:K) ::KeyDatum) => .List)) )) _
2: Comps ::= List{Comp,""}
(list ( _:List ((ListItem((K:K : K2:K) ::KeyDatum) => .List)) )) _
File: /home/dguth2/python-semantics/python-semantics-common.k
Location: (219,64,219,109)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Comps ::= List{Comp,""}
(list ( _:List ((ListItem(K:K) => .List)) )) _
2: ExceptClauses ::= NeList{ExceptClause,""}
(list ( _:List ((ListItem(K:K) => .List)) )) _
File: /home/dguth2/python-semantics/python-semantics-common.k
Location: (224,64,224,92)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: AssignTargets ::= NeList{Target,"="}
([ Ts2:K ])= Ts:AssignTargets
2: AssignTargets ::= NeList{Target,"="}
([ Ts2:K ])= Ts:AssignTargets
File: /home/dguth2/python-semantics/python-semantics-assignment.k
Location: (11,52,11,78)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Stmt ::= "del" NeTargets
del ((HOLE . _:Id), _)
2: Stmt ::= "del" NeTargets
del ((HOLE . _:Id), _)
File: /home/dguth2/python-semantics/python-semantics-assignment.k
Location: (27,11,27,30)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Stmt ::= "del" NeTargets
del ((HOLE [ _:K ]), _)
2: Stmt ::= "del" NeTargets
del ((HOLE [ _:K ]), _)
File: /home/dguth2/python-semantics/python-semantics-assignment.k
Location: (28,11,28,29)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Stmt ::= "del" NeTargets
del ((K:K [ HOLE ]), _:K)
2: Stmt ::= "del" NeTargets
del ((K:K [ HOLE ]), _:K)
File: /home/dguth2/python-semantics/python-semantics-assignment.k
Location: (29,11,29,29)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Arguments ::= List{Argument,","}
O:Object, (Id2String ( X:Id ))
2: NeExps ::= NeList{Exp,","}
O:Object, (Id2String ( X:Id ))
File: /home/dguth2/python-semantics/python-semantics-attribute-ref.k
Location: (17,55,17,70)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1:
.K => if (((((((((((((O:K is (ref ( "bool" )))) or ((O is (ref ( "NoneType" )
)))) or ((O is (ref ( "function" ))))) or ((O is (ref ( "slice" ))))) or ((
O is (ref ( "generator" ))))) or ((O is (ref ( "builtin-function" ))))) or
((O is (ref ( "builtin-method" ))))) or ((O is (ref ( "traceback" ))))) or
((O is (ref ( "code" ))))) or ((O is (ref ( "frame" ))))) or ((O is (ref (
"method" ))))) or ((O is (ref ( "cell" ))))) : raiseInternal ( "TypeError"
, "type is not an acceptable base type" ) ~> if ((((gettype ( O )) is (ref
( "type" )))) or (bool ( (hasbase ( Winner:K , (gettype ( O )) )) ))) :
pass else : (test ( (hasbase ( (gettype ( O )) , Winner )) , (setWinner ( (
gettype ( O )) )) , (raiseInternal ( "TypeError" ,
"metaclass conflict: the metaclass of a derived class must be a (non-strict) subclass of the metaclasses of all its bases"
)) ))
2:
.K => if (((((((((((((O:K is (ref ( "bool" )))) or ((O is (ref ( "NoneType" )
)))) or ((O is (ref ( "function" ))))) or ((O is (ref ( "slice" ))))) or ((
O is (ref ( "generator" ))))) or ((O is (ref ( "builtin-function" ))))) or
((O is (ref ( "builtin-method" ))))) or ((O is (ref ( "traceback" ))))) or
((O is (ref ( "code" ))))) or ((O is (ref ( "frame" ))))) or ((O is (ref (
"method" ))))) or ((O is (ref ( "cell" ))))) : (raiseInternal ( "TypeError"
, "type is not an acceptable base type" )) ~> if ((((gettype ( O )) is (
ref ( "type" )))) or (bool ( (hasbase ( Winner:K , (gettype ( O )) )) ))) :
pass else : (test ( (hasbase ( (gettype ( O )) , Winner )) , (setWinner (
(gettype ( O )) )) , (raiseInternal ( "TypeError" ,
"metaclass conflict: the metaclass of a derived class must be a (non-strict) subclass of the metaclasses of all its bases"
)) ))
File: /home/dguth2/python-semantics/python-semantics-classes.k
Location: (54,9,54,655)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1:
"class" |-> #if IsMethod:Bool #then (ref ( "builtin-method" )) #else (ref
( "builtin-function" )) #fi
2:
"class" |-> #if IsMethod:Bool #then (ref ( "builtin-method" )) #else (ref
( "builtin-function" )) #fi
File: /home/dguth2/python-semantics/python-semantics-builtin-modules.k
Location: (139,81,139,171)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1:
"class" |-> #if IsMethod:K #then (ref ( "builtin-method" )) #else (ref (
"builtin-function" )) #fi
2:
"class" |-> #if IsMethod:K #then (ref ( "builtin-method" )) #else (ref (
"builtin-function" )) #fi
File: /home/dguth2/python-semantics/python-semantics-builtin-modules.k
Location: (151,81,151,171)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Exp ::= Exp "+" Exp
(tuple ( ((getref2 ( (ref ( Frame:Int )) , "f_cells" )) [ N:K ]) )) + (
makeClosure ( (list ( L:List )) ))
2: Exp ::= Exp "+" Exp
(tuple ( ((getref2 ( (ref ( Frame:Int )) , "f_cells" )) [ N:K ]) )) + (
makeClosure ( (list ( L:List )) ))
File: /home/dguth2/python-semantics/python-semantics-functions.k
Location: (93,48,93,113)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Exps ::= List{Exp,","}
(#if (Ex:Exp ==K (ref ( "None" ))) #then (ref ( "None" )) #else (Ex . (
String2Id ( "class" ))) #fi), (Ex, (#if (Ex ==K (ref ( "None" ))) #then
(ref ( "None" )) #else (Ex . (String2Id ( "traceback" ))) #fi))
2: NeExps ::= NeList{Exp,","}
(#if (Ex:Exp ==K (ref ( "None" ))) #then (ref ( "None" )) #else (Ex . (
String2Id ( "class" ))) #fi), (Ex, (#if (Ex ==K (ref ( "None" ))) #then
(ref ( "None" )) #else (Ex . (String2Id ( "traceback" ))) #fi))
File: /home/dguth2/python-semantics/python-semantics-try.k
Location: (128,64,129,60)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1:
invokeBuiltin ( (obj ( "weakref.call" , _:Bag )) , ListItem(O:Object) ,
.Map ) => #if ((getattr ( O , "referent" )) =/=K .Obj) #then (ref ( (
getattr ( O , "referent" )) )) #else (ref ( "None" )) #fi
2:
invokeBuiltin ( (obj ( "weakref.call" , _:Bag )) , ListItem(O:Object) ,
.Map ) => #if ((getattr ( O , "referent" )) =/=K .Obj) #then (ref ( (
getattr ( O , "referent" )) )) #else (ref ( "None" )) #fi
File: /home/dguth2/python-semantics/python-semantics-garbage-collection.k
Location: (124,12,124,171)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Arguments ::= List{Argument,","}
(ref ( "sys" )), (ref ( "_imp" ))
2: NeExps ::= NeList{Exp,","}
(ref ( "sys" )), (ref ( "_imp" ))
File: /home/dguth2/python-semantics/python-semantics-import.k
Location: (15,182,15,205)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
Self:K, (ref ( "None" ))
2: Arguments ::= List{Argument,","}
Self:K, (ref ( "None" ))
File: /home/dguth2/python-semantics/python-semantics-io.k
Location: (77,95,77,112)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
Self:K, (ref ( "None" ))
2: Arguments ::= List{Argument,","}
Self:K, (ref ( "None" ))
File: /home/dguth2/python-semantics/python-semantics-io.k
Location: (85,97,85,114)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Arguments ::= List{Argument,","}
Name:Object, (strvalue ( Mode:K ))
2: NeExps ::= NeList{Exp,","}
Name:Object, (strvalue ( Mode:K ))
File: /home/dguth2/python-semantics/python-semantics-io.k
Location: (135,39,135,59)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: Arguments ::= List{Argument,","}
(O:K . (String2Id ( "getitem" ))), ((ref ( "range" )) ( (* Indices:Object
) ))
2: NeExps ::= NeList{Exp,","}
(O:K . (String2Id ( "getitem" ))), ((ref ( "range" )) ( (* Indices:Object
) ))
File: /home/dguth2/python-semantics/python-semantics-slicing.k
Location: (22,55,22,108)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
O:Object, ((ref ( "None" )), -1)
2: Arguments ::= List{Argument,","}
O:Object, ((ref ( "None" )), -1)
File: /home/dguth2/python-semantics/python-semantics-strings.k
Location: (46,87,46,105)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
O:Object, (Sep:Object, -1)
2: Arguments ::= List{Argument,","}
O:Object, (Sep:Object, -1)
File: /home/dguth2/python-semantics/python-semantics-strings.k
Location: (47,108,47,118)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
O:Object, (substrString ( FieldName:K , 1 , (findCharsInString ( FieldName ,
".[" , 1 )) ))
2: Arguments ::= List{Argument,","}
O:Object, (substrString ( FieldName:K , 1 , (findCharsInString ( FieldName ,
".[" , 1 )) ))
File: /home/dguth2/python-semantics/python-semantics-strings.k
Location: (94,207,94,275)
Compilation Phase: Ambiguity filter
[Warning] Parser: Parsing ambiguity. Arbitrarily choosing the first.
1: NeExps ::= NeList{Exp,","}
(convertField ( O:Object , (substrString ( Field:K , (findCharsInString (
Field , ":!" , 0 )) , ((findCharsInString ( Field , ":!" , 0 )) +Int 3) ))
)), (substrString ( Field , ((findCharsInString ( Field , ":" , 0 )) +Int 1
) , (lengthString ( Field )) ))
2: Arguments ::= List{Argument,","}
(convertField ( O:Object , (substrString ( Field:K , (findCharsInString (
Field , ":!" , 0 )) , ((findCharsInString ( Field , ":!" , 0 )) +Int 3) ))
)), (substrString ( Field , ((findCharsInString ( Field , ":" , 0 )) +Int 1
) , (lengthString ( Field )) ))
File: /home/dguth2/python-semantics/python-semantics-strings.k
Location: (108,79,108,275)
Compilation Phase: Ambiguity filter
[Error] Compiler: Unbounded Variable Frame:K .
File: /home/dguth2/python-semantics/python-semantics-garbage-collection.k
Location: (80,67,80,72)
Compilation Phase: class org.kframework.compile.checks.CheckVariables
[Error] Compiler: Unbounded Variable C:Bag .
File: /home/dguth2/python-semantics/python-semantics-garbage-collection.k
Location: (70,217,70,218)
Compilation Phase: class org.kframework.compile.checks.CheckVariables
[Error] Compiler: Unbounded Variable K:K .
File: /home/dguth2/python-semantics/python-semantics-garbage-collection.k
Location: (58,88,58,89)
Compilation Phase: class org.kframework.compile.checks.CheckVariables

This includes some of the errors that I had before but also includes new errors that seem to be the result of AmbDuplicateFilter and TypeInferenceSupremumFilter not working correctly on the new kil classes. Why that may be I didn't investigate. The final errors I collected from multiple nondeterministic runs of the command (and I may not have all of them, either) and seem to result from certain variable terms not showing up in the list of variables found in the right-hand side of a rule. Again, why that is I don't know and I haven't investigated.

The good news out of all of this is that while there is still plenty of work left to be done, at no point did the C parser crash or fail to produce the correct data. Which means that all the work that really remains is to fix up the K framework to work with all the nuances and details.

Anyway, this concludes my expedition into the C parser. If you want any more research to be done on this, you will have to get either Radu or whoever will inherit my Python semantics to do it.

It would be good to have a unified README file at the top of the K tool distribution. I'm going to start working on that soon. In the K meeting, there were some proposals on how to possibly also invoke it, or parts of it, using a -longhelp option, or something similar. I can take care of the contents of the README file.

1. kompile simple-untyped
2. krun krun programs/diverse/sortings.simple
3. Type 1 Ctrl+Z
4. ps ux

Result: the process is still shown in the list.

This don't happen if we use Ctrl+C instead.

When ktest is recursively searching for programs under a directory, and a results directory is also given, it wasn't clear where the IO for a program should be found.
Some definitions have subdirectories matching the program directories, others have just one results folder with all the expected IO at the root. So, we decided in the K meeting that that's a reasonable default - first look in the corresponding subdirectory, then try the root.

fslwork$ krun
[Error] Critical: Could not find a compiled K definition. Please ensure that either a compiled K definition exists in the current directory with its default name, or that --k-definition or --compiled-def have been specified.

We agreed that all messages output to users will use up to 80 characters per line, to fit any terminals. For example, compile outputs this message:

fslwork$ kompile
[Error] Critical: You have to provide a file in order to compile!.
File: command line
Location: System file.

Actually, I'm not sure that these should be errors. We should simply output "usage" information. But no matter what, let's stick to 80 characters.

Using #symInt(n) gives compilation errors. Only expressions like #symInt(1) are supported. It would be nice to support id's inside #symInt(), like it was before the elimination of #Id. This would make symbolic execution results more readable.
How to reproduce:
kompile -v -symbolic simple-untyped
krun -cPC=true -cIN="ListItem(n)" programs/exceptions/exceptions_01.simple

Result:
Critical: Parse error: Syntax error near unexpected character ')'
File: ListItem(n)
Location: (1,11,1,11)

I think I found another bug that is related with name clashing with built-in names. Here's my first bug about this: runtimeverification/k#34

Now the problem is, this module:

module BUG

  syntax Stx ::= S(Stx, Stx, Stx) [strict(1), seqstrict(3, 2)]
               | "end"

  configuration
    <k> $PGM:Stx </k>

endmodule

fails to compile with the error:

➜  bug  kompile bug.k
[Error] Critical: Parse error: Syntax error near unexpected character ':'
        File: /home/omer/K/k/dist/include/builtins/string.k
        Location: (69,11,69,11)

but when I rename S nonterminal with, for example, Asdf, it compiles fine. This suggests to me that we have a name clash problem here. (though I couldn't find the name S used in string.k file -- maybe it's somewhere in Java parts?)

It would be nice to see what's going on when ktest executes. For example, to display a message each time a definition kompiles, or a PDF is generated, or programs are executed, etc. If that is too much text, then we may consider adding a -verbose option to ktest.

Although it is done similar to that of simple-untyped.

More precisely, the rule for reading is the following:

rule [scanner-nextInt]:

invokeImpl(
methodClosure(,,,,,, 'NoMethodBody(_))::methodType(sig(MethodName:Id, ),), _,
'ListWrap(.KList)
) => I :: int
...

ListItem(I:Int) => . ...
when
Id2String(MethodName) ==String "nextInt"
[read]

If i run a program taht should read two numbers and print them, It just hangs.

How to test it:

1. Download java semantics
2. cd java-semantics-semantics
3. chmod +x ../tools/*
4. kompile java
5. add ../tools to $PATH
6. kjrun.sh ../programs/01_smoke_tests/read.java

fslwork$ kompile --help

usage: help [-addTopCell] [-c | -doc | -latex | -m | -pdf | -xml] [-check
] [-def ] [-fastKast] [-h | -v | -version] [-html] [-k
] [-kexp] [-l ] [-lib ] [-loud] [-ml | -smt |
-symbolic | -symeq] [-nofile] [-nosmt] [-o ] [-sortCells]
[-step ] [-style ] [-supercool ] [-superheat ]
[-synmod ] [-transition ] [-unparse] [-w ]

Compiles the K definitions given as arguments.

...

I do not understand the usage information of compile above. It looks like we want people to type "help" followed by some options. There is no placeholder for the .k definition itself there. Also, the comment right after confuses me: "Compiles the K definitions given as arguments." So we can compile several definitions at the same time?

I thing the usage info of krun looks better:

fslwork$ krun --help
usage: krun [options]
...

People know what options mean, and we don't have to edit in two places when adding a new option.

Consider the following definition:

module TEST

syntax Foo ::= foo(Int, Int)

rule foo(A, B) => A +Int B

endmodule

kompiling this definition and running:

krun --backend java-symbolic --no-smt -cPGM="foo(1, 2)"

Should rewrite to 3. Instead, it throws an AssertionError because Method.invoke failed with an argument type mismatch. If you check the type of the arguments you will see that they are 1-element KSequences instead of IntTokens.

Trying to exclude the test fixed by
120a528
I made a change

 <test definition="tests/regression/java-rewrite-engine/io/test2/test.k"
       extensions="test"
       programs="tests/regression/java-rewrite-engine/io/test2/programs"
+      exclude="tests/regression/java-rewrite-engine/io/test2/programs/readInt.test"
       results="tests/regression/java-rewrite-engine/io/test2/tests">
   <kompile-option name="-ml" />
   <all-programs>

which should have just set exclude="readInt.test". It would be nice if there was a warning for excludes that list a single program which doesn't actually exist.

The main idea of this issue is to create a flag to ktest that causes it to pass the specified options to every invocation of kompile or krun.
The suggestions for the option names are "--kompile-options" or "--krun-options".

Let us consider the following definition:

module TOK-SYNTAX

  syntax Exp ::= Id "(" Id ")"

endmodule

module TOK
  imports TOK-SYNTAX

  syntax Id ::= "a" | "b" | "c"

  rule a(b) => a(c)

  configuration <k> $PGM:Exp </k>
endmodule

If this is compiled and the executed on the program "a(b)" then the result is

<k>
    a ( b )
</k>

and not

<k>
    a ( c )
</k> 

as expected. The reason is given by the fact that the rules is compiled as

eq <_>_</_>(k, _~>_(_`(_`)('_`(_`), _`,`,_(_`(_`)('a, .KList), _`(_`)('b, .KList))), GeneratedFreshVar0:K), k) = 
<_>_</_>(k, _~>_(_`(_`)('_`(_`), _`,`,_(_`(_`)('a, .KList), _`(_`)('c, .KList))), GeneratedFreshVar0:K), k) 
[metadata "filename=(/Users/dlucanu/teste-temp-k/tokens/tok.k) location=(12,3,12,19) computational=()"] .

and the program is parsed as

_`(_`)('_`(_`), _`,`,_(_`(_`)(#token("Id", "a"), .KList), _`(_`)(#token("Id", "b"), .KList)))

Note that the Id constants have different representations: in the rule a labelled form and in the parsed program is a token.

If the syntax declaration

  syntax Id ::= "a" | "b" | "c"

is moved in the syntax module, then it works, but I am not sure that this the right solution.

Now there are several definitions broken (some of them belong to our collaborators from France) and it took me a while to figure out this behaviour.

I cannot see a clean solution now. May be we should discuss this in the next meeting.

For programs which may not terminate, or may take a lot of time, a -timeout option might be useful.

Kompiling the definition

module CV 

  syntax Id ::= "B"

endmodule

produces the following error:
$ kompile cv
[Error] Critical: Production "B" has not been imported in this module.
Defined in module: CV file: /Users/dlucanu/teste-temp-k/constvsvar/cv.k
File: /Users/dlucanu/k/dist/include/builtins/bool.k
Location: (26,16,26,17)

The row 26 in bool.k is
rule true andBool B:Bool => B:Bool

If I type

ktest -def simple-typed-static.k

everything is fine: the definition is kompiled and the PDF file is also generated and has the expected name and extension.

However, if I type

ktest -def simple-typed-static

(without the .k extension) then everything seems to work as well, except that the generated PDF has no .pdf extension. But it is a correct PDF file.

All you have to do is to make sure the generated PDF file always has the .pdf extension.

I am going to copy-paste the body of my email to the k list here so that it doesn't get lost. In short, we should use an arbitrary-precision binary floating point format (like Gnu MPFR) for the K framework.

So, I started thinking a little bit about what would be involved in providing high-quality floating-point support in the k framework (because our current support is very bad and the Java rewrite engine is an opportunity to improve it). Unfortunately, it turns out that the design I think is best is a somewhat involved project and I do not believe it would make sense for me to begin working on it at this time. However, I want to share my thoughts on this topic with the group because it is not necessarily immediately apparent what the correct design should be and so since I have given some thought to it I wanted to inform the group so that they can act accordingly when the time arrives to add this functionality.

Before I explain what I have in mind, I want to spend a little bit of time explaining the requirements as I see them of a floating-point library in the K framework.

1. The primary purpose of the Float type in the K framework should be to provide support suitable for giving semantics to those floating point operations implemented natively either as builtin functions (in an interpreted language like Python) or in hardware (as in a language like C). Thus, it should not provide functionality which is customarily implemented by libraries rather than a language specification itself.
2. Floating-point arithmetic across multiple programming languages has a variety of features. Some languages have infinity, -infinity, nan, and -0, others do not. Some languages have 32 bit floats, some have 64 bit floats, some have 80 bit floats, some have 128 bit floats, and many have some combination of these. Thus, the Float type in the K framework should not attempt to provide semantics to these types of concerns but instead provide a wide range of possible precisions and demand that the definer of the semantics implement language-specific details as they see fit (such as for example by checking the value of a multiplication for overflow and assigning a Infinity value).
3. Programming languages contain implementations of transcendental functions that are generally provided by an FPU unit on the processor. We want to provide semantics to these types of functions. Thus, we must provide a Float implementation that operates not only on precise values but also on approximations of various precisions.
4. Many, if not all, modern floating point types in programming languages are based on the IEEE 754 specification for floating point numbers to varying degrees of conformity. Thus, we must at the very least provide the basic pieces of functionality necessary to construct the semantics of such floating point numbers in the languages we define.

Taking all of these into consideration, what I propose is that we utilize for our floating-point implementation an arbitrary-precision binary (i.e. not base 10 but base 2 fractions) floating point format, and provide a number of hooks for dealing with precision, as well as the hooks for things like addition, multiplication, comparison, logarithms, trigonometry, etc. Obviously once I am gone you can all do your searches to attempt to decide what libraries to use precisely, but at an initial glance Gnu MPFR (http://www.mpfr.org/) seems more than suitable.

The main obstacle to this design decision, sadly, is that there is currently not any library containing Java bindings for the code, which is written in C. So it would be necessary to use JNI to insert this functionality into the framework. However, the advantage of this approach would be that providing JNI bindings for MPFR can be an open-source project independent of the K framework and potentially separately maintained in the long term.

Anyway, that's my thoughts on this matter. As I said, it doesn't seem like a project that would be worthwhile for me to begin working on at this time, but I wanted to explain what research I had done for those people who will pick up where I have left off.

There's still an issue about this on the Google Code issue tracker but I am making a new one here because I ran into something specific and I'm not sure if Radu is aware of it, because he's been working on the KItem thing and I don't know how far he's gotten.

Consider the following module:

module TEST

syntax KItem ::= close(Int)

endmodule

Run the command:

kast -e "close(5)"

This should work. But instead it says "Desired start symbol not found: K"

In ParseConfigsFilter and ParseRulesFilter there are calls to ss.getAttributes().containsAttribute("kore"). However, I believe that actually tests whether the attributes attached to ss themselves have the "kore" attribute attached to them rather than testing whether ss has the "kore" attribute attached to it.

Thus I think the following patch should be applied. If I have misunderstood something, let me know in the next 18 hours.

diff --git a/javasources/KTool/src/org/kframework/parser/generator/ParseConfigsFilter.java b/javasources/KTool/src/org/kframework/parser/generator/ParseConfigsFilter.java
index 0f39eff..b4e56d2 100644
--- a/javasources/KTool/src/org/kframework/parser/generator/ParseConfigsFilter.java
+++ b/javasources/KTool/src/org/kframework/parser/generator/ParseConfigsFilter.java
@@ -80,7 +80,7 @@ public class ParseConfigsFilter extends BasicTransformer {
                    ((Sentence) config).setAttributes(ss.getAttributes());
                } else {
                    String parsed = null;
-                   if (ss.getAttributes().containsAttribute("kore")) {
+                   if (ss.containsAttribute("kore")) {
                        Stopwatch sww = new Stopwatch();
                        parsed = org.kframework.parser.concrete.KParser.ParseKoreString(ss.getContent());
                        if (GlobalSettings.verbose)
diff --git a/javasources/KTool/src/org/kframework/parser/generator/ParseRulesFilter.java b/javasources/KTool/src/org/kframework/parser/generator/ParseRulesFilter.java
index 0ae08ff..1a3679a 100644
--- a/javasources/KTool/src/org/kframework/parser/generator/ParseRulesFilter.java
+++ b/javasources/KTool/src/org/kframework/parser/generator/ParseRulesFilter.java
@@ -112,7 +112,7 @@ public class ParseRulesFilter extends BasicTransformer {
                    ((Sentence) config).setAttributes(ss.getAttributes());
                } else {
                    String parsed = null;
-                   if (ss.getAttributes().containsAttribute("kore")) {
+                   if (ss.containsAttribute("kore")) {
                        Stopwatch sww = new Stopwatch();
                        parsed = org.kframework.parser.concrete.KParser.ParseKoreString(ss.getContent());
                        if (GlobalSettings.verbose)