Skip to content

Commit

Permalink
wip
Browse files Browse the repository at this point in the history
  • Loading branch information
lukaszcz committed Nov 7, 2023
1 parent 47ae86b commit f60a0c4
Show file tree
Hide file tree
Showing 13 changed files with 195 additions and 84 deletions.
8 changes: 7 additions & 1 deletion src/Juvix/Compiler/Internal/Data/CoercionInfo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import Data.List qualified as List
import Juvix.Compiler.Internal.Data.InstanceInfo
import Juvix.Compiler.Internal.Extra.Base
import Juvix.Compiler.Internal.Language
import Juvix.Extra.Serialize
import Juvix.Prelude

data CoercionInfo = CoercionInfo
Expand All @@ -15,15 +16,20 @@ data CoercionInfo = CoercionInfo
_coercionInfoResult :: Expression,
_coercionInfoArgs :: [FunctionParameter]
}
deriving stock (Eq)
deriving stock (Eq, Generic)

instance Hashable CoercionInfo where
hashWithSalt salt CoercionInfo {..} = hashWithSalt salt _coercionInfoResult

instance Serialize CoercionInfo

-- | Maps trait names to available coercions
newtype CoercionTable = CoercionTable
{ _coercionTableMap :: HashMap InductiveName [CoercionInfo]
}
deriving stock (Eq, Generic)

instance Serialize CoercionTable

makeLenses ''CoercionInfo
makeLenses ''CoercionTable
Expand Down
90 changes: 53 additions & 37 deletions src/Juvix/Compiler/Internal/Data/InfoTable.hs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
module Juvix.Compiler.Internal.Data.InfoTable
( module Juvix.Compiler.Internal.Data.InfoTable.Base,
( module Juvix.Compiler.Store.Internal.Language,
buildTable,
extendWithReplExpression,
lookupConstructor,
Expand All @@ -12,41 +12,55 @@ module Juvix.Compiler.Internal.Data.InfoTable
lookupConstructorType,
getAxiomBuiltinInfo,
getFunctionBuiltinInfo,
buildTableShallow,
mkConstructorEntries,
)
where

import Data.Generics.Uniplate.Data
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Data.CoercionInfo
import Juvix.Compiler.Internal.Data.InfoTable.Base
import Juvix.Compiler.Internal.Data.InstanceInfo
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty (ppTrace)
import Juvix.Compiler.Store.Internal.Language
import Juvix.Prelude

type MCache = Cache ModuleIndex InfoTable
buildTable :: (Foldable f) => StoredModuleTable -> f Module -> InfoTable
buildTable mtab = mconcatMap (computeTable mtab)

buildTable :: (Foldable f) => f Module -> InfoTable
buildTable = run . evalCache (computeTable True) mempty . getMany
functionInfoFromFunctionDef :: FunctionDef -> FunctionInfo
functionInfoFromFunctionDef FunctionDef {..} =
FunctionInfo
{ _functionInfoName = _funDefName,
_functionInfoType = _funDefType,
_functionInfoArgsInfo = _funDefArgsInfo,
_functionInfoBuiltin = _funDefBuiltin,
_functionInfoCoercion = _funDefCoercion,
_functionInfoInstance = _funDefInstance,
_functionInfoTerminating = _funDefTerminating,
_functionInfoPragmas = _funDefPragmas
}

buildTable' :: (Foldable f) => Bool -> f Module -> InfoTable
buildTable' recurIntoImports = run . evalCache (computeTable recurIntoImports) mempty . getMany

buildTableShallow :: Module -> InfoTable
buildTableShallow = buildTable' False . pure @[]

getMany :: (Members '[MCache] r, Foldable f) => f Module -> Sem r InfoTable
getMany = mconcatMap (cacheGet . ModuleIndex)
inductiveInfoFromInductiveDef :: InductiveDef -> InductiveInfo
inductiveInfoFromInductiveDef InductiveDef {..} =
InductiveInfo
{ _inductiveInfoName = _inductiveName,
_inductiveInfoType = _inductiveType,
_inductiveInfoBuiltin = _inductiveBuiltin,
_inductiveInfoParameters = _inductiveParameters,
_inductiveInfoConstructors = map (^. inductiveConstructorName) _inductiveConstructors,
_inductiveInfoPositive = _inductivePositive,
_inductiveInfoTrait = _inductiveTrait,
_inductiveInfoPragmas = _inductivePragmas
}

extendWithReplExpression :: Expression -> InfoTable -> InfoTable
extendWithReplExpression e =
over
infoFunctions
( HashMap.union
( HashMap.fromList
[ (f ^. funDefName, FunctionInfo f)
[ (f ^. funDefName, functionInfoFromFunctionDef f)
| f <- letFunctionDefs e
]
)
Expand All @@ -64,18 +78,20 @@ letFunctionDefs e =
LetFunDef f -> pure f
LetMutualBlock (MutualBlockLet fs) -> fs

computeTable :: forall r. (Members '[MCache] r) => Bool -> ModuleIndex -> Sem r InfoTable
computeTable recurIntoImports (ModuleIndex m) = compute
computeTable :: StoredModuleTable -> Module -> InfoTable
computeTable mtab m = compute
where
compute :: Sem r InfoTable
compute = do
infoInc <- mconcatMapM (cacheGet . (^. importModule)) imports
return (InfoTable {..} <> infoInc)
compute :: InfoTable
compute =
InfoTable {..} <> mconcatMap goImport imports
where
goImport :: Import -> InfoTable
goImport Import {..} =
let sm = lookupStoredModule mtab _importModuleName
in sm ^. storedModuleInfoTable <> mconcatMap goImport (sm ^. storedModuleImports)

imports :: [Import]
imports
| recurIntoImports = m ^. moduleBody . moduleImports
| otherwise = []
imports = m ^. moduleBody . moduleImports

mutuals :: [MutualStatement]
mutuals =
Expand All @@ -93,7 +109,7 @@ computeTable recurIntoImports (ModuleIndex m) = compute
_infoInductives :: HashMap Name InductiveInfo
_infoInductives =
HashMap.fromList
[ (d ^. inductiveName, InductiveInfo d)
[ (d ^. inductiveName, inductiveInfoFromInductiveDef d)
| d <- inductives
]

Expand All @@ -108,10 +124,10 @@ computeTable recurIntoImports (ModuleIndex m) = compute
_infoFunctions :: HashMap Name FunctionInfo
_infoFunctions =
HashMap.fromList $
[ (f ^. funDefName, FunctionInfo f)
[ (f ^. funDefName, functionInfoFromFunctionDef f)
| StatementFunction f <- mutuals
]
<> [ (f ^. funDefName, FunctionInfo f)
<> [ (f ^. funDefName, functionInfoFromFunctionDef f)
| s <- ss,
f <- letFunctionDefs s
]
Expand All @@ -127,12 +143,12 @@ computeTable recurIntoImports (ModuleIndex m) = compute
_infoInstances = foldr (flip updateInstanceTable) mempty $ mapMaybe mkInstance (HashMap.elems _infoFunctions)
where
mkInstance :: FunctionInfo -> Maybe InstanceInfo
mkInstance (FunctionInfo FunctionDef {..})
| _funDefInstance =
mkInstance (FunctionInfo {..})
| _functionInfoInstance =
instanceFromTypedExpression
( TypedExpression
{ _typedType = _funDefType,
_typedExpression = ExpressionIden (IdenFunction _funDefName)
{ _typedType = _functionInfoType,
_typedExpression = ExpressionIden (IdenFunction _functionInfoName)
}
)
| otherwise =
Expand All @@ -142,12 +158,12 @@ computeTable recurIntoImports (ModuleIndex m) = compute
_infoCoercions = foldr (flip updateCoercionTable) mempty $ mapMaybe mkCoercion (HashMap.elems _infoFunctions)
where
mkCoercion :: FunctionInfo -> Maybe CoercionInfo
mkCoercion (FunctionInfo FunctionDef {..})
| _funDefCoercion =
mkCoercion (FunctionInfo {..})
| _functionInfoCoercion =
coercionFromTypedExpression
( TypedExpression
{ _typedType = _funDefType,
_typedExpression = ExpressionIden (IdenFunction _funDefName)
{ _typedType = _functionInfoType,
_typedExpression = ExpressionIden (IdenFunction _functionInfoName)
}
)
| otherwise =
Expand Down Expand Up @@ -214,7 +230,7 @@ lookupAxiom f = HashMap.lookupDefault impossible f <$> asks (^. infoAxioms)
lookupInductiveType :: (Member (Reader InfoTable) r) => Name -> Sem r Expression
lookupInductiveType v = do
info <- lookupInductive v
let ps = info ^. inductiveInfoDef . inductiveParameters
let ps = info ^. inductiveInfoParameters
return $
foldr
(\_ k -> uni --> k)
Expand All @@ -240,7 +256,7 @@ getFunctionBuiltinInfo :: (Member (Reader InfoTable) r) => Name -> Sem r (Maybe
getFunctionBuiltinInfo n = do
maybeFunInfo <- HashMap.lookup n <$> asks (^. infoFunctions)
return $ case maybeFunInfo of
Just funInfo -> funInfo ^. functionInfoDef . funDefBuiltin
Just funInfo -> funInfo ^. functionInfoBuiltin
Nothing -> Nothing

mkConstructorEntries :: InductiveDef -> [(ConstructorName, ConstructorInfo)]
Expand Down
20 changes: 16 additions & 4 deletions src/Juvix/Compiler/Internal/Data/InstanceInfo.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Internal.Extra.Base
import Juvix.Compiler.Internal.Language
import Juvix.Extra.Serialize
import Juvix.Prelude

data InstanceParam
Expand All @@ -12,39 +13,50 @@ data InstanceParam
| InstanceParamFun InstanceFun
| InstanceParamHole Hole
| InstanceParamMeta VarName
deriving stock (Eq)
deriving stock (Eq, Generic)

instance Serialize InstanceParam

data InstanceApp = InstanceApp
{ _instanceAppHead :: Name,
_instanceAppArgs :: [InstanceParam],
-- | The original expression from which this InstanceApp was created
_instanceAppExpression :: Expression
}
deriving stock (Eq)
deriving stock (Eq, Generic)

instance Serialize InstanceApp

data InstanceFun = InstanceFun
{ _instanceFunLeft :: InstanceParam,
_instanceFunRight :: InstanceParam,
-- | The original expression from which this InstanceFun was created
_instanceFunExpression :: Expression
}
deriving stock (Eq)
deriving stock (Eq, Generic)

instance Serialize InstanceFun

data InstanceInfo = InstanceInfo
{ _instanceInfoInductive :: InductiveName,
_instanceInfoParams :: [InstanceParam],
_instanceInfoResult :: Expression,
_instanceInfoArgs :: [FunctionParameter]
}
deriving stock (Eq)
deriving stock (Eq, Generic)

instance Hashable InstanceInfo where
hashWithSalt salt InstanceInfo {..} = hashWithSalt salt _instanceInfoResult

instance Serialize InstanceInfo

-- | Maps trait names to available instances
newtype InstanceTable = InstanceTable
{ _instanceTableMap :: HashMap InductiveName [InstanceInfo]
}
deriving stock (Eq, Generic)

instance Serialize InstanceTable

makeLenses ''InstanceApp
makeLenses ''InstanceFun
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Internal/Extra.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,11 +8,11 @@ where

import Data.HashMap.Strict qualified as HashMap
import Data.Stream qualified as Stream
import Juvix.Compiler.Internal.Data.InfoTable.Base
import Juvix.Compiler.Internal.Extra.Base
import Juvix.Compiler.Internal.Extra.Clonable
import Juvix.Compiler.Internal.Extra.DependencyBuilder
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Store.Internal.Data.InfoTable
import Juvix.Prelude

constructorArgTypes :: ConstructorInfo -> ([VarName], [Expression])
Expand Down
2 changes: 1 addition & 1 deletion src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ goModuleNoVisited (ModuleIndex m) = do
mapM_ goImport (b ^. moduleImports)

goImport :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Visit ModuleIndex] r) => Import -> Sem r ()
goImport (Import m) = visit m
goImport (Import m) = undefined

goPreModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Visit ModuleIndex] r) => PreModule -> Sem r ()
goPreModule m = do
Expand Down
10 changes: 8 additions & 2 deletions src/Juvix/Compiler/Internal/Language.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,10 +43,12 @@ data Module' stmt = Module
deriving stock (Data, Generic)

newtype Import = Import
{ _importModule :: ModuleIndex
{ _importModuleName :: Name
}
deriving stock (Data, Generic)

instance Serialize Import

data ModuleBody' stmt = ModuleBody
{ _moduleImports :: [Import],
_moduleStatements :: [stmt]
Expand Down Expand Up @@ -81,6 +83,8 @@ data AxiomDef = AxiomDef
}
deriving stock (Data, Generic)

instance Serialize AxiomDef

data FunctionDef = FunctionDef
{ _funDefName :: FunctionName,
_funDefType :: Expression,
Expand Down Expand Up @@ -317,7 +321,9 @@ instance Serialize Pattern
newtype InductiveParameter = InductiveParameter
{ _inductiveParamName :: VarName
}
deriving stock (Eq, Data)
deriving stock (Eq, Data, Generic)

instance Serialize InductiveParameter

data InductiveDef = InductiveDef
{ _inductiveName :: InductiveName,
Expand Down
4 changes: 2 additions & 2 deletions src/Juvix/Compiler/Internal/Pretty/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,12 @@ module Juvix.Compiler.Internal.Pretty.Base
where

import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Data.InfoTable.Base
import Juvix.Compiler.Internal.Data.InstanceInfo (instanceInfoResult, instanceTableMap)
import Juvix.Compiler.Internal.Data.NameDependencyInfo
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty.Options
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types (Arity)
import Juvix.Compiler.Store.Internal.Data.InfoTable
import Juvix.Data.CodeAnn
import Juvix.Prelude

Expand Down Expand Up @@ -274,7 +274,7 @@ instance PrettyCode PreLetStatement where

instance PrettyCode Import where
ppCode i = do
name' <- ppCode (i ^. importModule . moduleIxModule . moduleName)
name' <- ppCode (i ^. importModuleName)
return $ kwImport <+> name'

instance PrettyCode BuiltinAxiom where
Expand Down
8 changes: 5 additions & 3 deletions src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
Original file line number Diff line number Diff line change
Expand Up @@ -327,14 +327,16 @@ goImport ::
(Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
Import 'Scoped ->
Sem r Internal.Import
goImport Import {..} = do
let m = _importModule ^. moduleRefModule
goImport Import {..} = undefined

{- let m = _importModule ^. moduleRefModule
m' <- goTopModule m
return
( Internal.Import
{ _importModule = Internal.ModuleIndex m'
{ _importModuleName = undefined
}
)
-}

-- | Ignores functions
goAxiomInductive ::
Expand Down
Loading

0 comments on commit f60a0c4

Please sign in to comment.