Environment for variable erasure

1 files changed, 21 insertions, 3 deletions

diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml
index 3d48789..665f558 100644
--- a/xacml-proofs/compiler/bin/main.ml
+++ b/xacml-proofs/compiler/bin/main.ml
@@ -322,7 +322,10 @@ let canonicalize_identifier ?(version = None) (ident : string) : string =
   in
   "compiled_" ^ (String.of_char_list filtered)
 
-let compile_rule (elt : xml_element) : (lean_expression list) * lean_expression =
+let compile_rule
+      (env : (string * lean_expression) list)
+      (elt : xml_element)
+    : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "RuleId" attrs in
@@ -355,11 +358,25 @@ let compile_rule (elt : xml_element) : (lean_expression list) * lean_expression
    Application
      ((Identifier "ElementTree.Node"), [Identifier identifier; List []]))
 
+let compile_variable_definition (elt : xml_element) : string * lean_expression =
+  let (tag_name, attrs, children) = elt in
+  assert (String.equal tag_name "VariableDefinition");
+  let identifier = get_attr_exn "VariableId" attrs in
+  let value = get_child_exn "Expression" children in
+  (identifier, compile_expression value)
+
 let compile_policy (elt : xml_element) : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Policy");
   let identifier = get_attr_exn "PolicyId" attrs in
   let version = get_attr_exn "Version" attrs in
+  let variables =
+    List.fold (get_children "VariableDefinition" children)
+      ~init:[]
+      ~f:(fun x y ->
+        let (key, value) = compile_variable_definition 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
@@ -372,7 +389,8 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio
         List (List.map ~f:compile_obligation_expression obligation_expressions);
         List (List.map ~f:compile_advice_expression advice_expressions);])in
   let identifier = canonicalize_identifier identifier ~version:(Some version) in
-  let children = List.map ~f:compile_rule (get_children "Rule" children) in
+  let children = List.map ~f:(compile_rule variables)
+                   (get_children "Rule" children) in
   ([Define
       (identifier,
        Application
@@ -383,7 +401,7 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio
       [Identifier identifier;
        List (List.map ~f:snd children)]))
 
-let compile_policyset (elt : xml_element) : (lean_expression list) * lean_expression =
+let rec compile_policyset (elt : xml_element) : (lean_expression list) * lean_expression =
   let (tag_name, attrs, children) = elt in
   assert (String.equal tag_name "Rule");
   let identifier = get_attr_exn "PolicySetId" attrs in