Struct TermDag

pub struct TermDag { /* private fields */ }

A hashconsing arena for Terms.

Implementations

impl TermDag

pub fn size(&self) -> usize

Returns the number of nodes in this DAG.

pub fn lookup(&self, node: &Term) -> TermId

Convert the given term to its id.

Panics if the term does not already exist in this TermDag.

pub fn get(&self, id: TermId) -> &Term

Convert the given id to the corresponding term.

Panics if the id is not valid.

pub fn app(&mut self, sym: String, children: Vec<Term>) -> Term

Make and return a Term::App with the given head symbol and children, and insert into the DAG if it is not already present.

Panics if any of the children are not already in the DAG.

pub fn lit(&mut self, lit: Literal) -> Term

Make and return a Term::Lit with the given literal, and insert into the DAG if it is not already present.

pub fn var(&mut self, sym: String) -> Term

Make and return a Term::Var with the given symbol, and insert into the DAG if it is not already present.

pub fn expr_to_term(&mut self, expr: &GenericExpr<String, String>) -> Term

Recursively converts the given expression to a term.

This involves inserting every subexpression into this DAG. Because TermDags are hashconsed, the resulting term is guaranteed to maximally share subterms.

pub fn term_to_expr(&self, term: &Term, span: Span) -> Expr

Recursively converts the given term to an expression.

Panics if the term contains subterms that are not in the DAG.

pub fn to_string(&self, term: &Term) -> String

Converts the given term to a string.

Panics if the term or any of its subterms are not in the DAG.

Trait Implementations

impl Clone for TermDag

fn clone(&self) -> TermDag

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for TermDag

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for TermDag

fn default() -> TermDag

Returns the “default value” for a type.

impl PartialEq for TermDag

fn eq(&self, other: &TermDag) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for TermDag

impl StructuralPartialEq for TermDag