content: {- |
  Module      :  ./CSL/ASUtils.hs
  Description :  Utils for the abstract syntax of EnCL
  Copyright   :  (c) Dominik Dietrich, Ewaryst Schulz, DFKI Bremen 2011
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Ewaryst.Schulz@dfki.de
  Stability   :  experimental
  Portability :  portable
  
  
  Utils to create and access abstract syntax data
  -}
  
  module CSL.ASUtils
      ( getDefiniens        -- accessor function for AssDefinition
      , getArguments        -- accessor function for AssDefinition
      , isFunDef            -- predicate for AssDefinition
      , isInterval          -- predicate for EXPRESSION
      , mkDefinition        -- constructor for AssDefinition
      , updateDefinition    -- updates the definiens
      , mapExpr             -- maps function over EXPRESSION arguments
  
      , varDeclName
      , varDeclToVar
      , opDeclToOp
  
      , mkVar               -- Variable constructor
      , mkOp                -- Simple Operator constructor
      , mkPredefOp          -- Simple Operator constructor for predefined ops
      , mkUserdefOp
  
      , mkAndAnalyzeOp
      , mkAndAnalyzeOp'
      , toElimConst         -- Constant naming for elim constants, see Analysis.hs
      , simpleName
      , setOfUserDefined
      , setOfConstsAndEPSpecs
      ) where
  
  import Common.Id as Id
  
  import qualified Data.Set as Set
  import Data.List (sort, mapAccumL)
  
  import CSL.AS_BASIC_CSL
  import CSL.Fold
  
  {- ---------------------------------------------------------------------------
  Preliminaries and Utilities
  --------------------------------------------------------------------------- -}
  
  -- | A simple operator constructor from given operator name and arguments
  mkOp :: String -> [EXPRESSION] -> EXPRESSION
  mkOp s el = Op (OpUser $ SimpleConstant s) [] el nullRange
  
  -- | A variable constructor
  mkVar :: String -> EXPRESSION
  mkVar = Var . mkSimpleId
  
  -- | A simple operator constructor from given operator id and arguments
  mkPredefOp :: OPNAME -> [EXPRESSION] -> EXPRESSION
  mkPredefOp n el = Op (OpId n) [] el nullRange
  
  -- | A simple operator constructor from given operator id and arguments
  mkUserdefOp :: String -> [EXTPARAM] -> [EXPRESSION] -> Range -> EXPRESSION
  mkUserdefOp n = Op (OpUser $ SimpleConstant n)
  
  
  foldNaryToBinary :: OPID -> Range -> [EXPRESSION] -> EXPRESSION
  foldNaryToBinary op rg exps = foldl f (f (head exps) (exps !! 1)) $ drop 2 exps
      where f e' e'' = Op op [] [e', e''] rg
  
  mkAndAnalyzeOp :: OperatorState st => st -> String -> [EXTPARAM] -> [EXPRESSION]
                 -> Range -> EXPRESSION
  
  mkAndAnalyzeOp st s eps exps rg =
      either f g $ mkAndAnalyzeOp' False st s eps exps rg
      where f = error
            g e = e
  
  -- | Lookup the string in the given 'OperatorState'
  mkAndAnalyzeOp' :: OperatorState st => Bool -- ^ process binders
                  -> st -> String -> [EXTPARAM] -> [EXPRESSION]
                 -> Range -> Either String EXPRESSION
  mkAndAnalyzeOp' b st s eps exps rg =
      case lookupOperator st s (length exps) of
        Left False
            | isVar st s -> if null exps && null eps
                            then Right $ Var Token { tokStr = s, tokPos = rg }
                            else Left "Variable requires no (extended) parameters"
            | otherwise -> f exps $ OpUser $ SimpleConstant s
        {- if registered it must be registered with the given arity or
        as flex-op, otherwise we don't accept it -}
        Left True -> Left "Wrong arity"
        Right oi
            | null eps ->
                if foldNAry oi && length exps > 2
                then Right $ foldNaryToBinary (OpId $ opname oi) rg exps
                else let exps' =
                          case bind oi of
                            Just x -> if b then processBinderArgs x exps else exps
                            _ -> exps
                     in f exps' $ OpId $ opname oi
  
            | otherwise -> Left "No extended parameters allowed"
      where f exps' op = Right $ Op op eps exps' rg
  
  {- | For given binder arguments we replace the constant-expressions at the
  bound variable positions by variable-expressions and also all constants with
  the name of a variable in the arguments at binder body positions. -}
  processBinderArgs :: BindInfo -> [EXPRESSION] -> [EXPRESSION]
  processBinderArgs (BindInfo {bindingVarPos = bvl, boundBodyPos = bbl}) exps =
      let bvl' = sort bvl
          (vs, vl) = varSet $ map (exps !!) bvl'
          g l'@((j, ve) : l) (i, e)
              | j == i -- at bound variable position
                  = (l, ve)
              | otherwise = (l', g' (i, e))
          g l x = (l, g' x)
          g' (i, e)
              | elem i bbl -- at binder body position
                  = constsToVars vs e
              | otherwise = e
      in snd $ mapAccumL g (zip bvl' vl) $ zip [0 ..] exps
  
  
  mapExpr :: (EXPRESSION -> EXPRESSION) -> EXPRESSION -> EXPRESSION
  mapExpr f e =
      case e of
        Op oi epl args rg -> Op oi epl (map f args) rg
        List exps rg -> List (map f exps) rg
        _ -> e
  
  
  -- | Transforms Op-Expressions to a set of op-names and a Var-list
  varSet :: [EXPRESSION] -> (Set.Set String, [EXPRESSION])
  varSet l =
      let opToVar' s (Op v _ _ rg') =
              ( Set.insert (simpleName v) s
              , Var Token { tokStr = simpleName v, tokPos = rg' } )
          opToVar' s v@(Var tok) = (Set.insert (tokStr tok) s, v)
          opToVar' _ x =
              error $ "varSet: not supported varexpression at " ++ show x
      in mapAccumL opToVar' Set.empty l
  
  -- | Replaces Op occurrences to Var if the op is in the given set
  constsToVars :: Set.Set String -> EXPRESSION -> EXPRESSION
  constsToVars env e =
      let substRec =
           idRecord
           { foldOp =
              \ _ s epl' args rg' ->
                  if Set.member (simpleName s) env then
                      if null args
                      then Var Token { tokStr = simpleName s, tokPos = rg' }
                      else error $ "constsToVars: variable must not have"
                               ++ " arguments:" ++ show args
                  else Op s epl' args rg'
           , foldList = \ _ l rg' -> List l rg'
           }
      in foldTerm substRec e
  
  
  updateDefinition :: EXPRESSION -> AssDefinition -> AssDefinition
  updateDefinition e' (ConstDef _) = ConstDef e'
  updateDefinition e' (FunDef l _) = FunDef l e'
  
  
  mkDefinition :: [String] -> EXPRESSION -> AssDefinition
  mkDefinition l e = if null l then ConstDef e else FunDef l e
  
  getDefiniens :: AssDefinition -> EXPRESSION
  getDefiniens (ConstDef e) = e
  getDefiniens (FunDef _ e) = e
  
  getArguments :: AssDefinition -> [String]
  getArguments (FunDef l _) = l
  getArguments _ = []
  
  isFunDef :: AssDefinition -> Bool
  isFunDef (FunDef _ _) = True
  isFunDef _ = False
  
  isInterval :: EXPRESSION -> Bool
  isInterval (Interval {}) = True
  isInterval _ = False
  
  simpleName :: OPID -> String
  simpleName (OpId n) = showOPNAME n
  simpleName (OpUser (SimpleConstant s)) = s
  simpleName (OpUser x) = error "simpleName: ElimConstant not supported: " ++
                          show x
  
  toElimConst :: ConstantName -> Int -> ConstantName
  toElimConst (SimpleConstant s) i = ElimConstant s i
  toElimConst ec _ = error $ "toElimConst: already an elim const " ++ show ec
  
  varDeclName :: VarDecl -> String
  varDeclName (VarDecl n _) = Id.tokStr n
  
  varDeclToVar :: VarDecl -> EXPRESSION
  varDeclToVar (VarDecl n _) = Var n
  
  opDeclToOp :: OpDecl -> EXPRESSION
  opDeclToOp (OpDecl n epl vdl rg ) = Op (OpUser n) epl (map varDeclToVar vdl) rg
  
  -- | Returns a set of user defined constants ignoring 'EXTPARAM' instantiation.
  setOfUserDefined :: EXPRESSION -> Set.Set String
  setOfUserDefined = g Set.empty
      where
        g s x =
         case x of
           Op oi@(OpUser _) _ al _ -> foldl g (Set.insert (simpleName oi) s) al
           -- handle also non-userdefined ops.
           Op _ _ al _ -> foldl g s al
           -- ignoring lists (TODO: they should be removed soon anyway)
           _ -> s
  
  -- | Returns a set of user defined constants and 'EXTPARAM' specifications.
  setOfConstsAndEPSpecs :: EXPRESSION -> (Set.Set String, Set.Set EXTPARAM)
  setOfConstsAndEPSpecs = g (Set.empty, Set.empty)
      where
        g s@(s1, s2) x =
         case x of
           Op oi@(OpUser _) epl al _ ->
               foldl g ( Set.insert (simpleName oi) s1
                       , foldr Set.insert s2 epl) al
           -- handle also non-userdefined ops.
           Op _ _ al _ -> foldl g s al
           -- ignoring lists (TODO: they should be removed soon anyway)
           _ -> s
  