forked from anakrish/Rego-FStar
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Rego.Value.fsti
32 lines (22 loc) · 864 Bytes
/
Rego.Value.fsti
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
// Copyright (c) Microsoft Corporation.
// Licensed under the MIT License.
module Rego.Value
[@@ PpxDerivingYoJson; PpxDerivingShow ]
type value:eqtype =
| Null
| Bool of bool
| Number of int (* TODO: number can be i64, u64, f64 or big decimal *)
| String of string
| Array of list value
| Set of list value
| Object of list (value * value)
| Undefined
type ord = x:int { x = -1 || x = 0 || x = 1}
val cmp (v1:value) (v2:value) : ord
val insert_into_array (arr:value) (v:value) : value
val insert_into_object (obj:value) (key:value) (v:value) : value
val insert_into_set (set:value) (item:value) : value
val lookup_path (obj:value) (path:list value) : value
val insert_at_path (obj:value) (path: list value) (v:value) : value
val to_json (v:value) : string
val to_json_pretty (v:value) : string