simplicity/types/
incomplete.rs1use crate::dag::{Dag, DagLike, NoSharing};
12use crate::types::union_bound::PointerLike;
13
14use super::{Bound, BoundRef, Context};
15
16use std::fmt;
17use std::sync::Arc;
18
19#[derive(Clone)]
21pub enum Incomplete {
22 Free(String),
24 Cycle,
26 Sum(Arc<Incomplete>, Arc<Incomplete>),
28 Product(Arc<Incomplete>, Arc<Incomplete>),
30 Final(Arc<super::Final>),
32}
33
34impl DagLike for &'_ Incomplete {
35 type Node = Incomplete;
36 fn data(&self) -> &Incomplete {
37 self
38 }
39 fn as_dag_node(&self) -> Dag<Self> {
40 match *self {
41 Incomplete::Free(_) | Incomplete::Cycle | Incomplete::Final(_) => Dag::Nullary,
42 Incomplete::Sum(ref left, ref right) | Incomplete::Product(ref left, ref right) => {
43 Dag::Binary(left, right)
44 }
45 }
46 }
47}
48
49impl fmt::Debug for Incomplete {
50 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
51 fmt::Display::fmt(self, f)
52 }
53}
54
55impl fmt::Display for Incomplete {
56 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
57 let mut skip_next = false;
58 for data in self.verbose_pre_order_iter::<NoSharing>(None) {
59 if skip_next {
60 skip_next = false;
61 continue;
62 }
63
64 match (data.node, data.n_children_yielded) {
65 (Incomplete::Free(ref s), _) => f.write_str(s)?,
66 (Incomplete::Cycle, _) => f.write_str("<self-reference>")?,
67 (Incomplete::Sum(ref left, _), 0) if left.is_unit() => {
69 skip_next = true;
70 }
71 (Incomplete::Sum(ref left, _), 1) if left.is_unit() => {}
72 (Incomplete::Sum(ref left, _), 2) if left.is_unit() => {
73 f.write_str("?")?;
74 }
75 (Incomplete::Sum(..), 0) | (Incomplete::Product(..), 0) => {
77 if data.index > 0 {
78 f.write_str("(")?;
79 }
80 }
81 (Incomplete::Sum(..), 2) | (Incomplete::Product(..), 2) => {
82 if data.index > 0 {
83 f.write_str(")")?;
84 }
85 }
86 (Incomplete::Sum(..), _) => f.write_str(" + ")?,
87 (Incomplete::Product(..), _) => f.write_str(" × ")?,
88 (Incomplete::Final(ref fnl), _) => fnl.fmt(f)?,
89 }
90 }
91 Ok(())
92 }
93}
94
95impl Incomplete {
96 pub fn is_unit(&self) -> bool {
98 if let Incomplete::Final(ref fnl) = self {
99 fnl.is_unit()
100 } else {
101 false
102 }
103 }
104
105 pub(super) fn occurs_check<'brand>(
110 ctx: &Context<'brand>,
111 bound_ref: BoundRef<'brand>,
112 ) -> Option<Arc<Self>> {
113 use std::collections::HashSet;
114
115 use super::context::OccursCheckId;
116 use super::BoundRef;
117
118 enum OccursCheckStack<'brand> {
120 Iterate(BoundRef<'brand>),
121 Complete(OccursCheckId<'brand>),
122 }
123
124 let mut stack = vec![OccursCheckStack::Iterate(bound_ref)];
126 let mut in_progress = HashSet::new();
127 let mut completed = HashSet::new();
128 while let Some(top) = stack.pop() {
129 let bound = match top {
130 OccursCheckStack::Complete(id) => {
131 in_progress.remove(&id);
132 completed.insert(id);
133 continue;
134 }
135 OccursCheckStack::Iterate(b) => b,
136 };
137
138 let id = bound.occurs_check_id();
139 if completed.contains(&id) {
140 continue;
143 }
144 if !in_progress.insert(id) {
145 return Some(Arc::new(Self::Cycle));
147 }
148
149 stack.push(OccursCheckStack::Complete(id));
150 if let Some((_, child)) = (ctx, bound.shallow_clone()).right_child() {
151 stack.push(OccursCheckStack::Iterate(child));
152 }
153 if let Some((_, child)) = (ctx, bound).left_child() {
154 stack.push(OccursCheckStack::Iterate(child));
155 }
156 }
157
158 None
159 }
160
161 pub(super) fn from_bound_ref<'brand>(
162 ctx: &Context<'brand>,
163 bound_ref: BoundRef<'brand>,
164 ) -> Arc<Self> {
165 if let Some(err) = Self::occurs_check(ctx, bound_ref.shallow_clone()) {
166 return err;
167 }
168
169 let mut finalized = vec![];
172 for data in (ctx, bound_ref).post_order_iter::<NoSharing>() {
173 let bound_get = data.node.0.get(&data.node.1);
174 let final_data = match bound_get {
175 Bound::Free(s) => Incomplete::Free(s),
176 Bound::Complete(ref arc) => Incomplete::Final(Arc::clone(arc)),
177 Bound::Sum(..) => Incomplete::Sum(
178 Arc::clone(&finalized[data.left_index.unwrap()]),
179 Arc::clone(&finalized[data.right_index.unwrap()]),
180 ),
181 Bound::Product(..) => Incomplete::Product(
182 Arc::clone(&finalized[data.left_index.unwrap()]),
183 Arc::clone(&finalized[data.right_index.unwrap()]),
184 ),
185 };
186
187 finalized.push(Arc::new(final_data));
188 }
189 finalized.pop().unwrap()
190 }
191}