Commit 5d57e761 authored by Sebastian Erdweg's avatar Sebastian Erdweg

finished migration of stratego intepreters

parent 07cd4603
......@@ -12,6 +12,8 @@ import qualified Data.Abstract.Powerset as Abs
import qualified Data.Concrete.Powerset as Con
import qualified Data.Concrete.Error as Con
import qualified Data.Abstract.Error as Abs
import qualified Data.Concrete.Failure as ConF
import qualified Data.Abstract.Failure as AbsF
import qualified Data.Concrete.Boolean as Con
import qualified Data.Abstract.Boolean as Abs
import qualified Data.Abstract.Interval as Abs
......@@ -57,6 +59,13 @@ instance (Complete a', Eq a, Hashable a, Galois (Con.Pow a) a', Eq b, Hashable b
Con.Success y -> Abs.Success (alphaSing y)
gamma = error "noncomputable"
instance (Eq e, Hashable e, Eq b, Hashable b, Complete b', Galois (Con.Pow b) b')
=> Galois (Con.Pow (ConF.Failure e b)) (AbsF.Failure e b') where
alpha = lifted $ \e -> case e of
ConF.Fail x -> AbsF.Fail x
ConF.Success y -> AbsF.Success (alphaSing y)
gamma = error "noncomputable"
instance (Hashable a, Eq a, Complete a', Galois (Con.Pow a) a')
=> Galois (Con.Pow (Maybe a)) (Maybe a') where
alpha = lifted $ \e -> case e of
......
flags: {}
extra-package-dbs: []
resolver: lts-13.4
resolver: lts-12.10
packages:
- 'lib'
- 'rtg'
......
......@@ -19,8 +19,9 @@ import qualified Criterion.Measurement as CM
import qualified Criterion.Types as CT
import Data.ATerm
import Data.Abstract.HandleError
import qualified Data.Abstract.PreciseStore as S
import Data.Abstract.Error
import qualified Data.Abstract.Failure as F
import qualified Data.Abstract.Map as S
import Data.Abstract.Terminating
import Data.Foldable
import Data.HashSet (HashSet)
......@@ -57,7 +58,7 @@ measure analysisName action = do
-- | Runs the given semantics on the given function within the given
-- case study.
caseStudy :: (Strat -> StratEnv -> W.TermEnv -> W.Term -> Terminating (W.Pow (Error () (W.TermEnv,W.Term)))) -> String -> String -> IO (HashSet W.Term)
caseStudy :: (Strat -> StratEnv -> W.TermEnv -> W.Term -> Terminating (W.Pow (F.Failure String (Error () (W.TermEnv,W.Term))))) -> String -> String -> IO (HashSet W.Term)
caseStudy eval name function = do
printf "------------------ case study: %s ----------------------\n" name
file <- TIO.readFile =<< getDataFileName (printf "case-studies/%s/%s.aterm" name name)
......@@ -72,3 +73,4 @@ caseStudy eval name function = do
where
filterResults = fmap (\r -> case r of Success (_,t) -> t; SuccessOrFail _ (_,t) -> t; Fail _ -> error "")
. filter (\r -> case r of Success _ -> True; SuccessOrFail _ _ -> True; Fail _ -> False)
. fmap (\r -> case r of F.Success t -> t; F.Fail msg -> error msg)
{-# LANGUAGE OverloadedStrings #-}
module Pretty.Haskell where
import Prelude hiding ((<>))
import WildcardSemantics
import qualified Data.Text as T
......
......@@ -2,6 +2,8 @@
{-# LANGUAGE ScopedTypeVariables #-}
module Pretty.JavaScript where
import Prelude hiding ((<>))
import WildcardSemantics
import Text.PrettyPrint hiding (sep)
-- import Control.Exception
......
{-# LANGUAGE OverloadedStrings #-}
module Pretty.PCF where
import Prelude hiding ((<>))
import WildcardSemantics
import Text.PrettyPrint
......
module Pretty.Results where
import Prelude hiding ((<>))
import WildcardSemantics
import Data.Foldable
......
......@@ -29,18 +29,21 @@ import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Transformer.Abstract.Completion
import Control.Arrow.Transformer.Abstract.Fixpoint
import Control.Arrow.Transformer.Abstract.HandleExcept
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Failure
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
import Control.Category hiding ((.))
import Data.Abstract.FreeCompletion (FreeCompletion(Lower,Top))
import qualified Data.Abstract.FreeCompletion as F
import Data.Abstract.HandleError (Error)
import qualified Data.Abstract.HandleError as E
import qualified Data.Abstract.FreeCompletion as Free
import Data.Abstract.Error (Error)
import qualified Data.Abstract.Error as E
import Data.Abstract.Failure (Failure)
import qualified Data.Abstract.Failure as F
import Data.Abstract.Maybe
import Data.Abstract.PreciseStore (Store)
import qualified Data.Abstract.PreciseStore as S
import Data.Abstract.Map (Map)
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (Terminating,fromTerminating)
import Data.Abstract.Widening as W
......@@ -64,25 +67,27 @@ import Text.Printf
data Constr = Constr Text | StringLit Text | NumLit Int deriving (Eq, Ord, Show)
newtype Term = Term (GrammarBuilder Constr) deriving (Complete, Eq, Hashable, PreOrd, Show)
type TermEnv = Store TermVar Term
type TermEnv = Map TermVar Term
newtype Interp s a b =
Interp (
Fix (Strat,Term) Term
(Reader StratEnv
(State TermEnv
(Except ()
(Completion
(Fixpoint s () ()
(->)))))) a b)
runInterp :: Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (FreeCompletion (Error () (TermEnv, b)))
(ReaderT StratEnv
(StateT TermEnv
(ExceptT ()
(FailureT String
(CompletionT
(FixT s () ()
(->))))))) a b)
runInterp :: Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (FreeCompletion (Failure String (Error () (TermEnv, b))))
runInterp (Interp f) i senv tenv a =
runFix' stackWidening grammarWidening
(runCompletion
(runExcept
(runState
(runReader f))))
runFixT' stackWidening grammarWidening
(runCompletionT
(runFailureT
(runExceptT
(runStateT
(runReaderT f)))))
(tenv, (senv, a))
where
stackWidening :: SW.StackWidening (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) (TermEnv, (StratEnv, (Strat, Term)))
......@@ -91,13 +96,13 @@ runInterp (Interp f) i senv tenv a =
(SW.maxSize i
(SW.reuse bestChoice
(SW.fromWidening (S.widening widening W.** widening)))))
grammarWidening = F.widening (E.widening (\_ _ -> ()) (S.widening widening W.** widening))
grammarWidening = Free.widening (F.widening (E.widening (\_ _ -> ()) (S.widening widening W.** widening)))
bestChoice :: (TermEnv, Term) -> [(TermEnv, Term)] -> (TermEnv, Term)
bestChoice e [] = e
bestChoice _ (x:_) = x
eval :: Int -> Strat -> StratEnv -> TermEnv -> Term -> Terminating (FreeCompletion (Error () (TermEnv, Term)))
eval :: Int -> Strat -> StratEnv -> TermEnv -> Term -> Terminating (FreeCompletion (Failure String (Error () (TermEnv, Term))))
eval i s = runInterp (eval' s) i
-- Create grammars -----------------------------------------------------------------------------------
......@@ -128,8 +133,8 @@ deriving instance Arrow (Interp s)
deriving instance ArrowChoice (Interp s)
deriving instance ArrowReader StratEnv (Interp s)
deriving instance ArrowState TermEnv (Interp s)
deriving instance ArrowFail () (Interp s)
deriving instance (Complete (FreeCompletion y), PreOrd y) => ArrowExcept x y () (Interp s)
deriving instance ArrowFail String (Interp s)
deriving instance ArrowExcept () (Interp s)
deriving instance PreOrd b => PreOrd (Interp s a b)
deriving instance (Complete (FreeCompletion b), PreOrd b) => Complete (Interp s a b)
deriving instance PreOrd b => LowerBounded (Interp s a b)
......@@ -187,7 +192,7 @@ instance IsTerm Term (Interp s) where
Constr c'' | c'' == c && eqLength ps ts -> do
ts' <- matchSubterms -< (ps,ts)
cons -< (Constructor c,ts')
_ -> fail -< ()) -<< mapSnd (map Term) (toSubterms g)
_ -> throw -< ()) -<< mapSnd (map Term) (toSubterms g)
matchTermAgainstExplode _ _ = undefined
......@@ -195,9 +200,9 @@ instance IsTerm Term (Interp s) where
matchTermAgainstString = proc (s,Term g) -> matchLit -< (normalize (epsilonClosure g), StringLit s)
equal = proc (Term g1, Term g2) -> case g1 g2 of
g | isEmpty g -> fail -< ()
g | isEmpty g -> throw -< ()
| isSingleton (normalize (epsilonClosure g1)) && isSingleton (normalize (epsilonClosure g2)) -> returnA -< Term g
| otherwise -> returnA fail' -< Term g
| otherwise -> (returnA -< Term g) (throw -< ())
convertFromList = undefined
......@@ -206,7 +211,7 @@ instance IsTerm Term (Interp s) where
Constr c' -> do
ts' <- f -< ts
cons -< (Constructor c',ts')
_ -> fail -< ()) -< mapSnd toTerms (toSubterms g)
_ -> throw -< ()) -< mapSnd toTerms (toSubterms g)
cons = proc (Constructor c,ts) -> returnA -< Term (normalize (epsilonClosure (addConstructor (Constr c) (fromTerms ts))))
numberLiteral = arr numberGrammar
......@@ -222,11 +227,11 @@ instance TermUtils Term where
instance IsTermEnv TermEnv Term (Interp s) where
getTermEnv = get
putTermEnv = put
lookupTermVar f g = proc (v,env) ->
lookupTermVar f g = proc (v,env,ex) ->
case S.lookup v env of
Just t -> f -< t
JustNothing t -> joined f g -< (t,())
Nothing -> g -< ()
JustNothing t -> joined f g -< (t,ex)
Nothing -> g -< ex
insertTerm = arr $ \(v,t,env) -> S.insert v t env
deleteTermVars = arr $ \(vars,env) -> foldr' S.delete env vars
unionTermEnvs = arr (\(vars,e1,e2) -> S.union e1 (foldr' S.delete e2 vars))
......@@ -249,9 +254,9 @@ instance Galois (C.Pow C.TermEnv) TermEnv where
instance Soundness StratEnv (Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack)) where
sound senv xs f g = Q.forAll (Q.choose (2,3)) $ \i ->
let con :: FreeCompletion (Error () (TermEnv,_))
let con :: FreeCompletion (Failure String (Error () (TermEnv,_)))
con = Lower (alpha (fmap (\(x,tenv) -> C.runInterp f senv tenv x) xs))
abst :: FreeCompletion (Error () (TermEnv,_))
abst :: FreeCompletion (Failure String (Error () (TermEnv,_)))
-- TODO: using fromTerminating is a bit of a hack...
abst = fromTerminating Top $ runInterp g i senv (alpha (fmap snd xs)) (alpha (fmap fst xs))
in Q.counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con abst
......@@ -276,14 +281,14 @@ fromTerm (Term g) = g
checkConstructorAndLength :: Constructor -> [t'] -> Interp s (Constr, [GrammarBuilder Constr]) (Constructor, ([t'], [Term]))
checkConstructorAndLength (Constructor c) ts = proc (c', gs) -> case c' of
Constr c'' | c == c'' && eqLength ts gs -> returnA -< (Constructor c, (ts, toTerms gs))
_ -> fail -< ()
_ -> throw -< ()
matchLit :: Interp s (GrammarBuilder Constr, Constr) Term
-- TODO: check if production to n has empty argument list? This should be the case by design.
matchLit = proc (g,l) -> case g `produces` l of
True | isSingleton g -> returnA -< Term g
| otherwise -> returnA fail' -< Term g
False -> fail -< ()
| otherwise -> (returnA -< Term g) (throw -< ())
False -> throw -< ()
stringGrammar :: Text -> Term
stringGrammar s = Term (singleton (StringLit s))
......
......@@ -7,6 +7,7 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures -fno-warn-orphans #-}
module WildcardSemantics where
......@@ -26,7 +27,8 @@ import Control.Arrow.Fix
import Control.Arrow.Reader
import Control.Arrow.State
import Control.Arrow.Transformer.Abstract.Fixpoint
import Control.Arrow.Transformer.Abstract.HandleExcept
import Control.Arrow.Transformer.Abstract.Except
import Control.Arrow.Transformer.Abstract.Failure
import Control.Arrow.Transformer.Abstract.Powerset
import Control.Arrow.Transformer.Reader
import Control.Arrow.Transformer.State
......@@ -35,11 +37,12 @@ import Control.DeepSeq
import Control.Monad hiding (fail)
import Data.Abstract.FreeCompletion
import Data.Abstract.HandleError
import Data.Abstract.Error
import Data.Abstract.Failure
import Data.Abstract.Maybe
import qualified Data.Abstract.Powerset as A
import Data.Abstract.PreciseStore (Store)
import qualified Data.Abstract.PreciseStore as S
import Data.Abstract.Map (Map)
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (Terminating,fromTerminating)
import Data.Abstract.Widening as W
......@@ -66,26 +69,28 @@ data Term
| Wildcard
deriving (Eq)
type TermEnv = Store TermVar Term
type TermEnv = Map TermVar Term
-- |
newtype Interp s a b =
Interp (
Fix (Strat,Term) Term
(Reader StratEnv
(State TermEnv
(Except ()
(Powerset
(Fixpoint s () ()
(->)))))) a b)
runInterp :: Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (A.Pow (Error () (TermEnv,b)))
(ReaderT StratEnv
(StateT TermEnv
(ExceptT ()
(FailureT String
(PowT
(FixT s () ()
(->))))))) a b)
runInterp :: Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) a b -> Int -> StratEnv -> TermEnv -> a -> Terminating (A.Pow (Failure String (Error () (TermEnv,b))))
runInterp (Interp f) k senv tenv a =
runFix' stackWidening W.finite
(runPowerset
(runExcept
(runState
(runReader f))))
runFixT' stackWidening W.finite
(runPowT
(runFailureT
(runExceptT
(runStateT
(runReaderT f)))))
(tenv, (senv, a))
where
stackWidening :: SW.StackWidening (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack) (TermEnv, (StratEnv, (Strat, Term)))
......@@ -97,7 +102,7 @@ from' (tenv,(senv,(s,t))) = ((s,senv),(tenv,t))
to' :: ((Strat, StratEnv), (TermEnv, Term)) -> (TermEnv, (StratEnv, (Strat, Term)))
to' ((s,senv),(tenv,t)) = (tenv,(senv,(s,t)))
eval :: Int -> Strat -> StratEnv -> TermEnv -> Term -> Terminating (A.Pow (Error () (TermEnv,Term)))
eval :: Int -> Strat -> StratEnv -> TermEnv -> Term -> Terminating (A.Pow (Failure String (Error () (TermEnv,Term))))
eval i s = runInterp (eval' s) i
-- Instances -----------------------------------------------------------------------------------------
......@@ -106,9 +111,9 @@ deriving instance Arrow (Interp s)
deriving instance ArrowChoice (Interp s)
deriving instance ArrowReader StratEnv (Interp s)
deriving instance ArrowState TermEnv (Interp s)
deriving instance ArrowFail () (Interp s)
deriving instance ArrowFail String (Interp s)
deriving instance ArrowFix (Strat,Term) Term (Interp s)
deriving instance PreOrd y => ArrowExcept x y () (Interp s)
deriving instance ArrowExcept () (Interp s)
deriving instance ArrowDeduplicate Term Term (Interp s)
deriving instance PreOrd b => PreOrd (Interp s a b)
deriving instance (Complete b, PreOrd b) => Complete (Interp s a b)
......@@ -125,11 +130,11 @@ instance HasStratEnv (Interp s) where
instance IsTermEnv TermEnv Term (Interp s) where
getTermEnv = get
putTermEnv = put
lookupTermVar f g = proc (v,env) ->
lookupTermVar f g = proc (v,env,ex) ->
case S.lookup v env of
Just t -> f -< t
JustNothing t -> joined f g -< (t,())
Nothing -> g -< ()
JustNothing t -> joined f g -< (t,ex)
Nothing -> g -< ex
insertTerm = arr $ \(v,t,env) -> S.insert v t env
deleteTermVars = arr $ \(vars,env) -> foldr' S.delete env vars
unionTermEnvs = arr (\(vars,e1,e2) -> S.union e1 (foldr' S.delete e2 vars))
......@@ -141,24 +146,24 @@ instance IsTerm Term (Interp s) where
returnA -< Cons c ts''
Wildcard -> do
ts'' <- matchSubterms -< (ts,[ Wildcard | _ <- [1..(length ts)] ])
returnA fail' -< Cons c ts''
_ -> fail -< ()
(returnA -< Cons c ts'') (throw -< ())
_ -> throw -< ()
matchTermAgainstString = proc (s,t) -> case t of
StringLiteral s'
| s == s' -> returnA -< t
| otherwise -> fail -< ()
| otherwise -> throw -< ()
Wildcard ->
returnA fail' -< StringLiteral s
_ -> fail' -< ()
(returnA -< StringLiteral s) (throw -< ())
_ -> throw -< ()
matchTermAgainstNumber = proc (n,t) -> case t of
NumberLiteral n'
| n == n' -> returnA -< t
| otherwise -> fail -< ()
| otherwise -> throw -< ()
Wildcard ->
success fail' -< NumberLiteral n
_ -> fail' -< ()
(returnA -< NumberLiteral n) (throw -< ())
_ -> throw -< ()
matchTermAgainstExplode matchCons matchSubterms = proc t -> case t of
Cons (Constructor c) ts -> do
......@@ -188,22 +193,22 @@ instance IsTerm Term (Interp s) where
| c == c' && eqLength ts ts' -> do
ts'' <- zipWithA equal -< (ts,ts')
returnA -< Cons c ts''
| otherwise -> fail -< ()
| otherwise -> throw -< ()
(StringLiteral s, StringLiteral s')
| s == s' -> success -< t1
| otherwise -> fail -< ()
| otherwise -> throw -< ()
(NumberLiteral n, NumberLiteral n')
| n == n' -> success -< t1
| otherwise -> fail -< ()
(Wildcard, t) -> fail' success -< t
(t, Wildcard) -> fail' success -< t
(_,_) -> fail' -< ()
| otherwise -> throw -< ()
(Wildcard, t) -> (returnA -< t) (throw -< ())
(t, Wildcard) -> (returnA -< t) (throw -< ())
(_,_) -> throw -< ()
convertFromList = proc (c,ts) -> case (c,go ts) of
(StringLiteral c', Just ts'') -> returnA -< Cons (Constructor c') ts''
(Wildcard, Just _) -> fail' success -< Wildcard
(_, Nothing) -> fail' success -< Wildcard
_ -> fail' -< ()
(Wildcard, Just _) -> (returnA -< Wildcard) (throw -< ())
(_, Nothing) -> (returnA -< Wildcard) (throw -< ())
_ -> throw -< ()
where
go t = case t of
Cons "Cons" [x,tl] -> (x:) <$> go tl
......@@ -218,7 +223,7 @@ instance IsTerm Term (Interp s) where
returnA -< Cons c ts'
StringLiteral _ -> returnA -< t
NumberLiteral _ -> returnA -< t
Wildcard -> fail' success -< Wildcard
Wildcard -> (returnA -< Wildcard) (throw -< ())
cons = arr (uncurry Cons)
numberLiteral = arr NumberLiteral
......@@ -226,9 +231,9 @@ instance IsTerm Term (Interp s) where
instance Soundness StratEnv (Interp (SW.Categories (Strat,StratEnv) (TermEnv, Term) SW.Stack)) where
sound senv xs f g = forAll (choose (0,3)) $ \i ->
let con :: A.Pow (Error () (TermEnv,_))
let con :: A.Pow (Failure String (Error () (TermEnv,_)))
con = A.dedup $ alpha (fmap (\(x,tenv) -> C.runInterp f senv tenv x) xs)
abst :: A.Pow (Error () (TermEnv,_))
abst :: A.Pow (Failure String (Error () (TermEnv,_)))
abst = A.dedup $ fromTerminating (error "non-terminating wildcard semantics") $ runInterp g i senv (alpha (fmap snd xs)) (alpha (fmap fst xs))
in counterexample (printf "%s ⊑/ %s" (show con) (show abst)) $ con abst
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment