diff options
Diffstat (limited to 'xacml-proofs/compiler/lib/compiler.ml')
| -rw-r--r-- | xacml-proofs/compiler/lib/compiler.ml | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/xacml-proofs/compiler/lib/compiler.ml b/xacml-proofs/compiler/lib/compiler.ml index 8938c63..73ecd6e 100644 --- a/xacml-proofs/compiler/lib/compiler.ml +++ b/xacml-proofs/compiler/lib/compiler.ml @@ -509,7 +509,7 @@ let rec compile_policyset List.filter_map ~f:(function | Element (("PolicySet", _, _) as elt) -> Some (compile_policyset policy_elements elt) - | Element (("PolicySetIdReference", attrs, _children)) -> + | Element (("PolicySetIdReference", attrs, children)) -> let identifier = match children with | [PCData identifier] -> identifier | _ -> failwith "invalid PolicySetIdReference" @@ -604,12 +604,11 @@ let order_element_definitions elts = let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in sort (module String) ~nodes:nodes ~edges:edges ~what:Topological_sort.What.Nodes -let compile : Xml.xml -> lean_expression list = function +let compile policy_elements : Xml.xml -> lean_expression list = function | Element ((tag_name, _attributes, _children) as elt) -> let { metadata_definitions; element_definitions; root_identifier; _ } = (match tag_name with | "PolicySet" -> - let policy_elements = (policy_element_names elt) in compile_policyset policy_elements elt | "Policy" -> compile_policy elt | _ -> failwith (Printf.sprintf "(%s)" tag_name)) @@ -628,9 +627,19 @@ let compile : Xml.xml -> lean_expression list = function metadata_definitions @ element_definitions @ [Identifier root_identifier] | PCData s -> failwith s -let compile' (policy : string) : string = - policy - |> Xml.parse_string - |> compile +let xml_element_of_Xml : Xml.xml -> xml_element = function + | Element (elt) -> elt + | _ -> failwith "not an element" + + +let compile' (policies : string list) : string = + let policies = List.map ~f:Xml.parse_string policies in + let policy_elements = List.map ~f:xml_element_of_Xml policies + |> List.map ~f:policy_element_names + |> List.concat in + List.map + policies + ~f:(compile policy_elements) + |> List.concat |> List.map ~f:fmt_lean_expression |> String.concat ~sep:"\n" |