Maude-help mailing list

[Steven Eker <steveneker AT gmail.com>]

The reason this is not a parse error is that Maude only enforces kind correctness, not sort correctness, at parse time. Sort correctness is enforced at runtime with expressions that don't sort check after rewriting going to the kind. The reason for this is that it's common to have expressions that don't sort check at parse time but do when instantiated at runtime. For example the integer exponentiation function ^ is only defined for Nat exponents  but in an equation you might want to give it an _expression_ that has sort Int so Maude gives you the benefit of the doubt. You might find the command

show kinds .

useful to see which sort is in which kind (or weakly connected component, in the subsort digraph).

Steven

On Thu, Dec 7, 2023 at 6:41 AM Raghu Ranganathan <rraghu.11502 AT gmail.com> wrote:

fmod LIST-OPS{X :: TRIV} is
  pr LIST*{X} .
  var A : X$Elt .
  var B : Nat .
  var C : List{X} .
   
  op index : List{X} Nat -> X$Elt .
  eq index(A,0) = head(A) .
  eq index(A,s B) = index(tail(A),B) .
endfm

fmod LIST-TEST is pr LIST-OPS{Nat} . endfm

This is the code i have, the strange portion is how A is of kind X$Elt but still is allowed to compile

as an argument in the equation for index. I am wondering how to detect these bugs when they happen.