diff options
| -rw-r--r-- | xacml-proofs/compiler/bin/main.ml | 40 |
1 files changed, 34 insertions, 6 deletions
diff --git a/xacml-proofs/compiler/bin/main.ml b/xacml-proofs/compiler/bin/main.ml index 86da69b..ad1e6c4 100644 --- a/xacml-proofs/compiler/bin/main.ml +++ b/xacml-proofs/compiler/bin/main.ml @@ -124,12 +124,40 @@ let compile_rule_combinator_algorithm : string -> lean_expression = function (* 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.equal tag_name "AttributeValue"); let kind = get_attr_exn "DataType" attrs in match List.nth_exn children 0 with - | PCData s -> (Tuple [(String kind); (String s)]) + | PCData value -> compile_primitive kind value | _ -> failwith "invalid value expression" let compile_attribute_designator (elt : xml_element) : lean_expression = @@ -141,13 +169,13 @@ let compile_attribute_designator (elt : xml_element) : lean_expression = 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)])) - | _ -> (Application ((Identifier "none"), []))) + | _ -> (Identifier "none")) in Application ((Identifier "AttributeDesignator.mk"), [(String category); (String identifier); - (Identifier kind); + (compile_xml_type kind); issuer; (Bool (Bool.of_string must_be_present))]) @@ -193,8 +221,8 @@ 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", []) + | "Permit" -> Identifier "EffectType.permit" + | "Deny" -> Identifier "EffectType.deny" | _ -> failwith "invalid <EffectType>" in let target = match get_child "Target" children with @@ -202,7 +230,7 @@ let compile_rule (elt : xml_element) : lean_expression = | None -> List [] in let condition = match get_child "Condition" children with | Some cond -> compile_condition cond - | None -> Application (Identifier "None", []) in + | None -> Identifier "none" in let metadata = Application ((Identifier "Rule.mk"), |