Alloy.hs

{-# LANGUAGE RankNTypes, FlexibleContexts #-}
{-
 Copyright (C) 2012-2015 Kacper Bak, Jimmy Liang, Michal Antkiewicz, 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.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
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))

header :: GenEnv -> Concat
header    genEnv  = CString $ unlines
    [ "open util/integer"
    , "pred show {}"
    , if (validate $ claferargs genEnv)
      then ""
      else "run show " ++ forScopes genEnv
    , ""]

-- 07th Mayo 2012 Rafael Olaechea
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 _ _ -> CString ""

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"
  ]

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 $ if _isAbstract c then "abstract " else ""
  , CString "sig "
  , Concat NoTrace [CString $ _uid c, genExtends $ _super c, CString "\n", rest]
  ]
  where
  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 (genRefName $ _uid c)
                         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

genRefName :: String -> String
genRefName name = name ++ "_ref"

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 "") (((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)
  : (genRefSubrelationConstriant (uidIClaferMap 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 = concatMap 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 "[bug] Alloy.getConst: should not be given a goal." -- 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.@" ++ genRefName (_uid c) ++ ") != (y.@" ++ genRefName (_uid c) ++ ") "
                   ]
              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

-- See Common.NestedInheritanceMatch
genRefSubrelationConstriant :: UIDIClaferMap -> IClafer   -> Concat
genRefSubrelationConstriant    uidIClaferMap'   headClafer =
  if isJust $ _reference headClafer
  then
    case match of
      Nothing -> CString ""
      Just NestedInheritanceMatch
        { _superClafer = superClafer
        ,  _superClafersTarget = superClafersTarget
        }  -> case (isProperRefinement uidIClaferMap' match, not $ null superClafersTarget) of
                 ((True, True, True), True) -> CString $ concat
                  [ genRefName $ _uid headClafer
                  , " in "
                  , genRefName $ _uid superClafer
                  ]
                 _ -> CString ""
  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 _ "integer" _ _ -> CString "Int"
  IClaferId _ "int" _ _ -> CString "Int"
  IClaferId _ "string" _ _ -> CString "Int"
  IClaferId _ "ref" _ _ -> CString $ "@"  ++ getTClaferUID iType' ++ "_ref"
    where
      getTClaferUID (Just TMap{_so = TClafer{_hi = [u]}}) = u
      getTClaferUID (Just TMap{_so = TClafer{_hi = (u:_)}}) = u
      getTClaferUID t = error $ "[bug] Alloy.genPExp'.getTClaferUID: unknown type: " ++ show t
  IClaferId _ sid istop _ -> CString $
      if head sid == '~'
        then sid
        else case iType' of
          Just TInteger -> vsident
          Just TDouble -> vsident
          Just TReal -> vsident
          Just TString -> vsident
          _ -> sid'
    where
    sid' = (if istop then "" else '@' : genRelName "") ++ sid
    vsident = sid' ++  ".@"  ++ genRefName (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 double numbers allowed"
  IReal _ -> 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 iSumSet)
      else Concat (IrPExp pid') $ intl exps'' (map CString $ genOp 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 _ _ _ x = error $ "[bug] Alloy.genIFunExp: expecting a IFunExp, instead got: " ++ show x--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 ")"]

genOp :: String -> [String]
genOp    op'
  | op' == iPlus = [".plus[", "]"]
  | op' == iSub  = [".minus[", "]"]
  | 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 op' = error $ "[bug] Alloy.genOp: Unmatched operator: " ++ op'

-- 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    True  = "disj"
genDisj    False = ""

-- 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 _ _ _ (IFunExp _ (x : (PExp _ _ _ (IInt _ )) : _))) = x
removeright (PExp _ _ _ (IFunExp _ (x : (PExp _ _ _ (IStr _ )) : _))) = x
removeright (PExp _ _ _ (IFunExp _ (x : (PExp _ _ _ (IDouble _ )) : _))) = x
removeright (PExp t id' pos (IFunExp o (x1:x2:xs))) = PExp t id' pos (IFunExp o (x1:(removeright x2):xs))
removeright x@PExp{} = error $ "[bug] AlloyGenerator.removeright: expects a PExp with a IFunExp inside but was given: " ++ show x --This should never happen

getRight :: PExp -> PExp
getRight (PExp _ _ _ (IFunExp _ (_:x:_))) = getRight x
getRight p = p