mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 10:03:22 +03:00
[scope] Move InfoTable to a new module
This commit is contained in:
parent
b685af034d
commit
1d39124fac
43
src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs
Normal file
43
src/MiniJuvix/Syntax/Concrete/Scoped/InfoTable.hs
Normal file
@ -0,0 +1,43 @@
|
||||
-- |
|
||||
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.InfoTable where
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
|
||||
newtype FunctionInfo = FunctionInfo {
|
||||
_functionInfoType :: Expression
|
||||
}
|
||||
|
||||
newtype ConstructorInfo = ConstructorInfo {
|
||||
_constructorInfoType :: Expression
|
||||
}
|
||||
|
||||
data AxiomInfo = AxiomInfo {
|
||||
_axiomInfoType :: Expression,
|
||||
_axiomInfoBackends :: [BackendItem]
|
||||
}
|
||||
|
||||
newtype InductiveInfo = InductiveInfo {
|
||||
_inductiveInfoDef :: InductiveDef 'Scoped
|
||||
}
|
||||
|
||||
data InfoTable = InfoTable {
|
||||
_infoConstructors :: HashMap ConstructorRef ConstructorInfo,
|
||||
_infoAxioms :: HashMap AxiomRef AxiomInfo,
|
||||
_infoInductives :: HashMap InductiveRef InductiveInfo,
|
||||
_infoFunctions :: HashMap FunctionRef FunctionInfo
|
||||
}
|
||||
|
||||
emptyInfoTable :: InfoTable
|
||||
emptyInfoTable = InfoTable {
|
||||
_infoConstructors = mempty,
|
||||
_infoAxioms = mempty,
|
||||
_infoInductives = mempty,
|
||||
_infoFunctions = mempty
|
||||
}
|
||||
|
||||
makeLenses ''InfoTable
|
||||
makeLenses ''InductiveInfo
|
||||
makeLenses ''ConstructorInfo
|
||||
makeLenses ''AxiomInfo
|
||||
makeLenses ''FunctionInfo
|
@ -1,9 +1,12 @@
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scope where
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.Scope
|
||||
( module MiniJuvix.Syntax.Concrete.Scoped.Scope,
|
||||
module MiniJuvix.Syntax.Concrete.Scoped.InfoTable )
|
||||
where
|
||||
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.InfoTable
|
||||
import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
|
||||
import qualified Data.HashMap.Strict as HashMap
|
||||
|
||||
newtype LocalVariable = LocalVariable
|
||||
{ variableName :: S.Symbol
|
||||
@ -36,41 +39,7 @@ data Scope = Scope
|
||||
deriving stock (Show)
|
||||
|
||||
|
||||
newtype FunctionInfo = FunctionInfo {
|
||||
_functionInfoType :: Expression
|
||||
}
|
||||
|
||||
newtype ConstructorInfo = ConstructorInfo {
|
||||
_constructorInfoType :: Expression
|
||||
}
|
||||
|
||||
data AxiomInfo = AxiomInfo {
|
||||
_axiomInfoType :: Expression,
|
||||
_axiomInfoBackends :: [BackendItem]
|
||||
}
|
||||
|
||||
newtype InductiveInfo = InductiveInfo {
|
||||
_inductiveInfoDef :: InductiveDef 'Scoped
|
||||
}
|
||||
|
||||
data InfoTable = InfoTable {
|
||||
_infoConstructors :: HashMap ConstructorRef ConstructorInfo,
|
||||
_infoAxioms :: HashMap AxiomRef AxiomInfo,
|
||||
_infoInductives :: HashMap InductiveRef InductiveInfo,
|
||||
_infoFunctions :: HashMap FunctionRef FunctionInfo
|
||||
}
|
||||
|
||||
instance Semigroup InfoTable where
|
||||
(<>) = undefined
|
||||
instance Monoid InfoTable where
|
||||
mempty = undefined
|
||||
|
||||
makeLenses ''ExportInfo
|
||||
makeLenses ''InfoTable
|
||||
makeLenses ''InductiveInfo
|
||||
makeLenses ''ConstructorInfo
|
||||
makeLenses ''AxiomInfo
|
||||
makeLenses ''FunctionInfo
|
||||
makeLenses ''SymbolInfo
|
||||
makeLenses ''LocalVars
|
||||
makeLenses ''Scope
|
||||
@ -109,11 +78,3 @@ emptyScope absPath =
|
||||
_scopeTopModules = mempty,
|
||||
_scopeBindGroup = mempty
|
||||
}
|
||||
|
||||
emptyInfoTable :: InfoTable
|
||||
emptyInfoTable = InfoTable {
|
||||
_infoConstructors = mempty,
|
||||
_infoAxioms = mempty,
|
||||
_infoInductives = mempty,
|
||||
_infoFunctions = mempty
|
||||
}
|
||||
|
@ -3,9 +3,8 @@ module MiniJuvix.Syntax.Concrete.Scoped.Scoper.InfoTableBuilder where
|
||||
import qualified Data.HashMap.Strict as HashMap
|
||||
import MiniJuvix.Prelude
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Language
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scope
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Name
|
||||
import MiniJuvix.Syntax.Concrete.Scoped.Scope
|
||||
|
||||
data InfoTableBuilder m a where
|
||||
RegisterAxiom :: AxiomDef 'Scoped -> InfoTableBuilder m ()
|
||||
|
@ -127,7 +127,6 @@ goConstructorDef (InductiveConstructorDef c ty) = A.InductiveConstructorDef c <$
|
||||
|
||||
goExpression :: forall r. Members '[Error Err] r => Expression -> Sem r A.Expression
|
||||
goExpression e = case e of
|
||||
-- TODO: Continue here
|
||||
ExpressionIdentifier nt -> return (goIden nt)
|
||||
ExpressionParensIdentifier nt -> return (goIden nt)
|
||||
ExpressionApplication a -> A.ExpressionApplication <$> goApplication a
|
||||
|
Loading…
Reference in New Issue
Block a user