mirror of
https://github.com/github/semantic.git
synced 2024-11-24 00:42:33 +03:00
Split Domain into multiple effects.
This commit is contained in:
Rob Rix
parent
661227365a
commit
c07324ff90
@ -123,23 +123,23 @@ instance ( Applicative term
|
||||
)
|
||||
=> Algebra (A.Domain term Addr (Concrete term) :+: sig) (DomainC term m) where
|
||||
alg = \case
|
||||
L (A.Unit k) -> k Unit
|
||||
L (A.Bool b k) -> k (Bool b)
|
||||
L (A.AsBool c k) -> case c of
|
||||
L (L (A.Unit k)) -> k Unit
|
||||
L (R (L (A.Bool b k))) -> k (Bool b)
|
||||
L (R (L (A.AsBool c k))) -> case c of
|
||||
Bool b -> k b
|
||||
_ -> fail "expected Bool"
|
||||
L (A.String s k) -> k (String s)
|
||||
L (A.AsString c k) -> case c of
|
||||
L (R (R (L (A.String s k)))) -> k (String s)
|
||||
L (R (R (L (A.AsString c k)))) -> case c of
|
||||
String s -> k s
|
||||
_ -> fail "expected String"
|
||||
L (A.Lam b k) -> do
|
||||
L (R (R (R (L (A.Lam b k))))) -> do
|
||||
path <- ask
|
||||
span <- ask
|
||||
k (Closure path span b)
|
||||
L (A.AsLam c k) -> case c of
|
||||
L (R (R (R (L (A.AsLam c k))))) -> case c of
|
||||
Closure _ _ b -> k b
|
||||
_ -> fail "expected Closure"
|
||||
L (A.Record fields k) -> do
|
||||
L (R (R (R (R (A.Record fields k))))) -> do
|
||||
eval <- DomainC ask
|
||||
fields' <- for fields $ \ (name, t) -> do
|
||||
addr <- A.alloc name
|
||||
@ -147,7 +147,7 @@ instance ( Applicative term
|
||||
A.assign @Addr @(Concrete term) addr v
|
||||
pure (name, addr)
|
||||
k (Record (Map.fromList fields'))
|
||||
L (A.AsRecord c k) -> case c of
|
||||
L (R (R (R (R (A.AsRecord c k))))) -> case c of
|
||||
Record fields -> k (map (fmap pure) (Map.toList fields))
|
||||
_ -> fail "expected Record"
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
@ -1,78 +1,111 @@
|
||||
{-# LANGUAGE AllowAmbiguousTypes #-}
|
||||
{-# LANGUAGE DeriveFunctor #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE QuantifiedConstraints #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
module Analysis.Effect.Domain
|
||||
( -- * Domain effect
|
||||
unit
|
||||
, UnitDomain(..)
|
||||
, bool
|
||||
, asBool
|
||||
, BoolDomain(..)
|
||||
, string
|
||||
, asString
|
||||
, StringDomain(..)
|
||||
, lam
|
||||
, asLam
|
||||
, FunctionDomain(..)
|
||||
, record
|
||||
, asRecord
|
||||
, Domain(..)
|
||||
, RecordDomain(..)
|
||||
, Domain
|
||||
-- * Re-exports
|
||||
, Algebra
|
||||
, Has
|
||||
, run
|
||||
) where
|
||||
|
||||
import Analysis.Name
|
||||
import Control.Algebra
|
||||
import Data.Text (Text)
|
||||
import GHC.Generics (Generic1)
|
||||
import Syntax.Scope (Scope)
|
||||
import Analysis.Name
|
||||
import Control.Algebra
|
||||
import Data.Text (Text)
|
||||
import GHC.Generics (Generic1)
|
||||
import Syntax.Scope (Scope)
|
||||
|
||||
unit :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => m abstract
|
||||
unit = send (Unit @term @addr pure)
|
||||
unit :: Has (UnitDomain abstract) sig m => m abstract
|
||||
unit = send (Unit pure)
|
||||
|
||||
bool :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => Bool -> m abstract
|
||||
bool b = send (Bool @term @addr b pure)
|
||||
data UnitDomain abstract m k
|
||||
= Unit (abstract -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
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 s = send (String @term @addr s pure)
|
||||
|
||||
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)
|
||||
instance HFunctor (UnitDomain abstract)
|
||||
instance Effect (UnitDomain abstract)
|
||||
|
||||
|
||||
lam :: Has (Domain term addr abstract) sig m => Named (Scope () term addr) -> m abstract
|
||||
bool :: Has (BoolDomain abstract) sig m => Bool -> m abstract
|
||||
bool b = send (Bool b pure)
|
||||
|
||||
asBool :: Has (BoolDomain abstract) sig m => abstract -> m Bool
|
||||
asBool v = send (AsBool v pure)
|
||||
|
||||
data BoolDomain abstract m k
|
||||
= Bool Bool (abstract -> m k)
|
||||
| AsBool abstract (Bool -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
instance HFunctor (BoolDomain abstract)
|
||||
instance Effect (BoolDomain abstract)
|
||||
|
||||
|
||||
string :: Has (StringDomain abstract) sig m => Text -> m abstract
|
||||
string s = send (String s pure)
|
||||
|
||||
asString :: Has (StringDomain abstract) sig m => abstract -> m Text
|
||||
asString v = send (AsString v pure)
|
||||
|
||||
data StringDomain abstract m k
|
||||
= String Text (abstract -> m k)
|
||||
| AsString abstract (Text -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
instance HFunctor (StringDomain abstract)
|
||||
instance Effect (StringDomain abstract)
|
||||
|
||||
|
||||
lam :: Has (FunctionDomain term addr abstract) sig m => Named (Scope () term addr) -> m abstract
|
||||
lam b = send (Lam b pure)
|
||||
|
||||
-- FIXME: Support partial concretization of lambdas.
|
||||
asLam :: Has (Domain term addr abstract) sig m => abstract -> m (Named (Scope () term addr))
|
||||
asLam :: Has (FunctionDomain term addr abstract) sig m => abstract -> m (Named (Scope () term addr))
|
||||
asLam v = send (AsLam v pure)
|
||||
|
||||
data FunctionDomain term addr abstract m k
|
||||
= Lam (Named (Scope () term addr)) (abstract -> m k)
|
||||
| AsLam abstract (Named (Scope () term addr) -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
record :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => [(Name, term addr)] -> m abstract
|
||||
instance HFunctor (FunctionDomain term addr abstract)
|
||||
instance Effect (FunctionDomain term addr abstract)
|
||||
|
||||
|
||||
record :: Has (RecordDomain term addr abstract) sig m => [(Name, term addr)] -> m abstract
|
||||
record fs = send (Record fs pure)
|
||||
|
||||
-- FIXME: Support partial concretization of records.
|
||||
asRecord :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => abstract -> m [(Name, term addr)]
|
||||
asRecord :: Has (RecordDomain term addr abstract) sig m => abstract -> m [(Name, term addr)]
|
||||
asRecord v = send (AsRecord v pure)
|
||||
|
||||
|
||||
data Domain term addr abstract m k
|
||||
= Unit (abstract -> m k)
|
||||
| Bool Bool (abstract -> m k)
|
||||
| AsBool abstract (Bool -> m k)
|
||||
| String Text (abstract -> m k)
|
||||
| AsString abstract (Text -> m k)
|
||||
| Lam (Named (Scope () term addr)) (abstract -> m k)
|
||||
| AsLam abstract (Named (Scope () term addr) -> m k)
|
||||
| Record [(Name, term addr)] (abstract -> m k)
|
||||
| AsRecord abstract ([(Name, term addr)] -> m k)
|
||||
data RecordDomain term addr abstract m k
|
||||
= Record [(Name, term addr)] (abstract -> m k)
|
||||
| AsRecord abstract ([(Name, term addr)] -> m k)
|
||||
deriving (Functor, Generic1)
|
||||
|
||||
instance HFunctor (Domain term addr abstract)
|
||||
instance Effect (Domain term addr abstract)
|
||||
instance HFunctor (RecordDomain term addr abstract)
|
||||
instance Effect (RecordDomain term addr abstract)
|
||||
|
||||
|
||||
type Domain term addr abstract
|
||||
= UnitDomain abstract
|
||||
:+: BoolDomain abstract
|
||||
:+: StringDomain abstract
|
||||
:+: FunctionDomain term addr abstract
|
||||
:+: RecordDomain term addr abstract
|
||||
|
||||
@ -125,25 +125,25 @@ instance MonadTrans (DomainC term) where
|
||||
-- FIXME: decompose into a product domain and two atomic domains
|
||||
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.Unit k) -> k mempty
|
||||
L (A.Bool _ k) -> k mempty
|
||||
L (A.AsBool _ k) -> k True <|> k False
|
||||
L (A.String s k) -> k (Value (String s) mempty)
|
||||
L (A.AsString _ k) -> k mempty
|
||||
L (A.Lam b k) -> do
|
||||
L (L (A.Unit k)) -> k mempty
|
||||
L (R (L (A.Bool _ k))) -> k mempty
|
||||
L (R (L (A.AsBool _ k))) -> k True <|> k False
|
||||
L (R (R (L (A.String s k)))) -> k (Value (String s) mempty)
|
||||
L (R (R (L (A.AsString _ k)))) -> k mempty
|
||||
L (R (R (R (L (A.Lam b k))))) -> do
|
||||
path <- ask
|
||||
span <- ask
|
||||
k (Value (Closure path span b) mempty)
|
||||
L (A.AsLam (Value v _) k) -> case v of
|
||||
L (R (R (R (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.Record f k) -> do
|
||||
L (R (R (R (R (A.Record f k))))) -> do
|
||||
eval <- DomainC ask
|
||||
fields <- for f $ \ (k, t) -> do
|
||||
addr <- alloc @Addr k
|
||||
v <- lift (eval t)
|
||||
v <$ A.assign @Addr @(Value (Semi term)) addr v
|
||||
k (fold fields)
|
||||
L (A.AsRecord _ k) -> k []
|
||||
L (R (R (R (R (A.AsRecord _ k))))) -> k []
|
||||
R other -> DomainC (send (handleCoercible other))
|
||||
|
||||
@ -230,23 +230,23 @@ instance ( Alternative m
|
||||
)
|
||||
=> Algebra (A.Domain term Addr Type :+: sig) (DomainC term m) where
|
||||
alg = \case
|
||||
L (A.Unit k) -> k (Alg Unit)
|
||||
L (A.Bool _ k) -> k (Alg Bool)
|
||||
L (A.AsBool t k) -> do
|
||||
L (L (A.Unit k)) -> k (Alg Unit)
|
||||
L (R (L (A.Bool _ k))) -> k (Alg Bool)
|
||||
L (R (L (A.AsBool t k))) -> do
|
||||
unify t (Alg Bool)
|
||||
k True <|> k False
|
||||
L (A.String _ k) -> k (Alg String)
|
||||
L (A.AsString t k) -> do
|
||||
L (R (R (L (A.String _ k)))) -> k (Alg String)
|
||||
L (R (R (L (A.AsString t k)))) -> do
|
||||
unify t (Alg String)
|
||||
k mempty
|
||||
L (A.Lam (Named n b) k) -> do
|
||||
L (R (R (R (L (A.Lam (Named n b) k))))) -> 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))
|
||||
L (A.AsLam t k) -> do
|
||||
L (R (R (R (L (A.AsLam t k))))) -> do
|
||||
arg <- meta
|
||||
ret <- meta
|
||||
unify t (Alg (arg :-> ret))
|
||||
@ -259,7 +259,7 @@ instance ( Alternative m
|
||||
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 (A.Record fields k) -> do
|
||||
L (R (R (R (R (A.Record fields k))))) -> do
|
||||
eval <- DomainC ask
|
||||
fields' <- for fields $ \ (k, t) -> do
|
||||
addr <- alloc @Addr k
|
||||
@ -267,7 +267,7 @@ instance ( Alternative m
|
||||
(k, v) <$ A.assign addr v
|
||||
-- FIXME: should records reference types by address instead?
|
||||
k (Alg (Record (Map.fromList fields')))
|
||||
L (A.AsRecord t k) -> do
|
||||
L (R (R (R (R (A.AsRecord t k))))) -> do
|
||||
unify t (Alg (Record mempty))
|
||||
k mempty -- FIXME: return whatever fields we have, when it’s actually a Record
|
||||
|
||||
|
||||
@ -74,19 +74,19 @@ eval eval = \case
|
||||
A.assign addr a'
|
||||
A.bind n addr (eval (instantiate1 (pure addr) b))
|
||||
If c t e -> do
|
||||
c' <- eval c >>= A.asBool @Term @address
|
||||
c' <- eval c >>= A.asBool
|
||||
if c' then eval t else eval e
|
||||
Load p -> eval p >>= A.asString @Term @address >> A.unit @Term @address -- FIXME: add a load command or something
|
||||
Unit -> A.unit @Term @address
|
||||
Bool b -> A.bool @Term @address b
|
||||
String s -> A.string @Term @address s
|
||||
Load p -> eval p >>= A.asString >> A.unit -- FIXME: add a load command or something
|
||||
Unit -> A.unit
|
||||
Bool b -> A.bool b
|
||||
String s -> A.string s
|
||||
Record fields -> A.record fields
|
||||
a :. b -> do
|
||||
a' <- eval a >>= A.asRecord @Term @address
|
||||
a' <- eval a >>= A.asRecord
|
||||
maybe (freeVariable (show b)) eval (lookup b a')
|
||||
a :? b -> do
|
||||
a' <- eval a >>= A.asRecord @Term @address
|
||||
A.bool @Term @address (isJust (lookup b a'))
|
||||
A.bool (isJust (lookup b a'))
|
||||
|
||||
a := b -> do
|
||||
b' <- eval b
|
||||
@ -103,10 +103,10 @@ eval eval = \case
|
||||
Term.Var n -> pure n
|
||||
Term.Alg (R c) -> case c of
|
||||
If c t e -> do
|
||||
c' <- eval c >>= A.asBool @Term @address
|
||||
c' <- eval c >>= A.asBool
|
||||
if c' then ref t else ref e
|
||||
a :. b -> do
|
||||
a' <- eval a >>= A.asRecord @Term @address
|
||||
a' <- eval a >>= A.asRecord
|
||||
maybe (freeVariable (show b)) ref (lookup b a')
|
||||
c -> invalidRef (show c)
|
||||
Term.Alg (L (Ann span c)) -> local (const span) (ref c)
|
||||
|
||||
Loading…
Reference in New Issue
Block a user