(* RT^D backchaining spec. *)

(* core types *)
entity : type.
role_name : type.
role_expr : type.

(* role expression constructors *)
^ : entity -> role_expr.
role : entity -> role_name -> role_expr.
linked_role : entity -> role_name -> role_name -> role_expr.
inter : list role_expr -> role_expr.

(* credentials are facts *)
credential : entity -> role_name -> role_expr -> o.

delegation : entity -> entity -> role_expr -> entity -> o.

(* role membership predicates *)
for_role : entity -> entity -> role_expr -> o.
for_roles : entity -> entity -> list role_expr -> o.

for_role B2 D (role A R) <=
  (delegation B1 D (role A R) B2,
   for_role B1 D (role A R)).
for_role B B (role A R) <= 
   credential A R (^ B).
for_role D E (role A R0) <= 
  (credential A R0 (role B R1),
   for_role D E (role B R1)).
for_role D E (role A R0) <=
  (credential A R0 (linked_role B R1 R2),
   for_role A0 A0 (role B R1),
   for_role D E (role A0 R2)).
for_role D E (role A R) <=
  (credential A R (inter Res),
   for_roles D E Res).

for_roles D E nil.
for_roles D E (role A R::Res) <=
  (for_role D E (role A R),
   for_roles D E Res).