Expression evaluation

1 files changed, 26 insertions, 12 deletions

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 80b1436..8464aa0 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -96,7 +96,6 @@ inductive XmlType
   | rfc822Name        : XmlType
   | ipAddress         : XmlType
   | dnsName           : XmlType
-  | xpathExpression   : XmlType
 deriving BEq, Repr
 
 def Primitive : Type := XmlType × String
@@ -278,17 +277,32 @@ namespace Expression
   def apply_eval (name : FunctionID) (args : List Value) : Option Value :=
     if name == "urn:oasis:names:tc:xacml:1.0:function:rfc822Name-match" then
       match args with
-        | [Value.primitive lhs, Value.primitive rhs] => Value.primitive (lhs == rhs)
-        | _          => Value.primitive (#<XmlType.boolean, "Indeterminate">)
+        | [Value.primitive (XmlType.string,     lhs),
+           Value.primitive (XmlType.rfc822Name, rhs)] =>
+           Value.primitive (lhs == rhs)
+        | _ => Value.primitive (#<XmlType.boolean, "Indeterminate">)
     else Option.none
 
   def eval (expression : Expression) (context : Request) : Option Value :=
+    -- The return type of `<Apply>` may be made more specific by type unification.
+    --
+    -- The evaluation result can be specified to be "Indeterminate"; we encode
+    -- this as `Option.none` here for ergonomics, but we do give an instance for
+    -- `Coe (Option Value) Value`.
+    --
+    -- § 7.6 enumerates but does not describe the semantics for:
+    --
+    -- - <xacml:AttributeValue>
+    -- - <xacml:AttributeDesignator>
+    -- - <xacml:AttributeSelector>
+    -- - <xacml:Apply>
+    -- - <xacml:Function>
+    -- - <xacml:VariableReference>
     match expression with
-      | Expression.apply name args => apply_eval name args
-      -- TODO: Is this the correct semantics, or is it more like how bags are handled for <Match>?
-      -- | Expression.attribute_designator inner =>
-        -- (inner.eval ctx.req).map(fun x => )
-      | _ => Option.none
+      | Expression.apply name args            => apply_eval name args
+      | Expression.attribute_designator inner => inner.eval context
+      | Expression.attribute_value inner      => some inner
+      | _                                     => Option.none
 end Expression
 
 structure Match where
@@ -310,7 +324,7 @@ namespace Match
         do
           let result <- designator.eval context
           let results := match result with
-          | (Value.bag (Bag.mk attrs)) => 
+          | (Value.bag (Bag.mk attrs)) =>
             attrs.map
             fun attr =>
               let args := [value, Value.primitive attr]
@@ -318,11 +332,11 @@ namespace Match
           | (Value.primitive attr) =>
             let args := [value, Value.primitive attr]
             [(Expression.apply fn args).eval context]
-      
+
           let results := results.map (fun (x : Option Value) => (x : Value))
-          if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then 
+          if results.elem (Value.primitive (#<XmlType.boolean, "True">)) then
             (Value.primitive (#<XmlType.boolean, "True">))
-          else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then 
+          else if results.elem (Value.primitive (#<XmlType.boolean, "Indeterminate">)) then
             (Value.primitive (#<XmlType.boolean, "Indeterminate">))
           else Value.primitive (#<XmlType.boolean, "False">)
 end Match