import { Layout, Txt, makeScene2D } from "@motion-canvas/2d";
import {
  Direction,
  beginSlide,
  createRef,
  slideTransition,
} from "@motion-canvas/core";
import { theme } from "../theme";

const substitution = [
  "β-reduce [ (λ x . x) y ] => y\n\n",
  "Formal definition:",
  "1. x[x := N] = N",
  "2. y[x := N] = y if y != x",
  "3. (M N)[x := P] = (M[x := P]) (N[x := P])",
  "4. (λ x . M)[x := N] = λ x . M",
  "5. (λ y . M)[x := N] = λ y . (M[x := N]) if y != x and y is not _free_ in N",
  " +=> A variable is _free_ in a lambda term if it is not bound by a λ abstraction.",
];

export default makeScene2D(function* (view) {
  const rules = createRef<Txt>();

  view.add(
    <Layout layout direction="column" alignItems="center">
      <Txt fontSize={40} fontFamily={theme.font} fill={theme.text.hex}>
        The Lambda Calculus - Substitution Rules
      </Txt>
      <Txt
        ref={rules}
        fontSize={30}
        fontFamily={theme.font}
        fill={theme.text.hex}
      ></Txt>
    </Layout>
  );

  yield* slideTransition(Direction.Right);
  yield* beginSlide("The Lambda Calculus - Substitutions");

  for (const rule of substitution) {
    yield* rules().text(rules().text() + "\n\n" + rule, 1);
    yield* beginSlide("substitution - " + rule);
  }
});