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

Qualified constructors #3337

Draft
wants to merge 34 commits into
base: main
Choose a base branch
from
Draft

Qualified constructors #3337

wants to merge 34 commits into from

Conversation

janmasrovira
Copy link
Collaborator

@janmasrovira janmasrovira commented Feb 18, 2025

This pr makes an important breaking change to the Juvix scoper. Previously, when defining a type, the constructors were put into the current scope. After this pr, they must be accessed through the type module that is generated.

E.g.

type Unit := unit;

-- BEFORE
fun : Unit := unit;

-- AFTER
fun : Unit := Unit.unit;
-- or
open Unit using {unit} public;
fun : Unit := unit;

Additionally, this pr adds the option --migration to the juvix format command. This option takes the identity of some migration we want to apply. For the purposes of migrating the existing codebase, I've added the export-constructors migration. When this option is given, the juvix formatter automatically adds an open statement after each type definition.
E.g. Run juvix format --migration export-constructors Example.juvix.

module Example;

type T := a | b;

Result:

module Example;

type T :=
  | a
  | b;

open T using {a; b} public;

Using this method to migrate is not guaranteed to succeed, and manual adjustments might need to be made.

  1. Forward references to constructors need to be qualified. E.g.
syntax operator :: cons;  -- BEFORE
syntax operator List.:: cons;  -- AFTER

type List (A : Type) :=
  | nil
  | :: A (List A);
  1. Another thing to consider is that the migration should not be run twice on the same file, because then there will be repeated redundant open statements:
open List using {nil; ::} public;

open List using {nil; ::} public;

I created a fish script for this:

#!/usr/bin/env fish

cd ./tests
for dir in (fd -a -t f "Package.juvix" | xargs -I{} dirname "{}")
    set witness "$dir/.migrated"
    if test -e $witness
        echo "Already processed: $dir"
    else
        echo "Processing $dir"
        if juvix format  $dir --migration export-constructors --in-place
            touch $witness
        end
    end
end

@janmasrovira janmasrovira self-assigned this Feb 18, 2025
@janmasrovira janmasrovira force-pushed the qualified-constructors branch 7 times, most recently from 108d6aa to a2d623c Compare February 21, 2025 16:47
@janmasrovira janmasrovira marked this pull request as ready for review February 24, 2025 16:47
@janmasrovira janmasrovira force-pushed the qualified-constructors branch from 9c1bfcc to b230296 Compare February 25, 2025 08:52
@@ -8,6 +8,8 @@ type Nat :=
| zero
| suc Nat;

open Nat using {zero; suc} public;

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think for Nat it would be reasonable to have zero and suc qualified. They aren't used very often. But we don't need to change this in this PR.

@janmasrovira janmasrovira force-pushed the qualified-constructors branch 3 times, most recently from caa36c1 to de840b5 Compare February 26, 2025 08:03
@janmasrovira janmasrovira marked this pull request as draft February 26, 2025 15:57
@janmasrovira janmasrovira force-pushed the qualified-constructors branch from de840b5 to 50f9597 Compare February 26, 2025 23:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Don't export record constructor names
2 participants