Documentation

Pretty instance for expressions.

If the expression contains type annotations, the output quickly becomes practically unreadable. Consider stripping type annotations before pretty printing (see FreeC.IR.Strip) to improve readability.

Strips the type annotation of the given expression and of its sub-expressions recursively.

The similarity relation of expressions is governed by the the following inference rules

• Expressions with type annotations are similar if the annotated expressions are similar and their annotations are similar.

   Γ ⊢ τ ≈ τ', Γ ⊢ e ≈ f
  ———————————————————————
   Γ ⊢ e :: τ ≈ f :: τ'

• For all variables x and y, x and y are similar under a renaming Γ if they are mapped to each other by Γ.

   x ↦ y ∈ Γ
  ———————————
   Γ ⊢ x ≈ y

• A free variable x is similar to itself.

   x ∈ free(Γ)
  —————————————
   Γ ⊢ x ≈ x

• Two lambda abstractions are similar if their right-hand sides are similar under an extended Renaming that maps the variable patterns from the first lambda abstraction to the arguments of the second one. Furthermore, the types the lambda abstraction's arguments have been annotated with must be similar (if there are any).

   Γ ∪ { x₁ ↦ y₁, …, xₙ ↦ yₙ } ⊢ e ≈ f, Γ ⊢ p₁ ≈ q₁, …, Γ ⊢ pₙ ≈ qₙ
  ——————————————————————————————————————————————————————————————————
                  Γ ⊢ \p₁ … pₙ -> e ≈ \q₁ … qₙ -> f

  where xᵢ and yᵢ denote the names of the variables bound by the patterns pᵢ and qᵢ respectively.

• Two application expressions are similar if the callees and the arguments are similar.

   Γ ⊢ e₁ ≈ f₁, Γ ⊢ e₂ ≈ f₂
  ——————————————————————————
      Γ ⊢ e₁ e₂ ≈ f₁ f₂

• Two visible type application expressions are similar if the visibly applied expressions and the type arguments are similar.

   Γ ⊢ e ≈ f, Γ ⊢ τ ≈ τ'
  ———————————————————————
      Γ ⊢ e @τ ≈ f @τ'

• Two case expressions are similar if the expressions they match are similar and their alternatives are pairwise similar. Note that the order of the alternatives is important.

   Γ ⊢ e ≈ f,      Γ ⊢ alt₁ ≈ alt'₁,      …,      Γ ⊢ altₙ ≈ alt'ₙ
  —————————————————————————————————————————————————————————————————
   Γ ⊢ case e of { alt₁; …; altₙ } ≈ case f of { alt'₁; …; alt'ₙ }

• Two if expressions are similar if their conditions and branches are similar.

   Γ ⊢ e₁ ≈ f₁,       Γ ⊢ e₂ ≈ f₂,       Γ ⊢ e₃ ≈ f₃
  ———————————————————————————————————————————————————
   Γ ⊢ if e₁ then e₂ else e₃ ≈ if f₁ then f₂ else f₃

• Two let expressions are similar if their bindings and the expression are similar under an extended Renaming Γ' that maps the variables bound by the first let expression to the variables bound by the second let expression.

   Γ' ⊢ e ≈ f,    Γ' ⊢ b₁ ≈ d₁,    …,    Γ' ⊢ bₙ ≈ dₙ
  ——————————————————————————————————————————————————————
   Γ ⊢ let { b₁; …; bₙ } in e ≈ let { d₁; …; dₙ } in f

  where Γ' = Γ ∪ { x₁ ↦ y₁, …, xₙ ↦ yₙ } and x₁, …, xₙ and y₁, …, yₙ denote the names of variables bound by b₁, …, bₙ and d₁, …, dₙ, respectively.

• All AST nodes which do not contain any variables are similar to themselves under every Renaming Γ.

  ———————————  ———————————————————————————  ———————————————————————
   Γ ⊢ C ≈ C    Γ ⊢ undefined ≈ undefined    Γ ⊢ error s ≈ error s

  Where C is a constructor or integer literal and s is an arbitrary error message.

Expression refer to the used variables and constructors as wells as the types used in type signatures and visible type applications.

The error terms undefined and error "msg" refer to the functions undefinedFuncName and errorFuncName respectively. The term trace "msg" expr refers to the function traceFuncName.

Expressions can be parsed.

Applies the given type substitution to an expression.

Applies the given expression substitution to an the right-hand side of a let binding.

The variable that is bound by the binding is not renamed by this instance. The ApplySubst instance for expressions renames all variables that are bound by let expressions.

Applies the given expression substitution to the right-hand side of the given case-expression alternative.

Applies the given expression substitution to an expression.

This function uses the Converter monad, because we need to create fresh identifiers. This is because we have to rename arguments of lambda abstractions and case-alternatives, such that no name conflict can occur.

Applies the given expression substitution to the right-hand side of a function declaration.

Pretty instance for case expression alternatives.

Two alternatives that match the same constructor C are similar if their right-hand sides are similar under an extended Renaming that maps the variable patterns from the first alternative to the corresponding variable patterns from the second alternative. Additionally, the type annotations of their variable patterns must be similar (if there are any).

 Γ ∪ { x₁ ↦ y₁, …, xₙ ↦ yₙ } ⊢ e ≈ f, Γ ⊢ p₁ ≈ q₁, …, Γ ⊢ pₙ ≈ qₙ
——————————————————————————————————————————————————————————————————
            Γ ⊢ C p₁ … pₙ -> e ≈ C q₁ … qₙ -> f

where xᵢ and yᵢ denote the names of the variables bound by the patterns pᵢ and qᵢ respectively.

case expression alternatives refer to the matched constructor, the types the type annotations of the variable patterns refer to and the references of the right-hand side that are not bound by the variable patterns.

Applies the given type substitution to the right-hand side of the given case-expression alternative.

Applies the given expression substitution to the right-hand side of the given case-expression alternative.

Pretty instance for constructor patterns.

Constructor patterns refer to the matched constructor.

Pretty instance for variable patterns.

Instance to get the name of a let-binding.

Two variable patterns are similar if they either both don't have a type annotation or are annotated with similar types.

                     Γ ⊢ τ ≈ τ'
———————————  ——————————————————————————
 Γ ⊢ x ≈ y    Γ ⊢ (x :: τ) ≈ (y :: τ')

If one of the patterns has a bang pattern, the other one needs one as well.

                       Γ ⊢ τ ≈ τ'
—————————————  ————————————————————————————
 Γ ⊢ !x ≈ !y    Γ ⊢ !(x :: τ) ≈ !(y :: τ')

Variable patterns refer to the types used in their type annotation.

Applies the given type substitution to the type annotation of the given variable pattern.

Pretty instance for let expression binds.

Instance to get the name of a let-binding.

Two let bindings are similar if their variable pattern and expression are are similar.

 Γ' ⊢ p ≈ q  , Γ' ⊢ e ≈ f
——————————————————————————
    Γ ⊢ p = e ≈ q = f

Applies the given type substitution to the variable pattern and expression of the given let binding.

Applies the given expression substitution to an the right-hand side of a let binding.

The variable that is bound by the binding is not renamed by this instance. The ApplySubst instance for expressions renames all variables that are bound by let expressions.