From 8c2f61e8b4224efe632157c41c9b4ccc4fc5e74c Mon Sep 17 00:00:00 2001 From: Glyn Normington Date: Mon, 23 Nov 2020 16:38:40 +0000 Subject: [PATCH 1/2] Rough draft --- README.md | 106 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 106 insertions(+) create mode 100644 README.md diff --git a/README.md b/README.md new file mode 100644 index 0000000..e671d9d --- /dev/null +++ b/README.md @@ -0,0 +1,106 @@ +# JSONPath axiomatic semantics + +** WORK IN PROGRESS ** + +## sequences of JSON values + +A JSONPath is modelled as mapping one sequence of JSON values to another sequence of JSON values. +The `<>` notation is used for sequences, to try to distinguish these from JSON arrays. + +Empty sequence: `<>`. + +Concatenation: ` = ^ `. + +So, for example, the sequence `` is equivalent to the concatenation of three single item +sequences ` ^ ^ `. + +## sequence semantics +A selector `s` takes a sequence of values and applies to each one separately. +The results are then concatenated. + +``` +<> s = <> +(x^y)s = (x s)^(y s) +``` + +## JSON object construction + +If `m` and `n` are JSON objects with no keys in common, then `m ∪ n` is the JSON object containing +all the mappings of `m` and `n` (but no others). + +## compound path semantics + +If JSONPath `p` is selector `s` followed by JSONPath `t`, then for all JSON values `v`: +``` +p = (s)t +``` + +## root selector semantics +`$` is effectively a no-op. If `t` is a JSONPath (without a leading `$`), then: +``` +$t = t +``` +Question: do we need to use something like quasi quotes to clarify the above? + +## dot child +If `o` is a JSON object which does not have key `k`, then: +``` +.k = <> +``` +and: +``` +.k = +``` + +## union +``` +[u, v] = ([u]) ^ ([v]) +``` + +## bracket child +If `o` is a JSON object which does not have key `k` (for certain forms of k...), then: +``` +[k] = <> +``` +and: +``` +[k] = +``` + +## array slice +If `a` is an array, then: +``` +... details! ... +``` + +If `a` is not an array and `sl` is a slice expression, then: +``` +[sl] = <> +``` + +## recursive descent +If `z` is a scalar: +``` +.. = +``` +If `o` is an empty object: +``` +.. = <> +``` + +If `o` is a JSON object which does not have key `k`, then: +If `o` is an object comprised of `k:v` and an object p: +``` +.. = ()^(..)^(..) +``` +Note: since an object can be deconstructed to the form `o ∪ {k:v}` for arbitrary key `k` in +the original object, the ordering of the result is only partially defined. + +If `a` is an empty array: +``` +.. = <> +``` +If `h` is a JSON value and `t` is a JSON array: +``` +(^t).. = ()^(..)^(t..) +``` \ No newline at end of file From 92e9a9ba4aed50a84ebc670b883b597622d9f47a Mon Sep 17 00:00:00 2001 From: Glyn Normington Date: Mon, 30 Nov 2020 16:59:42 +0000 Subject: [PATCH 2/2] Address review comments --- README.md | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index e671d9d..d4c5469 100644 --- a/README.md +++ b/README.md @@ -42,7 +42,10 @@ If JSONPath `p` is selector `s` followed by JSONPath `t`, then for all JSON valu ``` Question: do we need to use something like quasi quotes to clarify the above? -## dot child +## selectors + +The following sections describe primitive selectors which can be strung together to form a JSONPath. +### dot child If `o` is a JSON object which does not have key `k`, then: ``` .k = <> @@ -52,12 +55,12 @@ and: .k = ``` -## union +### union ``` [u, v] = ([u]) ^ ([v]) ``` -## bracket child +### bracket child If `o` is a JSON object which does not have key `k` (for certain forms of k...), then: ``` [k] = <> @@ -67,7 +70,7 @@ and: [k] = ``` -## array slice +### array slice If `a` is an array, then: ``` ... details! ... @@ -78,7 +81,7 @@ If `a` is not an array and `sl` is a slice expression, then: [sl] = <> ``` -## recursive descent +### recursive descent If `z` is a scalar: ``` .. =