Rename inductive constructor (#2255)

Rename `InductiveConstructorDef` -> `ConstructorDef` in `Concrete` so
that it is consistent with `Internal` and its field names

src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs

@@ -435,15 +435,15 @@ goInductive def = do
     inductiveHeader = do
       docToHtml (run (runReader defaultOptions (execExactPrint Nothing (ppInductiveSignature def))))
 
-goConstructors :: forall r. (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => NonEmpty (InductiveConstructorDef 'Scoped) -> Sem r Html
+goConstructors :: forall r. (Members '[Reader HtmlOptions, Reader NormalizedTable] r) => NonEmpty (ConstructorDef 'Scoped) -> Sem r Html
 goConstructors cc = do
   tbl' <- table . tbody <$> mconcatMapM goConstructor cc
   return $
     Html.div ! Attr.class_ "subs constructors" $
       (p ! Attr.class_ "caption" $ "Constructors")
         <> tbl'
   where
-    goConstructor :: InductiveConstructorDef 'Scoped -> Sem r Html
+    goConstructor :: ConstructorDef 'Scoped -> Sem r Html
     goConstructor c = do
       src' <- srcPart
       doc' <- docPart

src/Juvix/Compiler/Builtins/Bool.hs

@@ -14,16 +14,16 @@ registerBoolDef d = do
     [c1, c2] -> registerTrue c1 >> registerFalse c2
     _ -> error "Bool should have exactly two constructors"
 
-registerTrue :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
-registerTrue d@InductiveConstructorDef {..} = do
+registerTrue :: (Member Builtins r) => ConstructorDef -> Sem r ()
+registerTrue d@ConstructorDef {..} = do
   let ctorTrue = _inductiveConstructorName
       ctorTy = _inductiveConstructorType
   boolTy <- getBuiltinName (getLoc d) BuiltinBool
   unless (ctorTy === boolTy) (error $ "true has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
   registerBuiltin BuiltinBoolTrue ctorTrue
 
-registerFalse :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
-registerFalse d@InductiveConstructorDef {..} = do
+registerFalse :: (Member Builtins r) => ConstructorDef -> Sem r ()
+registerFalse d@ConstructorDef {..} = do
   let ctorFalse = _inductiveConstructorName
       ctorTy = _inductiveConstructorType
   boolTy <- getBuiltinName (getLoc d) BuiltinBool

src/Juvix/Compiler/Builtins/Int.hs

@@ -13,8 +13,8 @@ registerIntDef d = do
     [c1, c2] -> registerIntCtor BuiltinIntOfNat c1 >> registerIntCtor BuiltinIntNegSuc c2
     _ -> error "Int should have exactly two constructors"
 
-registerIntCtor :: (Member Builtins r) => BuiltinConstructor -> InductiveConstructorDef -> Sem r ()
-registerIntCtor ctor d@InductiveConstructorDef {..} = do
+registerIntCtor :: (Member Builtins r) => BuiltinConstructor -> ConstructorDef -> Sem r ()
+registerIntCtor ctor d@ConstructorDef {..} = do
   let ctorName = _inductiveConstructorName
       ty = _inductiveConstructorType
       loc = getLoc d

src/Juvix/Compiler/Builtins/List.hs

@@ -18,17 +18,17 @@ registerListDef d = do
       [v] -> v ^. inductiveParamName
       _ -> error "List should have exactly one type parameter"
 
-registerNil :: Member Builtins r => VarName -> InductiveConstructorDef -> Sem r ()
-registerNil a d@InductiveConstructorDef {..} = do
+registerNil :: Member Builtins r => VarName -> ConstructorDef -> Sem r ()
+registerNil a d@ConstructorDef {..} = do
   let nil = _inductiveConstructorName
       ty = _inductiveConstructorType
   list_ <- getBuiltinName (getLoc d) BuiltinList
   let nilty = list_ @@ a
   unless (ty === nilty) (error $ "nil has the wrong type " <> ppTrace ty <> " | " <> ppTrace nilty)
   registerBuiltin BuiltinListNil nil
 
-registerCons :: Member Builtins r => VarName -> InductiveConstructorDef -> Sem r ()
-registerCons a d@InductiveConstructorDef {..} = do
+registerCons :: Member Builtins r => VarName -> ConstructorDef -> Sem r ()
+registerCons a d@ConstructorDef {..} = do
   let cons_ = _inductiveConstructorName
       ty = _inductiveConstructorType
   list_ <- getBuiltinName (getLoc d) BuiltinList

src/Juvix/Compiler/Builtins/Nat.hs

@@ -15,16 +15,16 @@ registerNatDef d = do
     [c1, c2] -> registerZero c1 >> registerSuc c2
     _ -> error "Nat numbers should have exactly two constructors"
 
-registerZero :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
-registerZero d@InductiveConstructorDef {..} = do
+registerZero :: (Member Builtins r) => ConstructorDef -> Sem r ()
+registerZero d@ConstructorDef {..} = do
   let zero = _inductiveConstructorName
       ty = _inductiveConstructorType
   nat <- getBuiltinName (getLoc d) BuiltinNat
   unless (ty === nat) (error $ "zero has the wrong type " <> ppTrace ty <> " | " <> ppTrace nat)
   registerBuiltin BuiltinNatZero zero
 
-registerSuc :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
-registerSuc d@InductiveConstructorDef {..} = do
+registerSuc :: (Member Builtins r) => ConstructorDef -> Sem r ()
+registerSuc d@ConstructorDef {..} = do
   let suc = _inductiveConstructorName
       ty = _inductiveConstructorType
   nat <- getBuiltinName (getLoc d) BuiltinNat

src/Juvix/Compiler/Concrete/Data/InfoTable.hs

@@ -16,7 +16,7 @@ data FunctionInfo
   deriving stock (Eq, Show)
 
 data ConstructorInfo = ConstructorInfo
-  { _constructorInfoDef :: InductiveConstructorDef 'Scoped,
+  { _constructorInfoDef :: ConstructorDef 'Scoped,
     _constructorInfoTypeName :: S.Symbol
   }
   deriving stock (Eq, Show)

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -10,7 +10,7 @@ import Juvix.Prelude
 
 data InfoTableBuilder m a where
   RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()
-  RegisterConstructor :: S.Symbol -> InductiveConstructorDef 'Scoped -> InfoTableBuilder m ()
+  RegisterConstructor :: S.Symbol -> ConstructorDef 'Scoped -> InfoTableBuilder m ()
   RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
   RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()

src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs

@@ -42,7 +42,7 @@ instance HasNameSignature (FunctionDef 'Parsed) where
     mapM_ addSigArg (a ^. signArgs)
     addAtoms (a ^. signRetType)
 
-instance HasNameSignature (InductiveDef 'Parsed, InductiveConstructorDef 'Parsed) where
+instance HasNameSignature (InductiveDef 'Parsed, ConstructorDef 'Parsed) where
   addArgs (i, c) = do
     mapM_ addConstructorParams (i ^. inductiveParameters)
     addAtoms (c ^. constructorType)

src/Juvix/Compiler/Concrete/Language.hs

@@ -452,7 +452,7 @@ type InductiveConstructorName s = SymbolType s
 
 type InductiveName s = SymbolType s
 
-data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
+data ConstructorDef (s :: Stage) = ConstructorDef
   { _constructorPipe :: Irrelevant (Maybe KeywordRef),
     _constructorColonKw :: Irrelevant KeywordRef,
     _constructorName :: InductiveConstructorName s,
@@ -461,11 +461,11 @@ data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
     _constructorType :: ExpressionType s
   }
 
-deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveConstructorDef s)
+deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (ConstructorDef s)
 
-deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (InductiveConstructorDef s)
+deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (ConstructorDef s)
 
-deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveConstructorDef s)
+deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (ConstructorDef s)
 
 data InductiveParameters (s :: Stage) = InductiveParameters
   { _inductiveParametersNames :: NonEmpty (SymbolType s),
@@ -487,7 +487,7 @@ data InductiveDef (s :: Stage) = InductiveDef
     _inductiveName :: InductiveName s,
     _inductiveParameters :: [InductiveParameters s],
     _inductiveType :: Maybe (ExpressionType s),
-    _inductiveConstructors :: NonEmpty (InductiveConstructorDef s),
+    _inductiveConstructors :: NonEmpty (ConstructorDef s),
     _inductivePositive :: Maybe KeywordRef
   }
 
@@ -1590,7 +1590,7 @@ makeLenses ''FunctionParameters
 makeLenses ''Import
 makeLenses ''OperatorSyntaxDef
 makeLenses ''IteratorSyntaxDef
-makeLenses ''InductiveConstructorDef
+makeLenses ''ConstructorDef
 makeLenses ''Module
 makeLenses ''TypeSignature
 makeLenses ''SigArg

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

@@ -897,9 +897,9 @@ instance SingI s => PrettyPrint (NonEmpty (InductiveParameters s)) where
 instance PrettyPrint a => PrettyPrint (Irrelevant a) where
   ppCode (Irrelevant a) = ppCode a
 
-instance SingI s => PrettyPrint (InductiveConstructorDef s) where
-  ppCode :: forall r. Members '[ExactPrint, Reader Options] r => InductiveConstructorDef s -> Sem r ()
-  ppCode InductiveConstructorDef {..} = do
+instance SingI s => PrettyPrint (ConstructorDef s) where
+  ppCode :: forall r. Members '[ExactPrint, Reader Options] r => ConstructorDef s -> Sem r ()
+  ppCode ConstructorDef {..} = do
     let constructorName' = annDef _constructorName (ppSymbolType _constructorName)
         constructorType' = ppExpressionType _constructorType
         doc' = ppCode <$> _constructorDoc
@@ -944,7 +944,7 @@ instance SingI s => PrettyPrint (InductiveDef s) where
         <> line
         <> indent constrs'
     where
-      ppConstructorBlock :: NonEmpty (InductiveConstructorDef s) -> Sem r ()
+      ppConstructorBlock :: NonEmpty (ConstructorDef s) -> Sem r ()
       ppConstructorBlock cs = vsep (ppCode <$> cs)
 
 instance SingI s => PrettyPrint (Statement s) where

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

@@ -287,7 +287,7 @@ reserveInductiveSymbol d = reserveSymbolSignatureOf S.KNameInductive d (d ^. ind
 reserveConstructorSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
   InductiveDef 'Parsed ->
-  InductiveConstructorDef 'Parsed ->
+  ConstructorDef 'Parsed ->
   Sem r S.Symbol
 reserveConstructorSymbol d c = reserveSymbolSignatureOf S.KNameConstructor (d, c) (c ^. constructorName)
 
@@ -708,7 +708,7 @@ checkInductiveDef InductiveDef {..} = do
         _inductiveKw
       }
   where
-    bindConstructor :: InductiveConstructorDef 'Scoped -> Sem r ()
+    bindConstructor :: ConstructorDef 'Scoped -> Sem r ()
     bindConstructor d =
       topBindings $
         bindReservedSymbol
@@ -718,12 +718,12 @@ checkInductiveDef InductiveDef {..} = do
               )
           )
     -- note that the constructor name is not bound here
-    checkConstructorDef :: S.Symbol -> S.Symbol -> InductiveConstructorDef 'Parsed -> Sem r (InductiveConstructorDef 'Scoped)
-    checkConstructorDef tyName constructorName' InductiveConstructorDef {..} = do
+    checkConstructorDef :: S.Symbol -> S.Symbol -> ConstructorDef 'Parsed -> Sem r (ConstructorDef 'Scoped)
+    checkConstructorDef tyName constructorName' ConstructorDef {..} = do
       constructorType' <- checkParseExpressionAtoms _constructorType
       doc' <- mapM checkJudoc _constructorDoc
       registerConstructor tyName
-        @$> InductiveConstructorDef
+        @$> ConstructorDef
           { _constructorName = constructorName',
             _constructorType = constructorType',
             _constructorDoc = doc',

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

@@ -1028,14 +1028,14 @@ inductiveParams = parens $ do
   _inductiveParametersType <- parseExpressionAtoms
   return InductiveParameters {..}
 
-constructorDef :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (InductiveConstructorDef 'Parsed)
+constructorDef :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => Irrelevant (Maybe KeywordRef) -> ParsecS r (ConstructorDef 'Parsed)
 constructorDef _constructorPipe = do
   _constructorDoc <- optional stashJudoc >> getJudoc
   _constructorPragmas <- optional stashPragmas >> getPragmas
   _constructorName <- symbol P.<?> "<constructor name>"
   _constructorColonKw <- Irrelevant <$> kw kwColon
   _constructorType <- parseExpressionAtoms P.<?> "<constructor type>"
-  return InductiveConstructorDef {..}
+  return ConstructorDef {..}
 
 wildcard :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Wildcard
 wildcard = Wildcard . snd <$> interval (kw kwWildcard)

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -170,7 +170,7 @@ goConstructor ::
   forall r.
   (Members '[InfoTableBuilder, Reader Internal.InfoTable, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable] r) =>
   Symbol ->
-  Internal.InductiveConstructorDef ->
+  Internal.ConstructorDef ->
   Sem r ConstructorInfo
 goConstructor sym ctor = do
   mblt <- mBuiltin

src/Juvix/Compiler/Internal/Extra.hs

@@ -213,12 +213,12 @@ instance HasExpressions InductiveDef where
           _inductivePragmas
         }
 
-instance HasExpressions InductiveConstructorDef where
-  leafExpressions f InductiveConstructorDef {..} = do
+instance HasExpressions ConstructorDef where
+  leafExpressions f ConstructorDef {..} = do
     ty' <- leafExpressions f _inductiveConstructorType
     examples' <- traverse (leafExpressions f) _inductiveConstructorExamples
     pure
-      InductiveConstructorDef
+      ConstructorDef
         { _inductiveConstructorExamples = examples',
           _inductiveConstructorType = ty',
           _inductiveConstructorName,

src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs

@@ -166,7 +166,7 @@ goFunctionDefHelper f = do
 
 -- constructors of an inductive type depend on the inductive type, not the other
 -- way round; an inductive type depends on the types of its constructors
-goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> InductiveConstructorDef -> Sem r ()
+goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> ConstructorDef -> Sem r ()
 goConstructorDef indName c = do
   addEdge (c ^. inductiveConstructorName) indName
   goExpression (Just indName) (c ^. inductiveConstructorType)

src/Juvix/Compiler/Internal/Language.hs

@@ -277,13 +277,13 @@ data InductiveDef = InductiveDef
     _inductiveExamples :: [Example],
     _inductiveType :: Expression,
     _inductiveParameters :: [InductiveParameter],
-    _inductiveConstructors :: [InductiveConstructorDef],
+    _inductiveConstructors :: [ConstructorDef],
     _inductivePositive :: Bool,
     _inductivePragmas :: Pragmas
   }
   deriving stock (Data)
 
-data InductiveConstructorDef = InductiveConstructorDef
+data ConstructorDef = ConstructorDef
   { _inductiveConstructorName :: ConstrName,
     _inductiveConstructorExamples :: [Example],
     _inductiveConstructorType :: Expression,
@@ -336,7 +336,7 @@ makeLenses ''Lambda
 makeLenses ''LambdaClause
 makeLenses ''FunctionParameter
 makeLenses ''InductiveParameter
-makeLenses ''InductiveConstructorDef
+makeLenses ''ConstructorDef
 makeLenses ''ConstructorApp
 
 instance Eq ModuleIndex where
@@ -405,8 +405,8 @@ instance HasAtomicity Pattern where
 instance HasLoc AxiomDef where
   getLoc a = getLoc (a ^. axiomName) <> getLoc (a ^. axiomType)
 
-instance HasLoc InductiveConstructorDef where
-  getLoc InductiveConstructorDef {..} =
+instance HasLoc ConstructorDef where
+  getLoc ConstructorDef {..} =
     getLoc _inductiveConstructorName <> getLoc _inductiveConstructorType
 
 instance HasLoc InductiveParameter where

src/Juvix/Compiler/Internal/Pretty/Base.hs

@@ -178,7 +178,7 @@ instance PrettyCode Hole where
     showNameId <- asks (^. optShowNameIds)
     return (addNameIdTag showNameId (h ^. holeId) kwHole)
 
-instance PrettyCode InductiveConstructorDef where
+instance PrettyCode ConstructorDef where
   ppCode c = do
     constructorName' <- ppCode (c ^. inductiveConstructorName)
     ty' <- ppCode (c ^. inductiveConstructorType)

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -655,14 +655,14 @@ goInductive ty@InductiveDef {..} = do
 
 goConstructorDef ::
   Members [Builtins, NameIdGen, Error ScoperError, Reader Pragmas] r =>
-  InductiveConstructorDef 'Scoped ->
-  Sem r Internal.InductiveConstructorDef
-goConstructorDef InductiveConstructorDef {..} = do
+  ConstructorDef 'Scoped ->
+  Sem r Internal.ConstructorDef
+goConstructorDef ConstructorDef {..} = do
   ty' <- goExpression _constructorType
   examples' <- goExamples _constructorDoc
   pragmas' <- goPragmas _constructorPragmas
   return
-    Internal.InductiveConstructorDef
+    Internal.ConstructorDef
       { _inductiveConstructorType = ty',
         _inductiveConstructorExamples = examples',
         _inductiveConstructorName = goSymbol _constructorName,

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs

@@ -84,13 +84,13 @@ checkInductive d = do
         checkParam :: InductiveParameter -> Sem (State LocalVars ': r) InductiveParameter
         checkParam = return
 
-checkConstructor :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveConstructorDef -> Sem r InductiveConstructorDef
+checkConstructor :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => ConstructorDef -> Sem r ConstructorDef
 checkConstructor c = do
   let _inductiveConstructorName = c ^. inductiveConstructorName
       _inductiveConstructorPragmas = c ^. inductiveConstructorPragmas
   _inductiveConstructorType <- checkType (c ^. inductiveConstructorType)
   _inductiveConstructorExamples <- mapM checkExample (c ^. inductiveConstructorExamples)
-  return InductiveConstructorDef {..}
+  return ConstructorDef {..}
 
 -- | check the arity of some ty : Type
 checkType :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => Expression -> Sem r Expression

src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs

@@ -20,7 +20,7 @@ import Juvix.Prelude hiding (fromEither)
 
 type MCache = Cache ModuleIndex Module
 
-registerConstructor :: Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
+registerConstructor :: Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r => ConstructorDef -> Sem r ()
 registerConstructor ctr = do
   ty <- constructorType (ctr ^. inductiveConstructorName)
   registerNameIdType (ctr ^. inductiveConstructorName . nameId) ty
@@ -120,16 +120,16 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
         { _localTypes = HashMap.fromList [(p ^. inductiveParamName, smallUniverseE (getLoc p)) | p <- _inductiveParameters],
           _localTyMap = mempty
         }
-    goConstructor :: InductiveConstructorDef -> Sem (Inference ': r) InductiveConstructorDef
-    goConstructor InductiveConstructorDef {..} = do
+    goConstructor :: ConstructorDef -> Sem (Inference ': r) ConstructorDef
+    goConstructor ConstructorDef {..} = do
       expectedRetTy <- constructorReturnType _inductiveConstructorName
       cty' <-
         runReader paramLocals $
           checkIsType (getLoc _inductiveConstructorType) _inductiveConstructorType
       examples' <- mapM checkExample _inductiveConstructorExamples
       whenJustM (matchTypes expectedRetTy ret) (const (errRet expectedRetTy))
       let c' =
-            InductiveConstructorDef
+            ConstructorDef
               { _inductiveConstructorType = cty',
                 _inductiveConstructorExamples = examples',
                 _inductiveConstructorName,
@@ -255,14 +255,14 @@ checkConstructorDef ::
       r
   ) =>
   InductiveDef ->
-  InductiveConstructorDef ->
+  ConstructorDef ->
   Sem r ()
 checkConstructorDef ty ctor = checkConstructorReturnType ty ctor
 
 checkConstructorReturnType ::
   (Members '[Reader InfoTable, Error TypeCheckerError] r) =>
   InductiveDef ->
-  InductiveConstructorDef ->
+  ConstructorDef ->
   Sem r ()
 checkConstructorReturnType indType ctor = do
   let ctorName = ctor ^. inductiveConstructorName