reserve constructors in type module

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