diff --git a/k-distribution/tests/regression-new/checks/wideningMacro.k b/k-distribution/tests/regression-new/checks/wideningMacro.k new file mode 100644 index 00000000000..d9ed077394d --- /dev/null +++ b/k-distribution/tests/regression-new/checks/wideningMacro.k @@ -0,0 +1,9 @@ +// Copyright (c) K Team. All Rights Reserved. +module WIDENINGMACRO + imports INT + imports BOOL + + syntax Bool ::= #bar ( Int ) [alias] + + rule #bar ( X ) => X +endmodule diff --git a/k-distribution/tests/regression-new/checks/wideningMacro.k.out b/k-distribution/tests/regression-new/checks/wideningMacro.k.out new file mode 100644 index 00000000000..15be25e7c42 --- /dev/null +++ b/k-distribution/tests/regression-new/checks/wideningMacro.k.out @@ -0,0 +1,6 @@ +[Error] Inner Parser: Unexpected sort Int for term parsed as production syntax {Sort} Sort ::= Sort "=>" Sort [klabel(#KRewrite), symbol]. Expected: Bool + Source(wideningMacro.k) + Location(8,10,8,25) + 8 | rule #bar ( X ) => X + . ^~~~~~~~~~~~~~~ +[Error] Compiler: Had 1 parsing errors. diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java index b59833e0f61..215d7176d67 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java @@ -8,6 +8,7 @@ import org.kframework.attributes.Location; import org.kframework.builtin.KLabels; import org.kframework.builtin.Sorts; +import org.kframework.compile.ExpandMacros; import org.kframework.compile.ResolveAnonVar; import org.kframework.definition.Module; import org.kframework.definition.NonTerminal; @@ -385,7 +386,9 @@ private static Optional getFunction(Term t) { * @return */ private static boolean isFunction(Term t, boolean isAnywhere) { - return getFunction(t).map(pr -> pr.production().att()).orElse(Att()).contains(Att.FUNCTION()) || isAnywhere; + return isAnywhere || + getFunction(t).filter(pr -> pr.production().att().contains(Att.FUNCTION()) + || ExpandMacros.isMacro(pr.production())).isPresent(); } /**