Enum Term 

pub enum Term {
    Lam {
        tag: Tag,
        pat: Box<Pattern>,
        bod: Box<Term>,
    },
    Var {
        nam: Name,
    },
    Link {
        nam: Name,
    },
    Let {
        pat: Box<Pattern>,
        val: Box<Term>,
        nxt: Box<Term>,
    },
    With {
        typ: Name,
        bod: Box<Term>,
    },
    Ask {
        pat: Box<Pattern>,
        val: Box<Term>,
        nxt: Box<Term>,
    },
    Use {
        nam: Option<Name>,
        val: Box<Term>,
        nxt: Box<Term>,
    },
    App {
        tag: Tag,
        fun: Box<Term>,
        arg: Box<Term>,
    },
    Fan {
        fan: FanKind,
        tag: Tag,
        els: Vec<Term>,
    },
    Num {
        val: Num,
    },
    Nat {
        val: u32,
    },
    Str {
        val: GlobalString,
    },
    List {
        els: Vec<Term>,
    },
    Oper {
        opr: Op,
        fst: Box<Term>,
        snd: Box<Term>,
    },
    Mat {
        bnd: Option<Name>,
        arg: Box<Term>,
        with_bnd: Vec<Option<Name>>,
        with_arg: Vec<Term>,
        arms: Vec<MatchRule>,
    },
    Swt {
        bnd: Option<Name>,
        arg: Box<Term>,
        with_bnd: Vec<Option<Name>>,
        with_arg: Vec<Term>,
        pred: Option<Name>,
        arms: Vec<Term>,
    },
    Fold {
        bnd: Option<Name>,
        arg: Box<Term>,
        with_bnd: Vec<Option<Name>>,
        with_arg: Vec<Term>,
        arms: Vec<MatchRule>,
    },
    Bend {
        bnd: Vec<Option<Name>>,
        arg: Vec<Term>,
        cond: Box<Term>,
        step: Box<Term>,
        base: Box<Term>,
    },
    Open {
        typ: Name,
        var: Name,
        bod: Box<Term>,
    },
    Ref {
        nam: Name,
    },
    Def {
        def: Definition,
        nxt: Box<Term>,
    },
    Era,
    Err,
}

Variants

Lam

Fields

tag: Tag

pat: Box<Pattern>

bod: Box<Term>

Var

Fields

nam: Name

Link

Fields

nam: Name

Let

Fields

pat: Box<Pattern>

val: Box<Term>

nxt: Box<Term>

With

Fields

typ: Name

bod: Box<Term>

Ask

Fields

pat: Box<Pattern>

val: Box<Term>

nxt: Box<Term>

Use

Fields

nam: Option<Name>

val: Box<Term>

nxt: Box<Term>

App

Fields

tag: Tag

fun: Box<Term>

arg: Box<Term>

Fan

Either a tuple or a superposition

Fields

fan: FanKind

tag: Tag

els: Vec<Term>

Num

Fields

val: Num

Nat

Fields

val: u32

Str

Fields

val: GlobalString

List

Fields

els: Vec<Term>

Oper

A numeric operation between built-in numbers.

Fields

opr: Op

fst: Box<Term>

snd: Box<Term>

Mat

Pattern matching on an ADT.

Fields

bnd: Option<Name>

arg: Box<Term>

with_bnd: Vec<Option<Name>>

with_arg: Vec<Term>

arms: Vec<MatchRule>

Swt

Native pattern matching on numbers

Fields

bnd: Option<Name>

arg: Box<Term>

with_bnd: Vec<Option<Name>>

with_arg: Vec<Term>

pred: Option<Name>

arms: Vec<Term>

Fold

Fields

bnd: Option<Name>

arg: Box<Term>

with_bnd: Vec<Option<Name>>

with_arg: Vec<Term>

arms: Vec<MatchRule>

Bend

Fields

bnd: Vec<Option<Name>>

arg: Vec<Term>

cond: Box<Term>

step: Box<Term>

base: Box<Term>

Open

Fields

typ: Name

var: Name

bod: Box<Term>

Ref

Fields

nam: Name

Def

Fields

def: Definition

nxt: Box<Term>

Era

Err

Implementations

impl Term

pub fn encode_str(val: &str) -> Term

pub fn encode_nat(val: u32) -> Term

impl Term

pub fn check_unbound_refs(&self, book: &Book, unbounds: &mut HashSet<Name>)

impl Term

pub fn check_unbound_vars<'a>( &'a mut self, scope: &mut Vec<Option<&'a Name>>, errs: &mut Vec<UnboundVarErr>, )

Checks that all variables are bound. Precondition: References have been resolved, implicit binds have been solved.

impl Term

pub fn display_pretty(&self, tab: usize) -> impl Display + '_

impl Term

pub fn collect_unscoped( &self, unscoped: &mut HashSet<Name>, scope: &mut Vec<Name>, )

pub fn apply_unscoped(&mut self, unscoped: &HashSet<Name>)

Transform the variables that we previously found were unscoped into their unscoped variants.

impl Term

pub fn subst_ref_to_ref(term: &mut Term, ref_map: &BTreeMap<Name, Name>) -> bool

Performs reference substitution within a term replacing any references found in ref_map with their corresponding targets.

impl Term

pub fn desugar_use(&mut self)

pub fn desugar_ctr_use(&mut self)

impl Term

pub fn desugar_with_blocks( &mut self, cur_block: Option<&Name>, def_names: &HashSet<Name>, ) -> Result<(), String>

impl Term

pub fn encode_matches(&mut self, adt_encoding: AdtEncoding)

impl Term

Dereferences any non recursive generated definitions in the term. Used after readback.

pub fn expand_generated(&mut self, book: &Book, recursive_defs: &BTreeSet<Name>)

impl Term

pub fn has_unscoped_diff(&self) -> bool

pub fn float_children_mut(&mut self) -> impl Iterator<Item = &mut Term>

impl Term

pub fn lift_local_defs( &mut self, parent: &Name, check: bool, defs: &mut IndexMap<Name, Definition>, gen: &mut usize, )

impl Term

pub fn linearize_match_binds(&mut self)

Linearize any binds preceding a match/switch term, up to the first bind used in either the scrutinee or the bind.

impl Term

pub fn linearize_vars(&mut self)

impl Term

pub fn children_mut_with_binds_mut( &mut self, ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &mut Option<Name>>)>

Because multiple children can share the same binds, this function is very restricted. Should only be called after desugaring bends/folds/matches/switches.

impl Term

pub fn resolve_refs<'a>( &'a mut self, def_names: &HashSet<Name>, main: Option<&Name>, scope: &mut HashMap<&'a Name, usize>, info: &mut Diagnostics, ) -> Result<(), String>

impl Term

pub fn resugar_lists(&mut self, adt_encoding: AdtEncoding)

Converts lambda-encoded lists ending with List/Nil to list literals.

impl Term

pub fn resugar_strings(&mut self, adt_encoding: AdtEncoding)

Converts lambda-encoded strings ending with String/nil to string literals.

impl Term

pub fn make_var_names_unique(&mut self)

impl Term

pub fn lam(pat: Pattern, bod: Term) -> Self

Lambda with a static tag

pub fn tagged_lam(tag: Tag, pat: Pattern, bod: Term) -> Self

Lambda with any tag

pub fn rfold_lams( term: Term, pats: impl DoubleEndedIterator<Item = Option<Name>>, ) -> Self

Wraps a term in lambdas, so that the outermost lambda is the first given element.

The lambda equivalent of Term::call.

pub fn var_or_era(nam: Option<Name>) -> Self

pub fn app(fun: Term, arg: Term) -> Self

pub fn tagged_app(tag: Tag, fun: Term, arg: Term) -> Self

pub fn call(called: Term, args: impl IntoIterator<Item = Term>) -> Self

Make a call term by folding args around a called function term with applications.

pub fn tagged_call( tag: Tag, called: Term, args: impl IntoIterator<Item = Term>, ) -> Self

pub fn arg_call(fun: Term, arg: Name) -> Self

Apply a variable to a term by the var name.

pub fn ref(name: &str) -> Self

pub fn str(str: &str) -> Self

pub fn sub_num(arg: Term, val: Num) -> Term

pub fn add_num(arg: Term, val: Num) -> Term

pub fn pattern(&self) -> Option<&Pattern>

pub fn pattern_mut(&mut self) -> Option<&mut Pattern>

pub fn children(&self) -> impl DoubleEndedIterator<Item = &Term> + Clone

pub fn children_mut(&mut self) -> impl DoubleEndedIterator<Item = &mut Term>

pub fn children_with_binds( &self, ) -> impl DoubleEndedIterator<Item = (&Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)> + Clone

An iterator over the subterms with an iterator over the binds introduced by the current term for each subterm.

Must only be called after fix_matches.

Example: A lambda introduces 1 bind for it’s only subterm, while a let expression introduces 0 binds for the value and many binds for the next term.

pub fn children_mut_with_binds( &mut self, ) -> impl DoubleEndedIterator<Item = (&mut Term, impl DoubleEndedIterator<Item = &Option<Name>> + Clone)>

Must only be called after fix_matches.

pub fn subst(&mut self, from: &Name, to: &Term)

Substitute the occurrences of a variable in a term with the given term.

Caution: can cause invalid shadowing of variables if used incorrectly. Ex: Using subst to beta-reduce (@a @b a b) converting it into @b b.

NOTE: Expects var bind information to be properly stored in match expressions, so it must run AFTER fix_match_terms.

NOTE: Since it doesn’t (can’t) handle with clauses in match terms, it must be run only AFTER with linearization.

pub fn subst_ctrs(&mut self, from: &Name, to: &Name)

Substitute the occurrences of a constructor name with the given name.

pub fn subst_type_ctrs(&mut self, from: &Name, to: &Name)

Substitutes the occurrences of a type constructor in the term with the given name.

pub fn subst_unscoped(&mut self, from: &Name, to: &Term)

Substitute the occurrence of an unscoped variable with the given term.

pub fn free_vars(&self) -> IndexMap<Name, u64>

Collects all the free variables that a term has and the number of times each var is used

pub fn unscoped_vars(&self) -> (IndexSet<Name>, IndexSet<Name>)

Returns the set of declared and the set of used unscoped variables

pub fn has_unscoped(&self) -> bool

Trait Implementations

impl Clone for Term

fn clone(&self) -> Self

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Term

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

Formats the value using the given formatter.

impl Default for Term

fn default() -> Term

Returns the “default value” for a type.

impl Display for Term

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

Formats the value using the given formatter.

impl Drop for Term

fn drop(&mut self)

Executes the destructor for this type.

impl Hash for Term

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for Term

fn eq(&self, other: &Term) -> 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 Term

impl StructuralPartialEq for Term