Skip to content

Commit

Permalink
Add format stdin smoke tests
Browse files Browse the repository at this point in the history
  • Loading branch information
vrom911 committed Apr 20, 2023
1 parent 46360a7 commit 65d7803
Show file tree
Hide file tree
Showing 2 changed files with 42 additions and 2 deletions.
3 changes: 1 addition & 2 deletions tests/positive/issue1731/builtinTrace.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ axiom trace : {A : Type} → A → A;

terminating
f : Nat → Nat → Nat;
f x y := if (x == 0) y (trace x >>> (f (sub x 1) y));
f x y := if (x == 0) y (trace x >>> f (sub x 1) y);

{-
f 4 0 =
Expand All @@ -19,6 +19,5 @@ trace 4 >>> f 3 0
=> trace 4 >>> trace 3 >>> trace 2 >>> trace 1 0
= 0
-}

main : IO;
main := printNatLn $ f 4 0;
41 changes: 41 additions & 0 deletions tests/smoke/Commands/format.smoke.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -128,3 +128,44 @@ tests:
stderr:
contains: "error"
exit-status: 1

- name: format-stdin
command:
- juvix
- --stdin
- format
- positive/Format.juvix
stdin: "module Format; open import Stdlib.Prelude; main : Nat; main := 5; "
stdout:
contains: |
module Format;
open import Stdlib.Prelude;
main : Nat;
main := 5;
exit-status: 1

- name: format-stdin-file-does-not-exist
command:
- juvix
- --stdin
- format
- positive/NonExistingFormat.juvix
stdin: "module Format; open import Stdlib.Prelude; main : Nat; main := 5; "
stderr:
contains: |
positive/NonExistingFormat.juvix: openFile: does not exist (No such file or directory)
exit-status: 1

- name: format-stdin-module-name-not-file-name
command:
- juvix
- --stdin
- format
- positive/Format.juvix
stdin: "module OtherFormat; open import Stdlib.Prelude; main : Nat; main := 5; "
stderr:
contains: |-
The top module
exit-status: 1

0 comments on commit 65d7803

Please sign in to comment.