mirror of
https://github.com/github/semantic.git
synced 2024-12-25 07:55:12 +03:00
Use Scope in Core.
This commit is contained in:
parent
37be0183c3
commit
fc757694c8
@ -65,7 +65,7 @@ data CoreF f a
|
||||
= Let Name
|
||||
-- | Sequencing without binding; analogous to '>>' or '*>'.
|
||||
| f a :>> f a
|
||||
| Lam (f (Incr (f a)))
|
||||
| Lam (Scope f a)
|
||||
-- | Function application; analogous to '$'.
|
||||
| f a :$ f a
|
||||
| Unit
|
||||
@ -83,10 +83,10 @@ data CoreF f a
|
||||
| Ann Loc (f a)
|
||||
deriving (Foldable, Functor, Traversable)
|
||||
|
||||
deriving instance (Eq a, forall a . Eq a => Eq (f a)) => Eq (CoreF f a)
|
||||
deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (CoreF f a)
|
||||
deriving instance (Ord a, forall a . Eq a => Eq (f a)
|
||||
, forall a . Ord a => Ord (f a)) => Ord (CoreF f a)
|
||||
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (CoreF f a)
|
||||
, forall a . Ord a => Ord (f a), Monad f) => Ord (CoreF f a)
|
||||
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (CoreF f a)
|
||||
|
||||
infixl 2 :$
|
||||
infixr 1 :>>
|
||||
@ -180,7 +180,7 @@ efold :: forall m n a b
|
||||
. (forall a . m a -> n a)
|
||||
-> (forall a . Name -> n a)
|
||||
-> (forall a . n a -> n a -> n a)
|
||||
-> (forall a . n (Incr (n a)) -> n a)
|
||||
-> (forall a . Scope n a -> n a)
|
||||
-> (forall a . n a -> n a -> n a)
|
||||
-> (forall a . n a)
|
||||
-> (forall a . Bool -> n a)
|
||||
@ -203,7 +203,7 @@ efold var let' seq' lam app unit bool if' string load edge frame dot assign ann
|
||||
Core c -> case c of
|
||||
Let a -> let' a
|
||||
a :>> b -> go h a `seq'` go h b
|
||||
Lam b -> lam (go (k . fmap (go h)) b)
|
||||
Lam b -> lam (foldScope k go h b)
|
||||
a :$ b -> go h a `app` go h b
|
||||
Unit -> unit
|
||||
Bool b -> bool b
|
||||
|
@ -187,9 +187,9 @@ foldScope :: (forall a . Incr (n a) -> m (Incr (n a)))
|
||||
foldScope k go h = Scope . go (k . fmap (go h)) . unScope
|
||||
|
||||
-- | Bind occurrences of a variable in a term, producing a term in which the variable is bound.
|
||||
bind :: (Applicative f, Eq a) => a -> f a -> f (Incr (f a))
|
||||
bind name = fmap (match name)
|
||||
bind :: (Applicative f, Eq a) => a -> f a -> Scope f a
|
||||
bind name = Scope . fmap (match name)
|
||||
|
||||
-- | Substitute a term for the free variable in a given term, producing a closed term.
|
||||
instantiate :: Monad f => f a -> f (Incr (f a)) -> f a
|
||||
instantiate t b = b >>= fromIncr t
|
||||
instantiate :: Monad f => f a -> Scope f a -> f a
|
||||
instantiate t = unScope >=> fromIncr t
|
||||
|
Loading…
Reference in New Issue
Block a user