[concrete] rename DataConstructor to InductiveConstructor

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -184,22 +184,22 @@ deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (
 -- Lift type construction declaration
 -------------------------------------------------------------------------------
 
-type DataConstructorName s = SymbolType s
+type InductiveConstructorName s = SymbolType s
 
 type InductiveName s = SymbolType s
 
-data DataConstructorDef (s :: Stage) = DataConstructorDef
-  { constructorName :: DataConstructorName s,
+data InductiveConstructorDef (s :: Stage) = InductiveConstructorDef
+  { constructorName :: InductiveConstructorName s,
     constructorType :: ExpressionType s
   }
 
-deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (DataConstructorDef s)
+deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveConstructorDef s)
 
-deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (DataConstructorDef s)
+deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (InductiveConstructorDef s)
 
-deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (DataConstructorDef s)
+deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveConstructorDef s)
 
-deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (DataConstructorDef s)
+deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (InductiveConstructorDef s)
 
 data InductiveParameter (s :: Stage) = InductiveParameter
   { inductiveParameterName :: SymbolType s,
@@ -218,7 +218,7 @@ data InductiveDef (s :: Stage) = InductiveDef
   { inductiveName :: InductiveName s,
     inductiveParameters :: [InductiveParameter s],
     inductiveType :: Maybe (ExpressionType s),
-    inductiveConstructors :: [DataConstructorDef s]
+    inductiveConstructors :: [InductiveConstructorDef s]
   }
 
 deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveDef s)

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -320,12 +320,12 @@ inductiveParam = parens $ do
   inductiveParameterType <- expressionAtoms
   return InductiveParameter {..}
 
-constructorDef :: MonadParsec e Text m => m (DataConstructorDef 'Parsed)
+constructorDef :: MonadParsec e Text m => m (InductiveConstructorDef 'Parsed)
 constructorDef = do
   constructorName <- symbol
   kwColon
   constructorType <- expressionAtoms
-  return DataConstructorDef {..}
+  return InductiveConstructorDef {..}
 
 --------------------------------------------------------------------------------
 -- Pattern section

src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs

@@ -212,8 +212,8 @@ ppOperatorSyntaxDef OperatorSyntaxDef {..} = do
             AssocLeft -> kwInfixl
             AssocNone -> kwInfix
 
-ppDataConstructorDef :: Members '[Reader Options] r => DataConstructorDef 'Scoped -> Sem r (Doc Ann)
-ppDataConstructorDef DataConstructorDef {..} = do
+ppInductiveConstructorDef :: Members '[Reader Options] r => InductiveConstructorDef 'Scoped -> Sem r (Doc Ann)
+ppInductiveConstructorDef InductiveConstructorDef {..} = do
   constructorName' <- ppSSymbol constructorName
   constructorType' <- ppExpression constructorType
   return $ constructorName' <+> kwColon <+> constructorType'
@@ -223,7 +223,7 @@ ppInductiveDef InductiveDef {..} = do
   inductiveName' <- ppSSymbol inductiveName
   inductiveParameters' <- hsep <$> mapM ppInductiveParameter inductiveParameters
   inductiveType' <- ppTypeType
-  inductiveConstructors' <- ppBlock ppDataConstructorDef inductiveConstructors
+  inductiveConstructors' <- ppBlock ppInductiveConstructorDef inductiveConstructors
   return $
     kwInductive <+> inductiveName' <+> inductiveParameters' <+?> inductiveType'
       <+> inductiveConstructors'

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -26,7 +26,7 @@ data ModuleScopeInfo = ModuleScopeInfo
   { -- | Absolute path to the module
     _syntaxPath :: S.AbsModulePath,
     -- | constructors introduced by inductive definitions (E.g. zero; suc).
-    _syntaxConstructors :: HashSet (DataConstructorName 'Parsed),
+    _syntaxConstructors :: HashSet (InductiveConstructorName 'Parsed),
     -- | data types  introduced by inductive definitions (E.g. ℕ).
     _syntaxInductives :: HashSet (InductiveName 'Parsed),
     -- | function names in scope. Function names are introduced with function clauses.
@@ -283,10 +283,10 @@ moduleScopeInfo absPath sModule = ModuleScopeInfo {..}
         getFun s = case s of
           -- StatementInductive InductiveDef {..} → HashSet.fromList (map constructorName inductiveConstructors)
           _ -> undefined
-    _syntaxConstructors :: HashSet (DataConstructorName 'Parsed)
+    _syntaxConstructors :: HashSet (InductiveConstructorName 'Parsed)
     _syntaxConstructors = mconcat (map getConstrs stmts)
       where
-        getConstrs :: Statement 'Scoped -> HashSet (DataConstructorName 'Parsed)
+        getConstrs :: Statement 'Scoped -> HashSet (InductiveConstructorName 'Parsed)
         getConstrs s = case s of
           StatementInductive InductiveDef {..} ->
             HashSet.fromList
@@ -370,13 +370,13 @@ symbolEntry S.Name' {..} =
 
 checkConstructorDef ::
   Members '[Error ScopeError, Reader LocalVars, State Scope, State ScopeState] r =>
-  DataConstructorDef 'Parsed ->
-  Sem r (DataConstructorDef 'Scoped)
-checkConstructorDef DataConstructorDef {..} = do
+  InductiveConstructorDef 'Parsed ->
+  Sem r (InductiveConstructorDef 'Scoped)
+checkConstructorDef InductiveConstructorDef {..} = do
   constructorType' <- checkParseExpressionAtoms constructorType
   constructorName' <- bindConstructorSymbol constructorName
   return
-    DataConstructorDef
+    InductiveConstructorDef
       { constructorName = constructorName',
         constructorType = constructorType'
       }