liyili2
commented
10 years ago I wonder if you can try the new version of the K and see what is the output now without using smart option. I think the output can be parsed at least.
Closed seoseokje closed 10 years ago
liyili2
commented
10 years ago I wonder if you can try the new version of the K and see what is the output now without using smart option. I think the output can be parsed at least.
seoseokje
commented
10 years ago I really appreciate your attention.
I updated k-framework to the newest version and I run it without smart option. and It WORKS! I am really appreciated!
I have one question for you.
what is difference between default output and --output smart? Is there anything I should be aware of?
liyili2
commented
10 years ago output with smart option is supposed to print out a nice format with minimum parentheses, so that the output looks nicer. As you can see, the current output can be parsed but it looks ugly in some places. The output with smart option is supposed to solve the problem. However, this option is not fully developed yet. It can work in some semantics but not all. I think you can use the normal option in this few months.
seoseokje
commented
10 years ago I tried to compiled output with normal version and it was compiled. It seems normal mode is good for now. Thank you very much!
grosu
commented
10 years ago This is very good news! Can you please show us the new pretty printed code, just to take a look?
Great work, Liyi!
seoseokje
commented
10 years ago int dwmonitor ( double * X, double * D ) { double s121 ; double s620 ; double w119 ; double q418 ; double q317 ; double z116 ; double s5914 ; double s4813 ; double z7712 ; double z5611 ; int i54 ; double s710 ; double s59 ; double s48 ; double z77 ; double z56 ; double q3 ; double q4 ; double s1 ; double s4 ; double s5 ; double s6 ; double s7 ; double s8 ; double w1 ; int w2 ; int i5 ; int i3 ; double z1 ; double z5 ; double z7 ; s8 = X [ 0 ] ; for ( i5 = 0 ; (i5 < 2) ; i5 = (i5 + 2) ) { z5 = ((i5 == 0) ? 0.0 : s59) ; z7 = ((i5 == 0) ? 1.0 : s710) ; s4 = (z7 * D [ i5 ]) ; s5 = (z5 + s4) ; s7 = (z7 * s8) ; z56 = s5 ; z77 = s7 ; s48 = (z77 * D [ (i5 + 1) ]) ; s59 = (z56 + s48) ; s710 = (z77 * s8) ; } for ( i54 = 2 ; (i54 < 3) ; i54 = (i54 + 1) ) { z5611 = ((i54 == 0) ? 0.0 : s59) ; z7712 = ((i54 == 0) ? 1.0 : s710) ; s4813 = (z7712 * D [ i54 ]) ; s5914 = (z5611 + s4813) ; } for ( i3 = 0 ; (i3 < 2) ; i3 = (i3
this is the result I got from normal printing. This was good enough to compile. and I only need to remove .K at the end of it. I had to replace many part when I was using --output smart before.
Thank you!
grosu
commented
10 years ago Not bad! I think if we had a bit a whitespacing a la Maude's format attribute, then this code would actually look good for humans, too. There aren't too many parentheses. But the .K at the end does not make much sense. Why is it there, Liyi, do you know?
liyili2
commented
10 years ago Actually, I do not know. I tested the code in C and similar code in Simple. I found that the simple version was fine but the C code had problem. I think I take care of this in my pretty printer. I will not print out .K if a K term is not empty. From the output of the code, we can see that it actually prints out the .K. It means that the term is divided into two part before we get the result term for pretty printer. One part is the actual C program, it is a K term. However, there is another K term which is an empty K term. I do not know if the c-semantics will use a ml parser to parse all terms. If it is, I think the problem might be from there, OR it is from some backend.
On Thu, Feb 20, 2014 at 5:38 PM, Grigore Rosu notifications@github.comwrote:
Not bad! I think if we had a bit a whitespacing a la Maude's format attribute, then this code would actually look good for humans, too. There aren't too many parentheses. But the .K at the end does not make much sense. Why is it there, Liyi, do you know?
Reply to this email directly or view it on GitHubhttps://github.com/kframework/k/issues/236#issuecomment-35683165 .
I am trying to print with smart option so that I can compile with the result. However, I encountered GC limit exceeded error when the code is larger than certain length. (code with only declaration gave me the same error). With shorter code it worked well.
source code tested: test.c
result without --output smart
K_OPTS