github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-12-01 09:15:01 +03:00
Code Issues Projects Releases Wiki Activity

Remove everything but the primitives from Intro.

Browse Source
This commit is contained in:
Rob Rix 2019-11-07 10:37:34 -05:00
parent 4a0aa126fd
commit 4185f213e3
No known key found for this signature in database
GPG Key ID: F188A01508EA1CF7
1 changed files with 3 additions and 73 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

76
semantic-analysis/src/Analysis/Intro.hs
View File

@ -1,81 +1,11 @@
{-# LANGUAGE DataKinds, DeriveGeneric, DeriveTraversable, FlexibleContexts, QuantifiedConstraints, StandaloneDeriving #-}
module Analysis.Intro
( unit
, bool
, string
, record
, lam
, lamFin
, lams
, unlam
, unlamFin
, lam'
, Intro(..)
, Name(..)
( Intro(..)
) where
import Analysis.Name
import Control.Applicative (Alternative(..))
import Control.Effect.Carrier
import Data.Text (Text)
import GHC.Generics (Generic1)
import Syntax.Fin as Fin
import Syntax.Module
import Syntax.Scope
import Syntax.Term
import Syntax.Var
unit :: (Carrier sig m, Member Intro sig) => m a
unit = send Unit
bool :: (Carrier sig m, Member Intro sig) => Bool -> m a
bool = send . Bool
string :: (Carrier sig m, Member Intro sig) => Text -> m a
string = send . String
record :: (Carrier sig m, Member Intro sig) => [(Name, m a)] -> m a
record fs = send (Record fs)
lam :: (Eq a, Carrier sig m, Member Intro sig) => Maybe Name -> a -> m a -> m a
lam u n b = send (Lam u (abstract1 n b))
lams :: (Eq a, Foldable t, Carrier sig m, Member Intro sig) => t (Maybe Name, a) -> m a -> m a
lams names body = foldr (uncurry lam) body names
unlam :: (Alternative m, Member Intro sig, RightModule sig) => a -> Term sig a -> m (Maybe Name, a, Term sig a)
unlam n (Alg sig) | Just (Lam n' b) <- prj sig = pure (n', n, instantiate1 (pure n) b)
unlam _ _ = empty
lamFin :: (Carrier sig m, Member Intro sig) => Maybe Name -> m (Fin ('S n)) -> m (Fin n)
lamFin u b = send (Lam u (abstractVar (maybe (B ()) F . Fin.strengthen) b))
unlamFin :: (Alternative m, Member Intro sig, RightModule sig) => Term sig (Fin n) -> m (Maybe Name, Term sig (Fin ('S n)))
unlamFin (Alg sig) | Just (Lam n b) <- prj sig = pure (n, instantiateVar (unVar (const (pure FZ)) (pure . FS)) b)
unlamFin _ = empty
lam' :: (Carrier sig m, Member Intro sig) => Maybe Name -> m (Var () a) -> m a
lam' u b = send (Lam u (toScope b))
data Intro f a
data Intro
= Unit
| Bool Bool
| String Text
| Record [(Name, f a)]
| Lam (Maybe Name) (Scope () f a)
deriving (Foldable, Functor, Generic1, Traversable)
deriving instance (Eq a, forall a . Eq a => Eq (f a), Monad f) => Eq (Intro f a)
deriving instance (Ord a, forall a . Eq a => Eq (f a)
, forall a . Ord a => Ord (f a), Monad f) => Ord (Intro f a)
deriving instance (Show a, forall a . Show a => Show (f a)) => Show (Intro f a)
instance HFunctor Intro
instance RightModule Intro where
Unit >>=* _ = Unit
Bool b >>=* _ = Bool b
String s >>=* _ = String s
Record fs >>=* f = Record (map (fmap (>>= f)) fs)
Lam n b >>=* f = Lam n (b >>=* f)
deriving (Eq, Ord, Show)