agda_mode/
pos.rs

1use serde::Deserialize;
2use std::fmt::{Display, Error, Formatter};
3use std::ops::Range;
4
5pub type IntPos = i32;
6
7/// A position in the file.
8#[serde(rename_all = "camelCase")]
9#[derive(Deserialize, Clone, Copy, Default, Debug, Eq, PartialEq)]
10pub struct Pos {
11    pub pos: usize,
12    pub line: usize,
13    pub col: usize,
14}
15
16#[serde(rename_all = "camelCase")]
17#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
18pub struct Interval {
19    pub file: Option<String>,
20    pub start: Pos,
21    pub end: Pos,
22}
23
24impl Interval {
25    pub fn range(&self) -> Range<usize> {
26        self.range_shift_left(0)
27    }
28
29    pub fn range_shift_left(&self, shift: usize) -> Range<usize> {
30        self.start.pos - shift..self.end.pos - shift
31    }
32
33    pub fn range_shift_right(&self, shift: usize) -> Range<usize> {
34        self.start.pos + shift..self.end.pos + shift
35    }
36}
37
38/// Normally, it's positive.
39pub type InteractionId = i32;
40
41/// Normally, it's also positive.
42pub type ProblemId = i32;
43
44#[serde(rename_all = "camelCase")]
45#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
46pub struct InteractionPoint {
47    pub id: InteractionId,
48    pub range: Vec<Interval>,
49}
50
51impl InteractionPoint {
52    pub fn the_interval(&self) -> &Interval {
53        debug_assert_eq!(self.range.len(), 1);
54        &self.range[0]
55    }
56}
57
58impl Display for InteractionPoint {
59    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
60        write!(f, "{:?}", self.id)
61    }
62}
63
64/// IDK why is this needed, but Emacs passes it to Agda.
65/// It's fine to omit this in the commands.
66#[derive(Debug, Clone, Eq, PartialEq)]
67pub enum AgdaRange {
68    NoRange,
69    Range(Interval),
70}
71
72impl Into<Option<Interval>> for AgdaRange {
73    fn into(self) -> Option<Interval> {
74        match self {
75            AgdaRange::NoRange => None,
76            AgdaRange::Range(i) => Some(i),
77        }
78    }
79}
80
81impl From<Option<Interval>> for AgdaRange {
82    fn from(i: Option<Interval>) -> Self {
83        i.map_or_else(Default::default, AgdaRange::Range)
84    }
85}
86
87impl Default for AgdaRange {
88    fn default() -> Self {
89        AgdaRange::NoRange
90    }
91}
agda_mode/pos.rs

agda_mode/
pos.rs
