reveal.dfy test passes

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -620,7 +620,6 @@ class DeclModifierData {
  public bool IsOpaque;
  public IToken OpaqueToken;
  public IToken FirstToken;
-
  }
 
  private ModuleKindEnum GetModuleKind(DeclModifierData mods) {

Source/DafnyCore/AST/Members/Method.cs

@@ -29,6 +29,7 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  Concat(Req).Concat(Ens).Concat(Reads.Expressions).Concat(Mod.Expressions);
  public override IEnumerable<INode> PreResolveChildren => Children;
 
+ public bool IsBlind { get; set; }
  public override string WhatKind => "method";
  public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } }
  public readonly IToken SignatureEllipsis;
@@ -125,6 +126,7 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  this.Outs = original.Outs.ConvertAll(p => cloner.CloneFormal(p, false));
  }
 
+ this.IsBlind = original.IsBlind;
  this.Reads = cloner.CloneSpecFrameExpr(original.Reads);
  this.Mod = cloner.CloneSpecFrameExpr(original.Mod);
  this.Body = cloner.CloneMethodBody(original);
@@ -142,9 +144,11 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  [Captured] List<AttributedExpression> ens,
  [Captured] Specification<Expression> decreases,
  [Captured] BlockStmt body,
- Attributes attributes, IToken signatureEllipsis, bool isByMethod = false)
+ Attributes attributes, IToken signatureEllipsis, 
+ bool isByMethod = false, bool isBlind = false)
  : base(rangeToken, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null,
  typeArgs, ins, req, ens, decreases) {
+ this.IsBlind = isBlind;
  Contract.Requires(rangeToken != null);
  Contract.Requires(name != null);
  Contract.Requires(cce.NonNullElements(typeArgs));

Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs

@@ -8,8 +8,13 @@ public class RevealStmt : Statement, ICloneable<RevealStmt>, ICanFormat {
  public const string RevealLemmaPrefix = "reveal_";
 
  public readonly List<Expression> Exprs;
- [FilledInDuringResolution] public readonly List<AssertLabel> LabeledAsserts = new List<AssertLabel>(); // to indicate that "Expr" denotes a labeled assertion
- [FilledInDuringResolution] public readonly List<Statement> ResolvedStatements = new List<Statement>();
+ [FilledInDuringResolution] 
+ public readonly List<AssertLabel> LabeledAsserts = new(); // to indicate that "Expr" denotes a labeled assertion
+ [FilledInDuringResolution] 
+ public readonly List<Statement> ResolvedStatements = new();
+ [FilledInDuringResolution] public bool InBlindContext { get; private set; }
+ [FilledInDuringResolution] public List<MemberDecl> RevealedMembers = new();
+
 
  public override IEnumerable<Statement> SubStatements {
  get { return ResolvedStatements; }
@@ -54,51 +59,71 @@ public RevealStmt(RangeToken rangeToken, List<Expression> exprs)
  return formatter.SetIndentPrintRevealStmt(indentBefore, OwnedTokens);
  }
 
- public void ResolveRevealStmt(PreTypeResolver preTypeResolver, ResolutionContext resolutionContext)
+ public void Resolve(PreTypeResolver resolver, ResolutionContext resolutionContext)
  {
  foreach (var expr in Exprs) {
  var name = SingleName(expr);
- var labeledAssert = name == null ? null : preTypeResolver.DominatingStatementLabels.Find(name) as AssertLabel;
+ var labeledAssert = name == null ? null : resolver.DominatingStatementLabels.Find(name) as AssertLabel;
  if (labeledAssert != null) {
  LabeledAsserts.Add(labeledAssert);
  } else {
- var revealResolutionContext = resolutionContext with { InReveal = true };
- if (expr is ApplySuffix applySuffix) {
- var methodCallInfo = preTypeResolver.ResolveApplySuffix(applySuffix, revealResolutionContext, true);
- if (methodCallInfo == null) {
- // error has already been reported
- } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
- preTypeResolver.Reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
- } else if (methodCallInfo.Callee.AtLabel != null) {
- Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
- preTypeResolver.Reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
+ if (resolutionContext.InBlindMethod) {
+ InBlindContext = true;
+ if (expr is NameSegment or ExprDotName) {
+ if (expr is NameSegment) {
+ resolver.ResolveNameSegment((NameSegment)expr, true, null, resolutionContext, true);
+ } else {
+ resolver.ResolveDotSuffix((ExprDotName)expr, true, null, resolutionContext, true);
+ }
+ var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
+ if (callee == null) {
+ // error from resolving child
+ } else {
+ RevealedMembers.Add(callee.Member);
+ }
  } else {
- var call = new CallStmt(RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
- ResolvedStatements.Add(call);
- }
- } else if (expr is NameSegment or ExprDotName) {
- if (expr is NameSegment) {
- preTypeResolver.ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
- } else {
- preTypeResolver.ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
- }
- var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
- if (callee == null) {
- } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
- //The revealed member is a function
- preTypeResolver.ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
- } else {
- var call = new CallStmt(RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
- ResolvedStatements.Add(call);
+ resolver.Reporter.Error(MessageSource.Resolver, Tok, "can't use parenthesis when revealing");
  }
  } else {
- preTypeResolver.ResolveExpression(expr, revealResolutionContext);
+ var revealResolutionContext = resolutionContext with { InReveal = true };
+ if (expr is ApplySuffix applySuffix) {
+ var methodCallInfo = resolver.ResolveApplySuffix(applySuffix, revealResolutionContext, true);
+ if (methodCallInfo == null) {
+ // error has already been reported
+ } else if (methodCallInfo.Callee.Member is TwoStateLemma && !revealResolutionContext.IsTwoState) {
+ resolver.Reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "a two-state function can only be revealed in a two-state context");
+ } else if (methodCallInfo.Callee.AtLabel != null) {
+ Contract.Assert(methodCallInfo.Callee.Member is TwoStateLemma);
+ resolver.Reporter.Error(MessageSource.Resolver, methodCallInfo.Tok, "to reveal a two-state function, do not list any parameters or @-labels");
+ } else {
+ var call = new CallStmt(RangeToken, new List<Expression>(), methodCallInfo.Callee, methodCallInfo.ActualParameters);
+ ResolvedStatements.Add(call);
+ }
+ } else if (expr is NameSegment or ExprDotName) {
+ if (expr is NameSegment) {
+ resolver.ResolveNameSegment((NameSegment)expr, true, null, revealResolutionContext, true);
+ } else {
+ resolver.ResolveDotSuffix((ExprDotName)expr, true, null, revealResolutionContext, true);
+ }
+ var callee = (MemberSelectExpr)((ConcreteSyntaxExpression)expr).ResolvedExpression;
+ if (callee == null) {
+ } else if (callee.Member is Lemma or TwoStateLemma && Attributes.Contains(callee.Member.Attributes, "axiom")) {
+ //The revealed member is a function
+ resolver.ReportError(callee.tok, "to reveal a function ({0}), append parentheses", callee.Member.ToString().Substring(7));
+ } else {
+ // TODO what is this case about? Revealing a constant?
+ var call = new CallStmt(RangeToken, new List<Expression>(), callee, new List<ActualBinding>(), expr.tok);
+ ResolvedStatements.Add(call);
+ }
+ } else {
+ resolver.ResolveExpression(expr, revealResolutionContext);
+ } 
  }
  }
  }
 
  foreach (var a in ResolvedStatements) {
- preTypeResolver.ResolveStatement(a, resolutionContext);
+ resolver.ResolveStatement(a, resolutionContext);
  }
  }
 }

Source/DafnyCore/Dafny.atg

@@ -1172,11 +1172,13 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
  IToken tokenWithTrailingDocString = Token.NoToken;
  IToken bodyStart = Token.NoToken;
  IToken bodyEnd = Token.NoToken;
+ bool isBlind = false;
  AllowedDeclModifiers allowed = AllowedDeclModifiers.None;
  string caption = "";
  ExtremePredicate.KType kType = ExtremePredicate.KType.Unspecified;
  .)
  SYNC
+ [ "blind" ] (. isBlind = true; .)
  ( "method" (. isPlainOlMethod = true; caption = "method";
  CheckAndSetTokenOnce(ref dmod.FirstToken);
  allowed = AllowedDeclModifiers.Ghost | AllowedDeclModifiers.Static; .)
@@ -1253,7 +1255,10 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
  (. var range = new RangeToken(dmod.FirstToken, t);
  if (isConstructor) {
  m = new Constructor(range, hasName ? name : new Name(dmod.FirstToken.ToRange(), "_ctor"), dmod.IsGhost, typeArgs, ins,
- req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis);
+ req, new Specification<FrameExpression>(reads, readsAttrs), 
+ new Specification<FrameExpression>(mod, modAttrs), ens, 
+ new Specification<Expression>(dec, decAttrs), 
+ (DividedBlockStmt)body, attrs, signatureEllipsis);
  } else if (isLeastLemma) {
  m = new LeastLemma(range, name, dmod.IsStatic, kType, typeArgs, ins, outs,
  req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
@@ -1269,7 +1274,10 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
  ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
  } else {
  m = new Method(range, name, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs,
- req, new Specification<FrameExpression>(reads, readsAttrs), new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
+ req, new Specification<FrameExpression>(reads, readsAttrs), 
+ new Specification<FrameExpression>(mod, modAttrs), ens, 
+ new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis,
+ isBlind: isBlind);
  }
  m.BodyStartTok = bodyStart;
  m.TokenWithTrailingDocString = tokenWithTrailingDocString;

Source/DafnyCore/DafnyPrelude.bpl

@@ -99,7 +99,7 @@ function TagFamily(Ty): TyTagFamily;
 // ---------------------------------------------------------------
 // -- Literals ---------------------------------------------------
 // ---------------------------------------------------------------
-function {:identity} Lit<T>(x: T): T { x }
+revealed function {:identity} Lit<T>(x: T): T { x }
 axiom (forall<T> x: T :: { $Box(Lit(x)) } $Box(Lit(x)) == Lit($Box(x)) );
 
 // Specialize Lit to concrete types.

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -120,7 +120,7 @@ public partial class PreTypeResolver : INewOrOldResolver {
  } else if (stmt is RevealStmt)
  {
  var s = (RevealStmt)stmt;
- s.ResolveRevealStmt(this, resolutionContext);
+ s.Resolve(this, resolutionContext);
  } else if (stmt is BreakStmt) {
  var s = (BreakStmt)stmt;
  if (s.TargetLabel != null) {

Source/DafnyCore/Resolver/ResolutionContext.cs

@@ -1,7 +1,7 @@
 namespace Microsoft.Dafny;
 
 public record ResolutionContext(ICodeContext CodeContext, bool IsTwoState, bool InOld, bool InReveal,
- bool InFunctionPostcondition, bool InFirstPhaseConstructor) {
+ bool InFunctionPostcondition, bool InFirstPhaseConstructor, bool InBlindMethod) {
 
  // Invariants:
  // InOld implies !IsTwoState
@@ -10,13 +10,14 @@ public record ResolutionContext(ICodeContext CodeContext, bool IsTwoState, bool
  public bool IsGhost => CodeContext.IsGhost;
 
  public ResolutionContext(ICodeContext codeContext, bool isTwoState)
- : this(codeContext, isTwoState, false, false, false, false) {
+ : this(codeContext, isTwoState, false, false, false, false, false) {
  }
 
  /// <summary>
  /// Return a ResolutionContext appropriate for the body of "codeContext".
  /// </summary>
  public static ResolutionContext FromCodeContext(ICodeContext codeContext) {
+ var isBlind = codeContext is Method method && method.IsBlind;
  bool isTwoState;
  if (codeContext is NoContext || codeContext is DatatypeDecl || codeContext is ConstantField) {
  isTwoState = false;
@@ -25,7 +26,9 @@ public ResolutionContext(ICodeContext codeContext, bool isTwoState)
  } else {
  isTwoState = true;
  }
- return new ResolutionContext(codeContext, isTwoState);
+ return new ResolutionContext(codeContext, isTwoState) {
+ InBlindMethod = isBlind
+ };
  }
 
  public IMethodCodeContext AsMethodCodeContext => CodeContext as IMethodCodeContext;

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -786,7 +786,7 @@ enum BuiltinFunction {
 
  private void BplIfIf(Bpl.IToken tk, bool yes, Bpl.Expr guard, BoogieStmtListBuilder builder, Action<BoogieStmtListBuilder> k) {
  if (yes) {
- var newBuilder = new BoogieStmtListBuilder(builder.tran, options);
+ var newBuilder = new BoogieStmtListBuilder(builder.tran, options, builder.Context);
  k(newBuilder);
  builder.Add(new Bpl.IfCmd(tk, guard, newBuilder.Collect(tk), null, null));
  } else {