K Framework: Cannot convert to subtype

Question

I'm trying evaluate Expressions to Values (Exps ::= Values) for function calls.

Here's a simple example:

module ERL-SYNTAX

  imports INT-SYNTAX
  imports STRING
  syntax Atom ::= "main" | "f"
  syntax Exp ::=  Atom | Int
  syntax Exp ::= Exp "(" Exps ")"             [seqstrict]
  syntax Exps ::= List{Exp, ","}              [seqstrict]

endmodule

module ERL-CONFIGURATION

  imports ERL-SYNTAX
  imports MAP

  syntax Value ::=  Atom | Int | "{" Values "}"
  syntax Values ::= List{Value, ","}
  syntax Exp ::= Value
  syntax Exps ::= Values
  syntax KResult ::= Value
  syntax KResult ::= Values

  configuration <cfg color="yellow">
                  <k color="green"> $PGM:Exp </k>
                  <fundefs> //some default function definitions
                    .Map (f |-> 5 , .Exps 
                    main |-> f ( 2 , 3 , .Exps ) , .Exps )
                  </fundefs>
                </cfg>
endmodule

module ERL

  imports ERL-SYNTAX
  imports ERL-CONFIGURATION

  //rule .Exps => .Values
  rule <k>F:Atom(_:Values) =>  L ...</k>
       <fundefs>...  F |-> L ...</fundefs>

endmodule

This gets stuck at

.Exps ~> #freezer_(_)ERL-SYNTAX1 ( main )

So I tried with this rule: .Exps => .Values to evaluate main().

To me, the strange thing is that this time heating 3 is ok:

.Values ~> #freezer_,ERL-SYNTAX1 ( 3 ) ~> #freezer,_ERL-SYNTAX1 ( 2 ) ~> ...

will be

3 , .Values ~> #freezer_,_ERL-SYNTAX1 ( 2 ) ~> ..

but here it gets stuck again.

How should I approach this problem?

Answer 1

Put the productions for Exps and Vals in the same module and give them the same klabel attribute. This will make them overload one another, at which point in time, the fact that .Values is a KResult should solve your problem.