Implement match compilation

1 files changed, 93 insertions, 21 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 382b99f..7dc2b44 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -43,7 +43,10 @@ let policy = {|<?xml version="1.0" encoding="UTF-8"?>
 
 
 
+type xml_element = (string * (string * string) list * Xml.xml list)
+
 type lean_expression = Identifier of string
+                     | Bool of bool
                      | String of string
                      | Number of int
                      | List of lean_expression list
@@ -52,6 +55,7 @@ type lean_expression = Identifier of string
 
 let rec fmt_lean_expression : lean_expression -> string = function
   | Identifier s -> s
+  | Bool b -> if b then "True" else "False"
   | String s -> Printf.sprintf "\"%s\"" s
   | Number n -> Int.to_string n
   | List xs -> Printf.sprintf "[%s]" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs))
@@ -62,13 +66,20 @@ let rec get_attr (needle : string) : (string * string) list -> string option = f
   | (k, v) :: xs -> if String.equal k needle then Some v else get_attr needle xs
   | _ -> None
 
-let rec get_children (kind : string) : Xml.xml list -> Xml.xml option = function
-  | (Element (tag_name, _, _) as x) :: xs ->
+let rec get_children (kind : string) : Xml.xml list -> xml_element list = function
+  | (Element ((tag_name, _, _) as x)) :: xs ->
      if String.equal tag_name kind
-     then Some x
+     then x :: get_children kind xs
      else get_children kind xs
   | PCData s :: xs -> get_children kind xs
-  | _ -> None
+  | _ -> []
+
+let get_child kind xs = List.nth (get_children kind xs) 0
+
+let xml_element_of_children (children : Xml.xml list) : xml_element list =
+  List.map children ~f:(function
+      | Element x -> x
+      | _ -> failwith "called on element with non-element children")
 
 let compile_rule_combinator_algorithm : string -> lean_expression = function
   | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-overrides" ->
@@ -95,33 +106,94 @@ let compile_rule_combinator_algorithm : string -> lean_expression = function
      (Identifier "RuleCombinatorAlgorithm.legacy_ordered_permit_overrides")
   | _ -> failwith "unknown rule combinator"
 
-let compile_match (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  failwith "unimplemented"
 
-let compile_all_of (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  failwith "unimplemented"
+open Option.Let_syntax
+(* let (tag_name, attributes, children) = elt in *)
 
-let compile_any_of (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  failwith "unimplemented"
+let compile_attribute_value (elt : xml_element) : lean_expression option =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "AttributeValue");
+  let%bind kind = get_attr "DataType" attrs in
+  match List.nth_exn children 0 with
+  | PCData s -> Some (Tuple [(String kind); (String s)])
+  | _ -> failwith "invalid value expression"
 
-let compile_target (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  Some (List [])
-  (* failwith "unimplemented" *)
+let compile_attribute_designator (elt : xml_element) : lean_expression option =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "AttributeDesignator");
+  let%bind category = get_attr "Category" attrs in
+  let%bind identifier = get_attr "AttributeId" attrs in
+  let%bind kind = get_attr "DataType" attrs in
+  let%bind must_be_present = get_attr "MustBePresent" attrs in
+  let issuer = 	(match get_attr "Issuer" attrs with
+    | Some s -> (Application ((Identifier "some"), [(String s)]))
+    | _ -> (Application ((Identifier "none"), [])))
+  in
+  Some (Application
+          ((Identifier "AttributeDesignator.mk"),
+           [(String category);
+            (String identifier);
+            (Identifier kind);
+            issuer;
+            (Bool (Bool.of_string must_be_present))]))
+
+let compile_match (elt : xml_element) : lean_expression option =
+  (* TODO: Can the match contain multiple value/designator pairs? *)
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "Match");
+  let%bind alg_id = get_attr "MatchId" attrs in
+  let%bind value = get_child "AttributeValue" children in
+  let%bind value = compile_attribute_value value in
+  let%bind designator = get_child "AttributeDesignator" children in
+  let%bind designator = compile_attribute_designator designator in
+  Some (Application
+          ((Identifier "Match.mk"),
+           [(String alg_id);
+            designator;
+            value]))
 
-let call_with (elt : Xml.xml) (f : (string * string) list -> Xml.xml list -> lean_expression option) : lean_expression option =
-  match elt with
-  | Element (tag_name, attributes, children) -> f attributes children
-  | _ -> failwith "elt is not an Element"
+let compile_all_of (elt : xml_element) : lean_expression option =
+  let (tag_name, _, children) = elt in
+  assert (String.equal tag_name "AllOf");
+  if phys_equal (List.length children) 0
+  then failwith "empty <AllOf>"
+  else failwith "unimplemented"
+
+let compile_any_of (elt : xml_element) : lean_expression option =
+  let (tag_name, _, children) = elt in
+  assert (String.equal tag_name "AnyOf");
+  if phys_equal (List.length children) 0
+  then failwith "empty <AnyOf>"
+  else failwith "unimplemented"
+
+let rec option_of_maybe_list : 'a option list -> 'a list option = function
+  | Some x :: xs -> (match option_of_maybe_list xs with
+                     | Some xs' -> Some (x::xs')
+                     | None -> None)
+  | [] -> Some []
+  | _ -> None
+
+let compile_target (elt : xml_element) : lean_expression option =
+  let (tag_name, _, children) = elt in
+  assert (String.equal tag_name "Target");
+  let%bind xs = List.map ~f:compile_any_of (xml_element_of_children children)
+                |> option_of_maybe_list in
+  Some (List xs)
+(* failwith "unimplemented" *)
+
+
 
 let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  let open Option.Let_syntax in
   let%bind alg_id = get_attr "RuleCombiningAlgId" attrs in
-  let%bind target = get_children "Target" children in
-  let%bind target = call_with target compile_target in
+  let%bind target = get_child "Target" children in
+  let%bind target = compile_target target in
   Some (Application
      ((Identifier "Policy.mk"),
       [(compile_rule_combinator_algorithm alg_id);
-       target]))
+       target;
+       (List []); (* TODO: Compile obligation expressions *)
+       (List []) (* TODO: Compile advice expressions *)
+    ]))
 
 let compile : Xml.xml -> lean_expression option = function
   | Element (tag_name, attributes, children) ->