Commit 83b52d4d authored by Sven Keidel's avatar Sven Keidel

import stratego

parent 5b9245d6
......@@ -2,7 +2,7 @@
let
hsEnv = pkgs.haskellPackages.ghcWithPackages(p: with p; [
Cabal cabal-install hlint text containers hspec mtl numeric-limits
Cabal cabal-install hlint text containers hspec mtl numeric-limits criterion
]);
in pkgs.stdenv.mkDerivation {
......
name: sturdy
name: sturdy-lib
version: 0.1.0.0
......
((haskell-mode . ((flycheck-ghc-search-path . ("/home/sven/documents/system-s/src/" "/home/sven/documents/system-s/dist/build/autogen/")))))
{-# LANGUAGE OverloadedStrings #-}
module Combine where
import Data.ATerm
import qualified Data.Text.IO as T
import System.Environment
main :: IO ()
main = do
[ast,core] <- getArgs
astATerm <- parseATerm <$> T.readFile ast
coreATerm <- parseATerm <$> T.readFile core
case (astATerm,coreATerm) of
(Right (ATerm "Specification" [List (sig:_)]),
Right (ATerm "Specification" [List [_, rules]])) ->
print (ATerm "Specification" [List [sig,rules]])
(Left _, Right _) -> error "Ast file did not parse correctly"
(Right _, Left _) -> error "Core file did not parse correctly"
(Left _, Left _) -> error "Ast and core file did not parse correctly"
(_, _) -> error "Unexpected ATerm"
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
module Grammar.RegularTreeGrammar where
import WildcardSemantics (Term)
import qualified WildcardSemantics as W
import Data.Constructor
import Data.Foldable
import Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as M
import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Hashable (Hashable(..))
import Data.Sequence (Seq)
import qualified Data.Sequence as S
import Data.Text (Text,unpack)
import Data.Vector (Vector)
import qualified Data.Vector as V
import Control.Monad
import Control.Monad.Reader
import Control.Monad.Writer
data Symbol = Symbol {-# UNPACK #-} !Int {-# UNPACK #-} !Text
data GrammarTerm
= Cons Constructor [GrammarTerm]
| AnyString
| StringLiteral Text
| AnyNumber
| NumberLiteral Int
| NonTerminal Symbol
deriving (Eq)
data Rule = Rule {-# UNPACK #-} !Symbol GrammarTerm deriving Eq
type Grammar = Vector Rule
type Summary = HashMap Rule Int
summary :: Grammar -> Term -> Maybe Summary
summary g = fmap (foldl' (flip (M.adjust (+ 1))) initial) . runTopDown g
where
initial :: Summary
initial = M.fromList $ (,0) <$> V.toList g
runTopDown :: Grammar -> Term -> Maybe (Seq Rule)
runTopDown grammar term = execWriterT (runReaderT (topDown (Symbol 0 "") term) grammar)
distanceSum :: Grammar -> Term -> Maybe Int
distanceSum g t = S.length <$> runTopDown g t
topDown :: (MonadReader Grammar m, MonadWriter (Seq Rule) m, MonadPlus m) => Symbol -> Term -> m ()
topDown startSymbol term = do
grammar <- ask
go grammar
where
go :: (MonadReader Grammar m, MonadWriter (Seq Rule) m, MonadPlus m) => Grammar -> m ()
go = V.foldr (\rule@(Rule symbol rhs) -> mplus (guard (startSymbol == symbol) >> match rhs term >> tell (return rule))) mzero
match :: (MonadReader Grammar m, MonadWriter (Seq Rule) m, MonadPlus m) => GrammarTerm -> Term -> m ()
match (Cons s ts) (W.Cons s' ts') | s == s' && length ts == length ts' = zipWithM_ match ts ts'
match AnyString (W.StringLiteral _) = return ()
match (StringLiteral s) (W.StringLiteral s') = guard $ s == s'
match AnyNumber (W.NumberLiteral _) = return ()
match (NumberLiteral n) (W.NumberLiteral n') = guard $ n == n'
match _ W.Wildcard = return ()
match (NonTerminal n) t = topDown n t
match _ _ = mzero
termsOfDistance :: Int -> Grammar -> HashSet Term
termsOfDistance maxDepth grammar = H.fromList $ toList $ go maxDepth (Symbol 0 "")
where
go :: Int -> Symbol -> Seq Term
go depth startSym = foldMap (\(Rule sym term) -> guard (startSym == sym) >> goTerm depth term) grammar
goTerm :: Int -> GrammarTerm -> Seq Term
goTerm 0 _ = mempty
goTerm depth term = case term of
Cons c ts -> W.Cons c <$> mapM (goTerm depth) ts
AnyString -> return W.Wildcard
StringLiteral t -> return $ W.StringLiteral t
AnyNumber -> return W.Wildcard
NumberLiteral t -> return $ W.NumberLiteral t
NonTerminal t -> go (depth - 1) t
{-
Start Symbol: NF
NF -> Zero()
NF -> Succ(NF)
NF -> Pred(NF)
NF -> Abs(String,Type,Expr)
Expr -> Zero()
Expr -> Succ(Expr)
Expr -> Pred(Expr)
Expr -> Var(String)
Expr -> App(Expr,Expr)
Expr -> Abs(String,Type,Expr)
Expr -> Ifz(Expr,Expr,Expr)
Type -> Num()
Type -> Fun(Type,Type)
-}
pcfEvalGrammar :: Grammar
pcfEvalGrammar =
V.fromList [
Rule nf $ Cons "Zero" [],
Rule nf $ Cons "Succ" [nf'],
Rule nf $ Cons "Pred" [nf'],
Rule nf $ Cons "Abs" [AnyString, typ', expr'],
Rule expr $ Cons "Var" [AnyString],
Rule expr $ Cons "App" [expr',expr'],
Rule expr $ Cons "Abs" [AnyString, typ', expr'],
Rule expr $ Cons "Zero" [],
Rule expr $ Cons "Succ" [expr'],
Rule expr $ Cons "Pred" [expr'],
Rule expr $ Cons "Ifz" [expr', expr', expr'],
Rule typ $ Cons "Num" [],
Rule typ $ Cons "Fun" [typ', typ']
]
where
nf = Symbol 0 "NF"
nf' = NonTerminal nf
expr = Symbol 1 "Expr"
expr' = NonTerminal expr
typ = Symbol 2 "Type"
typ' = NonTerminal typ
{-
Start Symbol: Value
Value -> Num
Value -> Abs(String,Type,Expr)
Num -> Zero()
Num -> Pred(Num)
Num -> Succ(Num)
Expr -> Var(String)
Expr -> App(Expr,Expr)
Expr -> Abs(String,Type,Expr)
Expr -> Zero
Expr -> Succ(Expr)
Expr -> Pred(Expr)
Expr -> Ifz(Expr,Expr,Expr)
Type -> Num()
Type -> Fun(Type,Type)
-}
pcfCheckEvalGrammar :: Grammar
pcfCheckEvalGrammar =
V.fromList [
Rule value num',
Rule value $ Cons "Abs" [AnyString, typ', expr'],
Rule num $ Cons "Zero" [],
Rule num $ Cons "Succ" [num'],
Rule num $ Cons "Pred" [num'],
Rule expr $ Cons "Var" [AnyString],
Rule expr $ Cons "App" [expr',expr'],
Rule expr $ Cons "Abs" [AnyString, typ', expr'],
Rule expr $ Cons "Zero" [],
Rule expr $ Cons "Succ" [expr'],
Rule expr $ Cons "Pred" [expr'],
Rule expr $ Cons "Ifz" [expr', expr', expr'],
Rule typ $ Cons "Num" [],
Rule typ $ Cons "Fun" [typ', typ']
]
where
value = Symbol 0 "Value"
num = Symbol 1 "Num"
num' = NonTerminal num
expr = Symbol 2 "Expr"
expr' = NonTerminal expr
typ = Symbol 3 "Type"
typ' = NonTerminal typ
instance Eq Symbol where
Symbol i _ == Symbol j _ = i == j
instance Ord Symbol where
Symbol i _ <= Symbol j _ = i <= j
Symbol i _ `compare` Symbol j _ = i `compare` j
instance Show Symbol where
show (Symbol _ t) = unpack t
instance Hashable Symbol where
hashWithSalt s (Symbol i _) = s `hashWithSalt` i
instance Show Rule where
show (Rule from to) = show from ++ " -> " ++ show to
instance Show GrammarTerm where
show (Cons c ts) = show c ++ if null ts then "" else show ts
show AnyString = "String"
show (StringLiteral s) = show s
show AnyNumber = "Int"
show (NumberLiteral n) = show n
show (NonTerminal n) = show n
instance Hashable GrammarTerm where
hashWithSalt s (Cons c ts) = s `hashWithSalt` (0::Int) `hashWithSalt` c `hashWithSalt` ts
hashWithSalt s AnyString = s `hashWithSalt` (1::Int)
hashWithSalt s (StringLiteral t) = s `hashWithSalt` (2::Int) `hashWithSalt` t
hashWithSalt s AnyNumber = s `hashWithSalt` (3::Int)
hashWithSalt s (NumberLiteral n) = s `hashWithSalt` (4::Int) `hashWithSalt` n
hashWithSalt s (NonTerminal n) = s `hashWithSalt` (5::Int) `hashWithSalt` n
instance Hashable Rule where
hashWithSalt s (Rule sym term) = s `hashWithSalt` sym `hashWithSalt` term
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
module Main where
import Prelude hiding (log)
import Syntax hiding (Fail)
import qualified WildcardSemantics as W
import qualified Data.AbstractPowerset as W
import qualified Pretty.Haskell as H
-- import qualified Pretty.JavaScript as J
-- import qualified Pretty.PCF as P
import Pretty.Results
import Paths_system_s
import Control.Monad
import qualified Criterion.Measurement as CM
import qualified Criterion.Types as CT
import Data.ATerm
import Data.Foldable
import Data.HashSet (HashSet)
import qualified Data.HashSet as H
import Data.Result
import Data.String
import qualified Data.Text.IO as TIO
import Data.Term (TermUtils)
import qualified Data.Term as T
import System.IO
import Text.PrettyPrint hiding (sep,(<>))
import Text.Printf
main :: IO ()
main = do
CM.initializeTime
prettyPrint H.ppHaskell =<< caseStudy (W.eval 3) "arrows" "desugar_arrow_0_0"
-- activate $ caseStudy "arrows" "desugar_arrow_0_0" 4 $
-- prettyPrint H.ppHaskell <>
-- sizeAnalysis <>
-- heightAnalysis
-- wittnessAnalysis
-- activate $ caseStudy "cca" "norm_0_0" 5 $
-- prettyPrint H.ppHaskell <>
-- sizeAnalysis <>
-- heightAnalysis <>
-- wittnessAnalysis
-- activate $ caseStudy "arith" "eval_0_0" 3 $
-- prettyPrint P.ppPCF <>
-- sizeAnalysis <>
-- heightAnalysis
-- activate $ caseStudy "pcf" "eval_0_0" 4 $
-- prettyPrint P.ppPCF <>
-- sizeAnalysis <>
-- heightAnalysis
-- wittnessAnalysis <>
-- ruleInvocationsAnalysis pcfEvalGrammar <>
-- classification pcfEvalGrammar 4
-- activate $ caseStudy "pcf" "check_eval_0_0" 5 $
-- prettyPrint P.ppPCF <>
-- sizeAnalysis <>
-- heightAnalysis <>
-- wittnessAnalysis <>
-- ruleInvocationsAnalysis pcfCheckEvalGrammar <>
-- classification pcfCheckEvalGrammar 4
-- activate $ caseStudy "go2js" "generate_js_ast_0_0" 4 $
-- prettyPrint J.tryPPJS <>
-- sizeAnalysis <>
-- heightAnalysis <>
-- wittnessAnalysis
prettyPrint :: (W.Term -> Doc) -> HashSet W.Term -> IO ()
prettyPrint pprint res =
if H.size res <= 200
then print $ ppResults pprint (toList res)
else printf "Output ommited because the result set contains %d elements\n" (H.size res)
sizeAnalysisSetup :: (Show t, TermUtils t) => (Analysis t -> IO ()) -> IO ()
sizeAnalysisSetup k =
withFile "size.csv" WriteMode $ \csv -> do
hPrintf csv "name;fun;depth;term;size\n"
k $ \name fun depth res -> measure "Size Analysis" $ forM_ res $ \t ->
hPrintf csv "%s;%s;%d;%s;%d\n" name fun depth (show t) (T.size t)
heightAnalysisSetup :: (Show t, TermUtils t) => (Analysis t -> IO ()) -> IO ()
heightAnalysisSetup k =
withFile "height.csv" WriteMode $ \csv -> do
hPrintf csv "name;fun;depth;term;height\n"
k $ \name fun depth res -> measure "Height Analysis" $ forM_ res $ \t ->
hPrintf csv "%s;%s;%d;%s;%d\n" name fun depth (show t) (T.height t)
-- wittnessAnalysisSetup :: (Analysis t -> IO ()) -> IO ()
-- wittnessAnalysisSetup k =
-- withFile "wittness.csv" WriteMode $ \csv -> do
-- hPrintf csv "name;fun;depth;term;wittness\n"
-- k $ \name fun depth res -> measure "Wittness Analysis" $ forM_ res $ \t ->
-- hPrintf csv "%s;%s;%d;%s;%s\n" name fun depth (show t) (show (U.isWittness (t,res)))
-- ruleInvocationsAnalysisSetup :: ((Grammar -> Analysis t) -> IO ()) -> IO ()
-- ruleInvocationsAnalysisSetup k =
-- withFile "rule.csv" WriteMode $ \csv -> do
-- hPrintf csv "name;fun;depth;term;ruleId;rule;invocation\n"
-- k $ \grammar name fun depth res -> measure "Rule Invocations Analysis" $ forM_ res $ \t ->
-- case summary grammar t of
-- Just s -> forM_ (M.toList s `zip` [(1::Int)..]) $ \((rule,count),ruleId) ->
-- hPrintf csv "%s;%s;%d;%s;%d;%s;%d\n" name fun depth (show t) ruleId (show rule) count
-- Nothing -> return ()
-- type Distance = Int
-- | Classifies terms as true and false, positive or negatives.
--
-- True-Positive: Terms in the analysis result that are part of the output language of the program transformation
-- False-Positive: Terms in the analysis result that are *not* part of the output language of the program transformation
-- True-Negative: Terms that occur neither in the output language of the program transformation nor in the analysis result
-- False-Negative: Terms in output language of the program transformation that do not occur in the analysis result
-- classificationSetup :: ((Grammar -> Distance -> Analysis t) -> IO ()) -> IO ()
-- classificationSetup k =
-- withFile "classification.csv" WriteMode $ \csv -> do
-- hPrintf csv "name;fun;depth;sample_distance;term;height;size;distance_sum;class\n"
-- k $ \grammar sampleDistance name fun depth analysis -> measure "Classification" $ do
-- let relevant = termsOfDistance sampleDistance grammar
-- selected = H.delete W.Wildcard analysis
-- (truePositive,falsePositive) = partition (\s -> any (\r -> s `wittnesses` r) relevant) selected
-- (_, falseNegative) = partition (\r -> any (\s -> s `wittnesses` r) selected) relevant
-- forM_ [("true_positive", truePositive), ("false_positive", falsePositive), ("false_negative", falseNegative)] $ \(klass,terms) ->
-- forM_ terms $ \t ->
-- hPrintf csv "%s;%s;%d;%d;%s;%d;%d;%d;%s\n"
-- name fun depth sampleDistance (show t) (T.height t) (T.size t) (distanceSum grammar t `orElse` 0) (klass :: String)
-- where
-- partition :: (Eq a, Hashable a) => (a -> Bool) -> HashSet a -> (HashSet a, HashSet a)
-- partition predicate = H.foldl' (\(pos,neg) t -> if predicate t then (H.insert t pos,neg) else (pos,H.insert t neg))
-- (H.empty,H.empty)
-- wittnesses :: W.Term -> W.Term -> Bool
-- wittnesses W.Wildcard W.Wildcard = True
-- wittnesses W.Wildcard (W.Cons _ []) = True
-- wittnesses W.Wildcard (W.StringLiteral _) = True
-- wittnesses W.Wildcard (W.NumberLiteral _) = True
-- wittnesses (W.Cons c ts) (W.Cons c' ts') = c == c' && length ts == length ts' && and (zipWith wittnesses ts ts')
-- wittnesses (W.StringLiteral s) (W.StringLiteral s') = s == s'
-- wittnesses (W.NumberLiteral n) (W.NumberLiteral n') = n == n'
-- wittnesses _ _ = False
-- for :: Functor f => f a -> (a -> b) -> f b
-- for = flip fmap
-- orElse :: Maybe a -> a -> a
-- orElse = flip fromMaybe
measure :: String -> IO () -> IO ()
measure analysisName action = do
(m,_) <- CM.measure (CT.nfIO action) 1
printf "- %s: %s\n" analysisName (CM.secs (CT.measCpuTime m))
type Analysis t = String -> String -> Int -> HashSet t -> IO ()
caseStudy :: (Strat -> StratEnv -> W.TermEnv -> W.Term -> W.Pow (Result (W.Term,W.TermEnv))) -> 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)
case parseModule =<< parseATerm file of
Left e -> fail (show e)
Right module_ -> do
let res = eval (Call (fromString function) [] []) (stratEnv module_) W.emptyEnv W.Wildcard
let terms = H.fromList $ toList $ filterResults (toList res)
_ <- CM.measure (CT.nfIO (return terms)) 1
return terms
where
filterResults = fmap (\r -> case r of Success (t,_) -> t; Fail -> error "")
. filter (\r -> case r of Success _ -> True; _ -> False)
{-# LANGUAGE OverloadedStrings #-}
module Pretty.Haskell where
import WildcardSemantics
import qualified Data.Text as T
import Text.PrettyPrint hiding (sep)
ppHaskell :: Term -> Doc
ppHaskell t = case t of
Cons "ArrProcedure" [pat,cmd] ->
text "proc " <> ppHaskell pat <> text " -> " <> ppHaskell cmd
Cons "OpApp" [l,StringLiteral o,r] ->
parens $ ppHaskell l <> space <> text (T.unpack o) <> space <> ppHaskell r
Cons "AppBin" [f,x@(Cons "AppBin" _)] ->
ppHaskell f <> space <> parens (ppHaskell x)
Cons "AppBin" [f,x] ->
ppHaskell f <> space <> ppHaskell x
Cons "Var" [StringLiteral x] -> text (T.unpack x)
Cons "Var" [Wildcard] -> ppWildcard
Cons "Abs" [args, body] ->
parens $ char '\\' <> ppSepList space args <> text " -> " <> ppHaskell body
Cons "Let" [bnds, body] ->
text "let " <> braces (ppLetBindings bnds) <>
text " in " <> ppHaskell body
Cons "If" [e1,e2,e3] ->
text "if " <> ppHaskell e1 <>
text " then " <> ppHaskell e2 <>
text " else " <> ppHaskell e3
Cons "Constr" [Cons "Unit" []] -> "()"
Cons "Constr" [StringLiteral t'] -> text (T.unpack t')
Cons "Product" [t'] -> parens (ppSepList comma t')
Cons "Tuple" [t1,t2] -> parens (ppHaskell t1 <> comma <> space <> ppSepList (comma <> space) t2)
Wildcard -> ppWildcard
_ -> error $ "unexpected haskell expression: " ++ show t
ppLetBindings :: Term -> Doc
ppLetBindings t = case t of
Wildcard -> ppWildcard
_ -> error $ "unexpected term: " ++ show t
ppSepList :: Doc -> Term -> Doc
ppSepList sep t = case t of
Cons "ECons" [x, Cons "Nil" []] -> ppHaskell x
Cons "ECons" [x, xs] -> ppHaskell x <> sep <> ppSepList sep xs
Cons "Cons" [x, Cons "Nil" []] -> ppHaskell x
Cons "Cons" [x, xs] -> ppHaskell x <> sep <> ppSepList sep xs
Cons "Nil" [] -> mempty
Wildcard -> ppWildcard
_ -> error $ "unexpected term: " ++ show t
ppWildcard :: Doc
ppWildcard = char '*'
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Pretty.JavaScript where
import WildcardSemantics
import Text.PrettyPrint hiding (sep)
-- import Control.Exception
-- import System.IO.Unsafe
-- import Control.DeepSeq
import qualified Data.Text as T
{-# NOINLINE tryPPJS #-}
tryPPJS :: Term -> Doc
tryPPJS t = text (show t)
--unsafePerformIO $ catch (evaluate (force (ppJS t))) (\(msg :: ErrorCall) -> error $ "cannot pretty print term " ++ show t ++ "\nError: " ++ show msg)
ppJS :: Term -> Doc
ppJS t = case t of
Cons "Program" [stmts] -> ppStatements stmts
Cons "Array" _ -> ppExp t
Cons "Call" _ -> ppExp t
Cons "Division" _ -> ppExp t
Cons "Substraction" _ -> ppExp t
Cons "Addition" _ -> ppExp t
Cons "Multiplication" _ -> ppExp t
Cons "Cons" [x,xs] -> ppJS x $$ ppJS xs
Cons "Nil" [] -> mempty
Cons "" [a,b] -> parens (ppJS a <> char ',' <> ppJS b)
Wildcard -> ppWildcard
_ -> error $ "unexpected term while pprinting javascript: " ++ show t
ppStatements :: Term -> Doc
ppStatements = ppSepList ppStatement ($$)
ppStatement :: Term -> Doc
ppStatement t = case t of
Cons "expStmt" [ident] -> ppIdentifier ident
Cons "varDecl" [ident, e] -> text "var" <+> ppIdentifier ident <+> char '=' <+> ppJS e <> char ';'
Cons "method" [ident, params, body] -> text "function" <+> ppIdentifier ident <> parens (ppParams params) <> braces (ppJS body)
Wildcard -> ppWildcard