anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2024-08-17 04:01:05 +03:00
Code Issues Projects Releases Wiki Activity

Reduce Internal boilerplate (#2874)

Browse Source 
This pr modifies the `HasExpressions` class to allow traversing direct
subexpressions rather than only leaf expressions. I've added the `lens`
library as a dependency to have access to generic traversals defined in
[Control.Lens.Plated](https://hackage.haskell.org/package/lens-5.3.2/docs/Control-Lens-Plated.html).
This commit is contained in:
Jan Mas Rovira 2024-07-09 23:39:19 +02:00 committed by GitHub
parent d08bf942b6
commit 840b7e95a6
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
18 changed files with 371 additions and 501 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
package.yaml
View File

@ -78,7 +78,7 @@ dependencies:
- megaparsec == 9.6.*
- commonmark == 0.2.*
- parsec == 3.1.*
- microlens-platform == 0.4.*
- lens == 5.2.*
- parser-combinators == 1.3.*
- path == 0.9.*
- path-io == 1.8.*

3
src/Juvix/Compiler/Concrete/Data/Highlight/Properties.hs
View File

@ -6,7 +6,6 @@ import Data.Aeson.TH
import Juvix.Data.Emacs
import Juvix.Extra.Strings qualified as Str
import Juvix.Prelude
import Lens.Micro.Platform qualified as Lens
data GenericProperty = GenericProperty
{ _gpropProperty :: Text,
@ -111,7 +110,7 @@ type RawType = Text
$( deriveToJSON
defaultOptions
{ fieldLabelModifier = over Lens._head toLower . dropPrefix "_rawProperties",
{ fieldLabelModifier = over _head toLower . dropPrefix "_rawProperties",
constructorTagModifier = map toLower
}
''RawProperties

39
src/Juvix/Compiler/Concrete/Language.hs
View File

@ -21,7 +21,6 @@ module Juvix.Compiler.Concrete.Language
)
where
import Data.Kind qualified as GHC
import Juvix.Compiler.Backend.Markdown.Data.Types (Mk)
import Juvix.Compiler.Concrete.Data.Builtins
import Juvix.Compiler.Concrete.Data.IfBranchKind
@ -49,100 +48,100 @@ import Juvix.Prelude.Pretty (Pretty, pretty, prettyText)
type Delims = Irrelevant (Maybe (KeywordRef, KeywordRef))
type RecordUpdateExtraType :: Stage -> GHC.Type
type RecordUpdateExtraType :: Stage -> GHCType
type family RecordUpdateExtraType s = res | res -> s where
RecordUpdateExtraType 'Parsed = ()
RecordUpdateExtraType 'Scoped = RecordUpdateExtra
type FieldArgIxType :: Stage -> GHC.Type
type FieldArgIxType :: Stage -> GHCType
type family FieldArgIxType s = res | res -> s where
FieldArgIxType 'Parsed = ()
FieldArgIxType 'Scoped = Int
type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type
type SideIfBranchConditionType :: Stage -> IfBranchKind -> GHCType
type family SideIfBranchConditionType s k = res where
SideIfBranchConditionType s 'BranchIfBool = ExpressionType s
SideIfBranchConditionType _ 'BranchIfElse = ()
type IfBranchConditionType :: Stage -> IfBranchKind -> GHC.Type
type IfBranchConditionType :: Stage -> IfBranchKind -> GHCType
type family IfBranchConditionType s k = res where
IfBranchConditionType s 'BranchIfBool = ExpressionType s
IfBranchConditionType _ 'BranchIfElse = Irrelevant KeywordRef
type ModuleIdType :: Stage -> ModuleIsTop -> GHC.Type
type ModuleIdType :: Stage -> ModuleIsTop -> GHCType
type family ModuleIdType s t = res where
ModuleIdType 'Parsed _ = ()
ModuleIdType 'Scoped 'ModuleLocal = ()
ModuleIdType 'Scoped 'ModuleTop = ModuleId
type SymbolType :: Stage -> GHC.Type
type SymbolType :: Stage -> GHCType
type family SymbolType s = res | res -> s where
SymbolType 'Parsed = Symbol
SymbolType 'Scoped = S.Symbol
type IdentifierType :: Stage -> GHC.Type
type IdentifierType :: Stage -> GHCType
type family IdentifierType s = res | res -> s where
IdentifierType 'Parsed = Name
IdentifierType 'Scoped = ScopedIden
type HoleType :: Stage -> GHC.Type
type HoleType :: Stage -> GHCType
type family HoleType s = res | res -> s where
HoleType 'Parsed = KeywordRef
HoleType 'Scoped = Hole
type PatternAtomIdenType :: Stage -> GHC.Type
type PatternAtomIdenType :: Stage -> GHCType
type family PatternAtomIdenType s = res | res -> s where
PatternAtomIdenType 'Parsed = Name
PatternAtomIdenType 'Scoped = PatternScopedIden
type ExpressionType :: Stage -> GHC.Type
type ExpressionType :: Stage -> GHCType
type family ExpressionType s = res | res -> s where
ExpressionType 'Parsed = ExpressionAtoms 'Parsed
ExpressionType 'Scoped = Expression
type PatternAtomType :: Stage -> GHC.Type
type PatternAtomType :: Stage -> GHCType
type family PatternAtomType s = res | res -> s where
PatternAtomType 'Parsed = PatternAtom 'Parsed
PatternAtomType 'Scoped = PatternArg
type PatternParensType :: Stage -> GHC.Type
type PatternParensType :: Stage -> GHCType
type family PatternParensType s = res | res -> s where
PatternParensType 'Parsed = PatternAtoms 'Parsed
PatternParensType 'Scoped = PatternArg
type PatternAtType :: Stage -> GHC.Type
type PatternAtType :: Stage -> GHCType
type family PatternAtType s = res | res -> s where
PatternAtType 'Parsed = PatternBinding
PatternAtType 'Scoped = PatternArg
type NameSignatureType :: Stage -> GHC.Type
type NameSignatureType :: Stage -> GHCType
type family NameSignatureType s = res | res -> s where
NameSignatureType 'Parsed = ()
NameSignatureType 'Scoped = NameSignature 'Scoped
type ModulePathType :: Stage -> ModuleIsTop -> GHC.Type
type ModulePathType :: Stage -> ModuleIsTop -> GHCType
type family ModulePathType s t = res | res -> t s where
ModulePathType 'Parsed 'ModuleTop = TopModulePath
ModulePathType 'Scoped 'ModuleTop = S.TopModulePath
ModulePathType 'Parsed 'ModuleLocal = Symbol
ModulePathType 'Scoped 'ModuleLocal = S.Symbol
type OpenModuleNameType :: Stage -> IsOpenShort -> GHC.Type
type OpenModuleNameType :: Stage -> IsOpenShort -> GHCType
type family OpenModuleNameType s short = res where
OpenModuleNameType s 'OpenFull = ModuleNameType s
OpenModuleNameType _ 'OpenShort = ()
type ModuleNameType :: Stage -> GHC.Type
type ModuleNameType :: Stage -> GHCType
type family ModuleNameType s = res | res -> s where
ModuleNameType 'Parsed = Name
ModuleNameType 'Scoped = S.Name
type ModuleInductiveType :: ModuleIsTop -> GHC.Type
type ModuleInductiveType :: ModuleIsTop -> GHCType
type family ModuleInductiveType t = res | res -> t where
ModuleInductiveType 'ModuleTop = ()
ModuleInductiveType 'ModuleLocal = LocalModuleOrigin
type ModuleEndType :: ModuleIsTop -> GHC.Type
type ModuleEndType :: ModuleIsTop -> GHCType
type family ModuleEndType t = res | res -> t where
ModuleEndType 'ModuleTop = ()
ModuleEndType 'ModuleLocal = KeywordRef

3
src/Juvix/Compiler/Internal/Data/InfoTable.hs
View File

@ -23,7 +23,6 @@ where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Extra
import Juvix.Compiler.Internal.Extra.CoercionInfo
import Juvix.Compiler.Internal.Extra.HasLetDefs
import Juvix.Compiler.Internal.Extra.InstanceInfo
import Juvix.Compiler.Internal.Pretty (ppTrace)
import Juvix.Compiler.Store.Internal.Data.FunctionsTable
@ -69,7 +68,7 @@ extendWithReplExpression e =
)
)
letFunctionDefs :: (HasLetDefs a) => a -> [FunctionDef]
letFunctionDefs :: (HasExpressions a) => a -> [FunctionDef]
letFunctionDefs e =
concat
[ concatMap (toList . flattenClause) _letClauses

39
src/Juvix/Compiler/Internal/Extra.hs
View File

@ -228,3 +228,42 @@ cloneFunctionDefSameName :: (Members '[NameIdGen] r) => FunctionDef -> Sem r Fun
cloneFunctionDefSameName f = do
f' <- clone f
return (set funDefName (f ^. funDefName) f')
subsInstanceHoles :: forall r a. (HasExpressions a, Member NameIdGen r) => HashMap InstanceHole Expression -> a -> Sem r a
subsInstanceHoles s = umapM helper
where
helper :: Expression -> Sem r Expression
helper le = case le of
ExpressionInstanceHole h -> clone (fromMaybe e (s ^. at h))
_ -> return e
where
e = toExpression le
subsHoles :: forall r a. (HasExpressions a, Member NameIdGen r) => HashMap Hole Expression -> a -> Sem r a
subsHoles s = umapM helper
where
helper :: Expression -> Sem r Expression
helper le = case le of
ExpressionHole h -> clone (fromMaybe e (s ^. at h))
_ -> return e
where
e = toExpression le
substitutionE :: forall r expr. (Member NameIdGen r, HasExpressions expr) => Subs -> expr -> Sem r expr
substitutionE m expr
| null m = pure expr
| otherwise = umapM go expr
where
go :: Expression -> Sem r Expression
go = \case
ExpressionIden i -> goName (i ^. idenName)
e -> return (toExpression e)
goName :: Name -> Sem r Expression
goName n =
case HashMap.lookup n m of
Just e -> clone e
Nothing -> return (toExpression n)
substituteIndParams :: forall r. (Member NameIdGen r) => [(InductiveParameter, Expression)] -> Expression -> Sem r Expression
substituteIndParams = substitutionE . HashMap.fromList . map (first (^. inductiveParamName))

310
src/Juvix/Compiler/Internal/Extra/Base.hs
View File

@ -1,167 +1,183 @@
{-# OPTIONS_GHC -Wno-orphans #-}
module Juvix.Compiler.Internal.Extra.Base where
import Data.HashMap.Strict qualified as HashMap
import Data.HashSet qualified as HashSet
import Juvix.Compiler.Internal.Data.LocalVars
import Juvix.Compiler.Internal.Extra.Clonable
import Juvix.Compiler.Internal.Language
import Juvix.Compiler.Internal.Pretty
import Juvix.Prelude
type Rename = HashMap VarName VarName
type Subs = HashMap VarName Expression
instance PrettyCode Subs where
ppCode :: forall r. (Member (Reader Options) r) => Subs -> Sem r (Doc Ann)
ppCode m = do
assocs' <- mapM ppAssoc (HashMap.toList m)
return (braces (align (concatWith (\a b -> a <> kwSemicolon <> hardline <+> b) assocs')))
where
ppAssoc :: (VarName, Expression) -> Sem r (Doc Ann)
ppAssoc (v, el) = do
v' <- ppCode v
el' <- ppCode el
return (v' <+> kwMapsto <+> el')
data ApplicationArg = ApplicationArg
{ _appArgIsImplicit :: IsImplicit,
_appArg :: Expression
}
deriving stock (Generic, Data)
makeLenses ''ApplicationArg
instance HasLoc ApplicationArg where
getLoc = getLoc . (^. appArg)
data LeafExpression
= LeafExpressionIden Iden
| LeafExpressionHole Hole
| LeafExpressionLiteral (WithLoc Literal)
| LeafExpressionUniverse SmallUniverse
| LeafExpressionInstanceHole InstanceHole
deriving stock (Eq)
class IsExpression a where
toExpression :: a -> Expression
instance IsExpression LeafExpression where
toExpression =
\case
LeafExpressionIden i -> ExpressionIden i
LeafExpressionLiteral i -> ExpressionLiteral i
LeafExpressionHole i -> ExpressionHole i
LeafExpressionUniverse i -> ExpressionUniverse i
LeafExpressionInstanceHole i -> ExpressionInstanceHole i
instance Plated Expression where
plate :: Traversal' Expression Expression
plate f e = case e of
ExpressionApplication a -> ExpressionApplication <$> directExpressions f a
ExpressionFunction fun -> ExpressionFunction <$> directExpressions f fun
ExpressionSimpleLambda l -> ExpressionSimpleLambda <$> directExpressions f l
ExpressionLambda l -> ExpressionLambda <$> directExpressions f l
ExpressionLet l -> ExpressionLet <$> directExpressions f l
ExpressionCase c -> ExpressionCase <$> directExpressions f c
ExpressionIden {} -> pure e
ExpressionLiteral {} -> pure e
ExpressionUniverse {} -> pure e
ExpressionHole {} -> pure e
ExpressionInstanceHole {} -> pure e
class HasExpressions a where
leafExpressions :: forall expr. (IsExpression expr) => Traversal a a LeafExpression expr
-- | Traverses itself if `a` is an Expression. Otherwise traverses children `Expression`s (not transitive).
directExpressions :: Traversal' a Expression
directExpressions_ :: forall f a. (HasExpressions a, Applicative f) => (Expression -> f ()) -> a -> f ()
directExpressions_ f = void . directExpressions (\e -> e <$ f e)
instance HasExpressions Expression where
directExpressions = id
instance (HasExpressions a, Traversable l) => HasExpressions (l a) where
directExpressions f = traverse (directExpressions f)
instance HasExpressions LambdaClause where
leafExpressions f l = do
_lambdaPatterns <- traverse (leafExpressions f) (l ^. lambdaPatterns)
_lambdaBody <- leafExpressions f (l ^. lambdaBody)
directExpressions f l = do
_lambdaPatterns <- directExpressions f (l ^. lambdaPatterns)
_lambdaBody <- directExpressions f (l ^. lambdaBody)
pure LambdaClause {..}
instance HasExpressions Lambda where
leafExpressions f l = do
_lambdaClauses <- traverse (leafExpressions f) (l ^. lambdaClauses)
_lambdaType <- traverse (leafExpressions f) (l ^. lambdaType)
directExpressions f l = do
_lambdaClauses <- directExpressions f (l ^. lambdaClauses)
_lambdaType <- directExpressions f (l ^. lambdaType)
pure Lambda {..}
instance HasExpressions Expression where
leafExpressions f e = case e of
ExpressionIden i -> toExpression <$> f (LeafExpressionIden i)
ExpressionApplication a -> ExpressionApplication <$> leafExpressions f a
ExpressionFunction fun -> ExpressionFunction <$> leafExpressions f fun
ExpressionSimpleLambda l -> ExpressionSimpleLambda <$> leafExpressions f l
ExpressionLambda l -> ExpressionLambda <$> leafExpressions f l
ExpressionLet l -> ExpressionLet <$> leafExpressions f l
ExpressionCase c -> ExpressionCase <$> leafExpressions f c
ExpressionLiteral l -> toExpression <$> f (LeafExpressionLiteral l)
ExpressionUniverse u -> toExpression <$> f (LeafExpressionUniverse u)
ExpressionHole h -> toExpression <$> f (LeafExpressionHole h)
ExpressionInstanceHole h -> toExpression <$> f (LeafExpressionInstanceHole h)
instance HasExpressions ConstructorApp where
leafExpressions f a = do
directExpressions f a = do
let _constrAppConstructor = a ^. constrAppConstructor
_constrAppType <- traverseOf _Just (leafExpressions f) (a ^. constrAppType)
_constrAppParameters <- traverseOf each (leafExpressions f) (a ^. constrAppParameters)
_constrAppType <- directExpressions f (a ^. constrAppType)
_constrAppParameters <- directExpressions f (a ^. constrAppParameters)
pure ConstructorApp {..}
instance HasExpressions PatternArg where
leafExpressions f a = do
directExpressions f a = do
let _patternArgIsImplicit = a ^. patternArgIsImplicit
_patternArgName = a ^. patternArgName
_patternArgPattern <- leafExpressions f (a ^. patternArgPattern)
_patternArgPattern <- directExpressions f (a ^. patternArgPattern)
pure PatternArg {..}
instance HasExpressions WildcardConstructor where
directExpressions _ WildcardConstructor {..} = do
pure
WildcardConstructor
{ _wildcardConstructor
}
instance HasExpressions Pattern where
leafExpressions f p = case p of
directExpressions f p = case p of
PatternVariable {} -> pure p
PatternConstructorApp a -> PatternConstructorApp <$> leafExpressions f a
PatternConstructorApp a -> PatternConstructorApp <$> directExpressions f a
PatternWildcardConstructor {} -> pure p
instance HasExpressions SideIfBranch where
leafExpressions f b = do
_sideIfBranchCondition <- leafExpressions f (b ^. sideIfBranchCondition)
_sideIfBranchBody <- leafExpressions f (b ^. sideIfBranchBody)
directExpressions f b = do
_sideIfBranchCondition <- directExpressions f (b ^. sideIfBranchCondition)
_sideIfBranchBody <- directExpressions f (b ^. sideIfBranchBody)
pure SideIfBranch {..}
instance HasExpressions SideIfs where
leafExpressions f b = do
_sideIfBranches <- traverse (leafExpressions f) (b ^. sideIfBranches)
_sideIfElse <- traverse (leafExpressions f) (b ^. sideIfElse)
directExpressions f b = do
_sideIfBranches <- directExpressions f (b ^. sideIfBranches)
_sideIfElse <- directExpressions f (b ^. sideIfElse)
pure SideIfs {..}
instance HasExpressions CaseBranchRhs where
leafExpressions f = \case
CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> leafExpressions f e
CaseBranchRhsIf e -> CaseBranchRhsIf <$> leafExpressions f e
directExpressions f = \case
CaseBranchRhsExpression e -> CaseBranchRhsExpression <$> directExpressions f e
CaseBranchRhsIf e -> CaseBranchRhsIf <$> directExpressions f e
instance HasExpressions CaseBranch where
leafExpressions f b = do
_caseBranchPattern <- leafExpressions f (b ^. caseBranchPattern)
_caseBranchRhs <- leafExpressions f (b ^. caseBranchRhs)
directExpressions f b = do
_caseBranchPattern <- directExpressions f (b ^. caseBranchPattern)
_caseBranchRhs <- directExpressions f (b ^. caseBranchRhs)
pure CaseBranch {..}
instance HasExpressions Case where
leafExpressions f l = do
_caseBranches :: NonEmpty CaseBranch <- traverse (leafExpressions f) (l ^. caseBranches)
_caseExpression <- leafExpressions f (l ^. caseExpression)
_caseExpressionType <- traverse (leafExpressions f) (l ^. caseExpressionType)
_caseExpressionWholeType <- traverse (leafExpressions f) (l ^. caseExpressionWholeType)
directExpressions f l = do
_caseBranches <- directExpressions f (l ^. caseBranches)
_caseExpression <- directExpressions f (l ^. caseExpression)
_caseExpressionType <- directExpressions f (l ^. caseExpressionType)
_caseExpressionWholeType <- directExpressions f (l ^. caseExpressionWholeType)
pure Case {..}
where
_caseParens = l ^. caseParens
instance HasExpressions MutualBlock where
leafExpressions f (MutualBlock defs) =
MutualBlock <$> traverse (leafExpressions f) defs
directExpressions f (MutualBlock defs) =
MutualBlock <$> directExpressions f defs
instance HasExpressions MutualBlockLet where
leafExpressions f (MutualBlockLet defs) =
MutualBlockLet <$> traverse (leafExpressions f) defs
directExpressions f (MutualBlockLet defs) =
MutualBlockLet <$> directExpressions f defs
instance HasExpressions LetClause where
leafExpressions f = \case
LetFunDef d -> LetFunDef <$> leafExpressions f d
LetMutualBlock b -> LetMutualBlock <$> leafExpressions f b
directExpressions f = \case
LetFunDef d -> LetFunDef <$> directExpressions f d
LetMutualBlock b -> LetMutualBlock <$> directExpressions f b
instance HasExpressions Let where
leafExpressions f l = do
_letClauses :: NonEmpty LetClause <- traverse (leafExpressions f) (l ^. letClauses)
_letExpression <- leafExpressions f (l ^. letExpression)
directExpressions f l = do
_letClauses :: NonEmpty LetClause <- directExpressions f (l ^. letClauses)
_letExpression <- directExpressions f (l ^. letExpression)
pure Let {..}
instance HasExpressions TypedExpression where
leafExpressions f a = do
_typedExpression <- leafExpressions f (a ^. typedExpression)
_typedType <- leafExpressions f (a ^. typedType)
directExpressions f a = do
_typedExpression <- directExpressions f (a ^. typedExpression)
_typedType <- directExpressions f (a ^. typedType)
pure TypedExpression {..}
instance HasExpressions SimpleBinder where
leafExpressions f (SimpleBinder v ty) = do
ty' <- leafExpressions f ty
directExpressions f (SimpleBinder v ty) = do
ty' <- directExpressions f ty
pure (SimpleBinder v ty')
instance HasExpressions SimpleLambda where
leafExpressions f (SimpleLambda bi b) = do
bi' <- leafExpressions f bi
b' <- leafExpressions f b
directExpressions f (SimpleLambda bi b) = do
bi' <- directExpressions f bi
b' <- directExpressions f b
pure (SimpleLambda bi' b')
instance HasExpressions FunctionParameter where
leafExpressions f FunctionParameter {..} = do
ty' <- leafExpressions f _paramType
directExpressions f FunctionParameter {..} = do
ty' <- directExpressions f _paramType
pure
FunctionParameter
{ _paramType = ty',
@ -170,64 +186,32 @@ instance HasExpressions FunctionParameter where
}
instance HasExpressions Function where
leafExpressions f (Function l r) = do
l' <- leafExpressions f l
r' <- leafExpressions f r
directExpressions f (Function l r) = do
l' <- directExpressions f l
r' <- directExpressions f r
pure (Function l' r')
instance HasExpressions ApplicationArg where
leafExpressions f ApplicationArg {..} = do
arg' <- leafExpressions f _appArg
directExpressions f ApplicationArg {..} = do
arg' <- directExpressions f _appArg
pure
ApplicationArg
{ _appArg = arg',
_appArgIsImplicit
}
instance (HasExpressions a) => HasExpressions (Maybe a) where
leafExpressions = _Just . leafExpressions
instance HasExpressions Application where
leafExpressions f (Application l r i) = do
l' <- leafExpressions f l
r' <- leafExpressions f r
directExpressions f (Application l r i) = do
l' <- directExpressions f l
r' <- directExpressions f r
pure (Application l' r' i)
-- | Prism
_LeafExpressionHole :: Traversal' LeafExpression Hole
_LeafExpressionHole f e = case e of
LeafExpressionHole h -> LeafExpressionHole <$> f h
_ -> pure e
holes :: (HasExpressions a) => Traversal' a Hole
holes = leafExpressions . _LeafExpressionHole
hasHoles :: (HasExpressions a) => a -> Bool
hasHoles = has holes
subsInstanceHoles :: forall r a. (HasExpressions a, Member NameIdGen r) => HashMap InstanceHole Expression -> a -> Sem r a
subsInstanceHoles s = leafExpressions helper
where
helper :: LeafExpression -> Sem r Expression
helper le = case le of
LeafExpressionInstanceHole h -> clone (fromMaybe e (s ^. at h))
_ -> return e
where
e = toExpression le
subsHoles :: forall r a. (HasExpressions a, Member NameIdGen r) => HashMap Hole Expression -> a -> Sem r a
subsHoles s = leafExpressions helper
where
helper :: LeafExpression -> Sem r Expression
helper le = case le of
LeafExpressionHole h -> clone (fromMaybe e (s ^. at h))
_ -> return e
where
e = toExpression le
letDefs :: (HasExpressions a) => a -> [Let]
letDefs a = [l | ExpressionLet l <- a ^.. allExpressions]
instance HasExpressions ArgInfo where
leafExpressions f ArgInfo {..} = do
d' <- traverse (leafExpressions f) _argInfoDefault
directExpressions f ArgInfo {..} = do
d' <- directExpressions f _argInfoDefault
return
ArgInfo
{ _argInfoDefault = d',
@ -235,10 +219,10 @@ instance HasExpressions ArgInfo where
}
instance HasExpressions FunctionDef where
leafExpressions f FunctionDef {..} = do
body' <- leafExpressions f _funDefBody
ty' <- leafExpressions f _funDefType
infos' <- traverse (leafExpressions f) _funDefArgsInfo
directExpressions f FunctionDef {..} = do
body' <- directExpressions f _funDefBody
ty' <- directExpressions f _funDefType
infos' <- directExpressions f _funDefArgsInfo
pure
FunctionDef
{ _funDefBody = body',
@ -253,14 +237,14 @@ instance HasExpressions FunctionDef where
}
instance HasExpressions MutualStatement where
leafExpressions f = \case
StatementFunction d -> StatementFunction <$> leafExpressions f d
StatementInductive d -> StatementInductive <$> leafExpressions f d
StatementAxiom d -> StatementAxiom <$> leafExpressions f d
directExpressions f = \case
StatementFunction d -> StatementFunction <$> directExpressions f d
StatementInductive d -> StatementInductive <$> directExpressions f d
StatementAxiom d -> StatementAxiom <$> directExpressions f d
instance HasExpressions AxiomDef where
leafExpressions f AxiomDef {..} = do
ty' <- leafExpressions f _axiomType
directExpressions f AxiomDef {..} = do
ty' <- directExpressions f _axiomType
pure
AxiomDef
{ _axiomType = ty',
@ -270,14 +254,19 @@ instance HasExpressions AxiomDef where
}
instance HasExpressions InductiveParameter where
leafExpressions _ param@InductiveParameter {} = do
pure param
directExpressions f InductiveParameter {..} = do
ty' <- directExpressions f _inductiveParamType
pure
InductiveParameter
{ _inductiveParamType = ty',
_inductiveParamName
}
instance HasExpressions InductiveDef where
leafExpressions f InductiveDef {..} = do
params' <- traverse (leafExpressions f) _inductiveParameters
constrs' <- traverse (leafExpressions f) _inductiveConstructors
ty' <- leafExpressions f _inductiveType
directExpressions f InductiveDef {..} = do
params' <- directExpressions f _inductiveParameters
constrs' <- directExpressions f _inductiveConstructors
ty' <- directExpressions f _inductiveType
pure
InductiveDef
{ _inductiveParameters = params',
@ -291,8 +280,8 @@ instance HasExpressions InductiveDef where
}
instance HasExpressions ConstructorDef where
leafExpressions f ConstructorDef {..} = do
ty' <- leafExpressions f _inductiveConstructorType
directExpressions f ConstructorDef {..} = do
ty' <- directExpressions f _inductiveConstructorType
pure
ConstructorDef
{ _inductiveConstructorType = ty',
@ -301,9 +290,6 @@ instance HasExpressions ConstructorDef where
_inductiveConstructorPragmas
}
substituteIndParams :: forall r. (Member NameIdGen r) => [(InductiveParameter, Expression)] -> Expression -> Sem r Expression
substituteIndParams = substitutionE . HashMap.fromList . map (first (^. inductiveParamName))
typeAbstraction :: IsImplicit -> Name -> FunctionParameter
typeAbstraction i var = FunctionParameter (Just var) i (ExpressionUniverse (SmallUniverse (getLoc var)))
@ -353,21 +339,20 @@ subsKind uids k =
[ (s, toExpression s') | s <- uids, let s' = toExpression (set nameKind k s)
]
substitutionE :: forall r expr. (Member NameIdGen r, HasExpressions expr) => Subs -> expr -> Sem r expr
substitutionE m
| null m = pure
| otherwise = leafExpressions goLeaf
where
goLeaf :: LeafExpression -> Sem r Expression
goLeaf = \case
LeafExpressionIden i -> goName (i ^. idenName)
e -> return (toExpression e)
data Expr
= Val Int
| Neg Expr
| Add Expr Expr
deriving stock (Eq, Ord, Show, Data)
goName :: Name -> Sem r Expression
goName n =
case HashMap.lookup n m of
Just e -> clone e
Nothing -> return (toExpression n)
instance Plated Expr where
plate f (Neg e) = Neg <$> f e
plate f (Add a b) = Add <$> f a <*> f b
plate _ a = pure a
-- | A Fold over all subexressions, including self
allExpressions :: (HasExpressions expr) => Fold expr Expression
allExpressions = cosmosOn directExpressions
smallUniverseE :: Interval -> Expression
smallUniverseE = ExpressionUniverse . SmallUniverse
@ -803,3 +788,6 @@ simpleFunDef funName ty body =
_funDefBuiltin = Nothing,
_funDefBody = body
}
umapM :: (Monad m, HasExpressions expr) => (Expression -> m Expression) -> expr -> m expr
umapM = transformMOn directExpressions

19
src/Juvix/Compiler/Internal/Extra/Clonable.hs
View File

@ -5,6 +5,7 @@ module Juvix.Compiler.Internal.Extra.Clonable
where
import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Internal.Extra.Base
import Juvix.Compiler.Internal.Extra.Binders
import Juvix.Compiler.Internal.Language
import Juvix.Prelude
@ -108,24 +109,10 @@ underBinders ps f = do
return (set nameId uid' v)
instance Clonable SideIfBranch where
freshNameIds SideIfBranch {..} = do
cond' <- freshNameIds _sideIfBranchCondition
body' <- freshNameIds _sideIfBranchBody
return
SideIfBranch
{ _sideIfBranchCondition = cond',
_sideIfBranchBody = body'
}
freshNameIds = directExpressions freshNameIds
instance Clonable SideIfs where
freshNameIds SideIfs {..} = do
branches' <- mapM freshNameIds _sideIfBranches
else' <- mapM freshNameIds _sideIfElse
return
SideIfs
{ _sideIfBranches = branches',
_sideIfElse = else'
}
freshNameIds = directExpressions freshNameIds
instance Clonable CaseBranchRhs where
freshNameIds = \case

146
src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
View File

@ -76,30 +76,24 @@ addCastEdges = do
addStartNode :: (Member (State StartNodes) r) => Name -> Sem r ()
addStartNode n = modify (HashSet.insert n)
addEdgeMay :: (Member (State DependencyGraph) r) => Maybe Name -> Name -> Sem r ()
addEdgeMay mn1 n2 = whenJust mn1 $ \n1 -> addEdge n1 n2
addEdgeMay :: (Members '[State DependencyGraph, Reader (Maybe Name)] r) => Name -> Sem r ()
addEdgeMay n2 = whenJustM ask $ \n1 -> addEdge n1 n2
addEdgeMayRev :: (Members '[State DependencyGraph, Reader (Maybe Name)] r) => Name -> Sem r ()
addEdgeMayRev n2 = whenJustM ask $ \n1 -> addEdge n2 n1
addNode :: (Member (State DependencyGraph) r) => Name -> Sem r ()
addNode n =
modify
( HashMap.alter
( \case
Just x -> Just x
Nothing -> Just (mempty :: HashSet Name)
)
n
)
modify @DependencyGraph . over (at n) $
\case
Just x -> Just x
Nothing -> Just (mempty :: HashSet Name)
addEdge :: (Member (State DependencyGraph) r) => Name -> Name -> Sem r ()
addEdge n1 n2 =
modify
( HashMap.alter
( \case
Just ns -> Just (HashSet.insert n2 ns)
Nothing -> Just (HashSet.singleton n2)
)
n1
)
modify @DependencyGraph . over (at n1) $ \case
Just ns -> Just (HashSet.insert n2 ns)
Nothing -> Just (HashSet.singleton n2)
checkStartNode :: (Members '[Reader ExportsTable, State StartNodes, State BuilderState] r) => Name -> Sem r ()
checkStartNode n = do
@ -116,11 +110,16 @@ goPreModule m = do
-- module is reachable if at least one of the declarations in it is reachable)
goPreStatements (m ^. moduleName) (b ^. moduleStatements)
goPreLetStatements :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Maybe Name -> [PreLetStatement] -> Sem r ()
goPreLetStatements ::
forall r.
(Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) =>
Maybe Name ->
[PreLetStatement] ->
Sem r ()
goPreLetStatements mp = \case
stmt : stmts -> do
goPreLetStatement mp stmt
goPreLetStatements (Just $ getPreLetStatementName stmt) stmts
runReader mp (goPreLetStatement stmt)
goPreLetStatements (Just (getPreLetStatementName stmt)) stmts
[] -> return ()
where
getPreLetStatementName :: PreLetStatement -> Name
@ -129,14 +128,12 @@ goPreLetStatements mp = \case
goPreLetStatement ::
forall r.
(Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) =>
Maybe Name ->
(Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState, Reader (Maybe Name)] r) =>
PreLetStatement ->
Sem r ()
goPreLetStatement mp = \case
goPreLetStatement = \case
PreLetFunctionDef f -> do
whenJust mp $ \n ->
addEdge (f ^. funDefName) n
addEdgeMayRev (f ^. funDefName)
goFunctionDefHelper f
-- | `p` is the parent -- the previous declaration or the enclosing module. A
@ -168,16 +165,18 @@ goAxiom :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, Stat
goAxiom p ax = do
checkStartNode (ax ^. axiomName)
addEdge (ax ^. axiomName) p
goExpression (Just (ax ^. axiomName)) (ax ^. axiomType)
runReader (Just (ax ^. axiomName)) (goExpression (ax ^. axiomType))
goInductive :: forall r. (Members '[Reader ExportsTable, State DependencyGraph, State StartNodes, State BuilderState] r) => Name -> InductiveDef -> Sem r ()
goInductive p i = do
checkStartNode (i ^. inductiveName)
let indName = i ^. inductiveName
checkStartNode indName
checkBuiltinInductiveStartNode i
addEdge (i ^. inductiveName) p
mapM_ (goInductiveParameter (Just (i ^. inductiveName))) (i ^. inductiveParameters)
goExpression (Just (i ^. inductiveName)) (i ^. inductiveType)
mapM_ (goConstructorDef (i ^. inductiveName)) (i ^. inductiveConstructors)
addEdge indName p
mapM_ (goConstructorDef indName) (i ^. inductiveConstructors)
runReader (Just indName) $ do
mapM_ goInductiveParameter (i ^. inductiveParameters)
goExpression (i ^. inductiveType)
-- BuiltinBool and BuiltinNat are required by the Internal to Core translation
-- when translating literal integers to Nats.
@ -223,46 +222,46 @@ goFunctionDefHelper f = do
addNode (f ^. funDefName)
checkStartNode (f ^. funDefName)
checkCast f
goExpression (Just (f ^. funDefName)) (f ^. funDefType)
goExpression (Just (f ^. funDefName)) (f ^. funDefBody)
mapM_ (goExpression (Just (f ^. funDefName))) (f ^.. funDefArgsInfo . each . argInfoDefault . _Just)
runReader (Just (f ^. funDefName)) $ do
goExpression (f ^. funDefType)
goExpression (f ^. funDefBody)
mapM_ goExpression (f ^.. funDefArgsInfo . each . argInfoDefault . _Just)
-- constructors of an inductive type depend on the inductive type, not the other
-- | 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, State BuilderState, Reader ExportsTable] r) => Name -> ConstructorDef -> Sem r ()
goConstructorDef indName c = do
addEdge (c ^. inductiveConstructorName) indName
goExpression (Just indName) (c ^. inductiveConstructorType)
runReader (Just indName) (goExpression (c ^. inductiveConstructorType))
goPattern :: forall r. (Member (State DependencyGraph) r) => Maybe Name -> PatternArg -> Sem r ()
goPattern n p = case p ^. patternArgPattern of
goPattern :: forall r. (Members '[State DependencyGraph, Reader (Maybe Name)] r) => PatternArg -> Sem r ()
goPattern p = case p ^. patternArgPattern of
PatternVariable {} -> return ()
PatternWildcardConstructor c -> goWildcardConstructor c
PatternConstructorApp a -> goApp a
where
goWildcardConstructor :: WildcardConstructor -> Sem r ()
goWildcardConstructor w = addEdgeMay n (w ^. wildcardConstructor)
goWildcardConstructor w = addEdgeMay (w ^. wildcardConstructor)
goApp :: ConstructorApp -> Sem r ()
goApp (ConstructorApp ctr ps _) = do
addEdgeMay n ctr
mapM_ (goPattern n) ps
addEdgeMay ctr
mapM_ goPattern ps
goExpression ::
forall r.
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
Maybe Name ->
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable, Reader (Maybe Name)] r) =>
Expression ->
Sem r ()
goExpression p e = case e of
ExpressionIden i -> addEdgeMay p (i ^. idenName)
goExpression e = case e of
ExpressionIden i -> addEdgeMay (i ^. idenName)
ExpressionUniverse {} -> return ()
ExpressionFunction f -> do
goFunctionParameter p (f ^. functionLeft)
goExpression_ (f ^. functionRight)
goFunctionParameter (f ^. functionLeft)
goExpression (f ^. functionRight)
ExpressionApplication (Application l r _) -> do
goExpression_ l
goExpression_ r
goExpression l
goExpression r
ExpressionLiteral {} -> return ()
ExpressionCase c -> goCase c
ExpressionHole {} -> return ()
@ -271,70 +270,67 @@ goExpression p e = case e of
ExpressionLet l -> goLet l
ExpressionSimpleLambda l -> goSimpleLambda l
where
goExpression_ :: Expression -> Sem r ()
goExpression_ = goExpression p
goSimpleLambda :: SimpleLambda -> Sem r ()
goSimpleLambda l = do
addEdgeMay p (l ^. slambdaBinder . sbinderVar)
addEdgeMay (l ^. slambdaBinder . sbinderVar)
goLambda :: Lambda -> Sem r ()
goLambda Lambda {..} = mapM_ goClause _lambdaClauses
where
goClause :: LambdaClause -> Sem r ()
goClause (LambdaClause {..}) = do
goExpression_ _lambdaBody
mapM_ (goPattern p) _lambdaPatterns
goClause LambdaClause {..} = do
goExpression _lambdaBody
mapM_ goPattern _lambdaPatterns
goCase :: Case -> Sem r ()
goCase c = do
goExpression_ (c ^. caseExpression)
goExpression (c ^. caseExpression)
mapM_ goBranch (c ^. caseBranches)
goBranch :: CaseBranch -> Sem r ()
goBranch = goCaseBranchRhs . (^. caseBranchRhs)
goBranch c = do
goPattern (c ^. caseBranchPattern)
goCaseBranchRhs (c ^. caseBranchRhs)
goSideIfBranch :: SideIfBranch -> Sem r ()
goSideIfBranch SideIfBranch {..} = do
goExpression_ _sideIfBranchCondition
goExpression_ _sideIfBranchBody
goExpression _sideIfBranchCondition
goExpression _sideIfBranchBody
goSideIfs :: SideIfs -> Sem r ()
goSideIfs SideIfs {..} = do
mapM_ goSideIfBranch _sideIfBranches
mapM_ goExpression_ _sideIfElse
mapM_ goExpression _sideIfElse
goCaseBranchRhs :: CaseBranchRhs -> Sem r ()
goCaseBranchRhs = \case
CaseBranchRhsExpression expr -> goExpression_ expr
CaseBranchRhsExpression expr -> goExpression expr
CaseBranchRhsIf s -> goSideIfs s
goLet :: Let -> Sem r ()
goLet l = do
mapM_ goLetClause (l ^. letClauses)
goExpression_ (l ^. letExpression)
goExpression (l ^. letExpression)
goLetClause :: LetClause -> Sem r ()
goLetClause = \case
LetFunDef f -> do
addEdgeMay p (f ^. funDefName)
addEdgeMay (f ^. funDefName)
goFunctionDefHelper f
LetMutualBlock MutualBlockLet {..} -> mapM_ goFunctionDefHelper _mutualLet
goInductiveParameter ::
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
Maybe Name ->
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable, Reader (Maybe Name)] r) =>
InductiveParameter ->
Sem r ()
goInductiveParameter p param = do
addEdgeMay p (param ^. inductiveParamName)
goExpression p (param ^. inductiveParamType)
goInductiveParameter param = do
addEdgeMay (param ^. inductiveParamName)
goExpression (param ^. inductiveParamType)
goFunctionParameter ::
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable] r) =>
Maybe Name ->
(Members '[State DependencyGraph, State StartNodes, State BuilderState, Reader ExportsTable, Reader (Maybe Name)] r) =>
FunctionParameter ->
Sem r ()
goFunctionParameter p param = do
whenJust (param ^. paramName) (addEdgeMay p)
goExpression p (param ^. paramType)
goFunctionParameter param = do
whenJust (param ^. paramName) addEdgeMay
goExpression (param ^. paramType)

115
src/Juvix/Compiler/Internal/Extra/HasLetDefs.hs
View File

@ -1,115 +0,0 @@
module Juvix.Compiler.Internal.Extra.HasLetDefs where
import Juvix.Compiler.Internal.Language
import Juvix.Prelude
class HasLetDefs a where
letDefs' :: [Let] -> a -> [Let]
letDefs :: (HasLetDefs a) => a -> [Let]
letDefs = letDefs' []
instance (HasLetDefs a, Foldable f) => HasLetDefs (f a) where
letDefs' = foldl' letDefs'
instance HasLetDefs Expression where
letDefs' acc = \case
ExpressionIden {} -> acc
ExpressionApplication x -> letDefs' acc x
ExpressionFunction x -> letDefs' acc x
ExpressionLiteral {} -> acc
ExpressionHole {} -> acc
ExpressionInstanceHole {} -> acc
ExpressionLet x -> letDefs' acc x
ExpressionUniverse {} -> acc
ExpressionSimpleLambda x -> letDefs' acc x
ExpressionLambda x -> letDefs' acc x
ExpressionCase x -> letDefs' acc x
instance HasLetDefs Application where
letDefs' acc Application {..} = letDefs' (letDefs' acc _appLeft) _appRight
instance HasLetDefs Function where
letDefs' acc Function {..} = letDefs' (letDefs' acc _functionLeft) _functionRight
instance HasLetDefs FunctionParameter where
letDefs' acc FunctionParameter {..} = letDefs' acc _paramType
instance HasLetDefs Let where
letDefs' acc x@Let {..} = x : letDefs' (letDefs' acc _letExpression) _letClauses
instance HasLetDefs LetClause where
letDefs' acc = \case
LetFunDef x -> letDefs' acc x
LetMutualBlock x -> letDefs' acc x
instance HasLetDefs SimpleLambda where
letDefs' acc SimpleLambda {..} = letDefs' (letDefs' acc _slambdaBinder) _slambdaBody
instance HasLetDefs SimpleBinder where
letDefs' acc SimpleBinder {..} = letDefs' acc _sbinderType
instance HasLetDefs Lambda where
letDefs' acc Lambda {..} = letDefs' (letDefs' acc _lambdaType) _lambdaClauses
instance HasLetDefs LambdaClause where
letDefs' acc LambdaClause {..} = letDefs' (letDefs' acc _lambdaBody) _lambdaPatterns
instance HasLetDefs PatternArg where
letDefs' acc PatternArg {..} = letDefs' acc _patternArgPattern
instance HasLetDefs Pattern where
letDefs' acc = \case
PatternVariable {} -> acc
PatternConstructorApp x -> letDefs' acc x
PatternWildcardConstructor {} -> acc
instance HasLetDefs ConstructorApp where
letDefs' acc ConstructorApp {..} = letDefs' (letDefs' acc _constrAppType) _constrAppParameters
instance HasLetDefs Case where
letDefs' acc Case {..} = letDefs' (letDefs' acc _caseExpression) _caseBranches
instance HasLetDefs SideIfs where
letDefs' acc SideIfs {..} = letDefs' (letDefs' acc _sideIfBranches) _sideIfElse
instance HasLetDefs CaseBranchRhs where
letDefs' acc = \case
CaseBranchRhsExpression e -> letDefs' acc e
CaseBranchRhsIf e -> letDefs' acc e
instance HasLetDefs SideIfBranch where
letDefs' acc SideIfBranch {..} = letDefs' (letDefs' acc _sideIfBranchCondition) _sideIfBranchBody
instance HasLetDefs CaseBranch where
letDefs' acc CaseBranch {..} = letDefs' acc _caseBranchRhs
instance HasLetDefs MutualBlockLet where
letDefs' acc MutualBlockLet {..} = letDefs' acc _mutualLet
instance HasLetDefs MutualBlock where
letDefs' acc MutualBlock {..} = letDefs' acc _mutualStatements
instance HasLetDefs MutualStatement where
letDefs' acc = \case
StatementInductive x -> letDefs' acc x
StatementFunction x -> letDefs' acc x
StatementAxiom x -> letDefs' acc x
instance HasLetDefs InductiveDef where
letDefs' acc InductiveDef {..} = letDefs' (letDefs' (letDefs' acc _inductiveType) _inductiveConstructors) _inductiveParameters
instance HasLetDefs InductiveParameter where
letDefs' acc InductiveParameter {..} = letDefs' acc _inductiveParamType
instance HasLetDefs ConstructorDef where
letDefs' acc ConstructorDef {..} = letDefs' acc _inductiveConstructorType
instance HasLetDefs FunctionDef where
letDefs' acc FunctionDef {..} = letDefs' (letDefs' (letDefs' acc _funDefType) _funDefBody) _funDefArgsInfo
instance HasLetDefs ArgInfo where
letDefs' acc ArgInfo {..} = letDefs' acc _argInfoDefault
instance HasLetDefs AxiomDef where
letDefs' acc AxiomDef {..} = letDefs' acc _axiomType

2
src/Juvix/Compiler/Internal/Language.hs
View File

@ -136,6 +136,7 @@ data TypedExpression = TypedExpression
{ _typedType :: Expression,
_typedExpression :: Expression
}
deriving stock (Generic, Data)
data LetClause
= -- | Non-recursive let definition
@ -469,6 +470,7 @@ data NormalizedExpression = NormalizedExpression
_normalizedExpressionOriginal :: Expression
}
makePrisms ''Expression
makeLenses ''SideIfBranch
makeLenses ''SideIfs
makeLenses ''CaseBranchRhs

93
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/Termination/Checker.hs
View File

@ -11,6 +11,7 @@ module Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Che
where
import Data.HashMap.Internal.Strict qualified as HashMap
import Juvix.Compiler.Internal.Extra.Base (directExpressions_)
import Juvix.Compiler.Internal.Language as Internal
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.FunctionCall
import Juvix.Compiler.Internal.Translation.FromInternal.Analysis.Termination.Data
@ -169,44 +170,6 @@ scanFunctionBody topbody = go [] topbody
goClause :: LambdaClause -> Sem r ()
goClause (LambdaClause pats clBody) = go (reverse (toList pats) ++ revArgs) clBody
scanCase ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
Case ->
Sem r ()
scanCase c = do
mapM_ scanCaseBranch (c ^. caseBranches)
scanExpression (c ^. caseExpression)
scanSideIfBranch ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
SideIfBranch ->
Sem r ()
scanSideIfBranch SideIfBranch {..} = do
scanExpression _sideIfBranchCondition
scanExpression _sideIfBranchBody
scanSideIfs ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
SideIfs ->
Sem r ()
scanSideIfs SideIfs {..} = do
mapM_ scanSideIfBranch _sideIfBranches
mapM_ scanExpression _sideIfElse
scanCaseBranchRhs ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
CaseBranchRhs ->
Sem r ()
scanCaseBranchRhs = \case
CaseBranchRhsExpression e -> scanExpression e
CaseBranchRhsIf e -> scanSideIfs e
scanCaseBranch ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
CaseBranch ->
Sem r ()
scanCaseBranch = scanCaseBranchRhs . (^. caseBranchRhs)
scanLet ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
Let ->
@ -228,7 +191,10 @@ scanTopExpression ::
(Members '[State CallMap] r) =>
Expression ->
Sem r ()
scanTopExpression = runReader (Nothing @FunctionRef) . runReader emptySizeInfo . scanExpression
scanTopExpression =
runReader (Nothing @FunctionRef)
. runReader emptySizeInfo
. scanExpression
scanExpression ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
@ -240,53 +206,14 @@ scanExpression e =
whenJustM (ask @(Maybe FunctionRef)) (\caller -> runReader caller (registerCall c))
mapM_ (scanExpression . snd) (c ^. callArgs)
Nothing -> case e of
ExpressionApplication a -> scanApplication a
ExpressionFunction f -> scanFunction f
ExpressionLambda l -> scanLambda l
ExpressionApplication a -> directExpressions_ scanExpression a
ExpressionFunction f -> directExpressions_ scanExpression f
ExpressionLambda l -> directExpressions_ scanExpression l
ExpressionLet l -> scanLet l
ExpressionCase l -> scanCase l
ExpressionSimpleLambda l -> scanSimpleLambda l
ExpressionCase l -> directExpressions_ scanExpression l
ExpressionSimpleLambda l -> directExpressions_ scanExpression l
ExpressionIden {} -> return ()
ExpressionHole {} -> return ()
ExpressionInstanceHole {} -> return ()
ExpressionUniverse {} -> return ()
ExpressionLiteral {} -> return ()
scanSimpleLambda ::
forall r.
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
SimpleLambda ->
Sem r ()
scanSimpleLambda SimpleLambda {..} = scanExpression _slambdaBody
scanLambda ::
forall r.
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
Lambda ->
Sem r ()
scanLambda Lambda {..} = mapM_ scanClause _lambdaClauses
where
scanClause :: LambdaClause -> Sem r ()
scanClause LambdaClause {..} = scanExpression _lambdaBody
scanApplication ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
Application ->
Sem r ()
scanApplication (Application l r _) = do
scanExpression l
scanExpression r
scanFunction ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
Function ->
Sem r ()
scanFunction (Function l r) = do
scanFunctionParameter l
scanExpression r
scanFunctionParameter ::
(Members '[State CallMap, Reader (Maybe FunctionRef), Reader SizeInfo] r) =>
FunctionParameter ->
Sem r ()
scanFunctionParameter p = scanExpression (p ^. paramType)

41
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew.hs
View File

@ -36,25 +36,30 @@ data FunctionDefaultInfo = FunctionDefaultInfo
{ _functionDefaultArgId :: ArgId,
_functionDefaultValue :: Expression
}
deriving stock (Generic, Data)
data FunctionDefault = FunctionDefault
{ _functionDefaultLeft :: FunctionParameter,
_functionDefaultDefault :: Maybe FunctionDefaultInfo,
_functionDefaultRight :: BuilderType
}
deriving stock (Generic, Data)
data BuilderType
= BuilderTypeNoDefaults Expression
| BuilderTypeDefaults FunctionDefault
deriving stock (Generic, Data)
data IsDefault
= ItIsDefault ArgId
| ItIsNotDefault
deriving stock (Generic, Data)
data AppBuilderArg = AppBuilderArg
{ _appBuilderArgIsDefault :: IsDefault,
_appBuilderArg :: ApplicationArg
}
deriving stock (Generic, Data)
data AppBuilder = AppBuilder
{ _appBuilderLeft :: Expression,
@ -68,9 +73,18 @@ makeLenses ''AppBuilderArg
makeLenses ''FunctionDefault
makeLenses ''FunctionDefaultInfo
instance PrettyCode FunctionDefault where
ppCode _ = return "ppCode(FunctionDefault)"
instance PrettyCode AppBuilderArg where
ppCode _ = return "ppCode(AppBuilderArg)"
instance PrettyCode BuilderType where
ppCode _ = return "ppCode(BuilderType)"
instance HasExpressions FunctionDefaultInfo where
leafExpressions f i = do
val' <- leafExpressions f (i ^. functionDefaultValue)
directExpressions f i = do
val' <- directExpressions f (i ^. functionDefaultValue)
pure
FunctionDefaultInfo
{ _functionDefaultValue = val',
@ -78,10 +92,10 @@ instance HasExpressions FunctionDefaultInfo where
}
instance HasExpressions FunctionDefault where
leafExpressions f FunctionDefault {..} = do
l' <- leafExpressions f _functionDefaultLeft
r' <- leafExpressions f _functionDefaultRight
d' <- leafExpressions f _functionDefaultDefault
directExpressions f FunctionDefault {..} = do
l' <- directExpressions f _functionDefaultLeft
r' <- directExpressions f _functionDefaultRight
d' <- directExpressions f _functionDefaultDefault
pure
FunctionDefault
{ _functionDefaultLeft = l',
@ -90,13 +104,13 @@ instance HasExpressions FunctionDefault where
}
instance HasExpressions BuilderType where
leafExpressions f = \case
BuilderTypeNoDefaults e -> BuilderTypeNoDefaults <$> leafExpressions f e
BuilderTypeDefaults l -> BuilderTypeDefaults <$> leafExpressions f l
directExpressions f = \case
BuilderTypeNoDefaults e -> BuilderTypeNoDefaults <$> directExpressions f e
BuilderTypeDefaults l -> BuilderTypeDefaults <$> directExpressions f l
instance HasExpressions AppBuilderArg where
leafExpressions f AppBuilderArg {..} = do
a' <- leafExpressions f _appBuilderArg
directExpressions f AppBuilderArg {..} = do
a' <- directExpressions f _appBuilderArg
pure
AppBuilderArg
{ _appBuilderArg = a',
@ -534,8 +548,9 @@ checkExpression expectedTy e = do
resolveInstanceHoles ::
forall a r.
(HasExpressions a) =>
(Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r) =>
( HasExpressions a,
Members '[Reader InfoTable, ResultBuilder, Error TypeCheckerError, NameIdGen, Inference, Termination, Reader InsertedArgsStack] r
) =>
Sem (Output TypedHole ': r) a ->
Sem r a
resolveInstanceHoles s = do

2
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/CheckerNew/Arity.hs
View File

@ -10,7 +10,7 @@ data ArgId = ArgId
_argIdDefinitionLoc :: Irrelevant Interval,
_argIdName :: Irrelevant (Maybe Name)
}
deriving stock (Eq, Ord)
deriving stock (Eq, Ord, Data)
-- | Used to detect of cycles of default arguments in the arity checker.
newtype InsertedArgsStack = InsertedArgsStack

8
src/Juvix/Compiler/Internal/Translation/FromInternal/Analysis/TypeChecking/Data/Inference.hs
View File

@ -113,11 +113,11 @@ closeState = \case
modify (HashMap.insert h x)
return x
goExpression :: Expression -> Sem r' Expression
goExpression = traverseOf leafExpressions aux
goExpression = umapM aux
where
aux :: LeafExpression -> Sem r' Expression
aux :: Expression -> Sem r' Expression
aux = \case
LeafExpressionHole h -> goHole h
ExpressionHole h -> goHole h
e -> return (toExpression e)
getMetavar :: (Member (State InferenceState) r) => Hole -> Sem r MetavarState
@ -415,7 +415,7 @@ runInferenceState inis = reinterpret (runState inis) $ \case
{ _unsolvedMeta = hol,
_unsolvedIsLoop = True
}
when (LeafExpressionHole hol `elem` holTy' ^.. leafExpressions) (throw er)
when (ExpressionHole hol `elem` holTy' ^.. allExpressions) (throw er)
s <- gets (fromJust . (^. inferenceMap . at hol))
case s of
Fresh -> modify (set (inferenceMap . at hol) (Just (Refined holTy')))

3
src/Juvix/Compiler/Pipeline/Lockfile.hs
View File

@ -15,7 +15,6 @@ import Juvix.Extra.Strings qualified as Str
import Juvix.Extra.Version
import Juvix.Prelude hiding ((.=))
import Juvix.Prelude.Aeson
import Lens.Micro.Platform qualified as Lens
data LockfileDependency = LockfileDependency
{ _lockfileDependencyDependency :: Dependency,
@ -110,7 +109,7 @@ instance FromJSON LockfileDependency where
lockfileV2Options :: Options
lockfileV2Options =
defaultOptions
{ fieldLabelModifier = over Lens._head toLower . dropPrefix "_lockfileV2",
{ fieldLabelModifier = over _head toLower . dropPrefix "_lockfileV2",
rejectUnknownFields = True,
omitNothingFields = True
}

3
src/Juvix/Compiler/Pipeline/Package/Base.hs
View File

@ -12,7 +12,6 @@ import Juvix.Compiler.Pipeline.Lockfile
import Juvix.Compiler.Pipeline.Package.Dependency
import Juvix.Extra.Paths
import Juvix.Prelude
import Lens.Micro.Platform qualified as Lens
data BuildDir
= DefaultBuildDir
@ -72,7 +71,7 @@ deriving stock instance Show Package
rawPackageOptions :: Options
rawPackageOptions =
defaultOptions
{ fieldLabelModifier = over Lens._head toLower . dropPrefix "_package",
{ fieldLabelModifier = over _head toLower . dropPrefix "_package",
rejectUnknownFields = True,
omitNothingFields = True
}

3
src/Juvix/Compiler/Pipeline/Package/Dependency.hs
View File

@ -10,7 +10,6 @@ import Data.Yaml hiding ((.=))
import Juvix.Extra.Strings qualified as Str
import Juvix.Prelude hiding ((.=))
import Juvix.Prelude.Pretty
import Lens.Micro.Platform qualified as Lens
data Dependency
= DependencyPath PathDependency
@ -90,7 +89,7 @@ instance FromJSON PathDependency where
gitDependencyOptions :: Options
gitDependencyOptions =
defaultOptions
{ fieldLabelModifier = over Lens._head toLower . dropPrefix "_gitDependency",
{ fieldLabelModifier = over _head toLower . dropPrefix "_gitDependency",
rejectUnknownFields = True,
omitNothingFields = True
}

41
src/Juvix/Prelude/Base/Foundation.hs
View File

@ -50,7 +50,7 @@ module Juvix.Prelude.Base.Foundation
module GHC.Generics,
module GHC.Num,
module GHC.Real,
module Lens.Micro.Platform,
module Control.Lens,
module Language.Haskell.TH.Syntax,
module Prettyprinter,
module Numeric,
@ -80,6 +80,40 @@ where
import Control.Applicative
import Control.DeepSeq
import Control.Lens hiding
( Context,
Index,
Indexed,
Level,
List,
argument,
au,
below,
children,
cons,
cosmos,
enum,
from,
holes,
ignored,
imapM,
indexed,
indices,
inside,
op,
para,
parts,
pre,
re,
repeated,
rmap,
snoc,
uncons,
universe,
unsnoc,
(#),
(<.>),
)
import Control.Monad.Catch (ExitCase (..), MonadMask, MonadThrow, generalBracket, throwM)
import Control.Monad.Extra hiding (fail, forM, mconcatMapM, whileJustM)
import Control.Monad.Extra qualified as Monad
@ -161,7 +195,6 @@ import GHC.Num
import GHC.Real
import GHC.Stack.Types
import Language.Haskell.TH.Syntax (Exp, Lift, Q)
import Lens.Micro.Platform
import Numeric hiding (exp, log, pi)
import Path (Abs, Dir, File, Path, Rel, SomeBase (..))
import Path qualified as PPath
@ -206,6 +239,10 @@ type GHCConstraint = GHC.Constraint
type LazyHashMap = LazyHashMap.HashMap
type SimpleFold s a = forall r. (Monoid r) => Getting r s a
type SimpleGetter s a = forall r. Getting r s a
traverseM ::
(Monad m, Traversable m, Applicative f) =>
(a1 -> f (m a2)) ->