diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/ast.ml | 10 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/ast.mli | 2 | ||||
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 35 |
3 files changed, 29 insertions, 18 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/ast.ml b/rego-proofs/compiler-rewrite/lib/ast.ml index 6a43425..98d8375 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.ml +++ b/rego-proofs/compiler-rewrite/lib/ast.ml @@ -53,7 +53,7 @@ type rule_head_lhs = reference [@@deriving eq, show] type rule_head_rhs = | Assignment of assign_operator * term - | Function of assign_operator * string list * term + | Function of assign_operator * term list * term | Set of term [@@deriving eq, show] @@ -98,6 +98,7 @@ let rec parse_term (tree : Yojson.Basic.t) : term = 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)) @@ -218,8 +219,7 @@ let parse_head tree = else if not (tree |> member "args" |> is_null) then Function ( assign_operator, - tree |> member "args" |> to_list - |> List.map ~f:(fun x -> x |> member "value" |> to_string), + 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 @@ -263,7 +263,9 @@ 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; - (In_channel.input_all ic, In_channel.input_all ec) + 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, _ = diff --git a/rego-proofs/compiler-rewrite/lib/ast.mli b/rego-proofs/compiler-rewrite/lib/ast.mli index 1d3d69a..514d5da 100644 --- a/rego-proofs/compiler-rewrite/lib/ast.mli +++ b/rego-proofs/compiler-rewrite/lib/ast.mli @@ -40,7 +40,7 @@ type rule_head_lhs = reference type rule_head_rhs = | Assignment of assign_operator * term - | Function of assign_operator * string list * term + | Function of assign_operator * term list * term | Set of term type rule_head = rule_head_lhs * rule_head_rhs diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 898ff51..21405a3 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -356,7 +356,7 @@ let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) (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)) -> @@ -370,7 +370,7 @@ let lift_term (env : environ) (rule : rule) (f : environ -> term -> ('a * term) (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 @@ -541,8 +541,6 @@ and compile_rule env subjects rule : (environ * lean_expression) list = (* | _ -> None) in *) - List.iter literals ~f:(fun lit -> show_literal lit |> print_endline); - let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in let env = List.map new_identifiers ~f:(fun (old_name, anonymous_name) -> @@ -551,13 +549,20 @@ and compile_rule env subjects rule : (environ * lean_expression) list = 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) -> - List.map args ~f:(fun arg_name -> (Var arg_name : term)) @ [output] + args @ [output] in let env_updates_and_constraints = @@ -568,7 +573,7 @@ and compile_rule env subjects rule : (environ * lean_expression) list = 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 identifier ~equal:String.equal -> + | Var identifier when List.mem (bound @ explicit_parameters) identifier ~equal:String.equal -> (Some identifier, [(identifier, { lean_id = subject; kind = Parameter; assigned = true })], None) @@ -584,10 +589,7 @@ and compile_rule env subjects rule : (environ * lean_expression) list = 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 -> - if List.mem parameters id ~equal:String.equal then - None - else Some id + | Var id -> Some id | _ -> None) in (non_parameters, @@ -597,11 +599,18 @@ and compile_rule env subjects rule : (environ * lean_expression) list = 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 + |> 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 })); @@ -685,7 +694,7 @@ let compile_definition env (rules : rule list) = | `ObjectRule _ -> [gensym "k"; gensym "v"] | `FunctionRule (args, _) -> - List.map args ~f:(fun arg_name -> gensym arg_name) + List.map args ~f:(fun _ -> gensym "arg") @ [gensym "y"] in let conditional_rules = @@ -769,7 +778,7 @@ let compile_error_condition env = Identifier value_name])))) | _ -> None) |> fold_and - + let compile_package = let string_of_reference : reference -> string = function | (Var name, xs) -> |