Skip to content

Commit

Permalink
Fixing a few translation problems
Browse files Browse the repository at this point in the history
  • Loading branch information
scottgw committed Mar 31, 2012
1 parent 4574b61 commit 41a7b26
Show file tree
Hide file tree
Showing 4 changed files with 137 additions and 60 deletions.
8 changes: 6 additions & 2 deletions ClassEnv.hs
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -9,14 +9,18 @@ import Language.Eiffel.TypeCheck.Class
import Language.Eiffel.TypeCheck.TypedExpr as T import Language.Eiffel.TypeCheck.TypedExpr as T


newtype ClassEnv body expr = ClassEnv (Map String (AbsClas body expr)) newtype ClassEnv body expr = ClassEnv (Map String (AbsClas body expr))
deriving Show


type TInterEnv = ClassEnv EmptyBody T.TExpr type TInterEnv = ClassEnv EmptyBody T.TExpr
type InterEnv = ClassEnv EmptyBody Expr type InterEnv = ClassEnv EmptyBody Expr



makeEnv :: [AbsClas body expr] -> ClassEnv body expr makeEnv :: [AbsClas body expr] -> ClassEnv body expr
makeEnv = ClassEnv . Map.fromList . map (\c -> (map toLower (className c), c)) makeEnv = ClassEnv . Map.fromList . map (\c -> (map toLower (className c), c))


-- |All keys' class-names in the class environment
envKeys :: ClassEnv body expr -> [String]
envKeys (ClassEnv m) = Map.keys m



-- |Lookup a class name in the environment. This name should be lower-case, -- |Lookup a class name in the environment. This name should be lower-case,
-- and the function takes care of common type synonyms -- and the function takes care of common type synonyms
Expand All @@ -28,4 +32,4 @@ envLookup name e@(ClassEnv m) =
] ]
in case lookup name translate of in case lookup name translate of
Just alias -> Map.lookup alias m Just alias -> Map.lookup alias m
Nothing -> Map.lookup name m Nothing -> Map.lookup (map toLower name) m
2 changes: 1 addition & 1 deletion DepGen.hs
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ depFeatures c acc = foldM depFeature acc (allFeatures c)
depAttrs :: ClasInterface -> [ClassOrGeneric] -> DepM [ClassOrGeneric] depAttrs :: ClasInterface -> [ClassOrGeneric] -> DepM [ClassOrGeneric]
depAttrs c = depDecls (map attrDecl $ allAttributes c) depAttrs c = depDecls (map attrDecl $ allAttributes c)


depFeature :: [ClassOrGeneric] -> FeatureEx -> DepM [ClassOrGeneric] depFeature :: [ClassOrGeneric] -> FeatureEx Expr -> DepM [ClassOrGeneric]
depFeature acc f = depFeature acc f =
let fSig = Decl (featureName f) (featureResult f) let fSig = Decl (featureName f) (featureResult f)
allDecls = fSig : featureArgs f allDecls = fSig : featureArgs f
Expand Down
57 changes: 33 additions & 24 deletions Domain.hs
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ thisDecl cls = D.Decl "this" (StructType (className cls) undefined)
fromClause :: E.Clause TExpr -> D.Clause D.Expr fromClause :: E.Clause TExpr -> D.Clause D.Expr
fromClause (E.Clause tagMb expr) = fromClause (E.Clause tagMb expr) =
let tag = fromMaybe "no_tag" tagMb let tag = fromMaybe "no_tag" tagMb
in D.Clause tag (teToD expr) in D.Clause tag (teToDCurr expr)


fromRoutine :: AbsClas body TExpr -> AbsRoutine abs TExpr -> Either ProcedureU ProcedureU fromRoutine :: AbsClas body TExpr -> AbsRoutine abs TExpr -> Either ProcedureU ProcedureU
fromRoutine clas rtn = fromRoutine clas rtn =
Expand All @@ -56,32 +56,41 @@ fromRoutine clas rtn =
E.NoType -> Left prcd E.NoType -> Left prcd
_ -> Right prcd _ -> Right prcd


teToD :: TExpr -> D.Expr teToDCurr = teToD (D.Var "this")
teToD te = go (contents te)
teToD :: D.Expr -> TExpr -> D.Expr
teToD curr' te = go curr' (contents te)
where where
go (T.Call trg name args _) = D.Call name (teToD trg : map teToD args) go' curr = go curr . contents
go (T.Access trg name _) = D.Access (teToD trg) name
go (T.EqExpr op e1 e2) = D.BinOpExpr (dEqOp op) (teToD e1) (teToD e2) go :: D.Expr -> UnPosTExpr -> D.Expr
go (T.Old e) = D.UnOpExpr D.Old (teToD e) go curr (T.Call trg name args _) =
go (T.CurrentVar _) = D.Var "this" let dtrg = go' curr trg
go (T.Attached _ e _) = ClassType cn _ = texpr trg
in D.Call (cn ++ "_" ++ name) (dtrg : map (go' dtrg) args)
go curr (T.Access trg name _) = D.Access (go' curr trg) name
go curr (T.EqExpr op e1 e2) =
D.BinOpExpr (dEqOp op) (go' curr e1) (go' curr e2)
go curr (T.Old e) = D.UnOpExpr D.Old (go' curr e)
go curr (T.CurrentVar _) = curr
go curr (T.Attached _ e _) =
let ClassType cn _ = texprTyp (contents e) let ClassType cn _ = texprTyp (contents e)
structType = D.StructType cn [] structType = D.StructType cn []
in D.BinOpExpr (D.RelOp D.Neq structType) (teToD e) D.LitNull in D.BinOpExpr (D.RelOp D.Neq structType) (go' curr e) D.LitNull
go (T.Box _ e) = teToD e go curr (T.Box _ e) = go' curr e
go (T.Unbox _ e) = teToD e go curr (T.Unbox _ e) = go' curr e
go (T.Cast _ e) = teToD e go curr (T.Cast _ e) = go' curr e
go (T.Var n _) = D.Var n go _curr (T.Var n _) = D.Var n
go (T.ResultVar _) = D.ResultVar go _curr (T.ResultVar _) = D.ResultVar
go (T.LitInt i) = D.LitInt i go _curr (T.LitInt i) = D.LitInt i
go (T.LitBool b) = D.LitBool b go _curr (T.LitBool b) = D.LitBool b
go (T.LitVoid _) = D.LitNull go _curr (T.LitVoid _) = D.LitNull
go (T.LitChar _) = error "teToD: unimplemented LitChar" go _curr (T.LitChar _) = error "teToD: unimplemented LitChar"
go (T.LitString _) = error "teToD: unimplemented LitString" go _curr (T.LitString _) = error "teToD: unimplemented LitString"
go (T.LitDouble _) = error "teToD: unimplemented LitDouble" go _curr (T.LitDouble _) = error "teToD: unimplemented LitDouble"
go (T.Agent _ _ _ _) = error "teToD: unimplemented Agent" go _curr (T.Agent _ _ _ _) = error "teToD: unimplemented Agent"
go (T.Tuple _) = error "teToD: unimplemented Tuple" go _curr (T.Tuple _) = error "teToD: unimplemented Tuple"
go (T.LitArray _) = error "teToD: unimplemented LitArray" go _curr (T.LitArray _) = error "teToD: unimplemented LitArray"


dEqOp o = D.RelOp (rel o) D.NoType dEqOp o = D.RelOp (rel o) D.NoType
where where
Expand Down
130 changes: 97 additions & 33 deletions Main.hs
Original file line number Original file line Diff line number Diff line change
@@ -1,9 +1,16 @@
module Main where module Main where


import Data.Either import Control.Applicative

import Data.Binary
import qualified Data.ByteString.Lazy as BS
import Data.List import Data.List

import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Map (Map) import qualified Data.Set as Set
import Data.Set (Set)


import Data.Maybe import Data.Maybe


import Language.Eiffel.Parser.Parser import Language.Eiffel.Parser.Parser
Expand All @@ -13,6 +20,8 @@ import Language.Eiffel.Position
import qualified Language.Eiffel.PrettyPrint as PP import qualified Language.Eiffel.PrettyPrint as PP


import Language.Eiffel.TypeCheck.Class import Language.Eiffel.TypeCheck.Class
import Language.Eiffel.TypeCheck.Expr (flatten)
import Language.Eiffel.TypeCheck.Context
import Language.Eiffel.TypeCheck.TypedExpr as T import Language.Eiffel.TypeCheck.TypedExpr as T


import qualified Language.DemonL.AST as D import qualified Language.DemonL.AST as D
Expand All @@ -26,31 +35,48 @@ import DepGen
import Domain import Domain
import GenerateSummaries import GenerateSummaries


main :: IO ()
main = do getDomain file = do
currDir <- getCurrentDirectory classEi <- parseClassFile file
let testDir = currDir </> "test"
-- print searchDirectories
-- files <- collectFileMap (testDir : searchDirectories)
-- print files
classEi <- parseClassFile (testDir </> "work_queue.e")
case classEi of case classEi of
Left e -> print e Left err -> error $ "getDomain: " ++ show err
Right cls -> do Right cls -> do
classInts <- Map.elems `fmap` readAllSummaries -- depGenInt files (className cls) classInts <- Map.elems `fmap` readAllSummaries
putStrLn "Generated dependencies" case depGen (makeEnv classInts) "work_queue" of
-- let unliked = rights (map (unlikeInterfaceM classInts) classInts) Left err -> error $ "getDomain: " ++ show err
let domainInts = either (error . show) id $ depGen (makeEnv classInts) "work_queue" Right domainInts ->
print (map className domainInts) case clasM classInts cls of
case clasM classInts cls of Left err -> error $ "getDomain: " ++ err
Left e -> print e Right tCls -> do
Right typedClass -> typeInterfaces domainInts >>= \ typedDomain -> tis <- typeInterfaces domainInts
case typedDomain of return (tis, tCls)
Left err -> print err
Right typedInts ->
print (PP.toDoc $ untype $ getDomainFile file = do
instrument (makeEnv typedInts) "dequeue" typedClass) classEi <- parseClassFile file
case classEi of
Left err -> error $ "getDomain: " ++ show err
Right cls -> do
classInts <- Map.elems `fmap` readAllSummaries
domainInts <- readDomain
case clasM classInts cls of
Left err -> error $ "getDomain: " ++ err
Right tCls -> return (domainInts, tCls)

readDomain :: IO ([AbsClas EmptyBody T.TExpr])
readDomain = decode <$> BS.readFile "typed_domain.tdom"


writeDomain file = do
(Right tis, _) <- getDomain file
BS.writeFile "typed_domain.tdom" $ encode tis

main :: IO ()
main = do
currDir <- getCurrentDirectory
let testFile = currDir </> "test" </> "work_queue.e"
(typedDomain, typedClass) <- getDomainFile testFile
print (PP.toDoc $ untype $
instrument (makeEnv typedDomain) "dequeue" typedClass)


instrument :: TInterEnv -> String -> AbsClas (RoutineBody TExpr) TExpr instrument :: TInterEnv -> String -> AbsClas (RoutineBody TExpr) TExpr
-> AbsClas (RoutineBody TExpr) TExpr -> AbsClas (RoutineBody TExpr) TExpr
Expand All @@ -68,7 +94,7 @@ instrumentBody :: TInterEnv -> Contract TExpr
-> RoutineBody TExpr -> RoutineBody TExpr -> RoutineBody TExpr -> RoutineBody TExpr
instrumentBody env ens (RoutineBody locals localProc body) = instrumentBody env ens (RoutineBody locals localProc body) =
let let
ensD = map (teToD . clauseExpr) (contractClauses ens) ensD = map (teToDCurr . clauseExpr) (contractClauses ens)
body' = snd $ stmt env [] ensD body body' = snd $ stmt env [] ensD body
in RoutineBody locals localProc body' in RoutineBody locals localProc body'
instrumentBody _ _ r = r instrumentBody _ _ r = r
Expand All @@ -94,7 +120,7 @@ block (cs, s) = (cs, Block s)


replaceClause :: [D.Expr] -> TExpr -> TExpr -> [D.Expr] replaceClause :: [D.Expr] -> TExpr -> TExpr -> [D.Expr]
replaceClause clauses old new = replaceClause clauses old new =
map (replaceExpr (teToD old) (teToD new)) clauses map (replaceExpr (teToDCurr old) (teToDCurr new)) clauses


replaceExpr :: D.Expr -> D.Expr -> D.Expr -> D.Expr replaceExpr :: D.Expr -> D.Expr -> D.Expr -> D.Expr
replaceExpr new old = go replaceExpr new old = go
Expand All @@ -111,7 +137,7 @@ dNeqNull :: Pos UnPosTExpr -> D.Expr
dNeqNull e = dNeqNull e =
let ClassType cn _ = texprTyp (contents e) let ClassType cn _ = texprTyp (contents e)
structType = D.StructType cn [] structType = D.StructType cn []
in D.BinOpExpr (D.RelOp D.Neq structType) (teToD e) D.LitNull in D.BinOpExpr (D.RelOp D.Neq structType) (teToDCurr e) D.LitNull


dConj :: [D.Expr] -> D.Expr dConj :: [D.Expr] -> D.Expr
dConj = foldr1 (D.BinOpExpr D.And) dConj = foldr1 (D.BinOpExpr D.And)
Expand All @@ -123,23 +149,38 @@ texprClassName e =


texprInterface :: TInterEnv -> TExpr -> AbsClas EmptyBody T.TExpr texprInterface :: TInterEnv -> TExpr -> AbsClas EmptyBody T.TExpr
texprInterface env e = texprInterface env e =
fromMaybe (error $ "texprInterface: " ++ show e) fromMaybe (error $ "texprInterface: " ++ show e ++ "," ++ show (envKeys env))
(envLookup (texprClassName e) env) (envLookup (texprClassName e) env)


flatten' :: TInterEnv -> Typ -> AbsClas EmptyBody T.TExpr
flatten' (ClassEnv e) typ =
case idErrorRead (flatten typ) (mkCtx typ (Map.elems e)) of
Left e -> error $ "flatten': " ++ e
Right c -> classMapExprs updRoutine id id c
where
updRoutine r = r { routineReq = updContract (routineReq r)
, routineEns = updContract (routineEns r)
}
updContract = mapContract (\cl -> cl {clauseExpr = go' (clauseExpr cl)})

go' e = attachPos (position e) (go $ contents e)
go (T.Call trg n args t) = T.Call (go' trg) n (map go' args) t
go (T.CurrentVar t) = T.CurrentVar typ

texprPre :: TInterEnv -> TExpr -> String -> [T.TExpr] texprPre :: TInterEnv -> TExpr -> String -> [T.TExpr]
texprPre env targ name = texprPre env targ name =
let iface = texprInterface env targ let iface = flatten' env (texpr targ)
in case findFeature iface name of in case findFeatureEx iface name of
Just rout -> map clauseExpr (contractClauses (routineReq rout)) Just feat -> map clauseExpr (featurePre feat)
Nothing -> error $ "texprPre: can't find routine" Nothing -> error $ "texprPre: can't find feature: " ++ show targ ++ "." ++ name


preCond :: TInterEnv -> TExpr -> [D.Expr] preCond :: TInterEnv -> TExpr -> [D.Expr]
preCond env ex = go (contents ex) preCond env ex = go (contents ex)
where where
go' = go . contents go' = go . contents
go (T.Call trg name args _) = go (T.Call trg name args _) =
let callPreTExpr = texprPre env trg name let callPreTExpr = texprPre env trg name
callPres = map teToD callPreTExpr callPres = map (teToD (teToDCurr trg)) callPreTExpr
in dNeqNull trg : concatMap go' (trg : args) ++ callPres in dNeqNull trg : concatMap go' (trg : args) ++ callPres
go (T.Access trg _ _) = dNeqNull trg : go' trg go (T.Access trg _ _) = dNeqNull trg : go' trg
go (T.Old e) = go' e go (T.Old e) = go' e
Expand Down Expand Up @@ -225,3 +266,26 @@ stmt' env decls ens = go
(fromCls, from') = stmt env decls bodyCls from (fromCls, from') = stmt env decls bodyCls from
in meldCall decls fromCls (Loop from' untl inv body' var) in meldCall decls fromCls (Loop from' untl inv body' var)
go e = error ("stmt'go: " ++ show e) go e = error ("stmt'go: " ++ show e)


data Indicator = Indicator Typ String deriving (Eq, Ord)
data Action = Action Typ String deriving (Eq, Ord)


domActions :: TInterEnv -> T.TExpr -> Set Action
domActions env e =
let pairs = typeCallPairs e
cls = texprInterface env e
post = undefined
-- Desired interface:
domActions' :: TInterEnv -> Set Indicator -> Set Action
domActions' = undefined
in error "domActions"

typeCallPairs :: T.TExpr -> Set Indicator
typeCallPairs = go'
where go' = go . contents
go (T.Call trg name args t) =
let argPairs = Set.unions (map typeCallPairs (trg : args))
in Set.insert (Indicator (texpr trg) name) argPairs
go _ = Set.empty

0 comments on commit 41a7b26

Please sign in to comment.