repl.smoke.yaml

working-directory: ./../../../tests/

tests:
  - name: repl-doc
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":doc Nat"
    stdout:
      contains: |
        --- Inductive natural numbers. I.e. whole non-negative numbers.
    exit-status: 0

  - name: repl-doc-no-doc
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":doc suc"
    stdout:
      contains: |
        No documentation available for suc
    exit-status: 0

  - name: repl-def
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":def suc"
    stdout:
      contains: |
        --- Inductive natural numbers. I.e. whole non-negative numbers.
        builtin nat type Nat :=
          | zero : Nat
          | suc : Nat → Nat
    exit-status: 0

  - name: repl-def-error
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":def 1 Nat"
    stdout:
      matches: |
        .*
    stderr:
      contains: |
        :def expects one or more identifiers
    exit-status: 0

  - name: repl-def-multiple
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":def + (+) (((+)))"
    stdout:
      contains: |
        --- Addition for ;Nat;s.
        builtin nat-plus + : Nat → Nat → Nat;
        + zero b := b;
        + (suc a) b := suc (a + b);
    exit-status: 0

  - name: repl-def-infix
    command:
      - juvix
      - repl
      - ../examples/milestone/HelloWorld/HelloWorld.juvix
    stdin: ":def +"
    stdout:
      contains: |
        --- Addition for ;Nat;s.
        builtin nat-plus + : Nat → Nat → Nat;
        + zero b := b;
        + (suc a) b := suc (a + b);
    exit-status: 0

  - name: open
    command:
      - juvix
      - repl
    stdout:
      contains: "Juvix REPL"
    exit-status: 0

  - name: infer-mutually-recursive-let-expression
    command:
      - juvix
      - repl
    stdin: ":type let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10"
    stdout:
      contains:
        "Bool"
    exit-status: 0

  - name: eval-mutually-recursive-let-expression
    command:
      - juvix
      - repl
    stdin: "let even : _; odd : _; odd zero := false; odd (suc n) := not (even n); even zero := true; even (suc n) := not (odd n) in even 10"
    stdout:
      contains:
        "true"
    exit-status: 0

  - name: quit
    command:
      - juvix
      - repl
    stdout:
      contains: "Juvix REPL"
    stdin: ":quit"
    exit-status: 0

  - name: load-stdlib-by-default
    command:
      - juvix
      - repl
    stdout:
      matches:
        regex: |
          Juvix REPL .*
          OK loaded: .*/stdlib/Stdlib/Prelude.juvix
    exit-status: 0

  - name: version-shows-same-juvix-version
    command:
      - juvix
      - repl
    stdin: ":version"
    stdout:
      matches:
        regex: |
          Juvix REPL version ([0-9]+\.[0-9]+\.[0-9]\-[a-z0-9]+): .*
          OK loaded: .*
          Stdlib.Prelude> \1
    exit-status: 0

  - name: check-type-null
    command:
      - juvix
      - repl
    stdout:
      contains: "{A : Type} → List A → Bool"
    stdin: ":type null"
    exit-status: 0

  - name: check-type-suc
    command:
      - juvix
      - repl
    stdout:
      contains: "Nat → Nat"
    stdin: ":type suc"
    exit-status: 0

  - name: check-type-suc-short
    command:
      - juvix
      - repl
    stdout:
      contains: "Nat → Nat"
    stdin: ":t suc"
    exit-status: 0

  - name: check-type-suc-short-stdlib
    command:
      shell:
        - bash
      script: |
        cd ./../juvix-stdlib && juvix repl Stdlib/Prelude.juvix
    stdout:
      contains: "Nat → Nat"
    stdin: ":t suc"
    exit-status: 0

  - name: eval-and-operations
    command:
      - juvix
      - repl
    stdin: "true && false"
    stdout:
      matches: |
        Juvix REPL .*
        OK loaded: .*
        Stdlib.Prelude> false
    exit-status: 0

  - name: eval-and-operations-with-spaces
    command:
      - juvix
      - repl
    stdin: "   true    &&    false"
    stdout:
      contains:
        "false"
    exit-status: 0

  - name: eval-suc-true
    command:
      - juvix
      - repl
    stdin: "suc true"
    stdout:
      contains:
        "Stdlib.Prelude> "
    stderr:
      contains: |
        The expression true has type:
          Bool
        but is expected to have type:
          Nat
    exit-status: 0

  - name: eval-let-expression
    command:
      - juvix
      - repl
    stdin: "let x : Nat; x := 2 + 1 in x"
    stdout:
      contains:
        "3"
    exit-status: 0

  - name: load-builtin-bool
    command:
      shell:
        - bash
      script: |
        cd ./Internal/positive/ && juvix repl
    stdin: ":load BuiltinBool.juvix"
    stdout:
      contains:
        "BuiltinBool>"
    exit-status: 0

  - name: load-builtin-bool-with-spaces
    command:
      shell:
        - bash
      script: |
        cd ./Internal/positive/ && juvix repl
    stdin: ":load    BuiltinBool.juvix"
    stdout:
      contains:
        BuiltinBool>
    exit-status: 0

  - name: load-builtin-bool-short-form
    command:
      shell:
        - bash
      script: |
        cd ./Internal/positive/ && juvix repl
    stdin: |
      :l BuiltinBool.juvix
      main
    stdout:
      contains: |
        true
    exit-status: 0

  - name: repl-file
    command:
      - juvix
      - repl
    args:
      - Internal/positive/BuiltinBool.juvix
    stdin: main
    stdout:
      contains: |
        true
    exit-status: 0

  - name: root-global
    command:
      - juvix
      - repl
    stdin: ":root"
    stdout:
      matches: |
        Juvix REPL .*
        OK loaded: .*
        Stdlib.Prelude> .*/global-project/
    exit-status: 0

  - name: eval-adding-two-literal-nats
    command:
      - juvix
      - repl
    stdin: "1 + 2"
    stdout:
      contains: |
        3
    exit-status: 0

  - name: repl-trace
    command:
      - juvix
      - repl
    args:
      - positive/issue1731/builtinTrace.juvix
    stdin: trace 2 >>> printNatLn 3
    stdout:
      contains: |
        3
    stderr: |
        2
    exit-status: 0

  - name: repl-trace-file
    command:
      - juvix
      - repl
    args:
      - positive/issue1731/builtinTrace.juvix
    stdin: f 4 0
    stdout:
      contains: |
       0
    stderr: |
       4
       3
       2
       1
    exit-status: 0

  - name: repl-fail
    command:
      - juvix
      - repl
    args:
      - positive/issue1731/builtinFail.juvix
    stdin: main
    stdout:
      contains: |
        Get
    stderr:
      contains: |
        evaluation error: failure: Enough
    exit-status: 0

  - name: print-values
    command:
      - juvix
      - repl
    stdin: "nil"
    stdout:
      contains: "nil"
    exit-status: 0

  - name: core-repl-type
    command:
      - juvix
      - dev
      - core
      - repl
    stdin: ":t (\\(A : Type) \\(x : A) \\(y : A) \\(B : Type) \\(z : B) \\(_ : A) x) Int 1 2 String"
    stdout:
      contains: |
        String → Int → Int

  - name: repl-import-no-dependencies
    command:
      shell:
        - bash
      script: |
        cd positive/NoDependencies && juvix repl Empty.juvix
    stdin: "import Foo\nFoo.bar"
    stdout:
      contains:
        bar
    exit-status: 0

  - name: repl-import-no-dependencies-type
    command:
      shell:
        - bash
      script: |
        cd positive/NoDependencies && juvix repl Empty.juvix
    stdin: "import Foo\n:t Foo.bar"
    stdout:
      contains:
        Bar
    exit-status: 0

  - name: repl-invalid-import
    command:
      shell:
        - bash
      script: |
        cd positive/NoDependencies && juvix repl Empty.juvix
    stdin: "import Invalid"
    stdout:
      contains: OK loaded
    stderr:
      contains:
        The module Invalid does not exist
    exit-status: 0

  - name: repl-import-type-error
    command:
      shell:
        - bash
      script: |
        temp=$(mktemp -d)
        trap 'rm -rf -- "$temp"' EXIT
        cp negative/Internal/WrongType.juvix $temp
        cd $temp
        echo "module Empty;" > Empty.juvix
        touch juvix.yaml
        juvix repl Empty.juvix
    stdin: "import WrongType"
    stdout:
      contains: OK loaded
    stderr:
      contains:
        is expected to have type
    exit-status: 0

  - name: import-from-stdlib
    command:
      - juvix
      - repl
    stdin: "import Stdlib.Data.Int.Ord as Int\n1 Int.== 1"
    stdout:
      contains: "true"
    exit-status: 0

  - name: import-then-open-from-stdlib
    command:
      - juvix
      - repl
    stdin: "import Stdlib.Data.Int.Ord as Int\nopen Int\n1 == 1"
    stdout:
      contains: "true"
    exit-status: 0

  - name: open-import-from-stdlib
    command:
      - juvix
      - repl
    stdin: "open import Stdlib.Data.Int.Ord\n1 == 1"
    stdout:
      contains: "true"
    exit-status: 0

  - name: infix-constructors
    command:
      - juvix
      - repl
    stdin: "(::) :: nil {Nat -> List Nat -> List Nat}"
    stdout:
      contains: "(::) :: nil"
    exit-status: 0