From d04e5cb8377384f920ff9d4b689836e1dc99e152 Mon Sep 17 00:00:00 2001
From: Jakob L. Kreuze
Date: Tue, 19 Sep 2023 19:34:23 -0400
Subject: Condition evaluation

---
 xacml-proofs/lean/Xacml.lean | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/xacml-proofs/lean/Xacml.lean b/xacml-proofs/lean/Xacml.lean
index 8a7a40e..8aadefd 100644
--- a/xacml-proofs/lean/Xacml.lean
+++ b/xacml-proofs/lean/Xacml.lean
@@ -456,11 +456,31 @@ deriving BEq, Repr
 -- n.b. "The <Condition> contains one <Expression> element"
 structure Rule where
   target      : Target
-  condition   : Expression
+  condition   : Option Expression
   effect      : EffectType
   obligations : List ObligationExpression
   advice      : List AdviceExpression
 
+namespace Rule
+  def eval (rule : Rule) (context : Request) : MatchResult :=
+    let condition :=
+      match rule.condition with
+        | some condition =>
+          -- The condition value SHALL be "True" if the <Condition> element
+          -- evaluates to "True".
+          let result := condition.eval context
+          if result == some (Value.primitive (#<XmlType.boolean, "True">)) then result
+          -- Its value SHALL be "False" if the <Condition> element evaluates to
+          -- "False".
+          else if result == some (Value.primitive (#<XmlType.boolean, "False">)) then result
+          -- The condition value SHALL be "Indeterminate", if the expression
+          -- contained in the <Condition> element evaluates to "Indeterminate."
+          else Value.primitive (#<XmlType.boolean, "Indeterminate">)
+        -- The condition value SHALL be "True" if the <Condition> element is absent.
+        | none => Value.primitive (#<XmlType.boolean, "True">)
+    sorry
+end Rule
+
 structure PolicySet where
   combinator  : CombinatorAlgorithm
   target      : Target
-- 
cgit v1.3