Order Lean definitions

2 files changed, 143 insertions, 73 deletions

diff --git a/xacml-proofs/compiler/bin/dune b/xacml-proofs/compiler/bin/dune
index 6d76295..239df43 100644
--- a/xacml-proofs/compiler/bin/dune
+++ b/xacml-proofs/compiler/bin/dune
@@ -1,5 +1,5 @@
 (executable
  (public_name compiler)
  (name main)
- (libraries base compiler str xml-light)
- (preprocess (pps ppx_let)))
+ (libraries base compiler str topological_sort xml-light)
+ (preprocess (pps ppx_let ppx_jane)))
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 36ca738..66a7145 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -353,10 +353,18 @@ let metadata_identifier_of ?(version = None) (ident : string) : string =
 let element_identifier_of ?(version = None) (ident : string) : string =
   canonicalize_identifier ~version:version ident ^ "_element"
 
+type compilation_intermediate =
+  { metadata_definitions : lean_expression list;
+    element_definitions : lean_expression list;
+    root_identifier : string;
+    edges : (int * int) list
+  }
+[@@deriving fields]
+
 let compile_rule
       (env : (string * lean_expression) list)
       (elt : xml_element)
-    : (lean_expression list) * string =
+    : compilation_intermediate =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "RuleId" attrs in
@@ -385,16 +393,20 @@ let compile_rule
                 advice_expressions);]) in
   let metadata_identifier = metadata_identifier_of identifier in
   let element_identifier = element_identifier_of identifier in
-  ([Define
-      (metadata_identifier,
-       Application
-         ((Identifier "PolicyElement.Rule"), [metadata]));
-    Define
-      (element_identifier,
-       Application
-         ((Identifier "ElementTree.Node"),
-          [Identifier metadata_identifier; List []]))],
-   element_identifier)
+  { metadata_definitions =
+      [Define
+         (metadata_identifier,
+          Application
+            ((Identifier "PolicyElement.Rule"), [metadata]))];
+    element_definitions =
+      [Define
+         (element_identifier,
+          Application
+            ((Identifier "ElementTree.Node"),
+             [Identifier metadata_identifier; List []]))];
+    root_identifier = element_identifier;
+    edges = []
+  }
 
 let compile_variable_definition
       (env : (string * lean_expression) list)
@@ -406,7 +418,7 @@ let compile_variable_definition
   let value = get_child_exn "Expression" children in
   (identifier, compile_expression env value)
 
-let compile_policy (elt : xml_element) : (lean_expression list) * string =
+let compile_policy (elt : xml_element) : compilation_intermediate =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Policy");
   let identifier = get_attr_exn "PolicyId" attrs in
@@ -436,18 +448,23 @@ let compile_policy (elt : xml_element) : (lean_expression list) * string =
                    (get_children "Rule" children) in
   let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in
   let element_identifier = element_identifier_of identifier ~version:(Some version) in
-  ((List.map ~f:fst children |> List.concat)
-   @ [Define
-        (metadata_identifier,
-         Application
-           ((Identifier "PolicyElement.Policy"), [metadata]));
-      Define
-        (element_identifier,
-         Application
-           ((Identifier "ElementTree.Node"),
-            [Identifier metadata_identifier;
-             List (List.map ~f:(fun x -> Identifier (snd x)) children)]))],
-   element_identifier)
+  { metadata_definitions =
+      (List.map ~f:metadata_definitions children |> List.concat)
+      @ [Define
+           (metadata_identifier,
+            Application
+              ((Identifier "PolicyElement.Policy"), [metadata]))];
+    element_definitions =
+      (List.map ~f:element_definitions children |> List.concat)
+      @ [Define
+           (element_identifier,
+            Application
+              ((Identifier "ElementTree.Node"),
+               [Identifier metadata_identifier;
+                List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))];
+    root_identifier = element_identifier;
+    edges = []
+  }
 
 let rec match_policy_reference elements identifier =
   match elements with
@@ -471,7 +488,7 @@ let rec match_policyset_reference elements identifier regexes =
 let rec compile_policyset
           policy_elements
           (elt : xml_element)
-        : (lean_expression list) * string =
+        : compilation_intermediate =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "PolicySetId" attrs in
@@ -488,51 +505,66 @@ let rec compile_policyset
         compile_target target;
         List (List.map ~f:(compile_obligation_expression []) obligation_expressions);
         List (List.map ~f:(compile_advice_expression []) advice_expressions);])in
-  let children = List.filter_map ~f:(function
-                     | Element (("PolicySet", _, _) as elt) ->
-                        Some (compile_policyset policy_elements elt)
-                     | Element (("PolicySetIdReference", attrs, children) as elt) ->
-                        let identifier = match children with
-                          | [PCData identifier] -> identifier
-                          | _ -> failwith "invalid PolicySetIdReference"
-                        in
-                        let regexes =
-                          List.filter_map ~f:(fun x -> x) [
-                              get_attr "xacml:Version" attrs;
-                              get_attr "xacml:EarliestVersion" attrs;
-                              get_attr "xacml:LatestVersion" attrs
-                            ]
-                        in
-                        List.iter ~f:(fun x -> assert (Str.string_match version_match_type_regex x 0)) ;
-                        let regexes = List.map ~f:Str.regexp regexes in
-                        (match match_policyset_reference policy_elements identifier regexes with
-                         | Some identifier -> Some ([], identifier)
-                         | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier))
-                     | Element (("Policy", _, _) as elt) -> Some (compile_policy elt)
-                     | Element (("PolicyIdReference", _, _) as elt) ->
-                        let identifier = match children with
-                          | [PCData identifier] -> identifier
-                          | _ -> failwith "invalid PolicyIdReference"
-                        in
-                        (match match_policy_reference policy_elements identifier with
-                         | Some identifier -> Some ([], identifier)
-                         | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier))
-                     | _ -> None)
-                   children in
+  let children =
+    List.filter_map ~f:(function
+        | Element (("PolicySet", _, _) as elt) ->
+           Some (compile_policyset policy_elements elt)
+        | Element (("PolicySetIdReference", attrs, children) as elt) ->
+           let identifier = match children with
+             | [PCData identifier] -> identifier
+             | _ -> failwith "invalid PolicySetIdReference"
+           in
+           let regexes =
+             List.filter_map ~f:(fun x -> x) [
+                 get_attr "xacml:Version" attrs;
+                 get_attr "xacml:EarliestVersion" attrs;
+                 get_attr "xacml:LatestVersion" attrs
+               ]
+           in
+           List.iter ~f:(fun x -> assert (Str.string_match version_match_type_regex x 0))
+             regexes ;
+           let regexes = List.map ~f:Str.regexp regexes in
+           (match match_policyset_reference policy_elements identifier regexes with
+            | Some identifier ->
+               Some { metadata_definitions = [];
+                      element_definitions = [];
+                      root_identifier = identifier;
+                      edges = [] }
+            | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier))
+        | Element (("Policy", _, _) as elt) -> Some (compile_policy elt)
+        | Element (("PolicyIdReference", _, _) as elt) ->
+           let identifier = match children with
+             | [PCData identifier] -> identifier
+             | _ -> failwith "invalid PolicyIdReference"
+           in
+           (match match_policy_reference policy_elements identifier with
+            | Some identifier ->
+               Some { metadata_definitions = [];
+                      element_definitions = [];
+                      root_identifier = identifier;
+                      edges = [] }
+            | _ -> failwith (Printf.sprintf "unbound reference to %s" identifier))
+        | _ -> None)
+      children in
   let metadata_identifier = metadata_identifier_of identifier ~version:(Some version) in
   let element_identifier = element_identifier_of identifier ~version:(Some version) in
-  ((List.map ~f:fst children |> List.concat)
-   @ [Define
-      (metadata_identifier,
-       Application
-         ((Identifier "PolicyElement.PolicySet"), [metadata]));
-    Define
-      (element_identifier,
-       Application
-         ((Identifier "ElementTree.Node"),
-          [Identifier metadata_identifier;
-           List (List.map ~f:(fun x -> Identifier (snd x)) children)]))],
-   element_identifier)
+  { metadata_definitions =
+      (List.map ~f:metadata_definitions children |> List.concat)
+      @ [Define
+           (metadata_identifier,
+            Application
+              ((Identifier "PolicyElement.PolicySet"), [metadata]))];
+    element_definitions =
+      (List.map ~f:element_definitions children |> List.concat)
+      @ [Define
+           (element_identifier,
+            Application
+              ((Identifier "ElementTree.Node"),
+               [Identifier metadata_identifier;
+                List (List.map ~f:(fun x -> Identifier (root_identifier x)) children)]))];
+    root_identifier = element_identifier;
+    edges = []
+  }
 
 let rec policy_element_names (root : xml_element) =
   let (tag_name, attrs, children) = root in
@@ -543,22 +575,60 @@ let rec policy_element_names (root : xml_element) =
      [`PolicySet (identifier, version)]
      @ (List.map ~f:policy_element_names (get_children "PolicySet" children) |> List.concat)
      @ (List.map ~f:policy_element_names (get_children "Policy" children) |> List.concat)
-  | "Policy" -> 
+  | "Policy" ->
      let identifier = get_attr_exn "PolicyId" attrs in
      let version = get_attr_exn "Version" attrs in
      [`Policy (identifier, version)]
   | _ -> []
 
+let find_edges (elts : lean_expression list) : (string * string) list =
+  List.map
+    ~f:(function
+      | Define (parent, Application (_, [_; List children])) ->
+         List.map ~f:(function
+             | Identifier child -> (child, parent)
+             | _ -> failwith "badly formed list of expressions")
+           children
+      | _ -> failwith "badly formed list of expressions")
+    elts
+  |> List.concat
+
+let find_nodes (elts : lean_expression list) : string list =
+  List.map
+    ~f:(function
+      | Define (identifier, _) -> identifier
+      | _ -> failwith "badly formed list of expressions")
+    elts
+
+let order_element_definitions element_definitions =
+  let nodes = find_nodes element_definitions in
+  let edges = find_edges element_definitions in
+  let open Topological_sort in
+  let edges = List.map edges ~f:(fun (from, to_) -> { Topological_sort.Edge.from; to_ }) in
+  sort (module String) nodes edges
+
 let compile : Xml.xml -> lean_expression list = function
   | Element ((tag_name, attributes, children) as elt) ->
-     let (defns, tree_root_identifier) =
+     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))
-     in defns @ [Identifier tree_root_identifier]
+     in
+     let element_definitions =
+       (match order_element_definitions element_definitions with
+        | Result.Ok ordering ->
+           List.map ordering
+             ~f:(fun needle ->
+               List.find_exn ~f:(function
+                   | Define (identifier, _) -> String.equal identifier needle
+                   | _ -> false)
+                 element_definitions)
+        | _ -> failwith "failed to order definitions")
+     in
+     metadata_definitions @ element_definitions @ [Identifier root_identifier]
   | PCData s -> failwith s
 
 let () = policy