fn convert()

in amzn-smt-ir/src/term/convert.rs [94:210]

• 111 lines of code
• 5 McCabe index (conditional complexity)

fn convert<L: Logic>(t: RawTerm) -> Result<Term<L>, InvalidTerm<L>>
where
    QualIdentifier: Into<IVar<L::Var>>,
{
    #[derive(Debug)]
    enum Type {
        Op(QualIdentifier, usize),
        Let(Vec<ISymbol>),
        Quantifier(quantifier::Kind, Vec<(ISymbol, ISort)>),
    }

    let ident = convert_qual_identifier;

    let convert_or_enqueue = |t: RawTerm, pending: &mut Vec<_>| {
        use RawTerm::*;
        match t {
            Constant(c) => Ok(Some(Term::Constant(c.into()))),
            QualIdentifier(q) => {
                let t = (ICoreOp::parse(ident(q), vec![]).map(Term::CoreOp))
                    .or_else(|InvalidOp { func, .. }| IOp::parse(func, vec![]).map(Term::OtherOp))
                    .unwrap_or_else(|InvalidOp { func, .. }| Term::Variable(func.into()));
                Ok(Some(t))
            }
            Application {
                qual_identifier: op,
                arguments: args,
            } => {
                pending.push(Either::Left(Type::Op(ident(op), args.len())));
                pending.extend(args.into_iter().rev().map(Either::Right));
                Ok(None)
            }
            Let { var_bindings, term } => {
                let mut vars = vec![];
                let mut ts = vec![];
                for (var, t) in var_bindings {
                    vars.push(var.into());
                    ts.push(t);
                }
                pending.push(Either::Left(Type::Let(vars)));
                pending.extend(ts.into_iter().rev().map(Either::Right));
                pending.push(Either::Right(*term));
                Ok(None)
            }
            Forall { vars, term } => {
                let vars = vars
                    .into_iter()
                    .map(|(sym, sort)| (sym.into(), Sort::from(sort).into()))
                    .collect();
                pending.push(Either::Left(Type::Quantifier(
                    quantifier::Kind::Universal,
                    vars,
                )));
                pending.push(Either::Right(*term));
                Ok(None)
            }
            Exists { vars, term } => {
                let vars = vars
                    .into_iter()
                    .map(|(sym, sort)| (sym.into(), Sort::from(sort).into()))
                    .collect();
                pending.push(Either::Left(Type::Quantifier(
                    quantifier::Kind::Existential,
                    vars,
                )));
                pending.push(Either::Right(*term));
                Ok(None)
            }
            Match { .. } => Err(InvalidTerm::Match),
            Attributes { term, .. } => {
                pending.push(Either::Right(*term));
                Ok(None)
            }
        }
    };

    let mut pending = vec![];
    let mut converted: Vec<Term<L>> = vec![];

    if let Some(t) = convert_or_enqueue(t, &mut pending)? {
        return Ok(t);
    };

    while let Some(next) = pending.pop() {
        match next {
            Either::Left(ty) => match ty {
                Type::Op(func, num_args) => {
                    let args = converted.drain(converted.len() - num_args..);
                    let args = args.collect::<Vec<_>>();
                    let op = (ICoreOp::parse(func, args).map(Term::CoreOp))
                        .or_else(|InvalidOp { func, args }| IOp::parse(func, args).map(Into::into))
                        .or_else(|InvalidOp { func, args }| {
                            IUF::parse(func.sym().clone(), args).map(Into::into)
                        })?;
                    converted.push(op);
                }
                Type::Let(vars) => {
                    let ts = converted.drain(converted.len() - vars.len()..);
                    let bindings = vars.into_iter().zip(ts).collect();
                    let term = converted.pop().unwrap();
                    converted.push(Term::Let(Let { bindings, term }.into()));
                }
                Type::Quantifier(kind, vars) => {
                    let t = converted.pop().unwrap();
                    let q = L::Quantifier::parse(kind, vars, t)?.into();
                    converted.push(Term::Quantifier(q));
                }
            },
            Either::Right(t) => {
                if let Some(t) = convert_or_enqueue(t, &mut pending)? {
                    converted.push(t);
                }
            }
        }
    }

    Ok(converted.pop().unwrap())
}