diff --git a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
index 730f61779e..8edf0227c6 100644
--- a/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
+++ b/src/Juvix/Compiler/Backend/Html/Translation/FromTyped.hs
@@ -435,7 +435,7 @@ 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 $
@@ -443,7 +443,7 @@ goConstructors cc = do
(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
diff --git a/src/Juvix/Compiler/Builtins/Bool.hs b/src/Juvix/Compiler/Builtins/Bool.hs
index 6e593b2705..9880744c93 100644
--- a/src/Juvix/Compiler/Builtins/Bool.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Builtins/Int.hs b/src/Juvix/Compiler/Builtins/Int.hs
index 4f5309d854..73ab7f34ca 100644
--- a/src/Juvix/Compiler/Builtins/Int.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Builtins/List.hs b/src/Juvix/Compiler/Builtins/List.hs
index 74062d1053..e53f77add0 100644
--- a/src/Juvix/Compiler/Builtins/List.hs
+++ b/src/Juvix/Compiler/Builtins/List.hs
@@ -18,8 +18,8 @@ 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
@@ -27,8 +27,8 @@ registerNil a d@InductiveConstructorDef {..} = do
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
diff --git a/src/Juvix/Compiler/Builtins/Nat.hs b/src/Juvix/Compiler/Builtins/Nat.hs
index dd171b6bbe..0a6991cfdb 100644
--- a/src/Juvix/Compiler/Builtins/Nat.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs b/src/Juvix/Compiler/Concrete/Data/InfoTable.hs
index d6b9bd6a80..e4bcc2cb0a 100644
--- a/src/Juvix/Compiler/Concrete/Data/InfoTable.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
index f3b625e79d..0119a4dcde 100644
--- a/src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs
+++ b/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 ()
diff --git a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs b/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
index 9421cb13c3..c3e3ad89ec 100644
--- a/src/Juvix/Compiler/Concrete/Data/NameSignature/Builder.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Concrete/Language.hs b/src/Juvix/Compiler/Concrete/Language.hs
index 75311ab08d..e0df8ac2ee 100644
--- a/src/Juvix/Compiler/Concrete/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs
index e0f8f63829..dc5d92072f 100644
--- a/src/Juvix/Compiler/Concrete/Print/Base.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs b/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
index 5da2893df5..ef670e9dd6 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs
+++ b/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',
diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
index facbe6deec..616eec616b 100644
--- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs
+++ b/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.> ""
_constructorColonKw <- Irrelevant <$> kw kwColon
_constructorType <- parseExpressionAtoms P.> ""
- return InductiveConstructorDef {..}
+ return ConstructorDef {..}
wildcard :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r Wildcard
wildcard = Wildcard . snd <$> interval (kw kwWildcard)
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index ec4440e708..e04791117e 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs
index edea61c7f3..27a8c62809 100644
--- a/src/Juvix/Compiler/Internal/Extra.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
index 8ff892c3f5..ad2fb4fda1 100644
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Internal/Language.hs b/src/Juvix/Compiler/Internal/Language.hs
index 921ccdcd6d..1c548ddc23 100644
--- a/src/Juvix/Compiler/Internal/Language.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs
index bfdd7b2d0c..74b6b95f9b 100644
--- a/src/Juvix/Compiler/Internal/Pretty/Base.hs
+++ b/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)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 9142dd31aa..021a5ab3eb 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/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,
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
index cfeb020072..a70fa1ed20 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/ArityChecking/Checker.hs
+++ b/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
diff --git a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs b/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
index 5f5ae4404e..01f8096bf0 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Checker.hs
+++ b/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,8 +120,8 @@ 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 $
@@ -129,7 +129,7 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
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