section_121.catala_en

@@Section 121@@

@@Begin metadata@@
/* 
declaration structure Period:
  data begin content date 
  data end content date

declaration scope PeriodMerge:
  context periods1 content collection Period 
  context periods2 content collection Period 
  context merged content collection Period

scope PeriodMerge:
  # Placeholders, overwritten by caller
  definition periods1 equals []
  definition periods2 equals []

  # TODO: find a way to implement the merging of two collections of date
  # periods into a single non-overlapping collection of date periods such 
  # that the output covers both input date ranges.
  definition output equals []

declaration scope Section121SinglePerson:
  context requirements_met condition 
  context requirements_ownership_met condition 
  context requirements_usage_met condition
  context date_of_sale_or_exchange content date
  context property_ownage content collection Period
  # Invariant: the periods in the collection are disjoint
  context property_usage_as_principal_residence 
    content collection Period
  # Invariant: the periods in the collection are disjoint
  context aggregate_periods_from_last_five_years content duration 
    depends on collection Period
  context gain_cap content money
  context gain_from_sale_or_exchange_of_property content money
  context income_excluded_from_gross_income_uncapped content money
  context income_excluded_from_gross_income content money

declaration structure PreviousSaleWhereSection121aApplied:
  data date_of_sale_or_exchange content date

declaration enumeration OtherSection121aSale:
  -- NoOtherSaleWhereSection121aApplied 
  -- MostRecentSaleWhereSection121aApplied content 
    PreviousSaleWhereSection121aApplied

declaration structure PersonalData:
  data property_ownage content collection Period
  data property_usage_as_principal_residence 
    content collection Period
  data other_section_121a_sale content OtherSection121aSale

declaration structure JointReturn: 
  data person1 content PersonalData 
  data person2 content PersonalData 

declaration structure DeadSpouseInfo:
  data return content PersonalData
  data date_of_spouse_death content date
  data death_spouse_info_at_time_of_death content PersonalData 

declaration enumeration ReturnType:
  -- SingleReturn content PersonalData
  -- JointReturn content JointReturn
  -- SingleReturnSurvivingSpouse content DeadSpouseInfo

declaration scope Section121TwoPersons:
  context person1 content PersonalData
  context section121Person1 scope Section121SinglePerson
  context person2 content PersonalData
  context section121Person2 scope Section121SinglePerson
  context section121a_requirements_met condition
  context section_121_b_3_applies content boolean 
    depends on OtherSection121aSale
  context section_121_b_2_A_condition condition
  context gain_cap_person_1 content money 
  context gain_cap_person_2 content money
  context gain_cap content money
  context return_type content ReturnType 
  context return_date content date
  context date_of_sale_or_exchange content date
  context gain_from_sale_or_exchange_of_property content money
  context income_excluded_from_gross_income_uncapped content money
  context income_excluded_from_gross_income content money
  context period_merge scope PeriodMerge

# Defining sub-scopes arguments
scope Section121TwoPersons:
  definition section121Person2.date_of_sale_or_exchange equals 
    date_of_sale_or_exchange
  definition section121Person1.date_of_sale_or_exchange equals 
    date_of_sale_or_exchange

  definition person1 equals match return_type with pattern 
    -- SingleReturn of data_person1 : data_person1
    -- JointReturn of data_couple : data_couple.person1
    -- SingleReturnSurvivingSpouse of data_single: data_single.return

  definition person2 equals match return_type with pattern 
    -- SingleReturn of data_person2 : data_person2
    -- JointReturn of data_couple : data_couple.person2
    -- SingleReturnSurvivingSpouse of data_single: data_single.return

  definition section121Person1.property_ownage equals person1.property_ownage

  definition section121Person1.property_usage_as_principal_residence equals 
    person1.property_usage_as_principal_residence

  definition section121Person2.property_ownage equals person2.property_ownage

  definition section121Person2.property_usage_as_principal_residence equals 
    person1.property_usage_as_principal_residence

  definition section121Person1.gain_from_sale_or_exchange_of_property equals 
    gain_from_sale_or_exchange_of_property
  definition section121Person2.gain_from_sale_or_exchange_of_property equals 
    gain_from_sale_or_exchange_of_property

  definition gain_cap_person_1 equals section121Person1.gain_cap 
  definition gain_cap_person_2 equals section121Person2.gain_cap

declaration scope Section121TwoPasses:
  context first_pass scope Section121TwoPersons
  context second_pass scope Section121TwoPersons
  context return_type content ReturnType 
  context return_date content date
  context date_of_sale_or_exchange content date
  context gain_from_sale_or_exchange_of_property content money
  context period_merge scope PeriodMerge
  context income_excluded_from_gross_income content money

# Defining sub-scopes arguments
scope Section121TwoPasses:
  definition first_pass.return_type equals return_type 
  definition second_pass.return_type equals return_type 
  
  definition first_pass.return_date equals return_date 
  definition second_pass.return_date equals return_date 

  definition first_pass.gain_from_sale_or_exchange_of_property equals 
    gain_from_sale_or_exchange_of_property
  definition second_pass.gain_from_sale_or_exchange_of_property equals 
    gain_from_sale_or_exchange_of_property

  definition first_pass.date_of_sale_or_exchange equals date_of_sale_or_exchange
  definition second_pass.date_of_sale_or_exchange equals date_of_sale_or_exchange

  definition income_excluded_from_gross_income equals 
    second_pass.income_excluded_from_gross_income
*/
@@End metadata@@

@(a) Exclusion@

Gross income shall not include gain from the sale or exchange of property if, 
during the 5-year period ending on the date of the sale or exchange, such 
property has been owned and used by the taxpayer as the taxpayer’s principal 
residence for periods aggregating 2 years or more. 
/*
scope Section121SinglePerson:
  # Here we aggregate over all the periods of the collection. For 
  # each period, three cases:
  # - either the period began less that 5 years before the 
  #   date_of_sale_or_exchange in which case we count if full
  # - either the period ended more that 5 years before the 
  #   date_of_sale_or_exchange in which case we don't count it 
  # - either the 5 years mark is inside the period and we only 
  #   cound the half after 5 years
  definition aggregate_periods_from_last_five_years of periods equals 
    sum duration for period in periods of (
      if date_of_sale_or_exchange <=@ period.begin +@ 5 year then
        period.end -@ period.begin
      else (if date_of_sale_or_exchange >=@ period.end +@ 5 year then 
        0 day 
      else ((period.end +@ 5 year) -@ date_of_sale_or_exchange))
    )

  # Regulation 1.121-1(c)(1): 2 years = 730 days
  # Regulation 1.121-1(c)(1): the periods of ownage and usage 
  # don't have to overlap
  rule requirements_ownership_met under condition 
    aggregate_periods_from_last_five_years of property_ownage >=^ 730 day
  consequence fulfilled 

  rule requirements_usage_met under condition 
    aggregate_periods_from_last_five_years of
       property_usage_as_principal_residence >=^ 730 day
  consequence fulfilled

  rule requirements_met under condition 
    requirements_ownership_met and requirements_usage_met
  consequence fulfilled

  definition income_excluded_from_gross_income_uncapped equals
    if requirements_met then gain_from_sale_or_exchange_of_property
    else $0
  
scope Section121TwoPersons:
  definition section121a_requirements_met equals section121Person1.requirements_met

  definition income_excluded_from_gross_income_uncapped equals 
    section121Person1.income_excluded_from_gross_income_uncapped

*/

@@(b) Limitations@@+

@(1) In general@

The amount of gain excluded from gross income under subsection (a) with 
respect to any sale or exchange shall not exceed $250,000.
/*
scope Section121SinglePerson:
  definition gain_cap equals $250,000
  
  # Big semantics insight for Catala. Here we could want to get rid of 
  # the "_uncapped" version of the variable. But in the current 
  # semantics we can't do that because we don't allow for recursion.
  definition income_excluded_from_gross_income equals 
    if income_excluded_from_gross_income_uncapped >=$ gain_cap then 
      gain_cap
    else 
      income_excluded_from_gross_income_uncapped

scope Section121TwoPersons: 
    definition gain_cap equals section121Person1.gain_cap 

    definition income_excluded_from_gross_income equals 
    if income_excluded_from_gross_income_uncapped >=$ gain_cap then 
      gain_cap
    else 
      income_excluded_from_gross_income_uncapped
*/

@(2) Special rules for joint returns@

In the case of a husband and wife who make a joint return for the taxable year  
of the sale or exchange of the property—

/*
# Taxable year of the sale or exchange ?=? year when the income is taxed
# Imagine a couple selling the house in 2020 and getting the payment in 
# 2021 where they file a joint return. Does (A) apply or not ? 
# Reasonably it should.
*/

@(A) $500,000 Limitation for certain joint returns@

Paragraph (1) shall be applied by substituting “$500,000” for “$250,000” if—

(i) either spouse meets the ownership requirements of subsection (a) with
respect to such property;

(ii) both spouses meet the use requirements of subsection (a) with respect to 
such property; and

(iii) neither spouse is ineligible for the benefits of subsection (a) with 
respect to such property by reason of paragraph (3).

/*
scope Section121TwoPersons:
  rule section_121_b_2_A_condition under condition 
  (return_type with pattern JointReturn of data_couple)
  and 
  # i) 
  (section121Person1.requirements_ownership_met or 
     section121Person2.requirements_ownership_met) 
  and
  # ii) 
  (section121Person1.requirements_usage_met and 
     section121Person2.requirements_usage_met)
  # iii)
  and
  (not (
      section_121_b_3_applies of data_couple.person1.other_section_121a_sale))
  and 
  (not (
      section_121_b_3_applies of data_couple.person2.other_section_121a_sale)) 
  consequence fulfilled
    
  exception
  rule section121a_requirements_met under condition 
    section_121_b_2_A_condition 
  consequence fulfilled
  
  exception 
  definition gain_cap under condition 
    section_121_b_2_A_condition
  consequence equals $500,000
*/

@(B) Other joint returns@
If such spouses do not meet the requirements of subparagraph (A), the limitation 
under paragraph (1) shall be the sum of the limitations under paragraph (1) to 
which each spouse would be entitled if such spouses had not been married. For 
purposes of the preceding sentence, each spouse shall be treated as owning the 
property during the period that either spouse owned the property.
/*
scope Section121TwoPasses under condition 
  (return_type with pattern JointReturn) and 
  not (first_pass.section_121_b_2_A_condition):

  definition second_pass.gain_cap equals 
    first_pass.gain_cap_person_1 +$ 
    first_pass.gain_cap_person_2

  definition period_merge.periods1 equals match return_type with pattern 
    -- JointReturn of joint_return: joint_return.person1.property_ownage
    -- SingleReturnSurvivingSpouse of dead_spouse_info : [] # does not happen
    -- SingleReturn of return : [] # does not happen
  definition period_merge.periods2 equals match return_type with pattern 
    -- JointReturn of joint_return: joint_return.person2.property_ownage
    -- SingleReturnSurvivingSpouse of dead_spouse_info : [] # does not happen
    -- SingleReturn of return : [] # does not happen

  definition second_pass.person1 equals PersonalData {
    -- property_ownage: period_merge.output
    -- property_usage_as_principal_residence: 
      first_pass.person1.property_usage_as_principal_residence
    -- other_section_121a_sale: first_pass.person1.other_section_121a_sale
  }
  definition second_pass.person2 equals PersonalData {
    -- property_ownage: period_merge.output
    -- property_usage_as_principal_residence: 
      first_pass.person2.property_usage_as_principal_residence
    -- other_section_121a_sale: first_pass.person2.other_section_121a_sale
  }
*/
@(3) Application to only 1 sale or exchange every 2 years@


Subsection (a) shall not apply to any sale or exchange by the taxpayer if, 
during the 2-year period ending on the date of such sale or exchange, there 
was any other sale or exchange by the taxpayer to which subsection (a) applied.
/*
scope Section121TwoPersons: 
  definition section_121_b_3_applies of other_section_121a_sale equals 
    (other_section_121a_sale with pattern 
       MostRecentSaleWhereSection121aApplied of other_sale) and
    date_of_sale_or_exchange -@ other_sale.date_of_sale_or_exchange <=^ 2 year
*/

@(4) Special rule for certain sales by surviving spouses@

/*
# Sarah: the year when your spouse dies, do you file a joint return or 
# separate returns?
*/
In the case of a sale or exchange of property by an unmarried individual whose 
spouse is deceased on the date of such sale, paragraph (1) shall be applied by 
substituting “$500,000” for “$250,000” if such sale occurs not later than 2 
years after the date of death of such spouse and the requirements of paragraph 
(2)(A) were met immediately before such date of death.
/*
scope Section121TwoPasses under condition 
  return_type with pattern SingleReturnSurvivingSpouse of single_data and 
  single_data.date_of_spouse_death <@ date_of_sale_or_exchange and
  date_of_sale_or_exchange <=@ single_data.date_of_spouse_death +@ 2 year 
  # So here we have to reexecute the scope Section121 using 
  # single_data.date_of_spouse_death instead of date_of_sale_or_exchange
  :
  
  definition second_pass.date_of_sale_or_exchange equals 
    match return_type with pattern
    -- SingleReturnSurvivingSpouse of single_data: single_data.date_of_spouse_death
    -- SingleReturn of return: date_of_sale_or_exchange # does not happen
    -- JointReturn of return: date_of_sale_or_exchange # does not happen
  definition second_pass.gain_cap equals $500,000
*/

@@(5) Exclusion of gain allocated to nonqualified use@@++

@(A) In general@

Subsection (a) shall not apply to so much of the gain from the sale or exchange 
of property as is allocated to periods of nonqualified use.

@(B) Gain allocated to periods of nonqualified use@

For purposes of subparagraph (A), gain shall be allocated to periods of 
nonqualified use based on the ratio which—

(i) the aggregate periods of nonqualified use during the period such property 
was owned by the taxpayer, bears to

(ii) the period such property was owned by the taxpayer.

@@(C) Period of nonqualified use@@+++ 

For purposes of this paragraph—

@(i) In general@

The term “period of nonqualified use” means any period (other than the portion 
of any period preceding January 1, 2009) during which the property is not used 
as the principal residence of the taxpayer or the taxpayer’s spouse or former 
spouse.

@(ii) Exceptions@ 

The term “period of nonqualified use” does not include—

(I) any portion of the 5-year period described in subsection (a) which is after 
the last date that such property is used as the principal residence of the 
taxpayer or the taxpayer’s spouse,

(II) any period (not to exceed an aggregate period of 10 years) during which the 
taxpayer or the taxpayer’s spouse is serving on qualified official extended duty 
(as defined in subsection (d)(9)(C)) described in clause (i), (ii), or (iii) of 
subsection (d)(9)(A), and

(III) any other period of temporary absence (not to exceed an aggregate period 
of 2 years) due to change of employment, health conditions, or such other 
unforeseen circumstances as may be specified by the Secretary.
@(D) Coordination with recognition of gain attributable to depreciation@

For purposes of this paragraph—

(i) subparagraph (A) shall be applied after the application of subsection 
(d)(6), and

(ii) subparagraph (B) shall be applied without regard to any gain to which 
subsection (d)(6) applies.