1
1
mirror of https://github.com/anoma/juvix.git synced 2024-10-26 17:52:17 +03:00

Remove abstract (#2219)

- Closes #2002 
- Closes #1690 
- Closes #2224
- Closes #2237
This commit is contained in:
Jan Mas Rovira 2023-06-30 15:01:46 +02:00 committed by GitHub
parent 38028d2dff
commit d69d8c6eca
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
76 changed files with 2318 additions and 2916 deletions

View File

@ -3,11 +3,13 @@ module Commands.Dev.Internal where
import Commands.Base
import Commands.Dev.Internal.Arity qualified as Arity
import Commands.Dev.Internal.Options
import Commands.Dev.Internal.Pretty qualified as InternalPretty
import Commands.Dev.Internal.Typecheck qualified as InternalTypecheck
import Commands.Dev.Internal.Pretty qualified as Pretty
import Commands.Dev.Internal.Reachability qualified as Reachability
import Commands.Dev.Internal.Typecheck qualified as Typecheck
runCommand :: (Members '[Embed IO, App] r) => InternalCommand -> Sem r ()
runCommand :: Members '[Embed IO, App] r => InternalCommand -> Sem r ()
runCommand = \case
Pretty opts -> InternalPretty.runCommand opts
Pretty opts -> Pretty.runCommand opts
Arity opts -> Arity.runCommand opts
TypeCheck opts -> InternalTypecheck.runCommand opts
TypeCheck opts -> Typecheck.runCommand opts
Reachability opts -> Reachability.runCommand opts

View File

@ -2,6 +2,7 @@ module Commands.Dev.Internal.Options where
import Commands.Dev.Internal.Arity.Options
import Commands.Dev.Internal.Pretty.Options
import Commands.Dev.Internal.Reachability.Options
import Commands.Dev.Internal.Typecheck.Options
import CommonOptions
@ -9,6 +10,7 @@ data InternalCommand
= Pretty InternalPrettyOptions
| TypeCheck InternalTypeOptions
| Arity InternalArityOptions
| Reachability InternalReachabilityOptions
deriving stock (Data)
parseInternalCommand :: Parser InternalCommand
@ -17,7 +19,8 @@ parseInternalCommand =
mconcat
[ commandPretty,
commandArity,
commandTypeCheck
commandTypeCheck,
commandReachability
]
where
commandArity :: Mod CommandFields InternalCommand
@ -29,6 +32,9 @@ parseInternalCommand =
commandTypeCheck :: Mod CommandFields InternalCommand
commandTypeCheck = command "typecheck" typeCheckInfo
commandReachability :: Mod CommandFields InternalCommand
commandReachability = command "reachability" reachabilityInfo
arityInfo :: ParserInfo InternalCommand
arityInfo =
info
@ -46,3 +52,9 @@ parseInternalCommand =
info
(TypeCheck <$> parseInternalType)
(progDesc "Translate a Juvix file to Internal and typecheck the result")
reachabilityInfo :: ParserInfo InternalCommand
reachabilityInfo =
info
(Reachability <$> parseInternalReachability)
(progDesc "Print reachability information")

View File

@ -3,7 +3,7 @@ module Commands.Dev.Internal.Pretty where
import Commands.Base
import Commands.Dev.Internal.Pretty.Options
import Juvix.Compiler.Internal.Pretty qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
runCommand :: (Members '[Embed IO, App] r) => InternalPrettyOptions -> Sem r ()
runCommand opts = do

View File

@ -0,0 +1,12 @@
module Commands.Dev.Internal.Reachability where
import Commands.Base
import Commands.Dev.Internal.Reachability.Options
import Juvix.Compiler.Internal.Pretty qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
runCommand :: (Members '[Embed IO, App] r) => InternalReachabilityOptions -> Sem r ()
runCommand opts = do
globalOpts <- askGlobalOptions
depInfo <- (^. Internal.resultDepInfo) <$> runPipeline (opts ^. internalReachabilityInputFile) upToInternal
renderStdOut (Internal.ppOut globalOpts depInfo)

View File

@ -0,0 +1,15 @@
module Commands.Dev.Internal.Reachability.Options where
import CommonOptions
newtype InternalReachabilityOptions = InternalReachabilityOptions
{ _internalReachabilityInputFile :: AppPath File
}
deriving stock (Data)
makeLenses ''InternalReachabilityOptions
parseInternalReachability :: Parser InternalReachabilityOptions
parseInternalReachability = do
_internalReachabilityInputFile <- parseInputJuvixFile
pure InternalReachabilityOptions {..}

View File

@ -5,8 +5,7 @@ import Commands.Dev.Termination.CallGraph.Options
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Language qualified as Internal
import Juvix.Compiler.Internal.Pretty qualified as Internal
-- import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination
import Juvix.Prelude.Pretty

View File

@ -4,7 +4,7 @@ import Commands.Base
import Commands.Dev.Termination.Calls.Options
import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
import Juvix.Compiler.Internal.Pretty qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination qualified as Termination
runCommand :: Members '[Embed IO, App] r => CallsOptions -> Sem r ()

View File

@ -4,7 +4,6 @@ module GlobalOptions
where
import CommonOptions
import Juvix.Compiler.Abstract.Pretty.Options qualified as Abstract
import Juvix.Compiler.Core.Options qualified as Core
import Juvix.Compiler.Internal.Pretty.Options qualified as Internal
import Juvix.Compiler.Pipeline
@ -32,12 +31,6 @@ instance CanonicalProjection GlobalOptions Internal.Options where
{ Internal._optShowNameIds = g ^. globalShowNameIds
}
instance CanonicalProjection GlobalOptions Abstract.Options where
project g =
Abstract.defaultOptions
{ Abstract._optShowNameIds = g ^. globalShowNameIds
}
instance CanonicalProjection GlobalOptions E.GenericOptions where
project GlobalOptions {..} =
E.GenericOptions

View File

@ -1,10 +0,0 @@
module Juvix.Compiler.Abstract.Data
( module Juvix.Compiler.Abstract.Data.Name,
module Juvix.Compiler.Abstract.Data.InfoTable,
module Juvix.Compiler.Abstract.Data.InfoTableBuilder,
)
where
import Juvix.Compiler.Abstract.Data.InfoTable
import Juvix.Compiler.Abstract.Data.InfoTableBuilder
import Juvix.Compiler.Abstract.Data.Name

View File

@ -1,44 +0,0 @@
module Juvix.Compiler.Abstract.Data.InfoTable where
import Juvix.Compiler.Abstract.Language
import Juvix.Prelude
newtype FunctionInfo = FunctionInfo
{ _functionInfoDef :: FunctionDef
}
deriving stock (Show)
data ConstructorInfo = ConstructorInfo
{ _constructorInfoInductive :: InductiveInfo,
_constructorInfoType :: Expression
}
newtype AxiomInfo = AxiomInfo
{ _axiomInfoType :: Expression
}
newtype InductiveInfo = InductiveInfo
{ _inductiveInfoDef :: InductiveDef
}
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

View File

@ -1,71 +0,0 @@
module Juvix.Compiler.Abstract.Data.InfoTableBuilder
( module Juvix.Compiler.Abstract.Data.InfoTableBuilder,
module Juvix.Compiler.Abstract.Data.InfoTable,
)
where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Abstract.Data.InfoTable
import Juvix.Compiler.Abstract.Language
import Juvix.Prelude
data InfoTableBuilder m a where
RegisterAxiom :: AxiomDef -> InfoTableBuilder m ()
RegisterConstructor :: InductiveInfo -> InductiveConstructorDef -> InfoTableBuilder m ()
RegisterInductive :: InductiveDef -> InfoTableBuilder m InductiveInfo
RegisterFunction :: FunctionDef -> InfoTableBuilder m ()
makeSem ''InfoTableBuilder
registerFunction' ::
(Member InfoTableBuilder r) =>
FunctionDef ->
Sem r FunctionDef
registerFunction' ts = registerFunction ts $> ts
registerAxiom' ::
(Member InfoTableBuilder r) =>
AxiomDef ->
Sem r AxiomDef
registerAxiom' a = registerAxiom a $> a
toState :: Sem (InfoTableBuilder ': r) a -> Sem (State InfoTable ': r) a
toState = reinterpret $ \case
RegisterAxiom d ->
let ref = AxiomRef (d ^. axiomName)
info =
AxiomInfo
{ _axiomInfoType = d ^. axiomType
}
in modify (over infoAxioms (HashMap.insert ref info))
RegisterConstructor _constructorInfoInductive def ->
let ref = ConstructorRef (def ^. constructorName)
info =
ConstructorInfo
{ _constructorInfoType = def ^. constructorType,
..
}
in modify (over infoConstructors (HashMap.insert ref info))
RegisterInductive ity ->
let ref = InductiveRef (ity ^. inductiveName)
info =
InductiveInfo
{ _inductiveInfoDef = ity
}
in modify (over infoInductives (HashMap.insert ref info)) $> info
RegisterFunction _functionInfoDef ->
let ref = FunctionRef (_functionInfoDef ^. funDefName)
info =
FunctionInfo
{ ..
}
in modify (over infoFunctions (HashMap.insert ref info))
runInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
runInfoTableBuilder = runState emptyInfoTable . toState
runInfoTableBuilder' :: InfoTable -> Sem (InfoTableBuilder ': r) a -> Sem r (InfoTable, a)
runInfoTableBuilder' t = runState t . toState
ignoreInfoTableBuilder :: Sem (InfoTableBuilder ': r) a -> Sem r a
ignoreInfoTableBuilder = fmap snd . runInfoTableBuilder

View File

@ -1,10 +0,0 @@
module Juvix.Compiler.Abstract.Data.NameDependencyInfo
( module Juvix.Compiler.Abstract.Data.NameDependencyInfo,
module Juvix.Data.DependencyInfo,
)
where
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Data.DependencyInfo
type NameDependencyInfo = DependencyInfo Name

View File

@ -1,10 +0,0 @@
module Juvix.Compiler.Abstract.Extra
( module Juvix.Compiler.Abstract.Language,
module Juvix.Compiler.Abstract.Extra.Functions,
module Juvix.Compiler.Abstract.Extra.DependencyBuilder,
)
where
import Juvix.Compiler.Abstract.Extra.DependencyBuilder
import Juvix.Compiler.Abstract.Extra.Functions
import Juvix.Compiler.Abstract.Language

View File

@ -1,342 +0,0 @@
module Juvix.Compiler.Abstract.Extra.Functions where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Abstract.Language
import Juvix.Data.Effect.NameIdGen
import Juvix.Prelude
data ApplicationArg = ApplicationArg
{ _appArgIsImplicit :: IsImplicit,
_appArg :: Expression
}
makeLenses ''ApplicationArg
patternVariables :: Traversal' Pattern VarName
patternVariables f p = case p of
PatternVariable v -> PatternVariable <$> f v
PatternWildcard {} -> pure p
PatternEmpty {} -> pure p
PatternConstructorApp app -> PatternConstructorApp <$> appVariables f app
patternArgVariables :: Traversal' PatternArg VarName
patternArgVariables f (PatternArg i n p) = PatternArg i <$> traverse f n <*> patternVariables f p
appVariables :: Traversal' ConstructorApp VarName
appVariables f = traverseOf constrAppParameters (traverse (patternArgVariables f))
idenName :: Iden -> Name
idenName = \case
IdenFunction (FunctionRef f) -> f
IdenConstructor (ConstructorRef c) -> c
IdenVar v -> v
IdenInductive (InductiveRef i) -> i
IdenAxiom (AxiomRef a) -> a
-- | A fold over all transitive children, including self
patternCosmos :: SimpleFold Pattern Pattern
patternCosmos f p = case p of
PatternVariable {} -> f p
PatternWildcard {} -> f p
PatternEmpty {} -> f p
PatternConstructorApp (ConstructorApp r args) ->
f p *> do
args' <- traverse (traverseOf patternArgPattern (patternCosmos f)) args
pure (PatternConstructorApp (ConstructorApp r args'))
patternArgNameFold :: SimpleFold (Maybe Name) Pattern
patternArgNameFold f = \case
Nothing -> mempty
Just n -> Const (getConst (f (PatternVariable n)))
-- | A fold over all transitive children, including self
patternArgCosmos :: SimpleFold PatternArg Pattern
patternArgCosmos f p = do
_patternArgPattern <- patternCosmos f (p ^. patternArgPattern)
_patternArgName <- patternArgNameFold f (p ^. patternArgName)
pure PatternArg {..}
where
_patternArgIsImplicit = p ^. patternArgIsImplicit
-- | A fold over all transitive children, excluding self
patternSubCosmos :: SimpleFold Pattern Pattern
patternSubCosmos f p = case p of
PatternVariable {} -> pure p
PatternWildcard {} -> pure p
PatternEmpty {} -> pure p
PatternConstructorApp (ConstructorApp r args) -> do
args' <- traverse (patternArgCosmos f) args
pure (PatternConstructorApp (ConstructorApp r args'))
viewApp :: Expression -> (Expression, [ApplicationArg])
viewApp e =
case e of
ExpressionApplication (Application l r i) ->
second (`snoc` ApplicationArg i r) (viewApp l)
_ -> (e, [])
viewAppArgAsPattern :: ApplicationArg -> Maybe PatternArg
viewAppArgAsPattern a = do
p' <- viewExpressionAsPattern (a ^. appArg)
return
( PatternArg
{ _patternArgIsImplicit = a ^. appArgIsImplicit,
_patternArgName = Nothing,
_patternArgPattern = p'
}
)
viewExpressionAsPattern :: Expression -> Maybe Pattern
viewExpressionAsPattern e = case viewApp e of
(f, args)
| Just c <- getConstructor f -> do
args' <- mapM viewAppArgAsPattern args
Just $ PatternConstructorApp (ConstructorApp c args')
(f, [])
| Just v <- getVariable f -> Just (PatternVariable v)
_ -> Nothing
where
getConstructor :: Expression -> Maybe ConstructorRef
getConstructor f = case f of
ExpressionIden (IdenConstructor n) -> Just n
_ -> Nothing
getVariable :: Expression -> Maybe VarName
getVariable f = case f of
ExpressionIden (IdenVar n) -> Just n
_ -> Nothing
addName :: (Member (State (HashMap Name Name)) r) => Name -> Name -> Sem r ()
addName na nb = modify (HashMap.insert na nb)
foldApplication :: Expression -> [ApplicationArg] -> Expression
foldApplication f args = case args of
[] -> f
((ApplicationArg i a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as
matchFunctionParameter ::
forall r.
(Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r) =>
FunctionParameter ->
FunctionParameter ->
Sem r ()
matchFunctionParameter pa pb = do
goParamName (pa ^. paramName) (pb ^. paramName)
goParamImplicit (pa ^. paramImplicit) (pb ^. paramImplicit)
goParamType (pa ^. paramType) (pb ^. paramType)
where
goParamType :: Expression -> Expression -> Sem r ()
goParamType ua ub = matchExpressions ua ub
goParamImplicit :: IsImplicit -> IsImplicit -> Sem r ()
goParamImplicit ua ub = unless (ua == ub) (throw @Text "implicit mismatch")
goParamName :: Maybe VarName -> Maybe VarName -> Sem r ()
goParamName (Just va) (Just vb) = addName va vb
goParamName _ _ = return ()
matchExpressions ::
forall r.
(Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r) =>
Expression ->
Expression ->
Sem r ()
matchExpressions = go
where
-- Soft free vars are allowed to be matched
isSoftFreeVar :: VarName -> Sem r Bool
isSoftFreeVar = asks . HashSet.member
go :: Expression -> Expression -> Sem r ()
go a b = case (a, b) of
(ExpressionIden ia, ExpressionIden ib) -> case (ia, ib) of
(IdenVar va, IdenVar vb) -> do
addIfFreeVar va vb
addIfFreeVar vb va
unlessM ((== Just vb) <$> gets @(HashMap Name Name) (^. at va)) err
(_, _) -> unless (ia == ib) err
(ExpressionIden {}, _) -> err
(_, ExpressionIden {}) -> err
(ExpressionApplication ia, ExpressionApplication ib) ->
goApp ia ib
(ExpressionApplication {}, _) -> err
(_, ExpressionApplication {}) -> err
(ExpressionLambda ia, ExpressionLambda ib) ->
goLambda ia ib
(ExpressionLambda {}, _) -> err
(_, ExpressionLambda {}) -> err
(ExpressionCase {}, ExpressionCase {}) -> error "not implemented"
(ExpressionCase {}, _) -> err
(_, ExpressionCase {}) -> err
(ExpressionUniverse ia, ExpressionUniverse ib) ->
unless (ia == ib) err
(ExpressionUniverse {}, _) -> err
(_, ExpressionUniverse {}) -> err
(ExpressionFunction ia, ExpressionFunction ib) ->
goFunction ia ib
(ExpressionFunction {}, _) -> err
(_, ExpressionFunction {}) -> err
(ExpressionLiteral ia, ExpressionLiteral ib) ->
unless (ia == ib) err
(ExpressionLiteral {}, _) -> err
(_, ExpressionLiteral {}) -> err
(ExpressionLet {}, ExpressionLet {}) -> error "not implemented"
(_, ExpressionLet {}) -> err
(ExpressionLet {}, _) -> err
(ExpressionHole _, ExpressionHole _) -> return ()
addIfFreeVar :: VarName -> VarName -> Sem r ()
addIfFreeVar va vb = whenM (isSoftFreeVar va) (addName va vb)
err :: Sem r a
err = throw @Text "Expression missmatch"
goLambda :: Lambda -> Lambda -> Sem r ()
goLambda = error "TODO not implemented yet"
goApp :: Application -> Application -> Sem r ()
goApp (Application al ar aim) (Application bl br bim) = do
unless (aim == bim) err
go al bl
go ar br
goFunction :: Function -> Function -> Sem r ()
goFunction (Function al ar) (Function bl br) = do
matchFunctionParameter al bl
matchExpressions ar br
class IsExpression a where
toExpression :: a -> Expression
instance IsExpression ConstructorRef where
toExpression = toExpression . IdenConstructor
instance IsExpression InductiveRef where
toExpression = toExpression . IdenInductive
instance IsExpression FunctionRef where
toExpression = toExpression . IdenFunction
instance IsExpression AxiomRef where
toExpression = toExpression . IdenAxiom
instance IsExpression Iden where
toExpression = ExpressionIden
instance IsExpression Expression where
toExpression = id
instance IsExpression Name where
toExpression n = case n ^. nameKind of
KNameConstructor -> toExpression (ConstructorRef n)
KNameInductive -> toExpression (InductiveRef n)
KNameFunction -> toExpression (FunctionRef n)
KNameAxiom -> toExpression (AxiomRef n)
KNameLocal -> toExpression (IdenVar n)
KNameLocalModule -> impossible
KNameTopModule -> impossible
instance IsExpression Universe where
toExpression = ExpressionUniverse
instance IsExpression Application where
toExpression = ExpressionApplication
instance IsExpression Function where
toExpression = ExpressionFunction
instance IsExpression ConstructorApp where
toExpression (ConstructorApp c args) =
foldApplication (toExpression c) (map toApplicationArg args)
isSmallUniverse' :: Expression -> Bool
isSmallUniverse' = \case
ExpressionUniverse u -> isSmallUniverse u
_ -> False
toApplicationArg :: PatternArg -> ApplicationArg
toApplicationArg p =
set appArgIsImplicit (p ^. patternArgIsImplicit) (helper (p ^. patternArgPattern))
where
helper :: Pattern -> ApplicationArg
helper = \case
PatternVariable v -> ApplicationArg Explicit (toExpression v)
PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
PatternEmpty -> impossible
PatternWildcard _ ->
ApplicationArg
Explicit
( ExpressionHole
( Hole
{ _holeId = error "hole with no id",
_holeKw = error "hole with no location"
}
)
)
clauseLhsAsExpression :: FunctionClause -> Expression
clauseLhsAsExpression cl =
foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
expressionArrow :: (IsExpression a, IsExpression b) => IsImplicit -> a -> b -> Expression
expressionArrow isImpl a b =
ExpressionFunction
( Function
( FunctionParameter
{ _paramName = Nothing,
_paramImplicit = isImpl,
_paramType = toExpression a
}
)
(toExpression b)
)
infixr 0 <>-->
(<>-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
(<>-->) = expressionArrow Implicit
infixr 0 -->
(-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
(-->) = expressionArrow Explicit
infix 4 ===
(===) :: (IsExpression a, IsExpression b) => a -> b -> Bool
a === b = (toExpression a ==% toExpression b) mempty
leftEq :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
leftEq a b free =
isRight
. run
. runError @Text
. runReader free
. evalState (mempty @(HashMap Name Name))
$ matchExpressions (toExpression a) (toExpression b)
infix 4 ==%
(==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
(==%) a b free = leftEq a b free || leftEq b a free
infixl 9 @@
(@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression
a @@ b = toExpression (Application (toExpression a) (toExpression b) Explicit)
freshVar :: (Member NameIdGen r) => Text -> Sem r VarName
freshVar n = do
uid <- freshNameId
return
Name
{ _nameId = uid,
_nameText = n,
_nameKind = KNameLocal,
_namePretty = n,
_nameFixity = Nothing,
_nameLoc = error "freshVar with no location"
}
freshHole :: (Member NameIdGen r) => Sem r Expression
freshHole = do
uid <- freshNameId
return $
ExpressionHole
( Hole
{ _holeId = uid,
_holeKw = error "freshHole with no location"
}
)

View File

@ -1,293 +0,0 @@
module Juvix.Compiler.Abstract.Language
( module Juvix.Compiler.Abstract.Language,
module Juvix.Compiler.Concrete.Language,
module Juvix.Data.Hole,
module Juvix.Compiler.Concrete.Data.Builtins,
module Juvix.Compiler.Concrete.Data.Literal,
module Juvix.Data.Universe,
module Juvix.Compiler.Abstract.Data.Name,
module Juvix.Data.Wildcard,
module Juvix.Data.IsImplicit,
)
where
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Concrete.Data.Builtins
import Juvix.Compiler.Concrete.Data.Literal
import Juvix.Compiler.Concrete.Language (symbolLoc)
import Juvix.Data.Hole
import Juvix.Data.IsImplicit
import Juvix.Data.Universe
import Juvix.Data.Wildcard
import Juvix.Prelude
type LocalModule = Module
type TopModule = Module
type TopModuleName = Name
data Module = Module
{ _moduleName :: Name,
_moduleExamples :: [Example],
_moduleBody :: ModuleBody,
_modulePragmas :: Pragmas
}
deriving stock (Eq, Show)
newtype ModuleBody = ModuleBody
{ _moduleStatements :: [Statement]
}
deriving stock (Eq, Show)
data Statement
= StatementInductive InductiveDef
| StatementFunction FunctionDef
| StatementImport TopModule
| StatementLocalModule LocalModule
| StatementAxiom AxiomDef
deriving stock (Eq, Show)
data Example = Example
{ _exampleId :: NameId,
_exampleExpression :: Expression
}
deriving stock (Eq, Show)
data FunctionDef = FunctionDef
{ _funDefName :: FunctionName,
_funDefTypeSig :: Expression,
_funDefExamples :: [Example],
_funDefClauses :: NonEmpty FunctionClause,
_funDefBuiltin :: Maybe BuiltinFunction,
_funDefTerminating :: Bool,
_funDefPragmas :: Pragmas
}
deriving stock (Eq, Show)
data FunctionClause = FunctionClause
{ _clauseName :: FunctionName,
_clausePatterns :: [PatternArg],
_clauseBody :: Expression
}
deriving stock (Eq, Show)
newtype FunctionRef = FunctionRef
{_functionRefName :: Name}
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype ConstructorRef = ConstructorRef
{_constructorRefName :: Name}
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype InductiveRef = InductiveRef
{_inductiveRefName :: Name}
deriving stock (Eq, Show)
deriving newtype (Hashable)
newtype AxiomRef = AxiomRef
{_axiomRefName :: Name}
deriving stock (Eq, Show)
deriving newtype (Hashable)
data Iden
= IdenFunction FunctionRef
| IdenConstructor ConstructorRef
| IdenVar VarName
| IdenInductive InductiveRef
| IdenAxiom AxiomRef
deriving stock (Eq, Show)
data CaseBranch = CaseBranch
{ _caseBranchPattern :: PatternArg,
_caseBranchExpression :: Expression
}
deriving stock (Eq, Show)
data Case = Case
{ _caseExpression :: Expression,
_caseBranches :: NonEmpty CaseBranch,
_caseParens :: Bool
}
deriving stock (Eq, Show)
newtype LetClause
= LetFunDef FunctionDef
deriving stock (Eq, Show)
data Let = Let
{ _letClauses :: NonEmpty LetClause,
_letExpression :: Expression
}
deriving stock (Eq, Show)
data Expression
= ExpressionIden Iden
| ExpressionApplication Application
| ExpressionLet Let
| ExpressionCase Case
| ExpressionUniverse Universe
| ExpressionFunction Function
| ExpressionLiteral LiteralLoc
| ExpressionHole Hole
| ExpressionLambda Lambda
deriving stock (Eq, Show)
data Application = Application
{ _appLeft :: Expression,
_appRight :: Expression,
_appImplicit :: IsImplicit
}
deriving stock (Eq, Show)
newtype Lambda = Lambda
{_lambdaClauses :: NonEmpty LambdaClause}
deriving stock (Eq, Show)
data LambdaClause = LambdaClause
{ _lambdaParameters :: NonEmpty PatternArg,
_lambdaBody :: Expression
}
deriving stock (Eq, Show)
data FunctionParameter = FunctionParameter
{ _paramName :: Maybe VarName,
_paramImplicit :: IsImplicit,
_paramType :: Expression
}
deriving stock (Eq, Show)
data Function = Function
{ _funParameter :: FunctionParameter,
_funReturn :: Expression
}
deriving stock (Eq, Show)
instance HasAtomicity Function where
atomicity = const (Aggregate funFixity)
-- | Fully applied constructor in a pattern.
data ConstructorApp = ConstructorApp
{ _constrAppConstructor :: ConstructorRef,
_constrAppParameters :: [PatternArg]
}
deriving stock (Eq, Show)
data PatternArg = PatternArg
{ _patternArgIsImplicit :: IsImplicit,
_patternArgName :: Maybe VarName,
_patternArgPattern :: Pattern
}
deriving stock (Eq, Show)
data Pattern
= PatternVariable VarName
| PatternConstructorApp ConstructorApp
| PatternWildcard Wildcard
| PatternEmpty
deriving stock (Eq, Show)
data InductiveDef = InductiveDef
{ _inductiveName :: InductiveName,
_inductiveBuiltin :: Maybe BuiltinInductive,
_inductiveParameters :: [FunctionParameter],
_inductiveType :: Expression,
_inductiveExamples :: [Example],
_inductiveConstructors :: [InductiveConstructorDef],
_inductivePositive :: Bool,
_inductivePragmas :: Pragmas
}
deriving stock (Eq, Show)
data InductiveConstructorDef = InductiveConstructorDef
{ _constructorName :: ConstrName,
_constructorExamples :: [Example],
_constructorType :: Expression,
_constructorPragmas :: Pragmas
}
deriving stock (Eq, Show)
data AxiomDef = AxiomDef
{ _axiomName :: AxiomName,
_axiomBuiltin :: Maybe BuiltinAxiom,
_axiomType :: Expression,
_axiomPragmas :: Pragmas
}
deriving stock (Eq, Show)
makeLenses ''Module
makeLenses ''Case
makeLenses ''CaseBranch
makeLenses ''Let
makeLenses ''LetClause
makeLenses ''Example
makeLenses ''PatternArg
makeLenses ''FunctionParameter
makeLenses ''Function
makeLenses ''FunctionDef
makeLenses ''FunctionClause
makeLenses ''InductiveDef
makeLenses ''ModuleBody
makeLenses ''InductiveConstructorDef
makeLenses ''ConstructorApp
makeLenses ''FunctionRef
makeLenses ''ConstructorRef
makeLenses ''InductiveRef
makeLenses ''AxiomRef
makeLenses ''AxiomDef
instance HasAtomicity Expression where
atomicity = \case
ExpressionIden {} -> Atom
ExpressionHole {} -> Atom
ExpressionUniverse u -> atomicity u
ExpressionCase u -> atomicity u
ExpressionLet l -> atomicity l
ExpressionApplication a -> atomicity a
ExpressionFunction f -> atomicity f
ExpressionLiteral f -> atomicity f
ExpressionLambda l -> atomicity l
instance HasAtomicity Case where
atomicity = const Atom
instance HasAtomicity Application where
atomicity = const (Aggregate appFixity)
instance HasAtomicity Let where
atomicity Let {..} = atomicity _letExpression
instance HasAtomicity Lambda where
atomicity = const Atom
instance HasAtomicity ConstructorApp where
atomicity (ConstructorApp _ ps)
| null ps = Atom
| otherwise = Aggregate appFixity
instance HasAtomicity Pattern where
atomicity = \case
PatternVariable {} -> Atom
PatternConstructorApp a -> atomicity a
PatternWildcard {} -> Atom
PatternEmpty -> Atom
instance HasAtomicity PatternArg where
atomicity p
| Implicit <- p ^. patternArgIsImplicit = Atom
| isJust (p ^. patternArgName) = Atom
| otherwise = atomicity (p ^. patternArgPattern)
instance HasLoc InductiveConstructorDef where
getLoc = getLoc . (^. constructorName)
instance HasLoc InductiveDef where
getLoc = getLoc . (^. inductiveName)
instance HasLoc AxiomDef where
getLoc = getLoc . (^. axiomName)
instance HasLoc FunctionDef where
getLoc = getLoc . (^. funDefName)

View File

@ -1,19 +0,0 @@
module Juvix.Compiler.Abstract.Pretty
( module Juvix.Compiler.Abstract.Pretty,
module Juvix.Compiler.Abstract.Pretty.Options,
)
where
import Juvix.Compiler.Abstract.Pretty.Base
import Juvix.Compiler.Abstract.Pretty.Options
import Juvix.Data.PPOutput
import Juvix.Prelude
ppOutDefault :: (PrettyCode c) => c -> AnsiText
ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
ppOut o = mkAnsiText . PPOutput . doc (project o)
ppTrace :: (PrettyCode c) => c -> Text
ppTrace = toAnsiText True . ppOutDefault

View File

@ -1,218 +0,0 @@
module Juvix.Compiler.Abstract.Pretty.Base
( module Juvix.Compiler.Abstract.Pretty.Base,
module Juvix.Data.CodeAnn,
module Juvix.Compiler.Abstract.Pretty.Options,
)
where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Abstract.Pretty.Options
import Juvix.Compiler.Concrete.Print.Base qualified as S
import Juvix.Data.CodeAnn
import Juvix.Prelude
doc :: (PrettyCode c) => Options -> c -> Doc Ann
doc opts =
run
. runReader opts
. ppCode
toSOptions :: Options -> S.Options
toSOptions Options {..} =
S.defaultOptions
{ S._optShowNameIds = _optShowNameIds
}
class PrettyCode c where
ppCode :: (Members '[Reader Options] r) => c -> Sem r (Doc Ann)
ppSCode :: (Members '[Reader Options] r, S.PrettyPrint c) => c -> Sem r (Doc Ann)
ppSCode c = do
opts <- asks toSOptions
return (S.docNoComments opts c)
ppDefault :: (PrettyCode c) => c -> Doc Ann
ppDefault = runPrettyCode defaultOptions
runPrettyCode :: (PrettyCode c) => Options -> c -> Doc Ann
runPrettyCode opts = run . runReader opts . ppCode
ppPostExpression ::
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
Fixity ->
a ->
Sem r (Doc Ann)
ppPostExpression = ppLRExpression isPostfixAssoc
ppRightExpression ::
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
Fixity ->
a ->
Sem r (Doc Ann)
ppRightExpression = ppLRExpression isRightAssoc
ppLeftExpression ::
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
Fixity ->
a ->
Sem r (Doc Ann)
ppLeftExpression = ppLRExpression isLeftAssoc
ppLRExpression ::
(HasAtomicity a, PrettyCode a, Member (Reader Options) r) =>
(Fixity -> Bool) ->
Fixity ->
a ->
Sem r (Doc Ann)
ppLRExpression associates fixlr e =
parensCond (atomParens associates (atomicity e) fixlr)
<$> ppCode e
ppCodeAtom ::
(HasAtomicity c, PrettyCode c, Members '[Reader Options] r) =>
c ->
Sem r (Doc Ann)
ppCodeAtom c = do
p' <- ppCode c
return $ if isAtomic c then p' else parens p'
instance PrettyCode Iden where
ppCode = ppCode . idenName
instance PrettyCode Application where
ppCode (Application l r i) = do
l' <- ppLeftExpression appFixity l
r' <- case i of
Explicit -> ppRightExpression appFixity r
Implicit -> implicitDelim i <$> ppCode r
return $ l' <+> r'
instance PrettyCode Universe where
ppCode Universe {..} = return $ kwType <+?> (pretty <$> _universeLevel)
instance PrettyCode PatternArg where
ppCode (PatternArg i n p) = do
n' <- traverse ppCode n
p' <- ppCode p
return $ (n' <&> (<> kwAt)) ?<> delimIf i (isJust n && not (isAtomic p)) p'
instance PrettyCode LambdaClause where
ppCode LambdaClause {..} = do
lambdaParameters' <- hsep . toList <$> mapM ppCode _lambdaParameters
lambdaBody' <- ppCode _lambdaBody
return $ lambdaParameters' <+> kwAssign <+> lambdaBody'
instance PrettyCode Lambda where
ppCode Lambda {..} = do
lambdaClauses' <- ppPipeBlock _lambdaClauses
return $ kwLambda <+> lambdaClauses'
ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items
ppBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
ppBlock items = vsep . toList <$> mapM (fmap endSemicolon . ppCode) items
instance PrettyCode ConstructorApp where
ppCode (ConstructorApp ctr args) = do
ctr' <- ppCode ctr
if
| null args -> do
args' <- hsep <$> mapM ppCode args
return (parens (ctr' <+> args'))
| otherwise -> return ctr'
instance PrettyCode Pattern where
ppCode = \case
PatternVariable v -> ppCode v
PatternWildcard {} -> return kwWildcard
PatternEmpty {} -> return $ parens mempty
PatternConstructorApp constr -> ppCode constr
instance PrettyCode Expression where
ppCode e = case e of
ExpressionIden i -> ppCode i
ExpressionUniverse u -> ppCode u
ExpressionApplication a -> ppCode a
ExpressionFunction f -> ppCode f
ExpressionLiteral l -> ppSCode l
ExpressionHole h -> ppSCode h
ExpressionLambda l -> ppCode l
ExpressionLet l -> ppCode l
ExpressionCase c -> ppCode c
instance PrettyCode CaseBranch where
ppCode CaseBranch {..} = do
pat <- ppCode _caseBranchPattern
e <- ppCode _caseBranchExpression
return $ kwPipe <+> pat <+> kwAssign <+> e
instance PrettyCode Case where
ppCode Case {..} = do
exp <- ppCode _caseExpression
branches <- indent' . vsep <$> mapM ppCode _caseBranches
return $ parensIf _caseParens (kwCase <+> exp <> line <> branches)
instance PrettyCode FunctionClause where
ppCode c = do
funName <- ppCode (c ^. clauseName)
clausePatterns' <- hsepMaybe <$> mapM ppCodeAtom (c ^. clausePatterns)
clauseBody' <- ppCode (c ^. clauseBody)
return $ funName <+?> clausePatterns' <+> kwAssign <+> clauseBody'
instance PrettyCode FunctionDef where
ppCode f = do
funDefName' <- ppCode (f ^. funDefName)
funDefType' <- ppCode (f ^. funDefTypeSig)
clauses' <- mapM ppCode (f ^. funDefClauses)
return $
funDefName'
<+> kwColonColon
<+> funDefType'
<> line
<> vsep (toList clauses')
instance PrettyCode LetClause where
ppCode = \case
LetFunDef f -> ppCode f
instance PrettyCode Let where
ppCode l = do
letClauses' <- blockIndent <$> ppBlock (l ^. letClauses)
letExpression' <- ppCode (l ^. letExpression)
return $ kwLet <+> letClauses' <+> kwIn <+> letExpression'
instance PrettyCode FunctionParameter where
ppCode FunctionParameter {..} = do
case _paramName of
Nothing -> ppLeftExpression funFixity _paramType
Just n -> do
paramName' <- ppCode n
paramType' <- ppCode _paramType
return $ implicitDelim _paramImplicit (paramName' <+> kwColon <+> paramType')
instance PrettyCode NameId where
ppCode (NameId k) = return (pretty k)
instance PrettyCode Name where
ppCode n = do
showNameId <- asks (^. optShowNameIds)
return (prettyName showNameId n)
instance PrettyCode Function where
ppCode Function {..} = do
funParameter' <- ppCode _funParameter
funReturn' <- ppRightExpression funFixity _funReturn
return $ funParameter' <+> kwArrow <+> funReturn'
instance PrettyCode FunctionRef where
ppCode FunctionRef {..} = ppCode _functionRefName
instance PrettyCode ConstructorRef where
ppCode ConstructorRef {..} = ppCode _constructorRefName
instance PrettyCode InductiveRef where
ppCode InductiveRef {..} = ppCode _inductiveRefName
instance PrettyCode AxiomRef where
ppCode AxiomRef {..} = ppCode _axiomRefName

View File

@ -1,15 +0,0 @@
module Juvix.Compiler.Abstract.Pretty.Options where
import Juvix.Prelude
newtype Options = Options
{ _optShowNameIds :: Bool
}
defaultOptions :: Options
defaultOptions =
Options
{ _optShowNameIds = False
}
makeLenses ''Options

View File

@ -1,10 +0,0 @@
module Juvix.Compiler.Abstract.Translation
( module Juvix.Compiler.Abstract.Language,
module Juvix.Compiler.Abstract.Data,
module Juvix.Compiler.Abstract.Translation.FromConcrete,
)
where
import Juvix.Compiler.Abstract.Data
import Juvix.Compiler.Abstract.Language
import Juvix.Compiler.Abstract.Translation.FromConcrete

View File

@ -1,630 +0,0 @@
module Juvix.Compiler.Abstract.Translation.FromConcrete
( module Juvix.Compiler.Abstract.Translation.FromConcrete,
module Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context,
)
where
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Abstract.Data.InfoTableBuilder
import Juvix.Compiler.Abstract.Language qualified as Abstract
import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Builtins
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Language qualified as Concrete
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
import Juvix.Data.NameKind
import Juvix.Prelude
unsupported :: Text -> a
unsupported msg = error $ msg <> "Scoped to Abstract: not yet supported"
fromConcrete :: (Members '[Error JuvixError, Builtins, NameIdGen] r) => Scoper.ScoperResult -> Sem r AbstractResult
fromConcrete _resultScoper =
mapError (JuvixError @ScoperError) $ do
(_resultTable, (_resultModulesCache, _resultModules)) <-
runInfoTableBuilder $
runReader @Pragmas mempty $
runState (ModulesCache mempty) $
mapM goTopModule ms
let _resultExports = _resultScoper ^. Scoper.resultExports
return AbstractResult {..}
where
ms = _resultScoper ^. Scoper.resultModules
fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Abstract.Expression
fromConcreteExpression = mapError (JuvixError @ScoperError) . ignoreInfoTableBuilder . runReader @Pragmas mempty . goExpression
fromConcreteImport ::
Members '[Error JuvixError, NameIdGen, Builtins, InfoTableBuilder, State ModulesCache] r =>
Scoper.Import 'Scoped ->
Sem r Abstract.TopModule
fromConcreteImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goImport
fromConcreteOpenImport ::
Members '[Error JuvixError, NameIdGen, Builtins, InfoTableBuilder, State ModulesCache] r =>
Scoper.OpenModule 'Scoped ->
Sem r (Maybe Abstract.TopModule)
fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'
goTopModule ::
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
Module 'Scoped 'ModuleTop ->
Sem r Abstract.TopModule
goTopModule = goModule
goLocalModule ::
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
Module 'Scoped 'ModuleLocal ->
Sem r Abstract.LocalModule
goLocalModule = goModule
goModule ::
forall r t.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r, SingI t) =>
Module 'Scoped t ->
Sem r Abstract.Module
goModule m = case sing :: SModuleIsTop t of
SModuleTop -> do
cache <- gets (^. cachedModules)
let moduleNameId :: S.NameId
moduleNameId = m ^. Concrete.modulePath . S.nameId
let processModule :: Sem r Abstract.Module
processModule = do
am <- goModule' m
modify (over cachedModules (HashMap.insert moduleNameId am))
return am
maybe processModule return (cache ^. at moduleNameId)
SModuleLocal -> goModule' m
where
goModule' :: Module 'Scoped t -> Sem r Abstract.Module
goModule' Module {..} = do
pragmas' <- goPragmas _modulePragmas
body' <- local (const pragmas') (goModuleBody _moduleBody)
examples' <- goExamples _moduleDoc
return
Abstract.Module
{ _moduleName = name',
_moduleBody = body',
_moduleExamples = examples',
_modulePragmas = pragmas'
}
where
name' :: Abstract.Name
name' = case sing :: SModuleIsTop t of
SModuleTop -> goSymbol (S.topModulePathName _modulePath)
SModuleLocal -> goSymbol _modulePath
goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas
goPragmas p = do
p' <- ask
return $ p' <> p ^. _Just . withLocParam . withSourceValue
goName :: S.Name -> Abstract.Name
goName name =
set Abstract.namePretty prettyStr (goSymbol (S.nameUnqualify name))
where
prettyStr :: Text
prettyStr = prettyText name
goSymbol :: S.Symbol -> Abstract.Name
goSymbol s =
Abstract.Name
{ _nameText = S.symbolText s,
_nameId = s ^. S.nameId,
_nameKind = getNameKind s,
_namePretty = S.symbolText s,
_nameLoc = s ^. S.nameConcrete . symbolLoc,
_nameFixity = s ^. S.nameFixity
}
goModuleBody ::
forall r.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
[Statement 'Scoped] ->
Sem r Abstract.ModuleBody
goModuleBody ss' = do
otherThanFunctions <- mapMaybeM goStatement ss
functions <- map (fmap Abstract.StatementFunction) <$> compiledFunctions
let _moduleStatements =
map
(^. indexedThing)
( sortOn
(^. indexedIx)
(otherThanFunctions <> functions)
)
return Abstract.ModuleBody {..}
where
ss :: [Indexed (Statement 'Scoped)]
ss = zipWith Indexed [0 ..] ss'
compiledFunctions :: Sem r [Indexed Abstract.FunctionDef]
compiledFunctions =
sequence $
[ Indexed i <$> funDef
| Indexed i sig <- sigs,
let name = sig ^. sigName,
let funDef = goTopFunctionDef sig (getClauses name)
]
where
getClauses :: S.Symbol -> [FunctionClause 'Scoped]
getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
sigs :: [Indexed (TypeSignature 'Scoped)]
sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
goImport ::
forall r.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache, Reader Pragmas] r) =>
Import 'Scoped ->
Sem r Abstract.TopModule
goImport t = goModule (t ^. importModule . moduleRefModule)
goStatement ::
forall r.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
Indexed (Statement 'Scoped) ->
Sem r (Maybe (Indexed Abstract.Statement))
goStatement (Indexed idx s) =
fmap (Indexed idx) <$> case s of
StatementAxiom d -> Just . Abstract.StatementAxiom <$> goAxiom d
StatementImport t -> Just . Abstract.StatementImport <$> goImport t
StatementSyntax {} -> return Nothing
StatementOpenModule o -> goOpenModule o
StatementInductive i -> Just . Abstract.StatementInductive <$> goInductive i
StatementModule f -> Just . Abstract.StatementLocalModule <$> goLocalModule f
StatementTypeSignature {} -> return Nothing
StatementFunctionClause {} -> return Nothing
goOpenModule' ::
forall r.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, State ModulesCache, Reader Pragmas] r) =>
OpenModule 'Scoped ->
Sem r (Maybe Abstract.TopModule)
goOpenModule' o
| isJust (o ^. openModuleImportKw) =
case o ^. openModuleName of
ModuleRef' (SModuleTop :&: m) -> Just <$> goModule (m ^. moduleRefModule)
_ -> impossible
| otherwise = return Nothing
goOpenModule ::
forall r.
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, State ModulesCache] r) =>
OpenModule 'Scoped ->
Sem r (Maybe Abstract.Statement)
goOpenModule o = fmap Abstract.StatementImport <$> goOpenModule' o
goLetFunctionDef ::
(Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Abstract.FunctionDef
goLetFunctionDef = goFunctionDefHelper
goFunctionDefHelper ::
forall r.
(Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError] r) =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Abstract.FunctionDef
goFunctionDefHelper sig@TypeSignature {..} clauses = do
let _funDefName = goSymbol _sigName
_funDefTerminating = isJust _sigTerminating
_funDefBuiltin = (^. withLocParam) <$> _sigBuiltin
_funDefTypeSig <- goExpression _sigType
_funDefExamples <- goExamples _sigDoc
_funDefPragmas <- goPragmas _sigPragmas
_funDefClauses <- case (_sigBody, nonEmpty clauses) of
(Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig))
(Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses')))
(Just body, Nothing) -> do
body' <- goExpression body
return
( pure
Abstract.FunctionClause
{ _clauseName = _funDefName,
_clausePatterns = [],
_clauseBody = body'
}
)
(Nothing, Just clauses') -> mapM goFunctionClause clauses'
let fun = Abstract.FunctionDef {..}
registerFunction' fun
goTopFunctionDef ::
forall r.
(Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Abstract.FunctionDef
goTopFunctionDef sig clauses = do
fun <- goFunctionDefHelper sig clauses
whenJust (sig ^. sigBuiltin) (registerBuiltinFunction fun . (^. withLocParam))
return fun
goExamples ::
forall r.
(Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
Maybe (Judoc 'Scoped) ->
Sem r [Abstract.Example]
goExamples = mapM goExample . maybe [] judocExamples
where
goExample :: Example 'Scoped -> Sem r Abstract.Example
goExample ex = do
e' <- goExpression (ex ^. exampleExpression)
return
Abstract.Example
{ _exampleExpression = e',
_exampleId = ex ^. exampleId
}
goFunctionClause ::
(Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
FunctionClause 'Scoped ->
Sem r Abstract.FunctionClause
goFunctionClause FunctionClause {..} = do
_clausePatterns' <- mapM goPatternArg _clausePatterns
_clauseBody' <- goExpression _clauseBody
return
Abstract.FunctionClause
{ _clauseName = goSymbol _clauseOwnerFunction,
_clausePatterns = _clausePatterns',
_clauseBody = _clauseBody'
}
goInductiveParameters ::
(Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
InductiveParameters 'Scoped ->
Sem r [Abstract.FunctionParameter]
goInductiveParameters InductiveParameters {..} = do
paramType' <- goExpression _inductiveParametersType
return $
map
( \nm ->
Abstract.FunctionParameter
{ _paramType = paramType',
_paramName = Just (goSymbol nm),
_paramImplicit = Explicit
}
)
(toList _inductiveParametersNames)
registerBuiltinInductive ::
(Members '[InfoTableBuilder, Error ScoperError, Builtins] r) =>
Abstract.InductiveDef ->
BuiltinInductive ->
Sem r ()
registerBuiltinInductive d = \case
BuiltinNat -> registerNatDef d
BuiltinBool -> registerBoolDef d
BuiltinInt -> registerIntDef d
registerBuiltinFunction ::
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
Abstract.FunctionDef ->
BuiltinFunction ->
Sem r ()
registerBuiltinFunction d = \case
BuiltinNatPlus -> registerNatPlus d
BuiltinNatSub -> registerNatSub d
BuiltinNatMul -> registerNatMul d
BuiltinNatUDiv -> registerNatUDiv d
BuiltinNatDiv -> registerNatDiv d
BuiltinNatMod -> registerNatMod d
BuiltinNatLe -> registerNatLe d
BuiltinNatLt -> registerNatLt d
BuiltinNatEq -> registerNatEq d
BuiltinBoolIf -> registerIf d
BuiltinBoolOr -> registerOr d
BuiltinBoolAnd -> registerAnd d
BuiltinIntEq -> registerIntEq d
BuiltinIntSubNat -> registerIntSubNat d
BuiltinIntPlus -> registerIntPlus d
BuiltinIntNegNat -> registerIntNegNat d
BuiltinIntNeg -> registerIntNeg d
BuiltinIntMul -> registerIntMul d
BuiltinIntDiv -> registerIntDiv d
BuiltinIntMod -> registerIntMod d
BuiltinIntSub -> registerIntSub d
BuiltinIntNonNeg -> registerIntNonNeg d
BuiltinIntLe -> registerIntLe d
BuiltinIntLt -> registerIntLt d
BuiltinSeq -> registerSeq d
registerBuiltinAxiom ::
(Members '[InfoTableBuilder, Error ScoperError, Builtins, NameIdGen] r) =>
Abstract.AxiomDef ->
BuiltinAxiom ->
Sem r ()
registerBuiltinAxiom d = \case
BuiltinIO -> registerIO d
BuiltinIOSequence -> registerIOSequence d
BuiltinIOReadline -> registerIOReadline d
BuiltinNatPrint -> registerNatPrint d
BuiltinNatToString -> registerNatToString d
BuiltinString -> registerString d
BuiltinStringPrint -> registerStringPrint d
BuiltinStringConcat -> registerStringConcat d
BuiltinStringEq -> registerStringEq d
BuiltinStringToNat -> registerStringToNat d
BuiltinBoolPrint -> registerBoolPrint d
BuiltinTrace -> registerTrace d
BuiltinFail -> registerFail d
BuiltinIntToString -> registerIntToString d
BuiltinIntPrint -> registerIntPrint d
goInductive ::
(Members '[InfoTableBuilder, Reader Pragmas, Builtins, Error ScoperError] r) =>
InductiveDef 'Scoped ->
Sem r Abstract.InductiveDef
goInductive ty@InductiveDef {..} = do
_inductiveParameters' <- concatMapM goInductiveParameters _inductiveParameters
_inductiveType' <- mapM goExpression _inductiveType
_inductivePragmas' <- goPragmas _inductivePragmas
_inductiveConstructors' <-
local (const _inductivePragmas') $
mapM goConstructorDef _inductiveConstructors
_inductiveExamples' <- goExamples _inductiveDoc
let loc = getLoc _inductiveName
indDef =
Abstract.InductiveDef
{ _inductiveParameters = _inductiveParameters',
_inductiveBuiltin = (^. withLocParam) <$> _inductiveBuiltin,
_inductiveName = goSymbol _inductiveName,
_inductiveType = fromMaybe (Abstract.ExpressionUniverse (smallUniverse loc)) _inductiveType',
_inductiveConstructors = toList _inductiveConstructors',
_inductiveExamples = _inductiveExamples',
_inductivePragmas = _inductivePragmas',
_inductivePositive = isJust (ty ^. inductivePositive)
}
whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef)
inductiveInfo <- registerInductive indDef
forM_ _inductiveConstructors' (registerConstructor inductiveInfo)
return (inductiveInfo ^. inductiveInfoDef)
goConstructorDef ::
(Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
InductiveConstructorDef 'Scoped ->
Sem r Abstract.InductiveConstructorDef
goConstructorDef InductiveConstructorDef {..} = do
ty' <- goExpression _constructorType
examples' <- goExamples _constructorDoc
pragmas' <- goPragmas _constructorPragmas
return
Abstract.InductiveConstructorDef
{ _constructorType = ty',
_constructorExamples = examples',
_constructorName = goSymbol _constructorName,
_constructorPragmas = pragmas'
}
goExpression ::
forall r.
(Members [Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
Expression ->
Sem r Abstract.Expression
goExpression = \case
ExpressionIdentifier nt -> return (goIden nt)
ExpressionParensIdentifier nt -> return (goIden nt)
ExpressionApplication a -> Abstract.ExpressionApplication <$> goApplication a
ExpressionCase a -> Abstract.ExpressionCase <$> goCase a
ExpressionInfixApplication ia -> Abstract.ExpressionApplication <$> goInfix ia
ExpressionPostfixApplication pa -> Abstract.ExpressionApplication <$> goPostfix pa
ExpressionLiteral l -> return (Abstract.ExpressionLiteral l)
ExpressionLambda l -> Abstract.ExpressionLambda <$> goLambda l
ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b))
ExpressionLet l -> Abstract.ExpressionLet <$> goLet l
ExpressionUniverse uni -> return (Abstract.ExpressionUniverse (goUniverse uni))
ExpressionFunction func -> Abstract.ExpressionFunction <$> goFunction func
ExpressionHole h -> return (Abstract.ExpressionHole h)
ExpressionIterator i -> goIterator i
where
goIden :: Concrete.ScopedIden -> Abstract.Expression
goIden x = Abstract.ExpressionIden $ case x of
ScopedAxiom a -> Abstract.IdenAxiom (Abstract.AxiomRef (goName (a ^. Concrete.axiomRefName)))
ScopedInductive i -> Abstract.IdenInductive (Abstract.InductiveRef (goName (i ^. Concrete.inductiveRefName)))
ScopedVar v -> Abstract.IdenVar (goSymbol v)
ScopedFunction fun -> Abstract.IdenFunction (Abstract.FunctionRef (goName (fun ^. Concrete.functionRefName)))
ScopedConstructor c -> Abstract.IdenConstructor (Abstract.ConstructorRef (goName (c ^. Concrete.constructorRefName)))
goLet :: Let 'Scoped -> Sem r Abstract.Let
goLet l = do
_letExpression <- goExpression (l ^. letExpression)
_letClauses <- goLetClauses (l ^. letClauses)
return Abstract.Let {..}
where
goLetClauses :: NonEmpty (LetClause 'Scoped) -> Sem r (NonEmpty Abstract.LetClause)
goLetClauses cl =
nonEmpty' <$> sequence [Abstract.LetFunDef <$> goSig sig | LetTypeSig sig <- toList cl]
where
goSig :: TypeSignature 'Scoped -> Sem r Abstract.FunctionDef
goSig sig = goLetFunctionDef sig getClauses
where
getClauses :: [FunctionClause 'Scoped]
getClauses =
[ c | LetFunClause c <- toList cl, sig ^. sigName == c ^. clauseOwnerFunction
]
goApplication :: Application -> Sem r Abstract.Application
goApplication (Application l arg) = do
l' <- goExpression l
r' <- goExpression r
return (Abstract.Application l' r' i)
where
(r, i) = case arg of
ExpressionBraces b -> (b ^. withLocParam, Implicit)
_ -> (arg, Explicit)
goPostfix :: PostfixApplication -> Sem r Abstract.Application
goPostfix (PostfixApplication l op) = do
l' <- goExpression l
let op' = goIden op
return (Abstract.Application op' l' Explicit)
goInfix :: InfixApplication -> Sem r Abstract.Application
goInfix (InfixApplication l op r) = do
l' <- goExpression l
let op' = goIden op
l'' = Abstract.ExpressionApplication (Abstract.Application op' l' Explicit)
r' <- goExpression r
return (Abstract.Application l'' r' Explicit)
goIterator :: Iterator 'Scoped -> Sem r Abstract.Expression
goIterator Iterator {..} = do
inipats' <- mapM goPatternArg inipats
rngpats' <- mapM goPatternArg rngpats
expr <- goExpression _iteratorBody
let lam =
Abstract.ExpressionLambda $
Abstract.Lambda $
Abstract.LambdaClause (nonEmpty' (inipats' ++ rngpats')) expr :| []
fn = goIden _iteratorName
inivals' <- mapM goExpression inivals
rngvals' <- mapM goExpression rngvals
return $ foldl' mkApp fn (lam : inivals' ++ rngvals')
where
inipats = map (^. initializerPattern) _iteratorInitializers
inivals = map (^. initializerExpression) _iteratorInitializers
rngpats = map (^. rangePattern) _iteratorRanges
rngvals = map (^. rangeExpression) _iteratorRanges
mkApp :: Abstract.Expression -> Abstract.Expression -> Abstract.Expression
mkApp a1 a2 = Abstract.ExpressionApplication $ Abstract.Application a1 a2 Explicit
goCase :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Case 'Scoped -> Sem r Abstract.Case
goCase c = do
_caseExpression <- goExpression (c ^. caseExpression)
_caseBranches <- mapM goBranch (c ^. caseBranches)
let _caseParens = c ^. caseParens
return Abstract.Case {..}
where
goBranch :: CaseBranch 'Scoped -> Sem r Abstract.CaseBranch
goBranch b = do
_caseBranchPattern <- goPatternArg (b ^. caseBranchPattern)
_caseBranchExpression <- goExpression (b ^. caseBranchExpression)
return Abstract.CaseBranch {..}
goLambda :: forall r. (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Lambda 'Scoped -> Sem r Abstract.Lambda
goLambda l = Abstract.Lambda <$> mapM goClause (l ^. lambdaClauses)
where
goClause :: LambdaClause 'Scoped -> Sem r Abstract.LambdaClause
goClause lc = do
ps' <- mapM goPatternArg (lc ^. lambdaParameters)
b' <- goExpression (lc ^. lambdaBody)
return (Abstract.LambdaClause ps' b')
goUniverse :: Universe -> Universe
goUniverse = id
goFunction :: (Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) => Function 'Scoped -> Sem r Abstract.Function
goFunction f = do
params <- goFunctionParameters (f ^. funParameters)
ret <- goExpression (f ^. funReturn)
return $
Abstract.Function (head params) $
foldr (\param acc -> Abstract.ExpressionFunction $ Abstract.Function param acc) ret (NonEmpty.tail params)
goFunctionParameters ::
(Members '[Error ScoperError, Reader Pragmas, InfoTableBuilder] r) =>
FunctionParameters 'Scoped ->
Sem r (NonEmpty Abstract.FunctionParameter)
goFunctionParameters FunctionParameters {..} = do
_paramType' <- goExpression _paramType
let mkParam param =
Abstract.FunctionParameter
{ Abstract._paramType = _paramType',
Abstract._paramImplicit = _paramImplicit,
Abstract._paramName = goSymbol <$> param
}
return . fromMaybe (pure (mkParam Nothing)) . nonEmpty $
mkParam . goFunctionParameter <$> _paramNames
where
goFunctionParameter :: FunctionParameter 'Scoped -> Maybe (SymbolType 'Scoped)
goFunctionParameter = \case
FunctionParameterName n -> Just n
FunctionParameterWildcard {} -> Nothing
goPatternApplication ::
(Members '[Error ScoperError, InfoTableBuilder] r) =>
PatternApp ->
Sem r Abstract.ConstructorApp
goPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternApplication a)
goPatternConstructor ::
(Members '[Error ScoperError, InfoTableBuilder] r) =>
ConstructorRef ->
Sem r Abstract.ConstructorApp
goPatternConstructor a = uncurry Abstract.ConstructorApp <$> viewApp (PatternConstructor a)
goInfixPatternApplication ::
(Members '[Error ScoperError, InfoTableBuilder] r) =>
PatternInfixApp ->
Sem r Abstract.ConstructorApp
goInfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternInfixApplication a)
goPostfixPatternApplication ::
(Members '[Error ScoperError, InfoTableBuilder] r) =>
PatternPostfixApp ->
Sem r Abstract.ConstructorApp
goPostfixPatternApplication a = uncurry Abstract.ConstructorApp <$> viewApp (PatternPostfixApplication a)
viewApp :: forall r. (Members '[Error ScoperError, InfoTableBuilder] r) => Pattern -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
viewApp p = case p of
PatternConstructor c -> return (goConstructorRef c, [])
PatternApplication app@(PatternApp _ r) -> do
r' <- goPatternArg r
second (`snoc` r') <$> viewAppLeft app
PatternInfixApplication (PatternInfixApp l c r) -> do
l' <- goPatternArg l
r' <- goPatternArg r
return (goConstructorRef c, [l', r'])
PatternPostfixApplication (PatternPostfixApp l c) -> do
l' <- goPatternArg l
return (goConstructorRef c, [l'])
PatternVariable {} -> err
PatternWildcard {} -> err
PatternEmpty {} -> err
where
viewAppLeft :: PatternApp -> Sem r (Abstract.ConstructorRef, [Abstract.PatternArg])
viewAppLeft app@(PatternApp l _)
| Implicit <- l ^. patternArgIsImplicit = throw (ErrImplicitPatternLeftApplication (ImplicitPatternLeftApplication app))
| otherwise = viewApp (l ^. patternArgPattern)
err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p))
goConstructorRef :: ConstructorRef -> Abstract.ConstructorRef
goConstructorRef (ConstructorRef' n) = Abstract.ConstructorRef (goName n)
goPatternArg :: (Members '[Error ScoperError, InfoTableBuilder] r) => PatternArg -> Sem r Abstract.PatternArg
goPatternArg p = do
pat' <- goPattern (p ^. patternArgPattern)
return
Abstract.PatternArg
{ _patternArgIsImplicit = p ^. patternArgIsImplicit,
_patternArgName = goSymbol <$> p ^. patternArgName,
_patternArgPattern = pat'
}
goPattern :: (Members '[Error ScoperError, InfoTableBuilder] r) => Pattern -> Sem r Abstract.Pattern
goPattern p = case p of
PatternVariable a -> return $ Abstract.PatternVariable (goSymbol a)
PatternConstructor c -> Abstract.PatternConstructorApp <$> goPatternConstructor c
PatternApplication a -> Abstract.PatternConstructorApp <$> goPatternApplication a
PatternInfixApplication a -> Abstract.PatternConstructorApp <$> goInfixPatternApplication a
PatternPostfixApplication a -> Abstract.PatternConstructorApp <$> goPostfixPatternApplication a
PatternWildcard i -> return (Abstract.PatternWildcard i)
PatternEmpty {} -> return Abstract.PatternEmpty
goAxiom :: (Members '[InfoTableBuilder, Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Abstract.AxiomDef
goAxiom a = do
_axiomType' <- goExpression (a ^. axiomType)
_axiomPragmas' <- goPragmas (a ^. axiomPragmas)
let axiom =
Abstract.AxiomDef
{ _axiomType = _axiomType',
_axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin,
_axiomName = goSymbol (a ^. axiomName),
_axiomPragmas = _axiomPragmas'
}
whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom . (^. withLocParam))
registerAxiom' axiom

View File

@ -1,31 +0,0 @@
module Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context
( module Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context,
module Juvix.Compiler.Abstract.Data.InfoTable,
)
where
import Juvix.Compiler.Abstract.Data.InfoTable
import Juvix.Compiler.Abstract.Language
import Juvix.Compiler.Abstract.Language qualified as Abstract
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Concrete
import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as Concrete
import Juvix.Compiler.Pipeline.EntryPoint qualified as E
import Juvix.Prelude
newtype ModulesCache = ModulesCache
{_cachedModules :: HashMap S.NameId Abstract.TopModule}
data AbstractResult = AbstractResult
{ _resultScoper :: Concrete.ScoperResult,
_resultTable :: InfoTable,
_resultModules :: NonEmpty TopModule,
_resultExports :: HashSet NameId,
_resultModulesCache :: ModulesCache
}
makeLenses ''AbstractResult
makeLenses ''ModulesCache
abstractResultEntryPoint :: Lens' AbstractResult E.EntryPoint
abstractResultEntryPoint = resultScoper . Concrete.resultParserResult . Concrete.resultEntry

View File

@ -8,12 +8,12 @@ import Data.Foldable
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Data.Text qualified as Text
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Asm.Data.InfoTable
import Juvix.Compiler.Asm.Interpreter.Base
import Juvix.Compiler.Asm.Interpreter.RuntimeState
import Juvix.Compiler.Asm.Pretty.Options
import Juvix.Compiler.Core.Pretty.Base qualified as Core
import Juvix.Compiler.Internal.Data.Name
import Juvix.Data.CodeAnn
import Juvix.Extra.Strings qualified as Str

View File

@ -9,7 +9,6 @@ import Data.ByteString.Builder qualified as Builder
import Data.HashMap.Strict qualified as HashMap
import Data.Time.Clock
import Data.Versions (prettySemVer)
import Juvix.Compiler.Abstract.Translation.FromConcrete qualified as Abstract
import Juvix.Compiler.Backend.Html.Data
import Juvix.Compiler.Backend.Html.Extra
import Juvix.Compiler.Backend.Html.Translation.FromTyped.Source hiding (go)
@ -18,7 +17,7 @@ import Juvix.Compiler.Concrete.Extra
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Print
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoped
import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Context qualified as InternalArity
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
@ -162,8 +161,7 @@ genJudocHtml JudocArgs {..} =
_judocArgsCtx
^. resultInternalArityResult
. InternalArity.resultInternalResult
. Internal.resultAbstract
. Abstract.resultScoper
. Internal.resultScoper
. Scoped.comments
entry :: EntryPoint
@ -177,8 +175,7 @@ genJudocHtml JudocArgs {..} =
_judocArgsCtx
^. InternalTyped.resultInternalArityResult
. InternalArity.resultInternalResult
. Internal.resultAbstract
. Abstract.resultScoper
. Internal.resultScoper
. Scoped.mainModule
htmlOpts :: HtmlOptions

View File

@ -1,8 +1,8 @@
module Juvix.Compiler.Builtins.Bool where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Abstract.Pretty
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty
import Juvix.Prelude
registerBoolDef :: (Member Builtins r) => InductiveDef -> Sem r ()
@ -16,16 +16,16 @@ registerBoolDef d = do
registerTrue :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
registerTrue d@InductiveConstructorDef {..} = do
let ctorTrue = _constructorName
ctorTy = _constructorType
let ctorTrue = _inductiveConstructorName
ctorTy = _inductiveConstructorType
boolTy <- getBuiltinName (getLoc d) BuiltinBool
unless (ctorTy === boolTy) (error $ "true has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
registerBuiltin BuiltinBoolTrue ctorTrue
registerFalse :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
registerFalse d@InductiveConstructorDef {..} = do
let ctorFalse = _constructorName
ctorTy = _constructorType
let ctorFalse = _inductiveConstructorName
ctorTy = _inductiveConstructorType
boolTy <- getBuiltinName (getLoc d) BuiltinBool
unless (ctorTy === boolTy) (error $ "false has the wrong type " <> ppTrace ctorTy <> " | " <> ppTrace boolTy)
registerBuiltin BuiltinBoolFalse ctorFalse
@ -37,9 +37,10 @@ registerIf f = do
false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
let if_ = f ^. funDefName
u = ExpressionUniverse smallUniverseNoLoc
vart <- freshVar "t"
vare <- freshVar "e"
hole <- freshHole
l = getLoc f
vart <- freshVar l "t"
vare <- freshVar l "e"
hole <- freshHole l
let e = toExpression vare
exClauses :: [(Expression, Expression)]
exClauses =
@ -62,8 +63,9 @@ registerOr f = do
true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
let or_ = f ^. funDefName
vare <- freshVar "e"
hole <- freshHole
l = getLoc f
vare <- freshVar l "e"
hole <- freshHole l
let e = toExpression vare
exClauses :: [(Expression, Expression)]
exClauses =
@ -86,8 +88,9 @@ registerAnd f = do
true_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
false_ <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
let and_ = f ^. funDefName
vare <- freshVar "e"
hole <- freshHole
l = getLoc f
vare <- freshVar l "e"
hole <- freshHole l
let e = toExpression vare
exClauses :: [(Expression, Expression)]
exClauses =

View File

@ -1,17 +1,18 @@
module Juvix.Compiler.Builtins.Control where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
registerSeq :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
registerSeq f = do
let u = ExpressionUniverse smallUniverseNoLoc
a <- freshVar "a"
b <- freshVar "b"
l = getLoc f
a <- freshVar l "a"
b <- freshVar l "b"
let seq = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
varn <- freshVar l "n"
varm <- freshVar l "m"
let n = toExpression varn
m = toExpression varm
exClauses :: [(Expression, Expression)]

View File

@ -1,26 +1,28 @@
module Juvix.Compiler.Builtins.Debug where
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
registerTrace :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
registerTrace :: Members '[Builtins, NameIdGen] r => AxiomDef -> Sem r ()
registerTrace f = do
let ftype = f ^. axiomType
u = ExpressionUniverse smallUniverseNoLoc
a <- freshVar "a"
l = getLoc f
a <- freshVar l "a"
let freeVars = HashSet.fromList [a]
unless
((ftype ==% (u <>--> a --> a)) freeVars)
(error "trace must be of type {A : Type} -> A -> A")
registerBuiltin BuiltinTrace (f ^. axiomName)
registerFail :: (Members '[Builtins, NameIdGen] r) => AxiomDef -> Sem r ()
registerFail :: Members '[Builtins, NameIdGen] r => AxiomDef -> Sem r ()
registerFail f = do
let ftype = f ^. axiomType
u = ExpressionUniverse smallUniverseNoLoc
a <- freshVar "a"
l = getLoc f
a <- freshVar l "a"
let freeVars = HashSet.fromList [a]
string_ <- getBuiltinName (getLoc f) BuiltinString
unless

View File

@ -4,9 +4,9 @@ module Juvix.Compiler.Builtins.Effect
where
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Abstract.Pretty
import Juvix.Compiler.Builtins.Error
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty
import Juvix.Prelude
data Builtins m a where
@ -87,7 +87,7 @@ registerFun ::
Sem r ()
registerFun fi = do
let op = fi ^. funInfoDef . funDefName
ty = fi ^. funInfoDef . funDefTypeSig
ty = fi ^. funInfoDef . funDefType
sig = fi ^. funInfoSignature
unless ((sig ==% ty) (HashSet.fromList (fi ^. funInfoFreeTypeVars))) (error "builtin has the wrong type signature")
registerBuiltin (fi ^. funInfoBuiltin) op
@ -101,5 +101,15 @@ registerFun fi = do
case zipExactMay (fi ^. funInfoClauses) clauses of
Nothing -> error "builtin has the wrong number of clauses"
Just z -> forM_ z $ \((exLhs, exBody), (lhs, body)) -> do
unless (exLhs =% lhs) (error "clause lhs does not match")
unless
(exLhs =% lhs)
( error
( "clause lhs does not match for "
<> ppTrace op
<> "\nExpected: "
<> ppTrace exLhs
<> "\nActual: "
<> ppTrace lhs
)
)
unless (exBody =% body) (error $ "clause body does not match " <> ppTrace exBody <> " | " <> ppTrace body)

View File

@ -1,7 +1,7 @@
module Juvix.Compiler.Builtins.IO where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
registerIO :: (Member Builtins r) => AxiomDef -> Sem r ()

View File

@ -1,7 +1,7 @@
module Juvix.Compiler.Builtins.Int where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
registerIntDef :: Member Builtins r => InductiveDef -> Sem r ()
@ -15,8 +15,8 @@ registerIntDef d = do
registerIntCtor :: (Member Builtins r) => BuiltinConstructor -> InductiveConstructorDef -> Sem r ()
registerIntCtor ctor d@InductiveConstructorDef {..} = do
let ctorName = _constructorName
ty = _constructorType
let ctorName = _inductiveConstructorName
ty = _inductiveConstructorType
loc = getLoc d
int <- getBuiltinName loc BuiltinInt
nat <- getBuiltinName loc BuiltinNat
@ -38,10 +38,11 @@ registerIntEq f = do
tybool <- builtinName BuiltinBool
false <- toExpression <$> builtinName BuiltinBoolFalse
natEq <- toExpression <$> builtinName BuiltinNatEq
varm <- freshVar "m"
varn <- freshVar "n"
h1 <- freshHole
h2 <- freshHole
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
h1 <- freshHole l
h2 <- freshHole l
let eq = f ^. funDefName
m = toExpression varm
n = toExpression varn
@ -71,7 +72,7 @@ registerIntSubNat f = do
let loc = getLoc f
int <- getBuiltinName loc BuiltinInt
nat <- getBuiltinName loc BuiltinNat
unless (f ^. funDefTypeSig === (nat --> nat --> int)) (error "int-sub-nat has the wrong type signature")
unless (f ^. funDefType === (nat --> nat --> int)) (error "int-sub-nat has the wrong type signature")
registerBuiltin BuiltinIntSubNat (f ^. funDefName)
registerIntPlus :: forall r. Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
@ -84,8 +85,9 @@ registerIntPlus f = do
natPlus <- toExpression <$> getBuiltinName loc BuiltinNatPlus
intSubNat <- toExpression <$> getBuiltinName loc BuiltinIntSubNat
let plus = f ^. funDefName
varn <- freshVar "m"
varm <- freshVar "n"
l = getLoc f
varn <- freshVar l "m"
varm <- freshVar l "n"
let m = toExpression varm
n = toExpression varn
(.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -115,7 +117,8 @@ registerIntNegNat f = do
negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
zero <- toExpression <$> builtinName BuiltinNatZero
suc <- toExpression <$> builtinName BuiltinNatSuc
varn <- freshVar "n"
let l = getLoc f
varn <- freshVar l "n"
let negNat = f ^. funDefName
n = toExpression varn
exClauses :: [(Expression, Expression)]
@ -143,7 +146,8 @@ registerIntNeg f = do
negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
negNat <- toExpression <$> builtinName BuiltinIntNegNat
suc <- toExpression <$> builtinName BuiltinNatSuc
varn <- freshVar "n"
let l = getLoc f
varn <- freshVar l "n"
let neg = f ^. funDefName
n = toExpression varn
exClauses :: [(Expression, Expression)]
@ -172,8 +176,9 @@ registerIntMul f = do
negNat <- toExpression <$> builtinName BuiltinIntNegNat
natMul <- toExpression <$> builtinName BuiltinNatMul
natSuc <- toExpression <$> builtinName BuiltinNatSuc
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let mul = f ^. funDefName
m = toExpression varm
n = toExpression varn
@ -205,8 +210,9 @@ registerIntDiv f = do
negNat <- toExpression <$> builtinName BuiltinIntNegNat
natDiv <- toExpression <$> builtinName BuiltinNatDiv
natSuc <- toExpression <$> builtinName BuiltinNatSuc
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let intDiv = f ^. funDefName
m = toExpression varm
n = toExpression varn
@ -238,8 +244,9 @@ registerIntMod f = do
negNat <- toExpression <$> builtinName BuiltinIntNegNat
natMod <- toExpression <$> builtinName BuiltinNatMod
natSuc <- toExpression <$> builtinName BuiltinNatSuc
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let intMod = f ^. funDefName
m = toExpression varm
n = toExpression varn
@ -268,8 +275,9 @@ registerIntSub f = do
int <- builtinName BuiltinInt
neg <- toExpression <$> builtinName BuiltinIntNeg
intPlus <- toExpression <$> builtinName BuiltinIntPlus
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let intSub = f ^. funDefName
m = toExpression varm
n = toExpression varn
@ -298,8 +306,9 @@ registerIntNonNeg f = do
negSuc <- toExpression <$> builtinName BuiltinIntNegSuc
true <- toExpression <$> builtinName BuiltinBoolTrue
false <- toExpression <$> builtinName BuiltinBoolFalse
varn <- freshVar "n"
h <- freshHole
let l = getLoc l
varn <- freshVar l "n"
h <- freshHole l
let intNonNeg = f ^. funDefName
n = toExpression varn
@ -334,8 +343,9 @@ registerIntLe f = do
bool_ <- builtinName BuiltinBool
nonNeg <- toExpression <$> builtinName BuiltinIntNonNeg
intSub <- toExpression <$> builtinName BuiltinIntSub
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let intLe = f ^. funDefName
(.-.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
x .-. y = intSub @@ x @@ y
@ -363,8 +373,9 @@ registerIntLt f = do
bool_ <- builtinName BuiltinBool
intLe <- toExpression <$> builtinName BuiltinIntLe
intPlus <- toExpression <$> builtinName BuiltinIntPlus
varm <- freshVar "m"
varn <- freshVar "n"
let l = getLoc f
varm <- freshVar l "m"
varn <- freshVar l "n"
let intLt = f ^. funDefName
(.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
x .+. y = intPlus @@ x @@ y

View File

@ -1,8 +1,8 @@
module Juvix.Compiler.Builtins.Nat where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Abstract.Pretty
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty
import Juvix.Data.Effect.NameIdGen
import Juvix.Prelude
@ -17,16 +17,16 @@ registerNatDef d = do
registerZero :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
registerZero d@InductiveConstructorDef {..} = do
let zero = _constructorName
ty = _constructorType
let zero = _inductiveConstructorName
ty = _inductiveConstructorType
nat <- getBuiltinName (getLoc d) BuiltinNat
unless (ty === nat) (error $ "zero has the wrong type " <> ppTrace ty <> " | " <> ppTrace nat)
registerBuiltin BuiltinNatZero zero
registerSuc :: (Member Builtins r) => InductiveConstructorDef -> Sem r ()
registerSuc d@InductiveConstructorDef {..} = do
let suc = _constructorName
ty = _constructorType
let suc = _inductiveConstructorName
ty = _inductiveConstructorType
nat <- getBuiltinName (getLoc d) BuiltinNat
unless (ty === (nat --> nat)) (error "suc has the wrong type")
registerBuiltin BuiltinNatSuc suc
@ -44,8 +44,9 @@ registerNatPlus f = do
zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
let plus = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
let n = toExpression varn
m = toExpression varm
(.+.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -72,9 +73,10 @@ registerNatMul f = do
suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
plus <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatPlus
let mul = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
h <- freshHole
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
h <- freshHole l
let n = toExpression varn
m = toExpression varm
(.*.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -100,9 +102,10 @@ registerNatSub f = do
zero <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatZero
suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
let sub = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
h <- freshHole
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
h <- freshHole l
let n = toExpression varn
m = toExpression varm
(.-.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -130,9 +133,10 @@ registerNatUDiv f = do
suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub
let divop = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
h <- freshHole
l = getLoc l
varn <- freshVar l "n"
varm <- freshVar l "m"
h <- freshHole l
let n = toExpression varn
m = toExpression varm
(./.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -152,15 +156,16 @@ registerNatUDiv f = do
_funInfoFreeTypeVars = []
}
registerNatDiv :: (Members '[Builtins, NameIdGen] r) => FunctionDef -> Sem r ()
registerNatDiv :: Members '[Builtins, NameIdGen] r => FunctionDef -> Sem r ()
registerNatDiv f = do
nat <- getBuiltinName (getLoc f) BuiltinNat
suc <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSuc
udiv <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatUDiv
sub <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatSub
let divop = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
let n = toExpression varn
m = toExpression varm
(./.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -186,8 +191,9 @@ registerNatMod f = do
divop <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatDiv
mul <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatMul
let modop = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
let n = toExpression varn
m = toExpression varm
exClauses =
@ -212,9 +218,10 @@ registerNatLe f = do
true <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
false <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
let le = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
h <- freshHole
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
h <- freshHole l
let n = toExpression varn
m = toExpression varm
(.<=.) :: (IsExpression a, IsExpression b) => a -> b -> Expression
@ -242,8 +249,9 @@ registerNatLt f = do
le <- toExpression <$> getBuiltinName (getLoc f) BuiltinNatLe
tybool <- getBuiltinName (getLoc f) BuiltinBool
let lt = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
let n = toExpression varn
m = toExpression varm
exClauses :: [(Expression, Expression)]
@ -269,9 +277,10 @@ registerNatEq f = do
true <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolTrue
false <- toExpression <$> getBuiltinName (getLoc f) BuiltinBoolFalse
let eq = f ^. funDefName
varn <- freshVar "n"
varm <- freshVar "m"
h <- freshHole
l = getLoc f
varn <- freshVar l "n"
varm <- freshVar l "m"
h <- freshHole l
let n = toExpression varn
m = toExpression varm
(.==.) :: (IsExpression a, IsExpression b) => a -> b -> Expression

View File

@ -1,7 +1,7 @@
module Juvix.Compiler.Builtins.String where
import Juvix.Compiler.Abstract.Extra
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
registerString :: (Member Builtins r) => AxiomDef -> Sem r ()

View File

@ -5,6 +5,7 @@ module Juvix.Compiler.Concrete.Extra
getModuleFilePath,
unfoldApplication,
groupStatements,
flattenStatement,
)
where
@ -128,3 +129,8 @@ groupStatements = \case
_inductiveName
^. S.nameConcrete
: map (^. constructorName . S.nameConcrete) constructors
flattenStatement :: Statement s -> [Statement s]
flattenStatement = \case
StatementModule m -> concatMap flattenStatement (m ^. moduleBody)
s -> [s]

View File

@ -1202,6 +1202,10 @@ deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (JudocA
deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (JudocAtom s)
newtype ModuleIndex = ModuleIndex
{ _moduleIxModule :: Module 'Scoped 'ModuleTop
}
makeLenses ''PatternArg
makeLenses ''UsingItem
makeLenses ''HidingItem
@ -1243,6 +1247,13 @@ makeLenses ''ExpressionAtoms
makeLenses ''Iterator
makeLenses ''Initializer
makeLenses ''Range
makeLenses ''ModuleIndex
instance Eq ModuleIndex where
(==) = (==) `on` (^. moduleIxModule . modulePath)
instance Hashable ModuleIndex where
hashWithSalt s = hashWithSalt s . (^. moduleIxModule . modulePath)
instance HasAtomicity Expression where
atomicity e = case e of

View File

@ -10,6 +10,7 @@ import Juvix.Compiler.Concrete.Data.Scope
import Juvix.Compiler.Concrete.Data.ScopedName qualified as Scoped
import Juvix.Compiler.Concrete.Language
import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as Parsed
import Juvix.Compiler.Pipeline.EntryPoint (EntryPoint)
import Juvix.Prelude
data ScoperResult = ScoperResult
@ -26,6 +27,9 @@ makeLenses ''ScoperResult
mainModule :: Lens' ScoperResult (Module 'Scoped 'ModuleTop)
mainModule = resultModules . _head1
entryPoint :: Lens' ScoperResult EntryPoint
entryPoint = resultParserResult . Parsed.resultEntry
mainModuleSope :: ScoperResult -> Scope
mainModuleSope r =
r

View File

@ -7,7 +7,6 @@ where
import Data.HashMap.Strict qualified as HashMap
import Data.Map.Strict qualified as Map
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Data.BinderList qualified as BL
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
@ -18,6 +17,7 @@ import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Language.Stripped qualified as Stripped
import Juvix.Compiler.Core.Language.Value
import Juvix.Compiler.Core.Pretty.Options
import Juvix.Compiler.Internal.Data.Name
import Juvix.Data.CodeAnn
import Juvix.Extra.Strings qualified as Str
@ -440,11 +440,28 @@ instance PrettyCode ConstructorInfo where
instance PrettyCode InfoTable where
ppCode :: forall r. (Member (Reader Options) r) => InfoTable -> Sem r (Doc Ann)
ppCode tbl = do
let header x = annotate AnnImportant ("--" <+> x) <> line
tys <- ppInductives (toList (tbl ^. infoInductives))
sigs <- ppSigs (sortOn (^. identifierSymbol) $ toList (tbl ^. infoIdentifiers))
ctx' <- ppContext (tbl ^. identContext)
axioms <- vsep <$> mapM ppCode (tbl ^. infoAxioms)
main <- maybe (return "") (\s -> (<> line) . (line <>) <$> ppName KNameFunction (identName tbl s)) (tbl ^. infoMain)
return (tys <> line <> line <> sigs <> line <> ctx' <> line <> main)
return
( header "Inductives:"
<> tys
<> line
<> header "Identifiers:"
<> sigs
<> line
<> header "Axioms:"
<> axioms
<> line
<> header "Context:"
<> ctx'
<> line
<> header "Main:"
<> main
)
where
ppSig :: Symbol -> Sem r (Maybe (Doc Ann))
ppSig s = do
@ -466,7 +483,7 @@ instance PrettyCode InfoTable where
let tydoc
| isDynamic ty = mempty
| otherwise = space <> colon <+> ty'
blt = if isJust (ii ^. identifierBuiltin) then (Str.builtin <+> mempty) else mempty
blt = if isJust (ii ^. identifierBuiltin) then (kwBuiltin <+> mempty) else mempty
return (Just (blt <> kwDef <+> sym' <> argsNum <> tydoc))
ppSigs :: [IdentifierInfo] -> Sem r (Doc Ann)
@ -500,6 +517,12 @@ instance PrettyCode InfoTable where
ctrs <- mapM (fmap (<> semi) . ppCode . lookupConstructorInfo tbl) (ii ^. inductiveConstructors)
return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line) <> kwSemicolon)
instance PrettyCode AxiomInfo where
ppCode ii = do
name <- ppName KNameAxiom (ii ^. axiomName)
ty <- ppCode (ii ^. axiomType)
return (kwAxiom <+> name <+> kwColon <+> ty <> kwSemicolon)
instance PrettyCode Stripped.ArgumentInfo where
ppCode :: (Member (Reader Options) r) => Stripped.ArgumentInfo -> Sem r (Doc Ann)
ppCode Stripped.ArgumentInfo {..} = do

View File

@ -21,7 +21,7 @@ defaultOptions =
traceOptions :: Options
traceOptions =
Options
{ _optShowIdentIds = False,
{ _optShowIdentIds = True,
_optShowDeBruijnIndices = True,
_optShowArgsNum = True
}

View File

@ -2,7 +2,6 @@ module Juvix.Compiler.Core.Translation.FromInternal where
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Data
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info qualified as Info
@ -10,16 +9,21 @@ import Juvix.Compiler.Core.Info.LocationInfo
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Info.PragmaInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Pretty qualified as Core
import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Int
import Juvix.Compiler.Core.Translation.FromInternal.Builtins.Nat
import Juvix.Compiler.Core.Translation.FromInternal.Data
import Juvix.Compiler.Internal.Data.Name
import Juvix.Compiler.Internal.Extra qualified as Internal
import Juvix.Compiler.Internal.Pretty qualified as Internal
import Juvix.Compiler.Internal.Translation.Extra qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking qualified as InternalTyped
import Juvix.Data.Loc qualified as Loc
import Juvix.Data.PPOutput
import Juvix.Extra.Strings qualified as Str
type MVisit = Visit Internal.ModuleIndex
data PreInductiveDef = PreInductiveDef
{ _preInductiveInternal :: Internal.InductiveDef,
_preInductiveInfo :: InductiveInfo
@ -47,7 +51,11 @@ mkIdentIndex = show . (^. Internal.nameId . Internal.unNameId)
fromInternal :: Internal.InternalTypedResult -> Sem k CoreResult
fromInternal i = do
(res, _) <- runInfoTableBuilder emptyInfoTable (evalState (i ^. InternalTyped.resultFunctions) (runReader (i ^. InternalTyped.resultIdenTypes) f))
res <-
execInfoTableBuilder emptyInfoTable
. evalState (i ^. InternalTyped.resultFunctions)
. runReader (i ^. InternalTyped.resultIdenTypes)
$ f
return $
CoreResult
{ _coreResultTable = res,
@ -59,7 +67,9 @@ fromInternal i = do
reserveLiteralIntToNatSymbol
reserveLiteralIntToIntSymbol
let resultModules = toList (i ^. InternalTyped.resultModules)
runReader (Internal.buildTable resultModules) (mapM_ goModule resultModules)
runReader (Internal.buildTable resultModules)
. evalVisitEmpty goModuleNoVisit
$ mapM_ goModule resultModules
tab <- getInfoTable
when
(isNothing (lookupBuiltinInductive tab BuiltinBool))
@ -70,32 +80,35 @@ fromInternal i = do
fromInternalExpression :: CoreResult -> Internal.Expression -> Sem r Node
fromInternalExpression res exp = do
let modules = res ^. coreResultInternalTypedResult . InternalTyped.resultModules
snd
<$> runReader
(Internal.buildTable modules)
( runInfoTableBuilder
(res ^. coreResultTable)
( evalState
(res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
( runReader
(res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
(fromTopIndex (goExpression exp))
)
)
)
fmap snd
. runReader (Internal.buildTable modules)
. runInfoTableBuilder (res ^. coreResultTable)
. evalState (res ^. coreResultInternalTypedResult . InternalTyped.resultFunctions)
. runReader (res ^. coreResultInternalTypedResult . InternalTyped.resultIdenTypes)
$ fromTopIndex (goExpression exp)
goModule ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable] r) =>
Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, MVisit] r =>
Internal.Module ->
Sem r ()
goModule m = mapM_ go (m ^. Internal.moduleBody . Internal.moduleStatements)
goModule = visit . Internal.ModuleIndex
goModuleNoVisit ::
forall r.
Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, MVisit] r =>
Internal.ModuleIndex ->
Sem r ()
goModuleNoVisit (Internal.ModuleIndex m) = do
mapM_ goImport (m ^. Internal.moduleBody . Internal.moduleImports)
mapM_ go (m ^. Internal.moduleBody . Internal.moduleStatements)
where
go :: Internal.Statement -> Sem r ()
go = \case
Internal.StatementAxiom a -> goAxiomInductive a >> goAxiomDef a
Internal.StatementMutual f -> goMutualBlock f
Internal.StatementInclude i -> mapM_ go (i ^. Internal.includeModule . Internal.moduleBody . Internal.moduleStatements)
goImport :: Internal.Import -> Sem r ()
goImport (Internal.Import i) = visit i
-- | predefine an inductive definition
preInductiveDef ::
@ -112,7 +125,7 @@ preInductiveDef i = do
ParameterInfo
{ _paramName = p ^. Internal.inductiveParamName . nameText,
_paramLocation = Just $ p ^. Internal.inductiveParamName . nameLoc,
_paramIsImplicit = False, -- TODO: not currently easily available in Internal
_paramIsImplicit = False,
_paramKind = mkSmallUniv
}
)
@ -816,17 +829,23 @@ addPatternVariableNames p lvl vars =
Internal.PatternVariable n -> [Just n]
Internal.PatternConstructorApp {} -> impossible
goExpression ::
goIden ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Expression ->
Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r =>
Internal.Iden ->
Sem r Node
goExpression = \case
Internal.ExpressionLet l -> goLet l
Internal.ExpressionLiteral l -> do
tab <- getInfoTable
return (goLiteral (fromJust $ tab ^. infoLiteralIntToNat) (fromJust $ tab ^. infoLiteralIntToInt) l)
Internal.ExpressionIden i -> case i of
goIden i = do
infoTableDebug <- Core.ppTrace <$> getInfoTable
let undeclared =
error
( "internal to core: undeclared identifier: "
<> txt
<> "\nat "
<> Internal.ppTrace (getLoc i)
<> "\n"
<> infoTableDebug
)
case i of
Internal.IdenVar n -> do
k <- HashMap.lookupDefault impossible id_ <$> asks (^. indexTableVars)
varsNum <- asks (^. indexTableVarsNum)
@ -847,7 +866,7 @@ goExpression = \case
return $ case m of
Just (IdentFun sym) -> mkIdent (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) sym
Just _ -> error ("internal to core: not a function: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Nothing -> undeclared
Just k -> do
varsNum <- asks (^. indexTableVarsNum)
return (mkVar (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. nameText)))) (varsNum - k - 1))
@ -856,13 +875,13 @@ goExpression = \case
return $ case m of
Just (IdentInd sym) -> mkTypeConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) sym []
Just _ -> error ("internal to core: not an inductive: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Nothing -> undeclared
Internal.IdenConstructor n -> do
m <- getIdent identIndex
case m of
Just (IdentConstr tag) -> return (mkConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) tag [])
return $ case m of
Just (IdentConstr tag) -> (mkConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) tag [])
Just _ -> error ("internal to core: not a constructor " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
Nothing -> undeclared
Internal.IdenAxiom n -> do
axiomInfoBuiltin <- Internal.getAxiomBuiltinInfo n
case axiomInfoBuiltin of
@ -874,16 +893,28 @@ goExpression = \case
Just (IdentFun sym) -> mkIdent (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) sym
Just (IdentInd sym) -> mkTypeConstr (setInfoLocation (n ^. nameLoc) (Info.singleton (NameInfo (n ^. namePretty)))) sym []
Just _ -> error ("internal to core: not an axiom: " <> txt)
Nothing -> error ("internal to core: undeclared identifier: " <> txt)
where
identIndex :: Text
identIndex = mkIdentIndex (Internal.getName i)
Nothing -> undeclared
where
identIndex :: Text
identIndex = mkIdentIndex (Internal.getName i)
id_ :: NameId
id_ = Internal.getName i ^. nameId
id_ :: NameId
id_ = Internal.getName i ^. nameId
txt :: Text
txt = Internal.getName i ^. Internal.nameText
txt :: Text
txt = Internal.ppTrace (Internal.getName i)
goExpression ::
forall r.
(Members '[InfoTableBuilder, Reader InternalTyped.TypesTable, State InternalTyped.FunctionsTable, Reader Internal.InfoTable, Reader IndexTable] r) =>
Internal.Expression ->
Sem r Node
goExpression = \case
Internal.ExpressionLet l -> goLet l
Internal.ExpressionLiteral l -> do
tab <- getInfoTable
return (goLiteral (fromJust $ tab ^. infoLiteralIntToNat) (fromJust $ tab ^. infoLiteralIntToInt) l)
Internal.ExpressionIden i -> goIden i
Internal.ExpressionApplication a -> goApplication a
Internal.ExpressionSimpleLambda l -> goSimpleLambda l
Internal.ExpressionLambda l -> goLambda l

View File

@ -1,8 +1,8 @@
module Juvix.Compiler.Core.Translation.FromInternal.Data.IndexTable where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Internal.Data.Name
data IndexTable = IndexTable
{ _indexTableVarsNum :: Index,

View File

@ -1,8 +1,12 @@
module Juvix.Compiler.Internal.Data
( module Juvix.Compiler.Internal.Data.InfoTable,
module Juvix.Compiler.Internal.Data.LocalVars,
module Juvix.Compiler.Internal.Data.Name,
module Juvix.Compiler.Internal.Data.NameDependencyInfo,
)
where
import Juvix.Compiler.Internal.Data.InfoTable
import Juvix.Compiler.Internal.Data.LocalVars
import Juvix.Compiler.Internal.Data.Name
import Juvix.Compiler.Internal.Data.NameDependencyInfo

View File

@ -1,68 +1,44 @@
module Juvix.Compiler.Internal.Data.InfoTable where
module Juvix.Compiler.Internal.Data.InfoTable
( module Juvix.Compiler.Internal.Data.InfoTable.Base,
buildTable,
buildTable1,
extendWithReplExpression,
lookupConstructor,
lookupConstructorArgTypes,
lookupFunction,
constructorReturnType,
constructorArgTypes,
lookupInductive,
lookupAxiom,
lookupInductiveType,
constructorType,
getAxiomBuiltinInfo,
getFunctionBuiltinInfo,
buildTableShallow,
)
where
import Data.Generics.Uniplate.Data
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Data.InfoTable.Base
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty (ppTrace)
import Juvix.Prelude
data ConstructorInfo = ConstructorInfo
{ _constructorInfoInductiveParameters :: [InductiveParameter],
_constructorInfoArgs :: [Expression],
_constructorInfoInductive :: InductiveName,
_constructorInfoBuiltin :: Maybe BuiltinConstructor
}
type MCache = Cache ModuleIndex InfoTable
newtype FunctionInfo = FunctionInfo
{ _functionInfoDef :: FunctionDef
}
newtype AxiomInfo = AxiomInfo
{ _axiomInfoDef :: AxiomDef
}
newtype InductiveInfo = InductiveInfo
{ _inductiveInfoDef :: InductiveDef
}
data InfoTable = InfoTable
{ _infoConstructors :: HashMap Name ConstructorInfo,
_infoAxioms :: HashMap Name AxiomInfo,
_infoFunctions :: HashMap Name FunctionInfo,
_infoInductives :: HashMap Name InductiveInfo
}
makeLenses ''InfoTable
makeLenses ''FunctionInfo
makeLenses ''ConstructorInfo
makeLenses ''AxiomInfo
makeLenses ''InductiveInfo
instance Semigroup InfoTable where
a <> b =
InfoTable
{ _infoConstructors = a ^. infoConstructors <> b ^. infoConstructors,
_infoAxioms = a ^. infoAxioms <> b ^. infoAxioms,
_infoFunctions = a ^. infoFunctions <> b ^. infoFunctions,
_infoInductives = a ^. infoInductives <> b ^. infoInductives
}
instance Monoid InfoTable where
mempty =
InfoTable
{ _infoConstructors = mempty,
_infoAxioms = mempty,
_infoFunctions = mempty,
_infoInductives = mempty
}
buildTable :: (Foldable f) => f Module -> InfoTable
buildTable = mconcatMap buildTable1
buildTable :: Foldable f => f Module -> InfoTable
buildTable = run . evalCache computeTable mempty . getMany
buildTable1 :: Module -> InfoTable
buildTable1 = run . evalState (mempty :: Cache) . buildTable1'
buildTable1 = buildTable . pure @[]
buildTable' :: (Members '[State Cache] r, Foldable f) => f Module -> Sem r InfoTable
buildTable' = mconcatMap buildTable1'
-- TODO do not recurse into imports
buildTableShallow :: Module -> InfoTable
buildTableShallow = buildTable . pure @[]
getMany :: (Members '[MCache] r, Foldable f) => f Module -> Sem r InfoTable
getMany = mconcatMap (cacheGet . ModuleIndex)
extendWithReplExpression :: Expression -> InfoTable -> InfoTable
extendWithReplExpression e =
@ -88,21 +64,16 @@ letFunctionDefs e =
LetFunDef f -> pure f
LetMutualBlock (MutualBlockLet fs) -> fs
-- | moduleName ↦ infoTable
type Cache = HashMap Name InfoTable
buildTable1' :: forall r. (Members '[State Cache] r) => Module -> Sem r InfoTable
buildTable1' m = do
mi <- gets @Cache (^. at (m ^. moduleName))
maybe compute return mi
computeTable :: forall r. (Members '[MCache] r) => ModuleIndex -> Sem r InfoTable
computeTable (ModuleIndex m) = compute
where
compute :: Sem r InfoTable
compute = do
infoInc <- buildTable' (map (^. includeModule) includes)
infoInc <- mconcatMapM (cacheGet . (^. importModule)) imports
return (InfoTable {..} <> infoInc)
includes :: [Include]
includes = [i | StatementInclude i <- ss]
imports :: [Import]
imports = m ^. moduleBody . moduleImports
mutuals :: [MutualStatement]
mutuals =
@ -127,14 +98,14 @@ buildTable1' m = do
_infoConstructors :: HashMap Name ConstructorInfo
_infoConstructors =
HashMap.fromList
[ (c ^. inductiveConstructorName, ConstructorInfo params args ind builtin)
[ (c ^. inductiveConstructorName, ConstructorInfo params ty ind builtin)
| d <- inductives,
let ind = d ^. inductiveName
n = length (d ^. inductiveConstructors)
params = d ^. inductiveParameters
builtins = maybe (replicate n Nothing) (map Just . builtinConstructors) (d ^. inductiveBuiltin),
(builtin, c) <- zipExact builtins (d ^. inductiveConstructors),
let args = c ^. inductiveConstructorParameters
let ty = c ^. inductiveConstructorType
]
_infoFunctions :: HashMap Name FunctionInfo
@ -144,14 +115,9 @@ buildTable1' m = do
| StatementFunction f <- mutuals
]
<> [ (f ^. funDefName, FunctionInfo f)
| s <- filter (not . isInclude) ss,
| s <- ss,
f <- letFunctionDefs s
]
where
isInclude :: Statement -> Bool
isInclude = \case
StatementInclude {} -> True
_ -> False
_infoAxioms :: HashMap Name AxiomInfo
_infoAxioms =
@ -163,23 +129,62 @@ buildTable1' m = do
ss :: [Statement]
ss = m ^. moduleBody . moduleStatements
lookupConstructor :: (Member (Reader InfoTable) r) => Name -> Sem r ConstructorInfo
lookupConstructor f = HashMap.lookupDefault impossible f <$> asks (^. infoConstructors)
lookupConstructor :: forall r. Member (Reader InfoTable) r => Name -> Sem r ConstructorInfo
lookupConstructor f = do
err <- impossibleErr
HashMap.lookupDefault err f <$> asks (^. infoConstructors)
where
impossibleErr :: Sem r a
impossibleErr = do
tbl <- asks (^. infoConstructors)
return
. error
$ "impossible: "
<> ppTrace f
<> " is not in the InfoTable\n"
<> "The registered constructors are: "
<> ppTrace (HashMap.keys tbl)
lookupConstructorArgTypes :: (Member (Reader InfoTable) r) => Name -> Sem r ([VarName], [Expression])
lookupConstructorArgTypes = fmap constructorArgTypes . lookupConstructor
lookupInductive :: (Member (Reader InfoTable) r) => InductiveName -> Sem r InductiveInfo
lookupInductive f = HashMap.lookupDefault impossible f <$> asks (^. infoInductives)
lookupInductive :: forall r. Member (Reader InfoTable) r => InductiveName -> Sem r InductiveInfo
lookupInductive f = do
err <- impossibleErr
HashMap.lookupDefault err f <$> asks (^. infoInductives)
where
impossibleErr :: Sem r a
impossibleErr = do
tbl <- asks (^. infoInductives)
return
. error
$ "impossible: "
<> ppTrace f
<> " is not in the InfoTable\n"
<> "The registered inductives are: "
<> ppTrace (HashMap.keys tbl)
lookupFunction :: (Member (Reader InfoTable) r) => Name -> Sem r FunctionInfo
lookupFunction f = HashMap.lookupDefault impossible f <$> asks (^. infoFunctions)
lookupFunction :: forall r. Member (Reader InfoTable) r => Name -> Sem r FunctionInfo
lookupFunction f = do
err <- impossibleErr
HashMap.lookupDefault err f <$> asks (^. infoFunctions)
where
impossibleErr :: Sem r a
impossibleErr = do
tbl <- asks (^. infoFunctions)
return
. error
$ "impossible: "
<> ppTrace f
<> " is not in the InfoTable\n"
<> "The registered functions are: "
<> ppTrace (HashMap.keys tbl)
lookupAxiom :: (Member (Reader InfoTable) r) => Name -> Sem r AxiomInfo
lookupAxiom f = HashMap.lookupDefault impossible f <$> asks (^. infoAxioms)
inductiveType :: (Member (Reader InfoTable) r) => Name -> Sem r Expression
inductiveType v = do
lookupInductiveType :: Member (Reader InfoTable) r => Name -> Sem r Expression
lookupInductiveType v = do
info <- lookupInductive v
let ps = info ^. inductiveInfoDef . inductiveParameters
return $
@ -193,10 +198,10 @@ inductiveType v = do
constructorArgTypes :: ConstructorInfo -> ([VarName], [Expression])
constructorArgTypes i =
( map (^. inductiveParamName) (i ^. constructorInfoInductiveParameters),
i ^. constructorInfoArgs
constructorArgs (i ^. constructorInfoType)
)
constructorType :: (Member (Reader InfoTable) r) => ConstrName -> Sem r Expression
constructorType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
constructorType c = do
info <- lookupConstructor c
let (inductiveParams, constrArgs) = constructorArgTypes info
@ -206,7 +211,7 @@ constructorType c = do
saturatedTy <- constructorReturnType c
return (foldFunType args saturatedTy)
constructorReturnType :: (Member (Reader InfoTable) r) => ConstrName -> Sem r Expression
constructorReturnType :: Member (Reader InfoTable) r => ConstrName -> Sem r Expression
constructorReturnType c = do
info <- lookupConstructor c
let inductiveParams = fst (constructorArgTypes info)

View File

@ -0,0 +1,54 @@
module Juvix.Compiler.Internal.Data.InfoTable.Base where
import Juvix.Compiler.Internal.Language
import Juvix.Prelude
data ConstructorInfo = ConstructorInfo
{ _constructorInfoInductiveParameters :: [InductiveParameter],
_constructorInfoType :: Expression,
_constructorInfoInductive :: InductiveName,
_constructorInfoBuiltin :: Maybe BuiltinConstructor
}
newtype FunctionInfo = FunctionInfo
{ _functionInfoDef :: FunctionDef
}
newtype AxiomInfo = AxiomInfo
{ _axiomInfoDef :: AxiomDef
}
newtype InductiveInfo = InductiveInfo
{ _inductiveInfoDef :: InductiveDef
}
data InfoTable = InfoTable
{ _infoConstructors :: HashMap Name ConstructorInfo,
_infoAxioms :: HashMap Name AxiomInfo,
_infoFunctions :: HashMap Name FunctionInfo,
_infoInductives :: HashMap Name InductiveInfo
}
makeLenses ''InfoTable
makeLenses ''FunctionInfo
makeLenses ''ConstructorInfo
makeLenses ''AxiomInfo
makeLenses ''InductiveInfo
instance Semigroup InfoTable where
a <> b =
InfoTable
{ _infoConstructors = a ^. infoConstructors <> b ^. infoConstructors,
_infoAxioms = a ^. infoAxioms <> b ^. infoAxioms,
_infoFunctions = a ^. infoFunctions <> b ^. infoFunctions,
_infoInductives = a ^. infoInductives <> b ^. infoInductives
}
instance Monoid InfoTable where
mempty =
InfoTable
{ _infoConstructors = mempty,
_infoAxioms = mempty,
_infoFunctions = mempty,
_infoInductives = mempty
}

View File

@ -1,5 +1,5 @@
module Juvix.Compiler.Abstract.Data.Name
( module Juvix.Compiler.Abstract.Data.Name,
module Juvix.Compiler.Internal.Data.Name
( module Juvix.Compiler.Internal.Data.Name,
module Juvix.Data.NameKind,
module Juvix.Data.NameId,
module Juvix.Data.Fixity,
@ -25,7 +25,20 @@ data Name = Name
makeLenses ''Name
varFromWildcard :: (Members '[NameIdGen] r) => Wildcard -> Sem r VarName
varFromHole :: Hole -> VarName
varFromHole h =
Name
{ _nameText = pp,
_nameKind = KNameLocal,
_namePretty = pp,
_nameLoc = getLoc h,
_nameId = h ^. holeId,
_nameFixity = Nothing
}
where
pp = "" <> prettyText (h ^. holeId)
varFromWildcard :: Members '[NameIdGen] r => Wildcard -> Sem r VarName
varFromWildcard w = do
_nameId <- freshNameId
let _nameText :: Text = "" <> prettyText _nameId

View File

@ -0,0 +1,10 @@
module Juvix.Compiler.Internal.Data.NameDependencyInfo
( module Juvix.Compiler.Internal.Data.NameDependencyInfo,
module Juvix.Data.DependencyInfo,
)
where
import Juvix.Compiler.Internal.Data.Name
import Juvix.Data.DependencyInfo
type NameDependencyInfo = DependencyInfo Name

View File

@ -4,6 +4,7 @@ module Juvix.Compiler.Internal.Extra
)
where
import Data.Generics.Uniplate.Data hiding (holes)
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Internal.Data.LocalVars
@ -25,6 +26,9 @@ data ApplicationArg = ApplicationArg
makeLenses ''ApplicationArg
instance HasLoc ApplicationArg where
getLoc = getLoc . (^. appArg)
class HasExpressions a where
leafExpressions :: Traversal' a Expression
@ -196,11 +200,13 @@ instance HasExpressions InductiveDef where
params' <- traverse (leafExpressions f) _inductiveParameters
constrs' <- traverse (leafExpressions f) _inductiveConstructors
examples' <- traverse (leafExpressions f) _inductiveExamples
ty' <- leafExpressions f _inductiveType
pure
InductiveDef
{ _inductiveParameters = params',
_inductiveConstructors = constrs',
_inductiveExamples = examples',
_inductiveType = ty',
_inductiveName,
_inductiveBuiltin,
_inductivePositive,
@ -208,16 +214,13 @@ instance HasExpressions InductiveDef where
}
instance HasExpressions InductiveConstructorDef where
-- leafExpressions f InductiveConstructorDef c args ret = do
leafExpressions f InductiveConstructorDef {..} = do
args' <- traverse (leafExpressions f) _inductiveConstructorParameters
ret' <- leafExpressions f _inductiveConstructorReturnType
ty' <- leafExpressions f _inductiveConstructorType
examples' <- traverse (leafExpressions f) _inductiveConstructorExamples
pure
InductiveConstructorDef
{ _inductiveConstructorExamples = examples',
_inductiveConstructorParameters = args',
_inductiveConstructorReturnType = ret',
_inductiveConstructorType = ty',
_inductiveConstructorName,
_inductiveConstructorPragmas
}
@ -304,7 +307,16 @@ foldFunType l r = go l
[] -> r
arg : args -> ExpressionFunction (Function arg (go args))
-- -- | a -> (b -> c) ==> ([a, b], c)
foldFunTypeExplicit :: [Expression] -> Expression -> Expression
foldFunTypeExplicit = foldFunType . map unnamedParameter
viewConstructorType :: Expression -> ([Expression], Expression)
viewConstructorType = first (map (^. paramType)) . unfoldFunType
constructorArgs :: Expression -> [Expression]
constructorArgs = fst . viewConstructorType
-- | a -> (b -> c) ==> ([a, b], c)
unfoldFunType :: Expression -> ([FunctionParameter], Expression)
unfoldFunType t = case t of
ExpressionFunction (Function l r) -> first (l :) (unfoldFunType r)
@ -317,53 +329,24 @@ unfoldTypeAbsType t = case t of
_ -> ([], t)
foldExplicitApplication :: Expression -> [Expression] -> Expression
foldExplicitApplication f = foldApplication f . map (Explicit,)
foldExplicitApplication f = foldApplication f . map (ApplicationArg Explicit)
foldApplication :: Expression -> [(IsImplicit, Expression)] -> Expression
foldApplication f = \case
foldApplication :: Expression -> [ApplicationArg] -> Expression
foldApplication f args = case args of
[] -> f
(i, a) : as -> foldApplication (ExpressionApplication (Application f a i)) as
((ApplicationArg i a) : as) -> foldApplication (ExpressionApplication (Application f a i)) as
unfoldApplication' :: Application -> (Expression, NonEmpty (IsImplicit, Expression))
unfoldApplication' (Application l' r' i') = second (|: (i', r')) (unfoldExpressionApp l')
unfoldApplication' :: Application -> (Expression, NonEmpty ApplicationArg)
unfoldApplication' (Application l' r' i') = second (|: (ApplicationArg i' r')) (unfoldExpressionApp l')
unfoldExpressionApp :: Expression -> (Expression, [(IsImplicit, Expression)])
unfoldExpressionApp :: Expression -> (Expression, [ApplicationArg])
unfoldExpressionApp = \case
ExpressionApplication (Application l r i) ->
second (`snoc` (i, r)) (unfoldExpressionApp l)
second (`snoc` ApplicationArg i r) (unfoldExpressionApp l)
e -> (e, [])
unfoldApplication :: Application -> (Expression, NonEmpty Expression)
unfoldApplication = fmap (fmap snd) . unfoldApplication'
reachableModules :: Module -> [Module]
reachableModules = fst . run . runOutputList . evalState (mempty :: HashSet Name) . go
where
go :: forall r. (Members '[State (HashSet Name), Output Module] r) => Module -> Sem r ()
go m = do
s <- get
unless
(HashSet.member (m ^. moduleName) s)
(output m >> goBody (m ^. moduleBody))
where
goBody :: ModuleBody -> Sem r ()
goBody = mapM_ goStatement . (^. moduleStatements)
goStatement :: Statement -> Sem r ()
goStatement = \case
StatementInclude (Include inc) -> go inc
_ -> return ()
(-->) :: Expression -> Expression -> Expression
(-->) a b =
ExpressionFunction
( Function
FunctionParameter
{ _paramName = Nothing,
_paramImplicit = Explicit,
_paramType = a
}
b
)
unfoldApplication = fmap (fmap (^. appArg)) . unfoldApplication'
-- | A fold over all transitive children, including self
patternCosmos :: SimpleFold Pattern Pattern
@ -444,3 +427,243 @@ viewExpressionAsPattern e = case viewApp e of
getVariable f = case f of
ExpressionIden (IdenVar n) -> Just n
_ -> Nothing
class IsExpression a where
toExpression :: a -> Expression
instance IsExpression Iden where
toExpression = ExpressionIden
instance IsExpression Expression where
toExpression = id
instance IsExpression Hole where
toExpression = ExpressionHole
instance IsExpression Name where
toExpression n = ExpressionIden (mkIden n)
where
mkIden = case n ^. nameKind of
KNameConstructor -> IdenConstructor
KNameInductive -> IdenInductive
KNameFunction -> IdenFunction
KNameAxiom -> IdenAxiom
KNameLocal -> IdenVar
KNameLocalModule -> impossible
KNameTopModule -> impossible
instance IsExpression SmallUniverse where
toExpression = ExpressionUniverse
instance IsExpression Application where
toExpression = ExpressionApplication
instance IsExpression Function where
toExpression = ExpressionFunction
instance IsExpression ConstructorApp where
toExpression (ConstructorApp c args _) =
foldApplication (toExpression c) (map toApplicationArg args)
toApplicationArg :: PatternArg -> ApplicationArg
toApplicationArg p =
set appArgIsImplicit (p ^. patternArgIsImplicit) (helper (p ^. patternArgPattern))
where
helper :: Pattern -> ApplicationArg
helper = \case
PatternVariable v -> ApplicationArg Explicit (toExpression v)
PatternConstructorApp a -> ApplicationArg Explicit (toExpression a)
expressionArrow :: (IsExpression a, IsExpression b) => IsImplicit -> a -> b -> Expression
expressionArrow isImpl a b =
ExpressionFunction
( Function
( FunctionParameter
{ _paramName = Nothing,
_paramImplicit = isImpl,
_paramType = toExpression a
}
)
(toExpression b)
)
infixr 0 <>-->
(<>-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
(<>-->) = expressionArrow Implicit
infixr 0 -->
(-->) :: (IsExpression a, IsExpression b) => a -> b -> Expression
(-->) = expressionArrow Explicit
infix 4 ===
(===) :: (IsExpression a, IsExpression b) => a -> b -> Bool
a === b = (toExpression a ==% toExpression b) mempty
leftEq :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
leftEq a b free =
isRight
. run
. runError @Text
. runReader free
. evalState (mempty @(HashMap Name Name))
$ matchExpressions (toExpression a) (toExpression b)
clauseLhsAsExpression :: FunctionClause -> Expression
clauseLhsAsExpression cl =
foldApplication (toExpression (cl ^. clauseName)) (map toApplicationArg (cl ^. clausePatterns))
infix 4 ==%
(==%) :: (IsExpression a, IsExpression b) => a -> b -> HashSet Name -> Bool
(==%) a b free = leftEq a b free || leftEq b a free
infixl 9 @@
(@@) :: (IsExpression a, IsExpression b) => a -> b -> Expression
a @@ b = toExpression (Application (toExpression a) (toExpression b) Explicit)
freshVar :: (Member NameIdGen r) => Interval -> Text -> Sem r VarName
freshVar _nameLoc n = do
uid <- freshNameId
return
Name
{ _nameId = uid,
_nameText = n,
_nameKind = KNameLocal,
_namePretty = n,
_nameFixity = Nothing,
_nameLoc
}
freshHole :: Members '[NameIdGen] r => Interval -> Sem r Hole
freshHole l = mkHole l <$> freshNameId
mkFreshHole :: Members '[NameIdGen] r => Interval -> Sem r Expression
mkFreshHole l = ExpressionHole <$> freshHole l
matchExpressions ::
forall r.
(Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r) =>
Expression ->
Expression ->
Sem r ()
matchExpressions = go
where
-- Soft free vars are allowed to be matched
isSoftFreeVar :: VarName -> Sem r Bool
isSoftFreeVar = asks . HashSet.member
go :: Expression -> Expression -> Sem r ()
go a b = case (a, b) of
(ExpressionIden ia, ExpressionIden ib) -> case (ia, ib) of
(IdenVar va, IdenVar vb) -> do
addIfFreeVar va vb
addIfFreeVar vb va
unlessM (matchVars va vb) err
(_, _) -> unless (ia == ib) err
(ExpressionIden (IdenVar va), ExpressionHole h) -> goHole va h
(ExpressionHole h, ExpressionIden (IdenVar vb)) -> goHole vb h
(ExpressionIden {}, _) -> err
(_, ExpressionIden {}) -> err
(ExpressionApplication ia, ExpressionApplication ib) ->
goApp ia ib
(ExpressionApplication {}, _) -> err
(_, ExpressionApplication {}) -> err
(ExpressionLambda ia, ExpressionLambda ib) ->
goLambda ia ib
(ExpressionLambda {}, _) -> err
(_, ExpressionLambda {}) -> err
(ExpressionCase {}, ExpressionCase {}) -> error "not implemented"
(ExpressionCase {}, _) -> err
(_, ExpressionCase {}) -> err
(ExpressionUniverse ia, ExpressionUniverse ib) ->
unless (ia == ib) err
(ExpressionUniverse {}, _) -> err
(_, ExpressionUniverse {}) -> err
(ExpressionFunction ia, ExpressionFunction ib) ->
goFunction ia ib
(ExpressionFunction {}, _) -> err
(_, ExpressionFunction {}) -> err
(ExpressionSimpleLambda {}, ExpressionSimpleLambda {}) -> error "not implemented"
(ExpressionSimpleLambda {}, _) -> err
(_, ExpressionSimpleLambda {}) -> err
(ExpressionLiteral ia, ExpressionLiteral ib) ->
unless (ia == ib) err
(ExpressionLiteral {}, _) -> err
(_, ExpressionLiteral {}) -> err
(ExpressionLet {}, ExpressionLet {}) -> error "not implemented"
(_, ExpressionLet {}) -> err
(ExpressionLet {}, _) -> err
(ExpressionHole _, ExpressionHole _) -> return ()
err :: Sem r a
err = throw @Text "Expression missmatch"
matchVars :: Name -> Name -> Sem r Bool
matchVars va vb = (== Just vb) <$> gets @(HashMap Name Name) (^. at va)
goHole :: Name -> Hole -> Sem r ()
goHole var h = do
whenM (gets @(HashMap Name Name) (HashMap.member var)) err
let vh = varFromHole h
addName var vh
addIfFreeVar :: VarName -> VarName -> Sem r ()
addIfFreeVar va vb = whenM (isSoftFreeVar va) (addName va vb)
goLambda :: Lambda -> Lambda -> Sem r ()
goLambda = error "TODO not implemented yet"
goApp :: Application -> Application -> Sem r ()
goApp (Application al ar aim) (Application bl br bim) = do
unless (aim == bim) err
go al bl
go ar br
goFunction :: Function -> Function -> Sem r ()
goFunction (Function al ar) (Function bl br) = do
matchFunctionParameter al bl
matchExpressions ar br
addName :: (Member (State (HashMap Name Name)) r) => Name -> Name -> Sem r ()
addName na nb = modify (HashMap.insert na nb)
matchFunctionParameter ::
forall r.
(Members '[State (HashMap Name Name), Reader (HashSet VarName), Error Text] r) =>
FunctionParameter ->
FunctionParameter ->
Sem r ()
matchFunctionParameter pa pb = do
goParamName (pa ^. paramName) (pb ^. paramName)
goParamImplicit (pa ^. paramImplicit) (pb ^. paramImplicit)
goParamType (pa ^. paramType) (pb ^. paramType)
where
goParamType :: Expression -> Expression -> Sem r ()
goParamType ua ub = matchExpressions ua ub
goParamImplicit :: IsImplicit -> IsImplicit -> Sem r ()
goParamImplicit ua ub = unless (ua == ub) (throw @Text "implicit mismatch")
goParamName :: Maybe VarName -> Maybe VarName -> Sem r ()
goParamName (Just va) (Just vb) = addName va vb
goParamName _ _ = return ()
isSmallUniverse' :: Expression -> Bool
isSmallUniverse' = \case
ExpressionUniverse {} -> True
_ -> False
allTypeSignatures :: Data a => a -> [Expression]
allTypeSignatures a =
[f ^. funDefType | f@FunctionDef {} <- universeBi a]
<> [f ^. axiomType | f@AxiomDef {} <- universeBi a]
<> [f ^. inductiveType | f@InductiveDef {} <- universeBi a]
idenName :: Iden -> Name
idenName = \case
IdenFunction f -> f
IdenConstructor c -> c
IdenVar v -> v
IdenInductive i -> i
IdenAxiom a -> a

View File

@ -1,53 +1,54 @@
module Juvix.Compiler.Abstract.Extra.DependencyBuilder (buildDependencyInfo, buildDependencyInfoExpr, ExportsTable) where
module Juvix.Compiler.Internal.Extra.DependencyBuilder
( buildDependencyInfo,
buildDependencyInfoPreModule,
buildDependencyInfoExpr,
buildDependencyInfoLet,
ExportsTable,
)
where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Abstract.Data.NameDependencyInfo
import Juvix.Compiler.Abstract.Extra.Functions
import Juvix.Compiler.Abstract.Language
import Juvix.Compiler.Internal.Data.NameDependencyInfo
import Juvix.Compiler.Internal.Extra
import Juvix.Prelude
-- adjacency set representation
type DependencyGraph = HashMap Name (HashSet Name)
newtype VisitedModules = VisitedModules
{ _visitedModulesSet :: HashSet Name
}
makeLenses ''VisitedModules
type StartNodes = HashSet Name
type ExportsTable = HashSet NameId
buildDependencyInfo :: NonEmpty TopModule -> ExportsTable -> NameDependencyInfo
buildDependencyInfoPreModule :: PreModule -> ExportsTable -> NameDependencyInfo
buildDependencyInfoPreModule ms tab =
buildDependencyInfoHelper tab (goPreModule ms)
buildDependencyInfo :: NonEmpty Module -> ExportsTable -> NameDependencyInfo
buildDependencyInfo ms tab =
buildDependencyInfoHelper tab (mapM_ goModule ms)
buildDependencyInfoHelper tab (mapM_ (visit . ModuleIndex) ms)
buildDependencyInfoExpr :: Expression -> NameDependencyInfo
buildDependencyInfoExpr = buildDependencyInfoHelper mempty . goExpression Nothing
buildDependencyInfoLet :: NonEmpty PreLetStatement -> NameDependencyInfo
buildDependencyInfoLet = buildDependencyInfoHelper mempty . mapM_ goPreLetStatement
buildDependencyInfoHelper ::
ExportsTable ->
( Sem
'[ Reader ExportsTable,
State DependencyGraph,
State StartNodes,
State VisitedModules
]
()
) ->
Sem '[Visit ModuleIndex, Reader ExportsTable, State DependencyGraph, State StartNodes] () ->
NameDependencyInfo
buildDependencyInfoHelper tbl m = createDependencyInfo graph startNodes
where
startNodes :: StartNodes
graph :: DependencyGraph
(startNodes, graph) =
run $
evalState (VisitedModules mempty) $
runState HashSet.empty $
execState HashMap.empty $
runReader tbl m
run
. runState HashSet.empty
. execState HashMap.empty
. runReader tbl
. evalVisitEmpty goModuleNoVisited
$ m
addStartNode :: (Member (State StartNodes) r) => Name -> Sem r ()
addStartNode n = modify (HashSet.insert n)
@ -73,6 +74,67 @@ checkStartNode n = do
(HashSet.member (n ^. nameId) tab)
(addStartNode n)
goModuleNoVisited :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, Visit ModuleIndex] r => ModuleIndex -> Sem r ()
goModuleNoVisited (ModuleIndex m) = do
checkStartNode (m ^. moduleName)
let b = m ^. moduleBody
mapM_ (goStatement (m ^. moduleName)) (b ^. moduleStatements)
mapM_ goImport (b ^. moduleImports)
goImport :: Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, Visit ModuleIndex] r => Import -> Sem r ()
goImport (Import m) = visit m
-- | Ignores includes
goPreModule :: Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => PreModule -> Sem r ()
goPreModule m = do
checkStartNode (m ^. moduleName)
let b = m ^. moduleBody
mapM_ (goPreStatement (m ^. moduleName)) (b ^. moduleStatements)
goStatement :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => Name -> Statement -> Sem r ()
goStatement parentModule = \case
StatementAxiom ax -> goAxiom parentModule ax
StatementMutual f -> goMutual parentModule f
goMutual :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => Name -> MutualBlock -> Sem r ()
goMutual parentModule (MutualBlock s) = mapM_ go s
where
go :: MutualStatement -> Sem r ()
go = \case
StatementInductive i -> goInductive parentModule i
StatementFunction i -> goTopFunctionDef parentModule i
goPreLetStatement ::
forall r.
Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r =>
PreLetStatement ->
Sem r ()
goPreLetStatement = \case
PreLetFunctionDef f -> goFunctionDefHelper f
-- | Declarations in a module depend on the module, not the other way round (a
-- module is reachable if at least one of the declarations in it is reachable)
goPreStatement :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => Name -> PreStatement -> Sem r ()
goPreStatement parentModule = \case
PreAxiomDef ax -> goAxiom parentModule ax
PreFunctionDef f -> goTopFunctionDef parentModule f
PreInductiveDef i -> goInductive parentModule i
goAxiom :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => Name -> AxiomDef -> Sem r ()
goAxiom parentModule ax = do
checkStartNode (ax ^. axiomName)
addEdge (ax ^. axiomName) parentModule
goExpression (Just (ax ^. axiomName)) (ax ^. axiomType)
goInductive :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes] r => Name -> InductiveDef -> Sem r ()
goInductive parentModule i = do
checkStartNode (i ^. inductiveName)
checkBuiltinInductiveStartNode i
addEdge (i ^. inductiveName) parentModule
mapM_ (goInductiveParameter (Just (i ^. inductiveName))) (i ^. inductiveParameters)
goExpression (Just (i ^. inductiveName)) (i ^. inductiveType)
mapM_ (goConstructorDef (i ^. inductiveName)) (i ^. inductiveConstructors)
-- BuiltinBool and BuiltinNat are required by the Internal to Core translation
-- when translating literal integers to Nats.
checkBuiltinInductiveStartNode :: forall r. Member (State StartNodes) r => InductiveDef -> Sem r ()
@ -87,47 +149,6 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
addInductiveStartNode :: Sem r ()
addInductiveStartNode = addStartNode (i ^. inductiveName)
guardNotVisited :: (Member (State VisitedModules) r) => Name -> Sem r () -> Sem r ()
guardNotVisited n cont =
unlessM
(HashSet.member n . (^. visitedModulesSet) <$> get)
(modify (over visitedModulesSet (HashSet.insert n)) >> cont)
goModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r) => Module -> Sem r ()
goModule m = do
checkStartNode (m ^. moduleName)
mapM_ (goStatement (m ^. moduleName)) (m ^. moduleBody . moduleStatements)
goLocalModule :: (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r) => Name -> Module -> Sem r ()
goLocalModule parentModule m = do
addEdge (m ^. moduleName) parentModule
goModule m
-- Declarations in a module depend on the module, not the other way round (a
-- module is reachable if at least one of the declarations in it is reachable)
goStatement :: forall r. Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State VisitedModules] r => Name -> Statement -> Sem r ()
goStatement parentModule = \case
StatementAxiom ax -> goAxiom ax
StatementFunction f -> goTopFunctionDef parentModule f
StatementImport m -> guardNotVisited (m ^. moduleName) (goModule m)
StatementLocalModule m -> goLocalModule parentModule m
StatementInductive i -> goInductive i
where
goAxiom :: AxiomDef -> Sem r ()
goAxiom ax = do
checkStartNode (ax ^. axiomName)
addEdge (ax ^. axiomName) parentModule
goExpression (Just (ax ^. axiomName)) (ax ^. axiomType)
goInductive :: InductiveDef -> Sem r ()
goInductive i = do
checkStartNode (i ^. inductiveName)
checkBuiltinInductiveStartNode i
addEdge (i ^. inductiveName) parentModule
mapM_ (goFunctionParameter (Just (i ^. inductiveName))) (i ^. inductiveParameters)
goExpression (Just (i ^. inductiveName)) (i ^. inductiveType)
mapM_ (goConstructorDef (i ^. inductiveName)) (i ^. inductiveConstructors)
goTopFunctionDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionDef -> Sem r ()
goTopFunctionDef modName f = do
addEdge (f ^. funDefName) modName
@ -139,15 +160,15 @@ goFunctionDefHelper ::
Sem r ()
goFunctionDefHelper f = do
checkStartNode (f ^. funDefName)
goExpression (Just (f ^. funDefName)) (f ^. funDefTypeSig)
goExpression (Just (f ^. funDefName)) (f ^. funDefType)
mapM_ (goFunctionClause (f ^. funDefName)) (f ^. funDefClauses)
-- constructors of an inductive type depend on the inductive type, not the other
-- way round; an inductive type depends on the types of its constructors
goConstructorDef :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> InductiveConstructorDef -> Sem r ()
goConstructorDef indName c = do
addEdge (c ^. constructorName) indName
goExpression (Just indName) (c ^. constructorType)
addEdge (c ^. inductiveConstructorName) indName
goExpression (Just indName) (c ^. inductiveConstructorType)
goFunctionClause :: (Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) => Name -> FunctionClause -> Sem r ()
goFunctionClause p c = do
@ -157,13 +178,11 @@ goFunctionClause p c = do
goPattern :: forall r. (Member (State DependencyGraph) r) => Maybe Name -> PatternArg -> Sem r ()
goPattern n p = case p ^. patternArgPattern of
PatternVariable {} -> return ()
PatternWildcard {} -> return ()
PatternEmpty -> return ()
PatternConstructorApp a -> goApp a
where
goApp :: ConstructorApp -> Sem r ()
goApp (ConstructorApp ctr ps) = do
addEdgeMay n (ctr ^. constructorRefName)
goApp (ConstructorApp ctr ps _) = do
addEdgeMay n ctr
mapM_ (goPattern n) ps
goExpression ::
@ -176,8 +195,8 @@ goExpression p e = case e of
ExpressionIden i -> addEdgeMay p (idenName i)
ExpressionUniverse {} -> return ()
ExpressionFunction f -> do
goFunctionParameter p (f ^. funParameter)
goExpression p (f ^. funReturn)
goFunctionParameter p (f ^. functionLeft)
goExpression p (f ^. functionRight)
ExpressionApplication (Application l r _) -> do
goExpression p l
goExpression p r
@ -186,14 +205,19 @@ goExpression p e = case e of
ExpressionHole {} -> return ()
ExpressionLambda l -> goLambda l
ExpressionLet l -> goLet l
ExpressionSimpleLambda l -> goSimpleLambda l
where
goSimpleLambda :: SimpleLambda -> Sem r ()
goSimpleLambda l = do
addEdgeMay p (l ^. slambdaVar)
goLambda :: Lambda -> Sem r ()
goLambda (Lambda clauses) = mapM_ goClause clauses
goLambda Lambda {..} = mapM_ goClause _lambdaClauses
where
goClause :: LambdaClause -> Sem r ()
goClause (LambdaClause {..}) = do
goExpression p _lambdaBody
mapM_ (goPattern p) _lambdaParameters
mapM_ (goPattern p) _lambdaPatterns
goCase :: Case -> Sem r ()
goCase c = do
@ -213,10 +237,21 @@ goExpression p e = case e of
LetFunDef f -> do
addEdgeMay p (f ^. funDefName)
goFunctionDefHelper f
LetMutualBlock MutualBlockLet {..} -> mapM_ goFunctionDefHelper _mutualLet
goInductiveParameter ::
(Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
Maybe Name ->
InductiveParameter ->
Sem r ()
goInductiveParameter p param =
addEdgeMay p (param ^. inductiveParamName)
goFunctionParameter ::
(Members '[State DependencyGraph, State StartNodes, Reader ExportsTable] r) =>
Maybe Name ->
FunctionParameter ->
Sem r ()
goFunctionParameter p param = goExpression p (param ^. paramType)
goFunctionParameter p param = do
whenJust (param ^. paramName) (addEdgeMay p)
goExpression p (param ^. paramType)

View File

@ -1,6 +1,6 @@
module Juvix.Compiler.Internal.Language
( module Juvix.Compiler.Internal.Language,
module Juvix.Compiler.Abstract.Data.Name,
module Juvix.Compiler.Internal.Data.Name,
module Juvix.Data.WithLoc,
module Juvix.Data.IsImplicit,
module Juvix.Data.Universe,
@ -9,36 +9,52 @@ module Juvix.Compiler.Internal.Language
)
where
import Juvix.Compiler.Abstract.Data.Name
import Juvix.Compiler.Concrete.Data.Builtins
import Juvix.Compiler.Internal.Data.Name
import Juvix.Data.Hole
import Juvix.Data.IsImplicit
import Juvix.Data.Universe hiding (smallUniverse)
import Juvix.Data.WithLoc
import Juvix.Prelude
data Module = Module
type Module = Module' Statement
type PreModule = Module' PreStatement
type ModuleBody = ModuleBody' Statement
type PreModuleBody = ModuleBody' PreStatement
newtype PreLetStatement
= PreLetFunctionDef FunctionDef
data PreStatement
= PreFunctionDef FunctionDef
| PreInductiveDef InductiveDef
| PreAxiomDef AxiomDef
data Module' stmt = Module
{ _moduleName :: Name,
_moduleExamples :: [Example],
_moduleBody :: ModuleBody,
_moduleBody :: ModuleBody' stmt,
_modulePragmas :: Pragmas
}
deriving stock (Data)
newtype Include = Include
{ _includeModule :: Module
newtype Import = Import
{ _importModule :: ModuleIndex
}
deriving stock (Data)
newtype ModuleBody = ModuleBody
{ _moduleStatements :: [Statement]
data ModuleBody' stmt = ModuleBody
{ _moduleImports :: [Import],
_moduleStatements :: [stmt]
}
deriving stock (Data)
data Statement
= StatementMutual MutualBlock
| StatementAxiom AxiomDef
| StatementInclude Include
deriving stock (Data)
data MutualStatement
@ -259,6 +275,7 @@ data InductiveDef = InductiveDef
{ _inductiveName :: InductiveName,
_inductiveBuiltin :: Maybe BuiltinInductive,
_inductiveExamples :: [Example],
_inductiveType :: Expression,
_inductiveParameters :: [InductiveParameter],
_inductiveConstructors :: [InductiveConstructorDef],
_inductivePositive :: Bool,
@ -268,9 +285,8 @@ data InductiveDef = InductiveDef
data InductiveConstructorDef = InductiveConstructorDef
{ _inductiveConstructorName :: ConstrName,
_inductiveConstructorParameters :: [Expression],
_inductiveConstructorExamples :: [Example],
_inductiveConstructorReturnType :: Expression,
_inductiveConstructorType :: Expression,
_inductiveConstructorPragmas :: Pragmas
}
deriving stock (Data)
@ -292,20 +308,26 @@ data Function = Function
instance Hashable Function
newtype ModuleIndex = ModuleIndex
{ _moduleIxModule :: Module
}
deriving stock (Data)
makeLenses ''ModuleIndex
makeLenses ''Case
makeLenses ''CaseBranch
makeLenses ''Module
makeLenses ''Module'
makeLenses ''Let
makeLenses ''MutualBlockLet
makeLenses ''MutualBlock
makeLenses ''Example
makeLenses ''PatternArg
makeLenses ''Include
makeLenses ''Import
makeLenses ''FunctionDef
makeLenses ''FunctionClause
makeLenses ''InductiveDef
makeLenses ''AxiomDef
makeLenses ''ModuleBody
makeLenses ''ModuleBody'
makeLenses ''Application
makeLenses ''TypedExpression
makeLenses ''Function
@ -317,6 +339,16 @@ makeLenses ''InductiveParameter
makeLenses ''InductiveConstructorDef
makeLenses ''ConstructorApp
instance Eq ModuleIndex where
(==) = (==) `on` (^. moduleIxModule . moduleName)
instance Hashable ModuleIndex where
hashWithSalt s = hashWithSalt s . (^. moduleIxModule . moduleName)
deriving newtype instance (Eq Import)
deriving newtype instance (Hashable Import)
instance HasAtomicity Case where
atomicity = const Atom
@ -373,6 +405,10 @@ instance HasAtomicity Pattern where
instance HasLoc AxiomDef where
getLoc a = getLoc (a ^. axiomName) <> getLoc (a ^. axiomType)
instance HasLoc InductiveConstructorDef where
getLoc InductiveConstructorDef {..} =
getLoc _inductiveConstructorName <> getLoc _inductiveConstructorType
instance HasLoc InductiveParameter where
getLoc (InductiveParameter n) = getLoc n

View File

@ -19,7 +19,7 @@ ppOutDefault = mkAnsiText . PPOutput . doc defaultOptions
ppOut :: (CanonicalProjection a Options, PrettyCode c) => a -> c -> AnsiText
ppOut o = mkAnsiText . PPOutput . doc (project o)
ppTrace :: (PrettyCode c) => c -> Text
ppTrace :: PrettyCode c => c -> Text
ppTrace = Ansi.renderStrict . reAnnotateS stylize . layoutPretty defaultLayoutOptions . doc traceOptions
ppPrint :: PrettyCode c => c -> Text

View File

@ -5,6 +5,9 @@ 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.NameDependencyInfo
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty.Options
import Juvix.Data.CodeAnn
@ -116,6 +119,30 @@ instance PrettyCode Literal where
ppPipeBlock :: (PrettyCode a, Members '[Reader Options] r, Traversable t) => t a -> Sem r (Doc Ann)
ppPipeBlock items = vsep <$> mapM (fmap (kwPipe <+>) . ppCode) items
instance (PrettyCode a, PrettyCode b, PrettyCode c) => PrettyCode (a, b, c) where
ppCode (a, b, c) = do
a' <- ppCode a
b' <- ppCode b
c' <- ppCode c
return $ tuple [a', b', c']
instance PrettyCode NameDependencyInfo where
ppCode DependencyInfo {..} = do
let header x = annotate AnnImportant x <> line
edges' <- vsep <$> mapM ppCode _depInfoEdgeList
reachable' <- ppCode (toList _depInfoReachable)
topsort' <- ppCode _depInfoTopSort
return $
header "Edges:"
<> edges'
<> line
<> header "Reachable:"
<> reachable'
<> line
<> header "Topologically sorted:"
<> topsort'
<> line
instance PrettyCode LambdaClause where
ppCode LambdaClause {..} = do
lambdaParameters' <- hsep <$> mapM ppCodeAtom _lambdaPatterns
@ -154,8 +181,8 @@ instance PrettyCode Hole where
instance PrettyCode InductiveConstructorDef where
ppCode c = do
constructorName' <- ppCode (c ^. inductiveConstructorName)
constructorParameters' <- mapM ppCodeAtom (c ^. inductiveConstructorParameters)
return (hsep $ constructorName' : constructorParameters')
ty' <- ppCode (c ^. inductiveConstructorType)
return (constructorName' <+> kwColon <+> ty')
ppBlock ::
(PrettyCode a, Members '[Reader Options] r, Traversable t) =>
@ -224,10 +251,10 @@ instance PrettyCode FunctionClause where
clauseBody' <- ppCode (c ^. clauseBody)
return $ nest 2 (funName <+?> clausePatterns' <+> kwAssign <+> clauseBody')
instance PrettyCode Include where
instance PrettyCode Import where
ppCode i = do
name' <- ppCode (i ^. includeModule . moduleName)
return $ kwInclude <+> name'
name' <- ppCode (i ^. importModule . moduleIxModule . moduleName)
return $ kwImport <+> name'
instance PrettyCode BuiltinAxiom where
ppCode = return . annotate AnnKeyword . pretty
@ -255,12 +282,12 @@ instance PrettyCode Statement where
ppCode = \case
StatementMutual f -> ppCode f
StatementAxiom f -> ppCode f
StatementInclude i -> ppCode i
instance PrettyCode ModuleBody where
ppCode m = do
includes <- mapM ppCode (m ^. moduleImports)
everything <- mapM ppCode (m ^. moduleStatements)
return $ vsep2 everything
return (vsep includes <> line <> line <> vsep2 everything)
instance PrettyCode Module where
ppCode :: Member (Reader Options) r => Module -> Sem r (Doc Ann)
@ -276,6 +303,22 @@ instance PrettyCode Module where
<> body'
<> line
instance PrettyCode Interval where
ppCode = return . annotate AnnCode . pretty
instance PrettyCode InfoTable where
ppCode tbl = do
inds <- ppCode (HashMap.keys (tbl ^. infoInductives))
constrs <- ppCode (HashMap.keys (tbl ^. infoConstructors))
let header :: Text -> Doc Ann = annotate AnnImportant . pretty
return $
header "InfoTable"
<> "\n========="
<> header "\nInductives: "
<> inds
<> header "\nConstructors: "
<> constrs
ppPostExpression ::
(PrettyCode a, HasAtomicity a, Member (Reader Options) r) =>
Fixity ->
@ -317,16 +360,19 @@ instance PrettyCode a => PrettyCode (Maybe a) where
Nothing -> return "Nothing"
Just p -> ("Just" <+>) <$> ppCode p
tuple :: [Doc ann] -> Doc ann
tuple = encloseSep "(" ")" ", "
instance (PrettyCode a, PrettyCode b) => PrettyCode (a, b) where
ppCode (x, y) = do
x' <- ppCode x
y' <- ppCode y
return $ encloseSep "(" ")" ", " [x', y']
return $ tuple [x', y']
instance (PrettyCode a) => PrettyCode [a] where
instance PrettyCode a => PrettyCode [a] where
ppCode x = do
cs <- mapM ppCode (toList x)
return $ encloseSep "[" "]" ", " cs
instance (PrettyCode a) => PrettyCode (NonEmpty a) where
instance PrettyCode a => PrettyCode (NonEmpty a) where
ppCode x = ppCode (toList x)

View File

@ -1,14 +1,14 @@
module Juvix.Compiler.Internal.Translation
( module Juvix.Compiler.Internal.Language,
module Juvix.Compiler.Internal.Translation.FromAbstract,
module Juvix.Compiler.Internal.Translation.FromAbstract.Data,
module Juvix.Compiler.Internal.Translation.FromConcrete,
module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
module Juvix.Compiler.Internal.Translation.FromInternal,
module Juvix.Compiler.Internal.Translation.FromInternal.Data,
)
where
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Translation.FromAbstract
import Juvix.Compiler.Internal.Translation.FromAbstract.Data
import Juvix.Compiler.Internal.Translation.FromConcrete hiding (MCache, goModuleNoCache, goStatement)
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal
import Juvix.Compiler.Internal.Translation.FromInternal.Data

View File

@ -23,7 +23,7 @@ unfoldPolyApplication a =
_ -> impossible
filterCompileTimeArgsOrPatterns :: (Member (Reader TypesTable) r) => Name -> [a] -> Sem r [a]
filterCompileTimeArgsOrPatterns idenName lst = do
filterCompileTimeArgsOrPatterns idenname lst = do
tab <- ask
let funParams = fst (unfoldFunType (ty tab))
typedArgs =
@ -32,7 +32,7 @@ filterCompileTimeArgsOrPatterns idenName lst = do
zip lst (map (^. paramType) funParams)
return $ typedArgs ++ drop (length funParams) lst
where
ty = HashMap.lookupDefault impossible (idenName ^. nameId)
ty = HashMap.lookupDefault impossible (idenname ^. nameId)
isUniverse :: Expression -> Bool
isUniverse = \case
(ExpressionUniverse {}) -> True

View File

@ -1,546 +0,0 @@
module Juvix.Compiler.Internal.Translation.FromAbstract
( module Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context,
TranslationState (..),
iniState,
fromAbstract,
fromAbstractExpression,
fromAbstractImport,
)
where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Abstract.Data.NameDependencyInfo
import Juvix.Compiler.Abstract.Extra.DependencyBuilder
import Juvix.Compiler.Abstract.Extra.DependencyBuilder qualified as Abstract
import Juvix.Compiler.Abstract.Language qualified as Abstract
import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context qualified as Abstract
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty.Base
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
import Juvix.Compiler.Pipeline.EntryPoint qualified as E
import Juvix.Prelude
data PreStatement
= PreFunctionDef FunctionDef
| PreInductiveDef InductiveDef
| PreAxiomDef AxiomDef
newtype TranslationState = TranslationState
{ -- | Top modules are supposed to be included at most once.
_translationStateIncluded :: HashSet Abstract.TopModuleName
}
iniState :: TranslationState
iniState =
TranslationState
{ _translationStateIncluded = mempty
}
makeLenses ''TranslationState
fromAbstract ::
Members '[Error JuvixError, NameIdGen] r =>
Abstract.AbstractResult ->
Sem r InternalResult
fromAbstract abstractResults = do
let abstractModules = abstractResults ^. Abstract.resultModules
exportsTbl = abstractResults ^. Abstract.resultExports
_resultModules' <-
runReader exportsTbl
. evalState iniState
$ mapM goModule abstractModules
let topModule = head _resultModules'
tbl = buildTable _resultModules'
unless
noTerminationOption
( mapError
(JuvixError @TerminationError)
(checkTermination tbl topModule)
)
return
InternalResult
{ _resultAbstract = abstractResults,
_resultModules = _resultModules',
_resultDepInfo = depInfo
}
where
noTerminationOption =
abstractResults
^. Abstract.abstractResultEntryPoint
. E.entryPointNoTermination
depInfo = buildDependencyInfo (abstractResults ^. Abstract.resultModules) (abstractResults ^. Abstract.resultExports)
fromAbstractExpression :: Members '[NameIdGen] r => Abstract.Expression -> Sem r Expression
fromAbstractExpression e = runReader depInfo (goExpression e)
where
depInfo :: NameDependencyInfo
depInfo = buildDependencyInfoExpr e
fromAbstractImport ::
Members '[Reader ExportsTable, State TranslationState, NameIdGen] r =>
Abstract.TopModule ->
Sem r (Maybe Include)
fromAbstractImport = goImport
goModule ::
(Members '[Reader ExportsTable, State TranslationState, NameIdGen] r) =>
Abstract.TopModule ->
Sem r Module
goModule m = do
expTbl <- ask
let depInfo :: NameDependencyInfo
depInfo = Abstract.buildDependencyInfo (pure m) expTbl
runReader depInfo $ do
_moduleBody' <- goModuleBody (m ^. Abstract.moduleBody)
examples' <- mapM goExample (m ^. Abstract.moduleExamples)
return
Module
{ _moduleName = m ^. Abstract.moduleName,
_moduleExamples = examples',
_moduleBody = _moduleBody',
_modulePragmas = m ^. Abstract.modulePragmas
}
buildLetMutualBlocks ::
Members '[Reader NameDependencyInfo] r =>
[FunctionDef] ->
Sem r [SCC FunctionDef]
buildLetMutualBlocks = fmap (map (fmap fromStmt)) . buildMutualBlocks . map PreFunctionDef
where
fromStmt :: PreStatement -> FunctionDef
fromStmt = \case
PreFunctionDef f -> f
_ -> impossible
-- | `StatementInclude`s are no included in the result
buildMutualBlocks ::
Members '[Reader NameDependencyInfo] r =>
[PreStatement] ->
Sem r [SCC PreStatement]
buildMutualBlocks ss = do
depInfo <- ask
let scomponents :: [SCC Abstract.Name] = buildSCCs depInfo
return (boolHack (mapMaybe nameToPreStatement scomponents))
where
-- If the builtin bool definition is found, it is moved at the front.
--
-- This is a hack needed to translate BuiltinStringToNat in
-- internal-to-core. BuiltinStringToNat is the only function that depends on
-- Bool implicitly (i.e. without mentioning it in its type). Eventually
-- BuiltinStringToNat needs to be removed and so this hack.
boolHack :: [SCC PreStatement] -> [SCC PreStatement]
boolHack s = case popFirstJust isBuiltinBool s of
(Nothing, _) -> s
(Just boolDef, rest) -> AcyclicSCC (PreInductiveDef boolDef) : rest
where
isBuiltinBool :: SCC PreStatement -> Maybe InductiveDef
isBuiltinBool = \case
CyclicSCC [PreInductiveDef b]
| Just BuiltinBool <- b ^. inductiveBuiltin -> Just b
_ -> Nothing
statementsByName :: HashMap Abstract.Name PreStatement
statementsByName = HashMap.fromList (map mkAssoc ss)
where
mkAssoc :: PreStatement -> (Abstract.Name, PreStatement)
mkAssoc s = case s of
PreInductiveDef i -> (i ^. inductiveName, s)
PreFunctionDef i -> (i ^. funDefName, s)
PreAxiomDef i -> (i ^. axiomName, s)
getStmt :: Abstract.Name -> Maybe PreStatement
getStmt n = statementsByName ^. at n
nameToPreStatement :: SCC Abstract.Name -> Maybe (SCC PreStatement)
nameToPreStatement = nonEmptySCC . fmap getStmt
where
nonEmptySCC :: SCC (Maybe a) -> Maybe (SCC a)
nonEmptySCC = \case
AcyclicSCC a -> AcyclicSCC <$> a
CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
unsupported :: Text -> a
unsupported thing = error ("Abstract to Internal: Not yet supported: " <> thing)
-- | Note that it ignores import statements
goDefinition ::
forall r.
Members '[Reader ExportsTable, Reader NameDependencyInfo, State TranslationState, NameIdGen] r =>
Abstract.Statement ->
Sem r [PreStatement]
goDefinition = \case
Abstract.StatementLocalModule m -> concatMapM goDefinition (m ^. Abstract.moduleBody . Abstract.moduleStatements)
Abstract.StatementInductive i -> pure . PreInductiveDef <$> goInductiveDef i
Abstract.StatementFunction i -> pure . PreFunctionDef <$> goFunctionDef i
Abstract.StatementAxiom a -> pure . PreAxiomDef <$> goAxiomDef a
Abstract.StatementImport {} -> return []
scanImports :: Abstract.ModuleBody -> [Abstract.TopModule]
scanImports (Abstract.ModuleBody stmts) = mconcatMap go stmts
where
go :: Abstract.Statement -> [Abstract.TopModule]
go = \case
Abstract.StatementLocalModule m -> scanImports (m ^. Abstract.moduleBody)
Abstract.StatementImport t -> [t]
Abstract.StatementInductive {} -> []
Abstract.StatementFunction {} -> []
Abstract.StatementAxiom {} -> []
goModuleBody ::
forall r.
Members '[Reader ExportsTable, Reader NameDependencyInfo, State TranslationState, NameIdGen] r =>
Abstract.ModuleBody ->
Sem r ModuleBody
goModuleBody b@(Abstract.ModuleBody stmts) = do
preDefs <- concatMapM goDefinition stmts
sccs <- buildMutualBlocks preDefs
let imports :: [Abstract.TopModule] = scanImports b
statements' = map goSCC sccs
imports' <- map StatementInclude <$> mapMaybeM goImport imports
return
ModuleBody
{ _moduleStatements = imports' <> statements'
}
where
goSCC :: SCC PreStatement -> Statement
goSCC = \case
AcyclicSCC s -> goAcyclic s
CyclicSCC c -> goCyclic (nonEmpty' c)
where
goCyclic :: NonEmpty PreStatement -> Statement
goCyclic c = StatementMutual (MutualBlock (goMutual <$> c))
where
goMutual :: PreStatement -> MutualStatement
goMutual = \case
PreInductiveDef i -> StatementInductive i
PreFunctionDef i -> StatementFunction i
_ -> impossible
goAcyclic :: PreStatement -> Statement
goAcyclic = \case
PreInductiveDef i -> one (StatementInductive i)
PreFunctionDef i -> one (StatementFunction i)
PreAxiomDef i -> StatementAxiom i
where
one :: MutualStatement -> Statement
one = StatementMutual . MutualBlock . pure
goImport :: (Members '[Reader ExportsTable, State TranslationState, NameIdGen] r) => Abstract.TopModule -> Sem r (Maybe Include)
goImport m = do
inc <- gets (HashSet.member (m ^. Abstract.moduleName) . (^. translationStateIncluded))
if
| inc -> return Nothing
| otherwise -> do
modify (over translationStateIncluded (HashSet.insert (m ^. Abstract.moduleName)))
m' <- goModule m
return
( Just
Include
{ _includeModule = m'
}
)
goTypeIden :: Abstract.Iden -> Iden
goTypeIden = \case
Abstract.IdenFunction f -> IdenFunction (f ^. Abstract.functionRefName)
Abstract.IdenConstructor {} -> unsupported "constructors in types"
Abstract.IdenVar v -> IdenVar v
Abstract.IdenInductive d -> IdenInductive (d ^. Abstract.inductiveRefName)
Abstract.IdenAxiom a -> IdenAxiom (a ^. Abstract.axiomRefName)
goAxiomDef :: Abstract.AxiomDef -> Sem r AxiomDef
goAxiomDef a = do
_axiomType' <- goType (a ^. Abstract.axiomType)
return
AxiomDef
{ _axiomName = a ^. Abstract.axiomName,
_axiomBuiltin = a ^. Abstract.axiomBuiltin,
_axiomType = _axiomType',
_axiomPragmas = a ^. Abstract.axiomPragmas
}
goFunctionParameter :: Abstract.FunctionParameter -> Sem r FunctionParameter
goFunctionParameter f = case f ^. Abstract.paramName of
Just var
| isSmallType (f ^. Abstract.paramType) ->
return
FunctionParameter
{ _paramName = Just var,
_paramImplicit = f ^. Abstract.paramImplicit,
_paramType = smallUniverseE (getLoc var)
}
| otherwise -> unsupported "named function arguments only for small types"
Nothing
| otherwise -> do
_paramType <- goType (f ^. Abstract.paramType)
return
FunctionParameter
{ _paramName = Nothing,
_paramImplicit = f ^. Abstract.paramImplicit,
_paramType
}
goFunction :: Abstract.Function -> Sem r Function
goFunction (Abstract.Function l r) = do
l' <- goFunctionParameter l
r' <- goType r
return (Function l' r')
goFunctionDef :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.FunctionDef -> Sem r FunctionDef
goFunctionDef f = do
_funDefClauses' <- mapM (goFunctionClause _funDefName') (f ^. Abstract.funDefClauses)
_funDefType' <- goType (f ^. Abstract.funDefTypeSig)
_funDefExamples' <- mapM goExample (f ^. Abstract.funDefExamples)
return
FunctionDef
{ _funDefName = _funDefName',
_funDefType = _funDefType',
_funDefClauses = _funDefClauses',
_funDefExamples = _funDefExamples',
_funDefBuiltin = f ^. Abstract.funDefBuiltin,
_funDefPragmas = f ^. Abstract.funDefPragmas,
_funDefTerminating = f ^. Abstract.funDefTerminating
}
where
_funDefName' :: Name
_funDefName' = f ^. Abstract.funDefName
goExample :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Example -> Sem r Example
goExample e = do
e' <- goExpression (e ^. Abstract.exampleExpression)
return
Example
{ _exampleExpression = e',
_exampleId = e ^. Abstract.exampleId
}
goFunctionClause :: Members '[NameIdGen, Reader NameDependencyInfo] r => Name -> Abstract.FunctionClause -> Sem r FunctionClause
goFunctionClause n c = do
_clauseBody' <- goExpression (c ^. Abstract.clauseBody)
_clausePatterns' <- mapM goPatternArg (c ^. Abstract.clausePatterns)
return
FunctionClause
{ _clauseName = n,
_clausePatterns = _clausePatterns',
_clauseBody = _clauseBody'
}
goPatternArg :: (Members '[NameIdGen] r) => Abstract.PatternArg -> Sem r PatternArg
goPatternArg p = do
pat' <- goPattern (p ^. Abstract.patternArgPattern)
return
PatternArg
{ _patternArgIsImplicit = p ^. Abstract.patternArgIsImplicit,
_patternArgName = p ^. Abstract.patternArgName,
_patternArgPattern = pat'
}
goPattern :: (Members '[NameIdGen] r) => Abstract.Pattern -> Sem r Pattern
goPattern p = case p of
Abstract.PatternVariable v -> return (PatternVariable v)
Abstract.PatternConstructorApp c -> PatternConstructorApp <$> goConstructorApp c
Abstract.PatternWildcard w -> PatternVariable <$> varFromWildcard w
Abstract.PatternEmpty -> unsupported "pattern empty"
goConstructorApp :: (Members '[NameIdGen] r) => Abstract.ConstructorApp -> Sem r ConstructorApp
goConstructorApp c = do
_constrAppParameters' <- mapM goPatternArg (c ^. Abstract.constrAppParameters)
return
ConstructorApp
{ _constrAppConstructor = c ^. Abstract.constrAppConstructor . Abstract.constructorRefName,
_constrAppParameters = _constrAppParameters',
_constrAppType = Nothing
}
isSmallType :: Abstract.Expression -> Bool
isSmallType e = case e of
Abstract.ExpressionUniverse u -> isSmallUni u
_ -> False
isSmallUni :: Universe -> Bool
isSmallUni u = 0 == fromMaybe 0 (u ^. universeLevel)
goUniverse :: Universe -> SmallUniverse
goUniverse u
| isSmallUni u = SmallUniverse (getLoc u)
| otherwise = unsupported "big universes"
goType :: Abstract.Expression -> Sem r Expression
goType e = case e of
Abstract.ExpressionIden i -> return (ExpressionIden (goTypeIden i))
Abstract.ExpressionUniverse u -> return (ExpressionUniverse (goUniverse u))
Abstract.ExpressionApplication a -> ExpressionApplication <$> goTypeApplication a
Abstract.ExpressionFunction f -> ExpressionFunction <$> goFunction f
Abstract.ExpressionLiteral {} -> unsupported "literals in types"
Abstract.ExpressionHole h -> return (ExpressionHole h)
Abstract.ExpressionLambda {} -> unsupported "lambda in types"
Abstract.ExpressionLet {} -> unsupported "let in types"
Abstract.ExpressionCase {} -> unsupported "case in types"
goLambda :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Lambda -> Sem r Lambda
goLambda (Abstract.Lambda cl') = do
_lambdaClauses <- mapM goClause cl'
let _lambdaType :: Maybe Expression = Nothing
return Lambda {..}
where
goClause :: Abstract.LambdaClause -> Sem r LambdaClause
goClause (Abstract.LambdaClause ps b) = do
ps' <- mapM (goPatternArg . explicit) ps
b' <- goExpression b
return (LambdaClause ps' b')
where
explicit :: Abstract.PatternArg -> Abstract.PatternArg
explicit p = case p ^. Abstract.patternArgIsImplicit of
Explicit -> p
Implicit -> unsupported "implicit patterns in lambda"
goApplication :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Application -> Sem r Application
goApplication (Abstract.Application f x i) = do
f' <- goExpression f
x' <- goExpression x
return (Application f' x' i)
goIden :: Abstract.Iden -> Iden
goIden i = case i of
Abstract.IdenFunction n -> IdenFunction (n ^. Abstract.functionRefName)
Abstract.IdenConstructor c -> IdenConstructor (c ^. Abstract.constructorRefName)
Abstract.IdenVar v -> IdenVar v
Abstract.IdenAxiom a -> IdenAxiom (a ^. Abstract.axiomRefName)
Abstract.IdenInductive a -> IdenInductive (a ^. Abstract.inductiveRefName)
goExpressionFunction :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Function -> Sem r Function
goExpressionFunction f = do
l' <- goParam (f ^. Abstract.funParameter)
r' <- goExpression (f ^. Abstract.funReturn)
return (Function l' r')
where
goParam :: Abstract.FunctionParameter -> Sem r FunctionParameter
goParam p = do
ty' <- goExpression (p ^. Abstract.paramType)
return (FunctionParameter (p ^. Abstract.paramName) (p ^. Abstract.paramImplicit) ty')
goExpression :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Expression -> Sem r Expression
goExpression e = case e of
Abstract.ExpressionIden i -> return (ExpressionIden (goIden i))
Abstract.ExpressionUniverse u -> return (ExpressionUniverse (goUniverse u))
Abstract.ExpressionFunction f -> ExpressionFunction <$> goExpressionFunction f
Abstract.ExpressionApplication a -> ExpressionApplication <$> goApplication a
Abstract.ExpressionLambda l -> ExpressionLambda <$> goLambda l
Abstract.ExpressionLiteral l -> return (ExpressionLiteral (goLiteral l))
Abstract.ExpressionHole h -> return (ExpressionHole h)
Abstract.ExpressionLet l -> ExpressionLet <$> goLet l
Abstract.ExpressionCase c -> ExpressionCase <$> goCase c
goLiteral :: Abstract.LiteralLoc -> LiteralLoc
goLiteral = fmap go
where
go :: Abstract.Literal -> Literal
go = \case
Abstract.LitString s -> LitString s
Abstract.LitInteger i -> LitInteger i
goCase :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.Case -> Sem r Case
goCase c = do
_caseExpression <- goExpression (c ^. Abstract.caseExpression)
_caseBranches <- mapM goCaseBranch (c ^. Abstract.caseBranches)
let _caseParens = c ^. Abstract.caseParens
_caseExpressionType :: Maybe Expression = Nothing
_caseExpressionWholeType :: Maybe Expression = Nothing
return Case {..}
goCaseBranch :: Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.CaseBranch -> Sem r CaseBranch
goCaseBranch b = do
_caseBranchPattern <- goPatternArg (b ^. Abstract.caseBranchPattern)
_caseBranchExpression <- goExpression (b ^. Abstract.caseBranchExpression)
return CaseBranch {..}
goLet :: forall r. (Members '[NameIdGen, Reader NameDependencyInfo] r) => Abstract.Let -> Sem r Let
goLet l = do
_letExpression <- goExpression (l ^. Abstract.letExpression)
mutualBlocks <- mapM goFunctionDef funDefs >>= buildLetMutualBlocks
let _letClauses = nonEmpty' (map goLetClauses mutualBlocks)
return Let {..}
where
funDefs :: [Abstract.FunctionDef]
funDefs = [f | Abstract.LetFunDef f <- toList (l ^. Abstract.letClauses)]
goLetClauses :: SCC FunctionDef -> LetClause
goLetClauses = \case
AcyclicSCC f -> LetFunDef f
CyclicSCC m -> LetMutualBlock (MutualBlockLet (nonEmpty' m))
goInductiveParameter :: Abstract.FunctionParameter -> Sem r InductiveParameter
goInductiveParameter f =
case (f ^. Abstract.paramName, f ^. Abstract.paramType) of
(Just var, Abstract.ExpressionUniverse u)
| isSmallUni u ->
return
InductiveParameter
{ _inductiveParamName = var
}
(Just {}, _) -> unsupported "only type variables of small types are allowed"
(Nothing, _) -> unsupported "unnamed inductive parameters"
goInductiveDef :: forall r. Members '[NameIdGen, Reader NameDependencyInfo] r => Abstract.InductiveDef -> Sem r InductiveDef
goInductiveDef i
| not (isSmallType (i ^. Abstract.inductiveType)) = unsupported "inductive indices"
| otherwise = do
inductiveParameters' <- mapM goInductiveParameter (i ^. Abstract.inductiveParameters)
let indTypeName = i ^. Abstract.inductiveName
inductiveConstructors' <-
mapM
goConstructorDef
(i ^. Abstract.inductiveConstructors)
examples' <- mapM goExample (i ^. Abstract.inductiveExamples)
return
InductiveDef
{ _inductiveName = indTypeName,
_inductiveParameters = inductiveParameters',
_inductiveBuiltin = i ^. Abstract.inductiveBuiltin,
_inductiveConstructors = inductiveConstructors',
_inductiveExamples = examples',
_inductivePositive = i ^. Abstract.inductivePositive,
_inductivePragmas = i ^. Abstract.inductivePragmas
}
where
goConstructorDef :: Abstract.InductiveConstructorDef -> Sem r InductiveConstructorDef
goConstructorDef c = do
(cParams, cReturnType) <- viewConstructorType (c ^. Abstract.constructorType)
examples' <- mapM goExample (c ^. Abstract.constructorExamples)
return
InductiveConstructorDef
{ _inductiveConstructorName = c ^. Abstract.constructorName,
_inductiveConstructorParameters = cParams,
_inductiveConstructorExamples = examples',
_inductiveConstructorReturnType = cReturnType,
_inductiveConstructorPragmas = c ^. Abstract.constructorPragmas
}
goTypeApplication :: Abstract.Application -> Sem r Application
goTypeApplication (Abstract.Application l r i) = do
l' <- goType l
r' <- goType r
return (Application l' r' i)
viewConstructorType :: Abstract.Expression -> Sem r ([Expression], Expression)
viewConstructorType = \case
Abstract.ExpressionFunction f -> first toList <$> viewFunctionType f
Abstract.ExpressionIden i -> return ([], ExpressionIden (goTypeIden i))
Abstract.ExpressionHole h -> return ([], ExpressionHole h)
Abstract.ExpressionApplication a -> do
a' <- goTypeApplication a
return ([], ExpressionApplication a')
Abstract.ExpressionUniverse u -> return ([], smallUniverseE (getLoc u))
Abstract.ExpressionLiteral {} -> unsupported "literal in a type"
Abstract.ExpressionLambda {} -> unsupported "lambda in a constructor type"
Abstract.ExpressionLet {} -> unsupported "let in a constructor type"
Abstract.ExpressionCase {} -> unsupported "case in a constructor type"
where
viewFunctionType :: Abstract.Function -> Sem r (NonEmpty Expression, Expression)
viewFunctionType (Abstract.Function p r) = do
(args, ret) <- viewConstructorType r
p' <- goFunctionParameter p
return $ case p' ^. paramName of
Just {} -> unsupported "named argument in constructor type"
Nothing -> (p' ^. paramType :| args, ret)

View File

@ -1,6 +0,0 @@
module Juvix.Compiler.Internal.Translation.FromAbstract.Data
( module Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context,
)
where
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context

View File

@ -1,27 +0,0 @@
module Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
( module Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context,
module Juvix.Compiler.Internal.Data.InfoTable,
)
where
import Juvix.Compiler.Abstract.Data.NameDependencyInfo qualified as DepInfo
import Juvix.Compiler.Abstract.Translation.FromConcrete.Data.Context qualified as Abstract
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped
import Juvix.Compiler.Internal.Data.InfoTable
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Pipeline.EntryPoint qualified as E
import Juvix.Prelude
data InternalResult = InternalResult
{ _resultAbstract :: Abstract.AbstractResult,
_resultModules :: NonEmpty Module,
_resultDepInfo :: DepInfo.NameDependencyInfo
}
makeLenses ''InternalResult
internalJuvixResultEntryPoint :: Lens' InternalResult E.EntryPoint
internalJuvixResultEntryPoint = resultAbstract . Abstract.abstractResultEntryPoint
internalJuvixResultScoped :: Lens' InternalResult Scoped.ScoperResult
internalJuvixResultScoped = resultAbstract . Abstract.resultScoper

View File

@ -0,0 +1,866 @@
module Juvix.Compiler.Internal.Translation.FromConcrete
( module Juvix.Compiler.Internal.Translation.FromConcrete,
module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
)
where
import Data.HashMap.Strict qualified as HashMap
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Builtins
import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
import Juvix.Compiler.Concrete.Extra qualified as Concrete
import Juvix.Compiler.Concrete.Language qualified as Concrete
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
import Juvix.Compiler.Internal.Data.NameDependencyInfo qualified as Internal
import Juvix.Compiler.Internal.Extra.DependencyBuilder
import Juvix.Compiler.Internal.Language (varFromWildcard)
import Juvix.Compiler.Internal.Language qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Checker
import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Data.NameKind
import Juvix.Prelude
type MCache = Cache Concrete.ModuleIndex Internal.Module
unsupported :: Text -> a
unsupported msg = error $ msg <> "Scoped to Internal: not yet supported"
fromConcrete ::
Members '[Reader EntryPoint, Error JuvixError, Builtins, NameIdGen] r =>
Scoper.ScoperResult ->
Sem r InternalResult
fromConcrete _resultScoper =
mapError (JuvixError @ScoperError) $ do
(modulesCache, _resultModules) <-
runReader @Pragmas mempty
. runReader @ExportsTable exportTbl
. runCacheEmpty goModuleNoCache
$ mapM goTopModule ms
let _resultTable = buildTable _resultModules
_resultDepInfo = buildDependencyInfo _resultModules exportTbl
_resultModulesCache = ModulesCache modulesCache
return InternalResult {..}
where
ms = _resultScoper ^. Scoper.resultModules
exportTbl = _resultScoper ^. Scoper.resultExports
-- | `StatementInclude`s are no included in the result
buildMutualBlocks ::
Members '[Reader Internal.NameDependencyInfo] r =>
[Internal.PreStatement] ->
Sem r [SCC Internal.PreStatement]
buildMutualBlocks ss = do
depInfo <- ask
let scomponents :: [SCC Internal.Name] = buildSCCs depInfo
return (boolHack (mapMaybe nameToPreStatement scomponents))
where
-- If the builtin bool definition is found, it is moved at the front.
--
-- This is a hack needed to translate BuiltinStringToNat in
-- internal-to-core. BuiltinStringToNat is the only function that depends on
-- Bool implicitly (i.e. without mentioning it in its type). Eventually
-- BuiltinStringToNat needs to be removed and so this hack.
boolHack :: [SCC Internal.PreStatement] -> [SCC Internal.PreStatement]
boolHack s = case popFirstJust isBuiltinBool s of
(Nothing, _) -> s
(Just boolDef, rest) -> AcyclicSCC (Internal.PreInductiveDef boolDef) : rest
where
isBuiltinBool :: SCC Internal.PreStatement -> Maybe Internal.InductiveDef
isBuiltinBool = \case
CyclicSCC [Internal.PreInductiveDef b]
| Just BuiltinBool <- b ^. Internal.inductiveBuiltin -> Just b
_ -> Nothing
statementsByName :: HashMap Internal.Name Internal.PreStatement
statementsByName = HashMap.fromList (map mkAssoc ss)
where
mkAssoc :: Internal.PreStatement -> (Internal.Name, Internal.PreStatement)
mkAssoc s = case s of
Internal.PreInductiveDef i -> (i ^. Internal.inductiveName, s)
Internal.PreFunctionDef i -> (i ^. Internal.funDefName, s)
Internal.PreAxiomDef i -> (i ^. Internal.axiomName, s)
getStmt :: Internal.Name -> Maybe Internal.PreStatement
getStmt n = statementsByName ^. at n
nameToPreStatement :: SCC Internal.Name -> Maybe (SCC Internal.PreStatement)
nameToPreStatement = nonEmptySCC . fmap getStmt
where
nonEmptySCC :: SCC (Maybe a) -> Maybe (SCC a)
nonEmptySCC = \case
AcyclicSCC a -> AcyclicSCC <$> a
CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
buildLetMutualBlocks ::
NonEmpty Internal.PreLetStatement ->
NonEmpty (SCC Internal.PreLetStatement)
buildLetMutualBlocks ss = nonEmpty' . mapMaybe nameToPreStatement $ scomponents
where
-- TODO buildDependencyInfoLet is repeating too much work when there are big nested lets
depInfo = buildDependencyInfoLet ss
scomponents :: [SCC Internal.Name] = buildSCCs depInfo
statementsByName :: HashMap Internal.Name Internal.PreLetStatement
statementsByName = HashMap.fromList (map mkAssoc (toList ss))
where
mkAssoc :: Internal.PreLetStatement -> (Internal.Name, Internal.PreLetStatement)
mkAssoc s = case s of
Internal.PreLetFunctionDef i -> (i ^. Internal.funDefName, s)
getStmt :: Internal.Name -> Maybe Internal.PreLetStatement
getStmt n = statementsByName ^. at n
nameToPreStatement :: SCC Internal.Name -> Maybe (SCC Internal.PreLetStatement)
nameToPreStatement = nonEmptySCC . fmap getStmt
where
nonEmptySCC :: SCC (Maybe a) -> Maybe (SCC a)
nonEmptySCC = \case
AcyclicSCC a -> AcyclicSCC <$> a
CyclicSCC p -> CyclicSCC . toList <$> nonEmpty (catMaybes p)
fromConcreteExpression :: (Members '[Error JuvixError, NameIdGen] r) => Scoper.Expression -> Sem r Internal.Expression
fromConcreteExpression = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goExpression
fromConcreteImport ::
Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r =>
Scoper.Import 'Scoped ->
Sem r Internal.Import
fromConcreteImport =
mapError (JuvixError @ScoperError)
. runReader @Pragmas mempty
. goImport
fromConcreteOpenImport ::
Members '[Reader ExportsTable, Error JuvixError, NameIdGen, Builtins, MCache] r =>
Scoper.OpenModule 'Scoped ->
Sem r (Maybe Internal.Import)
fromConcreteOpenImport = mapError (JuvixError @ScoperError) . runReader @Pragmas mempty . goOpenModule'
goLocalModule ::
Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
Module 'Scoped 'ModuleLocal ->
Sem r [Internal.PreStatement]
goLocalModule = concatMapM goStatement . (^. moduleBody)
goTopModule ::
Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
Module 'Scoped 'ModuleTop ->
Sem r Internal.Module
goTopModule = cacheGet . ModuleIndex
goModuleNoCache ::
Members '[Reader EntryPoint, Reader ExportsTable, Error JuvixError, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
ModuleIndex ->
Sem r Internal.Module
goModuleNoCache (ModuleIndex m) = do
p <- toPreModule m
tbl <- ask
let depInfo = buildDependencyInfoPreModule p tbl
r <- runReader depInfo (fromPreModule p)
noTerminationOption <- asks (^. entryPointNoTermination)
-- TODO we should reuse this table
let itbl = buildTableShallow r
unless
noTerminationOption
( mapError
(JuvixError @TerminationError)
(checkTermination itbl r)
)
return r
goPragmas :: Member (Reader Pragmas) r => Maybe ParsedPragmas -> Sem r Pragmas
goPragmas p = do
p' <- ask
return $ p' <> p ^. _Just . withLocParam . withSourceValue
goName :: S.Name -> Internal.Name
goName name =
set Internal.namePretty prettyStr (goSymbol (S.nameUnqualify name))
where
prettyStr :: Text
prettyStr = prettyText name
goSymbol :: S.Symbol -> Internal.Name
goSymbol s = goSymbolPretty (S.symbolText s) s
goSymbolPretty :: Text -> S.Symbol -> Internal.Name
goSymbolPretty pp s =
Internal.Name
{ _nameText = S.symbolText s,
_nameId = s ^. S.nameId,
_nameKind = getNameKind s,
_namePretty = pp,
_nameLoc = s ^. S.nameConcrete . symbolLoc,
_nameFixity = s ^. S.nameFixity
}
-- TODO give a better name?
traverseM' ::
forall r s t a b.
(Monad r, Monad s, Traversable t) =>
(a -> r (s b)) ->
t a ->
r (s (t b))
traverseM' f x = sequence <$> traverse f x
toPreModule ::
forall r t.
(SingI t, Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r) =>
Module 'Scoped t ->
Sem r Internal.PreModule
toPreModule Module {..} = do
pragmas' <- goPragmas _modulePragmas
body' <- local (const pragmas') (goModuleBody _moduleBody)
examples' <- goExamples _moduleDoc
return
Internal.Module
{ _moduleName = name',
_moduleBody = body',
_moduleExamples = examples',
_modulePragmas = pragmas'
}
where
name' :: Internal.Name
name' = case sing :: SModuleIsTop t of
SModuleTop -> goTopModulePath _modulePath
SModuleLocal -> goSymbol _modulePath
goTopModulePath :: S.TopModulePath -> Internal.Name
goTopModulePath p = goSymbolPretty (prettyText p) (S.topModulePathName p)
fromPreModule ::
forall r.
Members '[Reader Internal.NameDependencyInfo, Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
Internal.PreModule ->
Sem r Internal.Module
fromPreModule = traverseOf Internal.moduleBody fromPreModuleBody
fromPreModuleBody ::
forall r.
Members '[Reader Internal.NameDependencyInfo, Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
Internal.PreModuleBody ->
Sem r Internal.ModuleBody
fromPreModuleBody b = do
sccs <- buildMutualBlocks (b ^. Internal.moduleStatements)
let moduleStatements' = map goSCC sccs
return (set Internal.moduleStatements moduleStatements' b)
where
goSCC :: SCC Internal.PreStatement -> Internal.Statement
goSCC = \case
AcyclicSCC s -> goAcyclic s
CyclicSCC c -> goCyclic (nonEmpty' c)
where
goCyclic :: NonEmpty Internal.PreStatement -> Internal.Statement
goCyclic c = Internal.StatementMutual (Internal.MutualBlock (goMutual <$> c))
where
goMutual :: Internal.PreStatement -> Internal.MutualStatement
goMutual = \case
Internal.PreInductiveDef i -> Internal.StatementInductive i
Internal.PreFunctionDef i -> Internal.StatementFunction i
_ -> impossible
goAcyclic :: Internal.PreStatement -> Internal.Statement
goAcyclic = \case
Internal.PreInductiveDef i -> one (Internal.StatementInductive i)
Internal.PreFunctionDef i -> one (Internal.StatementFunction i)
Internal.PreAxiomDef i -> Internal.StatementAxiom i
where
one :: Internal.MutualStatement -> Internal.Statement
one = Internal.StatementMutual . Internal.MutualBlock . pure
goModuleBody ::
forall r.
Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
[Statement 'Scoped] ->
Sem r Internal.PreModuleBody
goModuleBody stmts = do
_moduleImports <- mapM goImport (scanImports stmts)
otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goStatement) ss
functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions
let _moduleStatements =
map
(^. indexedThing)
( sortOn
(^. indexedIx)
(otherThanFunctions <> functions)
)
return Internal.ModuleBody {..}
where
ss' = concatMap Concrete.flattenStatement stmts
ss :: [Indexed (Statement 'Scoped)]
ss = zipWith Indexed [0 ..] ss'
compiledFunctions :: Sem r [Indexed Internal.FunctionDef]
compiledFunctions =
sequence
[ Indexed i <$> funDef
| Indexed i sig <- sigs,
let name = sig ^. sigName,
let funDef = goTopFunctionDef sig (getClauses name)
]
where
getClauses :: S.Symbol -> [FunctionClause 'Scoped]
getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
sigs :: [Indexed (TypeSignature 'Scoped)]
sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
scanImports stmts = mconcatMap go stmts
where
go :: Statement 'Scoped -> [Import 'Scoped]
go = \case
StatementImport t -> [t]
StatementModule m -> concatMap go (m ^. moduleBody)
StatementOpenModule o -> maybeToList (openImport o)
StatementInductive {} -> []
StatementFunctionClause {} -> []
StatementTypeSignature {} -> []
StatementAxiom {} -> []
StatementSyntax {} -> []
where
openImport :: OpenModule 'Scoped -> Maybe (Import 'Scoped)
openImport o = case o ^. openModuleImportKw of
Nothing -> Nothing
Just _importKw ->
Just
Import
{ _importModule = case o ^. openModuleName . unModuleRef' of
SModuleTop :&: r -> r
SModuleLocal :&: _ -> impossible,
_importAsName = o ^. openImportAsName,
_importKw
}
goImport ::
forall r.
Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
Import 'Scoped ->
Sem r Internal.Import
goImport Import {..} = do
let m = _importModule ^. moduleRefModule
m' <- goTopModule m
return
( Internal.Import
{ _importModule = Internal.ModuleIndex m'
}
)
guardNotCached :: (Bool, Internal.Module) -> Maybe Internal.Module
guardNotCached (hit, m) = do
guard (not hit)
return m
goStatement ::
forall r.
Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
Statement 'Scoped ->
Sem r [Internal.PreStatement]
goStatement = \case
StatementInductive i -> pure . Internal.PreInductiveDef <$> goInductive i
StatementAxiom d -> pure . Internal.PreAxiomDef <$> goAxiom d
StatementModule f -> goLocalModule f
StatementImport {} -> return []
StatementSyntax {} -> return []
StatementOpenModule {} -> return []
StatementTypeSignature {} -> return []
StatementFunctionClause {} -> return []
goOpenModule' ::
forall r.
Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
OpenModule 'Scoped ->
Sem r (Maybe Internal.Import)
goOpenModule' o =
case o ^. openModuleImportKw of
Just kw ->
case o ^. openModuleName of
ModuleRef' (SModuleTop :&: m) ->
Just
<$> goImport
Import
{ _importKw = kw,
_importModule = m,
_importAsName = o ^. openImportAsName
}
_ -> impossible
Nothing -> return Nothing
goOpenModule ::
forall r.
Members '[Reader ExportsTable, Error ScoperError, Builtins, NameIdGen, Reader Pragmas, MCache] r =>
OpenModule 'Scoped ->
Sem r (Maybe Internal.Import)
goOpenModule o = goOpenModule' o
goLetFunctionDef ::
Members '[NameIdGen, Reader Pragmas, Error ScoperError] r =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Internal.FunctionDef
goLetFunctionDef = goFunctionDefHelper
goFunctionDefHelper ::
forall r.
Members '[NameIdGen, Reader Pragmas, Error ScoperError] r =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Internal.FunctionDef
goFunctionDefHelper sig@TypeSignature {..} clauses = do
let _funDefName = goSymbol _sigName
_funDefTerminating = isJust _sigTerminating
_funDefBuiltin = (^. withLocParam) <$> _sigBuiltin
_funDefType <- goExpression _sigType
_funDefExamples <- goExamples _sigDoc
_funDefPragmas <- goPragmas _sigPragmas
_funDefClauses <- case (_sigBody, nonEmpty clauses) of
(Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig))
(Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses')))
(Just body, Nothing) -> do
body' <- goExpression body
return
( pure
Internal.FunctionClause
{ _clauseName = _funDefName,
_clausePatterns = [],
_clauseBody = body'
}
)
(Nothing, Just clauses') -> mapM goFunctionClause clauses'
return Internal.FunctionDef {..}
goTopFunctionDef ::
forall r.
(Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
TypeSignature 'Scoped ->
[FunctionClause 'Scoped] ->
Sem r Internal.FunctionDef
goTopFunctionDef sig clauses = do
fun <- goFunctionDefHelper sig clauses
whenJust (sig ^. sigBuiltin) (registerBuiltinFunction fun . (^. withLocParam))
return fun
goExamples ::
forall r.
Members '[NameIdGen, Error ScoperError, Reader Pragmas] r =>
Maybe (Judoc 'Scoped) ->
Sem r [Internal.Example]
goExamples = mapM goExample . maybe [] judocExamples
where
goExample :: Example 'Scoped -> Sem r Internal.Example
goExample ex = do
e' <- goExpression (ex ^. exampleExpression)
return
Internal.Example
{ _exampleExpression = e',
_exampleId = ex ^. exampleId
}
goFunctionClause ::
Members '[NameIdGen, Error ScoperError, Reader Pragmas] r =>
FunctionClause 'Scoped ->
Sem r Internal.FunctionClause
goFunctionClause FunctionClause {..} = do
_clausePatterns' <- mapM goPatternArg _clausePatterns
_clauseBody' <- goExpression _clauseBody
return
Internal.FunctionClause
{ _clauseName = goSymbol _clauseOwnerFunction,
_clausePatterns = _clausePatterns',
_clauseBody = _clauseBody'
}
goInductiveParameters ::
Members '[NameIdGen, Error ScoperError, Reader Pragmas] r =>
InductiveParameters 'Scoped ->
Sem r [Internal.InductiveParameter]
goInductiveParameters InductiveParameters {..} = do
paramType' <- goExpression _inductiveParametersType
case paramType' of
Internal.ExpressionUniverse {} -> return ()
_ -> unsupported "only type variables of small types are allowed"
let goInductiveParameter :: S.Symbol -> Internal.InductiveParameter
goInductiveParameter var =
Internal.InductiveParameter
{ _inductiveParamName = goSymbol var
}
return (map goInductiveParameter (toList _inductiveParametersNames))
registerBuiltinInductive ::
(Members '[Error ScoperError, Builtins] r) =>
Internal.InductiveDef ->
BuiltinInductive ->
Sem r ()
registerBuiltinInductive d = \case
BuiltinNat -> registerNatDef d
BuiltinBool -> registerBoolDef d
BuiltinInt -> registerIntDef d
registerBuiltinFunction ::
(Members '[Error ScoperError, Builtins, NameIdGen] r) =>
Internal.FunctionDef ->
BuiltinFunction ->
Sem r ()
registerBuiltinFunction d = \case
BuiltinNatPlus -> registerNatPlus d
BuiltinNatSub -> registerNatSub d
BuiltinNatMul -> registerNatMul d
BuiltinNatUDiv -> registerNatUDiv d
BuiltinNatDiv -> registerNatDiv d
BuiltinNatMod -> registerNatMod d
BuiltinNatLe -> registerNatLe d
BuiltinNatLt -> registerNatLt d
BuiltinNatEq -> registerNatEq d
BuiltinBoolIf -> registerIf d
BuiltinBoolOr -> registerOr d
BuiltinBoolAnd -> registerAnd d
BuiltinIntEq -> registerIntEq d
BuiltinIntSubNat -> registerIntSubNat d
BuiltinIntPlus -> registerIntPlus d
BuiltinIntNegNat -> registerIntNegNat d
BuiltinIntNeg -> registerIntNeg d
BuiltinIntMul -> registerIntMul d
BuiltinIntDiv -> registerIntDiv d
BuiltinIntMod -> registerIntMod d
BuiltinIntSub -> registerIntSub d
BuiltinIntNonNeg -> registerIntNonNeg d
BuiltinIntLe -> registerIntLe d
BuiltinIntLt -> registerIntLt d
BuiltinSeq -> registerSeq d
registerBuiltinAxiom ::
(Members '[Error ScoperError, Builtins, NameIdGen] r) =>
Internal.AxiomDef ->
BuiltinAxiom ->
Sem r ()
registerBuiltinAxiom d = \case
BuiltinIO -> registerIO d
BuiltinIOSequence -> registerIOSequence d
BuiltinIOReadline -> registerIOReadline d
BuiltinNatPrint -> registerNatPrint d
BuiltinNatToString -> registerNatToString d
BuiltinString -> registerString d
BuiltinStringPrint -> registerStringPrint d
BuiltinStringConcat -> registerStringConcat d
BuiltinStringEq -> registerStringEq d
BuiltinStringToNat -> registerStringToNat d
BuiltinBoolPrint -> registerBoolPrint d
BuiltinTrace -> registerTrace d
BuiltinFail -> registerFail d
BuiltinIntToString -> registerIntToString d
BuiltinIntPrint -> registerIntPrint d
goInductive ::
Members '[NameIdGen, Reader Pragmas, Builtins, Error ScoperError] r =>
InductiveDef 'Scoped ->
Sem r Internal.InductiveDef
goInductive ty@InductiveDef {..} = do
_inductiveParameters' <- concatMapM goInductiveParameters _inductiveParameters
_inductiveType' <- mapM goExpression _inductiveType
_inductivePragmas' <- goPragmas _inductivePragmas
_inductiveConstructors' <-
local (const _inductivePragmas') $
mapM goConstructorDef _inductiveConstructors
_inductiveExamples' <- goExamples _inductiveDoc
let loc = getLoc _inductiveName
indDef =
Internal.InductiveDef
{ _inductiveParameters = _inductiveParameters',
_inductiveBuiltin = (^. withLocParam) <$> _inductiveBuiltin,
_inductiveName = goSymbol _inductiveName,
_inductiveType = fromMaybe (Internal.ExpressionUniverse (SmallUniverse loc)) _inductiveType',
_inductiveConstructors = toList _inductiveConstructors',
_inductiveExamples = _inductiveExamples',
_inductivePragmas = _inductivePragmas',
_inductivePositive = isJust (ty ^. inductivePositive)
}
whenJust ((^. withLocParam) <$> _inductiveBuiltin) (registerBuiltinInductive indDef)
return indDef
goConstructorDef ::
Members [NameIdGen, Error ScoperError, Reader Pragmas] r =>
InductiveConstructorDef 'Scoped ->
Sem r Internal.InductiveConstructorDef
goConstructorDef InductiveConstructorDef {..} = do
ty' <- goExpression _constructorType
examples' <- goExamples _constructorDoc
pragmas' <- goPragmas _constructorPragmas
return
Internal.InductiveConstructorDef
{ _inductiveConstructorType = ty',
_inductiveConstructorExamples = examples',
_inductiveConstructorName = goSymbol _constructorName,
_inductiveConstructorPragmas = pragmas'
}
goLiteral :: LiteralLoc -> Internal.LiteralLoc
goLiteral = fmap go
where
go :: Literal -> Internal.Literal
go = \case
LitString s -> Internal.LitString s
LitInteger i -> Internal.LitInteger i
goExpression ::
forall r.
Members [NameIdGen, Error ScoperError, Reader Pragmas] r =>
Expression ->
Sem r Internal.Expression
goExpression = \case
ExpressionIdentifier nt -> return (goIden nt)
ExpressionParensIdentifier nt -> return (goIden nt)
ExpressionApplication a -> Internal.ExpressionApplication <$> goApplication a
ExpressionCase a -> Internal.ExpressionCase <$> goCase a
ExpressionInfixApplication ia -> Internal.ExpressionApplication <$> goInfix ia
ExpressionPostfixApplication pa -> Internal.ExpressionApplication <$> goPostfix pa
ExpressionLiteral l -> return (Internal.ExpressionLiteral (goLiteral l))
ExpressionLambda l -> Internal.ExpressionLambda <$> goLambda l
ExpressionBraces b -> throw (ErrAppLeftImplicit (AppLeftImplicit b))
ExpressionLet l -> Internal.ExpressionLet <$> goLet l
ExpressionUniverse uni -> return (Internal.ExpressionUniverse (goUniverse uni))
ExpressionFunction func -> Internal.ExpressionFunction <$> goFunction func
ExpressionHole h -> return (Internal.ExpressionHole h)
ExpressionIterator i -> goIterator i
where
goIden :: Concrete.ScopedIden -> Internal.Expression
goIden x = Internal.ExpressionIden $ case x of
ScopedAxiom a -> Internal.IdenAxiom (goName (a ^. Concrete.axiomRefName))
ScopedInductive i -> Internal.IdenInductive (goName (i ^. Concrete.inductiveRefName))
ScopedVar v -> Internal.IdenVar (goSymbol v)
ScopedFunction fun -> Internal.IdenFunction (goName (fun ^. Concrete.functionRefName))
ScopedConstructor c -> Internal.IdenConstructor (goName (c ^. Concrete.constructorRefName))
goLet :: Let 'Scoped -> Sem r Internal.Let
goLet l = do
_letExpression <- goExpression (l ^. letExpression)
_letClauses <- goLetClauses (l ^. letClauses)
return Internal.Let {..}
where
goLetClauses :: NonEmpty (LetClause 'Scoped) -> Sem r (NonEmpty Internal.LetClause)
goLetClauses cl = fmap goSCC <$> preLetStatements cl
preLetStatements :: NonEmpty (LetClause 'Scoped) -> Sem r (NonEmpty (SCC Internal.PreLetStatement))
preLetStatements cl = do
pre <- nonEmpty' <$> sequence [Internal.PreLetFunctionDef <$> goSig sig | LetTypeSig sig <- toList cl]
return (buildLetMutualBlocks pre)
where
goSig :: TypeSignature 'Scoped -> Sem r Internal.FunctionDef
goSig sig = goLetFunctionDef sig clauses
where
clauses :: [FunctionClause 'Scoped]
clauses =
[ c | LetFunClause c <- toList cl, sig ^. sigName == c ^. clauseOwnerFunction
]
goSCC :: SCC Internal.PreLetStatement -> Internal.LetClause
goSCC = \case
AcyclicSCC (Internal.PreLetFunctionDef f) -> Internal.LetFunDef f
CyclicSCC fs -> Internal.LetMutualBlock (Internal.MutualBlockLet fs')
where
fs' :: NonEmpty Internal.FunctionDef
fs' = nonEmpty' (map getFun fs)
where
getFun :: Internal.PreLetStatement -> Internal.FunctionDef
getFun = \case
Internal.PreLetFunctionDef f -> f
goApplication :: Application -> Sem r Internal.Application
goApplication (Application l arg) = do
l' <- goExpression l
r' <- goExpression r
return (Internal.Application l' r' i)
where
(r, i) = case arg of
ExpressionBraces b -> (b ^. withLocParam, Implicit)
_ -> (arg, Explicit)
goPostfix :: PostfixApplication -> Sem r Internal.Application
goPostfix (PostfixApplication l op) = do
l' <- goExpression l
let op' = goIden op
return (Internal.Application op' l' Explicit)
goInfix :: InfixApplication -> Sem r Internal.Application
goInfix (InfixApplication l op r) = do
l' <- goExpression l
let op' = goIden op
l'' = Internal.ExpressionApplication (Internal.Application op' l' Explicit)
r' <- goExpression r
return (Internal.Application l'' r' Explicit)
goIterator :: Iterator 'Scoped -> Sem r Internal.Expression
goIterator Iterator {..} = do
inipats' <- mapM goPatternArg inipats
rngpats' <- mapM goPatternArg rngpats
expr <- goExpression _iteratorBody
let lam =
Internal.ExpressionLambda $
Internal.Lambda
{ _lambdaClauses = Internal.LambdaClause (nonEmpty' (inipats' ++ rngpats')) expr :| [],
_lambdaType = Nothing
}
fn = goIden _iteratorName
inivals' <- mapM goExpression inivals
rngvals' <- mapM goExpression rngvals
return $ foldl' mkApp fn (lam : inivals' ++ rngvals')
where
inipats = map (^. initializerPattern) _iteratorInitializers
inivals = map (^. initializerExpression) _iteratorInitializers
rngpats = map (^. rangePattern) _iteratorRanges
rngvals = map (^. rangeExpression) _iteratorRanges
mkApp :: Internal.Expression -> Internal.Expression -> Internal.Expression
mkApp a1 a2 = Internal.ExpressionApplication $ Internal.Application a1 a2 Explicit
goCase :: forall r. Members '[NameIdGen, Error ScoperError, Reader Pragmas] r => Case 'Scoped -> Sem r Internal.Case
goCase c = do
_caseExpression <- goExpression (c ^. caseExpression)
_caseBranches <- mapM goBranch (c ^. caseBranches)
let _caseParens = c ^. caseParens
_caseExpressionType :: Maybe Internal.Expression = Nothing
_caseExpressionWholeType :: Maybe Internal.Expression = Nothing
return Internal.Case {..}
where
goBranch :: CaseBranch 'Scoped -> Sem r Internal.CaseBranch
goBranch b = do
_caseBranchPattern <- goPatternArg (b ^. caseBranchPattern)
_caseBranchExpression <- goExpression (b ^. caseBranchExpression)
return Internal.CaseBranch {..}
goLambda :: forall r. Members '[NameIdGen, Error ScoperError, Reader Pragmas] r => Lambda 'Scoped -> Sem r Internal.Lambda
goLambda l = do
clauses' <- mapM goClause (l ^. lambdaClauses)
return
Internal.Lambda
{ _lambdaClauses = clauses',
_lambdaType = Nothing
}
where
goClause :: LambdaClause 'Scoped -> Sem r Internal.LambdaClause
goClause lc = do
ps' <- mapM goPatternArg (lc ^. lambdaParameters)
b' <- goExpression (lc ^. lambdaBody)
return (Internal.LambdaClause ps' b')
goUniverse :: Universe -> SmallUniverse
goUniverse u
| isSmallUniverse u = SmallUniverse (getLoc u)
| otherwise = error "only small universe is supported"
goFunction :: Members '[NameIdGen, Error ScoperError, Reader Pragmas] r => Function 'Scoped -> Sem r Internal.Function
goFunction f = do
params <- goFunctionParameters (f ^. funParameters)
ret <- goExpression (f ^. funReturn)
return $
Internal.Function (head params) $
foldr (\param acc -> Internal.ExpressionFunction $ Internal.Function param acc) ret (NonEmpty.tail params)
goFunctionParameters ::
Members '[NameIdGen, Error ScoperError, Reader Pragmas] r =>
FunctionParameters 'Scoped ->
Sem r (NonEmpty Internal.FunctionParameter)
goFunctionParameters FunctionParameters {..} = do
_paramType' <- goExpression _paramType
let mkParam param =
Internal.FunctionParameter
{ Internal._paramType = _paramType',
Internal._paramImplicit = _paramImplicit,
Internal._paramName = goSymbol <$> param
}
return . fromMaybe (pure (mkParam Nothing)) . nonEmpty $
mkParam . goFunctionParameter <$> _paramNames
where
goFunctionParameter :: FunctionParameter 'Scoped -> Maybe (SymbolType 'Scoped)
goFunctionParameter = \case
FunctionParameterName n -> Just n
FunctionParameterWildcard {} -> Nothing
mkConstructorApp :: Internal.ConstrName -> [Internal.PatternArg] -> Internal.ConstructorApp
mkConstructorApp a b = Internal.ConstructorApp a b Nothing
goPatternApplication ::
Members '[NameIdGen, Error ScoperError] r =>
PatternApp ->
Sem r Internal.ConstructorApp
goPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternApplication a)
goPatternConstructor ::
Members '[NameIdGen, Error ScoperError] r =>
ConstructorRef ->
Sem r Internal.ConstructorApp
goPatternConstructor a = uncurry mkConstructorApp <$> viewApp (PatternConstructor a)
goInfixPatternApplication ::
Members '[NameIdGen, Error ScoperError] r =>
PatternInfixApp ->
Sem r Internal.ConstructorApp
goInfixPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternInfixApplication a)
goPostfixPatternApplication ::
Members '[NameIdGen, Error ScoperError] r =>
PatternPostfixApp ->
Sem r Internal.ConstructorApp
goPostfixPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternPostfixApplication a)
viewApp :: forall r. Members '[NameIdGen, Error ScoperError] r => Pattern -> Sem r (Internal.ConstrName, [Internal.PatternArg])
viewApp p = case p of
PatternConstructor c -> return (goConstructorRef c, [])
PatternApplication app@(PatternApp _ r) -> do
r' <- goPatternArg r
second (`snoc` r') <$> viewAppLeft app
PatternInfixApplication (PatternInfixApp l c r) -> do
l' <- goPatternArg l
r' <- goPatternArg r
return (goConstructorRef c, [l', r'])
PatternPostfixApplication (PatternPostfixApp l c) -> do
l' <- goPatternArg l
return (goConstructorRef c, [l'])
PatternVariable {} -> err
PatternWildcard {} -> err
PatternEmpty {} -> err
where
viewAppLeft :: PatternApp -> Sem r (Internal.ConstrName, [Internal.PatternArg])
viewAppLeft app@(PatternApp l _)
| Implicit <- l ^. patternArgIsImplicit = throw (ErrImplicitPatternLeftApplication (ImplicitPatternLeftApplication app))
| otherwise = viewApp (l ^. patternArgPattern)
err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p))
goConstructorRef :: ConstructorRef -> Internal.Name
goConstructorRef (ConstructorRef' n) = goName n
goPatternArg :: Members '[NameIdGen, Error ScoperError] r => PatternArg -> Sem r Internal.PatternArg
goPatternArg p = do
pat' <- goPattern (p ^. patternArgPattern)
return
Internal.PatternArg
{ _patternArgIsImplicit = p ^. patternArgIsImplicit,
_patternArgName = goSymbol <$> p ^. patternArgName,
_patternArgPattern = pat'
}
goPattern :: Members '[NameIdGen, Error ScoperError] r => Pattern -> Sem r Internal.Pattern
goPattern p = case p of
PatternVariable a -> return $ Internal.PatternVariable (goSymbol a)
PatternConstructor c -> Internal.PatternConstructorApp <$> goPatternConstructor c
PatternApplication a -> Internal.PatternConstructorApp <$> goPatternApplication a
PatternInfixApplication a -> Internal.PatternConstructorApp <$> goInfixPatternApplication a
PatternPostfixApplication a -> Internal.PatternConstructorApp <$> goPostfixPatternApplication a
PatternWildcard i -> Internal.PatternVariable <$> varFromWildcard i
PatternEmpty {} -> error "unsupported empty pattern"
goAxiom :: (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) => AxiomDef 'Scoped -> Sem r Internal.AxiomDef
goAxiom a = do
_axiomType' <- goExpression (a ^. axiomType)
_axiomPragmas' <- goPragmas (a ^. axiomPragmas)
let axiom =
Internal.AxiomDef
{ _axiomType = _axiomType',
_axiomBuiltin = (^. withLocParam) <$> a ^. axiomBuiltin,
_axiomName = goSymbol (a ^. axiomName),
_axiomPragmas = _axiomPragmas'
}
whenJust (a ^. axiomBuiltin) (registerBuiltinAxiom axiom . (^. withLocParam))
return axiom

View File

@ -0,0 +1,33 @@
module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
( module Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context,
module Juvix.Compiler.Internal.Data.InfoTable,
)
where
import Juvix.Compiler.Concrete.Language qualified as Concrete
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Concrete
import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context qualified as Concrete
import Juvix.Compiler.Internal.Data.InfoTable
import Juvix.Compiler.Internal.Data.NameDependencyInfo
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Language qualified as Internal
import Juvix.Compiler.Pipeline.EntryPoint qualified as E
import Juvix.Prelude
-- | Top modules cache
newtype ModulesCache = ModulesCache
{_cachedModules :: HashMap Concrete.ModuleIndex Internal.Module}
data InternalResult = InternalResult
{ _resultScoper :: Concrete.ScoperResult,
_resultTable :: InfoTable,
_resultModules :: NonEmpty Module,
_resultDepInfo :: NameDependencyInfo,
_resultModulesCache :: ModulesCache
}
makeLenses ''InternalResult
makeLenses ''ModulesCache
internalResultEntryPoint :: Lens' InternalResult E.EntryPoint
internalResultEntryPoint = resultScoper . Concrete.resultParserResult . Concrete.resultEntry

View File

@ -5,8 +5,8 @@ module Juvix.Compiler.Internal.Translation.FromInternal
typeCheckExpression,
typeCheckExpressionType,
arityCheckExpression,
arityCheckInclude,
typeCheckInclude,
arityCheckImport,
typeCheckImport,
)
where
@ -14,7 +14,7 @@ import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Builtins.Effect
import Juvix.Compiler.Concrete.Data.Highlight.Input
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as ArityChecking
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking
@ -29,7 +29,10 @@ arityChecking ::
Sem r ArityChecking.InternalArityResult
arityChecking res@InternalResult {..} =
mapError (JuvixError @ArityChecking.ArityCheckerError) $ do
r <- runReader table (mapM ArityChecking.checkModule _resultModules)
r <-
runReader table
. evalCacheEmpty ArityChecking.checkModuleIndexNoCache
$ mapM ArityChecking.checkModule _resultModules
return
ArityChecking.InternalArityResult
{ _resultInternalResult = res,
@ -46,20 +49,22 @@ arityCheckExpression ::
arityCheckExpression exp = do
table <- extendedTableReplArtifacts exp
mapError (JuvixError @ArityChecking.ArityCheckerError)
$ runReader table
. runNameIdGenArtifacts
. runReader table
. runNameIdGenArtifacts
$ ArityChecking.inferReplExpression exp
arityCheckInclude ::
arityCheckImport ::
Members '[Error JuvixError, State Artifacts] r =>
Include ->
Sem r Include
arityCheckInclude i = do
let table = buildTable [i ^. includeModule]
Import ->
Sem r Import
arityCheckImport i = do
artiTable <- gets (^. artifactInternalTypedTable)
let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable
mapError (JuvixError @ArityChecking.ArityCheckerError)
$ runReader table
. runNameIdGenArtifacts
$ ArityChecking.checkInclude i
. runReader table
. runNameIdGenArtifacts
. evalCacheEmpty ArityChecking.checkModuleIndexNoCache
$ ArityChecking.checkImport i
typeCheckExpressionType ::
forall r.
@ -69,15 +74,15 @@ typeCheckExpressionType ::
typeCheckExpressionType exp = do
table <- extendedTableReplArtifacts exp
mapError (JuvixError @TypeCheckerError)
$ runTypesTableArtifacts
. ignoreHighlightBuilder
. runFunctionsTableArtifacts
. runBuiltinsArtifacts
. runNameIdGenArtifacts
. runReader table
. ignoreOutput @Example
. withEmptyVars
. runInferenceDef
. runTypesTableArtifacts
. ignoreHighlightBuilder
. runFunctionsTableArtifacts
. runBuiltinsArtifacts
. runNameIdGenArtifacts
. runReader table
. ignoreOutput @Example
. withEmptyVars
. runInferenceDef
$ inferExpression' Nothing exp >>= traverseOf typedType strongNormalize
typeCheckExpression ::
@ -86,23 +91,26 @@ typeCheckExpression ::
Sem r Expression
typeCheckExpression exp = (^. typedExpression) <$> typeCheckExpressionType exp
typeCheckInclude ::
typeCheckImport ::
Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r =>
Include ->
Sem r Include
typeCheckInclude i = do
let table = buildTable [i ^. includeModule]
Import ->
Sem r Import
typeCheckImport i = do
artiTable <- gets (^. artifactInternalTypedTable)
let table = buildTable [i ^. importModule . moduleIxModule] <> artiTable
modify (set artifactInternalTypedTable table)
mapError (JuvixError @TypeCheckerError)
$ runTypesTableArtifacts
. runFunctionsTableArtifacts
. ignoreHighlightBuilder
. runBuiltinsArtifacts
. runNameIdGenArtifacts
. ignoreOutput @Example
. runReader table
. withEmptyVars
$ checkInclude i
. runTypesTableArtifacts
. runFunctionsTableArtifacts
. ignoreHighlightBuilder
. runBuiltinsArtifacts
. runNameIdGenArtifacts
. ignoreOutput @Example
. runReader table
. withEmptyVars
-- TODO Store cache in Artifacts and use it here
. evalCacheEmpty checkModuleNoCache
$ checkImport i
typeChecking ::
Members '[HighlightBuilder, Error JuvixError, Builtins, NameIdGen] r =>
@ -116,6 +124,7 @@ typeChecking res@ArityChecking.InternalArityResult {..} =
. runState (mempty :: TypesTable)
. runState (mempty :: FunctionsTable)
. runReader table
. evalCacheEmpty checkModuleNoCache
$ mapM checkModule _resultModules
return
InternalTypedResult

View File

@ -6,18 +6,26 @@ where
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Pretty
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.LocalVars
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Data.Types
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.Error
import Juvix.Data.Effect.NameIdGen
import Juvix.Prelude hiding (fromEither)
type MCache = Cache ModuleIndex Module
checkModule ::
(Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r =>
Module ->
Sem r Module
checkModule Module {..} = do
checkModule = cacheGet . ModuleIndex
checkModuleIndexNoCache ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r =>
ModuleIndex ->
Sem r Module
checkModuleIndexNoCache (ModuleIndex Module {..}) = do
_moduleBody' <- checkModuleBody _moduleBody
return
Module
@ -26,21 +34,29 @@ checkModule Module {..} = do
}
checkModuleBody ::
(Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r =>
ModuleBody ->
Sem r ModuleBody
checkModuleBody ModuleBody {..} = do
_moduleStatements' <- mapM checkStatement _moduleStatements
_moduleImports' <- mapM checkImport _moduleImports
return
ModuleBody
{ _moduleStatements = _moduleStatements'
{ _moduleStatements = _moduleStatements',
_moduleImports = _moduleImports'
}
checkInclude ::
(Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
Include ->
Sem r Include
checkInclude = traverseOf includeModule checkModule
checkModuleIndex ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r =>
ModuleIndex ->
Sem r ModuleIndex
checkModuleIndex (ModuleIndex m) = ModuleIndex <$> checkModule m
checkImport ::
Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError, MCache] r =>
Import ->
Sem r Import
checkImport = traverseOf importModule checkModuleIndex
checkStatement ::
(Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) =>
@ -48,7 +64,6 @@ checkStatement ::
Sem r Statement
checkStatement s = case s of
StatementMutual b -> StatementMutual <$> checkMutualBlock b
StatementInclude i -> StatementInclude <$> checkInclude i
StatementAxiom a -> StatementAxiom <$> checkAxiom a
checkInductive :: forall r. (Members '[Reader InfoTable, NameIdGen, Error ArityCheckerError] r) => InductiveDef -> Sem r InductiveDef
@ -60,6 +75,7 @@ checkInductive d = do
(localVars, _inductiveParameters) <- checkParameters (d ^. inductiveParameters)
_inductiveExamples <- runReader localVars (mapM checkExample (d ^. inductiveExamples))
_inductiveConstructors <- runReader localVars (mapM checkConstructor (d ^. inductiveConstructors))
_inductiveType <- runReader localVars (checkType (d ^. inductiveType))
return InductiveDef {..}
where
checkParameters :: [InductiveParameter] -> Sem r (LocalVars, [InductiveParameter])
@ -72,9 +88,8 @@ checkConstructor :: (Members '[Reader LocalVars, Reader InfoTable, NameIdGen, Er
checkConstructor c = do
let _inductiveConstructorName = c ^. inductiveConstructorName
_inductiveConstructorPragmas = c ^. inductiveConstructorPragmas
_inductiveConstructorParameters <- mapM checkType (c ^. inductiveConstructorParameters)
_inductiveConstructorType <- checkType (c ^. inductiveConstructorType)
_inductiveConstructorExamples <- mapM checkExample (c ^. inductiveConstructorExamples)
_inductiveConstructorReturnType <- checkType (c ^. inductiveConstructorReturnType)
return InductiveConstructorDef {..}
-- | check the arity of some ty : Type
@ -198,7 +213,7 @@ guessArity = \case
Nothing -> ArityUnknown
Just a' -> foldArity (set ufoldArityParams a' u)
where
(f, args) = second (map fst . toList) (unfoldApplication' a)
(f, args) = second (map (^. appArgIsImplicit) . toList) (unfoldApplication' a)
refine :: [IsImplicit] -> [ArityParameter] -> Maybe [ArityParameter]
refine as ps = case (as, ps) of
@ -355,7 +370,7 @@ checkConstructorApp ::
Sem r ConstructorApp
checkConstructorApp ca = do
let c = ca ^. constrAppConstructor
args <- (^. constructorInfoArgs) <$> lookupConstructor c
args <- constructorArgs . (^. constructorInfoType) <$> lookupConstructor c
let arities = map typeArity args
n = length arities
ps = ca ^. constrAppParameters
@ -448,7 +463,7 @@ checkLambda ari l = do
idenArity :: (Members '[Reader LocalVars, Reader InfoTable] r) => Iden -> Sem r Arity
idenArity = \case
IdenVar v -> getLocalArity v
IdenInductive i -> typeArity <$> inductiveType i
IdenInductive i -> typeArity <$> lookupInductiveType i
IdenFunction f -> typeArity . (^. functionInfoDef . funDefType) <$> lookupFunction f
IdenConstructor c -> typeArity <$> constructorType c
IdenAxiom a -> typeArity . (^. axiomInfoDef . axiomType) <$> lookupAxiom a
@ -542,7 +557,7 @@ checkExpression hintArity expr = case expr of
_paramType <- checkType (p ^. paramType)
return FunctionParameter {..}
goApp :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
goApp :: Expression -> [ApplicationArg] -> Sem r Expression
goApp f args = do
case f of
ExpressionIden (IdenAxiom n) -> do
@ -561,7 +576,7 @@ checkExpression hintArity expr = case expr of
_ -> appHelper f args
_ -> appHelper f args
goBuiltinApp :: Name -> Int -> Int -> Expression -> [(IsImplicit, Expression)] -> Sem r Expression
goBuiltinApp :: Name -> Int -> Int -> Expression -> [ApplicationArg] -> Sem r Expression
goBuiltinApp n implArgsNum argsNum f args = do
args' <- goImplArgs implArgsNum args
if
@ -574,15 +589,15 @@ checkExpression hintArity expr = case expr of
_builtinNotFullyAplliedExpectedArgsNum = argsNum
}
where
goImplArgs :: Int -> [(IsImplicit, Expression)] -> Sem r [(IsImplicit, Expression)]
goImplArgs :: Int -> [ApplicationArg] -> Sem r [ApplicationArg]
goImplArgs 0 as = return as
goImplArgs k ((Implicit, _) : as) = goImplArgs (k - 1) as
goImplArgs k ((ApplicationArg Implicit _) : as) = goImplArgs (k - 1) as
goImplArgs _ as = return as
appHelper :: Expression -> [(IsImplicit, Expression)] -> Sem r Expression
appHelper :: Expression -> [ApplicationArg] -> Sem r Expression
appHelper fun0 args = do
(fun', args') :: (Expression, [(IsImplicit, Expression)]) <- case fun0 of
ExpressionHole {} -> (fun0,) <$> mapM (secondM (checkExpression ArityUnknown)) args
(fun', args') :: (Expression, [ApplicationArg]) <- case fun0 of
ExpressionHole {} -> (fun0,) <$> mapM (traverseOf appArg (checkExpression ArityUnknown)) args
ExpressionIden i -> (fun0,) <$> (idenArity i >>= helper (getLoc i))
ExpressionLiteral l -> (fun0,) <$> helper (getLoc l) arityLiteral
ExpressionUniverse l -> (fun0,) <$> helper (getLoc l) arityUniverse
@ -607,7 +622,7 @@ checkExpression hintArity expr = case expr of
ExpressionApplication {} -> impossible
return (foldApplication fun' args')
where
helper :: Interval -> Arity -> Sem r [(IsImplicit, Expression)]
helper :: Interval -> Arity -> Sem r [ApplicationArg]
helper i ari = do
let argsAris :: [Arity]
argsAris = map toArity (unfoldArity ari)
@ -615,36 +630,36 @@ checkExpression hintArity expr = case expr of
toArity = \case
ParamExplicit a -> a
ParamImplicit -> ArityUnit
argsWithHoles :: [(IsImplicit, Expression)] <- addHoles i hintArity ari args
argsWithHoles :: [ApplicationArg] <- addHoles i hintArity ari args
let argsWithAris :: [(IsImplicit, (Arity, Expression))]
argsWithAris = [(i', (a, e')) | (a, (i', e')) <- zip (argsAris ++ repeat ArityUnknown) argsWithHoles]
mapM (secondM (uncurry checkExpression)) argsWithAris
argsWithAris = [(i', (a, e')) | (a, (ApplicationArg i' e')) <- zip (argsAris ++ repeat ArityUnknown) argsWithHoles]
mapM (fmap (uncurry ApplicationArg) . secondM (uncurry checkExpression)) argsWithAris
addHoles ::
Interval ->
Arity ->
Arity ->
[(IsImplicit, Expression)] ->
Sem r [(IsImplicit, Expression)]
[ApplicationArg] ->
Sem r [ApplicationArg]
addHoles loc hint = go 0
where
go ::
Int ->
Arity ->
[(IsImplicit, Expression)] ->
Sem r [(IsImplicit, Expression)]
[ApplicationArg] ->
Sem r [ApplicationArg]
go idx ari goargs = case (ari, goargs) of
(ArityFunction (FunctionArity ParamImplicit r), (Implicit, e) : rest) ->
((Implicit, e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity (ParamExplicit {}) r), (Explicit, e) : rest) ->
((Explicit, e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity ParamImplicit r), (ApplicationArg Implicit e) : rest) ->
((ApplicationArg Implicit e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity (ParamExplicit {}) r), (ApplicationArg Explicit e) : rest) ->
((ApplicationArg Explicit e) :) <$> go (succ idx) r rest
(ArityFunction (FunctionArity ParamImplicit _), [])
-- When there are no remaining arguments and the expected arity of the
-- expression matches the current arity we should *not* insert a hole.
| ari == hint -> return []
(ArityFunction (FunctionArity ParamImplicit r), _) -> do
h <- newHole loc
((Implicit, ExpressionHole h) :) <$> go (succ idx) r goargs
(ArityFunction (FunctionArity (ParamExplicit {}) _), (Implicit, _) : _) ->
((ApplicationArg Implicit (ExpressionHole h)) :) <$> go (succ idx) r goargs
(ArityFunction (FunctionArity (ParamExplicit {}) _), (ApplicationArg Implicit _) : _) ->
throw
( ErrExpectedExplicitArgument
ExpectedExplicitArgument

View File

@ -2,7 +2,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking.D
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context qualified as Scoped
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context qualified as Internal
import Juvix.Compiler.Pipeline.EntryPoint qualified as E
import Juvix.Prelude
@ -17,7 +17,7 @@ mainModule :: Lens' InternalArityResult Module
mainModule = resultModules . _head1
internalArityResultEntryPoint :: Lens' InternalArityResult E.EntryPoint
internalArityResultEntryPoint = resultInternalResult . Internal.internalJuvixResultEntryPoint
internalArityResultEntryPoint = resultInternalResult . Internal.internalResultEntryPoint
internalArityResultScoped :: Lens' InternalArityResult Scoped.ScoperResult
internalArityResultScoped = resultInternalResult . Internal.internalJuvixResultScoped
internalArityResultScoped = resultInternalResult . Internal.resultScoper

View File

@ -102,7 +102,7 @@ instance ToGenericError WrongPatternIsImplicit where
<+> ppCode opts' pat
data ExpectedExplicitArgument = ExpectedExplicitArgument
{ _expectedExplicitArgumentApp :: (Expression, [(IsImplicit, Expression)]),
{ _expectedExplicitArgumentApp :: (Expression, [ApplicationArg]),
_expectedExplicitArgumentIx :: Int
}
@ -122,8 +122,8 @@ instance ToGenericError ExpectedExplicitArgument where
opts' = fromGenericOptions opts
app@(f, args) = e ^. expectedExplicitArgumentApp
idx = e ^. expectedExplicitArgumentIx
arg :: Expression
arg = snd (toList args !! idx)
arg :: ApplicationArg
arg = (toList args !! idx)
i = getLoc arg
msg =
"Expected an explicit argument as the"
@ -131,7 +131,7 @@ instance ToGenericError ExpectedExplicitArgument where
<+> "argument of"
<+> ppCode opts' f
<+> "but found"
<+> ppArg opts' Implicit arg
<+> ppArg opts' arg
<> "."
<> softline
<> "In the application"
@ -162,7 +162,7 @@ instance ToGenericError PatternFunction where
<+> "Function types cannot be pattern matched"
data TooManyArguments = TooManyArguments
{ _tooManyArgumentsApp :: (Expression, [(IsImplicit, Expression)]),
{ _tooManyArgumentsApp :: (Expression, [ApplicationArg]),
_tooManyArgumentsUnexpected :: Int
}
@ -180,13 +180,13 @@ instance ToGenericError TooManyArguments where
}
where
opts' = fromGenericOptions opts
i = getLocSpan (fromJust (nonEmpty (map snd unexpectedArgs)))
i = getLocSpan (nonEmpty' (map (^. appArg) unexpectedArgs))
(fun, args) = e ^. tooManyArgumentsApp
numUnexpected :: Int
numUnexpected = e ^. tooManyArgumentsUnexpected
unexpectedArgs :: [(IsImplicit, Expression)]
unexpectedArgs :: [ApplicationArg]
unexpectedArgs = reverse . take numUnexpected . reverse $ args
ppUnexpectedArgs = hsep (map (uncurry (ppArg opts')) unexpectedArgs)
ppUnexpectedArgs = hsep (map (ppArg opts') unexpectedArgs)
app :: Expression
app = foldApplication fun args
msg =
@ -207,7 +207,7 @@ instance ToGenericError TooManyArguments where
data FunctionApplied = FunctionApplied
{ _functionAppliedFunction :: Function,
_functionAppliedArguments :: [(IsImplicit, Expression)]
_functionAppliedArguments :: [ApplicationArg]
}
makeLenses ''FunctionApplied
@ -224,7 +224,7 @@ instance ToGenericError FunctionApplied where
}
where
opts' = fromGenericOptions opts
i = getLocSpan (fun :| map snd args)
i = getLocSpan (fun :| map (^. appArg) args)
args = e ^. functionAppliedArguments
fun = ExpressionFunction (e ^. functionAppliedFunction)
msg =

View File

@ -39,10 +39,11 @@ checkPositivity ty = do
noCheckPositivity <- asks (^. E.entryPointNoPositivity)
forM_ (ty ^. inductiveConstructors) $ \ctor -> do
let ctorName = ctor ^. inductiveConstructorName
args = constructorArgs (ctor ^. inductiveConstructorType)
unless (noCheckPositivity || ty ^. inductivePositive) $
mapM_
forM_
args
(checkStrictlyPositiveOccurrences ty ctorName indName numInductives Nothing)
(ctor ^. inductiveConstructorParameters)
checkStrictlyPositiveOccurrences ::
forall r.
@ -155,7 +156,8 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref =
when (recLimit > 0) $
forM_ (indType' ^. inductiveConstructors) $ \ctor' -> do
let ctorName' = ctor' ^. inductiveConstructorName
let errorRef = fromMaybe tyArg ref
errorRef = fromMaybe tyArg ref
args = constructorArgs (ctor' ^. inductiveConstructorType)
mapM_
( checkStrictlyPositiveOccurrences
indType'
@ -164,7 +166,7 @@ checkStrictlyPositiveOccurrences ty ctorName name recLimit ref =
(recLimit - 1)
(Just errorRef)
)
(ctor' ^. inductiveConstructorParameters)
args
helperInductiveApp indType' ps
[] -> return ()

View File

@ -1,53 +1,68 @@
module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability where
module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Reachability (filterUnreachable) where
import Juvix.Compiler.Abstract.Data.NameDependencyInfo
import Juvix.Compiler.Internal.Data.NameDependencyInfo
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Translation.FromAbstract.Data.Context
import Juvix.Compiler.Internal.Translation.FromConcrete.Data.Context
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.ArityChecking qualified as Arity
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context qualified as Typed
import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Prelude
type MCache = Cache ModuleIndex Module
filterUnreachable :: Members '[Reader EntryPoint] r => Typed.InternalTypedResult -> Sem r Typed.InternalTypedResult
filterUnreachable r = do
asks (^. entryPointSymbolPruningMode) >>= \case
KeepAll -> return r
FilterUnreachable -> return (set Typed.resultModules modules' r)
where
depInfo = r ^. (Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo)
depInfo = r ^. Typed.resultInternalArityResult . Arity.resultInternalResult . resultDepInfo
modules = r ^. Typed.resultModules
modules' = run $ runReader depInfo (mapM goModule modules)
modules' =
run
. runReader depInfo
. evalCacheEmpty goModuleNoCache
$ mapM goModule modules
askIsReachable :: Member (Reader NameDependencyInfo) r => Name -> Sem r Bool
askIsReachable n = do
depInfo <- ask
return (isReachable depInfo n)
returnIfReachable :: (Member (Reader NameDependencyInfo) r) => Name -> a -> Sem r (Maybe a)
returnIfReachable :: Member (Reader NameDependencyInfo) r => Name -> a -> Sem r (Maybe a)
returnIfReachable n a = do
r <- askIsReachable n
return
if
| r -> Just a
| otherwise -> Nothing
return (guard r $> a)
goModule :: (Member (Reader NameDependencyInfo) r) => Module -> Sem r Module
goModule m = do
stmts <- mapM goStatement (body ^. moduleStatements)
return m {_moduleBody = body {_moduleStatements = catMaybes stmts}}
goModuleNoCache :: forall r. Members [Reader NameDependencyInfo, MCache] r => ModuleIndex -> Sem r Module
goModuleNoCache (ModuleIndex m) = do
body' <- goBody (m ^. moduleBody)
return (set moduleBody body' m)
where
body = m ^. moduleBody
goBody :: ModuleBody -> Sem r ModuleBody
goBody body = do
_moduleStatements <- mapMaybeM goStatement (body ^. moduleStatements)
_moduleImports <- mapM goImport (body ^. moduleImports)
return ModuleBody {..}
goModule :: Members [Reader NameDependencyInfo, MCache] r => Module -> Sem r Module
goModule = cacheGet . ModuleIndex
goModuleIndex :: Members [Reader NameDependencyInfo, MCache] r => ModuleIndex -> Sem r ModuleIndex
goModuleIndex = fmap ModuleIndex . cacheGet
goStatement :: forall r. Member (Reader NameDependencyInfo) r => Statement -> Sem r (Maybe Statement)
goStatement s = case s of
StatementMutual m -> fmap StatementMutual <$> goMutual m
StatementAxiom ax -> returnIfReachable (ax ^. axiomName) s
StatementInclude i -> do
m <- goModule (i ^. includeModule)
return (Just (StatementInclude i {_includeModule = m}))
where
-- note that the first mutual statement is reachable iff all are reachable
goMutual :: MutualBlock -> Sem r (Maybe MutualBlock)
goMutual b@(MutualBlock (m :| _)) = case m of
StatementFunction f -> returnIfReachable (f ^. funDefName) b
StatementInductive f -> returnIfReachable (f ^. inductiveName) b
goImport :: forall r. Members [Reader NameDependencyInfo, MCache] r => Import -> Sem r Import
goImport i = do
_importModule <- goModuleIndex (i ^. importModule)
return Import {..}

View File

@ -18,6 +18,8 @@ import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Data.Effect.NameIdGen
import Juvix.Prelude hiding (fromEither)
type MCache = Cache ModuleIndex Module
registerConstructor :: Members '[HighlightBuilder, State TypesTable, Reader InfoTable] r => InductiveConstructorDef -> Sem r ()
registerConstructor ctr = do
ty <- constructorType (ctr ^. inductiveConstructorName)
@ -29,10 +31,22 @@ registerNameIdType uid ty = do
modify (set (highlightTypes . at uid) (Just ty))
checkModule ::
(Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r =>
Module ->
Sem r Module
checkModule Module {..} = do
checkModule = cacheGet . ModuleIndex
checkModuleIndex ::
Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r =>
ModuleIndex ->
Sem r ModuleIndex
checkModuleIndex = fmap ModuleIndex . cacheGet
checkModuleNoCache ::
Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r =>
ModuleIndex ->
Sem r Module
checkModuleNoCache (ModuleIndex Module {..}) = do
_moduleBody' <-
(evalState (mempty :: NegativeTypeParameters) . checkModuleBody) _moduleBody
return
@ -42,21 +56,23 @@ checkModule Module {..} = do
}
checkModuleBody ::
(Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r =>
ModuleBody ->
Sem r ModuleBody
checkModuleBody ModuleBody {..} = do
_moduleStatements' <- mapM checkStatement _moduleStatements
_moduleImports' <- mapM checkImport _moduleImports
return
ModuleBody
{ _moduleStatements = _moduleStatements'
{ _moduleStatements = _moduleStatements',
_moduleImports = _moduleImports'
}
checkInclude ::
(Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
Include ->
Sem r Include
checkInclude = traverseOf includeModule checkModule
checkImport ::
Members '[HighlightBuilder, Reader EntryPoint, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins, MCache] r =>
Import ->
Sem r Import
checkImport = traverseOf importModule checkModuleIndex
checkStatement ::
(Members '[HighlightBuilder, Reader EntryPoint, State NegativeTypeParameters, Reader InfoTable, Error TypeCheckerError, NameIdGen, State TypesTable, State FunctionsTable, Output Example, Builtins] r) =>
@ -64,7 +80,6 @@ checkStatement ::
Sem r Statement
checkStatement s = case s of
StatementMutual mut -> StatementMutual <$> runReader emptyLocalVars (checkTopMutualBlock mut)
StatementInclude i -> StatementInclude <$> checkInclude i
StatementAxiom ax -> do
registerNameIdType (ax ^. axiomName . nameId) (ax ^. axiomType)
return s
@ -76,13 +91,15 @@ checkInductiveDef ::
Sem r InductiveDef
checkInductiveDef InductiveDef {..} = runInferenceDef $ do
constrs' <- mapM goConstructor _inductiveConstructors
ty <- inductiveType _inductiveName
ty <- lookupInductiveType _inductiveName
registerNameIdType (_inductiveName ^. nameId) ty
examples' <- mapM checkExample _inductiveExamples
inductiveType' <- runReader paramLocals (checkDefType _inductiveType)
let d =
InductiveDef
{ _inductiveConstructors = constrs',
_inductiveExamples = examples',
_inductiveType = inductiveType',
_inductiveName,
_inductiveBuiltin,
_inductivePositive,
@ -101,23 +118,22 @@ checkInductiveDef InductiveDef {..} = runInferenceDef $ do
goConstructor :: InductiveConstructorDef -> Sem (Inference ': r) InductiveConstructorDef
goConstructor InductiveConstructorDef {..} = do
expectedRetTy <- constructorReturnType _inductiveConstructorName
cty' <- runReader paramLocals $ do
void (checkIsType (getLoc ret) ret)
mapM (checkIsType (getLoc _inductiveConstructorName)) _inductiveConstructorParameters
cty' <-
runReader paramLocals $
checkIsType (getLoc _inductiveConstructorType) _inductiveConstructorType
examples' <- mapM checkExample _inductiveConstructorExamples
whenJustM (matchTypes expectedRetTy ret) (const (errRet expectedRetTy))
let c' =
InductiveConstructorDef
{ _inductiveConstructorParameters = cty',
{ _inductiveConstructorType = cty',
_inductiveConstructorExamples = examples',
_inductiveConstructorReturnType,
_inductiveConstructorName,
_inductiveConstructorPragmas
}
registerConstructor c'
return c'
where
ret = _inductiveConstructorReturnType
ret = snd (viewConstructorType _inductiveConstructorType)
errRet :: Expression -> Sem (Inference ': r) a
errRet expected =
throw
@ -154,7 +170,7 @@ checkFunctionDef ::
Sem r FunctionDef
checkFunctionDef FunctionDef {..} = do
funDef <- do
_funDefType' <- checkFunctionDefType _funDefType
_funDefType' <- checkDefType _funDefType
registerIdenType _funDefName _funDefType'
_funDefClauses' <- mapM (checkFunctionClause _funDefType') _funDefClauses
return
@ -173,12 +189,12 @@ checkIsType ::
Sem r Expression
checkIsType = checkExpression . smallUniverseE
checkFunctionDefType ::
checkDefType ::
forall r.
(Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, Error TypeCheckerError, NameIdGen, Reader LocalVars, Inference, Builtins, Output Example, State TypesTable] r) =>
Expression ->
Sem r Expression
checkFunctionDefType ty = checkIsType loc ty
checkDefType ty = checkIsType loc ty
where
loc = getLoc ty
@ -245,9 +261,9 @@ checkConstructorReturnType ::
Sem r ()
checkConstructorReturnType indType ctor = do
let ctorName = ctor ^. inductiveConstructorName
ctorReturnType = ctor ^. inductiveConstructorReturnType
tyName = indType ^. inductiveName
indParams = map (^. inductiveParamName) (indType ^. inductiveParameters)
ctorReturnType = snd (viewConstructorType (ctor ^. inductiveConstructorType))
expectedReturnType =
foldExplicitApplication
(ExpressionIden (IdenInductive tyName))
@ -401,7 +417,7 @@ checkPattern = go
indName = IdenInductive (info ^. constructorInfoInductive)
loc = getLoc a
paramHoles <- map ExpressionHole <$> replicateM numIndParams (freshHole loc)
let patternTy = foldApplication (ExpressionIden indName) (map (Explicit,) paramHoles)
let patternTy = foldApplication (ExpressionIden indName) (map (ApplicationArg Explicit) paramHoles)
whenJustM
(matchTypes patternTy (ExpressionHole hole))
err
@ -485,9 +501,6 @@ checkPattern = go
)
return (Right (ind, zipExact params args))
freshHole :: (Members '[Inference, NameIdGen] r) => Interval -> Sem r Hole
freshHole l = mkHole l <$> freshNameId
inferExpression' ::
forall r.
(Members '[HighlightBuilder, Reader InfoTable, State FunctionsTable, State TypesTable, Reader LocalVars, Error TypeCheckerError, NameIdGen, Inference, Output Example, Builtins] r) =>
@ -699,7 +712,7 @@ inferExpression' hint e = case e of
info <- lookupAxiom v
return (TypedExpression (info ^. axiomInfoDef . axiomType) (ExpressionIden i))
IdenInductive v -> do
kind <- inductiveType v
kind <- lookupInductiveType v
return (TypedExpression kind (ExpressionIden i))
goApplication :: Application -> Sem r TypedExpression

View File

@ -21,11 +21,13 @@ runPP opts = highlight_ . run . runReader opts
highlight_ :: Doc Ann -> Doc Ann
highlight_ = annotate AnnCode
ppApp :: Micro.Options -> (Expression, [(IsImplicit, Expression)]) -> Doc Ann
ppApp :: Micro.Options -> (Expression, [ApplicationArg]) -> Doc Ann
ppApp opts (fun, args) =
hsep (ppAtom opts fun : map (uncurry (ppArg opts)) args)
hsep (ppAtom opts fun : map (ppArg opts) args)
ppArg :: Micro.Options -> IsImplicit -> Expression -> Doc Ann
ppArg opts im arg = case im of
Implicit -> braces (ppCode opts arg)
Explicit -> ppAtom opts arg
ppArg :: Micro.Options -> ApplicationArg -> Doc Ann
ppArg opts arg = case arg ^. appArgIsImplicit of
Implicit -> braces (ppCode opts e)
Explicit -> ppAtom opts e
where
e = arg ^. appArg

View File

@ -6,7 +6,6 @@ module Juvix.Compiler.Pipeline
)
where
import Juvix.Compiler.Abstract.Translation qualified as Abstract
import Juvix.Compiler.Asm.Error qualified as Asm
import Juvix.Compiler.Asm.Options qualified as Asm
import Juvix.Compiler.Asm.Pipeline qualified as Asm
@ -57,15 +56,10 @@ upToScoping ::
Sem r Scoper.ScoperResult
upToScoping = upToParsing >>= Scoper.fromParsed
upToAbstract ::
(Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
Sem r Abstract.AbstractResult
upToAbstract = upToScoping >>= Abstract.fromConcrete
upToInternal ::
(Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
Sem r Internal.InternalResult
upToInternal = upToAbstract >>= Internal.fromAbstract
upToInternal = upToScoping >>= Internal.fromConcrete
upToInternalArity ::
(Members '[HighlightBuilder, Reader EntryPoint, Files, NameIdGen, Builtins, Error JuvixError, PathResolver] r) =>
@ -236,16 +230,19 @@ corePipelineIOEither entry = do
typedTable :: Internal.InfoTable
typedTable = typedResult ^. Typed.resultInfoTable
internalResult :: Internal.InternalResult
internalResult =
typedResult
^. Typed.resultInternalArityResult
. Arity.resultInternalResult
coreTable :: Core.InfoTable
coreTable = coreRes ^. Core.coreResultTable
scopedResult :: Scoped.ScoperResult
scopedResult =
typedResult
^. Typed.resultInternalArityResult
. Arity.resultInternalResult
. Internal.resultAbstract
. Abstract.resultScoper
internalResult
^. Internal.resultScoper
parserResult :: P.ParserResult
parserResult = scopedResult ^. Scoped.resultParserResult
@ -255,23 +252,19 @@ corePipelineIOEither entry = do
mainModuleScope_ :: Scope
mainModuleScope_ = Scoped.mainModuleSope scopedResult
abstractResult :: Abstract.AbstractResult
abstractResult = typedResult ^. Typed.resultInternalArityResult . Arity.resultInternalResult . Internal.resultAbstract
in Right $
foldl'
(flip ($))
art
[ set artifactMainModuleScope (Just mainModuleScope_),
set artifactParsing (parserResult ^. P.resultBuilderState),
set artifactAbstractInfoTable (abstractResult ^. Abstract.resultTable),
set artifactInternalModuleCache (internalResult ^. Internal.resultModulesCache),
set artifactInternalTypedTable typedTable,
set artifactCoreTable coreTable,
set artifactScopeTable resultScoperTable,
set artifactScopeExports (scopedResult ^. Scoped.resultExports),
set artifactTypes typesTable,
set artifactFunctions functionsTable,
set artifactAbstractModuleCache (abstractResult ^. Abstract.resultModulesCache),
set artifactScoperState (scopedResult ^. Scoped.resultScoperState)
]
where
@ -279,7 +272,6 @@ corePipelineIOEither entry = do
initialArtifacts =
Artifacts
{ _artifactParsing = Concrete.iniState,
_artifactAbstractInfoTable = Abstract.emptyInfoTable,
_artifactMainModuleScope = Nothing,
_artifactInternalTypedTable = mempty,
_artifactTypes = mempty,
@ -290,7 +282,6 @@ corePipelineIOEither entry = do
_artifactScopeTable = Scoped.emptyInfoTable,
_artifactBuiltins = iniBuiltins,
_artifactScopeExports = mempty,
_artifactInternalTranslationState = Internal.TranslationState mempty,
_artifactAbstractModuleCache = Abstract.ModulesCache mempty,
_artifactInternalModuleCache = Internal.ModulesCache mempty,
_artifactScoperState = Scoper.iniScoperState
}

View File

@ -5,8 +5,6 @@
-- `runStateLikeArtifacts` wrapper.
module Juvix.Compiler.Pipeline.Artifacts where
import Juvix.Compiler.Abstract.Data.InfoTableBuilder qualified as Abstract
import Juvix.Compiler.Abstract.Translation.FromConcrete qualified as Abstract
import Juvix.Compiler.Builtins
import Juvix.Compiler.Concrete.Data.InfoTable qualified as Scoped
import Juvix.Compiler.Concrete.Data.InfoTableBuilder qualified as Scoped
@ -16,10 +14,11 @@ import Juvix.Compiler.Concrete.Data.Scope
import Juvix.Compiler.Concrete.Data.Scope qualified as S
import Juvix.Compiler.Concrete.Data.Scope qualified as Scoped
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping (ScoperError)
import Juvix.Compiler.Core.Data.InfoTableBuilder qualified as Core
import Juvix.Compiler.Internal.Data.InfoTable qualified as Internal
import Juvix.Compiler.Internal.Extra.DependencyBuilder (ExportsTable)
import Juvix.Compiler.Internal.Language qualified as Internal
import Juvix.Compiler.Internal.Translation.FromAbstract qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.TypeChecking.Data.Context
import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Prelude
@ -28,7 +27,6 @@ import Juvix.Prelude
-- restarted while preserving existing state.
data Artifacts = Artifacts
{ _artifactParsing :: BuilderState,
_artifactAbstractInfoTable :: Abstract.InfoTable,
-- Scoping
_artifactResolver :: ResolverState,
_artifactBuiltins :: BuiltinsState,
@ -37,15 +35,13 @@ data Artifacts = Artifacts
_artifactScopeExports :: HashSet NameId,
_artifactMainModuleScope :: Maybe Scope,
_artifactScoperState :: Scoped.ScoperState,
-- Concrete -> Internal
_artifactInternalModuleCache :: Internal.ModulesCache,
-- Typechecking
_artifactTypes :: TypesTable,
_artifactFunctions :: FunctionsTable,
-- | This includes the InfoTable from all type checked modules
_artifactInternalTypedTable :: Internal.InfoTable,
-- Concrete -> Abstract
_artifactAbstractModuleCache :: Abstract.ModulesCache,
-- Abstract -> Internal
_artifactInternalTranslationState :: Internal.TranslationState,
-- Core
_artifactCoreTable :: Core.InfoTable
}
@ -72,9 +68,6 @@ runPathResolverArtifacts = runStateLikeArtifacts runPathResolverPipe' artifactRe
runBuiltinsArtifacts :: Members '[Error JuvixError, State Artifacts] r => Sem (Builtins ': r) a -> Sem r a
runBuiltinsArtifacts = runStateLikeArtifacts runBuiltins artifactBuiltins
runAbstractInfoTableBuilderArtifacts :: Members '[State Artifacts] r => Sem (Abstract.InfoTableBuilder : r) a -> Sem r a
runAbstractInfoTableBuilderArtifacts = runStateLikeArtifacts Abstract.runInfoTableBuilder' artifactAbstractInfoTable
runParserInfoTableBuilderArtifacts :: Members '[State Artifacts] r => Sem (Concrete.InfoTableBuilder : r) a -> Sem r a
runParserInfoTableBuilderArtifacts = runStateLikeArtifacts Concrete.runParserInfoTableBuilderRepl artifactParsing
@ -122,3 +115,23 @@ runStateLikeArtifacts runEff l m = do
(s', a) <- runEff s m
modify' (set l s')
return a
runCacheArtifacts ::
(Hashable k, Members '[State Artifacts] r) =>
Lens' Artifacts (HashMap k v) ->
(k -> Sem (Cache k v ': r) v) ->
(Sem (Cache k v ': r) a) ->
Sem r a
runCacheArtifacts l f = runStateLikeArtifacts (runCache f) l
runFromConcreteCache ::
Members '[Reader EntryPoint, State Artifacts, Builtins, NameIdGen, Reader ExportsTable, Error JuvixError] r =>
Sem (Internal.MCache ': r) a ->
Sem r a
runFromConcreteCache =
runCacheArtifacts
(artifactInternalModuleCache . Internal.cachedModules)
( mapError (JuvixError @ScoperError)
. runReader (mempty :: Pragmas)
. Internal.goModuleNoCache
)

View File

@ -1,6 +1,7 @@
module Juvix.Compiler.Pipeline.Repl where
import Juvix.Compiler.Abstract.Translation qualified as Abstract
import Juvix.Compiler.Builtins (Builtins)
import Juvix.Compiler.Concrete.Data.InfoTableBuilder qualified as Concrete
import Juvix.Compiler.Concrete.Data.ParsedInfoTableBuilder.BuilderState qualified as C
import Juvix.Compiler.Concrete.Data.Scope qualified as Scoper
import Juvix.Compiler.Concrete.Language
@ -9,6 +10,7 @@ import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
import Juvix.Compiler.Concrete.Translation.FromSource qualified as Parser
import Juvix.Compiler.Core qualified as Core
import Juvix.Compiler.Internal qualified as Internal
import Juvix.Compiler.Internal.Translation.FromConcrete qualified as FromConcrete
import Juvix.Compiler.Pipeline.Artifacts
import Juvix.Compiler.Pipeline.EntryPoint
import Juvix.Prelude
@ -24,8 +26,7 @@ arityCheckExpression p = do
. runScoperScopeArtifacts
)
$ Scoper.scopeCheckExpression scopeTable p
>>= Abstract.fromConcreteExpression
>>= Internal.fromAbstractExpression
>>= Internal.fromConcreteExpression
>>= Internal.arityCheckExpression
expressionUpToAtomsParsed ::
@ -63,57 +64,54 @@ scopeCheckExpression p = do
. Scoper.scopeCheckExpression scopeTable
$ p
runToInternal ::
Members '[Reader EntryPoint, State Artifacts, Error JuvixError] r =>
Sem
( State Scoper.ScoperState
: FromConcrete.MCache
: Reader Scoper.ScopeParameters
: Reader (HashSet NameId)
: State Scoper.Scope
: Concrete.InfoTableBuilder
: Builtins
: NameIdGen
: r
)
b ->
Sem r b
runToInternal m = do
parsedModules <- gets (^. artifactParsing . C.stateModules)
runNameIdGenArtifacts
. runBuiltinsArtifacts
. runScoperInfoTableBuilderArtifacts
. runScoperScopeArtifacts
. runReaderArtifacts artifactScopeExports
. runReader (Scoper.ScopeParameters mempty parsedModules)
. runFromConcreteCache
. runStateArtifacts artifactScoperState
$ m
openImportToInternal ::
Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r =>
OpenModule 'Parsed ->
Sem r (Maybe Internal.Include)
openImportToInternal o = do
parsedModules <- gets (^. artifactParsing . C.stateModules)
( runNameIdGenArtifacts
. runBuiltinsArtifacts
. runAbstractInfoTableBuilderArtifacts
. runScoperInfoTableBuilderArtifacts
. runScoperScopeArtifacts
. runStateArtifacts artifactInternalTranslationState
. runReaderArtifacts artifactScopeExports
. runReader (Scoper.ScopeParameters mempty parsedModules)
. runStateArtifacts artifactAbstractModuleCache
. runStateArtifacts artifactScoperState
)
$ do
mTopModule <-
Scoper.scopeCheckOpenModule o
>>= Abstract.fromConcreteOpenImport
case mTopModule of
Nothing -> return Nothing
Just m -> Internal.fromAbstractImport m
Sem r (Maybe Internal.Import)
openImportToInternal o = runToInternal $ do
Scoper.scopeCheckOpenModule o
>>= Internal.fromConcreteOpenImport
importToInternal ::
Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r =>
Import 'Parsed ->
Sem r (Maybe Internal.Include)
importToInternal i = do
parsedModules <- gets (^. artifactParsing . C.stateModules)
( runNameIdGenArtifacts
. runBuiltinsArtifacts
. runAbstractInfoTableBuilderArtifacts
. runScoperInfoTableBuilderArtifacts
. runScoperScopeArtifacts
. runStateArtifacts artifactInternalTranslationState
. runReaderArtifacts artifactScopeExports
. runReader (Scoper.ScopeParameters mempty parsedModules)
. runStateArtifacts artifactAbstractModuleCache
. runStateArtifacts artifactScoperState
)
$ Scoper.scopeCheckImport i
>>= Abstract.fromConcreteImport
>>= Internal.fromAbstractImport
Sem r Internal.Import
importToInternal i = runToInternal $ do
Scoper.scopeCheckImport i
>>= Internal.fromConcreteImport
importToInternal' ::
Members '[Reader EntryPoint, Error JuvixError, State Artifacts] r =>
Internal.Include ->
Sem r Internal.Include
importToInternal' = Internal.arityCheckInclude >=> Internal.typeCheckInclude
Internal.Import ->
Sem r Internal.Import
importToInternal' = Internal.arityCheckImport >=> Internal.typeCheckImport
parseReplInput ::
Members '[PathResolver, Files, State Artifacts, Error JuvixError] r =>
@ -121,10 +119,9 @@ parseReplInput ::
Text ->
Sem r Parser.ReplInput
parseReplInput fp txt =
( runNameIdGenArtifacts
. runBuiltinsArtifacts
. runParserInfoTableBuilderArtifacts
)
runNameIdGenArtifacts
. runBuiltinsArtifacts
. runParserInfoTableBuilderArtifacts
$ Parser.replInputFromTextSource fp txt
expressionUpToTyped ::
@ -150,27 +147,29 @@ registerImport ::
Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r =>
Import 'Parsed ->
Sem r ()
registerImport i = do
mInclude <- importToInternal i
whenJust mInclude (importToInternal' >=> fromInternalInclude)
registerImport =
importToInternal >=> importToInternal' >=> fromInternalImport
registerOpenImport ::
Members '[Error JuvixError, State Artifacts, Reader EntryPoint] r =>
OpenModule 'Parsed ->
Sem r ()
registerOpenImport o = do
mInclude <- openImportToInternal o
whenJust mInclude (importToInternal' >=> fromInternalInclude)
mImport <- openImportToInternal o
whenJust mImport (importToInternal' >=> fromInternalImport)
fromInternalInclude :: Members '[State Artifacts] r => Internal.Include -> Sem r ()
fromInternalInclude i = do
let table = Internal.buildTable [i ^. Internal.includeModule]
fromInternalImport :: Members '[State Artifacts] r => Internal.Import -> Sem r ()
fromInternalImport i = do
artiTable <- gets (^. artifactInternalTypedTable)
let table = Internal.buildTable [i ^. Internal.importModule . Internal.moduleIxModule] <> artiTable
runReader table
. runCoreInfoTableBuilderArtifacts
. runFunctionsTableArtifacts
. readerTypesTableArtifacts
. runReader Core.initIndexTable
$ Core.goModule (i ^. Internal.includeModule)
-- TODO add cache in Artifacts
. evalVisitEmpty Core.goModuleNoVisit
$ Core.goModule (i ^. Internal.importModule . Internal.moduleIxModule)
fromInternalExpression :: Members '[State Artifacts] r => Internal.Expression -> Sem r Core.Node
fromInternalExpression exp = do

View File

@ -1,12 +1,16 @@
module Juvix.Data.Effect
( module Juvix.Data.Effect.Fail,
module Juvix.Data.Effect.Files,
module Juvix.Data.Effect.Cache,
module Juvix.Data.Effect.NameIdGen,
module Juvix.Data.Effect.Visit,
module Juvix.Data.Effect.Log,
)
where
import Juvix.Data.Effect.Cache
import Juvix.Data.Effect.Fail
import Juvix.Data.Effect.Files
import Juvix.Data.Effect.Log
import Juvix.Data.Effect.NameIdGen hiding (toState)
import Juvix.Data.Effect.Visit

View File

@ -0,0 +1,71 @@
module Juvix.Data.Effect.Cache
( runCache,
evalCache,
evalCacheEmpty,
runCacheEmpty,
cacheGet,
cacheLookup,
Cache,
)
where
import Juvix.Prelude.Base
data Cache k v m a where
CacheGet :: k -> Cache k v m v
CacheLookup :: k -> Cache k v m (Maybe v)
makeSem ''Cache
-- | Run a 'Cache' effect purely.
runCache ::
Hashable k =>
(k -> Sem (Cache k v ': r) v) ->
HashMap k v ->
Sem (Cache k v ': r) a ->
Sem r (HashMap k v, a)
runCache f c = runState c . re f
{-# INLINE runCache #-}
evalCache ::
Hashable k =>
(k -> Sem (Cache k v ': r) v) ->
HashMap k v ->
Sem (Cache k v ': r) a ->
Sem r a
evalCache f c = fmap snd . runCache f c
{-# INLINE evalCache #-}
evalCacheEmpty ::
Hashable k =>
(k -> Sem (Cache k v ': r) v) ->
Sem (Cache k v ': r) a ->
Sem r a
evalCacheEmpty f = evalCache f mempty
{-# INLINE evalCacheEmpty #-}
runCacheEmpty ::
Hashable k =>
(k -> Sem (Cache k v ': r) v) ->
Sem (Cache k v ': r) a ->
Sem r (HashMap k v, a)
runCacheEmpty f = runCache f mempty
{-# INLINE runCacheEmpty #-}
re ::
forall k v r a.
Hashable k =>
(k -> Sem (Cache k v ': r) v) ->
Sem (Cache k v ': r) a ->
Sem (State (HashMap k v) ': r) a
re f = reinterpret $ \case
CacheLookup k -> gets @(HashMap k v) (^. at k)
CacheGet k -> do
mv <- gets @(HashMap k v) (^. at k)
case mv of
Nothing -> do
x <- re f (f k)
modify' @(HashMap k v) (set (at k) (Just x))
return x
Just v -> return v
{-# INLINE re #-}

View File

@ -0,0 +1,66 @@
-- | Visit every key at most once
module Juvix.Data.Effect.Visit
( runVisit,
runVisitEmpty,
evalVisit,
evalVisitEmpty,
Visit,
visit,
)
where
import Data.HashSet qualified as HashSet
import Juvix.Prelude.Base
data Visit k m a where
Visit :: k -> Visit k m ()
makeSem ''Visit
-- | Run a 'Visit' effect purely.
runVisit ::
Hashable k =>
(k -> Sem (Visit k ': r) ()) ->
HashSet k ->
Sem (Visit k ': r) a ->
Sem r (HashSet k, a)
runVisit f c = runState c . re f
{-# INLINE runVisit #-}
runVisitEmpty ::
Hashable k =>
(k -> Sem (Visit k ': r) ()) ->
Sem (Visit k ': r) a ->
Sem r (HashSet k, a)
runVisitEmpty f = runVisit f mempty
{-# INLINE runVisitEmpty #-}
evalVisitEmpty ::
Hashable k =>
(k -> Sem (Visit k ': r) ()) ->
Sem (Visit k ': r) a ->
Sem r a
evalVisitEmpty f = fmap snd . runVisitEmpty f
{-# INLINE evalVisitEmpty #-}
evalVisit ::
Hashable k =>
(k -> Sem (Visit k ': r) ()) ->
HashSet k ->
Sem (Visit k ': r) a ->
Sem r a
evalVisit f c = fmap snd . runVisit f c
{-# INLINE evalVisit #-}
re ::
forall k r a.
Hashable k =>
(k -> Sem (Visit k ': r) ()) ->
Sem (Visit k ': r) a ->
Sem (State (HashSet k) ': r) a
re vis = reinterpret $ \case
Visit k ->
unlessM (HashSet.member k <$> get @(HashSet k)) $ do
modify' (HashSet.insert k)
re vis (vis k)
{-# INLINE re #-}

View File

@ -57,8 +57,11 @@ smallUniverse = mkUniverse (Just smallLevel)
isSmallUniverse :: Universe -> Bool
isSmallUniverse = (== smallLevel) . getUniverseLevel
smallUniverseNoLoc :: Universe
smallUniverseNoLoc = smallUniverse (error "Universe with no location")
smallUniverseNoLoc :: SmallUniverse
smallUniverseNoLoc = SmallUniverse (error "SmallUniverse with no location")
isSmallUni :: Universe -> Bool
isSmallUni u = 0 == fromMaybe defaultLevel (u ^. universeLevel)
instance HasAtomicity Universe where
atomicity u = case u ^. universeLevel of

View File

@ -4,6 +4,7 @@ module Juvix.Prelude
module Juvix.Prelude.Trace,
module Juvix.Prelude.Path,
module Juvix.Prelude.Prepath,
module Juvix.Prelude.Tagged,
module Juvix.Data,
)
where
@ -13,4 +14,5 @@ import Juvix.Prelude.Base
import Juvix.Prelude.Lens
import Juvix.Prelude.Path
import Juvix.Prelude.Prepath
import Juvix.Prelude.Tagged
import Juvix.Prelude.Trace

View File

@ -58,6 +58,7 @@ module Juvix.Prelude.Base
module Polysemy.Fixpoint,
module Polysemy.Output,
module Polysemy.Reader,
module Polysemy.Tagged,
module Polysemy.Resource,
module Polysemy.State,
module Language.Haskell.TH.Syntax,
@ -163,6 +164,7 @@ import Polysemy.Output
import Polysemy.Reader
import Polysemy.Resource
import Polysemy.State
import Polysemy.Tagged hiding (tag)
import Prettyprinter (Doc, (<+>))
import Safe.Exact
import Safe.Foldable
@ -192,8 +194,6 @@ import Text.Show qualified as Show
import Text.Show.Unicode (urecover, ushow)
import Prelude (Double)
--------------------------------------------------------------------------------
traverseM ::
(Monad m, Traversable m, Applicative f) =>
(a1 -> f (m a2)) ->

View File

@ -0,0 +1,12 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
-- | This module requires AllowAmbiguousTypes, so it is separated from Base
module Juvix.Prelude.Tagged where
import Polysemy
import Polysemy.Tagged hiding (tag)
import Polysemy.Tagged qualified as Polysemy
-- | We rename it to ptag to avoid clashes with the commonly used `tag` identifier.
ptag :: forall k e r a. Member (Tagged k e) r => Sem (e ': r) a -> Sem r a
ptag = Polysemy.tag @k

View File

@ -175,7 +175,7 @@ tests =
$(mkRelFile "HigherOrderLambda.juvix")
$(mkRelFile "out/HigherOrderLambda.out"),
PosTest
"Type Aliases"
"Type Aliases (Church)"
$(mkRelDir ".")
$(mkRelFile "Church.juvix")
$(mkRelFile "out/Church.out"),

View File

@ -42,13 +42,14 @@ testDescr PosTest {..} =
check n = assertBool ("unreachable not filtered: " ++ unpack n) (HashSet.member (unpack n) _reachable)
getNames :: Internal.Module -> [Text]
getNames m = concatMap getDeclName (m ^. (Internal.moduleBody . Internal.moduleStatements))
getNames m =
concatMap getDeclName (m ^. Internal.moduleBody . Internal.moduleStatements)
<> concatMap (getNames . (^. Internal.importModule . Internal.moduleIxModule)) (m ^. Internal.moduleBody . Internal.moduleImports)
where
getDeclName :: Internal.Statement -> [Text]
getDeclName = \case
Internal.StatementMutual (Internal.MutualBlock f) -> map getMutualName (toList f)
Internal.StatementAxiom ax -> [ax ^. (Internal.axiomName . Internal.nameText)]
Internal.StatementInclude i -> getNames (i ^. Internal.includeModule)
getMutualName :: Internal.MutualStatement -> Text
getMutualName = \case
Internal.StatementFunction f -> f ^. Internal.funDefName . Internal.nameText

View File

@ -24,7 +24,7 @@ testDescr NegTest {..} =
_testRoot = tRoot,
_testAssertion = Single $ do
entryPoint <- defaultEntryPointCwdIO file'
res <- runIOEither entryPoint upToAbstract
res <- runIOEither entryPoint upToInternal
case mapLeft fromJuvixError res of
Left (Just err) -> whenJust (_checkErr err) assertFailure
Left Nothing -> assertFailure "An error ocurred but it was not in the scoper."