Prepare to replay XACML repository on top of this one

4 files changed, 113 insertions, 0 deletions

diff --git a/rego-proofs/Rego/.gitignore b/rego-proofs/Rego/.gitignore
new file mode 100644
index 0000000..20c60d7
--- /dev/null
+++ b/rego-proofs/Rego/.gitignore
@@ -0,0 +1,2 @@
+/build
+/lake-packages/*
diff --git a/rego-proofs/Rego/Rego.lean b/rego-proofs/Rego/Rego.lean
new file mode 100644
index 0000000..ce52b89
--- /dev/null
+++ b/rego-proofs/Rego/Rego.lean
@@ -0,0 +1,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
diff --git a/rego-proofs/Rego/lake-manifest.json b/rego-proofs/Rego/lake-manifest.json
new file mode 100644
index 0000000..9b0ab31
--- /dev/null
+++ b/rego-proofs/Rego/lake-manifest.json
@@ -0,0 +1,27 @@
+{"version": 4,
+ "packagesDir": "lake-packages",
+ "packages":
+ [{"git":
+   {"url": "https://github.com/leanprover-community/mathlib4.git",
+    "subDir?": null,
+    "rev": "f85368f49bea5a60679f40625f31177479d7f732",
+    "name": "mathlib",
+    "inputRev?": null}},
+  {"git":
+   {"url": "https://github.com/gebner/quote4",
+    "subDir?": null,
+    "rev": "7ae096b232087096ff0243a2b70d32720d2621ae",
+    "name": "Qq",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/JLimperg/aesop",
+    "subDir?": null,
+    "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
+    "name": "aesop",
+    "inputRev?": "master"}},
+  {"git":
+   {"url": "https://github.com/leanprover/std4",
+    "subDir?": null,
+    "rev": "5507f9d8409f93b984ce04eccf4914d534e6fca2",
+    "name": "std",
+    "inputRev?": "main"}}]}
diff --git a/rego-proofs/Rego/lakefile.lean b/rego-proofs/Rego/lakefile.lean
new file mode 100644
index 0000000..acc69c1
--- /dev/null
+++ b/rego-proofs/Rego/lakefile.lean
@@ -0,0 +1,14 @@
+import Lake
+open Lake DSL
+
+package «rego» {
+  -- add any package configuration options here
+}
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
+
+@[default_target]
+lean_lib «Rego» {
+  -- add any library configuration options here
+}