Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use a custom deserializer instead of wrapper types #6

Merged
merged 51 commits into from
Nov 21, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
143737e
Add `serde-itf` crate with native deserialization
romac Oct 26, 2023
f539d16
Use the Visitor pattern
romac Oct 26, 2023
8f0dbfd
Support for BigInt
romac Oct 26, 2023
3cc1311
Move values under `value` module
romac Oct 26, 2023
f595a56
Cleanup
romac Oct 26, 2023
e481cf7
Move tests into `serde-itf` crate and delete `itf` crate
romac Oct 26, 2023
0823107
Rename `serde-itf` crate to `itf`
romac Oct 26, 2023
a56363c
update visit_bigint for num_bigint::BigInt
rnbguy Nov 18, 2023
c03bec1
update itf::value::BigInt deserialize for num_bigint::BigInt
rnbguy Nov 18, 2023
92bb9d3
visit_bigint when deserialize_tuple
rnbguy Nov 18, 2023
d34686e
all integers are bigints
rnbguy Nov 18, 2023
27b1975
use num_bigint::BigInt in deserialized stuct directly
rnbguy Nov 18, 2023
553b9ca
reactivate failing test
rnbguy Nov 18, 2023
e552e93
rm unused import
rnbguy Nov 18, 2023
255cb80
fix tuple deserialize
rnbguy Nov 18, 2023
c2b56f5
fix set deserialize
rnbguy Nov 18, 2023
2bbeb1a
regression tests
rnbguy Nov 18, 2023
0b34d1c
bunch of bigint testcases from debugging
rnbguy Nov 19, 2023
0547a77
rm dbg!()
rnbguy Nov 19, 2023
1ff92d8
use serde_json::Value over json string
rnbguy Nov 19, 2023
d89d2fb
add testcases for Value::deserialize(Value)
rnbguy Nov 19, 2023
eeb0570
Merge branch 'main' into native-types
romac Nov 20, 2023
4efbf20
Update code coverage workflow
romac Nov 20, 2023
c6b1f48
Update codecov config
romac Nov 20, 2023
468bc00
Hide `Value` enum from documentation
romac Nov 20, 2023
b10e7b0
revert c03bec1
rnbguy Nov 20, 2023
7ee8043
update tests
rnbguy Nov 20, 2023
29a580c
fix failing tests
rnbguy Nov 20, 2023
e53d02d
fix incorrect test
rnbguy Nov 20, 2023
21aa057
itf::Value over itf::value::Value
rnbguy Nov 20, 2023
51a3f58
add a complete test
rnbguy Nov 20, 2023
11981c4
add portability test between i64 and BigInt
rnbguy Nov 20, 2023
d91d408
support deserializing Number to BigInt
rnbguy Nov 20, 2023
05b1d4f
test deserialization failure from true bigint to i64
rnbguy Nov 20, 2023
79bfbeb
add success case for true bigint deserialization
rnbguy Nov 20, 2023
9920493
test for failure when deserialize bigint to int in enum
rnbguy Nov 20, 2023
33decd2
Add example and update README
romac Nov 20, 2023
3d2b8ca
Update changelog
romac Nov 20, 2023
27a483e
Include README in top-level crate doc
romac Nov 20, 2023
b06e4b5
Split `Deserializer` impl and `Error` into their own modules
romac Nov 20, 2023
a2eef53
Add a `itf::de::from_bigint` deserializer function to convert from `B…
romac Nov 20, 2023
bb0658f
disallow implicit deser from bigint to (u)int
rnbguy Nov 21, 2023
2888463
disallow implicit deser from int to bigint
rnbguy Nov 21, 2023
87eb1d0
use Integer as DeserializeAs to deserialize from BigInt to (u)int
rnbguy Nov 21, 2023
54aee5a
update tests for explicit serialization from BigInt to (u)int
rnbguy Nov 21, 2023
c71bcc9
Re-export `serde_with::As` under `itf::de::As` to enable its use with…
romac Nov 21, 2023
1ce3943
Add doc comments to the helpers
romac Nov 21, 2023
7090e9e
Document public items
romac Nov 21, 2023
e39f141
Remove unused `Error::Io` variant
romac Nov 21, 2023
9d62110
Document `Error`
romac Nov 21, 2023
e2aef1c
Redefine `itf::de::Integer` as `TryFromInto<BigInt>`
romac Nov 21, 2023
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 23 additions & 1 deletion .codecov.yml
Original file line number Diff line number Diff line change
@@ -1,4 +1,26 @@
codecov:
require_ci_to_pass: yes
bot: romac

coverage:
precision: 2
round: nearest
range: "50...100"

status:
project:
default:
target: auto
threshold: 5%
removed_code_behavior: adjust_base
paths:
- "itf"
patch:
default:
target: auto
threshold: 5%
paths:
- "itf"

changes:
default:
informational: true
30 changes: 20 additions & 10 deletions .github/workflows/coverage.yml
Original file line number Diff line number Diff line change
@@ -1,31 +1,41 @@
name: Coverage

on:
pull_request:
push:
branches: main
paths:
- itf/**
pull_request:
paths:
- itf/**

jobs:
coverage:
runs-on: ubuntu-latest
defaults:
run:
working-directory: itf
env:
CARGO_TERM_COLOR: always
steps:
- uses: actions/checkout@v3
- name: Install Rust
uses: actions-rs/toolchain@v1
- name: Checkout
uses: actions/checkout@v4
- name: Setup Rust toolchain
uses: actions-rust-lang/setup-rust-toolchain@v1
with:
toolchain: stable
override: true
toolchain: nightly
components: llvm-tools-preview
- name: Install cargo-nextest
uses: taiki-e/install-action@cargo-nextest
- name: Install cargo-llvm-cov
uses: taiki-e/install-action@cargo-llvm-cov
- name: Install cargo-nextest
uses: taiki-e/install-action@nextest
- name: Generate code coverage
run: cargo llvm-cov nextest --all-features --workspace --lcov --output-path lcov.info
- name: Generate text report
run: cargo llvm-cov report
- name: Upload coverage to Codecov
uses: codecov/codecov-action@v3
with:
token: ${{ secrets.CODECOV_TOKEN }} # not required for public repos
files: lcov.info
token: ${{ secrets.CODECOV_TOKEN }}
files: itf/lcov.info
fail_ci_if_error: true
10 changes: 10 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,21 @@
# CHANGELOG

## Unreleased

- Deserialize ITF values into native Rust types with a custom deserializer
instead of having to go through `Itf<A>` wrapper type.
([#6](https://github.com/informalsystems/itf-rs/pull/6))

## v0.1.2

*November 10th, 2023*

- Add `From<T> where T: From<BigInt>` instance for `ItfBigInt`

## v0.1.1

*November 10th, 2023*

- Add support for new `timestamp` field in meta section of ITF traces

## v0.1
Expand Down
61 changes: 32 additions & 29 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,11 @@ Rust library for consuming [Apalache ITF Traces][itf-adr].
**Trace:** [`MissionariesAndCannibals.itf.json`](./apalache-itf/tests/fixtures/MissionariesAndCannibals.itf.json)

```rust
use serde::Deserialize;
use std::collections::{BTreeSet, BTreeMap};

use itf::{trace_from_str, ItfMap, ItfSet};
use serde::Deserialize;

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Bank {
#[serde(rename = "N")]
North,
Expand All @@ -33,7 +33,7 @@ enum Bank {
South,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Deserialize)]
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Person {
#[serde(rename = "c1_OF_PERSON")]
Cannibal1,
Expand All @@ -51,30 +51,31 @@ enum Person {
#[derive(Clone, Debug, Deserialize)]
struct State {
pub bank_of_boat: Bank,
pub who_is_on_bank: ItfMap<Bank, ItfSet<Person>>,
pub who_is_on_bank: BTreeMap<Bank, BTreeSet<Person>>,
}

let data = include_str!("../tests/fixtures/MissionariesAndCannibals.itf.json");
let trace: Trace<State> = trace_from_str(data).unwrap();
let trace: itf::Trace<State> = itf::trace_from_str(data).unwrap();

dbg!(trace);
```

**Output:**

```rust
trace = Trace {
meta: TraceMeta {
description: None,
```rust,ignore
[itf/examples/cannibals.rs:45] trace = Trace {
meta: Meta {
format: None,
format_description: None,
source: Some(
"MC_MissionariesAndCannibalsTyped.tla",
),
description: None,
var_types: {
"bank_of_boat": "Str",
"who_is_on_bank": "Str -> Set(PERSON)",
},
format: None,
format_description: None,
timestamp: None,
other: {},
},
params: [],
Expand All @@ -85,7 +86,7 @@ trace = Trace {
loop_index: None,
states: [
State {
meta: StateMeta {
meta: Meta {
index: Some(
0,
),
Expand All @@ -96,16 +97,16 @@ trace = Trace {
who_is_on_bank: {
West: {},
East: {
Missionary2,
Cannibal1,
Cannibal2,
Missionary1,
Missionary2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
1,
),
Expand All @@ -115,18 +116,18 @@ trace = Trace {
bank_of_boat: West,
who_is_on_bank: {
West: {
Missionary2,
Cannibal2,
Missionary2,
},
East: {
Missionary1,
Cannibal1,
Missionary1,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
2,
),
Expand All @@ -139,15 +140,15 @@ trace = Trace {
Cannibal2,
},
East: {
Missionary2,
Cannibal1,
Missionary1,
Missionary2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
3,
),
Expand All @@ -157,8 +158,8 @@ trace = Trace {
bank_of_boat: West,
who_is_on_bank: {
West: {
Missionary1,
Cannibal2,
Missionary1,
Missionary2,
},
East: {
Expand All @@ -168,7 +169,7 @@ trace = Trace {
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
4,
),
Expand All @@ -177,19 +178,19 @@ trace = Trace {
value: State {
bank_of_boat: East,
who_is_on_bank: {
East: {
Cannibal2,
Cannibal1,
},
West: {
Missionary1,
Missionary2,
},
East: {
Cannibal1,
Cannibal2,
},
},
},
},
State {
meta: StateMeta {
meta: Meta {
index: Some(
5,
),
Expand All @@ -198,13 +199,13 @@ trace = Trace {
value: State {
bank_of_boat: West,
who_is_on_bank: {
East: {},
West: {
Cannibal1,
Cannibal2,
Missionary1,
Missionary2,
},
East: {},
},
},
},
Expand All @@ -227,7 +228,9 @@ Copyright © 2023 Informal Systems Inc. and itf-rs authors.

Licensed under the Apache License, Version 2.0 (the "License"); you may not use the files in this repository except in compliance with the License. You may obtain a copy of the License at

https://www.apache.org/licenses/LICENSE-2.0
```text
https://www.apache.org/licenses/LICENSE-2.0
```

Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License.

Expand Down
7 changes: 4 additions & 3 deletions itf/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ rust-version = "1.65"

[dependencies]
num-bigint = { version = "0.4", features = ["serde"] }
serde = { version = "1", features = ["derive"] }
serde_json = "1"
thiserror = "1"
num-traits = { version = "0.2" }
serde = { version = "1", features = ["derive"] }
serde_json = { version = "1", features = ["raw_value"] }
serde_with = { version = "3.4.0" }
48 changes: 48 additions & 0 deletions itf/examples/cannibals.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
#![allow(dead_code)]

use std::collections::{BTreeMap, BTreeSet};

use serde::Deserialize;

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Bank {
#[serde(rename = "N")]
North,

#[serde(rename = "W")]
West,

#[serde(rename = "E")]
East,

#[serde(rename = "S")]
South,
}

#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Deserialize)]
enum Person {
#[serde(rename = "c1_OF_PERSON")]
Cannibal1,

#[serde(rename = "c2_OF_PERSON")]
Cannibal2,

#[serde(rename = "m1_OF_PERSON")]
Missionary1,

#[serde(rename = "m2_OF_PERSON")]
Missionary2,
}

#[derive(Clone, Debug, Deserialize)]
struct State {
pub bank_of_boat: Bank,
pub who_is_on_bank: BTreeMap<Bank, BTreeSet<Person>>,
}

fn main() {
let data = include_str!("../tests/fixtures/MissionariesAndCannibals.itf.json");
let trace: itf::Trace<State> = itf::trace_from_str(data).unwrap();

dbg!(trace);
}
20 changes: 20 additions & 0 deletions itf/src/de.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
use serde::de::DeserializeOwned;

use crate::Value;

mod error;
pub use error::Error;

mod helpers;
pub use helpers::As;
pub use helpers::Integer;

mod deserializer;

#[doc(hidden)]
pub fn decode_value<T>(value: Value) -> Result<T, Error>
where
T: DeserializeOwned,
{
T::deserialize(value)
}
Loading
Loading