From c35669c3af639489d5ddd65d1e993946077eee66 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Wed, 3 May 2023 17:16:22 -0700 Subject: [PATCH] Rename JSON.AST to JSON.Values --- src/JSON/API.dfy | 10 ++++----- src/JSON/Deserializer.dfy | 38 ++++++++++++++++---------------- src/JSON/Grammar.dfy | 2 +- src/JSON/README.md | 16 ++++++++------ src/JSON/Serializer.dfy | 22 +++++++++--------- src/JSON/Spec.dfy | 10 ++++----- src/JSON/Tests.dfy | 4 ++-- src/JSON/Tutorial.dfy | 28 +++++++++++------------ src/JSON/{AST.dfy => Values.dfy} | 2 +- 9 files changed, 67 insertions(+), 65 deletions(-) rename src/JSON/{AST.dfy => Values.dfy} (87%) diff --git a/src/JSON/API.dfy b/src/JSON/API.dfy index 6077bb3d..74f9c89e 100644 --- a/src/JSON/API.dfy +++ b/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>) + function {:opaque} Serialize(js: Values.JSON) : (bs: SerializationResult>) { var js :- Serializer.JSON(js); ZeroCopy.Serialize(js) } - method SerializeAlloc(js: AST.JSON) returns (bs: SerializationResult>) + method SerializeAlloc(js: Values.JSON) returns (bs: SerializationResult>) { var js :- Serializer.JSON(js); bs := ZeroCopy.SerializeAlloc(js); } - method SerializeInto(js: AST.JSON, bs: array) returns (len: SerializationResult) + method SerializeInto(js: Values.JSON, bs: array) returns (len: SerializationResult) modifies bs { var js :- Serializer.JSON(js); len := ZeroCopy.SerializeInto(js, bs); } - function {:opaque} Deserialize(bs: seq) : (js: DeserializationResult) + function {:opaque} Deserialize(bs: seq) : (js: DeserializationResult) { var js :- ZeroCopy.Deserialize(bs); Deserializer.JSON(js) diff --git a/src/JSON/Deserializer.dfy b/src/JSON/Deserializer.dfy index 8b735ed2..3b413592 100644 --- a/src/JSON/Deserializer.dfy +++ b/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,7 +135,7 @@ module {:options "-functionSyntax:4"} JSON.Deserializer { Success(if sign.Char?('-') then -n else n) } - function Number(js: Grammar.jnumber): DeserializationResult { + function Number(js: Grammar.jnumber): DeserializationResult { var JNumber(minus, num, frac, exp) := js; var n :- ToInt(minus, num); @@ -143,38 +143,38 @@ module {:options "-functionSyntax:4"} JSON.Deserializer { 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> { + function Object(js: Grammar.jobject): DeserializationResult> { Seq.MapWithResult(d requires d in js.data => KeyValue(d.t), js.data) } - function Array(js: Grammar.jarray): DeserializationResult> { + function Array(js: Grammar.jarray): DeserializationResult> { Seq.MapWithResult(d requires d in js.data => Value(d.t), js.data) } - function Value(js: Grammar.Value): DeserializationResult { + function Value(js: Grammar.Value): DeserializationResult { 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 { + function JSON(js: Grammar.JSON): DeserializationResult { Value(js.t) } } diff --git a/src/JSON/Grammar.dfy b/src/JSON/Grammar.dfy index 7f6013d9..c32b8b3c 100644 --- a/src/JSON/Grammar.dfy +++ b/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" diff --git a/src/JSON/README.md b/src/JSON/README.md index 1e3355a0..e81467da 100644 --- a/src/JSON/README.md +++ b/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): ```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); } ``` diff --git a/src/JSON/Serializer.dfy b/src/JSON/Serializer.dfy index 8a64bf92..1f936deb 100644 --- a/src/JSON/Serializer.dfy +++ b/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 { + function Number(dec: Values.Decimal): Result { var minus: jminus := Sign(dec.n); var num: jnum :- Int(Math.Abs(dec.n)); var frac: Maybe := Empty(); @@ -103,7 +103,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer { const COLON: Structural := MkStructural(Grammar.COLON) - function KeyValue(kv: (string, AST.JSON)): Result { + function KeyValue(kv: (string, Values.JSON)): Result { var k :- String(kv.0); var v :- Value(kv.1); Success(Grammar.KeyValue(k, COLON, v)) @@ -121,7 +121,7 @@ module {:options "-functionSyntax:4"} JSON.Serializer { const COMMA: Structural := MkStructural(Grammar.COMMA) - function Object(obj: seq<(string, AST.JSON)>): Result { + function Object(obj: seq<(string, Values.JSON)>): Result { var items :- Seq.MapWithResult(v requires v in obj => KeyValue(v), obj); Success(Bracketed(MkStructural(LBRACE), MkSuffixedSequence(items, COMMA), @@ -129,14 +129,14 @@ module {:options "-functionSyntax:4"} JSON.Serializer { } - function Array(arr: seq): Result { + function Array(arr: seq): Result { 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 { + function Value(js: Values.JSON): Result { 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 { + function JSON(js: Values.JSON): Result { var val :- Value(js); Success(MkStructural(val)) } diff --git a/src/JSON/Spec.dfy b/src/JSON/Spec.dfy index 6f71414f..8a76ea1e 100644 --- a/src/JSON/Spec.dfy +++ b/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,7 +15,7 @@ include "../Collections/Sequences/Seq.dfy" /// "../Unicode/UnicodeStringsWithoutUnicodeChar.dfy" /// "../Unicode/UnicodeStringsWithUnicodeChar.dfy" -include "AST.dfy" +include "Values.dfy" include "Errors.dfy" include "Utils/Str.dfy" @@ -23,7 +23,7 @@ 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 diff --git a/src/JSON/Tests.dfy b/src/JSON/Tests.dfy index 04e57a08..2a04681c 100644 --- a/src/JSON/Tests.dfy +++ b/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) { js := API.Deserialize(bs); diff --git a/src/JSON/Tutorial.dfy b/src/JSON/Tutorial.dfy index 9ee445e3..04800fd5 100644 --- a/src/JSON/Tutorial.dfy +++ b/src/JSON/Tutorial.dfy @@ -6,15 +6,15 @@ include "API.dfy" include "ZeroCopy/API.dfy" -/// This library offers two APIs: a high-level one (giving abstract syntax trees +/// This library offers two APIs: a high-level one (giving abstract value trees /// with no concrete syntactic details) and a low-level one (including all /// information about blanks, separator positions, character escapes, etc.). /// -/// ## High-level API (Abstract syntax) +/// ## High-level API (JSON values) module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { import API - import opened AST + import opened Values import opened Wrappers /// Note that you will need to include one of the two files that defines UnicodeStrings @@ -23,7 +23,7 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { import opened UnicodeStrings -/// The high-level API works with fairly simple ASTs that contain native Dafny +/// The high-level API works with fairly simple datatype values that contain native Dafny /// strings: method {:test} Test() { @@ -36,8 +36,8 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { /// writing raw bytes directly from disk or from the network instead). var SIMPLE_JS :- expect ToUTF8Checked("[true]"); - var SIMPLE_AST := Array([Bool(true)]); - expect API.Deserialize(SIMPLE_JS) == Success(SIMPLE_AST); + var SIMPLE_VALUE := Array([Bool(true)]); + expect API.Deserialize(SIMPLE_JS) == Success(SIMPLE_VALUE); /// Here is a larger object, written using a verbatim string (with `@"`). In /// verbatim strings `""` represents a single double-quote character): @@ -62,7 +62,7 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { } ] }"); - var CITIES_AST := + var CITIES_VALUE := Object([ ("Cities", Array([ Object([ @@ -85,12 +85,12 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { ]) ])) ]); - expect API.Deserialize(CITIES_JS) == Success(CITIES_AST); + expect API.Deserialize(CITIES_JS) == Success(CITIES_VALUE); /// Serialization works similarly, with `API.Serialize`. For this first example /// the generated string matches what we started with exactly: - expect API.Serialize(SIMPLE_AST) == Success(SIMPLE_JS); + expect API.Serialize(SIMPLE_VALUE) == Success(SIMPLE_JS); /// For more complex object, the generated layout may not be exactly the same; note in particular how the representation of numbers and the whitespace have changed. @@ -98,7 +98,7 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { @"{""Cities"":[{""Name"":""Boston"",""Founded"":1630,""Population"":689386,""Area (km2)"":45842e-1},{""Name"":""Rome"",""Founded"":-753,""Population"":2873e3,""Area (km2)"":1285},{""Name"":""Paris"",""Founded"":null,""Population"":2161e3,""Area (km2)"":23835e-1}]}" ); - expect API.Serialize(CITIES_AST) == Success(EXPECTED); + expect API.Serialize(CITIES_VALUE) == Success(EXPECTED); /// Additional methods are defined in `API.dfy` to serialize an object into an /// existing buffer or into an array. Below is the smaller example from the @@ -110,7 +110,7 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { ""Population"": 689386, ""Area (km2)"": 4584.2}]}"); - var CITY_AST := + var CITY_VALUE := Object([("Cities", Array([ Object([ ("Name", String("Boston")), @@ -118,13 +118,13 @@ module {:options "-functionSyntax:4"} JSON.Examples.AbstractSyntax { ("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'); } } @@ -148,7 +148,7 @@ module {:options "-functionSyntax:4"} JSON.Examples.ConcreteSyntax { /// The low-level API exposes the same functions and methods as the high-level /// one, but the type that they consume and produce is `Grammar.JSON` (defined /// in `Grammar.dfy` as a `Grammar.Value` surrounded by optional whitespace) -/// instead of `AST.JSON` (defined in `AST.dfy`). Since `Grammar.JSON` contains +/// instead of `Values.JSON` (defined in `Values.dfy`). Since `Grammar.JSON` contains /// all formatting information, re-serializing an object produces the original /// value: diff --git a/src/JSON/AST.dfy b/src/JSON/Values.dfy similarity index 87% rename from src/JSON/AST.dfy rename to src/JSON/Values.dfy index 17d5629f..76952ec2 100644 --- a/src/JSON/AST.dfy +++ b/src/JSON/Values.dfy @@ -1,6 +1,6 @@ // RUN: %verify "%s" -module {:options "-functionSyntax:4"} JSON.AST { +module {:options "-functionSyntax:4"} JSON.Values { datatype Decimal = Decimal(n: int, e10: int) // (n) * 10^(e10)