Cannot compute least sort of term (where the terms are lists)

user_1278288 0
Viewed 54

I have the following productions:

syntax Id
syntax Exp ::= Id
syntax Exps ::= List{Exp, ","}
syntax Ids ::= List{Id, ","}

What does this error mean?

[Error] Critical: Cannot compute least sort of term:
_,__KOOL-UNTYPED-SYNTAX(Id(#"x"),, .List{"_,__KOOL-UNTYPED-SYNTAX"}(.KList)).
Possible sorts are [Ids, Exps], but their least common subsort is
GeneratedListBottom{_,__KOOL-UNTYPED-SYNTAX}, which is not a possible sort.All
terms must have a unique least sort; consider assigning unique KLabels to
overloaded productions/completing the subsort lattice.
  while evaluating function project:Stmts
  while evaluating function initKCell
  while evaluating function initThreadCell
  while evaluating function initThreadsCell
  while evaluating function initTCell
kframework
1 Answers

K is not sure whether the term x, .List is an Ids or an Exps.

We want to tell K that:

  1. All Lists of Ids are Lists of Exps:

    syntax Exps ::= Ids

  2. Lists of Ids with the same elements as a list of Exps are the same. We tell K that Exps and Ids parse to the same AST node using the klabel attribute:

    syntax Exps ::= List{Exp, ","} [klabel(exps)]
syntax Ids ::= List{Id, ","} [klabel(exps)]
user_12782880
Related