diff options
| author | Jakob L. Kreuze | 2023-12-21 13:20:58 -0500 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-12-21 13:20:58 -0500 |
| commit | be7067d632aa665c20f96d3b344a84c95b0f8ff8 (patch) | |
| tree | fc5564a72cc42c8a21d3e943f645afcaae78f5a5 /rego-proofs/compiler-rewrite/lib/compiler.ml | |
| parent | 5918f84a1a05881d93d9fab83104feca9981bfaa (diff) | |
Check-in remaining files
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') |