Commit c1e59648 authored by Sven Keidel's avatar Sven Keidel

get PCF stratego case study running

parent 95fae671
......@@ -36,7 +36,6 @@ import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Profunctor
#define TRACE
#ifdef TRACE
import Debug.Trace
import Text.Printf
......@@ -80,7 +79,7 @@ instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c) => ArrowFi
-- If we are in a loop, return the cached value or bottom otherwise.
-- Furthermore, add x' to the current component.
(addToComponent &&> initializeCache)
(lmap snd $ addToComponent &&> initializeCache)
#else
......@@ -103,7 +102,10 @@ instance (Identifiable a, LowerBounded b, Profunctor c,ArrowChoice c) => ArrowFi
-- If we are in a loop, return the cached value or bottom otherwise.
-- Furthermore, add x' to the current component.
(addToComponent &&> initializeCache)
(proc (x,x') -> do
c <- askConst -< ()
y <- addToComponent &&> initializeCache -< x'
returnA -< trace (printf "loop [%s] = %s" (printDom c (x,x')) (printCod c y)) y)
#endif
instance (ArrowJoin c, ArrowChoice c) => ArrowJoin (FixT s a b c) where
......@@ -133,13 +135,13 @@ instance (Arrow c, Profunctor c) => ArrowDeduplicate x y (FixT s a b c) where
dedup f = f
----- Helper functions -----
stackWiden' :: (ArrowReader (s a) c,ArrowChoice c) => ConstT (Constant s a b) c (a,a) b -> ConstT (Constant s a b) c a b -> ConstT (Constant s a b) c a b
stackWiden' :: (ArrowReader (s a) c,ArrowChoice c) => ConstT (Constant s a b) c (a,a) b -> ConstT (Constant s a b) c (a,a) b -> ConstT (Constant s a b) c a b
stackWiden' (ConstT (StaticT f)) (ConstT (StaticT g)) =
constT $ \c ->
rmap (\(s,x) -> let ~(s',(l,x')) = stackWidening c s x
in case l of
NoLoop -> Left (s',(x,x'))
Loop -> Right x'
Loop -> Right (x,x')
) (const ask &&& id)
>>>
(local (f c) ||| g c)
......
......@@ -31,6 +31,7 @@ import Control.Category
import Data.Profunctor
import Data.Order hiding (lub)
import Data.Monoidal
import Data.Coerce
-- Due to "Generalising Monads to Arrows", by John Hughes, in Science of Computer Programming 37.
newtype ReaderT r c x y = ReaderT { runReaderT :: c (r,x) y }
......@@ -43,8 +44,8 @@ instance (Profunctor c, Arrow c) => Profunctor (ReaderT r c) where
instance ArrowTrans (ReaderT r) where
type Dom (ReaderT r) x y = (r,x)
type Cod (ReaderT r) x y = y
lift = ReaderT
unlift = runReaderT
lift = coerce
unlift = coerce
instance ArrowLift (ReaderT r) where
lift' f = lift $ lmap snd f
......
......@@ -34,6 +34,7 @@ import Data.Hashable
import Data.Order hiding (lub)
import Data.Monoidal
import Data.Profunctor
import Data.Coerce
-- Due to "Generalising Monads to Arrows", by John Hughes, in Science of Computer Programming 37.
newtype StateT s c x y = StateT { runStateT :: c (s,x) (s,y) }
......@@ -52,8 +53,8 @@ instance (Profunctor c, Arrow c) => Profunctor (StateT s c) where
instance ArrowTrans (StateT s) where
type Dom (StateT s) x y = (s,x)
type Cod (StateT s) x y = (s,y)
lift = StateT
unlift = runStateT
lift = coerce
unlift = coerce
instance ArrowLift (StateT s) where
lift' f = lift (second f)
......
......@@ -28,6 +28,7 @@ import Control.Arrow.Abstract.Join
import Data.Profunctor
import Data.Monoidal
import Data.Order hiding (lub)
import Data.Coerce
newtype WriterT w c x y = WriterT { runWriterT :: c x (w,y) }
......@@ -39,8 +40,8 @@ instance (Profunctor c, Arrow c) => Profunctor (WriterT w c) where
instance ArrowTrans (WriterT w) where
type Dom (WriterT w) x y = x
type Cod (WriterT w) x y = (w,y)
lift = WriterT
unlift = runWriterT
lift = coerce
unlift = coerce
instance Monoid w => ArrowLift (WriterT w) where
lift' f = lift (rmap (\y -> (mempty,y)) f)
......@@ -67,7 +68,7 @@ instance (Monoid w, ArrowChoice c, Profunctor c) => ArrowChoice (WriterT w c) wh
f +++ g = lift $ rmap distribute2 (unlift f +++ unlift g)
instance (Monoid w, ArrowApply c, Profunctor c) => ArrowApply (WriterT w c) where
app = lift $ lmap (first runWriterT) app
app = lift $ lmap (first unlift) app
instance (Monoid w, ArrowState s c) => ArrowState s (WriterT w c) where
get = lift' get
......
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Arrows #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Abstract.Except where
import Prelude hiding (id,(.))
......@@ -24,6 +26,7 @@ import Data.Abstract.FreeCompletion (FreeCompletion(..))
import Data.Abstract.Widening
import GHC.Generics (Generic, Generic1)
import GHC.TypeLits
-- | Abstrat domain for exceptions. This abstract domain approximates
-- error more precisely because 'Success ⋢ Fail'. Use this type for
......@@ -77,6 +80,9 @@ instance (PreOrd e, PreOrd a, Complete (FreeCompletion e), Complete (FreeComplet
instance (UpperBounded e, UpperBounded a) => UpperBounded (Except e a) where
top = SuccessOrFail top top
instance (TypeError ('Text "Except does not have a lower bound. You probably want to use bottom of Data.Abstract.Terminating"), PreOrd a, PreOrd e) => LowerBounded (Except e a) where
bottom = error "do not implement"
instance (PreOrd a, PreOrd e, UpperBounded (FreeCompletion e), UpperBounded (FreeCompletion a))
=> UpperBounded (FreeCompletion (Except e a)) where
top = case (top,top) of
......@@ -121,9 +127,6 @@ instance (Complete e, ArrowJoin c, ArrowChoice c, Profunctor c) => ArrowMonad (E
SuccessOrFail e' y -> SuccessOrFail (e e') y
lub _ _ = error "cannot happen"
instance PreOrd a => LowerBounded (Except () a) where
bottom = Fail ()
instance Foldable (Except e) where
foldMap = foldMapDefault
......
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
module Data.Abstract.Maybe where
import Prelude hiding (Maybe(..))
import qualified Prelude as Con
import Control.DeepSeq
import Control.Monad(ap)
import Control.Arrow(second)
......@@ -10,9 +16,13 @@ import Data.Hashable
import Data.Traversable
import Data.Abstract.Widening
import GHC.Generics(Generic)
-- | Abstract 'Maybe' type with an upper bound for 'Just' and 'Nothing'
data Maybe a = Just a | Nothing | JustNothing a
deriving (Eq,Ord,Show)
deriving (Eq,Ord,Show,Generic)
instance NFData a => NFData (Maybe a)
instance (Hashable a) => Hashable (Maybe a) where
hashWithSalt s (Just a) = s `hashWithSalt` (1::Int) `hashWithSalt` a
......@@ -79,3 +89,8 @@ instance Traversable Maybe where
traverse _ Nothing = pure Nothing
traverse f (Just a) = Just <$> f a
traverse f (JustNothing a) = JustNothing <$> f a
fromConcreteMaybe :: Con.Maybe a -> Maybe a
fromConcreteMaybe m = case m of
Con.Just a -> Just a
Con.Nothing -> Nothing
......@@ -18,6 +18,9 @@ import Data.Maybe
import Data.Abstract.Widening(Widening,Stable(..))
import Data.Functor.Const
import Data.Lens
import Data.Utils (maybeHead)
import qualified Debug.Trace as Debug
-- | A stack widening operator @(▽ :: s -> a -> (s,a))@ follows the same
-- idea as a regular widening operator, but does not have the
......@@ -71,7 +74,7 @@ project f widen s a =
let (s',(l,b)) = widen (getConst s) (get f a)
in (Const s',(l,set f b a))
data Stack a = Stack Int [a]
data Stack a = Stack { size :: Int, _stack :: [a]}
instance Semigroup (Stack a) where (<>) = mappend
instance Monoid (Stack a) where
mempty = Stack 0 []
......@@ -85,6 +88,9 @@ stack f s@(Stack n st) x =
let (_,(l,x')) = f s x
in (Stack (n+1) (x':st),(l,x'))
trace :: (s a -> a -> String) -> StackWidening s a -> StackWidening s a
trace showA widening s x = Debug.trace (showA s x) (widening s x)
-- | Return the same elements until the specified maximum stack size
-- is reached, then call the fallback widening.
maxSize :: Int -> StackWidening Stack a -> StackWidening Stack a
......@@ -92,35 +98,32 @@ maxSize limit fallback s@(Stack n _) x
| n < limit = (s,(NoLoop,x))
| otherwise = fallback s x
-- | Reuse an element from the stack that is greater than the current
-- element. If no such elements exist, call the fallback widening.
reuse :: PreOrd a => (a -> [a] -> a) -> StackWidening Stack a -> StackWidening Stack a
reuse bestChoice fallback s@(Stack _ st) x
| null st = (s,(NoLoop,x))
| not (null candidates) = (s,(Loop,bestChoice x candidates))
| otherwise = fallback s x
where
-- All elements in the stack that are greater than the current
-- element are potential candidates.
candidates = [ y | y <- st, x y ]
-- | Reuses an element from the stack. If no such elements exists, the
-- fallback widening is called.
reuse :: (a -> [a] -> Maybe a) -> StackWidening Stack a -> StackWidening Stack a
reuse choice fallback s@(Stack _ st) x
| null st = (s,(NoLoop,x))
| otherwise = case choice x st of
Just x' -> (s,(Loop,x'))
Nothing -> fallback s x
reuseFirst :: PreOrd a => StackWidening Stack a -> StackWidening Stack a
reuseFirst = reuse (\_ -> head)
reuseFirst = reuse (\x xs -> maybeHead [ x' | x' <- xs, x x' ])
data Groups k s a = Groups (HashMap k (s a))
instance (Identifiable k, Monoid (s a)) => Semigroup (Groups k s a) where (<>) = mappend
instance (Identifiable k, Monoid (s a)) => Monoid (Groups k s a) where
data Groups k b s a = Groups (HashMap k (s b))
instance (Identifiable k, Monoid (s b)) => Semigroup (Groups k b s a) where (<>) = mappend
instance (Identifiable k, Monoid (s b)) => Monoid (Groups k b s a) where
mempty = Groups M.empty
mappend (Groups m) (Groups m') = Groups (m `mappend` m')
instance (Show k, Show (s a)) => Show (Groups k s a) where
instance (Show k, Show (s b)) => Show (Groups k b s a) where
show (Groups m) = show (M.toList m)
groupBy :: (Monoid (s a), Identifiable k) => (a -> k) -> StackWidening s a -> StackWidening (Groups k s) a
groupBy f fallback (Groups m) a =
let k = f a
groupBy :: (Monoid (s b), Identifiable k) => Iso' a (k,b) -> StackWidening s b -> StackWidening (Groups k b s) a
groupBy f widen (Groups m) a =
let (k,b) = get f a
s = fromMaybe mempty (M.lookup k m)
(s',(l,a')) = fallback s a
in (Groups (M.insert k s' m), (l,a'))
(s',(l,b')) = widen s b
in (Groups (M.insert k s' m), (l,get (from f) (k,b')))
fromWidening :: Complete a => Widening a -> StackWidening Stack a
fromWidening w s@(Stack _ l) a = case l of
......
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
module Data.Abstract.WeakMap(Map,widening,empty,insert,lookup,lookup',delete,delete',deleteIfNotPresent,deleteIfNotPresent',union,fromList,fromList') where
import Prelude hiding (lookup)
import Control.DeepSeq
import Data.Identifiable
import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.Order
import qualified Data.Abstract.Maybe as A
import Data.Abstract.Widening
import Data.Coerce
import Data.Hashable
import Text.Printf
newtype Map a b = Map (HashMap a (A.Maybe b)) deriving (Eq,Hashable,NFData)
instance (Identifiable a, PreOrd b) => PreOrd (Map a b) where
() = withMap2 $ \m1 m2 -> all (\(k,v) -> M.lookup k m1 Just v) (M.toList m2)
instance (Identifiable a, Complete b) => Complete (Map a b) where
() = withMap2 $ M.intersectionWith ()
instance (Show a,Show b) => Show (Map a b) where
show (Map h)
| M.null h = "[]"
| otherwise = "[" ++ init (unwords (map showElem (M.toList h))) ++ "]"
where
showElem (k,m) = case m of
A.Just x -> printf "%s -> %s," (show k) (show x)
A.Nothing -> printf "%s❌," (show k)
A.JustNothing x -> printf "%s? -> %s," (show k) (show x)
widening :: Identifiable a => Widening b -> Widening (Map a b)
widening w = withMap2 $ \m1 m2 -> sequenceA $ M.intersectionWith (A.widening w) m1 m2
empty :: Map a b
empty = Map M.empty
insert :: Identifiable a => a -> b -> Map a b -> Map a b
insert a b = withMap $ M.insert a (A.Just b)
lookup :: (Identifiable a) => a -> b -> Map a b -> A.Maybe b
lookup a def = withMap $ \m -> case M.lookup a m of
Just (A.Just x) -> A.Just x
Just A.Nothing -> A.Nothing
Just (A.JustNothing b) -> A.JustNothing b
Nothing -> A.JustNothing def
lookup' :: (Identifiable a, UpperBounded b) => a -> Map a b -> A.Maybe b
lookup' a = lookup a top
delete :: Identifiable a => a -> Map a b -> Map a b
delete a = withMap $ M.insert a A.Nothing
delete' :: (Foldable f, Identifiable a) => f a -> Map a b -> Map a b
delete' l m = foldl (flip delete) m l
deleteIfNotPresent :: Identifiable a => a -> Map a b -> Map a b
deleteIfNotPresent a = withMap $ M.insertWith (\_ old -> old) a A.Nothing
deleteIfNotPresent' :: (Foldable f, Identifiable a) => f a -> Map a b -> Map a b
deleteIfNotPresent' l m = foldl (flip deleteIfNotPresent) m l
union :: (Identifiable a, Complete b) => Map a b -> Map a b -> Map a b
union = withMap2 $ M.unionWith join
where
join (A.Just a) _ = A.Just a
join A.Nothing b = b
join (A.JustNothing a) b = A.Just a b
fromList :: Identifiable a => [(a,b)] -> Map a b
fromList l = fromList' [ (a,A.Just b) | (a,b) <- l]
fromList' :: Identifiable a => [(a,A.Maybe b)] -> Map a b
fromList' l = coerce (M.fromList l)
withMap2 :: Coercible c c' => (HashMap a (A.Maybe b) -> HashMap a (A.Maybe b) -> c) -> Map a b -> Map a b -> c'
withMap2 = coerce
{-# INLINE withMap2 #-}
withMap :: Coercible c c' => (HashMap a (A.Maybe b) -> c) -> Map a b -> c'
withMap = coerce
{-# INLINE withMap #-}
......@@ -5,7 +5,6 @@
module Data.Concrete.Error where
import Data.Hashable
import Data.Monoidal
import Data.Profunctor
import Control.Monad
......
{-
Haskell code for the paper "Profunctor Optics: Modular Data Accessors"
by Matthew Pickering, Jeremy Gibbons, and Nicolas Wu
to appear in "The Art, Science, and Engineering of Programming" 1(2), 2017
-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}
module Data.Lens where
......@@ -13,6 +7,12 @@ import Data.Functor.Const
import Data.Functor.Identity
import Data.Monoid
{-
Haskell code for the paper "Profunctor Optics: Modular Data Accessors"
by Matthew Pickering, Jeremy Gibbons, and Nicolas Wu
to appear in "The Art, Science, and Engineering of Programming" 1(2), 2017
-}
type Optic p s t a b = p a b -> p s t
type Iso s t a b = forall p. Profunctor p => Optic p s t a b
......@@ -91,3 +91,18 @@ instance (Strong c) => Strong (SecondT u c) where
instance (Choice c) => Choice (SecondT u c) where
left' (SecondT f) = SecondT (dimap (\(u,e) -> either (Left . (u,)) (Right . (u,)) e) (either (second' Left) (second' Right)) (left' f))
right' (SecondT f) = SecondT (dimap (\(u,e) -> either (Left . (u,)) (Right . (u,)) e) (either (second' Left) (second' Right)) (right' f))
-- | Due to https://hackage.haskell.org/package/lens-4.17/docs/src/Control.Lens.Internal.Iso.html
data Exchange a b s t = Exchange (s -> a) (b -> t)
instance Profunctor (Exchange a b) where
dimap f g (Exchange f' g') = Exchange (f' . f) (g . g')
lmap f (Exchange f' g') = Exchange (f' . f) g'
rmap g (Exchange f' g') = Exchange f' (g . g')
withIso :: Iso s t a b -> ((s -> a) -> (b -> t) -> r) -> r
withIso f k = let (Exchange f' g') = f (Exchange id id)
in k f' g'
from :: Iso s t a b -> Iso b a t s
from f = withIso f $ \f' g' -> iso g' f'
......@@ -6,3 +6,7 @@ import qualified Data.Map as Map
lookupM :: (Ord k, Monoid v) => k -> Map k v -> v
lookupM x m = fromMaybe mempty $ Map.lookup x m
maybeHead :: [a] -> Maybe a
maybeHead (a:_) = Just a
maybeHead [] = Nothing
......@@ -32,7 +32,7 @@ import qualified Data.Abstract.StackWidening as SW
import Data.Order
import Data.Hashable
import Data.Profunctor
import Data.Lens (_2)
import Data.Lens (iso')
import GHC.Generics
......@@ -132,8 +132,7 @@ spec = do
(proc x -> f -< (Even,x-I.Interval 1 1))) -< x
in
it "even([0,∞]) should be top" $
let ?stackWiden = SW.groupBy fst
$ SW.project _2
let ?stackWiden = SW.groupBy (iso' id id)
$ SW.stack
$ SW.maxSize 3
$ SW.reuseFirst
......
......@@ -19,7 +19,7 @@
-- | k-CFA analysis for PCF where numbers are approximated by intervals.
module IntervalAnalysis where
import Prelude hiding (Bounded,fail,(.))
import Prelude hiding (Bounded,fail,(.),exp)
import Control.Category
import Control.Arrow
......@@ -81,7 +81,7 @@ type Addr = (Text,CallString Label)
-- maximum interval bound, the depth @k@ of the longest call string,
-- an environment, and the input of the computation.
evalInterval :: (?bound :: IV) => Int -> [(Text,Val)] -> State Label Expr -> Terminating (Failure String Val)
evalInterval k env e = -- runInterp eval ?bound k env (generate e)
evalInterval k env0 e = -- runInterp eval ?bound k env (generate e)
runFixT stackWiden (T.widening (E.widening widenVal))
(runTerminatingT
(runFailureT
......@@ -96,13 +96,12 @@ evalInterval k env e = -- runInterp eval ?bound k env (generate e)
(FailureT String
(TerminatingT
(FixT _ () () (->))))))) Expr Val))))))
(env,generate e)
(env0,generate e)
where
widenVal = widening (W.bounded ?bound I.widening)
stackWiden :: SW.StackWidening _ (Env,Expr)
stackWiden = SW.filter (\(_,ex) -> case ex of App {} -> True; Y {} -> True; _ -> False)
$ SW.groupBy (\(_,ex) -> label ex :: Label)
$ SW.project L._1
$ SW.groupBy (L.iso' (\(env,exp) -> (exp,env)) (\(exp,env) -> (env,exp)))
$ SW.stack
$ SW.maxSize 3
$ SW.reuseFirst
......
......@@ -6,33 +6,41 @@ import Prelude hiding (exp)
import SortSemantics -- hiding (sortContext)
import Syntax hiding (Fail)
import CaseStudy
import SortContext(Context,Sort(..))
import qualified SortContext as Ctx
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.WeakMap as S
import qualified Data.HashMap.Lazy as M
import Criterion
import Criterion.Main
main :: IO ()
main = defaultMain [
bgroup "Sort Semantics" [
bench "reduce Add(Zero,y)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp"
prog = Match (Cons "Add" [Cons "Zero" [], "y"]) `Seq` Build "y"
in nf (eval 0 10 prog M.empty ?ctx emptyEnv) exp
,
bench "should support recursion" $
let ?ctx = Ctx.empty in
let t = convertToList [numerical, numerical, numerical] ?ctx
tenv = termEnv [("x",t)]
prog = Let [("map", map')] (Match "x" `Seq` Call "map" [Build (NumberLiteral 1)] ["x"])
in nf (eval 2 3 prog M.empty ?ctx emptyEnv) t
main = do
pcf <- pcfCaseStudy
defaultMain [
bgroup "Sort Semantics" [
bench "reduce Add(Zero,y)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp"
prog = Match (Cons "Add" [Cons "Zero" [], "y"]) `Seq` Build "y"
in nf (eval 0 10 prog M.empty ?ctx emptyEnv) exp
,
bench "should support recursion" $
let ?ctx = Ctx.empty in
let t = convertToList [numerical, numerical, numerical] ?ctx
prog = Let [("map", map')] (Scope ["x"] (Match "x" `Seq` Call "map" [Build (NumberLiteral 1)] ["x"]))
in nf (eval 2 3 prog M.empty ?ctx emptyEnv) t
,
bench "pcf" $
let ?ctx = signature pcf in
let senv = stratEnv pcf
in nf (eval 5 10 (Call "eval_0_0" [] []) senv ?ctx emptyEnv) (term (Tuple [List (Tuple [Lexical, "Val"]), "Exp"]))
]
]
]
where
term :: (?ctx :: Context) => Sort -> Term
term s = Term s ?ctx
......@@ -40,9 +48,6 @@ main = defaultMain [
numerical :: (?ctx :: Context) => Term
numerical = term Numerical
termEnv :: [(TermVar, Term)] -> TermEnv
termEnv = S.fromList
emptyEnv :: TermEnv
emptyEnv = S.empty
......
This diff is collapsed.
Specification([Signature([Constructors([ExtOpDecl("Var",FunType([ConstType(Sort("String",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("App",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Abs",FunType([ConstType(Sort("String",[])),ConstType(Sort("Type",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Zero",ConstType(Sort("Exp",[]))),ExtOpDecl("Succ",FunType([ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Pred",FunType([ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Ifz",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Closure",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("List",[Sort("Val",[])]))],ConstType(Sort("Val",[])))),ExtOpDecl("Z",ConstType(Sort("Val",[]))),ExtOpDecl("S",FunType([ConstType(Sort("Val",[]))],ConstType(Sort("Val",[])))),ExtOpDecl("Num",ConstType(Sort("Type",[]))),ExtOpDecl("Fun",FunType([ConstType(Sort("Type",[])),ConstType(Sort("Type",[]))],ConstType(Sort("Type",[])))),ExtOpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),ExtOpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),ExtOpDecl("DR_UNDEFINE",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),ExtOpDecl("DR_DUMMY",ConstType(Sort("ATerm",[]))),ExtOpDecl("",ConstType(Sort("Tuple",[Sort("Nil",[])]))),ExtOpDecl("",FunType([ConstType(SortVar("a"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Nil",[])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Nil",[])])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Cons",[SortVar("c"),Sort("Nil",[])])])])]))))])]),Strategies([ExtSDef("check",[],[]),ExtSDef("eval",[],[]),ExtSDef("check-eval",[],[]),ExtSDef("lookup",[],[]),ExtSDef("Anno_Cong__",[VarDec("t_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("u_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Var",[VarDec("v_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("App",[VarDec("w_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("x_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Abs",[VarDec("y_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("z_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("a_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Zero",[],[]),ExtSDef("Succ",[VarDec("b_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Pred",[VarDec("c_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Ifz",[VarDec("d_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("e_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("f_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Closure",[VarDec("g_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("h_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Z",[],[]),ExtSDef("S",[VarDec("i_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Num",[],[]),ExtSDef("Fun",[VarDec("j_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("k_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Nil",[],[]),ExtSDef("Cons",[VarDec("l_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("m_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[],[]),ExtSDef("",[VarDec("n_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("o_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("p_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("q_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("r_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("s_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_UNDEFINE",[VarDec("t_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_DUMMY",[],[])])])
\ No newline at end of file
Specification([Signature([Constructors([ExtOpDecl("Var",FunType([ConstType(Sort("String",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("App",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Abs",FunType([ConstType(Sort("String",[])),ConstType(Sort("Type",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Zero",ConstType(Sort("Exp",[]))),ExtOpDecl("Succ",FunType([ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Pred",FunType([ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Ifz",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[])),ConstType(Sort("Exp",[]))],ConstType(Sort("Exp",[])))),ExtOpDecl("Closure",FunType([ConstType(Sort("Exp",[])),ConstType(Sort("List",[Sort("String",[]),Sort("Val",[])]))],ConstType(Sort("Val",[])))),ExtOpDecl("Z",ConstType(Sort("Val",[]))),ExtOpDecl("S",FunType([ConstType(Sort("Val",[]))],ConstType(Sort("Val",[])))),ExtOpDecl("Num",ConstType(Sort("Type",[]))),ExtOpDecl("Fun",FunType([ConstType(Sort("Type",[])),ConstType(Sort("Type",[]))],ConstType(Sort("Type",[])))),ExtOpDecl("Nil",ConstType(Sort("List",[SortVar("a")]))),ExtOpDecl("Cons",FunType([ConstType(SortVar("a")),ConstType(Sort("List",[SortVar("a")]))],ConstType(Sort("List",[SortVar("a")])))),ExtOpDecl("DR_UNDEFINE",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),ExtOpDecl("DR_DUMMY",ConstType(Sort("ATerm",[]))),ExtOpDecl("",ConstType(Sort("Tuple",[Sort("Nil",[])]))),ExtOpDecl("",FunType([ConstType(SortVar("a"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Nil",[])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Nil",[])])])])))),ExtOpDecl("",FunType([ConstType(SortVar("a")),ConstType(SortVar("b")),ConstType(SortVar("c"))],ConstType(Sort("Tuple",[Sort("Cons",[SortVar("a"),Sort("Cons",[SortVar("b"),Sort("Cons",[SortVar("c"),Sort("Nil",[])])])])]))))])]),Strategies([ExtSDef("check",[],[]),ExtSDef("eval",[],[]),ExtSDef("check-eval",[],[]),ExtSDef("lookup",[],[]),ExtSDef("Anno_Cong__",[VarDec("t_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("u_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Var",[VarDec("v_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("App",[VarDec("w_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("x_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Abs",[VarDec("y_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("z_3",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("a_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Zero",[],[]),ExtSDef("Succ",[VarDec("b_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Pred",[VarDec("c_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Ifz",[VarDec("d_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("e_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("f_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Closure",[VarDec("g_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("h_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Z",[],[]),ExtSDef("S",[VarDec("i_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Num",[],[]),ExtSDef("Fun",[VarDec("j_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("k_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("Nil",[],[]),ExtSDef("Cons",[VarDec("l_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("m_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[],[]),ExtSDef("",[VarDec("n_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("o_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("p_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("",[VarDec("q_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("r_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[])))),VarDec("s_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_UNDEFINE",[VarDec("t_4",FunType([ConstType(Sort("ATerm",[]))],ConstType(Sort("ATerm",[]))))],[]),ExtSDef("DR_DUMMY",[],[])])])
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
......@@ -38,7 +38,9 @@ Specification(
, OpDecl(
"Closure"
, FunType(
[ConstType(SortNoArgs("Exp")), ConstType(Sort("List", [SortNoArgs("Val")]))]
[ ConstType(SortNoArgs("Exp"))
, ConstType(Sort("List", [SortNoArgs("String"), SortNoArgs("Val")]))
]
, ConstType(SortNoArgs("Val"))
)
)
......
This diff is collapsed.
......@@ -10,7 +10,7 @@ signature
Pred : Exp -> Exp
Ifz : Exp * Exp * Exp -> Exp
Closure : Exp * List(Val) -> Val
Closure : Exp * List(String, Val) -> Val
Z : Val
S : Val -> Val
......@@ -22,7 +22,7 @@ signature
: ()
: a -> (a)
: a * b -> (a, b)
: a * b * c -> (a, b, c)
: a * b * c -> (a, b, c)
strategies
......
module CaseStudy where
import Syntax
import qualified Data.Text.IO as TIO
import qualified Data.ATerm as A
import Paths_sturdy_stratego
import Text.Printf
pcfCaseStudy :: IO Module
pcfCaseStudy = caseStudy "pcf"
caseStudy :: String -> IO Module
caseStudy name = do
file <- TIO.readFile =<< getDataFileName (printf "case-studies/%s/%s.aterm" name name)
case parseModule =<< A.parseATerm file of
Left e -> fail (show e)
Right module_ -> return module_
......@@ -50,7 +50,6 @@ import Data.Order
import Data.Term
import Data.Text (Text)
import Data.Profunctor
import Data.Lens (Prism')
import qualified Data.Lens as L
import Data.Abstract.FreeCompletion (FreeCompletion(Lower,Top))
import qualified Data.Abstract.FreeCompletion as Free
......@@ -91,7 +90,7 @@ type Interp s a b =
(->))))))))) a b
runInterp :: Interp _ a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (FreeCompletion (Failure String (Except () (TermEnv, b))))
runInterp f i senv tenv a =
runInterp f i senv0 tenv0 a =
runFixT stackWidening (T.widening grammarWidening)
(runTerminatingT
(runCompletionT
......@@ -100,25 +99,18 @@ runInterp f i senv tenv a =
(runStateT
(runReaderT
(runGrammarT f)))))))
(tenv, (senv, a))
(tenv0, (senv0, a))
where
stackWidening :: SW.StackWidening _ (TermEnv, (StratEnv, (Strat, Term)))
stackWidening = SW.filter' (L.second (L.second (L.first stratCall)))
$ SW.groupBy (\(_,(_,((stratVar,_,_),_))) -> stratVar)
$ SW.project (L.second (L._2 . L._2))
$ SW.groupBy (L.iso' (\(tenv,(senv,(strat,term))) -> ((strat,senv),(term,tenv))) (\((strat,senv),(term,tenv)) -> (tenv,(senv,(strat,term)))))
$ SW.stack
$ SW.reuseFirst
$ SW.maxSize i
$ SW.fromWidening (S.widening widening W.** widening)
$ SW.fromWidening (widening W.** S.widening widening)
grammarWidening = Free.widening (F.widening (E.widening (\_ _ -> (Stable,())) (S.widening widening W.** widening)))