github/semantic
1
1
Fork 0
mirror of https://github.com/github/semantic.git synced 2024-12-25 16:02:43 +03:00
Code Issues Projects Releases Wiki Activity

Parameterize terms by addresses.

Browse Source
This commit is contained in:
Rob Rix 2019-12-19 11:52:05 -05:00
parent 1bc3c65efe
commit e546950f29
No known key found for this signature in database
GPG Key ID: F188A01508EA1CF7
3 changed files with 36 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
semantic-analysis/src/Analysis/Effect/Domain.hs
View File

@ -27,49 +27,49 @@ import Data.Text (Text)
import GHC.Generics (Generic1)
import Syntax.Scope (Scope)
abstract :: Has (Domain term abstract) sig m => Intro term Name -> m abstract
abstract :: Has (Domain term addr abstract) sig m => Intro term addr -> m abstract
abstract concrete = send (Abstract concrete pure)
concretize :: Has (Domain term abstract) sig m => abstract -> m (Intro term Name)
concretize :: Has (Domain term addr abstract) sig m => abstract -> m (Intro term addr)
concretize abstract = send (Concretize abstract pure)
unit :: forall term abstract m sig . Has (Domain term abstract) sig m => m abstract
unit = abstract @term A.Unit
unit :: forall term addr abstract m sig . Has (Domain term addr abstract) sig m => m abstract
unit = abstract @term @addr A.Unit
bool :: forall term abstract m sig . Has (Domain term abstract) sig m => Bool -> m abstract
bool = abstract @term . A.Bool
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 abstract m sig . (Has (Domain term abstract) sig m, MonadFail m, forall a . Show a => Show (term a)) => abstract -> m Bool
asBool = concretize @term >=> \case
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
string :: forall term abstract m sig . Has (Domain term abstract) sig m => Text -> m abstract
string = abstract @term . A.String
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 abstract m sig . (Has (Domain term abstract) sig m, MonadFail m, forall a . Show a => Show (term a)) => abstract -> m Text
asString = concretize @term >=> \case
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
lam :: Has (Domain term abstract) sig m => Named (Scope () term Name) -> m abstract
lam :: Has (Domain term addr abstract) sig m => Named (Scope () term addr) -> m abstract
lam = abstract . A.Lam
asLam :: (Has (Domain term abstract) sig m, MonadFail m, forall a . Show a => Show (term a)) => abstract -> m (Named (Scope () term Name))
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
data Domain term abstract m k
= Abstract (Intro term Name) (abstract -> m k)
| Concretize abstract (Intro term Name -> m k)
data Domain term addr abstract m k
= Abstract (Intro term addr) (abstract -> m k)
| Concretize abstract (Intro term addr -> m k)
deriving (Functor, Generic1)
instance HFunctor (Domain term abstract)
instance Effect (Domain term abstract)
instance HFunctor (Domain term addr abstract)
instance Effect (Domain term addr abstract)
typeError :: (Show a, MonadFail m) => String -> a -> m b

2
semantic-analysis/src/Analysis/Typecheck.hs
View File

@ -243,7 +243,7 @@ instance ( Alternative m
, Monad term
, MonadFail m
, Has Intro.Intro syn term
) => Algebra (Domain term Type :+: sig) (DomainC term m) where
) => Algebra (Domain term Name Type :+: sig) (DomainC term m) where
alg (L (Abstract v k)) = case v of
Intro.Unit -> k (Alg Unit)
Intro.Bool _ -> k (Alg Bool)

32
semantic-core/src/Core/Eval.hs
View File

@ -34,22 +34,23 @@ import qualified System.Path as Path
type Term = Term.Term (Ann Span :+: Core :+: Intro)
eval :: forall address value m sig
. ( Has (Domain Term value) sig m
. ( Has (Domain Term address value) sig m
, Has (Env address) sig m
, Has (Heap address value) sig m
, Has (Reader Span) sig m
, MonadFail m
, Semigroup value
, Show address
)
=> Analysis address value m
-> (Term Name -> m value)
-> (Term Name -> m value)
-> (Term address -> m value)
-> (Term address -> m value)
eval Analysis{..} eval = \case
Term.Var n -> lookupEnv' n >>= deref' n
Term.Var n -> deref' n n
Term.Alg (R (L c)) -> case c of
Rec (Named n b) -> do
addr <- A.alloc @address n
v <- A.bind n addr (eval (instantiate1 (pure n) b))
v <- A.bind n addr (eval (instantiate1 (pure addr) b))
v <$ A.assign addr v
-- NB: Combining the results of the evaluations allows us to model effects in abstract domains. This in turn means that we can define an abstract domain modelling the types-and-effects of computations by means of a 'Semigroup' instance which takes the type of its second operand and the union of both operands’ effects.
--
@ -59,18 +60,18 @@ eval Analysis{..} eval = \case
a' <- eval a
addr <- A.alloc @address n
A.assign addr a'
A.bind n addr ((a' <>) <$> eval (instantiate1 (pure n) b))
A.bind n addr ((a' <>) <$> eval (instantiate1 (pure addr) b))
Lam (Named n b) -> A.lam (Named n b)
f :$ a -> do
Named n b <- eval f >>= asLam
a' <- eval a
addr <- A.alloc @address n
A.assign addr a'
A.bind n addr (eval (instantiate1 (pure n) b))
A.bind n addr (eval (instantiate1 (pure addr) b))
If c t e -> do
c' <- eval c >>= A.asBool @Term
c' <- eval c >>= A.asBool @Term @address
if c' then eval t else eval e
Load p -> eval p >>= A.asString @Term >> A.unit @Term -- FIXME: add a load command or something
Load p -> eval p >>= A.asString @Term @address >> A.unit @Term @address -- FIXME: add a load command or something
Record fields -> traverse (traverse eval) fields >>= record
a :. b -> do
a' <- ref a
@ -78,29 +79,28 @@ eval Analysis{..} eval = \case
a :? b -> do
a' <- ref a
mFound <- a' ... b
A.bool @Term (isJust mFound)
A.bool @Term @address (isJust mFound)
a := b -> do
b' <- eval b
addr <- ref a
b' <$ A.assign addr b'
Term.Alg (R (R c)) -> case c of
Unit -> A.unit @Term
Bool b -> A.bool @Term b
String s -> A.string @Term s
Unit -> A.unit @Term @address
Bool b -> A.bool @Term @address b
String s -> A.string @Term @address s
Term.Alg (L (Ann span c)) -> local (const span) (eval c)
where freeVariable s = fail ("free variable: " <> s)
uninitialized s = fail ("uninitialized variable: " <> s)
invalidRef s = fail ("invalid ref: " <> s)
lookupEnv' n = A.lookupEnv n >>= maybe (freeVariable (show n)) pure
deref' n = A.deref @address >=> maybe (uninitialized (show n)) pure
ref = \case
Term.Var n -> lookupEnv' n
Term.Var n -> pure n
Term.Alg (R (L c)) -> case c of
If c t e -> do
c' <- eval c >>= A.asBool @Term
c' <- eval c >>= A.asBool @Term @address
if c' then ref t else ref e
a :. b -> do
a' <- ref a