Rename JSON.AST to JSON.Values

src/JSON/API.dfy

@@ -8,31 +8,31 @@ include "ZeroCopy/API.dfy"
 module {:options "-functionSyntax:4"} JSON.API {
   import opened BoundedInts
   import opened Errors
-  import AST
+  import Values
   import Serializer
   import Deserializer
   import ZeroCopy = ZeroCopy.API
 
-  function {:opaque} Serialize(js: AST.JSON) : (bs: SerializationResult<seq<byte>>)
+  function {:opaque} Serialize(js: Values.JSON) : (bs: SerializationResult<seq<byte>>)
   {
     var js :- Serializer.JSON(js);
     ZeroCopy.Serialize(js)
   }
 
-  method SerializeAlloc(js: AST.JSON) returns (bs: SerializationResult<array<byte>>)
+  method SerializeAlloc(js: Values.JSON) returns (bs: SerializationResult<array<byte>>)
   {
     var js :- Serializer.JSON(js);
     bs := ZeroCopy.SerializeAlloc(js);
   }
 
-  method SerializeInto(js: AST.JSON, bs: array<byte>) returns (len: SerializationResult<uint32>)
+  method SerializeInto(js: Values.JSON, bs: array<byte>) returns (len: SerializationResult<uint32>)
     modifies bs
   {
     var js :- Serializer.JSON(js);
     len := ZeroCopy.SerializeInto(js, bs);
   }
 
-  function {:opaque} Deserialize(bs: seq<byte>) : (js: DeserializationResult<AST.JSON>)
+  function {:opaque} Deserialize(bs: seq<byte>) : (js: DeserializationResult<Values.JSON>)
   {
     var js :- ZeroCopy.Deserialize(bs);
     Deserializer.JSON(js)

src/JSON/Deserializer.dfy

@@ -1,9 +1,9 @@
 // RUN: %verify "%s" --unicode-char:false ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
 // RUN: %verify "%s" --unicode-char:true ../Unicode/UnicodeStringsWithUnicodeChar.dfy
 
-/// ===============================================
-///  Deserialization from JSON.Grammar to JSON.AST
-/// ===============================================
+/// ==================================================
+///  Deserialization from JSON.Grammar to JSON.Values
+/// ==================================================
 ///
 /// For the spec, see ``JSON.Spec.dfy``.
 
@@ -13,7 +13,7 @@ include "../BoundedInts.dfy"
 include "Utils/Views.dfy"
 include "Utils/Vectors.dfy"
 include "Errors.dfy"
-include "AST.dfy"
+include "Values.dfy"
 include "Grammar.dfy"
 include "Spec.dfy"
 
@@ -27,7 +27,7 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
   import opened Utils.Str
   import opened UnicodeStrings
 
-  import AST
+  import Values
   import Spec
   import opened Errors
   import opened Utils.Vectors
@@ -135,46 +135,46 @@ module {:options "-functionSyntax:4"} JSON.Deserializer {
     Success(if sign.Char?('-') then -n else n)
   }
 
-  function Number(js: Grammar.jnumber): DeserializationResult<AST.Decimal> {
+  function Number(js: Grammar.jnumber): DeserializationResult<Values.Decimal> {
     var JNumber(minus, num, frac, exp) := js;
     var n :-
       ToInt(minus, num);
     var e10 :- match exp
       case Empty => Success(0)
       case NonEmpty(JExp(_, sign, num)) => ToInt(sign, num);
     match frac
-    case Empty => Success(AST.Decimal(n, e10))
+    case Empty => Success(Values.Decimal(n, e10))
     case NonEmpty(JFrac(_, num)) =>
       var pow10 := num.Length() as int;
       var frac :- ToInt(minus, num);
-      Success(AST.Decimal(n * Pow(10, pow10) + frac, e10 - pow10))
+      Success(Values.Decimal(n * Pow(10, pow10) + frac, e10 - pow10))
   }
 
-  function KeyValue(js: Grammar.jKeyValue): DeserializationResult<(string, AST.JSON)> {
+  function KeyValue(js: Grammar.jKeyValue): DeserializationResult<(string, Values.JSON)> {
     var k :- String(js.k);
     var v :- Value(js.v);
     Success((k, v))
   }
 
-  function Object(js: Grammar.jobject): DeserializationResult<seq<(string, AST.JSON)>> {
+  function Object(js: Grammar.jobject): DeserializationResult<seq<(string, Values.JSON)>> {
     Seq.MapWithResult(d requires d in js.data => KeyValue(d.t), js.data)
   }
 
-  function Array(js: Grammar.jarray): DeserializationResult<seq<AST.JSON>> {
+  function Array(js: Grammar.jarray): DeserializationResult<seq<Values.JSON>> {
     Seq.MapWithResult(d requires d in js.data => Value(d.t), js.data)
   }
 
-  function Value(js: Grammar.Value): DeserializationResult<AST.JSON> {
+  function Value(js: Grammar.Value): DeserializationResult<Values.JSON> {
     match js
-    case Null(_) => Success(AST.Null())
-    case Bool(b) => Success(AST.Bool(Bool(b)))
-    case String(str) => var s :- String(str); Success(AST.String(s))
-    case Number(dec) => var n :- Number(dec); Success(AST.Number(n))
-    case Object(obj) => var o :- Object(obj); Success(AST.Object(o))
-    case Array(arr) => var a :- Array(arr); Success(AST.Array(a))
+    case Null(_) => Success(Values.Null())
+    case Bool(b) => Success(Values.Bool(Bool(b)))
+    case String(str) => var s :- String(str); Success(Values.String(s))
+    case Number(dec) => var n :- Number(dec); Success(Values.Number(n))
+    case Object(obj) => var o :- Object(obj); Success(Values.Object(o))
+    case Array(arr) => var a :- Array(arr); Success(Values.Array(a))
   }
 
-  function JSON(js: Grammar.JSON): DeserializationResult<AST.JSON> {
+  function JSON(js: Grammar.JSON): DeserializationResult<Values.JSON> {
     Value(js.t)
   }
 }

src/JSON/Grammar.dfy

@@ -4,7 +4,7 @@
 ///  Low-level JSON grammar (Concrete syntax)
 /// ==========================================
 ///
-/// See ``JSON.AST`` for the high-level interface.
+/// See ``JSON.Values`` for the high-level interface.
 
 include "../BoundedInts.dfy"
 include "Utils/Views.dfy"

src/JSON/README.md

@@ -6,13 +6,15 @@ This library provides two APIs:
 
 - A low-level (zero-copy) API that is efficient, verified (see [What is verified?](#what-is-verified) below for details) and allows incremental changes (re-serialization is much faster for unchanged objects), but is more cumbersome to use.  This API operates on concrete syntax trees that capture details of punctuation and blanks and represent strings using unescaped, undecoded utf-8 byte sequences.
 
-- A high-level API built on top of the previous one.  This API is more convenient to use, but it is unverified and less efficient. It produces abstract syntax trees that represent strings using Dafny's built-in `string` type.
+- A high-level API built on top of the previous one.  This API is more convenient to use, but it is unverified and less efficient. It produces abstract datatype value trees that represent strings using Dafny's built-in `string` type.
+
+Both APIs provides functions for serialization (JSON values to utf-8 bytes) and deserialization (utf-8 bytes to JSON values).
+See the Unicode module in `../Unicode` if you need to read or produce JSON text in other encodings.
 
-Both APIs provides functions for serialization (utf-8 bytes to AST) and deserialization (AST to utf-8 bytes).  Unverified transcoding functions are provided in `Utils/Unicode.dfy` if you need to read or produce JSON text in other encodings.
 
 ## Library usage
 
-The tutorial in [`Tutorial.dfy`](Tutorial.dfy) shows how to import the library, call the high-level API, and use the low-level API to make localized modifications to a partial parse of a JSON AST.  The main entry points are `API.Serialize` (to go from utf-8 bytes to a JSON AST), and `API.Deserialize` (for the reverse operation):
+The tutorial in [`Tutorial.dfy`](Tutorial.dfy) shows how to import the library, call the high-level API, and use the low-level API to make localized modifications to a partial parse of a JSON AST.  The main entry points are `API.Serialize` (to go from a JSON value to utf-8 bytes), and `API.Deserialize` (for the reverse operation):
 
 <!-- %check-verify %save tmp-json.dfy -->
 ```dafny
@@ -22,7 +24,7 @@ include "src/Unicode/UnicodeStringsWithoutUnicodeChar.dfy"
 
 import JSON.API
 import opened UnicodeStrings
-import opened JSON.AST
+import opened JSON.Values
 import opened Wrappers
 
 method Test(){
@@ -32,20 +34,20 @@ method Test(){
     ""Population"": 689386,
     ""Area (km2)"": 4584.2}]}");
 
-  var CITY_AST := Object([("Cities", Array([
+  var CITY_VALUE := Object([("Cities", Array([
     Object([
       ("Name", String("Boston")),
       ("Founded", Number(Int(1630))),
       ("Population", Number(Int(689386))),
       ("Area (km2)", Number(Decimal(45842, -1)))])]))]);
 
-  expect API.Deserialize(CITY_JS) == Success(CITY_AST);
+  expect API.Deserialize(CITY_JS) == Success(CITY_VALUE);
 
   var EXPECTED :- expect ToUTF8Checked(
     @"{""Cities"":[{""Name"":""Boston"",""Founded"":1630,""Population"":689386,""Area (km2)"":45842e-1}]}"
   );
 
-  expect API.Serialize(CITY_AST) == Success(EXPECTED);
+  expect API.Serialize(CITY_VALUE) == Success(EXPECTED);
 }
 ```
 

src/JSON/Serializer.dfy

@@ -1,9 +1,9 @@
 // RUN: %verify "%s" --unicode-char:false ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
 // RUN: %verify "%s" --unicode-char:true ../Unicode/UnicodeStringsWithUnicodeChar.dfy
 
-/// =============================================
-///  Serialization from JSON.AST to JSON.Grammar
-/// =============================================
+/// ================================================
+///  Serialization from JSON.Values to JSON.Grammar
+/// ================================================
 ///
 /// For the spec, see ``JSON.Spec.dfy``.
 
@@ -14,7 +14,7 @@ include "../Math.dfy"
 include "Utils/Views.dfy"
 include "Utils/Vectors.dfy"
 include "Errors.dfy"
-include "AST.dfy"
+include "Values.dfy"
 include "Grammar.dfy"
 include "Spec.dfy"
 
@@ -25,7 +25,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
   import opened BoundedInts
   import opened Utils.Str
 
-  import AST
+  import Values
   import Spec
   import opened Errors
   import opened Utils.Vectors
@@ -81,7 +81,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
     Success(View.OfBytes(bs))
   }
 
-  function Number(dec: AST.Decimal): Result<jnumber> {
+  function Number(dec: Values.Decimal): Result<jnumber> {
     var minus: jminus := Sign(dec.n);
     var num: jnum :- Int(Math.Abs(dec.n));
     var frac: Maybe<jfrac> := Empty();
@@ -103,7 +103,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
   const COLON: Structural<jcolon> :=
     MkStructural(Grammar.COLON)
 
-  function KeyValue(kv: (string, AST.JSON)): Result<jKeyValue> {
+  function KeyValue(kv: (string, Values.JSON)): Result<jKeyValue> {
     var k :- String(kv.0);
     var v :- Value(kv.1);
     Success(Grammar.KeyValue(k, COLON, v))
@@ -121,22 +121,22 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
   const COMMA: Structural<jcomma> :=
     MkStructural(Grammar.COMMA)
 
-  function Object(obj: seq<(string, AST.JSON)>): Result<jobject> {
+  function Object(obj: seq<(string, Values.JSON)>): Result<jobject> {
     var items :- Seq.MapWithResult(v requires v in obj => KeyValue(v), obj);
     Success(Bracketed(MkStructural(LBRACE),
                       MkSuffixedSequence(items, COMMA),
                       MkStructural(RBRACE)))
   }
 
 
-  function Array(arr: seq<AST.JSON>): Result<jarray> {
+  function Array(arr: seq<Values.JSON>): Result<jarray> {
     var items :- Seq.MapWithResult(v requires v in arr => Value(v), arr);
     Success(Bracketed(MkStructural(LBRACKET),
                       MkSuffixedSequence(items, COMMA),
                       MkStructural(RBRACKET)))
   }
 
-  function Value(js: AST.JSON): Result<Grammar.Value> {
+  function Value(js: Values.JSON): Result<Grammar.Value> {
     match js
     case Null => Success(Grammar.Null(View.OfBytes(NULL)))
     case Bool(b) => Success(Grammar.Bool(Bool(b)))
@@ -146,7 +146,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer {
     case Array(arr) => var a :- Array(arr); Success(Grammar.Array(a))
   }
 
-  function JSON(js: AST.JSON): Result<Grammar.JSON> {
+  function JSON(js: Values.JSON): Result<Grammar.JSON> {
     var val :- Value(js);
     Success(MkStructural(val))
   }

src/JSON/Spec.dfy

@@ -1,9 +1,9 @@
 // RUN: %verify "%s" --unicode-char:false ../Unicode/UnicodeStringsWithoutUnicodeChar.dfy
 // RUN: %verify "%s" --unicode-char:true ../Unicode/UnicodeStringsWithUnicodeChar.dfy
 
-/// =============================================
-///  Serialization from AST.JSON to bytes (Spec)
-/// =============================================
+/// ================================================
+///  Serialization from Values.JSON to bytes (Spec)
+/// ================================================
 ///
 /// This is the high-level spec.  For the implementation, see
 /// ``JSON.Serializer.dfy``.
@@ -15,15 +15,15 @@ include "../Collections/Sequences/Seq.dfy"
 /// "../Unicode/UnicodeStringsWithoutUnicodeChar.dfy"
 /// "../Unicode/UnicodeStringsWithUnicodeChar.dfy"
 
-include "AST.dfy"
+include "Values.dfy"
 include "Errors.dfy"
 include "Utils/Str.dfy"
 
 module {:options "-functionSyntax:4"} JSON.Spec {
   import opened BoundedInts
 
   import opened Utils.Str
-  import opened AST
+  import opened Values
   import opened Wrappers
   import opened Errors
   import opened UnicodeStrings

src/JSON/Tests.dfy

@@ -77,10 +77,10 @@ module JSON.Tests.AbstractSyntaxWrapper refines Wrapper {
   import opened Wrappers
   import Grammar
   import API
-  import AST
+  import Values
   import Spec
 
-  type JSON = AST.JSON
+  type JSON = Values.JSON
 
   method Deserialize(bs: bytes) returns (js: DeserializationResult<JSON>) {
     js := API.Deserialize(bs);