commits
With the definition of a choice of atom now admitting a homogeneous
representation, we no longer need to make assumptions about the order
arguments are applied to CombineAtom in StringAxiomSet, so can make it a
functor.
This significantly tidies the representation of a choice of atom
by folding the previous `Left, Right, and Foreign` constructors into
a single `anyValue`.
Before, we had this ATOM/COERCIBLE_ATOM split to solve circular
references, where COERCIBLE_ATOM was a thin wrapper around ATOM to
introduce coercions. The idea was that one might want to opt-out
entirely from the coercion system and which requires having a complete ATOM
definition without any of the extra stuff that coercions introduce. In
practice, that idea was already very leaky, with hard-coded requirements
that atoms be coercible already in place that would be hard to remove.
And besides, one can always opt out of coercions on their own types by
declaring `coerce = _ => None`, and on some predefined type by writing a
wrapper with such a definition.
This change flips the previous architecture so that the full ATOM
signature includes coercions and a thin BASE_ATOM module which includes a type definition,
a tag, and a way to wrap a value into an `anyValue`
(also, I renamed `hValue` to `anyValue` for clarity).
This should be the last substantial change to the signature of ATOM.
Note that a spindle instance has to be chosen before pipelines are run
in the repo settings.
This doesn't port over the testing across multiple node versions that
github had. The easiest way to do that as far as I can see would be
having two workflows, each pulling in a separate `nodejs<ver>` package
from nixpkgs. Maybe I'm missing something in the docs
(https://docs.tangled.org/spindles.html#pipelines), though?
For now, I think it's fine to test on a single version of node anyway.
Implement parsing library
Combine and coerce atoms generically
Tidy ATOM signature and substitution semantics
Add option for strings to appear in structured judgments
Add fact locality to method context for useful elimination suggestions
Add ghost term to filter for useful introduction rules
Add mutual induction for string terms
Before, we had this ATOM/COERCIBLE_ATOM split to solve circular
references, where COERCIBLE_ATOM was a thin wrapper around ATOM to
introduce coercions. The idea was that one might want to opt-out
entirely from the coercion system and which requires having a complete ATOM
definition without any of the extra stuff that coercions introduce. In
practice, that idea was already very leaky, with hard-coded requirements
that atoms be coercible already in place that would be hard to remove.
And besides, one can always opt out of coercions on their own types by
declaring `coerce = _ => None`, and on some predefined type by writing a
wrapper with such a definition.
This change flips the previous architecture so that the full ATOM
signature includes coercions and a thin BASE_ATOM module which includes a type definition,
a tag, and a way to wrap a value into an `anyValue`
(also, I renamed `hValue` to `anyValue` for clarity).
This should be the last substantial change to the signature of ATOM.
Note that a spindle instance has to be chosen before pipelines are run
in the repo settings.
This doesn't port over the testing across multiple node versions that
github had. The easiest way to do that as far as I can see would be
having two workflows, each pulling in a separate `nodejs<ver>` package
from nixpkgs. Maybe I'm missing something in the docs
(https://docs.tangled.org/spindles.html#pipelines), though?
For now, I think it's fine to test on a single version of node anyway.