clafer-0.3.10: src/Language/Clafer/Generator/Alloy.hs
{-# LANGUAGE RankNTypes, FlexibleContexts #-}
{-
Copyright (C) 2012-2013 Kacper Bak, Jimmy Liang, Rafael Olaechea <http://gsd.uwaterloo.ca>
Permission is hereby granted, free of charge, to any person obtaining a copy of
this software and associated documentation files (the "Software"), to deal in
the Software without restriction, including without limitation the rights to
use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
of the Software, and to permit persons to whom the Software is furnished to do
so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
-}
-- | Generates Alloy4.1 or 4.2 code for a Clafer model
module Language.Clafer.Generator.Alloy (genModule) where
import Control.Applicative
import Control.Monad.State
import Data.List
import Data.Maybe
import Prelude
import Language.Clafer.Common
import Language.Clafer.ClaferArgs
import Language.Clafer.Front.AbsClafer
import Language.Clafer.Generator.Concat
import Language.Clafer.Intermediate.Intclafer hiding (exp)
data GenEnv = GenEnv
{ claferargs :: ClaferArgs
, uidIClaferMap :: UIDIClaferMap
, forScopes :: String
} deriving (Show)
-- | Alloy code generation
-- 07th Mayo 2012 Rafael Olaechea
-- Added Logic to print a goal block in case there is at least one goal.
genModule :: ClaferArgs -> (IModule, GEnv) -> [(UID, Integer)] -> (Result, [(Span, IrTrace)])
genModule claferargs' (imodule, genv) scopes = (flatten output, filter ((/= NoTrace) . snd) $ mapLineCol output)
where
genScopes :: [(UID, Integer)] -> String
genScopes [] = ""
genScopes scopes' = " but " ++ intercalate ", " (map (\ (uid', scope) -> show scope ++ " " ++ uid') scopes')
forScopes' = "for 1" ++ genScopes scopes
genEnv = GenEnv claferargs' (uidClaferMap genv) forScopes'
output = header genEnv +++ (cconcat $ map (genDeclaration genEnv) (_mDecls imodule)) +++
if ((not $ skip_goals claferargs') && length goals_list > 0) then
CString "objectives o_global {\n" +++ (cintercalate (CString ",\n") goals_list) +++ CString "\n}"
else
CString ""
where
goals_list = filterNull (map (genDeclarationGoalsOnly genEnv) (_mDecls imodule))
header :: GenEnv -> Concat
header genEnv = CString $ unlines
[ "open util/integer"
, "pred show {}"
, if (validate $ claferargs genEnv) || (noalloyruncommand $ claferargs genEnv)
then ""
else "run show " ++ forScopes genEnv
, ""]
-- 07th Mayo 2012 Rafael Olaechea
-- Modified so that we can collect all goals into a single block as required per the way goals are handled in modified alloy.
genDeclarationGoalsOnly :: GenEnv -> IElement -> Concat
genDeclarationGoalsOnly genEnv x = case x of
IEClafer _ -> CString ""
IEConstraint _ _ -> CString ""
IEGoal _ (PExp _ _ _ innerexp) -> case innerexp of
IFunExp op' exps' -> if op' == iGMax || op' == iGMin then
mkMetric op' $ genPExp genEnv [] (head exps')
else
error "unary operator distinct from (min/max) at the topmost level of a goal element"
_ -> error "no unary operator (min/max) at the topmost level of a goal element."
-- 07th Mayo 2012 Rafael Olaechea
-- Removed goal from this function as they will now all be collected into a single block.
genDeclaration :: GenEnv -> IElement -> Concat
genDeclaration genEnv x = case x of
IEClafer clafer' -> (genClafer genEnv [] clafer') +++ (mkFact $ cconcat $ genSetUniquenessConstraint clafer')
IEConstraint True pexp -> mkFact $ genPExp genEnv [] pexp
IEConstraint False pexp -> mkAssert genEnv (genAssertName pexp) $ genPExp genEnv [] pexp
IEGoal _ (PExp _ _ _ innerexp) -> case innerexp of
IFunExp op' _ -> if op' == iGMax || op' == iGMin then
CString ""
else
error "unary operator distinct from (min/max) at the topmost level of a goal element"
_ -> error "no unary operator (min/max) at the topmost level of a goal element."
mkFact :: Concat -> Concat
mkFact x@(CString "") = x
mkFact xs = cconcat [CString "fact ", mkSet xs, CString "\n"]
genAssertName :: PExp -> Concat
genAssertName PExp{_inPos=(Span _ (Pos line _))} = CString $ "assertOnLine_" ++ show line
mkAssert :: GenEnv -> Concat -> Concat -> Concat
mkAssert _ _ x@(CString "") = x
mkAssert genEnv name xs = cconcat
[ CString "assert ", name, CString " "
, mkSet xs
, CString "\n"
, CString "check ", name, CString " "
, CString $ forScopes genEnv
, CString "\n\n"
]
mkMetric :: String -> Concat -> Concat
mkMetric goalopname xs = cconcat [ if goalopname == iGMax then CString "maximize" else CString "minimize", CString " ", xs, CString " "]
mkSet :: Concat -> Concat
mkSet xs = cconcat [CString "{ ", xs, CString " }"]
showSet :: Concat -> [Concat] -> Concat
showSet delim xs = showSet' delim $ filterNull xs
where
showSet' _ [] = CString "{}"
showSet' delim' xs' = mkSet $ cintercalate delim' xs'
optShowSet :: [Concat] -> Concat
optShowSet [] = CString ""
optShowSet xs = CString "\n" +++ showSet (CString "\n ") xs
-- optimization: top level cardinalities
-- optimization: if only boolean parents, then set card is known
genClafer :: GenEnv -> [String] -> IClafer -> Concat
genClafer genEnv resPath clafer'
= (cunlines $ filterNull
[ cardFact
+++ claferDecl clafer' (
(showSet (CString "\n, ") $ genRelations genEnv clafer')
+++ (optShowSet $ filterNull $ genConstraints genEnv resPath clafer')
)
]
)
+++ CString "\n"
+++ children'
where
children' = cconcat $ filterNull $ map
(genClafer genEnv ((_uid clafer') : resPath)) $
getSubclafers $ _elements clafer'
cardFact
| null resPath && (null $ flatten $ genOptCard clafer') =
case genCard (_uid clafer') $ _card clafer' of
CString "set" -> CString ""
c -> mkFact c
| otherwise = CString ""
claferDecl :: IClafer -> Concat -> Concat
claferDecl c rest = cconcat
[ genOptCard c
, CString $ genAbstract $ _isAbstract c
, CString "sig "
, Concat NoTrace [CString $ _uid c, genExtends $ _super c, CString "\n", rest]
]
where
genAbstract isAbs = if isAbs then "abstract " else ""
genExtends Nothing = CString ""
genExtends (Just (PExp _ _ _ (IClaferId _ i _ _))) = CString " " +++ Concat NoTrace [CString $ "extends " ++ i]
-- todo: handle multiple inheritance
genExtends _ = CString ""
genOptCard :: IClafer -> Concat
genOptCard c
| glCard' `elem` ["lone", "one", "some"] = cardConcat (_uid c) False [CString glCard'] +++ (CString " ")
| otherwise = CString ""
where
glCard' = genIntervalCrude $ _glCard c
-- -----------------------------------------------------------------------------
-- overlapping inheritance is a new clafer with val (unlike only relation)
-- relations: overlapping inheritance (val rel), children
-- adds parent relation
-- 29/March/2012 Rafael Olaechea: ref is now prepended with clafer name to be able to refer to it from partial instances.
genRelations :: GenEnv -> IClafer -> [Concat]
genRelations genEnv c = maybeToList r ++ (map mkRel $ getSubclafers $ _elements c)
where
r = if isJust $ _reference c
then
Just $ Concat NoTrace [CString $ genRel (if (noalloyruncommand $ claferargs genEnv) then (_uid c ++ "_ref") else "ref")
c {_card = Just (1, 1)} $
flatten $ refType genEnv c]
else
Nothing
mkRel c' = Concat NoTrace [CString $ genRel (genRelName $ _uid c') c' $ _uid c']
genRelName :: String -> String
genRelName name = "r_" ++ name
genRel :: String -> IClafer -> String -> String
genRel name c rType = genAlloyRel name (genCardCrude $ _card c) rType'
where
rType' = if isPrimitive rType then "Int" else rType
genAlloyRel :: String -> String -> String -> String
genAlloyRel name card' rType = concat [name, " : ", card', " ", rType]
refType :: GenEnv -> IClafer -> Concat
refType genEnv c = fromMaybe (CString "") $ fmap ((genType genEnv).getTarget) $ _ref <$> _reference c
getTarget :: PExp -> PExp
getTarget x = case x of
PExp _ _ _ (IFunExp op' (_:pexp:_)) -> if op' == iJoin then pexp else x
_ -> x
genType :: GenEnv -> PExp -> Concat
genType genEnv x@(PExp _ _ _ y@(IClaferId _ _ _ _)) = genPExp genEnv []
x{_exp = y{_isTop = True}}
genType m x = genPExp m [] x
-- -----------------------------------------------------------------------------
-- constraints
-- parent + group constraints + reference + user constraints
-- a = NUMBER do all x : a | x = NUMBER (otherwise alloy sums a set)
genConstraints :: GenEnv -> [String] -> IClafer -> [Concat]
genConstraints genEnv resPath c
= (genParentConst resPath c)
: (genGroupConst genEnv c)
{- genPathConst produces incorrect code for top-level clafers
abstract System
abstract Connection
connections -> Connection *
sig c0_connections
{ ref : one c0_Connection }
{ one @r_c0_connections.this
ref = (@r_c0_System.@r_c0_Connection) }
r_c0_System does not exist because System is top-level. The constraint is useless anyway, since all instances
of Connection are nested under all Systems anyway.
disabled code:
: genPathConst genEnv (if (noalloyruncommand $ claferargs genEnv) then (_uid c ++ "_ref") else "ref") resPath c
-}
: constraints
where
constraints = concat $ map genConst $ _elements c
genConst x = case x of
IEConstraint True pexp -> [ genPExp genEnv ((_uid c) : resPath) pexp ]
IEConstraint False pexp -> [ CString "// Assertion " +++ (genAssertName pexp) +++ CString " ignored since nested assertions are not supported in Alloy.\n"]
IEClafer c' ->
(if genCardCrude (_card c') `elem` ["one", "lone", "some"]
then CString ""
else mkCard ({- do not use the genRelName as the constraint name -} _uid c') False (genRelName $ _uid c') $ fromJust (_card c')
)
: (genParentSubrelationConstriant (uidIClaferMap genEnv) c')
: (genSetUniquenessConstraint c')
IEGoal _ _ -> error "getConst function from Alloy generator was given a Goal, this function should only be given a Constrain or Clafer" -- This should never happen
genSetUniquenessConstraint :: IClafer -> [Concat]
genSetUniquenessConstraint c =
(case _reference c of
Just (IReference True _) ->
(case _card c of
Just (lb, ub) -> if (lb > 1 || ub > 1 || ub == -1)
then [ CString $ (
(case isTopLevel c of
False -> "all disj x, y : this.@" ++ (genRelName $ _uid c)
True -> " all disj x, y : " ++ (_uid c)))
++ " | (x.@ref) != (y.@ref) "
]
else []
_ -> [])
_ -> []
)
genParentSubrelationConstriant :: UIDIClaferMap -> IClafer -> Concat
genParentSubrelationConstriant uidIClaferMap' headClafer =
case match of
Nothing -> CString ""
Just NestedInheritanceMatch {
_superClafer = superClafer
} -> if (isProperNesting uidIClaferMap' match) && (not $ isTopLevel superClafer)
then CString $ concat
[ genRelName $ _uid headClafer
, " in "
, genRelName $ _uid superClafer
]
else CString ""
where
match = matchNestedInheritance uidIClaferMap' headClafer
-- optimization: if only boolean features then the parent is unique
genParentConst :: [String] -> IClafer -> Concat
genParentConst [] _ = CString ""
genParentConst _ c = genOptParentConst c
genOptParentConst :: IClafer -> Concat
genOptParentConst c
| glCard' == "one" = CString ""
| glCard' == "lone" = Concat NoTrace [CString $ "one " ++ rel]
| otherwise = Concat NoTrace [CString $ "one @" ++ rel ++ ".this"]
-- eliminating problems with cyclic containment;
-- should be added to cases when cyclic containment occurs
-- , " && no iden & @", rel, " && no ~@", rel, " & @", rel]
where
rel = genRelName $ _uid c
glCard' = genIntervalCrude $ _glCard c
genGroupConst :: GenEnv -> IClafer -> Concat
genGroupConst genEnv clafer'
| _isAbstract clafer' || null children' || flatten card' == "" = CString ""
| otherwise = cconcat [CString "let children = ", brArg id $ CString children', CString" | ", card']
where
superHierarchy :: [IClafer]
superHierarchy = findHierarchy getSuper (uidIClaferMap genEnv) clafer'
children' = intercalate " + " $ map (genRelName._uid) $
getSubclafers $ concatMap _elements superHierarchy
card' = mkCard (_uid clafer') True "children" $ _interval $ fromJust $ _gcard $ clafer'
mkCard :: String -> Bool -> String -> (Integer, Integer) -> Concat
mkCard constraintName group' element' crd
| crd' == "set" || crd' == "" = CString ""
| crd' `elem` ["one", "lone", "some"] = CString $ crd' ++ " " ++ element'
| otherwise = interval'
where
interval' = genInterval constraintName group' element' crd
crd' = flatten $ interval'
{-
-- generates expression for references that point to expressions (not single clafers)
genPathConst :: GenEnv -> String -> [String] -> IClafer -> Concat
genPathConst genEnv name resPath c
| isRefPath (c ^. reference) = cconcat [CString name, CString " = ",
fromMaybe (error "genPathConst: impossible.") $
fmap ((brArg id).(genPExp genEnv resPath)) $
_ref <$> _reference c]
| otherwise = CString ""
isRefPath :: Maybe IReference -> Bool
isRefPath Nothing = False
isRefPath (Just IReference{_ref=s}) = not $ isSimplePath s
isSimplePath :: PExp -> Bool
isSimplePath (PExp _ _ _ (IClaferId _ _ _ _)) = True
isSimplePath (PExp _ _ _ (IFunExp op' _)) = op' == iUnion
isSimplePath _ = False
-}
-- -----------------------------------------------------------------------------
-- Not used?
-- genGCard element gcard = genInterval element $ interval $ fromJust gcard
genCard :: String -> Maybe Interval -> Concat
genCard element' crd = genInterval element' False element' $ fromJust crd
genCardCrude :: Maybe Interval -> String
genCardCrude crd = genIntervalCrude $ fromJust crd
genIntervalCrude :: Interval -> String
genIntervalCrude x = case x of
(1, 1) -> "one"
(0, 1) -> "lone"
(1, -1) -> "some"
_ -> "set"
genInterval :: String -> Bool -> String -> Interval -> Concat
genInterval constraintName group' element' x = case x of
(1, 1) -> cardConcat constraintName group' [CString "one"]
(0, 1) -> cardConcat constraintName group' [CString "lone"]
(1, -1) -> cardConcat constraintName group' [CString "some"]
(0, -1) -> CString "set" -- "set"
(n, exinteger) ->
case (s1, s2) of
(Just c1, Just c2) -> cconcat [c1, CString " and ", c2]
(Just c1, Nothing) -> c1
(Nothing, Just c2) -> c2
(Nothing, Nothing) -> undefined
where
s1 = if n == 0
then Nothing
else Just $ cardLowerConcat constraintName group' [CString $ concat [show n, " <= #", element']]
s2 =
do
result <- genExInteger element' x exinteger
return $ cardUpperConcat constraintName group' [CString result]
cardConcat :: String -> Bool -> [Concat] -> Concat
cardConcat constraintName = Concat . ExactCard constraintName
cardLowerConcat :: String -> Bool -> [Concat] -> Concat
cardLowerConcat constraintName = Concat . LowerCard constraintName
cardUpperConcat :: String -> Bool -> [Concat] -> Concat
cardUpperConcat constraintName = Concat . UpperCard constraintName
genExInteger :: String -> Interval -> Integer -> Maybe Result
genExInteger element' (y,z) x =
if (y==0 && z==0) then Just $ concat ["#", element', " = ", "0"] else
if x == -1 then Nothing else Just $ concat ["#", element', " <= ", show x]
-- -----------------------------------------------------------------------------
-- Generate code for logical expressions
genPExp :: GenEnv -> [String] -> PExp -> Concat
genPExp genEnv resPath x = genPExp' genEnv resPath $ adjustPExp resPath x
genPExp' :: GenEnv -> [String] -> PExp -> Concat
genPExp' genEnv resPath (PExp iType' pid' pos exp') = case exp' of
IDeclPExp q d pexp -> Concat (IrPExp pid') $
[ CString $ genQuant q, CString " "
, cintercalate (CString ", ") $ map ((genDecl genEnv resPath)) d
, CString $ optBar d, genPExp' genEnv resPath pexp]
where
optBar [] = ""
optBar _ = " | "
IClaferId _ "ref" _ _ -> CString "@ref"
IClaferId _ sid istop _ -> CString $
if head sid == '~' then sid else
if isNothing iType' then sid' else case fromJust $ iType' of
TInteger -> vsident
TReal -> vsident
TString -> vsident
_ -> sid'
where
sid' = (if istop then "" else '@' : genRelName "") ++ sid
-- 29/March/2012 Rafael Olaechea: ref is now prepended with clafer name to be able to refer to it from partial instances.
-- 30/March/2012 Rafael Olaechea added referredClaferUniqeuid to fix problems when having this.x > number (e.g test/positive/i10.cfr )
vsident = if (noalloyruncommand $ claferargs genEnv) then sid' ++ ".@" ++ referredClaferUniqeuid ++ "_ref" else sid' ++ ".@ref"
where referredClaferUniqeuid = if sid == "this" then (head resPath) else sid
IFunExp _ _ -> case exp'' of
IFunExp _ _ -> genIFunExp pid' genEnv resPath exp''
_ -> genPExp' genEnv resPath $ PExp iType' pid' pos exp''
where
exp'' = transformExp exp'
IInt n -> CString $ show n
IDouble _ -> error "no real numbers allowed"
IStr _ -> error "no strings allowed"
-- 3-May-2012 Rafael Olaechea.
-- Removed transfromation from x = -2 to x = (0-2) as this creates problem with partial instances.
-- See http://gsd.uwaterloo.ca:8888/question/461/new-translation-of-negative-number-x-into-0-x-is.
transformExp :: IExp -> IExp
transformExp (IFunExp op' (e1:_))
| op' == iMin = IFunExp iMul [PExp (_iType e1) "" noSpan $ IInt (-1), e1]
transformExp x@(IFunExp op' exps'@(e1:e2:_))
| op' == iXor = IFunExp iNot [PExp (Just TBoolean) "" noSpan (IFunExp iIff exps')]
| op' == iJoin && isClaferName' e1 && isClaferName' e2 &&
getClaferName e1 == thisIdent && head (getClaferName e2) == '~' =
IFunExp op' [e1{_iType = Just $ TClafer []}, e2]
| otherwise = x
transformExp x = x
genIFunExp :: String -> GenEnv -> [String] -> IExp -> Concat
genIFunExp pid' genEnv resPath (IFunExp op' exps') =
if (op' == iSumSet)
then genIFunExp pid' genEnv resPath (IFunExp iSumSet' [(removeright (head exps')), (getRight $ head exps')])
else if (op' == iSumSet')
then Concat (IrPExp pid') $ intl exps'' (map CString $ genOp (Alloy42 `elem` (mode $ claferargs genEnv)) iSumSet)
else Concat (IrPExp pid') $ intl exps'' (map CString $ genOp (Alloy42 `elem` (mode $ claferargs genEnv)) op')
where
intl
| op' == iSumSet' = flip $ interleave
| op' `elem` arithBinOps && length exps' == 2 = interleave
| otherwise = \xs ys -> reverse $ interleave (reverse xs) (reverse ys)
exps'' = map (optBrArg genEnv resPath) exps'
genIFunExp _ _ _ _ = error "Function genIFunExp from Alloy Generator expected a IFunExp as an argument but was given something else" --This should never happen
optBrArg :: GenEnv -> [String] -> PExp -> Concat
optBrArg genEnv resPath x = brFun (genPExp' genEnv resPath) x
where
brFun = case x of
PExp _ _ _ (IClaferId _ _ _ _) -> ($)
PExp _ _ _ (IInt _) -> ($)
_ -> brArg
interleave :: [Concat] -> [Concat] -> [Concat]
interleave [] [] = []
interleave (x:xs) [] = x:xs
interleave [] (x:xs) = x:xs
interleave (x:xs) ys = x : interleave ys xs
brArg :: (a -> Concat) -> a -> Concat
brArg f arg = cconcat [CString "(", f arg, CString ")"]
-- isAlloy42
genOp :: Bool -> String -> [String]
genOp True op'
| op' == iPlus = [".plus[", "]"]
| op' == iSub = [".minus[", "]"]
| otherwise = genOp False op'
genOp _ op'
| op' == iSumSet = ["sum temp : "," | temp."]
| op' == iProdSet = ["prod temp : "," | temp."]
| op' `elem` unOps = [op']
| op' == iPlus = [".add[", "]"]
| op' == iSub = [".sub[", "]"]
| op' == iMul = [".mul[", "]"]
| op' == iDiv = [".div[", "]"]
| op' == iRem = [".rem[", "]"]
| op' `elem` logBinOps ++ relBinOps ++ arithBinOps = [" " ++ op' ++ " "]
| op' == iUnion = [" + "]
| op' == iDifference = [" - "]
| op' == iIntersection = [" & "]
| op' == iDomain = [" <: "]
| op' == iRange = [" :> "]
| op' == iJoin = ["."]
| op' == iIfThenElse = [" => ", " else "]
genOp _ _ = error "This should never happen"
-- adjust parent
adjustPExp :: [String] -> PExp -> PExp
adjustPExp resPath (PExp t pid' pos x) = PExp t pid' pos $ adjustIExp resPath x
adjustIExp :: [String] -> IExp -> IExp
adjustIExp resPath x = case x of
IDeclPExp q d pexp -> IDeclPExp q d $ adjustPExp resPath pexp
IFunExp op' exps' -> adjNav $ IFunExp op' $ map adjExps exps'
where
(adjNav, adjExps) = if op' == iJoin then (aNav, id)
else (id, adjustPExp resPath)
IClaferId _ _ _ _ -> aNav x
_ -> x
where
aNav = fst.(adjustNav resPath)
adjustNav :: [String] -> IExp -> (IExp, [String])
adjustNav resPath x@(IFunExp op' (pexp0:pexp:_))
| op' == iJoin = (IFunExp iJoin
[pexp0{_exp = iexp0},
pexp{_exp = iexp}], path')
| otherwise = (x, resPath)
where
(iexp0, path) = adjustNav resPath (_exp pexp0)
(iexp, path') = adjustNav path (_exp pexp)
adjustNav resPath x@(IClaferId _ id' _ _)
| id' == parentIdent = (x{_sident = "~@" ++ (genRelName $ head resPath)}, tail resPath)
| otherwise = (x, resPath)
adjustNav _ _ = error "Function adjustNav Expect a IFunExp or IClaferID as one of it's argument but it was given a differnt IExp" --This should never happen
genQuant :: IQuant -> String
genQuant x = case x of
INo -> "no"
ILone -> "lone"
IOne -> "one"
ISome -> "some"
IAll -> "all"
genDecl :: GenEnv -> [String] -> IDecl -> Concat
genDecl genEnv resPath x = case x of
IDecl disj locids pexp -> cconcat [CString $ genDisj disj, CString " ",
CString $ intercalate ", " locids, CString " : ", genPExp genEnv resPath pexp]
genDisj :: Bool -> String
genDisj x = case x of
False -> ""
True -> "disj"
-- mapping line/columns between Clafer and Alloy code
data AlloyEnv = AlloyEnv {
lineCol :: (LineNo, ColNo),
mapping :: [(Span, IrTrace)]
} deriving (Eq,Show)
mapLineCol :: Concat -> [(Span, IrTrace)]
mapLineCol code = mapping $ execState (mapLineCol' code) (AlloyEnv (firstLine, firstCol) [])
addCode :: MonadState AlloyEnv m => String -> m ()
addCode str = modify (\s -> s {lineCol = lineno (lineCol s) str})
mapLineCol' :: MonadState AlloyEnv m => Concat -> m ()
mapLineCol' (CString str) = addCode str
mapLineCol' c@(Concat srcPos' n) = do
posStart <- gets lineCol
_ <- mapM mapLineCol' n
posEnd <- gets lineCol
{-
- Alloy only counts inner parenthesis as part of the constraint, but not outer parenthesis.
- ex1. the constraint looks like this in the file
- (constraint a) <=> (constraint b)
- But the actual constraint in the API is
- constraint a) <=> (constraint b
-
- ex2. the constraint looks like this in the file
- (((#((this.@r_c2_Finger).@r_c3_Pinky)).add[(#((this.@r_c2_Finger).@r_c4_Index))]).add[(#((this.@r_c2_Finger).@r_c5_Middle))]) = 0
- But the actual constraint in the API is
- #((this.@r_c2_Finger).@r_c3_Pinky)).add[(#((this.@r_c2_Finger).@r_c4_Index))]).add[(#((this.@r_c2_Finger).@r_c5_Middle))]) = 0
-
- Seems unintuitive since the brackets are now unbalanced but that's how they work in Alloy. The next
- few lines of code is counting the beginning and ending parenthesis's and subtracting them from the
- positions in the map file.
- Same is true for square brackets.
- This next little snippet is rather inefficient since we are retraversing the Concat's to flatten.
- But it's the simplest and correct solution I can think of right now.
-}
let flat = flatten c
raiseStart = countLeading "([" flat
deductEnd = -(countTrailing ")]" flat)
modify (\s -> s {mapping = (Span (uncurry Pos $ posStart `addColumn` raiseStart) (uncurry Pos $ posEnd `addColumn` deductEnd), srcPos') : (mapping s)})
addColumn :: Interval -> Integer -> Interval
addColumn (x, y) c = (x, y + c)
countLeading :: String -> String -> Integer
countLeading c xs = toInteger $ length $ takeWhile (`elem` c) xs
countTrailing :: String -> String -> Integer
countTrailing c xs = countLeading c (reverse xs)
lineno :: (Integer, ColNo) -> String -> (Integer, ColNo)
lineno (l, c) str = (l + newLines, (if newLines > 0 then firstCol else c) + newCol)
where
newLines = toInteger $ length $ filter (== '\n') str
newCol = toInteger $ length $ takeWhile (/= '\n') $ reverse str
firstCol :: ColNo
firstCol = 1 :: ColNo
firstLine :: LineNo
firstLine = 1 :: LineNo
removeright :: PExp -> PExp
removeright (PExp _ _ _ (IFunExp _ (x : (PExp _ _ _ (IClaferId _ _ _ _)) : _))) = x
removeright (PExp t id' pos (IFunExp o (x1:x2:xs))) = (PExp t id' pos (IFunExp o (x1:(removeright x2):xs)))
removeright (PExp _ _ _ _) = error "Function removeright from the AlloyGenerator expects a PExp with a IFunExp inside, was given something else" --This should never happen
getRight :: PExp -> PExp
getRight (PExp _ _ _ (IFunExp _ (_:x:_))) = getRight x
getRight p = p