diff --git a/src/Juvix/Compiler/Internal/Extra.hs b/src/Juvix/Compiler/Internal/Extra.hs index b35300824d..76d51d6229 100644 --- a/src/Juvix/Compiler/Internal/Extra.hs +++ b/src/Juvix/Compiler/Internal/Extra.hs @@ -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)) diff --git a/src/Juvix/Compiler/Internal/Extra/Base.hs b/src/Juvix/Compiler/Internal/Extra/Base.hs index a4c607d34e..7eec74d6cb 100644 --- a/src/Juvix/Compiler/Internal/Extra/Base.hs +++ b/src/Juvix/Compiler/Internal/Extra/Base.hs @@ -5,7 +5,6 @@ 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 @@ -207,29 +206,9 @@ instance HasExpressions Application where r' <- directExpressions f r pure (Application l' r' i) -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 - letDefs :: (HasExpressions a) => a -> [Let] letDefs a = [l | ExpressionLet l <- a ^.. allExpressions] -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 - instance HasExpressions ArgInfo where directExpressions f ArgInfo {..} = do d' <- directExpressions f _argInfoDefault @@ -311,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))) @@ -378,22 +354,6 @@ instance Plated Expr where allExpressions :: (HasExpressions expr) => Fold expr Expression allExpressions = cosmosOn directExpressions -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) - smallUniverseE :: Interval -> Expression smallUniverseE = ExpressionUniverse . SmallUniverse diff --git a/src/Juvix/Compiler/Internal/Extra/Clonable.hs b/src/Juvix/Compiler/Internal/Extra/Clonable.hs index ad2ad2a071..cc02814e93 100644 --- a/src/Juvix/Compiler/Internal/Extra/Clonable.hs +++ b/src/Juvix/Compiler/Internal/Extra/Clonable.hs @@ -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