diff options
39 files changed, 18 insertions, 2973 deletions
diff --git a/rego-proofs/compiler-rewrite/bin/dune b/rego-proofs/compiler-rewrite/bin/dune deleted file mode 100644 index a53c710..0000000 --- a/rego-proofs/compiler-rewrite/bin/dune +++ /dev/null @@ -1,5 +0,0 @@ -(executable - (public_name compiler_rewrite) - (name main) - (libraries core compiler_rewrite)) - diff --git a/rego-proofs/compiler-rewrite/test/dune b/rego-proofs/compiler-rewrite/test/dune deleted file mode 100644 index 63a9a47..0000000 --- a/rego-proofs/compiler-rewrite/test/dune +++ /dev/null @@ -1,3 +0,0 @@ -(test - (name compiler_rewrite) - (libraries alcotest compiler_rewrite core)) diff --git a/rego-proofs/compiler.scm b/rego-proofs/compiler.scm deleted file mode 100755 index 8deb14c..0000000 --- a/rego-proofs/compiler.scm +++ /dev/null @@ -1,29 +0,0 @@ -#!/usr/bin/guile -s -!# - -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(let ((current-directory (dirname (current-filename)))) - (add-to-load-path current-directory) - (add-to-load-path (string-join (list current-directory ".deps" "guile-lens") - file-name-separator-string)) - (add-to-load-path (string-join (list current-directory ".deps" "minikanren") - file-name-separator-string))) - -(use-modules (compiler-rewrite main)) - -(main (program-arguments)) diff --git a/rego-proofs/compiler-rewrite/.gitignore b/rego-proofs/compiler/.gitignore index e35d885..e35d885 100644 --- a/rego-proofs/compiler-rewrite/.gitignore +++ b/rego-proofs/compiler/.gitignore diff --git a/rego-proofs/compiler-rewrite/.ocamlformat b/rego-proofs/compiler/.ocamlformat index c870de9..c870de9 100644 --- a/rego-proofs/compiler-rewrite/.ocamlformat +++ b/rego-proofs/compiler/.ocamlformat diff --git a/rego-proofs/compiler/bin/dune b/rego-proofs/compiler/bin/dune new file mode 100644 index 0000000..2676d29 --- /dev/null +++ b/rego-proofs/compiler/bin/dune @@ -0,0 +1,5 @@ +(executable + (public_name compiler) + (name main) + (libraries core compiler)) + diff --git a/rego-proofs/compiler-rewrite/bin/main.ml b/rego-proofs/compiler/bin/main.ml index b5f04fa..f1b213c 100644 --- a/rego-proofs/compiler-rewrite/bin/main.ml +++ b/rego-proofs/compiler/bin/main.ml @@ -1,7 +1,7 @@ open Core -open Compiler_rewrite.Ast -open Compiler_rewrite.Compiler -open Compiler_rewrite.Lean +open Compiler +open Compiler__.Ast +open Compiler__.Lean let () = let file_name = Array.get (Sys.get_argv ()) 1 in diff --git a/rego-proofs/compiler-rewrite/compiler_rewrite.opam b/rego-proofs/compiler/compiler.opam index 8dbe763..8dbe763 100644 --- a/rego-proofs/compiler-rewrite/compiler_rewrite.opam +++ b/rego-proofs/compiler/compiler.opam diff --git a/rego-proofs/compiler-rewrite/dune-project b/rego-proofs/compiler/dune-project index e989552..dc06bf3 100644 --- a/rego-proofs/compiler-rewrite/dune-project +++ b/rego-proofs/compiler/dune-project @@ -1,6 +1,6 @@ (lang dune 3.11) -(name compiler_rewrite) +(name compiler) (generate_opam_files true) @@ -9,6 +9,6 @@ (maintainers "Jakob Kreuze") (package - (name compiler_rewrite) + (name compiler) (synopsis "Compiler from Rego to a Lean shallow embedding") (depends ocaml dune)) diff --git a/rego-proofs/compiler/lean.scm b/rego-proofs/compiler/lean.scm deleted file mode 100644 index 39af35f..0000000 --- a/rego-proofs/compiler/lean.scm +++ /dev/null @@ -1,374 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler lean) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler types) - #:use-module (compiler utilities) ; for subscript-digits - #:use-module (ice-9 match) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (oop goops) - #:export (<lean-predicate> - <lean-fact> - <lean-computable-definition> - <lean-expression> - <lean-exists> - <lean-for-all> - <lean-conjunction> - <lean-compare> - <lean-funcall> - <lean-intro-locals> - <lean-assignment-chain> - <lean-option> - <lean-tuple> - - compile - - lean-expression? - - lean-builtin-function? - reference->lean-name)) - -;; For inductive predicates -(define-class <lean-predicate> () - ;; the sort object in question encoded by this predicate - (kind #:init-keyword #:kind - #:getter kind) - (name #:init-keyword #:name - #:getter name) - (subject #:init-keyword #:subject - #:getter subject) - ;; fallback rule, if any - (default #:init-keyword #:default - #:getter default) - ;; other rules of inference for the predicate - (facts #:init-keyword #:facts - #:getter facts)) - -;; Arm of an inductive predicate -(define-class <lean-fact> () - ;; if `body' is true, then the predicate is true for `conclusion' - (conclusion #:init-keyword #:conclusion - #:getter conclusion) - (body #:init-keyword #:body - #:getter body)) - -;; A Lean `def' form -(define-class <lean-computable-definition> () - (identifier #:init-keyword #:identifier) - (type #:init-keyword #:type) - (value #:init-keyword #:value)) - -(define-class <lean-expression> ()) - -;; Compiled to ∃ -(define-class <lean-exists> (<lean-expression>) - ;; list of identifier/type pairs - (variables #:init-keyword #:variables - #:getter variables) - (body #:init-keyword #:body - #:getter body)) - -(define-method (tree-map (form <lean-exists>) f scope breadcrumb) - (match form - (($ <lean-exists> variables body) - (let ((inner (with-modified-slot form 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∀ -(define-class <lean-for-all> (<lean-expression>) - ;; list of identifier/type pairs - (variables #:init-keyword #:variables - #:getter variables) - (body #:init-keyword #:body - #:getter body)) - -(define-method (tree-map (form <lean-for-all>) f scope breadcrumb) - (match form - (($ <lean-for-all> variables body) - (let ((inner (with-modified-slot form 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∧ -(define-class <lean-conjunction> (<lean-expression>) - (clauses #:init-keyword #:clauses - #:getter clauses)) - -(define-method (tree-map (form <lean-conjunction>) f scope breadcrumb) - (match form - (($ <lean-conjunction> clauses) - (let ((inner (with-modified-slot form 'clauses - (tree-map clauses f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∨ -(define-class <lean-disjunction> (<lean-expression>) - (clauses #:init-keyword #:clauses - #:getter clauses)) - -(define-method (tree-map (form <lean-disjunction>) f scope breadcrumb) - (match form - (($ <lean-disjunction> clauses) - (let ((inner (with-modified-slot form 'clauses - (tree-map clauses f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; `Prop'-producing comparison between two Lean values -(define-class <lean-compare> (<lean-expression>) - (kind #:init-keyword #:kind - #:getter kind) - (left #:init-keyword #:left - #:getter left) - (right #:init-keyword #:right - #:getter right)) - -(define-method (tree-map (form <lean-compare>) f scope breadcrumb) - (match form - (($ <lean-compare> kind left right) - (let ((new (make <lean-compare> - #:kind kind - #:left (tree-map left f scope breadcrumb) - #:right (tree-map right f scope breadcrumb)))) - (f scope breadcrumb new))))) - -;; Expression arising from a call to computable Lean function -(define-class <lean-funcall> (<lean-expression>) - (name #:init-keyword #:name - #:getter name) - (args #:init-keyword #:args - #:getter args)) - -(define-method (tree-map (form <lean-funcall>) f scope breadcrumb) - (match form - (($ <lean-funcall> name args) - (let* ((inner (with-modified-slot form 'name - (tree-map name f scope breadcrumb))) - (inner (with-modified-slot form 'args - (tree-map args f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Introduction of local identifiers; compiled to a `let' statement -(define-class <lean-intro-locals> (<lean-expression>) - ;; List of (name value) pairs - (identifiers #:init-keyword #:identifiers - #:getter identifiers) - (body #:init-keyword #:body - #:accessor inner)) - -;; Compiled to `do { let iname₁ ← expr₁; ... pure (expr_{n + 1}) }' -(define-class <lean-assignment-chain> (<lean-expression>) - (identifiers #:init-keyword #:identifiers - #:getter identifiers)) - -;; Is this needed? -(define-class <lean-option> (<lean-expression>)) - -(define-class <lean-tuple> (<lean-expression>) - (items #:init-keyword #:items - #:getter items)) - - - - -(define-generic compile) - -;; Caller responsible for parenthesizing expressions. - -(define (wrap s) - (string-concatenate (list "(" s ")"))) - -(define-method (compile (x <lean-predicate>)) - (define has-default (default x)) - (define conditional-facts - (filter (lambda (fact) - (not (equal? fact (default x)))) - (facts x))) - - (with-output-to-string - (lambda () - (format #t "inductive ~a (~a : Rego.Any) : Prop" (name x) (subject x)) - (newline) - - (when has-default - (format #t "| default : ¬ (~a) → ~a ~a" - (compile (make <lean-disjunction> ; ¬ (~a) - #:clauses (map body conditional-facts))) - (name x) ; → ~a ~a - (subject x)) - (newline)) - - (for-each - (lambda (rule i) - (format #t "| rule~a : ~a → ~a ~a" - (number->subscript i) ; rule~a - (compile (clauses rule)) ; ~a → - (name x) ; → ~a - (subject x)) - (newline)) - conditional-facts - (iota (length conditional-facts)))))) - -(define-method (compile (x <lean-compare>)) - (define symbol - (match (kind x) - ('eq "=") - ('gt ">") - ('ge "≥") - ('lt "<") - ('le "≤"))) - (string-concatenate `(,(wrap (compile (left x))) " " - ,symbol " " - ,(wrap (compile (right x)))))) - -(define-method (compile (x <lean-exists>)) - (string-concatenate - `("∃ " - ,(string-join - (map (lambda (identifier) - (format #f "(~a : Rego.Any)" (compile identifier))) - (variables x)) - " ") - ", " - ,(wrap (compile (body x)))))) - -(define-method (compile (x <lean-for-all>)) - (string-concatenate - `("∀ " - ,(string-join - (map (lambda (identifier) - (format #f "(~a : Rego.Any)" (compile identifier))) - (variables x)) - " ") - ", " - ,(wrap (compile (body x)))))) - -(define-method (compile (x <lean-funcall>)) - (string-concatenate - `(,(name x) - " " - ,(string-join (map (compose wrap compile) (args x)) " ")))) - -(define-method (compile (x <lean-intro-locals>)) - (string-concatenate - `("(" - ,(string-join - (map (match-lambda - ((name value) (format #f "let ~a := ~a" (compile name) (compile value)))) - (identifiers x)) - "; ") - "; " - ,(compile (inner x)) - ")"))) - -(define-method (compile (x <lean-conjunction>)) - (string-join (map (compose wrap compile) (clauses x)) " ∧ ")) - -(define-method (compile (x <lean-disjunction>)) - (string-join (map (compose wrap compile) (clauses x)) " ∨ ")) - -(define-method (compile (x <lean-tuple>)) - (string-concatenate - `("(" - ,(string-join (map (compose wrap compile) (items x)) ", ") - ")"))) - -(define-method (compile (x <variable-ref>)) - (match x - (($ <variable-ref> name) name))) - -(define-method (compile (x <constant>)) - (match x - (($ <constant> value) (compile value)))) - -(define-method (compile (x <set-literal>)) - (match x - (($ <set-literal> elems) - (assert (equal? elems (delete-duplicates! elems))) - (format #f "(Rego.Any.set [~a])" (string-join (map compile elems) ", "))))) - -;; TODO: Remove me. -(define-method (compile (x <reference>)) - (define recur - (match-lambda - ((($ <constant> idx) rest ...) - (cond ((string? idx) (format #f ".~a~a" idx (recur rest))) - ((number? idx) (format #f "[~a]~a" idx (recur rest))) - (else (format #f "(~a)~a" (compile idx) (recur rest))))) - ((y rest ...) - (format #f "[~a]~a" (compile y) (recur rest))) - ('() ""))) - (match x - (($ <reference> parts) (format #f "~a~a" - (compile (first parts)) - (recur (drop parts 1)))))) - -(define-method (compile (x <lean-assignment-chain>)) - (define intermediate-assignments - (map (match-lambda - ((identifier-name expr) (format #f "~a ← ~a" (compile identifier-name) (compile expr)))) - (identifiers x))) - (format #f "do { ~a; pure (~a) }" - (string-join intermediate-assignments "; ") - (compile (car (last (identifiers x)))))) - -(define-method (compile (x <boolean>)) - (format #f "Rego.Any.bool ~a" (if x "True" "False"))) - -(define-method (compile (x <string>)) - (format #f "Rego.Any.str \"~a\"" x)) - -(define-method (compile (x <number>)) - (format #f "Rego.Any.num ~a" x)) - -(define-method (compile (x <list>)) - (format #f "[~a]" (string-join (map compile x) ", "))) - -(define-method (compile (x <vector>)) - (format #f "#[~a]" (string-join (map compile (array->list x)) ", "))) - - - -(define (lean-expression? expr) - (or (is-a? expr <lean-expression>) - (boolean? expr) - (string? expr) - (number? expr))) - -(define (instance->sexp inst) - (cons (class-name (class-of inst)) - (map (compose (cut slot-ref inst <>) slot-definition-name) - (class-slots (class-of inst))))) - - - -(define (lean-builtin-function? lean-name) - "Whether LEAN-NAME is a function provided by the Rego library or Lean prelude" - (member lean-name '("Array.contains"))) - -(define (sanitize s) - s) - -(define (reference->lean-name reference) - (match reference - (($ <reference> (x)) (sanitize x)) - (($ <reference> (x xs ...)) - (if (and (equal? (to-pretty-sexp x) `(<variable-ref> "internal")) - (equal? (to-pretty-sexp xs) (list `(<constant> "member_2")))) - "Array.contains" - (error "Unimplemented"))))) diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler/lib/ast.ml index 98d8375..98d8375 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.ml +++ b/rego-proofs/compiler/lib/ast.ml diff --git a/rego-proofs/compiler-rewrite/lib/ast.mli b/rego-proofs/compiler/lib/ast.mli index 514d5da..514d5da 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.mli +++ b/rego-proofs/compiler/lib/ast.mli diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler/lib/compiler.ml index 3b0384a..3b0384a 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler/lib/compiler.ml diff --git a/rego-proofs/compiler-rewrite/lib/compiler.mli b/rego-proofs/compiler/lib/compiler.mli index 0bef961..0bef961 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.mli +++ b/rego-proofs/compiler/lib/compiler.mli diff --git a/rego-proofs/compiler-rewrite/lib/dune b/rego-proofs/compiler/lib/dune index 72a5e68..139237e 100644 --- a/rego-proofs/compiler-rewrite/lib/dune +++ b/rego-proofs/compiler/lib/dune @@ -1,5 +1,5 @@ (library - (name compiler_rewrite) + (name compiler) (libraries core unix yojson) (preprocess (pps ppx_deriving.eq ppx_deriving.show ppx_fields_conv))) diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler/lib/lean.ml index 6bb4265..6bb4265 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.ml +++ b/rego-proofs/compiler/lib/lean.ml diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler/lib/lean.mli index f6a769a..f6a769a 100644 --- a/rego-proofs/compiler-rewrite/lib/lean.mli +++ b/rego-proofs/compiler/lib/lean.mli diff --git a/rego-proofs/compiler/main.scm b/rego-proofs/compiler/main.scm deleted file mode 100644 index 87d057a..0000000 --- a/rego-proofs/compiler/main.scm +++ /dev/null @@ -1,65 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler main) - #:use-module (compiler passes bool-to-prop) - #:use-module (compiler passes compile-constraints) - #:use-module (compiler passes compile-definition) - #:use-module (compiler passes compile-exists-some) - #:use-module (compiler passes compile-for-all) - #:use-module (compiler passes compile-funcall) - #:use-module (compiler passes compile-local-references) - #:use-module (compiler passes compile-object-literal) - #:use-module (compiler passes compile-reference) - #:use-module (compiler passes emit-specification) - #:use-module (compiler passes extract-identifiers) - #:use-module (compiler passes lift-comprehensions) - #:use-module (compiler passes lift-implicit-anonymous) - #:use-module (compiler passes parse-policy) - #:use-module (compiler passes read-and-parse) - #:use-module (compiler utilities) - #:use-module (ice-9 pretty-print) - #:use-module (srfi srfi-1) - #:export (main)) - -(define (main args) - "Entry point to the transpiler - -In normal interactive usage, it is expected that `args' is the result -of `(program-arguments)'." - (unless (= 2 (length args)) - (format (current-error-port) "usage: ~a [REGO-POLICY]~%" (first args)) - (quit 1)) - (let ((policy-file-name (second args))) - (unless (file-exists? policy-file-name) - (format (current-error-port) "file does not exist: ~a~%" policy-file-name) - (quit 1)) - (let* ((ast (read-and-parse policy-file-name)) - (policy (parse-policy ast)) - (policy (add-rules-to-scope policy)) - (policy (compile-definition policy)) - (policy (compile-comprehensions policy)) - (policy (compile-exists-some policy)) - (policy (lift-implicit-anonymous policy)) - (policy (compile-for-all policy)) - (policy (compile-object-literal policy)) - (policy (compile-constraints policy)) - (policy (compile-funcall policy)) - (policy (compile-reference policy)) - (policy (compile-bool-to-prop policy)) - (policy (compile-local-references policy))) - (pretty-print (to-pretty-sexp policy)) - (emit-specification policy)))) diff --git a/rego-proofs/compiler/passes/bool-to-prop.scm b/rego-proofs/compiler/passes/bool-to-prop.scm deleted file mode 100644 index 4c2fb95..0000000 --- a/rego-proofs/compiler/passes/bool-to-prop.scm +++ /dev/null @@ -1,51 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes bool-to-prop) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:export (compile-bool-to-prop)) - -(define (compile-bool-to-prop policy) - (define (rewrite-top-level form) - (match form - (($ <constant> value) - (if (boolean? value) - (make <lean-compare> - #:kind 'eq - #:left form - #:right (make <constant> #:value #t)) - form)) - (($ <lean-assignment-chain> value) - (make <lean-compare> - #:kind 'eq - #:left form - #:right (make <constant> #:value #t))) - (_ form))) - (policy-map - policy - (lambda (_scope _breadcrumb form) - (match form - (($ <lean-conjunction> conjunction) - (make <lean-conjunction> - #:clauses (map rewrite-top-level conjunction))) - (($ <for-all> _domain _key _value conjunction) - (with-modified-slot form 'body - (map rewrite-top-level conjunction))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/compile-constraints.scm b/rego-proofs/compiler/passes/compile-constraints.scm deleted file mode 100644 index 3e7b16b..0000000 --- a/rego-proofs/compiler/passes/compile-constraints.scm +++ /dev/null @@ -1,134 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-constraints) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (oop goops) - #:export (compile-constraints)) - -;; > The assignment operator (:=) is used to assign values to variables. -;; > Variables assigned inside a rule are locally scoped to that rule and shadow -;; > global variables. -;; -;; In Lean, assignment is represented as a `let'. Internally, it adds an -;; identifier to the scope. -;; -;; > Comparison (==) checks if two values are equal within a rule. If the left -;; > or right hand side contains a variable that has not been assigned a value, -;; > the compiler throws an error. -;; -;; In Lean, comparison is represented as a comparison (specifically `=') in the -;; conjunction of a rule. -;; -;; Unification (=) combines assignment and comparison. Rego will assign -;; variables to values that make the comparison true. Unification lets you ask -;; for values for variables that make an expression true. -;; -;; Unification is also represented as a comparison in Lean, just with one of the -;; sides being a free variable. - -(define (is-local-assignment? form) - (match form - ((($ <reference> (($ <variable-ref> "assign"))) left right) #t) - (_ #f))) - -(define (collapse-extents extents) - (match extents - (((singleton-form)) extents) - (((singleton-form) next ...) - (if (is-local-assignment? singleton-form) - (cons (cons singleton-form (first next)) - (collapse-extents (drop next 1))) - (cons (first extents) - (collapse-extents (drop extents 1))))) - (_ extents))) - -(define (process-local-extent scope breadcrumb xs) - (assert (list? xs)) - (if (and (positive? (length xs)) - (is-local-assignment? (first xs))) - (let ((assignments (take-while is-local-assignment? xs)) - (body (drop-while is-local-assignment? xs))) - `(,(make <lean-intro-locals> - #:identifiers - (map (match-lambda - ((($ <reference> (($ <variable-ref> "assign"))) left right) - ;; We're defining a new local, so let's add it to the scope. - (let ((local (make <local> - #:identifier left - #:lean-name left - #:constraints - (match right - (($ <reference> (right-identifier)) - `((== ,(canonicalize left breadcrumb) - ,(canonicalize right (originating-breadcrumb scope breadcrumb right-identifier))))) - (($ <variable-ref> _) - `((== ,(canonicalize left breadcrumb) - ,(canonicalize right (originating-breadcrumb scope breadcrumb right))))) - (($ <constant> value) - `((== ,(canonicalize left breadcrumb) - ,(scheme-value->type value)))) - (_ '()))))) - (add-to-scope scope breadcrumb local)) - - `(,left ,right))) - assignments) - #:body - (make <lean-conjunction> #:clauses body)))) - xs)) - -(define (process-all scope breadcrumb form) - (fold-right append '() (map (cut process-local-extent scope breadcrumb <>) - (collapse-extents (partition-on form is-local-assignment?))))) - -(define (is-assignment? scope breadcrumb left) - (match left - (($ <reference> (($ <variable-ref> identifier))) - (not (scope-contains? scope breadcrumb identifier))) - (($ <variable-ref> identifier) - (not (scope-contains? scope breadcrumb left))) - (_ #f))) - -(define (compile-constraints policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - ((($ <reference> (($ <variable-ref> name))) left right) - (if (and (string= name "assign") (is-assignment? scope breadcrumb left)) - form - (make <lean-compare> - #:kind (match name - ("assign" 'eq) - ("equal" 'eq) - ("eq" 'eq) - ("gt" 'gt) - ("gte" 'ge) - ("lt" 'lt) - ("lte" 'le)) - #:left left - #:right right))) - ((xs ...) - (if (any is-local-assignment? xs) - (process-all scope breadcrumb xs) - xs)) - (_ form))))) diff --git a/rego-proofs/compiler/passes/compile-definition.scm b/rego-proofs/compiler/passes/compile-definition.scm deleted file mode 100644 index b9f7ce8..0000000 --- a/rego-proofs/compiler/passes/compile-definition.scm +++ /dev/null @@ -1,74 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-definition) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (ice-9 pretty-print) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-11) - #:export (compile-definition)) - -(define (find-default rules) - (find default-rule? rules)) - -(define (all-but-default rules) - (let ((result (filter (negate default-rule?) rules))) - (unless (member (- (length rules) (length result)) '(0 1) ) - (error "expected at most 1 default rule, found" - (- (length rules) (length result)))) - result)) - -(define (process-rule-group rule-group) - (define subject-ref (make <variable-ref> #:name "rulesubject")) - (define (collapse-rule rule) - (match rule - (($ <rule> default head ($ <body> clauses) else-arm) - (make <lean-conjunction> - #:clauses `(,@clauses - ,(make <lean-compare> - #:left subject-ref - #:right (right head) - #:kind 'eq)))))) - (match rule-group - ((left rules ...) - (list - (make <definition> - #:left left - #:kind (kind (head (first rules))) ;; TODO: When do we rewrite as `plain'? - #:right #f - #:default (let ((default (find-default rules))) - (if default - (collapse-rule default) - default)) - #:rules (map collapse-rule (all-but-default rules))) - (variable-ref->local subject-ref))))) - -;; Convert grouped rules into a `<definition>' -(define (compile-definition policy) - (define new-scope (scope policy)) - (define new-rules - (map (lambda (rule-group) - (match (process-rule-group rule-group) - ((definition subject-ref) - (add-to-scope new-scope `(,(left definition)) subject-ref) - definition))) - (rules policy))) - (with-modified-slot (with-modified-slot policy 'rules new-rules) 'scope new-scope)) diff --git a/rego-proofs/compiler/passes/compile-exists-some.scm b/rego-proofs/compiler/passes/compile-exists-some.scm deleted file mode 100644 index 82849e3..0000000 --- a/rego-proofs/compiler/passes/compile-exists-some.scm +++ /dev/null @@ -1,89 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-exists-some) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:export (compile-exists-some)) - -(define (exists-some? form) - (is-a? form <exists-some>)) - -(define (exists-some->variables identifiers) - (map (lambda (x) - (match x - (($ <variable-ref> _) x) - (($ <funcall> - ($ <reference> - (($ <variable-ref> "internal") - ($ <constant> "member_2"))) - args) - (first args)))) - identifiers)) - -(define (exists-some->constraints identifiers) - (fold append '() - (map (lambda (x) - (match x - (($ <variable-ref> _) '()) - (($ <funcall> - ($ <reference> - (($ <variable-ref> "internal") - ($ <constant> "member_2"))) - args) - `(,x)))) - identifiers))) - -(define (process-quantified-extent scope breadcrumb xs) - (assert (list? xs)) - (if (and (positive? (length xs)) - (exists-some? (first xs))) - ;; Add any extracted variables to the scope. - (let ((variables (exists-some->variables (identifiers (first xs))))) - (for-each (lambda (variable) - (let ((local (make <local> - #:identifier variable - #:lean-name variable))) - ;; (format #t "Here: ~a~%" (to-pretty-sexp local)) - (add-to-scope scope breadcrumb local))) - variables) - - (make <lean-exists> - #:variables variables - #:body - (make <lean-conjunction> - #:clauses (append (exists-some->constraints (identifiers (first xs))) - (drop xs 1))))) - xs)) - -(define (process-all scope breadcrumb form) - (assert (list? form)) - (map (cut process-quantified-extent scope breadcrumb <>) - (partition-on form exists-some?))) - -(define (compile-exists-some policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (if (and (list? form) (any exists-some? form)) - (process-all scope breadcrumb form) - form)))) diff --git a/rego-proofs/compiler/passes/compile-for-all.scm b/rego-proofs/compiler/passes/compile-for-all.scm deleted file mode 100644 index ccc4185..0000000 --- a/rego-proofs/compiler/passes/compile-for-all.scm +++ /dev/null @@ -1,48 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-for-all) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:export (compile-for-all)) - -(define (compile-for-all policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <for-all> domain key value body) - (assert (is-a? value <variable-ref>)) - - (let ((local (variable-ref->local value))) - (add-to-scope scope breadcrumb local)) - - (make <lean-for-all> - #:variables `(,value) - #:body (make <lean-conjunction> - #:clauses - `(,(cond ;; TODO: Type inference. - (else (make <lean-funcall> - #:name "Array.contains" - #:args `(,value ,domain) - ))) - ,@body)))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/compile-funcall.scm b/rego-proofs/compiler/passes/compile-funcall.scm deleted file mode 100644 index 28dfdc1..0000000 --- a/rego-proofs/compiler/passes/compile-funcall.scm +++ /dev/null @@ -1,36 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-funcall) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:export (compile-funcall)) - -(define (compile-funcall policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <funcall> function-name args) - (assert (or (scope-contains? scope breadcrumb function-name) - (lean-builtin-function? (reference->lean-name function-name)))) - (make <lean-funcall> - #:name (reference->lean-name function-name) - #:args args)) - (anything-else anything-else))))) diff --git a/rego-proofs/compiler/passes/compile-local-references.scm b/rego-proofs/compiler/passes/compile-local-references.scm deleted file mode 100644 index 42d4585..0000000 --- a/rego-proofs/compiler/passes/compile-local-references.scm +++ /dev/null @@ -1,74 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-local-references) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (ice-9 pretty-print) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-11) - #:export (compile-local-references)) - -(define (extract-references-to-unresolved scope breadcrumb form) - ;; TODO: Document me! - (define new-identifiers (list)) - (define new-clauses (list)) - (define (recur scope breadcrumb form) - (match form - (($ <variable-ref> name) - ;; FIXME: Really, we should panic if the above fails. - ;; (unless (scope-contains? scope breadcrumb) - ;; (error "reference to unidentified variable" name)) - (let ((local (find-local scope breadcrumb form))) - (if (and local (not (resolved? local))) - (let* ((new-ident (fresh-identifier (all-valid-identifiers scope breadcrumb))) - (new-ref (make <variable-ref> #:name new-ident))) - (set! new-identifiers `(,new-ref ,@new-identifiers)) - ;; FIXME: This is syntactically a funcall but semantically something else. - (set! new-clauses `(,(make <lean-funcall> - #:name (lean-name local) - #:args `(,new-ref)) - ,@new-clauses)) - (make <variable-ref> #:name (lean-name local))) - form ; See above - ))) - (_ form))) - (let ((result (tree-map form recur scope breadcrumb))) - (values new-identifiers `(,@result ,@new-clauses)))) - -(define (compile-local-references policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <lean-conjunction> clauses) - (let-values (((new-identifiers new-clauses) (extract-references-to-unresolved scope breadcrumb clauses))) - ;; Add new identifiers to the scope. - (for-each (lambda (identifier) - (add-to-scope scope breadcrumb (variable-ref->local identifier))) - new-identifiers) - (if (positive? (length new-identifiers)) - (make <lean-conjunction> - #:clauses - `(,(make <lean-exists> - #:variables new-identifiers - #:body new-clauses))) - form))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/compile-object-literal.scm b/rego-proofs/compiler/passes/compile-object-literal.scm deleted file mode 100644 index 3daa69c..0000000 --- a/rego-proofs/compiler/passes/compile-object-literal.scm +++ /dev/null @@ -1,35 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-object-literal) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:export (compile-object-literal)) - -(define (compile-object-literal policy) - (policy-map - policy - (lambda (_scope _breadcrumb form) - (match form - (($ <constant> - ($ <object-literal> pairs)) - (make <lean-funcall> - #:name "List.toAssocList'" - #:args (list (map (lambda (x) (make <lean-tuple> #:items x)) pairs)))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/compile-reference.scm b/rego-proofs/compiler/passes/compile-reference.scm deleted file mode 100644 index 0d28206..0000000 --- a/rego-proofs/compiler/passes/compile-reference.scm +++ /dev/null @@ -1,73 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes compile-reference) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler type-inference) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:export (compile-reference)) - -(define (compile-reference policy) - - (define (specialize breadcrumb scope) - (define (recur input-identifier form new-identifiers) - (match form - ((target rest ...) - (with-anonymous-identifiers (new-identifiers target-cast-id deref-id) - (cond ((and (infer-is-a? input-identifier 'array breadcrumb scope) - (infer-is-a? input-identifier 'number breadcrumb scope)) - `((,target-cast-id ,(make <lean-funcall> - #:name "Rego.expectArray" - #:args `(,input-identifier))) - (,deref-id ,(make <lean-funcall> - #:name "Array.get?" - #:args `(,target-cast-id ,target))) - ,@(recur deref-id rest new-identifiers))) - ((and (infer-is-a? input-identifier 'set breadcrumb scope) - (infer-is-a? input-identifier 'number breadcrumb scope)) - `((,target-cast-id ,(make <lean-funcall> - #:name "Rego.expectSet" - #:args `(,input-identifier))) - (,deref-id ,(make <lean-funcall> - #:name "Array.get?" - ;; Yes, you're reading this right. Set indices start at `1', - ;; despite array indices starting at `0'. - #:args `(,target-cast-id ,target))) - ,@(recur deref-id rest new-identifiers))) - (else - `((,target-cast-id ,(make <lean-funcall> - #:name "Rego.expectObject" - #:args `(,input-identifier))) - (,deref-id ,(make <lean-funcall> - #:name "Rego.Object.ref" - #:args `(,target-cast-id ,target))) - ,@(recur deref-id rest new-identifiers)))))) - (() '()))) - recur) - - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <reference> (singleton)) - singleton) - (($ <reference> (first rest ...)) - (make <lean-assignment-chain> #:identifiers ((specialize breadcrumb scope) first rest '()))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/emit-specification.scm b/rego-proofs/compiler/passes/emit-specification.scm deleted file mode 100644 index ae0ee45..0000000 --- a/rego-proofs/compiler/passes/emit-specification.scm +++ /dev/null @@ -1,65 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes emit-specification) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-2) - #:use-module (srfi srfi-26) - #:export (emit-specification)) - -;; (define (compile-rule rule) -;; (assert (is-a? rule <rule>)) -;; (match rule -;; (($ <rule> default head ($ <body> conjunction)) -;; (make <lean-fact> -;; #:conclusion (right head) -;; #:body (if (> (length conjunction) 1) -;; (make <lean-conjunction> #:clauses (map compile-expr conjunction)) -;; (first conjunction)))))) - -(define (compile-definition definition) - (match definition - (($ <definition> kind left _right default rules) - (assert (is-a? left <reference>)) - (make <lean-predicate> - ;; TODO: Not really correct now, is it? - #:kind kind - #:name (inductive-name definition) - ;; TODO: Find unique name - #:subject "rulesubject" - #:default default - #:facts rules)))) - -(define (emit-specification policy) - "Emit a Lean file specifying the semantics of `policy'." - (assert (is-a? policy <policy>)) - (match policy - (($ <policy> package imports _ rules _) - (format #t "-- package ~a~%" package) - (newline) - (for-each (cut format #t "-- imports ~a~%" <>) imports) - (newline) - (for-each (lambda (x) - (display (compile x)) - (newline)) - (map compile-definition rules)) - (newline)))) diff --git a/rego-proofs/compiler/passes/extract-identifiers.scm b/rego-proofs/compiler/passes/extract-identifiers.scm deleted file mode 100644 index af8694b..0000000 --- a/rego-proofs/compiler/passes/extract-identifiers.scm +++ /dev/null @@ -1,82 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes extract-identifiers) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (compiler lean) - #:use-module (ice-9 match) - #:use-module (ice-9 regex) - #:use-module (lens) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (srfi srfi-69) - #:export (add-rules-to-scope)) - -(define (identify-variables policy) - ;; TODO: Document me! - (define new-scope (make <scope> #:identifiers (make-hash-table))) - ;; Identify identifiers at terminals by observing rule heads. - (for-each - (lambda (rule-group) - (for-each - (lambda (rule i) - (let* ((breadcrumb `(,(name (head rule)) ,i)) - (lhs (left (head rule))) - (rhs (right (head rule)))) - (match `(,lhs ,rhs) - ((($ <reference> (($ <variable-ref> identifier-left))) - ($ <reference> (($ <variable-ref> identifier)))) - (add-to-scope new-scope breadcrumb (variable-ref->local (first (inner rhs)))) - (let ((local (make <local> - #:identifier (first (inner lhs)) - #:lean-name (first (inner lhs)) - #:constraints - `((== ,(canonicalize identifier-left breadcrumb) - ,(canonicalize identifier breadcrumb)))))) - (add-to-scope new-scope breadcrumb local))) - ;; Deprecated form? - ((($ <reference> (($ <variable-ref> identifier-left))) - ($ <variable-ref> identifier)) - (add-to-scope new-scope breadcrumb (variable-ref->local rhs)) - (let ((local (make <local> - #:identifier (first (inner lhs)) - #:lean-name (first (inner lhs)) - #:constraints - `((== ,(canonicalize identifier-left breadcrumb) - ,(canonicalize identifier breadcrumb)))))) - (add-to-scope new-scope breadcrumb local))) - ((($ <reference> (($ <variable-ref> identifier))) - ($ <constant> value)) - (let ((local (make <local> - #:identifier (first (inner lhs)) - #:lean-name (first (inner lhs)) - #:constraints - `((== ,(canonicalize identifier breadcrumb) - ,(scheme-value->type value)))))) - (add-to-scope new-scope breadcrumb local))) - (_ #f ;; TODO: Type inference should work on object keys as well. - )))) - (cdr rule-group) - (iota (length (cdr rule-group))))) - (rules policy)) - new-scope) - -(define (add-rules-to-scope policy) - ;; TODO: Document me! - (over (ι-policy-scope) (lambda (_) (identify-variables policy)) policy)) diff --git a/rego-proofs/compiler/passes/lift-comprehensions.scm b/rego-proofs/compiler/passes/lift-comprehensions.scm deleted file mode 100644 index c3840d2..0000000 --- a/rego-proofs/compiler/passes/lift-comprehensions.scm +++ /dev/null @@ -1,72 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes lift-comprehensions) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (ice-9 pretty-print) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-11) - #:export (compile-comprehensions)) - -(define (compile-comprehensions policy) - (define new-definitions (list)) - - ;; For generating anonymous rule names. - (define top-level-names (map (compose inner first inner left) (rules policy))) - - (define (new-comprehension-definition breadcrumb comprehension) - (match comprehension - (($ <constant> ($ <comprehension> 'object key value body)) - (let* ((name (fresh-identifier top-level-names "objectcomp")) - (definition (make <definition> - #:kind 'field-eqv - #:left key - #:right value - #:default #f - #:rules (if (not (list? body)) - `(,body) - body))) - (local (make <local> - #:identifier (make <variable-ref> #:name name) - #:constraints `((== ,(canonicalize name breadcrumb) object)) - #:lean-name (make <variable-ref> #:name (format #f "~a_eqv" name))))) - (values local definition))))) - - (let ((policy - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <constant> ($ <comprehension> 'object key value body)) - (let-values (((identifier definition) (new-comprehension-definition breadcrumb form))) - ;; Add the resulting rule to the policy. - (set! new-definitions `(,definition ,@new-definitions)) - - ;; Also add it to the scope. - (add-to-scope scope breadcrumb identifier) - - ;; Make like Indiana Jones and swap this out with a reference to the - ;; new lifted object. - (make <reference> #:parts `(,(inner identifier))))) - (_ form)))))) - (match policy - (($ <policy> _package _imports _scope rules _comments) - (with-modified-slot policy 'rules - (append rules new-definitions)))))) diff --git a/rego-proofs/compiler/passes/lift-implicit-anonymous.scm b/rego-proofs/compiler/passes/lift-implicit-anonymous.scm deleted file mode 100644 index cb718e8..0000000 --- a/rego-proofs/compiler/passes/lift-implicit-anonymous.scm +++ /dev/null @@ -1,62 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes lift-implicit-anonymous) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler lean) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-11) - #:export (lift-implicit-anonymous)) - -(define (extract-anonymous-references scope breadcrumb form) - ;; FIXME: Do we need to validate that a generated name doesn't conflict with - ;; /any/ child scopes of the <conjunction>? - (define new-identifiers (list)) - (define (recur scope breadcrumb form) - (match form - (($ <variable-ref> name) - (if (string-prefix? "$" name) - (let* ((new-ident (fresh-identifier (all-valid-identifiers scope breadcrumb))) - (new-ref (make <variable-ref> #:name new-ident))) - (set! new-identifiers `(,new-ref ,@new-identifiers)) - new-ref) - form)) - (_ form))) - (let ((result (tree-map form recur scope breadcrumb))) - (values new-identifiers result))) - -(define (lift-implicit-anonymous policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ <lean-conjunction> clauses) - (let-values (((new-identifiers new-clauses) (extract-anonymous-references scope breadcrumb clauses))) - ;; Add new identifiers to the scope. - (for-each (lambda (identifier) - (add-to-scope scope breadcrumb (variable-ref->local identifier))) - new-identifiers) - (if (positive? (length new-identifiers)) - (make <lean-conjunction> - #:clauses - `(,(make <lean-exists> - #:variables new-identifiers - #:body new-clauses))) - form))) - (_ form))))) diff --git a/rego-proofs/compiler/passes/parse-policy.scm b/rego-proofs/compiler/passes/parse-policy.scm deleted file mode 100644 index fca48f5..0000000 --- a/rego-proofs/compiler/passes/parse-policy.scm +++ /dev/null @@ -1,257 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes parse-policy) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (lens) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-2) - #:use-module (srfi srfi-26) - #:use-module (srfi srfi-69) - #:export (parse-policy)) - -(define (parse-policy ast) - "Parse `ast', an abstract syntax tree from OPA, into a `<policy>'" - (assert (list? ast)) - (make <policy> - #:package (extract-package ast) - #:imports (extract-imports ast) - #:rules (extract-rules ast) - #:scope (make <scope> - #:identifiers (make-hash-table)))) - -(define (extract-package ast) - "Return, as a string, the name of the package specified by `ast'" - (define package-spec (assoc-ref ast "package")) - (define path-spec (assoc-ref package-spec "path")) - (define components - (map (lambda (component) - (assoc-ref component "value")) - (array->list path-spec))) - - ;; Ensure no component is #f - (assert (every identity components)) - - (string-join components ".")) - -(define (extract-imports ast) - "Return, as a list of strings, the package imports in `ast'" - (define import-spec (assoc-ref ast "imports")) - (define import-paths - (map (lambda (package-spec) - (assoc-ref package-spec "path")) - (if import-spec - (array->list import-spec) - '()))) - - ;; Ensure no path is #f - (assert (every identity import-paths)) - ;; Ensure every path is a `ref' - (assert (every (lambda (import-path) - (string= "ref" (assoc-ref import-path "type"))) - import-paths)) - - (let* ((values (map (cut assoc-ref <> "value") import-paths)) - (values (map array->list values))) - (map (lambda (value-list) - (string-join (map (cut assoc-ref <> "value") - value-list) - ".")) - values))) - -(define (extract-rules ast) - "Group rules in `ast' by name, parsing each into a <rule> record" - (define (recur rule) - (make <rule> - #:default (assoc-ref rule "default") - #:head (preprocess-head (assoc-ref rule "head")) - #:body (make <body> - #:conjunction (extract-conjunction (preprocess-body (assoc-ref rule "body")))) - #:else-arm (if (assoc-ref rule "else") - (recur (assoc-ref rule "else")) - #f))) - (define rules - (let ((rules (array->list (assoc-ref ast "rules")))) - (map recur rules))) - (define targets - (map (match-lambda - (($ <rule> _default head _body _else) - (left head))) - rules)) - (define result - (map (lambda (target) - (cons target - (filter (match-lambda - (($ <rule> _default head _body _else) - (equal? target (left head)))) - rules))) - targets)) - (delete-duplicates! targets) - - ;; No individual rule should have failed to extract. - (assert (every identity result)) - - result) - -(define (determine-head-kind head-obj) - "Return the appropriate symbol describing the kind of rule that `head-obj' represents - -value-eqv: assignment to a variable (varname IS value IF condition) -field-eqv: assignment to a reference (varname[field] IS value IF condition) - set-memq: assertion of set membership (varname CONTAINS value IF condition)" - (cond ((and (assoc "key" head-obj) (assoc "value" head-obj)) - 'field-eqv) - ((and (assoc "ref" head-obj) (assoc "value" head-obj)) - 'value-eqv) - ((and (assoc "key" head-obj) (assoc "ref" head-obj)) - 'set-memq) - (else (error "unidentified rule kind" head-obj)))) - -(define (preprocess-head head-obj) - ;; Head rules will sometimes have an "assign" key, but this is only when the - ;; right-hand side is a scalar value. - (define lhs (make <reference> - #:parts (preprocess-body (array->list (assoc-ref head-obj "ref"))))) - (define rhs (preprocess-body - (if (eqv? 'set-memq (determine-head-kind head-obj)) - (assoc-ref head-obj "key") - (assoc-ref head-obj "value")))) - (let ((kind (determine-head-kind head-obj))) - (make <head> - #:name (assoc-ref head-obj "name") - #:kind kind - #:lhs lhs - #:rhs rhs))) - -(define (preprocess-body body-obj) - (cond ;; Non-array strings should be turned into lists. - ((and (array? body-obj) (not (string? body-obj))) - (preprocess-body (array->list body-obj))) - ;; Objects with a `type' field represent constants in Rego, so parse - ;; them into a Scheme type. - ((and (alist? body-obj) (assoc "type" body-obj)) - (parse-literal (map-key preprocess-body "value" body-obj))) - ;; Otherwise, map over all values in the object. - ((alist? body-obj) - (map (lambda (kv) - (cons (car kv) (preprocess-body (cdr kv)))) - body-obj)) - ;; Recurse on list. - ((list? body-obj) (map preprocess-body body-obj)) - ;; Look inside the `identifiers' of an `<exists-some>' - ((is-a? body-obj <exists-some>) (preprocess-body (identifiers body-obj))) - ;; Anything else is the identity. - (else body-obj))) - -(define (parse-literal term-obj) - "Parse into a Scheme record `term-obj' containing `type,' `value' keys" - (match (assoc-ref term-obj "type") - ("var" (parse-variable-ref term-obj)) - ("ref" (parse-reference (assoc-ref term-obj "value"))) - ("call" (let ((parts (assoc-ref term-obj "value"))) - (make <funcall> #:name (first parts) #:args (drop parts 1)))) - (_ (parse-constant term-obj)))) - -(define (pairs->object-literal pairs) - (make <object-literal> - #:pairs pairs)) - -(define (parse-constant term-obj) - "Parse a constant literal (boolean, number, string, array, set, or object)" - (let ((type (assoc-ref term-obj "type")) - (value (assoc-ref term-obj "value"))) - (make <constant> - #:value - (cond ((or (boolean? value) - (number? value) - (string? value)) value) - ((string= "array" type) (if (null? value) - #() - (list->vector value))) - ((string= "set" type) (make <set-literal> - #:elems value)) - ((string= "object" type) (pairs->object-literal value)) - ((string= "arraycomprehension" type) - (make <comprehension> - #:kind 'array - #:key (assoc-ref value "term") - #:value #f - #:body (extract-conjunction (preprocess-body (assoc-ref value "body"))))) - ((string= "setcomprehension" type) - (make <comprehension> - #:kind 'set - #:key (assoc-ref value "term") - #:value #f - #:body (extract-conjunction (preprocess-body (assoc-ref value "body"))))) - ((string= "objectcomprehension" type) - (make <comprehension> - #:kind 'object - #:key (assoc-ref value "key") - #:value (assoc-ref value "value") - #:body (extract-conjunction (preprocess-body (assoc-ref value "body"))))) - (else (error "unidentified type" type)))))) - -(define (parse-variable-ref term-obj) - "Parse a reference to a named variable" - (make <variable-ref> #:name (assoc-ref term-obj "value"))) - -(define (parse-reference ref-obj) - (assert (list? ref-obj)) - (make <reference> #:parts ref-obj)) - - - - - -(define* (extract-rule default head body #:optional else-arm) - "Extract an individual parsed rule" - (if else-arm - (make <rule> - #:default default - #:head head - #:body (make <body> #:conjunction (extract-conjunction (inner body))) - #:else-arm (apply extract-rule else-arm)) - (make <rule> - #:default default - #:head head - #:body (make <body> #:conjunction (extract-conjunction (inner body)))))) - -(define (extract-conjunction conjunction) - "Extract the body of a parsed rule" - ;; Every part of the conjunction is an alist with a `terms' field. - (assert (every alist? conjunction)) - (assert (every (lambda (part) (assoc "terms" part)) conjunction)) - (map (lambda (part) - (maybe-extract-for-all (assoc-ref part "terms"))) - conjunction)) - -(define (maybe-extract-for-all term-obj) - (if (and (alist? term-obj) (assoc "domain" term-obj)) - (make <for-all> - #:domain (assoc-ref term-obj "domain") - #:key (assoc-ref term-obj "key") - #:value (assoc-ref term-obj "value") - #:body (extract-conjunction (assoc-ref term-obj "body"))) - (maybe-extract-exists-some term-obj))) - -(define (maybe-extract-exists-some term-obj) - (if (and (alist? term-obj) (assoc "symbols" term-obj)) - (make <exists-some> #:identifiers (assoc-ref term-obj "symbols")) - term-obj)) diff --git a/rego-proofs/compiler/passes/read-and-parse.scm b/rego-proofs/compiler/passes/read-and-parse.scm deleted file mode 100644 index e25a7f5..0000000 --- a/rego-proofs/compiler/passes/read-and-parse.scm +++ /dev/null @@ -1,65 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler passes read-and-parse) - #:use-module (ice-9 popen) - #:use-module (ice-9 rdelim) - #:use-module (json) - #:use-module (rnrs base) - #:use-module (rnrs io ports) - #:export (read-and-parse - read-and-parse-string)) - -(define (call-command-with-output-error-to-string cmd) - "Invoke CMD, recording what it writes to `stdout' and `stderr' - -Multi-valued return. The first value is a string or `eof-object?' -containing the content of `stdout', and the second value is a string or -`eof-object?' containing the content of `stderr'." - (let* ((err-cons (pipe)) - (port (with-error-to-port (cdr err-cons) - (λ() (open-input-pipe cmd)))) - (_ (setvbuf (car err-cons) 'block - (* 1024 1024 16))) - (result (read-delimited "" port))) - (close-port (cdr err-cons)) - (values - result - (read-delimited "" (car err-cons))))) - -(define (read-and-parse file-name) - "Pass to read the contents of FILE-NAME and output a syntax tree" - (define-values (stdout stderr) - (call-command-with-output-error-to-string - (string-concatenate (list "opa parse -f json " file-name)))) - - ;; Fail if anything was written to stdout. - (unless (eof-object? stderr) - (display stderr)) - (assert (eof-object? stderr)) - - (json-string->scm stdout)) - -(define (read-and-parse-string code) - "Pass to read the contents of FILE-NAME and output a syntax tree" - (define quoted (with-output-to-string (lambda () (write code)))) - (define-values (stdout stderr) - (call-command-with-output-error-to-string - (string-concatenate (list "echo -ne " quoted " | opa parse -f json /dev/stdin")))) - (unless (eof-object? stderr) - (display stderr)) - (assert (eof-object? stderr)) - (json-string->scm stdout)) diff --git a/rego-proofs/compiler/test.scm b/rego-proofs/compiler/test.scm deleted file mode 100644 index 2e822b2..0000000 --- a/rego-proofs/compiler/test.scm +++ /dev/null @@ -1,500 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler test) - #:use-module (compiler passes bool-to-prop) - #:use-module (compiler passes compile-constraints) - #:use-module (compiler passes compile-exists-some) - #:use-module (compiler passes compile-for-all) - #:use-module (compiler passes compile-funcall) - #:use-module (compiler passes compile-local-references) - #:use-module (compiler passes compile-object-literal) - #:use-module (compiler passes compile-reference) - #:use-module (compiler passes emit-specification) - #:use-module (compiler passes extract-identifiers) - #:use-module (compiler passes lift-comprehensions) - #:use-module (compiler passes lift-implicit-anonymous) - #:use-module (compiler passes parse-policy) - #:use-module (compiler passes read-and-parse) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (srfi srfi-64)) - - - -(define (test-harness) - (let ((runner (test-runner-null)) - (num-passed 0) - (num-failed 0)) - (test-runner-on-test-end! runner - (lambda (runner) - (case (test-result-kind runner) - ((pass xpass) (set! num-passed (+ num-passed 1))) - ((fail xfail) (set! num-failed (+ num-failed 1))) - (else #t)))) - (test-runner-on-final! runner - (lambda (runner) - (format #t "Passing tests: ~d.~%Failing tests: ~d.~%" - num-passed num-failed))) - runner)) - -(test-runner-factory (lambda () (test-harness))) - - - -(test-begin "parsing-tests") - -(define (template-rego-code code) - "Return CODE with necessary boilerplate to be run" - (format #f "package test - -import future.keywords.contains -import future.keywords.every -import future.keywords.if -import future.keywords.in - -~a\n" code)) - -(define (template-and-parse code) - "Template CODE and run it through the parsing-adjacent passes - -Returns a `<policy>'" - (let* ((code (template-rego-code code)) - (ast (read-and-parse-string code)) - (policy (parse-policy ast))) - policy)) - -(define (select-rule policy) - "Strip all of POLICY but the single rule it defines - -Error if POLICY has more than one rule." - (match policy - (($ <policy> _package _imports _scope rules _comments) - (cadr (first rules))))) - -;; Open Policy Agent provides a specification [1] of Rego's grammar. The -;; compiler makes two passes (`preprocess-policy' and `parse-policy') to -;; transform the AST into something that's more usable from Scheme. -;; -;; This suite of tests serves as documentation for what every form in the -;; grammar should look like (roughly) after the pass. Both passes take context -;; into account, so the two forms aren't directly equivalent. -;; -;; [1]: https://www.openpolicyagent.org/docs/latest/policy-reference/#grammar - -;; module = package { import } policy -;; package = "package" ref -;; import = "import" ref [ "as" var ] -;; policy = { rule } -;; -;; ↔ -;; -;; #<<policy> package: ... imports: ... rules: ... comments: ...> -;; where -;; (string? package) -;; (and (list? imports) (every string? imports)) -;; (and (list? rules)) - -(let ((parse-result (template-and-parse "pi := 3.14159"))) - (match parse-result - (($ <policy> package imports scope rules comments) - (test-assert (string? package)) - (test-assert (and (list? imports) (every string? imports))) - (test-assert (string? package)) - (test-assert (and (list? imports) (every string? imports)))))) - -;; rule = [ "default" ] rule-head { rule-body } -;; -;; ↔ -;; -;; #<<rule> default: ... head: ... body: ... else-arm: ...> -;; where -;; (boolean? default) -;; (head? head) -;; (body? body) -;; (rule? else-arm) - -(let ((parse-result (template-and-parse "pi := 3.14159"))) - (match (select-rule parse-result) - (($ <rule> default head body) - (test-assert (boolean? default)) - (test-assert (is-a? head <head>)) - (test-assert (is-a? body <body>))))) - -(let ((parse-result (template-and-parse "phi := 3.14159 if False else := 1.61803"))) - (match (select-rule parse-result) - (($ <rule> default head body else-arm) - (test-assert (boolean? default)) - (test-assert (is-a? head <head>)) - (test-assert (is-a? body <body>)) - (test-assert (is-a? else-arm <rule>))))) - -;; rule-head = ( ref | var ) ( rule-head-set | rule-head-obj | rule-head-func | rule-head-comp ) -;; rule-head-comp = [ assign-operator term ] [ "if" ] -;; rule-head-obj = "[" term "]" [ assign-operator term ] [ "if" ] -;; rule-head-func = "(" rule-args ")" [ assign-operator term ] [ "if" ] -;; rule-args = term { "," term } -;; rule-head-set = "contains" term [ "if" ] | "[" term "]" -;; -;; ↔ -;; -;; #<<head> name: ... kind: ... lhs: ... rhs: ...> -;; where -;; (member kind '(value-eqv field-eqv set-memq)) - -(let ((parse-result (template-and-parse "pi := 3.14159"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> name kind lhs rhs) - _body) - (test-assert (eqv? kind 'value-eqv))))) - -(let ((parse-result (template-and-parse "pi contains 3.14159"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> name kind lhs rhs) - _body) - (test-assert (eqv? kind 'set-memq))))) - -(let ((parse-result (template-and-parse "pi[\"value\"] := 3.14159"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> name kind lhs rhs) - _body) - (test-assert (eqv? kind 'field-eqv))))) - -;; TODO: When implemented, write a parse test for `rule-head-func' - -;; rule-body = [ "else" [ assign-operator term ] [ "if" ] ] ( "{" query "}" ) | literal -;; -;; ↔ -;; -;; #<<body> conjunction: ...> -;; where -;; (list? conjunction) -;; -;; query = literal { ( ";" | ( [CR] LF ) ) literal } -;; -;; ↔ -;; -;; (list ...) - -(let ((parse-result (template-and-parse "pi := 3.14159"))) - (match (select-rule parse-result) - (($ <rule> - _default - _head - ($ <body> conjunction)) - (test-assert (list? conjunction))))) - -;; # Literals -;; -;; literal = ( some-decl | expr | "not" expr ) { with-modifier } - -;; with-modifier = "with" term "as" term -;; -;; ↔ -;; -;; #<<with-modifier> with: ... as: ...> - -;; TODO: When implemented, write a parse test for `with-modifier'. - -;; some-decl = "some" term { "," term } { "in" expr } -;; -;; ↔ -;; -;; #<<exists-some> terms: ...> - -(let ((parse-result (template-and-parse "q1 contains name if { some site; name := site.name }"))) - (match (select-rule parse-result) - (($ <rule> - _default - _head - ($ <body> (($ <exists-some> (($ <variable-ref> "site"))) - terms ...))) - (test-assert (list? terms))))) - -;; expr = term | expr-call | expr-infix | expr-every | expr-parens | unary-expr -;; expr-call = var [ "." var ] "(" [ expr { "," expr } ] ")" -;; expr-infix = expr infix-operator expr -;; expr-parens = "(" expr ")" -;; unary-expr = "-" expr -;; infix-operator = assign-operator | bool-operator | arith-operator | bin-operator -;; bool-operator = "==" | "!=" | "<" | ">" | ">=" | "<=" -;; arith-operator = "+" | "-" | "*" | "/" -;; bin-operator = "&" | "|" -;; assign-operator = ":=" | "=" -;; -;; ↔ -;; -;; (operator . operands) - -;; expr-every = "every" var { "," var } "in" ( term | expr-call | expr-infix ) "{" query "}" -;; -;; ↔ -;; -;; #<<for-all> domain: ... key: ... value: ... body: ...> - -(let ((parse-result (template-and-parse "q1 contains name if { every site in sites { name := site.name } }"))) - (match (select-rule parse-result) - (($ <rule> - _default - _head - ($ <body> - (($ <for-all> - ($ <variable-ref> "sites") - 'null - ($ <variable-ref> "site") - body) - terms ...))) - (test-assert (list? body)) - (test-assert (list? terms))))) - -;; membership = term [ "," term ] "in" term -;; -;; ↔ -;; -;; (#<<reference> parts: (#<<variable-ref> name: "internal">, #<<variable-ref> name: "member_2">) term ...) - -(let ((parse-result (template-and-parse "q1 contains name if { some site in sites; name := site.name }"))) - (match (select-rule parse-result) - (($ <rule> - _default - _head - ($ <body> - (($ <exists-some> - (($ <funcall> - ($ <reference> (($ <variable-ref> "internal") - ($ <constant> "member_2"))) - (($ <variable-ref> "site") - ($ <variable-ref> "sites"))))) - terms ...))) - (test-assert (list? terms))))) - -;; # Terms -;; -;; term = ref | var | scalar | array | object | set | membership | array-compr | object-compr | set-compr - -;; array-compr = "[" term "|" query "]" -;; -;; ↔ -;; -;; #<<comprehension> kind: ... key ... value ... body: ...> -;; where -;; (member? kind '(array set object)) -;; (list? body) - -(let ((parse-result (template-and-parse "namelist := [ x | some site in sites; name := site.name ]"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <comprehension> - 'array - ($ <variable-ref> "x") - #f - body))) - _body) - (test-assert (list? body))))) - -;; set-compr = "{" term "|" query "}" -;; -;; ↔ -;; -;; #<<set-compr> from: ... where: ...> -;; where -;; (list? where) - -(let ((parse-result (template-and-parse "namelist := { x | some site in sites; name := site.name }"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <comprehension> - 'set - ($ <variable-ref> "x") - #f - body))) - _body) - (test-assert (list? body))))) - -;; object-compr = "{" object-item "|" query "}" -;; -;; ↔ -;; -;; #<<object-compr> key: ... from: ... where: ...> -;; where -;; (list? where) - -(let ((parse-result (template-and-parse "namelist := { name: site | some site in sites; name := site.name }"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <comprehension> - 'object - ($ <variable-ref> "name") - ($ <variable-ref> "site") - body))) - _body) - (test-assert (list? body))))) - -;; ref = ( var | array | object | set | array-compr | object-compr | set-compr | expr-call ) { ref-arg } -;; ref-arg = ref-arg-dot | ref-arg-brack -;; ref-arg-brack = "[" ( scalar | var | array | object | set | "_" ) "]" -;; ref-arg-dot = "." var -;; -;; ↔ -;; -;; #<<reference> parts: ...> -;; where -;; (list? parts) -;; -;; var = ( ALPHA | "_" ) { ALPHA | DIGIT | "_" } -;; -;; ↔ -;; -;; #<<variable-ref> name: ...> -;; where -;; (string? name) - -(let ((parse-result (template-and-parse "newlist := site.names"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <reference> - (($ <variable-ref> "site") - ($ <constant> "names")))) - _body) - (test-assert #t)))) - -;; array = "[" term { "," term } "]" -;; -;; ↔ -;; -;; #(...) - -(let ((parse-result (template-and-parse "naturals := [1, 2, 3, 4, 5]"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - #(($ <constant> 1) - ($ <constant> 2) - ($ <constant> 3) - ($ <constant> 4) - ($ <constant> 5)))) - _body) - (test-assert #t)))) - -;; object = "{" object-item { "," object-item } "}" -;; object-item = ( scalar | ref | var ) ":" term -;; -;; ↔ -;; -;; #<<constant> value: #<<object-literal> pairs: ...>> - -(let ((parse-result (template-and-parse "naturals := { \"first\": 1, \"second\": 2 }"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <object-literal> - ((($ <constant> "first") ($ <constant> 1)) - (($ <constant> "second") ($ <constant> 2)))))) - _body) - (test-assert #t)))) - -(let ((parse-result (template-and-parse "naturals := { first: 1, second: 2 }"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <object-literal> - ((($ <variable-ref> "first") ($ <constant> 1)) - (($ <variable-ref> "second") ($ <constant> 2)))))) - _body) - (test-assert #t)))) - -;; set = empty-set | non-empty-set -;; non-empty-set = "{" term { "," term } "}" -;; empty-set = "set(" ")" -;; -;; ↔ -;; -;; #<<set-literal> elts: ...> -;; #<<set-literal> elts: '()> - -(let ((parse-result (template-and-parse "naturals := { 1, 2, 3 }"))) - (match (select-rule parse-result) - (($ <rule> - _default - ($ <head> _name _kind _lhs - ($ <constant> - ($ <set-literal> - (($ <constant> 1) ($ <constant> 2) ($ <constant> 3))))) - _body) - (test-assert #t)))) - -;; ## The following are mapped to Scheme objects - -;; scalar = string | NUMBER | TRUE | FALSE | NULL -;; string = STRING | raw-string -;; raw-string = "`" { CHAR-"`" } "`" - -(test-end "parsing-tests") - -(test-begin "integration-tests") - -(define (compile-policy policy-file-name) - (let* ((ast (read-and-parse policy-file-name)) - (policy (parse-policy ast)) - (policy (add-rules-to-scope policy)) - (policy (compile-comprehensions policy)) - (policy (compile-exists-some policy)) - (policy (lift-implicit-anonymous policy)) - (policy (compile-for-all policy)) - (policy (compile-object-literal policy)) - (policy (compile-constraints policy)) - (policy (compile-funcall policy)) - (policy (compile-reference policy)) - (policy (compile-bool-to-prop policy)) - (policy (compile-local-references policy))) - (with-output-to-string - (lambda () - (emit-specification policy))))) - -(test-equal (compile-policy "examples/01-computable-assign-scalar.rego") - "-- package data.examples.computable_assign_scalar\n\n\ninductive pi_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (Rego.Any.num 3.14159)) → pi_eqv v\n\n\n") - -(test-equal (compile-policy "examples/02-computable-assign-composite.rego") - "-- package data.examples.computable_assign_composite\n\n\ninductive rect_eqv (v : Rego.Any) : Prop\n| rule₀ : (v = (List.toAssocList' ([((Rego.Any.str \"height\"), (Rego.Any.num 4)), ((Rego.Any.str \"width\"), (Rego.Any.num 2))]))) → rect_eqv v\n\n\n") - -(test-end "integration-tests") diff --git a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml b/rego-proofs/compiler/test/compiler.ml index 1d9d926..741ae3a 100644 --- a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml +++ b/rego-proofs/compiler/test/compiler.ml @@ -1,5 +1,6 @@ open Core -open Compiler_rewrite +open Compiler +open Compiler__ module To_test = struct let extract_variables = Compiler.extract_variables_wrapper @@ -25,7 +26,6 @@ q { x := 2 } |} in - let open Compiler_rewrite.Compiler in let { bound; _ } = To_test.extract_variables (extract_query policy_code) in Alcotest.(check strings) "expected identifier list" [ "x" ] bound @@ -40,7 +40,6 @@ q { z := 4 } |} in - let open Compiler_rewrite.Compiler in let { bound; _ } = To_test.extract_variables (extract_query policy_code) in Alcotest.(check strings) "expected identifier list" [ "x"; "y"; "z" ] bound @@ -54,7 +53,6 @@ q { y := x } |} in - let open Compiler_rewrite.Compiler in let { bound; _ } = To_test.extract_variables (extract_query policy_code) in Alcotest.(check strings) "expected identifier list" [ "x"; "y" ] bound @@ -68,7 +66,6 @@ q { y == 8 } |} in - let open Compiler_rewrite.Compiler in let { free; bound; _ } = To_test.extract_variables (extract_query policy_code) in Alcotest.(check strings) "expected identifier list" [] free; @@ -84,7 +81,6 @@ q { z = 7 } |} in - let open Compiler_rewrite.Compiler in let { free; bound; _ } = To_test.extract_variables (extract_query policy_code) in Alcotest.(check strings) "expected identifier list" [ "z" ] free; @@ -92,12 +88,12 @@ q { "expected identifier list" [ "y" ] bound let test_identifier () = - let open Compiler_rewrite.Lean in + let open Lean in let ast = Identifier "test" in Alcotest.(check string) "expected string" "test" (To_test.fmt ast) let test_transform_simple_1 () = - let open Compiler_rewrite.Ast in + let open Ast in let rule = { head = ((Var "fruit", [Var "apple"; Var "seeds"]), Assignment (Assign, (Scalar (Number 12.)))); default = false; body = [Expr (Term (Scalar (Bool true)), None)]; diff --git a/rego-proofs/compiler/test/dune b/rego-proofs/compiler/test/dune new file mode 100644 index 0000000..ea3bc5f --- /dev/null +++ b/rego-proofs/compiler/test/dune @@ -0,0 +1,3 @@ +(test + (name compiler) + (libraries alcotest compiler core)) diff --git a/rego-proofs/compiler/type-inference.scm b/rego-proofs/compiler/type-inference.scm deleted file mode 100644 index b5f4189..0000000 --- a/rego-proofs/compiler/type-inference.scm +++ /dev/null @@ -1,112 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler type-inference) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler types) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (minikanren mk) - #:use-module (minikanren mkextraforms) - #:use-module (minikanren mkprelude) - #:use-module (srfi srfi-1) - #:use-module (oop goops) - #:export (infer-type - infer-is-a?)) - -;; Given a pair (x y), assert that y is a valid type for dereferencing. -(define valid-deref - (lambda (x y) - (conde - ((== x 'object) (== y 'string)) - ((== x 'array) (== y 'number)) - ((== x 'list) (== y 'number))))) - -;; `all' but not implemented as a macro. -(define primitive-all - (lambda (xs) - (match xs - (() succeed) - ((x) x) - ((x xs2 ...) - (conda (x (primitive-all xs2)) - (else fail)))))) - - - -(define types - '(null bool number string array set object - any)) - -(define constraints - '(== membero)) - -(define (normalize form) - "Return FORM with all free variables replaced with a unique `var'" - (map (lambda (x) - (if (and (symbol? x) - (not (memq x types)) - (not (memq x constraints))) - (var x) - x)) - form)) - -(define (free-variables form) - "Return all `var' forms in a normalized FORM" - (filter var? form)) - -(define (mk-variable-for constraints identifier breadcrumb) - "Search CONSTRAINTS for the minikanren variable associated with IDENTIFIER - -`breadcrumb' is necessary to uniquely identify `identifier'." - (find (lambda (x) - (eqv? (canonicalize identifier breadcrumb) - (vector-ref x 0))) - (flat-map free-variables constraints))) - -(define (evaluate-constraints constraints) - "Make CONSTRAINTS, generated by compiler passes, usable by minikanren" - (map (match-lambda - (('== args ...) (apply == args)) - (('membero args ...) (apply membero args))) - constraints)) - -(define (infer-type identifier breadcrumb scope) - "Return a list of possible types for IDENTIFIER - -`breadcrumb' is necessary to uniquely identify `identifier' within `scope'." - (let* ((constraints (collapse-constraints scope)) - (constraints (map normalize constraints)) - (variables (flat-map free-variables constraints))) - (let* ((x (var 'pairs)) - (solutions - (map-inf #f - (lambda (s) - (reify (walk* x s))) - ((primitive-all (append ;; (list (== x variables)) - `(,(== x (mk-variable-for constraints identifier breadcrumb))) - (evaluate-constraints constraints))) - empty-s)))) - (delete-duplicates! solutions)))) - -(define (infer-is-a? identifier type breadcrumb scope) - "Return whether or not we can infer IDENTIFIER to be a TYPE - -`breadcrumb' is necessary to uniquely identify `identifier' within `scope'." - (let ((possible-types (infer-type identifier breadcrumb scope))) - (if (= 1 (length possible-types)) - (eqv? type (first possible-types)) - #f))) diff --git a/rego-proofs/compiler/types.scm b/rego-proofs/compiler/types.scm deleted file mode 100644 index ecb38ed..0000000 --- a/rego-proofs/compiler/types.scm +++ /dev/null @@ -1,487 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler types) - #:use-module ((rnrs base) #:select (assert)) - #:use-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (lens) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (srfi srfi-69) - #:export (policy-map - tree-map - - <policy> - scope - rules - ι-policy-scope - ι-policy-rules - - <scope> - identifiers - with-anonymous-identifiers - add-to-scope - originating-breadcrumb - canonicalize - collapse-constraints - all-valid-identifiers - scope-contains? - find-local - - <local> - inner - constraints - lean-name - resolved? - variable-ref->local - - <definition> - - <rule> - default-rule? - head - body - ι-rule-body - inductive-name - - <head> - name - kind - left - right - - <body> - ι-body-conjunction - - <funcall> - args - - <for-all> - - <exists-some> - - <constant> - scheme-value->type - - <set-literal> - - <object-literal> - - <comprehension> - - <variable-ref> - - <reference>)) - -(define (policy-map policy f) - "Return POLICY where F has been applied to every form in the rules" - (over (ι-policy-rules) - (lambda (rule-groups) - (map (match-lambda - ;; ((group-head rules ...) - ;; `(,group-head - ;; ,@(map (lambda (rule i) - ;; (let ((breadcrumb `(,(name (head rule)) ,i))) - ;; (tree-map rule f (scope policy) breadcrumb))) - ;; rules - ;; (iota (length rules))))) - (($ <definition> kind left right default rules) - (let ((collective-rules `(,default ,@rules))) - (make <definition> - #:kind kind - #:left left - #:right right - #:default (tree-map default f (scope policy) `(,left default)) - #:rules (map (lambda (rule i) - (let ((breadcrumb `(,left ,i))) - (tree-map rule f (scope policy) breadcrumb))) - rules - (iota (length rules))))))) - rule-groups)) - policy)) - -;; `f' is called with `scope' and `breadcrumb' as auxiliary arguments. -;; -;; `scope' is a `<scope>', which gives opaque access to the variables that have -;; been defined in the policy, and any constraints we've mined thus far in the -;; compilation process. (In general, it's devoid of helpful information until -;; the `extract-identifiers' pass runs.) -;; -;; `breadcrumb' is a marker that specifies where the `form' argument exists in -;; the policy. Rego is lexically scoped, so this information is important for -;; determining which identifiers are in-scope for a particular place in the -;; program. The breadcrumb is always a list that begins with (1.) the name of -;; the current rule group and (2.) the index of the head being observed. -;; Following that is a sequence of list indices corresponding to this particular -;; path in the tree. For example: -;; -;; ("q" 0 0) -;; -;; Corresponds to the first clause in the conjunction of the first rule that -;; defines `q'. - -(define-method (tree-map form f scope breadcrumb) - form) - -(define-method (tree-map (form <list>) f scope breadcrumb) - (f scope breadcrumb - (map (lambda (x i) - (let ((breadcrumb (add-to-end breadcrumb i))) - (f scope breadcrumb (tree-map x f scope breadcrumb)))) - form - (iota (length form))))) - - - -;; Type representing an individual `.rego' file -(define-class <policy> () - (package #:init-value #f - #:init-keyword #:package) - (imports #:init-value #f - #:init-keyword #:imports) - (scope #:init-value #f - #:init-keyword #:scope - #:accessor scope) - (rules #:init-value #f - #:init-keyword #:rules - #:accessor rules) - (comments #:init-value #f - #:init-keyword #:comments)) - -;; Lens for focusing the rules of a <policy> -(define-slot-lens ι-policy-rules 'rules) - -;; Lens for focusing the global of a <policy> -(define-slot-lens ι-policy-scope 'scope) - - - -(define-class <scope> () - (identifiers #:init-keyword #:identifiers - #:accessor inner)) - -(define-class <local> () - (resolved #:init-form #f - #:init-keyword #:resolved - #:accessor resolved?) - (identifier #:init-keyword #:identifier - #:accessor inner) - (constraints #:init-form '() - #:init-keyword #:constraints - #:accessor constraints) - ;; Name of the object as it will appear in the emitted Lean code. - (lean-name #:init-keyword #:lean-name - #:accessor lean-name)) - -(define (variable-ref->local ref) - ;; TODO: Document me! - ;; - ;; This produces a dumb "it's just a name, haha" local with no constraints - ;; attached. - (make <local> #:identifier ref #:lean-name ref #:resolved #t)) - -(define-syntax with-anonymous-identifiers - (lambda (stx) - (syntax-case stx () - ((_ (new-identifiers ids ...) body ...) - (let ((let-clauses - (flat-map (lambda (id) - #`((#,(datum->syntax stx id) (fresh-identifier new-identifiers)) - (new-identifiers (cons #,(datum->syntax stx id) new-identifiers)) - (#,(datum->syntax stx id) (make <variable-ref> - #:name #,(datum->syntax stx id))))) - (syntax->datum #'(ids ...))))) - #`(let* (#,@let-clauses) - body ...)))))) - -(define (add-to-scope scope breadcrumb local) - "Add a new LOCAL to BREADCRUMB in SCOPE" - (define looking-at (hash-table-ref/default (inner scope) breadcrumb '())) - (assert (is-a? scope <scope>)) - (assert (is-a? local <local>)) - (assert (list? breadcrumb)) - (hash-table-append-item! (inner scope) breadcrumb local)) - -(define (originating-breadcrumb scope breadcrumb identifier) - "Return the part of the program in which IDENTIFIER was defined - -This is for the variable that `identifier' names in `breadcrumb' /only/. In -practice, `identifier' can refer to many distinct variables depending, on the -context, hence the restriction. - -Returns `#f' if `identifier' is not valid in `breadcrumb.'" - (define (recur breadcrumb) - (define looking-at (hash-table-ref/default (inner scope) breadcrumb '())) - (cond ((null? breadcrumb) #f) - ((assoc identifier looking-at) breadcrumb) - (else (recur (drop-right breadcrumb 1))))) - (assert (is-a? scope <scope>)) - (assert (is-a? identifier <variable-ref>)) - (assert (list? breadcrumb)) - (recur breadcrumb)) - -(define (canonicalize identifier breadcrumb) - "Return a unique symbol for IDENTIFIER - -Uniqueness is determined by the scope in which an identifier is /introduced/, so -`breadcrumb' is expected to be the region of the program where `identifier' was -defined. If this needs to be determined (i.e., for uses of identifiers aside -from definitions), `originating-breadcrumb' can determine the provenance of an -identifier." - (string->symbol - (format #f "~a.~a" - identifier - (hash (with-output-to-string - (lambda () (write `(,@breadcrumb ,identifier)))) - (* 1024 1024))))) - -(define any-type '(null bool number string array object)) - -(define (collapse-constraints scope) - "Return all constraints in SCOPE - -This is independent of context, which is okay, because the identifiers in the -resulting list of constraints are canonicalized such that they are unique and -can be associated with identifiers as they appear in the AST programmatically." - (flat-map (lambda (grouping) - (let ((breadcrumb (first grouping)) - (identifiers (drop grouping 1))) - (flat-map (lambda (local) - `((membero ,(canonicalize (inner local) breadcrumb) ,any-type) - ,@(constraints local))) - identifiers))) - (hash-table->alist (inner scope)))) - -(define (all-valid-identifiers scope breadcrumb) - "Return all identifiers that can be referenced in the scope specified by BREADCRUMB" - (define (recur breadcrumb) - (define looking-at (hash-table-ref/default (inner scope) breadcrumb '())) - (if (null? breadcrumb) - looking-at - `(,@looking-at ,@(recur (drop-right breadcrumb 1))))) - (assert (is-a? scope <scope>)) - (assert (list? breadcrumb)) - (recur breadcrumb)) - -(define (scope-contains? scope breadcrumb identifier) - "Whether SCOPE contains IDENTIFIER at the point indicated by BREADCRUMB - -`scope' is a <scope>, `breadcrumb' is a list given to the `f' of `mutate-tree', -and `identifier' is a <reference>" - (match identifier - ;; FIXME: It isn't clear to me that this is correct. There might be other - ;; variables within `parts' that also need to be validated. But, then, - ;; what's the point in using this function? - (($ <reference> parts) (cut scope-contains? scope breadcrumb (first parts))) - (($ <variable-ref> _) (member identifier (map inner (all-valid-identifiers scope breadcrumb)))) - (_ (error "type unsupp")))) - -(define (find-local scope breadcrumb name) - ;; TODO: Document me! - (find (lambda (identifier) - (equal? name (inner identifier))) - (all-valid-identifiers scope breadcrumb))) - - - -(define-class <definition> () - ;; the sort object in question encoded by this predicate - (kind #:init-keyword #:kind - #:getter kind) ; memq '(plain value-eqv field-eqv set-memq array-memq) - (left #:init-keyword #:left - #:accessor left) - (right #:init-form #f - #:init-keyword #:right - #:accessor right) - (default #:init-keyword #:default - #:accessor default) - (rules #:init-keyword #:rules - #:accessor rules)) - -;; The intensional database of a Rego program is defined by its rules. -(define-class <rule> () - (default #:init-form #f - #:init-keyword #:default - #:accessor default-rule?) - (head #:init-keyword #:head - #:accessor head) - (body #:init-keyword #:body - #:accessor body) - (else-arm #:init-form #f - #:init-keyword #:else-arm - #:accessor else-arm)) - -;; Lens for focusing the body of a <rule> -(define-slot-lens ι-rule-body 'body) - -(define-method (tree-map (form <rule>) f scope breadcrumb) - (match form - (($ <rule> default head body) - ;; A rule body introduces a new scope. - (let* ((inner (with-modified-slot form 'head - (tree-map head f scope breadcrumb))) - (inner (with-modified-slot inner 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -(define (inductive-name x) - (define suffix - (match (kind x) - ('value-eqv "_eqv") - ('field-eqv "_eqv") - ('set-memq "_memq"))) - (match (left x) - (($ <reference> (($ <variable-ref> name) _maybe-more ...)) - (string-concatenate `(,name ,suffix))))) - - - -;; A (named) relation (equality or inclusion) that holds if the body of the rule is true. -(define-class <head> () - (name #:init-keyword #:name - #:accessor name) - (kind #:init-keyword #:kind ; memq '(value-eqv field-eqv set-memq array-memq) - #:accessor kind) - (lhs #:init-keyword #:lhs - #:accessor left) - (rhs #:init-keyword #:rhs - #:accessor right)) - -(define-method (tree-map (form <head>) f scope breadcrumb) - (match form - (($ <head> name kind lhs rhs) - ;; A rule body introduces a new scope. - (let* ((inner (with-modified-slot form 'kind - (tree-map kind f scope breadcrumb))) - ;; (inner (with-modified-slot inner 'lhs - ;; (tree-map lhs f scope breadcrumb))) - (inner (with-modified-slot inner 'rhs - (tree-map rhs f scope breadcrumb)))) - (f scope breadcrumb inner))))) - - - -;; A conjunction that defines whether a rule should apply. -(define-class <body> () - (conjunction #:init-keyword #:conjunction - #:accessor inner)) - -(define-method (tree-map (form <body>) f scope breadcrumb) - (match form - (($ <body> conjunction) - (let ((inner (with-modified-slot form 'conjunction - (tree-map conjunction f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Lens for focusing the contents of a <body> -(define-slot-lens ι-body-conjunction 'conjunction) - - - -;; Call to a Rego function -(define-class <funcall> () - (ref #:init-keyword #:name ; <reference> (to the function being called) - #:accessor name) - (args #:init-keyword #:args ; list of <term> - #:accessor args)) - -;; Universal quantification over some domain of Rego values -(define-class <for-all> () - (domain #:init-keyword #:domain) - (key #:init-keyword #:key) - (value #:init-keyword #:value) - (body #:init-keyword #:body)) - -(define-method (tree-map (form <for-all>) f scope breadcrumb) - (match form - (($ <for-all> domain key value body) - (let ((inner (with-modified-slot form 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Existential quantification over some domain of Rego values -(define-class <exists-some> () - (identifiers #:init-keyword #:identifiers - #:accessor identifiers)) - -(define-method (tree-map (form <exists-some>) f scope breadcrumb) - (match form - (($ <exists-some> identifiers) - (let ((inner (with-modified-slot form 'identifiers - (map (cut tree-map <> f scope breadcrumb) - identifiers)))) - (f scope breadcrumb inner))))) - - - -;; Any literal that evaluates to itself, inclusive of comprehensions. -(define-class <constant> () - (value #:init-keyword #:value)) ; scheme value - -(define-method (tree-map (form <constant>) f scope breadcrumb) - (f scope breadcrumb form)) - -(define-class <set-literal> () - (elems #:init-keyword #:elems)) ; list of [scheme value | <set-literal> | <object-literal>] - -(define-class <object-literal> () - (pairs #:init-keyword #:pairs)) ; list of [(string, scheme value | <set-literal> | <object-literal>)] - -(define-class <comprehension> () - (kind #:init-keyword #:kind) ; one of '(array set object) - (key #:init-keyword #:key) - (value #:init-keyword #:value) - (body #:init-keyword #:body)) - -(define (scheme-value->type x) - (cond ((boolean? x) 'bool) - ((number? x) 'number) - (else 'any))) - - - -;; A place within a (possibly nested) data structure. -;; -;; As described in the documentation for `<variable-ref>', this is our semantic -;; encoding for variable dereferencing. Referring to a variable in scope would -;; be encoded as a `<reference>' containing a single `<variable-ref>'. -(define-class <reference> () - (parts #:init-keyword #:parts - #:accessor inner)) - -(define-method (equal? (x <reference>) (y <reference>)) - (equal? (inner x) (inner y))) - -(define-method (tree-map (form <reference>) f scope breadcrumb) - (match form - (($ <reference> parts) - (let ((inner (with-modified-slot form 'parts - (tree-map parts f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; A name within a lexical environment. -;; -;; Semantically, we don't treat a bare `<variable-ref>' as evaluating to the -;; value it refers to. For such an operation, we wrap the `<variable-ref>' in a -;; `<reference>'. -(define-class <variable-ref> () - (name #:init-keyword #:name ; <string> - #:accessor inner)) - -(define-method (equal? (x <variable-ref>) (y <variable-ref>)) - (equal? (inner x) (inner y))) diff --git a/rego-proofs/compiler/utilities.scm b/rego-proofs/compiler/utilities.scm deleted file mode 100644 index 783d153..0000000 --- a/rego-proofs/compiler/utilities.scm +++ /dev/null @@ -1,167 +0,0 @@ -;;; Copyright © 2023 Jakob L. Kreuze <zerodaysfordays@sdf.org> -;;; -;;; This program is free software; you can redistribute it and/or -;;; modify it under the terms of the GNU General Public License as -;;; published by the Free Software Foundation; either version 3 of the -;;; License, or (at your option) any later version. -;;; -;;; This program is distributed in the hope that it will be useful, -;;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -;;; General Public License for more details. -;;; -;;; You should have received a copy of the GNU General Public License -;;; along with this program. If not, see -;;; <http://www.gnu.org/licenses/>. - -(define-module (compiler utilities) - #:use-module (ice-9 match) - #:use-module (oop goops) - #:use-module (srfi srfi-1) - #:use-module (srfi srfi-26) - #:use-module (srfi srfi-31) - #:use-module (srfi srfi-69) - #:export (alist? - map-key - update-alist - - add-to-end - - hash-table-append! - hash-table-append-item! - - fresh-identifier - number->subscript - - map-slot - define-slot-lens - with-modified-slot - derive-display - to-pretty-sexp - - partition-on - flat-map)) - -(define (alist? xs) - "Return #t when XS is an alist" - (and (list? xs) - (every (lambda (elem) - (and (pair? elem) - (string? (car elem)))) - xs))) - -(define (map-key f key alist) - "Return ALIST where F has been applied to the value of KEY" - (map (lambda (kv) - (if (equal? key (car kv)) - (cons (car kv) (f (cdr kv))) - kv)) - alist)) - -(define (update-alist x y) - "Return X ∪ Y where the values for any duplicate keys come from Y" - (append y (filter (lambda (kv) (not (member (car kv) y))) x))) - -(define (add-to-end xs x) - "Add a single item X to the end of XS" - (append xs (list x))) - -(define (hash-table-append! hash-table key xs) - "Append list XS to the value stored at KEY in HASH-TABLE, or '() if KEY not present" - (if (hash-table-exists? hash-table key) - (hash-table-set! hash-table key (append (hash-table-ref hash-table key) xs)) - (hash-table-set! hash-table key xs))) - -(define (hash-table-append-item! hash-table key item) - "Append single ITEM to the value stored at KEY in HASH-TABLE, or '() if KEY not present" - (if (hash-table-exists? hash-table key) - (hash-table-set! hash-table key (add-to-end (hash-table-ref hash-table key) item)) - (hash-table-set! hash-table key (list item)))) - -(define* (fresh-identifier identifiers #:optional (pre "anonym")) - "Return an identifier which does not occur in IDENTIFIERS" - (define (try n) - (let ((candidate-identifier (string-append pre (number->subscript n)))) - (if (member candidate-identifier identifiers) - (try (+ n 1)) - candidate-identifier))) - (try 0)) - -(define (number->subscript n) - "Return N as a string consisting of subscript numerals" - (string-map (match-lambda - (#\0 #\₀) - (#\1 #\₁) - (#\2 #\₂) - (#\3 #\₃) - (#\4 #\₄) - (#\5 #\₅) - (#\6 #\₆) - (#\7 #\₇) - (#\8 #\₈) - (#\9 #\₉)) - (number->string n))) - -(define-syntax map-slot - (syntax-rules () - ((map-slot instance slot f) - (let ((clone (shallow-clone instance))) - (slot-set! clone slot (f (slot-ref clone slot))) - clone)))) - -(define-syntax define-slot-lens - (syntax-rules () - ((define-slot-lens name slot) - (define (name) - (lens (lambda (s) (slot-ref s slot)) - (lambda (s f) (map-slot s slot f))))))) - -(define-syntax with-modified-slot - (syntax-rules () - ((with-modified-slot instance slot new-value) - (let ((clone (shallow-clone instance))) - (slot-set! clone slot new-value) - clone)))) - -(define-syntax derive-display - (syntax-rules () - ((derive-display class) - (define-method (display (x class) port) - (format port "#<~a " (class-name class)) - (for-each (compose (lambda (y) - (display y port) - (display " ")) - (cut slot-ref x <>) - (cut slot-definition-name <>)) - (class-slots class)) - (display ">" port))))) - -(define (to-pretty-sexp form) - (cond ((hash-table? form) - (to-pretty-sexp (hash-table->alist form))) - ((instance? form) - `(,(class-name (class-of form)) - ,@(map (compose to-pretty-sexp - (cut slot-ref form <>) - (cut slot-definition-name <>)) - (class-slots (class-of form))))) - ((list? form) (map to-pretty-sexp form)) - ((and (array? form) (not (string? form))) - (list->array 1 (map to-pretty-sexp (array->list form)))) - ((pair? form) (cons (to-pretty-sexp (car form)) - (to-pretty-sexp (cdr form)))) - (else form))) - - -(define (partition-on xs pred) - (define (recur result running cur) - (cond ((null? cur) - (cons (reverse! running) result)) - ((pred (first cur)) - (recur (cons (reverse! running) result) (list (first cur)) (cdr cur))) - (else - (recur result (cons (car cur) running) (cdr cur))))) - (reverse! (filter (negate null?) (recur '() '() xs)))) - -(define* (flat-map proc #:rest args) - (fold append '() (apply map proc args))) |