Qualified constructors (#3337)

- Closes #3328

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);
```
3. 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
```

app/Commands/Format.hs

@@ -50,16 +50,22 @@ targetFromOptions opts = do
 formatProject ::
   forall r.
   (Members (ScopeEff ': Output FormattedFileInfo ': AppEffects) r) =>
+  Migration ->
   Sem r FormatResult
-formatProject = silenceProgressLog . runPipelineOptions . runPipelineSetup $ do
-  res :: [ProcessedNode ScoperResult] <- processProjectUpToScoping
-  pkgId :: PackageId <- (^. entryPointPackageId) <$> ask
-  res' :: [(ImportNode, SourceCode)] <- runReader pkgId $ forM res $ \node -> do
-    src <- formatModuleInfo node
-    return (node ^. processedNode, src)
-  formatRes <- formatProjectSourceCode res'
-  formatPkgRes <- formatPackageDotJuvix
-  return (formatRes <> formatPkgRes)
+formatProject migr = silenceProgressLog
+  . runPipelineOptions
+  . local (set pipelineMigration migr)
+  . runPipelineSetup
+  $ do
+    mpkg <- asks (^. entryPointMainPackageId)
+    res :: [ProcessedNode ScoperResult] <- runReader mpkg processProjectUpToScoping
+    pkgId :: PackageId <- (^. entryPointPackageId) <$> ask
+    res' :: [(ImportNode, SourceCode)] <- runReader pkgId $ forM res $ \node -> do
+      src <- formatModuleInfo node
+      return (node ^. processedNode, src)
+    formatRes <- formatProjectSourceCode res'
+    formatPkgRes <- formatPackageDotJuvix
+    return (formatRes <> formatPkgRes)
 
 formatPackageDotJuvix :: forall r. (Members (Output FormattedFileInfo ': ScopeEff ': AppEffects) r) => Sem r FormatResult
 formatPackageDotJuvix = do
@@ -72,7 +78,7 @@ runCommand opts = do
   runOutputSem (renderFormattedOutput target opts) . runScopeFileApp $ do
     res <- case target of
       TargetFile p -> format p
-      TargetProject -> formatProject
+      TargetProject -> formatProject (opts ^. formatMigration)
       TargetStdin -> do
         entry <- getEntryPointStdin
         runReader entry formatStdin
@@ -98,7 +104,13 @@ renderModeFromOptions target opts formattedInfo
       | formattedInfo ^. formattedFileInfoContentsModified = res
       | otherwise = NoEdit Silent
 
-renderFormattedOutput :: forall r. (Members '[EmbedIO, App, Files] r) => FormatTarget -> FormatOptions -> FormattedFileInfo -> Sem r ()
+renderFormattedOutput ::
+  forall r.
+  (Members '[EmbedIO, App, Files] r) =>
+  FormatTarget ->
+  FormatOptions ->
+  FormattedFileInfo ->
+  Sem r ()
 renderFormattedOutput target opts fInfo = do
   let renderMode = renderModeFromOptions target opts fInfo
   outputResult renderMode

app/Commands/Format/Options.hs

@@ -5,12 +5,27 @@ import CommonOptions
 data FormatOptions = FormatOptions
   { _formatInput :: Maybe (AppPath FileOrDir),
     _formatCheck :: Bool,
+    _formatMigration :: Migration,
     _formatInPlace :: Bool
   }
   deriving stock (Data)
 
 makeLenses ''FormatOptions
 
+parseMigration :: Parser Migration
+parseMigration = do
+  m <-
+    optional $
+      option
+        (enumReader (Proxy @Migrate))
+        ( long "migration"
+            <> metavar "MIGRATION"
+            <> completer (enumCompleter (Proxy @Migrate))
+            <> help "Migrates files in a project (doesn't work in single file mode or stdin)"
+        )
+
+  pure (Migration m)
+
 parseInputFileOrDir :: Parser (AppPath FileOrDir)
 parseInputFileOrDir = do
   _pathPath <-
@@ -26,6 +41,7 @@ parseInputFileOrDir = do
 parseFormat :: Parser FormatOptions
 parseFormat = do
   _formatInput <- optional parseInputFileOrDir
+  _formatMigration <- parseMigration
   _formatCheck <-
     switch
       ( long "check"

app/Commands/Markdown.hs

@@ -47,7 +47,8 @@ goProject ::
   (Members (Reader MarkdownOptions ': AppEffects) r) =>
   Sem r ()
 goProject = runPipelineOptions . runPipelineSetup $ do
-  res :: [ProcessedNode ScoperResult] <- processProjectUpToScoping
+  mpkg <- asks (^. entryPointMainPackageId)
+  res :: [ProcessedNode ScoperResult] <- runReader mpkg processProjectUpToScoping
   forM_ res (goScoperResult . (^. processedNodeData))
 
 goScoperResult :: (Members (Reader MarkdownOptions ': AppEffects) r) => Scoper.ScoperResult -> Sem r ()

examples/demo/Demo.juvix

@@ -27,6 +27,8 @@ type Tree (A : Type) :=
       right : Tree A;
     };
 
+open Tree using {leaf; node} public;
+
 mirror {A} : (tree : Tree A) -> Tree A
   | tree@(leaf _) := tree
   | (node x l r) := node x (mirror r) (mirror l);

examples/milestone/Bank/Bank.juvix

@@ -20,6 +20,8 @@ type Token :=
     amount : Nat;
   };
 
+open Token using {mkToken} public;
+
 --- This module defines the type for balances and its associated operations.
 module Balances;
   Balances : Type := List (Pair Field Nat);

examples/milestone/Hanoi/Hanoi.juvix

@@ -34,6 +34,8 @@ type Peg :=
   | middle
   | right;
 
+open Peg using {left; middle; right} public;
+
 showPeg : Peg -> String
   | left := "left"
   | middle := "middle"
@@ -46,6 +48,8 @@ type Move :=
     to : Peg;
   };
 
+open Move using {mkMove} public;
+
 showMove (move : Move) : String :=
   showPeg (Move.from move) ++str " -> " ++str showPeg (Move.to move);
 

examples/milestone/TicTacToe/Logic/Board.juvix

@@ -12,6 +12,8 @@ type Board :=
     squares : List (List Square);
   };
 
+open Board using {mkBoard} public;
+
 --- Returns the list of numbers corresponding to the empty ;Square;s
 possibleMoves : (list : List Square) -> List Nat
   | nil := nil

examples/milestone/TicTacToe/Logic/GameState.juvix

@@ -12,13 +12,17 @@ type Error :=
   | --- a fatal occurred
     terminate : String → Error;
 
+open Error using {noError; continue; terminate} public;
+
 type GameState :=
   mkGameState@{
     board : Board;
     player : Symbol;
     error : Error;
   };
 
+open GameState using {mkGameState} public;
+
 --- Textual representation of a ;GameState;
 showGameState (state : GameState) : String := showBoard (GameState.board state);
 

examples/milestone/TicTacToe/Logic/Square.juvix

@@ -15,9 +15,11 @@ type Square :=
       player : Symbol;
     };
 
+open Square using {empty; occupied} public;
+
 instance
 eqSquareI : Eq Square :=
-  mkEq@{
+  Eq.mk@{
     isEqual (square1 square2 : Square) : Bool :=
       case square1, square2 of
         | empty m, empty n := m == n

examples/milestone/TicTacToe/Logic/Symbol.juvix

@@ -10,9 +10,11 @@ type Symbol :=
   | --- The cross token
     X;
 
+open Symbol using {O; X} public;
+
 instance
 eqSymbolI : Eq Symbol :=
-  mkEq@{
+  Eq.mk@{
     isEqual (sym1 sym2 : Symbol) : Bool :=
       case sym1, sym2 of
         | O, O := true

include/package-base/Juvix/Builtin/V1/Bool.juvix

@@ -5,3 +5,5 @@ builtin bool
 type Bool :=
   | false
   | true;
+
+open Bool using {false; true} public;

include/package-base/Juvix/Builtin/V1/List.juvix

@@ -2,11 +2,13 @@ module Juvix.Builtin.V1.List;
 
 import Juvix.Builtin.V1.Fixity open;
 
-syntax operator :: cons;
+syntax operator List.:: cons;
 --- Inductive list.
 builtin list
 type List (A : Type) :=
   | --- The empty list
     nil
   | --- An element followed by a list
     :: A (List A);
+
+open List using {nil; ::} public;

include/package-base/Juvix/Builtin/V1/Maybe.juvix

@@ -6,3 +6,5 @@ builtin maybe
 type Maybe A :=
   | nothing
   | just A;
+
+open Maybe using {nothing; just} public;

include/package-base/Juvix/Builtin/V1/Nat/Base.juvix

@@ -8,6 +8,8 @@ type Nat :=
   | zero
   | suc Nat;
 
+open Nat using {zero; suc} public;
+
 syntax operator + additive;
 
 --- Addition for ;Nat;s.

include/package/PackageDescription/Basic.juvix

@@ -13,3 +13,5 @@ type Package :=
   --- Use this in situations where you don't want the package configuration file
   --- to use the standard library.
   basicPackage;
+
+open Package using {basicPackage} public;

include/package/PackageDescription/V1.juvix

@@ -17,6 +17,8 @@ type Package :=
     buildDir : Maybe String
   };
 
+open Package using {mkPackage} public;
+
 --- A ;SemVer; defines a version that conforms to the Semantic Versioning specification.
 type SemVer :=
   mkSemVer {
@@ -27,11 +29,13 @@ type SemVer :=
     meta : Maybe String
   };
 
+open SemVer using {mkSemVer} public;
+
 --- A ;Dependency; defines a Juvix package dependency.
 type Dependency :=
   | --- A filesystem path to another Juvix Package.
     path {path : String}
-  | --- A ;git; repository containing a Juvix package at its root
+  | --- A git repository containing a Juvix package at its root
     git {
       -- A name for this dependency
       name : String;
@@ -40,9 +44,11 @@ type Dependency :=
       -- The git ref to checkout
       ref : String
     }
-  | --- The ;defaultStdlib; that is bundled with the Juvix compiler.
+  | --- The default Stdlib that is bundled with the Juvix compiler.
     defaultStdlib;
 
+open Dependency using {path; git; defaultStdlib} public;
+
 --- The default version used in `defaultPackage`.
 defaultVersion : SemVer := mkVersion 0 0 0;
 

include/package/PackageDescription/V2.juvix

@@ -17,6 +17,8 @@ type Package :=
     buildDir : Maybe String
   };
 
+open Package using {mkPackage} public;
+
 --- A ;SemVer; defines a version that conforms to the Semantic Versioning specification.
 type SemVer :=
   mkSemVer@{
@@ -27,11 +29,13 @@ type SemVer :=
     meta : Maybe String
   };
 
+open SemVer using {mkSemVer} public;
+
 --- A ;Dependency; defines a Juvix package dependency.
 type Dependency :=
   | --- A filesystem path to another Juvix Package.
     path@{pathStr : String}
-  | --- A ;git; repository containing a Juvix package at its root
+  | --- A git repository containing a Juvix package at its root
     git@{
       -- A name for this dependency
       name : String;
@@ -40,9 +44,11 @@ type Dependency :=
       -- The git ref to checkout
       ref : String
     }
-  | --- The ;defaultStdlib; that is bundled with the Juvix compiler.
+  | --- The default Stdlib that is bundled with the Juvix compiler.
     defaultStdlib;
 
+open Dependency using {path; git; defaultStdlib} public;
+
 --- Construct a ;SemVer; with useful default arguments.
 mkVersion
   (major minor patch : Nat)

src/Juvix/Compiler/Concrete/Language/Base.hs

@@ -295,12 +295,13 @@ deriving stock instance Ord (Statement 'Scoped)
 
 data ReservedInductiveDef = ReservedInductiveDef
   { _reservedInductiveDef :: InductiveDef 'Parsed,
+    _reservedInductiveConstructors :: NonEmpty S.Symbol,
     _reservedInductiveDefModule :: Module 'Parsed 'ModuleLocal
   }
   deriving stock (Show, Eq, Ord)
 
 data ProjectionDef s = ProjectionDef
-  { _projectionConstructor :: S.Symbol,
+  { _projectionConstructor :: SymbolType s,
     _projectionField :: SymbolType s,
     _projectionType :: ExpressionType s,
     _projectionKind :: ProjectionKind,
@@ -3340,8 +3341,8 @@ instance HasLoc (OpenModule s short) where
       <>? fmap getLoc _openModuleUsingHiding
       <>? getLocPublicAnn _openModulePublic
 
-instance HasLoc (ProjectionDef s) where
-  getLoc = getLoc . (^. projectionConstructor)
+instance (SingI s) => HasLoc (ProjectionDef s) where
+  getLoc = getLocSymbolType . (^. projectionConstructor)
 
 getLocFunctionSymbolType :: forall s. (SingI s) => FunctionSymbolType s -> Interval
 getLocFunctionSymbolType = case sing :: SStage s of

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -1635,7 +1635,7 @@ instance (SingI s) => PrettyPrint (ProjectionDef s) where
       <+> noLoc ":= projection"
       <+> noLoc (pretty _projectionFieldIx)
       <+> noLoc "for"
-      <+> ppCode _projectionConstructor
+      <+> ppSymbolType _projectionConstructor
 
 ppReservedInductiveDefType :: forall s. (SingI s) => PrettyPrinting (ReservedInductiveDefType s)
 ppReservedInductiveDefType x = case sing :: SStage s of

src/Juvix/Compiler/Concrete/Translation/FromParsed.hs

@@ -17,7 +17,9 @@ import Juvix.Prelude
 fromParsed ::
   ( Members
       '[ HighlightBuilder,
+         Reader Migration,
          Reader PackageId,
+         Reader MainPackageId,
          Reader ModuleTable,
          Reader Parsed.ParserResult,
          Error JuvixError,
@@ -27,7 +29,6 @@ fromParsed ::
   ) =>
   Sem r ScoperResult
 fromParsed = do
-  pkg <- ask
   tab <- ask
   r <- ask
-  scopeCheck pkg (getScopedModuleTable tab) r
+  scopeCheck (getScopedModuleTable tab) r