Skip to content
This repository has been archived by the owner on Apr 21, 2018. It is now read-only.

Commit

Permalink
Infer hole types.
Browse files Browse the repository at this point in the history
  • Loading branch information
@barrucadu
barrucadu committed May 6, 2017
1 parent 375cefd commit f17a11b
Show file tree
Hide file tree
Showing 8 changed files with 116 additions and 41 deletions.
7 changes: 4 additions & 3 deletions Test/CoCo/Discover.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ import Test.CoCo.TypeInfo (TypeInfo(..), getVariableBaseName)
import Test.CoCo.Util
import Test.CoCo.Logic
import Test.CoCo.Eval (runSingle)
import Test.CoCo.Sig (Sig(..))
import Test.CoCo.Sig (Sig(..), complete)

-- | Attempt to discover properties of the given set of concurrent
-- operations. Returns three sets of observations about, respectively:
Expand Down Expand Up @@ -124,8 +124,9 @@ discoverSingleWithSeeds' :: forall s t o x. (NFData o, NFData x, Ord o, Ord x)
-> Int
-> ST t (Generator s (ConcST t) (Maybe (Ann s (ConcST t) o x), Ann s (ConcST t) o x), [Observation])
discoverSingleWithSeeds' typeInfos seedPreds sig seeds lim =
let g = newGenerator'([(e, (Nothing, initialAnn False)) | e <- expressions sig] ++
[(e, (Nothing, initialAnn True)) | e <- backgroundExpressions sig])
let sigc = complete sig
g = newGenerator'([(e, (Nothing, initialAnn False)) | e <- expressions sigc] ++
[(e, (Nothing, initialAnn True)) | e <- backgroundExpressions sigc])
in second crun <$> findObservations g 0
where
-- check every term on the current tier for equality and
Expand Down
10 changes: 10 additions & 0 deletions Test/CoCo/Expr.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ module Test.CoCo.Expr
, ($$)
, bind
, hole
, holeOf
, let_
, lit
, commLit
Expand Down Expand Up @@ -299,6 +300,15 @@ bind is binder body = do
hole :: HasTypeRep s m a => proxy a -> Expr s m ()
hole p = Var (typeRep p) (Hole ())

-- | A typed hole (from a 'TypeRep'). If given the state type, this is
-- equivalent to 'stateVar'.
--
-- @exprSize (holeOf ty) == 1@
holeOf :: TypeRep s m -> Expr s m ()
holeOf ty
| ty == stateTypeRep = stateVar
| otherwise = Var ty (Hole ())

-- | Bind a value to a collection of holes, if well typed. The
-- numbering of unbound holes may be changed by this function.
--
Expand Down
24 changes: 23 additions & 1 deletion Test/CoCo/Sig.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@
-- Expression signatures for property discovery.
module Test.CoCo.Sig where

import Test.CoCo.Expr (Schema)
import Data.List (nub)

import Test.CoCo.Expr (Schema, holeOf, unLit)
import Test.CoCo.Type (TypeRep, dynTypeRep, funTys, stateTypeRep)

-- | A collection of expressions.
data Sig s m o x = Sig
Expand All @@ -31,3 +34,22 @@ data Sig s m o x = Sig
-- guaranteed to work, its purpose is to cause interference when
-- evaluating other terms.
}

-- | Complete a signature: add missing holes and the state variable to
-- the background.
complete :: Sig s m o x -> Sig s m o x
complete sig =
let holes = [ h
| h <- map holeOf (stateTypeRep : inferHoles sig)
, h `notElem` expressions sig
, h `notElem` backgroundExpressions sig
]
in sig { backgroundExpressions = holes ++ backgroundExpressions sig }

-- | Infer necessary hole types in a signature.
inferHoles :: Sig s m o x -> [TypeRep s m]
inferHoles sig = nub $ concatMap holesFor (expressions sig) ++ concatMap holesFor (backgroundExpressions sig) where
holesFor = maybe [] (funTyHoles . dynTypeRep . snd) . unLit
funTyHoles ty = case funTys ty of
Just (argTy, resultTy) -> argTy : funTyHoles resultTy
Nothing -> []
4 changes: 0 additions & 4 deletions examples/ComplexStack.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,6 @@ sigLS = Sig
-> Maybe Int
-> ConcST t ())
, commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ())
, hole (Proxy :: Proxy (Maybe Int))
, stateVar
]
, observation = toListLS
, backToSeed = toListLS
Expand Down Expand Up @@ -131,8 +129,6 @@ sigCAS = Sig
-> Maybe Int
-> ConcST t ())
, commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ())
, hole (Proxy :: Proxy (Maybe Int))
, stateVar
]
, observation = toListCAS
, backToSeed = toListCAS
Expand Down
96 changes: 72 additions & 24 deletions examples/ComplexStack.out
View file
Original file line number Diff line number Diff line change
@@ -1,28 +1,36 @@
dupLS @ =[= dupLS @ >> swapLS @
dupLS @ =[= (dupLS @) ||| (rotLS @)
dupLS @ =[= (dupLS @) ||| (swapLS @)
popLS @ =[= popLS @ >> rotLS @
popLS @ =[= (rotLS @) ||| (popLS @)
popLS @ =[= (swapLS @) ||| (popLS @)
overLS @ =[= (overLS @) ||| (rotLS @)
peekLS @ =[= dupLS @ >> popLS @
peekLS @ =[= swapLS @ >> swapLS @
peekLS @ =[= (dupLS @) ||| (popLS @)
peekLS @ =[= (swapLS @) ||| (swapLS @)
peekLS @ =[= popLS @ >>= \m -> whenJust pushLS @ m
dupLS @ =[= dupLS @ >> swapLS @
dupLS @ =[= (dupLS @) ||| (rotLS @)
dupLS @ =[= (dupLS @) ||| (swapLS @)
popLS @ =[= popLS @ >> rotLS @
popLS @ =[= (rotLS @) ||| (popLS @)
popLS @ =[= (swapLS @) ||| (popLS @)
overLS @ =[= (overLS @) ||| (rotLS @)
peekLS @ =[= dupLS @ >> popLS @
peekLS @ =[= swapLS @ >> swapLS @
peekLS @ =[= pushLS x @ >> popLS @
peekLS @ =[= (dupLS @) ||| (popLS @)
peekLS @ =[= (swapLS @) ||| (swapLS @)
peekLS @ =[= (popLS @) ||| (pushLS x @)
peekLS @ =[= popLS @ >>= \m -> whenJust pushLS @ m
pushLS x @ >> pushLS x @ =[= (dupLS @) ||| (pushLS x @)
(pushLS x @) ||| (pushLS x @) =[= (dupLS @) ||| (pushLS x @)

dupCAS @ =[= dupCAS @ >> swapCAS @
dupCAS @ =[= (dupCAS @) ||| (rotCAS @)
dupCAS @ =[= (dupCAS @) ||| (swapCAS @)
popCAS @ =[= popCAS @ >> rotCAS @
popCAS @ =[= (rotCAS @) ||| (popCAS @)
popCAS @ =[= (swapCAS @) ||| (popCAS @)
overCAS @ =[= (overCAS @) ||| (rotCAS @)
peekCAS @ =[= dupCAS @ >> popCAS @
peekCAS @ =[= swapCAS @ >> swapCAS @
peekCAS @ =[= (dupCAS @) ||| (popCAS @)
peekCAS @ =[= (swapCAS @) ||| (swapCAS @)
peekCAS @ =[= popCAS @ >>= \m -> whenJust pushCAS @ m
dupCAS @ =[= dupCAS @ >> swapCAS @
dupCAS @ =[= (dupCAS @) ||| (rotCAS @)
dupCAS @ =[= (dupCAS @) ||| (swapCAS @)
popCAS @ =[= popCAS @ >> rotCAS @
popCAS @ =[= (rotCAS @) ||| (popCAS @)
popCAS @ =[= (swapCAS @) ||| (popCAS @)
overCAS @ =[= (overCAS @) ||| (rotCAS @)
peekCAS @ =[= dupCAS @ >> popCAS @
peekCAS @ =[= swapCAS @ >> swapCAS @
peekCAS @ =[= pushCAS x @ >> popCAS @
peekCAS @ =[= (dupCAS @) ||| (popCAS @)
peekCAS @ =[= (swapCAS @) ||| (swapCAS @)
peekCAS @ =[= (popCAS @) ||| (pushCAS x @)
peekCAS @ =[= popCAS @ >>= \m -> whenJust pushCAS @ m
pushCAS x @ >> pushCAS x @ =[= (dupCAS @) ||| (pushCAS x @)
(pushCAS x @) ||| (pushCAS x @) =[= (dupCAS @) ||| (pushCAS x @)

dupLS @ === dupCAS @
popLS @ === popCAS @
Expand All @@ -39,7 +47,9 @@ peekCAS @ =[= popCAS @ >>= \m -> whenJust pushCAS @ m
peekCAS @ =[= swapLS @ >> swapLS @
peekCAS @ =[= (dupLS @) ||| (popLS @)
peekCAS @ =[= (swapLS @) ||| (swapLS @)
peekCAS @ =[= (popLS @) ||| (pushLS x @)
peekCAS @ =[= popLS @ >>= \m -> whenJust pushLS @ m
pushLS x @ === pushCAS x @
dupLS @ >> dupLS @ === dupCAS @ >> dupCAS @
dupLS @ >> dupLS @ === (dupCAS @) ||| (dupCAS @)
dupLS @ >> dupLS @ =[= (dupCAS @) ||| (overCAS @)
Expand Down Expand Up @@ -81,33 +91,71 @@ peekCAS @ =[= popCAS @ >>= \m -> whenJust pushCAS @ m
swapLS @ >> overLS @ === swapCAS @ >> overCAS @
swapLS @ >> overLS @ =[= (overCAS @) ||| (swapCAS @)
dupCAS @ >> overCAS @ =[= (dupLS @) ||| (overLS @)
dupLS @ >> pushLS x @ === dupCAS @ >> pushCAS x @
dupLS @ >> pushLS x @ =[= (dupCAS @) ||| (pushCAS x @)
overCAS @ >> dupCAS @ =[= (dupLS @) ||| (overLS @)
overCAS @ >> popCAS @ =[= (dupLS @) ||| (popLS @)
overCAS @ >> popCAS @ =[= (overLS @) ||| (popLS @)
overCAS @ >> rotCAS @ =[= (overLS @) ||| (rotLS @)
popCAS @ >> overCAS @ =[= (overLS @) ||| (popLS @)
popCAS @ >> swapCAS @ =[= (swapLS @) ||| (popLS @)
popLS @ >> pushLS x @ === popCAS @ >> pushCAS x @
pushLS x @ >> dupLS @ === pushCAS x @ >> dupCAS @
pushLS x @ >> dupLS @ =[= (dupCAS @) ||| (pushCAS x @)
pushLS x @ >> rotLS @ === pushCAS x @ >> rotCAS @
pushLS x @ >> rotLS @ =[= (rotCAS @) ||| (pushCAS x @)
rotCAS @ >> overCAS @ =[= (overLS @) ||| (rotLS @)
rotCAS @ >> swapCAS @ =[= (rotLS @) ||| (swapLS @)
rotLS @ >> pushLS x @ === rotCAS @ >> pushCAS x @
rotLS @ >> pushLS x @ =[= (rotCAS @) ||| (pushCAS x @)
swapCAS @ >> dupCAS @ =[= (dupLS @) ||| (swapLS @)
swapCAS @ >> popCAS @ =[= (swapLS @) ||| (popLS @)
swapCAS @ >> rotCAS @ =[= (rotLS @) ||| (swapLS @)
overCAS @ >> swapCAS @ =[= (overLS @) ||| (swapLS @)
overLS @ >> pushLS x @ === overCAS @ >> pushCAS x @
overLS @ >> pushLS x @ =[= (overCAS @) ||| (pushCAS x @)
pushLS x @ >> overLS @ === pushCAS x @ >> overCAS @
pushLS x @ >> overLS @ =[= (overCAS @) ||| (pushCAS x @)
pushLS x @ >> swapLS @ === pushCAS x @ >> swapCAS @
pushLS x @ >> swapLS @ =[= (swapCAS @) ||| (pushCAS x @)
swapCAS @ >> overCAS @ =[= (overLS @) ||| (swapLS @)
swapLS @ >> pushLS x @ === swapCAS @ >> pushCAS x @
swapLS @ >> pushLS x @ =[= (swapCAS @) ||| (pushCAS x @)
(dupLS @) ||| (dupLS @) === dupCAS @ >> dupCAS @
(dupLS @) ||| (dupLS @) === (dupCAS @) ||| (dupCAS @)
(dupLS @) ||| (dupLS @) =[= (dupCAS @) ||| (overCAS @)
(popLS @) ||| (popLS @) === popCAS @ >> popCAS @
(popLS @) ||| (popLS @) === (popCAS @) ||| (popCAS @)
(rotLS @) ||| (rotLS @) === rotCAS @ >> rotCAS @
(rotLS @) ||| (rotLS @) === (rotCAS @) ||| (rotCAS @)
dupCAS @ >> pushCAS x @ =[= (dupLS @) ||| (pushLS x @)
popCAS @ >> pushCAS x @ =[= (popLS @) ||| (pushLS x @)
pushCAS x @ >> dupCAS @ =[= (dupLS @) ||| (pushLS x @)
pushCAS x @ >> rotCAS @ =[= (rotLS @) ||| (pushLS x @)
rotCAS @ >> pushCAS x @ =[= (rotLS @) ||| (pushLS x @)
(dupLS @) ||| (overLS @) === (dupCAS @) ||| (overCAS @)
(overLS @) ||| (popLS @) === (overCAS @) ||| (popCAS @)
(rotLS @) ||| (swapLS @) === (rotCAS @) ||| (swapCAS @)
overCAS @ >> pushCAS x @ =[= (overLS @) ||| (pushLS x @)
pushCAS x @ >> overCAS @ =[= (overLS @) ||| (pushLS x @)
pushCAS x @ >> swapCAS @ =[= (swapLS @) ||| (pushLS x @)
pushLS x @ >> pushLS x @ =[= (dupCAS @) ||| (pushCAS x @)
pushLS x @ >> pushLS x @ === (pushCAS x @) ||| (pushCAS x @)
swapCAS @ >> pushCAS x @ =[= (swapLS @) ||| (pushLS x @)
(dupCAS @) ||| (dupCAS @) =[= (dupLS @) ||| (overLS @)
(overLS @) ||| (overLS @) === overCAS @ >> overCAS @
(overLS @) ||| (overLS @) === (overCAS @) ||| (overCAS @)
(overLS @) ||| (swapLS @) === (overCAS @) ||| (swapCAS @)
pushLS x @ >> pushLS x1 @ === pushCAS x @ >> pushCAS x1 @
pushLS x @ >> pushLS x1 @ =[= (pushCAS x @) ||| (pushCAS x1 @)
(dupLS @) ||| (pushLS x @) === (dupCAS @) ||| (pushCAS x @)
(rotLS @) ||| (pushLS x @) === (rotCAS @) ||| (pushCAS x @)
(overLS @) ||| (pushLS x @) === (overCAS @) ||| (pushCAS x @)
(swapLS @) ||| (pushLS x @) === (swapCAS @) ||| (pushCAS x @)
pushCAS x @ >> pushCAS x1 @ =[= (pushLS x @) ||| (pushLS x1 @)
(pushLS x @) ||| (pushLS x @) === pushCAS x @ >> pushCAS x @
(pushLS x @) ||| (pushLS x @) =[= (dupCAS @) ||| (pushCAS x @)
(pushLS x @) ||| (pushLS x1 @) === (pushCAS x @) ||| (pushCAS x1 @)
dupLS @ >> whenJust pushLS @ m === dupCAS @ >> whenJust pushCAS @ m
dupLS @ >> whenJust pushLS @ m =[= (dupCAS @) ||| (whenJust pushCAS @ m)
popLS @ >> whenJust pushLS @ m === popCAS @ >> whenJust pushCAS @ m
Expand Down
5 changes: 1 addition & 4 deletions examples/MVar.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,7 @@ sig = Sig
, lit "readMVar" (readMVar :: MVar (ConcST t) Int -> ConcST t Int)
]
, backgroundExpressions =
[ commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ())
, hole (Proxy :: Proxy Int)
, stateVar
]
[ commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ()) ]
, observation = tryTakeMVar
, backToSeed = tryTakeMVar
, setState = \v mi -> tryTakeMVar v >> maybe (pure ()) (void . tryPutMVar v) mi
Expand Down
5 changes: 0 additions & 5 deletions examples/Stack.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,6 @@ sigLS = Sig
-> Maybe Int
-> ConcST t ())
, commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ())
, hole (Proxy :: Proxy Int)
, hole (Proxy :: Proxy (Maybe Int))
, stateVar
]
, observation = toListLS
, backToSeed = toListLS
Expand Down Expand Up @@ -89,8 +86,6 @@ sigCAS = Sig
-> Maybe Int
-> ConcST t ())
, commLit "|||" ((|||) :: ConcST t Ignore -> ConcST t Ignore -> ConcST t ())
, hole (Proxy :: Proxy (Maybe Int))
, stateVar
]
, observation = toListCAS
, backToSeed = toListCAS
Expand Down
6 changes: 6 additions & 0 deletions examples/Stack.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,23 @@
push2LS x1 x @ =[= pushLS x @ >> pushLS x @
push2LS x1 x @ =[= (pushLS x @) ||| (pushLS x @)

peekCAS @ =[= pushCAS x @ >> popCAS @
peekCAS @ =[= (popCAS @) ||| (pushCAS x @)
peekCAS @ =[= popCAS @ >>= \m -> whenJust pushCAS @ m

popLS @ === popCAS @
peekLS @ === peekCAS @
peekCAS @ =[= (popLS @) ||| (pushLS x @)
peekCAS @ =[= popLS @ >>= \m -> whenJust pushLS @ m
pushLS x @ === pushCAS x @
pushCAS x1 @ =[= push2LS x x1 @ >> popLS @
popLS @ >> popLS @ === popCAS @ >> popCAS @
popLS @ >> popLS @ === (popCAS @) ||| (popCAS @)
whenJust pushLS @ m === whenJust pushCAS @ m
popLS @ >> pushLS x @ === popCAS @ >> pushCAS x @
(popLS @) ||| (popLS @) === popCAS @ >> popCAS @
(popLS @) ||| (popLS @) === (popCAS @) ||| (popCAS @)
popCAS @ >> pushCAS x @ =[= (popLS @) ||| (pushLS x @)
popLS @ >> whenJust pushLS @ m === popCAS @ >> whenJust pushCAS @ m
popLS @ >> whenJust pushLS @ m =[= (popCAS @) ||| (whenJust pushCAS @ m)
whenJust pushLS @ m >> popLS @ === whenJust pushCAS @ m >> popCAS @
Expand Down

0 comments on commit f17a11b

Please sign in to comment.