flux_infer/fixpoint_encoding/
decoding.rs

1use flux_middle::{
2    big_int::BigInt,
3    rty::{self, EarlyReftParam, InternalFuncKind, List, SpecFuncKind},
4};
5use flux_rustc_bridge::lowering::Lower;
6use itertools::Itertools;
7
8use super::{ConstKey, FixpointCtxt, fixpoint};
9
10impl<'genv, 'tcx, Tag> FixpointCtxt<'genv, 'tcx, Tag>
11where
12    Tag: std::hash::Hash + Eq + Copy,
13{
14    #[allow(dead_code)]
15    pub(crate) fn fixpoint_to_expr(
16        &self,
17        fexpr: &fixpoint::Expr,
18    ) -> Result<rty::Expr, FixpointParseError> {
19        match fexpr {
20            fixpoint::Expr::Constant(constant) => {
21                let c = match constant {
22                    fixpoint::Constant::Numeral(num) => rty::Constant::Int(BigInt::from(*num)),
23                    fixpoint::Constant::Real(dec) => rty::Constant::Real(rty::Real(*dec)),
24                    fixpoint::Constant::Boolean(b) => rty::Constant::Bool(*b),
25                    fixpoint::Constant::String(s) => rty::Constant::Str(s.0),
26                    fixpoint::Constant::BitVec(bv, size) => rty::Constant::BitVec(*bv, *size),
27                };
28                Ok(rty::Expr::constant(c))
29            }
30            fixpoint::Expr::Var(fvar) => {
31                match fvar {
32                    fixpoint::Var::Underscore => {
33                        unreachable!("Underscore should not appear in exprs")
34                    }
35                    fixpoint::Var::Global(global_var, _) => {
36                        if let Some(const_key) = self.ecx.const_env.const_map_rev.get(global_var) {
37                            match const_key {
38                                ConstKey::Uif(def_id) => {
39                                    Ok(rty::Expr::global_func(SpecFuncKind::Uif(*def_id)))
40                                }
41                                ConstKey::RustConst(def_id) => Ok(rty::Expr::const_def_id(*def_id)),
42                                ConstKey::Alias(_flux_id, _args) => {
43                                    unreachable!("Should be special-cased as the head of an app")
44                                }
45                                ConstKey::Lambda(lambda) => Ok(rty::Expr::abs(lambda.clone())),
46                                ConstKey::PrimOp(bin_op) => {
47                                    Ok(rty::Expr::internal_func(InternalFuncKind::Rel(
48                                        bin_op.clone(),
49                                    )))
50                                }
51                                ConstKey::Cast(_sort, _sort1) => {
52                                    unreachable!(
53                                        "Should be specially handled as the head of a function app."
54                                    )
55                                }
56                            }
57                        } else {
58                            Err(FixpointParseError::NoGlobalVar(*global_var))
59                        }
60                    }
61                    fixpoint::Var::Local(fname) => {
62                        if let Some(var) = self.ecx.local_var_env.reverse_map.get(fname) {
63                            Ok(rty::Expr::var(*var))
64                        } else {
65                            Err(FixpointParseError::NoLocalVar(*fname))
66                        }
67                    }
68                    fixpoint::Var::DataCtor(adt_id, variant_idx) => {
69                        let def_id = self.scx.adt_sorts[adt_id.as_usize()];
70                        Ok(rty::Expr::ctor_enum(def_id, *variant_idx))
71                    }
72                    fixpoint::Var::TupleCtor { .. }
73                    | fixpoint::Var::TupleProj { .. }
74                    | fixpoint::Var::DataProj { .. }
75                    | fixpoint::Var::UIFRel(_) => {
76                        unreachable!(
77                            "Trying to convert an atomic var, but reached a var that should only occur as the head of an app (and be special-cased in conversion as a result)"
78                        )
79                    }
80                    fixpoint::Var::Param(EarlyReftParam { index, name }) => {
81                        Ok(rty::Expr::early_param(*index, *name))
82                    }
83                    fixpoint::Var::ConstGeneric(const_generic) => {
84                        Ok(rty::Expr::const_generic(*const_generic))
85                    }
86                }
87            }
88            fixpoint::Expr::App(fhead, fargs) => {
89                match &**fhead {
90                    fixpoint::Expr::Var(fixpoint::Var::TupleProj { arity, field }) => {
91                        if fargs.len() == 1 {
92                            let earg = self.fixpoint_to_expr(&fargs[0])?;
93                            Ok(rty::Expr::field_proj(
94                                earg,
95                                rty::FieldProj::Tuple { arity: *arity, field: *field },
96                            ))
97                        } else {
98                            Err(FixpointParseError::ProjArityMismatch(fargs.len()))
99                        }
100                    }
101                    fixpoint::Expr::Var(fixpoint::Var::DataProj { adt_id, field }) => {
102                        if fargs.len() == 1 {
103                            let earg = self.fixpoint_to_expr(&fargs[0])?;
104                            Ok(rty::Expr::field_proj(
105                                earg,
106                                rty::FieldProj::Adt {
107                                    def_id: self.scx.adt_sorts[adt_id.as_usize()],
108                                    field: *field,
109                                },
110                            ))
111                        } else {
112                            Err(FixpointParseError::ProjArityMismatch(fargs.len()))
113                        }
114                    }
115                    fixpoint::Expr::Var(fixpoint::Var::TupleCtor { arity }) => {
116                        if fargs.len() == *arity {
117                            let eargs = fargs
118                                .iter()
119                                .map(|farg| self.fixpoint_to_expr(farg))
120                                .try_collect()?;
121                            Ok(rty::Expr::tuple(eargs))
122                        } else {
123                            Err(FixpointParseError::TupleCtorArityMismatch(*arity, fargs.len()))
124                        }
125                    }
126                    fixpoint::Expr::Var(fixpoint::Var::UIFRel(fbinrel)) => {
127                        if fargs.len() == 2 {
128                            let e1 = self.fixpoint_to_expr(&fargs[0])?;
129                            let e2 = self.fixpoint_to_expr(&fargs[1])?;
130                            let binrel = match fbinrel {
131                                fixpoint::BinRel::Eq => rty::BinOp::Eq,
132                                fixpoint::BinRel::Ne => rty::BinOp::Ne,
133                                // FIXME: (ck) faked sort information
134                                //
135                                // This needs to be a sort that goes to the UIFRel
136                                // case in fixpoint conversion. Again, if we actually
137                                // need to inspect the sorts this will die unless the
138                                // arguments are actually Strs.
139                                fixpoint::BinRel::Gt => rty::BinOp::Gt(rty::Sort::Str),
140                                fixpoint::BinRel::Ge => rty::BinOp::Ge(rty::Sort::Str),
141                                fixpoint::BinRel::Lt => rty::BinOp::Lt(rty::Sort::Str),
142                                fixpoint::BinRel::Le => rty::BinOp::Le(rty::Sort::Str),
143                            };
144                            Ok(rty::Expr::binary_op(binrel, e1, e2))
145                        } else {
146                            Err(FixpointParseError::UIFRelArityMismatch(fargs.len()))
147                        }
148                    }
149                    fixpoint::Expr::Var(fixpoint::Var::Global(global_var, _)) => {
150                        if let Some(const_key) = self.ecx.const_env.const_map_rev.get(global_var) {
151                            match const_key {
152                                // NOTE: Only a few of these are meaningfully needed,
153                                // e.g. ConstKey::Alias because the rty Expr has its
154                                // args as a part of it.
155                                ConstKey::PrimOp(bin_op) => {
156                                    if fargs.len() != 2 {
157                                        Err(FixpointParseError::PrimOpArityMismatch(fargs.len()))
158                                    } else {
159                                        Ok(rty::Expr::prim_val(
160                                            bin_op.clone(),
161                                            self.fixpoint_to_expr(&fargs[0])?,
162                                            self.fixpoint_to_expr(&fargs[1])?,
163                                        ))
164                                    }
165                                }
166                                ConstKey::Cast(sort1, sort2) => {
167                                    if fargs.len() != 1 {
168                                        Err(FixpointParseError::CastArityMismatch(fargs.len()))
169                                    } else {
170                                        Ok(rty::Expr::cast(
171                                            sort1.clone(),
172                                            sort2.clone(),
173                                            self.fixpoint_to_expr(&fargs[0])?,
174                                        ))
175                                    }
176                                }
177                                ConstKey::Alias(assoc_id, generic_args) => {
178                                    let lowered_args: flux_rustc_bridge::ty::GenericArgs =
179                                        generic_args.lower(self.genv.tcx()).unwrap();
180                                    let generic_args = rty::refining::Refiner::default_for_item(
181                                        self.genv,
182                                        assoc_id.parent(),
183                                    )
184                                    .unwrap()
185                                    .refine_generic_args(assoc_id.parent(), &lowered_args)
186                                    .unwrap();
187                                    let alias_reft =
188                                        rty::AliasReft { assoc_id: *assoc_id, args: generic_args };
189                                    let args = fargs
190                                        .iter()
191                                        .map(|farg| self.fixpoint_to_expr(farg))
192                                        .try_collect()?;
193                                    Ok(rty::Expr::alias(alias_reft, args))
194                                }
195                                ConstKey::Uif(..)
196                                | ConstKey::RustConst(..)
197                                | ConstKey::Lambda(..) => {
198                                    // These should be treated as a normal app.
199                                    self.fixpoint_app_to_expr(fhead, fargs)
200                                }
201                            }
202                        } else {
203                            Err(FixpointParseError::NoGlobalVar(*global_var))
204                        }
205                    }
206                    fhead => self.fixpoint_app_to_expr(fhead, fargs),
207                }
208            }
209            fixpoint::Expr::Neg(fexpr) => {
210                let e = self.fixpoint_to_expr(fexpr)?;
211                Ok(rty::Expr::neg(&e))
212            }
213            fixpoint::Expr::BinaryOp(fbinop, boxed_args) => {
214                let binop = match fbinop {
215                    // FIXME: (ck) faked sort information
216                    //
217                    // See what we do for binrel for an explanation.
218                    fixpoint::BinOp::Add => rty::BinOp::Add(rty::Sort::Int),
219                    fixpoint::BinOp::Sub => rty::BinOp::Sub(rty::Sort::Int),
220                    fixpoint::BinOp::Mul => rty::BinOp::Mul(rty::Sort::Int),
221                    fixpoint::BinOp::Div => rty::BinOp::Div(rty::Sort::Int),
222                    fixpoint::BinOp::Mod => rty::BinOp::Mod(rty::Sort::Int),
223                };
224                let [fe1, fe2] = &**boxed_args;
225                let e1 = self.fixpoint_to_expr(fe1)?;
226                let e2 = self.fixpoint_to_expr(fe2)?;
227                Ok(rty::Expr::binary_op(binop, e1, e2))
228            }
229            fixpoint::Expr::IfThenElse(boxed_args) => {
230                let [fe1, fe2, fe3] = &**boxed_args;
231                let e1 = self.fixpoint_to_expr(fe1)?;
232                let e2 = self.fixpoint_to_expr(fe2)?;
233                let e3 = self.fixpoint_to_expr(fe3)?;
234                Ok(rty::Expr::ite(e1, e2, e3))
235            }
236            fixpoint::Expr::And(fexprs) => {
237                let exprs: Vec<rty::Expr> = fexprs
238                    .iter()
239                    .map(|fexpr| self.fixpoint_to_expr(fexpr))
240                    .try_collect()?;
241                Ok(rty::Expr::and_from_iter(exprs))
242            }
243            fixpoint::Expr::Or(fexprs) => {
244                let exprs: Vec<rty::Expr> = fexprs
245                    .iter()
246                    .map(|fexpr| self.fixpoint_to_expr(fexpr))
247                    .try_collect()?;
248                Ok(rty::Expr::or_from_iter(exprs))
249            }
250            fixpoint::Expr::Not(fexpr) => {
251                let e = self.fixpoint_to_expr(fexpr)?;
252                Ok(rty::Expr::not(&e))
253            }
254            fixpoint::Expr::Imp(boxed_args) => {
255                let [fe1, fe2] = &**boxed_args;
256                let e1 = self.fixpoint_to_expr(fe1)?;
257                let e2 = self.fixpoint_to_expr(fe2)?;
258                Ok(rty::Expr::binary_op(rty::BinOp::Imp, e1, e2))
259            }
260            fixpoint::Expr::Iff(boxed_args) => {
261                let [fe1, fe2] = &**boxed_args;
262                let e1 = self.fixpoint_to_expr(fe1)?;
263                let e2 = self.fixpoint_to_expr(fe2)?;
264                Ok(rty::Expr::binary_op(rty::BinOp::Iff, e1, e2))
265            }
266            fixpoint::Expr::Atom(fbinrel, boxed_args) => {
267                let binrel = match fbinrel {
268                    fixpoint::BinRel::Eq => rty::BinOp::Eq,
269                    fixpoint::BinRel::Ne => rty::BinOp::Ne,
270                    // FIXME: (ck) faked sort information
271                    //
272                    // I'm pretty sure that it is OK to give `rty::Sort::Int`
273                    // because we only emit `fixpoint::BinRel::Gt`, etc. when we
274                    // have an Int/Real/Char sort (and further this sort info
275                    // isn't further used). But if we inspect this in other
276                    // places then things could break.
277                    fixpoint::BinRel::Gt => rty::BinOp::Gt(rty::Sort::Int),
278                    fixpoint::BinRel::Ge => rty::BinOp::Ge(rty::Sort::Int),
279                    fixpoint::BinRel::Lt => rty::BinOp::Lt(rty::Sort::Int),
280                    fixpoint::BinRel::Le => rty::BinOp::Le(rty::Sort::Int),
281                };
282                let [fe1, fe2] = &**boxed_args;
283                let e1 = self.fixpoint_to_expr(fe1)?;
284                let e2 = self.fixpoint_to_expr(fe2)?;
285                Ok(rty::Expr::binary_op(binrel, e1, e2))
286            }
287            fixpoint::Expr::Let(_var, _boxed_args) => {
288                // TODO: (ck) uncomment this and fix the missing code in the todo!()
289                //
290                // let [fe1, fe2] = &**boxed_args;
291                // let e1 = self.fixpoint_to_expr(fe1)?;
292                // let e2 = self.fixpoint_to_expr(fe2)?;
293                // let e2_binder =
294                todo!("Convert `var` in e2 to locally nameless var, then fill in sort");
295                // Ok(rty::Expr::let_(e1, e2_binder))
296            }
297            fixpoint::Expr::ThyFunc(itf) => Ok(rty::Expr::global_func(SpecFuncKind::Thy(*itf))),
298            fixpoint::Expr::IsCtor(var, fe) => {
299                let (def_id, variant_idx) = match var {
300                    fixpoint::Var::DataCtor(adt_id, variant_idx) => {
301                        let def_id = self.scx.adt_sorts[adt_id.as_usize()];
302                        Ok((def_id, *variant_idx))
303                    }
304                    _ => Err(FixpointParseError::WrongVarInIsCtor(*var)),
305                }?;
306                let e = self.fixpoint_to_expr(fe)?;
307                Ok(rty::Expr::is_ctor(def_id, variant_idx, e))
308            }
309        }
310    }
311
312    fn fixpoint_app_to_expr(
313        &self,
314        fhead: &fixpoint::Expr,
315        fargs: &[fixpoint::Expr],
316    ) -> Result<rty::Expr, FixpointParseError> {
317        let head = self.fixpoint_to_expr(fhead)?;
318        let args = fargs
319            .iter()
320            .map(|farg| self.fixpoint_to_expr(farg))
321            .try_collect()?;
322        Ok(rty::Expr::app(head, List::empty(), args))
323    }
324}
325
326#[derive(Debug)]
327pub enum FixpointParseError {
328    /// UIFRels are encoded as Apps, but they are as of right now only binary
329    /// relations so they must have 2 arguments only.
330    UIFRelArityMismatch(usize),
331    /// Expected arity (based off of the tuple ctor), actual arity (the numer of args)
332    TupleCtorArityMismatch(usize, usize),
333    /// The number of arguments should only ever be 1 for a tuple proj
334    ProjArityMismatch(usize),
335    NoGlobalVar(fixpoint::GlobalVar),
336    /// Casts should only have 1 arg
337    CastArityMismatch(usize),
338    PrimOpArityMismatch(usize),
339    NoLocalVar(fixpoint::LocalVar),
340    /// Expecting fixpoint::Var::DataCtor
341    WrongVarInIsCtor(fixpoint::Var),
342}
flux_infer/fixpoint_encoding/decoding.rs

flux_infer/fixpoint_encoding/
decoding.rs
