Skip to content

Commit

Permalink
Do not differentiate between names in fixpoint
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann committed Nov 30, 2023
1 parent 7e2af62 commit dd6c2c3
Show file tree
Hide file tree
Showing 4 changed files with 129 additions and 119 deletions.
52 changes: 18 additions & 34 deletions crates/flux-fixpoint/src/constraint.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ pub enum Constraint<T: Types> {
Pred(Pred<T>, #[derive_where(skip)] Option<T::Tag>),
Conj(Vec<Self>),
Guard(Pred<T>, Box<Self>),
ForAll(T::Name, Sort, Pred<T>, Box<Self>),
ForAll(T::Var, Sort, Pred<T>, Box<Self>),
}

#[derive(Clone, Hash)]
Expand Down Expand Up @@ -49,17 +49,16 @@ pub struct PolyFuncSort {
fsort: FuncSort,
}

#[derive_where(Hash, Debug)]
#[derive_where(Hash)]
pub enum Pred<T: Types> {
And(Vec<Self>),
KVar(T::KVid, Vec<T::Name>),
KVar(T::KVar, Vec<T::Var>),
Expr(Expr<T>),
}

#[derive_where(Hash, Debug)]
#[derive_where(Hash)]
pub enum Expr<T: Types> {
Var(T::Name),
ConstVar(T::ConstName),
Var(T::Var),
Constant(Constant),
BinaryOp(BinOp, Box<[Self; 2]>),
App(Func<T>, Vec<Self>),
Expand All @@ -70,16 +69,14 @@ pub enum Expr<T: Types> {
Unit,
}

#[derive_where(Hash, Debug)]
#[derive_where(Hash)]
pub enum Func<T: Types> {
Var(T::Name),
/// uninterepreted function
Uif(T::ConstName),
Var(T::Var),
/// interpreted (theory) function
Itf(Symbol),
}

#[derive(Clone, Copy, Hash, Debug)]
#[derive(Clone, Copy, Hash)]
pub enum Proj {
Fst,
Snd,
Expand All @@ -88,14 +85,14 @@ pub enum Proj {
#[derive_where(Hash)]
pub struct Qualifier<T: Types> {
pub name: String,
pub args: Vec<(T::Name, Sort)>,
pub args: Vec<(T::Var, Sort)>,
pub body: Expr<T>,
pub global: bool,
}

#[derive(Clone, Copy, Debug)]
#[derive(Clone, Copy)]
pub struct Const<T: Types> {
pub name: T::ConstName,
pub name: T::Var,
pub val: i128,
}

Expand Down Expand Up @@ -124,7 +121,7 @@ pub enum UnOp {
Neg,
}

#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
pub enum Constant {
Int(BigInt),
Real(i128),
Expand Down Expand Up @@ -198,7 +195,7 @@ impl<T: Types> fmt::Display for Constraint<T> {
write!(f, "\n)")
}
Constraint::ForAll(x, sort, body, head) => {
write!(f, "(forall (({x:?} {sort}) {body})")?;
write!(f, "(forall (({x} {sort}) {body})")?;
write!(PadAdapter::wrap_fmt(f, 2), "\n{head}")?;
write!(f, "\n)")
}
Expand Down Expand Up @@ -255,31 +252,20 @@ impl fmt::Display for Sort {
Sort::BitVec(size) => write!(f, "(BitVec Size{})", size),
Sort::Pair(s1, s2) => write!(f, "(Pair {s1} {s2})"),
Sort::Func(sort) => write!(f, "{sort}"),
Sort::App(ctor, ts) => write!(f, "({ctor} {:?})", ts.iter().format(" ")),
Sort::App(ctor, ts) => write!(f, "({ctor} {})", ts.iter().format(" ")),
}
}
}

impl fmt::Display for PolyFuncSort {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(
f,
"(func({}, [{:?}]))",
self.params,
self.fsort.inputs_and_output.iter().format("; ")
)
write!(f, "(func({}, [{}]))", self.params, self.fsort.inputs_and_output.iter().format("; "))
}
}

impl fmt::Display for FuncSort {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "(func(0, [{:?}]))", self.inputs_and_output.iter().format("; "))
}
}

impl fmt::Debug for Sort {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
fmt::Display::fmt(self, f)
write!(f, "(func(0, [{}]))", self.inputs_and_output.iter().format("; "))
}
}

Expand All @@ -294,7 +280,7 @@ impl<T: Types> fmt::Display for Pred<T> {
}
}
Pred::KVar(kvid, vars) => {
write!(f, "(${kvid} {:?})", vars.iter().format(" "))
write!(f, "(${kvid} {})", vars.iter().format(" "))
}
Pred::Expr(expr) => write!(f, "({expr})"),
}
Expand Down Expand Up @@ -329,7 +315,6 @@ impl<T: Types> fmt::Display for Expr<T> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Expr::Var(x) => write!(f, "{x}"),
Expr::ConstVar(x) => write!(f, "{x}"),
Expr::Constant(c) => write!(f, "{c}"),
Expr::BinaryOp(op, box [e1, e2]) => {
write!(f, "{} {op} {}", FmtParens(e1), FmtParens(e2))?;
Expand Down Expand Up @@ -359,8 +344,7 @@ impl<T: Types> fmt::Display for Expr<T> {
impl<T: Types> fmt::Display for Func<T> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
Func::Var(name) => write!(f, "{name:?}"),
Func::Uif(uif) => write!(f, "{uif:?}"),
Func::Var(name) => write!(f, "{name}"),
Func::Itf(itf) => write!(f, "{itf}"),
}
}
Expand Down
53 changes: 39 additions & 14 deletions crates/flux-fixpoint/src/lib.rs
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,5 @@
#![feature(rustc_private, min_specialization, lazy_cell, box_patterns, let_chains)]

// extern crate rustc_index;
extern crate rustc_macros;
extern crate rustc_serialize;
extern crate rustc_span;
Expand Down Expand Up @@ -29,25 +28,51 @@ use serde::{de, Deserialize};

use crate::constraint::DEFAULT_QUALIFIERS;

pub trait Symbol: fmt::Display + Hash {}

impl<T: fmt::Display + Hash> Symbol for T {}

pub trait Types {
type ConstName: fmt::Display + fmt::Debug + Hash;
type KVid: fmt::Display + fmt::Debug + Hash;
type Name: fmt::Display + fmt::Debug + Hash;
type Tag: fmt::Display + fmt::Debug + Hash + FromStr;
type KVar: Symbol;
type Var: Symbol;
type Tag: fmt::Display + Hash + FromStr;
}

#[macro_export]
macro_rules! declare_types {
(type KVar = $kvar:ty; type Var = $var:ty; type Tag = $tag:ty;) => {
pub mod fixpoint_generated {
pub struct FixpointTypes;
pub type Expr = $crate::Expr<FixpointTypes>;
pub type Pred = $crate::Pred<FixpointTypes>;
pub type Func = $crate::Func<FixpointTypes>;
pub type Constraint = $crate::Constraint<FixpointTypes>;
pub type KVar = $crate::KVar<FixpointTypes>;
pub type ConstInfo = $crate::ConstInfo<FixpointTypes>;
pub type Task = $crate::Task<FixpointTypes>;
pub type Qualifier = $crate::Qualifier<FixpointTypes>;
pub use $crate::{PolyFuncSort, Proj, Sort, SortCtor};
}

impl $crate::Types for fixpoint_generated::FixpointTypes {
type KVar = $kvar;
type Var = $var;
type Tag = $tag;
}
};
}

struct StringTypes;

impl Types for StringTypes {
type ConstName = &'static str;
type KVid = &'static str;
type Name = &'static str;
type KVar = &'static str;
type Var = &'static str;
type Tag = String;
}

#[derive_where(Hash, Debug)]
#[derive_where(Hash)]
pub struct ConstInfo<T: Types> {
pub name: T::ConstName,
pub name: T::Var,
pub orig: rustc_span::Symbol,
pub sort: Sort,
}
Expand Down Expand Up @@ -90,9 +115,9 @@ pub struct Stats {
#[derive(Deserialize, Debug)]
pub struct CrashInfo(Vec<serde_json::Value>);

#[derive_where(Debug, Hash)]
#[derive_where(Hash)]
pub struct KVar<T: Types> {
kvid: T::KVid,
kvid: T::KVar,
sorts: Vec<Sort>,
comment: String,
}
Expand Down Expand Up @@ -162,7 +187,7 @@ impl<T: Types> Task<T> {
}

impl<T: Types> KVar<T> {
pub fn new(kvid: T::KVid, sorts: Vec<Sort>, comment: String) -> Self {
pub fn new(kvid: T::KVar, sorts: Vec<Sort>, comment: String) -> Self {
Self { kvid, sorts, comment }
}
}
Expand Down Expand Up @@ -219,7 +244,7 @@ impl<T: Types> fmt::Display for KVar<T> {

impl<T: Types> fmt::Display for ConstInfo<T> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "(constant {:?} {:?}) // orig: {}", self.name, self.sort, self.orig)
write!(f, "(constant {} {}) // orig: {}", self.name, self.sort, self.orig)
}
}

Expand Down
Loading

0 comments on commit dd6c2c3

Please sign in to comment.