simplicity/node/
hiding.rs

1use crate::node::{
2    CoreConstructible, DisconnectConstructible, JetConstructible, WitnessConstructible,
3};
4use crate::types::{Context, Error};
5use crate::{Cmr, FailEntropy, HasCmr, Word};
6
7/// Wrapper that allows a node to be "hidden" during program construction.
8///
9/// ## Program construction
10///
11/// When a program is constructed in post-order,
12/// the parent node is created based on its children.
13/// We use this fact to introduce special branching logic:
14///
15/// 1. A `case` node with a left "hidden" child and a right non-hidden child becomes `assertr`.
16/// 2. A `case` node with a left non-hidden child and a right "hidden" child becomes `assertl`.
17/// 3. Otherwise, any node with "hidden" children becomes itself "hidden" with an updated CMR.
18/// 4. Any node with non-hidden children remains unchanged.
19///
20/// The program can be extracted from the wrapper when construction is finished.
21/// The program is invalid if the root node is "hidden".
22///
23/// ## Wrapping
24///
25/// A node can be wrapped via [`Hiding::from`] to add hiding support.
26/// A wrapped node can be converted into a "hidden" node via [`Hiding::hide`].
27/// Finally, a "hidden" node can be manually created via [`Hiding::hidden`].
28///
29/// ## Virtual hidden nodes
30///
31/// The wrapper merely _simulates_ hidden nodes.
32/// At no point are actual hidden nodes created.
33/// To stress this fact, I write "hidden" in quotation marks.
34#[derive(Clone, Debug, Eq, PartialEq)]
35pub struct Hiding<'brand, N> {
36    result: HidingResult<N>,
37    /// Inference context for program construction.
38    ///
39    /// Even a "hidden" node needs an inference context
40    /// because the context may be queried via [`CoreConstructible::inference_context`].
41    /// When a "hidden" node is converted into an assertion via the
42    /// [`CoreConstructible::case`] constructor, this context is required to build the case node.
43    /// For soundness, the same context should be returned for all nodes of the same program.
44    ctx: Context<'brand>,
45}
46
47type HidingResult<N> = Result<N, Cmr>;
48
49impl<'brand, N> Hiding<'brand, N> {
50    /// Create a "hidden" node with the given CMR.
51    ///
52    /// To enable the construction of possible parent nodes,
53    /// the inference context of the current program must be passed.
54    pub const fn hidden(cmr: Cmr, ctx: Context<'brand>) -> Self {
55        // # Soundness
56        // The hidden node introduces no type variables.
57        Self {
58            result: Err(cmr),
59            ctx,
60        }
61    }
62
63    fn hidden_cloned_ctx(&self, cmr: Cmr) -> Self {
64        Self {
65            result: Err(cmr),
66            ctx: self.ctx.shallow_clone(),
67        }
68    }
69
70    /// Access the non-hidden node inside in the wrapper.
71    ///
72    /// Return `None` if the wrapped node is "hidden".
73    pub fn as_node(&self) -> Option<&N> {
74        self.result.as_ref().ok()
75    }
76
77    /// Consume the wrapper and return the non-hidden node that was inside.
78    ///
79    /// Return `None` if the wrapped node is "hidden".
80    pub fn get_node(self) -> Option<N> {
81        self.result.ok()
82    }
83}
84
85impl<N: HasCmr> Hiding<'_, N> {
86    /// Ensure that the wrapped node is "hidden".
87    /// Convert non-hidden nodes into "hidden" nodes with the same CMR.
88    pub fn hide(self) -> Self {
89        // # Soundness
90        // Hiding a node means converting it into its CMR.
91        // The node's type variables remain in the inference context.
92        //
93        // The type variables of a "hidden" child don't influence the construction of a parent,
94        // because merely the child's CMR is passed to the parent constructor.
95        // A CMR has no connection to any type variables.
96        //
97        // Hiding a node creates a CMR that is independent from the original node.
98        // The CMR can be used in one part of the program
99        // while the node itself is used in a different part.
100        match self.result {
101            Ok(node) => Self::hidden(node.cmr(), self.ctx),
102            Err(..) => self,
103        }
104    }
105}
106
107impl<N: HasCmr> HasCmr for Hiding<'_, N> {
108    fn cmr(&self) -> Cmr {
109        match &self.result {
110            Ok(node) => node.cmr(),
111            Err(cmr) => *cmr,
112        }
113    }
114}
115
116// We need `N: CoreConstructible` to access the inference context.
117// Because of this, implementations of `{Jet, Disconnect, Witness}Constructible`
118// for `Hiding<N>` require `N: CoreConstructible`.
119impl<'brand, N: CoreConstructible<'brand>> From<N> for Hiding<'brand, N> {
120    fn from(node: N) -> Self {
121        Self {
122            ctx: node.inference_context().shallow_clone(),
123            result: Ok(node),
124        }
125    }
126}
127
128// # Soundness
129// See [`Hiding::hide`].
130impl<'brand, N: CoreConstructible<'brand> + HasCmr> CoreConstructible<'brand>
131    for Hiding<'brand, N>
132{
133    fn iden(inference_context: &Context<'brand>) -> Self {
134        N::iden(inference_context).into()
135    }
136
137    fn unit(inference_context: &Context<'brand>) -> Self {
138        N::unit(inference_context).into()
139    }
140
141    fn injl(child: &Self) -> Self {
142        match &child.result {
143            Ok(child) => N::injl(child).into(),
144            Err(cmr) => child.hidden_cloned_ctx(Cmr::injl(*cmr)),
145        }
146    }
147
148    fn injr(child: &Self) -> Self {
149        match &child.result {
150            Ok(child) => N::injr(child).into(),
151            Err(cmr) => child.hidden_cloned_ctx(Cmr::injr(*cmr)),
152        }
153    }
154
155    fn take(child: &Self) -> Self {
156        match &child.result {
157            Ok(child) => N::take(child).into(),
158            Err(cmr) => child.hidden_cloned_ctx(Cmr::take(*cmr)),
159        }
160    }
161
162    fn drop_(child: &Self) -> Self {
163        match &child.result {
164            Ok(child) => N::drop_(child).into(),
165            Err(cmr) => child.hidden_cloned_ctx(Cmr::drop(*cmr)),
166        }
167    }
168
169    fn comp(left: &Self, right: &Self) -> Result<Self, Error> {
170        match (&left.result, &right.result) {
171            (Ok(left), Ok(right)) => N::comp(left, right).map(Self::from),
172            _ => Ok(left.hidden_cloned_ctx(Cmr::comp(left.cmr(), right.cmr()))),
173        }
174    }
175
176    fn case(left: &Self, right: &Self) -> Result<Self, Error> {
177        match (&left.result, &right.result) {
178            (Ok(left), Ok(right)) => N::case(left, right).map(Self::from),
179            (Err(left), Ok(right)) => N::assertr(*left, right).map(Self::from),
180            (Ok(left), Err(right)) => N::assertl(left, *right).map(Self::from),
181            _ => Ok(left.hidden_cloned_ctx(Cmr::case(left.cmr(), right.cmr()))),
182        }
183    }
184
185    fn assertl(left: &Self, right: Cmr) -> Result<Self, Error> {
186        match &left.result {
187            Ok(left) => N::assertl(left, right).map(Self::from),
188            _ => Ok(left.hidden_cloned_ctx(Cmr::case(left.cmr(), right))),
189        }
190    }
191
192    fn assertr(left: Cmr, right: &Self) -> Result<Self, Error> {
193        match &right.result {
194            Ok(right) => N::assertr(left, right).map(Self::from),
195            _ => Ok(right.hidden_cloned_ctx(Cmr::case(left, right.cmr()))),
196        }
197    }
198
199    fn pair(left: &Self, right: &Self) -> Result<Self, Error> {
200        match (&left.result, &right.result) {
201            (Ok(left), Ok(right)) => N::pair(left, right).map(Self::from),
202            _ => Ok(left.hidden_cloned_ctx(Cmr::pair(left.cmr(), right.cmr()))),
203        }
204    }
205
206    fn fail(inference_context: &Context<'brand>, entropy: FailEntropy) -> Self {
207        N::fail(inference_context, entropy).into()
208    }
209
210    fn const_word(inference_context: &Context<'brand>, word: Word) -> Self {
211        N::const_word(inference_context, word).into()
212    }
213
214    fn inference_context(&self) -> &Context<'brand> {
215        &self.ctx
216    }
217}
218
219impl<'brand, J, N> JetConstructible<'brand, J> for Hiding<'brand, N>
220where
221    N: JetConstructible<'brand, J> + CoreConstructible<'brand>,
222{
223    fn jet(inference_context: &Context<'brand>, jet: J) -> Self {
224        N::jet(inference_context, jet).into()
225    }
226}
227
228impl<'brand, X, N> DisconnectConstructible<'brand, Option<X>> for Hiding<'brand, N>
229where
230    N: DisconnectConstructible<'brand, Option<X>> + CoreConstructible<'brand> + HasCmr,
231{
232    fn disconnect(left: &Self, right: &Option<X>) -> Result<Self, Error> {
233        match &left.result {
234            Ok(left) => N::disconnect(left, right).map(Self::from),
235            Err(..) => Ok(left.hidden_cloned_ctx(Cmr::disconnect(left.cmr()))),
236        }
237    }
238}
239
240impl<'brand, W, N> WitnessConstructible<'brand, W> for Hiding<'brand, N>
241where
242    N: WitnessConstructible<'brand, W> + CoreConstructible<'brand>,
243{
244    fn witness(inference_context: &Context<'brand>, witness: W) -> Self {
245        N::witness(inference_context, witness).into()
246    }
247}