Disabled the feature, test almost working except for unused imports

Source/DafnyCore/Compilers/GoLang/Compiler-go.cs

@@ -3592,32 +3592,6 @@ protected class ClassWriter : IClassWriter {
  }
  }
 
- protected override ConcreteSyntaxTree EmitCoercionToNativeForm(Type from, IToken tok, ConcreteSyntaxTree wr) {
- // Don't expand! We want to distinguish string from seq<char> here
- from = from.Normalize();
- if (from is UserDefinedType udt && udt.Name == "string") {
- wr.Write('(');
- var w = wr.Fork();
- wr.Write(").String()");
- return w;
- } else {
- return wr;
- }
- }
-
- protected override ConcreteSyntaxTree EmitCoercionFromNativeForm(Type to, IToken tok, ConcreteSyntaxTree wr) {
- // Don't expand! We want to distinguish string from seq<char> here
- to = to.Normalize();
- if (to is UserDefinedType udt && udt.Name == "string") {
- wr.Write($"{HelperModulePrefix}SeqOfString(");
- var w = wr.Fork();
- wr.Write(")");
- return w;
- } else {
- return wr;
- }
- }
-
  protected override ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) {
  var w = wr.Fork();
  wr.Write(".(int)");

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -827,12 +827,6 @@ protected interface IClassWriter {
  return wr;
  }
 
- protected virtual ConcreteSyntaxTree EmitCoercionToNativeForm(Type/*?*/ from, IToken tok, ConcreteSyntaxTree wr) {
- return wr;
- }
- protected virtual ConcreteSyntaxTree EmitCoercionFromNativeForm(Type/*?*/ to, IToken tok, ConcreteSyntaxTree wr) {
- return wr;
- }
  protected virtual ConcreteSyntaxTree EmitCoercionToNativeInt(ConcreteSyntaxTree wr) {
  return wr;
  }
@@ -4450,9 +4444,6 @@ private class ArrayLvalueImpl : ILvalue {
  } else {
  type = instantiatedType;
  }
- if (s.Method.IsExtern(out _, out _)) {
- type = NativeForm(type);
- }
  outTypes.Add(type);
  outFormalTypes.Add(p.Type);
  outLhsTypes.Add(s.Lhs[i].Type);
@@ -4512,12 +4503,8 @@ private class ArrayLvalueImpl : ILvalue {
  var fromType = s.Args[i].Type;
  var toType = s.Method.Ins[i].Type;
  var instantiatedToType = toType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
- // Order of coercions is important here: EmitCoercionToNativeForm may coerce into a type we're unaware of, so it *has* to be last
  var w = EmitCoercionIfNecessary(fromType, toType, s.Tok, wr);
  w = EmitDowncastIfNecessary(fromType, instantiatedToType, s.Tok, w);
- if (s.Method.IsExtern(out _, out _)) {
- w = EmitCoercionToNativeForm(toType, s.Tok, w);
- }
  TrExpr(s.Args[i], w, false, wStmts);
  sep = ", ";
  }
@@ -4546,9 +4533,6 @@ private class ArrayLvalueImpl : ILvalue {
  // The type information here takes care both of implicit upcasts and
  // implicit downcasts from type parameters (see above).
  ConcreteSyntaxTree wRhs = EmitAssignment(lvalue, s.Lhs[j].Type, outTypes[l], wr, s.Tok);
- if (s.Method.IsExtern(out _, out _)) {
- wRhs = EmitCoercionFromNativeForm(p.Type, s.Tok, wRhs);
- }
  wRhs.Write(outTmps[l]);
  // Coercion from the out type to the LHS type is the responsibility
  // of the EmitAssignment above

Test/comp/GoModule.dfy

@@ -1,35 +1,46 @@
-// RUN: %dafny /compile:3 /spillTargetCode:2 "%s" /compileTarget:go > "%t"
+// RUN: %dafny /compile:3 /spillTargetCode:2 /unicodeChar:0 "%s" /compileTarget:go > "%t"
 // note: putting /compileTarget:go after "%s" overrides user-provided option
 // RUN: %diff "%s.expect" "%t"
 
-// "url" is a built-in package, so it should be accessible to the
-// test suite without further requirements on the setup.
-module {:extern "url", "net/url"} URL {
- class URL {
- var {:extern "Host"} host: string
- var {:extern "Path"} pathname: string
- var {:extern "RawQuery"} search: string
- }
+module Test {
 
- trait {:extern "", "error"} Error { }
+ import URL
+ import GoModuleConversions
 
- method {:extern "url", "Parse"} Parse(address: string) returns (url: URL, error: Error?)
-}
-
-method TryUrl(address: string) {
- var u, e := URL.Parse(address);
+ method TryUrl(address: string) {
+ var u, e := GoModuleConversions.Parse(address);
  if (e != null) {
-  print "Parse error: ", e, "\n";
+ print "Parse error: ", e, "\n";
  } else {
-  print "The address ", address, "\n";
-  print "has the following parts:\n";
-  print "host: ", u.host, "\n";
-  print "pathname: ", u.pathname, "\n";
-  print "search: ", u.search, "\n";
+ print "The address ", address, "\n";
+ print "has the following parts:\n";
+ print "host: ", u.host, "\n";
+ print "pathname: ", u.pathname, "\n";
+ print "search: ", u.search, "\n";
  }
-}
+ }
 
-method Main() {
+ method Main() {
  TryUrl("http:https://localhost:8080/default.htm?year=1915&month=august&day=29");
  TryUrl("http:https://localhost:8080/default.htm%");
+ }
 }
+
+// "url" is a built-in package, so it should be accessible to the
+// test suite without further requirements on the setup.
+module {:extern "url", "net/url"} URL {
+
+ class URL {
+ var {:extern "Host"} host: string
+ var {:extern "Path"} pathname: string
+ var {:extern "RawQuery"} search: string
+ }
+
+ trait {:extern "", "error"} Error { }
+}
+
+module {:extern "GoModuleConversions"} GoModuleConversions {
+ import opened URL
+ method {:extern "ParseURL"} Parse(address: string) returns (url: URL, error: Error?)
+}
+

Test/comp/GoModuleConversions.go

@@ -0,0 +1,11 @@
+package GoModuleConversions
+
+import (
+ "dafny"
+ url "net/url"
+)
+
+func ParseURL(dafnyAddress dafny.Sequence) (*url.URL, error) {
+ var address = dafny.SequenceVerbatimString(dafnyAddress, false);
+ return url.Parse(address)
+}