Function application, typed

A function's index is the curried arrow α → β → γ, the SMT sort (-> α β γ). A function term applies directly, f a b : Env (Term γ), or through apply/apply2/apply3, or applyN f (.cons a (.last b)) at any arity. Fewer arguments than the arity is a partial application, at the remaining function index.

Applications flatten: applying a term that is already an application appends to its arguments, so all these spellings build the same flat term, which needs no higher-order logic.

def Cvc.Typed.Term.applyHo [Ω] {α β : Type} (f : Term (α → β)) (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.Untyped.Term.applyHo f arg

inductive Cvc.Typed.View.Fun.OnAny [Ω] (β : Type) [ToTyp β] : Type

Fun's operators whose result's sort is a type variable.

• applyHo [Ω] {β : Type} [ToTyp β] (α : Typ) (f : Term (α.function (Typ?.typ (Typ.of β))).Denote) (arg : Term α.Denote) : OnAny β

  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.Typed.View.Fun.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Fun τ))

Takes a term apart one level, at its sort, if Fun owns its operator and the term's sort fits it.

Equations

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

inductive Cvc.Typed.View.Fun [Ω] : Typ → Type

Fun's operators, taken apart one level, indexed by the sort each produces.

• any [Ω] {τ : Typ} : OnAny τ.Denote → View.Fun τ

  An operator whose result's sort is a type variable.

Applying any number of arguments

structure Cvc.Typed.Term.Args [Ω] (φ β : Type) : Type

Arguments taking a function of index φ down to a result of index β, at least one.

Built with last and cons: .cons a (.last b) is a then b.

• terms : Cvc.Untyped.Terms
• nonEmpty : 0 < Array.size (terms self)

def Cvc.Typed.Term.Args.last [Ω] {α β : Type} (arg : Term α) : Args (α → β) β

The final argument; β is whatever the function has left, a function sort if it is partial.

Equations

• Cvc.Typed.Term.Args.last arg = { terms := #[arg.erase], nonEmpty := ⋯ }

def Cvc.Typed.Term.Args.cons [Ω] {α φ β : Type} (arg : Term α) (rest : Args φ β) : Args (α → φ) β

One more argument, in front of the ones collected so far.

Equations

• Cvc.Typed.Term.Args.cons arg rest = { terms := #[arg.erase] ++ Cvc.Typed.Term.Args.terms✝ rest, nonEmpty := ⋯ }

def Cvc.Typed.Term.Args.toUntyped [Ω] {φ β : Type} (args : Args φ β) : Untyped.Terms

The arguments' terms, sort-erased and in order, as the sort-erased Term.applyN takes them.

Equations

• args.toUntyped = Cvc.Typed.Term.Args.terms✝ args

@[reducible, inline]

abbrev Cvc.Typed.Term.Args.erase [Ω] {φ β : Type} (args : Args φ β) : Untyped.Terms

The arguments' terms, sort-erased and in order, as the sort-erased Term.applyN takes them.

Equations

• args.erase = args.toUntyped

def Cvc.Typed.Term.applyN [Ω] {φ β : Type} (f : Term φ) (args : Args φ β) : Env (Term β)

Applies a function to some arguments: all of them, or fewer for a partial application.

Equations

• f.applyN args = f.erase.applyN (Cvc.Typed.Term.Args.terms✝ args) ⋯

@[instance_reducible]

instance Cvc.Typed.Term.instCoeFunForallForallEnv [Ω] {α β : Type} : CoeFun (Term (α → β)) fun (x : Term (α → β)) => Term α → Env (Term β)

Equations

• Cvc.Typed.Term.instCoeFunForallForallEnv = { coe := fun (f : Cvc.Typed.Term (α → β)) (arg : Cvc.Typed.Term α) => f.applyN (Cvc.Typed.Term.Args.last arg) }

@[instance_reducible]

instance Cvc.Typed.Term.instCoeFunEnvForallForall [Ω] {α β : Type} : CoeFun (Env (Term (α → β))) fun (x : Env (Term (α → β))) => Term α → Env (Term β)

Equations

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

def Cvc.Typed.Term.apply [Ω] {α β : Type} (f : Term (α → β)) (arg : Term α) : Env (Term β)

Applies a function to one argument.

Equations

• f.apply arg = f.applyN (Cvc.Typed.Term.Args.last arg)

def Cvc.Typed.Term.apply2 [Ω] {α β γ : Type} (f : Term (α → β → γ)) (fst : Term α) (snd : Term β) : Env (Term γ)

Applies a function to two arguments.

Equations

• f.apply2 fst snd = f.applyN (Cvc.Typed.Term.Args.cons fst (Cvc.Typed.Term.Args.last snd))

def Cvc.Typed.Term.apply3 [Ω] {α β γ δ : Type} (f : Term (α → β → γ → δ)) (fst : Term α) (snd : Term β) (thd : Term γ) : Env (Term δ)

Applies a function to three arguments.

Equations

• f.apply3 fst snd thd = f.applyN (Cvc.Typed.Term.Args.cons fst (Cvc.Typed.Term.Args.cons snd (Cvc.Typed.Term.Args.last thd)))

Viewing an application

The arguments' sorts come as a list of Typs, from which the function's index is computed, and matching on the list refines both: .apply [.int, .bool] f (.cons x (.last b)) gives f : Term (Int → Bool → τ.Denote), x : Term Int and b : Term Bool.

inductive Cvc.Typed.View.Apply.Args [Ω] : List Typ → Type

An application's arguments, each a Term σ.Denote at its sort σ; never empty.

• last [Ω] {τ : Typ} (t : Term τ.Denote) : Args [τ]

  The last argument.

• cons [Ω] {τs : List Typ} {τ : Typ} (t : Term τ.Denote) (rest : Args τs) : Args (τ :: τs)

  One more argument, in front of the others.

def Cvc.Typed.View.Apply.Args.toArgs [Ω] {doms : List Typ} {β : Type} : Args doms → Term.Args (Typ.arrows doms β) β

The same arguments as a Term.Args, so that a viewed application can be rebuilt.

Equations

• (Cvc.Typed.View.Apply.Args.last t).toArgs = Cvc.Typed.Term.Args.last t
• (Cvc.Typed.View.Apply.Args.cons t rest).toArgs = Cvc.Typed.Term.Args.cons t rest.toArgs

inductive Cvc.Typed.View.Apply [Ω] : Typ → Type

An uninterpreted function's application, of sort τ, taken apart one level.

• apply [Ω] {τ : Typ} (doms : List Typ) (f : Term (Typ.arrows doms τ.Denote)) (args : Args doms) : View.Apply τ

  f a₁ … aₙ, fully applied.

def Cvc.Typed.View.Apply.of [Ω] (τ : Typ) (t : Term τ.Denote) : Env (Option (View.Apply τ))

Takes a function application of sort τ apart one level, none for any other term.

Also none when an argument's sort is one no Typ describes.

Equations

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