agda_mode/cmd/
goal.rs

1use crate::base::Rewrite;
2use crate::pos::{AgdaRange, InteractionId, Pos};
3use std::fmt::{Display, Error, Formatter};
4
5/// Text in the goal.
6#[derive(Debug, Clone)]
7pub struct GoalInput {
8    id: InteractionId,
9    range: AgdaRange,
10    code: String,
11}
12
13impl GoalInput {
14    pub fn new(id: InteractionId, range: AgdaRange, code: String) -> Self {
15        GoalInput { id, range, code }
16    }
17
18    pub fn simple(id: InteractionId) -> Self {
19        Self::no_range(id, String::new())
20    }
21
22    pub fn no_range(id: InteractionId, code: String) -> Self {
23        Self::new(id, Default::default(), code)
24    }
25}
26
27impl Display for GoalInput {
28    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
29        write!(f, "{:?} {} {:?}", self.id, self.range, self.code)
30    }
31}
32
33impl Display for Pos {
34    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
35        write!(f, "(Pn () {:?} {:?} {:?})", self.pos, self.line, self.col)
36    }
37}
38
39impl Display for AgdaRange {
40    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
41        match self {
42            AgdaRange::NoRange => f.write_str("noRange"),
43            AgdaRange::Range(r) => {
44                write!(f, "(intervalsToRange ")?;
45                match &r.file {
46                    None => f.write_str("Nothing"),
47                    Some(file) => write!(f, "(Just (mkAbsolute {:?}))", file),
48                }?;
49                write!(f, " [Interval {} {}])", r.start, r.end)
50            }
51        }
52    }
53}
54
55#[derive(Debug, Clone)]
56pub struct InputWithRewrite {
57    pub rewrite: Rewrite,
58    pub input: GoalInput,
59}
60
61impl From<GoalInput> for InputWithRewrite {
62    fn from(input: GoalInput) -> Self {
63        InputWithRewrite {
64            input,
65            rewrite: Default::default(),
66        }
67    }
68}
69
70impl Display for InputWithRewrite {
71    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
72        write!(f, "{:?} {}", self.rewrite, self.input)
73    }
74}
agda_mode/cmd/goal.rs

agda_mode/cmd/
goal.rs
