Enable AutoExtern to consume from multiple source files (#2292)

Source/AutoExtern.Test/Minimal/Library1.cs

@@ -0,0 +1,5 @@
+namespace NS;
+
+public interface Intf {
+  public string Prop { get; }
+}

Source/AutoExtern.Test/Minimal/Library.cs → Source/AutoExtern.Test/Minimal/Library2.cs

@@ -1,9 +1,5 @@
 namespace NS;
 
-public interface Intf {
-  public string Prop { get; }
-}
-
 public class Impl : Intf {
   public int Field;
   public string Prop => Field.ToString();

Source/AutoExtern.Test/Tests.cs

@@ -21,11 +21,12 @@ public void MinimalTest() {
     startInfo.ArgumentList.Add("../AutoExtern.dll");
 
     startInfo.ArgumentList.Add("Library.csproj"); // Project file
-    startInfo.ArgumentList.Add("Library.cs"); // Source file
     startInfo.ArgumentList.Add("NS"); // Namespace
     startInfo.ArgumentList.Add("Library.dfy.template"); // Template
     startInfo.ArgumentList.Add("CSharpModel.dfy"); // Target for CSharpModel.dfy
     startInfo.ArgumentList.Add("Library.dfy"); // Target file
+    startInfo.ArgumentList.Add("Library1.cs"); // Source file
+    startInfo.ArgumentList.Add("Library2.cs"); // Source file
 
     var dotnet = Process.Start(startInfo);
 

Source/AutoExtern.Test/Tutorial/ClientApp/Makefile

@@ -2,7 +2,8 @@ AutoExtern ?= dotnet run --project ../../../AutoExtern/AutoExtern.csproj --
 Dafny ?= dotnet run --project ../../../DafnyDriver/DafnyDriver.csproj --
 
 LibraryProjectFile := ../Library/Library.csproj
-LibrarySourceFile := ../Library/Library.cs
+LibrarySourceFile1 := ../Library/Library1.cs
+LibrarySourceFile2 := ../Library/Library2.cs
 LibraryRootNamespace := Library
 
 LibraryTemplateFile := LibraryModel.dfy.template
@@ -16,14 +17,15 @@ ExpectFile := $(AppDafnyFile).expect
 
 default: dotnet-run
 
-$(LibraryModelFile): $(LibraryProjectFile) $(LibrarySourceFile) $(LibraryTemplateFile)
+$(LibraryModelFile): $(LibraryProjectFile) $(LibrarySourceFile1) $(LibrarySourceFile2) $(LibraryTemplateFile)
 	$(AutoExtern) \
 		$(LibraryProjectFile) \
-		$(LibrarySourceFile) \
 		$(LibraryRootNamespace) \
 		$(LibraryTemplateFile) \
 		$(CSharpModelFile) \
-		$(LibraryModelFile)
+		$(LibraryModelFile) \
+		$(LibrarySourceFile1) \
+		$(LibrarySourceFile2)
 
 $(AppDafnyCSharpFile): $(AppDafnyFile)
 	$(Dafny) -compile:0 -noVerify -spillTargetCode:3 "$<"

Source/AutoExtern.Test/Tutorial/Library/Library1.cs

@@ -0,0 +1,21 @@
+namespace Library;
+
+public interface LinkedList<T> {
+  public int Length { get; }
+}
+
+public class Nil<T> : LinkedList<T> {
+  public int Length => 0;
+}
+
+public class Cons<T> : LinkedList<T> {
+  public T hd;
+  public LinkedList<T> tl;
+
+  public int Length => 1 + tl.Length;
+
+  public Cons(T hd, LinkedList<T> tl) {
+    this.hd = hd;
+    this.tl = tl;
+  }
+}

Source/AutoExtern.Test/Tutorial/Library/Library.cs → Source/AutoExtern.Test/Tutorial/Library/Library2.cs

@@ -1,25 +1,5 @@
 namespace Library;
 
-public interface LinkedList<T> {
-  public int Length { get; }
-}
-
-public class Nil<T> : LinkedList<T> {
-  public int Length => 0;
-}
-
-public class Cons<T> : LinkedList<T> {
-  public T hd;
-  public LinkedList<T> tl;
-
-  public int Length => 1 + tl.Length;
-
-  public Cons(T hd, LinkedList<T> tl) {
-    this.hd = hd;
-    this.tl = tl;
-  }
-}
-
 public class Entry<TItem> {
   public TItem item;
   public int count { get; set; }

Source/AutoExtern/Program.cs

@@ -124,7 +124,7 @@ public AST(SyntaxTree syntax, SemanticModel model) {
     this.model = model;
   }
 
-  public static AST FromFile(string projectPath, string filePath, string cSharpRootNS) {
+  public static IEnumerable<AST> FromFiles(string projectPath, IEnumerable<string> sourceFiles, string cSharpRootNS) {
     // https://github.com/dotnet/roslyn/issues/44586
     MSBuildLocator.RegisterDefaults();
     var workspace = Microsoft.CodeAnalysis.MSBuild.MSBuildWorkspace.Create();
@@ -141,10 +141,12 @@ public static AST FromFile(string projectPath, string filePath, string cSharpRoo
     }
 
     var compilation = project.GetCompilationAsync().Result!;
-    var fullPath = Path.GetFullPath(filePath);
-    var syntax = compilation.SyntaxTrees.First(st => Path.GetFullPath(st.FilePath) == fullPath);
-    var model = compilation.GetSemanticModel(syntax);
-    return new AST(syntax, new SemanticModel(cSharpRootNS, model));
+    return sourceFiles.Select(filePath => {
+      var fullPath = Path.GetFullPath(filePath);
+      var syntax = compilation.SyntaxTrees.First(st => Path.GetFullPath(st.FilePath) == fullPath);
+      var model = compilation.GetSemanticModel(syntax);
+      return new AST(syntax, new SemanticModel(cSharpRootNS, model));
+    });
   }
 
   private CompilationUnitSyntax Root => syntax.GetCompilationUnitRoot();
@@ -398,10 +400,16 @@ public static string ReadTemplate(string templatePath) {
     return template;
   }
 
-  public static string GenerateDafnyCode(string projectPath, string filePath, string cSharpRootNS) {
-    var ast = AST.FromFile(projectPath, filePath, cSharpRootNS);
+  public static string GenerateDafnyCode(string projectPath, IList<string> sourceFiles, string cSharpRootNS) {
     var wr = new StringWriter();
-    ast.Pp(wr, "");
+    var asts = AST.FromFiles(projectPath, sourceFiles, cSharpRootNS).ToList();
+    var last = asts.Last();
+    foreach (var ast in asts) {
+      ast.Pp(wr, "");
+      if (ast != last) {
+        wr.WriteLine();
+      }
+    }
     return wr.ToString();
   }
 
@@ -415,13 +423,14 @@ public static void CopyCSharpModel(string destPath) {
 
   public static void Main(string[] args) {
     if (args.Length < 6) {
-      Fail("Usage: AutoExtern {project.csproj} {file.cs} {Root.Namespace} {TemplateFile.dfy} {CSharpModel.dfy} {Output.dfy}");
+      Fail("Usage: AutoExtern {project.csproj} {Root.Namespace} {TemplateFile.dfy} {CSharpModel.dfy} {Output.dfy} {file.cs}*");
     }
 
-    var (projectPath, filePath, cSharpRootNS, templatePath, modelPath, outputPath) =
-      (args[0], args[1], args[2], args[3], args[4], args[5]);
+    var (projectPath, cSharpRootNS, templatePath, modelPath, outputPath) =
+      (args[0], args[1], args[2], args[3], args[4]);
+    var sourceFiles = args.Skip(5).ToList();
 
-    var dafnyCode = GenerateDafnyCode(projectPath, filePath, cSharpRootNS);
+    var dafnyCode = GenerateDafnyCode(projectPath, sourceFiles, cSharpRootNS);
     var template = ReadTemplate(templatePath);
     File.WriteAllText(outputPath, template.Replace(Placeholder, dafnyCode), Encoding.UTF8);