anoma/juvix
1
1
Fork 0
mirror of https://github.com/anoma/juvix.git synced 2025-01-09 01:09:18 +03:00
Code Issues Projects Releases Wiki Activity

Binder refactor (#1598)

Browse Source
This commit is contained in:
janmasrovira 2022-10-28 15:40:09 +02:00 committed by GitHub
parent 13a1dad107
commit 59e6712452
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
24 changed files with 636 additions and 548 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Juvix/Compiler/Asm/Translation/FromCore.hs
View File

@ -162,7 +162,7 @@ genCode infoTable fi =
goLet :: Bool -> Int -> BinderList Value -> Core.Let -> Code'
goLet isTail tempSize refs (Core.Let {..}) =
DL.append
(DL.snoc (go False tempSize refs _letValue) (mkInstr PushTemp))
(DL.snoc (go False tempSize refs (_letItem ^. Core.letItemValue)) (mkInstr PushTemp))
(snocPopTemp isTail $ go isTail (tempSize + 1) (BL.extend (Ref (DRef (TempRef tempSize))) refs) _letBody)
goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code'

8
src/Juvix/Compiler/Core/Evaluator.hs
View File

@ -60,14 +60,14 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
NCst {} -> n
NApp (App i l r) ->
case eval' env l of
Closure env' (Lambda _ b) -> let !v = eval' env r in eval' (v : env') b
Closure env' (Lambda _ _ b) -> let !v = eval' env r in eval' (v : env') b
v -> evalError "invalid application" (mkApp i v (substEnv env r))
NBlt (BuiltinApp _ op args) -> applyBuiltin n env op args
NCtr (Constr i tag args) -> mkConstr i tag (map' (eval' env) args)
NLam l@Lambda {} -> Closure env l
NLet (Let _ v b) -> let !v' = eval' env v in eval' (v' : env) b
NLet (Let _ (LetItem _ v) b) -> let !v' = eval' env v in eval' (v' : env) b
NRec (LetRec _ vs b) ->
let !vs' = map (eval' env') (toList vs)
let !vs' = map (eval' env' . (^. letItemValue)) (toList vs)
!env' = revAppend vs' env
in foldr GHC.pseq (eval' env' b) vs'
NCase (Case i v bs def) ->
@ -86,7 +86,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node
branch n !env !args !tag !def = \case
(CaseBranch _ tag' _ b) : _ | tag' == tag -> eval' (revAppend args env) b
(CaseBranch _ tag' _ _ b) : _ | tag' == tag -> eval' (revAppend args env) b
_ : bs' -> branch n env args tag def bs'
[] -> case def of
Just b -> eval' env b

14
src/Juvix/Compiler/Core/Extra.hs
View File

@ -80,7 +80,7 @@ cosmos f = ufoldA reassemble f
-- binder of the variable.
-- if fv = x1, x2, .., xn
-- the result is of the form λx1 λx2 .. λ xn b
captureFreeVars :: [(Index, Info)] -> Node -> Node
captureFreeVars :: [(Index, Binder)] -> Node -> Node
captureFreeVars fv
| n == 0 = id
| otherwise = mkLambdasB infos . mapFreeVars
@ -122,7 +122,7 @@ developBeta = umap go
where
go :: Node -> Node
go n = case n of
NApp (App _ (NLam (Lambda _ body)) arg) -> subst arg body
NApp (App _ (NLam (Lambda {..})) arg) -> subst arg _lambdaBody
_ -> n
etaExpand :: Int -> Node -> Node
@ -145,17 +145,17 @@ convertClosures = umap go
where
go :: Node -> Node
go n = case n of
Closure env (Lambda i b) -> substEnv env (mkLambda i b)
Closure env (Lambda i bi b) -> substEnv env (mkLambda i bi b)
_ -> n
convertRuntimeNodes :: Node -> Node
convertRuntimeNodes = convertClosures
argumentInfoFromInfo :: Info -> ArgumentInfo
argumentInfoFromInfo i =
argumentInfoFromBinder :: Binder -> ArgumentInfo
argumentInfoFromBinder i =
ArgumentInfo
{ _argumentName = getInfoName i,
_argumentType = getInfoType i,
{ _argumentName = i ^. binderName,
_argumentType = i ^. binderType,
_argumentIsImplicit = Explicit
}

517
src/Juvix/Compiler/Core/Extra/Base.hs
View File

@ -2,9 +2,7 @@ module Juvix.Compiler.Core.Extra.Base where
import Data.Functor.Identity
import Data.List qualified as List
import Data.List.NonEmpty (fromList)
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.BinderInfo
import Juvix.Compiler.Core.Language
{------------------------------------------------------------------------}
@ -46,23 +44,26 @@ mkConstr i tag args = NCtr (Constr i tag args)
mkConstr' :: Tag -> [Node] -> Node
mkConstr' = mkConstr Info.empty
mkLambda :: Info -> Node -> Node
mkLambda i b = NLam (Lambda i b)
mkLambda :: Info -> Binder -> Node -> Node
mkLambda i bi b = NLam (Lambda i bi b)
mkLambda' :: Node -> Node
mkLambda' = mkLambda Info.empty
mkLambda' = mkLambda Info.empty emptyBinder
mkLet :: Info -> Node -> Node -> Node
mkLet i v b = NLet (Let i v b)
mkLetItem' :: Node -> LetItem
mkLetItem' = LetItem emptyBinder
mkLet :: Info -> Binder -> Node -> Node -> Node
mkLet i bi v b = NLet (Let i (LetItem bi v) b)
mkLet' :: Node -> Node -> Node
mkLet' = mkLet Info.empty
mkLet' = mkLet Info.empty emptyBinder
mkLetRec :: Info -> NonEmpty Node -> Node -> Node
mkLetRec :: Info -> NonEmpty LetItem -> Node -> Node
mkLetRec i vs b = NRec (LetRec i vs b)
mkLetRec' :: NonEmpty Node -> Node -> Node
mkLetRec' = mkLetRec Info.empty
mkLetRec' = mkLetRec Info.empty . fmap mkLetItem'
mkCase :: Info -> Node -> [CaseBranch] -> Maybe Node -> Node
mkCase i v bs def = NCase (Case i v bs def)
@ -77,7 +78,16 @@ mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
mkMatch' = mkMatch Info.empty
mkIf :: Info -> Node -> Node -> Node -> Node
mkIf i v b1 b2 = mkCase i v [CaseBranch Info.empty (BuiltinTag TagTrue) 0 b1] (Just b2)
mkIf i v b1 b2 = mkCase i v [br] (Just b2)
where
br =
CaseBranch
{ _caseBranchInfo = mempty,
_caseBranchTag = BuiltinTag TagTrue,
_caseBranchBinders = [],
_caseBranchBindersNum = 0,
_caseBranchBody = b1
}
mkIf' :: Node -> Node -> Node -> Node
mkIf' = mkIf Info.empty
@ -85,14 +95,20 @@ mkIf' = mkIf Info.empty
{------------------------------------------------------------------------}
{- Type constructors -}
mkPi :: Info -> Type -> Type -> Type
mkPi i ty b = NPi (Pi i ty b)
mkPi :: Info -> Binder -> Type -> Type
mkPi i bi b = NPi (Pi i bi b)
mkPi' :: Type -> Type -> Type
mkPi' = mkPi Info.empty
mkPi' = mkPi Info.empty . Binder Nothing
mkPis :: [(Info, Type)] -> Type -> Type
mkPis tys ty = foldr (uncurry mkPi) ty tys
mkPis :: [Binder] -> Type -> Type
mkPis tys ty = foldr (mkPi mempty) ty tys
rePi :: PiLhs -> Type -> Type
rePi PiLhs {..} = mkPi _piLhsInfo _piLhsBinder
rePis :: [PiLhs] -> Type -> Type
rePis tys ty = foldr rePi ty tys
mkPis' :: [Type] -> Type -> Type
mkPis' tys ty = foldr mkPi' ty tys
@ -143,16 +159,18 @@ mkDynamic' = mkDynamic Info.empty
{- functions on Type -}
-- | Unfold a type into the target and the arguments (left-to-right)
unfoldType :: Type -> (Type, [(Info, Type)])
unfoldType ty = case ty of
NPi (Pi i l r) -> let (tgt, args) = unfoldType r in (tgt, (i, l) : args)
_ -> (ty, [])
unfoldPi :: Type -> ([PiLhs], Type)
unfoldPi ty = case ty of
NPi (Pi i bi r) ->
let (args, target) = unfoldPi r
in (PiLhs i bi : args, target)
_ -> ([], ty)
typeArgs :: Type -> [Type]
typeArgs = map snd . snd . unfoldType
typeArgs = map (^. piLhsBinder . binderType) . fst . unfoldPi
typeTarget :: Type -> Type
typeTarget = fst . unfoldType
typeTarget = snd . unfoldPi
isDynamic :: Type -> Bool
isDynamic = \case
@ -164,12 +182,12 @@ isDynamic = \case
-- `expandType [int, string] (int -> any) = int -> string -> any`.
expandType :: [Type] -> Type -> Type
expandType argtys ty =
let (tgt, tyargs) = unfoldType ty
let (tyargs, target) = unfoldPi ty
in if
| length tyargs >= length argtys ->
ty
| isDynamic tgt ->
mkPis tyargs (mkPis' (drop (length tyargs) argtys) tgt)
| isDynamic target ->
rePis tyargs (mkPis' (drop (length tyargs) argtys) target)
| otherwise ->
impossible
@ -193,31 +211,32 @@ unfoldApps = go []
unfoldApps' :: Node -> (Node, [Node])
unfoldApps' = second (map snd) . unfoldApps
mkLambdas :: [Info] -> Node -> Node
mkLambdas is n = foldl' (flip mkLambda) n (reverse is)
reLambda :: LambdaLhs -> Node -> Node
reLambda lhs = mkLambda (lhs ^. lambdaLhsInfo) (lhs ^. lambdaLhsBinder)
-- | the given info corresponds to the binder info
mkLambdaB :: Info -> Node -> Node
mkLambdaB = mkLambda . singletonInfoBinder
reLambdas :: [LambdaLhs] -> Node -> Node
reLambdas is n = foldl' (flip reLambda) n (reverse is)
-- | the given infos correspond to the binder infos
mkLambdasB :: [Info] -> Node -> Node
mkLambdaB :: Binder -> Node -> Node
mkLambdaB = mkLambda mempty
mkLambdasB :: [Binder] -> Node -> Node
mkLambdasB is n = foldl' (flip mkLambdaB) n (reverse is)
mkLambdas' :: Int -> Node -> Node
mkLambdas' k
| k < 0 = impossible
| otherwise = mkLambdas (replicate k Info.empty)
| otherwise = mkLambdasB (replicate k emptyBinder)
unfoldLambdasRev :: Node -> ([Info], Node)
unfoldLambdasRev :: Node -> ([LambdaLhs], Node)
unfoldLambdasRev = go []
where
go :: [Info] -> Node -> ([Info], Node)
go :: [LambdaLhs] -> Node -> ([LambdaLhs], Node)
go acc n = case n of
NLam (Lambda i b) -> go (i : acc) b
NLam (Lambda i bi b) -> go (LambdaLhs i bi : acc) b
_ -> (acc, n)
unfoldLambdas :: Node -> ([Info], Node)
unfoldLambdas :: Node -> ([LambdaLhs], Node)
unfoldLambdas = first reverse . unfoldLambdasRev
unfoldLambdas' :: Node -> (Int, Node)
@ -226,33 +245,38 @@ unfoldLambdas' = first length . unfoldLambdas
{------------------------------------------------------------------------}
{- functions on Pattern -}
getBinderPatternInfos :: Pattern -> [Info]
getBinderPatternInfos :: Pattern -> [Binder]
getBinderPatternInfos = go []
where
go :: [Info] -> Pattern -> [Info]
go :: [Binder] -> Pattern -> [Binder]
go acc = \case
PatConstr (PatternConstr {..}) ->
foldl' go acc _patternConstrArgs
PatBinder (PatternBinder {..}) ->
go (_patternBinderInfo : acc) _patternBinderPattern
PatWildcard {} ->
acc
PatConstr PatternConstr {..} -> foldl' go acc _patternConstrArgs
PatBinder p -> go (p ^. patternBinder : acc) (p ^. patternBinderPattern)
PatWildcard {} -> acc
getPatternInfos :: Pattern -> [Info]
getPatternInfos = go []
where
go :: [Info] -> Pattern -> [Info]
go acc = \case
PatConstr (PatternConstr {..}) ->
foldl' go (_patternConstrInfo : acc) _patternConstrArgs
PatBinder (PatternBinder {..}) ->
go (_patternBinderInfo : acc) _patternBinderPattern
PatWildcard (PatternWildcard {..}) ->
_patternWildcardInfo : acc
PatConstr PatternConstr {..} -> foldl' go (_patternConstrInfo : acc) _patternConstrArgs
PatBinder PatternBinder {..} -> go acc _patternBinderPattern
PatWildcard PatternWildcard {..} -> _patternWildcardInfo : acc
{------------------------------------------------------------------------}
{- generic Node destruction -}
data NodeChild = NodeChild
{ -- | immediate child of some node
_childNode :: Node,
-- | Binders introduced by the child
_childBinders :: [Binder],
-- | length of `_childBinders`
_childBindersNum :: Int
}
makeLenses ''NodeChild
-- | `NodeDetails` is a convenience datatype which provides the most commonly needed
-- information about a node in a generic fashion.
data NodeDetails = NodeDetails
@ -264,21 +288,78 @@ data NodeDetails = NodeDetails
_nodeSubinfos :: [Info],
-- | 'nodeChildren' are the children, in a fixed order, i.e., the immediate
-- recursive subnodes
_nodeChildren :: [Node],
-- | 'nodeChildBindersNum' is the number of binders introduced for each
-- child in the parent node. Same length and order as in `nodeChildren`.
_nodeChildBindersNum :: [Int],
-- | 'nodeChildBindersInfo' is information about binders for each child, if
-- present. Same length and order as in `nodeChildren`.
_nodeChildBindersInfo :: [[Info]],
_nodeChildren :: [NodeChild],
-- | 'nodeReassemble' reassembles the node from the info, the subinfos and
-- the children (which should be in the same fixed order as in the
-- 'nodeSubinfos' and 'nodeChildren' component).
_nodeReassemble :: Info -> [Info] -> [Node] -> Node
_nodeReassemble :: Info -> [Info] -> [NodeChild] -> Node
}
makeLenses ''NodeDetails
{-# INLINE noBinders #-}
noBinders :: Node -> NodeChild
noBinders n =
NodeChild
{ _childNode = n,
_childBinders = [],
_childBindersNum = 0
}
{-# INLINE oneBinder #-}
oneBinder :: Binder -> Node -> NodeChild
oneBinder bi n =
NodeChild
{ _childNode = n,
_childBinders = [bi],
_childBindersNum = 1
}
{-# INLINE manyBinders #-}
manyBinders :: [Binder] -> Node -> NodeChild
manyBinders bis n =
NodeChild
{ _childNode = n,
_childBinders = bis,
_childBindersNum = length bis
}
type Reassemble = Info -> [Info] -> [NodeChild] -> Node
{-# INLINE noChildren #-}
noChildren :: (Info -> Node) -> Reassemble
noChildren f i _ _ = f i
{-# INLINE oneChild #-}
oneChild :: (Info -> NodeChild -> Node) -> Reassemble
oneChild f i _ ch = case ch of
[c] -> f i c
_ -> impossible
{-# INLINE twoChildren #-}
twoChildren :: (Info -> NodeChild -> NodeChild -> Node) -> Reassemble
twoChildren f i _ ch = case ch of
[l, r] -> f i l r
_ -> impossible
{-# INLINE manyChildren #-}
manyChildren :: (Info -> [NodeChild] -> Node) -> Reassemble
manyChildren f i _ = f i
{-# INLINE someChildren #-}
someChildren :: (Info -> NonEmpty NodeChild -> Node) -> Reassemble
someChildren f i _ = f i . nonEmpty'
{-# INLINE someChildrenI #-}
someChildrenI :: (Info -> [Info] -> NonEmpty NodeChild -> Node) -> Reassemble
someChildrenI f i is = f i is . nonEmpty'
{-# INLINE twoManyChildrenI #-}
twoManyChildrenI :: (Info -> [Info] -> NodeChild -> NodeChild -> [NodeChild] -> Node) -> Reassemble
twoManyChildrenI f i is = \case
(x : y : xs) -> f i is x y xs
_ -> impossible
-- | Destruct a node into NodeDetails. This is an ugly internal function used to
-- implement more high-level accessors and recursors.
destruct :: Node -> NodeDetails
@ -288,145 +369,123 @@ destruct = \case
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkVar i' idx
_nodeReassemble = noChildren $ \i' -> mkVar i' idx
}
NIdt (Ident i sym) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkIdent i' sym
_nodeReassemble = noChildren $ \i' -> mkIdent i' sym
}
NCst (Constant i c) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkConstant i' c
_nodeReassemble = noChildren $ \i' -> mkConstant i' c
}
NApp (App i l r) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [l, r],
_nodeChildBindersNum = [0, 0],
_nodeChildBindersInfo = [[], []],
_nodeReassemble = \i' _ args' -> mkApp i' (hd args') (args' !! 1)
_nodeChildren = map noBinders [l, r],
_nodeReassemble = twoChildren $ \i' l' r' -> mkApp i' (l' ^. childNode) (r' ^. childNode)
}
NBlt (BuiltinApp i op args) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = args,
_nodeChildBindersNum = map (const 0) args,
_nodeChildBindersInfo = map (const []) args,
_nodeReassemble = \i' _ args' -> mkBuiltinApp i' op args'
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' args' -> mkBuiltinApp i' op (map (^. childNode) args')
}
NCtr (Constr i tag args) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = args,
_nodeChildBindersNum = map (const 0) args,
_nodeChildBindersInfo = map (const []) args,
_nodeReassemble = \i' _ args' -> mkConstr i' tag args'
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' -> mkConstr i' tag . map (^. childNode)
}
NLam (Lambda i b) ->
NLam (Lambda i bi b) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [b],
_nodeChildBindersNum = [1],
_nodeChildBindersInfo = [fetchBinderInfo i],
_nodeReassemble = \i' _ args' -> mkLambda i' (hd args')
_nodeChildren = [oneBinder bi b],
_nodeReassemble = oneChild $ \i' ch' -> mkLambda i' (hd (ch' ^. childBinders)) (ch' ^. childNode)
}
NLet (Let i v b) ->
NLet (Let i (LetItem bi v) b) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [v, b],
_nodeChildBindersNum = [0, 1],
_nodeChildBindersInfo = [[], fetchBinderInfo i],
_nodeReassemble = \i' _ args' -> mkLet i' (hd args') (args' !! 1)
_nodeChildren = [noBinders v, oneBinder bi b],
_nodeReassemble = twoChildren $ \i' v' b' ->
mkLet i' (hd (b' ^. childBinders)) (v' ^. childNode) (b' ^. childNode)
}
NRec (LetRec i vs b) ->
let n = length vs
in NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = b : toList vs,
_nodeChildBindersNum = replicate (n + 1) n,
_nodeChildBindersInfo = replicate (n + 1) (getInfoBinders n i),
_nodeReassemble = \i' _ args' -> mkLetRec i' (fromList (tl args')) (hd args')
}
NCase (Case i v bs Nothing) ->
let branchBinderNums = map (^. caseBranchBindersNum) bs
branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
in NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = map (^. caseBranchInfo) bs,
_nodeChildren = v : map (^. caseBranchBody) bs,
_nodeChildBindersNum = 0 : branchBinderNums,
_nodeChildBindersInfo = [] : branchBinderInfos,
_nodeReassemble = \i' is' args' ->
mkCase
i'
(hd args')
( zipWith3Exact
( \br is body' ->
br
{ _caseBranchInfo = is,
_caseBranchBody = body'
}
)
bs
is'
(tl args')
)
Nothing
}
NCase (Case i v bs (Just def)) ->
let branchBinderNums = map (^. caseBranchBindersNum) bs
branchBinderInfos = map (\(CaseBranch {..}) -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
in NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = map (^. caseBranchInfo) bs,
_nodeChildren = v : def : map (^. caseBranchBody) bs,
_nodeChildBindersNum = 0 : 0 : branchBinderNums,
_nodeChildBindersInfo = [] : [] : branchBinderInfos,
_nodeReassemble = \i' is' args' ->
mkCase
i'
(hd args')
( zipWith3Exact
( \br is body' ->
br
{ _caseBranchInfo = is,
_caseBranchBody = body'
}
)
bs
is'
(tl (tl args'))
)
(Just (hd (tl args')))
}
NMatch (Match i vs bs) ->
let branchBinderInfos =
map
( \br ->
concatMap
getBinderPatternInfos
(reverse (toList (br ^. matchBranchPatterns)))
)
bs
branchBinderNums = map length branchBinderInfos
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren =
let binders :: [Binder]
values :: [Node]
(binders, values) = unzip [(it ^. letItemBinder, it ^. letItemValue) | it <- toList vs]
in map (manyBinders binders) (b : values),
_nodeReassemble = someChildren $ \i' (b' :| values') ->
let items' =
nonEmpty'
[ LetItem (item ^. letItemBinder) (v' ^. childNode) | (v', item) <- zipExact values' (toList vs)
]
in mkLetRec i' items' (b' ^. childNode)
}
NCase (Case i v brs mdef) ->
let branchChildren :: [NodeChild]
branchChildren =
[ manyBinders (br ^. caseBranchBinders) (br ^. caseBranchBody)
| br <- brs
]
in case mdef of
Nothing ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = map (^. caseBranchInfo) brs,
_nodeChildren = noBinders v : branchChildren,
_nodeReassemble = someChildrenI $ \i' is' (v' :| bodies') ->
let branches :: [CaseBranch]
branches =
[ br
{ _caseBranchInfo = ib',
_caseBranchBinders = body' ^. childBinders,
_caseBranchBody = body' ^. childNode
}
| (body', ib', br) <- zip3Exact bodies' is' brs
]
in mkCase i' (v' ^. childNode) branches Nothing
}
Just def ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = map (^. caseBranchInfo) brs,
_nodeChildren = noBinders v : noBinders def : branchChildren,
_nodeReassemble = twoManyChildrenI $ \i' is' v' def' bodies' ->
let branches :: [CaseBranch]
branches =
[ br
{ _caseBranchInfo = ib',
_caseBranchBinders = body' ^. childBinders,
_caseBranchBody = body' ^. childNode
}
| (body', ib', br) <- zip3Exact bodies' is' brs
]
in mkCase i' (v' ^. childNode) branches (Just (def' ^. childNode))
}
NMatch (Match i vs branches) ->
let branchChildren :: [NodeChild]
branchChildren =
[ manyBinders binders (br ^. matchBranchBody)
| br <- branches,
let binders = concatMap getBinderPatternInfos (reverse (toList (br ^. matchBranchPatterns)))
]
branchPatternInfos :: [Info]
branchPatternInfos =
concatMap
( \br ->
@ -434,107 +493,94 @@ destruct = \case
(reverse . getPatternInfos)
(br ^. matchBranchPatterns)
)
bs
branches
n = length vs
in NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = branchPatternInfos,
_nodeChildren = toList vs ++ map (^. matchBranchBody) bs,
_nodeChildBindersNum = replicate n 0 ++ branchBinderNums,
_nodeChildBindersInfo = replicate n [] ++ branchBinderInfos,
_nodeReassemble = \i' is' args' ->
mkMatch
i'
(fromList $ List.take n args')
( zipWithExact
( \br body' ->
br
{ _matchBranchPatterns =
fromList $ setPatternsInfos is' (toList (br ^. matchBranchPatterns)),
_matchBranchBody = body'
}
)
bs
(drop n args')
)
_nodeChildren = map noBinders (toList vs) ++ branchChildren,
_nodeReassemble = someChildrenI $ \i' is' chs' ->
let values' :: NonEmpty NodeChild
bodies' :: [NodeChild]
(values', bodies') = first nonEmpty' (splitAtExact n (toList chs'))
branches' :: [MatchBranch]
branches' =
[ br
{ _matchBranchPatterns = nonEmpty' $ setPatternsInfos binders' is' (toList (br ^. matchBranchPatterns)),
_matchBranchBody = body' ^. childNode
}
| (body', br) <- zipExact bodies' branches,
let binders' = body' ^. childBinders
]
in mkMatch i' (fmap (^. childNode) values') branches'
}
NPi (Pi i ty b) ->
NPi (Pi i bi b) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [ty, b],
_nodeChildBindersNum = [0, 1],
_nodeChildBindersInfo = [[], fetchBinderInfo i],
_nodeReassemble = \i' _ args' -> mkPi i' (hd args') (args' !! 1)
_nodeChildren = [noBinders (bi ^. binderType), oneBinder bi b],
_nodeReassemble = twoChildren $ \i' bi' b' ->
-- NOTE the binder type here is treated as a node
let binder :: Binder
binder = set binderType (bi' ^. childNode) (hd (b' ^. childBinders))
in mkPi i' binder (b' ^. childNode)
}
NUniv (Univ i l) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkUniv i' l
_nodeReassemble = noChildren $ \i' -> mkUniv i' l
}
NTyp (TypeConstr i sym args) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = args,
_nodeChildBindersNum = map (const 0) args,
_nodeChildBindersInfo = map (const []) args,
_nodeReassemble = \i' _ args' -> mkTypeConstr i' sym args'
_nodeChildren = map noBinders args,
_nodeReassemble = manyChildren $ \i' -> mkTypeConstr i' sym . map (^. childNode)
}
NPrim (TypePrim i prim) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkTypePrim i' prim
_nodeReassemble = noChildren $ \i' -> mkTypePrim i' prim
}
NDyn (Dynamic i) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = [],
_nodeChildBindersNum = [],
_nodeChildBindersInfo = [],
_nodeReassemble = \i' _ _ -> mkDynamic i'
_nodeReassemble = noChildren $ \i' -> mkDynamic i'
}
Closure env (Lambda i b) ->
Closure env (Lambda i bi b) ->
NodeDetails
{ _nodeInfo = i,
_nodeSubinfos = [],
_nodeChildren = b : env,
_nodeChildBindersNum = 1 : map (const 0) env,
_nodeChildBindersInfo = fetchBinderInfo i : map (const []) env,
_nodeReassemble = \i' _ args' -> Closure (tl args') (Lambda i' (hd args'))
_nodeChildren = oneBinder bi b : map noBinders env,
_nodeReassemble = someChildren $ \i' (b' :| env') ->
Closure (map (^. childNode) env') (Lambda i' bi (b' ^. childNode))
}
where
fetchBinderInfo :: Info -> [Info]
fetchBinderInfo i = [getInfoBinder i]
setPatternsInfos :: [Binder] -> [Info] -> [Pattern] -> [Pattern]
setPatternsInfos binders infos = snd . setPatternsInfos' binders infos
where
setPatternsInfos' :: [Binder] -> [Info] -> [Pattern] -> (([Binder], [Info]), [Pattern])
setPatternsInfos' bs is [] = ((bs, is), [])
setPatternsInfos' bs is (p : ps) =
let ((bs', is'), p') = setPatInfos bs is p
(bis'', ps') = setPatternsInfos' bs' is' ps
in (bis'', p' : ps')
setPatternsInfos :: [Info] -> [Pattern] -> [Pattern]
setPatternsInfos is ps = snd $ setPatternsInfos' is ps
setPatternsInfos' :: [Info] -> [Pattern] -> ([Info], [Pattern])
setPatternsInfos' is [] = (is, [])
setPatternsInfos' is (p : ps) =
let (is', p') = setPatInfos is p
(is'', ps') = setPatternsInfos' is' ps
in (is'', p' : ps')
setPatInfos :: [Info] -> Pattern -> ([Info], Pattern)
setPatInfos is = \case
PatWildcard x ->
(tl is, PatWildcard (x {_patternWildcardInfo = hd is}))
PatBinder x ->
(tl is, PatBinder (x {_patternBinderInfo = hd is}))
PatConstr x ->
let (is', ps) = setPatternsInfos' (tl is) (x ^. patternConstrArgs)
in (is', PatConstr (x {_patternConstrInfo = hd is, _patternConstrArgs = ps}))
setPatInfos :: [Binder] -> [Info] -> Pattern -> (([Binder], [Info]), Pattern)
setPatInfos bs is = \case
PatWildcard x ->
((bs, tl is), PatWildcard (x {_patternWildcardInfo = hd is}))
PatBinder x ->
((tl bs, is), PatBinder (x {_patternBinder = hd bs}))
PatConstr x ->
let (bis', ps) = setPatternsInfos' bs (tl is) (x ^. patternConstrArgs)
in (bis', PatConstr (x {_patternConstrInfo = hd is, _patternConstrArgs = ps}))
hd :: [a] -> a
hd = List.head
@ -542,23 +588,24 @@ destruct = \case
tl :: [a] -> [a]
tl = List.tail
reassemble :: Node -> [Node] -> Node
reassemble n = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos)
reassembleDetails :: NodeDetails -> [Node] -> Node
reassembleDetails d ns = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) children'
where
d = destruct n
children' :: [NodeChild]
children' = zipWithExact (set childNode) ns (d ^. nodeChildren)
children :: Node -> [Node]
reassemble :: Node -> [Node] -> Node
reassemble = reassembleDetails . destruct
children :: Node -> [NodeChild]
children = (^. nodeChildren) . destruct
-- children together with the number of binders
bchildren :: Node -> [(Int, Node)]
bchildren n =
let ni = destruct n
in zipExact (ni ^. nodeChildBindersNum) (ni ^. nodeChildren)
childrenNodes :: Node -> [Node]
childrenNodes = map (^. childNode) . children
-- shallow children: not under binders
-- | shallow children: not under binders
schildren :: Node -> [Node]
schildren = map snd . filter (\p -> fst p == 0) . bchildren
schildren = map (^. childNode) . filter (\p -> null (p ^. childBinders)) . children
getInfo :: Node -> Info
getInfo = (^. nodeInfo) . destruct

2
src/Juvix/Compiler/Core/Extra/Recursors/Base.hs
View File

@ -1,7 +1,6 @@
module Juvix.Compiler.Core.Extra.Recursors.Base
( module Juvix.Compiler.Core.Data.BinderList,
module Juvix.Compiler.Core.Language,
module Juvix.Compiler.Core.Info.BinderInfo,
module Juvix.Compiler.Core.Extra.Recursors.Collector,
module Juvix.Compiler.Core.Extra.Recursors.Recur,
)
@ -10,5 +9,4 @@ where
import Juvix.Compiler.Core.Data.BinderList (BinderList)
import Juvix.Compiler.Core.Extra.Recursors.Collector
import Juvix.Compiler.Core.Extra.Recursors.Recur
import Juvix.Compiler.Core.Info.BinderInfo
import Juvix.Compiler.Core.Language

10
src/Juvix/Compiler/Core/Extra/Recursors/Collector.hs
View File

@ -16,19 +16,19 @@ makeLenses ''Collector
unitCollector :: Collector a ()
unitCollector = Collector () (\_ _ -> ())
binderInfoCollector' :: BinderList Info -> Collector (Int, [Info]) (BinderList Info)
binderInfoCollector' :: BinderList Binder -> Collector (Int, [Binder]) (BinderList Binder)
binderInfoCollector' ini = Collector ini collect
where
collect :: (Int, [Info]) -> BinderList Info -> BinderList Info
collect :: (Int, [Binder]) -> BinderList Binder -> BinderList Binder
collect (k, bi) c
| k == 0 = c
| otherwise = BL.prepend (reverse bi) c
binderInfoCollector :: Collector (Int, [Info]) (BinderList Info)
binderInfoCollector :: Collector (Int, [Binder]) (BinderList Binder)
binderInfoCollector = binderInfoCollector' mempty
binderNumCollector' :: Int -> Collector (Int, [Info]) Index
binderNumCollector' :: Int -> Collector (Int, [Binder]) Index
binderNumCollector' ini = Collector ini (\(k, _) c -> c + k)
binderNumCollector :: Collector (Int, [Info]) Index
binderNumCollector :: Collector (Int, [Binder]) Index
binderNumCollector = binderNumCollector' 0

8
src/Juvix/Compiler/Core/Extra/Recursors/Fold.hs
View File

@ -7,7 +7,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Base
ufoldG ::
forall c a f.
Applicative f =>
Collector (Int, [Info]) c ->
Collector (Int, [Binder]) c ->
(a -> [a] -> a) ->
(c -> Node -> f a) ->
Node ->
@ -24,8 +24,6 @@ ufoldG coll uplus f = go (coll ^. cEmpty)
ni = destruct n
mas :: [f a]
mas =
zipWith3Exact
(\n' k bis -> go ((coll ^. cCollect) (k, bis) c) n')
map
(\n' -> go ((coll ^. cCollect) (n' ^. childBindersNum, n' ^. childBinders) c) (n' ^. childNode))
(ni ^. nodeChildren)
(ni ^. nodeChildBindersNum)
(ni ^. nodeChildBindersInfo)

8
src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
View File

@ -7,7 +7,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Fold
ufoldA :: Applicative f => (a -> [a] -> a) -> (Node -> f a) -> Node -> f a
ufoldA uplus f = ufoldG unitCollector uplus (const f)
ufoldLA :: Applicative f => (a -> [a] -> a) -> (BinderList Info -> Node -> f a) -> Node -> f a
ufoldLA :: Applicative f => (a -> [a] -> a) -> (BinderList Binder -> Node -> f a) -> Node -> f a
ufoldLA uplus f = ufoldG binderInfoCollector uplus f
ufoldNA :: Applicative f => (a -> [a] -> a) -> (Index -> Node -> f a) -> Node -> f a
@ -19,13 +19,13 @@ walk = ufoldA (foldr mappend)
walkN :: Applicative f => (Index -> Node -> f ()) -> Node -> f ()
walkN = ufoldNA (foldr mappend)
walkL :: Applicative f => (BinderList Info -> Node -> f ()) -> Node -> f ()
walkL :: Applicative f => (BinderList Binder -> Node -> f ()) -> Node -> f ()
walkL = ufoldLA (foldr mappend)
ufold :: (a -> [a] -> a) -> (Node -> a) -> Node -> a
ufold uplus f = runIdentity . ufoldA uplus (return . f)
ufoldL :: (a -> [a] -> a) -> (BinderList Info -> Node -> a) -> Node -> a
ufoldL :: (a -> [a] -> a) -> (BinderList Binder -> Node -> a) -> Node -> a
ufoldL uplus f = runIdentity . ufoldLA uplus (\is -> return . f is)
ufoldN :: (a -> [a] -> a) -> (Index -> Node -> a) -> Node -> a
@ -34,7 +34,7 @@ ufoldN uplus f = runIdentity . ufoldNA uplus (\idx -> return . f idx)
gather :: (a -> Node -> a) -> a -> Node -> a
gather f acc = run . execState acc . walk (\n' -> modify' (`f` n'))
gatherL :: (BinderList Info -> a -> Node -> a) -> a -> Node -> a
gatherL :: (BinderList Binder -> a -> Node -> a) -> a -> Node -> a
gatherL f acc = run . execState acc . walkL (\is n' -> modify' (\a -> f is a n'))
gatherN :: (Index -> a -> Node -> a) -> a -> Node -> a

45
src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
View File

@ -14,12 +14,12 @@ type family DirTy d = res | res -> d where
DirTy 'TopDown = Recur
DirTy 'BottomUp = Node -- For bottom up maps we never recur on the children
-- `umapG` maps the nodes bottom-up, i.e., when invoking the mapper function the
-- | `umapG` maps the nodes bottom-up, i.e., when invoking the mapper function the
-- recursive subnodes have already been mapped
umapG ::
forall c m.
Monad m =>
Collector (Int, [Info]) c ->
Collector (Int, [Binder]) c ->
(c -> Node -> m Node) ->
Node ->
m Node
@ -29,19 +29,13 @@ umapG coll f = go (coll ^. cEmpty)
go c n =
let ni = destruct n
in do
ns <-
sequence $
zipWith3Exact
(\n' k bis -> go ((coll ^. cCollect) (k, bis) c) n')
(ni ^. nodeChildren)
(ni ^. nodeChildBindersNum)
(ni ^. nodeChildBindersInfo)
f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
ns <- mapM (\n' -> go ((coll ^. cCollect) (n' ^. childBindersNum, n' ^. childBinders) c) (n' ^. childNode)) (ni ^. nodeChildren)
f c (reassembleDetails ni ns)
dmapG ::
forall c m.
Monad m =>
Collector (Int, [Info]) c ->
Collector (Int, [Binder]) c ->
(c -> Node -> m Recur) ->
Node ->
m Node
@ -52,23 +46,16 @@ dmapG coll f = go (coll ^. cEmpty)
r <- f c n
case r of
End n' -> return n'
Recur n' -> do
Recur n' ->
let ni = destruct n'
ns <-
sequence $
zipWith3Exact
goChild
(ni ^. nodeChildren)
(ni ^. nodeChildBindersNum)
(ni ^. nodeChildBindersInfo)
return ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
in reassembleDetails ni <$> mapM goChild (ni ^. nodeChildren)
where
goChild :: Node -> Int -> [Info] -> m Node
goChild n'' k bis = go ((coll ^. cCollect) (k, bis) c) n''
goChild :: NodeChild -> m Node
goChild ch = go ((coll ^. cCollect) (ch ^. childBindersNum, ch ^. childBinders) c) (ch ^. childNode)
type CtxTy :: Ctx -> GHC.Type
type family CtxTy x = res | res -> x where
CtxTy 'CtxBinderList = BinderList Info
CtxTy 'CtxBinderList = BinderList Binder
CtxTy 'CtxBinderNum = Index
CtxTy 'CtxNone = ()
@ -83,17 +70,17 @@ type family RetTy m dir mon r = res | res -> mon r where
type BodyTy :: (GHC.Type -> GHC.Type) -> Direction -> Monadic -> Ctx -> Ret -> GHC.Type
type family BodyTy m dir mon x r = res | res -> x r where
BodyTy m dir 'Monadic 'CtxBinderList r = BinderList Info -> Node -> RetTy m dir 'Monadic r
BodyTy m dir 'Monadic 'CtxBinderList r = BinderList Binder -> Node -> RetTy m dir 'Monadic r
BodyTy m dir 'Monadic 'CtxBinderNum r = Int -> Node -> RetTy m dir 'Monadic r
BodyTy m dir 'Monadic 'CtxNone r = Node -> RetTy m dir 'Monadic r
BodyTy _ dir 'NonMonadic 'CtxBinderList r = BinderList Info -> Node -> RetTy Identity dir 'NonMonadic r
BodyTy _ dir 'NonMonadic 'CtxBinderList r = BinderList Binder -> Node -> RetTy Identity dir 'NonMonadic r
BodyTy _ dir 'NonMonadic 'CtxBinderNum r = Int -> Node -> RetTy Identity dir 'NonMonadic r
BodyTy _ dir 'NonMonadic 'CtxNone r = Node -> RetTy Identity dir 'NonMonadic r
type NodeMapArg :: (GHC.Type -> GHC.Type) -> Direction -> Monadic -> CollectorIni -> Ctx -> Ret -> GHC.Type
type family NodeMapArg m dir mon i x r = res | res -> i x r where
NodeMapArg m dir mon 'Ini x r = (CtxTy x, BodyTy m dir mon x r)
NodeMapArg m dir mon 'NoIni 'CtxBinderList r = BinderList Info -> Node -> RetTy m dir mon r
NodeMapArg m dir mon 'NoIni 'CtxBinderList r = BinderList Binder -> Node -> RetTy m dir mon r
NodeMapArg m dir mon 'NoIni 'CtxBinderNum r = Int -> Node -> RetTy m dir mon r
NodeMapArg m dir mon 'NoIni 'CtxNone r = Node -> RetTy m dir mon r
@ -106,7 +93,7 @@ type OverIdentity :: GHC.Type -> GHC.Type
type family OverIdentity t = res where
OverIdentity (a -> b) = a -> OverIdentity b
OverIdentity ((), b) = ((), OverIdentity b)
OverIdentity (BinderList Info, b) = (BinderList Info, OverIdentity b)
OverIdentity (BinderList Binder, b) = (BinderList Binder, OverIdentity b)
OverIdentity (Index, b) = (Index, OverIdentity b)
OverIdentity leaf = Identity leaf
@ -122,7 +109,7 @@ instance EmbedIdentity b => EmbedIdentity ((), b) where
instance EmbedIdentity b => EmbedIdentity (Index, b) where
embedIden (a, b) = (a, embedIden b)
instance EmbedIdentity b => EmbedIdentity (BinderList Info, b) where
instance EmbedIdentity b => EmbedIdentity (BinderList Binder, b) where
embedIden (a, b) = (a, embedIden b)
instance EmbedIdentity Node where
@ -201,7 +188,7 @@ nodeMapE sdir smon sini sctx sret f = case smon :: SMonadic mon of
fromSimple :: forall g. Functor g => g Node -> g Recur
fromSimple = fmap Recur
nodeMapG' ::
Collector (Int, [Info]) c ->
Collector (Int, [Binder]) c ->
(c -> Node -> m (DirTy dir)) ->
Node ->
m Node

24
src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
View File

@ -4,13 +4,13 @@ import Juvix.Compiler.Core.Extra.Recursors.Base
import Juvix.Compiler.Core.Extra.Recursors.Map
import Juvix.Compiler.Core.Extra.Recursors.Parameters
dmapLRM :: Monad m => (BinderList Info -> Node -> m Recur) -> Node -> m Node
dmapLRM :: Monad m => (BinderList Binder -> Node -> m Recur) -> Node -> m Node
dmapLRM = nodeMapI STopDown
dmapLM :: Monad m => (BinderList Info -> Node -> m Node) -> Node -> m Node
dmapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
dmapLM = nodeMapI STopDown
umapLM :: Monad m => (BinderList Info -> Node -> m Node) -> Node -> m Node
umapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
umapLM = nodeMapI SBottomUp
dmapNRM :: Monad m => (Index -> Node -> m Recur) -> Node -> m Node
@ -31,13 +31,13 @@ dmapM = nodeMapI STopDown
umapM :: Monad m => (Node -> m Node) -> Node -> m Node
umapM = nodeMapI SBottomUp
dmapLRM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Recur) -> Node -> m Node
dmapLRM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Recur) -> Node -> m Node
dmapLRM' = nodeMapI STopDown
dmapLM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Node) -> Node -> m Node
dmapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
dmapLM' = nodeMapI STopDown
umapLM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Node) -> Node -> m Node
umapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
umapLM' = nodeMapI SBottomUp
dmapNRM' :: Monad m => (Index, Index -> Node -> m Recur) -> Node -> m Node
@ -49,13 +49,13 @@ dmapNM' = nodeMapI STopDown
umapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
umapNM' = nodeMapI SBottomUp
dmapLR :: (BinderList Info -> Node -> Recur) -> Node -> Node
dmapLR :: (BinderList Binder -> Node -> Recur) -> Node -> Node
dmapLR = nodeMapI STopDown
dmapL :: (BinderList Info -> Node -> Node) -> Node -> Node
dmapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
dmapL = nodeMapI STopDown
umapL :: (BinderList Info -> Node -> Node) -> Node -> Node
umapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
umapL = nodeMapI SBottomUp
dmapNR :: (Index -> Node -> Recur) -> Node -> Node
@ -76,13 +76,13 @@ dmap = nodeMapI STopDown
umap :: (Node -> Node) -> Node -> Node
umap = nodeMapI SBottomUp
dmapLR' :: (BinderList Info, BinderList Info -> Node -> Recur) -> Node -> Node
dmapLR' :: (BinderList Binder, BinderList Binder -> Node -> Recur) -> Node -> Node
dmapLR' = nodeMapI STopDown
dmapL' :: (BinderList Info, BinderList Info -> Node -> Node) -> Node -> Node
dmapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
dmapL' = nodeMapI STopDown
umapL' :: (BinderList Info, BinderList Info -> Node -> Node) -> Node -> Node
umapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
umapL' = nodeMapI SBottomUp
dmapNR' :: (Index, Index -> Node -> Recur) -> Node -> Node

15
src/Juvix/Compiler/Core/Extra/Stripped/Base.hs
View File

@ -33,7 +33,20 @@ mkConstr' :: Symbol -> Tag -> [Node] -> Node
mkConstr' sym = mkConstr (ConstrInfo Nothing TyDynamic sym)
mkLet :: LetInfo -> Node -> Node -> Node
mkLet i v b = NLet (Let i v b)
mkLet i v b = NLet (Let i item b)
where
binder :: Binder
binder =
Binder
{ _binderName = i ^. letInfoBinderName,
_binderType = i ^. letInfoBinderType
}
item :: LetItem
item =
LetItem
{ _letItemBinder = binder,
_letItemValue = v
}
mkLet' :: Node -> Node -> Node
mkLet' = mkLet (LetInfo Nothing TyDynamic)

44
src/Juvix/Compiler/Core/Info/BinderInfo.hs
View File

@ -1,44 +0,0 @@
module Juvix.Compiler.Core.Info.BinderInfo where
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Language
-- | Info about a single binder. Associated with Lambda and Pi.
newtype BinderInfo = BinderInfo {_infoBinder :: Info}
instance IsInfo BinderInfo
kBinderInfo :: Key BinderInfo
kBinderInfo = Proxy
-- | Info about multiple binders. Associated with LetRec.
newtype BindersInfo = BindersInfo {_infoBinders :: [Info]}
instance IsInfo BindersInfo
kBindersInfo :: Key BindersInfo
kBindersInfo = Proxy
makeLenses ''BinderInfo
makeLenses ''BindersInfo
getInfoBinder :: Info -> Info
getInfoBinder i =
case Info.lookup kBinderInfo i of
Just (BinderInfo {..}) -> _infoBinder
Nothing -> Info.empty
getInfoBinders :: Int -> Info -> [Info]
getInfoBinders n i =
case Info.lookup kBindersInfo i of
Just (BindersInfo {..}) -> _infoBinders
Nothing -> replicate n Info.empty
setInfoBinders :: [Info] -> Info -> Info
setInfoBinders = Info.insert . BindersInfo
setInfoBinder :: Info -> Info -> Info
setInfoBinder = Info.insert . BinderInfo
singletonInfoBinder :: Info -> Info
singletonInfoBinder i = setInfoBinder i mempty

15
src/Juvix/Compiler/Core/Info/FreeVarsInfo.hs
View File

@ -30,15 +30,16 @@ computeFreeVarsInfo = umapN go
fvi =
FreeVarsInfo $
foldr
( \(m, n') acc ->
HashMap.unionWith (+) acc $
HashMap.mapKeys (\j -> j - m) $
HashMap.filterWithKey
(\j _ -> j < m)
(getFreeVarsInfo n' ^. infoFreeVars)
( \n' acc ->
let m = n' ^. childBindersNum
in HashMap.unionWith (+) acc $
HashMap.mapKeys (\j -> j - m) $
HashMap.filterWithKey
(\j _ -> j < m)
(getFreeVarsInfo (n' ^. childNode) ^. infoFreeVars)
)
mempty
(bchildren n)
(children n)
getFreeVarsInfo :: Node -> FreeVarsInfo
getFreeVarsInfo = fromJust . Info.lookup kFreeVarsInfo . getInfo

2
src/Juvix/Compiler/Core/Info/IdentInfo.hs
View File

@ -32,7 +32,7 @@ computeIdentInfo = umap go
foldr
(HashMap.unionWith (+) . (^. infoIdents) . getIdentInfo)
mempty
(children n)
(childrenNodes n)
getIdentInfo :: Node -> IdentInfo
getIdentInfo = Info.lookupDefault (IdentInfo mempty) . getInfo

31
src/Juvix/Compiler/Core/Language.hs
View File

@ -9,6 +9,8 @@ import Juvix.Compiler.Core.Language.Nodes
{---------------------------------------------------------------------------------}
type Type = Node
type Var = Var' Info
type Ident = Ident' Info
@ -21,11 +23,17 @@ type BuiltinApp = BuiltinApp' Info Node
type Constr = Constr' Info Node
type Lambda = Lambda' Info Node
type Binder = Binder' Node
type Let = Let' Info Node
type LambdaLhs = LambdaLhs' Info Type
type LetRec = LetRec' Info Node
type Lambda = Lambda' Info Node Type
type LetItem = LetItem' Node Type
type Let = Let' Info Node Type
type LetRec = LetRec' Info Node Type
type Case = Case' Info Info Node
@ -37,11 +45,13 @@ type MatchBranch = MatchBranch' Info Node
type PatternWildcard = PatternWildcard' Info
type PatternBinder = PatternBinder' Info
type PatternBinder = PatternBinder' Info Node
type PatternConstr = PatternConstr' Info
type PatternConstr = PatternConstr' Info Node
type Pattern = Pattern' Info
type Pattern = Pattern' Info Node
type PiLhs = PiLhs' Info Node
type Pi = Pi' Info Node
@ -102,8 +112,6 @@ data Node
-- All nodes in an environment must be values.
type Env = [Node]
type Type = Node
instance HasAtomicity Node where
atomicity = \case
NVar x -> atomicity x
@ -123,3 +131,10 @@ instance HasAtomicity Node where
NPrim x -> atomicity x
NDyn x -> atomicity x
Closure {} -> Aggregate lambdaFixity
emptyBinder :: Binder
emptyBinder =
Binder
{ _binderName = Nothing,
_binderType = NDyn (Dynamic mempty)
}

202
src/Juvix/Compiler/Core/Language/Nodes.hs
View File

@ -10,19 +10,34 @@ import Juvix.Compiler.Core.Language.Base
import Juvix.Compiler.Core.Language.Primitives
-- | De Bruijn index of a locally bound variable.
data Var' i = Var {_varInfo :: i, _varIndex :: !Index}
data Var' i = Var
{ _varInfo :: i,
_varIndex :: !Index
}
-- | Global identifier of a function (with corresponding `Node` in the global
-- context).
data Ident' i = Ident {_identInfo :: i, _identSymbol :: !Symbol}
data Ident' i = Ident
{ _identInfo :: i,
_identSymbol :: !Symbol
}
data Constant' i = Constant {_constantInfo :: i, _constantValue :: !ConstantValue}
data Constant' i = Constant
{ _constantInfo :: i,
_constantValue :: !ConstantValue
}
data ConstantValue
= ConstInteger !Integer
| ConstString !Text
deriving stock (Eq)
-- | Info about a single binder. Associated with Lambda and Pi.
data Binder' ty = Binder
{ _binderName :: Maybe Name,
_binderType :: ty
}
-- Other things we might need in the future:
-- - ConstFloat or ConstFixedPoint
@ -59,26 +74,38 @@ data Constr' i a = Constr
_constrArgs :: ![a]
}
data Lambda' i a = Lambda
-- | Useful for unfolding lambdas
data LambdaLhs' i ty = LambdaLhs
{ _lambdaLhsInfo :: i,
_lambdaLhsBinder :: Binder' ty
}
data Lambda' i a ty = Lambda
{ _lambdaInfo :: i,
_lambdaBinder :: Binder' ty,
_lambdaBody :: !a
}
-- | `let x := value in body` is not reducible to lambda + application for the
-- purposes of ML-polymorphic / dependent type checking or code generation!
data Let' i a = Let
data Let' i a ty = Let
{ _letInfo :: i,
_letValue :: !a,
_letItem :: {-# UNPACK #-} !(LetItem' a ty),
_letBody :: !a
}
data LetItem' a ty = LetItem
{ _letItemBinder :: Binder' ty,
_letItemValue :: a
}
-- | Represents a block of mutually recursive local definitions. Both in the
-- body and in the values `length _letRecValues` implicit binders are introduced
-- which hold the functions/values being defined.
-- the last item _letRecValues will have have index $0 in the body.
data LetRec' i a = LetRec
data LetRec' i a ty = LetRec
{ _letRecInfo :: i,
_letRecValues :: !(NonEmpty a),
_letRecValues :: !(NonEmpty (LetItem' a ty)),
_letRecBody :: !a
}
@ -91,12 +118,13 @@ data Case' i bi a = Case
_caseDefault :: !(Maybe a)
}
-- | `CaseBranch tag argsNum branch`
-- - `argsNum` is the number of arguments of the constructor tagged with `tag`,
-- equal to the number of implicit binders above `branch`
-- | `CaseBranch tag binders bindersNum branch`
-- - `binders` are the arguments of the constructor tagged with `tag`,
-- length of `binders` is equal to `bindersNum`
data CaseBranch' i a = CaseBranch
{ _caseBranchInfo :: i,
_caseBranchTag :: !Tag,
_caseBranchBinders :: [Binder' a],
_caseBranchBindersNum :: !Int,
_caseBranchBody :: !a
}
@ -116,29 +144,34 @@ data Match' i a = Match
-- 2)) (Var 1)) (Var 0)'. So the de Bruijn indices increase from right to left.
data MatchBranch' i a = MatchBranch
{ _matchBranchInfo :: i,
_matchBranchPatterns :: !(NonEmpty (Pattern' i)),
_matchBranchPatterns :: !(NonEmpty (Pattern' i a)),
_matchBranchBody :: !a
}
data Pattern' i
data Pattern' i a
= PatWildcard (PatternWildcard' i)
| PatBinder (PatternBinder' i)
| PatConstr (PatternConstr' i)
deriving stock (Eq)
| PatBinder (PatternBinder' i a)
| PatConstr (PatternConstr' i a)
newtype PatternWildcard' i = PatternWildcard
{ _patternWildcardInfo :: i
}
data PatternBinder' i = PatternBinder
{ _patternBinderInfo :: i,
_patternBinderPattern :: Pattern' i
data PatternBinder' i a = PatternBinder
{ _patternBinder :: Binder' a,
_patternBinderPattern :: Pattern' i a
}
data PatternConstr' i = PatternConstr
data PatternConstr' i a = PatternConstr
{ _patternConstrInfo :: i,
_patternConstrTag :: !Tag,
_patternConstrArgs :: ![Pattern' i]
_patternConstrArgs :: ![Pattern' i a]
}
-- | Useful for unfolding Pi
data PiLhs' i a = PiLhs
{ _piLhsInfo :: i,
_piLhsBinder :: Binder' a
}
-- | Dependent Pi-type. Compilation-time only. Pi implicitly introduces a binder
@ -146,10 +179,17 @@ data PatternConstr' i = PatternConstr
-- body` in more familiar notation, but references to `x` in `body` are via de
-- Bruijn index. For example, Pi A : Type . A -> A translates to (omitting
-- Infos): Pi (Univ level) (Pi (Var 0) (Var 1)).
data Pi' i a = Pi {_piInfo :: i, _piType :: !a, _piBody :: !a}
data Pi' i a = Pi
{ _piInfo :: i,
_piBinder :: Binder' a,
_piBody :: !a
}
-- | Universe. Compilation-time only.
data Univ' i = Univ {_univInfo :: i, _univLevel :: !Int}
data Univ' i = Univ
{ _univInfo :: i,
_univLevel :: !Int
}
-- | Type constructor application. Compilation-time only.
data TypeConstr' i a = TypeConstr
@ -197,13 +237,13 @@ instance HasAtomicity (Constr' i a) where
| null _constrArgs = Atom
| otherwise = Aggregate lambdaFixity
instance HasAtomicity (Lambda' i a) where
instance HasAtomicity (Lambda' i a ty) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (Let' i a) where
instance HasAtomicity (Let' i a ty) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (LetRec' i a) where
instance HasAtomicity (LetRec' i a ty) where
atomicity _ = Aggregate lambdaFixity
instance HasAtomicity (Case' i bi a) where
@ -215,15 +255,15 @@ instance HasAtomicity (Match' i a) where
instance HasAtomicity (PatternWildcard' i) where
atomicity _ = Atom
instance HasAtomicity (PatternBinder' i) where
instance HasAtomicity (PatternBinder' i a) where
atomicity _ = Atom
instance HasAtomicity (PatternConstr' i) where
instance HasAtomicity (PatternConstr' i a) where
atomicity PatternConstr {..}
| null _patternConstrArgs = Atom
| otherwise = Aggregate appFixity
instance HasAtomicity (Pattern' i) where
instance HasAtomicity (Pattern' i a) where
atomicity = \case
PatWildcard x -> atomicity x
PatBinder x -> atomicity x
@ -247,6 +287,31 @@ instance HasAtomicity (Dynamic' i) where
lambdaFixity :: Fixity
lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
makeLenses ''LambdaLhs'
makeLenses ''PiLhs'
makeLenses ''Binder'
makeLenses ''Var'
makeLenses ''Ident'
makeLenses ''Constant'
makeLenses ''App'
makeLenses ''BuiltinApp'
makeLenses ''Constr'
makeLenses ''Let'
makeLenses ''LetRec'
makeLenses ''Case'
makeLenses ''CaseBranch'
makeLenses ''Match'
makeLenses ''MatchBranch'
makeLenses ''PatternWildcard'
makeLenses ''PatternBinder'
makeLenses ''PatternConstr'
makeLenses ''Pi'
makeLenses ''Lambda'
makeLenses ''Univ'
makeLenses ''TypeConstr'
makeLenses ''Dynamic'
makeLenses ''LetItem'
instance Eq (Var' i) where
(Var _ idx1) == (Var _ idx2) = idx1 == idx2
@ -268,39 +333,20 @@ instance Eq a => Eq (BuiltinApp' i a) where
instance Eq a => Eq (Constr' i a) where
(Constr _ tag1 args1) == (Constr _ tag2 args2) = tag1 == tag2 && args1 == args2
instance Eq a => Eq (Lambda' i a) where
(Lambda _ b1) == (Lambda _ b2) = b1 == b2
instance Eq a => Eq (Let' i a) where
(Let _ v1 b1) == (Let _ v2 b2) = v1 == v2 && b1 == b2
instance Eq a => Eq (LetRec' i a) where
(LetRec _ vs1 b1) == (LetRec _ vs2 b2) = vs1 == vs2 && b1 == b2
instance Eq a => Eq (Case' i bi a) where
(Case _ v1 bs1 def1) == (Case _ v2 bs2 def2) = v1 == v2 && bs1 == bs2 && def1 == def2
instance Eq a => Eq (CaseBranch' i a) where
(CaseBranch _ tag1 n1 b1) == (CaseBranch _ tag2 n2 b2) = tag1 == tag2 && n1 == n2 && b1 == b2
(==) =
eqOn (^. caseBranchTag)
..&&.. eqOn (^. caseBranchBody)
instance Eq a => Eq (Match' i a) where
(Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
instance Eq a => Eq (MatchBranch' i a) where
(MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
instance Eq (PatternWildcard' i) where
_ == _ = True
instance Eq (PatternBinder' i) where
(PatternBinder _ p1) == (PatternBinder _ p2) = p1 == p2
instance Eq (PatternConstr' i) where
(PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
instance Eq a => Eq (Pi' i a) where
(Pi _ ty1 b1) == (Pi _ ty2 b2) = ty1 == ty2 && b1 == b2
instance Eq (Univ' i) where
(Univ _ l1) == (Univ _ l2) = l1 == l2
@ -313,26 +359,40 @@ instance Eq (TypePrim' i) where
instance Eq (Dynamic' i) where
(Dynamic _) == (Dynamic _) = True
makeLenses ''Var'
makeLenses ''Ident'
makeLenses ''Constant'
makeLenses ''App'
makeLenses ''BuiltinApp'
makeLenses ''Constr'
makeLenses ''Let'
makeLenses ''LetRec'
makeLenses ''Case'
makeLenses ''CaseBranch'
makeLenses ''Match'
makeLenses ''MatchBranch'
makeLenses ''PatternWildcard'
makeLenses ''PatternBinder'
makeLenses ''PatternConstr'
makeLenses ''Pi'
makeLenses ''Lambda'
makeLenses ''Univ'
makeLenses ''TypeConstr'
makeLenses ''Dynamic'
deriving stock instance Eq a => Eq (Pattern' i a)
instance Eq a => Eq (LetItem' a ty) where
(==) = eqOn (^. letItemValue)
-- | ignores the binder
instance Eq a => Eq (Lambda' i a ty) where
(==) = eqOn (^. lambdaBody)
-- | ignores the binder
instance Eq a => Eq (Let' i a ty) where
(==) =
eqOn (^. letItem)
..&&.. eqOn (^. letBody)
instance Eq a => Eq (LetRec' i a ty) where
(==) =
eqOn (^. letRecBody)
..&&.. eqOn (^. letRecValues)
instance Eq a => Eq (Pi' i a) where
(==) =
eqOn (^. piBinder . binderType)
..&&.. eqOn (^. piBody)
-- | ignores the binder
instance Eq a => Eq (PatternBinder' i a) where
(==) = eqOn (^. patternBinderPattern)
instance Eq a => Eq (MatchBranch' i a) where
(MatchBranch _ pats1 b1) == (MatchBranch _ pats2 b2) = pats1 == pats2 && b1 == b2
instance Eq a => Eq (PatternConstr' i a) where
(PatternConstr _ tag1 ps1) == (PatternConstr _ tag2 ps2) = tag1 == tag2 && ps1 == ps2
instance Hashable (Ident' i) where
hashWithSalt s = hashWithSalt s . (^. identSymbol)

10
src/Juvix/Compiler/Core/Language/Stripped.hs
View File

@ -56,14 +56,20 @@ type Constant = Constant' ()
type Apps = Apps' Fun () Node
data Fun = FunVar Var | FunIdent Ident
data Fun
= FunVar Var
| FunIdent Ident
deriving stock (Eq)
type BuiltinApp = BuiltinApp' () Node
type Constr = Constr' ConstrInfo Node
type Let = Let' LetInfo Node
type Binder = Binder' Type
type LetItem = LetItem' Node Type
type Let = Let' LetInfo Node Type
type Case = Case' CaseInfo CaseBranchInfo Node

6
src/Juvix/Compiler/Core/Language/Stripped/Type.hs
View File

@ -3,7 +3,11 @@ module Juvix.Compiler.Core.Language.Stripped.Type where
import Juvix.Compiler.Core.Language.Base
import Juvix.Compiler.Core.Language.Primitives
data Type = TyDynamic | TyPrim Primitive | TyApp TypeApp | TyFun TypeFun
data Type
= TyDynamic
| TyPrim Primitive
| TyApp TypeApp
| TyFun TypeFun
deriving stock (Eq)
data TypeApp = TypeApp

64
src/Juvix/Compiler/Core/Pretty/Base.hs
View File

@ -9,9 +9,7 @@ import Data.HashMap.Strict qualified as HashMap
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Data.Stripped.InfoTable qualified as Stripped
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.BinderInfo
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Info.TypeInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Language.Stripped qualified as Stripped
import Juvix.Compiler.Core.Pretty.Options
@ -126,12 +124,12 @@ ppCodeConstr' name c = do
Nothing -> ppCode (c ^. constrTag)
return $ foldl' (<+>) n' args'
ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Maybe Name -> Maybe (Doc Ann) -> Let' i a -> Sem r (Doc Ann)
ppCodeLet' :: (PrettyCode a, Member (Reader Options) r) => Maybe Name -> Maybe (Doc Ann) -> Let' i a ty -> Sem r (Doc Ann)
ppCodeLet' name mty lt = do
n' <- case name of
Just nm -> ppCode nm
Nothing -> return kwQuestion
v' <- ppCode (lt ^. letValue)
v' <- ppCode (lt ^. letItem . letItemValue)
b' <- ppCode (lt ^. letBody)
let tty = case mty of
Just ty ->
@ -162,7 +160,7 @@ instance PrettyCode PatternWildcard where
instance PrettyCode PatternBinder where
ppCode PatternBinder {..} = do
n <- case getInfoName _patternBinderInfo of
n <- case _patternBinder ^. binderName of
Just name -> ppCode name
Nothing -> return kwQuestion
case _patternBinderPattern of
@ -191,8 +189,9 @@ ppPatterns pats = do
instance PrettyCode Let where
ppCode :: forall r. Member (Reader Options) r => Let -> Sem r (Doc Ann)
ppCode x = do
let name = getInfoName (getInfoBinder (x ^. letInfo))
ty = getInfoType (getInfoBinder (x ^. letInfo))
let binder = x ^. letItem . letItemBinder
name = binder ^. binderName
ty = binder ^. binderType
in do
mty <- case ty of
NDyn {} -> return Nothing
@ -202,24 +201,23 @@ instance PrettyCode Let where
instance PrettyCode LetRec where
ppCode :: forall r. Member (Reader Options) r => LetRec -> Sem r (Doc Ann)
ppCode LetRec {..} = do
let n = length _letRecValues
ns <- mapM getName (getInfoBinders n _letRecInfo)
vs <- mapM ppCode _letRecValues
names <- mapM (getName . (^. letItemBinder)) _letRecValues
vs <- mapM (ppCode . (^. letItemValue)) _letRecValues
b' <- ppCode _letRecBody
return $ case ns of
[hns] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
return $ case names of
hns :| [] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
_ ->
let bss =
indent' $
align $
concatWith (\a b -> a <> kwSemicolon <> line <> b) $
zipWithExact (\name val -> name <+> kwAssign <+> val) ns (toList vs)
nss = enclose kwSquareL kwSquareR (concatWith (<+>) ns)
zipWithExact (\name val -> name <+> kwAssign <+> val) (toList names) (toList vs)
nss = enclose kwSquareL kwSquareR (concatWith (<+>) names)
in kwLetRec <> nss <> line <> bss <> line <> kwIn <> line <> b'
where
getName :: Info -> Sem r (Doc Ann)
getName :: Binder -> Sem r (Doc Ann)
getName i =
case getInfoName i of
case i ^. binderName of
Just name -> ppCode name
Nothing -> return kwQuestion
@ -238,13 +236,12 @@ instance PrettyCode Node where
NCtr x ->
let name = getInfoName (x ^. constrInfo)
in ppCodeConstr' name x
NLam (Lambda i body) -> do
NLam (Lambda _ bi body) -> do
b <- ppCode body
let bi = getInfoBinder i
lam <- case getInfoName bi of
lam <- case bi ^. binderName of
Just name -> do
n <- ppCode name
case getInfoType bi of
case bi ^. binderType of
NDyn {} -> return $ kwLambda <> n
ty -> do
tty <- ppCode ty
@ -254,28 +251,29 @@ instance PrettyCode Node where
NLet x -> ppCode x
NRec l -> ppCode l
NCase x@Case {..} ->
let branchBinderNames = map (\(CaseBranch {..}) -> map getInfoName (getInfoBinders _caseBranchBindersNum _caseBranchInfo)) _caseBranches
branchTagNames = map (\(CaseBranch {..}) -> getInfoName _caseBranchInfo) _caseBranches
let branchBinderNames = map (\CaseBranch {..} -> map (^. binderName) _caseBranchBinders) _caseBranches
branchTagNames = map (\CaseBranch {..} -> getInfoName _caseBranchInfo) _caseBranches
in ppCodeCase' branchBinderNames branchTagNames x
NMatch Match {..} -> do
let branchPatterns = map (^. matchBranchPatterns) _matchBranches
let branchBodies = map (^. matchBranchBody) _matchBranches
branchBodies = map (^. matchBranchBody) _matchBranches
pats <- mapM ppPatterns branchPatterns
vs <- mapM ppCode _matchValues
bs <- sequence $ zipWithExact (\ps br -> ppCode br >>= \br' -> return $ ps <+> kwMapsto <+> br') pats branchBodies
let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
return $ kwMatch <+> hsep (punctuate comma (toList vs)) <+> kwWith <+> bss
NPi Pi {..} ->
case getInfoName $ getInfoBinder _piInfo of
Just name -> do
n <- ppCode name
ty <- ppCode _piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
Nothing -> do
ty <- ppLeftExpression funFixity _piType
b <- ppRightExpression funFixity _piBody
return $ ty <+> kwArrow <+> b
let piType = _piBinder ^. binderType
in case _piBinder ^. binderName of
Just name -> do
n <- ppCode name
ty <- ppCode piType
b <- ppCode _piBody
return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
Nothing -> do
ty <- ppLeftExpression funFixity piType
b <- ppRightExpression funFixity _piBody
return $ ty <+> kwArrow <+> b
NUniv Univ {..} ->
return $ kwType <+> pretty _univLevel
NPrim TypePrim {..} -> ppCode _typePrimPrimitive

38
src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
View File

@ -8,24 +8,22 @@ import Juvix.Compiler.Core.Data.BinderList (BinderList)
import Juvix.Compiler.Core.Data.BinderList qualified as BL
import Juvix.Compiler.Core.Data.InfoTableBuilder
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info.BinderInfo qualified as Info
import Juvix.Compiler.Core.Info.NameInfo
import Juvix.Compiler.Core.Pretty
import Juvix.Compiler.Core.Transformation.Base
lambdaLiftNode :: forall r. Member InfoTableBuilder r => BinderList Info -> Node -> Sem r Node
lambdaLiftNode :: forall r. Member InfoTableBuilder r => BinderList Binder -> Node -> Sem r Node
lambdaLiftNode aboveBl top =
mkLambdas topArgs <$> dmapLRM' (topArgsBinderList <> aboveBl, go) body
reLambdas topArgs <$> dmapLRM' (topArgsBinderList <> aboveBl, go) body
where
(topArgs, body) = unfoldLambdas top
topArgsBinderList :: BinderList Info
topArgsBinderList = BL.fromList topArgs
topArgsBinderList :: BinderList Binder
topArgsBinderList = BL.fromList (map (^. lambdaLhsBinder) topArgs)
typeFromArgs :: [ArgumentInfo] -> Type
typeFromArgs = \case
[] -> mkDynamic' -- change this when we have type info about the body
(a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
-- extracts the argument info from the binder
go :: BinderList Info -> Node -> Sem r Recur
go :: BinderList Binder -> Node -> Sem r Recur
go bl = \case
NLam l -> goLambda l
NRec l -> goLetRec l
@ -33,15 +31,13 @@ lambdaLiftNode aboveBl top =
where
goLambda :: Lambda -> Sem r Recur
goLambda lm = do
let lambdaBinder :: Info
lambdaBinder = Info.getInfoBinder (lm ^. lambdaInfo)
l' <- lambdaLiftNode (BL.extend lambdaBinder bl) (NLam lm)
l' <- lambdaLiftNode (BL.extend (lm ^. lambdaBinder) bl) (NLam lm)
let freevars = toList (freeVarsSet l')
freevarsAssocs :: [(Index, Info)]
freevarsAssocs :: [(Index, Binder)]
freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
fBody' = captureFreeVars freevarsAssocs l'
argsInfo :: [ArgumentInfo]
argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
argsInfo = map (argumentInfoFromBinder . snd) freevarsAssocs
f <- freshSymbol
registerIdent
IdentifierInfo
@ -59,20 +55,20 @@ lambdaLiftNode aboveBl top =
goLetRec :: LetRec -> Sem r Recur
goLetRec letr = do
let defs :: [Node]
defs = toList (letr ^. letRecValues)
defs = toList (letr ^.. letRecValues . each . letItemValue)
ndefs :: Int
ndefs = length defs
letRecBinders :: [Info]
letRecBinders = Info.getInfoBinders ndefs (letr ^. letRecInfo)
bl' :: BinderList Info
letRecBinders :: [Binder]
letRecBinders = letr ^.. letRecValues . each . letItemBinder
bl' :: BinderList Binder
bl' = BL.prepend letRecBinders bl
topSyms :: [Symbol] <- forM defs (const freshSymbol)
let recItemsFreeVars :: [(Var, Info)]
let recItemsFreeVars :: [(Var, Binder)]
recItemsFreeVars = mapMaybe helper (toList (mconcatMap freeVarsSet defs))
where
-- free vars in each let
-- throw away variables bound in the letrec and shift others
helper :: Var -> Maybe (Var, Info)
helper :: Var -> Maybe (Var, Binder)
helper v
| v ^. varIndex < ndefs = Nothing
| otherwise = Just (set varIndex idx' v, BL.lookup idx' bl)
@ -99,18 +95,18 @@ lambdaLiftNode aboveBl top =
[ do
let topBody = captureFreeVars (map (first (^. varIndex)) recItemsFreeVars) b
argsInfo :: [ArgumentInfo]
argsInfo = map (argumentInfoFromInfo . snd) recItemsFreeVars
argsInfo = map (argumentInfoFromBinder . snd) recItemsFreeVars
registerIdentNode sym topBody
registerIdent
IdentifierInfo
{ _identifierSymbol = sym,
_identifierName = getInfoName itemInfo,
_identifierName = itemBinder ^. binderName,
_identifierType = typeFromArgs argsInfo,
_identifierArgsNum = length recItemsFreeVars,
_identifierArgsInfo = argsInfo,
_identifierIsExported = False
}
| (sym, (itemInfo, b)) <- zipExact topSyms (zipExact letRecBinders liftedDefs)
| (sym, (itemBinder, b)) <- zipExact topSyms (zipExact letRecBinders liftedDefs)
]
letItems :: [Node]
letItems =

104
src/Juvix/Compiler/Core/Translation/FromSource.hs
View File

@ -4,19 +4,18 @@ module Juvix.Compiler.Core.Translation.FromSource
)
where
import Control.Monad.Combinators.NonEmpty qualified as NonEmpty
import Control.Monad.Fail qualified as P
import Control.Monad.Trans.Class (lift)
import Data.HashMap.Strict qualified as HashMap
import Data.List qualified as List
import Data.List.NonEmpty (fromList)
import Data.List.NonEmpty qualified as NonEmpty
import Juvix.Compiler.Core.Data.InfoTable
import Juvix.Compiler.Core.Data.InfoTableBuilder
import Juvix.Compiler.Core.Extra
import Juvix.Compiler.Core.Info qualified as Info
import Juvix.Compiler.Core.Info.BinderInfo as BinderInfo
import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
import Juvix.Compiler.Core.Info.NameInfo as NameInfo
import Juvix.Compiler.Core.Info.TypeInfo as TypeInfo
import Juvix.Compiler.Core.Language
import Juvix.Compiler.Core.Transformation.Eta
import Juvix.Compiler.Core.Translation.FromSource.Lexer
@ -38,11 +37,6 @@ runParser fileName tab input =
(_, Left err) -> Left (ParserError err)
(tbl, Right r) -> Right (tbl, r)
binderInfo :: Name -> Type -> Info
binderInfo name ty =
let info = setInfoType ty (Info.singleton (NameInfo name))
in Info.singleton (BinderInfo info)
freshName ::
Member NameIdGen r =>
NameKind ->
@ -203,17 +197,15 @@ parseDefinition sym ty = do
&& not (isDynamic (typeTarget ty))
)
$ parseFailure off "type mismatch: too many lambdas"
lift $ setIdentArgsInfo sym (map toArgumentInfo is)
lift $ setIdentArgsInfo sym (map (toArgumentInfo . (^. lambdaLhsBinder)) is)
where
toArgumentInfo :: Info -> ArgumentInfo
toArgumentInfo i =
toArgumentInfo :: Binder -> ArgumentInfo
toArgumentInfo bi =
ArgumentInfo
{ _argumentName = getInfoName bi,
_argumentType = getInfoType bi,
{ _argumentName = bi ^. binderName,
_argumentType = bi ^. binderType,
_argumentIsImplicit = Explicit
}
where
bi = getInfoBinder i
statementInductive ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -367,7 +359,7 @@ seqExpr' varsNum vars node = do
mkConstr
Info.empty
(BuiltinTag TagBind)
[node, mkLambda (binderInfo name mkDynamic') node']
[node, mkLambda mempty (Binder (Just name) mkDynamic') node']
cmpExpr ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -569,8 +561,8 @@ atoms ::
HashMap Text Level ->
ParsecS r Node
atoms varsNum vars = do
es <- P.some (atom varsNum vars)
return $ mkApps' (List.head es) (List.tail es)
es <- NonEmpty.some (atom varsNum vars)
return $ mkApps' (head es) (NonEmpty.tail es)
atom ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -649,8 +641,9 @@ exprPi varsNum vars = do
ty <- expr varsNum vars
kw kwComma
let vars' = HashMap.insert (name ^. nameText) varsNum vars
bi = Binder (Just name) ty
body <- expr (varsNum + 1) vars'
return $ mkPi (binderInfo name ty) ty body
return $ mkPi mempty bi body
exprLambda ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -661,8 +654,9 @@ exprLambda varsNum vars = do
lambda
(name, mty) <- lambdaName
let vars' = HashMap.insert (name ^. nameText) varsNum vars
bi = Binder (Just name) (fromMaybe mkDynamic' mty)
body <- bracedExpr (varsNum + 1) vars'
return $ mkLambda (binderInfo name (fromMaybe mkDynamic' mty)) body
return $ mkLambda mempty bi body
where
lambdaName =
parens
@ -687,7 +681,9 @@ exprLetrecOne varsNum vars = do
value <- bracedExpr (varsNum + 1) vars'
kw kwIn
body <- bracedExpr (varsNum + 1) vars'
return $ mkLetRec (Info.singleton (BindersInfo [Info.singleton (NameInfo name)])) (fromList [value]) body
let item :: LetItem
item = LetItem (Binder (Just name) mkDynamic') value
return $ mkLetRec mempty (pure item) body
exprLetrecMany ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -701,35 +697,33 @@ exprLetrecMany varsNum vars = do
parseFailure off "expected at least one identifier name in letrec signature"
let (vars', varsNum') = foldl' (\(vs, k) txt -> (HashMap.insert txt k vs, k + 1)) (vars, varsNum) defNames
defs <- letrecDefs defNames varsNum' vars'
kw kwIn
body <- bracedExpr varsNum' vars'
let infos = map (Info.singleton . NameInfo . fst) defs
let values = map snd defs
return $ mkLetRec (Info.singleton (BindersInfo infos)) (fromList values) body
return $ mkLetRec mempty defs body
letrecNames :: ParsecS r [Text]
letrecNames = P.between (symbol "[") (symbol "]") (P.many identifier)
letrecNames :: ParsecS r (NonEmpty Text)
letrecNames = P.between (symbol "[") (symbol "]") (NonEmpty.some identifier)
letrecDefs ::
forall r.
Members '[InfoTableBuilder, NameIdGen] r =>
[Text] ->
NonEmpty Text ->
Index ->
HashMap Text Level ->
ParsecS r [(Name, Node)]
letrecDefs names varsNum vars = case names of
[] -> return []
n : names' -> do
off <- P.getOffset
(txt, i) <- identifierL
when (n /= txt) $
parseFailure off "identifier name doesn't match letrec signature"
name <- lift $ freshName KNameLocal txt i
kw kwAssign
v <- bracedExpr varsNum vars
if
| null names' -> optional (kw kwSemicolon) >> kw kwIn
| otherwise -> kw kwSemicolon
rest <- letrecDefs names' varsNum vars
return $ (name, v) : rest
ParsecS r (NonEmpty LetItem)
letrecDefs names varsNum vars = forM names letrecItem
where
letrecItem :: Text -> ParsecS r LetItem
letrecItem n = do
off <- P.getOffset
(txt, i) <- identifierL
when (n /= txt) $
parseFailure off "identifier name doesn't match letrec signature"
name <- lift $ freshName KNameLocal txt i
kw kwAssign
v <- bracedExpr varsNum vars
kw kwSemicolon
return $ LetItem (Binder (Just name) mkDynamic') v
letrecDef ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -756,8 +750,9 @@ exprLet varsNum vars = do
value <- bracedExpr varsNum vars
kw kwIn
let vars' = HashMap.insert (name ^. nameText) varsNum vars
binder = Binder (Just name) (fromMaybe mkDynamic' mty)
body <- bracedExpr (varsNum + 1) vars'
return $ mkLet (binderInfo name (fromMaybe mkDynamic' mty)) value body
return $ mkLet mempty binder value body
exprCase ::
Members '[InfoTableBuilder, NameIdGen] r =>
@ -820,12 +815,12 @@ caseMatchingBranch varsNum vars = do
txt <- identifier
r <- lift (getIdent txt)
case r of
Just (IdentFun {}) ->
Just IdentFun {} ->
parseFailure off ("not a constructor: " ++ fromText txt)
Just (IdentInd {}) ->
Just IdentInd {} ->
parseFailure off ("not a constructor: " ++ fromText txt)
Just (IdentConstr tag) -> do
ns <- P.many parseLocalName
ns :: [Name] <- P.many parseLocalName
let bindersNum = length ns
ci <- lift $ getConstructorInfo tag
when
@ -841,8 +836,9 @@ caseMatchingBranch varsNum vars = do
(vars, varsNum)
ns
br <- bracedExpr (varsNum + bindersNum) vars'
let info = setInfoName (ci ^. constructorName) $ setInfoBinders (map (Info.singleton . NameInfo) ns) Info.empty
return $ CaseBranch info tag bindersNum br
let info = setInfoName (ci ^. constructorName) mempty
binders = [Binder (Just name) mkDynamic' | name <- ns]
return $ CaseBranch info tag binders bindersNum br
Nothing ->
parseFailure off ("undeclared identifier: " ++ fromText txt)
@ -894,14 +890,15 @@ matchBranch patsNum varsNum vars = do
kw kwAssign
unless (length pats == patsNum) $
parseFailure off "wrong number of patterns"
let pis = concatMap (reverse . getBinderPatternInfos) pats
let (vars', varsNum') =
let pis :: [Binder]
pis = concatMap (reverse . getBinderPatternInfos) pats
(vars', varsNum') =
foldl'
( \(vs, k) name ->
(HashMap.insert (name ^. nameText) k vs, k + 1)
)
(vars, varsNum)
(map (fromJust . getInfoName) pis)
(map (fromJust . (^. binderName)) pis)
br <- bracedExpr varsNum' vars'
return $ MatchBranch Info.empty (fromList pats) br
@ -939,7 +936,8 @@ binderOrConstrPattern parseArgs = do
n <- lift $ freshName KNameLocal txt i
mp <- optional binderPattern
let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
return $ PatBinder (PatternBinder (setInfoName n Info.empty) pat)
binder = Binder (Just n) mkDynamic'
return $ PatBinder (PatternBinder binder pat)
binderPattern ::
Members '[InfoTableBuilder, NameIdGen] r =>

3
src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
View File

@ -11,3 +11,6 @@ fromMain = error "not yet implemented"
translateNode :: Node -> Stripped.Node
translateNode _ = Stripped.mkVar' 0
translateType :: Node -> Stripped.Type
translateType _ = error "not yet implemented"

10
src/Juvix/Prelude/Base.hs
View File

@ -366,13 +366,21 @@ readerState m = get >>= (`runReader` m)
infixr 3 .&&.
(.&&.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
(a .&&. b) c = a c && b c
(f .&&. g) a = f a && g a
infixr 3 ..&&..
(..&&..) :: (a -> b -> Bool) -> (a -> b -> Bool) -> (a -> b -> Bool)
(f ..&&.. g) a = f a .&&. g a
infixr 2 .||.
(.||.) :: (a -> Bool) -> (a -> Bool) -> a -> Bool
(a .||. b) c = a c || b c
eqOn :: Eq b => (a -> b) -> a -> a -> Bool
eqOn = ((==) `on`)
class CanonicalProjection a b where
project :: a -> b

2
tests/Core/positive/test040.jvc
View File

@ -31,7 +31,7 @@ def mutrec :=
1
else
x * f (x - 1)
} in z
} in z;
in writeLn (f 5) >> writeLn (f 10) >> writeLn (f 100) >> writeLn (g 5) >> writeLn (h 5);
letrec x := 3