Merge branch 'json-merge-without-parameterized-subset-types' into jso…

…n-merge # Conflicts: # src/JSON/Tests.dfy
dafny-lang · May 4, 2023 · 79551df · 79551df
2 parents c35669c + 4287c0b
commit 79551df
Show file tree

Hide file tree

Showing 4 changed files with 22 additions and 19 deletions.
diff --git a/src/JSON/Deserializer.dfy b/src/JSON/Deserializer.dfy
@@ -68,10 +68,10 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
   }
 
   // TODO: Verify this function
-  function Unescape(str: seq<uint16>, start: nat := 0): DeserializationResult<seq<uint16>>
+  function {:tailrecursion} {:vcs_split_on_every_assert} Unescape(str: seq<uint16>, start: nat := 0, prefix: seq<uint16> := []): DeserializationResult<seq<uint16>>
     decreases |str| - start
   { // Assumes UTF-16 strings
-    if start >= |str| then Success([])
+    if start >= |str| then Success(prefix)
     else if str[start] == '\\' as uint16 then
       if |str| == start + 1 then
         Failure(EscapeAtEOS)
@@ -85,9 +85,8 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
             if exists c | c in code :: c !in HEX_TABLE_16 then
               Failure(UnsupportedEscape16(code))
             else
-              var tl :- Unescape(str, start + 6);
               var hd := ToNat16(code);
-              Success([hd])
+              Unescape(str, start + 6, prefix + [hd])
         else
           var unescaped: uint16 := match c
             case 0x22 => 0x22 as uint16 // \" => quotation mark
@@ -101,11 +100,9 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
           if unescaped as int == 0 then
             Failure(UnsupportedEscape16(str[start..start+2]))
           else
-            var tl :- Unescape(str, start + 2);
-            Success([unescaped] + tl)
+            Unescape(str, start + 2, prefix + [unescaped])
     else
-      var tl :- Unescape(str, start + 1);
-      Success([str[start]] + tl)
+      Unescape(str, start + 1, prefix + [str[start]])
   }
 
   function String(js: Grammar.jstring): DeserializationResult<string> {

diff --git a/src/JSON/Tests.dfy b/src/JSON/Tests.dfy
@@ -1,6 +1,9 @@
 // RUN: %run "%s" --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
 // RUN: %run "%s" --unicode-char:true --input ../Unicode/UnicodeStringsWithUnicodeChar.dfy
 
+// RUN: %run -t:java "%s" --unicode-char:false --input ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
+// RUN: %run -t:java "%s" --unicode-char:true --input ../Unicode/UnicodeStringsWithUnicodeChar.dfy
+
 include "Errors.dfy"
 include "API.dfy"
 include "ZeroCopy/API.dfy"

diff --git a/src/JSON/Utils/Parsers.dfy b/src/JSON/Utils/Parsers.dfy
@@ -13,9 +13,10 @@ module {:options "-functionSyntax:4"} JSON.Utils.Parsers {
 
   type SplitResult<+T, +R> = Result<Split<T>, CursorError<R>>
 
-  type Parser<!T, +R> = p: Parser_<T, R> | p.Valid?()
-      // BUG(https://github.com/dafny-lang/dafny/issues/2103)
-    witness ParserWitness<T, R>() // BUG(https://github.com/dafny-lang/dafny/issues/2175)
+  // BUG(https://github.com/dafny-lang/dafny/issues/3883)
+  // type Parser<!T, +R> = p: Parser_<T, R> | p.Valid?()
+  //     // BUG(https://github.com/dafny-lang/dafny/issues/2103)
+  //   witness ParserWitness<T, R>() // BUG(https://github.com/dafny-lang/dafny/issues/2175)
   datatype Parser_<!T, +R> = Parser(fn: FreshCursor -> SplitResult<T, R>,
                                     ghost spec: T -> bytes) {
     ghost predicate Valid?() {
@@ -48,8 +49,9 @@ module {:options "-functionSyntax:4"} JSON.Utils.Parsers {
       && (forall cs': FreshCursor | pre(cs') :: fn(cs').Success? ==> fn(cs').value.StrictlySplitFrom?(cs', spec))
     }
   }
-  type SubParser<!T, +R> = p: SubParser_<T, R> | p.Valid?()
-    witness SubParserWitness<T, R>() // BUG(https://github.com/dafny-lang/dafny/issues/2175)
+  // BUG(https://github.com/dafny-lang/dafny/issues/3883)
+  // type SubParser<!T, +R> = p: SubParser_<T, R> | p.Valid?()
+  //   witness SubParserWitness<T, R>() // BUG(https://github.com/dafny-lang/dafny/issues/2175)
 
   function {:opaque} SubParserWitness<T, R>(): (subp: SubParser_<T, R>)
     ensures subp.Valid?()

diff --git a/src/JSON/ZeroCopy/Deserializer.dfy b/src/JSON/ZeroCopy/Deserializer.dfy
@@ -24,8 +24,8 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
     type JSONError = Errors.DeserializationError
     type Error = CursorError<JSONError>
     type ParseResult<+T> = SplitResult<T, JSONError>
-    type Parser<!T> = Parsers.Parser<T, JSONError>
-    type SubParser<!T> = Parsers.SubParser<T, JSONError>
+    type Parser_<!T> = Parsers.Parser_<T, JSONError>
+    type SubParser_<!T> = Parsers.SubParser_<T, JSONError>
 
     // BUG(https://github.com/dafny-lang/dafny/issues/2179)
     const SpecView := (v: Vs.View) => Spec.View(v);
@@ -54,8 +54,9 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
       return Cursor(cs.s, cs.beg, point', cs.end).Split();
     }
 
-    function {:opaque} Structural<T>(cs: FreshCursor, parser: Parser<T>)
+    function {:opaque} Structural<T>(cs: FreshCursor, parser: Parser_<T>)
       : (pr: ParseResult<Structural<T>>)
+      requires parser.Valid?()
       requires forall cs :: parser.fn.requires(cs)
       ensures pr.Success? ==> pr.value.StrictlySplitFrom?(cs, st => Spec.Structural(st, parser.spec))
     {
@@ -77,8 +78,8 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
       SP(Grammar.Structural(before, val, after), cs)
     }
 
-    type ValueParser = sp: SubParser<Value> |
-        forall t :: sp.spec(t) == Spec.Value(t)
+    type ValueParser = sp: SubParser_<Value> |
+        sp.Valid?() && forall t :: sp.spec(t) == Spec.Value(t)
       witness *
   }
   type Error = Core.Error
@@ -151,7 +152,7 @@ module {:options "-functionSyntax:4"} JSON.ZeroCopy.Deserializer {
       Success(cs.Split())
     }
 
-    function {:opaque} BracketedFromParts(ghost cs: Cursor,
+    function {:opaque} {:vcs_split_on_every_assertion} BracketedFromParts(ghost cs: Cursor,
                                           open: Split<Structural<jopen>>,
                                           elems: Split<seq<TSuffixedElement>>,
                                           close: Split<Structural<jclose>>)