1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94

use serde::Deserialize;

use crate::base::TokenBased;
use crate::pos::InteractionPoint;

pub use self::di::*;
pub use self::give::*;
pub use self::goal::*;
pub use self::hl::*;
pub use self::oc::*;

/// Display info.
mod di;
/// About the "Give" action.
mod give;
/// Goal information.
mod goal;
/// Highlighting.
mod hl;
/// Output constraints (user goals & unsolved metas).
mod oc;

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
pub struct MakeCase {
    pub variant: MakeCaseVariant,
    pub interaction_point: InteractionPoint,
    pub clauses: Vec<String>,
}

/// Status information.
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq, Hash)]
pub struct Status {
    /// Are implicit arguments displayed?
    pub show_implicit_arguments: bool,
    /// Has the module been successfully type checked?
    pub checked: bool,
}

#[derive(Deserialize, Copy, Clone, Debug, Eq, PartialEq, Hash)]
pub enum MakeCaseVariant {
    Function,
    ExtendedLambda,
}

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
pub struct OneSolution {
    pub interaction_point: InteractionPoint,
    pub expression: String,
}

/// Agda response.
#[serde(tag = "kind")]
#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
pub enum Resp {
    HighlightingInfo(HighlightingInfo),
    Status {
        status: Status,
    },
    JumpToError {
        filepath: String,
        position: i32,
    },
    InteractionPoints {
        #[serde(rename = "interactionPoints")]
        interaction_points: Vec<InteractionPoint>,
    },
    GiveAction(GiveAction),
    /// Response is list of printed clauses.
    MakeCase(MakeCase),
    /// Solution for one or more meta-variables.
    SolveAll {
        solutions: Vec<OneSolution>,
    },
    DisplayInfo {
        info: Option<DisplayInfo>,
    },
    /// The integer is the message's debug level.
    RunningInfo {
        #[serde(rename = "debugLevel")]
        debug_level: i32,
        message: String,
    },
    ClearRunningInfo,
    /// Clear highlighting of the given kind.
    ClearHighlighting {
        #[serde(rename = "tokenBased")]
        token_based: TokenBased,
    },
    /// A command sent when an abort command has completed successfully.
    DoneAborting,
}