Checkout.lean

Checkout.lean

structure User where
  name : String
  permissions : List String
deriving Repr, DecidableEq

def nobody : User := { name := "", permissions := [] }

structure Document where
  title : String
  owner : User
  req_perm : List String
  derivation : Nat
deriving Repr, DecidableEq

def nothing : Document := { title := "", owner := nobody, req_perm := [], derivation := 0 }

def check_out (u : User) (d : Document) : Document :=
  if (has_perm? u d) ∧ nobody_owns then
    { d with owner := u, derivation := 1 + d.derivation }
  else
    d
  where
    nobody_owns : Bool := d.owner = nobody
    has_perm? (u : User) (d : Document) : Bool :=
      u.permissions.any (fun x => d.req_perm.contains x)

def check_in (u : User) (d : Document) : Document :=
  if d.owner = u then
    { d with owner := nobody, derivation := 1 + d.derivation }
  else
    d

---------

def root : User := { name := "root", permissions := ["Admin"] }
def alice : User := { name := "Alice", permissions := ["Admin", "User"] }
def bob : User := { name := "Bob", permissions := ["User"] }

def passwords : Document := { title := "passwords.txt", owner := nobody, req_perm := ["Admin"], derivation := 0 }
def todos : Document := { title := "todos.txt", owner := nobody, req_perm := ["User"], derivation := 0}

#eval check_out root passwords     -- Changes document owner to root
#eval check_out root todos         -- Does not change document owner

#eval check_out alice passwords    -- Changes document owner to alice
#eval check_out alice todos        -- Changes document owner to alice

#eval check_out bob passwords      -- Does not change document owner
#eval check_out bob todos          -- Changes document owner to bob

#eval
  let doc := check_out bob todos;  -- Should let bob take ownership
  check_out alice doc              -- Should not let alice take ownership

#eval
  let doc := check_out bob todos;  -- Should let bob take ownership
  let doc' := check_in bob doc;    -- Should return doc owner to nobody
  check_out alice doc'             -- Changes document owner to alice