See the official user manual for the most up-to-date version of the information on this page.
Index of options
The table below summarize the options available in Agda 2.3.2.1. You can also use agda --help for the latest list. We only list those options that can be given in .agda files in the {-# OPTIONS ... #-} form.
Option | Effect | More information |
---|---|---|
--show-implicit | Show implicit arguments when printing | |
--show-irrelevant | Enables printing of irrelevant terms (which by default are printed as _) | 2.3.2 notes |
--no-universe-polymorphism | Disables universe polymorphism | 2.3.0 notes |
--safe | Disables postulates, unsafe OPTION pragmas (e.g. --type-in-type ) and primTrustMe | 2.3.0 notes |
--allow-unsolved-metas | Enables importing of modules with unsolved metavariables | |
--experimental-irrelevance | Enables potentially unsound irrelevance features (irrelevant levels, irrelevant data matching) | |
--no-irrelevant-projections | Disables the automatic generation of projections for irrelevant fields | 2.2.10 notes |
--guardedness-preserving-type-construtors | Enables the treatment of type constructors as inductive constructors during productivity checking | 2.2.8 notes |
--injective-type-constructors | Enables automatic injectivity of type constructors (makes Agda non-classical, see notes) | 2.2.8 notes |
--no-coverage-check | Disables the case coverage checker for functions | |
--no-positivity-check | Disables the strict-positivity check on data type constructors | |
--no-termination-check | Disables the termination checker (globally, see pragma above to disable termination checking of individual definitions) | |
--termination-depth=N | Enables counting in the termination checker (N >= 1) | See below; also 2.2.8 notes |
--sized-types | Enables definitions using sized types | |
--type-in-type | Disables universe level checking during typechecking (makes Agda inconsistent: Girard's paradox) |
OPTIONS
{-# OPTIONS -opt1 --opt2 ... #-}
Passes command-line options to Agda.
Injective type constructors off by default.
Automatic injectivity of type constructors has been disabled (by default). To enable it, use the flag --injective-type-constructors, either on the command line or in an OPTIONS pragma. Note that this flag makes Agda anti-classical and possibly inconsistent: Agda with excluded middle is inconsistent http://thread.gmane.org/gmane.comp.lang.agda/1367 See test/succeed/InjectiveTypeConstructors.agda for an example.
Termination checker can count.
There is a new flag --termination-depth=N accepting values N >= 1 (with N = 1 being the default) which influences the behavior of the termination checker. So far, the termination checker has only distinguished three cases when comparing the argument of a recursive call with the formal parameter of the callee.
< : the argument is structurally smaller than the parameter = : they are equal ? : the argument is bigger or unrelated to the parameter
This behavior, which is still the default (N = 1), will not recognise the following functions as terminating.
mutual f : ℕ → ℕ f zero = zero f (suc zero) = zero f (suc (suc n)) = aux n aux : ℕ → ℕ aux m = f (suc m)
The call graph
f --(<)--> aux --(?)--> f
yields a recursive call from f to f via aux where the relation of call argument to callee parameter is computed as "unrelated" (composition of < and ?).
Setting N >= 2 allows a finer analysis: n has two constructors less than suc (suc n), and suc m has one more than m, so we get the call graph:
f --(-2)--> aux --(+1)--> f
The indirect call f --> f is now labeled with (-1), and the termination checker can recognise that the call argument is decreasing on this path.
Setting the termination depth to N means that the termination checker counts decrease up to N and increase up to N-1. The default, N=1, means that no increase is counted, every increase turns to "unrelated".
In practice, examples like the one above sometimes arise when "with" is used. As an example, the program
f : ℕ → ℕ f zero = zero f (suc zero) = zero f (suc (suc n)) with zero ... | _ = f (suc n)
is internally represented as
mutual f : ℕ → ℕ f zero = zero f (suc zero) = zero f (suc (suc n)) = aux n zero aux : ℕ → ℕ → ℕ aux m k = f (suc m)
Thus, by default, the definition of f using "with" is not accepted by the termination checker, even though it looks structural (suc n is a subterm of suc suc n). Now, the termination checker is satisfied if the option "--termination-depth=2" is used.
Caveats:
- This is an experimental feature, hopefully being replaced by
something smarter in the near future.
- Increasing the termination depth will quickly lead to very long
termination checking times. So, use with care. Setting termination depth to 100 by habit, just to be on the safe side, is not a good idea!
- Increasing termination depth only makes sense for linear data
types such as ℕ and Size. For other types, increase cannot be recognised. For instance, consider a similar example with lists. data List : Set where nil : List cons : ℕ → List → List mutual f : List → List f nil = nil f (cons x nil) = nil f (cons x (cons y ys)) = aux y ys aux : ℕ → List → List aux z zs = f (cons z zs) Here the termination checker compares cons z zs to z and also to zs. In both cases, the result will be "unrelated", no matter how high we set the termination depth. This is because when comparing cons z zs to zs, for instance, z is unrelated to zs, thus, cons z zs is also unrelated to zs. We cannot say it is just "one larger" since z could be a very large term. Note that this points to a weakness of untyped termination checking. To regain the benefit of increased termination depth, we need to index our lists by a linear type such as ℕ or Size. With termination depth 2, the above example is accepted for vectors instead of lists.
The codata keyword has been removed. To use coinduction, use the following new builtins: INFINITY, SHARP and FLAT. Example:
# OPTIONS --universe-polymorphism #module Coinduction where open import Level infix 1000 ♯_ postulate ∞ : ∀ {a} (A : Set a) → Set a ♯_ : ∀ {a} {A : Set a} → A → ∞ A ♭ : ∀ {a} {A : Set a} → ∞ A → A# BUILTIN INFINITY ∞ ## BUILTIN SHARP ♯_ ## BUILTIN FLAT ♭ #
Note that (non-dependent) pattern matching on SHARP is no longer allowed.
Note also that strange things might happen if you try to combine the pragmas above with COMPILED_TYPE, COMPILED_DATA or COMPILED pragmas, or if the pragmas do not occur right after the postulates.
The compiler compiles the INFINITY builtin to nothing (more or less), so that the use of coinduction does not get in the way of FFI declarations:
data Colist (A : Set) : Set where [] : Colist A _∷_ : (x : A) (xs : ∞ (Colist A)) → Colist A# COMPILED_DATA Colist [] [] (:) #
Infinite types.
If the new flag --guardedness-preserving-type-constructors is used, then type constructors are treated as inductive constructors when we check productivity (but only in parameters, and only if they are used strictly positively or not at all). This makes examples such as the following possible:
data Rec (A : ∞ Set) : Set where fold : ♭ A → Rec A -- Σ cannot be a record type below. data Σ (A : Set) (B : A → Set) : Set where _,_ : (x : A) → B x → Σ A B syntax Σ A (λ x → B) = Σ[ x ∶ A ] B -- Corecursive definition of the W-type. W : (A : Set) → (A → Set) → Set W A B = Rec (♯ (Σ[ x ∶ A ] (B x → W A B))) syntax W A (λ x → B) = W[ x ∶ A ] B sup : {A : Set} {B : A → Set} (x : A) (f : B x → W A B) → W A B sup x f = fold (x , f) W-rec : {A : Set} {B : A → Set} (P : W A B → Set) → (∀ {x} {f : B x → W A B} → (∀ y → P (f y)) → P (sup x f)) → ∀ x → P x W-rec P h (fold (x , f)) = h (λ y → W-rec P h (f y)) -- Induction-recursion encoded as corecursion-recursion. data Label : Set where ′0 ′1 ′2 ′σ ′π ′w : Label mutual U : Set U = Σ Label U′ U′ : Label → Set U′ ′0 = ⊤ U′ ′1 = ⊤ U′ ′2 = ⊤ U′ ′σ = Rec (♯ (Σ[ a ∶ U ] (El a → U))) U′ ′π = Rec (♯ (Σ[ a ∶ U ] (El a → U))) U′ ′w = Rec (♯ (Σ[ a ∶ U ] (El a → U))) El : U → Set El (′0 , _) = ⊥ El (′1 , _) = ⊤ El (′2 , _) = Bool El (′σ , fold (a , b)) = Σ[ x ∶ El a ] El (b x) El (′π , fold (a , b)) = (x : El a) → El (b x) El (′w , fold (a , b)) = W[ x ∶ El a ] El (b x) U-rec : (P : ∀ u → El u → Set) → P (′1 , _) tt → P (′2 , _) true → P (′2 , _) false → (∀ {a b x y} → P a x → P (b x) y → P (′σ , fold (a , b)) (x , y)) → (∀ {a b f} → (∀ x → P (b x) (f x)) → P (′π , fold (a , b)) f) → (∀ {a b x f} → (∀ y → P (′w , fold (a , b)) (f y)) → P (′w , fold (a , b)) (sup x f)) → ∀ u (x : El u) → P u x U-rec P P1 P2t P2f Pσ Pπ Pw = rec where rec : ∀ u (x : El u) → P u x rec (′0 , _) () rec (′1 , _) _ = P1 rec (′2 , _) true = P2t rec (′2 , _) false = P2f rec (′σ , fold (a , b)) (x , y) = Pσ (rec _ x) (rec _ y) rec (′π , fold (a , b)) f = Pπ (λ x → rec _ (f x)) rec (′w , fold (a , b)) (fold (x , f)) = Pw (λ y → rec _ (f y))
The --guardedness-preserving-type-constructors extension is based on a rather operational understanding of ∞/♯_; it's not yet clear if this extension is consistent.
others
TODO