import Base
import ./lib.bend as J

law encode_null:
  { J.Json.encode(J.JNull{}) == "null" : String }

law encode_true:
  { J.Json.encode(J.JBool{True{}}) == "true" : String }

law encode_false:
  { J.Json.encode(J.JBool{False{}}) == "false" : String }

law encode_num_zero:
  { J.Json.encode(J.JNum{0}) == "0" : String }

law encode_num_42:
  { J.Json.encode(J.JNum{42}) == "42" : String }

law encode_str_hi:
  { J.Json.encode(J.JStr{"hi"}) == "\"hi\"" : String }

law show_eq_encode_null:
  { J.Json.show(J.JNull{}) == J.Json.encode(J.JNull{}) : String }

law decode_null:
  { J.Json.decode("null") == Some{J.JNull{}} : Maybe<&2, J.Json> }

law decode_true:
  { J.Json.decode("true") == Some{J.JBool{True{}}} : Maybe<&2, J.Json> }

law decode_false:
  { J.Json.decode("false") == Some{J.JBool{False{}}} : Maybe<&2, J.Json> }

law decode_num_42:
  { J.Json.decode("42") == Some{J.JNum{42}} : Maybe<&2, J.Json> }

law decode_str_hi:
  { J.Json.decode("\"hi\"") == Some{J.JStr{"hi"}} : Maybe<&2, J.Json> }

law decode_ws_true:
  { J.Json.decode(" true ") == Some{J.JBool{True{}}} : Maybe<&2, J.Json> }

law roundtrip_null:
  { J.Json.decode(J.Json.encode(J.JNull{})) == Some{J.JNull{}} : Maybe<&2, J.Json> }

law roundtrip_true:
  {
    J.Json.decode(J.Json.encode(J.JBool{True{}})) == Some{J.JBool{True{}}}
    : Maybe<&2, J.Json>
  }

law roundtrip_false:
  {
    J.Json.decode(J.Json.encode(J.JBool{False{}})) == Some{J.JBool{False{}}}
    : Maybe<&2, J.Json>
  }

law roundtrip_num_42:
  {
    J.Json.decode(J.Json.encode(J.JNum{42})) == Some{J.JNum{42}}
    : Maybe<&2, J.Json>
  }

law roundtrip_str_hi:
  {
    J.Json.decode(J.Json.encode(J.JStr{"hi"})) == Some{J.JStr{"hi"}}
    : Maybe<&2, J.Json>
  }

law encode_num_1:
  { J.Json.encode(J.JNum{1}) == "1" : String }

law encode_str_empty:
  { J.Json.encode(J.JStr{""}) == "\"\"" : String }

law decode_num_0:
  { J.Json.decode("0") == Some{J.JNum{0}} : Maybe<&2, J.Json> }

law decode_str_empty:
  { J.Json.decode("\"\"") == Some{J.JStr{""}} : Maybe<&2, J.Json> }

law roundtrip_num_0:
  { J.Json.decode(J.Json.encode(J.JNum{0})) == Some{J.JNum{0}} : Maybe<&2, J.Json> }

law roundtrip_str_empty:
  { J.Json.decode(J.Json.encode(J.JStr{""})) == Some{J.JStr{""}} : Maybe<&2, J.Json> }

law show_eq_encode_true:
  { J.Json.show(J.JBool{True{}}) == J.Json.encode(J.JBool{True{}}) : String }

law decode_ws_null:
  { J.Json.decode("  null  ") == Some{J.JNull{}} : Maybe<&2, J.Json> }