Skip to main content

reify

logicaffeine_kernel::ring

Function reify 

Source 
pub fn reify(term: &Term) -> Result<Polynomial, ReifyError>
Expand description

Reify a Syntax term into a polynomial representation.

This function converts the deep embedding of terms (Syntax) into the internal polynomial representation used for normalization.

§Supported Term Forms

  • SLit n - Integer literal becomes a constant polynomial
  • SVar i - De Bruijn variable becomes a polynomial variable
  • SName "x" - Named global becomes a polynomial variable (hashed)
  • SApp (SApp (SName "add") a) b - Addition of two terms
  • SApp (SApp (SName "sub") a) b - Subtraction of two terms
  • SApp (SApp (SName "mul") a) b - Multiplication of two terms

§Errors

Returns ReifyError::NonPolynomial for unsupported operations (div, mod) or unknown function symbols.

§Named Variables

Named variables (via SName) are converted to unique negative indices to avoid collision with De Bruijn indices (which are non-negative).