agda-mode 0.1.8

Accessing Agda's interaction mode via command line, in Rust
Documentation 
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

use serde::Deserialize;
use std::fmt::{Display, Error, Formatter};
use std::ops::Range;

pub type IntPos = i32;

/// A position in the file.
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Copy, Default, Debug, Eq, PartialEq)]
pub struct Pos {
    pub pos: usize,
    pub line: usize,
    pub col: usize,
}

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct Interval {
    pub file: Option<String>,
    pub start: Pos,
    pub end: Pos,
}

impl Interval {
    pub fn range(&self) -> Range<usize> {
        self.range_shift_left(0)
    }

    pub fn range_shift_left(&self, shift: usize) -> Range<usize> {
        self.start.pos - shift..self.end.pos - shift
    }

    pub fn range_shift_right(&self, shift: usize) -> Range<usize> {
        self.start.pos + shift..self.end.pos + shift
    }
}

/// Normally, it's positive.
pub type InteractionId = i32;

/// Normally, it's also positive.
pub type ProblemId = i32;

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct InteractionPoint {
    pub id: InteractionId,
    pub range: Vec<Interval>,
}

impl InteractionPoint {
    pub fn the_interval(&self) -> &Interval {
        debug_assert_eq!(self.range.len(), 1);
        &self.range[0]
    }
}

impl Display for InteractionPoint {
    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
        write!(f, "{:?}", self.id)
    }
}

/// IDK why is this needed, but Emacs passes it to Agda.
/// It's fine to omit this in the commands.
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum AgdaRange {
    NoRange,
    Range(Interval),
}

impl Into<Option<Interval>> for AgdaRange {
    fn into(self) -> Option<Interval> {
        match self {
            AgdaRange::NoRange => None,
            AgdaRange::Range(i) => Some(i),
        }
    }
}

impl From<Option<Interval>> for AgdaRange {
    fn from(i: Option<Interval>) -> Self {
        i.map_or_else(Default::default, AgdaRange::Range)
    }
}

impl Default for AgdaRange {
    fn default() -> Self {
        AgdaRange::NoRange
    }
}