diff options
Diffstat (limited to 'rego-proofs/compiler-rewrite/lib/compiler.ml')
| -rw-r--r-- | rego-proofs/compiler-rewrite/lib/compiler.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/rego-proofs/compiler-rewrite/lib/compiler.ml b/rego-proofs/compiler-rewrite/lib/compiler.ml index 03f37d0..3b0384a 100644 --- a/rego-proofs/compiler-rewrite/lib/compiler.ml +++ b/rego-proofs/compiler-rewrite/lib/compiler.ml @@ -10,7 +10,6 @@ type definition_kind = Complete | 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 @@ -21,6 +20,9 @@ let fold_and props = | 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 @@ -259,7 +261,7 @@ let rec compile_term env : term -> lean_expression = let terms' = List.map ~f:(compile_term env) terms in if List.is_empty terms' then target' - else Application (Identifier "Rego.Any.deref", [target'] @ terms') + else [target'] @ terms' |> fold_deref | Array xs -> let xs' = List.map ~f:(compile_term env) xs in Application (Identifier "Rego.Any.array", xs') |