Merge branch 'supportAllOptionTypesInProjectFile' of github.com:keybo…

…ardDrummer/dafny into supportAllOptionTypesInProjectFile

.github/workflows/refman.yml

@@ -15,15 +15,14 @@ jobs:
  with:
  branch: master
 
- build:
+ build-refman:
  needs: check-deep-tests
  if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
  runs-on: ${{ matrix.os }}
  strategy:
  fail-fast: false
  matrix:
- os: [ macos-latest ]
- # os: [macos-latest, ubuntu-latest ]
+ os: [ ubuntu-latest ]
  steps:
  - name: OS
  run: echo ${{ runner.os }} ${{ matrix.os }}
@@ -41,28 +40,10 @@ jobs:
  - name: Install latex pandoc - Linux
  if: runner.os == 'Linux'
  run: |
- sudo apt-get install texlive texlive-xetex
- wget https://github.com/jgm/pandoc/releases/download/2.10.1/pandoc-2.10.1-1-amd64.deb
+ sudo apt-get install texlive-full
+ wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
  sudo dpkg -i *.deb
  rm -rf *.deb
- # apt-get has pandoc, but it is outdated
- - name: Extra linux packages
- if: matrix.os == 'ubuntu-latest'
- run: |
- sudo apt-get install texlive-science
- sudo tlmgr init-usertree
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
- pandoc -v
- which latex || echo NOT FOUND latex
- which xelatex || echo NOT FOUND xelatex
- sudo gem install rouge
- - if: matrix.os != 'ubuntu-latest' && runner.os == 'Linux'
- run: |
- sudo apt-get install texlive-math-extra
- sudo tlmgr init-usertree
- sudo tlmgr update --self
- sudo tlmgr install framed tcolorbox environ trimspaces unicode-math
  pandoc -v
  which latex || echo NOT FOUND latex
  which xelatex || echo NOT FOUND xelatex

Source/DafnyCore/AST/Members/Field.cs

@@ -9,14 +9,15 @@ public class Field : MemberDecl, ICanFormat, IHasDocstring, ISymbol {
  public readonly bool IsMutable; // says whether or not the field can ever change values
  public readonly bool IsUserMutable; // says whether or not code is allowed to assign to the field (IsUserMutable implies IsMutable)
  public PreType PreType;
- public readonly Type Type;
+
+ public readonly Type Type; // Might be null after parsing and set during resolution
  [ContractInvariantMethod]
  void ObjectInvariant() {
  Contract.Invariant(Type != null);
  Contract.Invariant(!IsUserMutable || IsMutable); // IsUserMutable ==> IsMutable
  }
 
- public override IEnumerable<INode> Children => Type.Nodes;
+ public override IEnumerable<INode> Children => Type?.Nodes ?? Enumerable.Empty<INode>();
 
  public Field(RangeToken rangeToken, Name name, bool isGhost, Type type, Attributes attributes)
  : this(rangeToken, name, false, isGhost, true, true, type, attributes) {

Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs

@@ -177,7 +177,8 @@ public LiteralModuleDecl(ModuleDefinition module, ModuleDefinition parent, Guid
 
  var bindings = ModuleDef.BindModuleNames(resolver, parentBindings);
  if (!parentBindings.BindName(Name, this, bindings)) {
- resolver.Reporter.Error(MessageSource.Resolver, tok, "Duplicate module name: {0}", Name);
+ parentBindings.TryLookup(Name, out var otherModule);
+ resolver.Reporter.Error(MessageSource.Resolver, new NestedToken(tok, otherModule.tok), "Duplicate module name: {0}", Name);
  }
  }
 

Source/DafnyCore/AST/Modules/ModuleBindings.cs

@@ -25,14 +25,14 @@ public class ModuleBindings {
  }
  }
 
- public bool TryLookup(IToken name, out ModuleDecl m) {
+ public bool TryLookup(string name, out ModuleDecl m) {
  Contract.Requires(name != null);
  return TryLookupFilter(name, out m, l => true);
  }
 
- public bool TryLookupFilter(IToken name, out ModuleDecl m, Func<ModuleDecl, bool> filter) {
+ public bool TryLookupFilter(string name, out ModuleDecl m, Func<ModuleDecl, bool> filter) {
  Contract.Requires(name != null);
- if (modules.TryGetValue(name.val, out m) && filter(m)) {
+ if (modules.TryGetValue(name, out m) && filter(m)) {
  return true;
  } else if (parent != null) {
  return parent.TryLookupFilter(name, out m, filter);
@@ -56,7 +56,7 @@ public class ModuleBindings {
  Contract.Assert(qid != null);
  IToken root = qid.Path[0].StartToken;
  result = null;
- bool res = TryLookupFilter(root, out result,
+ bool res = TryLookupFilter(root.val, out result,
  m => context != m && ((context.EnclosingModuleDefinition == m.EnclosingModuleDefinition && context.Exports.Count == 0) || m is LiteralModuleDecl));
  return res;
  }
@@ -72,7 +72,7 @@ public class ModuleBindings {
  Contract.Assert(qid != null);
  IToken root = qid.Path[0].StartToken;
  result = null;
- bool res = TryLookupFilter(root, out result,
+ bool res = TryLookupFilter(root.val, out result,
  m => context != m && ((context.EnclosingModuleDefinition == m.EnclosingModuleDefinition && context.Exports.Count == 0) || m is LiteralModuleDecl));
  return res;
  }
@@ -82,7 +82,7 @@ public class ModuleBindings {
  Contract.Assert(qid != null);
  IToken root = qid.Path[0].StartToken;
  result = null;
- bool res = TryLookupFilter(root, out result, m => m.EnclosingModuleDefinition != context);
+ bool res = TryLookupFilter(root.val, out result, m => m.EnclosingModuleDefinition != context);
  return res;
  }
 }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -646,7 +646,7 @@ public class AccessibleMember {
  // the add was successful
  } else {
  // there's already something with this name
- var yes = bindings.TryLookup(subDecl.tok, out var prevDecl);
+ var yes = bindings.TryLookup(subDecl.tok.val, out var prevDecl);
  Contract.Assert(yes);
  if (prevDecl is AbstractModuleDecl || prevDecl is AliasModuleDecl) {
  resolver.Reporter.Error(MessageSource.Resolver, subDecl.tok, "Duplicate name of import: {0}", subDecl.Name);

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -110,13 +110,26 @@ public UserDefinedType(Cloner cloner, UserDefinedType original)
  /// Return the upcast of "receiverType" that has base type "member.EnclosingClass".
  /// Assumes that "receiverType" normalizes to a UserDefinedFunction with a .ResolveClass that is a subtype
  /// of "member.EnclosingClass".
+ /// Preserves non-null-ness of "receiverType" if it is a non-null reference.
  /// Otherwise:
  /// Return "receiverType" (expanded).
  /// </summary>
  public static Type UpcastToMemberEnclosingType(Type receiverType, MemberDecl/*?*/ member) {
  Contract.Requires(receiverType != null);
  if (member != null && member.EnclosingClass != null && !(member.EnclosingClass is ValuetypeDecl)) {
- return receiverType.AsParentType(member.EnclosingClass);
+ var parentType = receiverType.AsParentType(member.EnclosingClass);
+
+ if (receiverType.IsNonNullRefType) {
+ if (parentType == null) {
+ return null;
+ } else if (parentType.ResolvedClass is ClassLikeDecl { IsReferenceTypeDecl: true }) {
+ return CreateNonNullType(parentType);
+ } else {
+ return parentType;
+ }
+ } else {
+ return parentType;
+ }
  }
  return receiverType.NormalizeExpandKeepConstraints();
  }

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -5,6 +5,7 @@ module {:extern "DAST"} DAST {
 
  datatype Type =
  Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) |
+ Nullable(Type) |
  Tuple(seq<Type>) |
  Array(element: Type) |
  Seq(element: Type) |
@@ -49,6 +50,8 @@ module {:extern "DAST"} DAST {
  Call(on: Expression, name: string, typeArgs: seq<Type>, args: seq<Expression>, outs: Optional<seq<Ident>>) |
  Return(expr: Expression) |
  EarlyReturn() |
+ TailRecursive(body: seq<Statement>) |
+ JumpTailCallStart() |
  Halt() |
  Print(Expression)
 

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -382,6 +382,12 @@ interface StatementContainer {
  return ret;
  }
 
+ public TailRecursiveBuilder TailRecursive() {
+ var ret = new TailRecursiveBuilder();
+ AddBuildable(ret);
+ return ret;
+ }
+
  public CallStmtBuilder Call() {
  var ret = new CallStmtBuilder();
  AddBuildable(ret);
@@ -640,6 +646,35 @@ class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement {
  }
  }
 
+ class TailRecursiveBuilder : StatementContainer, BuildableStatement {
+ readonly List<object> body = new();
+
+ public TailRecursiveBuilder() { }
+
+ public void AddStatement(DAST.Statement item) {
+ body.Add(item);
+ }
+
+ public void AddBuildable(BuildableStatement item) {
+ body.Add(item);
+ }
+
+ public List<object> ForkList() {
+ var ret = new List<object>();
+ this.body.Add(ret);
+ return ret;
+ }
+
+ public DAST.Statement Build() {
+ List<DAST.Statement> builtStatements = new();
+ StatementContainer.RecursivelyBuild(body, builtStatements);
+
+ return (DAST.Statement)DAST.Statement.create_TailRecursive(
+ Sequence<DAST.Statement>.FromArray(builtStatements.ToArray())
+ );
+ }
+ }
+
  class CallStmtBuilder : ExprContainer, BuildableStatement {
  object on = null;
  string name = null;

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -130,13 +130,29 @@ class DafnyCompiler : SinglePassCompiler {
  }
 
  protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
- if (from.AsSubsetType == null && to.AsSubsetType != null) {
+ if (from != null && to != null && from.IsNonNullRefType != to.IsNonNullRefType) {
+ if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
+ var nullConvert = stmt.Builder.Convert(GenType(from), GenType(to));
+
+ if (from is UserDefinedType fromUdt && fromUdt.ResolvedClass is NonNullTypeDecl fromNonNull) {
+ from = fromNonNull.RhsWithArgument(fromUdt.TypeArgs);
+ }
+
+ if (to is UserDefinedType toUdt && toUdt.ResolvedClass is NonNullTypeDecl toNonNull) {
+ to = toNonNull.RhsWithArgument(toUdt.TypeArgs);
+ }
+
+ return EmitCoercionIfNecessary(from, to, tok, new BuilderSyntaxTree<ExprContainer>(nullConvert));
+ } else {
+ return base.EmitCoercionIfNecessary(from, to, tok, wr);
+ }
+ } else if (from != null && to != null && from.AsSubsetType == null && to.AsSubsetType != null) {
  if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
  return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.Convert(GenType(from), GenType(to)));
  } else {
  return base.EmitCoercionIfNecessary(from, to, tok, wr);
  }
- } else if (from.AsSubsetType != null && to.AsSubsetType == null) {
+ } else if (from != null && to != null && from.AsSubsetType != null && to.AsSubsetType == null) {
  if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
  return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.Convert(GenType(from), GenType(to)));
  } else {
@@ -515,12 +531,27 @@ private class ClassWriter : IClassWriter {
  return type.ToString();
  }
 
+ protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntaxTree wr) {
+ var beforeReturnBlock = wr.Fork();
+ EmitReturn(m.Outs, wr);
+ return beforeReturnBlock;
+ }
+
  protected override ConcreteSyntaxTree EmitTailCallStructure(MemberDecl member, ConcreteSyntaxTree wr) {
- throw new NotImplementedException();
+ if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
+ var recBuilder = stmtContainer.Builder.TailRecursive();
+ return new BuilderSyntaxTree<StatementContainer>(recBuilder);
+ } else {
+ throw new InvalidOperationException();
+ }
  }
 
  protected override void EmitJumpToTailCallStart(ConcreteSyntaxTree wr) {
- throw new NotImplementedException();
+ if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
+ stmtContainer.Builder.AddStatement((DAST.Statement)DAST.Statement.create_JumpTailCallStart());
+ } else {
+ throw new InvalidOperationException();
+ }
  }
 
  internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok, MemberDecl/*?*/ member = null) {
@@ -701,8 +732,12 @@ private class ClassWriter : IClassWriter {
 
  protected override void TrCallStmt(CallStmt s, string receiverReplacement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wrStmts, ConcreteSyntaxTree wrStmtsAfterCall) {
  if (wr is BuilderSyntaxTree<StatementContainer> stmtContainer) {
- var callBuilder = stmtContainer.Builder.Call();
- base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree<ExprContainer>(callBuilder), wrStmts, wrStmtsAfterCall);
+ if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {
+ base.TrCallStmt(s, receiverReplacement, wr, wrStmts, wrStmtsAfterCall);
+ } else {
+ var callBuilder = stmtContainer.Builder.Call();
+ base.TrCallStmt(s, receiverReplacement, new BuilderSyntaxTree<ExprContainer>(callBuilder), wrStmts, wrStmtsAfterCall);
+ }
  } else {
  throw new InvalidOperationException("Cannot call statement in this context: " + currentBuilder);
  }
@@ -795,6 +830,10 @@ private class ExprLvalue : ILvalue {
  }
  }
 
+ protected override void EmitAssignment(string lhs, Type/*?*/ lhsType, string rhs, Type/*?*/ rhsType, ConcreteSyntaxTree wr) {
+ throw new InvalidOperationException("Cannot use stringified version of assignment");
+ }
+
  protected override ILvalue IdentLvalue(string var) {
  return new BuilderLvalue(var);
  }
@@ -1019,7 +1058,13 @@ private class ExprLvalue : ILvalue {
  ));
  break;
  case StaticReceiverExpr:
- throw new NotImplementedException();
+ if (e.Type.NormalizeExpandKeepConstraints() is UserDefinedType udt && udt.ResolvedClass is DatatypeDecl dt &&
+ DatatypeWrapperEraser.IsErasableDatatypeWrapper(Options, dt, out _)) {
+ baseExpr = (DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(udt.ResolvedClass));
+ } else {
+ baseExpr = (DAST.Expression)DAST.Expression.create_Companion(PathFromTopLevel(e.Type.AsTopLevelTypeWithMembers));
+ }
+ break;
  default:
  DAST.Type baseType;
  if (e.Type.AsNewtype != null) {
@@ -1152,11 +1197,11 @@ private class ExprLvalue : ILvalue {
  private DAST.Type TypeNameASTFromTopLevel(TopLevelDecl topLevel, List<Type> typeArgs) {
  var path = PathFromTopLevel(topLevel);
 
- // TODO(shadaj): do something with nullable references
- // bool nonNull = false;
+ bool nonNull = true;
  if (topLevel is NonNullTypeDecl non) {
- // nonNull = true;
  topLevel = non.Rhs.AsTopLevelTypeWithMembers;
+ } else if (topLevel is ClassLikeDecl) {
+ nonNull = false;
  }
 
  ResolvedType resolvedType;
@@ -1175,11 +1220,17 @@ private class ExprLvalue : ILvalue {
  throw new InvalidOperationException(topLevel.GetType().ToString());
  }
 
- return (DAST.Type)DAST.Type.create_Path(
+ DAST.Type baseType = (DAST.Type)DAST.Type.create_Path(
  path,
  Sequence<DAST.Type>.FromArray(typeArgs.Select(m => GenType(m)).ToArray()),
  resolvedType
  );
+
+ if (nonNull) {
+ return baseType;
+ } else {
+ return (DAST.Type)DAST.Type.create_Nullable(baseType);
+ }
  }
 
  public override ConcreteSyntaxTree Expr(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wStmts) {
@@ -1495,6 +1546,20 @@ private class ExprLvalue : ILvalue {
  }
  }
 
+ protected override void EmitLambdaApply(ConcreteSyntaxTree wr, out ConcreteSyntaxTree wLambda, out ConcreteSyntaxTree wArg) {
+ if (wr is BuilderSyntaxTree<StatementContainer> builder) {
+ var lambda = builder.Builder.Call();
+ wLambda = new BuilderSyntaxTree<ExprContainer>(lambda);
+ wArg = new BuilderSyntaxTree<ExprContainer>(lambda);
+ } else if (wr is BuilderSyntaxTree<ExprContainer> exprBuilder) {
+ var lambda = exprBuilder.Builder.Call();
+ wLambda = new BuilderSyntaxTree<ExprContainer>(lambda);
+ wArg = new BuilderSyntaxTree<ExprContainer>(lambda);
+ } else {
+ throw new InvalidOperationException();
+ }
+ }
+
  protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,
  ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts, out ConcreteSyntaxTree wrRhs, out ConcreteSyntaxTree wrBody) {
  if (wr is BuilderSyntaxTree<ExprContainer> builder) {