Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.
New syntax using x ← e to bind values on the left-hand-side of a function clause.
Instance search is more performant thanks to a new indexing structure.
Additionally, users can now control how instances should be selected
in the case multiple candidates exist.
User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
are now on by default.
Agda versioning scheme switches to the Haskell Package Versioning Policy
so Agda can be more reliably used as a library.
Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...
Agda supports GHC versions 8.6.5 to 9.10.1.
[Breaking] The option --overlapping-instances, which allows
backtracking during instance search, has been renamed to--backtracking-instance-search.
These options are now on by default:
--exact-split: Warn about clauses that are not definitional equalities.--keep-pattern-variables: Do not introduce dot patterns in interactive splitting.--postfix-projections: Print projections and projection patterns in postfix.--save-metas: Try to not unfold metavariable solutions in interface files.To revert to the old behavior, use options --no-....
The following options are now considered infective:
(Issue #5264)
--allow-exec--cumulativity--experimental-irrelevance--injective-type-constructors--omega-in-omega--rewriting--type-in-typeThis means that if a module has one of these flags enabled,
then all modules importing it must also have that flag enabled.
New warnings:
CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
Used to be a hard error; now Agda continues, ignoring eta-equality.
ConflictingPragmaOptions if giving both --this and --that
when --this implies --no-that (and analogous for --no-this implies--that, etc).
ConstructorDoesNotFitInData when a constructor parameter
is too big (in the sense of universe level) for the target data type of the constructor.
Error warning, used to be a hard error.
DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
or declared inductive twice.
UselessMacro when a macro block does not contain any function definitions.
WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
Used to be a hard error.
Rejected rewrite rules no longer cause a hard error but instead cause
an error warning. The following warnings were added to document the
various reasons for rejection:
RewriteLHSNotDefinitionOrConstructorRewriteVariablesNotBoundByLHSRewriteVariablesBoundMoreThanOnceRewriteLHSReducesRewriteHeadSymbolIsProjectionRewriteHeadSymbolIsProjectionLikeFunctionRewriteHeadSymbolIsTypeConstructorRewriteHeadSymbolContainsMetasRewriteConstructorParametersNotGeneralRewriteContainsUnsolvedMetaVariablesRewriteBlockedOnProblemsRewriteRequiresDefinitionsRewriteDoesNotTargetRewriteRelationRewriteBeforeFunctionDefinitionRewriteBeforeMutualFunctionDefinitionNew option --require-unique-meta-solutions
(turned on by default).
Disabling it with --no-require-unique-meta-solutions allows the type checker
to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
The --lossy-unification flag implies --no-require-unique-meta-solutions.
New pragma INJECTIVE_FOR_INFERENCE
which treats functions as injective for inferring implicit arguments if--no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
file where the function is used, and not necessarily in the file where it is defined.
For example:
postulate
reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})
does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.
Additions to the Agda syntax.
Left-hand side let:using x ← e
(PR #7078)
This new construct can be use in left-hand sides together with with andrewrite to give names to subexpressions. It is the left-hand side
counterpart of a let-binding and supports the same limited form of pattern
matching on eta-expandable record values.
It can be quite useful when you have a function doing a series of nestedwiths that share some expressions. Something like
fun : A → B fun x using z ← e with foo z ... | p with bar z ... | q = r
Here the expression e doesn't have to be repeated in the two with-expressions.
As in a with, multiple bindings can be separated by a |, and variables to
the left are in scope in bindings to the right.
Pattern synonyms can now expose existing instance arguments
(PR 7173).
Example:
data D : Set where
c : {{D}} → D
pattern p {{d}} = c {{d}}
This allows us to explicitly bind these argument in a pattern match
and supply them explicitly when using the pattern synonym in an expression.
f : D → D
f (p {{d = x}}) = p {{d = x}}
We cannot create new instance arguments this way, though.
The following is rejected:
data D : Set where
c : D → D
pattern p {{d}} = c dChanges to type checker and other components defining the Agda language.
Agda now uses discrimination trees to store and look up instance
definitions, rather than linearly searching through all instances for
a given "class" (PR #7109).
This is a purely internal change, and should not result in any change
to which programs are accepted or rejected. However, it significantly
improves the performance of instance search, especially for the case
of a "type class" indexed by a single type argument. The new lookup
procedure should never be slower than the previous implementation.
Changes to the meta-programming facilities.
[Breaking] Erased constructors are now supported in reflection machinery.
Quantity argument was added to data-cons. For erased constructors this
argument has a value of quantity-0, otherwise it's quantity-ω.defineData now requires setting quantity for each constructor.
Add new primitive to run instance search from reflection code:
-- Try to solve open instance constraints. When wrapped in `noConstraints`, -- fails if there are unsolved instance constraints left over that originate -- from the current macro invokation. Outside constraints are still attempted, -- but failure to solve them are ignored by `noConstraints`. solveInstanceConstraints : TC ⊤
A new reflection primitive workOnTypes : TC A → TC A was added toAgda.Builtin.Reflection. This runs the given computation at the type level,
which enables the use of erased things. In particular, this is needed when
working with (dependent) function types with erased arguments. For example,
one can get the type of the tuple constructor _,_ (which now takes its type
parameters as erased arguments, see above) and unify it with the current goal
as follows:
macro testM : Term → TC ⊤ testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t)) typeOfComma = testM
[Breaking] The Auto command
Agsy has been replaced by an entirely new implementation Mimer
(PR #6410).
This fixes problems where Auto would fail in the presence of language features
it did not know about, such as copatterns or anything cubical.
The reimplementation does not support case splitting (-c), disproving
(-d) or refining (-r).
The Agda input method for Emacs has been extended by several character bindings.
The list of changes can be obtained with a git diff on the sources:
git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el
Highlighting some changes to Agda as a library.
New module Agda.Syntax.Common.KeywordRange providing type KwRange isomorphic to Range
to indicate source positions that just span keywords (PR #7162).
The motivation for KwRange is to distinguish such ranges from ranges for whole subtrees,
e.g. in data type Agda.Syntax.Concrete.Declaration.
API:
module Agda.Syntax.Common.KeywordRange where type KwRange -- From Range to KwRange kwRange :: HasRange a => a -> KwRange -- From KwRange to Range instance HasRange KwRange where getRange :: KwRange -> Range
New hook in Agda.Compiler.ToTreeless to enable custom pipelines in compiler backends
(PR #7273).
For 2.7.0, the following issues were
closed
(see bug tracker):
@tactic does not kick in for lambdasGenericWarningwith...in... instead of old-school inspect--exact-split and --postfix-projections default?private blocksgetDefinition gives wrong constructor for record from applied parameterised moduleshow does not respect abstract/opaque when normalising a term in a holeModuleDoesntExport has imprecise deadcode highlightinginstance definition with unsolved type--postfix-projections do not make use of mixfix syntaxThese (relevant) pull requests were merged for 2.7.0:
unquote applicationsINJECTIVE_FOR_INFERENCE pragmalet__IMPOSSIBLE__ for nullary syntaxConstructorDoesNotFitInData instead of hard error.workOnTypes reflection primitivematchPatternexecutable-dynamic)--keep-pattern-variables the default--termination-depth in user manualglue1 bindings by @ncfavier in #7021user-manual to stdlib-v2.0 by @jamesmckinna in #7043flake.nix by @lawcho in #7032defBlocked as neverUnblock by @andreasabel in #7046cancel-workflow-action by @L-TChen in #7074.agda-lib for Agda builtins by @ibbem in #6988let by @UlfNorell in #7078instantiateFull before with-abstraction. by @andreasabel in #7151__IMPOSSIBLE__ for nullary syntax by @andreasabel in #7160unquote applications by @ncfavier in #6570INJECTIVE_FOR_INFERENCE pragma by @WhatisRT in #6640SmallSet for funFlags, make more boolean fields a FunctionFlag by @andreasabel in #7244ConstructorDoesNotFitInData instead of hard error. by @andreasabel in #7292workOnTypes reflection primitive by @jespercockx in #7310RecordData instead of Defn from isRecord by @andreasabel in #7348executable-dynamic) by @andreasabel in #7353--keep-pattern-variables the default by @andreasabel in #7355matchPattern by @jespercockx in #7347--termination-depth in user manual by @andreasabel in #7358isRecord etc. to return RecordData instead of Defn. by @andreasabel in #6843Full Changelog: v2.6.4.3...v2.6.20240714
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4