agda_mode/resp/
oc.rs

1use crate::base::{Comparison, Polarity};
2use crate::pos::{InteractionId, Interval, ProblemId};
3use serde::Deserialize;
4use std::fmt::{Display, Error, Formatter};
5
6#[serde(rename_all = "camelCase")]
7#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
8pub struct OutputForm {
9    pub range: Vec<Interval>,
10    pub problems: Vec<ProblemId>,
11    pub constraint: OutputConstraint<String>,
12}
13
14#[serde(rename_all = "camelCase")]
15#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
16pub struct FindInstanceCandidate {
17    #[serde(rename = "type")]
18    pub of_type: String,
19    pub value: String,
20}
21
22#[serde(rename_all = "camelCase")]
23#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
24pub struct JustSomething<Obj> {
25    pub constraint_obj: Obj,
26}
27
28#[serde(rename_all = "camelCase")]
29#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
30pub struct PostponedCheckArgs<Obj> {
31    pub constraint_obj: Obj,
32    pub of_type: String,
33    #[serde(rename = "type")]
34    pub the_type: String,
35    pub arguments: Vec<String>,
36}
37
38#[serde(rename_all = "camelCase")]
39#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
40pub struct CmpSomething<Obj> {
41    pub constraint_objs: (Obj, Obj),
42    pub comparison: Comparison,
43}
44
45#[serde(rename_all = "camelCase")]
46#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
47pub struct FindInstanceOF<Obj> {
48    pub constraint_obj: Obj,
49    #[serde(rename = "type")]
50    pub of_type: String,
51    pub candidates: Vec<FindInstanceCandidate>,
52}
53
54#[serde(rename_all = "camelCase")]
55#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
56pub struct TypedAssign<Obj> {
57    pub constraint_obj: Obj,
58    #[serde(rename = "type")]
59    pub of_type: String,
60    pub value: String,
61}
62
63#[serde(rename_all = "camelCase")]
64#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
65pub struct OfType<Obj> {
66    pub constraint_obj: Obj,
67    #[serde(rename = "type")]
68    pub of_type: String,
69}
70
71#[serde(tag = "kind")]
72#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
73pub enum OutputConstraint<Obj> {
74    OfType(OfType<Obj>),
75    CmpInType {
76        #[serde(rename = "constraintObjs")]
77        constraint_objs: (Obj, Obj),
78        #[serde(rename = "type")]
79        of_type: String,
80        comparison: Comparison,
81    },
82    CmpElim {
83        #[serde(rename = "constraintObjs")]
84        constraint_objs: (Vec<Obj>, Vec<Obj>),
85        #[serde(rename = "type")]
86        of_type: String,
87        polarities: Vec<Polarity>,
88    },
89    JustType(JustSomething<Obj>),
90    JustSort(JustSomething<Obj>),
91    CmpTypes(CmpSomething<Obj>),
92    CmpLevels(CmpSomething<Obj>),
93    CmpTeles(CmpSomething<Obj>),
94    CmpSorts(CmpSomething<Obj>),
95    Guard {
96        constraint: Box<OutputConstraint<Obj>>,
97        problem: ProblemId,
98    },
99    Assign {
100        #[serde(rename = "constraintObj")]
101        constraint_obj: Obj,
102        value: String,
103    },
104    TypedAssign(TypedAssign<Obj>),
105    PostponedCheckArgs(PostponedCheckArgs<Obj>),
106    IsEmptyType {
107        #[serde(rename = "type")]
108        the_type: String,
109    },
110    SizeLtSat {
111        #[serde(rename = "type")]
112        the_type: String,
113    },
114    FindInstanceOF(FindInstanceOF<Obj>),
115    PTSInstance {
116        #[serde(rename = "constraintObjs")]
117        constraint_objs: (Obj, Obj),
118    },
119    PostponedCheckFunDef {
120        name: String,
121        #[serde(rename = "type")]
122        of_type: String,
123    },
124}
125
126pub type VisibleGoal = OutputConstraint<InteractionId>;
127pub type InvisibleGoal = OutputConstraint<String>;
128
129impl<Obj> OutputConstraint<Obj> {
130    pub fn try_into_of_type(self) -> Result<OfType<Obj>, Self> {
131        if let OutputConstraint::OfType(o) = self {
132            Ok(o)
133        } else {
134            Err(self)
135        }
136    }
137
138    pub fn try_as_of_type(&self) -> Result<&OfType<Obj>, &Self> {
139        if let OutputConstraint::OfType(o) = self {
140            Ok(o)
141        } else {
142            Err(self)
143        }
144    }
145}
146
147pub trait CollectObjs<Obj> {
148    fn collect_objs(&self, collect: impl FnMut(&Obj));
149}
150
151macro_rules! simple_collect_objs {
152    ($class:ident) => {
153        impl<Obj> CollectObjs<Obj> for $class<Obj> {
154            fn collect_objs(&self, mut collect: impl FnMut(&Obj)) {
155                collect(&self.constraint_obj)
156            }
157        }
158    };
159}
160
161simple_collect_objs!(JustSomething);
162simple_collect_objs!(PostponedCheckArgs);
163simple_collect_objs!(OfType);
164simple_collect_objs!(FindInstanceOF);
165simple_collect_objs!(TypedAssign);
166
167impl<Obj> CollectObjs<Obj> for Vec<Obj> {
168    fn collect_objs(&self, collect: impl FnMut(&Obj)) {
169        self.iter().for_each(collect)
170    }
171}
172
173impl<Obj> CollectObjs<Obj> for (Obj, Obj) {
174    fn collect_objs(&self, mut collect: impl FnMut(&Obj)) {
175        let (a, b) = self;
176        collect(a);
177        collect(b);
178    }
179}
180
181impl<Obj> CollectObjs<Obj> for (Vec<Obj>, Vec<Obj>) {
182    fn collect_objs(&self, mut collect: impl FnMut(&Obj)) {
183        let (a, b) = self;
184        a.collect_objs(|x| collect(x));
185        b.collect_objs(collect);
186    }
187}
188
189impl<Obj> CollectObjs<Obj> for CmpSomething<Obj> {
190    fn collect_objs(&self, collect: impl FnMut(&Obj)) {
191        self.constraint_objs.collect_objs(collect);
192    }
193}
194
195impl<Obj> CollectObjs<Obj> for OutputConstraint<Obj> {
196    fn collect_objs(&self, mut collect: impl FnMut(&Obj)) {
197        use OutputConstraint::*;
198        match self {
199            OfType(o) => o.collect_objs(collect),
200            CmpInType {
201                constraint_objs, ..
202            } => constraint_objs.collect_objs(collect),
203            CmpElim {
204                constraint_objs, ..
205            } => constraint_objs.collect_objs(collect),
206            JustType(a) => a.collect_objs(collect),
207            JustSort(a) => a.collect_objs(collect),
208            CmpTypes(c) => c.collect_objs(collect),
209            CmpLevels(c) => c.collect_objs(collect),
210            CmpTeles(c) => c.collect_objs(collect),
211            CmpSorts(c) => c.collect_objs(collect),
212            Guard { constraint, .. } => constraint.collect_objs(collect),
213            Assign { constraint_obj, .. } => collect(constraint_obj),
214            TypedAssign(o) => o.collect_objs(collect),
215            PostponedCheckArgs(o) => o.collect_objs(collect),
216            IsEmptyType { .. } => {}
217            SizeLtSat { .. } => {}
218            FindInstanceOF(o) => o.collect_objs(collect),
219            PTSInstance { constraint_objs } => constraint_objs.collect_objs(collect),
220            PostponedCheckFunDef { .. } => {}
221        }
222    }
223}
224
225impl<Obj: Display> Display for JustSomething<Obj> {
226    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
227        self.constraint_obj.fmt(f)
228    }
229}
230
231impl<Obj: Display> Display for CmpSomething<Obj> {
232    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
233        let (a, b) = &self.constraint_objs;
234        write!(f, "{} {} {}", a, self.comparison, b)
235    }
236}
237
238impl<Obj: Display> Display for OfType<Obj> {
239    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
240        write!(f, "{} : {}", self.constraint_obj, self.of_type)
241    }
242}
243
244impl<Obj: Display> Display for TypedAssign<Obj> {
245    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
246        write!(
247            f,
248            "{} := {} :? {}",
249            self.constraint_obj, self.value, self.of_type
250        )
251    }
252}
253
254impl<Obj: Display> Display for PostponedCheckArgs<Obj> {
255    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
256        write!(f, "{} := ({}", self.constraint_obj, self.of_type)?;
257        for argument in &self.arguments {
258            write!(f, " {}", argument)?;
259        }
260        write!(f, ") ?: {}", self.the_type)
261    }
262}
263
264impl Display for FindInstanceCandidate {
265    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
266        write!(f, "{} : {}", self.value, self.of_type)
267    }
268}
269
270impl<Obj: Display> Display for FindInstanceOF<Obj> {
271    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
272        write!(
273            f,
274            "Resolve instance argument {} : {}, candidates: ",
275            self.constraint_obj, self.of_type
276        )?;
277        for argument in &self.candidates {
278            write!(f, "{}, ", argument)?;
279        }
280        Ok(())
281    }
282}
283
284impl<Obj: Display + std::fmt::Debug> Display for OutputConstraint<Obj> {
285    fn fmt(&self, f: &mut Formatter) -> Result<(), Error> {
286        use OutputConstraint::*;
287        match self {
288            OfType(o) => o.fmt(f),
289            CmpInType {
290                constraint_objs: (a, b),
291                of_type,
292                comparison,
293            } => write!(f, "{} {} {} of type {}", a, comparison, b, of_type),
294            CmpElim {
295                constraint_objs: (xs, ys),
296                of_type,
297                polarities,
298                // TODO: this can be improved, and the debug trait bound can be removed
299            } => write!(f, "{:?} {:?} {:?} of type {}", xs, polarities, ys, of_type),
300            JustType(j) => j.fmt(f),
301            JustSort(j) => j.fmt(f),
302            CmpTypes(c) => c.fmt(f),
303            CmpLevels(c) => c.fmt(f),
304            CmpTeles(c) => c.fmt(f),
305            CmpSorts(c) => c.fmt(f),
306            Guard {
307                constraint,
308                problem,
309            } => write!(f, "{} (blocked by {})", constraint, problem),
310            Assign {
311                constraint_obj,
312                value,
313            } => write!(f, "{} := {}", constraint_obj, value),
314            TypedAssign(o) => o.fmt(f),
315            PostponedCheckArgs(o) => o.fmt(f),
316            IsEmptyType { the_type } => write!(f, "Is empty: {}", the_type),
317            SizeLtSat { the_type } => write!(f, "Not empty type of sizes: {}", the_type),
318            FindInstanceOF(o) => o.fmt(f),
319            PTSInstance {
320                constraint_objs: (a, b),
321            } => write!(f, "PTS Instance for {}, {}", a, b),
322            PostponedCheckFunDef { name, of_type } => {
323                write!(f, "Check definition of {} : {}", name, of_type)
324            }
325        }
326    }
327}
agda_mode/resp/oc.rs

agda_mode/resp/
oc.rs
