mirror of
https://github.com/anoma/juvix.git
synced 2025-01-04 21:51:35 +03:00
Remove type arguments and type abstractions from Nodes (#1655)
This commit is contained in:
Łukasz Czajka
GitHub
parent
503f5279ba
commit
d9b020ec27
@ -14,14 +14,21 @@ runCommand opts = do
|
||||
(tab, mnode) <- getRight (mapLeft JuvixError (Core.runParser f Core.emptyInfoTable s'))
|
||||
let tab' = Core.applyTransformations (project opts ^. coreReadTransformations) tab
|
||||
embed (Scoper.scopeTrace tab')
|
||||
unless (project opts ^. coreReadNoPrint) (renderStdOut (Core.ppOut opts tab'))
|
||||
unless (project opts ^. coreReadNoPrint) $ do
|
||||
renderStdOut (Core.ppOut opts tab')
|
||||
whenJust mnode $ doEval tab'
|
||||
where
|
||||
doEval :: Core.InfoTable -> Core.Node -> Sem r ()
|
||||
doEval tab' node = when (project opts ^. coreReadEval) $ do
|
||||
embed (putStrLn "--------------------------------")
|
||||
embed (putStrLn "| Eval |")
|
||||
embed (putStrLn "--------------------------------")
|
||||
Eval.evalAndPrint opts tab' node
|
||||
doEval tab' node =
|
||||
if
|
||||
| project opts ^. coreReadEval -> do
|
||||
embed (putStrLn "--------------------------------")
|
||||
embed (putStrLn "| Eval |")
|
||||
embed (putStrLn "--------------------------------")
|
||||
Eval.evalAndPrint opts tab' node
|
||||
| otherwise -> do
|
||||
embed (putStrLn "-- Node")
|
||||
renderStdOut (Core.ppOut opts node)
|
||||
embed (putStrLn "")
|
||||
f :: FilePath
|
||||
f = project opts ^. coreReadInputFile . pathPath
|
||||
|
||||
@ -41,7 +41,6 @@ data IdentifierInfo = IdentifierInfo
|
||||
_identifierLocation :: Maybe Location,
|
||||
_identifierSymbol :: Symbol,
|
||||
_identifierType :: Type,
|
||||
-- _identifierArgsNum will be used often enough to justify avoiding recomputation
|
||||
_identifierArgsNum :: Int,
|
||||
_identifierArgsInfo :: [ArgumentInfo],
|
||||
_identifierIsExported :: Bool
|
||||
|
||||
@ -5,5 +5,6 @@ import Juvix.Prelude
|
||||
data TransformationId
|
||||
= LambdaLifting
|
||||
| TopEtaExpand
|
||||
| RemoveTypeArgs
|
||||
| Identity
|
||||
deriving stock (Data)
|
||||
|
||||
@ -44,6 +44,7 @@ pcompletions = do
|
||||
LambdaLifting -> strLifting
|
||||
TopEtaExpand -> strTopEtaExpand
|
||||
Identity -> strIdentity
|
||||
RemoveTypeArgs -> strRemoveTypeArgs
|
||||
|
||||
lexeme :: MonadParsec e Text m => m a -> m a
|
||||
lexeme = L.lexeme L.hspace
|
||||
@ -59,12 +60,14 @@ transformation =
|
||||
symbol strLifting $> LambdaLifting
|
||||
<|> symbol strIdentity $> Identity
|
||||
<|> symbol strTopEtaExpand $> TopEtaExpand
|
||||
<|> symbol strRemoveTypeArgs $> RemoveTypeArgs
|
||||
|
||||
allStrings :: [Text]
|
||||
allStrings =
|
||||
[ strLifting,
|
||||
strTopEtaExpand,
|
||||
strIdentity
|
||||
strIdentity,
|
||||
strRemoveTypeArgs
|
||||
]
|
||||
|
||||
strLifting :: Text
|
||||
@ -75,3 +78,6 @@ strTopEtaExpand = "top-eta-expand"
|
||||
|
||||
strIdentity :: Text
|
||||
strIdentity = "identity"
|
||||
|
||||
strRemoveTypeArgs :: Text
|
||||
strRemoveTypeArgs = "remove-type-args"
|
||||
|
||||
@ -182,6 +182,11 @@ isDynamic = \case
|
||||
NDyn {} -> True
|
||||
_ -> False
|
||||
|
||||
isTypeConstr :: Type -> Bool
|
||||
isTypeConstr ty = case typeTarget ty of
|
||||
NUniv {} -> True
|
||||
_ -> False
|
||||
|
||||
-- | `expandType argtys ty` expands the dynamic target of `ty` to match the
|
||||
-- number of arguments with types specified by `argstys`. For example,
|
||||
-- `expandType [int, string] (int -> any) = int -> string -> any`.
|
||||
|
||||
@ -32,3 +32,13 @@ binderNumCollector' ini = Collector ini (\(k, _) c -> c + k)
|
||||
|
||||
binderNumCollector :: Collector (Int, [Binder]) Index
|
||||
binderNumCollector = binderNumCollector' 0
|
||||
|
||||
pairCollector :: Collector a b -> Collector a c -> Collector a (b, c)
|
||||
pairCollector coll1 coll2 =
|
||||
Collector
|
||||
{ _cEmpty = (coll1 ^. cEmpty, coll2 ^. cEmpty),
|
||||
_cCollect = \a (b, c) -> ((coll1 ^. cCollect) a b, (coll2 ^. cCollect) a c)
|
||||
}
|
||||
|
||||
identityCollector :: c -> Collector a c
|
||||
identityCollector ini = Collector ini (const id)
|
||||
|
||||
@ -9,10 +9,10 @@ import Juvix.Compiler.Core.Extra.Base
|
||||
import Juvix.Compiler.Core.Extra.Recursors.Base
|
||||
import Juvix.Compiler.Core.Extra.Recursors.Parameters
|
||||
|
||||
type DirTy :: Direction -> GHC.Type
|
||||
type family DirTy d = res | res -> d where
|
||||
DirTy 'TopDown = Recur
|
||||
DirTy 'BottomUp = Node -- For bottom up maps we never recur on the children
|
||||
type DirTy :: Direction -> GHC.Type -> GHC.Type
|
||||
type family DirTy d c = res | res -> d where
|
||||
DirTy 'TopDown c = Recur' c
|
||||
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
|
||||
-- recursive subnodes have already been mapped
|
||||
@ -36,7 +36,7 @@ dmapG ::
|
||||
forall c m.
|
||||
Monad m =>
|
||||
Collector (Int, [Binder]) c ->
|
||||
(c -> Node -> m Recur) ->
|
||||
(c -> Node -> m (Recur' c)) ->
|
||||
Node ->
|
||||
m Node
|
||||
dmapG coll f = go (coll ^. cEmpty)
|
||||
@ -45,170 +45,80 @@ dmapG coll f = go (coll ^. cEmpty)
|
||||
go c n = do
|
||||
r <- f c n
|
||||
case r of
|
||||
End n' -> return n'
|
||||
Recur n' ->
|
||||
End' n' -> return n'
|
||||
Recur' (c', n') ->
|
||||
let ni = destruct n'
|
||||
in reassembleDetails ni <$> mapM goChild (ni ^. nodeChildren)
|
||||
where
|
||||
goChild :: NodeChild -> m Node
|
||||
goChild ch = go ((coll ^. cCollect) (ch ^. childBindersNum, ch ^. childBinders) c) (ch ^. childNode)
|
||||
where
|
||||
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 Binder
|
||||
CtxTy 'CtxBinderNum = Index
|
||||
CtxTy 'CtxNone = ()
|
||||
|
||||
type RetTy :: (GHC.Type -> GHC.Type) -> Direction -> Monadic -> Ret -> GHC.Type
|
||||
type family RetTy m dir mon r = res | res -> mon r where
|
||||
RetTy m 'TopDown 'Monadic 'RetRecur = m Recur
|
||||
RetTy m 'TopDown 'Monadic 'RetSimple = m Node
|
||||
RetTy _ 'TopDown 'NonMonadic 'RetRecur = Recur
|
||||
RetTy _ 'TopDown 'NonMonadic 'RetSimple = Node
|
||||
RetTy m 'BottomUp 'Monadic 'RetSimple = m Node
|
||||
RetTy _ 'BottomUp 'NonMonadic 'RetSimple = Node
|
||||
|
||||
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 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 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 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
|
||||
|
||||
type NodeMapRet :: (GHC.Type -> GHC.Type) -> Monadic -> GHC.Type
|
||||
type family NodeMapRet m mon = res | res -> mon m where
|
||||
NodeMapRet m 'Monadic = m Node
|
||||
NodeMapRet Identity 'NonMonadic = Node
|
||||
type OverIdentity' :: GHC.Type -> GHC.Type
|
||||
type family OverIdentity' t = res where
|
||||
OverIdentity' (a -> b) = a -> OverIdentity' b
|
||||
OverIdentity' leaf = Identity leaf
|
||||
|
||||
type OverIdentity :: GHC.Type -> GHC.Type
|
||||
type family OverIdentity t = res where
|
||||
OverIdentity (a -> b) = a -> OverIdentity b
|
||||
OverIdentity ((), b) = ((), OverIdentity b)
|
||||
OverIdentity (BinderList Binder, b) = (BinderList Binder, OverIdentity b)
|
||||
OverIdentity (Index, b) = (Index, OverIdentity b)
|
||||
OverIdentity leaf = Identity leaf
|
||||
OverIdentity ((), b) = ((), OverIdentity' b)
|
||||
OverIdentity (BinderList Binder, b) = (BinderList Binder, OverIdentity' b)
|
||||
OverIdentity (Index, b) = (Index, OverIdentity' b)
|
||||
OverIdentity leaf = OverIdentity' leaf
|
||||
|
||||
class EmbedIdentity a where
|
||||
embedIden :: a -> OverIdentity a
|
||||
|
||||
instance EmbedIdentity b => EmbedIdentity (a -> b) where
|
||||
embedIden f = embedIden . f
|
||||
class EmbedIdentity' a where
|
||||
embedIden' :: a -> OverIdentity' a
|
||||
|
||||
instance EmbedIdentity b => EmbedIdentity ((), b) where
|
||||
embedIden (a, b) = (a, embedIden b)
|
||||
instance EmbedIdentity' b => EmbedIdentity' (a -> b) where
|
||||
embedIden' f = embedIden' . f
|
||||
|
||||
instance EmbedIdentity b => EmbedIdentity (Index, b) where
|
||||
embedIden (a, b) = (a, embedIden b)
|
||||
instance EmbedIdentity' b => EmbedIdentity ((), b) where
|
||||
embedIden (a, b) = (a, embedIden' b)
|
||||
|
||||
instance EmbedIdentity b => EmbedIdentity (BinderList Binder, b) where
|
||||
embedIden (a, b) = (a, embedIden b)
|
||||
instance EmbedIdentity' b => EmbedIdentity (Index, b) where
|
||||
embedIden (a, b) = (a, embedIden' b)
|
||||
|
||||
instance EmbedIdentity Node where
|
||||
embedIden = Identity
|
||||
instance EmbedIdentity' b => EmbedIdentity (BinderList Binder, b) where
|
||||
embedIden (a, b) = (a, embedIden' b)
|
||||
|
||||
instance EmbedIdentity Recur where
|
||||
embedIden = Identity
|
||||
instance EmbedIdentity' b => EmbedIdentity (a -> b) where
|
||||
embedIden a = embedIden' a
|
||||
|
||||
type KDefaultIdentity :: Monadic -> (GHC.Type -> GHC.Type) -> GHC.Constraint
|
||||
type family KDefaultIdentity mon m = res | res -> m where
|
||||
KDefaultIdentity 'Monadic m = m ~ m
|
||||
KDefaultIdentity 'NonMonadic m = Identity ~ m
|
||||
instance EmbedIdentity' (c, Node) where
|
||||
embedIden' = Identity
|
||||
|
||||
type KCompatibleDir :: Direction -> Ret -> GHC.Constraint
|
||||
type family KCompatibleDir dir r = res where
|
||||
KCompatibleDir 'TopDown r = r ~ r
|
||||
KCompatibleDir 'BottomUp r = r ~ 'RetSimple
|
||||
instance EmbedIdentity' Node where
|
||||
embedIden' = Identity
|
||||
|
||||
nodeMapE ::
|
||||
forall (dir :: Direction) (mon :: Monadic) (i :: CollectorIni) (x :: Ctx) (r :: Ret) m.
|
||||
( Monad m,
|
||||
KDefaultIdentity mon m,
|
||||
KCompatibleDir dir r
|
||||
) =>
|
||||
instance EmbedIdentity' Recur where
|
||||
embedIden' = Identity
|
||||
|
||||
instance EmbedIdentity' (Recur' c) where
|
||||
embedIden' = Identity
|
||||
|
||||
fromSimple :: Functor g => c -> g Node -> g (Recur' c)
|
||||
fromSimple c = fmap (\x -> Recur' (c, x))
|
||||
|
||||
fromRecur :: Functor g => c -> g Recur -> g (Recur' c)
|
||||
fromRecur c =
|
||||
fmap
|
||||
( \case
|
||||
End x -> End' x
|
||||
Recur x -> Recur' (c, x)
|
||||
)
|
||||
|
||||
fromPair :: Functor g => d -> g (c, Node) -> g (Recur' (c, d))
|
||||
fromPair d = fmap (\(c, x) -> Recur' ((c, d), x))
|
||||
|
||||
nodeMapG' ::
|
||||
Monad m =>
|
||||
Sing dir ->
|
||||
Sing mon ->
|
||||
Sing i ->
|
||||
Sing x ->
|
||||
Sing r ->
|
||||
NodeMapArg m dir mon i x r ->
|
||||
Collector (Int, [Binder]) c ->
|
||||
(c -> Node -> m (DirTy dir c)) ->
|
||||
Node ->
|
||||
NodeMapRet m mon
|
||||
nodeMapE sdir smon sini sctx sret f = case smon :: SMonadic mon of
|
||||
SMonadic ->
|
||||
case (sdir, sini, sctx, sret) of
|
||||
(STopDown, SNoIni, SCtxBinderList, SRetSimple) -> nodeMapG' binderInfoCollector (\bi -> fromSimple . f bi)
|
||||
(STopDown, SNoIni, SCtxBinderList, SRetRecur) -> nodeMapG' binderInfoCollector f
|
||||
(STopDown, SNoIni, SCtxBinderNum, SRetSimple) -> nodeMapG' binderNumCollector (\bi -> fromSimple . f bi)
|
||||
(STopDown, SNoIni, SCtxBinderNum, SRetRecur) -> nodeMapG' binderNumCollector f
|
||||
(STopDown, SNoIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (fromSimple . f))
|
||||
(STopDown, SNoIni, SCtxNone, SRetRecur) -> nodeMapG' binderInfoCollector (const f)
|
||||
(STopDown, SIni, SCtxBinderList, SRetSimple) -> nodeMapG' (binderInfoCollector' (fst f)) (\bi -> fromSimple . snd f bi)
|
||||
(STopDown, SIni, SCtxBinderList, SRetRecur) -> nodeMapG' (binderInfoCollector' (fst f)) (snd f)
|
||||
(STopDown, SIni, SCtxBinderNum, SRetSimple) -> nodeMapG' (binderNumCollector' (fst f)) (\bi -> fromSimple . snd f bi)
|
||||
(STopDown, SIni, SCtxBinderNum, SRetRecur) -> nodeMapG' (binderNumCollector' (fst f)) (snd f)
|
||||
(STopDown, SIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (fromSimple . snd f))
|
||||
(STopDown, SIni, SCtxNone, SRetRecur) -> nodeMapG' binderInfoCollector (const (snd f))
|
||||
(SBottomUp, SNoIni, SCtxBinderList, SRetSimple) -> nodeMapG' binderInfoCollector f
|
||||
(SBottomUp, SNoIni, SCtxBinderNum, SRetSimple) -> nodeMapG' binderNumCollector f
|
||||
(SBottomUp, SNoIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const f)
|
||||
(SBottomUp, SIni, SCtxBinderList, SRetSimple) -> nodeMapG' (binderInfoCollector' (fst f)) (snd f)
|
||||
(SBottomUp, SIni, SCtxBinderNum, SRetSimple) -> nodeMapG' (binderNumCollector' (fst f)) (snd f)
|
||||
(SBottomUp, SIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (snd f))
|
||||
SNonMonadic ->
|
||||
runIdentity
|
||||
. case (sdir, sini, sctx, sret) of
|
||||
(STopDown, SNoIni, SCtxBinderList, SRetSimple) -> nodeMapG' binderInfoCollector (\bi -> fromSimple . embedIden f bi)
|
||||
(STopDown, SNoIni, SCtxBinderList, SRetRecur) -> nodeMapG' binderInfoCollector (embedIden f)
|
||||
(STopDown, SNoIni, SCtxBinderNum, SRetSimple) -> nodeMapG' binderNumCollector (\bi -> fromSimple . embedIden f bi)
|
||||
(STopDown, SNoIni, SCtxBinderNum, SRetRecur) -> nodeMapG' binderNumCollector (embedIden f)
|
||||
(STopDown, SNoIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (fromSimple . embedIden f))
|
||||
(STopDown, SNoIni, SCtxNone, SRetRecur) -> nodeMapG' binderInfoCollector (const (embedIden f))
|
||||
(STopDown, SIni, SCtxBinderList, SRetSimple) -> nodeMapG' (binderInfoCollector' (fst f)) (\bi -> fromSimple . snd (embedIden f) bi)
|
||||
(STopDown, SIni, SCtxBinderList, SRetRecur) -> nodeMapG' (binderInfoCollector' (fst f)) (snd (embedIden f))
|
||||
(STopDown, SIni, SCtxBinderNum, SRetSimple) -> nodeMapG' (binderNumCollector' (fst f)) (\bi -> fromSimple . snd (embedIden f) bi)
|
||||
(STopDown, SIni, SCtxBinderNum, SRetRecur) -> nodeMapG' (binderNumCollector' (fst f)) (snd (embedIden f))
|
||||
(STopDown, SIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (fromSimple . snd (embedIden f)))
|
||||
(STopDown, SIni, SCtxNone, SRetRecur) -> nodeMapG' binderInfoCollector (const (snd (embedIden f)))
|
||||
(SBottomUp, SNoIni, SCtxBinderList, SRetSimple) -> nodeMapG' binderInfoCollector (embedIden f)
|
||||
(SBottomUp, SNoIni, SCtxBinderNum, SRetSimple) -> nodeMapG' binderNumCollector (embedIden f)
|
||||
(SBottomUp, SNoIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (embedIden f))
|
||||
(SBottomUp, SIni, SCtxBinderList, SRetSimple) -> nodeMapG' (binderInfoCollector' (fst f)) (snd (embedIden f))
|
||||
(SBottomUp, SIni, SCtxBinderNum, SRetSimple) -> nodeMapG' (binderNumCollector' (fst f)) (snd (embedIden f))
|
||||
(SBottomUp, SIni, SCtxNone, SRetSimple) -> nodeMapG' binderInfoCollector (const (snd (embedIden f)))
|
||||
where
|
||||
fromSimple :: forall g. Functor g => g Node -> g Recur
|
||||
fromSimple = fmap Recur
|
||||
nodeMapG' ::
|
||||
Collector (Int, [Binder]) c ->
|
||||
(c -> Node -> m (DirTy dir)) ->
|
||||
Node ->
|
||||
m Node
|
||||
nodeMapG' = case sdir of
|
||||
STopDown -> dmapG
|
||||
SBottomUp -> umapG
|
||||
|
||||
-- | Implicit version of dmapE
|
||||
nodeMapI ::
|
||||
forall (dir :: Direction) (mon :: Monadic) (i :: CollectorIni) (x :: Ctx) (r :: Ret) m.
|
||||
( SingI mon,
|
||||
SingI i,
|
||||
SingI x,
|
||||
SingI r,
|
||||
Monad m,
|
||||
KDefaultIdentity mon m,
|
||||
KCompatibleDir dir r
|
||||
) =>
|
||||
Sing dir ->
|
||||
NodeMapArg m dir mon i x r ->
|
||||
Node ->
|
||||
NodeMapRet m mon
|
||||
nodeMapI dir = nodeMapE dir sing sing sing sing
|
||||
m Node
|
||||
nodeMapG' sdir = case sdir of
|
||||
STopDown -> dmapG
|
||||
SBottomUp -> umapG
|
||||
|
||||
@ -1,95 +1,114 @@
|
||||
module Juvix.Compiler.Core.Extra.Recursors.Map.Named where
|
||||
|
||||
import Data.Functor.Identity
|
||||
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 Binder -> Node -> m Recur) -> Node -> m Node
|
||||
dmapLRM = nodeMapI STopDown
|
||||
dmapLRM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromRecur bi . f bi)
|
||||
|
||||
dmapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
|
||||
dmapLM = nodeMapI STopDown
|
||||
dmapLM f = nodeMapG' STopDown binderInfoCollector (\bi -> fromSimple bi . f bi)
|
||||
|
||||
umapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
|
||||
umapLM = nodeMapI SBottomUp
|
||||
umapLM f = nodeMapG' SBottomUp binderInfoCollector f
|
||||
|
||||
dmapNRM :: Monad m => (Index -> Node -> m Recur) -> Node -> m Node
|
||||
dmapNRM = nodeMapI STopDown
|
||||
dmapNRM f = nodeMapG' STopDown binderNumCollector (\bi -> fromRecur bi . f bi)
|
||||
|
||||
dmapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
|
||||
dmapNM = nodeMapI STopDown
|
||||
dmapNM f = nodeMapG' STopDown binderNumCollector (\bi -> fromSimple bi . f bi)
|
||||
|
||||
umapNM :: Monad m => (Index -> Node -> m Node) -> Node -> m Node
|
||||
umapNM = nodeMapI STopDown
|
||||
umapNM f = nodeMapG' SBottomUp binderNumCollector f
|
||||
|
||||
dmapRM :: Monad m => (Node -> m Recur) -> Node -> m Node
|
||||
dmapRM = nodeMapI STopDown
|
||||
dmapRM f = nodeMapG' STopDown unitCollector (const (fromRecur mempty . f))
|
||||
|
||||
dmapM :: Monad m => (Node -> m Node) -> Node -> m Node
|
||||
dmapM = nodeMapI STopDown
|
||||
dmapM f = nodeMapG' STopDown unitCollector (const (fromSimple mempty . f))
|
||||
|
||||
umapM :: Monad m => (Node -> m Node) -> Node -> m Node
|
||||
umapM = nodeMapI SBottomUp
|
||||
umapM f = nodeMapG' SBottomUp unitCollector (const f)
|
||||
|
||||
dmapLRM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Recur) -> Node -> m Node
|
||||
dmapLRM' = nodeMapI STopDown
|
||||
dmapLRM' f = nodeMapG' STopDown (binderInfoCollector' (fst f)) (\bi -> fromRecur bi . snd f bi)
|
||||
|
||||
dmapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
|
||||
dmapLM' = nodeMapI STopDown
|
||||
dmapLM' f = nodeMapG' STopDown (binderInfoCollector' (fst f)) (\bi -> fromSimple bi . snd f bi)
|
||||
|
||||
umapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
|
||||
umapLM' = nodeMapI SBottomUp
|
||||
umapLM' f = nodeMapG' SBottomUp (binderInfoCollector' (fst f)) (snd f)
|
||||
|
||||
dmapNRM' :: Monad m => (Index, Index -> Node -> m Recur) -> Node -> m Node
|
||||
dmapNRM' = nodeMapI STopDown
|
||||
dmapNRM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromRecur bi . snd f bi)
|
||||
|
||||
dmapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
|
||||
dmapNM' = nodeMapI STopDown
|
||||
dmapNM' f = nodeMapG' STopDown (binderNumCollector' (fst f)) (\bi -> fromSimple bi . snd f bi)
|
||||
|
||||
umapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
|
||||
umapNM' = nodeMapI SBottomUp
|
||||
umapNM' f = nodeMapG' SBottomUp (binderNumCollector' (fst f)) (snd f)
|
||||
|
||||
dmapLR :: (BinderList Binder -> Node -> Recur) -> Node -> Node
|
||||
dmapLR = nodeMapI STopDown
|
||||
dmapLR f = runIdentity . dmapLRM (embedIden f)
|
||||
|
||||
dmapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
|
||||
dmapL = nodeMapI STopDown
|
||||
dmapL f = runIdentity . dmapLM (embedIden f)
|
||||
|
||||
umapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
|
||||
umapL = nodeMapI SBottomUp
|
||||
umapL f = runIdentity . umapLM (embedIden f)
|
||||
|
||||
dmapNR :: (Index -> Node -> Recur) -> Node -> Node
|
||||
dmapNR = nodeMapI STopDown
|
||||
dmapNR f = runIdentity . dmapNRM (embedIden f)
|
||||
|
||||
dmapN :: (Index -> Node -> Node) -> Node -> Node
|
||||
dmapN = nodeMapI STopDown
|
||||
dmapN f = runIdentity . dmapNM (embedIden f)
|
||||
|
||||
umapN :: (Index -> Node -> Node) -> Node -> Node
|
||||
umapN = nodeMapI SBottomUp
|
||||
umapN f = runIdentity . umapNM (embedIden f)
|
||||
|
||||
dmapR :: (Node -> Recur) -> Node -> Node
|
||||
dmapR = nodeMapI STopDown
|
||||
dmapR f = runIdentity . dmapRM (embedIden f)
|
||||
|
||||
dmap :: (Node -> Node) -> Node -> Node
|
||||
dmap = nodeMapI STopDown
|
||||
dmap f = runIdentity . dmapM (embedIden f)
|
||||
|
||||
umap :: (Node -> Node) -> Node -> Node
|
||||
umap = nodeMapI SBottomUp
|
||||
umap f = runIdentity . umapM (embedIden f)
|
||||
|
||||
dmapLR' :: (BinderList Binder, BinderList Binder -> Node -> Recur) -> Node -> Node
|
||||
dmapLR' = nodeMapI STopDown
|
||||
dmapLR' f = runIdentity . dmapLRM' (embedIden f)
|
||||
|
||||
dmapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
|
||||
dmapL' = nodeMapI STopDown
|
||||
dmapL' f = runIdentity . dmapLM' (embedIden f)
|
||||
|
||||
umapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
|
||||
umapL' = nodeMapI SBottomUp
|
||||
umapL' f = runIdentity . umapLM' (embedIden f)
|
||||
|
||||
dmapNR' :: (Index, Index -> Node -> Recur) -> Node -> Node
|
||||
dmapNR' = nodeMapI STopDown
|
||||
dmapNR' f = runIdentity . dmapNRM' (embedIden f)
|
||||
|
||||
dmapN' :: (Index, Index -> Node -> Node) -> Node -> Node
|
||||
dmapN' = nodeMapI STopDown
|
||||
dmapN' f = runIdentity . dmapNM' (embedIden f)
|
||||
|
||||
umapN' :: (Index, Index -> Node -> Node) -> Node -> Node
|
||||
umapN' = nodeMapI SBottomUp
|
||||
umapN' f = runIdentity . umapNM' (embedIden f)
|
||||
|
||||
dmapCLM :: Monad m => (c -> BinderList Binder -> Node -> m (c, Node)) -> c -> Node -> m Node
|
||||
dmapCLM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderInfoCollector) (\(c, bi) -> fromPair bi . f c bi)
|
||||
|
||||
dmapCNM :: Monad m => (c -> Index -> Node -> m (c, Node)) -> c -> Node -> m Node
|
||||
dmapCNM f ini = nodeMapG' STopDown (pairCollector (identityCollector ini) binderNumCollector) (\(c, bi) -> fromPair bi . f c bi)
|
||||
|
||||
dmapCM :: Monad m => (c -> Node -> m (c, Node)) -> c -> Node -> m Node
|
||||
dmapCM f ini = nodeMapG' STopDown (identityCollector ini) (\c -> fmap Recur' . f c)
|
||||
|
||||
dmapCL :: (c -> BinderList Binder -> Node -> (c, Node)) -> c -> Node -> Node
|
||||
dmapCL f ini = runIdentity . dmapCLM (embedIden f) ini
|
||||
|
||||
dmapCN :: (c -> Index -> Node -> (c, Node)) -> c -> Node -> Node
|
||||
dmapCN f ini = runIdentity . dmapCNM (embedIden f) ini
|
||||
|
||||
dmapC :: (c -> Node -> (c, Node)) -> c -> Node -> Node
|
||||
dmapC f ini = runIdentity . dmapCM (embedIden f) ini
|
||||
|
||||
@ -2,11 +2,10 @@ module Juvix.Compiler.Core.Extra.Recursors.Recur where
|
||||
|
||||
import Juvix.Compiler.Core.Language
|
||||
|
||||
data Recur' c
|
||||
= End' Node
|
||||
| Recur' (c, Node)
|
||||
|
||||
data Recur
|
||||
= End Node
|
||||
| Recur Node
|
||||
|
||||
recurNode :: Lens' Recur Node
|
||||
recurNode f = \case
|
||||
End n -> End <$> f n
|
||||
Recur n -> Recur <$> f n
|
||||
|
||||
@ -1,20 +0,0 @@
|
||||
module Juvix.Compiler.Core.Info.TypeInfo where
|
||||
|
||||
import Juvix.Compiler.Core.Extra.Base
|
||||
import Juvix.Compiler.Core.Info qualified as Info
|
||||
import Juvix.Compiler.Core.Language
|
||||
|
||||
newtype TypeInfo = TypeInfo {_infoType :: Type}
|
||||
|
||||
instance IsInfo TypeInfo
|
||||
|
||||
kTypeInfo :: Key TypeInfo
|
||||
kTypeInfo = Proxy
|
||||
|
||||
makeLenses ''TypeInfo
|
||||
|
||||
getInfoType :: Info -> Type
|
||||
getInfoType i = maybe mkDynamic' (^. infoType) (Info.lookup kTypeInfo i)
|
||||
|
||||
setInfoType :: Type -> Info -> Info
|
||||
setInfoType = Info.insert . TypeInfo
|
||||
@ -271,7 +271,7 @@ instance HasAtomicity (Pattern' i a) where
|
||||
PatConstr x -> atomicity x
|
||||
|
||||
instance HasAtomicity (Pi' i a) where
|
||||
atomicity _ = Aggregate lambdaFixity
|
||||
atomicity _ = Aggregate funFixity
|
||||
|
||||
instance HasAtomicity (Univ' i) where
|
||||
atomicity _ = Atom
|
||||
|
||||
@ -338,11 +338,19 @@ instance PrettyCode Stripped.Node where
|
||||
branchTagNames = map (^. (caseBranchInfo . Stripped.caseBranchInfoConstrName)) _caseBranches
|
||||
in ppCodeCase' branchBinderNames branchTagNames x
|
||||
|
||||
instance PrettyCode ConstructorInfo where
|
||||
ppCode :: Member (Reader Options) r => ConstructorInfo -> Sem r (Doc Ann)
|
||||
ppCode ci = do
|
||||
name <- ppName KNameConstructor (ci ^. constructorName)
|
||||
ty <- ppCode (ci ^. constructorType)
|
||||
return $ name <+> colon <+> ty
|
||||
|
||||
instance PrettyCode InfoTable where
|
||||
ppCode :: forall r. Member (Reader Options) r => InfoTable -> Sem r (Doc Ann)
|
||||
ppCode tbl = do
|
||||
tys <- ppInductives (toList (tbl ^. infoInductives))
|
||||
ctx' <- ppContext (tbl ^. identContext)
|
||||
return ("-- IdentContext" <> line <> ctx' <> line)
|
||||
return ("-- Types" <> line <> tys <> line <> "-- Identifiers" <> line <> ctx' <> line)
|
||||
where
|
||||
ppContext :: IdentContext -> Sem r (Doc Ann)
|
||||
ppContext ctx = do
|
||||
@ -356,7 +364,21 @@ instance PrettyCode InfoTable where
|
||||
mname' = (\nm -> nm <> "!" <> prettyText s) mname
|
||||
sym' <- ppName KNameLocal mname'
|
||||
body' <- ppCode n
|
||||
return (kwDef <+> sym' <+> kwAssign <+> nest 2 body')
|
||||
let ii = fromJust $ HashMap.lookup s (tbl ^. infoIdentifiers)
|
||||
ty = ii ^. identifierType
|
||||
ty' <- ppCode ty
|
||||
let tydoc = if isDynamic ty then mempty else space <> colon <+> ty'
|
||||
return (kwDef <+> sym' <> tydoc <+> kwAssign <+> nest 2 body')
|
||||
ppInductives :: [InductiveInfo] -> Sem r (Doc Ann)
|
||||
ppInductives inds = do
|
||||
inds' <- mapM ppInductive inds
|
||||
return (vsep inds')
|
||||
where
|
||||
ppInductive :: InductiveInfo -> Sem r (Doc Ann)
|
||||
ppInductive ii = do
|
||||
name <- ppName KNameInductive (ii ^. inductiveName)
|
||||
ctrs <- mapM (fmap (<> semi) . ppCode) (ii ^. inductiveConstructors)
|
||||
return (kwInductive <+> name <+> braces (line <> indent' (vsep ctrs) <> line))
|
||||
|
||||
instance PrettyCode Stripped.InfoTable where
|
||||
ppCode :: forall r. Member (Reader Options) r => Stripped.InfoTable -> Sem r (Doc Ann)
|
||||
|
||||
@ -13,6 +13,7 @@ import Juvix.Compiler.Core.Transformation.Base
|
||||
import Juvix.Compiler.Core.Transformation.Eta
|
||||
import Juvix.Compiler.Core.Transformation.Identity
|
||||
import Juvix.Compiler.Core.Transformation.LambdaLifting
|
||||
import Juvix.Compiler.Core.Transformation.RemoveTypeArgs
|
||||
import Juvix.Compiler.Core.Transformation.TopEtaExpand
|
||||
|
||||
applyTransformations :: [TransformationId] -> InfoTable -> InfoTable
|
||||
@ -23,3 +24,4 @@ applyTransformations ts tbl = foldl' (flip appTrans) tbl ts
|
||||
LambdaLifting -> lambdaLifting
|
||||
Identity -> identity
|
||||
TopEtaExpand -> topEtaExpand
|
||||
RemoveTypeArgs -> removeTypeArgs
|
||||
|
||||
@ -10,7 +10,17 @@ import Juvix.Compiler.Core.Data.InfoTable
|
||||
import Juvix.Compiler.Core.Data.InfoTableBuilder
|
||||
import Juvix.Compiler.Core.Language
|
||||
|
||||
type Transformation = InfoTable -> InfoTable
|
||||
mapIdents :: (IdentifierInfo -> IdentifierInfo) -> InfoTable -> InfoTable
|
||||
mapIdents = over infoIdentifiers . fmap
|
||||
|
||||
mapInductives :: (InductiveInfo -> InductiveInfo) -> InfoTable -> InfoTable
|
||||
mapInductives = over infoInductives . fmap
|
||||
|
||||
mapConstructors :: (ConstructorInfo -> ConstructorInfo) -> InfoTable -> InfoTable
|
||||
mapConstructors = over infoConstructors . fmap
|
||||
|
||||
mapAxioms :: (AxiomInfo -> AxiomInfo) -> InfoTable -> InfoTable
|
||||
mapAxioms = over infoAxioms . fmap
|
||||
|
||||
mapT :: (Symbol -> Node -> Node) -> InfoTable -> InfoTable
|
||||
mapT f tab = tab {_identContext = HashMap.mapWithKey f (tab ^. identContext)}
|
||||
|
||||
@ -74,5 +74,5 @@ etaExpandApps tab =
|
||||
Just ci -> length (ci ^. inductiveParams)
|
||||
Nothing -> 0
|
||||
|
||||
etaExpansionApps :: Transformation
|
||||
etaExpansionApps :: InfoTable -> InfoTable
|
||||
etaExpansionApps tab = mapT (const (etaExpandApps tab)) tab
|
||||
|
||||
126
src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
Normal file
126
src/Juvix/Compiler/Core/Transformation/RemoveTypeArgs.hs
Normal file
@ -0,0 +1,126 @@
|
||||
module Juvix.Compiler.Core.Transformation.RemoveTypeArgs
|
||||
( removeTypeArgs,
|
||||
module Juvix.Compiler.Core.Transformation.Base,
|
||||
)
|
||||
where
|
||||
|
||||
import Data.HashMap.Strict qualified as HashMap
|
||||
import Juvix.Compiler.Core.Data.BinderList qualified as BL
|
||||
import Juvix.Compiler.Core.Extra
|
||||
import Juvix.Compiler.Core.Transformation.Base
|
||||
|
||||
convertNode :: InfoTable -> Node -> Node
|
||||
convertNode tab = convert mempty
|
||||
where
|
||||
unsupported :: forall a. a
|
||||
unsupported = error "remove type arguments: unsupported node"
|
||||
|
||||
convert :: BinderList Binder -> Node -> Node
|
||||
convert vars = dmapLR' (vars, go)
|
||||
|
||||
go :: BinderList Binder -> Node -> Recur
|
||||
go vars node = case node of
|
||||
NVar v@(Var {..}) ->
|
||||
let ty = BL.lookup _varIndex vars ^. binderType
|
||||
in if
|
||||
| isTypeConstr ty -> End (mkDynamic _varInfo)
|
||||
| otherwise -> End (NVar (shiftVar (-k) v))
|
||||
where
|
||||
k = length (filter (isTypeConstr . (^. binderType)) (take _varIndex (toList vars)))
|
||||
NApp (App {}) ->
|
||||
let (h, args) = unfoldApps node
|
||||
ty =
|
||||
case h of
|
||||
NVar (Var {..}) ->
|
||||
BL.lookup _varIndex vars ^. binderType
|
||||
NIdt (Ident {..}) ->
|
||||
let fi = fromJust $ HashMap.lookup _identSymbol (tab ^. infoIdentifiers)
|
||||
in fi ^. identifierType
|
||||
_ -> unsupported
|
||||
args' = filterArgs ty args
|
||||
in if
|
||||
| null args' ->
|
||||
End (convert vars h)
|
||||
| otherwise ->
|
||||
End (mkApps (convert vars h) (map (second (convert vars)) args'))
|
||||
NCtr (Constr {..}) ->
|
||||
let ci = fromJust $ HashMap.lookup _constrTag (tab ^. infoConstructors)
|
||||
ty = ci ^. constructorType
|
||||
args' = filterArgs ty _constrArgs
|
||||
in End (mkConstr _constrInfo _constrTag (map (convert vars) args'))
|
||||
NCase (Case {..}) ->
|
||||
End (mkCase _caseInfo (convert vars _caseValue) (map convertBranch _caseBranches) (fmap (convert vars) _caseDefault))
|
||||
where
|
||||
convertBranch :: CaseBranch -> CaseBranch
|
||||
convertBranch br@CaseBranch {..} =
|
||||
let binders' = filterBinders vars _caseBranchBinders
|
||||
body' =
|
||||
convert
|
||||
(BL.prependRev _caseBranchBinders vars)
|
||||
_caseBranchBody
|
||||
in br
|
||||
{ _caseBranchBinders = binders',
|
||||
_caseBranchBindersNum = length binders',
|
||||
_caseBranchBody = body'
|
||||
}
|
||||
filterBinders :: BinderList Binder -> [Binder] -> [Binder]
|
||||
filterBinders _ [] = []
|
||||
filterBinders vars' (b : bs)
|
||||
| isTypeConstr (b ^. binderType) =
|
||||
filterBinders (BL.cons b vars') bs
|
||||
filterBinders vars' (b : bs) =
|
||||
over binderType (convert vars') b : filterBinders (BL.cons b vars') bs
|
||||
NLam (Lambda {..})
|
||||
| isTypeConstr (_lambdaBinder ^. binderType) ->
|
||||
End (convert (BL.cons _lambdaBinder vars) _lambdaBody)
|
||||
NPi (Pi {..})
|
||||
| isTypeConstr (_piBinder ^. binderType) && not (isTypeConstr _piBody) ->
|
||||
End (convert (BL.cons _piBinder vars) _piBody)
|
||||
_ -> Recur node
|
||||
where
|
||||
filterArgs :: Type -> [a] -> [a]
|
||||
filterArgs ty args =
|
||||
map fst $
|
||||
filter (not . isTypeConstr . snd) (zip args (typeArgs ty ++ repeat mkDynamic'))
|
||||
|
||||
convertIdent :: InfoTable -> IdentifierInfo -> IdentifierInfo
|
||||
convertIdent tab ii =
|
||||
ii
|
||||
{ _identifierType = ty',
|
||||
_identifierArgsInfo = map (over argumentType (convertNode tab) . fst) $ filter (not . isTypeConstr . snd) (zipExact (ii ^. identifierArgsInfo) tyargs),
|
||||
_identifierArgsNum = length (typeArgs ty')
|
||||
}
|
||||
where
|
||||
tyargs = typeArgs (ii ^. identifierType)
|
||||
ty' = convertNode tab (ii ^. identifierType)
|
||||
|
||||
convertConstructor :: InfoTable -> ConstructorInfo -> ConstructorInfo
|
||||
convertConstructor tab ci =
|
||||
ci
|
||||
{ _constructorType = ty',
|
||||
_constructorArgsNum = length (typeArgs ty')
|
||||
}
|
||||
where
|
||||
ty' = convertNode tab (ci ^. constructorType)
|
||||
|
||||
convertInductive :: InfoTable -> InductiveInfo -> InductiveInfo
|
||||
convertInductive tab ii =
|
||||
ii
|
||||
{ _inductiveKind = ty',
|
||||
_inductiveParams = map (over paramKind (convertNode tab) . fst) $ filter (not . isTypeConstr . snd) (zipExact (ii ^. inductiveParams) tyargs),
|
||||
_inductiveConstructors = map (convertConstructor tab) (ii ^. inductiveConstructors)
|
||||
}
|
||||
where
|
||||
tyargs = typeArgs (ii ^. inductiveKind)
|
||||
ty' = convertNode tab (ii ^. inductiveKind)
|
||||
|
||||
convertAxiom :: InfoTable -> AxiomInfo -> AxiomInfo
|
||||
convertAxiom tab = over axiomType (convertNode tab)
|
||||
|
||||
removeTypeArgs :: InfoTable -> InfoTable
|
||||
removeTypeArgs tab =
|
||||
mapAxioms (convertAxiom tab) $
|
||||
mapInductives (convertInductive tab) $
|
||||
mapConstructors (convertConstructor tab) $
|
||||
mapIdents (convertIdent tab) $
|
||||
mapT (const (convertNode tab)) tab
|
||||
@ -801,7 +801,7 @@ caseMatchingBranch varsNum vars = do
|
||||
ns
|
||||
br <- bracedExpr (varsNum + bindersNum) vars'
|
||||
let info = setInfoName (ci ^. constructorName) mempty
|
||||
binders = [Binder name (Just loc) mkDynamic' | (name, loc) <- ns]
|
||||
binders = zipWith (\(name, loc) -> Binder name (Just loc)) ns (typeArgs (ci ^. constructorType) ++ repeat mkDynamic')
|
||||
return $ CaseBranch info tag binders bindersNum br
|
||||
Nothing ->
|
||||
parseFailure off ("undeclared identifier: " ++ fromText txt)
|
||||
|
||||
@ -249,5 +249,10 @@ tests =
|
||||
"Eta-expansion"
|
||||
"."
|
||||
"test044.jvc"
|
||||
"out/test044.out"
|
||||
"out/test044.out",
|
||||
PosTest
|
||||
"Type application and abstraction"
|
||||
"."
|
||||
"test045.jvc"
|
||||
"out/test045.out"
|
||||
]
|
||||
|
||||
@ -3,6 +3,7 @@ module Core.Transformation where
|
||||
import Base
|
||||
import Core.Transformation.Identity qualified as Identity
|
||||
import Core.Transformation.Lifting qualified as Lifting
|
||||
import Core.Transformation.RemoveTypeArgs qualified as RemoveTypeArgs
|
||||
import Core.Transformation.TopEtaExpand qualified as TopEtaExpand
|
||||
|
||||
allTests :: TestTree
|
||||
@ -11,5 +12,6 @@ allTests =
|
||||
"JuvixCore transformations"
|
||||
[ Identity.allTests,
|
||||
TopEtaExpand.allTests,
|
||||
Lifting.allTests
|
||||
Lifting.allTests,
|
||||
RemoveTypeArgs.allTests
|
||||
]
|
||||
|
||||
21
test/Core/Transformation/RemoveTypeArgs.hs
Normal file
21
test/Core/Transformation/RemoveTypeArgs.hs
Normal file
@ -0,0 +1,21 @@
|
||||
module Core.Transformation.RemoveTypeArgs (allTests) where
|
||||
|
||||
import Base
|
||||
import Core.Eval.Positive qualified as Eval
|
||||
import Core.Transformation.Base
|
||||
import Juvix.Compiler.Core.Transformation
|
||||
|
||||
allTests :: TestTree
|
||||
allTests = testGroup "Remove type arguments" (map liftTest Eval.tests)
|
||||
|
||||
pipe :: [TransformationId]
|
||||
pipe = [LambdaLifting, RemoveTypeArgs]
|
||||
|
||||
liftTest :: Eval.PosTest -> TestTree
|
||||
liftTest _testEval =
|
||||
fromTest
|
||||
Test
|
||||
{ _testTransformations = pipe,
|
||||
_testAssertion = const (return ()),
|
||||
_testEval
|
||||
}
|
||||
1
tests/Core/positive/out/test045.out
Normal file
1
tests/Core/positive/out/test045.out
Normal file
@ -0,0 +1 @@
|
||||
15
|
||||
@ -7,8 +7,10 @@ inductive list : Π A : Type, Type {
|
||||
|
||||
def id : Π A : Type, A → A := λ(A : Type) λ(x : A) x;
|
||||
|
||||
def hd : Π A : Type, list A → A := λA λl case l of { cons _ x _ := x };
|
||||
def hd : Π A : Type, list A → A := λ(A : Type) λl case l of { cons _ x _ := x };
|
||||
|
||||
def tl : Π A : Type, list A → list A := λA λl case l of { cons _ _ y := y };
|
||||
def tl : Π A : Type, list A → list A := λ(A : Type) λl case l of { cons _ _ y := y };
|
||||
|
||||
hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int)))))
|
||||
def main := hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int)))));
|
||||
|
||||
main
|
||||
|
||||
@ -7,4 +7,6 @@ def fun' := λ(T : Type → Type) λ(A : Type) λ(B : T A) λ(x : B)
|
||||
let h := λ(b : B) λ(a : A) a * b - b in
|
||||
f (λ(y : B) h y x);
|
||||
|
||||
fun int 2 + fun' (λA A) int int 3
|
||||
def main := fun int 2 + fun' (λA A) int int 3;
|
||||
|
||||
main
|
||||
|
||||
26
tests/Core/positive/test045.jvc
Normal file
26
tests/Core/positive/test045.jvc
Normal file
@ -0,0 +1,26 @@
|
||||
-- type application and abstraction
|
||||
|
||||
inductive list : Π A : Type, Type {
|
||||
cons : Π A : Type, A → list A → list A;
|
||||
nil : Π A : Type, list A;
|
||||
};
|
||||
|
||||
def id : Π A : Type, A → A := λ(A : Type) λ(x : A) x;
|
||||
|
||||
def hd : Π A : Type, list A → A := λ(A : Type) λl case l of { cons _ x _ := x };
|
||||
|
||||
def tl : Π A : Type, list A → list A := λ(A : Type) λl case l of { cons _ _ y := y };
|
||||
|
||||
def f := λ(A : Type) λ(x : A) λ(B : Type) λ(y : B) x + y;
|
||||
|
||||
def g := λ(A : Type) λ(xs : list A) λ(B : Type) λ(ys : list B) case xs of {
|
||||
cons A' x _ := case ys of {
|
||||
cons B' y _ := f A' x B' y;
|
||||
nil _ := x;
|
||||
};
|
||||
nil _ := 0;
|
||||
};
|
||||
|
||||
def main := g int (cons int 2 (nil int)) int (cons int 3 (nil int)) * f int 1 int (hd int (tl int (id (list int) (cons int 1 (cons int 2 (nil int))))));
|
||||
|
||||
main
|
||||
Loading…
Reference in New Issue
Block a user