path: root/xacml-proofs/compiler/bin/main.ml

open Base

let version_regex = Str.regexp "^\\([0-9]+\\.\\)*[0-9]+$"
let version_match_type_regex = Str.regexp "^\\(\\(\\d+|\\*\\)\\.\\)*\\(\\d+|\\*|\\+\\)$"

let policy = {|<?xml version="1.0" encoding="UTF-8"?>
<Policy
  xmlns="urn:oasis:names:tc:xacml:3.0:core:schema:wd-17"
  xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
  xsi:schemaLocation="urn:oasis:names:tc:xacml:3.0:core:schema:wd-17
  http://docs.oasis-open.org/xacml/3.0/xacml-core-v3-schema-wd-17.xsd"
  PolicyId="urn:oasis:names:tc:xacml:3.0:example:SimplePolicy1"
  Version="1.0"
  RuleCombiningAlgId="urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-overrides">
  <Description>
    Medi Corp access control policy
  </Description>
  <Target/>
  <Rule
    RuleId= "urn:oasis:names:tc:xacml:3.0:example:SimpleRule1"
    Effect="Permit">
    <Description>
      Any subject with an e-mail name in the med.example.com domain
      can perform any action on any resource.
    </Description>
    <Target>
      <AnyOf>
        <AllOf>
          <Match
            MatchId="urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match">
          <AttributeValue
            DataType="http://www.w3.org/2001/XMLSchema#string"
              >med.example.com</AttributeValue>
          <AttributeDesignator
            MustBePresent="false"
            Category="urn:oasis:names:tc:xacml:1.0:subject-category:access-subject"
            AttributeId="urn:oasis:names:tc:xacml:1.0:subject:subject-id"
            DataType="urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"/>
          </Match>
        </AllOf>
      </AnyOf>
    </Target>
  </Rule>
</Policy>
|}



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
                     | 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
  | 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))
  | 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
  | Some x -> x
  | _ -> failwith message

let rec get_attr (needle : string) : (string * string) list -> string option = function
  | (k, v) :: xs -> if String.(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.(tag_name = kind)
     then x :: get_children kind xs
     else get_children kind xs
  | PCData s :: xs -> get_children kind xs
  | _ -> []

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
      | 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" ->
     (Identifier "RuleCombinatorAlgorithm.deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.ordered_permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:deny-unless-permit" ->
     (Identifier "RuleCombinatorAlgorithm.deny_unless_permit")
  | "urn:oasis:names:tc:xacml:3.0:rule-combining-algorithm:permit-unless-deny" ->
     (Identifier "RuleCombinatorAlgorithm.permit_unless_deny")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:first-applicable" ->
     (Identifier "RuleCombinatorAlgorithm.first_applicable")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.1:rule-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.0:rule-combining-algorithm:permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_permit_overrides")
  | "urn:oasis:names:tc:xacml:1.1:rule-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "RuleCombinatorAlgorithm.legacy_ordered_permit_overrides")
  | _ -> failwith "unknown rule combinator"

let compile_policy_combinator_algorithm : string -> lean_expression = function
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.ordered_permit_overrides")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:deny-unless-permit" ->
     (Identifier "PolicyCombinatorAlgorithm.deny_unless_permit")
  | "urn:oasis:names:tc:xacml:3.0:policy-combining-algorithm:permit-unless-deny" ->
     (Identifier "PolicyCombinatorAlgorithm.permit_unless_deny")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:first-applicable" ->
     (Identifier "PolicyCombinatorAlgorithm.first_applicable")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:only-one-applicable" ->
     (Identifier "PolicyCombinatorAlgorithm.only_one_applicable")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-deny-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_deny_overrides")
  | "urn:oasis:names:tc:xacml:1.0:policy-combining-algorithm:permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_permit_overrides")
  | "urn:oasis:names:tc:xacml:1.1:policy-combining-algorithm:ordered-permit-overrides" ->
     (Identifier "PolicyCombinatorAlgorithm.legacy_ordered_permit_overrides")
  | _ -> failwith "unknown policy combinator"

(* let (tag_name, attributes, children) = elt in *)

let compile_xml_type (s : string) : lean_expression =
  let kind = match s with
    | "http://www.w3.org/2001/XMLSchema#string"                -> "string"
    | "http://www.w3.org/2001/XMLSchema#boolean"               -> "boolean"
    | "http://www.w3.org/2001/XMLSchema#integer"               -> "integer"
    | "http://www.w3.org/2001/XMLSchema#double"                -> "double"
    | "http://www.w3.org/2001/XMLSchema#time"                  -> "time"
    | "http://www.w3.org/2001/XMLSchema#date"                  -> "date"
    | "http://www.w3.org/2001/XMLSchema#dateTime"              -> "dateTime"
    | "http://www.w3.org/2001/XMLSchema#anyURI"                -> "anyURI"
    | "http://www.w3.org/2001/XMLSchema#hexBinary"             -> "hexBinary"
    | "http://www.w3.org/2001/XMLSchema#base64Binary"          -> "base64Binary"
    | "http://www.w3.org/2001/XMLSchema#dayTimeDuration"       -> "dayTimeDuration"
    | "http://www.w3.org/2001/XMLSchema#yearMonthDuration"     -> "yearMonthDuration"
    | "urn:oasis:names:tc:xacml:1.0:data-type:x500Name"        -> "x500Name"
    | "urn:oasis:names:tc:xacml:1.0:data-type:rfc822Name"      -> "rfc822Name"
    | "urn:oasis:names:tc:xacml:2.0:data-type:ipAddress"       -> "ipAddress"
    | "urn:oasis:names:tc:xacml:2.0:data-type:dnsName"         -> "dnsName"
    | "urn:oasis:names:tc:xacml:3.0:data-type:xpathExpression" -> "xpathExpression"
    | _ -> failwith "unknown DataType"
  in
  Identifier ("XmlType." ^ kind)

let compile_primitive kind value : lean_expression =
  Application
    (Identifier "Value.primitive",
     [(Tuple [compile_xml_type kind; (String value)])])

let compile_attribute_value (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "AttributeValue"));
  let kind = get_attr_exn "DataType" attrs in
  match List.nth_exn children 0 with
  | PCData value -> compile_primitive kind value
  | _ -> failwith "invalid value expression"

let compile_attribute_designator (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "AttributeDesignator"));
  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)]))
    | _ -> (Identifier "none"))
  in
  Application
    ((Identifier "AttributeDesignator.mk"),
     [(String category);
      (String identifier);
      (compile_xml_type kind);
      issuer;
      (Bool (Bool.of_string must_be_present))])

let compile_match (elt : xml_element) : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "Match"));
  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 =
  let (tag_name, _, children) = elt in
  assert (String.(tag_name = "AllOf"));
  assert (not Int.((List.length children) = 0)); (* "empty <AllOf>" *)
  List (List.map ~f:compile_match (get_children "Match" children))

let compile_any_of (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.(tag_name = "AnyOf"));
  assert (not Int.((List.length children) = 0)); (* "empty <AnyOf>" *)
  List (List.map ~f:compile_all_of (get_children "AllOf" children))

let compile_target (elt : xml_element) : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.(tag_name = "Target"));
  List (List.map ~f:compile_any_of (xml_element_of_children children))



let rec compile_expression
          (env : (string * lean_expression) list)
          (elt : xml_element)
        : lean_expression =
  let (tag_name, attrs, children) = elt in
  match tag_name with
  | "Apply" ->
     let args = List.filter_map children ~f:(function
                    | Element ("Description", _, _) -> None
                    | Element elt -> Some (compile_expression env elt)
                    | _ -> None) in
     Application (Identifier "Expression.apply", args)
  | "Function" ->
     let name = get_attr_exn "FunctionID" attrs in
     Application (Identifier "Expression.function", [String name])
  | "AttributeDesignator" ->
     Application
       (Identifier "Expression.attribute_designator",
        [compile_attribute_designator elt])
  | "AttributeValue" ->
     Application
       (Identifier "Expression.attribute_value",
        [compile_attribute_value elt])
  | "VariableReference" ->
     let identifier = get_attr_exn "VariableId" attrs in
     (match List.Assoc.find ~equal:String.equal env identifier with
      | Some value -> value
      | _ -> failwith "unbound variable")
  | _ -> failwith "unknown expression type"

let compile_condition
      (env : (string * lean_expression) list)
      (elt : xml_element)
    : lean_expression =
  let (tag_name, _, children) = elt in
  assert (String.(tag_name = "Condition"));
  match children with
  | [Element elt] -> compile_expression env elt
  | _ -> failwith "invalid <Condition> form"

let compile_attribute_assignment_expression
      (env : (string * lean_expression) list)
      (elt : xml_element)
    : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "AdviceExpression"));
  let category = get_attr_exn "Category" attrs in
  let identifier = get_attr_exn "Identifier" attrs in
  let expression = get_child_exn "Expression" children in
  let issuer = (match get_attr "Identifier" attrs with
                | Some issuer -> Application (Identifier "some", [String issuer])
                | None -> Application (Identifier "none", [])) in
  Application
    (Identifier "AttributeAssignmentExpression.mk",
     [String category;
      String identifier;
      issuer;
      compile_expression env expression])

let compile_obligation_expression
      (env : (string * lean_expression) list)
      (elt : xml_element)
    : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "ObligationExpression"));
  let identifier = get_attr_exn "ObligationId" attrs in
  let assignments = get_children "AttributeAssignmentExpression" children in
  let fulfill_on = match get_attr_exn "FullfillOn" attrs with
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  Application
    (Identifier "ObligationExpression.mk",
     [List (List.map assignments ~f:(compile_attribute_assignment_expression env));
      String identifier;
      fulfill_on])

let compile_advice_expression
      (env : (string * lean_expression) list)
      (elt : xml_element)
    : lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "AdviceExpression"));
  let identifier = get_attr_exn "AdviceId" attrs in
  let assignments = get_children "AttributeAssignmentExpression" children in
  let applies_to = match get_attr_exn "AppliesTo" attrs with
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  Application
    (Identifier "ObligationExpression.mk",
     [List (List.map assignments ~f:(compile_attribute_assignment_expression env));
      String identifier;
      applies_to])

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 metadata_identifier_of ?(version = None) (ident : string) : string =
  canonicalize_identifier ~version:version ident ^ "_metadata"

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)
    : compilation_intermediate =
  let (tag_name, attrs, children) = elt in
  assert (String.(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
    | "Permit" -> Identifier "EffectType.permit"
    | "Deny" -> Identifier "EffectType.deny"
    | _ -> failwith "invalid <EffectType>"
  in
  let target = match get_child "Target" children with
    | Some tgt -> compile_target tgt
    | None -> List [] in
  let condition = match get_child "Condition" children with
    | Some cond -> compile_condition env cond
    | None -> Identifier "none" in
  let metadata =
    Application
      ((Identifier "Rule.mk"),
       [target;
        condition;
        effect;
        List (List.map ~f:(compile_obligation_expression env)
                obligation_expressions);
        List (List.map ~f:(compile_advice_expression env)
                advice_expressions);]) in
  let metadata_identifier = metadata_identifier_of identifier in
  let element_identifier = element_identifier_of identifier in
  { 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)
      (elt : xml_element)
    : string * lean_expression =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "VariableDefinition"));
  let identifier = get_attr_exn "VariableId" attrs in
  let value = get_child_exn "Expression" children in
  (identifier, compile_expression env value)

let order_variable_definitions elts =
  let rec find_variable_references identifier : Xml.xml -> (string * string) list =
    function
    | Element ("VariableReference", attrs, _) ->
       let referenced_identifier = get_attr_exn "VariableId" attrs in
       [(identifier, referenced_identifier)]
    | Element (_, _, children) ->
       List.map ~f:(find_variable_references identifier)
         children
       |> List.concat
    | _ -> []
  in
  let nodes =
    List.map
      ~f:(function
        | ("VariableDefinition", attrs, _) -> get_attr_exn "VariableId" attrs
        | _ -> failwith "unreachable")
      elts in
  let edges =
    List.map
      ~f:(function
        | ("VariableDefinition", attrs, children) as elt ->
           find_variable_references (get_attr_exn "VariableId" attrs) (Element elt)
        | _ -> failwith "unreachable")
      elts
    |> List.concat
  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_policy (elt : xml_element) : compilation_intermediate =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "Policy"));
  let identifier = get_attr_exn "PolicyId" attrs in
  let version = get_attr_exn "Version" attrs in
  assert (Str.string_match version_regex version 0);
  let variables = get_children "VariableDefinition" children in
  let variables =
    match order_variable_definitions variables with
    | Ok ordering ->
       List.map ordering
         ~f:(fun needle ->
           List.find_exn ~f:(function
               | ("VariableDefinition", attrs, _) ->
                  String.(needle = (get_attr_exn "VariableId" attrs))
               | _ -> false)
             variables)
    | _ -> failwith "failed to order variable definitions"
  in
  let variables =
    List.fold variables
      ~init:[]
      ~f:(fun x y ->
        let (key, value) = compile_variable_definition x y in
        (key,value) :: x)
  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
  let target = get_child_exn "Target" children in
  let metadata =
    Application
      ((Identifier "Policy.mk"),
       [compile_rule_combinator_algorithm alg_id;
        compile_target target;
        List (List.map ~f:(compile_obligation_expression variables)
                obligation_expressions);
        List (List.map ~f:(compile_advice_expression variables)
                advice_expressions);])in
  let children = List.map ~f:(compile_rule variables)
                   (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
  { 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
  | `Policy (identifier', version) :: xs ->
     if String.(identifier = identifier')
     then Some (canonicalize_identifier ~version:(Some version) identifier)
     else match_policy_reference xs identifier
  | `PolicySet (_, _) :: xs -> match_policy_reference xs identifier
  | [] -> None

let rec match_policyset_reference elements identifier regexes =
  match elements with
  | `PolicySet (identifier', version) :: xs ->
     if String.(identifier = identifier') &&
        List.for_all ~f:(fun regex -> Str.string_match regex version 0) regexes
     then Some (canonicalize_identifier ~version:(Some version) identifier)
     else match_policyset_reference xs identifier regexes
  | `Policy (_, _) :: xs -> match_policyset_reference xs identifier regexes
  | [] -> None

let rec compile_policyset
          policy_elements
          (elt : xml_element)
        : compilation_intermediate =
  let (tag_name, attrs, children) = elt in
  assert (String.(tag_name = "Rule"));
  let identifier = get_attr_exn "PolicySetId" attrs in
  let version = get_attr_exn "Version" attrs in
  assert (Str.string_match version_regex version 0);
  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
  let target = get_child_exn "Target" children in
  let metadata =
    Application
      ((Identifier "PolicySet.mk"),
       [compile_policy_combinator_algorithm alg_id;
        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))
             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
  { 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
  match tag_name with
  | "PolicySet" ->
     let identifier = get_attr_exn "PolicySetId" attrs in
     let version = get_attr_exn "Version" attrs in
     [`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" ->
     let identifier = get_attr_exn "PolicyId" attrs in
     let version = get_attr_exn "Version" attrs in
     [`Policy (identifier, version)]
  | _ -> []

let order_element_definitions elts =
  let nodes =
    List.map
      ~f:(function
        | Define (identifier, _) -> identifier
        | _ -> failwith "badly formed list of expressions")
      elts in
  let edges =
    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
  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 { 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
     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.(identifier = needle)
                   | _ -> false)
                 element_definitions)
        | _ -> failwith "failed to order definitions")
     in
     metadata_definitions @ element_definitions @ [Identifier root_identifier]
  | PCData s -> failwith s

let () = policy
         |> Xml.parse_string
         |> compile
         |> List.map ~f:fmt_lean_expression
         |> List.iter ~f:Caml.print_endline