flams_stex/quickparse/stex/
mod.rs

1pub mod rules;
2pub mod structs;
3
4use std::path::Path;
5
6use flams_ontology::{
7    languages::Language,
8    narration::{paragraphs::ParagraphKind, problems::CognitiveDimension},
9    uris::{ArchiveId, ArchiveURITrait, DocumentURI, ModuleURI, Name, SymbolURI},
10};
11use flams_system::backend::AnyBackend;
12use flams_utils::{
13    parsing::ParseStr,
14    prelude::{TreeChild, TreeLike},
15    sourcerefs::{LSPLineCol, SourceRange},
16    vecmap::VecSet,
17};
18use rules::{
19    MathStructureArg, MathStructureArgIter, NotationArg, NotationArgIter, ParagraphArg,
20    ParagraphArgIter, ProblemArg, ProblemArgIter, SModuleArg, SModuleArgIter, SymdeclArg,
21    SymdeclArgIter, SymdefArg, SymdefArgIter, TextSymdeclArg, TextSymdeclArgIter, VardefArg,
22    VardefArgIter,
23};
24use smallvec::SmallVec;
25use structs::{
26    InlineMorphAssIter, InlineMorphAssign, ModuleOrStruct, ModuleReference, ModuleRules,
27    MorphismKind, STeXModuleStore, STeXParseState, STeXToken, SymbolReference, SymnameMode,
28};
29
30use crate::quickparse::stex::rules::{IncludeProblemArg, MHGraphicsArg};
31
32use super::latex::LaTeXParser;
33
34#[derive(Default, Debug)]
35pub struct STeXParseDataI {
36    pub annotations: Vec<STeXAnnot>,
37    pub diagnostics: VecSet<STeXDiagnostic>,
38    pub modules: SmallVec<(ModuleURI, ModuleRules<LSPLineCol>), 1>,
39    pub dependencies: Vec<std::sync::Arc<Path>>,
40}
41impl STeXParseDataI {
42    #[inline]
43    #[must_use]
44    pub fn lock(self) -> STeXParseData {
45        flams_utils::triomphe::Arc::new(parking_lot::Mutex::new(self))
46    }
47    #[inline]
48    pub fn replace(self, old: &STeXParseData) {
49        *old.lock() = self;
50    }
51    #[inline]
52    #[must_use]
53    pub fn is_empty(&self) -> bool {
54        self.annotations.is_empty() && self.diagnostics.is_empty()
55    }
56}
57
58pub type STeXParseData = flams_utils::triomphe::Arc<parking_lot::Mutex<STeXParseDataI>>;
59
60#[allow(clippy::large_enum_variant)]
61#[derive(Debug, Clone, serde::Serialize)]
62pub enum STeXAnnot {
63    Module {
64        uri: ModuleURI,
65        name_range: SourceRange<LSPLineCol>,
66        opts: Vec<SModuleArg<LSPLineCol, Self>>,
67        sig: Option<Language>,
68        meta_theory: Option<ModuleReference>,
69        full_range: SourceRange<LSPLineCol>,
70        smodule_range: SourceRange<LSPLineCol>,
71        children: Vec<Self>,
72    },
73    MathStructure {
74        uri: SymbolReference<LSPLineCol>,
75        extends: Vec<(SymbolReference<LSPLineCol>, SourceRange<LSPLineCol>)>,
76        name_range: SourceRange<LSPLineCol>,
77        opts: Vec<MathStructureArg<LSPLineCol, Self>>,
78        full_range: SourceRange<LSPLineCol>,
79        children: Vec<Self>,
80        mathstructure_range: SourceRange<LSPLineCol>,
81    },
82    ConservativeExt {
83        uri: SymbolReference<LSPLineCol>,
84        ext_range: SourceRange<LSPLineCol>,
85        full_range: SourceRange<LSPLineCol>,
86        extstructure_range: SourceRange<LSPLineCol>,
87        children: Vec<Self>,
88    },
89    MorphismEnv {
90        full_range: SourceRange<LSPLineCol>,
91        name_range: SourceRange<LSPLineCol>,
92        env_range: SourceRange<LSPLineCol>,
93        uri: SymbolURI,
94        star: bool,
95        domain: ModuleOrStruct<LSPLineCol>,
96        domain_range: SourceRange<LSPLineCol>,
97        kind: MorphismKind,
98        children: Vec<Self>,
99    },
100    InlineMorphism {
101        full_range: SourceRange<LSPLineCol>,
102        token_range: SourceRange<LSPLineCol>,
103        name_range: SourceRange<LSPLineCol>,
104        uri: SymbolURI,
105        domain: ModuleOrStruct<LSPLineCol>,
106        domain_range: SourceRange<LSPLineCol>,
107        kind: MorphismKind,
108        assignments: Vec<InlineMorphAssign<LSPLineCol, Self>>,
109    },
110    SemanticMacro {
111        uri: SymbolReference<LSPLineCol>,
112        argnum: u8,
113        token_range: SourceRange<LSPLineCol>,
114        full_range: SourceRange<LSPLineCol>,
115    },
116    VariableMacro {
117        name: Name,
118        argnum: u8,
119        orig: SourceRange<LSPLineCol>,
120        sequence: bool,
121        token_range: SourceRange<LSPLineCol>,
122        full_range: SourceRange<LSPLineCol>,
123    },
124    Svar {
125        name: Name,
126        token_range: SourceRange<LSPLineCol>,
127        full_range: SourceRange<LSPLineCol>,
128        arg_range: SourceRange<LSPLineCol>,
129        name_range: Option<SourceRange<LSPLineCol>>,
130    },
131    ImportModule {
132        archive_range: Option<SourceRange<LSPLineCol>>,
133        path_range: SourceRange<LSPLineCol>,
134        module: ModuleReference,
135        token_range: SourceRange<LSPLineCol>,
136        full_range: SourceRange<LSPLineCol>,
137    },
138    UseModule {
139        archive_range: Option<SourceRange<LSPLineCol>>,
140        path_range: SourceRange<LSPLineCol>,
141        module: ModuleReference,
142        token_range: SourceRange<LSPLineCol>,
143        full_range: SourceRange<LSPLineCol>,
144    },
145    UseStructure {
146        structure: SymbolReference<LSPLineCol>,
147        structure_range: SourceRange<LSPLineCol>,
148        token_range: SourceRange<LSPLineCol>,
149        full_range: SourceRange<LSPLineCol>,
150    },
151    SetMetatheory {
152        archive_range: Option<SourceRange<LSPLineCol>>,
153        path_range: SourceRange<LSPLineCol>,
154        module: ModuleReference,
155        token_range: SourceRange<LSPLineCol>,
156        full_range: SourceRange<LSPLineCol>,
157    },
158    Inputref {
159        archive: Option<(ArchiveId, SourceRange<LSPLineCol>)>,
160        filepath: (std::sync::Arc<str>, SourceRange<LSPLineCol>),
161        token_range: SourceRange<LSPLineCol>,
162        full_range: SourceRange<LSPLineCol>,
163    },
164    MHInput {
165        archive: Option<(ArchiveId, SourceRange<LSPLineCol>)>,
166        filepath: (std::sync::Arc<str>, SourceRange<LSPLineCol>),
167        token_range: SourceRange<LSPLineCol>,
168        full_range: SourceRange<LSPLineCol>,
169    },
170    #[allow(clippy::type_complexity)]
171    Symdecl {
172        uri: SymbolReference<LSPLineCol>,
173        main_name_range: SourceRange<LSPLineCol>,
174        parsed_args: Vec<SymdeclArg<LSPLineCol, Self>>,
175        token_range: SourceRange<LSPLineCol>,
176        full_range: SourceRange<LSPLineCol>,
177    },
178    #[allow(clippy::type_complexity)]
179    TextSymdecl {
180        uri: SymbolReference<LSPLineCol>,
181        main_name_range: SourceRange<LSPLineCol>,
182        parsed_args: Vec<TextSymdeclArg<LSPLineCol, Self>>,
183        token_range: SourceRange<LSPLineCol>,
184        full_range: SourceRange<LSPLineCol>,
185    },
186    Notation {
187        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
188        token_range: SourceRange<LSPLineCol>,
189        name_range: SourceRange<LSPLineCol>,
190        notation_args: Vec<NotationArg<LSPLineCol, Self>>,
191        full_range: SourceRange<LSPLineCol>,
192    },
193    RenameDecl {
194        uri: SymbolReference<LSPLineCol>,
195        token_range: SourceRange<LSPLineCol>,
196        orig_range: SourceRange<LSPLineCol>,
197        name_range: Option<SourceRange<LSPLineCol>>,
198        macroname_range: SourceRange<LSPLineCol>,
199        full_range: SourceRange<LSPLineCol>,
200    },
201    Assign {
202        uri: SymbolReference<LSPLineCol>,
203        token_range: SourceRange<LSPLineCol>,
204        orig_range: SourceRange<LSPLineCol>,
205        full_range: SourceRange<LSPLineCol>,
206    },
207    #[allow(clippy::type_complexity)]
208    Symdef {
209        uri: SymbolReference<LSPLineCol>,
210        main_name_range: SourceRange<LSPLineCol>,
211        parsed_args: Vec<SymdefArg<LSPLineCol, Self>>,
212        token_range: SourceRange<LSPLineCol>,
213        full_range: SourceRange<LSPLineCol>,
214    },
215    #[allow(clippy::type_complexity)]
216    Vardef {
217        name: Name,
218        main_name_range: SourceRange<LSPLineCol>,
219        parsed_args: Vec<VardefArg<LSPLineCol, Self>>,
220        token_range: SourceRange<LSPLineCol>,
221        full_range: SourceRange<LSPLineCol>,
222    },
223    #[allow(clippy::type_complexity)]
224    Varseq {
225        name: Name,
226        main_name_range: SourceRange<LSPLineCol>,
227        parsed_args: Vec<VardefArg<LSPLineCol, Self>>,
228        token_range: SourceRange<LSPLineCol>,
229        full_range: SourceRange<LSPLineCol>,
230    },
231    SymName {
232        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
233        full_range: SourceRange<LSPLineCol>,
234        token_range: SourceRange<LSPLineCol>,
235        name_range: SourceRange<LSPLineCol>,
236        mode: SymnameMode<LSPLineCol>,
237    },
238    IncludeProblem {
239        filepath: (std::sync::Arc<str>, SourceRange<LSPLineCol>),
240        archive: Option<(ArchiveId, SourceRange<LSPLineCol>)>,
241        full_range: SourceRange<LSPLineCol>,
242        token_range: SourceRange<LSPLineCol>,
243        args: Vec<IncludeProblemArg<LSPLineCol>>,
244    },
245    Symuse {
246        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
247        full_range: SourceRange<LSPLineCol>,
248        token_range: SourceRange<LSPLineCol>,
249        name_range: SourceRange<LSPLineCol>,
250    },
251    Symref {
252        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
253        full_range: SourceRange<LSPLineCol>,
254        token_range: SourceRange<LSPLineCol>,
255        name_range: SourceRange<LSPLineCol>,
256        text: (SourceRange<LSPLineCol>, Vec<Self>),
257    },
258    Definiens {
259        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
260        full_range: SourceRange<LSPLineCol>,
261        token_range: SourceRange<LSPLineCol>,
262        name_range: Option<SourceRange<LSPLineCol>>,
263    },
264    Defnotation {
265        full_range: SourceRange<LSPLineCol>,
266    },
267    Paragraph {
268        kind: ParagraphKind,
269        full_range: SourceRange<LSPLineCol>,
270        name_range: SourceRange<LSPLineCol>,
271        symbol: Option<SymbolReference<LSPLineCol>>,
272        parsed_args: Vec<ParagraphArg<LSPLineCol, Self>>,
273        children: Vec<Self>,
274    },
275    Problem {
276        sub: bool,
277        full_range: SourceRange<LSPLineCol>,
278        name_range: SourceRange<LSPLineCol>,
279        parsed_args: Vec<ProblemArg<LSPLineCol, Self>>,
280        children: Vec<Self>,
281    },
282    Precondition {
283        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
284        full_range: SourceRange<LSPLineCol>,
285        token_range: SourceRange<LSPLineCol>,
286        dim_range: SourceRange<LSPLineCol>,
287        symbol_range: SourceRange<LSPLineCol>,
288        dim: CognitiveDimension,
289    },
290    Objective {
291        uri: SmallVec<SymbolReference<LSPLineCol>, 1>,
292        full_range: SourceRange<LSPLineCol>,
293        token_range: SourceRange<LSPLineCol>,
294        dim_range: SourceRange<LSPLineCol>,
295        symbol_range: SourceRange<LSPLineCol>,
296        dim: CognitiveDimension,
297    },
298    InlineParagraph {
299        kind: ParagraphKind,
300        full_range: SourceRange<LSPLineCol>,
301        token_range: SourceRange<LSPLineCol>,
302        symbol: Option<SymbolReference<LSPLineCol>>,
303        parsed_args: Vec<ParagraphArg<LSPLineCol, Self>>,
304        children: Vec<Self>,
305        children_range: SourceRange<LSPLineCol>,
306    },
307    MHGraphics {
308        filepath: (std::sync::Arc<str>, SourceRange<LSPLineCol>),
309        archive: Option<(ArchiveId, SourceRange<LSPLineCol>)>,
310        full_range: SourceRange<LSPLineCol>,
311        token_range: SourceRange<LSPLineCol>,
312        args: Vec<MHGraphicsArg<LSPLineCol>>,
313    },
314}
315impl STeXAnnot {
316    fn from_tokens<I: IntoIterator<Item = STeXToken<LSPLineCol>>>(
317        iter: I,
318        mut modules: Option<&mut SmallVec<(ModuleURI, ModuleRules<LSPLineCol>), 1>>,
319    ) -> Vec<Self> {
320        let mut v = Vec::new();
321        macro_rules! cont {
322      ($e:ident) => { $e.into_iter().map(|o| o.into_other(cont!(+))).collect() };
323      (+) => { |v| Self::from_tokens(v,if let Some(m) = modules.as_mut() { Some(*m) } else { None }) };
324    }
325        for t in iter {
326            match t {
327                STeXToken::Module {
328                    uri,
329                    name_range,
330                    sig,
331                    meta_theory,
332                    full_range,
333                    smodule_range,
334                    children,
335                    rules,
336                    opts,
337                } => {
338                    if let Some(ref mut m) = modules {
339                        m.push((uri.clone(), rules))
340                    };
341                    v.push(Self::Module {
342                        uri,
343                        name_range,
344                        sig,
345                        meta_theory,
346                        full_range,
347                        smodule_range,
348                        opts: cont!(opts),
349                        children: Self::from_tokens(children, None),
350                    });
351                }
352                STeXToken::MHGraphics {
353                    filepath,
354                    archive,
355                    full_range,
356                    token_range,
357                    args,
358                } => v.push(STeXAnnot::MHGraphics {
359                    filepath,
360                    archive,
361                    full_range,
362                    token_range,
363                    args,
364                }),
365                STeXToken::UseStructure {
366                    structure,
367                    structure_range,
368                    full_range,
369                    token_range,
370                } => v.push(STeXAnnot::UseStructure {
371                    structure,
372                    structure_range,
373                    full_range,
374                    token_range,
375                }),
376                STeXToken::ConservativeExt {
377                    uri,
378                    ext_range,
379                    full_range,
380                    children,
381                    extstructure_range,
382                } => v.push(Self::ConservativeExt {
383                    uri,
384                    ext_range,
385                    full_range,
386                    children: Self::from_tokens(children, None),
387                    extstructure_range,
388                }),
389                STeXToken::MathStructure {
390                    uri,
391                    extends,
392                    name_range,
393                    opts,
394                    full_range,
395                    children,
396                    mathstructure_range,
397                    ..
398                } => {
399                    v.push(Self::MathStructure {
400                        uri,
401                        extends,
402                        name_range,
403                        opts: cont!(opts),
404                        full_range,
405                        children: Self::from_tokens(children, None),
406                        mathstructure_range,
407                    });
408                }
409                STeXToken::MorphismEnv {
410                    uri,
411                    star,
412                    env_range,
413                    full_range,
414                    children,
415                    name_range,
416                    domain,
417                    domain_range,
418                    kind,
419                    ..
420                } => v.push(Self::MorphismEnv {
421                    uri,
422                    env_range,
423                    star,
424                    full_range,
425                    children: Self::from_tokens(children, None),
426                    name_range,
427                    domain,
428                    domain_range,
429                    kind,
430                }),
431                STeXToken::InlineMorphism {
432                    full_range,
433                    token_range,
434                    name_range,
435                    uri,
436                    domain,
437                    domain_range,
438                    kind,
439                    assignments,
440                    ..
441                } => v.push(Self::InlineMorphism {
442                    full_range,
443                    token_range,
444                    name_range,
445                    uri,
446                    domain,
447                    domain_range,
448                    kind,
449                    assignments: cont!(assignments),
450                }),
451                STeXToken::SemanticMacro {
452                    uri,
453                    argnum,
454                    token_range,
455                    full_range,
456                } => v.push(STeXAnnot::SemanticMacro {
457                    uri,
458                    argnum,
459                    token_range,
460                    full_range,
461                }),
462                STeXToken::VariableMacro {
463                    name,
464                    sequence,
465                    argnum,
466                    orig,
467                    token_range,
468                    full_range,
469                } => v.push(STeXAnnot::VariableMacro {
470                    name,
471                    argnum,
472                    sequence,
473                    orig,
474                    token_range,
475                    full_range,
476                }),
477                STeXToken::Svar {
478                    name,
479                    full_range,
480                    token_range,
481                    name_range,
482                    arg_range,
483                } => v.push(STeXAnnot::Svar {
484                    name,
485                    full_range,
486                    token_range,
487                    name_range,
488                    arg_range,
489                }),
490                STeXToken::ImportModule {
491                    archive_range,
492                    path_range,
493                    module,
494                    token_range,
495                    full_range,
496                } => v.push(STeXAnnot::ImportModule {
497                    archive_range,
498                    path_range,
499                    module,
500                    token_range,
501                    full_range,
502                }),
503                STeXToken::UseModule {
504                    archive_range,
505                    path_range,
506                    module,
507                    token_range,
508                    full_range,
509                } => v.push(STeXAnnot::UseModule {
510                    archive_range,
511                    path_range,
512                    module,
513                    token_range,
514                    full_range,
515                }),
516                STeXToken::IncludeProblem {
517                    filepath,
518                    full_range,
519                    token_range,
520                    archive,
521                    args,
522                } => v.push(STeXAnnot::IncludeProblem {
523                    filepath,
524                    archive,
525                    full_range,
526                    token_range,
527                    args,
528                }),
529                STeXToken::SetMetatheory {
530                    archive_range,
531                    path_range,
532                    module,
533                    token_range,
534                    full_range,
535                } => v.push(STeXAnnot::SetMetatheory {
536                    archive_range,
537                    path_range,
538                    module,
539                    token_range,
540                    full_range,
541                }),
542                STeXToken::Inputref {
543                    archive,
544                    filepath,
545                    token_range,
546                    full_range,
547                } => v.push(STeXAnnot::Inputref {
548                    archive,
549                    filepath,
550                    token_range,
551                    full_range,
552                }),
553                STeXToken::MHInput {
554                    archive,
555                    filepath,
556                    token_range,
557                    full_range,
558                } => v.push(STeXAnnot::MHInput {
559                    archive,
560                    filepath,
561                    token_range,
562                    full_range,
563                }),
564                STeXToken::Symdecl {
565                    uri,
566                    main_name_range,
567                    token_range,
568                    full_range,
569                    parsed_args,
570                } => v.push(STeXAnnot::Symdecl {
571                    uri,
572                    main_name_range,
573                    token_range,
574                    full_range,
575                    parsed_args: cont!(parsed_args),
576                }),
577                STeXToken::TextSymdecl {
578                    uri,
579                    main_name_range,
580                    full_range,
581                    parsed_args,
582                    token_range,
583                } => v.push(Self::TextSymdecl {
584                    uri,
585                    main_name_range,
586                    full_range,
587                    token_range,
588                    parsed_args: cont!(parsed_args),
589                }),
590                STeXToken::Definiens {
591                    uri,
592                    full_range,
593                    token_range,
594                    name_range,
595                } => v.push(Self::Definiens {
596                    uri,
597                    full_range,
598                    token_range,
599                    name_range,
600                }),
601                STeXToken::Defnotation { full_range } => {
602                    v.push(STeXAnnot::Defnotation { full_range })
603                }
604                STeXToken::Notation {
605                    uri,
606                    token_range,
607                    name_range,
608                    notation_args,
609                    full_range,
610                } => v.push(STeXAnnot::Notation {
611                    uri,
612                    token_range,
613                    name_range,
614                    full_range,
615                    notation_args: cont!(notation_args),
616                }),
617                STeXToken::Symdef {
618                    uri,
619                    main_name_range,
620                    token_range,
621                    full_range,
622                    parsed_args,
623                } => v.push(STeXAnnot::Symdef {
624                    uri,
625                    main_name_range,
626                    token_range,
627                    full_range,
628                    parsed_args: cont!(parsed_args),
629                }),
630                STeXToken::Vardef {
631                    name,
632                    main_name_range,
633                    token_range,
634                    full_range,
635                    parsed_args,
636                } => v.push(STeXAnnot::Vardef {
637                    name,
638                    main_name_range,
639                    token_range,
640                    full_range,
641                    parsed_args: cont!(parsed_args),
642                }),
643                STeXToken::Varseq {
644                    name,
645                    main_name_range,
646                    token_range,
647                    full_range,
648                    parsed_args,
649                } => v.push(STeXAnnot::Varseq {
650                    name,
651                    main_name_range,
652                    token_range,
653                    full_range,
654                    parsed_args: cont!(parsed_args),
655                }),
656                STeXToken::Symref {
657                    uri,
658                    full_range,
659                    token_range,
660                    name_range,
661                    text,
662                } => v.push(STeXAnnot::Symref {
663                    uri,
664                    full_range,
665                    token_range,
666                    name_range,
667                    text: (text.0, Self::from_tokens(text.1, None)),
668                }),
669                STeXToken::Precondition {
670                    uri,
671                    full_range,
672                    token_range,
673                    dim_range,
674                    symbol_range,
675                    dim,
676                } => v.push(STeXAnnot::Precondition {
677                    uri,
678                    full_range,
679                    token_range,
680                    dim_range,
681                    symbol_range,
682                    dim,
683                }),
684                STeXToken::Objective {
685                    uri,
686                    full_range,
687                    token_range,
688                    dim_range,
689                    symbol_range,
690                    dim,
691                } => v.push(STeXAnnot::Objective {
692                    uri,
693                    full_range,
694                    token_range,
695                    dim_range,
696                    symbol_range,
697                    dim,
698                }),
699                STeXToken::SymName {
700                    uri,
701                    full_range,
702                    token_range,
703                    name_range,
704                    mode: mod_,
705                } => v.push(STeXAnnot::SymName {
706                    uri,
707                    full_range,
708                    token_range,
709                    name_range,
710                    mode: mod_,
711                }),
712                STeXToken::Symuse {
713                    uri,
714                    full_range,
715                    token_range,
716                    name_range,
717                } => v.push(STeXAnnot::Symuse {
718                    uri,
719                    full_range,
720                    token_range,
721                    name_range,
722                }),
723                STeXToken::Paragraph {
724                    kind,
725                    full_range,
726                    name_range,
727                    symbol,
728                    parsed_args,
729                    children,
730                } => v.push(STeXAnnot::Paragraph {
731                    symbol,
732                    kind,
733                    full_range,
734                    name_range,
735                    parsed_args: cont!(parsed_args),
736                    children: Self::from_tokens(children, None),
737                }),
738                STeXToken::Problem {
739                    sub,
740                    full_range,
741                    name_range,
742                    parsed_args,
743                    children,
744                } => v.push(STeXAnnot::Problem {
745                    sub,
746                    full_range,
747                    name_range,
748                    parsed_args: cont!(parsed_args),
749                    children: Self::from_tokens(children, None),
750                }),
751                STeXToken::InlineParagraph {
752                    kind,
753                    full_range,
754                    token_range,
755                    children_range,
756                    symbol,
757                    parsed_args,
758                    children,
759                } => v.push(STeXAnnot::InlineParagraph {
760                    symbol,
761                    kind,
762                    full_range,
763                    token_range,
764                    children_range,
765                    parsed_args: cont!(parsed_args),
766                    children: Self::from_tokens(children, None),
767                }),
768                STeXToken::RenameDecl {
769                    uri,
770                    token_range,
771                    orig_range,
772                    name_range,
773                    macroname_range,
774                    full_range,
775                } => v.push(STeXAnnot::RenameDecl {
776                    uri,
777                    token_range,
778                    orig_range,
779                    name_range,
780                    macroname_range,
781                    full_range,
782                }),
783                STeXToken::Assign {
784                    uri,
785                    token_range,
786                    orig_range,
787                    full_range,
788                } => v.push(STeXAnnot::Assign {
789                    uri,
790                    token_range,
791                    orig_range,
792                    full_range,
793                }),
794                STeXToken::Vec(vi) => v.extend(Self::from_tokens(
795                    vi,
796                    if let Some(m) = modules.as_mut() {
797                        Some(*m)
798                    } else {
799                        None
800                    },
801                )),
802            }
803        }
804        v
805    }
806
807    #[must_use]
808    #[inline]
809    pub const fn range(&self) -> SourceRange<LSPLineCol> {
810        match self {
811            Self::Module { full_range, .. }
812            | Self::MathStructure { full_range, .. }
813            | Self::SemanticMacro { full_range, .. }
814            | Self::ImportModule { full_range, .. }
815            | Self::UseModule { full_range, .. }
816            | Self::SetMetatheory { full_range, .. }
817            | Self::Symdecl { full_range, .. }
818            | Self::Symdef { full_range, .. }
819            | Self::IncludeProblem { full_range, .. }
820            | Self::SymName { full_range, .. }
821            | Self::Symuse { full_range, .. }
822            | Self::Symref { full_range, .. }
823            | Self::Vardef { full_range, .. }
824            | Self::VariableMacro { full_range, .. }
825            | Self::Varseq { full_range, .. }
826            | Self::Notation { full_range, .. }
827            | Self::Svar { full_range, .. }
828            | Self::Definiens { full_range, .. }
829            | Self::Defnotation { full_range }
830            | Self::ConservativeExt { full_range, .. }
831            | Self::Paragraph { full_range, .. }
832            | Self::Problem { full_range, .. }
833            | Self::UseStructure { full_range, .. }
834            | Self::InlineParagraph { full_range, .. }
835            | Self::MorphismEnv { full_range, .. }
836            | Self::RenameDecl { full_range, .. }
837            | Self::Assign { full_range, .. }
838            | Self::Inputref { full_range, .. }
839            | Self::MHInput { full_range, .. }
840            | Self::InlineMorphism { full_range, .. }
841            | Self::Precondition { full_range, .. }
842            | Self::Objective { full_range, .. }
843            | Self::MHGraphics { full_range, .. }
844            | Self::TextSymdecl { full_range, .. } => *full_range,
845        }
846    }
847}
848
849pub enum AnnotIter<'a> {
850    Module(
851        std::iter::Chain<
852            SModuleArgIter<'a, LSPLineCol, STeXAnnot>,
853            std::slice::Iter<'a, STeXAnnot>,
854        >,
855    ),
856    InlineAss(InlineMorphAssIter<'a, LSPLineCol, STeXAnnot>),
857    Slice(std::slice::Iter<'a, STeXAnnot>),
858    Paragraph(std::iter::Chain<ParagraphArgIter<'a, STeXAnnot>, std::slice::Iter<'a, STeXAnnot>>),
859    Problem(std::iter::Chain<ProblemArgIter<'a, STeXAnnot>, std::slice::Iter<'a, STeXAnnot>>),
860    Structure(
861        std::iter::Chain<
862            MathStructureArgIter<'a, LSPLineCol, STeXAnnot>,
863            std::slice::Iter<'a, STeXAnnot>,
864        >,
865    ),
866    Symdecl(SymdeclArgIter<'a, LSPLineCol, STeXAnnot>),
867    TextSymdecl(TextSymdeclArgIter<'a, LSPLineCol, STeXAnnot>),
868    Notation(NotationArgIter<'a, LSPLineCol, STeXAnnot>),
869    Symdef(SymdefArgIter<'a, LSPLineCol, STeXAnnot>),
870    Vardef(VardefArgIter<'a, LSPLineCol, STeXAnnot>),
871}
872impl<'a> From<std::slice::Iter<'a, STeXAnnot>> for AnnotIter<'a> {
873    #[inline]
874    fn from(v: std::slice::Iter<'a, STeXAnnot>) -> Self {
875        Self::Slice(v)
876    }
877}
878impl<'a> Iterator for AnnotIter<'a> {
879    type Item = &'a STeXAnnot;
880    #[inline]
881    fn next(&mut self) -> Option<Self::Item> {
882        match self {
883            Self::Module(i) => i.next(),
884            Self::Structure(i) => i.next(),
885            Self::InlineAss(i) => i.next(),
886            Self::Paragraph(i) => i.next(),
887            Self::Problem(i) => i.next(),
888            Self::Symdecl(i) => i.next(),
889            Self::TextSymdecl(i) => i.next(),
890            Self::Notation(i) => i.next(),
891            Self::Symdef(i) => i.next(),
892            Self::Vardef(i) => i.next(),
893            Self::Slice(i) => i.next(),
894        }
895    }
896}
897
898impl TreeLike for STeXAnnot {
899    type Child<'a> = &'a Self;
900    type RefIter<'a> = AnnotIter<'a>;
901    fn children(&self) -> Option<Self::RefIter<'_>> {
902        match self {
903            Self::Module { opts, children, .. } => Some(AnnotIter::Module(
904                SModuleArgIter::new(opts).chain(children.iter()),
905            )),
906            Self::InlineMorphism { assignments, .. } => {
907                Some(AnnotIter::InlineAss(InlineMorphAssIter::new(assignments)))
908            }
909            Self::Paragraph {
910                parsed_args,
911                children,
912                ..
913            }
914            | Self::InlineParagraph {
915                parsed_args,
916                children,
917                ..
918            } => Some(AnnotIter::Paragraph(
919                ParagraphArgIter::new(parsed_args).chain(children.iter()),
920            )),
921            Self::Problem {
922                parsed_args,
923                children,
924                ..
925            } => Some(AnnotIter::Problem(
926                ProblemArgIter::new(parsed_args).chain(children.iter()),
927            )),
928            Self::Symdecl { parsed_args, .. } => {
929                Some(AnnotIter::Symdecl(SymdeclArgIter::new(parsed_args)))
930            }
931            Self::TextSymdecl { parsed_args, .. } => {
932                Some(AnnotIter::TextSymdecl(TextSymdeclArgIter::new(parsed_args)))
933            }
934            Self::Notation { notation_args, .. } => {
935                Some(AnnotIter::Notation(NotationArgIter::new(notation_args)))
936            }
937            Self::Symdef { parsed_args, .. } => {
938                Some(AnnotIter::Symdef(SymdefArgIter::new(parsed_args)))
939            }
940            Self::Vardef { parsed_args, .. } | Self::Varseq { parsed_args, .. } => {
941                Some(AnnotIter::Vardef(VardefArgIter::new(parsed_args)))
942            }
943            Self::MathStructure { children, opts, .. } => Some(AnnotIter::Structure(
944                MathStructureArgIter::new(opts).chain(children.iter()),
945            )),
946            Self::ConservativeExt { children, .. } | Self::MorphismEnv { children, .. } => {
947                Some(AnnotIter::Slice(children.iter()))
948            }
949            Self::SemanticMacro { .. }
950            | Self::VariableMacro { .. }
951            | Self::ImportModule { .. }
952            | Self::UseModule { .. }
953            | Self::SetMetatheory { .. }
954            | Self::Inputref { .. }
955            | Self::MHInput { .. }
956            | Self::SymName { .. }
957            | Self::Symref { .. }
958            | Self::Symuse { .. }
959            | Self::Svar { .. }
960            | Self::Definiens { .. }
961            | Self::Defnotation { .. }
962            | Self::UseStructure { .. }
963            | Self::Precondition { .. }
964            | Self::Objective { .. }
965            | Self::RenameDecl { .. }
966            | Self::IncludeProblem { .. }
967            | Self::MHGraphics { .. }
968            | Self::Assign { .. } => None,
969        }
970    }
971}
972
973impl TreeChild<STeXAnnot> for &STeXAnnot {
974    fn children<'a>(&self) -> Option<AnnotIter<'a>>
975    where
976        Self: 'a,
977    {
978        <STeXAnnot as TreeLike>::children(self)
979    }
980}
981
982#[derive(Copy, Clone, Debug, PartialEq, Eq)]
983pub enum DiagnosticLevel {
984    Error,
985    Warning,
986    Info,
987    Hint,
988}
989
990#[derive(PartialEq, Eq, Debug)]
991pub struct STeXDiagnostic {
992    pub level: DiagnosticLevel,
993    pub message: String,
994    pub range: SourceRange<LSPLineCol>,
995}
996
997#[must_use]
998pub fn quickparse<'a, S: STeXModuleStore>(
999    uri: &'a DocumentURI,
1000    source: &'a str,
1001    path: &'a Path,
1002    backend: &'a AnyBackend,
1003    store: S,
1004) -> STeXParseDataI {
1005    let mut diagnostics = VecSet::new();
1006    let mut modules = SmallVec::new();
1007    let err = |message, range, level| {
1008        diagnostics.insert(STeXDiagnostic {
1009            level,
1010            message,
1011            range,
1012        })
1013    };
1014    let mut parser = if S::FULL {
1015        LaTeXParser::with_rules(
1016            ParseStr::new(source),
1017            STeXParseState::new(Some(uri.archive_uri()), Some(path), uri, backend, store),
1018            err,
1019            LaTeXParser::default_rules()
1020                .into_iter()
1021                .chain(rules::all_rules()),
1022            LaTeXParser::default_env_rules()
1023                .into_iter()
1024                .chain(rules::all_env_rules()),
1025        )
1026    } else {
1027        LaTeXParser::with_rules(
1028            ParseStr::new(source),
1029            STeXParseState::new(Some(uri.archive_uri()), Some(path), uri, backend, store),
1030            err,
1031            LaTeXParser::default_rules()
1032                .into_iter()
1033                .chain(rules::declarative_rules()),
1034            LaTeXParser::default_env_rules()
1035                .into_iter()
1036                .chain(rules::declarative_env_rules()),
1037        )
1038    };
1039
1040    let annotations = STeXAnnot::from_tokens(&mut parser, Some(&mut modules));
1041
1042    let dependents = parser.state.dependencies;
1043    STeXParseDataI {
1044        annotations,
1045        diagnostics,
1046        modules,
1047        dependencies: dependents,
1048    }
1049}