diff options
| author | Jakob L. Kreuze | 2023-10-04 18:54:20 -0400 |
|---|---|---|
| committer | Jakob L. Kreuze | 2023-10-04 18:54:20 -0400 |
| commit | 5e2e29e88ecc657faeb9d26e86a69d6b7efa2a8b (patch) | |
| tree | 12e12f234d6e93231cf825ac3aa4e40b64d1a693 /xacml-proofs | |
| parent | ac49ddc525a52b97025787e8a5861a9ea73c3db6 (diff) | |
Fix ordering issue with PolicySet compilation
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index 924760b..8c06545 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -400,8 +400,11 @@ let compile_policyset (elt : xml_element) : (lean_expression list) * lean_expres List (List.map ~f:compile_obligation_expression obligation_expressions); List (List.map ~f:compile_advice_expression advice_expressions);])in let identifier = canonicalize_identifier identifier ~version:(Some version) in - let children = List.map ~f:compile_policy (get_children "Policy" children) - @ List.map ~f:compile_rule (get_children "Rule" children) in + let children = List.filter_map ~f:(function + | Element (("Policy", _, _) as elt) -> Some (compile_policy elt) + | Element (("Rule", _, _) as elt) -> Some (compile_rule elt) + | _ -> None) + children in ([Define (identifier, Application |