agda_mode/resp/
di.rs

1use super::{GoalSpecific, InvisibleGoal, ResponseContextEntry, VisibleGoal};
2use crate::base::{Cohesion, ComputeMode, Hiding, Relevance};
3use crate::pos::InteractionPoint;
4use crate::resp::OutputForm;
5use serde::Deserialize;
6
7#[serde(rename_all = "camelCase")]
8#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
9pub struct CommandState {
10    pub interaction_points: Vec<InteractionPoint>,
11    pub current_file: String,
12}
13
14#[serde(rename_all = "camelCase")]
15#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
16pub struct InferredType {
17    pub command_state: CommandState,
18    pub time: String,
19    pub expr: String,
20}
21
22#[serde(rename_all = "camelCase")]
23#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
24pub struct NormalForm {
25    pub compute_mode: ComputeMode,
26    pub command_state: CommandState,
27    pub time: String,
28    pub expr: String,
29}
30
31#[serde(rename_all = "camelCase")]
32#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
33pub struct Context {
34    pub interaction_point: InteractionPoint,
35    pub context: Vec<ResponseContextEntry>,
36}
37
38#[serde(rename_all = "camelCase")]
39#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
40pub struct AgdaError {
41    pub message: Option<String>,
42}
43
44impl Into<String> for AgdaError {
45    fn into(self) -> String {
46        self.message.unwrap_or_else(|| "Unknown error".to_owned())
47    }
48}
49
50impl<Ok> Into<Result<Ok, String>> for AgdaError {
51    fn into(self) -> Result<Ok, String> {
52        Err(self.into())
53    }
54}
55
56#[serde(rename_all = "camelCase")]
57#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
58pub struct NamedPrettyTCM {
59    pub name: String,
60    pub term: String,
61}
62
63/// One item in the `telToList` telescope list.
64#[serde(rename_all = "camelCase")]
65#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
66pub struct TelescopicItem {
67    pub dom: String,
68    pub name: Option<String>,
69    pub finite: bool,
70    pub cohesion: Cohesion,
71    pub relevance: Relevance,
72    pub hiding: Hiding,
73}
74
75#[serde(rename_all = "camelCase")]
76#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
77pub struct ModuleContents {
78    pub names: Vec<String>,
79    pub contents: Vec<NamedPrettyTCM>,
80    pub telescope: Vec<TelescopicItem>,
81}
82
83#[serde(rename_all = "camelCase")]
84#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
85pub struct AllGoalsWarnings {
86    pub visible_goals: Vec<VisibleGoal>,
87    pub invisible_goals: Vec<InvisibleGoal>,
88    pub warnings: String,
89    pub errors: String,
90}
91
92/// Something that is displayed in the Emacs mode,
93/// serialized with more details.
94#[serde(tag = "kind")]
95#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
96pub enum DisplayInfo {
97    CompilationOk {
98        warnings: String,
99        errors: String,
100    },
101    Constraints {
102        constraints: Vec<OutputForm>,
103    },
104    AllGoalsWarnings(AllGoalsWarnings),
105    Time {
106        time: String,
107    },
108    Error(AgdaError),
109    IntroNotFound,
110    IntroConstructorUnknown {
111        /// Available constructors
112        constructors: Vec<String>,
113    },
114    Auto {
115        info: String,
116    },
117    ModuleContents(ModuleContents),
118    SearchAbout {
119        search: String,
120        results: Vec<NamedPrettyTCM>,
121    },
122    WhyInScope {
123        thing: String,
124        filepath: String,
125        message: String,
126    },
127    NormalForm(NormalForm),
128    InferredType(InferredType),
129    Context(Context),
130    Version {
131        version: String,
132    },
133    GoalSpecific(GoalSpecific),
134}
agda_mode/resp/di.rs

agda_mode/resp/
di.rs
