blob: ce52b89d2516c06322f2bc732e3384fea55668bd (
plain)
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
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
import Lean.Data.AssocList
import Lean.Data.Json
namespace Rego
inductive Any where
-- Scalar types
| null
| bool (b : Bool)
| num (n : Lean.JsonNumber)
| str (s : String)
-- Composite types
| array (xs : Array Any)
| set (elts : List Any) -- FIXME: `List` obviously isn't correct here.
| object (field : Lean.AssocList String Any)
deriving Inhabited
namespace Any
def expectBool (x : Any) : Option Bool :=
if let Any.bool b := x then some b else none
def expectNumber (x : Any) : Option Lean.JsonNumber :=
if let Any.num n := x then some n else none
def expectArray (x : Any) : Option (Array Any) :=
if let Any.array y := x then some y else none
def expectObject (x : Any) : Option (Lean.AssocList String Any) :=
if let Any.object y := x then some y else none
end Any
-- TODO: Complete implementation
def eqv : Any → Any → Bool
| Any.null, Any.null => True
| Any.bool b₁, Any.bool b₂ => b₁ = b₂
| _, _ => False
instance : BEq Any where
beq := eqv
abbrev Set := List
abbrev Number := Lean.JsonNumber
abbrev Object := Lean.AssocList String Any
namespace Number
def toNat' (n : Number) : Option Nat :=
if n.exponent = 0 && n.mantissa ≥ 0 then
some (Int.toNat n.mantissa)
else none
end Number
namespace Object
def ref (obj : Object) (attr : String) : Option Any :=
Lean.AssocList.find? attr obj
end Object
def obj_eqv (x y : Object) : Bool :=
(List.map Prod.snd (Lean.AssocList.toList x))
== (List.map Prod.snd (Lean.AssocList.toList y))
instance : BEq Object where
beq := obj_eqv
end Rego
|
© 2015 - 2026 Jakob L. Kreuze
