Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add deriving for Eq #3176

Merged
merged 10 commits into from
Nov 22, 2024
Merged

Add deriving for Eq #3176

merged 10 commits into from
Nov 22, 2024

Conversation

janmasrovira
Copy link
Collaborator

@janmasrovira janmasrovira commented Nov 14, 2024

This pr adds automatic implementation of Eq instances for inductive types. To create such an instance the user will use the same syntax as a regular instance with two differences.

  1. It is prefixed with the deriving keyword.
  2. It has no body.

E.g.

deriving instance
eqProductI {A B} {{Eq A}} {{Eq B}} : Eq (Pair A B);

This desugars into an instance that returns true when the constructors match and all arguments are equal according to their respective instances. There is no special handling of type errors occurring in the generated code. I.e. if the user forgets a necessary instance argument in the type signature, a type error will occur in the generated code.

Stdlib PR

Future work

@janmasrovira janmasrovira added enhancement New feature or request deriving labels Nov 14, 2024
@janmasrovira janmasrovira self-assigned this Nov 14, 2024
@janmasrovira janmasrovira linked an issue Nov 14, 2024 that may be closed by this pull request
@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch 7 times, most recently from 26043c8 to 0f7c81a Compare November 20, 2024 16:21
commit 267b34a
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Wed Nov 20 14:18:11 2024 +0100

    give proper name of builtins

commit d0dc415
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Wed Nov 20 14:09:37 2024 +0100

    better error message

commit ccd9044
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Wed Nov 20 11:27:05 2024 +0100

    allow implicit args

commit 768f45d
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 18:44:50 2024 +0100

    stdlib

commit e778aaf
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 18:29:00 2024 +0100

    clean

commit 17939c7
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 18:27:22 2024 +0100

    update stdlib

commit 46d7388
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 18:18:22 2024 +0100

    pragmas

commit 58d1063
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 18:09:23 2024 +0100

    do not group deriving statements

commit 057fdbb
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 15:14:31 2024 +0100

    default case

commit d280fe7
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 14:55:36 2024 +0100

    fix

commit e3a7a76
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Tue Nov 19 09:57:22 2024 +0100

    from concrete

commit f8fd9f4
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Mon Nov 18 18:45:20 2024 +0100

    refactor Fail

commit a889cb6
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Mon Nov 18 18:00:27 2024 +0100

    wip

commit 734f7c1
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Mon Nov 18 13:00:14 2024 +0100

    wip

commit 6a2d7d2
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 15 13:29:44 2024 +0100

    parsing and printing deriving kw

commit 412a654
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 15 12:52:11 2024 +0100

    add deriving kw

commit 1101462
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Fri Nov 15 12:51:18 2024 +0100

    style

commit 3aeec44
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 14 17:39:09 2024 +0100

    remove section titles from parser

commit 15ec17d
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 14 15:29:57 2024 +0100

    update stdlib

commit 546b5b2
Author: Jan Mas Rovira <janmasrovira@gmail.com>
Date:   Thu Nov 14 11:27:04 2024 +0100

    make Eq builtin

commit 8658420
Author: Paul Cadman <git@paulcadman.dev>
Date:   Wed Nov 20 07:53:21 2024 +0000

    Support running nockma code with a running Anoma client (#3180)

    This PR:

    1. Adds a new interpretation for the Anoma effect, which makes gRPC
    calls to an existing Anoma client instead of spawning a new one.
    2. Adds a new `nockma run` mode, `with-client`, which can be used to run
    an Anoma program against a running Anoma client, using its URL and gRPC
    port.
    3. separates the `nockma run` command into subcommands.

    CLI docs:

    ## `nockma run`

    ```
    Usage: juvix dev nockma run COMMAND

      Subcommands used to run an Anoma program. Use with artefacts obtained from
      compilation with the anoma target

    Available options:
      -h,--help                Show this help text

    Available commands:
      builtin-evaluator        Run with the builtin Nockma evaluator
      ephemeral-client         Run with an ephemeral Anoma client
      with-client              Run with a running Anoma client
    ```

    ### `with-client`

    ```
    Usage: juvix dev nockma run with-client
             NOCKMA_FILE [--args ARGS_FILE] (-p|--grpc-port PORT) [--url URL]

      Run with a running Anoma client

    Available options:
      NOCKMA_FILE              Path to a .nockma file
      --args ARGS_FILE         Path to file containing args. The args file should
                               contain a list (i.e. to pass 2 and [1 4] as args, the
                               contents should be [2 [1 4] 0]).
      -p,--grpc-port PORT      The GRPC port of a running Anoma client
      --url URL                The URL of a running Anoma client. default: localhost
      -h,--help                Show this help text
    ```

    ### `ephemeral-client`

    ```
    Usage: juvix dev nockma run ephemeral-client
             NOCKMA_FILE [--args ARGS_FILE] --anoma-dir ANOMA_DIR

      Run with an ephemeral Anoma client

    Available options:
      NOCKMA_FILE              Path to a .nockma file
      --args ARGS_FILE         Path to file containing args. The args file should
                               contain a list (i.e. to pass 2 and [1 4] as args, the
                               contents should be [2 [1 4] 0]).
      --anoma-dir ANOMA_DIR    Path to anoma repository
      -h,--help                Show this help text
    ```

    ### `builtin-evaluator`

    ```
    Usage: juvix dev nockma run builtin-evaluator
             NOCKMA_FILE [--args ARGS_FILE] [--profile]

      Run with the builtin Nockma evaluator

    Available options:
      NOCKMA_FILE              Path to a .nockma file
      --args ARGS_FILE         Path to file containing args. The args file should
                               contain a list (i.e. to pass 2 and [1 4] as args, the
                               contents should be [2 [1 4] 0]).
      --profile                Report evaluator profiling statistics
      -h,--help                Show this help text
    ```

commit 455249d
Author: Łukasz Czajka <62751+lukaszcz@users.noreply.github.com>
Date:   Tue Nov 19 20:34:52 2024 +0100

    HTML generation: make the light theme lighter (#3168)

    * Closes #3141
    * Adds the `latte-light` theme with lighter background and makes it the
    default. This is a bit subjective, but in my opinion the light theme
    should not have a background darker than the browser window pane. It
    should be close to white.

commit eab02a7
Author: Paul Cadman <git@paulcadman.dev>
Date:   Tue Nov 19 17:34:13 2024 +0000

    Remove `GetAnomaProcess` from the Anoma effect (#3179)

    This PR removes `GetAnomaProcess` from the Anoma effect.

    Use the `launchAnoma` function to start a persistent Anoma client /
    server (used by `juvix dev anoma node`).

    Other changes:

    * It's no longer necessary to pass the protobuf files to `grpcurl`
    because the Anoma client now supports gRPC reflection.
    * We pass the elixir start command to `mix` via `-e` argument instead of
    using a temporary file.

    The purpose for this change is that we I want to add an interpreter for
    Anoma that makes gRPC calls to an exisitng Anoma client.
    `GetAnomaProcess` has no meaning for this interpreter.
@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch 2 times, most recently from ddb089c to 40f4a87 Compare November 20, 2024 17:42
@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch from 40f4a87 to 99af0ac Compare November 20, 2024 17:48
@janmasrovira janmasrovira marked this pull request as ready for review November 21, 2024 08:10
@lukaszcz lukaszcz self-requested a review November 21, 2024 09:05
Copy link
Collaborator

@lukaszcz lukaszcz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There is no positive compilation test. A major feature should have one.

@lukaszcz
Copy link
Collaborator

I don't know what change causes this, but whenever I'm trying to typecheck something with this branch's version of Juvix, I'm getting:

juvix: The yaml file "/Users/heliax/Documents/juvix/tests/Compilation/positive/.juvix-build/0.6.8/stdlib/juvix.yaml" does not exist
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:517:9 in juvix-0.6.8-LFi8mkf9iIiLR0CpABw6YB:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Pipeline/Package.hs:96:15 in juvix-0.6.8-LFi8mkf9iIiLR0CpABw6YB:Juvix.Compiler.Pipeline.Package

@janmasrovira janmasrovira marked this pull request as draft November 21, 2024 17:00
@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch 2 times, most recently from 317abf0 to 4bc40ec Compare November 21, 2024 17:20
@janmasrovira
Copy link
Collaborator Author

janmasrovira commented Nov 21, 2024

There is no positive compilation test. A major feature should have one.

I've added one in 256547e

@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch from 4bc40ec to 256547e Compare November 21, 2024 17:21
@janmasrovira janmasrovira force-pushed the 3137-deriving-mechanism branch from 256547e to d38c1ca Compare November 21, 2024 18:22
@lukaszcz
Copy link
Collaborator

I don't know what change causes this, but whenever I'm trying to typecheck something with this branch's version of Juvix, I'm getting:

juvix: The yaml file "/Users/heliax/Documents/juvix/tests/Compilation/positive/.juvix-build/0.6.8/stdlib/juvix.yaml" does not exist
CallStack (from HasCallStack):
  error, called at src/Juvix/Prelude/Base/Foundation.hs:517:9 in juvix-0.6.8-LFi8mkf9iIiLR0CpABw6YB:Juvix.Prelude.Base.Foundation
  error, called at src/Juvix/Compiler/Pipeline/Package.hs:96:15 in juvix-0.6.8-LFi8mkf9iIiLR0CpABw6YB:Juvix.Compiler.Pipeline.Package

This was caused by me forgetting to do git submodule init on a newly cloned Juvix repository.

@janmasrovira janmasrovira marked this pull request as ready for review November 22, 2024 09:26
Copy link
Collaborator

@lukaszcz lukaszcz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The generated code for recursive data types is inefficient, unless the pragma inline: case is used. I opened a separate issue for this and I'll fix it: #3186

@janmasrovira janmasrovira merged commit c100812 into main Nov 22, 2024
4 checks passed
@janmasrovira janmasrovira deleted the 3137-deriving-mechanism branch November 22, 2024 12:13
@paulcadman paulcadman added this to the 0.6.9 milestone Nov 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
deriving enhancement New feature or request traits
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Deriving mechanism
3 participants