Support compilation of multiple files

3 files changed, 20 insertions, 10 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 3a2073e..946d65d 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -2,6 +2,7 @@ open Core
 open Compiler
 
 let () =
-  let file_name = Array.get (Sys.get_argv ()) 1 in
-  let policy_code = In_channel.read_all file_name in
+  let argv = Sys.get_argv () in
+  let file_names = Array.sub argv ~pos:1 ~len:(Array.length argv - 1) |> Array.to_list in
+  let policy_code = List.map file_names ~f:In_channel.read_all in
   compile' policy_code |> Stdio.print_endline
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"
diff --git a/xacml-proofs/compiler/lib/compiler.mli b/xacml-proofs/compiler/lib/compiler.mli
index 09198ba..0106059 100644
--- a/xacml-proofs/compiler/lib/compiler.mli
+++ b/xacml-proofs/compiler/lib/compiler.mli
@@ -1 +1 @@
-val compile' : string -> string
+val compile' : string list -> string