Internal representation of `if _ then _ else _`

[ttuegel]

It often happens (particularly during function evaluation) that we have if _ then _ else _ patterns, which are encoded in Kore as

(P ∧ A) ∨ (¬P ∧ B)  // if P then A else B

which evaluates the predicate P twice. We would prefer to have something like an alias,

// cond-itional, in homage to Lisp
alias \cond(P, A, B) := (P ∧ A) ∨ (¬P ∧ B)

with some recognition that the predicate P need only be evaluated once.
Further, in a chain of conditions,

\cond(P, A, \cond(P', B, C))

if P = ⊤, then we never need to consider P'.

I would like to introduce an internal TermLike node,

-- represents a nested sequence of conditionals as above
newtype Cond variable = Cond { getCond :: Seq (Predicate variable, TermLike variable) }

data TermLikeF variable
    = ...
    | CondF (Cond variable)

(Presently, using a Predicate in this place would introduce a circular dependency, but it is not complicated to refactor that dependency away.)

[xc93]

This alias definition alias \cond(P, A, B) := (P ∧ A) ∨ (¬P ∧ B) makes sense, and I like it very much.
In terms of the implementation, what is the type of \cond(P,A,B) when it is applied to a predicate P and two terms (functional? partially-functional?) A and B?

[ttuegel]

To answer your question, I should amend my definition slightly and include the sorts:

alias \cond{R, S}(@P:R, @A:S, @B:S) : S := (⌈@P⌉ ∧ @A) ∨ (¬⌈@P⌉ ∧ @B)

(All the variables should be set variables; I know ultimately they should be meta-variables, but presently we make a distinction because there aren't meta-variables.) I included ⌈_⌉ on the right-hand side now because we don't have a way to constrain @P to be a predicate. That matches my Lisp-y inspiration better anyway: nil (\bottom) is "false" (second branch) and everything else is "true" (first branch). If @A and @B are both function-like, \cond is function-like, respectively functional.