Subject: ANNOUNCE: Agda 2.2.10 Newsgroups: gmane.comp.lang.agda Date: Sunday 20th February 2011 18:23:52 UTC (over 5 years ago) Hi, Agda 2.2.10 has now been released. Important changes since 2.2.8: Language -------- * New flag: --without-K. This flag makes pattern matching more restricted. If the flag is activated, then Agda only accepts certain case-splits. If the type of the variable to be split is D pars ixs, where D is a data (or record) type, pars stands for the parameters, and ixs the indices, then the following requirements must be satisfied: * The indices ixs must be applications of constructors to distinct variables. * These variables must not be free in pars. The intended purpose of --without-K is to enable experiments with a propositional equality without the K rule. Let us define propositional equality as follows: data _≡_ {A : Set} : A → A → Set where refl : ∀ x → x ≡ x Then the obvious implementation of the J rule is accepted: J : {A : Set} (P : {x y : A} → x ≡ y → Set) → (∀ x → P (refl x)) → ∀ {x y} (x≡y : x ≡ y) → P x≡y J P p (refl x) = p x The same applies to Christine Paulin-Mohring's version of the J rule: J′ : {A : Set} {x : A} (P : {y : A} → x ≡ y → Set) → P (refl x) → ∀ {y} (x≡y : x ≡ y) → P x≡y J′ P p (refl x) = p On the other hand, the obvious implementation of the K rule is not accepted: K : {A : Set} (P : {x : A} → x ≡ x → Set) → (∀ x → P (refl x)) → ∀ {x} (x≡x : x ≡ x) → P x≡x K P p (refl x) = p x However, we have /not/ proved that activation of --without-K ensures that the K rule cannot be proved in some other way. * Irrelevant declarations. Postulates and functions can be marked as irrelevant by prefixing the name with a dot when the name is declared. Example: postulate .irrelevant : {A : Set} → .A → A Irrelevant names may only be used in irrelevant positions or in definitions of things which have been declared irrelevant. The axiom irrelevant above can be used to define a projection from an irrelevant record field: data Subset (A : Set) (P : A → Set) : Set where _#_ : (a : A) → .(P a) → Subset A P elem : ∀ {A P} → Subset A P → A elem (a # p) = a .certificate : ∀ {A P} (x : Subset A P) → P (elem x) certificate (a # p) = irrelevant p The right-hand side of certificate is relevant, so we cannot define certificate (a # p) = p (because p is irrelevant). However, certificate is declared to be irrelevant, so it can use the axiom irrelevant. Furthermore the first argument of the axiom is irrelevant, which means that irrelevant p is well-formed. As shown above the axiom irrelevant justifies irrelevant projections. Previously no projections were generated for irrelevant record fields, such as the field certificate in the following record type: record Subset (A : Set) (P : A → Set) : Set where constructor _#_ field elem : A .certificate : P elem Now projections are generated automatically for irrelevant fields (unless the flag --no-irrelevant-projections is used). Note that irrelevant projections are highly experimental. * Termination checker recognises projections. Projections now preserve sizes, both in patterns and expressions. Example: record Wrap (A : Set) : Set where constructor wrap field unwrap : A open Wrap public data WNat : Set where zero : WNat suc : Wrap WNat → WNat id : WNat → WNat id zero = zero id (suc w) = suc (wrap (id (unwrap w))) In the structural ordering unwrap w ≤ w. This means that unwrap w ≤ w < suc w, and hence the recursive call to id is accepted. Projections also preserve guardedness. Tools ----- * Hyperlinks for top-level module names now point to the start of the module rather than to the declaration of the module name. This applies both to the Emacs mode and to the output of agda --html. * Most occurrences of record field names are now highlighted as "fields". Previously many occurrences were highlighted as "functions". * Emacs mode: It is no longer possible to change the behaviour of the TAB key by customising agda2-indentation. * Epic compiler backend. A new compiler backend is being implemented. This backend makes use of Edwin Brady's language Epic (http://www.cs.st-andrews.ac.uk/~eb/epic.php) and its compiler. The backend should handle most Agda code, but is still at an experimental stage: more testing is needed, and some things written below may not be entirely true. The Epic compiler can be invoked from the command line using the flag --epic: agda --epic --epic-flag= |
|||