flams_ontology/content/
checking.rs

1use crate::{
2    uris::{ModuleURI, SymbolURI}, LocalBackend, MaybeResolved, Unchecked
3};
4
5use super::{
6    declarations::{
7        morphisms::Morphism,
8        structures::{Extension, MathStructure},
9        Declaration, OpenDeclaration
10    },
11    modules::NestedModule,
12};
13
14pub trait ModuleChecker: LocalBackend {
15    fn open(&mut self, elem: &mut OpenDeclaration<Unchecked>);
16    fn close(&mut self, elem: &mut Declaration);
17}
18
19enum Elem {
20    Extension(SymbolURI, SymbolURI),
21    NestedModule(SymbolURI),
22    MathStructure {
23        uri: SymbolURI,
24        macroname: Option<Box<str>>,
25    },
26    Morphism {
27        uri: SymbolURI,
28        domain: ModuleURI,
29        total: bool,
30    },
31}
32
33impl Elem {
34    fn close(self, v: Vec<Declaration>, checker: &mut impl ModuleChecker) -> Declaration {
35        match self {
36            Self::Extension(uri, target) => {
37                //println!("Require declaration {target}");
38                let target = MaybeResolved::resolve(target,|m| checker.get_declaration(m));
39                Declaration::Extension(Extension {
40                    uri,
41                    target,
42                    elements: v.into_boxed_slice(),
43                })
44            }
45            Self::NestedModule(uri) => {
46                //println!("Closing nested module {uri}");
47                Declaration::NestedModule(NestedModule {
48                    uri,
49                    elements: v.into_boxed_slice(),
50                })
51            }
52            Self::MathStructure { uri, macroname } => {
53                //println!("Closing structure {uri}");
54                Declaration::MathStructure(MathStructure {
55                    uri,
56                    macroname,
57                    elements: v.into_boxed_slice(),
58                })
59            }
60            Self::Morphism { uri, domain, total } => {
61                //println!("Require domain {domain}");
62                let domain = MaybeResolved::resolve(domain,|d| checker.get_module(d));
63                Declaration::Morphism(Morphism {
64                    uri,
65                    domain,
66                    total,
67                    elements: v.into_boxed_slice(),
68                })
69            }
70        }
71    }
72}
73
74pub(super) struct ModuleCheckIter<'a, Check: ModuleChecker> {
75    stack: Vec<(
76        Elem,
77        std::vec::IntoIter<OpenDeclaration<Unchecked>>,
78        Vec<Declaration>,
79    )>,
80    curr_in: std::vec::IntoIter<OpenDeclaration<Unchecked>>,
81    curr_out: Vec<Declaration>,
82    checker: &'a mut Check,
83    uri: &'a ModuleURI,
84}
85impl<Check: ModuleChecker> ModuleCheckIter<'_, Check> {
86    pub fn go(
87        elems: Vec<OpenDeclaration<Unchecked>>,
88        checker: &mut Check,
89        uri: &ModuleURI,
90    ) -> Vec<Declaration> {
91        let mut slf = ModuleCheckIter {
92            stack: Vec::new(),
93            curr_in: elems.into_iter(),
94            curr_out: Vec::new(),
95            checker,
96            uri,
97        };
98        loop {
99            while let Some(next) = slf.curr_in.next() {
100                slf.do_elem(next);
101            }
102            if let Some((e, curr_in, curr_out)) = slf.stack.pop() {
103                slf.curr_in = curr_in;
104                let dones = std::mem::replace(&mut slf.curr_out, curr_out);
105                let mut closed = e.close(dones, slf.checker);
106                slf.checker.close(&mut closed);
107                slf.curr_out.push(closed);
108            } else {
109                return slf.curr_out;
110            }
111        }
112    }
113
114    fn do_elem(&mut self, mut e: OpenDeclaration<Unchecked>) {
115        self.checker.open(&mut e);
116        match e {
117            OpenDeclaration::Import(uri) => {
118                //println!("Require import {uri}");
119                let m = if !uri.clone() == *self.uri {
120                    MaybeResolved::unresolved(uri)
121                } else {
122                    MaybeResolved::resolve(uri,|u| self.checker.get_module(u))
123                };
124                let mut m = Declaration::Import(m);
125                self.checker.close(&mut m);
126                self.curr_out.push(m);
127            }
128            OpenDeclaration::Symbol(s) => {
129                let mut m = Declaration::Symbol(s);
130                self.checker.close(&mut m);
131                self.curr_out.push(m);
132            }
133            OpenDeclaration::Extension(Extension {
134                target,
135                uri,
136                elements,
137            }) => {
138                let old_in = std::mem::replace(&mut self.curr_in, elements.into_iter());
139                let old_out = std::mem::take(&mut self.curr_out);
140                self.stack
141                    .push((Elem::Extension(uri, target), old_in, old_out));
142            }
143            OpenDeclaration::NestedModule(NestedModule { uri, elements }) => {
144                let old_in = std::mem::replace(&mut self.curr_in, elements.into_iter());
145                let old_out = std::mem::take(&mut self.curr_out);
146                self.stack.push((Elem::NestedModule(uri), old_in, old_out));
147            }
148            OpenDeclaration::MathStructure(MathStructure {
149                uri,
150                macroname,
151                elements,
152            }) => {
153                let old_in = std::mem::replace(&mut self.curr_in, elements.into_iter());
154                let old_out = std::mem::take(&mut self.curr_out);
155                self.stack
156                    .push((Elem::MathStructure { uri, macroname }, old_in, old_out));
157            }
158            OpenDeclaration::Morphism(Morphism {
159                uri,
160                domain,
161                total,
162                elements,
163            }) => {
164                let old_in = std::mem::replace(&mut self.curr_in, elements.into_iter());
165                let old_out = std::mem::take(&mut self.curr_out);
166                self.stack
167                    .push((Elem::Morphism { uri, domain, total }, old_in, old_out));
168            }
169        }
170    }
171}
flams_ontology/content/checking.rs

flams_ontology/content/
checking.rs
