Skip to content

Commit

Permalink
Ensure type inference checks rhsSort <: lhsSort for macro rules (#3666)
Browse files Browse the repository at this point in the history
Closes #3661
  • Loading branch information
Scott-Guest authored Sep 27, 2023
1 parent a26d8e1 commit bc1ffc5
Show file tree
Hide file tree
Showing 3 changed files with 19 additions and 1 deletion.
9 changes: 9 additions & 0 deletions k-distribution/tests/regression-new/checks/wideningMacro.k
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
@@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -385,7 +386,9 @@ private static Optional<ProductionReference> 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();
}

/**
Expand Down

0 comments on commit bc1ffc5

Please sign in to comment.