mirror of
https://github.com/github/semantic.git
synced 2024-12-26 08:25:19 +03:00
Split concretization into the primitive operations.
This allows us to produce values of the correct type for abstract domains which don’t distinguish between primitive types, and to act on the expected type when e.g. typechecking by unifying.
This commit is contained in:
Rob Rix
parent
582c71f355
commit
37e5ba4986
@ -111,14 +111,15 @@ instance ( Applicative term
|
||||
, Has (A.Heap Addr (Concrete term)) sig m
|
||||
, Has (Reader Path.AbsRelFile) sig m
|
||||
, Has (Reader Span) sig m
|
||||
, MonadFail m
|
||||
)
|
||||
=> Algebra (Domain term Addr (Concrete term) :+: sig) (DomainC term m) where
|
||||
alg = \case
|
||||
L (Abstract i k) -> case i of
|
||||
I.Unit -> k Unit
|
||||
I.Bool b -> k (Bool b)
|
||||
I.String s -> k (String s)
|
||||
I.Lam b -> do
|
||||
I.Unit -> k Unit
|
||||
I.Bool b -> k (Bool b)
|
||||
I.String s -> k (String s)
|
||||
I.Lam b -> do
|
||||
path <- ask
|
||||
span <- ask
|
||||
k (Closure path span b)
|
||||
@ -130,12 +131,18 @@ instance ( Applicative term
|
||||
A.assign @Addr @(Concrete term) addr v
|
||||
pure (name, addr)
|
||||
k (Record (Map.fromList fields'))
|
||||
L (Concretize c k) -> case c of
|
||||
Unit -> k I.Unit
|
||||
Bool b -> k (I.Bool b)
|
||||
String s -> k (I.String s)
|
||||
Closure _ _ b -> k (I.Lam b)
|
||||
Record fields -> k (I.Record (map (fmap pure) (Map.toList fields)))
|
||||
L (AsBool c k) -> case c of
|
||||
Bool b -> k b
|
||||
_ -> fail "expected Bool"
|
||||
L (AsString c k) -> case c of
|
||||
String s -> k s
|
||||
_ -> fail "expected String"
|
||||
L (AsLam c k) -> case c of
|
||||
Closure _ _ b -> k b
|
||||
_ -> fail "expected Closure"
|
||||
L (AsRecord c k) -> case c of
|
||||
Record fields -> k (map (fmap pure) (Map.toList fields))
|
||||
_ -> fail "expected Record"
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
|
||||
|
||||
@ -9,7 +9,6 @@
|
||||
module Analysis.Effect.Domain
|
||||
( -- * Domain effect
|
||||
abstract
|
||||
, concretize
|
||||
, unit
|
||||
, bool
|
||||
, asBool
|
||||
@ -30,8 +29,6 @@ import Analysis.Intro (Intro)
|
||||
import qualified Analysis.Intro as A
|
||||
import Analysis.Name
|
||||
import Control.Algebra
|
||||
import Control.Monad ((>=>))
|
||||
import Control.Monad.Fail as Fail
|
||||
import Data.Text (Text)
|
||||
import GHC.Generics (Generic1)
|
||||
import Syntax.Scope (Scope)
|
||||
@ -39,9 +36,6 @@ import Syntax.Scope (Scope)
|
||||
abstract :: Has (Domain term addr abstract) sig m => Intro term addr -> m abstract
|
||||
abstract concrete = send (Abstract concrete pure)
|
||||
|
||||
concretize :: Has (Domain term addr abstract) sig m => abstract -> m (Intro term addr)
|
||||
concretize abstract = send (Concretize abstract pure)
|
||||
|
||||
|
||||
unit :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => m abstract
|
||||
unit = abstract @term @addr A.Unit
|
||||
@ -49,46 +43,37 @@ unit = abstract @term @addr A.Unit
|
||||
bool :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => Bool -> m abstract
|
||||
bool = abstract @term @addr . A.Bool
|
||||
|
||||
asBool :: forall term addr abstract m sig . (Has (Domain term addr abstract) sig m, MonadFail m, Show addr, forall a . Show a => Show (term a)) => abstract -> m Bool
|
||||
asBool = concretize @term @addr >=> \case
|
||||
A.Bool b -> pure b
|
||||
other -> typeError "Bool" other
|
||||
asBool :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => abstract -> m Bool
|
||||
asBool v = send (AsBool @term @addr v pure)
|
||||
|
||||
string :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => Text -> m abstract
|
||||
string = abstract @term @addr . A.String
|
||||
|
||||
asString :: forall term addr abstract m sig . (Has (Domain term addr abstract) sig m, MonadFail m, Show addr, forall a . Show a => Show (term a)) => abstract -> m Text
|
||||
asString = concretize @term @addr >=> \case
|
||||
A.String t -> pure t
|
||||
other -> typeError "String" other
|
||||
asString :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => abstract -> m Text
|
||||
asString v = send (AsString @term @addr v pure)
|
||||
|
||||
|
||||
lam :: Has (Domain term addr abstract) sig m => Named (Scope () term addr) -> m abstract
|
||||
lam = abstract . A.Lam
|
||||
|
||||
asLam :: (Has (Domain term addr abstract) sig m, MonadFail m, Show addr, forall a . Show a => Show (term a)) => abstract -> m (Named (Scope () term addr))
|
||||
asLam = concretize >=> \case
|
||||
A.Lam b -> pure b
|
||||
other -> typeError "Lam" other
|
||||
asLam :: Has (Domain term addr abstract) sig m => abstract -> m (Named (Scope () term addr))
|
||||
asLam v = send (AsLam v pure)
|
||||
|
||||
|
||||
record :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => [(Name, term addr)] -> m abstract
|
||||
record = abstract @term . A.Record
|
||||
|
||||
asRecord :: forall term addr abstract m sig . (Has (Domain term addr abstract) sig m, MonadFail m, Show addr, forall a . Show a => Show (term a)) => abstract -> m [(Name, term addr)]
|
||||
asRecord = concretize @term >=> \case
|
||||
A.Record fs -> pure fs
|
||||
other -> typeError "Record" other
|
||||
asRecord :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => abstract -> m [(Name, term addr)]
|
||||
asRecord v = send (AsRecord v pure)
|
||||
|
||||
|
||||
data Domain term addr abstract m k
|
||||
= Abstract (Intro term addr) (abstract -> m k)
|
||||
| Concretize abstract (Intro term addr -> m k)
|
||||
= Abstract (Intro term addr) (abstract -> m k)
|
||||
| AsBool abstract (Bool -> m k)
|
||||
| AsString abstract (Text -> m k)
|
||||
| AsLam abstract (Named (Scope () term addr) -> m k)
|
||||
| AsRecord abstract ([(Name, term addr)] -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
instance HFunctor (Domain term addr abstract)
|
||||
instance Effect (Domain term addr abstract)
|
||||
|
||||
|
||||
typeError :: (Show a, MonadFail m) => String -> a -> m b
|
||||
typeError expected actual = Fail.fail $ "expected " <> expected <> ", got " <> show actual
|
||||
|
||||
@ -112,7 +112,7 @@ instance MonadTrans (DomainC term) where
|
||||
lift = DomainC . lift
|
||||
|
||||
-- FIXME: decompose into a product domain and two atomic domains
|
||||
instance Has (Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRelFile :+: Reader Span) sig m => Algebra (A.Domain term Addr (Value (Semi term)) :+: sig) (DomainC term m) where
|
||||
instance (Alternative m, Has (Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRelFile :+: Reader Span) sig m, MonadFail m) => Algebra (A.Domain term Addr (Value (Semi term)) :+: sig) (DomainC term m) where
|
||||
alg = \case
|
||||
L (A.Abstract i k) -> case i of
|
||||
I.Unit -> k mempty
|
||||
@ -129,8 +129,11 @@ instance Has (Env Addr :+: A.Heap Addr (Value (Semi term)) :+: Reader Path.AbsRe
|
||||
v <- lift (eval t)
|
||||
v <$ A.assign @Addr @(Value (Semi term)) addr v
|
||||
k (fold fields)
|
||||
L (A.Concretize (Value s _) k) -> case s of
|
||||
Abstract -> k I.Unit -- FIXME: this should be broken down for case analysis
|
||||
String s -> k (I.String s)
|
||||
Closure _ _ b -> k (I.Lam b)
|
||||
L (A.AsBool _ k) -> k True <|> k False
|
||||
L (A.AsString _ k) -> k mempty
|
||||
L (A.AsLam (Value v _) k) -> case v of
|
||||
Closure _ _ b -> k b
|
||||
String _ -> fail $ "expected closure, got String"
|
||||
Abstract -> fail $ "expected closure, got Abstract"
|
||||
L (A.AsRecord _ k) -> k []
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
@ -101,7 +101,7 @@ newtype DomainC term m a = DomainC (ReaderC (term Addr -> m ScopeGraph) m a)
|
||||
instance MonadTrans (DomainC term) where
|
||||
lift = DomainC . lift
|
||||
|
||||
instance (Has (Env Addr :+: A.Heap Addr ScopeGraph :+: Reader Path.AbsRelFile :+: Reader Span) sig m, Monad term) => Algebra (Domain term Addr ScopeGraph :+: sig) (DomainC term m) where
|
||||
instance (Alternative m, Has (Env Addr :+: A.Heap Addr ScopeGraph :+: Reader Path.AbsRelFile :+: Reader Span) sig m, Monad term) => Algebra (Domain term Addr ScopeGraph :+: sig) (DomainC term m) where
|
||||
alg = \case
|
||||
L (Abstract i k) -> case i of
|
||||
Unit -> k mempty
|
||||
@ -123,5 +123,8 @@ instance (Has (Env Addr :+: A.Heap Addr ScopeGraph :+: Reader Path.AbsRelFile :+
|
||||
let v' = ScopeGraph (Map.singleton (Decl k path span) mempty) <> v
|
||||
v' <$ A.assign @Addr addr v'
|
||||
k (fold fields')
|
||||
L (Concretize _ k) -> k Unit -- FIXME: break Concretize out by constructor.
|
||||
L (AsBool _ k) -> k True <|> k False
|
||||
L (AsString _ k) -> k mempty
|
||||
L (AsLam _ k) -> alloc (Name mempty) >>= k . Named (Name mempty) . lift . pure
|
||||
L (AsRecord _ k) -> k []
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
@ -223,38 +223,56 @@ instance ( Alternative m
|
||||
, Has (Env Addr) sig m
|
||||
, Has Fresh sig m
|
||||
, Has (A.Heap Addr Type) sig m
|
||||
, Has (State (Set.Set Constraint)) sig m
|
||||
, Monad term
|
||||
, MonadFail m
|
||||
, Has Intro.Intro syn term
|
||||
)
|
||||
=> Algebra (Domain term Addr Type :+: sig) (DomainC term m) where
|
||||
alg (L (Abstract v k)) = case v of
|
||||
Intro.Unit -> k (Alg Unit)
|
||||
Intro.Bool _ -> k (Alg Bool)
|
||||
Intro.String _ -> k (Alg String)
|
||||
Intro.Lam (Named n b) -> do
|
||||
eval <- DomainC ask
|
||||
addr <- alloc @Name n
|
||||
arg <- meta
|
||||
A.assign addr arg
|
||||
ty <- lift (eval (instantiate1 (pure n) b))
|
||||
k (Alg (arg :-> ty))
|
||||
Intro.Record fields -> do
|
||||
eval <- DomainC ask
|
||||
fields' <- for fields $ \ (k, t) -> do
|
||||
addr <- alloc @Addr k
|
||||
v <- lift (eval t)
|
||||
(k, v) <$ A.assign addr v
|
||||
-- FIXME: should records reference types by address instead?
|
||||
k (Alg (Record (Map.fromList fields')))
|
||||
alg = \case
|
||||
L (Abstract v k) -> case v of
|
||||
Intro.Unit -> k (Alg Unit)
|
||||
Intro.Bool _ -> k (Alg Bool)
|
||||
Intro.String _ -> k (Alg String)
|
||||
Intro.Lam (Named n b) -> do
|
||||
eval <- DomainC ask
|
||||
addr <- alloc @Name n
|
||||
arg <- meta
|
||||
A.assign addr arg
|
||||
ty <- lift (eval (instantiate1 (pure n) b))
|
||||
k (Alg (arg :-> ty))
|
||||
Intro.Record fields -> do
|
||||
eval <- DomainC ask
|
||||
fields' <- for fields $ \ (k, t) -> do
|
||||
addr <- alloc @Addr k
|
||||
v <- lift (eval t)
|
||||
(k, v) <$ A.assign addr v
|
||||
-- FIXME: should records reference types by address instead?
|
||||
k (Alg (Record (Map.fromList fields')))
|
||||
|
||||
alg (L (Concretize t k)) = case t of
|
||||
Alg Unit -> k Intro.Unit
|
||||
Alg Bool -> k (Intro.Bool True) <|> k (Intro.Bool False)
|
||||
Alg String -> k (Intro.String mempty)
|
||||
Alg (_ :-> b) -> concretize @term b >>= k . Intro.Lam . Named (Name mempty) . lift . send
|
||||
Alg (Record t) -> traverse (traverse concretize) (Map.toList t) >>= k . Intro.Record . map (fmap send)
|
||||
t -> fail ("can’t concretize " <> show t)
|
||||
alg (R other) = DomainC (send (handleCoercible other))
|
||||
L (AsBool t k) -> do
|
||||
unify t (Alg Bool)
|
||||
k True <|> k False
|
||||
L (AsString t k) -> do
|
||||
unify t (Alg String)
|
||||
k mempty
|
||||
L (AsLam t k) -> do
|
||||
arg <- meta
|
||||
ret <- meta
|
||||
unify t (Alg (arg :-> ret))
|
||||
b <- concretize ret
|
||||
k (Named (Name mempty) (lift b)) where
|
||||
concretize = \case
|
||||
Alg Unit -> pure Intro.unit
|
||||
Alg Bool -> pure (Intro.bool True) <|> pure (Intro.bool False)
|
||||
Alg String -> pure (Intro.string mempty)
|
||||
Alg (_ :-> b) -> send . Intro.Lam . Named (Name mempty) . lift <$> concretize b
|
||||
Alg (Record t) -> Intro.record <$> traverse (traverse concretize) (Map.toList t)
|
||||
t -> fail $ "can’t concretize " <> show t -- FIXME: concretize type variables by incrementally solving constraints
|
||||
L (AsRecord t k) -> do
|
||||
unify t (Alg (Record mempty))
|
||||
k mempty -- FIXME: return whatever fields we have, when it’s actually a Record
|
||||
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
-- FIXME: we don’t get the chance to unify anything because concretization asks for an intro form, not an intro form of a specific type
|
||||
|
||||
Loading…
Reference in New Issue
Block a user