diff options
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 123 |
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 |