diff options
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 71 |
1 files changed, 50 insertions, 21 deletions
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index 665f558..9d1cce4 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -233,13 +233,16 @@ let compile_target (elt : xml_element) : lean_expression = -let rec compile_expression (elt : xml_element) : lean_expression = +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 elt) + | Element elt -> Some (compile_expression env elt) | _ -> None) in Application (Identifier "Expression.apply", args) | "Function" -> @@ -253,17 +256,30 @@ let rec compile_expression (elt : xml_element) : lean_expression = Application (Identifier "Expression.attribute_value", [compile_attribute_value elt]) - | "VariableReference" -> failwith "unimplemented" + | "VariableReference" -> + (match children with + | [PCData identifier] -> + (match List.Assoc.find ~equal:String.equal env identifier with + | Some value -> value + (* TODO: Delayed referencing of variables? *) + | _ -> failwith "unbound variable") + | _ -> failwith "invalid <VariableReference>") | _ -> failwith "unknown expression type" -let compile_condition (elt : xml_element) : lean_expression = +let compile_condition + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = let (tag_name, _, children) = elt in assert (String.equal tag_name "Condition"); match children with - | [Element elt] -> compile_expression elt + | [Element elt] -> compile_expression env elt | _ -> failwith "invalid <Condition> form" -let compile_attribute_assignment_expression (elt : xml_element) : lean_expression = +let compile_attribute_assignment_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = let (tag_name, attrs, children) = elt in assert (String.equal tag_name "AdviceExpression"); let category = get_attr_exn "Category" attrs in @@ -277,9 +293,12 @@ let compile_attribute_assignment_expression (elt : xml_element) : lean_expressio [String category; String identifier; issuer; - compile_expression expression]) + compile_expression env expression]) -let compile_obligation_expression (elt : xml_element) : lean_expression = +let compile_obligation_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = let (tag_name, attrs, children) = elt in assert (String.equal tag_name "ObligationExpression"); let identifier = get_attr_exn "ObligationId" attrs in @@ -291,11 +310,14 @@ let compile_obligation_expression (elt : xml_element) : lean_expression = in Application (Identifier "ObligationExpression.mk", - [List (List.map assignments ~f:compile_attribute_assignment_expression); + [List (List.map assignments ~f:(compile_attribute_assignment_expression env)); String identifier; fulfill_on]) -let compile_advice_expression (elt : xml_element) : lean_expression = +let compile_advice_expression + (env : (string * lean_expression) list) + (elt : xml_element) + : lean_expression = let (tag_name, attrs, children) = elt in assert (String.equal tag_name "AdviceExpression"); let identifier = get_attr_exn "AdviceId" attrs in @@ -307,7 +329,7 @@ let compile_advice_expression (elt : xml_element) : lean_expression = in Application (Identifier "ObligationExpression.mk", - [List (List.map assignments ~f:compile_attribute_assignment_expression); + [List (List.map assignments ~f:(compile_attribute_assignment_expression env)); String identifier; applies_to]) @@ -340,7 +362,7 @@ let compile_rule | Some tgt -> compile_target tgt | None -> List [] in let condition = match get_child "Condition" children with - | Some cond -> compile_condition cond + | Some cond -> compile_condition env cond | None -> Identifier "none" in let metadata = Application @@ -348,8 +370,10 @@ let compile_rule [target; condition; effect; - List (List.map ~f:compile_obligation_expression obligation_expressions); - List (List.map ~f:compile_advice_expression advice_expressions);]) in + List (List.map ~f:(compile_obligation_expression env) + obligation_expressions); + List (List.map ~f:(compile_advice_expression env) + advice_expressions);]) in let identifier = canonicalize_identifier identifier in ([Define (identifier, @@ -358,12 +382,15 @@ let compile_rule Application ((Identifier "ElementTree.Node"), [Identifier identifier; List []])) -let compile_variable_definition (elt : xml_element) : string * lean_expression = +let compile_variable_definition + (env : (string * lean_expression) list) + (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) + (identifier, compile_expression env value) let compile_policy (elt : xml_element) : (lean_expression list) * lean_expression = let (tag_name, attrs, children) = elt in @@ -374,7 +401,7 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio List.fold (get_children "VariableDefinition" children) ~init:[] ~f:(fun x y -> - let (key, value) = compile_variable_definition y in + let (key, value) = compile_variable_definition x y in (key,value) :: x) in let obligation_expressions = get_children "ObligationExpression" children in @@ -386,8 +413,10 @@ let compile_policy (elt : xml_element) : (lean_expression list) * lean_expressio ((Identifier "Policy.mk"), [compile_rule_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 + List (List.map ~f:(compile_obligation_expression variables) + obligation_expressions); + List (List.map ~f:(compile_advice_expression variables) + advice_expressions);])in let identifier = canonicalize_identifier identifier ~version:(Some version) in let children = List.map ~f:(compile_rule variables) (get_children "Rule" children) in @@ -415,8 +444,8 @@ let rec compile_policyset (elt : xml_element) : (lean_expression list) * lean_ex ((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 + 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.filter_map ~f:(function | Element (("PolicySet", _, _) as elt) -> Some (compile_policyset elt) |