mirror of
https://github.com/circify/circ.git
synced 2026-01-09 13:48:02 -05:00
move op Display impls to ir::term::fmt (#198)
This commit is contained in:
@@ -1,7 +1,8 @@
|
||||
//! Machinery for formatting IR types
|
||||
use super::{
|
||||
check, ext, map::Map, Array, ComputationMetadata, Node, Op, PartyId, PostOrderIter, Sort, Term,
|
||||
TermMap, Value, VariableMetadata,
|
||||
check, ext, map::Map, Array, BoolNaryOp, BvBinOp, BvBinPred, BvNaryOp, BvUnOp,
|
||||
ComputationMetadata, FpBinOp, FpBinPred, FpUnOp, FpUnPred, IntBinPred, IntNaryOp, Node, Op,
|
||||
PartyId, PfNaryOp, PfUnOp, PostOrderIter, Sort, Term, TermMap, Value, VariableMetadata,
|
||||
};
|
||||
use crate::cfg::{cfg, is_cfg_set};
|
||||
|
||||
@@ -12,6 +13,154 @@ use itertools::Itertools;
|
||||
|
||||
use std::fmt::{Debug, Display, Error as FmtError, Formatter, Result as FmtResult, Write};
|
||||
|
||||
impl Display for BoolNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BoolNaryOp::And => write!(f, "and"),
|
||||
BoolNaryOp::Or => write!(f, "or"),
|
||||
BoolNaryOp::Xor => write!(f, "xor"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for BvBinOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvBinOp::Sub => write!(f, "bvsub"),
|
||||
BvBinOp::Udiv => write!(f, "bvudiv"),
|
||||
BvBinOp::Urem => write!(f, "bvurem"),
|
||||
BvBinOp::Shl => write!(f, "bvshl"),
|
||||
BvBinOp::Ashr => write!(f, "bvashr"),
|
||||
BvBinOp::Lshr => write!(f, "bvlshr"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for BvBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvBinPred::Ult => write!(f, "bvult"),
|
||||
BvBinPred::Ugt => write!(f, "bvugt"),
|
||||
BvBinPred::Ule => write!(f, "bvule"),
|
||||
BvBinPred::Uge => write!(f, "bvuge"),
|
||||
BvBinPred::Slt => write!(f, "bvslt"),
|
||||
BvBinPred::Sgt => write!(f, "bvsgt"),
|
||||
BvBinPred::Sle => write!(f, "bvsle"),
|
||||
BvBinPred::Sge => write!(f, "bvsge"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for BvNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvNaryOp::Add => write!(f, "bvadd"),
|
||||
BvNaryOp::Mul => write!(f, "bvmul"),
|
||||
BvNaryOp::Or => write!(f, "bvor"),
|
||||
BvNaryOp::And => write!(f, "bvand"),
|
||||
BvNaryOp::Xor => write!(f, "bvxor"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for BvUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvUnOp::Not => write!(f, "bvnot"),
|
||||
BvUnOp::Neg => write!(f, "bvneg"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for FpBinOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpBinOp::Add => write!(f, "fpadd"),
|
||||
FpBinOp::Mul => write!(f, "fpmul"),
|
||||
FpBinOp::Sub => write!(f, "fpsub"),
|
||||
FpBinOp::Div => write!(f, "fpdiv"),
|
||||
FpBinOp::Rem => write!(f, "fprem"),
|
||||
FpBinOp::Max => write!(f, "fpmax"),
|
||||
FpBinOp::Min => write!(f, "fpmin"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for FpUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpUnOp::Neg => write!(f, "fpneg"),
|
||||
FpUnOp::Abs => write!(f, "fpabs"),
|
||||
FpUnOp::Sqrt => write!(f, "fpsqrt"),
|
||||
FpUnOp::Round => write!(f, "fpround"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for FpBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpBinPred::Le => write!(f, "fple"),
|
||||
FpBinPred::Lt => write!(f, "fplt"),
|
||||
FpBinPred::Eq => write!(f, "fpeq"),
|
||||
FpBinPred::Ge => write!(f, "fpge"),
|
||||
FpBinPred::Gt => write!(f, "fpgt"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for FpUnPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpUnPred::Normal => write!(f, "fpnormal"),
|
||||
FpUnPred::Subnormal => write!(f, "fpsubnormal"),
|
||||
FpUnPred::Zero => write!(f, "fpzero"),
|
||||
FpUnPred::Infinite => write!(f, "fpinfinite"),
|
||||
FpUnPred::Nan => write!(f, "fpnan"),
|
||||
FpUnPred::Negative => write!(f, "fpnegative"),
|
||||
FpUnPred::Positive => write!(f, "fppositive"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for PfNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
PfNaryOp::Add => write!(f, "+"),
|
||||
PfNaryOp::Mul => write!(f, "*"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for PfUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
PfUnOp::Neg => write!(f, "-"),
|
||||
PfUnOp::Recip => write!(f, "pfrecip"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for IntNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
IntNaryOp::Add => write!(f, "intadd"),
|
||||
IntNaryOp::Mul => write!(f, "intmul"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for IntBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
IntBinPred::Lt => write!(f, "<"),
|
||||
IntBinPred::Gt => write!(f, ">"),
|
||||
IntBinPred::Le => write!(f, "<="),
|
||||
IntBinPred::Ge => write!(f, ">="),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// State that influences how IR is formatted.
|
||||
struct IrFormatter<'a, 'b> {
|
||||
cfg: &'a IrCfg,
|
||||
|
||||
@@ -31,7 +31,6 @@ use serde::{Deserialize, Deserializer, Serialize, Serializer};
|
||||
use std::borrow::Borrow;
|
||||
use std::cell::Cell;
|
||||
use std::collections::BTreeMap;
|
||||
use std::fmt::{Debug, Display, Formatter, Result as FmtResult};
|
||||
|
||||
pub mod bv;
|
||||
pub mod dist;
|
||||
@@ -342,16 +341,6 @@ pub enum BoolNaryOp {
|
||||
Or,
|
||||
}
|
||||
|
||||
impl Display for BoolNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BoolNaryOp::And => write!(f, "and"),
|
||||
BoolNaryOp::Or => write!(f, "or"),
|
||||
BoolNaryOp::Xor => write!(f, "xor"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Bit-vector binary operator
|
||||
pub enum BvBinOp {
|
||||
@@ -369,19 +358,6 @@ pub enum BvBinOp {
|
||||
Lshr,
|
||||
}
|
||||
|
||||
impl Display for BvBinOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvBinOp::Sub => write!(f, "bvsub"),
|
||||
BvBinOp::Udiv => write!(f, "bvudiv"),
|
||||
BvBinOp::Urem => write!(f, "bvurem"),
|
||||
BvBinOp::Shl => write!(f, "bvshl"),
|
||||
BvBinOp::Ashr => write!(f, "bvashr"),
|
||||
BvBinOp::Lshr => write!(f, "bvlshr"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Bit-vector binary predicate
|
||||
pub enum BvBinPred {
|
||||
@@ -404,21 +380,6 @@ pub enum BvBinPred {
|
||||
Sge,
|
||||
}
|
||||
|
||||
impl Display for BvBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvBinPred::Ult => write!(f, "bvult"),
|
||||
BvBinPred::Ugt => write!(f, "bvugt"),
|
||||
BvBinPred::Ule => write!(f, "bvule"),
|
||||
BvBinPred::Uge => write!(f, "bvuge"),
|
||||
BvBinPred::Slt => write!(f, "bvslt"),
|
||||
BvBinPred::Sgt => write!(f, "bvsgt"),
|
||||
BvBinPred::Sle => write!(f, "bvsle"),
|
||||
BvBinPred::Sge => write!(f, "bvsge"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Bit-vector n-ary operator
|
||||
pub enum BvNaryOp {
|
||||
@@ -434,18 +395,6 @@ pub enum BvNaryOp {
|
||||
Xor,
|
||||
}
|
||||
|
||||
impl Display for BvNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvNaryOp::Add => write!(f, "bvadd"),
|
||||
BvNaryOp::Mul => write!(f, "bvmul"),
|
||||
BvNaryOp::Or => write!(f, "bvor"),
|
||||
BvNaryOp::And => write!(f, "bvand"),
|
||||
BvNaryOp::Xor => write!(f, "bvxor"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Bit-vector unary operator
|
||||
pub enum BvUnOp {
|
||||
@@ -455,15 +404,6 @@ pub enum BvUnOp {
|
||||
Neg,
|
||||
}
|
||||
|
||||
impl Display for BvUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
BvUnOp::Not => write!(f, "bvnot"),
|
||||
BvUnOp::Neg => write!(f, "bvneg"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Floating-point binary operator
|
||||
pub enum FpBinOp {
|
||||
@@ -483,20 +423,6 @@ pub enum FpBinOp {
|
||||
Min,
|
||||
}
|
||||
|
||||
impl Display for FpBinOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpBinOp::Add => write!(f, "fpadd"),
|
||||
FpBinOp::Mul => write!(f, "fpmul"),
|
||||
FpBinOp::Sub => write!(f, "fpsub"),
|
||||
FpBinOp::Div => write!(f, "fpdiv"),
|
||||
FpBinOp::Rem => write!(f, "fprem"),
|
||||
FpBinOp::Max => write!(f, "fpmax"),
|
||||
FpBinOp::Min => write!(f, "fpmin"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Floating-point unary operator
|
||||
pub enum FpUnOp {
|
||||
@@ -510,17 +436,6 @@ pub enum FpUnOp {
|
||||
Round,
|
||||
}
|
||||
|
||||
impl Display for FpUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpUnOp::Neg => write!(f, "fpneg"),
|
||||
FpUnOp::Abs => write!(f, "fpabs"),
|
||||
FpUnOp::Sqrt => write!(f, "fpsqrt"),
|
||||
FpUnOp::Round => write!(f, "fpround"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Floating-point binary predicate
|
||||
pub enum FpBinPred {
|
||||
@@ -536,18 +451,6 @@ pub enum FpBinPred {
|
||||
Gt,
|
||||
}
|
||||
|
||||
impl Display for FpBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpBinPred::Le => write!(f, "fple"),
|
||||
FpBinPred::Lt => write!(f, "fplt"),
|
||||
FpBinPred::Eq => write!(f, "fpeq"),
|
||||
FpBinPred::Ge => write!(f, "fpge"),
|
||||
FpBinPred::Gt => write!(f, "fpgt"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Floating-point unary predicate
|
||||
pub enum FpUnPred {
|
||||
@@ -567,20 +470,6 @@ pub enum FpUnPred {
|
||||
Positive,
|
||||
}
|
||||
|
||||
impl Display for FpUnPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
FpUnPred::Normal => write!(f, "fpnormal"),
|
||||
FpUnPred::Subnormal => write!(f, "fpsubnormal"),
|
||||
FpUnPred::Zero => write!(f, "fpzero"),
|
||||
FpUnPred::Infinite => write!(f, "fpinfinite"),
|
||||
FpUnPred::Nan => write!(f, "fpnan"),
|
||||
FpUnPred::Negative => write!(f, "fpnegative"),
|
||||
FpUnPred::Positive => write!(f, "fppositive"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Finite field n-ary operator
|
||||
pub enum PfNaryOp {
|
||||
@@ -590,15 +479,6 @@ pub enum PfNaryOp {
|
||||
Mul,
|
||||
}
|
||||
|
||||
impl Display for PfNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
PfNaryOp::Add => write!(f, "+"),
|
||||
PfNaryOp::Mul => write!(f, "*"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Finite field n-ary operator
|
||||
pub enum PfUnOp {
|
||||
@@ -608,15 +488,6 @@ pub enum PfUnOp {
|
||||
Recip,
|
||||
}
|
||||
|
||||
impl Display for PfUnOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
PfUnOp::Neg => write!(f, "-"),
|
||||
PfUnOp::Recip => write!(f, "pfrecip"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Integer n-ary operator
|
||||
pub enum IntNaryOp {
|
||||
@@ -626,15 +497,6 @@ pub enum IntNaryOp {
|
||||
Mul,
|
||||
}
|
||||
|
||||
impl Display for IntNaryOp {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
IntNaryOp::Add => write!(f, "intadd"),
|
||||
IntNaryOp::Mul => write!(f, "intmul"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug, Copy, Serialize, Deserialize)]
|
||||
/// Integer binary predicate. See [Op::Eq] for equality.
|
||||
pub enum IntBinPred {
|
||||
@@ -648,17 +510,6 @@ pub enum IntBinPred {
|
||||
Ge,
|
||||
}
|
||||
|
||||
impl Display for IntBinPred {
|
||||
fn fmt(&self, f: &mut Formatter) -> FmtResult {
|
||||
match self {
|
||||
IntBinPred::Lt => write!(f, "<"),
|
||||
IntBinPred::Gt => write!(f, ">"),
|
||||
IntBinPred::Le => write!(f, "<="),
|
||||
IntBinPred::Ge => write!(f, ">="),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Serialize for Term {
|
||||
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
|
||||
where
|
||||
|
||||
Reference in New Issue
Block a user