Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

This is for 

Jira Legacy
serverSystem JIRA
serverId50130123-f232-3df4-bccb-c16e7d83cd3e
keyRHOL-533

...

The algorithm is (men ~ patterns, women ~ terms):

    while ∃ free man m who still has a woman w to propose to {
       w = first woman on m’s list to whom m has not yet proposed
       if w is free
         (m, w) become engaged
       else some pair (m', w) already exists
         if w prefers m to m'
            m' becomes free
           (m, w) become engaged 
         else
           (m', w) remain engaged

This assumes that there are M patterns and N terms and that M = N. 
If M < N, there will not be a match unless there is a wildcard or a remainder (see their sections below) and we should short-circuit unless there is one.

...

Code Block
new z in {
    for (@x <- Nil) { z } matches for (@x <- _) { zs }
    //the pattern is on the rhs of `matches` keyword
}

...