Code

JSON support#51

Code

Merged

robin-aws merged 92 commits intomasterdafny-lang/libraries:masterfrom json-mergedafny-lang/libraries:json-mergeCopy head branch name to clipboardMay 5, 2023

+4,213-29

Commits

Commits on Sep 2, 2022

• feat: Add a JSON serializer/deserializer

  cpitclaudel

  committed
  4e43e63

  Copy full SHA for 4e43e63

• json: Add an efficient serializer

  cpitclaudel

  committed
  f611179

  Copy full SHA for f611179

• json: Move away from member functions to reduce the number of lambdas

  Show description for e3d8e83
  cpitclaudel

  committed
  e3d8e83

  Copy full SHA for e3d8e83

• json: Clean up grammar and put separators after items, not before

  cpitclaudel

  committed
  c5394f7

  Copy full SHA for c5394f7

• json: Complete soundness proof

  cpitclaudel

  committed
  72708eb

  Copy full SHA for 72708eb

• json: Add a clean low-level API

  cpitclaudel

  committed
  2a0c713

  Copy full SHA for 2a0c713

• json: Speed things up using by method bodies in a few places

  cpitclaudel

  committed
  593b32e

  Copy full SHA for 593b32e

• json: Small cleanup in types

  cpitclaudel

  committed
  4c50ce6

  Copy full SHA for 4c50ce6

• json(wip): Start working on high-level API

  cpitclaudel

  committed
  0198334

  Copy full SHA for 0198334

• json: Clean up encoder and add decoder

  cpitclaudel

  committed
  a827a77

  Copy full SHA for a827a77

• json: Optimize traversals and add support for unicode escapes

  cpitclaudel

  committed
  8af0e54

  Copy full SHA for 8af0e54

• json: Finish unicode encoding and decoding

  cpitclaudel

  committed
  32068c0

  Copy full SHA for 32068c0

• json: Adopt a consistent naming scheme across modules

  cpitclaudel

  committed
  5ffcf35

  Copy full SHA for 5ffcf35

• json: Clean up API files

  cpitclaudel

  committed
  6ba1735

  Copy full SHA for 6ba1735

• json: Merge latest changes to the vectors library

  cpitclaudel

  committed
  74f9b0b

  Copy full SHA for 74f9b0b

• json: Move IntPow and IntLog to their own utility module

  cpitclaudel

  committed
  a0a8166

  Copy full SHA for a0a8166

• json: Add a README

  cpitclaudel

  committed
  c032f8b

  Copy full SHA for c032f8b

• json: Add a useful postcondition to Views.Merge

  cpitclaudel

  committed
  2de6306

  Copy full SHA for 2de6306

• json: Speed up a proof

  cpitclaudel

  committed
  92a8f8d

  Copy full SHA for 92a8f8d

• json: Move all math code to NonlinearArithmetic/ and use /noNLArith

  cpitclaudel

  committed
  390e288

  Copy full SHA for 390e288

• json: Add a tutorial

  cpitclaudel

  committed
  dcd06cc

  Copy full SHA for dcd06cc

Commits on Sep 15, 2022

• Update src/JSON/README.md

  Show description for f23ed82
  

  cpitclaudel

  and

  MikaelMayer

  authored
  f23ed82

  Copy full SHA for f23ed82

Commits on Dec 30, 2022

• json: Fix two typos in the README

  cpitclaudel

  committed
  efc4b0b

  Copy full SHA for efc4b0b

• json: Add a TODO

  cpitclaudel

  committed
  d7064d2

  Copy full SHA for d7064d2

• Merge remote-tracking branch 'origin/master' into json-merge

  cpitclaudel

  committed
  4e6b74a

  Copy full SHA for 4e6b74a

• json: Rename parameters and functions based on review

  cpitclaudel

  committed
  d75efc1

  Copy full SHA for d75efc1

• json: Update to latest Dafny

  cpitclaudel

  committed
  ddea84f

  Copy full SHA for ddea84f

• json: Rename LowLevel and HighLevel to Concrete and Abstract

  cpitclaudel

  committed
  92dcba1

  Copy full SHA for 92dcba1

• json: More renamings

  cpitclaudel

  committed
  515c6fb

  Copy full SHA for 515c6fb

• json: Apply @MikaelMayer's feedback

  cpitclaudel

  committed
  95462d2

  Copy full SHA for 95462d2

• json: Add lit headers to run verification and tests in CI

  cpitclaudel

  committed
  1670c1d

  Copy full SHA for 1670c1d

Commits on Feb 20, 2023

• Merge branch 'master' into json-merge

  alex-chew

  authored
  b448fde

  Copy full SHA for b448fde

Commits on Mar 4, 2023

• Merge branch 'master' into json-merge

  robin-aws

  authored
  cdb9fd0

  Copy full SHA for cdb9fd0

• Updating lit syntax and a few function methods

  robin-aws

  committed
  3c71738

  Copy full SHA for 3c71738

• Remaining lit syntax fixes

  robin-aws

  committed
  d1bc8dc

  Copy full SHA for d1bc8dc

• Updating CI to use 3.13.1 and 4.0.0

  Show description for 634f88c
  robin-aws

  committed
  634f88c

  Copy full SHA for 634f88c

Commits on Mar 6, 2023

• Split up the most expensive assertion batch

  robin-aws

  committed
  08cf34d

  Copy full SHA for 08cf34d

Commits on Mar 16, 2023

• Merge branch 'master' into json-merge

  fabiomadge

  authored
  26af65f

  Copy full SHA for 26af65f

• drop support for old Dafny versions

  fabiomadge

  committed
  578cb95

  Copy full SHA for 578cb95

• format

  fabiomadge

  committed
  b96bbae

  Copy full SHA for b96bbae

• fix doctest

  fabiomadge

  committed
  eb41584

  Copy full SHA for eb41584

• fix workflow

  fabiomadge

  committed
  899fcb7

  Copy full SHA for 899fcb7

• drop old Dafny in the doc tests as well

  fabiomadge

  committed
  9a321aa

  Copy full SHA for 9a321aa

• stable formatting

  fabiomadge

  committed
  06dd2c6

  Copy full SHA for 06dd2c6

• update setup-dafny-action

  fabiomadge

  committed
  22f2258

  Copy full SHA for 22f2258

• update literals

  fabiomadge

  committed
  829ae34

  Copy full SHA for 829ae34

• weaken test

  fabiomadge

  committed
  8c7efb8

  Copy full SHA for 8c7efb8

• revert assert by

  fabiomadge

  committed
  9b4bd4a

  Copy full SHA for 9b4bd4a

Commits on Mar 20, 2023

• Dafny 4

  fabiomadge

  committed
  7fb9e02

  Copy full SHA for 7fb9e02

Commits on Apr 6, 2023

• Optimize UnicodeEncodingForm.EncodeScalarSequence

  robin-aws

  committed
  a1cae95

  Copy full SHA for a1cae95

Commits on Apr 11, 2023

• fix Serializer

  fabiomadge

  committed
  5553fb8

  Copy full SHA for 5553fb8

• RUN: %verify

  fabiomadge

  committed
  7723fb5

  Copy full SHA for 7723fb5

Commits on Apr 19, 2023

• Merge branch 'json-merge' of github.com:dafny-lang/libraries into json-merge

  robin-aws

  committed
  5d196cd

  Copy full SHA for 5d196cd

• fix Deserializer

  fabiomadge

  committed
  e0827c5

  Copy full SHA for e0827c5

• Generalize JSON code to work with either --unicode-char mode

  Show description for 942be81
  

  robin-aws

  and

  fabiomadge

  authored
  942be81

  Copy full SHA for 942be81

• Merge branch 'master' into json-merge

  fabiomadge

  authored
  32bddbe

  Copy full SHA for 32bddbe

• format

  fabiomadge

  committed
  2029a96

  Copy full SHA for 2029a96

• docs

  fabiomadge

  committed
  c984b22

  Copy full SHA for c984b22

Commits on Apr 20, 2023

• Merge branch 'json-merge' of github.com:dafny-lang/libraries into json-merge

  Show description for bbf2891
  robin-aws

  committed
  bbf2891

  Copy full SHA for bbf2891

• Axiomatize trivially true but expensive assertion

  robin-aws

  committed
  99d189b

  Copy full SHA for 99d189b

• Refactor - resolves but doesn’t verify yet

  robin-aws

  committed
  dc50674

  Copy full SHA for dc50674

Commits on Apr 21, 2023

• really fix the deserializer

  fabiomadge

  committed
  0a8acf7

  Copy full SHA for 0a8acf7

Commits on Apr 26, 2023

• Attempt at function by method, doesn’t verify yet

  robin-aws

  committed
  d36231a

  Copy full SHA for d36231a

• Revert "Attempt at function by method, doesn’t verify yet"

  Show description for 43e51b1
  robin-aws

  committed
  43e51b1

  Copy full SHA for 43e51b1

• Simple extra-argument tail recursion

  robin-aws

  committed
  989c6d9

  Copy full SHA for 989c6d9

• Have you even ever coded before Robin

  robin-aws

  committed
  407432f

  Copy full SHA for 407432f

Commits on Apr 27, 2023

• Bound resource count instead of time

  Show description for ff5ce0b
  robin-aws

  committed
  ff5ce0b

  Copy full SHA for ff5ce0b

• Bound resource count instead of time

  Show description for 0ea991d
  robin-aws

  committed
  0ea991d

  Copy full SHA for 0ea991d

• Don’t include UnicodeStrings directly, augment CI to test both ways

  robin-aws

  committed
  99f0662

  Copy full SHA for 99f0662

• Revert "Don’t include UnicodeStrings directly, augment CI to test both ways"

  Show description for fb26d7f
  robin-aws

  committed
  fb26d7f

  Copy full SHA for fb26d7f

• Different approach with multiple lit commands instead

  robin-aws

  committed
  10545c8

  Copy full SHA for 10545c8

Commits on May 3, 2023

• Tweak comment

  robin-aws

  committed
  e84b10a

  Copy full SHA for e84b10a

• ZeroCopy code doesn’t depend on UnicodeStrings module(s)

  robin-aws

  committed
  53ce3dd

  Copy full SHA for 53ce3dd

• Formatting

  robin-aws

  committed
  6136cda

  Copy full SHA for 6136cda

• Fix README.md

  robin-aws

  committed
  4aacbd6

  Copy full SHA for 4aacbd6

• Actually check-examples uses —unicode-char:false

  robin-aws

  committed
  7d626c5

  Copy full SHA for 7d626c5

Commits on May 4, 2023

• Rename JSON.AST to JSON.Values

  robin-aws

  committed
  c35669c

  Copy full SHA for c35669c

• Add Bug note, test on Java too

  robin-aws

  committed
  4287c0b

  Copy full SHA for 4287c0b

• Merge branch 'json-merge-without-parameterized-subset-types' into json-merge

  Show description for 79551df
  robin-aws

  committed
  79551df

  Copy full SHA for 79551df

• Remove unused function that can’t be compiled for Java

  Show description for 8992608
  robin-aws

  committed
  8992608

  Copy full SHA for 8992608

• Formatting

  robin-aws

  committed
  f277ffe

  Copy full SHA for f277ffe

• Double checking ZeroCopy/Deserializer.dfy verifies with the subset types

  robin-aws

  committed
  d2fa10f

  Copy full SHA for d2fa10f

• Revert "Double checking ZeroCopy/Deserializer.dfy verifies with the subset types"

  Show description for acdb6ec
  robin-aws

  committed
  acdb6ec

  Copy full SHA for acdb6ec

• Progress on verifying again

  robin-aws

  committed
  ceed951

  Copy full SHA for ceed951

• Revert "Progress on verifying again"

  Show description for fc2ee8c
  robin-aws

  committed
  fc2ee8c

  Copy full SHA for fc2ee8c

• Undoing subset type workaround

  Show description for 53b7abf
  robin-aws

  committed
  53b7abf

  Copy full SHA for 53b7abf

• Formatting

  robin-aws

  committed
  2753e76

  Copy full SHA for 2753e76

Commits on May 5, 2023

• Apply suggestions from code review

  Show description for 35cca47
  

  robin-aws

  and

  MikaelMayer

  authored
  35cca47

  Copy full SHA for 35cca47

• Removing stale TODOs

  robin-aws

  committed
  62d5c89

  Copy full SHA for 62d5c89

• Mikael’s calc rewrite

  robin-aws

  committed
  da1b5ac

  Copy full SHA for da1b5ac

• Formatting

  robin-aws

  committed
  45055e1

  Copy full SHA for 45055e1

• I said, FORMATTING

  robin-aws

  committed
  a58e01d

  Copy full SHA for a58e01d