agda_mode/resp/
goal.rs

1use crate::base::{ComputeMode, Rewrite};
2use crate::pos::InteractionPoint;
3use serde::Deserialize;
4
5#[serde(rename_all = "camelCase")]
6#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
7pub struct ResponseContextEntry {
8    pub original_name: String,
9    pub reified_name: String,
10    pub binding: String,
11    pub in_scope: bool,
12}
13
14#[serde(tag = "kind")]
15#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
16pub enum GoalTypeAux {
17    GoalOnly,
18    GoalAndHave { expr: String },
19    GoalAndElaboration { term: String },
20}
21
22#[serde(rename_all = "camelCase")]
23#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
24pub struct GoalType {
25    pub rewrite: Rewrite,
26    pub type_aux: GoalTypeAux,
27    #[serde(rename = "type")]
28    pub the_type: String,
29    pub entries: Vec<ResponseContextEntry>,
30    pub boundary: Vec<String>,
31    pub output_forms: Vec<String>,
32}
33
34/// Information about one goal.
35#[serde(tag = "kind")]
36#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
37pub enum GoalInfo {
38    HelperFunction {
39        signature: String,
40    },
41    NormalForm {
42        #[serde(rename = "computeMode")]
43        compute_mode: ComputeMode,
44        expr: String,
45    },
46    GoalType(GoalType),
47    CurrentGoal {
48        rewrite: Rewrite,
49        #[serde(rename = "type")]
50        the_type: String,
51    },
52    InferredType {
53        expr: String,
54    },
55}
56
57#[serde(rename_all = "camelCase")]
58#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
59pub struct GoalSpecific {
60    pub interaction_point: InteractionPoint,
61    pub goal_info: GoalInfo,
62}
agda_mode/resp/goal.rs

agda_mode/resp/
goal.rs
