agda_mode/
base.rs

1use serde::Deserialize;
2use std::fmt::{Display, Error, Formatter};
3
4/// Modifier for interactive commands,
5/// specifying the amount of normalization in the output.
6#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
7pub enum Rewrite {
8    AsIs,
9    Instantiated,
10    HeadNormal,
11    Simplified,
12    Normalised,
13}
14
15impl Default for Rewrite {
16    fn default() -> Self {
17        Rewrite::Simplified
18    }
19}
20
21/// Modifier for the interactive computation command,
22/// specifying the mode of computation and result display.
23#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
24pub enum ComputeMode {
25    DefaultCompute,
26    IgnoreAbstract,
27    UseShowInstance,
28}
29
30impl Default for ComputeMode {
31    fn default() -> Self {
32        ComputeMode::DefaultCompute
33    }
34}
35
36#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
37pub enum Comparison {
38    CmpEq,
39    CmpLeq,
40}
41
42impl Display for Comparison {
43    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
44        f.write_str(match self {
45            Comparison::CmpEq => "==",
46            Comparison::CmpLeq => "<=",
47        })
48    }
49}
50
51/// An extension of [`Comparison`](self::Comparison) to `>=`.
52#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
53pub enum CompareDirection {
54    DirEq,
55    DirLeq,
56    DirGeq,
57}
58
59impl From<Comparison> for CompareDirection {
60    fn from(from: Comparison) -> Self {
61        match from {
62            Comparison::CmpEq => CompareDirection::DirEq,
63            Comparison::CmpLeq => CompareDirection::DirLeq,
64        }
65    }
66}
67
68/// Polarity for equality and subtype checking.
69#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
70pub enum Polarity {
71    /// monotone
72    Covariant,
73    /// antitone
74    Contravariant,
75    /// no information (mixed variance)
76    Invariant,
77    /// constant
78    Nonvariant,
79}
80
81impl Display for Polarity {
82    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
83        f.write_str(match self {
84            Polarity::Covariant => "+",
85            Polarity::Contravariant => "-",
86            Polarity::Invariant => "*",
87            Polarity::Nonvariant => "_",
88        })
89    }
90}
91
92/// Modifier for interactive commands,
93/// specifying whether safety checks should be ignored.
94#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
95pub enum UseForce {
96    /// Ignore additional checks, like termination/positivity...
97    WithForce,
98    /// Don't ignore any checks.
99    WithoutForce,
100}
101
102#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
103pub enum Remove {
104    Remove,
105    Keep,
106}
107
108/// Is the highlighting "token-based", i.e. based only on
109/// information from the lexer?
110#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
111pub enum TokenBased {
112    TokenBased,
113    NotOnlyTokenBased,
114}
115
116impl Default for TokenBased {
117    fn default() -> Self {
118        TokenBased::NotOnlyTokenBased
119    }
120}
121
122#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
123pub enum Hiding {
124    YesOverlap,
125    NoOverlap,
126    Hidden,
127    NotHidden,
128}
129
130/// A function argument can be relevant or irrelevant.
131/// See "Agda.TypeChecking.Irrelevance".
132#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
133pub enum Relevance {
134    /// The argument is (possibly) relevant at compile-time.
135    Relevant,
136    /// The argument may never flow into evaluation position.
137    /// Therefore, it is irrelevant at run-time.
138    /// It is treated relevantly during equality checking.
139    NonStrict,
140    /// The argument is irrelevant at compile- and runtime.
141    Irrelevant,
142}
143
144/// Cohesion modalities
145/// see "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" (arXiv:1509.07584)
146/// types are now given an additional topological layer which the modalities interact with.
147#[derive(Deserialize, Debug, Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
148pub enum Cohesion {
149    /// Same points, discrete topology, idempotent comonad, box - like.
150    Flat,
151    /// Identity modality.
152    Continuous,
153    /// Same points, codiscrete topology, idempotent monad, diamond-like.
154    Sharp,
155    /// Single point space, artificially added for Flat left-composition.
156    Squash,
157}
agda_mode/base.rs

agda_mode/
base.rs
