Inductive exprMatchSubject : Type := | EMS_False : exprMatchSubject | EMS_True : exprMatchSubject | EMS_WithRolesAll : RoleSets.t -> exprMatchSubject | EMS_WithRolesAny : RoleSets.t -> exprMatchSubject | EMS_And : list exprMatchSubject -> exprMatchSubject | EMS_Or : list exprMatchSubject -> exprMatchSubject .
Inductive exprMatchSubjectEvalR (s : subject) : exprMatchSubject -> Prop := | EMSR_True : exprMatchSubjectEvalR s EMS_True | EMSR_WithRolesAll : forall (r : RoleSets.t), RoleSets.Subset r (sRoles s) -> exprMatchSubjectEvalR s (EMS_WithRolesAll r) | EMSR_WithRolesAny : forall (r : RoleSets.t), (exists x, RoleSets.In x r /\ RoleSets.In x (sRoles s)) -> exprMatchSubjectEvalR s (EMS_WithRolesAny r) | EMSR_And : forall (es : list exprMatchSubject), Forall (exprMatchSubjectEvalR s) es -> exprMatchSubjectEvalR s (EMS_And es) | EMSR_Or : forall (es : list exprMatchSubject), Exists (exprMatchSubjectEvalR s) es -> exprMatchSubjectEvalR s (EMS_Or es) .
Fixpoint exprMatchSubjectEvalF (s : subject) (e : exprMatchSubject) : bool := match e with | EMS_False => false | EMS_True => true | EMS_WithRolesAll r => RoleSets.subset r (sRoles s) | EMS_WithRolesAny r => RoleSets.exists_ (fun x => RoleSets.mem x (sRoles s)) r | EMS_And es => forallb (exprMatchSubjectEvalF s) es | EMS_Or es => existsb (exprMatchSubjectEvalF s) es end.
Theorem exprMatchSubjectEvalEquivalentT : forall s e, true = exprMatchSubjectEvalF s e <-> exprMatchSubjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchSubjectEvalEquivalentF : forall s e, false = exprMatchSubjectEvalF s e <-> ~exprMatchSubjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchSubjectEvalRolesAllEmpty : forall s, true = exprMatchSubjectEvalF s (EMS_WithRolesAll RoleSets.empty). Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchSubjectEvalRolesAnyEmpty : forall s, false = exprMatchSubjectEvalF s (EMS_WithRolesAny RoleSets.empty). Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Inductive exprMatchAction : Type := | EMA_False : exprMatchAction | EMA_True : exprMatchAction | EMA_WithName : actionName -> exprMatchAction | EMA_And : list exprMatchAction -> exprMatchAction | EMA_Or : list exprMatchAction -> exprMatchAction .
Inductive exprMatchActionEvalR (a : action) : exprMatchAction -> Prop := | EMAR_True : exprMatchActionEvalR a EMA_True | EMAR_WithName : forall (x : actionName), ivName (aName a) = ivName x -> exprMatchActionEvalR a (EMA_WithName x) | EMAR_And : forall (es : list exprMatchAction), Forall (exprMatchActionEvalR a) es -> exprMatchActionEvalR a (EMA_And es) | EMAR_Or : forall (es : list exprMatchAction), Exists (exprMatchActionEvalR a) es -> exprMatchActionEvalR a (EMA_Or es) .
Fixpoint exprMatchActionEvalF (a : action) (e : exprMatchAction) : bool := match e with | EMA_False => false | EMA_True => true | EMA_WithName n => eqb (ivName (aName a)) (ivName n) | EMA_And xs => forallb (exprMatchActionEvalF a) xs | EMA_Or xs => existsb (exprMatchActionEvalF a) xs end.
Theorem exprMatchActionEvalEquivalentT : forall s e, true = exprMatchActionEvalF s e <-> exprMatchActionEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchActionEvalEquivalentF : forall a e, false = exprMatchActionEvalF a e <-> ~exprMatchActionEvalR a e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Inductive exprMatchObject : Type := | EMO_False : exprMatchObject | EMO_True : exprMatchObject | EMO_WithType : typeName -> exprMatchObject | EMO_WithAttributesAll : AttributeNameMaps.t attributeValue -> exprMatchObject | EMO_WithAttributesAny : AttributeNameMaps.t attributeValue -> exprMatchObject | EMO_And : list exprMatchObject -> exprMatchObject | EMO_Or : list exprMatchObject -> exprMatchObject .
Inductive exprMatchObjectEvalR (o : object) : exprMatchObject -> Prop := | EMOR_True : exprMatchObjectEvalR o EMO_True | EMOR_WithName : forall (t : typeName), ivName (oType o) = ivName t -> exprMatchObjectEvalR o (EMO_WithType t) | EMOR_WithAttributesAll : forall (required : AttributeNameMaps.t attributeValue), (forall (k : attributeName) (v : attributeValue), AttributeNameMaps.MapsTo k v required -> AttributeNameMaps.MapsTo k v (oAttributes o)) -> exprMatchObjectEvalR o (EMO_WithAttributesAll required) | EMOR_WithAttributesAny : forall (required : AttributeNameMaps.t attributeValue), (exists k : attributeName, (exists v : attributeValue, AttributeNameMaps.MapsTo k v required /\ AttributeNameMaps.MapsTo k v (oAttributes o))) -> exprMatchObjectEvalR o (EMO_WithAttributesAny required) | EMOR_And : forall (es : list exprMatchObject), Forall (exprMatchObjectEvalR o) es -> exprMatchObjectEvalR o (EMO_And es) | EMOR_Or : forall (es : list exprMatchObject), Exists (exprMatchObjectEvalR o) es -> exprMatchObjectEvalR o (EMO_Or es) .
Fixpoint exprMatchObjectEvalF (o : object) (e : exprMatchObject) : bool := match e with | EMO_False => false | EMO_True => true | EMO_WithType n => eqb (ivName (oType o)) (ivName n) | EMO_WithAttributesAll attributesRequired => let attributesHeld := oAttributes o in forallb (fun p => mapsB attributesHeld (fst p) (snd p)) (AttributeNameMaps.elements attributesRequired) | EMO_WithAttributesAny attributesRequired => let attributesHeld := oAttributes o in existsb (fun p => mapsB attributesHeld (fst p) (snd p)) (AttributeNameMaps.elements attributesRequired) | EMO_And xs => forallb (exprMatchObjectEvalF o) xs | EMO_Or xs => existsb (exprMatchObjectEvalF o) xs end.
Theorem exprMatchObjectEvalEquivalentT : forall s e, true = exprMatchObjectEvalF s e <-> exprMatchObjectEvalR s e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchObjectEvalEquivalentF : forall a e, false = exprMatchObjectEvalF a e <-> ~exprMatchObjectEvalR a e. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchObjectWithAllEmpty : forall o, exprMatchObjectEvalF o (EMO_WithAttributesAll (AttributeNameMaps.empty attributeValue)) = true. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.
Theorem exprMatchObjectWithAnyEmpty : forall o, exprMatchObjectEvalF o (EMO_WithAttributesAny (AttributeNameMaps.empty attributeValue)) = false. Proof. (* Proof omitted for brevity; see Matches.v for proofs. *) Qed.