diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 21405a3..03f37d0 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -441,12 +441,11 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function (env'', ForAll (([key; value], "Rego.Any"), - (Application - (Identifier "And", - [(Application - ((Identifier "Membership.mem"), - [Tuple [Identifier key; Identifier value]; domain'])); - query'])) + 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 @@ -456,12 +455,11 @@ let rec compile_expr env : expr -> (environ * lean_expression) = function (env'', ForAll (([value], "Rego.Any"), - (Application - (Identifier "And", - [(Application - ((Identifier "Membership.mem"), - [Identifier value; domain'])); - query'])) + fold_and + [(Application + ((Identifier "Membership.mem"), + [Identifier value; domain'])); + query'] |> simplify_expression)) and compile_literal env : literal -> (environ * lean_expression) = function @@ -479,7 +477,7 @@ 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 -> Application (Identifier "And", xs) |> simplify_expression in + | xs -> xs |> fold_and |> simplify_expression in (env', form) and compile_comprehension env anonymous_name (comp : term) = @@ -653,11 +651,11 @@ and compile_rule env subjects rule : (environ * lean_expression) list = (env'', if List.is_empty quantified_names then - Application (Identifier "And", [form]) - |> simplify_expression + fold_and [form] |> simplify_expression else Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), - Application (Identifier "And", constraints @ comprehension_constraints @ [form]) + constraints @ comprehension_constraints @ [form] + |> fold_and |> simplify_expression)) :: (match rule.otherwise with | Some branch -> compile_rule env subjects branch |