-- The "=== inline ===" strings below are a hack around the fact that
-- Dex currently does two passes of inlining and prints the results of
-- both.  Surrounding the CHECK block with these commands constrains
-- the body to occur in the output from the first inlining pass.

@noinline
def id'(x:Nat) -> Nat = x

-- CHECK-LABEL: Inline for into for
"Inline for into for"

%passes inline
:pp
  xs = for i:(Fin 10). ordinal i
  for j. xs[j] + 2
-- CHECK: === inline ===
-- CHECK: for
-- CHECK-NOT: for
-- CHECK: === inline ===

-- CHECK-LABEL: Inline for into sum
"Inline for into sum"

%passes inline
:pp sum for i:(Fin 10). ordinal i
-- CHECK: === inline ===
-- CHECK: for
-- CHECK-NOT: for
-- CHECK: === inline ===

-- CHECK-LABEL: Inline nested for into for
"Inline nested for into for"

%passes inline
:pp
  xs = for i:(Fin 10). for j:(Fin 20). ordinal i * ordinal j
  for j i. xs[i, j] + 2
-- CHECK: === inline ===
-- CHECK: for
-- CHECK: for
-- CHECK-NOT: for
-- CHECK: === inline ===

-- CHECK-LABEL: Inlining does not reorder effects
"Inlining does not reorder effects"

-- Note that it _would be_ legal to reorder independent effects, but
-- the inliner currently does not do that.  But the effect in this
-- example is not legal to reorder in any case.

%passes inline
:pp run_state 0 \ct.
  xs = for i:(Fin 10).
    ct := (get ct) + 1
    ordinal i
  for j.
    ct := (get ct) * 2
    xs[j] + 2
-- CHECK: === inline ===
-- CHECK: for
-- CHECK: for
-- CHECK: === inline ===

-- CHECK-LABEL: Inlining does not duplicate the inlinee through beta reduction
"Inlining does not duplicate the inlinee through beta reduction"

-- The check is for the error call in the dynamic check that `ix` has
-- type `Fin 100`.
%passes inline
:pp
  ix = (id' 20)@(Fin 100)
  (for i:(Fin 100). ordinal i + ordinal i)[ix]
-- CHECK: === inline ===
-- CHECK: error
-- CHECK-NOT: error
-- CHECK: === inline ===

-- CHECK-LABEL: Inlining does not violate type IR through beta reduction
"Inlining does not violate type IR through beta reduction"

-- Beta reducing this ix into the `i` index of the `for` should stop
-- before it produces anything a type expression can't handle, and
-- thus execute.

:p
  ix = (1@(Fin 2))
  sum (for i:(Fin 2) j:(..i). ordinal j)[ix]
-- CHECK: 1
-- CHECK-NOT: Compiler bug

-- CHECK-LABEL: Inlining simplifies case-of-known-constructor
"Inlining simplifies case-of-known-constructor"

-- Inlining xs exposes a case-of-known-constructor opportunity here;
-- the first inlining pass doesn't take it (yet) because it's
-- conservative about inlining `i` into the body of `xs`, but the
-- second pass does.
%passes inline
:pp
  xs = for i:(Either (Fin 3) (Fin 4)).
    case i of
      Left k -> 1
      Right k -> 2
  for j:(Fin 3). xs[Left j]
-- CHECK: === inline ===
-- CHECK: for
-- CHECK: case
-- CHECK: === inline ===
-- CHECK: for
-- CHECK-NOT: case

-- CHECK-LABEL: Inlining carries out the case-of-case optimization
"Inlining carries out the case-of-case optimization"

-- Before inlining there are two cases, but attempting to inline `x`
-- reveals a case-of-case opprtunity, which in turn exposes
-- case-of-known-constructor in each branch, leading to just one case
-- in the end.
%passes inline
:pp
  x = if id'(3) > 2
        then Just 4
        else Nothing
  case x of
    Just a -> a * a
    Nothing -> 0
-- CHECK: === inline ===
-- CHECK: case
-- CHECK-NOT: case
-- CHECK: === inline ===