mirror of
https://github.com/github/semantic.git
synced 2025-01-03 21:16:12 +03:00
Let the other interpreters infer location from value
This commit is contained in:
parent
53d4a41cff
commit
4a60f0cd59
@ -83,26 +83,26 @@ instance (NonDetEff :< fs) => MonadNonDet (Eff fs) where
|
||||
-- Coinductively-cached evaluation
|
||||
--
|
||||
-- Examples:
|
||||
-- Files.readFile "test.py" (Just Python) >>= runTask . parse pythonParser2 >>= pure . evalCache @Monovariant @Type
|
||||
-- Files.readFile "test.py" (Just Python) >>= runTask . parse pythonParser2 >>= pure . evalCache @Precise @(Value (Data.Union.Union Language.Python.Assignment2.Syntax) (Record Location) Precise)
|
||||
evalCache :: forall l v syntax ann
|
||||
-- evalCache @Type <term>
|
||||
-- evalCache @(Value (Data.Union.Union Language.Python.Assignment2.Syntax) (Record Location) Precise) <term>
|
||||
evalCache :: forall v syntax ann
|
||||
. ( Ord v
|
||||
, Ord l
|
||||
, Ord (LocationFor v)
|
||||
, Ord ann
|
||||
, Ord1 (Cell l)
|
||||
, Ord1 (Cell (LocationFor v))
|
||||
, Ord1 syntax
|
||||
, Foldable (Cell l)
|
||||
, Foldable (Cell (LocationFor v))
|
||||
, FreeVariables1 syntax
|
||||
, Functor syntax
|
||||
, MonadAddress l (Eff (CachingInterpreter l (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (CachingInterpreter l (Term syntax ann) v))
|
||||
, Semigroup (Cell l v)
|
||||
, AbstractValue l v
|
||||
, Eval v (Eff (CachingInterpreter l (Term syntax ann) v)) syntax
|
||||
, MonadAddress (LocationFor v) (Eff (CachingInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (CachingInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, AbstractValue (LocationFor v) v
|
||||
, Eval v (Eff (CachingInterpreter (LocationFor v) (Term syntax ann) v)) syntax
|
||||
)
|
||||
=> Term syntax ann
|
||||
-> CachingResult l (Term syntax ann) v
|
||||
evalCache e = run @(CachingInterpreter l (Term syntax ann) v) (fixCache @l (fix (evCache @l (evCollect @l (evRoots @l)))) pure e)
|
||||
-> CachingResult (LocationFor v) (Term syntax ann) v
|
||||
evalCache e = run @(CachingInterpreter (LocationFor v) (Term syntax ann) v) (fixCache @(LocationFor v) (fix (evCache @(LocationFor v) (evCollect @(LocationFor v) (evRoots @(LocationFor v))))) pure e)
|
||||
|
||||
|
||||
evCache :: forall l t v m
|
||||
|
@ -6,6 +6,7 @@ import Abstract.FreeVariables
|
||||
import Abstract.Interpreter
|
||||
import Abstract.Primitive
|
||||
import Abstract.Store
|
||||
import Abstract.Value
|
||||
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect hiding (run)
|
||||
@ -42,9 +43,11 @@ subterms term = para (foldMap (uncurry ((<>) . point))) term <> point term
|
||||
|
||||
|
||||
-- Dead code analysis
|
||||
--
|
||||
-- Example:
|
||||
-- evalDead @Precise @(Value Syntax Precise) @Syntax (if' true (Abstract.Syntax.int 1) (Abstract.Syntax.int 2))
|
||||
evalDead :: forall l v syntax ann
|
||||
-- evalDead @(Value Syntax Precise) <term>
|
||||
|
||||
evalDead :: forall v syntax ann
|
||||
. ( Ord v
|
||||
, Ord ann
|
||||
, Ord1 syntax
|
||||
@ -52,14 +55,14 @@ evalDead :: forall l v syntax ann
|
||||
, Foldable syntax
|
||||
, FreeVariables1 syntax
|
||||
, Functor syntax
|
||||
, Eval v (Eff (DeadCodeInterpreter l (Term syntax ann) v)) syntax
|
||||
, MonadAddress l (Eff (DeadCodeInterpreter l (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (DeadCodeInterpreter l (Term syntax ann) v))
|
||||
, Semigroup (Cell l v)
|
||||
, Eval v (Eff (DeadCodeInterpreter (LocationFor v) (Term syntax ann) v)) syntax
|
||||
, MonadAddress (LocationFor v) (Eff (DeadCodeInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (DeadCodeInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
)
|
||||
=> Term syntax ann
|
||||
-> DeadCodeResult l (Term syntax ann) v
|
||||
evalDead e0 = run @(DeadCodeInterpreter l (Term syntax ann) v) $ do
|
||||
-> DeadCodeResult (LocationFor v) (Term syntax ann) v
|
||||
evalDead e0 = run @(DeadCodeInterpreter (LocationFor v) (Term syntax ann) v) $ do
|
||||
killAll (Dead (subterms e0))
|
||||
fix (evDead ev) pure e0
|
||||
|
||||
|
@ -8,6 +8,7 @@ import Abstract.FreeVariables
|
||||
import Abstract.Interpreter
|
||||
import Abstract.Primitive
|
||||
import Abstract.Store
|
||||
import Abstract.Value
|
||||
|
||||
import Control.Effect
|
||||
import Control.Monad.Effect hiding (run)
|
||||
@ -35,44 +36,43 @@ instance (Writer (g (Configuration l t v)) :< fs) => MonadTrace l t v g (Eff fs)
|
||||
-- Tracing and reachable state analyses
|
||||
--
|
||||
-- Examples
|
||||
-- evalTrace @Precise @(Value Syntax Precise) @Syntax (makeLam "x" (var "x") # true)
|
||||
-- evalReach @Precise @(Value Syntax Precise) @Syntax (makeLam "x" (var "x") # true)
|
||||
-- evalTrace @(Value Syntax Precise) <term>
|
||||
-- evalReach @(Value Syntax Precise) <term>
|
||||
|
||||
evalTrace :: forall l v syntax ann
|
||||
. ( Ord v, Ord ann, Ord1 syntax, Ord1 (Cell l)
|
||||
evalTrace :: forall v syntax ann
|
||||
. ( Ord v, Ord ann, Ord1 syntax, Ord1 (Cell (LocationFor v))
|
||||
, FreeVariables1 syntax
|
||||
, Functor syntax
|
||||
, MonadAddress l (Eff (TraceInterpreter l (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (TraceInterpreter l (Term syntax ann) v))
|
||||
, MonadGC l v (Eff (TraceInterpreter l (Term syntax ann) v))
|
||||
, Semigroup (Cell l v)
|
||||
, Eval v (Eff (TraceInterpreter l (Term syntax ann) v)) syntax
|
||||
, MonadAddress (LocationFor v) (Eff (TraceInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (TraceInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadGC (LocationFor v) v (Eff (TraceInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, Eval v (Eff (TraceInterpreter (LocationFor v) (Term syntax ann) v)) syntax
|
||||
)
|
||||
=> Term syntax ann -> Final (TracingInterpreter l (Term syntax ann) v []) v
|
||||
evalTrace = run @(TraceInterpreter l (Term syntax ann) v) . fix (evTell @l @(Term syntax ann) @v @[] ev) pure
|
||||
=> Term syntax ann -> Final (TracingInterpreter (LocationFor v) (Term syntax ann) v []) v
|
||||
evalTrace = run @(TraceInterpreter (LocationFor v) (Term syntax ann) v) . fix (evTell @[] ev) pure
|
||||
|
||||
evalReach :: forall l v syntax ann
|
||||
. ( Ord v, Ord ann, Ord l, Ord1 (Cell l), Ord1 syntax
|
||||
evalReach :: forall v syntax ann
|
||||
. ( Ord v, Ord ann, Ord (LocationFor v), Ord1 (Cell (LocationFor v)), Ord1 syntax
|
||||
, FreeVariables1 syntax
|
||||
, Functor syntax
|
||||
, MonadAddress l (Eff (ReachableStateInterpreter l (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (ReachableStateInterpreter l (Term syntax ann) v))
|
||||
, MonadGC l v (Eff (ReachableStateInterpreter l (Term syntax ann) v))
|
||||
, Semigroup (Cell l v)
|
||||
, Eval v (Eff (ReachableStateInterpreter l (Term syntax ann) v)) syntax
|
||||
, MonadAddress (LocationFor v) (Eff (ReachableStateInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadPrim v (Eff (ReachableStateInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, MonadGC (LocationFor v) v (Eff (ReachableStateInterpreter (LocationFor v) (Term syntax ann) v))
|
||||
, Semigroup (Cell (LocationFor v) v)
|
||||
, Eval v (Eff (ReachableStateInterpreter (LocationFor v) (Term syntax ann) v)) syntax
|
||||
)
|
||||
=> Term syntax ann -> Final (TracingInterpreter l (Term syntax ann) v Set.Set) v
|
||||
evalReach = run @(ReachableStateInterpreter l (Term syntax ann) v) . fix (evTell @l @(Term syntax ann) @v @Set.Set ev) pure
|
||||
=> Term syntax ann -> Final (TracingInterpreter (LocationFor v) (Term syntax ann) v Set.Set) v
|
||||
evalReach = run @(ReachableStateInterpreter (LocationFor v) (Term syntax ann) v) . fix (evTell @Set.Set ev) pure
|
||||
|
||||
|
||||
evTell :: forall l t v g m
|
||||
. ( Ord l
|
||||
, IsList (g (Configuration l t v))
|
||||
, Item (g (Configuration l t v)) ~ Configuration l t v
|
||||
, MonadTrace l t v g m
|
||||
, MonadEnv l v m
|
||||
, MonadStore l v m
|
||||
, MonadGC l v m
|
||||
evTell :: forall g t m v
|
||||
. ( IsList (g (Configuration (LocationFor v) t v))
|
||||
, Item (g (Configuration (LocationFor v) t v)) ~ Configuration (LocationFor v) t v
|
||||
, MonadTrace (LocationFor v) t v g m
|
||||
, MonadEnv (LocationFor v) v m
|
||||
, MonadStore (LocationFor v) v m
|
||||
, MonadGC (LocationFor v) v m
|
||||
)
|
||||
=> (Eval' t m v -> Eval' t m v)
|
||||
-> Eval' t m v
|
||||
@ -81,5 +81,5 @@ evTell ev0 ev' yield e = do
|
||||
env <- askEnv
|
||||
store <- getStore
|
||||
roots <- askRoots
|
||||
trace (fromList [Configuration e (Set.toList roots) env store] :: g (Configuration l t v))
|
||||
trace (fromList [Configuration e (Set.toList roots) env store] :: g (Configuration (LocationFor v) t v))
|
||||
ev0 ev' yield e
|
||||
|
Loading…
Reference in New Issue
Block a user