flams_ontology/narration/
checking.rs1use flams_utils::vecmap::VecMap;
2
3use crate::{
4 content::terms::Term,
5 uris::{DocumentElementURI, DocumentURI, ModuleURI, Name, SymbolURI},
6 Checked, DocumentRange, LocalBackend, MaybeResolved, Unchecked,
7};
8
9use super::{
10 paragraphs::{LogicalParagraph, ParagraphFormatting, ParagraphKind},
11 problems::{CognitiveDimension, GradingNote, Problem, Solutions},
12 sections::{Section, SectionLevel},
13 DocumentElement, LazyDocRef,
14};
15
16pub trait DocumentChecker: LocalBackend {
17 fn open(&mut self, elem: &mut DocumentElement<Unchecked>);
18 fn close(&mut self, elem: &mut DocumentElement<Checked>);
19}
20
21enum Elem {
22 Section {
23 range: DocumentRange,
24 uri: DocumentElementURI,
25 level: SectionLevel,
26 title: Option<DocumentRange>,
27 },
28 Slide {
29 range: DocumentRange,
30 uri: DocumentElementURI,
31 },
32 SkipSection,
33 Module {
34 range: DocumentRange,
35 module: ModuleURI,
36 },
37 Morphism {
38 range: DocumentRange,
39 morphism: SymbolURI,
40 },
41 MathStructure {
42 range: DocumentRange,
43 structure: SymbolURI,
44 },
45 Extension {
46 range: DocumentRange,
47 extension: SymbolURI,
48 target: SymbolURI,
49 },
50 Paragraph {
51 kind: ParagraphKind,
52 uri: DocumentElementURI,
53 formatting: ParagraphFormatting,
54 title: Option<DocumentRange>,
55 range: DocumentRange,
56 styles: Box<[Name]>,
57 fors: VecMap<SymbolURI, Option<Term>>,
58 },
59 Problem {
60 sub_problem: bool,
61 uri: DocumentElementURI,
62 autogradable: bool,
63 range: DocumentRange,
64 points: Option<f32>,
65 solutions: LazyDocRef<Solutions>,
66 gnotes: Vec<LazyDocRef<GradingNote>>,
67 hints: Vec<DocumentRange>,
68 notes: Vec<LazyDocRef<Box<str>>>,
69 title: Option<DocumentRange>,
70 styles: Box<[Name]>,
71 preconditions: Vec<(CognitiveDimension, SymbolURI)>,
72 objectives: Vec<(CognitiveDimension, SymbolURI)>,
73 },
74}
75impl Elem {
76 fn close(
77 self,
78 v: Vec<DocumentElement<Checked>>,
79 checker: &mut impl DocumentChecker,
80 ) -> DocumentElement<Checked> {
81 match self {
82 Self::Section {
83 range,
84 uri,
85 level,
86 title,
87 } => DocumentElement::Section(Section {
88 range,
89 uri,
90 level,
91 title,
92 children: v.into_boxed_slice(),
93 }),
94 Self::Slide { range, uri } => DocumentElement::Slide {
95 range,
96 uri,
97 children: v.into_boxed_slice(),
98 },
99 Self::SkipSection => DocumentElement::SkipSection(v.into_boxed_slice()),
100 Self::Module { range, module } => DocumentElement::Module {
101 range,
102 module: MaybeResolved::resolve(module, |m| checker.get_module(m)),
103 children: v.into_boxed_slice(),
104 },
105 Self::Morphism { range, morphism } => DocumentElement::Morphism {
106 range,
107 morphism: MaybeResolved::resolve(morphism, |m| checker.get_declaration(m)),
108 children: v.into_boxed_slice(),
109 },
110 Self::MathStructure { range, structure } => DocumentElement::MathStructure {
111 range,
112 structure: MaybeResolved::resolve(structure, |m| checker.get_declaration(m)),
113 children: v.into_boxed_slice(),
114 },
115 Self::Extension {
116 range,
117 extension,
118 target,
119 } => DocumentElement::Extension {
120 range,
121 extension: MaybeResolved::resolve(extension, |m| checker.get_declaration(m)),
122 target: MaybeResolved::resolve(target, |m| checker.get_declaration(m)),
123 children: v.into_boxed_slice(),
124 },
125 Self::Paragraph {
126 kind,
127 uri,
128 formatting,
129 title,
130 fors,
131 range,
132 styles,
133 } => DocumentElement::Paragraph(LogicalParagraph {
134 kind,
135 uri,
136 formatting,
137 title,
138 range,
139 styles,
140 fors,
141 children: v.into_boxed_slice(),
142 }),
143 Self::Problem {
144 sub_problem,
145 range,
146 uri,
147 autogradable,
148 points,
149 solutions,
150 gnotes,
151 hints,
152 notes,
153 title,
154 preconditions,
155 styles,
156 objectives,
157 } => DocumentElement::Problem(Problem {
158 sub_problem,
159 uri,
160 autogradable,
161 points,
162 title,
163 styles,
164 range,
165 solutions,
166 gnotes: gnotes.into_boxed_slice(),
167 hints: hints.into_boxed_slice(),
168 notes: notes.into_boxed_slice(),
169 preconditions: preconditions.into_boxed_slice(),
170 objectives: objectives.into_boxed_slice(),
171 children: v.into_boxed_slice(),
172 }),
173 }
174 }
175}
176
177#[allow(clippy::type_complexity)]
178pub(super) struct DocumentCheckIter<'a, Check: DocumentChecker> {
179 stack: Vec<(
180 Elem,
181 std::vec::IntoIter<DocumentElement<Unchecked>>,
182 Vec<DocumentElement<Checked>>,
183 )>,
184 curr_in: std::vec::IntoIter<DocumentElement<Unchecked>>,
185 curr_out: Vec<DocumentElement<Checked>>,
186 checker: &'a mut Check,
187 #[allow(dead_code)]
188 uri: &'a DocumentURI,
189}
190
191impl<Check: DocumentChecker> DocumentCheckIter<'_, Check> {
192 pub(super) fn go(
193 elems: Vec<DocumentElement<Unchecked>>,
194 checker: &mut Check,
195 uri: &DocumentURI,
196 ) -> Vec<DocumentElement<Checked>> {
197 let mut slf = DocumentCheckIter {
198 stack: Vec::new(),
199 curr_in: elems.into_iter(),
200 curr_out: Vec::new(),
201 checker,
202 uri,
203 };
204 loop {
205 while let Some(next) = slf.curr_in.next() {
206 slf.do_elem(next);
207 }
208 if let Some((e, curr_in, curr_out)) = slf.stack.pop() {
209 slf.curr_in = curr_in;
210 let dones = std::mem::replace(&mut slf.curr_out, curr_out);
211 let mut closed = e.close(dones, slf.checker);
212 slf.checker.close(&mut closed);
213 slf.curr_out.push(closed);
214 } else {
215 return slf.curr_out;
216 }
217 }
218 }
219
220 #[allow(clippy::too_many_lines)]
221 fn do_elem(&mut self, mut e: DocumentElement<Unchecked>) {
222 self.checker.open(&mut e);
223 let mut ret = match e {
224 DocumentElement::SetSectionLevel(lvl) => DocumentElement::SetSectionLevel(lvl),
225 DocumentElement::DocumentReference { id, range, target } => {
226 let target = MaybeResolved::resolve(target, |m| self.checker.get_document(m));
227 DocumentElement::DocumentReference { id, range, target }
228 }
229 DocumentElement::SymbolDeclaration(uri) => {
230 let symbol = MaybeResolved::resolve(uri, |m| self.checker.get_declaration(m));
231 DocumentElement::SymbolDeclaration(symbol)
232 }
233 DocumentElement::UseModule(module) => {
234 let module = MaybeResolved::resolve(module, |m| self.checker.get_module(m));
235 DocumentElement::UseModule(module)
236 }
237 DocumentElement::ImportModule(module) => {
238 let module = MaybeResolved::resolve(module, |m| self.checker.get_module(m));
239 DocumentElement::ImportModule(module)
240 }
241 DocumentElement::Notation {
242 symbol,
243 id,
244 notation,
245 } => DocumentElement::Notation {
246 symbol,
247 id,
248 notation,
249 },
250 DocumentElement::VariableNotation {
251 variable,
252 id,
253 notation,
254 } => DocumentElement::VariableNotation {
255 variable,
256 id,
257 notation,
258 },
259 DocumentElement::Variable(v) => DocumentElement::Variable(v),
260 DocumentElement::Definiendum { range, uri } => {
261 DocumentElement::Definiendum { range, uri }
262 }
263 DocumentElement::SymbolReference {
264 range,
265 uri,
266 notation,
267 } => DocumentElement::SymbolReference {
268 range,
269 uri,
270 notation,
271 },
272 DocumentElement::VariableReference {
273 range,
274 uri,
275 notation,
276 } => DocumentElement::VariableReference {
277 range,
278 uri,
279 notation,
280 },
281 DocumentElement::TopTerm { uri, term } => DocumentElement::TopTerm { uri, term },
282 DocumentElement::SkipSection(children) => {
283 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
284 let old_out = std::mem::take(&mut self.curr_out);
285 self.stack.push((Elem::SkipSection, old_in, old_out));
286 return;
287 }
288 DocumentElement::Section(Section {
289 range,
290 uri,
291 level,
292 title,
293 children,
294 }) => {
295 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
296 let old_out = std::mem::take(&mut self.curr_out);
297 self.stack.push((
298 Elem::Section {
299 range,
300 uri,
301 level,
302 title,
303 },
304 old_in,
305 old_out,
306 ));
307 return;
308 }
309 DocumentElement::Slide {
310 range,
311 uri,
312 children,
313 } => {
314 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
315 let old_out = std::mem::take(&mut self.curr_out);
316 self.stack
317 .push((Elem::Slide { range, uri }, old_in, old_out));
318 return;
319 }
320 DocumentElement::Module {
321 range,
322 module,
323 children,
324 } => {
325 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
326 let old_out = std::mem::take(&mut self.curr_out);
327 self.stack
328 .push((Elem::Module { range, module }, old_in, old_out));
329 return;
330 }
331 DocumentElement::Morphism {
332 range,
333 morphism,
334 children,
335 } => {
336 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
337 let old_out = std::mem::take(&mut self.curr_out);
338 self.stack
339 .push((Elem::Morphism { range, morphism }, old_in, old_out));
340 return;
341 }
342 DocumentElement::MathStructure {
343 range,
344 structure,
345 children,
346 } => {
347 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
348 let old_out = std::mem::take(&mut self.curr_out);
349 self.stack
350 .push((Elem::MathStructure { range, structure }, old_in, old_out));
351 return;
352 }
353 DocumentElement::Extension {
354 range,
355 extension,
356 target,
357 children,
358 } => {
359 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
360 let old_out = std::mem::take(&mut self.curr_out);
361 self.stack.push((
362 Elem::Extension {
363 range,
364 extension,
365 target,
366 },
367 old_in,
368 old_out,
369 ));
370 return;
371 }
372 DocumentElement::Paragraph(LogicalParagraph {
373 kind,
374 uri,
375 formatting,
376 title,
377 fors,
378 range,
379 styles,
380 children,
381 }) => {
382 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
383 let old_out = std::mem::take(&mut self.curr_out);
384 self.stack.push((
385 Elem::Paragraph {
386 kind,
387 uri,
388 formatting,
389 title,
390 fors,
391 range,
392 styles,
393 },
394 old_in,
395 old_out,
396 ));
397 return;
398 }
399 DocumentElement::Problem(Problem {
400 sub_problem,
401 uri,
402 autogradable,
403 points,
404 solutions,
405 range,
406 hints,
407 styles,
408 notes,
409 gnotes,
410 title,
411 children,
412 preconditions,
413 objectives,
414 }) => {
415 let old_in = std::mem::replace(&mut self.curr_in, children.into_iter());
416 let old_out = std::mem::take(&mut self.curr_out);
417 self.stack.push((
418 Elem::Problem {
419 sub_problem,
420 uri,
421 range,
422 autogradable,
423 points,
424 solutions,
425 gnotes,
426 styles,
427 hints,
428 notes,
429 title,
430 preconditions,
431 objectives,
432 },
433 old_in,
434 old_out,
435 ));
436 return;
437 }
438 };
439 self.checker.close(&mut ret);
440 self.curr_out.push(ret);
441 }
442}