-
Notifications
You must be signed in to change notification settings - Fork 459
Fold over Core without iter #200
Changes from all commits
4598da7
d7e4f21
fbb5688
e6e580d
07616d5
4cbc23b
9732017
aa1e36b
9eae24e
2f81268
49baa46
2743895
70f67c0
05a3097
0408cfc
b10912b
1751ad1
de7956b
0eb17e3
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -194,25 +194,8 @@ annWith :: (Carrier sig m, Member Core sig) => CallStack -> m a -> m a | |
| annWith callStack = maybe id (fmap send . Ann) (stackLoc callStack) | ||
|
|
||
|
|
||
| stripAnnotations :: (Member Core sig, Syntax sig) => Term sig a -> Term sig a | ||
| stripAnnotations = iter id alg Var Var | ||
| where alg t | Just c <- prj t, Ann _ b <- c = b | ||
| | otherwise = Term t | ||
|
|
||
|
|
||
| instance Syntax Core where | ||
| foldSyntax go k h = \case | ||
| Let a -> Let a | ||
| a :>> b -> go h a :>> go h b | ||
| Lam u b -> Lam u (foldSyntax go k h b) | ||
| a :$ b -> go h a :$ go h b | ||
| Unit -> Unit | ||
| Bool b -> Bool b | ||
| If c t e -> If (go h c) (go h t) (go h e) | ||
| String s -> String s | ||
| Load t -> Load (go h t) | ||
| Edge e t -> Edge e (go h t) | ||
| Frame -> Frame | ||
| a :. b -> go h a :. go h b | ||
| a := b -> go h a := go h b | ||
| Ann loc t -> Ann loc (go h t) | ||
| stripAnnotations :: (Member Core sig, HFunctor sig, forall g . Functor g => Functor (sig g)) => Term sig a -> Term sig a | ||
| stripAnnotations (Var v) = Var v | ||
| stripAnnotations (Term t) | ||
| | Just c <- prj t, Ann _ b <- c = stripAnnotations b | ||
| | otherwise = Term (hmap stripAnnotations t) | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is slightly less pretty than the |
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -11,7 +11,6 @@ module Data.Core.Pretty | |
| import Control.Effect.Reader | ||
| import Data.Core | ||
| import Data.File | ||
| import Data.Functor.Const | ||
| import Data.Name | ||
| import Data.Scope | ||
| import Data.Term | ||
|
|
@@ -56,57 +55,58 @@ inParens amount go = do | |
| body <- with amount go | ||
| pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body) | ||
|
|
||
| prettify :: (Member (Reader [AnsiDoc]) sig, Member (Reader Prec) sig, Carrier sig m) | ||
| => Style | ||
| -> Core (Const (m AnsiDoc)) a | ||
| -> m AnsiDoc | ||
| prettify style = \case | ||
| Let a -> pure $ keyword "let" <+> name a | ||
| Const a :>> Const b -> do | ||
| prec <- ask @Prec | ||
| fore <- with 12 a | ||
| aft <- with 12 b | ||
|
|
||
| let open = symbol ("{" <> softline) | ||
| close = symbol (softline <> "}") | ||
| separator = ";" <> Pretty.line | ||
| body = fore <> separator <> aft | ||
|
|
||
| pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body) | ||
|
|
||
| Lam n f -> inParens 11 $ do | ||
| (x, body) <- bind n f | ||
| pure (lambda <> x <+> arrow <+> body) | ||
|
|
||
| Frame -> pure $ primitive "frame" | ||
| Unit -> pure $ primitive "unit" | ||
| Bool b -> pure $ primitive (if b then "true" else "false") | ||
| String s -> pure . strlit $ Pretty.viaShow s | ||
|
|
||
| Const f :$ Const x -> inParens 11 $ (<+>) <$> f <*> x | ||
|
|
||
| If (Const con) (Const tru) (Const fal) -> do | ||
| con' <- "if" `appending` con | ||
| tru' <- "then" `appending` tru | ||
| fal' <- "else" `appending` fal | ||
| pure $ Pretty.sep [con', tru', fal'] | ||
|
|
||
| Load (Const p) -> "load" `appending` p | ||
| Edge Lexical (Const n) -> "lexical" `appending` n | ||
| Edge Import (Const n) -> "import" `appending` n | ||
| Const item :. Const body -> inParens 4 $ do | ||
| f <- item | ||
| g <- body | ||
| pure (f <> symbol "." <> g) | ||
|
|
||
| Const lhs := Const rhs -> inParens 3 $ do | ||
| f <- lhs | ||
| g <- rhs | ||
| pure (f <+> symbol "=" <+> g) | ||
|
|
||
| -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. | ||
| Ann _ (Const c) -> c | ||
| where bind (Ignored x) f = let x' = name x in (,) x' <$> local (x':) (getConst (unScope f)) | ||
| prettyCore :: Style -> Term Core User -> AnsiDoc | ||
| prettyCore style = run . runReader @Prec 0 . go (pure . name) | ||
| where go :: (Member (Reader Prec) sig, Carrier sig m) => (a -> m AnsiDoc) -> Term Core a -> m AnsiDoc | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
|
||
| go var = \case | ||
| Var v -> var v | ||
| Term t -> case t of | ||
| Let a -> pure $ keyword "let" <+> name a | ||
| a :>> b -> do | ||
| prec <- ask @Prec | ||
| fore <- with 12 (go var a) | ||
| aft <- with 12 (go var b) | ||
|
|
||
| let open = symbol ("{" <> softline) | ||
| close = symbol (softline <> "}") | ||
| separator = ";" <> Pretty.line | ||
| body = fore <> separator <> aft | ||
|
|
||
| pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body) | ||
|
|
||
| Lam n f -> inParens 11 $ do | ||
| (x, body) <- bind n f | ||
| pure (lambda <> x <+> arrow <+> body) | ||
|
|
||
| Frame -> pure $ primitive "frame" | ||
| Unit -> pure $ primitive "unit" | ||
| Bool b -> pure $ primitive (if b then "true" else "false") | ||
| String s -> pure . strlit $ Pretty.viaShow s | ||
|
|
||
| f :$ x -> inParens 11 $ (<+>) <$> go var f <*> go var x | ||
|
|
||
| If con tru fal -> do | ||
| con' <- "if" `appending` go var con | ||
| tru' <- "then" `appending` go var tru | ||
| fal' <- "else" `appending` go var fal | ||
| pure $ Pretty.sep [con', tru', fal'] | ||
|
|
||
| Load p -> "load" `appending` go var p | ||
| Edge Lexical n -> "lexical" `appending` go var n | ||
| Edge Import n -> "import" `appending` go var n | ||
| item :. body -> inParens 4 $ do | ||
| f <- go var item | ||
| g <- go var body | ||
| pure (f <> symbol "." <> g) | ||
|
|
||
| lhs := rhs -> inParens 3 $ do | ||
| f <- go var lhs | ||
| g <- go var rhs | ||
| pure (f <+> symbol "=" <+> g) | ||
|
|
||
| -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. | ||
| Ann _ c -> go var c | ||
| where bind (Ignored x) f = let x' = name x in (,) x' <$> go (incr (const (pure x')) var) (fromScope f) | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is the real meat of the change: we use |
||
| lambda = case style of | ||
| Unicode -> symbol "λ" | ||
| Ascii -> symbol "\\" | ||
|
|
@@ -117,8 +117,3 @@ prettify style = \case | |
|
|
||
| appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc | ||
| appending k item = (keyword k <+>) <$> item | ||
|
|
||
| prettyCore :: Style -> Term Core User -> AnsiDoc | ||
| prettyCore s = run . runReader @Prec 0 . runReader @[AnsiDoc] [] . cata id (prettify s) bound (pure . name) | ||
| where bound (Z _) = asks (head @AnsiDoc) | ||
| bound (S n) = local (tail @AnsiDoc) n | ||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,18 +1,11 @@ | ||
| {-# LANGUAGE DeriveTraversable, FlexibleInstances, LambdaCase, MultiParamTypeClasses, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, TypeOperators, UndecidableInstances #-} | ||
| {-# LANGUAGE DeriveTraversable, FlexibleInstances, MultiParamTypeClasses, QuantifiedConstraints, StandaloneDeriving, UndecidableInstances #-} | ||
| module Data.Term | ||
| ( Term(..) | ||
| , Syntax(..) | ||
| , iter | ||
| , cata | ||
| , interpret | ||
| ) where | ||
|
|
||
| import Control.Effect.Carrier | ||
| import Control.Monad (ap) | ||
| import Control.Monad.Module | ||
| import Data.Coerce (coerce) | ||
| import Data.Functor.Const | ||
| import Data.Scope | ||
|
|
||
| data Term sig a | ||
| = Var a | ||
|
|
@@ -48,46 +41,3 @@ instance RightModule sig => Monad (Term sig) where | |
|
|
||
| instance RightModule sig => Carrier sig (Term sig) where | ||
| eff = Term | ||
|
|
||
|
|
||
| class (HFunctor sig, forall g . Functor g => Functor (sig g)) => Syntax sig where | ||
| foldSyntax :: (forall x y . (x -> m y) -> f x -> n y) | ||
| -> (forall a . Incr () (n a) -> m (Incr () (n a))) | ||
| -> (a -> m b) | ||
| -> sig f a | ||
| -> sig n b | ||
|
|
||
| instance Syntax (Scope ()) where | ||
| foldSyntax go bound free = Scope . go (bound . fmap (go free)) . unScope | ||
|
|
||
| instance (Syntax l, Syntax r) => Syntax (l :+: r) where | ||
| foldSyntax go bound free (L l) = L (foldSyntax go bound free l) | ||
| foldSyntax go bound free (R r) = R (foldSyntax go bound free r) | ||
|
|
||
|
|
||
| iter :: forall m n sig a b | ||
| . Syntax sig | ||
| => (forall a . m a -> n a) | ||
| -> (forall a . sig n a -> n a) | ||
| -> (forall a . Incr () (n a) -> m (Incr () (n a))) | ||
| -> (a -> m b) | ||
| -> Term sig a | ||
| -> n b | ||
| iter var alg bound = go | ||
| where go :: forall x y . (x -> m y) -> Term sig x -> n y | ||
| go free = \case | ||
| Var a -> var (free a) | ||
| Term t -> alg (foldSyntax go bound free t) | ||
|
|
||
| cata :: Syntax sig | ||
| => (a -> b) | ||
| -> (forall a . sig (Const b) a -> b) | ||
| -> (Incr () b -> a) | ||
| -> (x -> a) | ||
| -> Term sig x | ||
| -> b | ||
| cata var alg k h = getConst . iter (coerce var) (Const . alg) (coerce k) (Const . h) | ||
|
|
||
|
|
||
| interpret :: (Carrier sig m, Member eff sig, Syntax eff) => (forall a . Incr () (m a) -> m (Incr () (m a))) -> (a -> m b) -> Term eff a -> m b | ||
| interpret = iter id send | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If we want to implement something like |
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Goodbye!