mirror of
https://github.com/github/semantic.git
synced 2024-12-22 06:11:49 +03:00
Express Evaluatable as an R-algebra.
Co-Authored-By: Josh Vera <vera@github.com>
This commit is contained in:
parent
ca21d42399
commit
a99f97854d
@ -14,7 +14,6 @@ import Data.Abstract.Value
|
||||
import Data.Abstract.FreeVariables
|
||||
import Data.Blob
|
||||
import Data.Traversable
|
||||
import Data.Function (fix)
|
||||
import Data.Functor.Foldable (Base, Recursive(..))
|
||||
import Data.Foldable (toList)
|
||||
import Data.Semigroup
|
||||
@ -53,7 +52,7 @@ require term = do
|
||||
where
|
||||
evalModule linker name = case linkerLookupTerm name linker of
|
||||
Just m -> do
|
||||
v <- step @v m
|
||||
v <- para eval m
|
||||
modify @(Linker term v) (linkerInsert name v)
|
||||
trace ("require[eval]:" <> name) (pure v)
|
||||
_ -> fail ("cannot find " <> show name)
|
||||
@ -67,7 +66,7 @@ evaluate :: forall v term.
|
||||
)
|
||||
=> term
|
||||
-> Final (Evaluating term v) v
|
||||
evaluate = run @(Evaluating term v) . fix (const step)
|
||||
evaluate = run @(Evaluating term v) . para eval
|
||||
|
||||
-- | Evaluate terms and an entry point to a value.
|
||||
evaluates :: forall v term.
|
||||
@ -79,11 +78,10 @@ evaluates :: forall v term.
|
||||
=> [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
|
||||
-> (Blob, term) -- Entrypoint
|
||||
-> Final (Evaluating term v) v
|
||||
evaluates pairs = run @(Evaluating term v) . fix go
|
||||
evaluates pairs (Blob{..}, t) = run @(Evaluating term v) $ do
|
||||
put (Linker @term @v Map.empty (Map.fromList (fmap toPathActionPair pairs)))
|
||||
trace ("step[entryPoint]: " <> show blobPath) (para eval t)
|
||||
where
|
||||
go _ (Blob{..}, t) = do
|
||||
put (Linker @term @v Map.empty (Map.fromList (fmap toPathActionPair pairs)))
|
||||
trace ("step[entryPoint]: " <> show blobPath) (step @v t)
|
||||
toPathActionPair (Blob{..}, t) = (dropExtensions blobPath, t)
|
||||
|
||||
|
||||
@ -120,7 +118,7 @@ evaluate' :: forall v term.
|
||||
)
|
||||
=> term
|
||||
-> Final (Evaluating' v) v
|
||||
evaluate' = run @(Evaluating' v) . fix (const step)
|
||||
evaluate' = run @(Evaluating' v) . para eval
|
||||
|
||||
-- | Evaluate terms and an entry point to a value.
|
||||
evaluates' :: forall v term.
|
||||
@ -132,14 +130,11 @@ evaluates' :: forall v term.
|
||||
=> [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
|
||||
-> (Blob, term) -- Entrypoint
|
||||
-> Final (Evaluating' v) v
|
||||
evaluates' pairs = run @(Evaluating' v) . fix go
|
||||
where
|
||||
go _ (Blob{..}, t) = do
|
||||
modules <- for pairs $ \(Blob{..}, t) -> do
|
||||
v <- trace ("step: " <> show blobPath) $ step @v t
|
||||
pure (dropExtensions blobPath, v)
|
||||
local (const (Linker' (Map.fromList modules))) (trace ("step: " <> show blobPath) (step @v t))
|
||||
|
||||
evaluates' pairs (Blob{..}, t) = run @(Evaluating' v) $ do
|
||||
modules <- for pairs $ \(Blob{..}, t) -> do
|
||||
v <- trace ("step: " <> show blobPath) $ para eval t
|
||||
pure (dropExtensions blobPath, v :: v)
|
||||
local (const (Linker' (Map.fromList modules))) (trace ("step: " <> show blobPath) (para eval t))
|
||||
|
||||
-- | The effects necessary for concrete interpretation.
|
||||
--
|
||||
@ -175,7 +170,7 @@ evaluate'' :: forall v term.
|
||||
)
|
||||
=> term
|
||||
-> Final (Evaluating'' v) v
|
||||
evaluate'' = run @(Evaluating'' v) . fix (const step)
|
||||
evaluate'' = run @(Evaluating'' v) . para eval
|
||||
|
||||
-- | Evaluate terms and an entry point to a value.
|
||||
evaluates'' :: forall v term.
|
||||
@ -187,10 +182,9 @@ evaluates'' :: forall v term.
|
||||
=> [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
|
||||
-> (Blob, term) -- Entrypoint
|
||||
-> Final (Evaluating'' v) v
|
||||
evaluates'' pairs = run @(Evaluating'' v) . fix go
|
||||
evaluates'' pairs (Blob{..}, t) = run @(Evaluating'' v) $ local @(Linker' (Evaluator v)) (const (Linker' (Map.fromList (map toPathActionPair pairs)))) (trace ("step: " <> show blobPath) (para eval t))
|
||||
where
|
||||
go _ (Blob{..}, t) = local (const (Linker' (Map.fromList (map toPathActionPair pairs)))) (trace ("step: " <> show blobPath) (step @v t))
|
||||
toPathActionPair (Blob{..}, t) = (dropExtensions blobPath, Evaluator (step @v t))
|
||||
toPathActionPair (Blob{..}, t) = (dropExtensions blobPath, Evaluator (para eval t))
|
||||
|
||||
|
||||
-- | The effects necessary for concrete interpretation.
|
||||
|
@ -25,8 +25,8 @@ import qualified Data.Union as U
|
||||
|
||||
-- | The 'Evaluatable' class defines the necessary interface for a term to be evaluated. While a default definition of 'eval' is given, instances with computational content must implement 'eval' to perform their small-step operational semantics.
|
||||
class Evaluatable es term v constr where
|
||||
eval :: constr term -> Eff es v
|
||||
default eval :: (Fail :< es, Show1 constr) => (constr term -> Eff es v)
|
||||
eval :: constr (term, Eff es v) -> Eff es v
|
||||
default eval :: (Fail :< es, Show1 constr) => (constr (term, Eff es v) -> Eff es v)
|
||||
eval expr = fail $ "Eval unspecialized for " ++ liftShowsPrec (const (const id)) (const id) 0 expr ""
|
||||
|
||||
-- | If we can evaluate any syntax which can occur in a 'Union', we can evaluate the 'Union'.
|
||||
@ -38,9 +38,9 @@ instance (Evaluatable es t v s) => Evaluatable es t v (TermF s a) where
|
||||
eval In{..} = eval termFOut
|
||||
|
||||
-- | Evaluate by first projecting a term to recurse one level.
|
||||
step :: forall v term es. (Evaluatable es term v (Base term), Recursive term)
|
||||
=> term -> Eff es v
|
||||
step = eval . project
|
||||
step :: Recursive term
|
||||
=> (term, Eff es v) -> Eff es v
|
||||
step = snd
|
||||
|
||||
|
||||
-- Instances
|
||||
@ -60,10 +60,10 @@ instance ( Ord (LocationFor v)
|
||||
, Recursive t
|
||||
)
|
||||
=> Evaluatable es t v [] where
|
||||
eval [] = pure unit -- Return unit value if this is an empty list of terms
|
||||
eval [x] = step x -- Return the value for the last term
|
||||
eval (x:xs) = do
|
||||
_ <- step @v x -- Evaluate the head term
|
||||
eval [] = pure unit -- Return unit value if this is an empty list of terms
|
||||
eval [(_, x)] = x -- Return the value for the last term
|
||||
eval ((_, x):xs) = do
|
||||
_ <- x -- Evaluate the head term
|
||||
env <- get @(EnvironmentFor v) -- Get the global environment after evaluation
|
||||
-- since it might have been modified by the
|
||||
-- 'step' evaluation above ^.
|
||||
@ -71,4 +71,4 @@ instance ( Ord (LocationFor v)
|
||||
-- Finally, evaluate the rest of the terms, but do so by calculating a new
|
||||
-- environment each time where the free variables in those terms are bound
|
||||
-- to the global environment.
|
||||
local (const (bindEnv (freeVariables1 xs) env)) (eval xs)
|
||||
local (const (bindEnv (liftFreeVariables (freeVariables . fst) xs) env)) (eval xs)
|
||||
|
@ -163,9 +163,9 @@ instance ( Ord (LocationFor (Value l t))
|
||||
interface val = inj . Value.Interface val <$> ask @(EnvironmentFor (Value l t))
|
||||
|
||||
eval' [] = interface unit
|
||||
eval' [x] = step x >>= interface
|
||||
eval' (x:xs) = do
|
||||
_ <- step @(Value l t) x
|
||||
eval' [(_, x)] = x >>= interface
|
||||
eval' ((_, x):xs) = do
|
||||
_ <- x
|
||||
env <- get @(EnvironmentFor (Value l t))
|
||||
local (envUnion env) (eval' xs)
|
||||
|
||||
|
@ -48,10 +48,10 @@ instance ( FreeVariables t
|
||||
) => Evaluatable es t (Value l t) Function where
|
||||
eval Function{..} = do
|
||||
env <- ask
|
||||
let params = toList (freeVariables1 functionParameters)
|
||||
let v = inj (Closure params functionBody env) :: Value l t
|
||||
let params = toList (liftFreeVariables (freeVariables . fst) functionParameters)
|
||||
let v = inj (Closure params (fst functionBody) env) :: Value l t
|
||||
|
||||
(name, addr) <- lookupOrAlloc functionName v env
|
||||
(name, addr) <- lookupOrAlloc (fst functionName) v env
|
||||
modify (envInsert name addr)
|
||||
pure v
|
||||
|
||||
@ -104,10 +104,10 @@ instance ( FreeVariables t -- To get free variables from the func
|
||||
) => Evaluatable es t (Value l t) Method where
|
||||
eval Method{..} = do
|
||||
env <- ask
|
||||
let params = toList (freeVariables1 methodParameters)
|
||||
let v = inj (Closure params methodBody env) :: Value l t
|
||||
let params = toList (liftFreeVariables (freeVariables . fst) methodParameters)
|
||||
let v = inj (Closure params (fst methodBody) env) :: Value l t
|
||||
|
||||
(name, addr) <- lookupOrAlloc methodName v env
|
||||
(name, addr) <- lookupOrAlloc (fst methodName) v env
|
||||
modify (envInsert name addr)
|
||||
pure v
|
||||
|
||||
@ -286,7 +286,7 @@ instance ( Show l
|
||||
, FreeVariables t
|
||||
)
|
||||
=> Evaluatable es t (Value l t) Import where
|
||||
eval (Import from _ _) = do
|
||||
eval (Import (from, _) _ _) = do
|
||||
interface <- require @(Value l t) @t from
|
||||
-- TODO: Consider returning the value instead of the interface.
|
||||
Interface _ env <- maybe
|
||||
|
@ -43,7 +43,7 @@ instance ( Ord l
|
||||
, Recursive t
|
||||
) => Evaluatable es t (Value l t) Call where
|
||||
eval Call{..} = do
|
||||
closure <- step @(Value l t) callFunction
|
||||
closure <- step callFunction
|
||||
Closure names body env <- maybe (fail "expected a closure") pure (prj closure :: Maybe (Closure l t))
|
||||
bindings <- for (zip names callParams) $ \(name, param) -> do
|
||||
v <- step param
|
||||
@ -51,7 +51,7 @@ instance ( Ord l
|
||||
assign a v
|
||||
pure (name, a)
|
||||
|
||||
local (const (foldr (uncurry envInsert) env bindings)) (step body)
|
||||
local (const (foldr (uncurry envInsert) env bindings)) (para eval body)
|
||||
|
||||
-- TODO: Implement type checking for Call
|
||||
instance Member Fail es => Evaluatable es t Type.Type Call
|
||||
|
@ -114,7 +114,7 @@ instance ( Semigroup (Cell (LocationFor v) v)
|
||||
=> Evaluatable es t v Assignment where
|
||||
eval Assignment{..} = do
|
||||
v <- step assignmentValue
|
||||
(var, a) <- ask >>= lookupOrAlloc assignmentTarget v
|
||||
(var, a) <- ask >>= lookupOrAlloc (fst assignmentTarget) v
|
||||
|
||||
modify (envInsert var a)
|
||||
pure v
|
||||
|
Loading…
Reference in New Issue
Block a user