Skip to content

Commit

Permalink
Refactor of registration of literalIntTo{Nat, Int} functions
Browse files Browse the repository at this point in the history
  • Loading branch information
@paulcadman
paulcadman committed Apr 11, 2023
1 parent 7d5cc5a commit b7be2b3
Show file tree
Hide file tree
Showing 4 changed files with 140 additions and 95 deletions.
84 changes: 84 additions & 0 deletions src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,8 @@ data InfoTableBuilder m a where
RegisterInductive :: Text -> InductiveInfo -> InfoTableBuilder m ()
RegisterIdentNode :: Symbol -> Node -> InfoTableBuilder m ()
RegisterMain :: Symbol -> InfoTableBuilder m ()
RegisterLiteralIntToNat :: Symbol -> InfoTableBuilder m ()
RegisterLiteralIntToInt :: Symbol -> InfoTableBuilder m ()
RemoveSymbol :: Symbol -> InfoTableBuilder m ()
OverIdentArgs :: Symbol -> ([Binder] -> [Binder]) -> InfoTableBuilder m ()
GetIdent :: Text -> InfoTableBuilder m (Maybe IdentKind)
Expand Down Expand Up @@ -107,6 +109,10 @@ runInfoTableBuilder tab =
modify' (over identContext (HashMap.insert sym node))
RegisterMain sym -> do
modify' (set infoMain (Just sym))
RegisterLiteralIntToInt sym -> do
modify' (set infoLiteralIntToInt (Just sym))
RegisterLiteralIntToNat sym -> do
modify' (set infoLiteralIntToNat (Just sym))
RemoveSymbol sym -> do
modify' (over infoMain (maybe Nothing (\sym' -> if sym' == sym then Nothing else Just sym')))
modify' (over infoIdentifiers (HashMap.delete sym))
Expand Down Expand Up @@ -215,3 +221,81 @@ declareNatBuiltins = do
[ (tagZero, "zero", id, Just BuiltinNatZero),
(tagSuc, "suc", \x -> mkPi' x x, Just BuiltinNatSuc)
]

reserveLiteralIntToNatSymbol :: Member InfoTableBuilder r => Sem r ()
reserveLiteralIntToNatSymbol = do
sym <- freshSymbol
registerLiteralIntToNat sym

reserveLiteralIntToIntSymbol :: Member InfoTableBuilder r => Sem r ()
reserveLiteralIntToIntSymbol = do
sym <- freshSymbol
registerLiteralIntToInt sym

-- | Register a function Int -> Nat used to transform literal integers to builtin Nat
setupLiteralIntToNat :: forall r. Member InfoTableBuilder r => (Symbol -> Sem r Node) -> Sem r ()
setupLiteralIntToNat mkNode = do
tab <- getInfoTable
whenJust (tab ^. infoLiteralIntToNat) go
where
go :: Symbol -> Sem r ()
go sym = do
ii <- info sym
registerIdent (ii ^. identifierName) ii
n <- mkNode sym
registerIdentNode sym n
where
info :: Symbol -> Sem r IdentifierInfo
info s = do
tab <- getInfoTable
ty <- targetType
return $
IdentifierInfo
{ _identifierSymbol = s,
_identifierName = freshIdentName tab "intToNat",
_identifierLocation = Nothing,
_identifierArgsNum = 1,
_identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty,
_identifierIsExported = False,
_identifierBuiltin = Nothing
}

targetType :: Sem r Node
targetType = do
tab <- getInfoTable
let natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
return (maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM)

-- | Register a function Int -> Int used to transform literal integers to builtin Int
setupLiteralIntToInt :: forall r. Member InfoTableBuilder r => Sem r Node -> Sem r ()
setupLiteralIntToInt node = do
tab <- getInfoTable
whenJust (tab ^. infoLiteralIntToInt) go
where
go :: Symbol -> Sem r ()
go sym = do
ii <- info sym
registerIdent (ii ^. identifierName) ii
n <- node
registerIdentNode sym n
where
info :: Symbol -> Sem r IdentifierInfo
info s = do
tab <- getInfoTable
ty <- targetType
return $
IdentifierInfo
{ _identifierSymbol = s,
_identifierName = freshIdentName tab "literalIntToInt",
_identifierLocation = Nothing,
_identifierArgsNum = 1,
_identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') ty,
_identifierIsExported = False,
_identifierBuiltin = Nothing
}

targetType :: Sem r Node
targetType = do
tab <- getInfoTable
let intSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinInt
return (maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Int" mempty) s []) intSymM)
17 changes: 6 additions & 11 deletions src/Juvix/Compiler/Core/Translation/FromInternal.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,30 +31,25 @@ mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)

fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
fromInternal i = do
(res, _) <- runInfoTableBuilder tab0 (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
(res, _) <- runInfoTableBuilder emptyInfoTable (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
return $
CoreResult
{ _coreResultTable = setupLiteralIntToInt intToIntSym (setupLiteralIntToNat intToNatSym res),
{ _coreResultTable = res,
_coreResultInternalTypedResult = i
}
where
tab0 :: InfoTable
tab0 = emptyInfoTable {_infoLiteralIntToNat = Just intToNatSym, _infoLiteralIntToInt = Just intToIntSym, _infoNextSymbol = intToIntSym + 1}

intToNatSym :: Symbol
intToNatSym = 0

intToIntSym :: Symbol
intToIntSym = intToNatSym + 1

f :: Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, State InternalTyped.FunctionsTable] r => Sem r ()
f = do
reserveLiteralIntToNatSymbol
reserveLiteralIntToIntSymbol
let resultModules = toList (i ^. InternalTyped.resultModules)
runReader (Internal.buildTable resultModules) (mapM_ goTopModule resultModules)
tab <- getInfoTable
when
(isNothing (lookupBuiltinInductive tab BuiltinBool))
declareBoolBuiltins
setupLiteralIntToNat literalIntToNatNode
setupLiteralIntToInt literalIntToIntNode

fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
fromInternalExpression res exp = do
Expand Down
81 changes: 32 additions & 49 deletions src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Int.hs
View file
Original file line number Diff line number Diff line change
@@ -1,56 +1,39 @@
module Juvix.Compiler.Core.Translation.FromInternal.Builtins.Int where

import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Core.Data
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Language

setupLiteralIntToInt :: Symbol -> InfoTable -> InfoTable
setupLiteralIntToInt sym tab =
tab
{ _infoIdentifiers = HashMap.insert sym ii (tab ^. infoIdentifiers),
_identContext = HashMap.insert sym node (tab ^. identContext),
_infoLiteralIntToInt = Just sym
}
where
ii =
IdentifierInfo
{ _identifierSymbol = sym,
_identifierName = freshIdentName tab "intToNat",
_identifierLocation = Nothing,
_identifierArgsNum = 1,
_identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') targetType,
_identifierIsExported = False,
_identifierBuiltin = Nothing
}
node =
case (tagOfNatM, tagNegSucM, boolSymM, intToNatSymM) of
(Just tagOfNat, Just tagNegSuc, Just boolSym, Just intToNatSym) ->
mkLambda' mkTypeInteger' $
mkIf'
boolSym
(mkBuiltinApp' OpIntLt [mkVar' 0, mkConstant' (ConstInteger 0)])
( mkConstr
(setInfoName "negSuc" mempty)
tagNegSuc
[ mkBuiltinApp'
OpIntSub
[ mkConstant' (ConstInteger 0),
mkBuiltinApp' OpIntAdd [mkVar' 0, mkConstant' (ConstInteger 1)]
]
]
)
( mkConstr
(setInfoName "ofNat" mempty)
tagOfNat
[mkApp' (mkIdent' intToNatSym) (mkVar' 0)]
)
_ -> mkLambda' mkTypeInteger' $ mkVar' 0

targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Int" mempty) s []) natIntM
tagOfNatM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntOfNat
tagNegSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntNegSuc
boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
natIntM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinInt
intToNatSymM = tab ^. infoLiteralIntToNat
-- | Returns the node representing a function Int -> Int that transforms literal
-- integers to builtin Int.
literalIntToIntNode :: Member InfoTableBuilder r => Sem r Node
literalIntToIntNode = do
tab <- getInfoTable
let intToNatSymM = tab ^. infoLiteralIntToNat
tagOfNatM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntOfNat
tagNegSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinIntNegSuc
boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
return $
case (tagOfNatM, tagNegSucM, boolSymM, intToNatSymM) of
(Just tagOfNat, Just tagNegSuc, Just boolSym, Just intToNatSym) ->
mkLambda' mkTypeInteger' $
mkIf'
boolSym
(mkBuiltinApp' OpIntLt [mkVar' 0, mkConstant' (ConstInteger 0)])
( mkConstr
(setInfoName "negSuc" mempty)
tagNegSuc
[ mkBuiltinApp'
OpIntSub
[ mkConstant' (ConstInteger 0),
mkBuiltinApp' OpIntAdd [mkVar' 0, mkConstant' (ConstInteger 1)]
]
]
)
( mkConstr
(setInfoName "ofNat" mempty)
tagOfNat
[mkApp' (mkIdent' intToNatSym) (mkVar' 0)]
)
_ -> mkLambda' mkTypeInteger' $ mkVar' 0
53 changes: 18 additions & 35 deletions src/Juvix/Compiler/Core/Translation/FromInternal/Builtins/Nat.hs
View file
Original file line number Diff line number Diff line change
@@ -1,42 +1,25 @@
module Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat where

import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Core.Data
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Language

setupLiteralIntToNat :: Symbol -> InfoTable -> InfoTable
setupLiteralIntToNat sym tab =
tab
{ _infoIdentifiers = HashMap.insert sym ii (tab ^. infoIdentifiers),
_identContext = HashMap.insert sym node (tab ^. identContext),
_infoLiteralIntToNat = Just sym
}
where
ii =
IdentifierInfo
{ _identifierSymbol = sym,
_identifierName = freshIdentName tab "intToNat",
_identifierLocation = Nothing,
_identifierArgsNum = 1,
_identifierType = mkPi mempty (Binder "x" Nothing mkTypeInteger') targetType,
_identifierIsExported = False,
_identifierBuiltin = Nothing
}
node =
case (tagZeroM, tagSucM, boolSymM) of
(Just tagZero, Just tagSuc, Just boolSym) ->
mkLambda' mkTypeInteger' $
mkIf'
boolSym
(mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
(mkConstr (setInfoName "zero" mempty) tagZero [])
(mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
_ ->
mkLambda' mkTypeInteger' $ mkVar' 0
targetType = maybe mkTypeInteger' (\s -> mkTypeConstr (setInfoName "Nat" mempty) s []) natSymM
tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
natSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinNat
-- | Returns the node representing a function Int -> Nat that is used to transform
-- literal integers to builtin Nat. The symbol representing the literalIntToNat function is passed
-- so that it can be called recusively.
literalIntToNatNode :: Member InfoTableBuilder r => Symbol -> Sem r Node
literalIntToNatNode sym = do
tab <- getInfoTable
let tagZeroM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatZero
tagSucM = (^. constructorTag) <$> lookupBuiltinConstructor tab BuiltinNatSuc
boolSymM = (^. inductiveSymbol) <$> lookupBuiltinInductive tab BuiltinBool
return $ case (tagZeroM, tagSucM, boolSymM) of
(Just tagZero, Just tagSuc, Just boolSym) ->
mkLambda' mkTypeInteger' $
mkIf'
boolSym
(mkBuiltinApp' OpEq [mkVar' 0, mkConstant' (ConstInteger 0)])
(mkConstr (setInfoName "zero" mempty) tagZero [])
(mkConstr (setInfoName "suc" mempty) tagSuc [mkApp' (mkIdent' sym) (mkBuiltinApp' OpIntSub [mkVar' 0, mkConstant' (ConstInteger 1)])])
_ -> mkLambda' mkTypeInteger' $ mkVar' 0

0 comments on commit b7be2b3

Please sign in to comment.