1use super::{
2 Atom, DeclarationPtr, Literal, Moo,
3 comprehension::Comprehension,
4 declaration::DeclarationKind,
5 pretty::{
6 pretty_domain_letting_declaration, pretty_expressions_as_top_level,
7 pretty_value_letting_declaration, pretty_variable_declaration,
8 },
9 serde::RcRefCellAsInner,
10};
11use itertools::izip;
12use serde::{Deserialize, Serialize};
13use serde_with::serde_as;
14use uniplate::{Biplate, Tree, Uniplate};
15
16use crate::{bug, into_matrix_expr, metadata::Metadata};
17use std::{
18 cell::{Ref, RefCell, RefMut},
19 collections::VecDeque,
20 fmt::Display,
21 rc::Rc,
22};
23
24use super::{Expression, ReturnType, SymbolTable, types::Typeable};
25
26#[serde_as]
33#[derive(Clone, PartialEq, Eq, Debug, Serialize, Deserialize)]
34pub struct SubModel {
35 constraints: Moo<Expression>,
36 #[serde_as(as = "RcRefCellAsInner")]
37 symbols: Rc<RefCell<SymbolTable>>,
38}
39
40impl SubModel {
41 #[doc(hidden)]
46 pub(super) fn new_top_level() -> SubModel {
47 SubModel {
48 constraints: Moo::new(Expression::Root(Metadata::new(), vec![])),
49 symbols: Rc::new(RefCell::new(SymbolTable::new())),
50 }
51 }
52
53 pub fn new(parent: Rc<RefCell<SymbolTable>>) -> SubModel {
57 SubModel {
58 constraints: Moo::new(Expression::Root(Metadata::new(), vec![])),
59 symbols: Rc::new(RefCell::new(SymbolTable::with_parent(parent))),
60 }
61 }
62
63 pub fn symbols_ptr_unchecked(&self) -> &Rc<RefCell<SymbolTable>> {
68 &self.symbols
69 }
70
71 pub fn symbols_ptr_unchecked_mut(&mut self) -> &mut Rc<RefCell<SymbolTable>> {
76 &mut self.symbols
77 }
78
79 pub fn symbols(&self) -> Ref<SymbolTable> {
81 (*self.symbols).borrow()
82 }
83
84 pub fn symbols_mut(&mut self) -> RefMut<SymbolTable> {
86 (*self.symbols).borrow_mut()
87 }
88
89 pub fn root(&self) -> &Expression {
94 &self.constraints
95 }
96
97 pub fn root_mut_unchecked(&mut self) -> &mut Expression {
102 Moo::make_mut(&mut self.constraints)
103 }
104
105 pub fn replace_root(&mut self, new_root: Expression) -> Expression {
111 let Expression::Root(_, _) = new_root else {
112 tracing::error!(new_root=?new_root,"new_root is not an Expression::root");
113 panic!("new_root is not an Expression::Root");
114 };
115
116 std::mem::replace(self.root_mut_unchecked(), new_root)
118 }
119
120 pub fn constraints(&self) -> &Vec<Expression> {
122 let Expression::Root(_, constraints) = self.constraints.as_ref() else {
123 bug!("The top level expression in a submodel should be Expr::Root");
124 };
125
126 constraints
127 }
128
129 pub fn constraints_mut(&mut self) -> &mut Vec<Expression> {
131 let Expression::Root(_, constraints) = Moo::make_mut(&mut self.constraints) else {
132 bug!("The top level expression in a submodel should be Expr::Root");
133 };
134
135 constraints
136 }
137
138 pub fn replace_constraints(&mut self, new_constraints: Vec<Expression>) -> Vec<Expression> {
140 std::mem::replace(self.constraints_mut(), new_constraints)
141 }
142
143 pub fn add_constraint(&mut self, constraint: Expression) {
145 self.constraints_mut().push(constraint);
146 }
147
148 pub fn add_constraints(&mut self, constraints: Vec<Expression>) {
150 self.constraints_mut().extend(constraints);
151 }
152
153 pub fn add_symbol(&mut self, decl: DeclarationPtr) -> Option<()> {
156 self.symbols_mut().insert(decl)
157 }
158
159 pub fn into_single_expression(self) -> Expression {
166 let constraints = self.constraints().clone();
167 match constraints.len() {
168 0 => Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true))),
169 1 => constraints[0].clone(),
170 _ => Expression::And(Metadata::new(), Moo::new(into_matrix_expr![constraints])),
171 }
172 }
173}
174
175impl Typeable for SubModel {
176 fn return_type(&self) -> Option<super::ReturnType> {
177 Some(ReturnType::Bool)
178 }
179}
180
181impl Display for SubModel {
182 #[allow(clippy::unwrap_used)] fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
184 for (name, decl) in self.symbols().clone().into_iter_local() {
185 match &decl.kind() as &DeclarationKind {
186 DeclarationKind::DecisionVariable(_) => {
187 writeln!(
188 f,
189 "{}",
190 pretty_variable_declaration(&self.symbols(), &name).unwrap()
191 )?;
192 }
193 DeclarationKind::ValueLetting(_) => {
194 writeln!(
195 f,
196 "{}",
197 pretty_value_letting_declaration(&self.symbols(), &name).unwrap()
198 )?;
199 }
200 DeclarationKind::DomainLetting(_) => {
201 writeln!(
202 f,
203 "{}",
204 pretty_domain_letting_declaration(&self.symbols(), &name).unwrap()
205 )?;
206 }
207 DeclarationKind::Given(d) => {
208 writeln!(f, "given {name}: {d}")?;
209 }
210
211 DeclarationKind::RecordField(_) => {
212 writeln!(f)?;
214 }
216 }
217 }
218
219 writeln!(f, "\nsuch that\n")?;
220
221 writeln!(f, "{}", pretty_expressions_as_top_level(self.constraints()))?;
222
223 Ok(())
224 }
225}
226
227impl Uniplate for SubModel {
241 fn uniplate(&self) -> (Tree<Self>, Box<dyn Fn(Tree<Self>) -> Self>) {
242 let (expr_tree, expr_ctx) = <Expression as Biplate<SubModel>>::biplate(self.root());
245
246 let symtab_ptr = self.symbols();
247 let (symtab_tree, symtab_ctx) = <SymbolTable as Biplate<SubModel>>::biplate(&symtab_ptr);
248
249 let tree = Tree::Many(VecDeque::from([expr_tree, symtab_tree]));
250
251 let self2 = self.clone();
252 let ctx = Box::new(move |x| {
253 let Tree::Many(xs) = x else {
254 panic!();
255 };
256
257 let root = expr_ctx(xs[0].clone());
258 let symtab = symtab_ctx(xs[1].clone());
259
260 let mut self3 = self2.clone();
261
262 let Expression::Root(_, _) = root else {
263 bug!("root expression not root");
264 };
265
266 *self3.root_mut_unchecked() = root;
267
268 *self3.symbols_mut() = symtab;
269
270 self3
271 });
272
273 (tree, ctx)
274 }
275}
276
277impl Biplate<Expression> for SubModel {
278 fn biplate(&self) -> (Tree<Expression>, Box<dyn Fn(Tree<Expression>) -> Self>) {
279 let symtab_ptr = self.symbols();
281 let (symtab_tree, symtab_ctx) = <SymbolTable as Biplate<Expression>>::biplate(&symtab_ptr);
282
283 let tree = Tree::Many(VecDeque::from([
284 Tree::One(self.root().clone()),
285 symtab_tree,
286 ]));
287
288 let self2 = self.clone();
289 let ctx = Box::new(move |x| {
290 let Tree::Many(xs) = x else {
291 panic!();
292 };
293
294 let Tree::One(root) = xs[0].clone() else {
295 panic!();
296 };
297
298 let symtab = symtab_ctx(xs[1].clone());
299
300 let mut self3 = self2.clone();
301
302 let Expression::Root(_, _) = root else {
303 bug!("root expression not root");
304 };
305
306 *self3.root_mut_unchecked() = root;
307
308 *self3.symbols_mut() = symtab;
309
310 self3
311 });
312
313 (tree, ctx)
314 }
315}
316
317impl Biplate<SubModel> for SubModel {
318 fn biplate(&self) -> (Tree<SubModel>, Box<dyn Fn(Tree<SubModel>) -> Self>) {
319 (
320 Tree::One(self.clone()),
321 Box::new(move |x| {
322 let Tree::One(x) = x else {
323 panic!();
324 };
325 x
326 }),
327 )
328 }
329}
330
331impl Biplate<Atom> for SubModel {
332 fn biplate(&self) -> (Tree<Atom>, Box<dyn Fn(Tree<Atom>) -> Self>) {
333 let (expression_tree, rebuild_self) = <SubModel as Biplate<Expression>>::biplate(self);
342 let (expression_list, rebuild_expression_tree) = expression_tree.list();
343
344 let (atom_trees, reconstruct_exprs): (VecDeque<_>, VecDeque<_>) = expression_list
346 .iter()
347 .map(|e| <Expression as Biplate<Atom>>::biplate(e))
348 .unzip();
349
350 let tree = Tree::Many(atom_trees);
351 let ctx = Box::new(move |atom_tree: Tree<Atom>| {
352 let Tree::Many(atoms) = atom_tree else {
355 panic!();
356 };
357
358 assert_eq!(
359 atoms.len(),
360 reconstruct_exprs.len(),
361 "the number of children should not change when using Biplate"
362 );
363
364 let expression_list: VecDeque<Expression> = izip!(atoms, &reconstruct_exprs)
365 .map(|(atom, recons)| recons(atom))
366 .collect();
367
368 let expression_tree = rebuild_expression_tree(expression_list);
370
371 rebuild_self(expression_tree)
373 });
374
375 (tree, ctx)
376 }
377}
378
379impl Biplate<Comprehension> for SubModel {
380 fn biplate(
381 &self,
382 ) -> (
383 Tree<Comprehension>,
384 Box<dyn Fn(Tree<Comprehension>) -> Self>,
385 ) {
386 let (f1_tree, f1_ctx) = <_ as Biplate<Comprehension>>::biplate(&self.constraints);
387 let (f2_tree, f2_ctx) =
388 <SymbolTable as Biplate<Comprehension>>::biplate(&self.symbols.borrow());
389
390 let tree = Tree::Many(VecDeque::from([f1_tree, f2_tree]));
391 let self2 = self.clone();
392 let ctx = Box::new(move |x| {
393 let Tree::Many(xs) = x else {
394 panic!();
395 };
396
397 let root = f1_ctx(xs[0].clone());
398 let symtab = f2_ctx(xs[1].clone());
399
400 let mut self3 = self2.clone();
401
402 let Expression::Root(_, _) = &*root else {
403 bug!("root expression not root");
404 };
405
406 *self3.symbols_mut() = symtab;
407 self3.constraints = root;
408
409 self3
410 });
411
412 (tree, ctx)
413 }
414}