# `Feel.Analysis.Refinement` [🔗](https://github.com/FeeJai/BDM/blob/feel-v0.1.0/apps/feel/lib/feel/analysis/refinement.ex#L1) 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 `:core` takes 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 of `1..3`) goes no further than the node. * the functions that apply facts to types and combine them (`narrow/2`, `meet/2`, `combine/4` and the rest), which are `Feel.Analysis.Narrowing`'s and are the same in both tiers, since there are no facts in `:core` to apply. * `restrict/2` and `restrict_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`; and `certain/2`, the subset that goes with `restrict/2`, which `Feel.Rules` asks 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.MomentTests` and `Feel.Analysis.MonthScaling`). `Feel.Analysis.Inference` types the kinds of an operation and whether it can be `null`, and asks `Operations` for 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 (`Inference` does 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. # `profiled` ```elixir @type profiled() :: Feel.Analysis.Narrowing.profiled() ``` Facts and the kinds of subject they are about (`Feel.Analysis.Narrowing`). # `tier` ```elixir @type tier() :: :full | :core ``` `:full` refines possible-value bounds; `:core` keeps kind-only bounds. Both are bounded analyses. # `call_subjects` # `certain` ```elixir @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). # `chain_facts` # `combine` # `combine` # `constant_type` ```elixir @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" # `exact?` ```elixir @spec exact?(tier()) :: boolean() ``` 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} # `facts` ```elixir @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) %{} # `forget` # `item_subject` # `kinds` # `meet` # `narrow` # `narrow_sources` # `narrow_sources` # `narrowed` # `operation_subjects` # `operation_subjects` ```elixir @spec operation_subjects(Feel.IR.t(), Feel.Analysis.Narrowing.origins() | nil) :: MapSet.t(Feel.Analysis.Narrowing.subject()) ``` # `origin_of` ```elixir @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 # `path_reads` # `path_reads` # `path_sources` # `path_sources` # `profile` # `reads_a_fact?` # `restrict` # `restrict_at` ```elixir @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 | 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 | 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>" # `restrict_elements` # `settle` ```elixir @spec settle(tier(), result) :: result when result: {:ok, Feel.IR.t(), term()} | {:error, term()} ``` 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 # `tiers` ```elixir @spec tiers() :: [tier(), ...] ``` The tiers, the default first. # `union_kinds` # `validate!` ```elixir @spec validate!(term()) :: tier() ``` 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 --- *Consult [api-reference.md](api-reference.md) for complete listing*