List Files | Just Commands | Repo | Logs

← back | Copy

------------------------------- MODULE DirectoryFlexible -------------------------------

EXTENDS Sequences, FiniteSets, Naturals

CONSTANTS
  CATEGORIES,
  PROBLEMS,
  TAGS,
  Null,
  Parent,
  CatRel,     \* ⊆ PROBLEMS × CATEGORIES
  TagRel,
  TextMatches

VARIABLES query, Directory

(*--algorithm DirectoryEvalFlexible
variables
  visibleCats = {},
  visibleProblems = {},
  catView = [c \in CATEGORIES |-> {}];

begin
  if query.text # Null then
    \* Case 1: Text search active
    visibleProblems := { p \in PROBLEMS : TextMatches(p, query.text) };
    catView := [c \in CATEGORIES |-> {}];
  else
    \* Case 2: Category/tag refinement
    if query.category = Null then
      visibleCats := CATEGORIES;
    else
      visibleCats := Descendants(query.category);
    end if;

    visibleProblems := { p \in PROBLEMS :
                           \E c \in visibleCats : <<p, c>> \in CatRel
                           /\ query.tags \subseteq { t \in TAGS : <<p, t>> \in TagRel } };

    catView := [ c \in CATEGORIES |->
                  IF c \in visibleCats
                    THEN { p \in visibleProblems : <<p, c>> \in CatRel }
                    ELSE {} ];
  end if;

  Directory := [ problems |-> visibleProblems,
                 catView  |-> catView ];
end algorithm; *)

===============================================================================