1
1
mirror of https://github.com/anoma/juvix.git synced 2024-11-30 05:42:26 +03:00

Improve Set and Map modules in the standard library (#3120)

* Updates the standard library to
https://github.com/anoma/juvix-stdlib/pull/130
* Also changes `null` to `isEmpty`, which required updating some tests

---------

Co-authored-by: Paul Cadman <git@paulcadman.dev>
This commit is contained in:
Łukasz Czajka 2024-10-24 13:29:33 +02:00 committed by GitHub
parent e951df077d
commit 8f180ccfda
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
8 changed files with 16 additions and 16 deletions

View File

@ -44,4 +44,4 @@ won (state : GameState) : Bool :=
draw (state : GameState) : Bool :=
let
squares := Board.squares (GameState.board state);
in null (possibleMoves (flatten squares));
in isEmpty (possibleMoves (flatten squares));

@ -1 +1 @@
Subproject commit e164aa14503ff11dbcf0dc96bcd4cfa4d757b76d
Subproject commit 7c7162aca573d116825857da272d83d0fc8afcf7

View File

@ -14,13 +14,13 @@ map' {A B} (f : A → B) : List A → List B :=
-- TODO: Restore when anoma backend supports strings
-- terminating
-- map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
-- if (null x) nil (f (phead x) :: map'' f (tail x));
-- if (isEmpty x) nil (f (phead x) :: map'' f (tail x));
lst : List Nat := 0 :: 1 :: nil;
main : List Nat :=
trace (null lst)
>-> trace (null (nil {Nat}))
trace (isEmpty lst)
>-> trace (isEmpty (nil {Nat}))
>-> trace (head 1 lst)
>-> trace (tail lst)
>-> trace (head 0 (tail lst))

View File

@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
lst : List Nat := 0 :: 1 :: nil;
main : Nat :=
ite (null lst) 1 0
+ ite (null (nil {Nat})) 1 0
ite (isEmpty lst) 1 0
+ ite (isEmpty (nil {Nat})) 1 0
+ head 1 lst
+ head 0 (tail lst)
+ head 0 (tail (map ((+) 1) lst))

View File

@ -11,7 +11,7 @@ map' {A B} (f : A → B) : List A → List B :=
terminating
map'' {A B} {{Partial}} (f : A → B) (x : List A) : List B :=
ite (null x) nil (f (phead x) :: map'' f (tail x));
ite (isEmpty x) nil (f (phead x) :: map'' f (tail x));
lst : List Nat := 0 :: 1 :: nil;
@ -24,8 +24,8 @@ printNatListLn (lst : List Nat) : IO :=
printNatList lst >>> printString "\n";
main : IO :=
printBoolLn (null lst)
>>> printBoolLn (null (nil {Nat}))
printBoolLn (isEmpty lst)
>>> printBoolLn (isEmpty (nil {Nat}))
>>> printNatLn (head 1 lst)
>>> printNatListLn (tail lst)
>>> printNatLn (head 0 (tail lst))

View File

@ -12,8 +12,8 @@ map' {A B} (f : A → B) : List A → List B :=
lst : List Nat := 0 :: 1 :: nil;
main : Nat :=
ite (null lst) 1 0
+ ite (null (nil {Nat})) 1 0
ite (isEmpty lst) 1 0
+ ite (isEmpty (nil {Nat})) 1 0
+ head 1 lst
+ head 0 (tail lst)
+ head 0 (tail (map ((+) 1) lst))

View File

@ -68,14 +68,14 @@ tests:
Stdlib.Prelude> \1
exit-status: 0
- name: check-type-null
- name: check-type-isEmpty
command:
- juvix
- dev
- repl
stdout:
contains: "{A : Type} -> (list : List A) -> Bool"
stdin: ":type null"
stdin: ":type isEmpty"
exit-status: 0
- name: check-type-suc

View File

@ -151,13 +151,13 @@ tests:
Stdlib.Prelude> \1
exit-status: 0
- name: check-type-null
- name: check-type-isEmpty
command:
- juvix
- repl
stdout:
contains: "{A : Type} -> (list : List A) -> Bool"
stdin: ":type null"
stdin: ":type isEmpty"
exit-status: 0
- name: check-type-suc