mirror of
https://github.com/anoma/juvix.git
synced 2024-12-04 06:23:13 +03:00
[concrete] rename DataType to Inductive
This commit is contained in:
parent
8c31d7097d
commit
d6b616bdd9
@ -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
|
||||
|
@ -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
|
||||
|
@ -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)
|
||||
|
@ -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
|
||||
|
Loading…
Reference in New Issue
Block a user