From 4ef90bd4f04a9df089c31f6eb44f5cb3c2680c49 Mon Sep 17 00:00:00 2001 From: Jakob L. Kreuze Date: Thu, 21 Dec 2023 13:38:41 -0500 Subject: Get rid of old compiler code --- rego-proofs/compiler-rewrite/.gitignore | 1 - rego-proofs/compiler-rewrite/.ocamlformat | 1 - rego-proofs/compiler-rewrite/bin/dune | 5 - rego-proofs/compiler-rewrite/bin/main.ml | 12 - rego-proofs/compiler-rewrite/compiler_rewrite.opam | 24 - rego-proofs/compiler-rewrite/dune-project | 14 - rego-proofs/compiler-rewrite/lib/ast.ml | 275 ------- rego-proofs/compiler-rewrite/lib/ast.mli | 108 --- rego-proofs/compiler-rewrite/lib/compiler.ml | 814 --------------------- rego-proofs/compiler-rewrite/lib/compiler.mli | 13 - rego-proofs/compiler-rewrite/lib/dune | 9 - rego-proofs/compiler-rewrite/lib/lean.ml | 63 -- rego-proofs/compiler-rewrite/lib/lean.mli | 25 - .../compiler-rewrite/test/compiler_rewrite.ml | 138 ---- rego-proofs/compiler-rewrite/test/dune | 3 - rego-proofs/compiler.scm | 29 - rego-proofs/compiler/.gitignore | 1 + rego-proofs/compiler/.ocamlformat | 1 + rego-proofs/compiler/bin/dune | 5 + rego-proofs/compiler/bin/main.ml | 12 + rego-proofs/compiler/compiler.opam | 24 + rego-proofs/compiler/dune-project | 14 + rego-proofs/compiler/lean.scm | 374 ---------- rego-proofs/compiler/lib/ast.ml | 275 +++++++ rego-proofs/compiler/lib/ast.mli | 108 +++ rego-proofs/compiler/lib/compiler.ml | 814 +++++++++++++++++++++ rego-proofs/compiler/lib/compiler.mli | 13 + rego-proofs/compiler/lib/dune | 9 + rego-proofs/compiler/lib/lean.ml | 63 ++ rego-proofs/compiler/lib/lean.mli | 25 + rego-proofs/compiler/main.scm | 65 -- rego-proofs/compiler/passes/bool-to-prop.scm | 51 -- .../compiler/passes/compile-constraints.scm | 134 ---- rego-proofs/compiler/passes/compile-definition.scm | 74 -- .../compiler/passes/compile-exists-some.scm | 89 --- rego-proofs/compiler/passes/compile-for-all.scm | 48 -- rego-proofs/compiler/passes/compile-funcall.scm | 36 - .../compiler/passes/compile-local-references.scm | 74 -- .../compiler/passes/compile-object-literal.scm | 35 - rego-proofs/compiler/passes/compile-reference.scm | 73 -- rego-proofs/compiler/passes/emit-specification.scm | 65 -- .../compiler/passes/extract-identifiers.scm | 82 --- .../compiler/passes/lift-comprehensions.scm | 72 -- .../compiler/passes/lift-implicit-anonymous.scm | 62 -- rego-proofs/compiler/passes/parse-policy.scm | 257 ------- rego-proofs/compiler/passes/read-and-parse.scm | 65 -- rego-proofs/compiler/test.scm | 500 ------------- rego-proofs/compiler/test/compiler.ml | 134 ++++ rego-proofs/compiler/test/dune | 3 + rego-proofs/compiler/type-inference.scm | 112 --- rego-proofs/compiler/types.scm | 487 ------------ rego-proofs/compiler/utilities.scm | 167 ----- 52 files changed, 1501 insertions(+), 4456 deletions(-) delete mode 100644 rego-proofs/compiler-rewrite/.gitignore delete mode 100644 rego-proofs/compiler-rewrite/.ocamlformat delete mode 100644 rego-proofs/compiler-rewrite/bin/dune delete mode 100644 rego-proofs/compiler-rewrite/bin/main.ml delete mode 100644 rego-proofs/compiler-rewrite/compiler_rewrite.opam delete mode 100644 rego-proofs/compiler-rewrite/dune-project delete mode 100644 rego-proofs/compiler-rewrite/lib/ast.ml delete mode 100644 rego-proofs/compiler-rewrite/lib/ast.mli delete mode 100644 rego-proofs/compiler-rewrite/lib/compiler.ml delete mode 100644 rego-proofs/compiler-rewrite/lib/compiler.mli delete mode 100644 rego-proofs/compiler-rewrite/lib/dune delete mode 100644 rego-proofs/compiler-rewrite/lib/lean.ml delete mode 100644 rego-proofs/compiler-rewrite/lib/lean.mli delete mode 100644 rego-proofs/compiler-rewrite/test/compiler_rewrite.ml delete mode 100644 rego-proofs/compiler-rewrite/test/dune delete mode 100755 rego-proofs/compiler.scm create mode 100644 rego-proofs/compiler/.gitignore create mode 100644 rego-proofs/compiler/.ocamlformat create mode 100644 rego-proofs/compiler/bin/dune create mode 100644 rego-proofs/compiler/bin/main.ml create mode 100644 rego-proofs/compiler/compiler.opam create mode 100644 rego-proofs/compiler/dune-project delete mode 100644 rego-proofs/compiler/lean.scm create mode 100644 rego-proofs/compiler/lib/ast.ml create mode 100644 rego-proofs/compiler/lib/ast.mli create mode 100644 rego-proofs/compiler/lib/compiler.ml create mode 100644 rego-proofs/compiler/lib/compiler.mli create mode 100644 rego-proofs/compiler/lib/dune create mode 100644 rego-proofs/compiler/lib/lean.ml create mode 100644 rego-proofs/compiler/lib/lean.mli delete mode 100644 rego-proofs/compiler/main.scm delete mode 100644 rego-proofs/compiler/passes/bool-to-prop.scm delete mode 100644 rego-proofs/compiler/passes/compile-constraints.scm delete mode 100644 rego-proofs/compiler/passes/compile-definition.scm delete mode 100644 rego-proofs/compiler/passes/compile-exists-some.scm delete mode 100644 rego-proofs/compiler/passes/compile-for-all.scm delete mode 100644 rego-proofs/compiler/passes/compile-funcall.scm delete mode 100644 rego-proofs/compiler/passes/compile-local-references.scm delete mode 100644 rego-proofs/compiler/passes/compile-object-literal.scm delete mode 100644 rego-proofs/compiler/passes/compile-reference.scm delete mode 100644 rego-proofs/compiler/passes/emit-specification.scm delete mode 100644 rego-proofs/compiler/passes/extract-identifiers.scm delete mode 100644 rego-proofs/compiler/passes/lift-comprehensions.scm delete mode 100644 rego-proofs/compiler/passes/lift-implicit-anonymous.scm delete mode 100644 rego-proofs/compiler/passes/parse-policy.scm delete mode 100644 rego-proofs/compiler/passes/read-and-parse.scm delete mode 100644 rego-proofs/compiler/test.scm create mode 100644 rego-proofs/compiler/test/compiler.ml create mode 100644 rego-proofs/compiler/test/dune delete mode 100644 rego-proofs/compiler/type-inference.scm delete mode 100644 rego-proofs/compiler/types.scm delete mode 100644 rego-proofs/compiler/utilities.scm diff --git a/rego-proofs/compiler-rewrite/.gitignore b/rego-proofs/compiler-rewrite/.gitignore deleted file mode 100644 index e35d885..0000000 --- a/rego-proofs/compiler-rewrite/.gitignore +++ /dev/null @@ -1 +0,0 @@ -_build diff --git a/rego-proofs/compiler-rewrite/.ocamlformat b/rego-proofs/compiler-rewrite/.ocamlformat deleted file mode 100644 index c870de9..0000000 --- a/rego-proofs/compiler-rewrite/.ocamlformat +++ /dev/null @@ -1 +0,0 @@ -version=0.26.1 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/bin/main.ml b/rego-proofs/compiler-rewrite/bin/main.ml deleted file mode 100644 index b5f04fa..0000000 --- a/rego-proofs/compiler-rewrite/bin/main.ml +++ /dev/null @@ -1,12 +0,0 @@ -open Core -open Compiler_rewrite.Ast -open Compiler_rewrite.Compiler -open Compiler_rewrite.Lean - -let () = - let file_name = Array.get (Sys.get_argv ()) 1 in - let policy_code = In_channel.read_all file_name in - ast_of_string policy_code - |> compile_package - |> List.map ~f:fmt_lean_expression - |> List.iter ~f:print_endline diff --git a/rego-proofs/compiler-rewrite/compiler_rewrite.opam b/rego-proofs/compiler-rewrite/compiler_rewrite.opam deleted file mode 100644 index 8dbe763..0000000 --- a/rego-proofs/compiler-rewrite/compiler_rewrite.opam +++ /dev/null @@ -1,24 +0,0 @@ -# This file is generated by dune, edit dune-project instead -opam-version: "2.0" -synopsis: "Compiler from Rego to a Lean shallow embedding" -maintainer: ["Jakob Kreuze"] -authors: ["Jakob Kreuze"] -depends: [ - "ocaml" - "dune" {>= "3.11"} - "odoc" {with-doc} -] -build: [ - ["dune" "subst"] {dev} - [ - "dune" - "build" - "-p" - name - "-j" - jobs - "@install" - "@runtest" {with-test} - "@doc" {with-doc} - ] -] diff --git a/rego-proofs/compiler-rewrite/dune-project b/rego-proofs/compiler-rewrite/dune-project deleted file mode 100644 index e989552..0000000 --- a/rego-proofs/compiler-rewrite/dune-project +++ /dev/null @@ -1,14 +0,0 @@ -(lang dune 3.11) - -(name compiler_rewrite) - -(generate_opam_files true) - -(authors "Jakob Kreuze") - -(maintainers "Jakob Kreuze") - -(package - (name compiler_rewrite) - (synopsis "Compiler from Rego to a Lean shallow embedding") - (depends ocaml dune)) diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler-rewrite/lib/ast.ml deleted file mode 100644 index 98d8375..0000000 --- a/rego-proofs/compiler-rewrite/lib/ast.ml +++ /dev/null @@ -1,275 +0,0 @@ -open Core -open Yojson.Basic.Util - -(* AST types. *) - -type expr = Term of term | Every of string option * string * term * query -[@@deriving eq, show] - -and literal = - | Exists of expr list * with_modifier option - | Expr of expr * with_modifier option - | Negate of expr * with_modifier option -[@@deriving eq, show] - -and query = literal list [@@deriving eq, show] - -and term = - | Scalar of scalar - | Var of string - | Ref of reference - | Array of term list - | Object of (object_key * term) list - | Set of term list - | ArrayComprehension of term * query - | ObjectComprehension of (object_key * term) * query - | SetComprehension of term * query - | Call of reference * term list -[@@deriving eq, show] - -and scalar = String of string | Number of float | Bool of bool | Null -[@@deriving eq, show] - -and reference = ref_target * term list [@@deriving eq, show] - -and ref_target = - | Var of string - | Array of term list - | Object of (object_key * term) list - | Set of term list - | ArrayComprehension of term * query - | ObjectComprehension of (object_key * term) * query - | SetComprehension of term * query - | Call of reference * term list -[@@deriving eq, show] - -and object_key = Scalar of scalar | Ref of reference | Var of string -[@@deriving eq, show] - -and with_modifier = (term * term) list [@@deriving eq, show] - -type assign_operator = Assign | Unify [@@deriving eq, show] -type rule_head_lhs = reference [@@deriving eq, show] - -type rule_head_rhs = - | Assignment of assign_operator * term - | Function of assign_operator * term list * term - | Set of term -[@@deriving eq, show] - -type rule_head = rule_head_lhs * rule_head_rhs [@@deriving eq, show] - -type rule = { - default : bool; - head : rule_head; - body : query; - otherwise : rule option; -} -[@@deriving eq, show] - -type import = { alias : string option; path : reference } [@@deriving eq, show] - -type package = { path : reference; imports : import list; policy : rule list } -[@@deriving eq, show] - -(* Additional JSON utility functions. *) - -let is_null : Yojson.Basic.t -> bool = function `Null -> true | _ -> false - -let to_bool_or_false : Yojson.Basic.t -> bool = function - | `Bool b -> b - | _ -> false - -let to_list_or_empty : Yojson.Basic.t -> Yojson.Basic.t list = function - | `Null -> [] - | `List xs -> xs - | _ -> failwith "Not a list or null" - -let object_key_of_term : term -> object_key = function - | Scalar s -> Scalar s - | Ref r -> Ref r - | Var v -> Var v - | _ -> failwith "failed to convert term to object_key" - -(* Code to parse the JSON output of `opa parse`. *) - -let rec parse_term (tree : Yojson.Basic.t) : term = - let term_type = tree |> member "type" |> to_string in - match term_type with - | "var" -> Var (tree |> member "value" |> to_string) - | "ref" -> Ref (tree |> member "value" |> to_list |> parse_ref) - | "null" -> Scalar Null - | "boolean" -> Scalar (Bool (tree |> member "value" |> to_bool)) - | "number" -> Scalar (Number (tree |> member "value" |> to_number)) - | "string" -> Scalar (String (tree |> member "value" |> to_string)) - | "array" -> - Array (tree |> member "value" |> to_list |> List.map ~f:parse_term) - | "set" -> Set (tree |> member "value" |> to_list |> List.map ~f:parse_term) - | "object" -> - Object - (tree |> member "value" |> to_list - |> List.map ~f:(function - | `List [ x; y ] -> - (x |> parse_term |> object_key_of_term, y |> parse_term) - | _ -> failwith "ill-formed object")) - | "arraycomprehension" -> - ArrayComprehension - ( tree |> member "value" |> member "term" |> parse_term, - tree |> member "value" |> member "body" |> to_list - |> List.map ~f:parse_literal ) - | "setcomprehension" -> - SetComprehension - ( tree |> member "value" |> member "term" |> parse_term, - tree |> member "value" |> member "body" |> to_list - |> List.map ~f:parse_literal ) - | "objectcomprehension" -> - ObjectComprehension - ( ( tree |> member "value" |> member "key" |> parse_term - |> object_key_of_term, - tree |> member "value" |> member "value" |> parse_term ), - tree |> member "value" |> member "body" |> to_list - |> List.map ~f:parse_literal ) - | "call" -> ( - match tree |> member "value" |> to_list with - | func :: args -> - Call - ( func |> member "value" |> to_list |> parse_ref, - List.map ~f:parse_term args ) - | _ -> failwith "ill-formed call") - | _ -> failwith ("unsupported term type " ^ term_type) - -and parse_literal tree : literal = - let with_expr = tree |> member "with" in - let with_expr = - match with_expr with - | `Null -> None - | `List xs -> - Some - (List.map xs ~f:(fun x -> - ( x |> member "target" |> parse_term, - x |> member "value" |> parse_term ))) - | _ -> - failwith - ("ill-formed with expression " ^ Yojson.Basic.to_string with_expr) - in - match tree |> member "terms" with - | `List (func :: args) -> - let term = - Term - (Call - ( func |> member "value" |> to_list |> parse_ref, - List.map ~f:parse_term args )) - in - if tree |> member "negated" |> to_bool_or_false then - Negate (term, with_expr) - else Expr (term, with_expr) - - | `List _ -> failwith "ill-formed call" - | x -> - if not (x |> member "symbols" |> is_null) then - Exists - ( x |> member "symbols" |> to_list - |> List.map ~f:(fun x -> Term (parse_term x)), - with_expr ) - else if x |> member "domain" |> is_null then - let term = Term (parse_term x) in - if tree |> member "negated" |> to_bool_or_false then - Negate (term, with_expr) - else Expr (term, with_expr) - else - let term = - Every - ( (if x |> member "key" |> is_null then None - else Some (x |> member "key" |> member "value" |> to_string)), - x |> member "value" |> member "value" |> to_string, - x |> member "domain" |> parse_term, - List.map ~f:parse_literal (x |> member "body" |> to_list) ) - in - if tree |> member "negated" |> to_bool_or_false then - Negate (term, with_expr) - else Expr (term, with_expr) - -and parse_ref_target tree : ref_target = - let term = parse_term tree in - match term with - | Var term -> Var term - | Array term -> Array term - | Object term -> Object term - | Set term -> Set term - | ArrayComprehension (term, y) -> ArrayComprehension (term, y) - | ObjectComprehension (term, y) -> ObjectComprehension (term, y) - | SetComprehension (term, y) -> SetComprehension (term, y) - | Call (term, y) -> Call (term, y) - | _ -> failwith ("unsupported ref_target " ^ show_term term) - -and parse_ref tree = - match tree with - | target :: args -> (parse_ref_target target, List.map ~f:parse_term args) - | _ -> failwith "empty reference" - -let parse_head tree = - (* Variables are desugared to empty references. *) - let lhs = tree |> member "ref" |> to_list |> parse_ref in - let assign_operator = - if tree |> member "assign" |> to_bool_or_false then Assign else Unify - in - let rhs = - if (tree |> member "value" |> is_null) && (not (tree |> member "key" |> is_null)) then - Set (tree |> member "key" |> parse_term) - else if not (tree |> member "args" |> is_null) then - Function - ( assign_operator, - tree |> member "args" |> to_list |> List.map ~f:parse_term, - tree |> member "value" |> parse_term ) - else Assignment (assign_operator, tree |> member "value" |> parse_term) - in - (lhs, rhs) - -let rec parse_rule tree = - { - default = tree |> member "default" |> to_bool_or_false; - head = tree |> member "head" |> parse_head; - body = List.map ~f:parse_literal (tree |> member "body" |> to_list_or_empty); - otherwise = - (match tree |> member "else" with - | `Null -> None - | else_branch -> Some (parse_rule else_branch)); - } - -let parse_import_path tree = - match tree |> member "type" |> to_string with - | "ref" -> tree |> member "value" |> to_list |> parse_ref - | _ -> failwith "unimplemented" - -let parse_import tree = - { - alias = tree |> member "alias" |> to_string_option; - path = tree |> member "path" |> parse_import_path; - } - -let parse_package tree = tree |> member "path" |> to_list |> parse_ref - -let parse_tree tree = - { - path = tree |> member "package" |> parse_package; - imports = - List.map ~f:parse_import (tree |> member "imports" |> to_list_or_empty); - policy = List.map ~f:parse_rule (tree |> member "rules" |> to_list_or_empty); - } - -(* OPA interaction. *) - -let invoke ?(stdin = "") ?(env = [||]) cmd = - let ic, oc, ec = UnixLabels.open_process_full cmd ~env in - Out_channel.output_string oc stdin; - Out_channel.close oc; - let i = In_channel.input_all ic in - let e = In_channel.input_all ec in - (i, e) - -let ast_of_string policy_code = - let stdout, _ = - invoke "/home/jakob/.local/bin/opa parse -f json /dev/stdin" - ~stdin:policy_code ~env:[||] - in - Yojson.Basic.from_string stdout |> parse_tree diff --git a/rego-proofs/compiler-rewrite/lib/ast.mli b/rego-proofs/compiler-rewrite/lib/ast.mli deleted file mode 100644 index 514d5da..0000000 --- a/rego-proofs/compiler-rewrite/lib/ast.mli +++ /dev/null @@ -1,108 +0,0 @@ -type expr = Term of term | Every of string option * string * term * query - -and literal = - | Exists of expr list * with_modifier option - | Expr of expr * with_modifier option - | Negate of expr * with_modifier option - -and query = literal list - -and term = - | Scalar of scalar - | Var of string - | Ref of reference - | Array of term list - | Object of (object_key * term) list - | Set of term list - | ArrayComprehension of term * query - | ObjectComprehension of (object_key * term) * query - | SetComprehension of term * query - | Call of reference * term list - -and scalar = String of string | Number of float | Bool of bool | Null -and reference = ref_target * term list - -and ref_target = - | Var of string - | Array of term list - | Object of (object_key * term) list - | Set of term list - | ArrayComprehension of term * query - | ObjectComprehension of (object_key * term) * query - | SetComprehension of term * query - | Call of reference * term list - -and object_key = Scalar of scalar | Ref of reference | Var of string -and with_modifier = (term * term) list - -type assign_operator = Assign | Unify -type rule_head_lhs = reference - -type rule_head_rhs = - | Assignment of assign_operator * term - | Function of assign_operator * term list * term - | Set of term - -type rule_head = rule_head_lhs * rule_head_rhs - -type rule = { - default : bool; - head : rule_head; - body : query; - otherwise : rule option; -} - -type import = { alias : string option; path : reference } -type package = { path : reference; imports : import list; policy : rule list } - -val ast_of_string : string -> package -val show_package : package -> string - -val equal_assign_operator : assign_operator -> assign_operator -> bool -val equal_expr : expr -> expr -> bool -val equal_import : import -> import -> bool -val equal_literal : literal -> literal -> bool -val equal_object_key : object_key -> object_key -> bool -val equal_package : package -> package -> bool -val equal_query : query -> query -> bool -val equal_ref_target : ref_target -> ref_target -> bool -val equal_reference : reference -> reference -> bool -val equal_rule : rule -> rule -> bool -val equal_rule_head : rule_head -> rule_head -> bool -val equal_rule_head_lhs : rule_head_lhs -> rule_head_lhs -> bool -val equal_rule_head_rhs : rule_head_rhs -> rule_head_rhs -> bool -val equal_scalar : scalar -> scalar -> bool -val equal_term : term -> term -> bool -val equal_with_modifier : with_modifier -> with_modifier -> bool -val pp_assign_operator : Format.formatter -> assign_operator -> unit -val pp_expr : Format.formatter -> expr -> unit -val pp_import : Format.formatter -> import -> unit -val pp_literal : Format.formatter -> literal -> unit -val pp_object_key : Format.formatter -> object_key -> unit -val pp_package : Format.formatter -> package -> unit -val pp_query : Format.formatter -> query -> unit -val pp_ref_target : Format.formatter -> ref_target -> unit -val pp_reference : Format.formatter -> reference -> unit -val pp_rule : Format.formatter -> rule -> unit -val pp_rule_head : Format.formatter -> rule_head -> unit -val pp_rule_head_lhs : Format.formatter -> rule_head_lhs -> unit -val pp_rule_head_rhs : Format.formatter -> rule_head_rhs -> unit -val pp_scalar : Format.formatter -> scalar -> unit -val pp_term : Format.formatter -> term -> unit -val pp_with_modifier : Format.formatter -> with_modifier -> unit -val show_assign_operator : assign_operator -> string -val show_expr : expr -> string -val show_import : import -> string -val show_literal : literal -> string -val show_object_key : object_key -> string -val show_package : package -> string -val show_query : query -> string -val show_ref_target : ref_target -> string -val show_reference : reference -> string -val show_rule : rule -> string -val show_rule_head : rule_head -> string -val show_rule_head_lhs : rule_head_lhs -> string -val show_rule_head_rhs : rule_head_rhs -> string -val show_scalar : scalar -> string -val show_term : term -> string -val show_with_modifier : with_modifier -> string diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml deleted file mode 100644 index 3b0384a..0000000 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ /dev/null @@ -1,814 +0,0 @@ -open Ast -open Core -open Lean - -type definition_kind = Complete - | Parameter - | ScalarRule - | SetRule - | ObjectRule - | FunctionRule -[@@deriving eq, show] - -let fold_or props = - match List.reduce props ~f:(fun x y -> Application (Identifier "Or", [y; x])) with - | Some x -> x - | None -> Bool true - -let fold_and props = - match List.reduce props ~f:(fun x y -> Application (Identifier "And", [y; x])) with - | Some x -> x - | None -> Bool false - -let fold_deref terms = - List.reduce_exn terms ~f:(fun x y -> Application (Identifier "Rego.Any.deref", [x; y])) - -let kind_and_args_of_rule = function - | { head = ((_, []), Assignment (_, term)); _ } -> - `ScalarRule term - | { head = ((_, _), Set term); _ } -> - `SetRule term - | { head = ((_, [key]), Assignment (_, value)); _ } -> - `ObjectRule (key, value) - | { head = ((_, _), Function (_, args, term)); _ } -> - `FunctionRule (args, term) - | { head = ((_, _), Assignment (_, _)); _ } as rule -> - failwith (Printf.sprintf "unknown rule form: %s" (show_rule rule)) - -let definition_kind_of_rule rule = - match kind_and_args_of_rule rule with - | `ScalarRule _ -> ScalarRule - | `SetRule _ -> SetRule - | `ObjectRule _ -> ObjectRule - | `FunctionRule _ -> FunctionRule - -type variable = { lean_id : string; - kind : definition_kind; - assigned : bool; - } -[@@deriving eq, show] - -module Environ = Map.Make (String) -type environ = variable Environ.t - -let gensym : string -> string = - let is_alphanum = function 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' -> true | _ -> false in - let counter = ref 0 in - fun (base : string) -> - let base = String.filter base ~f:is_alphanum in - let number = !counter in - counter := !counter + 1 ; - Printf.sprintf "v%s__%d" base number - -let extend_environment (env : environ) (vars : (string * variable) list) = - Environ.of_alist_exn vars - |> Map.merge env ~f:(fun ~key:_key -> function - | `Right v -> Some v - | `Left v -> Some v - | `Both (_, v) -> Some v) - -let toplevel = Environ.of_alist_exn [ - ("eq", { lean_id = "eq"; kind = Complete; assigned = true }); - ("equal", { lean_id = "equal"; kind = Complete; assigned = true }) - ] - -let term_of_object_key : object_key -> term = function - | Scalar s -> Scalar s - | Ref r -> Ref r - | Var v -> Var v - -let term_of_ref_target : ref_target -> term = function - | Var s -> Var s - | Array xs -> Array xs - | Object kvs -> Object kvs - | Set xs -> Set xs - | ArrayComprehension (key, q) -> ArrayComprehension (key, q) - | ObjectComprehension (key, q) -> ObjectComprehension (key, q) - | SetComprehension (key, q) -> SetComprehension (key, q) - | Call (fn, args) -> Call (fn, args) - -let ref_target_of_term : term -> ref_target = function - | Var s -> Var s - | Array xs -> Array xs - | Object kvs -> Object kvs - | Set xs -> Set xs - | ArrayComprehension (key, q) -> ArrayComprehension (key, q) - | ObjectComprehension (key, q) -> ObjectComprehension (key, q) - | SetComprehension (key, q) -> SetComprehension (key, q) - | Call (fn, args) -> Call (fn, args) - | _ -> failwith "cannot widen to ref_target" - -let literal_of_expr exp : literal = Expr (exp, None) -let literal_of_term t = Expr (Term t, None) - - -let map_with_environment_updates env xs fn = - List.fold xs ~init:(env, []) ~f:(fun (env, ys) x -> - let env', y = fn env x in - (env', ys @ [ y ])) - -let rec uniq eq = function - | [] -> [] - | hd::tl -> - if List.mem tl hd ~equal:eq then - uniq eq tl - else hd :: uniq eq tl - -type analysis_result = - { bound : string list; - free : string list; - used : string list } -[@@deriving show] - -let extract_variables (env : environ) (q : query) : analysis_result = - let empty = { bound = []; free = []; used = [] } in - let combine = - fun x y -> - match (x, y) with - | ({ bound = bound'; free = free'; used = used' }, - { bound = bound''; free = free''; used = used'' }) -> - { bound = bound' @ bound''; - free = free' @ free''; - used = used' @ used'' } in - let rec handle_term env : term -> analysis_result = function - (* If we see a variable in an assignment, and it isn't a parameter, it's bound. *) - | Call ((Var "assign", []), [ Var name; rhs ]) -> - let { bound; free; used } = handle_term env rhs in - (match Map.find env name with - | Some { kind = Parameter; _ } -> - { used = [name] @ used; free; bound } - | _ -> - { bound = [name] @ bound; free; used }) - (* Variables that haven't previously been introduced to the scope are free. *) - | Var name -> - if Map.find env name |> Option.is_some then - { free = []; bound = []; used = [name] } - else { free = [name]; bound = []; used = [] } - (* Otherwise, we'll recurse on the term. *) - | Ref (target, args) -> - let target = term_of_ref_target target in - if List.is_empty args then - handle_term env target - else - let terms = [target] @ args in - List.map terms ~f:(handle_term env) |> List.fold ~init:empty ~f:combine - | Array xs | Set xs -> - List.map xs ~f:(handle_term env) |> List.fold ~init:empty ~f:combine - | Object kvs -> List.map ~f:snd kvs - |> List.map ~f:(handle_term env) - |> List.fold ~init:empty ~f:combine - | Call (x, xs) -> - List.map ((Ref x : term)::xs) ~f:(handle_term env) |> List.fold ~init:empty ~f:combine - | _ -> empty - and handle_expr env = function - | Term t -> handle_term env t - | Every (Some key, value, _, q) -> - let env' = [(key, { lean_id = "unimportant"; kind = Complete; assigned = true }); - (value, { lean_id = "unimportant"; kind = Complete; assigned = true })] - |> extend_environment env in - List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine - | Every (None, value, _, q) -> - let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in - let env' = Map.set env ~key:value ~data:var in - List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine - and handle_literal env : literal -> analysis_result = function - | Exists (exprs, _) -> - List.map exprs ~f:(handle_expr env) |> List.fold ~init:empty ~f:combine - | Expr (expr, _) -> handle_expr env expr - | Negate (expr, _) -> handle_expr env expr - in - let { free; bound; used } = List.map q ~f:(handle_literal env) |> List.fold ~init:empty ~f:combine in - let free = List.filter free ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in - let used = List.filter used ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in - let uniq = uniq String.equal in - { free = free |> uniq; - bound = bound |> uniq; - used = used |> uniq } - -(* This is solely for the test suite. *) -let extract_variables_wrapper (q : query) : analysis_result = - extract_variables toplevel q - -(* --- *) - -(* This breaks a nested rule, such as one defining `w.x.y.z`, into as many as - needed such that every rule is of the form `x["y"] := _`. *) -let rec transform_rule_with_ref_head : rule -> rule list = function - (* Base case - this is a simple reference that we can deal with. *) - | { head = ((_, []), _); _ } | { head = ((_, [_]), _); _ } as rule -> - [rule] - | { head = ((tgt, xs), rhs); _ } as rule -> - let tail = List.last_exn xs in - let name = gensym "anonymous" in - [{ rule with head = ((Var name, [tail]), rhs) }] @ - transform_rule_with_ref_head { rule with head = ((tgt, List.drop_last_exn xs), Assignment (Assign, Var name)) } - -(* --- *) - -let rec simplify_expression = function - | Application (Identifier "And", xs) -> - let xs' = List.map ~f:simplify_expression xs - |> List.filter ~f:(function Bool true -> false | _ -> true) - in - (match xs' with - | [] -> Bool false - | [x] -> x - | xs' -> Application (Identifier "And", xs')) - | Application (Identifier "Eq", [Application (Identifier "Rego.Any.bool", [Bool a]); - Application (Identifier "Rego.Any.bool", [Bool b])]) -> - Bool (equal_bool a b) - | Application (Identifier "Ne", [Application (Identifier "Rego.Any.bool", [Bool a]); - Application (Identifier "Rego.Any.bool", [Bool b])]) -> - Bool (not (equal_bool a b)) - | Application (Identifier "Eq", [Application (Identifier "Rego.Any.str", [String a]); - Application (Identifier "Rego.Any.str", [String b])]) -> - Bool (equal_string a b) - | Application (Identifier "Ne", [Application (Identifier "Rego.Any.str", [String a]); - Application (Identifier "Rego.Any.str", [String b])]) -> - Bool (not (equal_string a b)) - | Application (Identifier "Eq", [Application (Identifier "Rego.Any.num", [Number a]); - Application (Identifier "Rego.Any.num", [Number b])]) -> - Bool (equal_float a b) - | Application (Identifier "Ne", [Application (Identifier "Rego.Any.num", [Number a]); - Application (Identifier "Rego.Any.num", [Number b])]) -> - Bool (not (equal_float a b)) - | expr -> expr - -(* --- *) - -let rec compile_term env : term -> lean_expression = - function - | Scalar s -> - (match s with - | String s -> Application (Identifier "Rego.Any.str", [String s]) - | Number x -> Application (Identifier "Rego.Any.num", [Number x]) - | Bool b -> Application (Identifier "Rego.Any.bool", [Bool b]) - | Null -> Application (Identifier "Rego.Any.null", [])) - | Var id -> - (match Map.find env id with - | Some { lean_id; kind = Complete; assigned = true } | - Some { lean_id; kind = Parameter; assigned = true } - -> Identifier lean_id - | Some { assigned = false; _ } -> - failwith (Printf.sprintf "identifier %s used before definition" id) - | Some var -> - failwith (Printf.sprintf - "variable found in environment but of unknown form %s" - (show_variable var)) - | None -> failwith (Printf.sprintf "unbound variable %s" id)) - | Ref (target, terms) -> - let target' = compile_term env (term_of_ref_target target) in - let terms' = List.map ~f:(compile_term env) terms in - if List.is_empty terms' then - target' - else [target'] @ terms' |> fold_deref - | Array xs -> - let xs' = List.map ~f:(compile_term env) xs in - Application (Identifier "Rego.Any.array", xs') - | Set xs -> - let xs' = List.map ~f:(compile_term env) xs in - Application (Identifier "Rego.Any.set", xs') - | Object kvs -> - let compile_kv = function - | (key, value) -> - let key' = compile_term env (term_of_object_key key) in - let value' = compile_term env value in - Tuple [key'; value'] in - let kvs' = List.map ~f:compile_kv kvs in - Application (Identifier "Rego.Any.object", kvs') - | ArrayComprehension (_term, _query) -> - failwith "ArrayComprehension encountered, should have been lifted" - | SetComprehension (_term, _query) -> - failwith "ArrayComprehension encountered, should have been lifted" - | ObjectComprehension ((_key, _value), _query) -> - failwith "ArrayComprehension encountered, should have been lifted" - | Call (fn, args) -> - let fn' = compile_term env (Ref fn) in - let args' = List.map ~f:(compile_term env) args in - Application (fn', args') - -let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) option) : (('a * term) list * rule) = - let empty = ([], []) in - let combine = fun (side_info, q) (side_info', term) -> - (side_info @ side_info', q @ [term]) in - let rec handle_term : term -> (('a * term) list * term) = function - | term when f env term |> Option.is_some -> - let (side_info, term') = f env term |> Option.value_exn in - ([(side_info, term)], term') - | Ref (target, args) -> - let target = term_of_ref_target target in - let terms = [target] @ args in - - let (side_info, terms') = - List.map terms ~f:handle_term - |> List.fold ~f:combine ~init:empty - in (side_info, Ref (ref_target_of_term (List.hd_exn terms'), List.tl_exn terms')) - | Array xs -> - let (side_info, terms) = - List.map xs ~f:handle_term - |> List.fold ~f:combine ~init:empty - in (side_info, Array terms) - | Set xs -> - let (side_info, terms) = - List.map xs ~f:handle_term - |> List.fold ~f:combine ~init:empty - in (side_info, Set terms) - | Object kvs -> - let (side_info, terms) = - List.map ~f:snd kvs - |> List.map ~f:handle_term - |> List.fold ~f:combine ~init:empty - in - (side_info, - Object - (List.zip_exn - (List.map ~f:fst kvs) - terms)) - | Call (x, xs) -> - let (side_info, terms) = - List.map ((Ref x : term)::xs) ~f:handle_term - |> List.fold ~f:combine ~init:empty - in - (match List.hd_exn terms with - | Ref reference -> - (side_info, Call (reference, List.tl_exn terms)) - | term -> failwith (show_term term |> Printf.sprintf "invalid call target %s")) - | term -> ([], term) - and handle_expr = function - | Term t -> - let (side_info, t') = handle_term t in (side_info, Term t') - | Every (k, v, t, q) -> - let (side_info, q') = - List.map q ~f:handle_literal - |> List.fold ~f:(fun (side_info, q) (side_info', term) -> - (side_info @ side_info', q @ [term])) - ~init:empty - in (side_info, Every (k, v, t, q')) - and handle_literal : literal -> (('a * term) list * literal) = function - | Exists (exprs, with_statement) -> - let (side_info, exprs') = - List.map exprs ~f:handle_expr - |> List.fold ~init:empty ~f:combine - in (side_info, Exists (exprs', with_statement)) - | Expr (expr, with_statement) -> - let (side_info, expr') = handle_expr expr in - (side_info, Expr (expr', with_statement)) - | Negate (expr, with_statement) -> - let (side_info, expr') = handle_expr expr in - (side_info, Negate (expr', with_statement)) - in - let { body = q; head; _ } = rule in - - let (side_info, query) = List.map ~f:handle_literal q |> List.fold ~init:empty ~f:combine in - let (side_info', head') = match head with - | (rf, Assignment (op, term)) -> - let (side_info, term') = handle_term term in - (side_info, (rf, Assignment (op, term'))) - | (rf, Function (op, args, term)) -> - let (side_info, term') = handle_term term in - (side_info, (rf, Function (op, args, term'))) - | (rf, Set term) -> - let (side_info, term') = handle_term term in - (side_info, (rf, Set term')) - in - (side_info @ side_info', { rule with body = query; head = head' }) - - -let rewrite_with (env : environ) (q : query) : ((string * string) list * lean_expression list) = - let empty = ([], []) in - let combine (x1, y1) (x2, y2) = (x1 @ x2, y1 @ y2) in - let rec handle_term substitutions : term -> ((string * string) list * lean_expression list) = function - | Var name as v -> - (match List.Assoc.find ~equal:equal_term substitutions v with - | Some value -> - let new_identifier = gensym name in - ([(name, new_identifier)], - [Application (Identifier "Eq", [Identifier new_identifier; - compile_term env value])]) - | None -> empty) - | Ref (target, args) -> - let target = term_of_ref_target target in - let terms = [target] @ args in - List.map terms ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine - | Array xs | Set xs -> - List.map xs ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine - | Object kvs -> List.map ~f:snd kvs - |> List.map ~f:(handle_term substitutions) - |> List.fold ~init:empty ~f:combine - | Call (x, xs) -> - List.map ((Ref x : term)::xs) ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine - | ArrayComprehension _ -> assert false (* TODO *) - | ObjectComprehension _ -> assert false (* TODO *) - | SetComprehension _ -> assert false (* TODO *) - | _ -> empty - and handle_expr substitutions = function - | Term t -> handle_term substitutions t - | Every (_, _, _, q) -> - List.map q ~f:handle_literal |> List.fold ~init:empty ~f:combine - and handle_literal : literal -> ((string * string) list * lean_expression list) = function - | Exists (exprs, Some with_statement) -> - List.map exprs ~f:(handle_expr with_statement) - |> List.fold ~init:empty ~f:combine - | Expr (expr, Some with_statement) -> - handle_expr with_statement expr - | Negate (expr, Some with_statement) -> - handle_expr with_statement expr - | _ -> - empty - in - List.map ~f:handle_literal q |> List.fold ~init:empty ~f:combine - -let rec compile_expr env : expr -> (environ * lean_expression) = function - | Term t -> - (match t with - (* Call is a special case, being the only kind of "term" that affects scope. *) - | Call ((Var "assign", []), [ Var name; rhs ]) -> - (* Assumption: `name' is in the `env' because of our up-front variable analysis, but we've marked it as unassigned. *) - let { lean_id; kind; assigned } = Map.find_exn env name in - assert ((not assigned) || not (equal_definition_kind kind Complete)) ; - - let variable = { assigned = true; lean_id; kind } in - let env' = Map.set env ~key:name ~data:variable in - ( - env', - compile_term env' (Call ((Var "eq", []), [ Var name; rhs ])) - ) - | t -> (env, compile_term env t)) - | Every (Some key, value, domain, query) -> - let domain' = compile_term env domain in - (* Extend the environment with the key and value. *) - let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; kind = Complete; assigned = true } - |> Map.set ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in - let (env'', query') = compile_query env' query in - (env'', - ForAll - (([key; value], "Rego.Any"), - fold_and - [(Application - ((Identifier "Membership.mem"), - [Tuple [Identifier key; Identifier value]; domain'])); - query'] - |> simplify_expression)) - | Every (None, value, domain, query) -> - let domain' = compile_term env domain in - (* Extend the environment with the value. *) - let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in - let (env'', query') = compile_query env' query in - (env'', - ForAll - (([value], "Rego.Any"), - fold_and - [(Application - ((Identifier "Membership.mem"), - [Identifier value; domain'])); - query'] - |> simplify_expression)) - -and compile_literal env : literal -> (environ * lean_expression) = function - | Exists (exprs, _) -> - let (env', form) = compile_query env (List.map ~f:literal_of_expr exprs) in - (env', form) - | Expr (expr, _) -> - let (env', inner) = compile_expr env expr in - (env', Application (Identifier "Ne", [inner; Application (Identifier "Rego.Any.bool", [Bool false])])) - | Negate (expr, _) -> - let (env', form) = compile_literal env (Expr (expr, None)) in - (env', Application (Identifier "Not", [form])) - -and compile_query env literals : (environ * lean_expression) = - let (env', forms) = map_with_environment_updates env literals compile_literal in - let form = match forms with - | [x] -> x - | xs -> xs |> fold_and |> simplify_expression in - (env', form) - -and compile_comprehension env anonymous_name (comp : term) = - match comp with - | ArrayComprehension (value, q) -> - let { free; _ } = extract_variables env [literal_of_term value] in - let env = List.map free ~f:(fun identifier -> - (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) - |> extend_environment env in - let (_, form) = compile_query env q in - Application (Identifier "array_specified_by", [Identifier anonymous_name; form]) - | SetComprehension (value, q) -> - let { free; _ } = extract_variables env [literal_of_term value] in - let env = List.map free ~f:(fun identifier -> - (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) - |> extend_environment env in - let (_, form) = compile_query env q in - Application (Identifier "set_specified_by", [Identifier anonymous_name; form]) - | ObjectComprehension ((key, value), q) -> - let { free; _ } = extract_variables env [literal_of_term (term_of_object_key key)] in - let { free = free'; _ } = extract_variables env [literal_of_term value] in - let free = free @ free' in - let env = List.map free ~f:(fun identifier -> - (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) - |> extend_environment env in - let (_, form) = compile_query env q in - Application (Identifier "object_specified_by", [Identifier anonymous_name; form]) - | _ -> failwith (show_term comp |> - (Printf.sprintf "called compile_comprehension on non-comprehension %s")) - -and compile_rule env subjects rule : (environ * lean_expression) list = - let (comprehensions, rule) = lift_term env rule - (fun _env term -> - let anonymous_name = gensym "comprehension" in - match term with - | ArrayComprehension _ | SetComprehension _ | ObjectComprehension _ -> - Some (anonymous_name, Var anonymous_name) - | _ -> None) in - (* Each comprehension is now mapped to an anonymous name. We'll add it to the - scope so we don't have an unbound variable error when we compile the - modified rule. *) - let env = List.map comprehensions - ~f:(fun (anonymous_name, _) -> - (anonymous_name, { lean_id = anonymous_name; kind = Parameter; assigned = true })) - |> extend_environment env in - - let { body = literals; _ } = rule in - - (* TODO: Deal with user-defined functions. *) - (* let (_, literals) = lift_term env literals *) - (* (fun env term -> *) - (* match term with *) - (* | Call ((Var identifier, []), _args) -> *) - (* (match Map.find env identifier with *) - (* | Some { kind = FunctionRule ; _ } -> *) - (* let anon_name = gensym "function_call" in *) - (* Some (anon_name, Var anon_name) *) - (* | _ -> None) *) - (* | _ -> None) in *) - - - let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in - let env = List.map new_identifiers - ~f:(fun (old_name, anonymous_name) -> - (old_name, { lean_id = anonymous_name; kind = Parameter; assigned = true })) - |> extend_environment env in - - let { free; bound; used } = extract_variables env literals in - let (used', parameters, env_updates, subject_constraints) = - let explicit_parameters = match rule |> kind_and_args_of_rule with - | `FunctionRule (args, _) -> - List.filter_map args ~f:(function - | Var id -> Some id - | _ -> None) - | _ -> [] - in - let candidates = match rule |> kind_and_args_of_rule with - | `ScalarRule term | `SetRule term -> - [term] - | `ObjectRule (key, value) -> - [key; value] - | `FunctionRule (args, output) -> - args @ [output] - in - - let env_updates_and_constraints = - List.map2_exn - subjects - candidates - ~f:(fun subject -> - function - (* In this case, we're dealing with a formal parameter, so we want - to have it be an alias of the lean_id for the subject. *) - | Var identifier when List.mem (bound @ explicit_parameters) identifier ~equal:String.equal -> - (Some identifier, - [(identifier, { lean_id = subject; kind = Parameter; assigned = true })], - None) - | term -> - let { free; _ } = extract_variables env [literal_of_term term] in - (None, - [(subject, { lean_id = subject; kind = Parameter; assigned = true })] - @ List.map free - ~f:(fun name -> - (name, { lean_id = gensym "param"; kind = Parameter; assigned = true })), - Some (Call ((Var "eq", []), [Var subject; term]) : term))) - in - - let parameters = env_updates_and_constraints |> List.filter_map ~f:(fun (x, _, _) -> x) in - let non_parameters = List.filter_map candidates ~f:(function - | Var id -> Some id - | _ -> None) in - - (non_parameters, - parameters, - env_updates_and_constraints |> List.map ~f:(fun (_, x, _) -> x) |> List.concat, - env_updates_and_constraints |> List.filter_map ~f:(fun (_, _, x) -> x)) - in - let env' = extend_environment env env_updates in - let bound = List.filter bound ~f:(fun identifier -> not (List.mem parameters identifier ~equal:String.equal)) in - - let free = free |> - List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in - - let used = used @ used' in - let used = used |> - List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in - let used = used - |> List.filter ~f:(fun name -> match Map.find_exn env' name with - | { kind = Complete; _ } -> false - | _ -> true) in - - let env' = - List.concat - [List.map free ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); - List.map used ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); - List.map bound ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = false }))] - |> extend_environment env' in - - let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env' k in lean_id) in - let constraints = - List.filter_map used ~f:(fun name -> - match Map.find env name with - | Some { lean_id; kind = ScalarRule; _ } -> - Some - (Application (Identifier "scalar_specified_by", - [Identifier lean_id; - Identifier (lean_id_of_identifier name)])) - | Some { lean_id; kind = SetRule; _ } -> - Some - (Application (Identifier "set_specified_by", - [Identifier lean_id; - Identifier (lean_id_of_identifier name)])) - | Some { lean_id; kind = ObjectRule; _ } -> - Some - (Application (Identifier "object_specified_by", - [Identifier lean_id; - Identifier (lean_id_of_identifier name)])) - | Some { lean_id; kind = FunctionRule; _ } -> - Some - (Application (Identifier "function_specified_by", - [Identifier lean_id; - Identifier (lean_id_of_identifier name)])) - | Some _ -> None - | None -> failwith (Printf.sprintf "unbound variable %s" name)) in - - let subject_constraints = List.map subject_constraints ~f:literal_of_term in - let (env'', form) = compile_query env' (literals @ subject_constraints) in - let comprehension_constraints = - List.map comprehensions ~f:(fun (name, form) -> compile_comprehension env name form) in - let quantified_names = free @ bound @ used in - - (env'', - if List.is_empty quantified_names then - fold_and [form] |> simplify_expression - else - Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), - constraints @ comprehension_constraints @ [form] - |> fold_and - |> simplify_expression)) - :: (match rule.otherwise with - | Some branch -> compile_rule env subjects branch - | None -> []) - -let compile_definition env (rules : rule list) = - assert (not (List.is_empty rules)); - - (* Assert that all rules are of the same kind. *) - assert (1 = (List.map rules ~f:definition_kind_of_rule - |> uniq equal_definition_kind - |> List.length)); - - (* Rules are grouped based on their head, so we can determine which variable - we're defining by looking at any arbitrarily-chosen rule. It's easy enough - to get the first. *) - let variable_being_defined = - match List.hd_exn rules with - | { head = (rf, _); _ } -> rf - in - - let (default_rules, conditional_rules) = - List.partition_tf rules ~f:(function - | { default = true; _ } -> true - | _ -> false) - in - (* There can be only one default rule. *) - assert (List.length default_rules <= 1); - - let subjects = - match List.hd_exn rules |> kind_and_args_of_rule with - | `ScalarRule _ | `SetRule _ -> - [gensym "x"] - | `ObjectRule _ -> - [gensym "k"; gensym "v"] - | `FunctionRule (args, _) -> - List.map args ~f:(fun _ -> gensym "arg") - @ [gensym "y"] - in - let conditional_rules = - List.map ~f:(compile_rule env subjects) conditional_rules - |> List.concat in - let conditional_arms = - List.mapi conditional_rules ~f:(fun i (_env', body) -> - (body, - (Printf.sprintf "rule%d" i, - [body], - List.map subjects ~f:(fun x -> Identifier x)))) in - let default_arms = - List.map default_rules ~f:(fun _ -> - let other_rule_bodies = List.map ~f:fst conditional_arms in - let body_form = - Application (Identifier "Not", [fold_or other_rule_bodies]) - in - ("rule_default", - [body_form], - List.map subjects ~f:(fun x -> Identifier x))) in - - let form = - let string_of_reference : reference -> string = function - | (Var name, []) -> name - | (Var name, [_]) -> name - | _ -> assert false (* unreachable *) - in - Inductive - (string_of_reference variable_being_defined, - [(subjects, "Rego.Any")], - List.append (List.map ~f:snd conditional_arms) default_arms) - in (env, form) - -let compile_policy env (rules : rule list) = - let group accessor l = - let rec grouping acc = function - | [] -> acc - | hd::tl -> - let l1,l2 = List.partition_tf ~f:(fun x -> equal_reference (accessor x) (accessor hd)) tl in - grouping ((hd::l1)::acc) l2 - in - grouping [] l in - let head_of_rule = function | {head = (rf, _); _ } -> rf in - let by_reference = group head_of_rule rules in - let env' = - List.map by_reference ~f:(function - | { head = ((Var name, []), Assignment _); _ } :: _ -> - (name, { lean_id = name ; kind = ScalarRule; assigned = true }) - | { head = ((Var name, [_]), Assignment _); _ } :: _ -> - (name, { lean_id = name ; kind = ObjectRule; assigned = true }) - | { head = ((Var name, []), Set _); _ } :: _ -> - (name, { lean_id = name ; kind = SetRule; assigned = true }) - | { head = ((Var name, []), Function _); _ } :: _ -> - (name, { lean_id = name ; kind = FunctionRule; assigned = true }) - | _ -> failwith "policy rule head is not a variable") - |> extend_environment env in - map_with_environment_updates env' by_reference compile_definition - -let compile_error_condition env = - Map.to_alist env - |> List.filter_map ~f:(fun (k, v) -> - match v with - | { kind = ScalarRule; _ } -> - let anon_name = gensym "the" in - Some( - ExistsUnique ( - ([anon_name], "Rego.Any"), - Application (Identifier "scalar_specified_by", - [Identifier anon_name; Identifier k]))) - | { kind = FunctionRule; _ } -> - let args_name = gensym "args" in - let value_name = gensym "value" in - Some( - ForAll - (([args_name], "Rego.Any"), - ExistsUnique ( - ([value_name], "Rego.Any"), - Application - (Identifier "eq", - [Application (Identifier k, [Identifier args_name]); - Identifier value_name])))) - | _ -> None) - |> fold_and - -let compile_package = - let string_of_reference : reference -> string = function - | (Var name, xs) -> - [name] - @ List.map xs ~f:(function - | Scalar (String x) -> x - | _ -> failwith "unreachable") - |> String.concat ~sep:"." - - | _ -> assert false (* unreachable *) - in - let compile_import = function - | { alias = None; path } -> - Printf.sprintf "imports %s" - (string_of_reference path) - |> String.escaped - | { alias = Some alias; path } -> - Printf.sprintf "imports %s as %s" - (string_of_reference path) - alias - |> String.escaped - in - function - | { path; imports; policy } -> - let policy = List.map ~f:transform_rule_with_ref_head policy |> List.concat in - let (env', forms) = compile_policy toplevel policy in - let error_form = Define ("rego_error", compile_error_condition env') in - [Comment (Printf.sprintf "package %s" - (string_of_reference path) - |> String.escaped)] - @ List.map imports ~f:(fun x -> Comment (compile_import x)) - @ forms - @ [error_form] diff --git a/rego-proofs/compiler-rewrite/lib/compiler.mli b/rego-proofs/compiler-rewrite/lib/compiler.mli deleted file mode 100644 index 0bef961..0000000 --- a/rego-proofs/compiler-rewrite/lib/compiler.mli +++ /dev/null @@ -1,13 +0,0 @@ -open Ast -open Lean - -type environ - -type analysis_result = - { bound : string list; - free : string list; - used : string list } - -val extract_variables_wrapper : query -> analysis_result -val transform_rule_with_ref_head : rule -> rule list -val compile_package : package -> lean_expression list diff --git a/rego-proofs/compiler-rewrite/lib/dune b/rego-proofs/compiler-rewrite/lib/dune deleted file mode 100644 index 72a5e68..0000000 --- a/rego-proofs/compiler-rewrite/lib/dune +++ /dev/null @@ -1,9 +0,0 @@ -(library - (name compiler_rewrite) - (libraries core unix yojson) - (preprocess - (pps ppx_deriving.eq ppx_deriving.show ppx_fields_conv))) - -(env - (dev - (flags (:standard -w -66 -w -37 -w -30 -w -32)))) diff --git a/rego-proofs/compiler-rewrite/lib/lean.ml b/rego-proofs/compiler-rewrite/lib/lean.ml deleted file mode 100644 index 6bb4265..0000000 --- a/rego-proofs/compiler-rewrite/lib/lean.ml +++ /dev/null @@ -1,63 +0,0 @@ -open Core - -type lean_expression = - | Comment of string - | Identifier of string - | Bool of bool - | String of string - | Number of float - | List of lean_expression list - | Tuple of lean_expression list - | Application of lean_expression * lean_expression list - | Define of string * lean_expression - | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list - | ForAll of judgement * lean_expression - | Exists of judgement * lean_expression - | ExistsUnique of judgement * lean_expression -[@@deriving eq, show] - -and judgement = string list * string [@@deriving eq, show] - -let fmt_judgement : judgement -> string = function - | vars, t -> Printf.sprintf "(%s : %s)" (String.concat ~sep:" " vars) t - -let rec fmt_lean_expression : lean_expression -> string = function - | Comment s -> Printf.sprintf "\n-- %s\n" s - | Identifier s -> s - | Bool b -> if b then "True" else "False" - | String s -> Printf.sprintf "\"%s\"" s - | Number n -> Float.to_string n - | List xs -> - Printf.sprintf "[%s]" - (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs)) - | Tuple xs -> - Printf.sprintf "(%s)" - (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs)) - | Application (head, args) -> - Printf.sprintf "(%s %s)" (fmt_lean_expression head) - (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args)) - | Define (ident, expr) -> - Printf.sprintf "def %s := (%s)" ident (fmt_lean_expression expr) - | ForAll (j, expr) -> - Printf.sprintf "∀ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) - | Exists (j, expr) -> - Printf.sprintf "∃ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) - | ExistsUnique (j, expr) -> - Printf.sprintf "∃! %s, %s" (fmt_judgement j) (fmt_lean_expression expr) - | Inductive (name, judgements, arms) -> - let fmt_arm (arm_name, exprs, values) = - let head = - Printf.sprintf - "%s %s" - name - (List.map ~f:fmt_lean_expression values |> String.concat ~sep:" ") - in - let body = - List.map ~f:fmt_lean_expression exprs - |> String.concat ~sep:" → " - in - Printf.sprintf " | %s : %s → %s" arm_name body head - in - Printf.sprintf "inductive %s %s where\n%s" name - (List.map ~f:fmt_judgement judgements |> String.concat ~sep:" ") - (List.map ~f:fmt_arm arms |> String.concat ~sep:"\n") diff --git a/rego-proofs/compiler-rewrite/lib/lean.mli b/rego-proofs/compiler-rewrite/lib/lean.mli deleted file mode 100644 index f6a769a..0000000 --- a/rego-proofs/compiler-rewrite/lib/lean.mli +++ /dev/null @@ -1,25 +0,0 @@ -type lean_expression = - | Comment of string - | Identifier of string - | Bool of bool - | String of string - | Number of float - | List of lean_expression list - | Tuple of lean_expression list - | Application of lean_expression * lean_expression list - | Define of string * lean_expression - | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list - | ForAll of judgement * lean_expression - | Exists of judgement * lean_expression - | ExistsUnique of judgement * lean_expression - -and judgement = string list * string - -val equal_lean_expression : lean_expression -> lean_expression -> bool -val equal_judgement : judgement -> judgement -> bool -val pp_lean_expression : Format.formatter -> lean_expression -> unit -val show_lean_expression : lean_expression -> string -val pp_judgement : Format.formatter -> judgement -> unit -val show_judgement : judgement -> string - -val fmt_lean_expression : lean_expression -> string diff --git a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml b/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml deleted file mode 100644 index 1d9d926..0000000 --- a/rego-proofs/compiler-rewrite/test/compiler_rewrite.ml +++ /dev/null @@ -1,138 +0,0 @@ -open Core -open Compiler_rewrite - -module To_test = struct - let extract_variables = Compiler.extract_variables_wrapper - let transform_ref_head = Compiler.transform_rule_with_ref_head - let fmt = Lean.fmt_lean_expression -end - -let strings = - Alcotest.testable - (Format.pp_print_list Format.pp_print_string) - (List.equal String.equal) - -let extract_query policy = - match Ast.ast_of_string policy with - | { policy = [ { body; _ } ]; _ } -> body - | _ -> failwith "failed to parse" - -let test_local_extraction_simple_1 () = - let policy_code = {| -package test - -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 - -let test_local_extraction_simple_2 () = - let policy_code = {| -package test - -q { - x := 2 - y := 3 - 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 - -let test_local_dependent_on_previously_defined_local () = - let policy_code = {| -package test - -q { - x := 2 - 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 - -let test_free_extraction_simple_1 () = - let policy_code = {| -package test - -q { - y := 7 - 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; - Alcotest.(check strings) - "expected identifier list" [ "y" ] bound - -let test_free_extraction_simple_2 () = - let policy_code = {| -package test - -q { - y := z - 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; - Alcotest.(check strings) - "expected identifier list" [ "y" ] bound - -let test_identifier () = - let open Compiler_rewrite.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 rule = { head = ((Var "fruit", [Var "apple"; Var "seeds"]), Assignment (Assign, (Scalar (Number 12.)))); - default = false; - body = [Expr (Term (Scalar (Bool true)), None)]; - otherwise = None } in - Alcotest.(check int) "expected rules" - 2 - (To_test.transform_ref_head rule |> List.length) - -let () = - let open Alcotest in - run "Compiler" - [ - ( "free variable extraction", - [ - test_case "free variable extraction simple (1)" `Quick - test_free_extraction_simple_1; - test_case "free variable extraction simple (2)" `Quick - test_free_extraction_simple_2; - ] ); - ( "local extraction", - [ - test_case "local extraction simple (1)" `Quick - test_local_extraction_simple_1; - test_case "local extraction simple (2)" `Quick - test_local_extraction_simple_2; - test_case - "local extraction with local dependent on previously-defined local \ - (1)" - `Quick test_local_dependent_on_previously_defined_local - ] ); - ( "nested definitions", - [ - test_case "local nested definitions (1)" `Quick - test_transform_simple_1; - ] ) ; - ( "ast formatting ", - [ test_case "identifier compilation" `Quick test_identifier ] ); - ] 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 -;;; -;;; 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 -;;; . - -(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/.gitignore b/rego-proofs/compiler/.gitignore new file mode 100644 index 0000000..e35d885 --- /dev/null +++ b/rego-proofs/compiler/.gitignore @@ -0,0 +1 @@ +_build diff --git a/rego-proofs/compiler/.ocamlformat b/rego-proofs/compiler/.ocamlformat new file mode 100644 index 0000000..c870de9 --- /dev/null +++ b/rego-proofs/compiler/.ocamlformat @@ -0,0 +1 @@ +version=0.26.1 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/bin/main.ml b/rego-proofs/compiler/bin/main.ml new file mode 100644 index 0000000..f1b213c --- /dev/null +++ b/rego-proofs/compiler/bin/main.ml @@ -0,0 +1,12 @@ +open Core +open Compiler +open Compiler__.Ast +open Compiler__.Lean + +let () = + let file_name = Array.get (Sys.get_argv ()) 1 in + let policy_code = In_channel.read_all file_name in + ast_of_string policy_code + |> compile_package + |> List.map ~f:fmt_lean_expression + |> List.iter ~f:print_endline diff --git a/rego-proofs/compiler/compiler.opam b/rego-proofs/compiler/compiler.opam new file mode 100644 index 0000000..8dbe763 --- /dev/null +++ b/rego-proofs/compiler/compiler.opam @@ -0,0 +1,24 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Compiler from Rego to a Lean shallow embedding" +maintainer: ["Jakob Kreuze"] +authors: ["Jakob Kreuze"] +depends: [ + "ocaml" + "dune" {>= "3.11"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] diff --git a/rego-proofs/compiler/dune-project b/rego-proofs/compiler/dune-project new file mode 100644 index 0000000..dc06bf3 --- /dev/null +++ b/rego-proofs/compiler/dune-project @@ -0,0 +1,14 @@ +(lang dune 3.11) + +(name compiler) + +(generate_opam_files true) + +(authors "Jakob Kreuze") + +(maintainers "Jakob Kreuze") + +(package + (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 -;;; -;;; 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 -;;; . - -(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 ( - - - - - - - - - - - - - - compile - - lean-expression? - - lean-builtin-function? - reference->lean-name)) - -;; For inductive predicates -(define-class () - ;; 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 () - ;; 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 () - (identifier #:init-keyword #:identifier) - (type #:init-keyword #:type) - (value #:init-keyword #:value)) - -(define-class ()) - -;; Compiled to ∃ -(define-class () - ;; list of identifier/type pairs - (variables #:init-keyword #:variables - #:getter variables) - (body #:init-keyword #:body - #:getter body)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ variables body) - (let ((inner (with-modified-slot form 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∀ -(define-class () - ;; list of identifier/type pairs - (variables #:init-keyword #:variables - #:getter variables) - (body #:init-keyword #:body - #:getter body)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ variables body) - (let ((inner (with-modified-slot form 'body - (tree-map body f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∧ -(define-class () - (clauses #:init-keyword #:clauses - #:getter clauses)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ clauses) - (let ((inner (with-modified-slot form 'clauses - (tree-map clauses f scope breadcrumb)))) - (f scope breadcrumb inner))))) - -;; Compiled to ∨ -(define-class () - (clauses #:init-keyword #:clauses - #:getter clauses)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 () - (kind #:init-keyword #:kind - #:getter kind) - (left #:init-keyword #:left - #:getter left) - (right #:init-keyword #:right - #:getter right)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ kind left right) - (let ((new (make - #: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 () - (name #:init-keyword #:name - #:getter name) - (args #:init-keyword #:args - #:getter args)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 () - ;; 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 () - (identifiers #:init-keyword #:identifiers - #:getter identifiers)) - -;; Is this needed? -(define-class ()) - -(define-class () - (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 )) - (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 ; ¬ (~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 )) - (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 )) - (string-concatenate - `("∃ " - ,(string-join - (map (lambda (identifier) - (format #f "(~a : Rego.Any)" (compile identifier))) - (variables x)) - " ") - ", " - ,(wrap (compile (body x)))))) - -(define-method (compile (x )) - (string-concatenate - `("∀ " - ,(string-join - (map (lambda (identifier) - (format #f "(~a : Rego.Any)" (compile identifier))) - (variables x)) - " ") - ", " - ,(wrap (compile (body x)))))) - -(define-method (compile (x )) - (string-concatenate - `(,(name x) - " " - ,(string-join (map (compose wrap compile) (args x)) " ")))) - -(define-method (compile (x )) - (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 )) - (string-join (map (compose wrap compile) (clauses x)) " ∧ ")) - -(define-method (compile (x )) - (string-join (map (compose wrap compile) (clauses x)) " ∨ ")) - -(define-method (compile (x )) - (string-concatenate - `("(" - ,(string-join (map (compose wrap compile) (items x)) ", ") - ")"))) - -(define-method (compile (x )) - (match x - (($ name) name))) - -(define-method (compile (x )) - (match x - (($ value) (compile value)))) - -(define-method (compile (x )) - (match x - (($ 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 )) - (define recur - (match-lambda - ((($ 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 - (($ parts) (format #f "~a~a" - (compile (first parts)) - (recur (drop parts 1)))))) - -(define-method (compile (x )) - (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 )) - (format #f "Rego.Any.bool ~a" (if x "True" "False"))) - -(define-method (compile (x )) - (format #f "Rego.Any.str \"~a\"" x)) - -(define-method (compile (x )) - (format #f "Rego.Any.num ~a" x)) - -(define-method (compile (x )) - (format #f "[~a]" (string-join (map compile x) ", "))) - -(define-method (compile (x )) - (format #f "#[~a]" (string-join (map compile (array->list x)) ", "))) - - - -(define (lean-expression? expr) - (or (is-a? expr ) - (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 - (($ (x)) (sanitize x)) - (($ (x xs ...)) - (if (and (equal? (to-pretty-sexp x) `( "internal")) - (equal? (to-pretty-sexp xs) (list `( "member_2")))) - "Array.contains" - (error "Unimplemented"))))) diff --git a/rego-proofs/compiler/lib/ast.ml b/rego-proofs/compiler/lib/ast.ml new file mode 100644 index 0000000..98d8375 --- /dev/null +++ b/rego-proofs/compiler/lib/ast.ml @@ -0,0 +1,275 @@ +open Core +open Yojson.Basic.Util + +(* AST types. *) + +type expr = Term of term | Every of string option * string * term * query +[@@deriving eq, show] + +and literal = + | Exists of expr list * with_modifier option + | Expr of expr * with_modifier option + | Negate of expr * with_modifier option +[@@deriving eq, show] + +and query = literal list [@@deriving eq, show] + +and term = + | Scalar of scalar + | Var of string + | Ref of reference + | Array of term list + | Object of (object_key * term) list + | Set of term list + | ArrayComprehension of term * query + | ObjectComprehension of (object_key * term) * query + | SetComprehension of term * query + | Call of reference * term list +[@@deriving eq, show] + +and scalar = String of string | Number of float | Bool of bool | Null +[@@deriving eq, show] + +and reference = ref_target * term list [@@deriving eq, show] + +and ref_target = + | Var of string + | Array of term list + | Object of (object_key * term) list + | Set of term list + | ArrayComprehension of term * query + | ObjectComprehension of (object_key * term) * query + | SetComprehension of term * query + | Call of reference * term list +[@@deriving eq, show] + +and object_key = Scalar of scalar | Ref of reference | Var of string +[@@deriving eq, show] + +and with_modifier = (term * term) list [@@deriving eq, show] + +type assign_operator = Assign | Unify [@@deriving eq, show] +type rule_head_lhs = reference [@@deriving eq, show] + +type rule_head_rhs = + | Assignment of assign_operator * term + | Function of assign_operator * term list * term + | Set of term +[@@deriving eq, show] + +type rule_head = rule_head_lhs * rule_head_rhs [@@deriving eq, show] + +type rule = { + default : bool; + head : rule_head; + body : query; + otherwise : rule option; +} +[@@deriving eq, show] + +type import = { alias : string option; path : reference } [@@deriving eq, show] + +type package = { path : reference; imports : import list; policy : rule list } +[@@deriving eq, show] + +(* Additional JSON utility functions. *) + +let is_null : Yojson.Basic.t -> bool = function `Null -> true | _ -> false + +let to_bool_or_false : Yojson.Basic.t -> bool = function + | `Bool b -> b + | _ -> false + +let to_list_or_empty : Yojson.Basic.t -> Yojson.Basic.t list = function + | `Null -> [] + | `List xs -> xs + | _ -> failwith "Not a list or null" + +let object_key_of_term : term -> object_key = function + | Scalar s -> Scalar s + | Ref r -> Ref r + | Var v -> Var v + | _ -> failwith "failed to convert term to object_key" + +(* Code to parse the JSON output of `opa parse`. *) + +let rec parse_term (tree : Yojson.Basic.t) : term = + let term_type = tree |> member "type" |> to_string in + match term_type with + | "var" -> Var (tree |> member "value" |> to_string) + | "ref" -> Ref (tree |> member "value" |> to_list |> parse_ref) + | "null" -> Scalar Null + | "boolean" -> Scalar (Bool (tree |> member "value" |> to_bool)) + | "number" -> Scalar (Number (tree |> member "value" |> to_number)) + | "string" -> Scalar (String (tree |> member "value" |> to_string)) + | "array" -> + Array (tree |> member "value" |> to_list |> List.map ~f:parse_term) + | "set" -> Set (tree |> member "value" |> to_list |> List.map ~f:parse_term) + | "object" -> + Object + (tree |> member "value" |> to_list + |> List.map ~f:(function + | `List [ x; y ] -> + (x |> parse_term |> object_key_of_term, y |> parse_term) + | _ -> failwith "ill-formed object")) + | "arraycomprehension" -> + ArrayComprehension + ( tree |> member "value" |> member "term" |> parse_term, + tree |> member "value" |> member "body" |> to_list + |> List.map ~f:parse_literal ) + | "setcomprehension" -> + SetComprehension + ( tree |> member "value" |> member "term" |> parse_term, + tree |> member "value" |> member "body" |> to_list + |> List.map ~f:parse_literal ) + | "objectcomprehension" -> + ObjectComprehension + ( ( tree |> member "value" |> member "key" |> parse_term + |> object_key_of_term, + tree |> member "value" |> member "value" |> parse_term ), + tree |> member "value" |> member "body" |> to_list + |> List.map ~f:parse_literal ) + | "call" -> ( + match tree |> member "value" |> to_list with + | func :: args -> + Call + ( func |> member "value" |> to_list |> parse_ref, + List.map ~f:parse_term args ) + | _ -> failwith "ill-formed call") + | _ -> failwith ("unsupported term type " ^ term_type) + +and parse_literal tree : literal = + let with_expr = tree |> member "with" in + let with_expr = + match with_expr with + | `Null -> None + | `List xs -> + Some + (List.map xs ~f:(fun x -> + ( x |> member "target" |> parse_term, + x |> member "value" |> parse_term ))) + | _ -> + failwith + ("ill-formed with expression " ^ Yojson.Basic.to_string with_expr) + in + match tree |> member "terms" with + | `List (func :: args) -> + let term = + Term + (Call + ( func |> member "value" |> to_list |> parse_ref, + List.map ~f:parse_term args )) + in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) + + | `List _ -> failwith "ill-formed call" + | x -> + if not (x |> member "symbols" |> is_null) then + Exists + ( x |> member "symbols" |> to_list + |> List.map ~f:(fun x -> Term (parse_term x)), + with_expr ) + else if x |> member "domain" |> is_null then + let term = Term (parse_term x) in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) + else + let term = + Every + ( (if x |> member "key" |> is_null then None + else Some (x |> member "key" |> member "value" |> to_string)), + x |> member "value" |> member "value" |> to_string, + x |> member "domain" |> parse_term, + List.map ~f:parse_literal (x |> member "body" |> to_list) ) + in + if tree |> member "negated" |> to_bool_or_false then + Negate (term, with_expr) + else Expr (term, with_expr) + +and parse_ref_target tree : ref_target = + let term = parse_term tree in + match term with + | Var term -> Var term + | Array term -> Array term + | Object term -> Object term + | Set term -> Set term + | ArrayComprehension (term, y) -> ArrayComprehension (term, y) + | ObjectComprehension (term, y) -> ObjectComprehension (term, y) + | SetComprehension (term, y) -> SetComprehension (term, y) + | Call (term, y) -> Call (term, y) + | _ -> failwith ("unsupported ref_target " ^ show_term term) + +and parse_ref tree = + match tree with + | target :: args -> (parse_ref_target target, List.map ~f:parse_term args) + | _ -> failwith "empty reference" + +let parse_head tree = + (* Variables are desugared to empty references. *) + let lhs = tree |> member "ref" |> to_list |> parse_ref in + let assign_operator = + if tree |> member "assign" |> to_bool_or_false then Assign else Unify + in + let rhs = + if (tree |> member "value" |> is_null) && (not (tree |> member "key" |> is_null)) then + Set (tree |> member "key" |> parse_term) + else if not (tree |> member "args" |> is_null) then + Function + ( assign_operator, + tree |> member "args" |> to_list |> List.map ~f:parse_term, + tree |> member "value" |> parse_term ) + else Assignment (assign_operator, tree |> member "value" |> parse_term) + in + (lhs, rhs) + +let rec parse_rule tree = + { + default = tree |> member "default" |> to_bool_or_false; + head = tree |> member "head" |> parse_head; + body = List.map ~f:parse_literal (tree |> member "body" |> to_list_or_empty); + otherwise = + (match tree |> member "else" with + | `Null -> None + | else_branch -> Some (parse_rule else_branch)); + } + +let parse_import_path tree = + match tree |> member "type" |> to_string with + | "ref" -> tree |> member "value" |> to_list |> parse_ref + | _ -> failwith "unimplemented" + +let parse_import tree = + { + alias = tree |> member "alias" |> to_string_option; + path = tree |> member "path" |> parse_import_path; + } + +let parse_package tree = tree |> member "path" |> to_list |> parse_ref + +let parse_tree tree = + { + path = tree |> member "package" |> parse_package; + imports = + List.map ~f:parse_import (tree |> member "imports" |> to_list_or_empty); + policy = List.map ~f:parse_rule (tree |> member "rules" |> to_list_or_empty); + } + +(* OPA interaction. *) + +let invoke ?(stdin = "") ?(env = [||]) cmd = + let ic, oc, ec = UnixLabels.open_process_full cmd ~env in + Out_channel.output_string oc stdin; + Out_channel.close oc; + let i = In_channel.input_all ic in + let e = In_channel.input_all ec in + (i, e) + +let ast_of_string policy_code = + let stdout, _ = + invoke "/home/jakob/.local/bin/opa parse -f json /dev/stdin" + ~stdin:policy_code ~env:[||] + in + Yojson.Basic.from_string stdout |> parse_tree diff --git a/rego-proofs/compiler/lib/ast.mli b/rego-proofs/compiler/lib/ast.mli new file mode 100644 index 0000000..514d5da --- /dev/null +++ b/rego-proofs/compiler/lib/ast.mli @@ -0,0 +1,108 @@ +type expr = Term of term | Every of string option * string * term * query + +and literal = + | Exists of expr list * with_modifier option + | Expr of expr * with_modifier option + | Negate of expr * with_modifier option + +and query = literal list + +and term = + | Scalar of scalar + | Var of string + | Ref of reference + | Array of term list + | Object of (object_key * term) list + | Set of term list + | ArrayComprehension of term * query + | ObjectComprehension of (object_key * term) * query + | SetComprehension of term * query + | Call of reference * term list + +and scalar = String of string | Number of float | Bool of bool | Null +and reference = ref_target * term list + +and ref_target = + | Var of string + | Array of term list + | Object of (object_key * term) list + | Set of term list + | ArrayComprehension of term * query + | ObjectComprehension of (object_key * term) * query + | SetComprehension of term * query + | Call of reference * term list + +and object_key = Scalar of scalar | Ref of reference | Var of string +and with_modifier = (term * term) list + +type assign_operator = Assign | Unify +type rule_head_lhs = reference + +type rule_head_rhs = + | Assignment of assign_operator * term + | Function of assign_operator * term list * term + | Set of term + +type rule_head = rule_head_lhs * rule_head_rhs + +type rule = { + default : bool; + head : rule_head; + body : query; + otherwise : rule option; +} + +type import = { alias : string option; path : reference } +type package = { path : reference; imports : import list; policy : rule list } + +val ast_of_string : string -> package +val show_package : package -> string + +val equal_assign_operator : assign_operator -> assign_operator -> bool +val equal_expr : expr -> expr -> bool +val equal_import : import -> import -> bool +val equal_literal : literal -> literal -> bool +val equal_object_key : object_key -> object_key -> bool +val equal_package : package -> package -> bool +val equal_query : query -> query -> bool +val equal_ref_target : ref_target -> ref_target -> bool +val equal_reference : reference -> reference -> bool +val equal_rule : rule -> rule -> bool +val equal_rule_head : rule_head -> rule_head -> bool +val equal_rule_head_lhs : rule_head_lhs -> rule_head_lhs -> bool +val equal_rule_head_rhs : rule_head_rhs -> rule_head_rhs -> bool +val equal_scalar : scalar -> scalar -> bool +val equal_term : term -> term -> bool +val equal_with_modifier : with_modifier -> with_modifier -> bool +val pp_assign_operator : Format.formatter -> assign_operator -> unit +val pp_expr : Format.formatter -> expr -> unit +val pp_import : Format.formatter -> import -> unit +val pp_literal : Format.formatter -> literal -> unit +val pp_object_key : Format.formatter -> object_key -> unit +val pp_package : Format.formatter -> package -> unit +val pp_query : Format.formatter -> query -> unit +val pp_ref_target : Format.formatter -> ref_target -> unit +val pp_reference : Format.formatter -> reference -> unit +val pp_rule : Format.formatter -> rule -> unit +val pp_rule_head : Format.formatter -> rule_head -> unit +val pp_rule_head_lhs : Format.formatter -> rule_head_lhs -> unit +val pp_rule_head_rhs : Format.formatter -> rule_head_rhs -> unit +val pp_scalar : Format.formatter -> scalar -> unit +val pp_term : Format.formatter -> term -> unit +val pp_with_modifier : Format.formatter -> with_modifier -> unit +val show_assign_operator : assign_operator -> string +val show_expr : expr -> string +val show_import : import -> string +val show_literal : literal -> string +val show_object_key : object_key -> string +val show_package : package -> string +val show_query : query -> string +val show_ref_target : ref_target -> string +val show_reference : reference -> string +val show_rule : rule -> string +val show_rule_head : rule_head -> string +val show_rule_head_lhs : rule_head_lhs -> string +val show_rule_head_rhs : rule_head_rhs -> string +val show_scalar : scalar -> string +val show_term : term -> string +val show_with_modifier : with_modifier -> string diff --git a/rego-proofs/compiler/lib/compiler.ml b/rego-proofs/compiler/lib/compiler.ml new file mode 100644 index 0000000..3b0384a --- /dev/null +++ b/rego-proofs/compiler/lib/compiler.ml @@ -0,0 +1,814 @@ +open Ast +open Core +open Lean + +type definition_kind = Complete + | Parameter + | ScalarRule + | SetRule + | ObjectRule + | FunctionRule +[@@deriving eq, show] + +let fold_or props = + match List.reduce props ~f:(fun x y -> Application (Identifier "Or", [y; x])) with + | Some x -> x + | None -> Bool true + +let fold_and props = + match List.reduce props ~f:(fun x y -> Application (Identifier "And", [y; x])) with + | Some x -> x + | None -> Bool false + +let fold_deref terms = + List.reduce_exn terms ~f:(fun x y -> Application (Identifier "Rego.Any.deref", [x; y])) + +let kind_and_args_of_rule = function + | { head = ((_, []), Assignment (_, term)); _ } -> + `ScalarRule term + | { head = ((_, _), Set term); _ } -> + `SetRule term + | { head = ((_, [key]), Assignment (_, value)); _ } -> + `ObjectRule (key, value) + | { head = ((_, _), Function (_, args, term)); _ } -> + `FunctionRule (args, term) + | { head = ((_, _), Assignment (_, _)); _ } as rule -> + failwith (Printf.sprintf "unknown rule form: %s" (show_rule rule)) + +let definition_kind_of_rule rule = + match kind_and_args_of_rule rule with + | `ScalarRule _ -> ScalarRule + | `SetRule _ -> SetRule + | `ObjectRule _ -> ObjectRule + | `FunctionRule _ -> FunctionRule + +type variable = { lean_id : string; + kind : definition_kind; + assigned : bool; + } +[@@deriving eq, show] + +module Environ = Map.Make (String) +type environ = variable Environ.t + +let gensym : string -> string = + let is_alphanum = function 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' -> true | _ -> false in + let counter = ref 0 in + fun (base : string) -> + let base = String.filter base ~f:is_alphanum in + let number = !counter in + counter := !counter + 1 ; + Printf.sprintf "v%s__%d" base number + +let extend_environment (env : environ) (vars : (string * variable) list) = + Environ.of_alist_exn vars + |> Map.merge env ~f:(fun ~key:_key -> function + | `Right v -> Some v + | `Left v -> Some v + | `Both (_, v) -> Some v) + +let toplevel = Environ.of_alist_exn [ + ("eq", { lean_id = "eq"; kind = Complete; assigned = true }); + ("equal", { lean_id = "equal"; kind = Complete; assigned = true }) + ] + +let term_of_object_key : object_key -> term = function + | Scalar s -> Scalar s + | Ref r -> Ref r + | Var v -> Var v + +let term_of_ref_target : ref_target -> term = function + | Var s -> Var s + | Array xs -> Array xs + | Object kvs -> Object kvs + | Set xs -> Set xs + | ArrayComprehension (key, q) -> ArrayComprehension (key, q) + | ObjectComprehension (key, q) -> ObjectComprehension (key, q) + | SetComprehension (key, q) -> SetComprehension (key, q) + | Call (fn, args) -> Call (fn, args) + +let ref_target_of_term : term -> ref_target = function + | Var s -> Var s + | Array xs -> Array xs + | Object kvs -> Object kvs + | Set xs -> Set xs + | ArrayComprehension (key, q) -> ArrayComprehension (key, q) + | ObjectComprehension (key, q) -> ObjectComprehension (key, q) + | SetComprehension (key, q) -> SetComprehension (key, q) + | Call (fn, args) -> Call (fn, args) + | _ -> failwith "cannot widen to ref_target" + +let literal_of_expr exp : literal = Expr (exp, None) +let literal_of_term t = Expr (Term t, None) + + +let map_with_environment_updates env xs fn = + List.fold xs ~init:(env, []) ~f:(fun (env, ys) x -> + let env', y = fn env x in + (env', ys @ [ y ])) + +let rec uniq eq = function + | [] -> [] + | hd::tl -> + if List.mem tl hd ~equal:eq then + uniq eq tl + else hd :: uniq eq tl + +type analysis_result = + { bound : string list; + free : string list; + used : string list } +[@@deriving show] + +let extract_variables (env : environ) (q : query) : analysis_result = + let empty = { bound = []; free = []; used = [] } in + let combine = + fun x y -> + match (x, y) with + | ({ bound = bound'; free = free'; used = used' }, + { bound = bound''; free = free''; used = used'' }) -> + { bound = bound' @ bound''; + free = free' @ free''; + used = used' @ used'' } in + let rec handle_term env : term -> analysis_result = function + (* If we see a variable in an assignment, and it isn't a parameter, it's bound. *) + | Call ((Var "assign", []), [ Var name; rhs ]) -> + let { bound; free; used } = handle_term env rhs in + (match Map.find env name with + | Some { kind = Parameter; _ } -> + { used = [name] @ used; free; bound } + | _ -> + { bound = [name] @ bound; free; used }) + (* Variables that haven't previously been introduced to the scope are free. *) + | Var name -> + if Map.find env name |> Option.is_some then + { free = []; bound = []; used = [name] } + else { free = [name]; bound = []; used = [] } + (* Otherwise, we'll recurse on the term. *) + | Ref (target, args) -> + let target = term_of_ref_target target in + if List.is_empty args then + handle_term env target + else + let terms = [target] @ args in + List.map terms ~f:(handle_term env) |> List.fold ~init:empty ~f:combine + | Array xs | Set xs -> + List.map xs ~f:(handle_term env) |> List.fold ~init:empty ~f:combine + | Object kvs -> List.map ~f:snd kvs + |> List.map ~f:(handle_term env) + |> List.fold ~init:empty ~f:combine + | Call (x, xs) -> + List.map ((Ref x : term)::xs) ~f:(handle_term env) |> List.fold ~init:empty ~f:combine + | _ -> empty + and handle_expr env = function + | Term t -> handle_term env t + | Every (Some key, value, _, q) -> + let env' = [(key, { lean_id = "unimportant"; kind = Complete; assigned = true }); + (value, { lean_id = "unimportant"; kind = Complete; assigned = true })] + |> extend_environment env in + List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine + | Every (None, value, _, q) -> + let var = ({ lean_id = "unimportant"; kind = Complete; assigned = true }) in + let env' = Map.set env ~key:value ~data:var in + List.map q ~f:(handle_literal env') |> List.fold ~init:empty ~f:combine + and handle_literal env : literal -> analysis_result = function + | Exists (exprs, _) -> + List.map exprs ~f:(handle_expr env) |> List.fold ~init:empty ~f:combine + | Expr (expr, _) -> handle_expr env expr + | Negate (expr, _) -> handle_expr env expr + in + let { free; bound; used } = List.map q ~f:(handle_literal env) |> List.fold ~init:empty ~f:combine in + let free = List.filter free ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in + let used = List.filter used ~f:(fun x -> List.mem bound ~equal:String.equal x |> not) in + let uniq = uniq String.equal in + { free = free |> uniq; + bound = bound |> uniq; + used = used |> uniq } + +(* This is solely for the test suite. *) +let extract_variables_wrapper (q : query) : analysis_result = + extract_variables toplevel q + +(* --- *) + +(* This breaks a nested rule, such as one defining `w.x.y.z`, into as many as + needed such that every rule is of the form `x["y"] := _`. *) +let rec transform_rule_with_ref_head : rule -> rule list = function + (* Base case - this is a simple reference that we can deal with. *) + | { head = ((_, []), _); _ } | { head = ((_, [_]), _); _ } as rule -> + [rule] + | { head = ((tgt, xs), rhs); _ } as rule -> + let tail = List.last_exn xs in + let name = gensym "anonymous" in + [{ rule with head = ((Var name, [tail]), rhs) }] @ + transform_rule_with_ref_head { rule with head = ((tgt, List.drop_last_exn xs), Assignment (Assign, Var name)) } + +(* --- *) + +let rec simplify_expression = function + | Application (Identifier "And", xs) -> + let xs' = List.map ~f:simplify_expression xs + |> List.filter ~f:(function Bool true -> false | _ -> true) + in + (match xs' with + | [] -> Bool false + | [x] -> x + | xs' -> Application (Identifier "And", xs')) + | Application (Identifier "Eq", [Application (Identifier "Rego.Any.bool", [Bool a]); + Application (Identifier "Rego.Any.bool", [Bool b])]) -> + Bool (equal_bool a b) + | Application (Identifier "Ne", [Application (Identifier "Rego.Any.bool", [Bool a]); + Application (Identifier "Rego.Any.bool", [Bool b])]) -> + Bool (not (equal_bool a b)) + | Application (Identifier "Eq", [Application (Identifier "Rego.Any.str", [String a]); + Application (Identifier "Rego.Any.str", [String b])]) -> + Bool (equal_string a b) + | Application (Identifier "Ne", [Application (Identifier "Rego.Any.str", [String a]); + Application (Identifier "Rego.Any.str", [String b])]) -> + Bool (not (equal_string a b)) + | Application (Identifier "Eq", [Application (Identifier "Rego.Any.num", [Number a]); + Application (Identifier "Rego.Any.num", [Number b])]) -> + Bool (equal_float a b) + | Application (Identifier "Ne", [Application (Identifier "Rego.Any.num", [Number a]); + Application (Identifier "Rego.Any.num", [Number b])]) -> + Bool (not (equal_float a b)) + | expr -> expr + +(* --- *) + +let rec compile_term env : term -> lean_expression = + function + | Scalar s -> + (match s with + | String s -> Application (Identifier "Rego.Any.str", [String s]) + | Number x -> Application (Identifier "Rego.Any.num", [Number x]) + | Bool b -> Application (Identifier "Rego.Any.bool", [Bool b]) + | Null -> Application (Identifier "Rego.Any.null", [])) + | Var id -> + (match Map.find env id with + | Some { lean_id; kind = Complete; assigned = true } | + Some { lean_id; kind = Parameter; assigned = true } + -> Identifier lean_id + | Some { assigned = false; _ } -> + failwith (Printf.sprintf "identifier %s used before definition" id) + | Some var -> + failwith (Printf.sprintf + "variable found in environment but of unknown form %s" + (show_variable var)) + | None -> failwith (Printf.sprintf "unbound variable %s" id)) + | Ref (target, terms) -> + let target' = compile_term env (term_of_ref_target target) in + let terms' = List.map ~f:(compile_term env) terms in + if List.is_empty terms' then + target' + else [target'] @ terms' |> fold_deref + | Array xs -> + let xs' = List.map ~f:(compile_term env) xs in + Application (Identifier "Rego.Any.array", xs') + | Set xs -> + let xs' = List.map ~f:(compile_term env) xs in + Application (Identifier "Rego.Any.set", xs') + | Object kvs -> + let compile_kv = function + | (key, value) -> + let key' = compile_term env (term_of_object_key key) in + let value' = compile_term env value in + Tuple [key'; value'] in + let kvs' = List.map ~f:compile_kv kvs in + Application (Identifier "Rego.Any.object", kvs') + | ArrayComprehension (_term, _query) -> + failwith "ArrayComprehension encountered, should have been lifted" + | SetComprehension (_term, _query) -> + failwith "ArrayComprehension encountered, should have been lifted" + | ObjectComprehension ((_key, _value), _query) -> + failwith "ArrayComprehension encountered, should have been lifted" + | Call (fn, args) -> + let fn' = compile_term env (Ref fn) in + let args' = List.map ~f:(compile_term env) args in + Application (fn', args') + +let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) option) : (('a * term) list * rule) = + let empty = ([], []) in + let combine = fun (side_info, q) (side_info', term) -> + (side_info @ side_info', q @ [term]) in + let rec handle_term : term -> (('a * term) list * term) = function + | term when f env term |> Option.is_some -> + let (side_info, term') = f env term |> Option.value_exn in + ([(side_info, term)], term') + | Ref (target, args) -> + let target = term_of_ref_target target in + let terms = [target] @ args in + + let (side_info, terms') = + List.map terms ~f:handle_term + |> List.fold ~f:combine ~init:empty + in (side_info, Ref (ref_target_of_term (List.hd_exn terms'), List.tl_exn terms')) + | Array xs -> + let (side_info, terms) = + List.map xs ~f:handle_term + |> List.fold ~f:combine ~init:empty + in (side_info, Array terms) + | Set xs -> + let (side_info, terms) = + List.map xs ~f:handle_term + |> List.fold ~f:combine ~init:empty + in (side_info, Set terms) + | Object kvs -> + let (side_info, terms) = + List.map ~f:snd kvs + |> List.map ~f:handle_term + |> List.fold ~f:combine ~init:empty + in + (side_info, + Object + (List.zip_exn + (List.map ~f:fst kvs) + terms)) + | Call (x, xs) -> + let (side_info, terms) = + List.map ((Ref x : term)::xs) ~f:handle_term + |> List.fold ~f:combine ~init:empty + in + (match List.hd_exn terms with + | Ref reference -> + (side_info, Call (reference, List.tl_exn terms)) + | term -> failwith (show_term term |> Printf.sprintf "invalid call target %s")) + | term -> ([], term) + and handle_expr = function + | Term t -> + let (side_info, t') = handle_term t in (side_info, Term t') + | Every (k, v, t, q) -> + let (side_info, q') = + List.map q ~f:handle_literal + |> List.fold ~f:(fun (side_info, q) (side_info', term) -> + (side_info @ side_info', q @ [term])) + ~init:empty + in (side_info, Every (k, v, t, q')) + and handle_literal : literal -> (('a * term) list * literal) = function + | Exists (exprs, with_statement) -> + let (side_info, exprs') = + List.map exprs ~f:handle_expr + |> List.fold ~init:empty ~f:combine + in (side_info, Exists (exprs', with_statement)) + | Expr (expr, with_statement) -> + let (side_info, expr') = handle_expr expr in + (side_info, Expr (expr', with_statement)) + | Negate (expr, with_statement) -> + let (side_info, expr') = handle_expr expr in + (side_info, Negate (expr', with_statement)) + in + let { body = q; head; _ } = rule in + + let (side_info, query) = List.map ~f:handle_literal q |> List.fold ~init:empty ~f:combine in + let (side_info', head') = match head with + | (rf, Assignment (op, term)) -> + let (side_info, term') = handle_term term in + (side_info, (rf, Assignment (op, term'))) + | (rf, Function (op, args, term)) -> + let (side_info, term') = handle_term term in + (side_info, (rf, Function (op, args, term'))) + | (rf, Set term) -> + let (side_info, term') = handle_term term in + (side_info, (rf, Set term')) + in + (side_info @ side_info', { rule with body = query; head = head' }) + + +let rewrite_with (env : environ) (q : query) : ((string * string) list * lean_expression list) = + let empty = ([], []) in + let combine (x1, y1) (x2, y2) = (x1 @ x2, y1 @ y2) in + let rec handle_term substitutions : term -> ((string * string) list * lean_expression list) = function + | Var name as v -> + (match List.Assoc.find ~equal:equal_term substitutions v with + | Some value -> + let new_identifier = gensym name in + ([(name, new_identifier)], + [Application (Identifier "Eq", [Identifier new_identifier; + compile_term env value])]) + | None -> empty) + | Ref (target, args) -> + let target = term_of_ref_target target in + let terms = [target] @ args in + List.map terms ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine + | Array xs | Set xs -> + List.map xs ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine + | Object kvs -> List.map ~f:snd kvs + |> List.map ~f:(handle_term substitutions) + |> List.fold ~init:empty ~f:combine + | Call (x, xs) -> + List.map ((Ref x : term)::xs) ~f:(handle_term substitutions) |> List.fold ~init:empty ~f:combine + | ArrayComprehension _ -> assert false (* TODO *) + | ObjectComprehension _ -> assert false (* TODO *) + | SetComprehension _ -> assert false (* TODO *) + | _ -> empty + and handle_expr substitutions = function + | Term t -> handle_term substitutions t + | Every (_, _, _, q) -> + List.map q ~f:handle_literal |> List.fold ~init:empty ~f:combine + and handle_literal : literal -> ((string * string) list * lean_expression list) = function + | Exists (exprs, Some with_statement) -> + List.map exprs ~f:(handle_expr with_statement) + |> List.fold ~init:empty ~f:combine + | Expr (expr, Some with_statement) -> + handle_expr with_statement expr + | Negate (expr, Some with_statement) -> + handle_expr with_statement expr + | _ -> + empty + in + List.map ~f:handle_literal q |> List.fold ~init:empty ~f:combine + +let rec compile_expr env : expr -> (environ * lean_expression) = function + | Term t -> + (match t with + (* Call is a special case, being the only kind of "term" that affects scope. *) + | Call ((Var "assign", []), [ Var name; rhs ]) -> + (* Assumption: `name' is in the `env' because of our up-front variable analysis, but we've marked it as unassigned. *) + let { lean_id; kind; assigned } = Map.find_exn env name in + assert ((not assigned) || not (equal_definition_kind kind Complete)) ; + + let variable = { assigned = true; lean_id; kind } in + let env' = Map.set env ~key:name ~data:variable in + ( + env', + compile_term env' (Call ((Var "eq", []), [ Var name; rhs ])) + ) + | t -> (env, compile_term env t)) + | Every (Some key, value, domain, query) -> + let domain' = compile_term env domain in + (* Extend the environment with the key and value. *) + let env' = Map.set env ~key:key ~data:{ lean_id = gensym key; kind = Complete; assigned = true } + |> Map.set ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in + let (env'', query') = compile_query env' query in + (env'', + ForAll + (([key; value], "Rego.Any"), + fold_and + [(Application + ((Identifier "Membership.mem"), + [Tuple [Identifier key; Identifier value]; domain'])); + query'] + |> simplify_expression)) + | Every (None, value, domain, query) -> + let domain' = compile_term env domain in + (* Extend the environment with the value. *) + let env' = Map.set env ~key:value ~data:{ lean_id = gensym value; kind = Complete; assigned = true } in + let (env'', query') = compile_query env' query in + (env'', + ForAll + (([value], "Rego.Any"), + fold_and + [(Application + ((Identifier "Membership.mem"), + [Identifier value; domain'])); + query'] + |> simplify_expression)) + +and compile_literal env : literal -> (environ * lean_expression) = function + | Exists (exprs, _) -> + let (env', form) = compile_query env (List.map ~f:literal_of_expr exprs) in + (env', form) + | Expr (expr, _) -> + let (env', inner) = compile_expr env expr in + (env', Application (Identifier "Ne", [inner; Application (Identifier "Rego.Any.bool", [Bool false])])) + | Negate (expr, _) -> + let (env', form) = compile_literal env (Expr (expr, None)) in + (env', Application (Identifier "Not", [form])) + +and compile_query env literals : (environ * lean_expression) = + let (env', forms) = map_with_environment_updates env literals compile_literal in + let form = match forms with + | [x] -> x + | xs -> xs |> fold_and |> simplify_expression in + (env', form) + +and compile_comprehension env anonymous_name (comp : term) = + match comp with + | ArrayComprehension (value, q) -> + let { free; _ } = extract_variables env [literal_of_term value] in + let env = List.map free ~f:(fun identifier -> + (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) + |> extend_environment env in + let (_, form) = compile_query env q in + Application (Identifier "array_specified_by", [Identifier anonymous_name; form]) + | SetComprehension (value, q) -> + let { free; _ } = extract_variables env [literal_of_term value] in + let env = List.map free ~f:(fun identifier -> + (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) + |> extend_environment env in + let (_, form) = compile_query env q in + Application (Identifier "set_specified_by", [Identifier anonymous_name; form]) + | ObjectComprehension ((key, value), q) -> + let { free; _ } = extract_variables env [literal_of_term (term_of_object_key key)] in + let { free = free'; _ } = extract_variables env [literal_of_term value] in + let free = free @ free' in + let env = List.map free ~f:(fun identifier -> + (identifier, { lean_id = (gensym identifier); kind = Parameter; assigned = true })) + |> extend_environment env in + let (_, form) = compile_query env q in + Application (Identifier "object_specified_by", [Identifier anonymous_name; form]) + | _ -> failwith (show_term comp |> + (Printf.sprintf "called compile_comprehension on non-comprehension %s")) + +and compile_rule env subjects rule : (environ * lean_expression) list = + let (comprehensions, rule) = lift_term env rule + (fun _env term -> + let anonymous_name = gensym "comprehension" in + match term with + | ArrayComprehension _ | SetComprehension _ | ObjectComprehension _ -> + Some (anonymous_name, Var anonymous_name) + | _ -> None) in + (* Each comprehension is now mapped to an anonymous name. We'll add it to the + scope so we don't have an unbound variable error when we compile the + modified rule. *) + let env = List.map comprehensions + ~f:(fun (anonymous_name, _) -> + (anonymous_name, { lean_id = anonymous_name; kind = Parameter; assigned = true })) + |> extend_environment env in + + let { body = literals; _ } = rule in + + (* TODO: Deal with user-defined functions. *) + (* let (_, literals) = lift_term env literals *) + (* (fun env term -> *) + (* match term with *) + (* | Call ((Var identifier, []), _args) -> *) + (* (match Map.find env identifier with *) + (* | Some { kind = FunctionRule ; _ } -> *) + (* let anon_name = gensym "function_call" in *) + (* Some (anon_name, Var anon_name) *) + (* | _ -> None) *) + (* | _ -> None) in *) + + + let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in + let env = List.map new_identifiers + ~f:(fun (old_name, anonymous_name) -> + (old_name, { lean_id = anonymous_name; kind = Parameter; assigned = true })) + |> extend_environment env in + + let { free; bound; used } = extract_variables env literals in + let (used', parameters, env_updates, subject_constraints) = + let explicit_parameters = match rule |> kind_and_args_of_rule with + | `FunctionRule (args, _) -> + List.filter_map args ~f:(function + | Var id -> Some id + | _ -> None) + | _ -> [] + in + let candidates = match rule |> kind_and_args_of_rule with + | `ScalarRule term | `SetRule term -> + [term] + | `ObjectRule (key, value) -> + [key; value] + | `FunctionRule (args, output) -> + args @ [output] + in + + let env_updates_and_constraints = + List.map2_exn + subjects + candidates + ~f:(fun subject -> + function + (* In this case, we're dealing with a formal parameter, so we want + to have it be an alias of the lean_id for the subject. *) + | Var identifier when List.mem (bound @ explicit_parameters) identifier ~equal:String.equal -> + (Some identifier, + [(identifier, { lean_id = subject; kind = Parameter; assigned = true })], + None) + | term -> + let { free; _ } = extract_variables env [literal_of_term term] in + (None, + [(subject, { lean_id = subject; kind = Parameter; assigned = true })] + @ List.map free + ~f:(fun name -> + (name, { lean_id = gensym "param"; kind = Parameter; assigned = true })), + Some (Call ((Var "eq", []), [Var subject; term]) : term))) + in + + let parameters = env_updates_and_constraints |> List.filter_map ~f:(fun (x, _, _) -> x) in + let non_parameters = List.filter_map candidates ~f:(function + | Var id -> Some id + | _ -> None) in + + (non_parameters, + parameters, + env_updates_and_constraints |> List.map ~f:(fun (_, x, _) -> x) |> List.concat, + env_updates_and_constraints |> List.filter_map ~f:(fun (_, _, x) -> x)) + in + let env' = extend_environment env env_updates in + let bound = List.filter bound ~f:(fun identifier -> not (List.mem parameters identifier ~equal:String.equal)) in + + let free = free |> + List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in + + let used = used @ used' in + let used = used |> + List.filter ~f:(fun name -> not (List.mem parameters name ~equal:String.equal)) in + let used = used + |> List.filter ~f:(fun name -> match Map.find_exn env' name with + | { kind = Complete; _ } -> false + | _ -> true) in + + let env' = + List.concat + [List.map free ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); + List.map used ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = true })); + List.map bound ~f:(fun name -> (name, { lean_id = gensym name; kind = Complete; assigned = false }))] + |> extend_environment env' in + + let lean_id_of_identifier k = (let { lean_id; _ } = Map.find_exn env' k in lean_id) in + let constraints = + List.filter_map used ~f:(fun name -> + match Map.find env name with + | Some { lean_id; kind = ScalarRule; _ } -> + Some + (Application (Identifier "scalar_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)])) + | Some { lean_id; kind = SetRule; _ } -> + Some + (Application (Identifier "set_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)])) + | Some { lean_id; kind = ObjectRule; _ } -> + Some + (Application (Identifier "object_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)])) + | Some { lean_id; kind = FunctionRule; _ } -> + Some + (Application (Identifier "function_specified_by", + [Identifier lean_id; + Identifier (lean_id_of_identifier name)])) + | Some _ -> None + | None -> failwith (Printf.sprintf "unbound variable %s" name)) in + + let subject_constraints = List.map subject_constraints ~f:literal_of_term in + let (env'', form) = compile_query env' (literals @ subject_constraints) in + let comprehension_constraints = + List.map comprehensions ~f:(fun (name, form) -> compile_comprehension env name form) in + let quantified_names = free @ bound @ used in + + (env'', + if List.is_empty quantified_names then + fold_and [form] |> simplify_expression + else + Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), + constraints @ comprehension_constraints @ [form] + |> fold_and + |> simplify_expression)) + :: (match rule.otherwise with + | Some branch -> compile_rule env subjects branch + | None -> []) + +let compile_definition env (rules : rule list) = + assert (not (List.is_empty rules)); + + (* Assert that all rules are of the same kind. *) + assert (1 = (List.map rules ~f:definition_kind_of_rule + |> uniq equal_definition_kind + |> List.length)); + + (* Rules are grouped based on their head, so we can determine which variable + we're defining by looking at any arbitrarily-chosen rule. It's easy enough + to get the first. *) + let variable_being_defined = + match List.hd_exn rules with + | { head = (rf, _); _ } -> rf + in + + let (default_rules, conditional_rules) = + List.partition_tf rules ~f:(function + | { default = true; _ } -> true + | _ -> false) + in + (* There can be only one default rule. *) + assert (List.length default_rules <= 1); + + let subjects = + match List.hd_exn rules |> kind_and_args_of_rule with + | `ScalarRule _ | `SetRule _ -> + [gensym "x"] + | `ObjectRule _ -> + [gensym "k"; gensym "v"] + | `FunctionRule (args, _) -> + List.map args ~f:(fun _ -> gensym "arg") + @ [gensym "y"] + in + let conditional_rules = + List.map ~f:(compile_rule env subjects) conditional_rules + |> List.concat in + let conditional_arms = + List.mapi conditional_rules ~f:(fun i (_env', body) -> + (body, + (Printf.sprintf "rule%d" i, + [body], + List.map subjects ~f:(fun x -> Identifier x)))) in + let default_arms = + List.map default_rules ~f:(fun _ -> + let other_rule_bodies = List.map ~f:fst conditional_arms in + let body_form = + Application (Identifier "Not", [fold_or other_rule_bodies]) + in + ("rule_default", + [body_form], + List.map subjects ~f:(fun x -> Identifier x))) in + + let form = + let string_of_reference : reference -> string = function + | (Var name, []) -> name + | (Var name, [_]) -> name + | _ -> assert false (* unreachable *) + in + Inductive + (string_of_reference variable_being_defined, + [(subjects, "Rego.Any")], + List.append (List.map ~f:snd conditional_arms) default_arms) + in (env, form) + +let compile_policy env (rules : rule list) = + let group accessor l = + let rec grouping acc = function + | [] -> acc + | hd::tl -> + let l1,l2 = List.partition_tf ~f:(fun x -> equal_reference (accessor x) (accessor hd)) tl in + grouping ((hd::l1)::acc) l2 + in + grouping [] l in + let head_of_rule = function | {head = (rf, _); _ } -> rf in + let by_reference = group head_of_rule rules in + let env' = + List.map by_reference ~f:(function + | { head = ((Var name, []), Assignment _); _ } :: _ -> + (name, { lean_id = name ; kind = ScalarRule; assigned = true }) + | { head = ((Var name, [_]), Assignment _); _ } :: _ -> + (name, { lean_id = name ; kind = ObjectRule; assigned = true }) + | { head = ((Var name, []), Set _); _ } :: _ -> + (name, { lean_id = name ; kind = SetRule; assigned = true }) + | { head = ((Var name, []), Function _); _ } :: _ -> + (name, { lean_id = name ; kind = FunctionRule; assigned = true }) + | _ -> failwith "policy rule head is not a variable") + |> extend_environment env in + map_with_environment_updates env' by_reference compile_definition + +let compile_error_condition env = + Map.to_alist env + |> List.filter_map ~f:(fun (k, v) -> + match v with + | { kind = ScalarRule; _ } -> + let anon_name = gensym "the" in + Some( + ExistsUnique ( + ([anon_name], "Rego.Any"), + Application (Identifier "scalar_specified_by", + [Identifier anon_name; Identifier k]))) + | { kind = FunctionRule; _ } -> + let args_name = gensym "args" in + let value_name = gensym "value" in + Some( + ForAll + (([args_name], "Rego.Any"), + ExistsUnique ( + ([value_name], "Rego.Any"), + Application + (Identifier "eq", + [Application (Identifier k, [Identifier args_name]); + Identifier value_name])))) + | _ -> None) + |> fold_and + +let compile_package = + let string_of_reference : reference -> string = function + | (Var name, xs) -> + [name] + @ List.map xs ~f:(function + | Scalar (String x) -> x + | _ -> failwith "unreachable") + |> String.concat ~sep:"." + + | _ -> assert false (* unreachable *) + in + let compile_import = function + | { alias = None; path } -> + Printf.sprintf "imports %s" + (string_of_reference path) + |> String.escaped + | { alias = Some alias; path } -> + Printf.sprintf "imports %s as %s" + (string_of_reference path) + alias + |> String.escaped + in + function + | { path; imports; policy } -> + let policy = List.map ~f:transform_rule_with_ref_head policy |> List.concat in + let (env', forms) = compile_policy toplevel policy in + let error_form = Define ("rego_error", compile_error_condition env') in + [Comment (Printf.sprintf "package %s" + (string_of_reference path) + |> String.escaped)] + @ List.map imports ~f:(fun x -> Comment (compile_import x)) + @ forms + @ [error_form] diff --git a/rego-proofs/compiler/lib/compiler.mli b/rego-proofs/compiler/lib/compiler.mli new file mode 100644 index 0000000..0bef961 --- /dev/null +++ b/rego-proofs/compiler/lib/compiler.mli @@ -0,0 +1,13 @@ +open Ast +open Lean + +type environ + +type analysis_result = + { bound : string list; + free : string list; + used : string list } + +val extract_variables_wrapper : query -> analysis_result +val transform_rule_with_ref_head : rule -> rule list +val compile_package : package -> lean_expression list diff --git a/rego-proofs/compiler/lib/dune b/rego-proofs/compiler/lib/dune new file mode 100644 index 0000000..139237e --- /dev/null +++ b/rego-proofs/compiler/lib/dune @@ -0,0 +1,9 @@ +(library + (name compiler) + (libraries core unix yojson) + (preprocess + (pps ppx_deriving.eq ppx_deriving.show ppx_fields_conv))) + +(env + (dev + (flags (:standard -w -66 -w -37 -w -30 -w -32)))) diff --git a/rego-proofs/compiler/lib/lean.ml b/rego-proofs/compiler/lib/lean.ml new file mode 100644 index 0000000..6bb4265 --- /dev/null +++ b/rego-proofs/compiler/lib/lean.ml @@ -0,0 +1,63 @@ +open Core + +type lean_expression = + | Comment of string + | Identifier of string + | Bool of bool + | String of string + | Number of float + | List of lean_expression list + | Tuple of lean_expression list + | Application of lean_expression * lean_expression list + | Define of string * lean_expression + | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list + | ForAll of judgement * lean_expression + | Exists of judgement * lean_expression + | ExistsUnique of judgement * lean_expression +[@@deriving eq, show] + +and judgement = string list * string [@@deriving eq, show] + +let fmt_judgement : judgement -> string = function + | vars, t -> Printf.sprintf "(%s : %s)" (String.concat ~sep:" " vars) t + +let rec fmt_lean_expression : lean_expression -> string = function + | Comment s -> Printf.sprintf "\n-- %s\n" s + | Identifier s -> s + | Bool b -> if b then "True" else "False" + | String s -> Printf.sprintf "\"%s\"" s + | Number n -> Float.to_string n + | List xs -> + Printf.sprintf "[%s]" + (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs)) + | Tuple xs -> + Printf.sprintf "(%s)" + (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs)) + | Application (head, args) -> + Printf.sprintf "(%s %s)" (fmt_lean_expression head) + (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args)) + | Define (ident, expr) -> + Printf.sprintf "def %s := (%s)" ident (fmt_lean_expression expr) + | ForAll (j, expr) -> + Printf.sprintf "∀ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) + | Exists (j, expr) -> + Printf.sprintf "∃ %s, %s" (fmt_judgement j) (fmt_lean_expression expr) + | ExistsUnique (j, expr) -> + Printf.sprintf "∃! %s, %s" (fmt_judgement j) (fmt_lean_expression expr) + | Inductive (name, judgements, arms) -> + let fmt_arm (arm_name, exprs, values) = + let head = + Printf.sprintf + "%s %s" + name + (List.map ~f:fmt_lean_expression values |> String.concat ~sep:" ") + in + let body = + List.map ~f:fmt_lean_expression exprs + |> String.concat ~sep:" → " + in + Printf.sprintf " | %s : %s → %s" arm_name body head + in + Printf.sprintf "inductive %s %s where\n%s" name + (List.map ~f:fmt_judgement judgements |> String.concat ~sep:" ") + (List.map ~f:fmt_arm arms |> String.concat ~sep:"\n") diff --git a/rego-proofs/compiler/lib/lean.mli b/rego-proofs/compiler/lib/lean.mli new file mode 100644 index 0000000..f6a769a --- /dev/null +++ b/rego-proofs/compiler/lib/lean.mli @@ -0,0 +1,25 @@ +type lean_expression = + | Comment of string + | Identifier of string + | Bool of bool + | String of string + | Number of float + | List of lean_expression list + | Tuple of lean_expression list + | Application of lean_expression * lean_expression list + | Define of string * lean_expression + | Inductive of string * judgement list * (string * lean_expression list * lean_expression list) list + | ForAll of judgement * lean_expression + | Exists of judgement * lean_expression + | ExistsUnique of judgement * lean_expression + +and judgement = string list * string + +val equal_lean_expression : lean_expression -> lean_expression -> bool +val equal_judgement : judgement -> judgement -> bool +val pp_lean_expression : Format.formatter -> lean_expression -> unit +val show_lean_expression : lean_expression -> string +val pp_judgement : Format.formatter -> judgement -> unit +val show_judgement : judgement -> string + +val fmt_lean_expression : lean_expression -> string 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 -;;; -;;; 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 -;;; . - -(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 -;;; -;;; 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 -;;; . - -(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 - (($ value) - (if (boolean? value) - (make - #:kind 'eq - #:left form - #:right (make #:value #t)) - form)) - (($ value) - (make - #:kind 'eq - #:left form - #:right (make #:value #t))) - (_ form))) - (policy-map - policy - (lambda (_scope _breadcrumb form) - (match form - (($ conjunction) - (make - #:clauses (map rewrite-top-level conjunction))) - (($ _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 -;;; -;;; 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 -;;; . - -(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 - ((($ (($ "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 - #:identifiers - (map (match-lambda - ((($ (($ "assign"))) left right) - ;; We're defining a new local, so let's add it to the scope. - (let ((local (make - #:identifier left - #:lean-name left - #:constraints - (match right - (($ (right-identifier)) - `((== ,(canonicalize left breadcrumb) - ,(canonicalize right (originating-breadcrumb scope breadcrumb right-identifier))))) - (($ _) - `((== ,(canonicalize left breadcrumb) - ,(canonicalize right (originating-breadcrumb scope breadcrumb right))))) - (($ value) - `((== ,(canonicalize left breadcrumb) - ,(scheme-value->type value)))) - (_ '()))))) - (add-to-scope scope breadcrumb local)) - - `(,left ,right))) - assignments) - #:body - (make #: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 - (($ (($ identifier))) - (not (scope-contains? scope breadcrumb identifier))) - (($ identifier) - (not (scope-contains? scope breadcrumb left))) - (_ #f))) - -(define (compile-constraints policy) - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - ((($ (($ name))) left right) - (if (and (string= name "assign") (is-assignment? scope breadcrumb left)) - form - (make - #: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 -;;; -;;; 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 -;;; . - -(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 #:name "rulesubject")) - (define (collapse-rule rule) - (match rule - (($ default head ($ clauses) else-arm) - (make - #:clauses `(,@clauses - ,(make - #:left subject-ref - #:right (right head) - #:kind 'eq)))))) - (match rule-group - ((left rules ...) - (list - (make - #: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 `' -(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 -;;; -;;; 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 -;;; . - -(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 )) - -(define (exists-some->variables identifiers) - (map (lambda (x) - (match x - (($ _) x) - (($ - ($ - (($ "internal") - ($ "member_2"))) - args) - (first args)))) - identifiers)) - -(define (exists-some->constraints identifiers) - (fold append '() - (map (lambda (x) - (match x - (($ _) '()) - (($ - ($ - (($ "internal") - ($ "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 - #:identifier variable - #:lean-name variable))) - ;; (format #t "Here: ~a~%" (to-pretty-sexp local)) - (add-to-scope scope breadcrumb local))) - variables) - - (make - #:variables variables - #:body - (make - #: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 -;;; -;;; 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 -;;; . - -(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 - (($ domain key value body) - (assert (is-a? value )) - - (let ((local (variable-ref->local value))) - (add-to-scope scope breadcrumb local)) - - (make - #:variables `(,value) - #:body (make - #:clauses - `(,(cond ;; TODO: Type inference. - (else (make - #: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 -;;; -;;; 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 -;;; . - -(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 - (($ function-name args) - (assert (or (scope-contains? scope breadcrumb function-name) - (lean-builtin-function? (reference->lean-name function-name)))) - (make - #: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 -;;; -;;; 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 -;;; . - -(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 - (($ 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 #:name new-ident))) - (set! new-identifiers `(,new-ref ,@new-identifiers)) - ;; FIXME: This is syntactically a funcall but semantically something else. - (set! new-clauses `(,(make - #:name (lean-name local) - #:args `(,new-ref)) - ,@new-clauses)) - (make #: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 - (($ 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 - #:clauses - `(,(make - #: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 -;;; -;;; 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 -;;; . - -(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 - (($ - ($ pairs)) - (make - #:name "List.toAssocList'" - #:args (list (map (lambda (x) (make #: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 -;;; -;;; 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 -;;; . - -(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 - #:name "Rego.expectArray" - #:args `(,input-identifier))) - (,deref-id ,(make - #: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 - #:name "Rego.expectSet" - #:args `(,input-identifier))) - (,deref-id ,(make - #: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 - #:name "Rego.expectObject" - #:args `(,input-identifier))) - (,deref-id ,(make - #: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 - (($ (singleton)) - singleton) - (($ (first rest ...)) - (make #: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 -;;; -;;; 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 -;;; . - -(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 )) -;; (match rule -;; (($ default head ($ conjunction)) -;; (make -;; #:conclusion (right head) -;; #:body (if (> (length conjunction) 1) -;; (make #:clauses (map compile-expr conjunction)) -;; (first conjunction)))))) - -(define (compile-definition definition) - (match definition - (($ kind left _right default rules) - (assert (is-a? left )) - (make - ;; 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 )) - (match 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 -;;; -;;; 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 -;;; . - -(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 #: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) - ((($ (($ identifier-left))) - ($ (($ identifier)))) - (add-to-scope new-scope breadcrumb (variable-ref->local (first (inner rhs)))) - (let ((local (make - #: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? - ((($ (($ identifier-left))) - ($ identifier)) - (add-to-scope new-scope breadcrumb (variable-ref->local rhs)) - (let ((local (make - #:identifier (first (inner lhs)) - #:lean-name (first (inner lhs)) - #:constraints - `((== ,(canonicalize identifier-left breadcrumb) - ,(canonicalize identifier breadcrumb)))))) - (add-to-scope new-scope breadcrumb local))) - ((($ (($ identifier))) - ($ value)) - (let ((local (make - #: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 -;;; -;;; 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 -;;; . - -(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 - (($ ($ 'object key value body)) - (let* ((name (fresh-identifier top-level-names "objectcomp")) - (definition (make - #:kind 'field-eqv - #:left key - #:right value - #:default #f - #:rules (if (not (list? body)) - `(,body) - body))) - (local (make - #:identifier (make #:name name) - #:constraints `((== ,(canonicalize name breadcrumb) object)) - #:lean-name (make #:name (format #f "~a_eqv" name))))) - (values local definition))))) - - (let ((policy - (policy-map - policy - (lambda (scope breadcrumb form) - (match form - (($ ($ '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 #:parts `(,(inner identifier))))) - (_ form)))))) - (match 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 -;;; -;;; 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 -;;; . - -(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 ? - (define new-identifiers (list)) - (define (recur scope breadcrumb form) - (match form - (($ name) - (if (string-prefix? "$" name) - (let* ((new-ident (fresh-identifier (all-valid-identifiers scope breadcrumb))) - (new-ref (make #: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 - (($ 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 - #:clauses - `(,(make - #: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 -;;; -;;; 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 -;;; . - -(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 `'" - (assert (list? ast)) - (make - #:package (extract-package ast) - #:imports (extract-imports ast) - #:rules (extract-rules ast) - #:scope (make - #: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 record" - (define (recur rule) - (make - #:default (assoc-ref rule "default") - #:head (preprocess-head (assoc-ref rule "head")) - #:body (make - #: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 - (($ _default head _body _else) - (left head))) - rules)) - (define result - (map (lambda (target) - (cons target - (filter (match-lambda - (($ _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 - #: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 - #: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 `' - ((is-a? body-obj ) (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 #:name (first parts) #:args (drop parts 1)))) - (_ (parse-constant term-obj)))) - -(define (pairs->object-literal pairs) - (make - #: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 - #:value - (cond ((or (boolean? value) - (number? value) - (string? value)) value) - ((string= "array" type) (if (null? value) - #() - (list->vector value))) - ((string= "set" type) (make - #:elems value)) - ((string= "object" type) (pairs->object-literal value)) - ((string= "arraycomprehension" type) - (make - #:kind 'array - #:key (assoc-ref value "term") - #:value #f - #:body (extract-conjunction (preprocess-body (assoc-ref value "body"))))) - ((string= "setcomprehension" type) - (make - #:kind 'set - #:key (assoc-ref value "term") - #:value #f - #:body (extract-conjunction (preprocess-body (assoc-ref value "body"))))) - ((string= "objectcomprehension" type) - (make - #: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 #:name (assoc-ref term-obj "value"))) - -(define (parse-reference ref-obj) - (assert (list? ref-obj)) - (make #:parts ref-obj)) - - - - - -(define* (extract-rule default head body #:optional else-arm) - "Extract an individual parsed rule" - (if else-arm - (make - #:default default - #:head head - #:body (make #:conjunction (extract-conjunction (inner body))) - #:else-arm (apply extract-rule else-arm)) - (make - #:default default - #:head head - #:body (make #: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 - #: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 #: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 -;;; -;;; 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 -;;; . - -(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 -;;; -;;; 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 -;;; . - -(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 `'" - (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 - (($ _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 } -;; -;; ↔ -;; -;; #< 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 - (($ 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 } -;; -;; ↔ -;; -;; #< 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) - (($ default head body) - (test-assert (boolean? default)) - (test-assert (is-a? head )) - (test-assert (is-a? body ))))) - -(let ((parse-result (template-and-parse "phi := 3.14159 if False else := 1.61803"))) - (match (select-rule parse-result) - (($ default head body else-arm) - (test-assert (boolean? default)) - (test-assert (is-a? head )) - (test-assert (is-a? body )) - (test-assert (is-a? else-arm ))))) - -;; 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 "]" -;; -;; ↔ -;; -;; #< 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) - (($ - _default - ($ 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) - (($ - _default - ($ 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) - (($ - _default - ($ 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 -;; -;; ↔ -;; -;; #< conjunction: ...> -;; where -;; (list? conjunction) -;; -;; query = literal { ( ";" | ( [CR] LF ) ) literal } -;; -;; ↔ -;; -;; (list ...) - -(let ((parse-result (template-and-parse "pi := 3.14159"))) - (match (select-rule parse-result) - (($ - _default - _head - ($ conjunction)) - (test-assert (list? conjunction))))) - -;; # Literals -;; -;; literal = ( some-decl | expr | "not" expr ) { with-modifier } - -;; with-modifier = "with" term "as" term -;; -;; ↔ -;; -;; #< with: ... as: ...> - -;; TODO: When implemented, write a parse test for `with-modifier'. - -;; some-decl = "some" term { "," term } { "in" expr } -;; -;; ↔ -;; -;; #< terms: ...> - -(let ((parse-result (template-and-parse "q1 contains name if { some site; name := site.name }"))) - (match (select-rule parse-result) - (($ - _default - _head - ($ (($ (($ "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 "}" -;; -;; ↔ -;; -;; #< 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) - (($ - _default - _head - ($ - (($ - ($ "sites") - 'null - ($ "site") - body) - terms ...))) - (test-assert (list? body)) - (test-assert (list? terms))))) - -;; membership = term [ "," term ] "in" term -;; -;; ↔ -;; -;; (#< parts: (#< name: "internal">, #< 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) - (($ - _default - _head - ($ - (($ - (($ - ($ (($ "internal") - ($ "member_2"))) - (($ "site") - ($ "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 "]" -;; -;; ↔ -;; -;; #< 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) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - 'array - ($ "x") - #f - body))) - _body) - (test-assert (list? body))))) - -;; set-compr = "{" term "|" query "}" -;; -;; ↔ -;; -;; #< 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) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - 'set - ($ "x") - #f - body))) - _body) - (test-assert (list? body))))) - -;; object-compr = "{" object-item "|" query "}" -;; -;; ↔ -;; -;; #< 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) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - 'object - ($ "name") - ($ "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 -;; -;; ↔ -;; -;; #< parts: ...> -;; where -;; (list? parts) -;; -;; var = ( ALPHA | "_" ) { ALPHA | DIGIT | "_" } -;; -;; ↔ -;; -;; #< name: ...> -;; where -;; (string? name) - -(let ((parse-result (template-and-parse "newlist := site.names"))) - (match (select-rule parse-result) - (($ - _default - ($ _name _kind _lhs - ($ - (($ "site") - ($ "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) - (($ - _default - ($ _name _kind _lhs - ($ - #(($ 1) - ($ 2) - ($ 3) - ($ 4) - ($ 5)))) - _body) - (test-assert #t)))) - -;; object = "{" object-item { "," object-item } "}" -;; object-item = ( scalar | ref | var ) ":" term -;; -;; ↔ -;; -;; #< value: #< pairs: ...>> - -(let ((parse-result (template-and-parse "naturals := { \"first\": 1, \"second\": 2 }"))) - (match (select-rule parse-result) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - ((($ "first") ($ 1)) - (($ "second") ($ 2)))))) - _body) - (test-assert #t)))) - -(let ((parse-result (template-and-parse "naturals := { first: 1, second: 2 }"))) - (match (select-rule parse-result) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - ((($ "first") ($ 1)) - (($ "second") ($ 2)))))) - _body) - (test-assert #t)))) - -;; set = empty-set | non-empty-set -;; non-empty-set = "{" term { "," term } "}" -;; empty-set = "set(" ")" -;; -;; ↔ -;; -;; #< elts: ...> -;; #< elts: '()> - -(let ((parse-result (template-and-parse "naturals := { 1, 2, 3 }"))) - (match (select-rule parse-result) - (($ - _default - ($ _name _kind _lhs - ($ - ($ - (($ 1) ($ 2) ($ 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/test/compiler.ml b/rego-proofs/compiler/test/compiler.ml new file mode 100644 index 0000000..741ae3a --- /dev/null +++ b/rego-proofs/compiler/test/compiler.ml @@ -0,0 +1,134 @@ +open Core +open Compiler +open Compiler__ + +module To_test = struct + let extract_variables = Compiler.extract_variables_wrapper + let transform_ref_head = Compiler.transform_rule_with_ref_head + let fmt = Lean.fmt_lean_expression +end + +let strings = + Alcotest.testable + (Format.pp_print_list Format.pp_print_string) + (List.equal String.equal) + +let extract_query policy = + match Ast.ast_of_string policy with + | { policy = [ { body; _ } ]; _ } -> body + | _ -> failwith "failed to parse" + +let test_local_extraction_simple_1 () = + let policy_code = {| +package test + +q { + x := 2 +} + |} in + let { bound; _ } = To_test.extract_variables (extract_query policy_code) in + Alcotest.(check strings) + "expected identifier list" [ "x" ] bound + +let test_local_extraction_simple_2 () = + let policy_code = {| +package test + +q { + x := 2 + y := 3 + z := 4 +} + |} in + let { bound; _ } = To_test.extract_variables (extract_query policy_code) in + Alcotest.(check strings) + "expected identifier list" [ "x"; "y"; "z" ] bound + +let test_local_dependent_on_previously_defined_local () = + let policy_code = {| +package test + +q { + x := 2 + y := x +} + |} in + let { bound; _ } = To_test.extract_variables (extract_query policy_code) in + Alcotest.(check strings) + "expected identifier list" [ "x"; "y" ] bound + +let test_free_extraction_simple_1 () = + let policy_code = {| +package test + +q { + y := 7 + y == 8 +} + |} in + let { free; bound; _ } = To_test.extract_variables (extract_query policy_code) in + Alcotest.(check strings) + "expected identifier list" [] free; + Alcotest.(check strings) + "expected identifier list" [ "y" ] bound + +let test_free_extraction_simple_2 () = + let policy_code = {| +package test + +q { + y := z + z = 7 +} + |} in + let { free; bound; _ } = To_test.extract_variables (extract_query policy_code) in + Alcotest.(check strings) + "expected identifier list" [ "z" ] free; + Alcotest.(check strings) + "expected identifier list" [ "y" ] bound + +let test_identifier () = + 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 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)]; + otherwise = None } in + Alcotest.(check int) "expected rules" + 2 + (To_test.transform_ref_head rule |> List.length) + +let () = + let open Alcotest in + run "Compiler" + [ + ( "free variable extraction", + [ + test_case "free variable extraction simple (1)" `Quick + test_free_extraction_simple_1; + test_case "free variable extraction simple (2)" `Quick + test_free_extraction_simple_2; + ] ); + ( "local extraction", + [ + test_case "local extraction simple (1)" `Quick + test_local_extraction_simple_1; + test_case "local extraction simple (2)" `Quick + test_local_extraction_simple_2; + test_case + "local extraction with local dependent on previously-defined local \ + (1)" + `Quick test_local_dependent_on_previously_defined_local + ] ); + ( "nested definitions", + [ + test_case "local nested definitions (1)" `Quick + test_transform_simple_1; + ] ) ; + ( "ast formatting ", + [ test_case "identifier compilation" `Quick test_identifier ] ); + ] 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 -;;; -;;; 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 -;;; . - -(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 -;;; -;;; 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 -;;; . - -(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 - - - scope - rules - ι-policy-scope - ι-policy-rules - - - identifiers - with-anonymous-identifiers - add-to-scope - originating-breadcrumb - canonicalize - collapse-constraints - all-valid-identifiers - scope-contains? - find-local - - - inner - constraints - lean-name - resolved? - variable-ref->local - - - - - default-rule? - head - body - ι-rule-body - inductive-name - - - name - kind - left - right - - - ι-body-conjunction - - - args - - - - - - - scheme-value->type - - - - - - - - - - )) - -(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))))) - (($ kind left right default rules) - (let ((collective-rules `(,default ,@rules))) - (make - #: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 `', 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 ) 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 () - (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 -(define-slot-lens ι-policy-rules 'rules) - -;; Lens for focusing the global of a -(define-slot-lens ι-policy-scope 'scope) - - - -(define-class () - (identifiers #:init-keyword #:identifiers - #:accessor inner)) - -(define-class () - (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 #: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 - #: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 )) - (assert (is-a? 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 )) - (assert (is-a? identifier )) - (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 )) - (assert (list? breadcrumb)) - (recur breadcrumb)) - -(define (scope-contains? scope breadcrumb identifier) - "Whether SCOPE contains IDENTIFIER at the point indicated by BREADCRUMB - -`scope' is a , `breadcrumb' is a list given to the `f' of `mutate-tree', -and `identifier' is a " - (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? - (($ parts) (cut scope-contains? scope breadcrumb (first parts))) - (($ _) (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 () - ;; 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 () - (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 -(define-slot-lens ι-rule-body 'body) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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) - (($ (($ 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 () - (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 ) f scope breadcrumb) - (match form - (($ 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 () - (conjunction #:init-keyword #:conjunction - #:accessor inner)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 -(define-slot-lens ι-body-conjunction 'conjunction) - - - -;; Call to a Rego function -(define-class () - (ref #:init-keyword #:name ; (to the function being called) - #:accessor name) - (args #:init-keyword #:args ; list of - #:accessor args)) - -;; Universal quantification over some domain of Rego values -(define-class () - (domain #:init-keyword #:domain) - (key #:init-keyword #:key) - (value #:init-keyword #:value) - (body #:init-keyword #:body)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 () - (identifiers #:init-keyword #:identifiers - #:accessor identifiers)) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 () - (value #:init-keyword #:value)) ; scheme value - -(define-method (tree-map (form ) f scope breadcrumb) - (f scope breadcrumb form)) - -(define-class () - (elems #:init-keyword #:elems)) ; list of [scheme value | | ] - -(define-class () - (pairs #:init-keyword #:pairs)) ; list of [(string, scheme value | | )] - -(define-class () - (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 `', this is our semantic -;; encoding for variable dereferencing. Referring to a variable in scope would -;; be encoded as a `' containing a single `'. -(define-class () - (parts #:init-keyword #:parts - #:accessor inner)) - -(define-method (equal? (x ) (y )) - (equal? (inner x) (inner y))) - -(define-method (tree-map (form ) f scope breadcrumb) - (match form - (($ 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 `' as evaluating to the -;; value it refers to. For such an operation, we wrap the `' in a -;; `'. -(define-class () - (name #:init-keyword #:name ; - #:accessor inner)) - -(define-method (equal? (x ) (y )) - (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 -;;; -;;; 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 -;;; . - -(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))) -- cgit v1.3