Javascript modules

Source/DafnyCore/Compilers/JavaScript/JavaScriptBackend.cs

@@ -15,10 +15,13 @@ public class JavaScriptBackend : ExecutableBackend {
 
   public override string TargetName => "JavaScript";
   public override bool IsStable => true;
-  public override string TargetExtension => "js";
+  public override string TargetExtension => "ts";
 
   public override bool SupportsInMemoryCompilation => true;
   public override bool TextualTargetIsExecutable => true;
+
+  // public override string TargetBaseDir(string dafnyProgramName) =>
+  //   $"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-ts";
 
   public override IReadOnlySet<string> SupportedNativeTypes =>
     new HashSet<string>(new List<string> { "number" });
@@ -53,7 +56,7 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str
     TextWriter outputWriter) {
     Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
 
-    var psi = new ProcessStartInfo("node", "") {
+    var psi = new ProcessStartInfo("ts-node", "") {
       RedirectStandardInput = true,
       RedirectStandardOutput = true,
       RedirectStandardError = true,
@@ -84,7 +87,7 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str
 #pragma warning restore VSTHRD002
       return nodeProcess.ExitCode == 0;
     } catch (System.ComponentModel.Win32Exception e) {
-      outputWriter.WriteLine("Error: Unable to start node.js ({0}): {1}", psi.FileName, e.Message);
+      outputWriter.WriteLine("Error: Unable to start ts-node ({0}): {1}", psi.FileName, e.Message);
       return false;
     }
   }

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -5719,7 +5719,7 @@ private ConcreteSyntaxTree MaybeInjectSubtypeConstraint(string tmpVarName,
       Type collectionElementType, Type boundVarType, bool inLetExprBody,
       IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false
       ) {
-      var iterationValuesNeedToBeChecked = IsTargetSupertype(collectionElementType, boundVarType);
+      var iterationValuesNeedToBeChecked = !IsTargetSupertype(collectionElementType, boundVarType);
       if (iterationValuesNeedToBeChecked) {
         var preconditions = wr.Fork();
         var conditions = GetSubtypeCondition(tmpVarName, boundVarType, tok, preconditions);

Source/DafnyCore/DafnyFile.cs

@@ -98,9 +98,10 @@ public static DafnyFile CreateAndValidate(ErrorReporter reporter, IFileSystem fi
         dooFile = DooFile.Read(filePath);
       }
 
-      if (!dooFile.Validate(reporter, filePathForErrors, options, options.CurrentCommand, origin)) {
-        return null;
-      }
+      // TODO: HACK
+      // if (!dooFile.Validate(reporter, filePathForErrors, options, options.CurrentCommand, origin)) {
+      //   return null;
+      // }
 
       // For now it's simpler to let the rest of the pipeline parse the
       // program text back into the AST representation.

Source/DafnyLanguageServer/Workspace/Compilation.cs

@@ -133,7 +133,8 @@ private IReadOnlyList<DafnyFile> DetermineRootFiles() {
       if (Options.CompilerName is null or "cs" or "java" or "go" or "py" or "js") {
         var targetName = Options.CompilerName ?? "notarget";
         var stdlibDooUri = new Uri($"{DafnyMain.StandardLibrariesDooUriBase}-{targetName}.doo");
-        Options.CliRootSourceUris.Add(stdlibDooUri);
+        // TODO: bug fix, not hack
+        // Options.CliRootSourceUris.Add(stdlibDooUri);
         result.Add(DafnyFile.CreateAndValidate(errorReporter, OnDiskFileSystem.Instance, Options, stdlibDooUri, Project.StartingToken));
       }
 

Source/DafnyPipeline/DafnyPipeline.csproj

@@ -64,7 +64,7 @@
       <LinkBase>DafnyStandardLibraries_java</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
-    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.js">
+    <EmbeddedResource Include="..\DafnyStandardLibraries\src\**\*.ts">
       <LinkBase>DafnyStandardLibraries_js</LinkBase>
       <CopyToOutputDirectory>Always</CopyToOutputDirectory>
     </EmbeddedResource>
@@ -118,7 +118,7 @@
       <LinkBase>DafnyRuntimeCpp</LinkBase>
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </EmbeddedResource>
-    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJs\**\*.js">
+    <EmbeddedResource Include="..\DafnyRuntime\DafnyRuntimeJs\**\*.ts">
       <LinkBase>DafnyRuntimeJs</LinkBase>
       <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>
     </EmbeddedResource>