flams_ontology/
ftml.rs

1#[cfg(doc)]
2use crate::{
3    content::{
4        declarations::{
5            structures::{Extension, MathStructure},
6            symbols::Symbol,
7        },
8        modules::{Module, NestedModule},
9    },
10    narration::{
11        documents::Document,
12        paragraphs::{LogicalParagraph, ParagraphKind},
13        problems::Problem,
14        sections::{Section, SectionLevel},
15        DocumentElement::Slide,
16    },
17    uris::{Name, PathURI},
18};
19
20pub const PREFIX: &str = "data-ftml-";
21
22macro_rules! ftml {
23    ($l:literal) => {
24        concat!("data-ftml-", $l)
25    };
26}
27
28macro_rules! do_keys {
29    ( $count:literal: $(
30        $(#[$meta:meta])*
31        $tag:ident
32        $(-? $otp:ty;)?
33        $(@ $tp:ty)?
34        =$val:literal
35        $(+ $($other:ident),+ ;)?
36        $(>> $($children:ident),+ ;)?
37        $(&>> $($nchildren:ident),+ ;)?
38        $(<= $($parents:ident),+ ;)?
39        $(- $($req:ident),+ ;)?
40        $(! $only:literal;)?
41        $(-! $not:literal;)?
42    )*
43    ) => {
44
45        pub const NUM_RULES: usize = $count;
46
47        #[derive(Copy,Clone,PartialEq, Eq,Hash)]
48        pub enum FTMLKey {
49            $(
50                #[doc = concat!(
51                    "<div class=\"flams-syntax\">\n\n`data-ftml-",
52                        $val
53                        $(,"`[`=\"`<[",stringify!($otp),"]>`\"`]`")?
54                        $(,"=\"`<[",stringify!($tp),"]>`\"")?
55                        ,"`"
56                        $(,
57                            "\n\nAdditional attributes: " $(,
58                                "[" ,stringify!($other),"](FTMLKey::",stringify!($other), "), "
59                            )*
60                            ,""
61                        )?
62                        $(,
63                            "\n\nChild nodes: " $(,
64                                "[" ,stringify!($children),"](FTMLKey::",stringify!($children), "), "
65                            )*
66                            ,""
67                        )?
68                        $(,
69                            "\n\n</div><div class=\"flams-syntax\"><div></div>\n\nChild nodes: " $(,
70                                "[" ,stringify!($nchildren),"](FTMLKey::",stringify!($nchildren), "), "
71                            )*
72                            ,""
73                        )?
74                        $(,
75                            "\n\nAttribute of: " $(,
76                                "[" ,stringify!($req),"](FTMLKey::",stringify!($req), "), "
77                            )*
78                            ,""
79                        )?
80                        $(,
81                            "\n\nOnly allowed in: " $(,
82                                "[" ,stringify!($parents),"](FTMLKey::",stringify!($parents), "), "
83                            )*
84                            ,""
85                        )?
86                    ,"\n\n</div>\n\n"
87                    $(
88                        , "<div class=\"warning\">\n\n*Only allowed "
89                        , $only,
90                        "*\n\n</div>\n\n"
91                    )?
92                    $(
93                        , "<div class=\"warning\">\n\n*Not allowed "
94                        , $not,
95                        "*\n\n</div>\n\n"
96                    )?
97                )]
98                $(#[$meta])*
99                $tag
100            ),*
101        }
102
103        paste::paste! {
104            mod attrstrings {$(
105                pub const [<$tag:snake:upper>]:&'static str
106                    = ftml!($val);
107            )*}
108            impl FTMLKey {
109                #[must_use]#[inline]
110                pub const fn as_str(self) -> &'static str {
111                    match self {$(
112                        Self::$tag => $val
113                    ),*}
114                }
115
116                #[must_use]#[inline]
117                pub const fn attr_name(self) -> &'static str {
118                    match self {$(
119                        Self::$tag => attrstrings::[<$tag:snake:upper>]
120                    ),*}
121                }
122            }
123        }
124    }
125}
126
127do_keys! {119:
128
129    /// Denotes a new [Section]. The given [SectionLevel] is only a sanity check;
130    /// the actual level is determined by the occurrence within a [Document].
131    Section                     @ SectionLevel  = "section"         + Id; -!"in [LogicalParagraph]s, [Problem]s or [Slide]s";
132
133    /// Denotes a new [LogicalParagraph] of [ParagraphKind::Definition]
134    /// for the given [Symbol]s using the given styles.
135    Definition                              = "definition"          + Id,Inline,Fors,Styles; &>> Definiens, Definiendum;
136    /// Denotes a new [LogicalParagraph] of [ParagraphKind::Assertion] (Theorems, Lemmata,
137    /// Axioms, etc.) for the given [Symbol]s using the given styles.
138    Assertion                               = "assertion"           + Id,Inline,Fors,Styles;
139    /// Denotes a new [LogicalParagraph] of [ParagraphKind::Example] (this includes counterexamples)
140    /// for the given [Symbol]s using the given styles.
141    Example                                 = "example"             + Id,Inline,Fors,Styles;
142    /// Denotes a new [LogicalParagraph] of [ParagraphKind::Paragraph]
143    /// for the given [Symbol]s using the given styles.
144    Paragraph                               = "paragraph"           + Id,Inline,Fors,Styles;
145
146    /// Denotes a new [Problem] with [`sub_problem`](Problem::sub_problem)`=false`
147    Problem                                 = "problem"             + Id,Styles,Autogradable,ProblemPoints ;
148    /// Denotes a new [Problem] with [`sub_problem`](Problem::sub_problem)`=true`
149    SubProblem                              = "subproblem"          + Id,Styles,Autogradable,ProblemPoints ;
150
151    /// Denotes a [Slide], implying that the [Document] is (or contains in some sense)
152    /// a presentation.
153    Slide                                   = "slide"               + Id;    -!"in [LogicalParagraph]s, [Problem]s or [Slide]s";
154
155
156    // --------------------------------------------------------------------------------
157
158    /// A (possibly empty) node that, when being rendered, should be replaced by the
159    /// current slide number.
160    SlideNumber                 = "slide-number"            !"in [Slide]s";
161
162    // ------------------------------------------------------------------------------------
163
164    /// Denotes a new [Module] (or [NestedModule]) with the given [Name] in the
165    /// current [Namespace](PathURI).
166    Module                      @ String        = "module"              + Metatheory, Signature;
167
168    /// Denotes a new [MathStructure] or [Extension] with the given [Name].
169    MathStructure               @ String        = "feature-structure"   + Macroname; !"in [Module]s";
170
171    /// <div class="flams-wip">TODO</div>
172    Morphism                                    = "feature-morphism"
173
174    Proof                                   = "proof"               + Id,Inline,Fors,Styles,ProofHide;
175    SubProof                                = "subproof"            + Id,Inline,Fors,Styles,ProofHide;
176
177
178
179    Style                       = "style"
180    Counter                     = "counter"
181    CounterParent               = "counter-parent"
182
183    DocTitle                    = "doctitle"
184    Title                       = "title"
185    ProofTitle                  = "prooftitle"
186    SubproofTitle               = "subprooftitle"
187
188    Symdecl                     = "symdecl"
189    Vardef                      = "vardef"
190    Varseq                      = "varseq"
191
192    Notation                    = "notation"
193    NotationComp                = "notationcomp"
194    NotationOpComp              = "notationopcomp"
195    Definiendum                 = "definiendum"         <= Definition, Paragraph, Assertion;
196
197    Type                        = "type"
198    Conclusion                  = "conclusion"
199    Definiens                   = "definiens"           <= Definition, Paragraph, Assertion;
200    Rule                        = "rule"
201
202    ArgSep                      = "argsep"
203    ArgMap                      = "argmap"
204    ArgMapSep                   = "argmap-sep"
205
206    Term                        = "term"
207    Arg                         = "arg"
208    HeadTerm                    = "headterm"
209
210    ImportModule                = "import"
211    UseModule                   = "usemodule"
212    InputRef                    = "inputref"
213
214    SetSectionLevel             = "sectionlevel"
215    SkipSection                 = "skipsection"
216
217
218    ProofMethod                 = "proofmethod"
219    ProofSketch                 = "proofsketch"
220    ProofTerm                   = "proofterm"
221    ProofBody                   = "proofbody"
222    ProofAssumption             = "spfassumption"
223    ProofStep                   = "spfstep"
224    ProofStepName               = "stepname"
225    ProofEqStep                 = "spfeqstep"
226    ProofPremise                = "premise"
227    ProofConclusion             = "spfconclusion"
228
229    PreconditionDimension       = "preconditiondimension"
230    PreconditionSymbol          = "preconditionsymbol"
231    ObjectiveDimension          = "objectivedimension"
232    ObjectiveSymbol             = "objectivesymbol"
233    AnswerClass                 = "answerclass"
234    AnswerClassPts              = "answerclass-pts"
235    AnswerclassFeedback         = "answerclass-feedback"
236    ProblemMinutes              = "problemminutes"
237    ProblemMultipleChoiceBlock  = "multiple-choice-block"
238    ProblemSingleChoiceBlock    = "single-choice-block"
239    ProblemChoice               = "problem-choice"
240    ProblemChoiceVerdict        = "problem-choice-verdict"
241    ProblemChoiceFeedback       = "problem-choice-feedback"
242    ProblemFillinsol            = "fillinsol"
243    ProblemFillinsolWidth       = "fillinsol-width"
244    ProblemFillinsolCase        = "fillin-case"
245    ProblemFillinsolCaseValue   = "fillin-case-value"
246    ProblemFillinsolCaseVerdict = "fillin-case-verdict"
247    ProblemSolution            = "solution"
248    ProblemHint                = "problemhint"
249    ProblemNote                 = "problemnote"
250    ProblemGradingNote         = "problemgnote"
251
252    Comp                        = "comp"
253    VarComp                     = "varcomp"
254    MainComp                    = "maincomp"
255    DefComp                     = "defcomp"
256
257    Invisible                   = "invisible"
258
259    IfInputref                  = "ifinputref"
260    ReturnType                  = "returntype"
261    ArgTypes                    = "argtypes"
262
263    SRef                        = "sref"
264    SRefIn                      = "srefin"
265    Slideshow                   = "slideshow"
266    SlideshowSlide              = "slideshow-slide"
267    CurrentSectionLevel         = "currentsectionlevel"
268    Capitalize                  = "capitalize"
269
270    Assign                      = "assign"
271    Rename                      = "rename"
272    RenameTo                    = "to"
273    AssignMorphismFrom          = "assignmorphismfrom"
274    AssignMorphismTo            = "assignmorphismto"
275
276    AssocType                   = "assoctype"
277    ArgumentReordering          = "reorderargs"
278    ArgNum                      = "argnum"
279    Bind                        = "bind"
280    MorphismDomain              = "domain"
281    MorphismTotal               = "total"
282    ArgMode                     = "argmode"
283    NotationId                  = "notationid"
284    Head                        = "head"
285    Language                    = "language"
286    /// The metatheory of a module, that provides the formal "language" the module
287    /// is in
288    Metatheory                              = "metatheory"      - Module;
289    Signature                               = "signature"       - Module;
290    Args                        = "args"
291    ProblemPoints               = "problempoints"               - Problem, SubProblem;
292    Autogradable                = "autogradable"                - Problem, SubProblem;
293    ProofHide                   = "proofhide"                   - Proof,SubProof;
294    Macroname                   = "macroname"                   - MathStructure;
295    Inline                      = "inline"                      - Definition, Paragraph, Assertion, Example, Problem, SubProblem;
296    Fors                        = "fors"                        - Definition, Paragraph, Assertion, Example, Proof, SubProof;
297    Id                          = "id"                          - Section,Definition, Paragraph, Assertion, Example, Proof, SubProof, Problem, SubProblem, Slide;
298    NotationFragment            = "notationfragment"
299    Precedence                  = "precedence"
300    Role                        = "role"
301    Styles                      = "styles"
302    Argprecs                    = "argprecs"
303}
304
305impl std::fmt::Display for FTMLKey {
306    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
307        write!(f, "{}", self.as_str())
308    }
309}
310
311impl std::fmt::Debug for FTMLKey {
312    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
313        write!(f, "{}", self.attr_name())
314    }
315}
flams_ontology/ftml.rs

flams_ontology/
ftml.rs
