Error terms produced by function evaluations should stuck the execution

[dlucanu]

Consider the following definition:

module TEST
  syntax Val ::= Int
  syntax Exp ::= Id | Val
  syntax Stmt ::= 
       Exp "=" Exp ";" [strict(2)]
     | Stmt Stmt [right]

  configuration
    <k> $PGM:Stmt </k>
    <state> .Map </state> 

  syntax KResult ::= Val

  rule <k> X:Id => St[X] ...</k>
       <state> St </state>

  rule <k> X:Id = V:Val; => .K ...</k>
       <state> St => St[X <- f(V)] </state>

  rule S1:Stmt S2:Stmt => S1 ~> S2

  syntax Val ::= f(Val) [function]
  rule f(1) => 2
endmodule

Note that the function f is partially defined. If we execute with above definition the program (stored in "ex.test") x = 3; y = x; we get the following output:

$ krun ex.test 
<k>
    .K
</k>
<state>
    x |-> f ( 3 )
    y |-> f ( f ( 3 ) )
</state>

We see that the program was completely executed, even if the configuration includes error terms produced by the evaluation of f. IMHO, the execution should stuck after the first assignment because x |-> f ( 3 ) is not a legal term (as it happened in Maude backend).

[grosu]

@dlucanu do you see the same output both with the pattern-match and the unification backends? To be honest, I am not entirely sure what the behavior should be here, and not even why the Maude backend got stuck. @andreistefanescu ?

[dlucanu]

I am working only with the default backend. I do not know how to choose one of the two backends. The help message says only " is one of [coq|java]. Each creates the kompiled K definition." I guess that I saw a related message a time ago, but it is hard to find it, there are over 8000 messages sent on [k].

In Maude was easy because an unevaluated function term is not of sort Val (and hence not of sort KResult):

 $ krun ex.test 
<k>
    f ( 3 ) ~> y = HOLE ;
</k>
<state>
    x |-> f ( 3 )
</state>
Dorels-MacBook-Pro:test dlucanu$ krun ex.test -o raw
Maude> rewrites: 0 in 0ms cpu (0ms real) (0 rewrites/second)
result #Int: setCounter(0)
rewrites: 100 in 0ms cpu (0ms real) (396825 rewrites/second)
result BagItem: 
< generatedTop > 
 < k > 'f(# 3(.KList)) ~> #freezer '_=_;(#token("Id", "y")(.KList),,HOLE)(.KList) </ k > 
 < state > Map2KLabel (#token("Id", "x")(.KList) |-> 'f(# 3(.KList)))(.KList) </ state > </ generatedTop >
rewrites: 6 in 0ms cpu (0ms real) (166666 rewrites/second)
result #NzNat: 1
Maude> Bye.

The above was kompiled with Maude backend from August. I guess that earlier versions stopped immediately after the first assignment. @traiansf knows more about that.

IMHO, a configuration with unevaluated function terms is not well-typed.

[dwightguth]

Unfortunately the problem is that we would like to be able to throw an error if a function fails to evaluate, but we need to also support the possibility of a user writing a side condition which is intended to be evaluated in a short-circuited fashion. E.g.:

rule X:Foo => bar
requires isBar(X) andThenBool functionOnlyDefinedOnBars(X)

This requires some notion of strategies in order to achieve. We have simply not gotten to the point in the java rewrite engine where this is possible yet.