Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Walking example

//! Mini lease vocabulary. Exercises all five atoms.

use std::math::{Nat, Money, Date, DateTime};
use std::diag::{Diagnostic, Severity};
use std::format::format;
use std::time::{today, now};

/// A natural person.
pub type Person { name: String, age: Nat }

/// A rentable real-estate unit.
pub type Property { address: String, sqft: Nat }

/// Lease — relation with intrinsic property body.
pub rel Lease(tenant: Person, property: Property) [0..*] [0..*] {
    monthly_rent: Money,
    start:        Date,
    end:          Date,
    status:       LeaseStatus,
}

pub enum LeaseStatus { Pending, Active, Expired, Terminated }

impl Person {
    /// All active leases held by this person.
    pub query active_leases(self) -> [Lease] {
        select l from l: Lease, Lease(self, _) where is_active(l)
    }
}

impl Lease {
    pub fn daily_rent(self) -> Money = self.monthly_rent / 30;
}

pub derive is_active(l: Lease) :- l.start <= today(), l.end > today();

pub mutate sign_lease(t: Person, p: Property, rent: Money, term_days: Nat) -> Lease {
    require { rent > 0, term_days > 0 }
    let l = insert Lease(t, p) {
        monthly_rent: rent,
        start:        today(),
        end:          today() + term_days.days,
        status:       Pending,
    };
    emit AuditLog { LeaseEvent::Signed { lease: l, at: now() } };
    return l;
}

pub check no_overlapping_leases(t: Person, p: Property) :-
    count { from l: Lease where l.tenant == t, l.property == p, is_active(l) } > 1
    => Diagnostic {
        severity: Severity::Error,
        code:     "Lease::E001",
        message:  format!("Tenant {} has overlapping active leases on {}", t.name, p.address),
    };

pub trait Renewable { fn renew(self, term_days: Nat) -> Self; }

impl Renewable for Lease {
    fn renew(self, term_days: Nat) -> Lease = Lease {
        ..self,
        start:  self.end,
        end:    self.end + term_days.days,
        status: Pending,
    };
}

#[derive(Json, Hashable)]
pub struct Receipt { lease: Lease, paid: Money, at: Date }

#[consistency(strict)]
pub standpoint CaliforniaTenancyLaw <: BaseTenancyLaw {
    pub check ab1482_rent_cap(l: Lease) :-
        l.monthly_rent > l.property.market_rate * 1.10
        => Diagnostic {
            severity: Severity::Error,
            code:     "CA::AB1482",
            message:  "Lease exceeds AB-1482 rent cap",
        };
}

pub sink AuditLog: LeaseEvent;

pub enum LeaseEvent {
    Signed     { lease: Lease, at: DateTime },
    Renewed    { lease: Lease, at: DateTime },
    Terminated { lease: Lease, at: DateTime },
}

test "active leases are returned for tenant" {
    let alice = insert Person { name: "Alice", age: 30 };
    let unit  = insert Property { address: "1 Main", sqft: 700 };
    let l = sign_lease(alice, unit, 2500, 365);
    assert alice.active_leases() == [l];
}