mirror of
https://github.com/github/semantic.git
synced 2024-11-24 08:54:07 +03:00
Rename the Term constructor to Alg.
This commit is contained in:
parent
87282872e6
commit
cde9635319
@ -39,7 +39,7 @@ eval :: ( Carrier sig m
|
|||||||
-> (Term (Ann Span :+: Core) Name -> m value)
|
-> (Term (Ann Span :+: Core) Name -> m value)
|
||||||
eval Analysis{..} eval = \case
|
eval Analysis{..} eval = \case
|
||||||
Var n -> lookupEnv' n >>= deref' n
|
Var n -> lookupEnv' n >>= deref' n
|
||||||
Term (R c) -> case c of
|
Alg (R c) -> case c of
|
||||||
Rec (Named (Ignored n) b) -> do
|
Rec (Named (Ignored n) b) -> do
|
||||||
addr <- alloc n
|
addr <- alloc n
|
||||||
v <- bind n addr (eval (instantiate1 (pure n) b))
|
v <- bind n addr (eval (instantiate1 (pure n) b))
|
||||||
@ -73,7 +73,7 @@ eval Analysis{..} eval = \case
|
|||||||
b' <- eval b
|
b' <- eval b
|
||||||
addr <- ref a
|
addr <- ref a
|
||||||
b' <$ assign addr b'
|
b' <$ assign addr b'
|
||||||
Term (L (Ann span c)) -> local (const span) (eval c)
|
Alg (L (Ann span c)) -> local (const span) (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)
|
||||||
@ -83,7 +83,7 @@ eval Analysis{..} eval = \case
|
|||||||
|
|
||||||
ref = \case
|
ref = \case
|
||||||
Var n -> lookupEnv' n
|
Var n -> lookupEnv' n
|
||||||
Term (R c) -> case c of
|
Alg (R c) -> case c of
|
||||||
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
|
||||||
@ -91,7 +91,7 @@ eval Analysis{..} eval = \case
|
|||||||
a' <- ref a
|
a' <- ref a
|
||||||
a' ... b >>= maybe (freeVariable (show b)) pure
|
a' ... b >>= maybe (freeVariable (show b)) pure
|
||||||
c -> invalidRef (show c)
|
c -> invalidRef (show c)
|
||||||
Term (L (Ann span c)) -> local (const span) (ref c)
|
Alg (L (Ann span c)) -> local (const span) (ref c)
|
||||||
|
|
||||||
|
|
||||||
prog1 :: (Carrier sig t, Member Core sig) => File (t Name)
|
prog1 :: (Carrier sig t, Member Core sig) => File (t Name)
|
||||||
|
@ -166,24 +166,24 @@ typecheckingAnalysis = Analysis{..}
|
|||||||
arg <- meta
|
arg <- meta
|
||||||
assign addr arg
|
assign addr arg
|
||||||
ty <- eval body
|
ty <- eval body
|
||||||
pure (Term (Arr arg ty))
|
pure (Alg (Arr arg ty))
|
||||||
apply _ f a = do
|
apply _ f a = do
|
||||||
_A <- meta
|
_A <- meta
|
||||||
_B <- meta
|
_B <- meta
|
||||||
unify (Term (Arr _A _B)) f
|
unify (Alg (Arr _A _B)) f
|
||||||
unify _A a
|
unify _A a
|
||||||
pure _B
|
pure _B
|
||||||
unit = pure (Term Unit)
|
unit = pure (Alg Unit)
|
||||||
bool _ = pure (Term Bool)
|
bool _ = pure (Alg Bool)
|
||||||
asBool b = unify (Term Bool) b >> pure True <|> pure False
|
asBool b = unify (Alg Bool) b >> pure True <|> pure False
|
||||||
string _ = pure (Term String)
|
string _ = pure (Alg String)
|
||||||
asString s = unify (Term String) s $> mempty
|
asString s = unify (Alg String) s $> mempty
|
||||||
record fields = do
|
record fields = do
|
||||||
fields' <- for fields $ \ (k, v) -> do
|
fields' <- for fields $ \ (k, v) -> do
|
||||||
addr <- alloc k
|
addr <- alloc k
|
||||||
(k, v) <$ assign addr v
|
(k, v) <$ assign addr v
|
||||||
-- FIXME: should records reference types by address instead?
|
-- FIXME: should records reference types by address instead?
|
||||||
pure (Term (Record (Map.fromList fields')))
|
pure (Alg (Record (Map.fromList fields')))
|
||||||
_ ... m = pure (Just m)
|
_ ... m = pure (Just m)
|
||||||
|
|
||||||
|
|
||||||
@ -212,8 +212,8 @@ solve :: (Carrier sig m, Member (State Substitution) sig, MonadFail m) => Set.Se
|
|||||||
solve cs = for_ cs solve
|
solve cs = for_ cs solve
|
||||||
where solve = \case
|
where solve = \case
|
||||||
-- FIXME: how do we enforce proper subtyping? row polymorphism or something?
|
-- FIXME: how do we enforce proper subtyping? row polymorphism or something?
|
||||||
Term (Record f1) :===: Term (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
|
Alg (Record f1) :===: Alg (Record f2) -> traverse solve (Map.intersectionWith (:===:) f1 f2) $> ()
|
||||||
Term (Arr a1 b1) :===: Term (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2)
|
Alg (Arr a1 b1) :===: Alg (Arr a2 b2) -> solve (a1 :===: a2) *> solve (b1 :===: b2)
|
||||||
Var m1 :===: Var m2 | m1 == m2 -> pure ()
|
Var m1 :===: Var m2 | m1 == m2 -> pure ()
|
||||||
Var m1 :===: t2 -> do
|
Var m1 :===: t2 -> do
|
||||||
sol <- solution m1
|
sol <- solution m1
|
||||||
|
@ -118,8 +118,8 @@ a >>> b = send (a :>> b)
|
|||||||
infixr 1 >>>
|
infixr 1 >>>
|
||||||
|
|
||||||
unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||||
unseq (Term sig) | Just (a :>> b) <- prj sig = pure (a, b)
|
unseq (Alg sig) | Just (a :>> b) <- prj sig = pure (a, b)
|
||||||
unseq _ = empty
|
unseq _ = empty
|
||||||
|
|
||||||
unseqs :: Member Core sig => Term sig a -> NonEmpty (Term sig a)
|
unseqs :: Member Core sig => Term sig a -> NonEmpty (Term sig a)
|
||||||
unseqs = go
|
unseqs = go
|
||||||
@ -135,8 +135,8 @@ Named u n :<- a >>>= b = send (Named u a :>>= abstract1 n b)
|
|||||||
infixr 1 >>>=
|
infixr 1 >>>=
|
||||||
|
|
||||||
unbind :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a)
|
unbind :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a)
|
||||||
unbind n (Term sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
|
unbind n (Alg sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
|
||||||
unbind _ _ = empty
|
unbind _ _ = empty
|
||||||
|
|
||||||
unstatement :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Maybe (Named a) :<- Term sig a, Term sig a)
|
unstatement :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Maybe (Named a) :<- Term sig a, Term sig a)
|
||||||
unstatement n t = first (first Just) <$> unbind n t <|> first (Nothing :<-) <$> unseq t
|
unstatement n t = first (first Just) <$> unbind n t <|> first (Nothing :<-) <$> unseq t
|
||||||
@ -164,8 +164,8 @@ lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a
|
|||||||
lams names body = foldr lam body names
|
lams names body = foldr lam body names
|
||||||
|
|
||||||
unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
|
unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
|
||||||
unlam n (Term sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
|
unlam n (Alg sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
|
||||||
unlam _ _ = empty
|
unlam _ _ = empty
|
||||||
|
|
||||||
($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
|
||||||
f $$ a = send (f :$ a)
|
f $$ a = send (f :$ a)
|
||||||
@ -179,8 +179,8 @@ infixl 8 $$
|
|||||||
infixl 8 $$*
|
infixl 8 $$*
|
||||||
|
|
||||||
unapply :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
unapply :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
|
||||||
unapply (Term sig) | Just (f :$ a) <- prj sig = pure (f, a)
|
unapply (Alg sig) | Just (f :$ a) <- prj sig = pure (f, a)
|
||||||
unapply _ = empty
|
unapply _ = empty
|
||||||
|
|
||||||
unapplies :: Member Core sig => Term sig a -> (Term sig a, Stack (Term sig a))
|
unapplies :: Member Core sig => Term sig a -> (Term sig a, Stack (Term sig a))
|
||||||
unapplies core = case unapply core of
|
unapplies core = case unapply core of
|
||||||
@ -237,6 +237,6 @@ annWith callStack = maybe id (annAt . snd) (stackLoc callStack)
|
|||||||
|
|
||||||
|
|
||||||
stripAnnotations :: forall ann a sig . (HFunctor sig, forall g . Functor g => Functor (sig g)) => Term (Ann ann :+: sig) a -> Term sig a
|
stripAnnotations :: forall ann a sig . (HFunctor sig, forall g . Functor g => Functor (sig g)) => Term (Ann ann :+: sig) a -> Term sig a
|
||||||
stripAnnotations (Var v) = Var v
|
stripAnnotations (Var v) = Var v
|
||||||
stripAnnotations (Term (L (Ann _ b))) = stripAnnotations b
|
stripAnnotations (Alg (L (Ann _ b))) = stripAnnotations b
|
||||||
stripAnnotations (Term (R b)) = Term (hmap stripAnnotations b)
|
stripAnnotations (Alg (R b)) = Alg (hmap stripAnnotations b)
|
||||||
|
@ -48,7 +48,7 @@ prettyCore :: Style -> Term Core Name -> AnsiDoc
|
|||||||
prettyCore style = precBody . go . fmap name
|
prettyCore style = precBody . go . fmap name
|
||||||
where go = \case
|
where go = \case
|
||||||
Var v -> atom v
|
Var v -> atom v
|
||||||
Term t -> case t of
|
Alg t -> case t of
|
||||||
Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
|
Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
|
||||||
[ keyword "rec" <+> name x
|
[ keyword "rec" <+> name x
|
||||||
, symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b)))
|
, symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b)))
|
||||||
@ -80,7 +80,7 @@ prettyCore style = precBody . go . fmap name
|
|||||||
]
|
]
|
||||||
|
|
||||||
statement ->
|
statement ->
|
||||||
let (bindings, return) = unstatements (Term statement)
|
let (bindings, return) = unstatements (Alg statement)
|
||||||
statements = toList (bindings :> (Nothing :<- return))
|
statements = toList (bindings :> (Nothing :<- return))
|
||||||
names = zipWith (\ i (n :<- _) -> maybe (pretty @Int i) (name . namedName) n) [0..] statements
|
names = zipWith (\ i (n :<- _) -> maybe (pretty @Int i) (name . namedName) n) [0..] statements
|
||||||
statements' = map (prettyStatement names) statements
|
statements' = map (prettyStatement names) statements
|
||||||
|
@ -10,7 +10,7 @@ import Control.Monad.Module
|
|||||||
|
|
||||||
data Term sig a
|
data Term sig a
|
||||||
= Var a
|
= Var a
|
||||||
| Term (sig (Term sig) a)
|
| Alg (sig (Term sig) a)
|
||||||
|
|
||||||
deriving instance ( Eq a
|
deriving instance ( Eq a
|
||||||
, RightModule sig
|
, RightModule sig
|
||||||
@ -37,14 +37,14 @@ instance RightModule sig => Applicative (Term sig) where
|
|||||||
(<*>) = ap
|
(<*>) = ap
|
||||||
|
|
||||||
instance RightModule sig => Monad (Term sig) where
|
instance RightModule sig => Monad (Term sig) where
|
||||||
Var a >>= f = f a
|
Var a >>= f = f a
|
||||||
Term t >>= f = Term (t >>=* f)
|
Alg t >>= f = Alg (t >>=* f)
|
||||||
|
|
||||||
instance RightModule sig => Carrier sig (Term sig) where
|
instance RightModule sig => Carrier sig (Term sig) where
|
||||||
eff = Term
|
eff = Alg
|
||||||
|
|
||||||
|
|
||||||
hoistTerm :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => (forall m x . sig m x -> sig' m x) -> Term sig a -> Term sig' a
|
hoistTerm :: (HFunctor sig, forall g . Functor g => Functor (sig g)) => (forall m x . sig m x -> sig' m x) -> Term sig a -> Term sig' a
|
||||||
hoistTerm f = go
|
hoistTerm f = go
|
||||||
where go (Var v) = Var v
|
where go (Var v) = Var v
|
||||||
go (Term t) = Term (f (hmap (hoistTerm f) t))
|
go (Alg t) = Alg (f (hmap (hoistTerm f) t))
|
||||||
|
Loading…
Reference in New Issue
Block a user