What the operators do to sets of values: the part of typing an operation that is refinement (D-133).
Feel.Analysis.Inference types left + right, -operand, left < right. It works out the kind of the result
from the kinds of the operands (a number, a date, a duration, a boolean) and whether the result can be null.
What a type can say besides is which values the result can have, [0..150] + 1 being [1..151], and whether the
values of the operands decide a comparison, [0..150] < 200 being true. That is the arithmetic on sets and the proofs
about them, and it is this module's: it is the one place that Inference reaches Feel.Analysis.Intervals,
Feel.Analysis.DateArithmetic, Feel.Analysis.MomentArithmetic, Feel.Analysis.MomentTests and
Feel.Analysis.MonthScaling through, and so is part of the seam that Feel.Analysis.Refinement is (D-133).
The functions take and give sets of numbers (Feel.Type.NumberSet): the numbers of a number, or the numbers that
stand for a date, a duration, a time and a date and time (Feel.Type.Image). They know nothing of kinds besides what
an operation itself needs (a date shifted by a duration of months and one shifted by a duration of seconds are not
the same arithmetic), and nothing of null, which is the second part of what most of them answer: whether the
operation can give null because of the values it is given, an overflow, a zero divisor, a year out of the calendar.
It is the caller that puts the sets into the alternatives of a type, and null into the union.
| Function | Of | Gives |
|---|---|---|
arithmetic/3 | two sets of numbers, or of the images of durations | the set of the result, and whether it can be null |
arithmetic_of_one/3 | one set of numbers, read twice as one value | the set of the result, and whether it can be null |
negate/1 | a set of numbers, or of the images of a duration | the set of the result |
divide_months/2 | the months of two durations | the numbers of the quotient, and whether it can be null |
divide_months_of_one/1 | the months of one duration, read twice as one value | the numbers of the quotient, and whether it can be null |
scale_months/3 | the months of a duration, and a number | the months of the product or the quotient |
seconds_between/2 | the days of two dates | the seconds between them |
shift_date/4 | the days of a date, and a duration | the days of the date moved, and whether it can be null |
shift_moment/5, moment_difference/4 | a time or a date and time, and a duration or another | the seconds, and whether it can be null |
decide/3, decide_moments/3 | two sets | whether the comparison is true for every pair, for none, or for some |
null_bounds/3 | two sets of numbers | which bounds on them would rule null out (D-161) |
They are functions of sets and need no tier: in :core the operands have no sets, and Inference does not ask for
the arithmetic on the whole range of two kinds more than once (D-133).
Summary
Types
The kinds of duration that a date, a time or a date and time can be moved by.
The numbers of a result, and whether it can be null because of the operation.
Functions
The numbers that left <operator> right can be, for the sets of numbers of the operands, and whether the result can
be null: an overflow past decimal128, a result too small to write, a division by zero, a power that has no value
(Feel.Analysis.Intervals, D-39).
The numbers that x <operator> x can be for one value x of the set that is read twice (D-170), and whether the result
can be null: x - x is 0, x / x is 1 unless x is 0, x * x is not below 0, and x + x is 2x.
Whether left <operator> right is true for every pair of numbers of the two sets (:always), for none (:never), or
for some (:unknown); the sets of numbers, and of the images of dates and durations, which are ordered as numbers are
(Feel.Analysis.Intervals).
The same for the sets of a time or a date and time, which are ordered by the clock or by the instant, as a pair of
them can differ in (Feel.Analysis.MomentTests, D-109).
The numbers that the quotient of two years and months durations can be, for the months of the dividend and of the
divisor, and whether it can be null. The run makes a number of the months of each, which it cannot for 10^34 months
and more, so those are cut and the result can be null for them (Feel.Analysis.MonthScaling).
The numbers that a years and months duration divided by itself can be, for its months, and whether it can be null
(D-170, D-207): the two operands are one value, so the quotient is 1 for a month that is not 0, as it is for a number,
and null for 0 and for the months that the run cannot make a number of, 10^34 and more
(Feel.Analysis.MonthScaling). A set with no month the run can use is no number, and null.
The seconds between two times, two dates and times, or a date and a date and time, to a second either way, and whether
the result can be null (one has a zone and the other has none, D-109). The kinds are those of the operands. It is
:error for a pair of kinds that has no difference (Feel.Analysis.MomentArithmetic).
The numbers that -operand can be. Negation cannot overflow, so there is no null to say.
Which bounds on the operands of left <operator> right would rule null out (D-161), for the sets of numbers of two
operands that cannot be null: :near_zero for operands at least 0.001 away from zero, :too_large for operands of
at most 1E+30, :range where the result needs both, and nil where it is not null, where it is certain (two single
numbers), or where these bounds do not rule it out. The operands are restricted as the hint says, and the result has no
null left. Feel.Analysis.Inference.null_bounds/3 is the one that takes types. With same: true the two sets are one
value read twice (D-170): x / x is null only for a zero, so the bounds that rule it out are those that keep x away
from zero, and a large x is no reason.
The months of a years and months duration times a number, or divided by one, for the months of a set and the numbers of
another, as the run rounds them (Feel.Analysis.MonthScaling, D-109), and whether the result can be null. It is
:error for a set that has no whole month.
The seconds between two dates, for the days of each: each day is 86,400 seconds.
The days that a date of the set of days plus (:add) or minus (:subtract) a duration can be, and whether the result
can be null (the year can leave the calendar). It is :error if either set has no value
(Feel.Analysis.DateArithmetic, D-109).
The seconds that a time or a date and time plus (:add) or minus (:subtract) a duration can be, and whether the
result can be null (Feel.Analysis.MomentArithmetic, D-109). It is :error if the duration has no value that the
move takes.
Types
@type duration_kind() :: :years_and_months_duration | :days_and_time_duration
The kinds of duration that a date, a time or a date and time can be moved by.
@type result() :: Feel.Analysis.Intervals.result()
The numbers of a result, and whether it can be null because of the operation.
Functions
@spec arithmetic( Feel.IR.arithmetic_operator(), Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t(), Feel.Analysis.Intervals.options() ) :: result()
The numbers that left <operator> right can be, for the sets of numbers of the operands, and whether the result can
be null: an overflow past decimal128, a result too small to write, a division by zero, a power that has no value
(Feel.Analysis.Intervals, D-39).
iex> alias Feel.Type.NumberSet
iex> to_150 = NumberSet.interval(Decimal.new(0), Decimal.new(150))
iex> {set, null?} = Feel.Analysis.Refinement.Operations.arithmetic(:add, to_150, NumberSet.point(Decimal.new(1)))
iex> {NumberSet.format(set), null?}
{"[1..151]", false}@spec arithmetic_of_one( :add | :subtract | :multiply | :divide, Feel.Type.NumberSet.t(), Feel.Analysis.Intervals.options() ) :: result()
The numbers that x <operator> x can be for one value x of the set that is read twice (D-170), and whether the result
can be null: x - x is 0, x / x is 1 unless x is 0, x * x is not below 0, and x + x is 2x.
iex> alias Feel.Type.NumberSet
iex> to_150 = NumberSet.interval(Decimal.new(0), Decimal.new(150))
iex> {set, null?} = Feel.Analysis.Refinement.Operations.arithmetic_of_one(:subtract, to_150)
iex> {NumberSet.format(set), null?}
{"0", false}@spec decide( Feel.IR.comparison_operator(), Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t() ) :: Feel.Analysis.Intervals.decision()
Whether left <operator> right is true for every pair of numbers of the two sets (:always), for none (:never), or
for some (:unknown); the sets of numbers, and of the images of dates and durations, which are ordered as numbers are
(Feel.Analysis.Intervals).
iex> alias Feel.Type.NumberSet
iex> to_150 = NumberSet.interval(Decimal.new(0), Decimal.new(150))
iex> Feel.Analysis.Refinement.Operations.decide(:lt, to_150, NumberSet.point(Decimal.new(200)))
:always@spec decide_moments( Feel.IR.comparison_operator(), Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t() ) :: Feel.Analysis.Intervals.decision()
The same for the sets of a time or a date and time, which are ordered by the clock or by the instant, as a pair of
them can differ in (Feel.Analysis.MomentTests, D-109).
@spec divide_months(Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t()) :: result()
The numbers that the quotient of two years and months durations can be, for the months of the dividend and of the
divisor, and whether it can be null. The run makes a number of the months of each, which it cannot for 10^34 months
and more, so those are cut and the result can be null for them (Feel.Analysis.MonthScaling).
@spec divide_months_of_one(Feel.Type.NumberSet.t()) :: result()
The numbers that a years and months duration divided by itself can be, for its months, and whether it can be null
(D-170, D-207): the two operands are one value, so the quotient is 1 for a month that is not 0, as it is for a number,
and null for 0 and for the months that the run cannot make a number of, 10^34 and more
(Feel.Analysis.MonthScaling). A set with no month the run can use is no number, and null.
iex> alias Feel.Type.NumberSet
iex> months = NumberSet.interval(Decimal.new(0), Decimal.new(14))
iex> {set, null?} = Feel.Analysis.Refinement.Operations.divide_months_of_one(months)
iex> {NumberSet.format(set), null?}
{"1", true}
iex> {set, null?} = Feel.Analysis.Refinement.Operations.divide_months_of_one(NumberSet.interval(Decimal.new(1), Decimal.new(14)))
iex> {NumberSet.format(set), null?}
{"1", false}
iex> {set, null?} = Feel.Analysis.Refinement.Operations.divide_months_of_one(NumberSet.point(Decimal.new("1E+34")))
iex> {set, null?}
{[], true}@spec moment_difference( atom(), Feel.Type.NumberSet.t(), atom(), Feel.Type.NumberSet.t() ) :: result() | :error
The seconds between two times, two dates and times, or a date and a date and time, to a second either way, and whether
the result can be null (one has a zone and the other has none, D-109). The kinds are those of the operands. It is
:error for a pair of kinds that has no difference (Feel.Analysis.MomentArithmetic).
@spec negate(Feel.Type.NumberSet.t()) :: Feel.Type.NumberSet.t()
The numbers that -operand can be. Negation cannot overflow, so there is no null to say.
iex> alias Feel.Type.NumberSet
iex> set = Feel.Analysis.Refinement.Operations.negate(NumberSet.interval(Decimal.new(1), Decimal.new(10)))
iex> NumberSet.format(set)
"[-10..-1]"@spec null_bounds( Feel.IR.arithmetic_operator(), Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t(), Feel.Analysis.Intervals.options() ) :: :near_zero | :too_large | :range | nil
Which bounds on the operands of left <operator> right would rule null out (D-161), for the sets of numbers of two
operands that cannot be null: :near_zero for operands at least 0.001 away from zero, :too_large for operands of
at most 1E+30, :range where the result needs both, and nil where it is not null, where it is certain (two single
numbers), or where these bounds do not rule it out. The operands are restricted as the hint says, and the result has no
null left. Feel.Analysis.Inference.null_bounds/3 is the one that takes types. With same: true the two sets are one
value read twice (D-170): x / x is null only for a zero, so the bounds that rule it out are those that keep x away
from zero, and a large x is no reason.
iex> alias Feel.Type.NumberSet
iex> to_150 = NumberSet.interval(Decimal.new(0), Decimal.new(150))
iex> Feel.Analysis.Refinement.Operations.null_bounds(:divide, to_150, NumberSet.point(Decimal.new(2)))
:near_zero
iex> Feel.Analysis.Refinement.Operations.null_bounds(:add, to_150, NumberSet.point(Decimal.new(2)))
nil@spec scale_months( :multiply | :divide, Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t() ) :: {:ok, result()} | :error
The months of a years and months duration times a number, or divided by one, for the months of a set and the numbers of
another, as the run rounds them (Feel.Analysis.MonthScaling, D-109), and whether the result can be null. It is
:error for a set that has no whole month.
@spec seconds_between(Feel.Type.NumberSet.t(), Feel.Type.NumberSet.t()) :: Feel.Type.NumberSet.t()
The seconds between two dates, for the days of each: each day is 86,400 seconds.
iex> alias Feel.Type.NumberSet
iex> later = NumberSet.point(Decimal.new(10))
iex> earlier = NumberSet.point(Decimal.new(8))
iex> NumberSet.format(Feel.Analysis.Refinement.Operations.seconds_between(later, earlier))
"172800"@spec shift_date( Feel.Type.NumberSet.t(), duration_kind(), Feel.Type.NumberSet.t(), :add | :subtract ) :: result() | :error
The days that a date of the set of days plus (:add) or minus (:subtract) a duration can be, and whether the result
can be null (the year can leave the calendar). It is :error if either set has no value
(Feel.Analysis.DateArithmetic, D-109).
@spec shift_moment( :time | :date_and_time, Feel.Type.NumberSet.t(), duration_kind(), Feel.Type.NumberSet.t(), :add | :subtract ) :: result() | :error
The seconds that a time or a date and time plus (:add) or minus (:subtract) a duration can be, and whether the
result can be null (Feel.Analysis.MomentArithmetic, D-109). It is :error if the duration has no value that the
move takes.