Compilation of typed literals

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"),