Function-application constructors, sort-erased

applyN takes an array and apply to apply4 are the fixed-arity spellings over it, so any arity is reachable. All of them build APPLY_UF, whose first child is the function itself.

They flatten. Applying a term that is already an APPLY_UF appends to its children rather than nesting, so apply2 (← apply f i) b and applyN f #[i, b] build the same (f i b). A nested application would hold a function-sorted term, which cvc5 admits only under a higher-order logic.

A partial application is legal. cvc5 accepts fewer arguments than the function's arity and gives the result the remaining function sort: applying (-> Int Bool Int) to one Int yields a term of sort (-> Bool Int). Too many arguments is an error, and so is none — APPLY_UF wants at least two children, the function and one argument.

applyHo is the different one: it is HO_APPLY, consumes exactly one argument whatever the arity, and needs a higher-order logic.

def Cvc.Untyped.Term.applyHo [Ω] (f arg : Term) : Env Term

Application of a single argument, leaving any remaining ones unapplied.

Needs a higher-order logic; Term.apply and Term.applyN are ordinary application.

Equations

• f.applyHo arg = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.HO_APPLY #[f, arg]

def Cvc.Untyped.View.Fun.of? [Ω] (viewed : Term) : Option View.Fun

Takes a term apart one level, if Fun owns its operator.

Equations

• One or more equations did not get rendered due to their size.

inductive Cvc.Untyped.View.Fun [Ω] : Type

Fun's operators, taken apart one level, sort-erased.

• applyHo [Ω] (f arg : Term) : View.Fun

  Application of a single argument, leaving any remaining ones unapplied.

  Needs a higher-order logic; Term.apply and Term.applyN are ordinary application.

def Cvc.Untyped.Term.applyN [Ω] (f : Term) (args : Terms) (_h : 0 < Array.size args := by (try grind) <;> fail "failed to prove there is at least one argument") : Env Term

Applies a function to the given arguments, however many.

Saturating when they fill the domain, and a partial application otherwise — cvc5 answers a term of the remaining function sort rather than refusing. More arguments than the domain has is an error, as is passing none.

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.apply [Ω] (f arg : Term) : Env Term

Applies a function to one argument.

Equations

• f.apply arg = f.applyN #[arg] ⋯

def Cvc.Untyped.Term.apply2 [Ω] (f fst snd : Term) : Env Term

Applies a function to two arguments.

Equations

• f.apply2 fst snd = f.applyN #[fst, snd] ⋯

def Cvc.Untyped.Term.apply3 [Ω] (f fst snd thd : Term) : Env Term

Applies a function to three arguments.

Equations

• f.apply3 fst snd thd = f.applyN #[fst, snd, thd] ⋯

def Cvc.Untyped.Term.apply4 [Ω] (f fst snd thd frth : Term) : Env Term

Applies a function to four arguments.

Equations

• f.apply4 fst snd thd frth = f.applyN #[fst, snd, thd, frth] ⋯

The view of an application

View.Apply takes an APPLY_UF apart; applyHo has the generated View.Fun.

inductive Cvc.Untyped.View.Apply [Ω] : Type

An uninterpreted function's application, taken apart one level, sort-erased.

• apply [Ω] (f : Term) (args : Args) : View.Apply

  f a₁ … aₙ, possibly a partial application.

def Cvc.Untyped.View.Apply.of? [Ω] (t : Term) : Option View.Apply

Takes a term apart one level, if it is an uninterpreted function's application.

Equations

• One or more equations did not get rendered due to their size.