{- |
Module      :  $Header$
Description :  Maude Comorphisms
Copyright   :  (c) Adrian Riesco, Facultad de Informatica UCM 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  ariesco@fdi.ucm.es
Stability   :  experimental
Portability :  portable

Comorphism from Maude to CASL.
-}

module Maude.PreComorphism where

import Data.Maybe
import qualified Data.List as List
import qualified Data.Set as Set
import qualified Data.Map as Map

import qualified Maude.Sign as MSign
import qualified Maude.Sentence as MSentence
import qualified Maude.Morphism as MMorphism
import qualified Maude.AS_Maude as MAS
import qualified Maude.Symbol as MSym
import Maude.Meta.HasName

import qualified CASL.Sign as CSign
import qualified CASL.Morphism as CMorphism
import qualified CASL.AS_Basic_CASL as CAS
import CASL.StaticAna

import Common.Id
import Common.Result
import Common.AS_Annotation
import Common.ProofUtils (charMap)
import qualified Common.Lib.Rel as Rel
import qualified Common.Lib.MapSet as MapSet

type IdMap = Map.Map Id Id
type OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

-- | generates a CASL morphism from a Maude morphism
mapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor
mapMorphism morph =
         let
           src = MMorphism.source morph
           tgt = MMorphism.target morph
           mk = kindMapId $ MSign.kindRel src
           mk' = kindMapId $ MSign.kindRel tgt
           smap = MMorphism.sortMap morph
           omap = MMorphism.opMap morph
           smap' = applySortMap2CASLSorts smap mk mk'
           omap' = maudeOpMap2CASLOpMap mk omap
           pmap = createPredMap mk smap
           (src', _) = maude2casl src []
           (tgt', _) = maude2casl tgt []
         in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

{- | translates the Maude morphism between operators into a CASL morpshim
between operators -}
maudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
maudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

{- | translates the mapping between two symbols representing operators into
a CASL operators map -}
translateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
  -> CMorphism.Op_map
translateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm
  = copm'
       where f = token2id . getName
             g x = Map.findWithDefault (errorId "translate op map entry")
                 (f x) im
             ot = CSign.OpType CAS.Total (map g ar) (g co)
             cop = (token2id from, ot)
             to' = (token2id to, CAS.Total)
             copm' = Map.insert cop to' copm
translateOpMapEntry _ _ _ _ = Map.empty

-- | generates a set of CASL symbol from a Maude Symbol
mapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol
mapSymbol sg (MSym.Sort q) = Set.singleton csym
           where mk = kindMapId $ MSign.kindRel sg
                 sym_id = token2id q
                 kind = Map.findWithDefault (errorId "map symbol") sym_id mk
                 pred_data = CSign.PredType [kind]
                 csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
mapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
           where mk = kindMapId $ MSign.kindRel sg
                 q' = token2id q
                 ar' = map (maudeSort2caslId mk) ar
                 co' = token2id $ getName co
                 op_data = CSign.OpType CAS.Total ar' co'
                 csym = CSign.Symbol q' $ CSign.OpAsItemType op_data
mapSymbol _ _ = Set.empty

-- | returns the sort in CASL of the Maude sort symbol
maudeSort2caslId :: IdMap -> MSym.Symbol -> Id
maudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")
                          (token2id $ getName sym) im

{- | creates the predicate map for the CASL morphism from the Maude sort map and
the map between sorts and kinds -}
createPredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
createPredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

-- | creates an entry of the predicate map for a single sort
createPredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map
  -> CMorphism.Pred_map
createPredMap4sort im from to = Map.insert key id_to
           where id_from = token2id $ getName from
                 id_to = token2id $ getName to
                 kind = Map.findWithDefault (errorId "predicate for sort")
                        id_from im
                 key = (id_from, CSign.PredType [kind])

{- | computes the sort morphism of CASL from the sort morphism in Maude
and the set of kinds -}
applySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap
  -> CMorphism.Sort_map
applySortMap2CASLSorts sm im im' = Map.fromList sml'
            where sml = Map.toList sm
                  sml' = foldr (applySortMap2CASLSort im im') [] sml

-- | computes the morphism for a single sort pair
applySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)
  -> [(Id, Id)] -> [(Id, Id)]
applySortMap2CASLSort im im' (s1, s2) l = l'
         where p1 = (mSym2caslId s1, mSym2caslId s2)
               f x = Map.findWithDefault
                   (errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)
               p2 = (f s1 im, f s2 im')
               l' = p1 : if s1 == s2
                    then l else p2 : l

-- | renames the sorts in a given kind
rename :: MMorphism.SortMap -> Token -> Token
rename sm tok = new_tok
          where sym = MSym.Sort tok
                sym' = if Map.member sym sm
                       then fromJust $ Map.lookup sym sm
                       else sym
                new_tok = getName sym'

-- | translates a Maude sentence into a CASL formula
mapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
mapSentence sg sen = let
    mk = kindMapId $ MSign.kindRel sg
    named = makeNamed "" sen
    form = mb_rl2formula mk named
  in return $ sentence $ case sen of
       MSentence.Equation (MAS.Eq _ _ _ ats) -> if any MAS.owise ats then let
           sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg
           (no_owise_sens, _, _) = splitOwiseEqs sg_sens
           no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
           in owiseSen2Formula mk no_owise_forms named
           else noOwiseSen2Formula mk named
       MSentence.Membership (MAS.Mb {}) -> form
       MSentence.Rule (MAS.Rl {}) -> form

{- | applies maude2casl to compute the CASL signature and sentences from
the Maude ones, and wraps them into a Result datatype -}
mapTheory :: (MSign.Sign, [Named MSentence.Sentence])
              -> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])
mapTheory (sg, nsens) = return $ maude2casl sg nsens

{- | computes new signature and sentences of CASL associated to the
given Maude signature and sentences -}
maude2casl :: MSign.Sign -> [Named MSentence.Sentence]
              -> (CSign.CASLSign, [Named CAS.CASLFORMULA])
maude2casl msign nsens = (csign {
                            CSign.sortRel =
                              Rel.union (Rel.fromKeysSet cs) sbs',
                            CSign.opMap = cops',
                            CSign.assocOps = assoc_ops,
                            CSign.predMap = preds,
                            CSign.declaredSymbols = syms }, new_sens)
   where csign = CSign.emptySign ()
         ss = MSign.sorts msign
         ss' = Set.map sym2id ss
         mk = kindMapId $ MSign.kindRel msign
         sbs = MSign.subsorts msign
         sbs' = maudeSbs2caslSbs sbs mk
         cs = Set.union ss' $ kindsFromMap mk
         preds = rewPredicates cs
         rs = rewPredicatesSens cs
         ops = deleteUniversal $ MSign.ops msign
         ksyms = kinds2syms cs
         (cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)
         axSens = axiomsSens mk ops
         ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
         cops' = universalOps cs cops $ booleanImported ops
         rs' = rewPredicatesCongSens cops'
         pred_forms = loadLibraries (MSign.sorts msign) ops
         ops_syms = ops2symbols cops'
         (no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens
         no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens
         owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens
         mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens
         preds_syms = preds2syms preds
         syms = Set.union ksyms $ Set.union ops_syms preds_syms
         new_sens = concat [rs, rs', no_owise_forms, owise_forms,
                            mb_rl_forms, ctor_sen, pred_forms, axSens]

{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts
for the kinds -}
maudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT
maudeSbs2caslSbs sbs im = Rel.fromMap m4
      where l = Map.toList $ Rel.toMap sbs
            l1 = [] -- map maudeSb2caslSb l
            l2 = idList2Subsorts $ Map.toList im
            l3 = map subsorts2Ids l
            m1 = Map.fromList l1
            m2 = Map.fromList l2
            m3 = Map.fromList l3
            m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3

idList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
idList2Subsorts [] = []
idList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il
      where t1 = (id1, Set.singleton id2)

maudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
maudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)

subsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
subsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

sortSym2id :: MSym.Symbol -> Id
sortSym2id (MSym.Sort q) = token2id q
sortSym2id _ = token2id $ mkSimpleId "error_translation"

-- | generates the sentences to state that the rew predicates are a congruence
rewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
rewPredicatesCongSens = MapSet.foldWithKey rewPredCong []

{- | generates the sentences to state that the rew predicates are a congruence
for a single operator -}
rewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]
  -> [Named CAS.CASLFORMULA]
rewPredCong op ot fs = case args of
                        [] -> fs
                        _ -> nq_form : fs
       where args = CSign.opArgs ot
             vars1 = rewPredCongPremise 0 args
             vars2 = rewPredCongPremise (length args) args
             res = CSign.opRes ot
             res_pred_type = CAS.Pred_type [res, res] nullRange
             pn = CAS.Qual_pred_name rewID res_pred_type nullRange
             name = "rew_cong_" ++ show op
             prems = rewPredsCong args vars1 vars2
             prems_conj = createConjForm prems
             os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange
             conc_term1 = CAS.Application os vars1 nullRange
             conc_term2 = CAS.Application os vars2 nullRange
             conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange
             form = createImpForm prems_conj conc_form
             nq_form = makeNamed name $ quantifyUniversally form

-- | generates a list of variables of the given sorts
rewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]
rewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss
rewPredCongPremise _ [] = []

-- | generates a list of rew predicates with the given variables
rewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM]
  -> [CAS.CASLFORMULA]
rewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms
          where pred_type = CAS.Pred_type [s, s] nullRange
                pn = CAS.Qual_pred_name rewID pred_type nullRange
                form = CAS.Predication pn [t, t'] nullRange
                forms = rewPredsCong ss ts ts'
rewPredsCong _ _ _ = []

-- | load the CASL libraries for the Maude built-in operators
loadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]
loadLibraries ss om = if natImported ss om then loadNaturalNatSens else []

-- | loads the sentences associated to the natural numbers
loadNaturalNatSens :: [Named CAS.CASLFORMULA]
loadNaturalNatSens = [] -- retrieve code from Rev 17944 if needed again!

-- | checks if a sentence is an constructor sentence
ctorCons :: Named CAS.CASLFORMULA -> Bool
ctorCons f = case sentence f of
      CAS.Sort_gen_ax _ _ -> True
      _ -> False

-- | checks if the boolean values are imported
booleanImported :: MSign.OpMap -> Bool
booleanImported = Map.member (mkSimpleId "if_then_else_fi")

-- | checks if the natural numbers are imported
natImported :: MSign.SortSet -> MSign.OpMap -> Bool
natImported ss om = b1 && b2 && b3
     where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss
           b2 = Map.member (mkSimpleId "s_") om
           b3 = not b2 || specialZeroSet (om Map.! mkSimpleId "s_")

specialZeroSet :: MSign.OpDeclSet -> Bool
specialZeroSet = Set.fold specialZero False

specialZero :: MSign.OpDecl -> Bool -> Bool
specialZero (_, ats) b = b' || b
         where b' = isSpecial ats

isSpecial :: [MAS.Attr] -> Bool
isSpecial [] = False
isSpecial (MAS.Special _ : _) = True
isSpecial (_ : ats) = isSpecial ats

{- | delete the universal operators from Maude specifications, that will be
substituted for one operator for each sort in the specification -}
deleteUniversal :: MSign.OpMap -> MSign.OpMap
deleteUniversal om = om5
         where om1 = Map.delete (mkSimpleId "if_then_else_fi") om
               om2 = Map.delete (mkSimpleId "_==_") om1
               om3 = Map.delete (mkSimpleId "_=/=_") om2
               om4 = Map.delete (mkSimpleId "upTerm") om3
               om5 = Map.delete (mkSimpleId "downTerm") om4

-- | generates the universal operators for all the sorts in the module
universalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap
universalOps kinds om True = Set.fold universalOpKind om kinds
universalOps _ om False = om

-- | generates the universal operators for a concrete module
universalOpKind :: Id -> CSign.OpMap -> CSign.OpMap
universalOpKind kind = MapSet.union $ MapSet.fromList
  [ (if_id, [if_opt]), (double_eq_id, [eq_opt]), (neg_double_eq_id, [eq_opt]) ]
        where if_id = str2id "if_then_else_fi"
              double_eq_id = str2id "_==_"
              neg_double_eq_id = str2id "_=/=_"
              bool_id = str2id "Bool"
              if_opt = CSign.OpType CAS.Total [bool_id, kind, kind] kind
              eq_opt = CSign.OpType CAS.Total [kind, kind] bool_id

-- | generates the formulas for the universal operators
universalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
universalSens = Set.fold universalSensKind []

-- | generates the formulas for the universal operators for the given sort
universalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
universalSensKind kind acc = concat [iss, eqs, neqs, acc]
         where iss = ifSens kind
               eqs = equalitySens kind
               neqs = nonEqualitySens kind

-- | generates the formulas for the if statement
ifSens :: Id -> [Named CAS.CASLFORMULA]
ifSens kind = [form'', neg_form'']
         where v1 = newVarIndex 1 kind
               v2 = newVarIndex 2 kind
               bk = str2id "Bool"
               bv = newVarIndex 2 bk
               true_type = CAS.Op_type CAS.Total [] bk nullRange
               true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
               true_term = CAS.Application true_id [] nullRange
               if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange
               if_name = str2id "if_then_else_fi"
               if_id = CAS.Qual_op_name if_name if_type nullRange
               if_term = CAS.Application if_id [bv, v1, v2] nullRange
               prem = CAS.mkStEq bv true_term
               concl = CAS.mkStEq if_term v1
               form = CAS.mkImpl prem concl
               form' = quantifyUniversally form
               neg_prem = CAS.Negation prem nullRange
               neg_concl = CAS.mkStEq if_term v2
               neg_form = CAS.mkImpl neg_prem neg_concl
               neg_form' = quantifyUniversally neg_form
               name1 = show kind ++ "_if_true"
               name2 = show kind ++ "_if_false"
               form'' = makeNamed name1 form'
               neg_form'' = makeNamed name2 neg_form'

-- | generates the formulas for the equality
equalitySens :: Id -> [Named CAS.CASLFORMULA]
equalitySens kind = [form'', comp_form'']
         where v1 = newVarIndex 1 kind
               v2 = newVarIndex 2 kind
               bk = str2id "Bool"
               b_type = CAS.Op_type CAS.Total [] bk nullRange
               true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
               true_term = CAS.Application true_id [] nullRange
               false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
               false_term = CAS.Application false_id [] nullRange
               prem = CAS.mkStEq v1 v2
               double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
                                nullRange
               double_eq_name = str2id "_==_"
               double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
               double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
               concl = CAS.mkStEq double_eq_term true_term
               form = CAS.mkImpl prem concl
               form' = quantifyUniversally form
               neg_prem = CAS.Negation prem nullRange
               new_concl = CAS.mkStEq double_eq_term false_term
               comp_form = CAS.mkImpl neg_prem new_concl
               comp_form' = quantifyUniversally comp_form
               name1 = show kind ++ "_==_true"
               name2 = show kind ++ "_==_false"
               form'' = makeNamed name1 form'
               comp_form'' = makeNamed name2 comp_form'

-- | generates the formulas for the inequality
nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]
nonEqualitySens kind = [form'', comp_form'']
         where v1 = newVarIndex 1 kind
               v2 = newVarIndex 2 kind
               bk = str2id "Bool"
               b_type = CAS.Op_type CAS.Total [] bk nullRange
               true_id = CAS.Qual_op_name (str2id "true") b_type nullRange
               true_term = CAS.Application true_id [] nullRange
               false_id = CAS.Qual_op_name (str2id "false") b_type nullRange
               false_term = CAS.Application false_id [] nullRange
               prem = CAS.mkStEq v1 v2
               double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind
                                nullRange
               double_eq_name = str2id "_==_"
               double_eq_id = CAS.mkQualOp double_eq_name double_eq_type
               double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
               concl = CAS.mkStEq double_eq_term false_term
               form = CAS.mkImpl prem concl
               form' = quantifyUniversally form
               neg_prem = CAS.Negation prem nullRange
               new_concl = CAS.mkStEq double_eq_term true_term
               comp_form = CAS.mkImpl neg_prem new_concl
               comp_form' = quantifyUniversally comp_form
               name1 = show kind ++ "_=/=_false"
               name2 = show kind ++ "_=/=_true"
               form'' = makeNamed name1 form'
               comp_form'' = makeNamed name2 comp_form'

-- | generates the sentences for the operator attributes
axiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]
axiomsSens im = Map.fold (axiomsSensODS im) []

axiomsSensODS :: IdMap -> MSign.OpDeclSet -> [Named CAS.CASLFORMULA]
                 -> [Named CAS.CASLFORMULA]
axiomsSensODS im ods l = Set.fold (axiomsSensOD im) l ods

axiomsSensOD :: IdMap -> MSign.OpDecl -> [Named CAS.CASLFORMULA]
  -> [Named CAS.CASLFORMULA]
axiomsSensOD im (ss, ats) l = Set.fold (axiomsSensSS im ats) l ss

axiomsSensSS :: IdMap -> [MAS.Attr] -> MSym.Symbol -> [Named CAS.CASLFORMULA]
  -> [Named CAS.CASLFORMULA]
axiomsSensSS im ats (MSym.Operator q ar co) l = l ++ l1
       where l1 = if elem MAS.Comm ats
                  then commSen im q ar co
                  else []
axiomsSensSS _ _ _ l = l

commSen :: IdMap -> MAS.Qid -> MSym.Symbols -> MSym.Symbol
  -> [Named CAS.CASLFORMULA]
commSen im q ar@[ar1, ar2] co = [form']
       where q' = token2id q
             f = (`maudeSymbol2caslSort` im)
             ar1' = f ar1
             ar2' = f ar2
             ot = CAS.Op_type CAS.Total (map f ar) (f co) nullRange
             os = CAS.Qual_op_name q' ot nullRange
             v1 = newVarIndex 1 ar1'
             v2 = newVarIndex 2 ar2'
             t1 = CAS.Application os [v1, v2] nullRange
             t2 = CAS.Application os [v2, v1] nullRange
             form = CAS.mkStEq t1 t2
             name = "comm_" ++ ms2vcs (show q') ++ "_" ++ show ar1'
             form' = makeNamed name $ quantifyUniversally form
commSen _ _ _ _ = []

-- (newVarIndex 1 (hd ar))

-- maudeSymbol2caslSort x im

{- | translates the Maude operator map into a tuple of CASL operators, CASL
associative operators, membership induced from each Maude operator,
and the set of sorts with the ctor attribute -}
translateOps :: IdMap -> MSign.OpMap -> OpTransTuple
translateOps im = Map.fold (translateOpDeclSet im)
  (MapSet.empty, MapSet.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above
translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods

{- | given an operator declaration updates the accumulator with the translation
to CASL operator, checking if the operator has the assoc attribute to insert
it in the map of associative operators, generating the membership predicate
induced by the operator declaration, and checking if it has the ctor
attribute to introduce the operator in the generators sentence -}
translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
translateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of
        [] -> (ops', assoc_ops', cs')
        _ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')
      where sym : tl = Set.toList syms
            syms' = Set.fromList tl
            (cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym
            ops' = MapSet.insert cop_id ot ops
            assoc_ops' = if any MAS.assoc ats
                         then MapSet.insert cop_id ot assoc_ops
                         else assoc_ops
            cs' = if any MAS.ctor ats
                  then Set.insert (Component cop_id ot) cs
                  else cs

{- | translates a Maude operator symbol into a pair with the id of the operator
and its CASL type -}
maudeSym2CASLOp :: IdMap -> MSym.Symbol
  -> Maybe (Id, CSign.OpType, CSign.OpType)
maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
      where f = token2id . getName
            g = (`maudeSymbol2caslSort` im)
            ot = CSign.OpType CAS.Total (map g ar) (g co)
            ot' = CSign.OpType CAS.Total (map f ar) (f co)
maudeSym2CASLOp _ _ = Nothing

-- | creates a conjuctive formula distinguishing the size of the list
createConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA
createConjForm = CAS.conjunct

-- | creates a implication formula distinguishing the size of the premises
createImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
createImpForm (CAS.Atom True _) form = form
createImpForm form1 form2 = CAS.mkImpl form1 form2

{- | generates the predicates asserting the "true" sort of the operator if all
the arguments have the correct sort -}
ops2predPremises :: IdMap -> [MSym.Symbol] -> Int
  -> ([CAS.CASLTERM], [CAS.CASLFORMULA])
ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
         where s' = token2id s
               kind = Map.findWithDefault (errorId "mb of op as predicate")
                      s' im
               pred_type = CAS.Pred_type [kind] nullRange
               pred_name = CAS.Qual_pred_name s' pred_type nullRange
               var = newVarIndex i kind
               form = CAS.Predication pred_name [var] nullRange
               (terms, forms) = ops2predPremises im ss (i + 1)
ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
         where k' = token2id k
               kind = Map.findWithDefault (errorId "mb of op as predicate")
                      k' im
               var = newVarIndex i kind
               (terms, forms) = ops2predPremises im ss (i + 1)
ops2predPremises _ _ _ = ([], [])


{- | traverses the Maude sentences, returning a pair of list of sentences.
The first list in the pair are the equations without the attribute "owise",
while the second one are the equations with this attribute -}
splitOwiseEqs :: [Named MSentence.Sentence] -> ([Named MSentence.Sentence]
  , [Named MSentence.Sentence], [Named MSentence.Sentence])
splitOwiseEqs [] = ([], [], [])
splitOwiseEqs (s : ss) = res
        where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss
              sen = sentence s
              res = case sen of
                     MSentence.Equation (MAS.Eq _ _ _ ats) ->
                       if any MAS.owise ats
                       then (no_owise_sens, s : owise_sens, mbs_rls)
                       else (s : no_owise_sens, owise_sens, mbs_rls)
                     _ -> (no_owise_sens, owise_sens, s : mbs_rls)

{- | translates a Maude equation defined without the "owise" attribute into
a CASL formula -}
noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
  -> Named CAS.CASLFORMULA
noOwiseSen2Formula im s = s'
       where MSentence.Equation eq = sentence s
             sen' = noOwiseEq2Formula im eq
             s' = s { sentence = sen' }

{- | translates a Maude equation defined with the "owise" attribute into
a CASL formula -}
owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
  -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
owiseSen2Formula im owise_forms s = s'
       where MSentence.Equation eq = sentence s
             sen' = owiseEq2Formula im owise_forms eq
             s' = s { sentence = sen' }

-- | translates a Maude membership or rule into a CASL formula
mb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA
mb_rl2formula im s = case sen of
                MSentence.Membership mb -> let
                                             mb' = mb2formula im mb
                                           in s { sentence = mb' }
                MSentence.Rule rl -> let
                                       rl' = rl2formula im rl
                                     in s { sentence = rl' }
                _ -> makeNamed "" CAS.falseForm
       where sen = sentence s

-- | generates a new variable qualified with the given number
newVarIndex :: Int -> Id -> CAS.CASLTERM
newVarIndex i sort = CAS.Qual_var var sort nullRange
    where var = mkSimpleId $ 'V' : show i

-- | generates a new variable
newVar :: Id -> CAS.CASLTERM
newVar sort = CAS.Qual_var var sort nullRange
    where var = mkSimpleId "V"

-- | Id for the rew predicate
rewID :: Id
rewID = token2id $ mkSimpleId "rew"

{- | translates a Maude equation without the "owise" attribute into a CASL
formula -}
noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
      where ct = maudeTerm2caslTerm im t
            ct' = maudeTerm2caslTerm im t'
            form = CAS.mkStEq ct ct'
noOwiseEq2Formula im (MAS.Eq t t' conds@(_ : _) _) = quantifyUniversally form
      where ct = maudeTerm2caslTerm im t
            ct' = maudeTerm2caslTerm im t'
            conds_form = conds2formula im conds
            concl_form = CAS.mkStEq ct ct'
            form = createImpForm conds_form concl_form

{- | transforms a Maude equation defined with the otherwise attribute into
a CASL formula -}
owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation
                   -> CAS.CASLFORMULA
owiseEq2Formula im no_owise_form eq = form
      where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq
            (op, ts, _) = fromJust $ getLeftApp eq_form
            ex_form = existencialNegationOtherEqs op ts no_owise_form
            imp_form = createImpForm ex_form eq_form
            form = CAS.mkForall vars imp_form

-- | generates a conjunction of negation of existencial quantifiers
existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
                               [Named CAS.CASLFORMULA] -> CAS.CASLFORMULA
existencialNegationOtherEqs op ts forms = form
      where ex_forms = concatMap (existencialNegationOtherEq op ts) forms
            form = CAS.conjunct ex_forms

{- | given a formula, if it refers to the same operator indicated by the
parameters the predicate creates a list with the negation of the existence of
variables that match the pattern described in the formula. In other case it
returns an empty list -}
existencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM]
  -> Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]
existencialNegationOtherEq req_op terms form = if ok then let
                     (_, ts, conds) = fromJust tpl
                     ts' = qualifyExVarsTerms ts
                     conds' = qualifyExVarsForms conds
                     prems = createEqs ts' terms ++ conds'
                     conj_form = CAS.conjunct prems
                     ex_form = if null vars' then conj_form else
                               CAS.mkExist vars' conj_form
                     neg_form = CAS.mkNeg ex_form
                          in [neg_form]
                else []
      where (inner_form, vars) = noQuantification $ sentence form
            vars' = qualifyExVars vars
            tpl = getLeftApp inner_form
            ok = case tpl of
                  Nothing -> False
                  Just _ -> let (op, ts, _) = fromJust tpl
                            in req_op == op && length terms == length ts

{- | qualifies the variables in a list of formulas with the suffix "_ex" to
distinguish them from the variables already bound -}
qualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]
qualifyExVarsForms = map qualifyExVarsForm

{- | qualifies the variables in a formula with the suffix "_ex" to distinguish
them from the variables already bound -}
qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA
qualifyExVarsForm (CAS.Equation t CAS.Strong t' r) =
    CAS.Equation qt CAS.Strong qt' r
        where qt = qualifyExVarsTerm t
              qt' = qualifyExVarsTerm t'
qualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r
        where ts' = qualifyExVarsTerms ts
qualifyExVarsForm f = f

{- | qualifies the variables in a list of terms with the suffix "_ex" to
distinguish them from the variables already bound -}
qualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]
qualifyExVarsTerms = map qualifyExVarsTerm

{- | qualifies the variables in a term with the suffix "_ex" to distinguish them
from the variables already bound -}
qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM
qualifyExVarsTerm (CAS.Qual_var var sort r) =
    CAS.Qual_var (qualifyExVarAux var) sort r
qualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r
           where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm (CAS.Sorted_term t s r) =
    CAS.Sorted_term (qualifyExVarsTerm t) s r
qualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r
qualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r
     where t1' = qualifyExVarsTerm t1
           t2' = qualifyExVarsTerm t2
qualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'
           where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) =
    CAS.Mixfix_parenthesized ts' r
           where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r
           where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r
           where ts' = map qualifyExVarsTerm ts
qualifyExVarsTerm t = t

{- | qualifies a list of variables with the suffix "_ex" to
distinguish them from the variables already bound -}
qualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]
qualifyExVars = map qualifyExVar

{- | qualifies a variable with the suffix "_ex" to distinguish it from
the variables already bound -}
qualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL
qualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r
     where vars' = map qualifyExVarAux vars

-- | qualifies a token with the suffix "_ex"
qualifyExVarAux :: Token -> Token
qualifyExVarAux var = mkSimpleId $ show var ++ "_ex"

-- | creates a list of strong equalities from two lists of terms
createEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
createEqs (t1 : ts1) (t2 : ts2) = CAS.mkStEq t1 t2 : ls
      where ls = createEqs ts1 ts2
createEqs _ _ = []

{- | extracts the operator at the top and the arguments of the lefthand side
in a strong equation -}
getLeftApp :: CAS.CASLFORMULA
  -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])
getLeftApp (CAS.Equation term CAS.Strong _ _) = case getLeftAppTerm term of
                    Nothing -> Nothing
                    Just (op, ts) -> Just (op, ts, [])
getLeftApp (CAS.Relation prem c concl _) = case getLeftApp concl of
       Just (op, ts, _) | c /= CAS.Equivalence -> Just (op, ts, conds)
           where conds = getPremisesImplication prem
       _ -> Nothing
getLeftApp _ = Nothing

{- | extracts the operator at the top and the arguments of the lefthand side
in an application term -}
getLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])
getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
getLeftAppTerm _ = Nothing

{- | extracts the formulas of the given premise, distinguishing whether it is
a conjunction or not -}
getPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]
getPremisesImplication (CAS.Junction CAS.Con forms _) =
    concatMap getPremisesImplication forms
getPremisesImplication form = [form]

-- | translate a Maude membership into a CASL formula
mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
      where ct = maudeTerm2caslTerm im t
            s' = token2id $ getName s
            form = CAS.Membership ct s' nullRange
mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
      where ct = maudeTerm2caslTerm im t
            s' = token2id $ getName s
            conds_form = conds2formula im conds
            concl_form = CAS.Membership ct s' nullRange
            form = CAS.mkImpl conds_form concl_form

-- | translate a Maude rule into a CASL formula
rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
rl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form
       where ty = token2id $ getName $ MAS.getTermType t
             kind = Map.findWithDefault (errorId "rl to formula") ty im
             pred_type = CAS.Pred_type [kind, kind] nullRange
             pred_name = CAS.Qual_pred_name rewID pred_type nullRange
             ct = maudeTerm2caslTerm im t
             ct' = maudeTerm2caslTerm im t'
             form = CAS.Predication pred_name [ct, ct'] nullRange
rl2formula im (MAS.Rl t t' conds@(_ : _) _) = quantifyUniversally form
       where ty = token2id $ getName $ MAS.getTermType t
             kind = Map.findWithDefault (errorId "rl to formula") ty im
             pred_type = CAS.Pred_type [kind, kind] nullRange
             pred_name = CAS.Qual_pred_name rewID pred_type nullRange
             ct = maudeTerm2caslTerm im t
             ct' = maudeTerm2caslTerm im t'
             conds_form = conds2formula im conds
             concl_form = CAS.Predication pred_name [ct, ct'] nullRange
             form = CAS.mkImpl conds_form concl_form

-- | translate a conjunction of Maude conditions to a CASL formula
conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA
conds2formula im conds = CAS.conjunct forms
        where forms = map (cond2formula im) conds

-- | translate a single Maude condition to a CASL formula
cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
cond2formula im (MAS.EqCond t t') = CAS.mkStEq ct ct'
       where ct = maudeTerm2caslTerm im t
             ct' = maudeTerm2caslTerm im t'
cond2formula im (MAS.MatchCond t t') = CAS.mkStEq ct ct'
       where ct = maudeTerm2caslTerm im t
             ct' = maudeTerm2caslTerm im t'
cond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange
      where ct = maudeTerm2caslTerm im t
            s' = token2id $ getName s
cond2formula im (MAS.RwCond t t') = CAS.mkPredication pred_name [ct, ct']
       where ct = maudeTerm2caslTerm im t
             ct' = maudeTerm2caslTerm im t'
             ty = token2id $ getName $ MAS.getTermType t
             kind = Map.findWithDefault (errorId "rw cond to formula") ty im
             pred_type = CAS.Pred_type [kind, kind] nullRange
             pred_name = CAS.Qual_pred_name rewID pred_type nullRange

-- | translates a Maude term into a CASL term
maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM
maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange
        where ty' = maudeType2caslSort ty im
maudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange
        where name = token2id q
              ty' = maudeType2caslSort ty im
              op_type = CAS.Op_type CAS.Total [] ty' nullRange
              op = CAS.Qual_op_name name op_type nullRange
maudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange
        where name = token2id q
              tts = map (maudeTerm2caslTerm im) ts
              ty' = maudeType2caslSort ty im
              types_tts = getTypes tts
              op_type = CAS.Op_type CAS.Total types_tts ty' nullRange
              op = CAS.Qual_op_name name op_type nullRange

maudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT
maudeSymbol2caslSort (MSym.Sort q) _ = token2id q
maudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im
      where q' = token2id q
            err = errorId "error translate symbol"
maudeSymbol2caslSort _ _ = errorId "error translate symbol"

maudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT
maudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
maudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im
      where q' = token2id $ getName q
            err = errorId "error translate type"

-- | obtains the types of the given terms
getTypes :: [CAS.CASLTERM] -> [Id]
getTypes = mapMaybe getType

-- | extracts the type of the temr
getType :: CAS.CASLTERM -> Maybe Id
getType (CAS.Qual_var _ kind _) = Just kind
getType (CAS.Application op _ _) = case op of
            CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind
            _ -> Nothing
getType _ = Nothing

-- | generates the formulas for the rewrite predicates
rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]
rewPredicatesSens = Set.fold rewPredicateSens []

-- | generates the formulas for the rewrite predicate of the given sort
rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]
rewPredicateSens kind acc = ref : trans : acc
        where ref = reflSen kind
              trans = transSen kind

-- | creates the reflexivity predicate for the given kind
reflSen :: Id -> Named CAS.CASLFORMULA
reflSen kind = makeNamed name $ quantifyUniversally form
        where v = newVar kind
              pred_type = CAS.Pred_type [kind, kind] nullRange
              pn = CAS.Qual_pred_name rewID pred_type nullRange
              form = CAS.Predication pn [v, v] nullRange
              name = "rew_refl_" ++ show kind

-- | creates the transitivity predicate for the given kind
transSen :: Id -> Named CAS.CASLFORMULA
transSen kind = makeNamed name $ quantifyUniversally form
        where v1 = newVarIndex 1 kind
              v2 = newVarIndex 2 kind
              v3 = newVarIndex 3 kind
              pred_type = CAS.Pred_type [kind, kind] nullRange
              pn = CAS.Qual_pred_name rewID pred_type nullRange
              prem1 = CAS.Predication pn [v1, v2] nullRange
              prem2 = CAS.Predication pn [v2, v3] nullRange
              concl = CAS.Predication pn [v1, v3] nullRange
              conj_form = CAS.conjunct [prem1, prem2]
              form = CAS.mkImpl conj_form concl
              name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites
rewPredicates :: Set.Set Id -> CSign.PredMap
rewPredicates = Set.fold rewPredicate MapSet.empty

-- | generate the predicates for the rewrites of the given sort
rewPredicate :: Id -> CSign.PredMap -> CSign.PredMap
rewPredicate kind = MapSet.insert rewID $ CSign.PredType [kind, kind]

-- | create the predicates that assign sorts to each term
kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
kindPredicates = Map.foldWithKey kindPredicate Map.empty

{- | create the predicates that assign the current sort to the
corresponding terms -}
kindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)
                 -> Map.Map Id (Set.Set CSign.PredType)
kindPredicate sort kind mis = if sort == str2id "Universal" then mis else
  let ar = Set.singleton $ CSign.PredType [kind]
  in Map.insertWith Set.union sort ar mis

-- | extract the kinds from the map of id's
kindsFromMap :: IdMap -> Set.Set Id
kindsFromMap = Map.fold Set.insert Set.empty

{- | transform the set of Maude sorts in a set of CASL sorts, including
only one sort for each kind. -}
sortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id
sortsTranslation = sortsTranslationList . Set.toList

{- | transform a list representing the Maude sorts in a set of CASL sorts,
including only one sort for each kind. -}
sortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id
sortsTranslationList [] _ = Set.empty
sortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
      where tops@(top : _) = List.sort $ getTop r s
            ss' = deleteRelated ss top r
            res = sortsTranslation ss' r

-- | return the maximal elements from the sort relation
getTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
getTop r tok = case succs of
           [] -> [tok]
           toks@(_ : _) -> concatMap (getTop r) toks
      where succs = Set.toList $ Rel.succs r tok

-- | delete from the list of sorts those in the same kind that the parameter
deleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel
  -> MSign.SortSet
deleteRelated ss sym r = foldr (f sym tc) Set.empty ss
      where tc = Rel.transClosure r
            f sort trC x y = if MSym.sameKind trC sort x
                                  then y
                                  else Set.insert x y

-- | build an Id from a token with the function mkId
token2id :: Token -> Id
token2id t = mkId ts
    where ts = maudeSymbol2validCASLSymbol t

-- | build an Id from a Maude symbol
sym2id :: MSym.Symbol -> Id
sym2id = token2id . getName

-- | generates an Id from a string
str2id :: String -> Id
str2id = token2id . mkSimpleId

-- | build an Id from a list of sorts, taking the first from the ordered list
sort2id :: [MSym.Symbol] -> Id
sort2id syms = mkId sym''
     where sym : _ = List.sort syms
           sym' = getName sym
           sym'' = maudeSymbol2validCASLSymbol sym'

-- | add universal quantification of all variables in the formula
quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
quantifyUniversally form = CAS.mkForall var_decl form
      where vars = getVars form
            var_decl = listVarDecl vars

{- | traverses a map with sorts as keys and sets of variables as value and
creates a list of variable declarations -}
listVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]
listVarDecl = Map.foldWithKey f []
      where f sort var_set =
                (CAS.Var_decl (Set.toList var_set) sort nullRange :)

-- | removes a quantification from a formula
noQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])
noQuantification (CAS.Quantification _ vars form _) = (form, vars)
noQuantification form = (form, [])

-- | translate the CASL sorts to symbols
kinds2syms :: Set.Set Id -> Set.Set CSign.Symbol
kinds2syms = Set.map kind2sym

-- | translate a CASL sort to a CASL symbol
kind2sym :: Id -> CSign.Symbol
kind2sym k = CSign.Symbol k CSign.SortAsItemType

-- | translates the CASL predicates into CASL symbols
preds2syms :: CSign.PredMap -> Set.Set CSign.Symbol
preds2syms = MapSet.foldWithKey createSym4id Set.empty

-- | creates a CASL symbol for a predicate
createSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol
  -> Set.Set CSign.Symbol
createSym4id pn pt = Set.insert sym
      where sym = CSign.Symbol pn $ CSign.PredAsItemType pt

-- | translates the CASL operators into CASL symbols
ops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol
ops2symbols = MapSet.foldWithKey createSymOp4id Set.empty

-- | creates a CASL symbol for an operator
createSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol
  -> Set.Set CSign.Symbol
createSymOp4id on ot = Set.insert sym
      where sym = CSign.Symbol on $ CSign.OpAsItemType ot

{- | extract the variables from a CASL formula and put them in a map
with keys the sort of the variables and value the set of variables
in this sort -}
getVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)
getVars (CAS.Quantification _ _ f _) = getVars f
getVars (CAS.Junction _ fs _) =
    foldr (Map.unionWith Set.union . getVars) Map.empty fs
getVars (CAS.Relation f1 _ f2 _) = Map.unionWith Set.union v1 v2
     where v1 = getVars f1
           v2 = getVars f2
getVars (CAS.Negation f _) = getVars f
getVars (CAS.Predication _ ts _) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVars (CAS.Definedness t _) = getVarsTerm t
getVars (CAS.Equation t1 _ t2 _) = Map.unionWith Set.union v1 v2
     where v1 = getVarsTerm t1
           v2 = getVarsTerm t2
getVars (CAS.Membership t _ _) = getVarsTerm t
getVars (CAS.Mixfix_formula t) = getVarsTerm t
getVars _ = Map.empty

-- | extract the variables of a CASL term
getVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)
getVarsTerm (CAS.Qual_var var sort _) =
    Map.insert sort (Set.singleton var) Map.empty
getVarsTerm (CAS.Application _ ts _) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
getVarsTerm (CAS.Cast t _ _) = getVarsTerm t
getVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith Set.union v3 m
     where v1 = getVarsTerm t1
           v2 = getVarsTerm t2
           v3 = getVars f
           m = Map.unionWith Set.union v1 v2
getVarsTerm (CAS.Mixfix_term ts) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVarsTerm (CAS.Mixfix_parenthesized ts _) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVarsTerm (CAS.Mixfix_bracketed ts _) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVarsTerm (CAS.Mixfix_braced ts _) =
    foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts
getVarsTerm _ = Map.empty

-- | generates the constructor constraint
ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
ctorSen isFree (sorts, _, ops) =
    let sortList = Set.toList sorts
        opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
                      (CSign.toOP_TYPE $ compType c) $ posOfId ide)
                 $ Set.toList ops
        allSyms = opSyms
        resType _ (CAS.Op_name _) = False
        resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s
        getIndex s = fromMaybe (-1) $ List.elemIndex s sortList
        addIndices (CAS.Op_name _) =
          error "CASL/StaticAna: Internal error in function addIndices"
        addIndices os@(CAS.Qual_op_name _ t _) =
            (os, map getIndex $ CAS.args_OP_TYPE t)
        collectOps s =
          CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
        constrs = map collectOps sortList
        f = CAS.mkSort_gen_ax constrs isFree
    in makeNamed
      ("ga_generated_" ++ showSepList (showString "_") showId sortList "") f

-- | transforms a maude identifier into a valid CASL identifier
maudeSymbol2validCASLSymbol :: Token -> [Token]
maudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""
    where str = ms2vcs $ show t

{- | transforms a string coding a Maude identifier into another string
representing a CASL identifier -}
ms2vcs :: String -> String
ms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s
ms2vcs s = if Map.member s stringMap
    then stringMap Map.! s
    else let f x y
               | Map.member x charMap = (charMap Map.! x) ++ "'" ++ y
               | x == '_' = "__" ++ y
               | otherwise = x : y
         in foldr f [] s

-- | map of reserved words
stringMap :: Map.Map String String
stringMap = Map.fromList
    [("true", "maudeTrue"),
     ("false", "maudeFalse"),
     ("not_", "neg__"),
     ("s_", "suc"),
     ("_+_", "__+__"),
     ("_*_", "__*__"),
     ("_<_", "__<__"),
     ("_<=_", "__<=__"),
     ("_>_", "__>__"),
     ("_>=_", "__>=__"),
     ("_and_", "__maudeAnd__")]

{- | splits the string into a list of tokens, separating the double
underscores from the rest of characters -}
splitDoubleUnderscores :: String -> String -> [Token]
splitDoubleUnderscores [] acc = if null acc
                                then []
                                else [mkSimpleId acc]
splitDoubleUnderscores ('_' : '_' : cs) acc = if null acc
                                              then dut : rest
                                              else acct : dut : rest
     where acct = mkSimpleId acc
           dut = mkSimpleId "__"
           rest = splitDoubleUnderscores cs []
splitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])


-- | error Id
errorId :: String -> Id
errorId s = token2id $ mkSimpleId $ "ERROR: " ++ s

kindId :: Id -> Id
kindId i = token2id $ mkSimpleId $ "kind_" ++ show i

kindMapId :: MSign.KindRel -> IdMap
kindMapId kr = Map.fromList krl'
     where krl = Map.toList kr
           krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl

mSym2caslId :: MSym.Symbol -> Id
mSym2caslId (MSym.Sort q) = token2id q
mSym2caslId (MSym.Kind q) = kindId q'
      where q' = token2id q
mSym2caslId _ = errorId "error translate symbol"

-- | checks the profile has at least one sort
atLeastOneSort :: MSign.OpMap -> MSign.OpMap
atLeastOneSort om = Map.fromList lom'
      where lom = Map.toList om
            lom' = filterAtLeastOneSort lom

filterAtLeastOneSort :: [(MAS.Qid, MSign.OpDeclSet)]
  -> [(MAS.Qid, MSign.OpDeclSet)]
filterAtLeastOneSort [] = []
filterAtLeastOneSort ((q, ods) : ls) = hd ++ filterAtLeastOneSort ls
     where ods' = atLeastOneSortODS ods
           hd = if Set.null ods'
                then []
                else [(q, ods')]

atLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet
atLeastOneSortODS ods = Set.fromList lods'
     where lods = Set.toList ods
           lods' = atLeastOneSortLODS lods

atLeastOneSortLODS :: [MSign.OpDecl] -> [MSign.OpDecl]
atLeastOneSortLODS [] = []
atLeastOneSortLODS ((ss, ats) : ls) = res ++ atLeastOneSortLODS ls
     where ss' = atLeastOneSortSS ss
           res = if Set.null ss'
                 then []
                 else [(ss', ats)]

atLeastOneSortSS :: Set.Set MSym.Symbol -> Set.Set MSym.Symbol
atLeastOneSortSS = Set.filter hasOneSort

hasOneSort :: MSym.Symbol -> Bool
hasOneSort (MSym.Operator _ ar co) = any isSymSort (co : ar)
hasOneSort _ = False

isSymSort :: MSym.Symbol -> Bool
isSymSort (MSym.Sort _) = True
isSymSort _ = False

{- | translates the Maude operator map into a tuple of CASL operators, CASL
associative operators, membership induced from each Maude operator,
and the set of sorts with the ctor attribute -}
translateOps' :: IdMap -> MSign.OpMap -> OpTransTuple
translateOps' im = Map.fold (translateOpDeclSet' im)
  (MapSet.empty, MapSet.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above
translateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet' im ods tpl = Set.fold (translateOpDecl' im) tpl ods

{- | given an operator declaration updates the accumulator with the translation
to CASL operator, checking if the operator has the assoc attribute to insert
it in the map of associative operators, generating the membership predicate
induced by the operator declaration, and checking if it has the ctor
attribute to introduce the operator in the generators sentence -}
translateOpDecl' :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
translateOpDecl' im (syms, ats) (ops, assoc_ops, cs) =
        if Set.null syms'
        then (ops', assoc_ops', cs')
        else translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')
      where (sym, syms') = Set.deleteFindMin syms
            Just (cop_id, ot, _) = maudeSym2CASLOp' im sym
            ops' = MapSet.insert cop_id ot ops
            assoc_ops' = if any MAS.assoc ats
                         then MapSet.insert cop_id ot assoc_ops
                         else assoc_ops
            cs' = if any MAS.ctor ats
                  then Set.insert (Component cop_id ot) cs
                  else cs

{- | translates a Maude operator symbol into a pair with the id of the operator
and its CASL type -}
maudeSym2CASLOp' :: IdMap -> MSym.Symbol
  -> Maybe (Id, CSign.OpType, CSign.OpType)
maudeSym2CASLOp' im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
      where f = token2id . getName
            g = (`maudeSymbol2caslSort'` im)
            ot = CSign.OpType CAS.Total (map g ar) (g co)
            ot' = CSign.OpType CAS.Total (map f ar) (f co)
maudeSym2CASLOp' _ _ = Nothing

maudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT
maudeSymbol2caslSort' (MSym.Sort q) _ =
    token2id $ mkSimpleId $ "kind_" ++ show q
maudeSymbol2caslSort' (MSym.Kind q) im = Map.findWithDefault err q' im
      where q' = token2id q
            err = errorId "error translate symbol"
maudeSymbol2caslSort' _ _ = errorId "error translate symbol"
