Progress towards blind functions

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -156,7 +156,13 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca
  }
 
  bool IsFunctionDecl() {
- switch (la.kind) {
+ var kind = la.kind;
+ return IsFunctionDecl(kind);
+ }
+
+ private bool IsFunctionDecl(int kind)
+ {
+ switch (kind) {
  case _function:
  case _predicate:
  case _copredicate:
@@ -618,6 +624,8 @@ class DeclModifierData {
  public bool IsStatic;
  public IToken StaticToken;
  public bool IsOpaque;
+ public bool IsBlind;
+ public IToken BlindToken;
  public IToken OpaqueToken;
  public IToken FirstToken;
  }

Source/DafnyCore/AST/Members/Function.cs

@@ -389,14 +389,15 @@ public enum CoCallClusterInvolvement {
 
  resolver.ResolveParameterDefaultValues(Ins, ResolutionContext.FromCodeContext(this));
 
+ var contractContext = new ResolutionContext(this, this is TwoStateFunction, false);
  foreach (var req in Req) {
- resolver.ResolveAttributes(req, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveAttributes(req, contractContext);
  Expression r = req.E;
- resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveExpression(r, contractContext);
  Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
  resolver.ConstrainTypeExprBool(r, "Precondition must be a boolean (got {0})");
  }
- resolver.ResolveAttributes(Reads, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveAttributes(Reads, contractContext);
  foreach (FrameExpression fr in Reads.Expressions) {
  resolver.ResolveFrameExpressionTopLevel(fr, FrameExpressionUse.Reads, this);
  }
@@ -407,16 +408,16 @@ public enum CoCallClusterInvolvement {
  }
  foreach (AttributedExpression e in Ens) {
  Expression r = e.E;
- resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateFunction));
- resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction) with { InFunctionPostcondition = true });
+ resolver.ResolveAttributes(e, contractContext);
+ resolver.ResolveExpression(r, contractContext with { InFunctionPostcondition = true });
  Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
  resolver.ConstrainTypeExprBool(r, "Postcondition must be a boolean (got {0})");
  }
  resolver.scope.PopMarker(); // function result name
 
- resolver.ResolveAttributes(Decreases, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveAttributes(Decreases, contractContext);
  foreach (Expression r in Decreases.Expressions) {
- resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveExpression(r, contractContext);
  // any type is fine
  }
  resolver.SolveAllTypeConstraints(); // solve type constraints in the specification
@@ -434,7 +435,7 @@ public enum CoCallClusterInvolvement {
  }
  }
  }
- resolver.ResolveExpression(Body, new ResolutionContext(this, this is TwoStateFunction));
+ resolver.ResolveExpression(Body, new ResolutionContext(this, this is TwoStateFunction, IsBlind));
  Contract.Assert(Body.Type != null); // follows from postcondition of ResolveExpression
  resolver.AddAssignableConstraint(tok, ResultType, Body.Type, "Function body type mismatch (expected {0}, got {1})");
  resolver.SolveAllTypeConstraints();
@@ -445,7 +446,7 @@ public enum CoCallClusterInvolvement {
  if (Result != null) {
  resolver.scope.Push(Result.Name, Result); // function return only visible in post-conditions (and in function attributes)
  }
- resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateFunction), true);
+ resolver.ResolveAttributes(this, contractContext, true);
  resolver.scope.PopMarker(); // function result name
 
  resolver.scope.PopMarker(); // formals

Source/DafnyCore/AST/Members/Method.cs

@@ -28,8 +28,6 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
  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;
@@ -126,7 +124,6 @@ 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);
@@ -145,10 +142,9 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  [Captured] Specification<Expression> decreases,
  [Captured] BlockStmt body,
  Attributes attributes, IToken signatureEllipsis, 
- bool isByMethod = false, bool isBlind = false)
+ bool isByMethod = 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));
@@ -287,29 +283,31 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  resolver.scope.Push(p.Name, p);
  }
 
- resolver.ResolveParameterDefaultValues(Ins, new ResolutionContext(this, this is TwoStateLemma));
+ var resolutionContext = new ResolutionContext(this, this is TwoStateLemma, IsBlind);
+ resolver.ResolveParameterDefaultValues(Ins, resolutionContext);
 
  // Start resolving specification...
  foreach (AttributedExpression e in Req) {
- resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateLemma));
- resolver.ResolveExpression(e.E, new ResolutionContext(this, this is TwoStateLemma));
+ resolver.ResolveAttributes(e, resolutionContext);
+ resolver.ResolveExpression(e.E, resolutionContext);
  Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
  resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})");
  }
 
- resolver.ResolveAttributes(Reads, new ResolutionContext(this, false));
+ var context = new ResolutionContext(this, false, IsBlind);
+ resolver.ResolveAttributes(Reads, context);
  foreach (FrameExpression fe in Reads.Expressions) {
  resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this);
  }
 
- resolver.ResolveAttributes(Mod, new ResolutionContext(this, false));
+ resolver.ResolveAttributes(Mod, context);
  foreach (FrameExpression fe in Mod.Expressions) {
  resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Modifies, this);
  }
 
- resolver.ResolveAttributes(Decreases, new ResolutionContext(this, false));
+ resolver.ResolveAttributes(Decreases, context);
  foreach (Expression e in Decreases.Expressions) {
- resolver.ResolveExpression(e, new ResolutionContext(this, this is TwoStateLemma));
+ resolver.ResolveExpression(e, resolutionContext);
  // any type is fine
  }
 
@@ -335,8 +333,9 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
 
  // ... continue resolving specification
  foreach (AttributedExpression e in Ens) {
- resolver.ResolveAttributes(e, new ResolutionContext(this, true));
- resolver.ResolveExpression(e.E, new ResolutionContext(this, true));
+ var ensuresContext = new ResolutionContext(this, true, false);
+ resolver.ResolveAttributes(e, ensuresContext);
+ resolver.ResolveExpression(e.E, ensuresContext);
  Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression
  resolver.ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})");
  }
@@ -370,7 +369,7 @@ public class Method : MethodOrFunction, TypeParameter.ParentType,
  }
 
  // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for greatest lemmas)
- resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateLemma), true);
+ resolver.ResolveAttributes(this, resolutionContext, true);
 
  resolver.Options.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value
  resolver.scope.PopMarker(); // for the out-parameters and outermost-level locals

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -13,7 +13,8 @@ public abstract class MethodOrFunction : MemberDecl {
  static MethodOrFunction() {
  DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError);
  }
-
+
+ public bool IsBlind { get; set; }
  public readonly List<TypeParameter> TypeArgs;
  public readonly List<AttributedExpression> Req;
  public readonly List<AttributedExpression> Ens;
@@ -39,6 +40,7 @@ public abstract class MethodOrFunction : MemberDecl {
  this.Decreases = cloner.CloneSpecExpr(original.Decreases);
  this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr);
  this.Ins = original.Ins.ConvertAll(p => cloner.CloneFormal(p, false));
+ IsBlind = original.IsBlind;
  }
 
  protected abstract bool Bodyless { get; }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -464,7 +464,7 @@ public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, IClonea
 
  resolver.scope.PushMarker();
  resolver.scope.AllowInstance = false;
- resolver.ResolveAttributes(this, new ResolutionContext(new NoContext(EnclosingModule), false), true); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members
+ resolver.ResolveAttributes(this, new ResolutionContext(new NoContext(EnclosingModule), false, false), true); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members
  resolver.scope.PopMarker();
 
  if (resolver.reporter.Count(ErrorLevel.Error) == prevErrorCount) {

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -61,7 +61,8 @@ public MatchFlattener(ErrorReporter reporter, FreshIdGenerator idGenerator)
  }
 
  if (node is ICallable callable) {
- resolutionContext = new ResolutionContext(callable, false);
+ // TODO investigate why the match flattener needs a resolution context.
+ resolutionContext = new ResolutionContext(callable, false, false);
  }
 
  if (node is NestedMatchStmt nestedMatchStmt) {

Source/DafnyCore/Dafny.atg

@@ -245,6 +245,7 @@ DeclModifier<ref DeclModifierData dmod>
  | "ghost" (. dmod.IsGhost = true; CheckAndSetToken(ref dmod.GhostToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .)
  | "static" (. dmod.IsStatic = true; CheckAndSetToken(ref dmod.StaticToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .)
  | "opaque" (. dmod.IsOpaque = true; CheckAndSetToken(ref dmod.OpaqueToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .)
+ | "blind" (. dmod.IsBlind = true; CheckAndSetToken(ref dmod.BlindToken); CheckAndSetTokenOnce(ref dmod.FirstToken); .)
  )
  .
 
@@ -1172,13 +1173,11 @@ 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; .)
@@ -1276,9 +1275,9 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
  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,
- isBlind: isBlind);
+ new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
  }
+ m.IsBlind = dmod.IsBlind;
  m.BodyStartTok = bodyStart;
  m.TokenWithTrailingDocString = tokenWithTrailingDocString;
  .)
@@ -1984,15 +1983,18 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  if (isTwoState && isPredicate) {
  Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
  f = new TwoStatePredicate(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result,
- reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
+ reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
+ new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
  } else if (isTwoState) {
  Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
  f = new TwoStateFunction(range, name, dmod.IsStatic, dmod.IsOpaque, typeArgs, formals, result, returnType,
- reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
+ reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
+ new Specification<Expression>(decreases, decAttrs), body, attrs, signatureEllipsis);
  } else if (isPredicate) {
  Contract.Assert(functionMethodToken == null || !dmod.IsGhost);
  f = new Predicate(range, name, dmod.IsStatic, isGhost, dmod.IsOpaque, typeArgs, formals, result,
- reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, new Specification<Expression>(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited,
+ reqs, new Specification<FrameExpression>(reads, readsAttrs), ens, 
+ new Specification<Expression>(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited,
  byMethodTok, byMethodBody, attrs, signatureEllipsis);
  } else if (isLeastPredicate) {
  Contract.Assert(functionMethodToken == null && !dmod.IsGhost);
@@ -2010,6 +2012,7 @@ FunctionDecl<DeclModifierData dmod, out Function/*!*/ f>
  byMethodTok, byMethodBody,
  attrs, signatureEllipsis);
  }
+ f.IsBlind = dmod.IsBlind;
  f.BodyStartTok = bodyStart;
  f.TokenWithTrailingDocString = tokenWithTrailingDocString;
  SystemModuleModifiers.Add(b => b.CreateArrowTypeDecl(formals.Count));

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -1308,7 +1308,7 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  }
  if (f.Body != null) {
  var prevErrorCount = ErrorCount;
- ResolveExpression(f.Body, new ResolutionContext(f, f is TwoStateFunction));
+ ResolveExpression(f.Body, new ResolutionContext(f, f is TwoStateFunction, f.IsBlind));
  AddSubtypeConstraint(Type2PreType(f.ResultType), f.Body.PreType, f.tok, "Function body type mismatch (expected {0}, got {1})");
  Constraints.SolveAllTypeConstraints($"body of {f.WhatKind} '{f.Name}'");
  }

Source/DafnyCore/Resolver/ResolutionContext.cs

@@ -9,8 +9,8 @@ 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, false) {
+ public ResolutionContext(ICodeContext codeContext, bool isTwoState, bool isBlind = false)
+ : this(codeContext, isTwoState, false, false, false, false, isBlind) {
  }
 
  /// <summary>