Something with destructors

dafny-lang · Oct 14, 2024 · b22c4f3 · b22c4f3
1 parent b1c8883
commit b22c4f3
Show file tree

Hide file tree

Showing 2 changed files with 34 additions and 20 deletions.
diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs
@@ -18,6 +18,8 @@ public class SystemModuleManager {
  public readonly Dictionary<int, SubsetTypeDecl> TotalArrowTypeDecls = new(); // same keys as arrowTypeDecl
  readonly Dictionary<List<bool>, TupleTypeDecl> tupleTypeDecls = new(new Dafny.IEnumerableComparer<bool>());
 
+ public IEnumerable<TupleTypeDecl> TupleTypeDecls => tupleTypeDecls.Values;
+
  internal readonly ValuetypeDecl[] valuetypeDecls;
 
  /// <summary>

diff --git a/Source/DafnyCore/Backends/GhostEraser.cs b/Source/DafnyCore/Backends/GhostEraser.cs
@@ -52,7 +52,8 @@ public static void EraseGhostCode(Program program) {
  foreach (var topLevelDecl in compileModule.TopLevelDecls) {
  if (topLevelDecl is DatatypeDecl datatypeDecl) {
  foreach (var constructor in datatypeDecl.Ctors) {
- RemoveGhostParameters(program, symbolTable, constructor, constructor.Formals);
+ var removalLocations = RemoveGhostParameters(program, symbolTable, constructor, constructor.Formals);
+ RemoveElementsAtGhostPositions(constructor.Destructors, removalLocations);
  }
  }
  if (topLevelDecl is TopLevelDeclWithMembers withMembers) {
@@ -100,48 +101,59 @@ public static void EraseGhostCode(Program program) {
 
  }
 
- private static void RemoveGhostParameters(Program program, SymbolTable symbolTable, IHasNavigationToken member,
+ private static List<int> RemoveGhostParameters(Program program, SymbolTable symbolTable, IHasNavigationToken member,
  List<Formal> formals) {
- var references = symbolTable.GetReferences(member);
+ var removalLocations = new List<int>();
+ for (var index = formals.Count - 1; index >= 0; index--) {
+ var formal = formals[index];
+ if (formal.IsGhost) {
+ removalLocations.Add(index);
+ }
+ }
+
+ for (int i = formals.Count - 1; i >= 0; i--) {
+ if (formals[i].IsGhost) {
+ formals.RemoveAt(i);
+ }
+ }
+
+ RemoveGhostParameters(program, symbolTable, member, removalLocations);
+ return removalLocations;
+ }
 
+ private static void RemoveGhostParameters(Program program, SymbolTable symbolTable, IHasNavigationToken member, List<int> removalLocations)
+ {
+ var references = symbolTable.GetReferences(member);
  foreach (var reference in references) {
  if (reference is MatchCase matchCase) {
- RemoveElementsAtGhostPositions(matchCase.Arguments);
+ RemoveElementsAtGhostPositions(matchCase.Arguments, removalLocations);
  }
  if (reference is IdPattern idPattern) {
- RemoveElementsAtGhostPositions(idPattern.Arguments);
+ RemoveElementsAtGhostPositions(idPattern.Arguments, removalLocations);
  }
  if (reference is DatatypeValue datatypeValue) {
- RemoveElementsAtGhostPositions(datatypeValue.Arguments);
+ RemoveElementsAtGhostPositions(datatypeValue.Arguments, removalLocations);
  }
  if (reference is FunctionCallExpr functionCallExpr) {
- RemoveElementsAtGhostPositions(functionCallExpr.Args);
+ RemoveElementsAtGhostPositions(functionCallExpr.Args, removalLocations);
 
  }
  if (reference is MemberSelectExpr memberSelectExpr) {
  var applySuffix = program.FindNode<ApplySuffix>(memberSelectExpr.Tok.Uri, memberSelectExpr.Tok.ToDafnyPosition());
  if (applySuffix != null) {
  if (applySuffix.Lhs == memberSelectExpr) {
- RemoveElementsAtGhostPositions(applySuffix.Args);
+ RemoveElementsAtGhostPositions(applySuffix.Args, removalLocations);
  }
  }
  }
  }
 
- for (int i = formals.Count - 1; i >= 0; i--) {
- if (formals[i].IsGhost) {
- formals.RemoveAt(i);
- }
- }
-
  return;
 
- void RemoveElementsAtGhostPositions<T>(List<T> list) {
- for (int i = list.Count - 1; i >= 0; i--) {
- if (formals[i].IsGhost) {
- list.RemoveAt(i);
- }
- }
+ }
+ static void RemoveElementsAtGhostPositions<T>(List<T> list, List<int> removalLocations) {
+ foreach (var index in removalLocations) {
+ list.RemoveAt(index);
  }
  }
 }