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

Merge pull request #1961 from github/circumvent-the-occurs-check

Browse Source 
Circumvent the occurs check
This commit is contained in:
Rob Rix 2018-06-13 16:59:12 -04:00 committed by GitHub
commit 57126e7101
9 changed files with 140 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

43
src/Control/Abstract/Evaluator.hs
View File

@ -1,4 +1,4 @@
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, RankNTypes, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
{-# LANGUAGE GADTs, GeneralizedNewtypeDeriving, RankNTypes, ScopedTypeVariables, TypeOperators #-}
module Control.Abstract.Evaluator
( Evaluator(..)
-- * Effects
@ -37,49 +37,46 @@ deriving instance Member NonDet effects => Alternative (Evaluator address value
-- Effects
-- | An effect for explicitly returning out of a function/method body.
data Return address value resume where
Return :: address -> Return address value address
data Return address resume where
Return :: address -> Return address address
deriving instance (Eq address, Eq value) => Eq (Return address value a)
deriving instance (Show address, Eq value) => Show (Return address value a)
deriving instance Eq address => Eq (Return address a)
deriving instance Show address => Show (Return address a)
earlyReturn :: forall address value effects
. Member (Return address value) effects
earlyReturn :: Member (Return address) effects
=> address
-> Evaluator address value effects address
earlyReturn = send . Return @address @value
earlyReturn = send . Return
catchReturn :: Member (Return address value) effects => Evaluator address value effects a -> (forall x . Return address value x -> Evaluator address value effects a) -> Evaluator address value effects a
catchReturn :: Member (Return address) effects => Evaluator address value effects a -> (forall x . Return address x -> Evaluator address value effects a) -> Evaluator address value effects a
catchReturn action handler = interpose pure (\ ret _ -> handler ret) action
runReturn :: Effectful (m address value) => m address value (Return address value ': effects) address -> m address value effects address
runReturn :: Effectful (m address value) => m address value (Return address ': effects) address -> m address value effects address
runReturn = raiseHandler (relay pure (\ (Return value) _ -> pure value))
-- | Effects for control flow around loops (breaking and continuing).
data LoopControl address value resume where
Break :: address -> LoopControl address value address
Continue :: address -> LoopControl address value address
data LoopControl address resume where
Break :: address -> LoopControl address address
Continue :: address -> LoopControl address address
deriving instance (Eq address, Eq value) => Eq (LoopControl address value a)
deriving instance (Show address, Show value) => Show (LoopControl address value a)
deriving instance Eq address => Eq (LoopControl address a)
deriving instance Show address => Show (LoopControl address a)
throwBreak :: forall address value effects
. Member (LoopControl address value) effects
throwBreak :: Member (LoopControl address) effects
=> address
-> Evaluator address value effects address
throwBreak = send . Break @address @value
throwBreak = send . Break
throwContinue :: forall address value effects
. Member (LoopControl address value) effects
throwContinue :: Member (LoopControl address) effects
=> address
-> Evaluator address value effects address
throwContinue = send . Continue @address @value
throwContinue = send . Continue
catchLoopControl :: Member (LoopControl address value) effects => Evaluator address value effects a -> (forall x . LoopControl address value x -> Evaluator address value effects a) -> Evaluator address value effects a
catchLoopControl :: Member (LoopControl address) effects => Evaluator address value effects a -> (forall x . LoopControl address x -> Evaluator address value effects a) -> Evaluator address value effects a
catchLoopControl action handler = interpose pure (\ control _ -> handler control) action
runLoopControl :: Effectful (m address value) => m address value (LoopControl address value ': effects) address -> m address value effects address
runLoopControl :: Effectful (m address value) => m address value (LoopControl address ': effects) address -> m address value effects address
runLoopControl = raiseHandler (relay pure (\ eff _ -> case eff of
Break value -> pure value
Continue value -> pure value))

6
src/Data/Abstract/Evaluatable.hs
View File

@ -46,7 +46,7 @@ class Show1 constr => Evaluatable constr where
, FreeVariables term
, Member (Allocator address value) effects
, Member (Env address) effects
, Member (LoopControl address value) effects
, Member (LoopControl address) effects
, Member (Modules address value) effects
, Member (Reader ModuleInfo) effects
, Member (Reader PackageInfo) effects
@ -55,7 +55,7 @@ class Show1 constr => Evaluatable constr where
, Member (Resumable EvalError) effects
, Member (Resumable ResolutionError) effects
, Member (Resumable (Unspecialized value)) effects
, Member (Return address value) effects
, Member (Return address) effects
, Member Trace effects
)
=> SubtermAlgebra constr term (Evaluator address value effects (ValueRef address))
@ -84,7 +84,7 @@ evaluatePackageWith :: forall address term value inner inner' inner'' outer
, Recursive term
, Reducer value (Cell address value)
, ValueRoots address value
, inner ~ (LoopControl address value ': Return address value ': Env address ': Allocator address value ': inner')
, inner ~ (LoopControl address ': Return address ': Env address ': Allocator address value ': inner')
, inner' ~ (Reader ModuleInfo ': inner'')
, inner'' ~ (Modules address value ': Reader Span ': Reader PackageInfo ': outer)
)

4
src/Data/Abstract/Type.hs
View File

@ -119,7 +119,7 @@ instance ( Member (Allocator address Type) effects
, Member (Env address) effects
, Member Fresh effects
, Member (Resumable TypeError) effects
, Member (Return address Type) effects
, Member (Return address) effects
)
=> AbstractFunction address Type effects where
closure names _ body = do
@ -146,7 +146,7 @@ instance ( Member (Allocator address Type) effects
, Member Fresh effects
, Member NonDet effects
, Member (Resumable TypeError) effects
, Member (Return address Type) effects
, Member (Return address) effects
)
=> AbstractValue address Type effects where
array fields = do

6
src/Data/Abstract/Value.hs
View File

@ -60,7 +60,7 @@ instance ( Coercible body (Eff effects)
, Member (Reader ModuleInfo) effects
, Member (Reader PackageInfo) effects
, Member (Resumable (ValueError address body)) effects
, Member (Return address (Value address body)) effects
, Member (Return address) effects
, Show address
)
=> AbstractFunction address (Value address body) effects where
@ -105,11 +105,11 @@ instance ( Coercible body (Eff effects)
, Member (Allocator address (Value address body)) effects
, Member (Env address) effects
, Member Fresh effects
, Member (LoopControl address (Value address body)) effects
, Member (LoopControl address) effects
, Member (Reader ModuleInfo) effects
, Member (Reader PackageInfo) effects
, Member (Resumable (ValueError address body)) effects
, Member (Return address (Value address body)) effects
, Member (Return address) effects
, Show address
)
=> AbstractValue address (Value address body) effects where

28
src/Semantic/Graph.hs
View File

@ -4,6 +4,7 @@ module Semantic.Graph
, GraphType(..)
, Graph
, Vertex
, GraphEff(..)
, style
, parsePackage
, withTermSpans
@ -64,9 +65,34 @@ runGraph graphType includePackages project
. resumingResolutionError
. resumingAddressError
. resumingValueError
. runTermEvaluator @_ @_ @(Value (Hole (Located Precise)) (Eff _))
. runTermEvaluator @_ @_ @(Value (Hole (Located Precise)) (GraphEff _))
. graphing
-- | The full list of effects in flight during the evaluation of terms. This, and other @newtype@s like it, are necessary to type 'Value', since the bodies of closures embed evaluators. This would otherwise require cycles in the effect list (i.e. references to @effects@ within @effects@ itself), which the typechecker forbids.
newtype GraphEff address a = GraphEff
{ runGraphEff :: Eff '[ LoopControl address
, Return address
, Env address
, Allocator address (Value address (GraphEff address))
, Reader ModuleInfo
, Modules address (Value address (GraphEff address))
, Reader Span
, Reader PackageInfo
, State (Graph Vertex)
, Resumable (ValueError address (GraphEff address))
, Resumable (AddressError address (Value address (GraphEff address)))
, Resumable ResolutionError
, Resumable EvalError
, Resumable (EnvironmentError address)
, Resumable (Unspecialized (Value address (GraphEff address)))
, Resumable (LoadError address (Value address (GraphEff address)))
, Trace
, Fresh
, State (Heap address Latest (Value address (GraphEff address)))
, State (ModuleTable (Maybe (address, Environment address)))
] a
}
-- | Parse a list of files into a 'Package'.
parsePackage :: (Member (Distribute WrappedTask) effs, Member Files effs, Member Resolution effs, Member Task effs, Member Trace effs)
=> Parser term -- ^ A parser.

26
src/Semantic/Util.hs
View File

@ -44,9 +44,33 @@ justEvaluating
. runEnvironmentError
. runEvalError
. runAddressError
. runTermEvaluator @_ @Precise @(Value Precise (Eff _))
. runTermEvaluator @_ @Precise @(Value Precise (UtilEff _))
. runValueError
newtype UtilEff address a = UtilEff
{ runUtilEff :: Eff '[ LoopControl address
, Return address
, Env address
, Allocator address (Value address (UtilEff address))
, Reader ModuleInfo
, Modules address (Value address (UtilEff address))
, Reader Span
, Reader PackageInfo
, Resumable (ValueError address (UtilEff address))
, Resumable (AddressError address (Value address (UtilEff address)))
, Resumable EvalError
, Resumable (EnvironmentError address)
, Resumable ResolutionError
, Resumable (Unspecialized (Value address (UtilEff address)))
, Resumable (LoadError address (Value address (UtilEff address)))
, Trace
, Fresh
, State (Heap address Latest (Value address (UtilEff address)))
, State (ModuleTable (Maybe (address, Environment address)))
, IO
] a
}
checking
= runM @_ @IO
. evaluating

21
test/Control/Abstract/Evaluator/Spec.hs
View File

@ -1,6 +1,7 @@
{-# LANGUAGE TypeOperators #-}
module Control.Abstract.Evaluator.Spec
( spec
, SpecEff(..)
) where
import Analysis.Abstract.Evaluating (evaluating)
@ -30,7 +31,7 @@ spec = parallel $ do
evaluate
= runM
. evaluating @Precise @(Value Precise (Eff _))
. evaluating @Precise @Val
. runReader (PackageInfo (name "test") Nothing mempty)
. runReader (ModuleInfo "test/Control/Abstract/Evaluator/Spec.hs")
. fmap reassociate
@ -45,3 +46,21 @@ evaluate
reassociate :: Either (SomeExc exc1) (Either (SomeExc exc2) (Either (SomeExc exc3) result)) -> Either (SomeExc (Sum '[exc3, exc2, exc1])) result
reassociate = mergeExcs . mergeExcs . mergeExcs . Right
type Val = Value Precise SpecEff
newtype SpecEff a = SpecEff
{ runSpecEff :: Eff '[ LoopControl Precise
, Return Precise
, Env Precise
, Allocator Precise Val
, Resumable (AddressError Precise Val)
, Resumable (EnvironmentError Precise)
, Resumable (ValueError Precise SpecEff)
, Reader ModuleInfo
, Reader PackageInfo
, Fresh
, State (Heap Precise Latest Val)
, State (ModuleTable (Maybe (Precise, Environment Precise)))
, IO
] a
}

53
test/SpecHelpers.hs
View File

@ -9,6 +9,7 @@ module SpecHelpers
, derefQName
, verbatim
, TermEvaluator(..)
, TestEff(..)
, Verbatim(..)
) where
@ -79,15 +80,15 @@ readFilePair paths = let paths' = fmap file paths in
runBothWith IO.readFilePair paths'
testEvaluating :: TermEvaluator term Precise
(Value Precise (Eff effects))
'[ Resumable (ValueError Precise (Eff effects))
, Resumable (AddressError Precise (Value Precise (Eff effects)))
Val
'[ Resumable (ValueError Precise TestEff)
, Resumable (AddressError Precise Val)
, Resumable EvalError, Resumable (EnvironmentError Precise)
, Resumable ResolutionError
, Resumable (Unspecialized (Value Precise (Eff effects)))
, Resumable (LoadError Precise (Value Precise (Eff effects)))
, Resumable (Unspecialized Val)
, Resumable (LoadError Precise Val)
, Fresh
, State (Heap Precise Latest (Value Precise (Eff effects)))
, State (Heap Precise Latest Val)
, State (ModuleTable (Maybe (Precise, Environment Precise)))
, Trace
]
@ -95,16 +96,16 @@ testEvaluating :: TermEvaluator term Precise
-> ((Either
(SomeExc
(Data.Sum.Sum
'[ ValueError Precise (Eff effects)
, AddressError Precise (Value Precise (Eff effects))
'[ ValueError Precise TestEff
, AddressError Precise Val
, EvalError
, EnvironmentError Precise
, ResolutionError
, Unspecialized (Value Precise (Eff effects))
, LoadError Precise (Value Precise (Eff effects))
, Unspecialized Val
, LoadError Precise Val
]))
[(Value Precise (Eff effects), Environment Precise)],
EvaluatingState Precise (Value Precise (Eff effects))),
[(Value Precise TestEff, Environment Precise)],
EvaluatingState Precise Val),
[String])
testEvaluating
= run
@ -118,8 +119,32 @@ testEvaluating
. runEvalError
. runAddressError
. runValueError
. (>>= (traverse deref1))
. runTermEvaluator @_ @_ @(Value Precise (Eff _))
. (>>= traverse deref1)
. runTermEvaluator @_ @_ @Val
type Val = Value Precise TestEff
newtype TestEff a = TestEff
{ runTestEff :: Eff '[ LoopControl Precise
, Return Precise
, Env Precise
, Allocator Precise Val
, Reader ModuleInfo
, Modules Precise Val
, Reader Span
, Reader PackageInfo
, Resumable (ValueError Precise TestEff)
, Resumable (AddressError Precise Val)
, Resumable EvalError
, Resumable (EnvironmentError Precise)
, Resumable ResolutionError
, Resumable (Unspecialized Val)
, Resumable (LoadError Precise Val)
, Fresh
, State (Heap Precise Latest Val)
, State (ModuleTable (Maybe (Precise, Environment Precise)))
, Trace
] a
}
deref1 (ptr, env) = runAllocator $ do
val <- deref ptr

2
vendor/effects vendored

@ -1 +1 @@
Subproject commit adec65af304cc31681ce02111985aa73e1f11cf5
Subproject commit 5db3a4f18ee8a2bf97762a9846b76ca21383126e