Cooling of contexts does not apply

[grosu]

In SIMPLE static we need to have a rule of the form:

context ltype(HOLE:LValue)

The heating part seems to work, but the cooling not. The following gets stuck on the top of the k cell:

int ~> #freezerltype0 ( )

Type is a KResult, and everything work which does not make use of the context above.

What is stranger for me but potentially useful for you is that the following variant of the context works fine:

context ltype(HOLE) requires isLValue(HOLE)

However, this latter approach, as @andreistefanescu noted, throws an exception when I have more complex structure on LValue.

I'm assigning @andreistefanescu , but maybe @cos can also help. I'm stuck with SIMPLE typed because of that. I think @daejunpark is too with his KOOL typed.

[cos]

@grosu, I can have a look so @andreistefanescu can focus on FUN. In which branch are you working?

[grosu]

Thanks, @cos. I'm working in the master of my fork grosu/k, but I just made a PR with some fixes in simple untyped and i pushed simple-static as well. See right at the end of the file, where the LValue sort is defined and the ltype wrapper. I'm switching to simple dynamic in the meanwhile

[cos]

note: #2103 is a workaround, change when this is fixed

[cos]

@grosu, is the workaround good enough for now, or should I look at it this evening?

[grosu]

@cos, I don't have a workaround for that, do you? I would take any reasonable workaround right now.

[cos]

@grosu, I thought #2103 somehow made it work, but now I understand it's work-in-progress. I will look into it now.

[cos]

seems like the sort on the HOLE exposes some bug related to sorted variables that is not easy to track down. Either way, the side-condition requires isLValue(HOLE) gets generated so we can start directly from there.

However, this latter approach, as @andreistefanescu noted, throws an exception when I have more complex structure on LValue.

@andreistefanescu, what would be that more complex structure?

[grosu]

1. comment context ltype(HOLE:LValue) and uncomment context ltype(HOLE) requires isLValue(HOLE)
2. uncomment rule isLValue(_:Exp[_:Exps]) => true
3. kompile and then execute factorial.simple.

This is what I get, which I reported a few hours ago and @andreistefanescu said it was a problem with the membership predicates:

D:\github\grosu\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static>kompile simple-typed-static.k
D:\github\grosu\k\k-distribution\tutorial\2_languages\1_simple\2_typed\1_static>krun ..\programs\diverse\factorial.simple
[Error] Internal: Uncaught exception thrown of type
UnsupportedOperationException.
Please rerun your program with the --debug flag to generate a stack trace, and
file a bug report at https://github.com/kframework/k/issues

[grosu]

I've found a combination of the various options to do the same thing which seems to work:

// We would like to say the following instead of the predicate rule below:
  syntax LValue ::= Id | Exp "[" Exps "]"
// but unfortunately that currently generates some ambiguous parsings.
//  syntax LValue ::= Id
//  rule isLValue(_:Exp[_:Exps]) => true

  syntax Exp ::= ltype(Exp)
// We would like to say:
//  context ltype(HOLE:LValue)
// but we currently cannot type the HOLE
  context ltype(HOLE) requires isLValue(HOLE)

//  context ltype(HOLE:LValue)
  syntax Exp ::= LValue

[grosu]

@cos everything seems to work with simple static now. i'll do a few more sanity checks and then make a final PR. before I do that, it would be great if you can take care of #2098. Otherwise I have to modify all the .out files, and probably @daejunpark, too.