diff options
Diffstat (limited to 'xacml-proofs')
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 58 |
1 files changed, 48 insertions, 10 deletions
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index 25c03e4..86da69b 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -62,6 +62,11 @@ let rec fmt_lean_expression : lean_expression -> string = function | Tuple xs -> Printf.sprintf "(%s)" (String.concat ~sep:", " (List.map ~f:fmt_lean_expression xs)) | Application (head, args) -> Printf.sprintf "(%s %s)" (fmt_lean_expression head) (String.concat ~sep:" " (List.map ~f:fmt_lean_expression args)) +let option_to_lean_expr (opt : lean_expression option) : lean_expression = + match opt with + | Some expr -> Application (Identifier "some", [expr]) + | None -> Application (Identifier "none", []) + let get_exn opt message = match opt with | Some x -> x @@ -162,16 +167,14 @@ let compile_match (elt : xml_element) : lean_expression = let compile_all_of (elt : xml_element) : lean_expression = let (tag_name, _, children) = elt in assert (String.equal tag_name "AllOf"); - if phys_equal (List.length children) 0 - then failwith "empty <AllOf>" - else failwith "unimplemented" + assert (not @@ phys_equal (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.equal tag_name "AnyOf"); - if phys_equal (List.length children) 0 - then failwith "empty <AnyOf>" - else failwith "unimplemented" + assert (not @@ phys_equal (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 @@ -180,22 +183,57 @@ let compile_target (elt : xml_element) : lean_expression = +let compile_condition (elt : xml_element) : lean_expression = + let (tag_name, _, children) = elt in + assert (String.equal tag_name "Condition"); + assert (phys_equal (List.length children) 1); + List [] (* TODO: Implement compile_expression *) + +let compile_rule (elt : xml_element) : lean_expression = + let (tag_name, attrs, children) = elt in + assert (String.equal tag_name "Rule"); + let effect = match get_attr_exn "Effect" attrs with + | "Permit" -> Application (Identifier "EffectType.permit", []) + | "Deny" -> Application (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 cond + | None -> Application (Identifier "None", []) in + let metadata = + Application + ((Identifier "Rule.mk"), + [target; + condition; + effect; + (List []); (* TODO: Compile obligation expressions *) + (List [])]) (* TODO: Compile advice expressions *) in + let wrapped = + Application + ((Identifier "PolicyElement.Rule"), [metadata]) in + Application + ((Identifier "ElementTree.Node"), [wrapped; List []]) + let compile_policy (attrs : (string * string) list) (children : Xml.xml list) : lean_expression = let alg_id = get_attr_exn "RuleCombiningAlgId" attrs in let target = get_child_exn "Target" children in - let target = compile_target target in let metadata = Application ((Identifier "Policy.mk"), - [(compile_rule_combinator_algorithm alg_id); - target; + [compile_rule_combinator_algorithm alg_id; + compile_target target; (List []); (* TODO: Compile obligation expressions *) (List [])]) (* TODO: Compile advice expressions *) in let wrapped = Application ((Identifier "PolicyElement.Policy"), [metadata]) in Application - ((Identifier "ElementTree.Node"), [wrapped; List []]) + ((Identifier "ElementTree.Node"), + [wrapped; + List (List.map ~f:compile_rule (get_children "Rule" children))]) let compile : Xml.xml -> lean_expression = function |