Use OCaml exceptions for more traceable errors

1 files changed, 62 insertions, 61 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 7dc2b44..25c03e4 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -62,10 +62,18 @@ let rec fmt_lean_expression : lean_expression -> string = function
   | 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))
 
+let get_exn opt message =
+  match opt with
+  | Some x -> x
+  | _ -> failwith message
+
 let rec get_attr (needle : string) : (string * string) list -> string option = function
   | (k, v) :: xs -> if String.equal k needle then Some v else get_attr needle xs
   | _ -> None
 
+let get_attr_exn needle attrs : string =
+  get_exn (get_attr needle attrs) "missing attribute"
+
 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
@@ -75,6 +83,8 @@ let rec get_children (kind : string) : Xml.xml list -> xml_element list = functi
   | _ -> []
 
 let get_child kind xs = List.nth (get_children kind xs) 0
+let get_child_exn kind xs =
+  get_exn (get_child kind xs) "no such child"
 
 let xml_element_of_children (children : Xml.xml list) : xml_element list =
   List.map children ~f:(function
@@ -107,105 +117,96 @@ let compile_rule_combinator_algorithm : string -> lean_expression = function
   | _ -> failwith "unknown rule combinator"
 
 
-open Option.Let_syntax
 (* let (tag_name, attributes, children) = elt in *)
 
-let compile_attribute_value (elt : xml_element) : lean_expression option =
+let compile_attribute_value (elt : xml_element) : lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "AttributeValue");
-  let%bind kind = get_attr "DataType" attrs in
+  let kind = get_attr_exn "DataType" attrs in
   match List.nth_exn children 0 with
-  | PCData s -> Some (Tuple [(String kind); (String s)])
+  | PCData s -> (Tuple [(String kind); (String s)])
   | _ -> failwith "invalid value expression"
 
-let compile_attribute_designator (elt : xml_element) : lean_expression option =
+let compile_attribute_designator (elt : xml_element) : lean_expression =
   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
+  let category = get_attr_exn "Category" attrs in
+  let identifier = get_attr_exn "AttributeId" attrs in
+  let kind = get_attr_exn "DataType" attrs in
+  let must_be_present = get_attr_exn "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))]))
+  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 =
+let compile_match (elt : xml_element) : lean_expression =
   (* 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 alg_id = get_attr_exn "MatchId" attrs in
+  let value = get_child_exn "AttributeValue" children in
+  let designator = get_child_exn "AttributeDesignator" children in
+  Application
+    ((Identifier "Match.mk"),
+     [(String alg_id);
+      compile_attribute_designator designator;
+      compile_attribute_value value])
 
-let compile_all_of (elt : xml_element) : lean_expression option =
+let compile_all_of (elt : xml_element) : lean_expression =
   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 compile_any_of (elt : xml_element) : lean_expression =
   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 compile_target (elt : xml_element) : lean_expression =
   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" *)
+  List (List.map ~f:compile_any_of (xml_element_of_children children))
 
 
 
-let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression option =
-  let%bind alg_id = get_attr "RuleCombiningAlgId" attrs 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;
-       (List []); (* TODO: Compile obligation expressions *)
-       (List []) (* TODO: Compile advice expressions *)
-    ]))
+let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression =
+  let alg_id = get_attr_exn "RuleCombiningAlgId" attrs in
+  let target = get_child_exn "Target" children in
+  let target = compile_target target in
+  let metadata =
+    Application
+      ((Identifier "Policy.mk"),
+       [(compile_rule_combinator_algorithm alg_id);
+        target;
+        (List []);  (* TODO: Compile obligation expressions *)
+        (List [])]) (* TODO: Compile advice expressions *) in
+  let wrapped =
+    Application
+      ((Identifier "PolicyElement.Policy"), [metadata]) in
+  Application
+      ((Identifier "ElementTree.Node"), [wrapped; List []])
+
 
-let compile : Xml.xml -> lean_expression option = function
+let compile : Xml.xml -> lean_expression = function
   | Element (tag_name, attributes, children) ->
      (match tag_name with
       | "Policy" -> compile_policy attributes children
       | _ -> failwith (Printf.sprintf "(%s)" tag_name))
   | PCData s -> failwith s
 
-let () =
-  match compile @@ Xml.parse_string policy with
-  | Some ast ->
-     ast
-     |> fmt_lean_expression
-     |> Caml.print_endline
-  | _ -> failwith "compilation failed!"
+let () = policy
+         |> Xml.parse_string
+         |> compile
+         |> fmt_lean_expression
+         |> Caml.print_endline