Prepare to replay XACML repository on top of this one

60 files changed, 1 insertions, 1 deletions

diff --git a/.deps/guile-lens b/rego-proofs/.deps/guile-lens
-Subproject 14b15d07255f9d3f55d40a3b750d13c9ee3a154
+Subproject 14b15d07255f9d3f55d40a3b750d13c9ee3a154
diff --git a/.deps/minikanren b/rego-proofs/.deps/minikanren
-Subproject e844d85512f8c055d3f96143ee506007389a25e
+Subproject e844d85512f8c055d3f96143ee506007389a25e
diff --git a/.dir-locals.el b/rego-proofs/.dir-locals.el
index 674c33e..674c33e 100644
--- a/.dir-locals.el
+++ b/rego-proofs/.dir-locals.el
diff --git a/Rego/.gitignore b/rego-proofs/Rego/.gitignore
index 20c60d7..20c60d7 100644
--- a/Rego/.gitignore
+++ b/rego-proofs/Rego/.gitignore
diff --git a/Rego/Rego.lean b/rego-proofs/Rego/Rego.lean
index ce52b89..ce52b89 100644
--- a/Rego/Rego.lean
+++ b/rego-proofs/Rego/Rego.lean
diff --git a/Rego/lake-manifest.json b/rego-proofs/Rego/lake-manifest.json
index 9b0ab31..9b0ab31 100644
--- a/Rego/lake-manifest.json
+++ b/rego-proofs/Rego/lake-manifest.json
diff --git a/Rego/lakefile.lean b/rego-proofs/Rego/lakefile.lean
index acc69c1..acc69c1 100644
--- a/Rego/lakefile.lean
+++ b/rego-proofs/Rego/lakefile.lean
diff --git a/compiler.scm b/rego-proofs/compiler.scm
index 327c823..8deb14c 100755
--- a/compiler.scm
+++ b/rego-proofs/compiler.scm
@@ -24,6 +24,6 @@
   (add-to-load-path (string-join (list current-directory ".deps" "minikanren")
                                  file-name-separator-string)))
 
-(use-modules (compiler main))
+(use-modules (compiler-rewrite main))
 
 (main (program-arguments))
diff --git a/compiler/lean.scm b/rego-proofs/compiler/lean.scm
index 39af35f..39af35f 100644
--- a/compiler/lean.scm
+++ b/rego-proofs/compiler/lean.scm
diff --git a/compiler/main.scm b/rego-proofs/compiler/main.scm
index 87d057a..87d057a 100644
--- a/compiler/main.scm
+++ b/rego-proofs/compiler/main.scm
diff --git a/compiler/passes/bool-to-prop.scm b/rego-proofs/compiler/passes/bool-to-prop.scm
index 4c2fb95..4c2fb95 100644
--- a/compiler/passes/bool-to-prop.scm
+++ b/rego-proofs/compiler/passes/bool-to-prop.scm
diff --git a/compiler/passes/compile-constraints.scm b/rego-proofs/compiler/passes/compile-constraints.scm
index 3e7b16b..3e7b16b 100644
--- a/compiler/passes/compile-constraints.scm
+++ b/rego-proofs/compiler/passes/compile-constraints.scm
diff --git a/compiler/passes/compile-definition.scm b/rego-proofs/compiler/passes/compile-definition.scm
index b9f7ce8..b9f7ce8 100644
--- a/compiler/passes/compile-definition.scm
+++ b/rego-proofs/compiler/passes/compile-definition.scm
diff --git a/compiler/passes/compile-exists-some.scm b/rego-proofs/compiler/passes/compile-exists-some.scm
index 82849e3..82849e3 100644
--- a/compiler/passes/compile-exists-some.scm
+++ b/rego-proofs/compiler/passes/compile-exists-some.scm
diff --git a/compiler/passes/compile-for-all.scm b/rego-proofs/compiler/passes/compile-for-all.scm
index ccc4185..ccc4185 100644
--- a/compiler/passes/compile-for-all.scm
+++ b/rego-proofs/compiler/passes/compile-for-all.scm
diff --git a/compiler/passes/compile-funcall.scm b/rego-proofs/compiler/passes/compile-funcall.scm
index 28dfdc1..28dfdc1 100644
--- a/compiler/passes/compile-funcall.scm
+++ b/rego-proofs/compiler/passes/compile-funcall.scm
diff --git a/compiler/passes/compile-local-references.scm b/rego-proofs/compiler/passes/compile-local-references.scm
index 42d4585..42d4585 100644
--- a/compiler/passes/compile-local-references.scm
+++ b/rego-proofs/compiler/passes/compile-local-references.scm
diff --git a/compiler/passes/compile-object-literal.scm b/rego-proofs/compiler/passes/compile-object-literal.scm
index 3daa69c..3daa69c 100644
--- a/compiler/passes/compile-object-literal.scm
+++ b/rego-proofs/compiler/passes/compile-object-literal.scm
diff --git a/compiler/passes/compile-reference.scm b/rego-proofs/compiler/passes/compile-reference.scm
index 0d28206..0d28206 100644
--- a/compiler/passes/compile-reference.scm
+++ b/rego-proofs/compiler/passes/compile-reference.scm
diff --git a/compiler/passes/emit-specification.scm b/rego-proofs/compiler/passes/emit-specification.scm
index ae0ee45..ae0ee45 100644
--- a/compiler/passes/emit-specification.scm
+++ b/rego-proofs/compiler/passes/emit-specification.scm
diff --git a/compiler/passes/extract-identifiers.scm b/rego-proofs/compiler/passes/extract-identifiers.scm
index af8694b..af8694b 100644
--- a/compiler/passes/extract-identifiers.scm
+++ b/rego-proofs/compiler/passes/extract-identifiers.scm
diff --git a/compiler/passes/lift-comprehensions.scm b/rego-proofs/compiler/passes/lift-comprehensions.scm
index c3840d2..c3840d2 100644
--- a/compiler/passes/lift-comprehensions.scm
+++ b/rego-proofs/compiler/passes/lift-comprehensions.scm
diff --git a/compiler/passes/lift-implicit-anonymous.scm b/rego-proofs/compiler/passes/lift-implicit-anonymous.scm
index cb718e8..cb718e8 100644
--- a/compiler/passes/lift-implicit-anonymous.scm
+++ b/rego-proofs/compiler/passes/lift-implicit-anonymous.scm
diff --git a/compiler/passes/parse-policy.scm b/rego-proofs/compiler/passes/parse-policy.scm
index fca48f5..fca48f5 100644
--- a/compiler/passes/parse-policy.scm
+++ b/rego-proofs/compiler/passes/parse-policy.scm
diff --git a/compiler/passes/read-and-parse.scm b/rego-proofs/compiler/passes/read-and-parse.scm
index e25a7f5..e25a7f5 100644
--- a/compiler/passes/read-and-parse.scm
+++ b/rego-proofs/compiler/passes/read-and-parse.scm
diff --git a/compiler/test.scm b/rego-proofs/compiler/test.scm
index 2e822b2..2e822b2 100644
--- a/compiler/test.scm
+++ b/rego-proofs/compiler/test.scm
diff --git a/compiler/type-inference.scm b/rego-proofs/compiler/type-inference.scm
index b5f4189..b5f4189 100644
--- a/compiler/type-inference.scm
+++ b/rego-proofs/compiler/type-inference.scm
diff --git a/compiler/types.scm b/rego-proofs/compiler/types.scm
index ecb38ed..ecb38ed 100644
--- a/compiler/types.scm
+++ b/rego-proofs/compiler/types.scm
diff --git a/compiler/utilities.scm b/rego-proofs/compiler/utilities.scm
index 783d153..783d153 100644
--- a/compiler/utilities.scm
+++ b/rego-proofs/compiler/utilities.scm
diff --git a/examples/01-computable-assign-scalar.general.lean b/rego-proofs/examples/01-computable-assign-scalar.general.lean
index 91d5f59..91d5f59 100644
--- a/examples/01-computable-assign-scalar.general.lean
+++ b/rego-proofs/examples/01-computable-assign-scalar.general.lean
diff --git a/examples/01-computable-assign-scalar.prune.lean b/rego-proofs/examples/01-computable-assign-scalar.prune.lean
index 6a88cb5..6a88cb5 100644
--- a/examples/01-computable-assign-scalar.prune.lean
+++ b/rego-proofs/examples/01-computable-assign-scalar.prune.lean
diff --git a/examples/01-computable-assign-scalar.rego b/rego-proofs/examples/01-computable-assign-scalar.rego
index 89bbc82..89bbc82 100644
--- a/examples/01-computable-assign-scalar.rego
+++ b/rego-proofs/examples/01-computable-assign-scalar.rego
diff --git a/examples/02-computable-assign-composite.lean b/rego-proofs/examples/02-computable-assign-composite.lean
index b26e469..b26e469 100644
--- a/examples/02-computable-assign-composite.lean
+++ b/rego-proofs/examples/02-computable-assign-composite.lean
diff --git a/examples/02-computable-assign-composite.rego b/rego-proofs/examples/02-computable-assign-composite.rego
index bc94115..bc94115 100644
--- a/examples/02-computable-assign-composite.rego
+++ b/rego-proofs/examples/02-computable-assign-composite.rego
diff --git a/examples/03-set-defined-by-predicate.general.lean b/rego-proofs/examples/03-set-defined-by-predicate.general.lean
index 42f8dec..42f8dec 100644
--- a/examples/03-set-defined-by-predicate.general.lean
+++ b/rego-proofs/examples/03-set-defined-by-predicate.general.lean
diff --git a/examples/03-set-defined-by-predicate.prune.lean b/rego-proofs/examples/03-set-defined-by-predicate.prune.lean
index 9532463..9532463 100644
--- a/examples/03-set-defined-by-predicate.prune.lean
+++ b/rego-proofs/examples/03-set-defined-by-predicate.prune.lean
diff --git a/examples/03-set-defined-by-predicate.rego b/rego-proofs/examples/03-set-defined-by-predicate.rego
index 185bf89..185bf89 100644
--- a/examples/03-set-defined-by-predicate.rego
+++ b/rego-proofs/examples/03-set-defined-by-predicate.rego
diff --git a/examples/04-rule-free-variables.general.lean b/rego-proofs/examples/04-rule-free-variables.general.lean
index 49b012a..49b012a 100644
--- a/examples/04-rule-free-variables.general.lean
+++ b/rego-proofs/examples/04-rule-free-variables.general.lean
diff --git a/examples/04-rule-free-variables.prune.lean b/rego-proofs/examples/04-rule-free-variables.prune.lean
index dd406a1..dd406a1 100644
--- a/examples/04-rule-free-variables.prune.lean
+++ b/rego-proofs/examples/04-rule-free-variables.prune.lean
diff --git a/examples/04-rule-free-variables.rego b/rego-proofs/examples/04-rule-free-variables.rego
index 695fc94..695fc94 100644
--- a/examples/04-rule-free-variables.rego
+++ b/rego-proofs/examples/04-rule-free-variables.rego
diff --git a/examples/05-head-subset-rule.general.lean b/rego-proofs/examples/05-head-subset-rule.general.lean
index b0d8f43..b0d8f43 100644
--- a/examples/05-head-subset-rule.general.lean
+++ b/rego-proofs/examples/05-head-subset-rule.general.lean
diff --git a/examples/05-head-subset-rule.prune.lean b/rego-proofs/examples/05-head-subset-rule.prune.lean
index 1d051eb..1d051eb 100644
--- a/examples/05-head-subset-rule.prune.lean
+++ b/rego-proofs/examples/05-head-subset-rule.prune.lean
diff --git a/examples/05-head-subset-rule.rego b/rego-proofs/examples/05-head-subset-rule.rego
index 3d43a67..3d43a67 100644
--- a/examples/05-head-subset-rule.rego
+++ b/rego-proofs/examples/05-head-subset-rule.rego
diff --git a/examples/06-complex-set-membership.general.lean b/rego-proofs/examples/06-complex-set-membership.general.lean
index 16c8e07..16c8e07 100644
--- a/examples/06-complex-set-membership.general.lean
+++ b/rego-proofs/examples/06-complex-set-membership.general.lean
diff --git a/examples/06-complex-set-membership.prune.lean b/rego-proofs/examples/06-complex-set-membership.prune.lean
index 2014588..2014588 100644
--- a/examples/06-complex-set-membership.prune.lean
+++ b/rego-proofs/examples/06-complex-set-membership.prune.lean
diff --git a/examples/06-complex-set-membership.rego b/rego-proofs/examples/06-complex-set-membership.rego
index 5f95708..5f95708 100644
--- a/examples/06-complex-set-membership.rego
+++ b/rego-proofs/examples/06-complex-set-membership.rego
diff --git a/examples/07-rule-with-dynamic-type.general.lean b/rego-proofs/examples/07-rule-with-dynamic-type.general.lean
index 80f9d86..80f9d86 100644
--- a/examples/07-rule-with-dynamic-type.general.lean
+++ b/rego-proofs/examples/07-rule-with-dynamic-type.general.lean
diff --git a/examples/07-rule-with-dynamic-type.prune.lean b/rego-proofs/examples/07-rule-with-dynamic-type.prune.lean
index ce1df37..ce1df37 100644
--- a/examples/07-rule-with-dynamic-type.prune.lean
+++ b/rego-proofs/examples/07-rule-with-dynamic-type.prune.lean
diff --git a/examples/07-rule-with-dynamic-type.rego b/rego-proofs/examples/07-rule-with-dynamic-type.rego
index c213ade..c213ade 100644
--- a/examples/07-rule-with-dynamic-type.rego
+++ b/rego-proofs/examples/07-rule-with-dynamic-type.rego
diff --git a/examples/08-object-comprehension.lean b/rego-proofs/examples/08-object-comprehension.lean
index 3425fa9..3425fa9 100644
--- a/examples/08-object-comprehension.lean
+++ b/rego-proofs/examples/08-object-comprehension.lean
diff --git a/examples/08-object-comprehension.rego b/rego-proofs/examples/08-object-comprehension.rego
index 8602c90..8602c90 100644
--- a/examples/08-object-comprehension.rego
+++ b/rego-proofs/examples/08-object-comprehension.rego
diff --git a/examples/09-simple-policy-combinator.lean b/rego-proofs/examples/09-simple-policy-combinator.lean
index 4e932a6..4e932a6 100644
--- a/examples/09-simple-policy-combinator.lean
+++ b/rego-proofs/examples/09-simple-policy-combinator.lean
diff --git a/examples/09-simple-policy-combinator.rego b/rego-proofs/examples/09-simple-policy-combinator.rego
index f840139..f840139 100644
--- a/examples/09-simple-policy-combinator.rego
+++ b/rego-proofs/examples/09-simple-policy-combinator.rego
diff --git a/examples/10-comprehensions.lean b/rego-proofs/examples/10-comprehensions.lean
index 6a6a77e..6a6a77e 100644
--- a/examples/10-comprehensions.lean
+++ b/rego-proofs/examples/10-comprehensions.lean
diff --git a/examples/10-comprehensions.rego b/rego-proofs/examples/10-comprehensions.rego
index a222299..a222299 100644
--- a/examples/10-comprehensions.rego
+++ b/rego-proofs/examples/10-comprehensions.rego
diff --git a/examples/11-with-keyword.rego b/rego-proofs/examples/11-with-keyword.rego
index bdb43b4..bdb43b4 100644
--- a/examples/11-with-keyword.rego
+++ b/rego-proofs/examples/11-with-keyword.rego
diff --git a/examples/12-some-keyword.rego b/rego-proofs/examples/12-some-keyword.rego
index c6e31b8..c6e31b8 100644
--- a/examples/12-some-keyword.rego
+++ b/rego-proofs/examples/12-some-keyword.rego
diff --git a/examples/13-else-keyword.rego b/rego-proofs/examples/13-else-keyword.rego
index f04887a..f04887a 100644
--- a/examples/13-else-keyword.rego
+++ b/rego-proofs/examples/13-else-keyword.rego
diff --git a/paper/methodology.org b/rego-proofs/paper/methodology.org
index 25ef4f5..25ef4f5 100644
--- a/paper/methodology.org
+++ b/rego-proofs/paper/methodology.org
diff --git a/run-tests.scm b/rego-proofs/run-tests.scm
index dbc5da2..dbc5da2 100755
--- a/run-tests.scm
+++ b/rego-proofs/run-tests.scm