diff options
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 5f8f797..8cf3cb6 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -375,7 +375,7 @@ and compile_query env literals : (environ * lean_expression) = | xs -> Application (Identifier "And", xs) |> simplify_expression in (env', form) -and compile_rule env subjects rule : (environ * lean_expression) = +and compile_rule env subjects rule : (environ * lean_expression) list = let { body = literals; _ } = rule in let (new_identifiers, _with_statement_constraints) = rewrite_with env literals in let env = List.map new_identifiers @@ -486,7 +486,9 @@ and compile_rule env subjects rule : (environ * lean_expression) = Exists ((List.map quantified_names ~f:lean_id_of_identifier , "Rego.Any"), Application (Identifier "And", subject_constraints @ constraints @ [form]) |> 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)); @@ -522,9 +524,11 @@ let compile_definition env (rules : rule list) = List.map args ~f:(fun arg_name -> gensym arg_name) @ [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 rule -> - let (_env', body) = compile_rule env subjects rule in + List.mapi conditional_rules ~f:(fun i (_env', body) -> (body, (Printf.sprintf "rule%d" i, [body], |