Support string type in the Rust backend (dafny-lang#4340)

Support string type in the Rust backend <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --- Stack created with [Sapling](https://sapling-scm.com). Best reviewed with [ReviewStack](https://reviewstack.dev/dafny-lang/dafny/pull/4340). * dafny-lang#4343 * dafny-lang#4341 * __->__ dafny-lang#4340
Dargones · Jul 27, 2023 · dcdf8b7 · dcdf8b7
1 parent 4116e55
commit dcdf8b7
Show file tree

Hide file tree

Showing 4 changed files with 664 additions and 529 deletions.
diff --git a/Source/DafnyCore/Compilers/Dafny/AST.dfy b/Source/DafnyCore/Compilers/Dafny/AST.dfy
@@ -5,7 +5,9 @@ module {:extern "DAST"} DAST {
 
   datatype Newtype = Newtype(name: string, base: Type)
 
-  datatype Type = Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) | Tuple(seq<Type>) | Passthrough(string) | TypeArg(Ident)
+  datatype Type = Path(seq<Ident>, typeArgs: seq<Type>, resolved: ResolvedType) | Tuple(seq<Type>) | Primitive(Primitive) | Passthrough(string) | TypeArg(Ident)
+
+  datatype Primitive = String | Bool
 
   datatype ResolvedType = Datatype(path: seq<Ident>) | Newtype
 

diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
@@ -201,11 +201,13 @@ private DAST.Type GenType(Type typ) {
       var xType = DatatypeWrapperEraser.SimplifyType(Options, typ);
 
       if (xType is BoolType) {
-        return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("bool"));
+        return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Bool());
       } else if (xType is IntType) {
         return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i32"));
       } else if (xType is RealType) {
         return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("f32"));
+      } else if (xType.IsStringType) {
+        return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_String());
       } else if (xType is UserDefinedType udt) {
         if (udt.ResolvedClass is TypeParameter tp) {
           if (thisContext != null && thisContext.ParentFormalTypeParametersToActuals.TryGetValue(tp, out var instantiatedTypeParameter)) {

diff --git a/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy
@@ -264,6 +264,12 @@ module {:extern "DCOMP"} DCOMP {
           s := s + ")";
         }
         case TypeArg(Ident(name)) => s := name;
+        case Primitive(p) => {
+          match p {
+            case String => s := "String";
+            case Bool => s := "bool";
+          }
+        }
         case Passthrough(v) => s := v;
       }
     }
@@ -530,7 +536,7 @@ module {:extern "DCOMP"} DCOMP {
         }
         case Literal(StringLiteral(l)) => {
           // TODO(shadaj): handle unicode properly
-          s := "\"" + l + "\"";
+          s := "\"" + l + "\".to_string()";
           isOwned := true;
         }
         case Ident(name) => {