Individual definitions for policy elements

1 files changed, 60 insertions, 31 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 49fef95..924760b 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -52,6 +52,7 @@ type lean_expression = Identifier of string
                      | List of lean_expression list
                      | Tuple of lean_expression list
                      | Application of lean_expression * lean_expression list
+                     | Define of string * lean_expression
 
 let rec fmt_lean_expression : lean_expression -> string = function
   | Identifier s -> s
@@ -61,6 +62,7 @@ let rec fmt_lean_expression : lean_expression -> string = function
   | List xs -> Printf.sprintf "[%s]" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
   | Tuple xs -> Printf.sprintf "(%s)" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
   | Application (head, args) -> Printf.sprintf "(%s %s)" (fmt_lean_expression head) (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args))
+  | Define (ident, expr) -> Printf.sprintf "def %s := (%s)" ident (fmt_lean_expression expr)
 
 let get_exn opt message =
   match opt with
@@ -309,9 +311,21 @@ let compile_advice_expression (elt : xml_element) : lean_expression =
       String identifier;
       applies_to])
 
-let compile_rule (elt : xml_element) : lean_expression =
+let canonicalize_identifier ?(version = None) (ident : string) : string =
+  let is_alphanumeric = function
+      'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' -> true
+      | _ -> false in
+  let filtered = match version with
+    | Some version -> List.filter ~f:is_alphanumeric
+                        (String.to_list (ident ^ "_" ^ version))
+    | None -> List.filter ~f:is_alphanumeric (String.to_list ident)
+  in
+  "compiled_" ^ (String.of_char_list filtered)
+
+let compile_rule (elt : xml_element) : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
+  let identifier = get_attr_exn "RuleId" attrs in
   let obligation_expressions = get_children "ObligationExpression" children in
   let advice_expressions = get_children "AdviceExpression"children  in
   let effect = match get_attr_exn "Effect" attrs with
@@ -333,15 +347,19 @@ let compile_rule (elt : xml_element) : lean_expression =
         effect;
         List (List.map ~f:compile_obligation_expression obligation_expressions);
         List (List.map ~f:compile_advice_expression advice_expressions);]) in
-  let wrapped =
-    Application
-      ((Identifier "PolicyElement.Rule"), [metadata]) in
-  Application
-      ((Identifier "ElementTree.Node"), [wrapped; List []])
+  let identifier = canonicalize_identifier identifier in
+  ([Define
+      (identifier,
+       Application
+         ((Identifier "PolicyElement.Rule"), [metadata]))],
+   Application
+     ((Identifier "ElementTree.Node"), [Identifier identifier; List []]))
 
-let compile_policy (elt : xml_element) : lean_expression =
+let compile_policy (elt : xml_element) : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Policy");
+  let identifier = get_attr_exn "PolicyId" attrs in
+  let version = get_attr_exn "Version" attrs in
   let obligation_expressions = get_children "ObligationExpression" children in
   let advice_expressions = get_children "AdviceExpression" children in
   let alg_id = get_attr_exn "RuleCombiningAlgId" attrs in
@@ -353,17 +371,23 @@ let compile_policy (elt : xml_element) : lean_expression =
         compile_target target;
         List (List.map ~f:compile_obligation_expression obligation_expressions);
         List (List.map ~f:compile_advice_expression advice_expressions);])in
-  let wrapped =
-    Application
-      ((Identifier "PolicyElement.Policy"), [metadata]) in
-  Application
-    ((Identifier "ElementTree.Node"),
-     [wrapped;
-      List (List.map ~f:compile_rule (get_children "Rule" children))])
+  let identifier = canonicalize_identifier identifier ~version:(Some version) in
+  let children = List.map ~f:compile_rule (get_children "Rule" children) in
+  ([Define
+      (identifier,
+       Application
+         ((Identifier "PolicyElement.Policy"), [metadata]))]
+   @ (List.map ~f:fst children |> List.concat),
+   Application
+     ((Identifier "ElementTree.Node"),
+      [Identifier identifier;
+       List (List.map ~f:snd children)]))
 
-let compile_policyset (elt : xml_element) : lean_expression =
+let compile_policyset (elt : xml_element) : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
+  let identifier = get_attr_exn "PolicySetId" attrs in
+  let version = get_attr_exn "Version" attrs in
   let obligation_expressions = get_children "ObligationExpression" children in
   let advice_expressions = get_children "AdviceExpression" children in
   let alg_id = get_attr_exn "PolicyCombiningAlgId" attrs in
@@ -375,26 +399,31 @@ let compile_policyset (elt : xml_element) : lean_expression =
         compile_target target;
         List (List.map ~f:compile_obligation_expression obligation_expressions);
         List (List.map ~f:compile_advice_expression advice_expressions);])in
-  let wrapped =
-    Application
-      ((Identifier "PolicyElement.PolicySet"), [metadata]) in
-  Application
-    ((Identifier "ElementTree.Node"),
-     [wrapped;
-      (* FIXME: This doesn't preserve order. *)
-      List ((List.map ~f:compile_policy (get_children "Policy" children))
-            @ (List.map ~f:compile_rule (get_children "Rule" children)))])
+  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
+  ([Define
+      (identifier,
+       Application
+         ((Identifier "PolicyElement.PolicySet"), [metadata]))]
+   @ (List.map ~f:fst children |> List.concat),
+   Application
+     ((Identifier "ElementTree.Node"),
+      [Identifier identifier;
+       List (List.map ~f:snd children)]))
 
-let compile : Xml.xml -> lean_expression = function
+let compile : Xml.xml -> lean_expression list = function
   | Element ((tag_name, attributes, children) as elt) ->
-     (match tag_name with
-      | "PolicySet" -> compile_policyset elt
-      | "Policy" -> compile_policy elt
-      | _ -> failwith (Printf.sprintf "(%s)" tag_name))
+     let (defns, tree) =
+       (match tag_name with
+        | "PolicySet" -> compile_policyset elt
+        | "Policy" -> compile_policy elt
+        | _ -> failwith (Printf.sprintf "(%s)" tag_name))
+     in defns @ [tree]
   | PCData s -> failwith s
 
 let () = policy
          |> Xml.parse_string
          |> compile
-         |> fmt_lean_expression
-         |> Caml.print_endline
+         |> List.map ~f:fmt_lean_expression
+         |> List.iter ~f:Caml.print_endline