The seam between the analysis of an expression and the proofs about the values it can have (D-133).
The analyzer gives every node a type, and a type can be exact to the value: a union that says
number in [1..151], "a" | "b", true, a date in a range (Feel.Type.Union, D-39, D-109). That is refinement.
What an expression is typed as, without it, is the kind of each value and whether it can be null: number,
string, a list of numbers, a context with these entries. Both tiers aim to contain returned values under the
declarations' assumptions; a refined bound can contain fewer possible values than its kind-only approximation.
This is bounded analysis, not a claim of exact sets or general soundness. The required execution contract is the
same value and diagnostics whichever tier was used; it
is the types, the warnings of prepare/2, and what the optimizer can take out because the types prove it, that
differ (Feel.Optimizer).
The refinement is close to half of the analysis in size (Feel.Analysis.Narrowing and the modules under it, which work
out the sets of numbers, dates and durations that an operation, a comparison or a condition leaves: 6,400 of the 13,800
lines of analysis/, and the parts of Paths and AllowedValues that work on sets besides), it is where a
mistake is not seen (an unsound fact lets the optimizer remove a check that was needed), and it is where prepare/2
spends its time on a source that is built to make it. So it is a tier of its own, and the analyzer reaches it only here:
| Tier | What the analysis gives |
|---|---|
:full | refined possible-value bounds and condition facts, subject to representation budgets (the default) |
:core | the types of the kinds: no set of values, and no fact from a condition; null is tracked as it is in :full |
prepare(source, analysis: :core) chooses the tier, and the executable keeps nothing of it, so a run does not know.
Function literals have the same observable signature in either tier (D-219): it comes from kind-only
analysis of their written environment, before condition facts, call specialization or optimization.
Full analysis makes that additional bounded pass only when the syntax contains functions. Body call
refinements remain available separately. Preparation warnings can use tier-specific inferred types;
runtime call diagnostics are built from actual argument values.
What is in the seam
The analyzer calls these and no module under them:
facts/3, which is what a condition says of its names in a branch: nothing in:core.constant_type/2, the type of a value that is known: its kind in:core.settle/2, which is called on what the analyzer gives for each node, and in:coretakes the sets out of its type, so that a set that some part of the analysis made (a built-in function's result, a property of a date, the elements of1..3) goes no further than the node.- the functions that apply facts to types and combine them (
narrow/2,meet/2,combine/4and the rest), which areFeel.Analysis.Narrowing's and are the same in both tiers, since there are no facts in:coreto apply. restrict/2andrestrict_elements/2, which narrow a type by the allowed values of a name (Feel.Analysis.TestSets), used only where the allowed values narrow (:declarations, D-138), which they do not in:core; andcertain/2, the subset that goes withrestrict/2, whichFeel.Rulesasks for the entries of a table (D-158).Feel.Analysis.Refinement.Operations, which is what the operators do to sets of values (D-133): the set of the result of an operation, and whether the sets of two operands decide a comparison (Feel.Analysis.Intervals,Feel.Analysis.DateArithmetic,Feel.Analysis.MomentArithmetic,Feel.Analysis.MomentTestsandFeel.Analysis.MonthScaling).Feel.Analysis.Inferencetypes the kinds of an operation and whether it can benull, and asksOperationsfor the sets. It is a function of types, so it needs no tier: given the types of:core, which have no sets, it answers with the kinds (Inferencedoes not start the arithmetic of sets for two operands that have none).
Two places outside the seam call the modules that work with sets, and are not behind it: Feel.Analysis.Paths (the
properties of a date, a duration, a time and a date and time from their sets) and Feel.Analysis.AllowedValues (the
tests of a name's allowed values as sets). They are functions of types, so they need no tier, and given the types of
:core they answer with the kinds. test/feel/analysis/refinement_test.exs keeps the list: a new caller of a module
of the refinement fails it until it is added here or goes through the seam.
Summary
Types
Facts and the kinds of subject they are about (Feel.Analysis.Narrowing).
:full refines possible-value bounds; :core keeps kind-only bounds. Both are bounded analyses.
Functions
The values of a type that the unary tests certainly accept (Feel.Analysis.TestSets.certain/2): the subset that goes with the
superset of restrict/2. Feel.Rules asks both (D-158).
The type of a value that is known (Feel.Type.Union.of_value/1): in :core it is the type of the kind, so 1 is number
and not number = 1.
Whether the tier carries value sets and condition facts. The historical name exact? selects refinement;
it does not promise exact set denotations. false in :core, where
there is nothing to make the facts of the operands of an and or an or for, and where the hints that tighter
allowed values would rule null out (Feel.Analysis.Inference.null_bounds/3) are not made.
What the condition says of the names it reads, in a branch (Feel.Analysis.Narrowing.facts/2). In :core it says nothing.
origins says what the locals that the condition reads are bound to, if they are bound to conditions
(Feel.Analysis.Narrowing.facts/3).
What a name that is bound to the value of the node says when it is read as a condition: the node, if it is one (a
comparison, and, not(…), a name) and nothing else. memo is a key of the process that the facts of the node are
kept under, which forget/1 takes away. In :core nothing.
A type with fun applied to what is at the end of some steps down into it: the entry of a context by its key, the
elements of a list by :each (the constraints of a member, D-161). Only the plain alternatives that have the member are
changed, and the rest are as they were, which is wider and so sound.
What the analyzer gave for a node, settled for the tier. In :core the type of the node has no set of values.
An error, or anything that is not a node with its information, is as it was.
The tiers, the default first.
Checks the tier an option names, and returns it. nil is :full.
Types
@type profiled() :: Feel.Analysis.Narrowing.profiled()
Facts and the kinds of subject they are about (Feel.Analysis.Narrowing).
@type tier() :: :full | :core
:full refines possible-value bounds; :core keeps kind-only bounds. Both are bounded analyses.
Functions
@spec certain(Feel.Type.Union.t(), Feel.IR.t()) :: Feel.Type.Union.t() | []
The values of a type that the unary tests certainly accept (Feel.Analysis.TestSets.certain/2): the subset that goes with the
superset of restrict/2. Feel.Rules asks both (D-158).
@spec constant_type(tier(), Feel.Value.t()) :: Feel.Type.Union.t()
The type of a value that is known (Feel.Type.Union.of_value/1): in :core it is the type of the kind, so 1 is number
and not number = 1.
iex> Feel.Type.Union.format(Feel.Analysis.Refinement.constant_type(:full, Decimal.new(1)))
"number = 1"
iex> Feel.Type.Union.format(Feel.Analysis.Refinement.constant_type(:core, Decimal.new(1)))
"number"Whether the tier carries value sets and condition facts. The historical name exact? selects refinement;
it does not promise exact set denotations. false in :core, where
there is nothing to make the facts of the operands of an and or an or for, and where the hints that tighter
allowed values would rule null out (Feel.Analysis.Inference.null_bounds/3) are not made.
iex> {Feel.Analysis.Refinement.exact?(:full), Feel.Analysis.Refinement.exact?(:core)}
{true, false}@spec facts( tier(), Feel.IR.t(), Feel.Analysis.Narrowing.branch(), Feel.Analysis.Narrowing.origins() | nil ) :: Feel.Analysis.Narrowing.facts()
What the condition says of the names it reads, in a branch (Feel.Analysis.Narrowing.facts/2). In :core it says nothing.
origins says what the locals that the condition reads are bound to, if they are bound to conditions
(Feel.Analysis.Narrowing.facts/3).
iex> {:ok, ast} = Feel.parse("x > 5")
iex> {:ok, %{ir: condition}} = Feel.Analysis.Analyzer.analyze(ast, [])
iex> Map.keys(Feel.Analysis.Refinement.facts(:full, condition, :then))
["x"]
iex> Feel.Analysis.Refinement.facts(:core, condition, :then)
%{}@spec operation_subjects(Feel.IR.t(), Feel.Analysis.Narrowing.origins() | nil) :: MapSet.t(Feel.Analysis.Narrowing.subject())
@spec origin_of(tier(), Feel.IR.t(), Feel.Analysis.Narrowing.memo_key()) :: Feel.Analysis.Narrowing.origin() | nil
What a name that is bound to the value of the node says when it is read as a condition: the node, if it is one (a
comparison, and, not(…), a name) and nothing else. memo is a key of the process that the facts of the node are
kept under, which forget/1 takes away. In :core nothing.
iex> {:ok, ast} = Feel.parse("x > 5")
iex> {:ok, %{ir: condition}} = Feel.Analysis.Analyzer.analyze(ast, [])
iex> match?({:node, _, nil}, Feel.Analysis.Refinement.origin_of(:full, condition, nil))
true
iex> Feel.Analysis.Refinement.origin_of(:core, condition, nil)
nil@spec restrict_at(Feel.Type.Union.t(), [Feel.Scope.step()], (Feel.Type.Union.t() -> Feel.Type.Union.t())) :: Feel.Type.Union.t()
A type with fun applied to what is at the end of some steps down into it: the entry of a context by its key, the
elements of a list by :each (the constraints of a member, D-161). Only the plain alternatives that have the member are
changed, and the rest are as they were, which is wider and so sound.
iex> person = [{:context, %{"age" => [:number, :null], "name" => [:string, :null]}}, :null]
iex> restricted = Feel.Analysis.Refinement.restrict_at(person, ["age"], fn _age -> [:string] end)
iex> Feel.Type.Union.format(restricted)
"context<age: string, name: string | Null> | Null"
iex> orders = [{:list, [{:context, %{"total" => [:number, :null]}}, :null]}, :null]
iex> Feel.Type.Union.format(Feel.Analysis.Refinement.restrict_at(orders, [:each, "total"], fn _total -> [:string] end))
"list<context<total: string> | Null> | Null"
iex> non_empty = Feel.Type.Union.non_empty({:list, [{:context, %{"total" => [:number]}}]})
iex> Feel.Type.Union.format(Feel.Analysis.Refinement.restrict_at(non_empty, [:each, "total"], fn _total -> [:string] end))
"non-empty list<context<total: string>>"What the analyzer gave for a node, settled for the tier. In :core the type of the node has no set of values.
An error, or anything that is not a node with its information, is as it was.
iex> node = {:const, %{span: {0, 1}, type: Feel.Type.Union.of_value(true)}, true}
iex> {:ok, settled, :info} = Feel.Analysis.Refinement.settle(:core, {:ok, node, :info})
iex> Feel.IR.type(settled)
[:boolean]
iex> Feel.Analysis.Refinement.settle(:full, {:ok, node, :info}) == {:ok, node, :info}
true@spec tiers() :: [tier(), ...]
The tiers, the default first.
Checks the tier an option names, and returns it. nil is :full.
Raises ArgumentError for any other.
iex> Feel.Analysis.Refinement.validate!(nil)
:full
iex> Feel.Analysis.Refinement.validate!(:core)
:core