K-user mailing list

[Traian Florin Șerbănuță <traian.serbanuta AT info.uaic.ro>]

I would say this is a feature.

After the parsing phase, all syntactic sorts are collapsed into the K sort.

As you noticed, you can still use semantic casts, or predicates to
constrain the matching pattern;  however, we don't usually constrain
the resulting pattern to be valid syntactically.

Nevertheless, you could do that by adding isExpr(B + A) to the condition.

Is this satisfactory?
best wishes,
Traian


2013/4/5 Emmanuel Castro 
<emmanuel.castro AT laposte.net>:
> Transformation can produce syntactically invalid terms.
> Consider the K language below. It transforms a+b into b+a, without
> complaining but only a+b is syntactically valid.
>
> Is it a bug or is it a feature?
>
> Note:
> If Kompile was able to infer types from syntax, it would produce:
> rule A:A + B:B => B + A when isA(A)
> And it would end into a type error.
>
> -------------------
>
> module T
>
>   syntax Expr ::= A "+" B
>
>   syntax A ::= "a"
>   syntax B ::= "b"
>
>   rule A + B => B + A when isA(A)
>
>   configuration
>     <T>
>       <k> $PGM:Expr </k>
>     </T>
>
> endmodule
>
> _______________________________________________
> k-user mailing list
> k-user AT cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>