Documentation

This should not simplify, because one of the branches of ifThenElse is not a Constr. Unless both branches are known constructors, the case-of-case transformation may increase the program size.

Similar to caseOfCase1, but the type of the true and false branches is [Integer] rather than Bool (note that Constr 0 has two parameters, x and xs).

The Delay should be floated into the lambda.

The Delay should not be floated into the lambda, because the argument (1 + 2) is not work-free.

The Delay should not be floated into the lambda in the first simplifier iteration, because one of the occurrences of a is not under Force. It should be floated into the lambda in the second simplifier iteration, after b is inlined.

A helper function to create a term which tests whether the inliner behaves as expected for a given pure or impure term. It receives a Quote that produces a term together with a list of free variables. The free variables are bound at the top level of the final term in order to ensure that the produced final term is well-scoped.

A single Var is pure.

force (delay a) is pure.

Note that this relies on forceDelayCancel to cancel the force and the delay, otherwise the inliner would treat the term as impure.

[(x -> y -> [x x]) (con integer 1)] is pure.

Note that the (con integer 1) won't get inlined: it isn't pre-inlined because x occurs twice, and it isn't post-inlined because costIsAcceptable Constant{} = False. However, the entire term will be inlined since it is pure.

force ([(x -> delay (y -> [x x])) (delay ([error (con integer 1)]))]) is pure, but it is very tricky to see so. It requires us to match up a force and a delay through several steps of intervening computation.

error is impure.

force (delay error) is impure.

force (force (force (delay (delay (delay (error)))))) is impure, since it is the same as error.

force (force (force (delay (delay a)))) is impure, since a may expand to an impure term such as error.

(a -> f (a 0 1) (a 2)) (x y -> g x y)

The first occurrence of a should be inlined because doing so does not increase the size or the cost.

The second occurrence of a should be unconditionally inlined in the second simplifier iteration, but in this test we are only running one iteration.

The UPLC term in this test should come from the following TPLC term after erasing its types:

(/\(p :: *) -> \(x : p) -> /\(q :: *) -> \(y : q) -> /\(r :: *) -> \(z : r) -> z)
  Int 1 Int 2 Int 3

This case is simple in the sense that each type abstraction is followed by a single term abstraction.

A test for the case when there are multiple applications between the Force at the top and the Delay at the top of the term inside the abstractions/applications.

A test for the case when there are multiple type abstractions over a single term abstraction/application.

The UPLC term in this test should come from the following TPLC term after erasing its types:

(/\(p1 :: *) (p2 :: *) -> \(x : p2) ->
  /\(q1 :: *) (q2 :: *) (q3 :: *) -> \(y1 : q1) (y2 : q2) (y3 : String) ->
    /\(r :: *) -> \(z1 : r) -> \(z2 : r) ->
      /\(t :: *) -> \(f : p1 -> q1 -> q2 -> String -> r -> r -> String) ->
        f x y1 y2 y3 z1 z2
) Int Int 1 Int String Int 2 "foo" "bar" Int 3 3 ByteString
(funcVar : Int -> Int -> String -> String -> Int -> String)

Note this term has multiple interleaved type and term instantiations/applications.

This is the first example in Note [CSE].

This is the second example in Note [CSE].

This is the third example in Note [CSE].