1
1
mirror of https://github.com/anoma/juvix.git synced 2024-12-14 08:27:03 +03:00

[scoper] Add function clauses to scoped InfoTable

This commit is contained in:
Paul Cadman 2022-03-29 10:32:56 +01:00
parent 3354847eb5
commit 9e8a64fd7c
3 changed files with 19 additions and 8 deletions

View File

@ -3,6 +3,7 @@
module MiniJuvix.Syntax.Concrete.Scoped.InfoTable where
import MiniJuvix.Prelude
import MiniJuvix.Syntax.Concrete.Language
import qualified MiniJuvix.Syntax.Concrete.Scoped.Name as S
newtype FunctionInfo = FunctionInfo {
_functionInfoType :: Expression
@ -25,7 +26,8 @@ data InfoTable = InfoTable {
_infoConstructors :: HashMap ConstructorRef ConstructorInfo,
_infoAxioms :: HashMap AxiomRef AxiomInfo,
_infoInductives :: HashMap InductiveRef InductiveInfo,
_infoFunctions :: HashMap FunctionRef FunctionInfo
_infoFunctions :: HashMap FunctionRef FunctionInfo,
_infoFunctionClauses :: HashMap S.Symbol (FunctionClause 'Scoped)
}
emptyInfoTable :: InfoTable

View File

@ -720,13 +720,12 @@ checkFunctionClause clause@FunctionClause {..} = do
clb <- checkParseExpressionAtoms _clauseBody
put s
return (clp, clw, clb)
return
FunctionClause
{ _clauseOwnerFunction = clauseOwnerFunction',
_clausePatterns = clausePatterns',
_clauseBody = clauseBody',
_clauseWhere = clauseWhere'
}
registerFunctionClause' FunctionClause
{ _clauseOwnerFunction = clauseOwnerFunction',
_clausePatterns = clausePatterns',
_clauseBody = clauseBody',
_clauseWhere = clauseWhere'
}
where
fun = _clauseOwnerFunction
checkTypeSigInScope :: Sem r S.Symbol

View File

@ -11,6 +11,7 @@ data InfoTableBuilder m a where
RegisterConstructor :: InductiveConstructorDef 'Scoped -> InfoTableBuilder m ()
RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
RegisterFunction :: TypeSignature 'Scoped -> InfoTableBuilder m ()
RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
makeSem ''InfoTableBuilder
@ -31,6 +32,11 @@ registerAxiom' :: Member InfoTableBuilder r =>
AxiomDef 'Scoped -> Sem r (AxiomDef 'Scoped)
registerAxiom' a = registerAxiom a $> a
registerFunctionClause' :: Member InfoTableBuilder r =>
FunctionClause 'Scoped -> Sem r (FunctionClause 'Scoped)
registerFunctionClause' a = registerFunctionClause a $> a
toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
toState = reinterpret $ \case
RegisterAxiom d ->
@ -61,6 +67,10 @@ toState = reinterpret $ \case
}
in modify (over infoFunctions (HashMap.insert ref info)
)
RegisterFunctionClause c -> let
key = c ^. clauseOwnerFunction
value = c
in modify (over infoFunctionClauses (HashMap.insert key value))
runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
runInfoTableBuilder = runState emptyInfoTable . toState