diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs index d91f0fd21..c03ab24a4 100644 --- a/src/MiniJuvix/Syntax/Concrete/Language.hs +++ b/src/MiniJuvix/Syntax/Concrete/Language.hs @@ -35,11 +35,11 @@ type family NameType (s :: Stage) :: (res :: GHC.Type) | res -> s where NameType 'Scoped = S.Name type family ExpressionType (s :: Stage) :: GHC.Type where - ExpressionType 'Parsed = (ExpressionAtoms 'Parsed) + ExpressionType 'Parsed = ExpressionAtoms 'Parsed ExpressionType 'Scoped = Expression type family PatternType (s :: Stage) :: GHC.Type where - PatternType 'Parsed = (PatternAtom 'Parsed) + PatternType 'Parsed = PatternAtom 'Parsed PatternType 'Scoped = Pattern type family ImportType (s :: Stage) :: GHC.Type where @@ -62,7 +62,7 @@ data Statement (s :: Stage) = StatementOperator OperatorSyntaxDef | StatementTypeSignature (TypeSignature s) | StatementImport (Import s) - | StatementDataType (DataTypeDef s) + | StatementInductive (InductiveDef s) | StatementModule (Module s 'ModuleLocal) | StatementOpenModule OpenModule | StatementFunctionClause (FunctionClause s) @@ -186,7 +186,7 @@ deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift ( type DataConstructorName s = SymbolType s -type DataTypeName s = SymbolType s +type InductiveName s = SymbolType s data DataConstructorDef (s :: Stage) = DataConstructorDef { constructorName :: DataConstructorName s, @@ -201,33 +201,33 @@ deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (Dat deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (DataConstructorDef s) -data DataTypeParameter (s :: Stage) = DataTypeParameter - { dataTypeParameterName :: SymbolType s, - dataTypeParameterType :: ExpressionType s +data InductiveParameter (s :: Stage) = InductiveParameter + { inductiveParameterName :: SymbolType s, + inductiveParameterType :: ExpressionType s } -deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (DataTypeParameter s) +deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveParameter s) -deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (DataTypeParameter s) +deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (InductiveParameter s) -deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (DataTypeParameter s) +deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveParameter s) -deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (DataTypeParameter s) +deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (InductiveParameter s) -data DataTypeDef (s :: Stage) = DataTypeDef - { dataTypeName :: DataTypeName s, - dataTypeParameters :: [DataTypeParameter s], - dataTypeType :: Maybe (ExpressionType s), - dataTypeConstructors :: [DataConstructorDef s] +data InductiveDef (s :: Stage) = InductiveDef + { inductiveName :: InductiveName s, + inductiveParameters :: [InductiveParameter s], + inductiveType :: Maybe (ExpressionType s), + inductiveConstructors :: [DataConstructorDef s] } -deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (DataTypeDef s) +deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (InductiveDef s) -deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (DataTypeDef s) +deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (InductiveDef s) -deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (DataTypeDef s) +deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (InductiveDef s) -deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (DataTypeDef s) +deriving stock instance (Lift (ExpressionType s), Lift (SymbolType s)) => Lift (InductiveDef s) -------------------------------------------------------------------------------- -- Pattern diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs index 6271a421e..ec6db3dd9 100644 --- a/src/MiniJuvix/Syntax/Concrete/Parser.hs +++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs @@ -82,7 +82,7 @@ statement = <|> (StatementOpenModule <$> openModule) <|> (StatementEval <$> eval) <|> (StatementImport <$> import_) - <|> (StatementDataType <$> dataTypeDef) + <|> (StatementInductive <$> inductiveDef) <|> (StatementPrint <$> printS) <|> (StatementModule <$> moduleDef) <|> (StatementAxiom <$> axiomDef) @@ -304,21 +304,21 @@ lambda = do -- Data type construction declaration ------------------------------------------------------------------------------- -dataTypeDef :: MonadParsec e Text m => m (DataTypeDef 'Parsed) -dataTypeDef = do +inductiveDef :: MonadParsec e Text m => m (InductiveDef 'Parsed) +inductiveDef = do kwInductive - dataTypeName <- symbol - dataTypeParameters <- P.many dataTypeParam - dataTypeType <- optional (kwColon >> expressionAtoms) - dataTypeConstructors <- braces $ P.sepEndBy constructorDef kwSemicolon - return DataTypeDef {..} + inductiveName <- symbol + inductiveParameters <- P.many inductiveParam + inductiveType <- optional (kwColon >> expressionAtoms) + inductiveConstructors <- braces $ P.sepEndBy constructorDef kwSemicolon + return InductiveDef {..} -dataTypeParam :: MonadParsec e Text m => m (DataTypeParameter 'Parsed) -dataTypeParam = parens $ do - dataTypeParameterName <- symbol +inductiveParam :: MonadParsec e Text m => m (InductiveParameter 'Parsed) +inductiveParam = parens $ do + inductiveParameterName <- symbol kwColon - dataTypeParameterType <- expressionAtoms - return DataTypeParameter {..} + inductiveParameterType <- expressionAtoms + return InductiveParameter {..} constructorDef :: MonadParsec e Text m => m (DataConstructorDef 'Parsed) constructorDef = do diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs index 751d8599a..c8796dc0b 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs @@ -168,7 +168,7 @@ ppStatement s = case s of StatementOperator op -> ppOperatorSyntaxDef op StatementTypeSignature sig -> ppTypeSignature sig StatementImport i -> ppImport i - StatementDataType d -> ppDataTypeDef d + StatementInductive d -> ppInductiveDef d StatementModule m -> ppModule m StatementOpenModule o -> ppOpen o StatementFunctionClause c -> ppFunctionClause c @@ -218,25 +218,25 @@ ppDataConstructorDef DataConstructorDef {..} = do constructorType' <- ppExpression constructorType return $ constructorName' <+> kwColon <+> constructorType' -ppDataTypeDef :: forall r. Members '[Reader Options] r => DataTypeDef 'Scoped -> Sem r (Doc Ann) -ppDataTypeDef DataTypeDef {..} = do - dataTypeName' <- ppSSymbol dataTypeName - dataTypeParameters' <- hsep <$> mapM ppDataTypeParameter dataTypeParameters - dataTypeType' <- ppTypeType - dataTypeConstructors' <- ppBlock ppDataConstructorDef dataTypeConstructors +ppInductiveDef :: forall r. Members '[Reader Options] r => InductiveDef 'Scoped -> Sem r (Doc Ann) +ppInductiveDef InductiveDef {..} = do + inductiveName' <- ppSSymbol inductiveName + inductiveParameters' <- hsep <$> mapM ppInductiveParameter inductiveParameters + inductiveType' <- ppTypeType + inductiveConstructors' <- ppBlock ppDataConstructorDef inductiveConstructors return $ - kwInductive <+> dataTypeName' <+> dataTypeParameters' <+?> dataTypeType' - <+> dataTypeConstructors' + kwInductive <+> inductiveName' <+> inductiveParameters' <+?> inductiveType' + <+> inductiveConstructors' where ppTypeType :: Sem r (Maybe (Doc Ann)) - ppTypeType = case dataTypeType of + ppTypeType = case inductiveType of Nothing -> return Nothing Just e -> Just . (kwColon <+>) <$> ppExpression e - ppDataTypeParameter :: DataTypeParameter 'Scoped -> Sem r (Doc Ann) - ppDataTypeParameter DataTypeParameter {..} = do - dataTypeParameterName' <- ppSSymbol dataTypeParameterName - dataTypeParameterType' <- ppExpression dataTypeParameterType - return $ parens (dataTypeParameterName' <+> kwColon <+> dataTypeParameterType') + ppInductiveParameter :: InductiveParameter 'Scoped -> Sem r (Doc Ann) + ppInductiveParameter InductiveParameter {..} = do + inductiveParameterName' <- ppSSymbol inductiveParameterName + inductiveParameterType' <- ppExpression inductiveParameterType + return $ parens (inductiveParameterName' <+> kwColon <+> inductiveParameterType') dotted :: [Doc Ann] -> Doc Ann dotted = concatWith (surround kwDot) diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs index bc7218e29..815892fd3 100644 --- a/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs +++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs @@ -28,7 +28,7 @@ data ModuleScopeInfo = ModuleScopeInfo -- | constructors introduced by inductive definitions (E.g. zero; suc). _syntaxConstructors :: HashSet (DataConstructorName 'Parsed), -- | data types introduced by inductive definitions (E.g. ℕ). - _syntaxDataTypes :: HashSet (DataTypeName 'Parsed), + _syntaxInductives :: HashSet (InductiveName 'Parsed), -- | function names in scope. Function names are introduced with function clauses. _syntaxFunctions :: HashSet (FunctionName 'Parsed), -- | locally defined modules. Imported modules are not included. @@ -281,23 +281,23 @@ moduleScopeInfo absPath sModule = ModuleScopeInfo {..} where getFun :: Statement 'Scoped -> Maybe (FunctionName 'Parsed) getFun s = case s of - -- StatementDataType DataTypeDef {..} → HashSet.fromList (map constructorName dataTypeConstructors) + -- StatementInductive InductiveDef {..} → HashSet.fromList (map constructorName inductiveConstructors) _ -> undefined _syntaxConstructors :: HashSet (DataConstructorName 'Parsed) _syntaxConstructors = mconcat (map getConstrs stmts) where getConstrs :: Statement 'Scoped -> HashSet (DataConstructorName 'Parsed) getConstrs s = case s of - StatementDataType DataTypeDef {..} -> + StatementInductive InductiveDef {..} -> HashSet.fromList - (map (S._nameConcrete . constructorName) dataTypeConstructors) + (map (S._nameConcrete . constructorName) inductiveConstructors) _ -> mempty - _syntaxDataTypes :: HashSet (DataTypeName 'Parsed) - _syntaxDataTypes = HashSet.fromList (mapMaybe getDT stmts) + _syntaxInductives :: HashSet (InductiveName 'Parsed) + _syntaxInductives = HashSet.fromList (mapMaybe getDT stmts) where - getDT :: Statement 'Scoped -> Maybe (DataTypeName 'Parsed) + getDT :: Statement 'Scoped -> Maybe (InductiveName 'Parsed) getDT s = case s of - StatementDataType DataTypeDef {..} -> Just (S._nameConcrete dataTypeName) + StatementInductive InductiveDef {..} -> Just (S._nameConcrete inductiveName) _ -> Nothing _syntaxOperators :: HashMap Symbol Fixity _syntaxOperators = HashMap.fromList (mapMaybe getDef stmts) @@ -381,45 +381,45 @@ checkConstructorDef DataConstructorDef {..} = do constructorType = constructorType' } -checkDataTypeDef :: +checkInductiveDef :: Members '[Error ScopeError, State Scope, State ScopeState] r => - DataTypeDef 'Parsed -> - Sem r (DataTypeDef 'Scoped) -checkDataTypeDef DataTypeDef {..} = do - localScope $ checkDataTypeRec dataTypeParameters + InductiveDef 'Parsed -> + Sem r (InductiveDef 'Scoped) +checkInductiveDef InductiveDef {..} = do + localScope $ checkInductiveRec inductiveParameters where - checkDataTypeRec :: + checkInductiveRec :: forall r. Members '[Error ScopeError, State Scope, State ScopeState, Reader LocalVars] r => - [DataTypeParameter 'Parsed] -> - Sem r (DataTypeDef 'Scoped) - checkDataTypeRec dtp = go dtp [] + [InductiveParameter 'Parsed] -> + Sem r (InductiveDef 'Scoped) + checkInductiveRec dtp = go dtp [] where - go :: [DataTypeParameter 'Parsed] -> [DataTypeParameter 'Scoped] -> Sem r (DataTypeDef 'Scoped) - go params dataTypeParameters' = + go :: [InductiveParameter 'Parsed] -> [InductiveParameter 'Scoped] -> Sem r (InductiveDef 'Scoped) + go params inductiveParameters' = case params of -- More params to check - (DataTypeParameter {..} : ps) -> do - dataTypeParameterType' <- checkParseExpressionAtoms dataTypeParameterType - dataTypeParameterName' <- freshVariable dataTypeParameterName + (InductiveParameter {..} : ps) -> do + inductiveParameterType' <- checkParseExpressionAtoms inductiveParameterType + inductiveParameterName' <- freshVariable inductiveParameterName let param' = - DataTypeParameter - { dataTypeParameterType = dataTypeParameterType', - dataTypeParameterName = dataTypeParameterName' + InductiveParameter + { inductiveParameterType = inductiveParameterType', + inductiveParameterName = inductiveParameterName' } - withBindLocalVariable (LocalVariable dataTypeParameterName') $ - go ps (dataTypeParameters' ++ [param']) + withBindLocalVariable (LocalVariable inductiveParameterName') $ + go ps (inductiveParameters' ++ [param']) -- All params have been checked [] -> do - dataTypeType' <- sequence (checkParseExpressionAtoms <$> dataTypeType) - dataTypeName' <- bindInductiveSymbol dataTypeName - dataTypeConstructors' <- mapM checkConstructorDef dataTypeConstructors + inductiveType' <- sequence (checkParseExpressionAtoms <$> inductiveType) + inductiveName' <- bindInductiveSymbol inductiveName + inductiveConstructors' <- mapM checkConstructorDef inductiveConstructors return - DataTypeDef - { dataTypeName = dataTypeName', - dataTypeParameters = dataTypeParameters', - dataTypeType = dataTypeType', - dataTypeConstructors = dataTypeConstructors' + InductiveDef + { inductiveName = inductiveName', + inductiveParameters = inductiveParameters', + inductiveType = inductiveType', + inductiveConstructors = inductiveConstructors' } checkTopModule :: @@ -875,7 +875,7 @@ checkStatement s = case s of StatementOperator opDef -> StatementOperator opDef <$ checkOperatorSyntaxDef opDef StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig StatementImport imp -> StatementImport <$> checkImport imp - StatementDataType dt -> StatementDataType <$> checkDataTypeDef dt + StatementInductive dt -> StatementInductive <$> checkInductiveDef dt StatementModule dt -> StatementModule <$> checkLocalModule dt StatementOpenModule open -> StatementOpenModule open <$ checkOpenModule open StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause