Proper executable for XACML compiler

5 files changed, 647 insertions, 678 deletions

diff --git a/xacml-proofs/compiler/bin/dune b/xacml-proofs/compiler/bin/dune
index 239df43..3d787bf 100644
--- a/xacml-proofs/compiler/bin/dune
+++ b/xacml-proofs/compiler/bin/dune
@@ -1,5 +1,4 @@
 (executable
  (public_name compiler)
  (name main)
- (libraries base compiler str topological_sort xml-light)
- (preprocess (pps ppx_let ppx_jane)))
+ (libraries core compiler))
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index d797e47..3a2073e 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -1,676 +1,7 @@
-open Base
+open Core
+open Compiler
 
-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
+let () =
+  let file_name = Array.get (Sys.get_argv ()) 1 in
+  let policy_code = In_channel.read_all file_name in
+  compile' policy_code |> Stdio.print_endline
diff --git a/xacml-proofs/compiler/lib/compiler.ml b/xacml-proofs/compiler/lib/compiler.ml
new file mode 100644
index 0000000..8938c63
--- /dev/null
+++ b/xacml-proofs/compiler/lib/compiler.ml
@@ -0,0 +1,636 @@
+open Base
+
+let version_regex = Str.regexp "^\\([0-9]+\\.\\)*[0-9]+$"
+let version_match_type_regex = Str.regexp "^\\(\\(\\d+|\\*\\)\\.\\)*\\(\\d+|\\*|\\+\\)$"
+
+
+
+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:nodes ~edges:edges ~what:Topological_sort.What.Nodes
+
+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 = "PolicySet"));
+  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)) ->
+           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", _, _)) ->
+           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:nodes ~edges:edges ~what:Topological_sort.What.Nodes
+
+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 compile' (policy : string) : string =
+  policy
+  |> Xml.parse_string
+  |> compile
+  |> List.map ~f:fmt_lean_expression
+  |> String.concat ~sep:"\n"
diff --git a/xacml-proofs/compiler/lib/compiler.mli b/xacml-proofs/compiler/lib/compiler.mli
new file mode 100644
index 0000000..09198ba
--- /dev/null
+++ b/xacml-proofs/compiler/lib/compiler.mli
@@ -0,0 +1 @@
+val compile' : string -> string
diff --git a/xacml-proofs/compiler/lib/dune b/xacml-proofs/compiler/lib/dune
index 15b8510..d243c0a 100644
--- a/xacml-proofs/compiler/lib/dune
+++ b/xacml-proofs/compiler/lib/dune
@@ -1,2 +1,4 @@
 (library
- (name compiler))
+ (name compiler)
+ (libraries base str topological_sort xml-light)
+ (preprocess (pps ppx_let ppx_jane)))