github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-12-25 16:02:43 +03:00
Code Issues Projects Releases Wiki Activity

Use separate functor & recursive types.

Browse Source
This commit is contained in:
Rob Rix 2019-06-28 11:41:53 -04:00
parent a6cd4debe6
commit f0fae35ec9
No known key found for this signature in database
GPG Key ID: F188A01508EA1CF7
4 changed files with 242 additions and 232 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

172
semantic-core/src/Analysis/Eval.hs
View File

@ -28,34 +28,34 @@ import Prelude hiding (fail)
eval :: (Carrier sig m, Member Naming sig, Member (Reader Loc) sig, MonadFail m) => Analysis address value m -> (Core Name -> m value) -> Core Name -> m value eval :: (Carrier sig m, Member Naming sig, Member (Reader Loc) sig, MonadFail m) => Analysis address value m -> (Core Name -> m value) -> Core Name -> m value
eval Analysis{..} eval = \case eval Analysis{..} eval = \case
Var n -> lookupEnv' n >>= deref' n Var n -> lookupEnv' n >>= deref' n
Core (Let n) -> alloc n >>= bind n >> unit Let n -> alloc n >>= bind n >> unit
Core (a :>> b) -> eval a >> eval b a :>> b -> eval a >> eval b
Core (Lam b) -> do Lam b -> do
n <- Gen <$> gensym "lam" n <- Gen <$> gensym "lam"
abstract eval n (instantiate (pure n) b) abstract eval n (instantiate (pure n) b)
Core (f :$ a) -> do f :$ a -> do
f' <- eval f f' <- eval f
a' <- eval a a' <- eval a
apply eval f' a' apply eval f' a'
Core Unit -> unit Unit -> unit
Core (Bool b) -> bool b Bool b -> bool b
Core (If c t e) -> do If c t e -> do
c' <- eval c >>= asBool c' <- eval c >>= asBool
if c' then eval t else eval e if c' then eval t else eval e
Core (String s) -> string s String s -> string s
Core (Load p) -> do Load p -> do
path <- eval p >>= asString path <- eval p >>= asString
lookupEnv' (Path path) >>= deref' (Path path) lookupEnv' (Path path) >>= deref' (Path path)
Core (Edge e a) -> ref a >>= edge e >> unit Edge e a -> ref a >>= edge e >> unit
Core Frame -> frame Frame -> frame
Core (a :. b) -> do a :. b -> do
a' <- ref a a' <- ref a
a' ... eval b a' ... eval b
Core (a := b) -> do a := b -> do
b' <- eval b b' <- eval b
addr <- ref a addr <- ref a
b' <$ assign addr b' b' <$ assign addr b'
Core (Ann loc c) -> local (const loc) (eval c) Ann loc c -> local (const loc) (eval c)
where freeVariable s = fail ("free variable: " <> s) where freeVariable s = fail ("free variable: " <> s)
uninitialized s = fail ("uninitialized variable: " <> s) uninitialized s = fail ("uninitialized variable: " <> s)
invalidRef s = fail ("invalid ref: " <> s) invalidRef s = fail ("invalid ref: " <> s)
@ -65,138 +65,138 @@ eval Analysis{..} eval = \case
ref = \case ref = \case
Var n -> lookupEnv' n Var n -> lookupEnv' n
Core (Let n) -> do Let n -> do
addr <- alloc n addr <- alloc n
addr <$ bind n addr addr <$ bind n addr
Core (If c t e) -> do If c t e -> do
c' <- eval c >>= asBool c' <- eval c >>= asBool
if c' then ref t else ref e if c' then ref t else ref e
Core (a :. b) -> do a :. b -> do
a' <- ref a a' <- ref a
a' ... ref b a' ... ref b
Core (Ann loc c) -> local (const loc) (ref c) Ann loc c -> local (const loc) (ref c)
c -> invalidRef (show c) c -> invalidRef (show c)
prog1 :: File (Core Name) prog1 :: File (Core Name)
prog1 = fromBody . lam foo $ block prog1 = fromBody . lam foo $ block
[ let' bar .= pure foo [ Let bar := pure foo
, if' (pure bar) , If (pure bar)
(Core.bool False) (Bool False)
(Core.bool True) (Bool True)
] ]
where (foo, bar) = (User "foo", User "bar") where (foo, bar) = (User "foo", User "bar")
prog2 :: File (Core Name) prog2 :: File (Core Name)
prog2 = fromBody $ fileBody prog1 $$ Core.bool True prog2 = fromBody $ fileBody prog1 :$ Bool True
prog3 :: File (Core Name) prog3 :: File (Core Name)
prog3 = fromBody $ lams [foo, bar, quux] prog3 = fromBody $ lams [foo, bar, quux]
(if' (pure quux) (If (pure quux)
(pure bar) (pure bar)
(pure foo)) (pure foo))
where (foo, bar, quux) = (User "foo", User "bar", User "quux") where (foo, bar, quux) = (User "foo", User "bar", User "quux")
prog4 :: File (Core Name) prog4 :: File (Core Name)
prog4 = fromBody prog4 = fromBody
$ let' foo .= Core.bool True $ Let foo := Bool True
<> if' (pure foo) <> If (pure foo)
(Core.bool True) (Bool True)
(Core.bool False) (Bool False)
where foo = User "foo" where foo = User "foo"
prog5 :: File (Core Name) prog5 :: File (Core Name)
prog5 = fromBody $ block prog5 = fromBody $ block
[ let' (User "mkPoint") .= lam (User "_x") (lam (User "_y") (block [ Let (User "mkPoint") := lam (User "_x") (lam (User "_y") (block
[ let' (User "x") .= pure (User "_x") [ Let (User "x") := pure (User "_x")
, let' (User "y") .= pure (User "_y")])) , Let (User "y") := pure (User "_y")]))
, let' (User "point") .= pure (User "mkPoint") $$ Core.bool True $$ Core.bool False , Let (User "point") := pure (User "mkPoint") :$ Bool True :$ Bool False
, pure (User "point") Core.... pure (User "x") , pure (User "point") :. pure (User "x")
, pure (User "point") Core.... pure (User "y") .= pure (User "point") Core.... pure (User "x") , pure (User "point") :. pure (User "y") := pure (User "point") :. pure (User "x")
] ]
prog6 :: [File (Core Name)] prog6 :: [File (Core Name)]
prog6 = prog6 =
[ File (Loc "dep" (locSpan (fromJust here))) $ block [ File (Loc "dep" (locSpan (fromJust here))) $ block
[ let' (Path "dep") .= Core.frame [ Let (Path "dep") := Frame
, pure (Path "dep") Core.... block , pure (Path "dep") :. block
[ let' (User "var") .= Core.bool True [ Let (User "var") := Bool True
] ]
] ]
, File (Loc "main" (locSpan (fromJust here))) $ block , File (Loc "main" (locSpan (fromJust here))) $ block
[ load (pure (Path "dep")) [ Load (pure (Path "dep"))
, let' (User "thing") .= pure (Path "dep") Core.... pure (User "var") , Let (User "thing") := pure (Path "dep") :. pure (User "var")
] ]
] ]
ruby :: File (Core Name) ruby :: File (Core Name)
ruby = fromBody . ann . block $ ruby = fromBody . ann . block $
[ ann (let' (User "Class") .= Core.frame) [ ann (Let (User "Class") := Frame)
, ann (pure (User "Class") Core.... , ann (pure (User "Class") :.
(ann (let' (User "new") .= lam (User "self") (block (ann (Let (User "new") := lam (User "self") (block
[ ann (let' (User "instance") .= Core.frame) [ ann (Let (User "instance") := Frame)
, ann (pure (User "instance") Core.... Core.edge Import (pure (User "self"))) , ann (pure (User "instance") :. Edge Import (pure (User "self")))
, ann (pure (User "instance") $$$ "initialize") , ann (pure (User "instance") $$ "initialize")
])))) ]))))
, ann (let' (User "(Object)") .= Core.frame) , ann (Let (User "(Object)") := Frame)
, ann (pure (User "(Object)") Core.... ann (Core.edge Import (pure (User "Class")))) , ann (pure (User "(Object)") :. ann (Edge Import (pure (User "Class"))))
, ann (let' (User "Object") .= Core.frame) , ann (Let (User "Object") := Frame)
, ann (pure (User "Object") Core.... block , ann (pure (User "Object") :. block
[ ann (Core.edge Import (pure (User "(Object)"))) [ ann (Edge Import (pure (User "(Object)")))
, ann (let' (User "nil?") .= lam (User "_") false) , ann (Let (User "nil?") := lam (User "_") false)
, ann (let' (User "initialize") .= lam (User "self") (pure (User "self"))) , ann (Let (User "initialize") := lam (User "self") (pure (User "self")))
, ann (let' __semantic_truthy .= lam (User "_") (Core.bool True)) , ann (Let __semantic_truthy := lam (User "_") (Bool True))
]) ])
, ann (pure (User "Class") Core.... Core.edge Import (pure (User "Object"))) , ann (pure (User "Class") :. Edge Import (pure (User "Object")))
, ann (let' (User "(NilClass)") .= Core.frame) , ann (Let (User "(NilClass)") := Frame)
, ann (pure (User "(NilClass)") Core.... block , ann (pure (User "(NilClass)") :. block
[ ann (Core.edge Import (pure (User "Class"))) [ ann (Edge Import (pure (User "Class")))
, ann (Core.edge Import (pure (User "(Object)"))) , ann (Edge Import (pure (User "(Object)")))
]) ])
, ann (let' (User "NilClass") .= Core.frame) , ann (Let (User "NilClass") := Frame)
, ann (pure (User "NilClass") Core.... block , ann (pure (User "NilClass") :. block
[ ann (Core.edge Import (pure (User "(NilClass)"))) [ ann (Edge Import (pure (User "(NilClass)")))
, ann (Core.edge Import (pure (User "Object"))) , ann (Edge Import (pure (User "Object")))
, ann (let' (User "nil?") .= lam (User "_") true) , ann (Let (User "nil?") := lam (User "_") true)
, ann (let' __semantic_truthy .= lam (User "_") (Core.bool False)) , ann (Let __semantic_truthy := lam (User "_") (Bool False))
]) ])
, ann (let' (User "(TrueClass)") .= Core.frame) , ann (Let (User "(TrueClass)") := Frame)
, ann (pure (User "(TrueClass)") Core.... block , ann (pure (User "(TrueClass)") :. block
[ ann (Core.edge Import (pure (User "Class"))) [ ann (Edge Import (pure (User "Class")))
, ann (Core.edge Import (pure (User "(Object)"))) , ann (Edge Import (pure (User "(Object)")))
]) ])
, ann (let' (User "TrueClass") .= Core.frame) , ann (Let (User "TrueClass") := Frame)
, ann (pure (User "TrueClass") Core.... block , ann (pure (User "TrueClass") :. block
[ ann (Core.edge Import (pure (User "(TrueClass)"))) [ ann (Edge Import (pure (User "(TrueClass)")))
, ann (Core.edge Import (pure (User "Object"))) , ann (Edge Import (pure (User "Object")))
]) ])
, ann (let' (User "(FalseClass)") .= Core.frame) , ann (Let (User "(FalseClass)") := Frame)
, ann (pure (User "(FalseClass)") Core.... block , ann (pure (User "(FalseClass)") :. block
[ ann (Core.edge Import (pure (User "Class"))) [ ann (Edge Import (pure (User "Class")))
, ann (Core.edge Import (pure (User "(Object)"))) , ann (Edge Import (pure (User "(Object)")))
]) ])
, ann (let' (User "FalseClass") .= Core.frame) , ann (Let (User "FalseClass") := Frame)
, ann (pure (User "FalseClass") Core.... block , ann (pure (User "FalseClass") :. block
[ ann (Core.edge Import (pure (User "(FalseClass)"))) [ ann (Edge Import (pure (User "(FalseClass)")))
, ann (Core.edge Import (pure (User "Object"))) , ann (Edge Import (pure (User "Object")))
, ann (let' __semantic_truthy .= lam (User "_") (Core.bool False)) , ann (Let __semantic_truthy := lam (User "_") (Bool False))
]) ])
, ann (let' (User "nil") .= pure (User "NilClass") $$$ "new") , ann (Let (User "nil") := pure (User "NilClass") $$ "new")
, ann (let' (User "true") .= pure (User "TrueClass") $$$ "new") , ann (Let (User "true") := pure (User "TrueClass") $$ "new")
, ann (let' (User "false") .= pure (User "FalseClass") $$$ "new") , ann (Let (User "false") := pure (User "FalseClass") $$ "new")
, ann (let' (User "require") .= lam (User "path") (Core.load (pure (User "path")))) , ann (Let (User "require") := lam (User "path") (Load (pure (User "path"))))
] ]
where -- _nil = pure (User "nil") where -- _nil = pure (User "nil")
true = pure (User "true") true = pure (User "true")
false = pure (User "false") false = pure (User "false")
self $$$ method = annWith callStack $ lam (User "_x") (pure (User "_x") Core.... pure (User method) $$ pure (User "_x")) $$ self self $$ method = annWith callStack $ lam (User "_x") (pure (User "_x") :. pure (User method) :$ pure (User "_x")) :$ self
__semantic_truthy = User "__semantic_truthy" __semantic_truthy = User "__semantic_truthy"

245
semantic-core/src/Data/Core.hs
View File

@ -1,29 +1,20 @@
{-# LANGUAGE DeriveTraversable, FlexibleContexts, LambdaCase, OverloadedStrings, QuantifiedConstraints, RankNTypes, ScopedTypeVariables, StandaloneDeriving, {-# LANGUAGE DeriveTraversable, FlexibleContexts, LambdaCase, OverloadedStrings, QuantifiedConstraints, RankNTypes,
TypeFamilies, TypeOperators #-} ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators #-}
module Data.Core module Data.Core
( Core(..) ( Core(..)
, project
, embed
, CoreF(..) , CoreF(..)
, Edge(..) , Edge(..)
, let'
, block , block
, lam , lam
, lams , lams
, unlam , unlam
, unseq , unseq
, unseqs , unseqs
, ($$)
, ($$*) , ($$*)
, unapply , unapply
, unapplies , unapplies
, unit
, bool
, if'
, string
, load
, edge
, frame
, (...)
, (.=)
, ann , ann
, annWith , annWith
, gfold , gfold
@ -50,35 +41,26 @@ data Edge = Lexical | Import
data Core a data Core a
= Var a = Var a
| Core (CoreF Core a) | Let Name
deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
data CoreF f a
= Let Name
-- | Sequencing without binding; analogous to '>>' or '*>'. -- | Sequencing without binding; analogous to '>>' or '*>'.
| f a :>> f a | Core a :>> Core a
| Lam (f (Incr (f a))) | Lam (Core (Incr (Core a)))
-- | Function application; analogous to '$'. -- | Function application; analogous to '$'.
| f a :$ f a | Core a :$ Core a
| Unit | Unit
| Bool Bool | Bool Bool
| If (f a) (f a) (f a) | If (Core a) (Core a) (Core a)
| String Text | String Text
-- | Load the specified file (by path). -- | Load the specified file (by path).
| Load (f a) | Load (Core a)
| Edge Edge (f a) | Edge Edge (Core a)
-- | Allocation of a new frame. -- | Allocation of a new frame.
| Frame | Frame
| f a :. f a | Core a :. Core a
-- | Assignment of a value to the reference returned by the lhs. -- | Assignment of a value to the reference returned by the lhs.
| f a := f a | Core a := Core a
| Ann Loc (f a) | Ann Loc (Core a)
deriving (Foldable, Functor, Traversable) deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
deriving instance (Eq a, forall x . Eq x => Eq (f x)) => Eq (CoreF f a)
deriving instance (Ord a, forall x . Eq x => Eq (f x)
, forall x . Ord x => Ord (f x)) => Ord (CoreF f a)
deriving instance (Show a, forall x . Show x => Show (f x)) => Show (CoreF f a)
infixl 2 :$ infixl 2 :$
infixr 1 :>> infixr 1 :>>
@ -86,37 +68,102 @@ infix 3 :=
infixl 4 :. infixl 4 :.
instance Semigroup (Core a) where instance Semigroup (Core a) where
a <> b = Core (a :>> b) (<>) = (:>>)
instance Applicative Core where instance Applicative Core where
pure = Var pure = Var
(<*>) = ap (<*>) = ap
instance Monad Core where instance Monad Core where
a >>= f = gfold id let' (<>) (Core . Lam) ($$) unit bool if' string load edge frame (...) (.=) (fmap Core . Ann) pure (f <$> a) a >>= f = gfold id Let (:>>) Lam (:$) Unit Bool If String Load Edge Frame (:.) (:=) Ann pure (f <$> a)
let' :: Name -> Core a project :: Core a -> Either a (CoreF Core a)
let' = Core . Let project (Var a) = Left a
project (Let n) = Right (LetF n)
project (a :>> b) = Right (a :>>$ b)
project (Lam b) = Right (LamF b)
project (f :$ a) = Right (f :$$ a)
project Unit = Right UnitF
project (Bool b) = Right (BoolF b)
project (If c t e) = Right (IfF c t e)
project (String s) = Right (StringF s)
project (Load b) = Right (LoadF b)
project (Edge e b) = Right (EdgeF e b)
project Frame = Right FrameF
project (a :. b) = Right (a :.$ b)
project (a := b) = Right (a :=$ b)
project (Ann l b) = Right (AnnF l b)
embed :: Either a (CoreF Core a) -> Core a
embed = either Var $ \case
LetF n -> Let n
a :>>$ b -> a :>> b
LamF b -> Lam b
f :$$ a -> f :$ a
UnitF -> Unit
BoolF b -> Bool b
IfF c t e -> If c t e
StringF s -> String s
LoadF b -> Load b
EdgeF e b -> Edge e b
FrameF -> Frame
a :.$ b -> a :. b
a :=$ b -> a := b
AnnF l b -> Ann l b
data CoreF f a
= LetF Name
-- | Sequencing without binding; analogous to '>>' or '*>'.
| f a :>>$ f a
| LamF (f (Incr (f a)))
-- | Function application; analogous to '$'.
| f a :$$ f a
| UnitF
| BoolF Bool
| IfF (f a) (f a) (f a)
| StringF Text
-- | Load the specified file (by path).
| LoadF (f a)
| EdgeF Edge (f a)
-- | Allocation of a new frame.
| FrameF
| f a :.$ f a
-- | Assignment of a value to the reference returned by the lhs.
| f a :=$ f a
| AnnF Loc (f a)
deriving (Foldable, Functor, Traversable)
deriving instance (Eq a, forall x . Eq x => Eq (f x)) => Eq (CoreF f a)
deriving instance (Ord a, forall x . Eq x => Eq (f x)
, forall x . Ord x => Ord (f x)) => Ord (CoreF f a)
deriving instance (Show a, forall x . Show x => Show (f x)) => Show (CoreF f a)
infixl 2 :$$
infixr 1 :>>$
infix 3 :=$
infixl 4 :.$
block :: Foldable t => t (Core a) -> Core a block :: Foldable t => t (Core a) -> Core a
block cs block cs
| null cs = unit | null cs = Unit
| otherwise = foldr1 (<>) cs | otherwise = foldr1 (<>) cs
lam :: Eq a => a -> Core a -> Core a lam :: Eq a => a -> Core a -> Core a
lam n b = Core (Lam (bind n b)) lam n b = Lam (bind n b)
lams :: (Eq a, Foldable t) => t a -> Core a -> Core a lams :: (Eq a, Foldable t) => t a -> Core a -> Core a
lams names body = foldr lam body names lams names body = foldr lam body names
unlam :: Alternative m => a -> Core a -> m (a, Core a) unlam :: Alternative m => a -> Core a -> m (a, Core a)
unlam n (Core (Lam b)) = pure (n, instantiate (pure n) b) unlam n (Lam b) = pure (n, instantiate (pure n) b)
unlam _ _ = empty unlam _ _ = empty
unseq :: Alternative m => Core a -> m (Core a, Core a) unseq :: Alternative m => Core a -> m (Core a, Core a)
unseq (Core (a :>> b)) = pure (a, b) unseq (a :>> b) = pure (a, b)
unseq _ = empty unseq _ = empty
unseqs :: Core a -> NonEmpty (Core a) unseqs :: Core a -> NonEmpty (Core a)
unseqs = go unseqs = go
@ -124,62 +171,26 @@ unseqs = go
Just (l, r) -> go l <> go r Just (l, r) -> go l <> go r
Nothing -> t :| [] Nothing -> t :| []
($$) :: Core a -> Core a -> Core a
f $$ a = Core (f :$ a)
infixl 2 $$
-- | Application of a function to a sequence of arguments. -- | Application of a function to a sequence of arguments.
($$*) :: Foldable t => Core a -> t (Core a) -> Core a ($$*) :: Foldable t => Core a -> t (Core a) -> Core a
($$*) = foldl' ($$) ($$*) = foldl' (:$)
infixl 9 $$* infixl 9 $$*
unapply :: Alternative m => Core a -> m (Core a, Core a) unapply :: Alternative m => Core a -> m (Core a, Core a)
unapply (Core (f :$ a)) = pure (f, a) unapply (f :$ a) = pure (f, a)
unapply _ = empty unapply _ = empty
unapplies :: Core a -> (Core a, Stack (Core a)) unapplies :: Core a -> (Core a, Stack (Core a))
unapplies core = case unapply core of unapplies core = case unapply core of
Just (f, a) -> (:> a) <$> unapplies f Just (f, a) -> (:> a) <$> unapplies f
Nothing -> (core, Nil) Nothing -> (core, Nil)
unit :: Core a
unit = Core Unit
bool :: Bool -> Core a
bool = Core . Bool
if' :: Core a -> Core a -> Core a -> Core a
if' c t e = Core (If c t e)
string :: Text -> Core a
string = Core . String
load :: Core a -> Core a
load = Core . Load
edge :: Edge -> Core a -> Core a
edge e b = Core (Edge e b)
frame :: Core a
frame = Core Frame
(...) :: Core a -> Core a -> Core a
a ... b = Core (a :. b)
infixl 4 ...
(.=) :: Core a -> Core a -> Core a
a .= b = Core (a := b)
infix 3 .=
ann :: HasCallStack => Core a -> Core a ann :: HasCallStack => Core a -> Core a
ann = annWith callStack ann = annWith callStack
annWith :: CallStack -> Core a -> Core a annWith :: CallStack -> Core a -> Core a
annWith callStack c = maybe c (flip (fmap Core . Ann) c) (stackLoc callStack) annWith callStack c = maybe c (flip Ann c) (stackLoc callStack)
gfold :: forall m n b gfold :: forall m n b
@ -205,20 +216,20 @@ gfold var let' seq' lam app unit bool if' string load edge frame dot assign ann
where go :: Core (m x) -> n x where go :: Core (m x) -> n x
go = \case go = \case
Var a -> var a Var a -> var a
Core (Let a) -> let' a Let a -> let' a
Core (a :>> b) -> go a `seq'` go b a :>> b -> go a `seq'` go b
Core (Lam b) -> lam (go (k . fmap go <$> b)) Lam b -> lam (go (k . fmap go <$> b))
Core (f :$ a) -> go f `app` go a f :$ a -> go f `app` go a
Core Unit -> unit Unit -> unit
Core (Bool b) -> bool b Bool b -> bool b
Core (If c t e) -> if' (go c) (go t) (go e) If c t e -> if' (go c) (go t) (go e)
Core (String s) -> string s String s -> string s
Core (Load t) -> load (go t) Load t -> load (go t)
Core (Edge e t) -> edge e (go t) Edge e t -> edge e (go t)
Core Frame -> frame Frame -> frame
Core (a :. b) -> go a `dot` go b a :. b -> go a `dot` go b
Core (a := b) -> go a `assign` go b a := b -> go a `assign` go b
Core (Ann loc t) -> ann loc (go t) Ann loc t -> ann loc (go t)
efold :: forall l m n z b efold :: forall l m n z b
. ( forall a b . Coercible a b => Coercible (n a) (n b) . ( forall a b . Coercible a b => Coercible (n a) (n b)
@ -246,23 +257,23 @@ efold :: forall l m n z b
efold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = eiter var alg efold var let' seq' lam app unit bool if' string load edge frame dot assign ann k = eiter var alg
where alg :: forall x l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x) where alg :: forall x l' c z' . Functor c => (forall l'' z'' x . (l'' x -> m (z'' x)) -> c (l'' x) -> n (z'' x)) -> (l' x -> m (z' x)) -> CoreF c (l' x) -> n (z' x)
alg go h = \case alg go h = \case
Let a -> let' a LetF a -> let' a
a :>> b -> go h a `seq'` go h b a :>>$ b -> go h a `seq'` go h b
Lam b -> lam (coerce (go LamF b -> lam (coerce (go
(coerce (k . fmap (go h)) (coerce (k . fmap (go h))
:: ((Incr :.: c :.: l') x -> m ((Incr :.: n :.: z') x))) :: ((Incr :.: c :.: l') x -> m ((Incr :.: n :.: z') x)))
(fmap coerce b))) -- FIXME: can we avoid this fmap and just coerce harder? (fmap coerce b))) -- FIXME: can we avoid this fmap and just coerce harder?
a :$ b -> go h a `app` go h b a :$$ b -> go h a `app` go h b
Unit -> unit UnitF -> unit
Bool b -> bool b BoolF b -> bool b
If c t e -> if' (go h c) (go h t) (go h e) IfF c t e -> if' (go h c) (go h t) (go h e)
String s -> string s StringF s -> string s
Load t -> load (go h t) LoadF t -> load (go h t)
Edge e t -> edge e (go h t) EdgeF e t -> edge e (go h t)
Frame -> frame FrameF -> frame
a :. b -> go h a `dot` go h b a :.$ b -> go h a `dot` go h b
a := b -> go h a `assign` go h b a :=$ b -> go h a `assign` go h b
Ann loc t -> ann loc (go h t) AnnF loc t -> ann loc (go h t)
-- | Efficient Mendler-style iteration. -- | Efficient Mendler-style iteration.
eiter :: forall l m n z b eiter :: forall l m n z b
@ -273,9 +284,9 @@ eiter :: forall l m n z b
-> n (z b) -> n (z b)
eiter var alg = go eiter var alg = go
where go :: forall l' z' x . (l' x -> m (z' x)) -> Core (l' x) -> n (z' x) where go :: forall l' z' x . (l' x -> m (z' x)) -> Core (l' x) -> n (z' x)
go h = \case go h c = case project c of
Var a -> var (h a) Left a -> var (h a)
Core b -> alg go h b Right b -> alg go h b
kfold :: (a -> b) kfold :: (a -> b)
-> (Name -> b) -> (Name -> b)

27
semantic-core/src/Data/Core/Parser.hs
View File

@ -10,8 +10,7 @@ module Data.Core.Parser
import Control.Applicative import Control.Applicative
import qualified Data.Char as Char import qualified Data.Char as Char
import Data.Core hiding (edge, string) import Data.Core
import qualified Data.Core as Core
import Data.Name import Data.Name
import Data.Semigroup import Data.Semigroup
import Data.String import Data.String
@ -50,8 +49,8 @@ core = expr
expr :: (TokenParsing m, Monad m) => m (Core Name) expr :: (TokenParsing m, Monad m) => m (Core Name)
expr = atom `chainl1` go where expr = atom `chainl1` go where
go = choice [ (...) <$ dot go = choice [ (:.) <$ dot
, ($$) <$ notFollowedBy dot , (:$) <$ notFollowedBy dot
] ]
atom :: (TokenParsing m, Monad m) => m (Core Name) atom :: (TokenParsing m, Monad m) => m (Core Name)
@ -69,24 +68,24 @@ comp :: (TokenParsing m, Monad m) => m (Core Name)
comp = braces (sconcat <$> sepEndByNonEmpty expr semi) <?> "compound statement" comp = braces (sconcat <$> sepEndByNonEmpty expr semi) <?> "compound statement"
ifthenelse :: (TokenParsing m, Monad m) => m (Core Name) ifthenelse :: (TokenParsing m, Monad m) => m (Core Name)
ifthenelse = if' ifthenelse = If
<$ reserved "if" <*> core <$ reserved "if" <*> core
<* reserved "then" <*> core <* reserved "then" <*> core
<* reserved "else" <*> core <* reserved "else" <*> core
<?> "if-then-else statement" <?> "if-then-else statement"
assign :: (TokenParsing m, Monad m) => m (Core Name) assign :: (TokenParsing m, Monad m) => m (Core Name)
assign = fmap Core . (:=) <$> try (lvalue <* symbolic '=') <*> core <?> "assignment" assign = (:=) <$> try (lvalue <* symbolic '=') <*> core <?> "assignment"
edge :: (TokenParsing m, Monad m) => m (Core Name) edge :: (TokenParsing m, Monad m) => m (Core Name)
edge = kw <*> expr where kw = choice [ Core.edge Lexical <$ reserved "lexical" edge = kw <*> expr where kw = choice [ Edge Lexical <$ reserved "lexical"
, Core.edge Import <$ reserved "import" , Edge Import <$ reserved "import"
, Core.load <$ reserved "load" , Load <$ reserved "load"
] ]
lvalue :: (TokenParsing m, Monad m) => m (Core Name) lvalue :: (TokenParsing m, Monad m) => m (Core Name)
lvalue = choice lvalue = choice
[ let' <$ reserved "let" <*> name [ Let <$ reserved "let" <*> name
, ident , ident
, parens expr , parens expr
] ]
@ -100,10 +99,10 @@ name = choice [regular, strpath] <?> "name" where
lit :: (TokenParsing m, Monad m) => m (Core Name) lit :: (TokenParsing m, Monad m) => m (Core Name)
lit = let x `given` n = x <$ reserved n in choice lit = let x `given` n = x <$ reserved n in choice
[ Core.bool True `given` "#true" [ Bool True `given` "#true"
, Core.bool False `given` "#false" , Bool False `given` "#false"
, Core.unit `given` "#unit" , Unit `given` "#unit"
, Core.frame `given` "#frame" , Frame `given` "#frame"
, lambda , lambda
] <?> "literal" ] <?> "literal"

30
semantic-core/src/Data/Core/Pretty.hs
View File

@ -116,8 +116,8 @@ prettify :: (Member Naming sig, Member (Reader Prec) sig, Member (Reader Style)
-> m AnsiDoc -> m AnsiDoc
prettify = \case prettify = \case
Var a -> pure $ name a Var a -> pure $ name a
Core (Let a) -> pure $ keyword "let" <+> name a Let a -> pure $ keyword "let" <+> name a
Core (a :>> b) -> do a :>> b -> do
prec <- ask @Prec prec <- ask @Prec
fore <- with 12 (prettify a) fore <- with 12 (prettify a)
aft <- with 12 (prettify b) aft <- with 12 (prettify b)
@ -129,41 +129,41 @@ prettify = \case
pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body) pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
Core (Lam f) -> inParens 11 $ do Lam f -> inParens 11 $ do
x <- Gen <$> gensym "" x <- Gen <$> gensym ""
body <- prettify (instantiate (pure x) f) body <- prettify (instantiate (pure x) f)
lam <- lambda lam <- lambda
arr <- arrow arr <- arrow
pure (lam <> name x <+> arr <+> body) pure (lam <> name x <+> arr <+> body)
Core Frame -> pure $ primitive "frame" Frame -> pure $ primitive "frame"
Core Unit -> pure $ primitive "unit" Unit -> pure $ primitive "unit"
Core (Bool b) -> pure $ primitive (if b then "true" else "false") Bool b -> pure $ primitive (if b then "true" else "false")
Core (String s) -> pure . strlit $ Pretty.viaShow s String s -> pure . strlit $ Pretty.viaShow s
Core (f :$ x) -> inParens 11 $ (<+>) <$> prettify f <*> prettify x f :$ x -> inParens 11 $ (<+>) <$> prettify f <*> prettify x
Core (If con tru fal) -> do If con tru fal -> do
con' <- "if" `appending` prettify con con' <- "if" `appending` prettify con
tru' <- "then" `appending` prettify tru tru' <- "then" `appending` prettify tru
fal' <- "else" `appending` prettify fal fal' <- "else" `appending` prettify fal
pure $ Pretty.sep [con', tru', fal'] pure $ Pretty.sep [con', tru', fal']
Core (Load p) -> "load" `appending` prettify p Load p -> "load" `appending` prettify p
Core (Edge Lexical n) -> "lexical" `appending` prettify n Edge Lexical n -> "lexical" `appending` prettify n
Core (Edge Import n) -> "import" `appending` prettify n Edge Import n -> "import" `appending` prettify n
Core (item :. body) -> inParens 5 $ do item :. body -> inParens 5 $ do
f <- prettify item f <- prettify item
g <- prettify body g <- prettify body
pure (f <> symbol "." <> g) pure (f <> symbol "." <> g)
Core (lhs := rhs) -> inParens 4 $ do lhs := rhs -> inParens 4 $ do
f <- prettify lhs f <- prettify lhs
g <- prettify rhs g <- prettify rhs
pure (f <+> symbol "=" <+> g) pure (f <+> symbol "=" <+> g)
-- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly. -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
Core (Ann _ c) -> prettify c Ann _ c -> prettify c
appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
appending k item = (keyword k <+>) <$> item appending k item = (keyword k <+>) <$> item