Merge pull request #369 from melt-umn/fix/reifyskolemwarnings

Error/warn on impossible reifications

grammars/silver/analysis/typechecking/core/BuiltInFunctions.sv

@@ -65,10 +65,33 @@ top::Expr ::= 'toString' '(' e1::Expr ')'
     else [err(top.location, "Operand to toString must be concrete types String, Integer, Float, or Boolean.  Instead it is of type " ++ prettyType(performSubstitution(e1.typerep, top.finalSubst)))];
 }
 
+function containsSkolem
+Boolean ::= ty::Type
+{
+  return case ty of
+         | skolemType(_) -> true
+         | nonterminalType(_, args) -> any(map(containsSkolem, args))
+         | decoratedType(ty) -> containsSkolem(ty)
+         | functionType(out, params, namedParams) -> containsSkolem(out) || any(map(containsSkolem, params)) || any(map((\x::NamedArgType -> containsSkolem(x.argType)), namedParams))
+         | _ -> false
+         end;
+}
+
 aspect production reifyFunctionLiteral
 top::Expr ::= 'reify'
 {
   top.upSubst = top.downSubst;
+
+  top.errors <-
+    case performSubstitution(top.typerep, top.finalSubst) of
+    | functionType(nonterminalType("core:Either", [stringType(), resultType]), [nonterminalType("core:reflect:AST", [])], []) ->
+       case resultType of
+       | skolemType(_) -> [err(top.location, "reify invocation attempts to reify to a skolem type - this will never succeed, see https://github.com/melt-umn/silver/issues/368")]
+       | ty when containsSkolem(ty) -> [wrn(top.location, "reify invocation attempts to reify to a type containing a skolem - this will only succeed in the case that the value does not actually contain an instance of the skolem type, see https://github.com/melt-umn/silver/issues/368")]
+       | _ -> []
+       end
+    | _ -> error("insane final type for reify implementation")
+    end;
 }
 
 aspect production newFunction

grammars/silver/definition/core/AGDcl.sv

@@ -64,6 +64,15 @@ top::AGDcl ::= h::AGDcl t::AGDcl
   top.errors <- warnIfMultJarName(h.jarName, t.jarName, top.location);
 }
 
+function makeAppendAGDclOfAGDcls
+AGDcl ::= dcls::AGDcls
+{
+  return case dcls of
+         | nilAGDcls(location=l) -> emptyAGDcl(location=l)
+         | consAGDcls(dcl, rest, location=l) -> appendAGDcl(dcl, makeAppendAGDclOfAGDcls(rest), location=l)
+         end;
+}
+
 abstract production jarNameDcl
 top::AGDcl ::= n::Name
 {

grammars/silver/extension/testing/WrongCode.sv

@@ -4,15 +4,22 @@ import silver:definition:core;
 import silver:definition:env;
 
 terminal WrongCode_kwd 'wrongCode' lexer classes {KEYWORD};
+terminal WarnCode_kwd 'warnCode' lexer classes {KEYWORD};
 terminal WrongFlowCode_kwd 'wrongFlowCode' lexer classes {KEYWORD};
 
+function containsMessage
+Boolean ::= text::String severity::Integer msgs::[Message]
+{
+  return any(map((\x::Message -> x.severity==severity && indexOf(text, x.output)!=-1), msgs));
+}
+
 concrete production wrongDecl
 top::AGDcl ::= 'wrongCode' s::String_t '{' ags::AGDcls '}'
 {
   top.unparse = "wrongCode" ++ s.lexeme ++ "{" ++ ags.unparse ++ "}";
 
   top.errors := 
-    if indexOf(substring(1, length(s.lexeme) - 1, s.lexeme), messagesToString(ags.errors)) == -1
+    if !containsMessage(substring(1, length(s.lexeme) - 1, s.lexeme), 2, ags.errors)
     then [err(top.location, "Wrong code did not raise an error containing " ++ s.lexeme ++ ". Bubbling up errors from lines " ++ toString($3.line) ++ " to " ++ toString($5.line))] ++ ags.errors
     else [];
 
@@ -22,13 +29,27 @@ top::AGDcl ::= 'wrongCode' s::String_t '{' ags::AGDcls '}'
   forwards to emptyAGDcl(location=top.location);
 }
 
+concrete production warnDecl
+top::AGDcl ::= 'warnCode' s::String_t '{' ags::AGDcls '}'
+{
+  top.unparse = "warnCode" ++ s.lexeme ++ "{" ++ ags.unparse ++ "}";
+
+  top.errors := 
+    if !containsMessage(substring(1, length(s.lexeme) - 1, s.lexeme), 1, ags.errors)
+    then [err(top.location, "Warn code did not raise a warning containing " ++ s.lexeme ++ ". Bubbling up errors from lines " ++ toString($3.line) ++ " to " ++ toString($5.line))] ++ ags.errors
+    else [];
+
+  forwards to makeAppendAGDclOfAGDcls(ags);
+  -- Forward to the decls so that we can use the stuff declared with warnings in other tests
+}
+
 concrete production wrongFlowDecl
 top::AGDcl ::= 'wrongFlowCode' s::String_t '{' ags::AGDcls '}'
 {
   top.unparse = "wrongFlowCode" ++ s.lexeme ++ "{" ++ ags.unparse ++ "}";
 
   top.errors := 
-    if indexOf(substring(1, length(s.lexeme) - 1, s.lexeme), messagesToString(ags.errors)) == -1
+    if !containsMessage(substring(1, length(s.lexeme) - 1, s.lexeme), 2, ags.errors)
     then [err(top.location, "Wrong code did not raise an error containing " ++ s.lexeme ++ ". Bubbling up errors from lines " ++ toString($3.line) ++ " to " ++ toString($5.line))] ++ ags.errors
     else [];
 

test/silver_features/Reflection.sv

@@ -173,20 +173,21 @@ equalityTest(reifyResToString(reify(anyAST(baz(anno2=_, anno1=_)))), "<OBJECT ::
 equalityTest(reifyResToString(reify(anyAST(baz(anno1=1, anno2=_)))), "<OBJECT :: (silver_features:Baz ::= Float)>", String, silver_tests);
 equalityTest(reifyResToString(reify(anyAST(baz(anno1=_, anno2=2.0)))), "<OBJECT :: (silver_features:Baz ::= Integer)>", String, silver_tests);
 
-function reifySkolem
-Either<String a> ::= x::AST
-{
-  return reify(x);
+wrongCode "skolem" {
+  function reifySkolem
+  Either<String a> ::= x::AST
+  {
+    return reify(x);
+  }
 }
 
--- This will have some sort of runtime type error involving skolems, but we can't test for it exactly since the exact message may vary.
-equalityTest(case reifySkolem(floatAST(4.0)) of left(_) -> true | right(_) -> false end, true, Boolean, silver_tests);
-
-function reifySkolem2
-Either<String (a ::= Integer)> ::= 
-{
-  local fn::(a ::= Integer) = \ i::Integer -> error(toString(i));
-  return reify(anyAST(fn));
+warnCode "skolem" {
+  function reifySkolem2
+  Either<String (a ::= Integer)> ::= 
+  {
+    local fn::(a ::= Integer) = \ i::Integer -> error(toString(i));
+    return reify(anyAST(fn));
+  }
 }
 
 equalityTest(case reifySkolem2() of left(_) -> false | right(_) -> true end, true, Boolean, silver_tests);