{- |
Module      :  ./Maude/PreComorphism.hs
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 :: Morphism -> Result CASLMor
mapMorphism morph :: Morphism
morph =
         let
           src :: Sign
src = Morphism -> Sign
MMorphism.source Morphism
morph
           tgt :: Sign
tgt = Morphism -> Sign
MMorphism.target Morphism
morph
           mk :: IdMap
mk = KindRel -> IdMap
kindMapId (KindRel -> IdMap) -> KindRel -> IdMap
forall a b. (a -> b) -> a -> b
$ Sign -> KindRel
MSign.kindRel Sign
src
           mk' :: IdMap
mk' = KindRel -> IdMap
kindMapId (KindRel -> IdMap) -> KindRel -> IdMap
forall a b. (a -> b) -> a -> b
$ Sign -> KindRel
MSign.kindRel Sign
tgt
           smap :: KindRel
smap = Morphism -> KindRel
MMorphism.sortMap Morphism
morph
           omap :: KindRel
omap = Morphism -> KindRel
MMorphism.opMap Morphism
morph
           smap' :: IdMap
smap' = KindRel -> IdMap -> IdMap -> IdMap
applySortMap2CASLSorts KindRel
smap IdMap
mk IdMap
mk'
           omap' :: Op_map
omap' = IdMap -> KindRel -> Op_map
maudeOpMap2CASLOpMap IdMap
mk KindRel
omap
           pmap :: Pred_map
pmap = IdMap -> KindRel -> Pred_map
createPredMap IdMap
mk KindRel
smap
           (src' :: CASLSign
src', _) = Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA])
maude2casl Sign
src []
           (tgt' :: CASLSign
tgt', _) = Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA])
maude2casl Sign
tgt []
         in CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLMor -> Result CASLMor) -> CASLMor -> Result CASLMor
forall a b. (a -> b) -> a -> b
$ CASLSign
-> CASLSign -> IdMap -> Op_map -> Pred_map -> () -> CASLMor
forall f e m.
Sign f e
-> Sign f e -> IdMap -> Op_map -> Pred_map -> m -> Morphism f e m
CMorphism.Morphism CASLSign
src' CASLSign
tgt' IdMap
smap' Op_map
omap' Pred_map
pmap ()

{- | translates the Maude morphism between operators into a CASL morpshim
between operators -}
maudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
maudeOpMap2CASLOpMap :: IdMap -> KindRel -> Op_map
maudeOpMap2CASLOpMap im :: IdMap
im = (Symbol -> Symbol -> Op_map -> Op_map)
-> Op_map -> KindRel -> Op_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (IdMap -> Symbol -> Symbol -> Op_map -> Op_map
translateOpMapEntry IdMap
im) Op_map
forall k a. Map k a
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 :: IdMap -> Symbol -> Symbol -> Op_map -> Op_map
translateOpMapEntry im :: IdMap
im (MSym.Operator from :: Qid
from ar :: Symbols
ar co :: Symbol
co) (MSym.Operator to :: Qid
to _ _) copm :: Op_map
copm
  = Op_map
copm'
       where f :: Symbol -> Id
f = Qid -> Id
token2id (Qid -> Id) -> (Symbol -> Qid) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName
             g :: Symbol -> Id
g x :: Symbol
x = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "translate op map entry")
                 (Symbol -> Id
f Symbol
x) IdMap
im
             ot :: OpType
ot = OpKind -> [Id] -> Id -> OpType
CSign.OpType OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
g Symbols
ar) (Symbol -> Id
g Symbol
co)
             cop :: (Id, OpType)
cop = (Qid -> Id
token2id Qid
from, OpType
ot)
             to' :: (Id, OpKind)
to' = (Qid -> Id
token2id Qid
to, OpKind
CAS.Total)
             copm' :: Op_map
copm' = (Id, OpType) -> (Id, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, OpType)
cop (Id, OpKind)
to' Op_map
copm
translateOpMapEntry _ _ _ _ = Op_map
forall k a. Map k a
Map.empty

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

-- | returns the sort in CASL of the Maude sort symbol
maudeSort2caslId :: IdMap -> MSym.Symbol -> Id
maudeSort2caslId :: IdMap -> Symbol -> Id
maudeSort2caslId im :: IdMap
im sym :: Symbol
sym = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "sort to id")
                          (Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
sym) IdMap
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 :: IdMap -> KindRel -> Pred_map
createPredMap im :: IdMap
im = (Symbol -> Symbol -> Pred_map -> Pred_map)
-> Pred_map -> KindRel -> Pred_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (IdMap -> Symbol -> Symbol -> Pred_map -> Pred_map
createPredMap4sort IdMap
im) Pred_map
forall k a. Map k a
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 :: IdMap -> Symbol -> Symbol -> Pred_map -> Pred_map
createPredMap4sort im :: IdMap
im from :: Symbol
from to :: Symbol
to = (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, PredType)
key Id
id_to
           where id_from :: Id
id_from = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
from
                 id_to :: Id
id_to = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
to
                 kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "predicate for sort")
                        Id
id_from IdMap
im
                 key :: (Id, PredType)
key = (Id
id_from, [Id] -> PredType
CSign.PredType [Id
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 :: KindRel -> IdMap -> IdMap -> IdMap
applySortMap2CASLSorts sm :: KindRel
sm im :: IdMap
im im' :: IdMap
im' = [(Id, Id)] -> IdMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Id, Id)]
sml'
            where sml :: [(Symbol, Symbol)]
sml = KindRel -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList KindRel
sm
                  sml' :: [(Id, Id)]
sml' = ((Symbol, Symbol) -> [(Id, Id)] -> [(Id, Id)])
-> [(Id, Id)] -> [(Symbol, Symbol)] -> [(Id, Id)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (IdMap -> IdMap -> (Symbol, Symbol) -> [(Id, Id)] -> [(Id, Id)]
applySortMap2CASLSort IdMap
im IdMap
im') [] [(Symbol, Symbol)]
sml

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

-- | renames the sorts in a given kind
rename :: MMorphism.SortMap -> Token -> Token
rename :: KindRel -> Qid -> Qid
rename sm :: KindRel
sm tok :: Qid
tok = Qid
new_tok
          where sym :: Symbol
sym = Qid -> Symbol
MSym.Sort Qid
tok
                sym' :: Symbol
sym' = if Symbol -> KindRel -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Symbol
sym KindRel
sm
                       then Maybe Symbol -> Symbol
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Symbol -> Symbol) -> Maybe Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> KindRel -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
sym KindRel
sm
                       else Symbol
sym
                new_tok :: Qid
new_tok = Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
sym'

-- | translates a Maude sentence into a CASL formula
mapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA
mapSentence :: Sign -> Sentence -> Result CASLFORMULA
mapSentence sg :: Sign
sg sen :: Sentence
sen = let
    mk :: IdMap
mk = KindRel -> IdMap
kindMapId (KindRel -> IdMap) -> KindRel -> IdMap
forall a b. (a -> b) -> a -> b
$ Sign -> KindRel
MSign.kindRel Sign
sg
    named :: Named Sentence
named = String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" Sentence
sen
    form :: Named CASLFORMULA
form = IdMap -> Named Sentence -> Named CASLFORMULA
mb_rl2formula IdMap
mk Named Sentence
named
  in CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence (Named CASLFORMULA -> CASLFORMULA)
-> Named CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ case Sentence
sen of
       MSentence.Equation (MAS.Eq _ _ _ ats :: [StmntAttr]
ats) -> if (StmntAttr -> Bool) -> [StmntAttr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StmntAttr -> Bool
MAS.owise [StmntAttr]
ats then let
           sg_sens :: [Named Sentence]
sg_sens = (Sentence -> Named Sentence) -> [Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "") ([Sentence] -> [Named Sentence]) -> [Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ Set Sentence -> [Sentence]
forall a. Set a -> [a]
Set.toList (Set Sentence -> [Sentence]) -> Set Sentence -> [Sentence]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Sentence
MSign.sentences Sign
sg
           (no_owise_sens :: [Named Sentence]
no_owise_sens, _, _) = [Named Sentence]
-> ([Named Sentence], [Named Sentence], [Named Sentence])
splitOwiseEqs [Named Sentence]
sg_sens
           no_owise_forms :: [Named CASLFORMULA]
no_owise_forms = (Named Sentence -> Named CASLFORMULA)
-> [Named Sentence] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Named Sentence -> Named CASLFORMULA
noOwiseSen2Formula IdMap
mk) [Named Sentence]
no_owise_sens
           in IdMap -> [Named CASLFORMULA] -> Named Sentence -> Named CASLFORMULA
owiseSen2Formula IdMap
mk [Named CASLFORMULA]
no_owise_forms Named Sentence
named
           else IdMap -> Named Sentence -> Named CASLFORMULA
noOwiseSen2Formula IdMap
mk Named Sentence
named
       MSentence.Membership (MAS.Mb {}) -> Named CASLFORMULA
form
       MSentence.Rule (MAS.Rl {}) -> Named CASLFORMULA
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 :: (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory (sg :: Sign
sg, nsens :: [Named Sentence]
nsens) = (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return ((CASLSign, [Named CASLFORMULA])
 -> Result (CASLSign, [Named CASLFORMULA]))
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA])
maude2casl Sign
sg [Named Sentence]
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 :: Sign -> [Named Sentence] -> (CASLSign, [Named CASLFORMULA])
maude2casl msign :: Sign
msign nsens :: [Named Sentence]
nsens = (CASLSign
forall f. Sign f ()
csign {
                            sortRel :: Rel Id
CSign.sortRel =
                              Rel Id -> Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (Set Id -> Rel Id
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet Set Id
cs) Rel Id
sbs',
                            opMap :: OpMap
CSign.opMap = OpMap
cops',
                            assocOps :: OpMap
CSign.assocOps = OpMap
assoc_ops,
                            predMap :: PredMap
CSign.predMap = PredMap
preds,
                            declaredSymbols :: Set Symbol
CSign.declaredSymbols = Set Symbol
syms }, [Named CASLFORMULA]
new_sens)
   where csign :: Sign f ()
csign = () -> Sign f ()
forall e f. e -> Sign f e
CSign.emptySign ()
         ss :: SortSet
ss = Sign -> SortSet
MSign.sorts Sign
msign
         ss' :: Set Id
ss' = (Symbol -> Id) -> SortSet -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> Id
sym2id SortSet
ss
         mk :: IdMap
mk = KindRel -> IdMap
kindMapId (KindRel -> IdMap) -> KindRel -> IdMap
forall a b. (a -> b) -> a -> b
$ Sign -> KindRel
MSign.kindRel Sign
msign
         sbs :: SubsortRel
sbs = Sign -> SubsortRel
MSign.subsorts Sign
msign
         sbs' :: Rel Id
sbs' = SubsortRel -> IdMap -> Rel Id
maudeSbs2caslSbs SubsortRel
sbs IdMap
mk
         cs :: Set Id
cs = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
ss' (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ IdMap -> Set Id
kindsFromMap IdMap
mk
         preds :: PredMap
preds = Set Id -> PredMap
rewPredicates Set Id
cs
         rs :: [Named CASLFORMULA]
rs = Set Id -> [Named CASLFORMULA]
rewPredicatesSens Set Id
cs
         ops :: OpMap
ops = OpMap -> OpMap
deleteUniversal (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
MSign.ops Sign
msign
         ksyms :: Set Symbol
ksyms = Set Id -> Set Symbol
kinds2syms Set Id
cs
         (cops :: OpMap
cops, assoc_ops :: OpMap
assoc_ops, _) = IdMap -> OpMap -> (OpMap, OpMap, Set Component)
translateOps IdMap
mk OpMap
ops -- (cops, assoc_ops, comps)
         axSens :: [Named CASLFORMULA]
axSens = IdMap -> OpMap -> [Named CASLFORMULA]
axiomsSens IdMap
mk OpMap
ops
         ctor_sen :: [a]
ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
         cops' :: OpMap
cops' = Set Id -> OpMap -> Bool -> OpMap
universalOps Set Id
cs OpMap
cops (Bool -> OpMap) -> Bool -> OpMap
forall a b. (a -> b) -> a -> b
$ OpMap -> Bool
booleanImported OpMap
ops
         rs' :: [Named CASLFORMULA]
rs' = OpMap -> [Named CASLFORMULA]
rewPredicatesCongSens OpMap
cops'
         pred_forms :: [Named CASLFORMULA]
pred_forms = SortSet -> OpMap -> [Named CASLFORMULA]
loadLibraries (Sign -> SortSet
MSign.sorts Sign
msign) OpMap
ops
         ops_syms :: Set Symbol
ops_syms = OpMap -> Set Symbol
ops2symbols OpMap
cops'
         (no_owise_sens :: [Named Sentence]
no_owise_sens, owise_sens :: [Named Sentence]
owise_sens, mbs_rls_sens :: [Named Sentence]
mbs_rls_sens) = [Named Sentence]
-> ([Named Sentence], [Named Sentence], [Named Sentence])
splitOwiseEqs [Named Sentence]
nsens
         no_owise_forms :: [Named CASLFORMULA]
no_owise_forms = (Named Sentence -> Named CASLFORMULA)
-> [Named Sentence] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Named Sentence -> Named CASLFORMULA
noOwiseSen2Formula IdMap
mk) [Named Sentence]
no_owise_sens
         owise_forms :: [Named CASLFORMULA]
owise_forms = (Named Sentence -> Named CASLFORMULA)
-> [Named Sentence] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> [Named CASLFORMULA] -> Named Sentence -> Named CASLFORMULA
owiseSen2Formula IdMap
mk [Named CASLFORMULA]
no_owise_forms) [Named Sentence]
owise_sens
         mb_rl_forms :: [Named CASLFORMULA]
mb_rl_forms = (Named Sentence -> Named CASLFORMULA)
-> [Named Sentence] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (IdMap -> Named Sentence -> Named CASLFORMULA
mb_rl2formula IdMap
mk) [Named Sentence]
mbs_rls_sens
         preds_syms :: Set Symbol
preds_syms = PredMap -> Set Symbol
preds2syms PredMap
preds
         syms :: Set Symbol
syms = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
ksyms (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Symbol
ops_syms Set Symbol
preds_syms
         new_sens :: [Named CASLFORMULA]
new_sens = [[Named CASLFORMULA]] -> [Named CASLFORMULA]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Named CASLFORMULA]
rs, [Named CASLFORMULA]
rs', [Named CASLFORMULA]
no_owise_forms, [Named CASLFORMULA]
owise_forms,
                            [Named CASLFORMULA]
mb_rl_forms, [Named CASLFORMULA]
forall a. [a]
ctor_sen, [Named CASLFORMULA]
pred_forms, [Named CASLFORMULA]
axSens]

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

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

maudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
maudeSb2caslSb :: (Symbol, SortSet) -> (Id, Set Id)
maudeSb2caslSb (sym :: Symbol
sym, st :: SortSet
st) = (Symbol -> Id
sortSym2id Symbol
sym, (Symbol -> Id) -> SortSet -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Id -> Id
kindId (Id -> Id) -> (Symbol -> Id) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Id
sortSym2id) SortSet
st)

subsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)
subsorts2Ids :: (Symbol, SortSet) -> (Id, Set Id)
subsorts2Ids (sym :: Symbol
sym, st :: SortSet
st) = (Symbol -> Id
sortSym2id Symbol
sym, (Symbol -> Id) -> SortSet -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> Id
sortSym2id SortSet
st)

sortSym2id :: MSym.Symbol -> Id
sortSym2id :: Symbol -> Id
sortSym2id (MSym.Sort q :: Qid
q) = Qid -> Id
token2id Qid
q
sortSym2id _ = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ String -> Qid
mkSimpleId "error_translation"

-- | generates the sentences to state that the rew predicates are a congruence
rewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]
rewPredicatesCongSens :: OpMap -> [Named CASLFORMULA]
rewPredicatesCongSens = (Id -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> OpMap -> [Named CASLFORMULA]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey Id -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA]
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 :: Id -> OpType -> [Named CASLFORMULA] -> [Named CASLFORMULA]
rewPredCong op :: Id
op ot :: OpType
ot fs :: [Named CASLFORMULA]
fs = case [Id]
args of
                        [] -> [Named CASLFORMULA]
fs
                        _ -> Named CASLFORMULA
nq_form Named CASLFORMULA -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. a -> [a] -> [a]
: [Named CASLFORMULA]
fs
       where args :: [Id]
args = OpType -> [Id]
CSign.opArgs OpType
ot
             vars1 :: [CASLTERM]
vars1 = Int -> [Id] -> [CASLTERM]
rewPredCongPremise 0 [Id]
args
             vars2 :: [CASLTERM]
vars2 = Int -> [Id] -> [CASLTERM]
rewPredCongPremise ([Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args) [Id]
args
             res :: Id
res = OpType -> Id
CSign.opRes OpType
ot
             res_pred_type :: PRED_TYPE
res_pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
res, Id
res] Range
nullRange
             pn :: PRED_SYMB
pn = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
res_pred_type Range
nullRange
             name :: String
name = "rew_cong_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
op
             prems :: [CASLFORMULA]
prems = [Id] -> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
rewPredsCong [Id]
args [CASLTERM]
vars1 [CASLTERM]
vars2
             prems_conj :: CASLFORMULA
prems_conj = [CASLFORMULA] -> CASLFORMULA
createConjForm [CASLFORMULA]
prems
             os :: OP_SYMB
os = Id -> OP_TYPE -> Range -> OP_SYMB
CAS.Qual_op_name Id
op (OpType -> OP_TYPE
CSign.toOP_TYPE OpType
ot) Range
nullRange
             conc_term1 :: CASLTERM
conc_term1 = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CAS.Application OP_SYMB
os [CASLTERM]
vars1 Range
nullRange
             conc_term2 :: CASLTERM
conc_term2 = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CAS.Application OP_SYMB
os [CASLTERM]
vars2 Range
nullRange
             conc_form :: CASLFORMULA
conc_form = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pn [CASLTERM
conc_term1, CASLTERM
conc_term2] Range
nullRange
             form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
createImpForm CASLFORMULA
prems_conj CASLFORMULA
conc_form
             nq_form :: Named CASLFORMULA
nq_form = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
name (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form

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

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

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

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

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

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

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

specialZeroSet :: MSign.OpDeclSet -> Bool
specialZeroSet :: OpDeclSet -> Bool
specialZeroSet = (OpDecl -> Bool -> Bool) -> Bool -> OpDeclSet -> Bool
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold OpDecl -> Bool -> Bool
specialZero Bool
False

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

isSpecial :: [MAS.Attr] -> Bool
isSpecial :: [Attr] -> Bool
isSpecial [] = Bool
False
isSpecial (MAS.Special _ : _) = Bool
True
isSpecial (_ : ats :: [Attr]
ats) = [Attr] -> Bool
isSpecial [Attr]
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 :: OpMap -> OpMap
deleteUniversal om :: OpMap
om = OpMap
om5
         where om1 :: OpMap
om1 = Qid -> OpMap -> OpMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (String -> Qid
mkSimpleId "if_then_else_fi") OpMap
om
               om2 :: OpMap
om2 = Qid -> OpMap -> OpMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (String -> Qid
mkSimpleId "_==_") OpMap
om1
               om3 :: OpMap
om3 = Qid -> OpMap -> OpMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (String -> Qid
mkSimpleId "_=/=_") OpMap
om2
               om4 :: OpMap
om4 = Qid -> OpMap -> OpMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (String -> Qid
mkSimpleId "upTerm") OpMap
om3
               om5 :: OpMap
om5 = Qid -> OpMap -> OpMap
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete (String -> Qid
mkSimpleId "downTerm") OpMap
om4

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

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

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

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

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

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

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

-- | generates the sentences for the operator attributes
axiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]
axiomsSens :: IdMap -> OpMap -> [Named CASLFORMULA]
axiomsSens im :: IdMap
im = (OpDeclSet -> [Named CASLFORMULA] -> [Named CASLFORMULA])
-> [Named CASLFORMULA] -> OpMap -> [Named CASLFORMULA]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (IdMap -> OpDeclSet -> [Named CASLFORMULA] -> [Named CASLFORMULA]
axiomsSensODS IdMap
im) []

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

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

axiomsSensSS :: IdMap -> [MAS.Attr] -> MSym.Symbol -> [Named CAS.CASLFORMULA]
  -> [Named CAS.CASLFORMULA]
axiomsSensSS :: IdMap
-> [Attr] -> Symbol -> [Named CASLFORMULA] -> [Named CASLFORMULA]
axiomsSensSS im :: IdMap
im ats :: [Attr]
ats (MSym.Operator q :: Qid
q ar :: Symbols
ar co :: Symbol
co) l :: [Named CASLFORMULA]
l = [Named CASLFORMULA]
l [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
l1
       where l1 :: [Named CASLFORMULA]
l1 = if Attr -> [Attr] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Attr
MAS.Comm [Attr]
ats
                  then IdMap -> Qid -> Symbols -> Symbol -> [Named CASLFORMULA]
commSen IdMap
im Qid
q Symbols
ar Symbol
co
                  else []
axiomsSensSS _ _ _ l :: [Named CASLFORMULA]
l = [Named CASLFORMULA]
l

commSen :: IdMap -> MAS.Qid -> MSym.Symbols -> MSym.Symbol
  -> [Named CAS.CASLFORMULA]
commSen :: IdMap -> Qid -> Symbols -> Symbol -> [Named CASLFORMULA]
commSen im :: IdMap
im q :: Qid
q ar :: Symbols
ar@[ar1 :: Symbol
ar1, ar2 :: Symbol
ar2] co :: Symbol
co = [Named CASLFORMULA
form']
       where q' :: Id
q' = Qid -> Id
token2id Qid
q
             f :: Symbol -> Id
f = (Symbol -> IdMap -> Id
`maudeSymbol2caslSort` IdMap
im)
             ar1' :: Id
ar1' = Symbol -> Id
f Symbol
ar1
             ar2' :: Id
ar2' = Symbol -> Id
f Symbol
ar2
             ot :: OP_TYPE
ot = OpKind -> [Id] -> Id -> Range -> OP_TYPE
CAS.Op_type OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
f Symbols
ar) (Symbol -> Id
f Symbol
co) Range
nullRange
             os :: OP_SYMB
os = Id -> OP_TYPE -> Range -> OP_SYMB
CAS.Qual_op_name Id
q' OP_TYPE
ot Range
nullRange
             v1 :: CASLTERM
v1 = Int -> Id -> CASLTERM
newVarIndex 1 Id
ar1'
             v2 :: CASLTERM
v2 = Int -> Id -> CASLTERM
newVarIndex 2 Id
ar2'
             t1 :: CASLTERM
t1 = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CAS.Application OP_SYMB
os [CASLTERM
v1, CASLTERM
v2] Range
nullRange
             t2 :: CASLTERM
t2 = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CAS.Application OP_SYMB
os [CASLTERM
v2, CASLTERM
v1] Range
nullRange
             form :: CASLFORMULA
form = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
t1 CASLTERM
t2
             name :: String
name = "comm_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
ms2vcs (Id -> String
forall a. Show a => a -> String
show Id
q') String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
ar1'
             form' :: Named CASLFORMULA
form' = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
name (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
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 :: IdMap -> OpMap -> (OpMap, OpMap, Set Component)
translateOps im :: IdMap
im = (OpDeclSet
 -> (OpMap, OpMap, Set Component) -> (OpMap, OpMap, Set Component))
-> (OpMap, OpMap, Set Component)
-> OpMap
-> (OpMap, OpMap, Set Component)
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (IdMap
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDeclSet IdMap
im)
  (OpMap
forall a b. MapSet a b
MapSet.empty, OpMap
forall a b. MapSet a b
MapSet.empty, Set Component
forall a. Set a
Set.empty)

-- | translates an operator declaration set into a tern as described above
translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet :: IdMap
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDeclSet im :: IdMap
im ods :: OpDeclSet
ods tpl :: (OpMap, OpMap, Set Component)
tpl = (OpDecl
 -> (OpMap, OpMap, Set Component) -> (OpMap, OpMap, Set Component))
-> (OpMap, OpMap, Set Component)
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl IdMap
im) (OpMap, OpMap, Set Component)
tpl OpDeclSet
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 :: IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl im :: IdMap
im (syms :: SortSet
syms, ats :: [Attr]
ats) (ops :: OpMap
ops, assoc_ops :: OpMap
assoc_ops, cs :: Set Component
cs) = case Symbols
tl of
        [] -> (OpMap
ops', OpMap
assoc_ops', Set Component
cs')
        _ -> IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl IdMap
im (SortSet
syms', [Attr]
ats) (OpMap
ops', OpMap
assoc_ops', Set Component
cs')
      where sym :: Symbol
sym : tl :: Symbols
tl = SortSet -> Symbols
forall a. Set a -> [a]
Set.toList SortSet
syms
            syms' :: SortSet
syms' = Symbols -> SortSet
forall a. Ord a => [a] -> Set a
Set.fromList Symbols
tl
            (cop_id :: Id
cop_id, ot :: OpType
ot, _) = Maybe (Id, OpType, OpType) -> (Id, OpType, OpType)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Id, OpType, OpType) -> (Id, OpType, OpType))
-> Maybe (Id, OpType, OpType) -> (Id, OpType, OpType)
forall a b. (a -> b) -> a -> b
$ IdMap -> Symbol -> Maybe (Id, OpType, OpType)
maudeSym2CASLOp IdMap
im Symbol
sym
            ops' :: OpMap
ops' = Id -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
cop_id OpType
ot OpMap
ops
            assoc_ops' :: OpMap
assoc_ops' = if (Attr -> Bool) -> [Attr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
MAS.assoc [Attr]
ats
                         then Id -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
cop_id OpType
ot OpMap
assoc_ops
                         else OpMap
assoc_ops
            cs' :: Set Component
cs' = if (Attr -> Bool) -> [Attr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
MAS.ctor [Attr]
ats
                  then Component -> Set Component -> Set Component
forall a. Ord a => a -> Set a -> Set a
Set.insert (Id -> OpType -> Component
Component Id
cop_id OpType
ot) Set Component
cs
                  else Set Component
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 :: IdMap -> Symbol -> Maybe (Id, OpType, OpType)
maudeSym2CASLOp im :: IdMap
im (MSym.Operator op :: Qid
op ar :: Symbols
ar co :: Symbol
co) = (Id, OpType, OpType) -> Maybe (Id, OpType, OpType)
forall a. a -> Maybe a
Just (Qid -> Id
token2id Qid
op, OpType
ot, OpType
ot')
      where f :: Symbol -> Id
f = Qid -> Id
token2id (Qid -> Id) -> (Symbol -> Qid) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName
            g :: Symbol -> Id
g = (Symbol -> IdMap -> Id
`maudeSymbol2caslSort` IdMap
im)
            ot :: OpType
ot = OpKind -> [Id] -> Id -> OpType
CSign.OpType OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
g Symbols
ar) (Symbol -> Id
g Symbol
co)
            ot' :: OpType
ot' = OpKind -> [Id] -> Id -> OpType
CSign.OpType OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
f Symbols
ar) (Symbol -> Id
f Symbol
co)
maudeSym2CASLOp _ _ = Maybe (Id, OpType, OpType)
forall a. Maybe a
Nothing

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

-- | creates a implication formula distinguishing the size of the premises
createImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA
createImpForm :: CASLFORMULA -> CASLFORMULA -> CASLFORMULA
createImpForm (CAS.Atom True _) form :: CASLFORMULA
form = CASLFORMULA
form
createImpForm form1 :: CASLFORMULA
form1 form2 :: CASLFORMULA
form2 = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CAS.mkImpl CASLFORMULA
form1 CASLFORMULA
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 :: IdMap -> Symbols -> Int -> ([CASLTERM], [CASLFORMULA])
ops2predPremises im :: IdMap
im (MSym.Sort s :: Qid
s : ss :: Symbols
ss) i :: Int
i = (CASLTERM
var CASLTERM -> [CASLTERM] -> [CASLTERM]
forall a. a -> [a] -> [a]
: [CASLTERM]
terms, CASLFORMULA
form CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
forms)
         where s' :: Id
s' = Qid -> Id
token2id Qid
s
               kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "mb of op as predicate")
                      Id
s' IdMap
im
               pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind] Range
nullRange
               pred_name :: PRED_SYMB
pred_name = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
s' PRED_TYPE
pred_type Range
nullRange
               var :: CASLTERM
var = Int -> Id -> CASLTERM
newVarIndex Int
i Id
kind
               form :: CASLFORMULA
form = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pred_name [CASLTERM
var] Range
nullRange
               (terms :: [CASLTERM]
terms, forms :: [CASLFORMULA]
forms) = IdMap -> Symbols -> Int -> ([CASLTERM], [CASLFORMULA])
ops2predPremises IdMap
im Symbols
ss (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
ops2predPremises im :: IdMap
im (MSym.Kind k :: Qid
k : ss :: Symbols
ss) i :: Int
i = (CASLTERM
var CASLTERM -> [CASLTERM] -> [CASLTERM]
forall a. a -> [a] -> [a]
: [CASLTERM]
terms, [CASLFORMULA]
forms)
         where k' :: Id
k' = Qid -> Id
token2id Qid
k
               kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "mb of op as predicate")
                      Id
k' IdMap
im
               var :: CASLTERM
var = Int -> Id -> CASLTERM
newVarIndex Int
i Id
kind
               (terms :: [CASLTERM]
terms, forms :: [CASLFORMULA]
forms) = IdMap -> Symbols -> Int -> ([CASLTERM], [CASLFORMULA])
ops2predPremises IdMap
im Symbols
ss (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 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 :: [Named Sentence]
-> ([Named Sentence], [Named Sentence], [Named Sentence])
splitOwiseEqs [] = ([], [], [])
splitOwiseEqs (s :: Named Sentence
s : ss :: [Named Sentence]
ss) = ([Named Sentence], [Named Sentence], [Named Sentence])
res
        where (no_owise_sens :: [Named Sentence]
no_owise_sens, owise_sens :: [Named Sentence]
owise_sens, mbs_rls :: [Named Sentence]
mbs_rls) = [Named Sentence]
-> ([Named Sentence], [Named Sentence], [Named Sentence])
splitOwiseEqs [Named Sentence]
ss
              sen :: Sentence
sen = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s
              res :: ([Named Sentence], [Named Sentence], [Named Sentence])
res = case Sentence
sen of
                     MSentence.Equation (MAS.Eq _ _ _ ats :: [StmntAttr]
ats) ->
                       if (StmntAttr -> Bool) -> [StmntAttr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any StmntAttr -> Bool
MAS.owise [StmntAttr]
ats
                       then ([Named Sentence]
no_owise_sens, Named Sentence
s Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
owise_sens, [Named Sentence]
mbs_rls)
                       else (Named Sentence
s Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
no_owise_sens, [Named Sentence]
owise_sens, [Named Sentence]
mbs_rls)
                     _ -> ([Named Sentence]
no_owise_sens, [Named Sentence]
owise_sens, Named Sentence
s Named Sentence -> [Named Sentence] -> [Named Sentence]
forall a. a -> [a] -> [a]
: [Named Sentence]
mbs_rls)

{- | translates a Maude equation defined without the "owise" attribute into
a CASL formula -}
noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
  -> Named CAS.CASLFORMULA
noOwiseSen2Formula :: IdMap -> Named Sentence -> Named CASLFORMULA
noOwiseSen2Formula im :: IdMap
im s :: Named Sentence
s = Named CASLFORMULA
s'
       where MSentence.Equation eq :: Equation
eq = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s
             sen' :: CASLFORMULA
sen' = IdMap -> Equation -> CASLFORMULA
noOwiseEq2Formula IdMap
im Equation
eq
             s' :: Named CASLFORMULA
s' = Named Sentence
s { sentence :: CASLFORMULA
sentence = CASLFORMULA
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 :: IdMap -> [Named CASLFORMULA] -> Named Sentence -> Named CASLFORMULA
owiseSen2Formula im :: IdMap
im owise_forms :: [Named CASLFORMULA]
owise_forms s :: Named Sentence
s = Named CASLFORMULA
s'
       where MSentence.Equation eq :: Equation
eq = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
s
             sen' :: CASLFORMULA
sen' = IdMap -> [Named CASLFORMULA] -> Equation -> CASLFORMULA
owiseEq2Formula IdMap
im [Named CASLFORMULA]
owise_forms Equation
eq
             s' :: Named CASLFORMULA
s' = Named Sentence
s { sentence :: CASLFORMULA
sentence = CASLFORMULA
sen' }

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

-- | generates a new variable qualified with the given number
newVarIndex :: Int -> Id -> CAS.CASLTERM
newVarIndex :: Int -> Id -> CASLTERM
newVarIndex i :: Int
i sort :: Id
sort = Qid -> Id -> Range -> CASLTERM
forall f. Qid -> Id -> Range -> TERM f
CAS.Qual_var Qid
var Id
sort Range
nullRange
    where var :: Qid
var = String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ 'V' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i

-- | generates a new variable
newVar :: Id -> CAS.CASLTERM
newVar :: Id -> CASLTERM
newVar sort :: Id
sort = Qid -> Id -> Range -> CASLTERM
forall f. Qid -> Id -> Range -> TERM f
CAS.Qual_var Qid
var Id
sort Range
nullRange
    where var :: Qid
var = String -> Qid
mkSimpleId "V"

-- | Id for the rew predicate
rewID :: Id
rewID :: Id
rewID = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ String -> Qid
mkSimpleId "rew"

{- | translates a Maude equation without the "owise" attribute into a CASL
formula -}
noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA
noOwiseEq2Formula :: IdMap -> Equation -> CASLFORMULA
noOwiseEq2Formula im :: IdMap
im (MAS.Eq t :: Term
t t' :: Term
t' [] _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
      where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
            ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
            form :: CASLFORMULA
form = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
ct CASLTERM
ct'
noOwiseEq2Formula im :: IdMap
im (MAS.Eq t :: Term
t t' :: Term
t' conds :: [Condition]
conds@(_ : _) _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
      where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
            ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
            conds_form :: CASLFORMULA
conds_form = IdMap -> [Condition] -> CASLFORMULA
conds2formula IdMap
im [Condition]
conds
            concl_form :: CASLFORMULA
concl_form = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
ct CASLTERM
ct'
            form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
createImpForm CASLFORMULA
conds_form CASLFORMULA
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 :: IdMap -> [Named CASLFORMULA] -> Equation -> CASLFORMULA
owiseEq2Formula im :: IdMap
im no_owise_form :: [Named CASLFORMULA]
no_owise_form eq :: Equation
eq = CASLFORMULA
form
      where (eq_form :: CASLFORMULA
eq_form, vars :: [VAR_DECL]
vars) = CASLFORMULA -> (CASLFORMULA, [VAR_DECL])
noQuantification (CASLFORMULA -> (CASLFORMULA, [VAR_DECL]))
-> CASLFORMULA -> (CASLFORMULA, [VAR_DECL])
forall a b. (a -> b) -> a -> b
$ IdMap -> Equation -> CASLFORMULA
noOwiseEq2Formula IdMap
im Equation
eq
            (op :: OP_SYMB
op, ts :: [CASLTERM]
ts, _) = Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
 -> (OP_SYMB, [CASLTERM], [CASLFORMULA]))
-> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
getLeftApp CASLFORMULA
eq_form
            ex_form :: CASLFORMULA
ex_form = OP_SYMB -> [CASLTERM] -> [Named CASLFORMULA] -> CASLFORMULA
existencialNegationOtherEqs OP_SYMB
op [CASLTERM]
ts [Named CASLFORMULA]
no_owise_form
            imp_form :: CASLFORMULA
imp_form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
createImpForm CASLFORMULA
ex_form CASLFORMULA
eq_form
            form :: CASLFORMULA
form = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
CAS.mkForall [VAR_DECL]
vars CASLFORMULA
imp_form

-- | generates a conjunction of negation of existencial quantifiers
existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->
                               [Named CAS.CASLFORMULA] -> CAS.CASLFORMULA
existencialNegationOtherEqs :: OP_SYMB -> [CASLTERM] -> [Named CASLFORMULA] -> CASLFORMULA
existencialNegationOtherEqs op :: OP_SYMB
op ts :: [CASLTERM]
ts forms :: [Named CASLFORMULA]
forms = CASLFORMULA
form
      where ex_forms :: [CASLFORMULA]
ex_forms = (Named CASLFORMULA -> [CASLFORMULA])
-> [Named CASLFORMULA] -> [CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (OP_SYMB -> [CASLTERM] -> Named CASLFORMULA -> [CASLFORMULA]
existencialNegationOtherEq OP_SYMB
op [CASLTERM]
ts) [Named CASLFORMULA]
forms
            form :: CASLFORMULA
form = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CAS.conjunct [CASLFORMULA]
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 :: OP_SYMB -> [CASLTERM] -> Named CASLFORMULA -> [CASLFORMULA]
existencialNegationOtherEq req_op :: OP_SYMB
req_op terms :: [CASLTERM]
terms form :: Named CASLFORMULA
form = if Bool
ok then let
                     (_, ts :: [CASLTERM]
ts, conds :: [CASLFORMULA]
conds) = Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
tpl
                     ts' :: [CASLTERM]
ts' = [CASLTERM] -> [CASLTERM]
qualifyExVarsTerms [CASLTERM]
ts
                     conds' :: [CASLFORMULA]
conds' = [CASLFORMULA] -> [CASLFORMULA]
qualifyExVarsForms [CASLFORMULA]
conds
                     prems :: [CASLFORMULA]
prems = [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
createEqs [CASLTERM]
ts' [CASLTERM]
terms [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
conds'
                     conj_form :: CASLFORMULA
conj_form = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CAS.conjunct [CASLFORMULA]
prems
                     ex_form :: CASLFORMULA
ex_form = if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
vars' then CASLFORMULA
conj_form else
                               [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
CAS.mkExist [VAR_DECL]
vars' CASLFORMULA
conj_form
                     neg_form :: CASLFORMULA
neg_form = CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CAS.mkNeg CASLFORMULA
ex_form
                          in [CASLFORMULA
neg_form]
                else []
      where (inner_form :: CASLFORMULA
inner_form, vars :: [VAR_DECL]
vars) = CASLFORMULA -> (CASLFORMULA, [VAR_DECL])
noQuantification (CASLFORMULA -> (CASLFORMULA, [VAR_DECL]))
-> CASLFORMULA -> (CASLFORMULA, [VAR_DECL])
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
form
            vars' :: [VAR_DECL]
vars' = [VAR_DECL] -> [VAR_DECL]
qualifyExVars [VAR_DECL]
vars
            tpl :: Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
tpl = CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
getLeftApp CASLFORMULA
inner_form
            ok :: Bool
ok = case Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
tpl of
                  Nothing -> Bool
False
                  Just _ -> let (op :: OP_SYMB
op, ts :: [CASLTERM]
ts, _) = Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. HasCallStack => Maybe a -> a
fromJust Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
tpl
                            in OP_SYMB
req_op OP_SYMB -> OP_SYMB -> Bool
forall a. Eq a => a -> a -> Bool
== OP_SYMB
op Bool -> Bool -> Bool
&& [CASLTERM] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CASLTERM]
terms Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [CASLTERM] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CASLTERM]
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 :: [CASLFORMULA] -> [CASLFORMULA]
qualifyExVarsForms = (CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
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 :: CASLFORMULA -> CASLFORMULA
qualifyExVarsForm (CAS.Equation t :: CASLTERM
t CAS.Strong t' :: CASLTERM
t' r :: Range
r) =
    CASLTERM -> Equality -> CASLTERM -> Range -> CASLFORMULA
forall f. TERM f -> Equality -> TERM f -> Range -> FORMULA f
CAS.Equation CASLTERM
qt Equality
CAS.Strong CASLTERM
qt' Range
r
        where qt :: CASLTERM
qt = CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t
              qt' :: CASLTERM
qt' = CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t'
qualifyExVarsForm (CAS.Predication op :: PRED_SYMB
op ts :: [CASLTERM]
ts r :: Range
r) = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
op [CASLTERM]
ts' Range
r
        where ts' :: [CASLTERM]
ts' = [CASLTERM] -> [CASLTERM]
qualifyExVarsTerms [CASLTERM]
ts
qualifyExVarsForm f :: CASLFORMULA
f = CASLFORMULA
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 :: [CASLTERM] -> [CASLTERM]
qualifyExVarsTerms = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
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 :: CASLTERM -> CASLTERM
qualifyExVarsTerm (CAS.Qual_var var :: Qid
var sort :: Id
sort r :: Range
r) =
    Qid -> Id -> Range -> CASLTERM
forall f. Qid -> Id -> Range -> TERM f
CAS.Qual_var (Qid -> Qid
qualifyExVarAux Qid
var) Id
sort Range
r
qualifyExVarsTerm (CAS.Application op :: OP_SYMB
op ts :: [CASLTERM]
ts r :: Range
r) = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CAS.Application OP_SYMB
op [CASLTERM]
ts' Range
r
           where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
qualifyExVarsTerm [CASLTERM]
ts
qualifyExVarsTerm (CAS.Sorted_term t :: CASLTERM
t s :: Id
s r :: Range
r) =
    CASLTERM -> Id -> Range -> CASLTERM
forall f. TERM f -> Id -> Range -> TERM f
CAS.Sorted_term (CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t) Id
s Range
r
qualifyExVarsTerm (CAS.Cast t :: CASLTERM
t s :: Id
s r :: Range
r) = CASLTERM -> Id -> Range -> CASLTERM
forall f. TERM f -> Id -> Range -> TERM f
CAS.Cast (CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t) Id
s Range
r
qualifyExVarsTerm (CAS.Conditional t1 :: CASLTERM
t1 f :: CASLFORMULA
f t2 :: CASLTERM
t2 r :: Range
r) = CASLTERM -> CASLFORMULA -> CASLTERM -> Range -> CASLTERM
forall f. TERM f -> FORMULA f -> TERM f -> Range -> TERM f
CAS.Conditional CASLTERM
t1' CASLFORMULA
f CASLTERM
t2' Range
r
     where t1' :: CASLTERM
t1' = CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t1
           t2' :: CASLTERM
t2' = CASLTERM -> CASLTERM
qualifyExVarsTerm CASLTERM
t2
qualifyExVarsTerm (CAS.Mixfix_term ts :: [CASLTERM]
ts) = [CASLTERM] -> CASLTERM
forall f. [TERM f] -> TERM f
CAS.Mixfix_term [CASLTERM]
ts'
           where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
qualifyExVarsTerm [CASLTERM]
ts
qualifyExVarsTerm (CAS.Mixfix_parenthesized ts :: [CASLTERM]
ts r :: Range
r) =
    [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
CAS.Mixfix_parenthesized [CASLTERM]
ts' Range
r
           where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
qualifyExVarsTerm [CASLTERM]
ts
qualifyExVarsTerm (CAS.Mixfix_bracketed ts :: [CASLTERM]
ts r :: Range
r) = [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
CAS.Mixfix_bracketed [CASLTERM]
ts' Range
r
           where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
qualifyExVarsTerm [CASLTERM]
ts
qualifyExVarsTerm (CAS.Mixfix_braced ts :: [CASLTERM]
ts r :: Range
r) = [CASLTERM] -> Range -> CASLTERM
forall f. [TERM f] -> Range -> TERM f
CAS.Mixfix_braced [CASLTERM]
ts' Range
r
           where ts' :: [CASLTERM]
ts' = (CASLTERM -> CASLTERM) -> [CASLTERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map CASLTERM -> CASLTERM
qualifyExVarsTerm [CASLTERM]
ts
qualifyExVarsTerm t :: CASLTERM
t = CASLTERM
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 :: [VAR_DECL] -> [VAR_DECL]
qualifyExVars = (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> VAR_DECL
qualifyExVar

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

-- | qualifies a token with the suffix "_ex"
qualifyExVarAux :: Token -> Token
qualifyExVarAux :: Qid -> Qid
qualifyExVarAux var :: Qid
var = String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ Qid -> String
forall a. Show a => a -> String
show Qid
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_ex"

-- | creates a list of strong equalities from two lists of terms
createEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]
createEqs :: [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
createEqs (t1 :: CASLTERM
t1 : ts1 :: [CASLTERM]
ts1) (t2 :: CASLTERM
t2 : ts2 :: [CASLTERM]
ts2) = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
t1 CASLTERM
t2 CASLFORMULA -> [CASLFORMULA] -> [CASLFORMULA]
forall a. a -> [a] -> [a]
: [CASLFORMULA]
ls
      where ls :: [CASLFORMULA]
ls = [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
createEqs [CASLTERM]
ts1 [CASLTERM]
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 :: CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
getLeftApp (CAS.Equation term :: CASLTERM
term CAS.Strong _ _) = case CASLTERM -> Maybe (OP_SYMB, [CASLTERM])
getLeftAppTerm CASLTERM
term of
                    Nothing -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. Maybe a
Nothing
                    Just (op :: OP_SYMB
op, ts :: [CASLTERM]
ts) -> (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. a -> Maybe a
Just (OP_SYMB
op, [CASLTERM]
ts, [])
getLeftApp (CAS.Relation prem :: CASLFORMULA
prem c :: Relation
c concl :: CASLFORMULA
concl _) = case CASLFORMULA -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
getLeftApp CASLFORMULA
concl of
       Just (op :: OP_SYMB
op, ts :: [CASLTERM]
ts, _) | Relation
c Relation -> Relation -> Bool
forall a. Eq a => a -> a -> Bool
/= Relation
CAS.Equivalence -> (OP_SYMB, [CASLTERM], [CASLFORMULA])
-> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. a -> Maybe a
Just (OP_SYMB
op, [CASLTERM]
ts, [CASLFORMULA]
conds)
           where conds :: [CASLFORMULA]
conds = CASLFORMULA -> [CASLFORMULA]
getPremisesImplication CASLFORMULA
prem
       _ -> Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. Maybe a
Nothing
getLeftApp _ = Maybe (OP_SYMB, [CASLTERM], [CASLFORMULA])
forall a. Maybe a
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 :: CASLTERM -> Maybe (OP_SYMB, [CASLTERM])
getLeftAppTerm (CAS.Application op :: OP_SYMB
op ts :: [CASLTERM]
ts _) = (OP_SYMB, [CASLTERM]) -> Maybe (OP_SYMB, [CASLTERM])
forall a. a -> Maybe a
Just (OP_SYMB
op, [CASLTERM]
ts)
getLeftAppTerm _ = Maybe (OP_SYMB, [CASLTERM])
forall a. Maybe a
Nothing

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

-- | translate a Maude membership into a CASL formula
mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA
mb2formula :: IdMap -> Membership -> CASLFORMULA
mb2formula im :: IdMap
im (MAS.Mb t :: Term
t s :: Sort
s [] _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
      where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
            s' :: Id
s' = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Sort -> Qid
forall a. HasName a => a -> Qid
getName Sort
s
            form :: CASLFORMULA
form = CASLTERM -> Id -> Range -> CASLFORMULA
forall f. TERM f -> Id -> Range -> FORMULA f
CAS.Membership CASLTERM
ct Id
s' Range
nullRange
mb2formula im :: IdMap
im (MAS.Mb t :: Term
t s :: Sort
s conds :: [Condition]
conds@(_ : _) _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
      where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
            s' :: Id
s' = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Sort -> Qid
forall a. HasName a => a -> Qid
getName Sort
s
            conds_form :: CASLFORMULA
conds_form = IdMap -> [Condition] -> CASLFORMULA
conds2formula IdMap
im [Condition]
conds
            concl_form :: CASLFORMULA
concl_form = CASLTERM -> Id -> Range -> CASLFORMULA
forall f. TERM f -> Id -> Range -> FORMULA f
CAS.Membership CASLTERM
ct Id
s' Range
nullRange
            form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CAS.mkImpl CASLFORMULA
conds_form CASLFORMULA
concl_form

-- | translate a Maude rule into a CASL formula
rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA
rl2formula :: IdMap -> Rule -> CASLFORMULA
rl2formula im :: IdMap
im (MAS.Rl t :: Term
t t' :: Term
t' [] _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
       where ty :: Id
ty = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Type -> Qid
forall a. HasName a => a -> Qid
getName (Type -> Qid) -> Type -> Qid
forall a b. (a -> b) -> a -> b
$ Term -> Type
MAS.getTermType Term
t
             kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "rl to formula") Id
ty IdMap
im
             pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind, Id
kind] Range
nullRange
             pred_name :: PRED_SYMB
pred_name = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
pred_type Range
nullRange
             ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
             ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
             form :: CASLFORMULA
form = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pred_name [CASLTERM
ct, CASLTERM
ct'] Range
nullRange
rl2formula im :: IdMap
im (MAS.Rl t :: Term
t t' :: Term
t' conds :: [Condition]
conds@(_ : _) _) = CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
       where ty :: Id
ty = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Type -> Qid
forall a. HasName a => a -> Qid
getName (Type -> Qid) -> Type -> Qid
forall a b. (a -> b) -> a -> b
$ Term -> Type
MAS.getTermType Term
t
             kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "rl to formula") Id
ty IdMap
im
             pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind, Id
kind] Range
nullRange
             pred_name :: PRED_SYMB
pred_name = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
pred_type Range
nullRange
             ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
             ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
             conds_form :: CASLFORMULA
conds_form = IdMap -> [Condition] -> CASLFORMULA
conds2formula IdMap
im [Condition]
conds
             concl_form :: CASLFORMULA
concl_form = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pred_name [CASLTERM
ct, CASLTERM
ct'] Range
nullRange
             form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CAS.mkImpl CASLFORMULA
conds_form CASLFORMULA
concl_form

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

-- | translate a single Maude condition to a CASL formula
cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA
cond2formula :: IdMap -> Condition -> CASLFORMULA
cond2formula im :: IdMap
im (MAS.EqCond t :: Term
t t' :: Term
t') = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
ct CASLTERM
ct'
       where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
             ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
cond2formula im :: IdMap
im (MAS.MatchCond t :: Term
t t' :: Term
t') = CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CAS.mkStEq CASLTERM
ct CASLTERM
ct'
       where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
             ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
cond2formula im :: IdMap
im (MAS.MbCond t :: Term
t s :: Sort
s) = CASLTERM -> Id -> Range -> CASLFORMULA
forall f. TERM f -> Id -> Range -> FORMULA f
CAS.Membership CASLTERM
ct Id
s' Range
nullRange
      where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
            s' :: Id
s' = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Sort -> Qid
forall a. HasName a => a -> Qid
getName Sort
s
cond2formula im :: IdMap
im (MAS.RwCond t :: Term
t t' :: Term
t') = PRED_SYMB -> [CASLTERM] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
CAS.mkPredication PRED_SYMB
pred_name [CASLTERM
ct, CASLTERM
ct']
       where ct :: CASLTERM
ct = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t
             ct' :: CASLTERM
ct' = IdMap -> Term -> CASLTERM
maudeTerm2caslTerm IdMap
im Term
t'
             ty :: Id
ty = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Type -> Qid
forall a. HasName a => a -> Qid
getName (Type -> Qid) -> Type -> Qid
forall a b. (a -> b) -> a -> b
$ Term -> Type
MAS.getTermType Term
t
             kind :: Id
kind = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (String -> Id
errorId "rw cond to formula") Id
ty IdMap
im
             pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind, Id
kind] Range
nullRange
             pred_name :: PRED_SYMB
pred_name = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
pred_type Range
nullRange

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

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

maudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT
maudeType2caslSort :: Type -> IdMap -> Id
maudeType2caslSort (MAS.TypeSort q :: Sort
q) _ = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Sort -> Qid
forall a. HasName a => a -> Qid
getName Sort
q
maudeType2caslSort (MAS.TypeKind q :: Kind
q) im :: IdMap
im = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
err Id
q' IdMap
im
      where q' :: Id
q' = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ Kind -> Qid
forall a. HasName a => a -> Qid
getName Kind
q
            err :: Id
err = String -> Id
errorId "error translate type"

-- | obtains the types of the given terms
getTypes :: [CAS.CASLTERM] -> [Id]
getTypes :: [CASLTERM] -> [Id]
getTypes = (CASLTERM -> Maybe Id) -> [CASLTERM] -> [Id]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe CASLTERM -> Maybe Id
getType

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

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

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

-- | creates the reflexivity predicate for the given kind
reflSen :: Id -> Named CAS.CASLFORMULA
reflSen :: Id -> Named CASLFORMULA
reflSen kind :: Id
kind = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
name (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
        where v :: CASLTERM
v = Id -> CASLTERM
newVar Id
kind
              pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind, Id
kind] Range
nullRange
              pn :: PRED_SYMB
pn = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
pred_type Range
nullRange
              form :: CASLFORMULA
form = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pn [CASLTERM
v, CASLTERM
v] Range
nullRange
              name :: String
name = "rew_refl_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
kind

-- | creates the transitivity predicate for the given kind
transSen :: Id -> Named CAS.CASLFORMULA
transSen :: Id -> Named CASLFORMULA
transSen kind :: Id
kind = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed String
name (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
quantifyUniversally CASLFORMULA
form
        where v1 :: CASLTERM
v1 = Int -> Id -> CASLTERM
newVarIndex 1 Id
kind
              v2 :: CASLTERM
v2 = Int -> Id -> CASLTERM
newVarIndex 2 Id
kind
              v3 :: CASLTERM
v3 = Int -> Id -> CASLTERM
newVarIndex 3 Id
kind
              pred_type :: PRED_TYPE
pred_type = [Id] -> Range -> PRED_TYPE
CAS.Pred_type [Id
kind, Id
kind] Range
nullRange
              pn :: PRED_SYMB
pn = Id -> PRED_TYPE -> Range -> PRED_SYMB
CAS.Qual_pred_name Id
rewID PRED_TYPE
pred_type Range
nullRange
              prem1 :: CASLFORMULA
prem1 = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pn [CASLTERM
v1, CASLTERM
v2] Range
nullRange
              prem2 :: CASLFORMULA
prem2 = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pn [CASLTERM
v2, CASLTERM
v3] Range
nullRange
              concl :: CASLFORMULA
concl = PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CAS.Predication PRED_SYMB
pn [CASLTERM
v1, CASLTERM
v3] Range
nullRange
              conj_form :: CASLFORMULA
conj_form = [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CAS.conjunct [CASLFORMULA
prem1, CASLFORMULA
prem2]
              form :: CASLFORMULA
form = CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CAS.mkImpl CASLFORMULA
conj_form CASLFORMULA
concl
              name :: String
name = "rew_trans_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
kind

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

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

-- | create the predicates that assign sorts to each term
kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)
kindPredicates :: IdMap -> Map Id (Set PredType)
kindPredicates = (Id -> Id -> Map Id (Set PredType) -> Map Id (Set PredType))
-> Map Id (Set PredType) -> IdMap -> Map Id (Set PredType)
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> Id -> Map Id (Set PredType) -> Map Id (Set PredType)
kindPredicate Map Id (Set PredType)
forall k a. Map k a
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 :: Id -> Id -> Map Id (Set PredType) -> Map Id (Set PredType)
kindPredicate sort :: Id
sort kind :: Id
kind mis :: Map Id (Set PredType)
mis = if Id
sort Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Id
str2id "Universal" then Map Id (Set PredType)
mis else
  let ar :: Set PredType
ar = PredType -> Set PredType
forall a. a -> Set a
Set.singleton (PredType -> Set PredType) -> PredType -> Set PredType
forall a b. (a -> b) -> a -> b
$ [Id] -> PredType
CSign.PredType [Id
kind]
  in (Set PredType -> Set PredType -> Set PredType)
-> Id
-> Set PredType
-> Map Id (Set PredType)
-> Map Id (Set PredType)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Set PredType -> Set PredType -> Set PredType
forall a. Ord a => Set a -> Set a -> Set a
Set.union Id
sort Set PredType
ar Map Id (Set PredType)
mis

-- | extract the kinds from the map of id's
kindsFromMap :: IdMap -> Set.Set Id
kindsFromMap :: IdMap -> Set Id
kindsFromMap = (Id -> Set Id -> Set Id) -> Set Id -> IdMap -> Set Id
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Set Id
forall a. Set a
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 :: SortSet -> SubsortRel -> Set Id
sortsTranslation = Symbols -> SubsortRel -> Set Id
sortsTranslationList (Symbols -> SubsortRel -> Set Id)
-> (SortSet -> Symbols) -> SortSet -> SubsortRel -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortSet -> Symbols
forall a. Set a -> [a]
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 :: Symbols -> SubsortRel -> Set Id
sortsTranslationList [] _ = Set Id
forall a. Set a
Set.empty
sortsTranslationList (s :: Symbol
s : ss :: Symbols
ss) r :: SubsortRel
r = Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbols -> Id
sort2id Symbols
tops) Set Id
res
      where tops :: Symbols
tops@(top :: Symbol
top : _) = Symbols -> Symbols
forall a. Ord a => [a] -> [a]
List.sort (Symbols -> Symbols) -> Symbols -> Symbols
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Symbol -> Symbols
getTop SubsortRel
r Symbol
s
            ss' :: SortSet
ss' = Symbols -> Symbol -> SubsortRel -> SortSet
deleteRelated Symbols
ss Symbol
top SubsortRel
r
            res :: Set Id
res = SortSet -> SubsortRel -> Set Id
sortsTranslation SortSet
ss' SubsortRel
r

-- | return the maximal elements from the sort relation
getTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]
getTop :: SubsortRel -> Symbol -> Symbols
getTop r :: SubsortRel
r tok :: Symbol
tok = case Symbols
succs of
           [] -> [Symbol
tok]
           toks :: Symbols
toks@(_ : _) -> (Symbol -> Symbols) -> Symbols -> Symbols
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SubsortRel -> Symbol -> Symbols
getTop SubsortRel
r) Symbols
toks
      where succs :: Symbols
succs = SortSet -> Symbols
forall a. Set a -> [a]
Set.toList (SortSet -> Symbols) -> SortSet -> Symbols
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Symbol -> SortSet
forall a. Ord a => Rel a -> a -> Set a
Rel.succs SubsortRel
r Symbol
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 :: Symbols -> Symbol -> SubsortRel -> SortSet
deleteRelated ss :: Symbols
ss sym :: Symbol
sym r :: SubsortRel
r = (Symbol -> SortSet -> SortSet) -> SortSet -> Symbols -> SortSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Symbol -> SubsortRel -> Symbol -> SortSet -> SortSet
f Symbol
sym SubsortRel
tc) SortSet
forall a. Set a
Set.empty Symbols
ss
      where tc :: SubsortRel
tc = SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a
Rel.transClosure SubsortRel
r
            f :: Symbol -> SubsortRel -> Symbol -> SortSet -> SortSet
f sort :: Symbol
sort trC :: SubsortRel
trC x :: Symbol
x y :: SortSet
y = if SubsortRel -> Symbol -> Symbol -> Bool
MSym.sameKind SubsortRel
trC Symbol
sort Symbol
x
                                  then SortSet
y
                                  else Symbol -> SortSet -> SortSet
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
x SortSet
y

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

-- | build an Id from a Maude symbol
sym2id :: MSym.Symbol -> Id
sym2id :: Symbol -> Id
sym2id = Qid -> Id
token2id (Qid -> Id) -> (Symbol -> Qid) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName

-- | generates an Id from a string
str2id :: String -> Id
str2id :: String -> Id
str2id = Qid -> Id
token2id (Qid -> Id) -> (String -> Qid) -> String -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Qid
mkSimpleId

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

-- | add universal quantification of all variables in the formula
quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA
quantifyUniversally :: CASLFORMULA -> CASLFORMULA
quantifyUniversally form :: CASLFORMULA
form = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
CAS.mkForall [VAR_DECL]
var_decl CASLFORMULA
form
      where vars :: Map Id (Set Qid)
vars = CASLFORMULA -> Map Id (Set Qid)
getVars CASLFORMULA
form
            var_decl :: [VAR_DECL]
var_decl = Map Id (Set Qid) -> [VAR_DECL]
listVarDecl Map Id (Set Qid)
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 Id (Set Qid) -> [VAR_DECL]
listVarDecl = (Id -> Set Qid -> [VAR_DECL] -> [VAR_DECL])
-> [VAR_DECL] -> Map Id (Set Qid) -> [VAR_DECL]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Id -> Set Qid -> [VAR_DECL] -> [VAR_DECL]
f []
      where f :: Id -> Set Qid -> [VAR_DECL] -> [VAR_DECL]
f sort :: Id
sort var_set :: Set Qid
var_set =
                ([Qid] -> Id -> Range -> VAR_DECL
CAS.Var_decl (Set Qid -> [Qid]
forall a. Set a -> [a]
Set.toList Set Qid
var_set) Id
sort Range
nullRange VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
:)

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

-- | translate the CASL sorts to symbols
kinds2syms :: Set.Set Id -> Set.Set CSign.Symbol
kinds2syms :: Set Id -> Set Symbol
kinds2syms = (Id -> Symbol) -> Set Id -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Symbol
kind2sym

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

-- | translates the CASL predicates into CASL symbols
preds2syms :: CSign.PredMap -> Set.Set CSign.Symbol
preds2syms :: PredMap -> Set Symbol
preds2syms = (Id -> PredType -> Set Symbol -> Set Symbol)
-> Set Symbol -> PredMap -> Set Symbol
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey Id -> PredType -> Set Symbol -> Set Symbol
createSym4id Set Symbol
forall a. Set a
Set.empty

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

-- | translates the CASL operators into CASL symbols
ops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol
ops2symbols :: OpMap -> Set Symbol
ops2symbols = (Id -> OpType -> Set Symbol -> Set Symbol)
-> Set Symbol -> OpMap -> Set Symbol
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey Id -> OpType -> Set Symbol -> Set Symbol
createSymOp4id Set Symbol
forall a. Set a
Set.empty

-- | creates a CASL symbol for an operator
createSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol
  -> Set.Set CSign.Symbol
createSymOp4id :: Id -> OpType -> Set Symbol -> Set Symbol
createSymOp4id on :: Id
on ot :: OpType
ot = Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
sym
      where sym :: Symbol
sym = Id -> SymbType -> Symbol
CSign.Symbol Id
on (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> SymbType
CSign.OpAsItemType OpType
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 :: CASLFORMULA -> Map Id (Set Qid)
getVars (CAS.Quantification _ _ f :: CASLFORMULA
f _) = CASLFORMULA -> Map Id (Set Qid)
getVars CASLFORMULA
f
getVars (CAS.Junction _ fs :: [CASLFORMULA]
fs _) =
    (CASLFORMULA -> Map Id (Set Qid) -> Map Id (Set Qid))
-> Map Id (Set Qid) -> [CASLFORMULA] -> Map Id (Set Qid)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set Qid -> Set Qid -> Set Qid)
-> Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Qid -> Set Qid -> Set Qid
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid))
-> (CASLFORMULA -> Map Id (Set Qid))
-> CASLFORMULA
-> Map Id (Set Qid)
-> Map Id (Set Qid)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> Map Id (Set Qid)
getVars) Map Id (Set Qid)
forall k a. Map k a
Map.empty [CASLFORMULA]
fs
getVars (CAS.Relation f1 :: CASLFORMULA
f1 _ f2 :: CASLFORMULA
f2 _) = (Set Qid -> Set Qid -> Set Qid)
-> Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Qid -> Set Qid -> Set Qid
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map Id (Set Qid)
v1 Map Id (Set Qid)
v2
     where v1 :: Map Id (Set Qid)
v1 = CASLFORMULA -> Map Id (Set Qid)
getVars CASLFORMULA
f1
           v2 :: Map Id (Set Qid)
v2 = CASLFORMULA -> Map Id (Set Qid)
getVars CASLFORMULA
f2
getVars (CAS.Negation f :: CASLFORMULA
f _) = CASLFORMULA -> Map Id (Set Qid)
getVars CASLFORMULA
f
getVars (CAS.Predication _ ts :: [CASLTERM]
ts _) =
    (CASLTERM -> Map Id (Set Qid) -> Map Id (Set Qid))
-> Map Id (Set Qid) -> [CASLTERM] -> Map Id (Set Qid)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Set Qid -> Set Qid -> Set Qid)
-> Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Qid -> Set Qid -> Set Qid
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid))
-> (CASLTERM -> Map Id (Set Qid))
-> CASLTERM
-> Map Id (Set Qid)
-> Map Id (Set Qid)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLTERM -> Map Id (Set Qid)
getVarsTerm) Map Id (Set Qid)
forall k a. Map k a
Map.empty [CASLTERM]
ts
getVars (CAS.Definedness t :: CASLTERM
t _) = CASLTERM -> Map Id (Set Qid)
getVarsTerm CASLTERM
t
getVars (CAS.Equation t1 :: CASLTERM
t1 _ t2 :: CASLTERM
t2 _) = (Set Qid -> Set Qid -> Set Qid)
-> Map Id (Set Qid) -> Map Id (Set Qid) -> Map Id (Set Qid)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set Qid -> Set Qid -> Set Qid
forall a. Ord a => Set a -> Set a -> Set a
Set.union Map Id (Set Qid)
v1 Map Id (Set Qid)
v2
     where v1 :: Map Id (Set Qid)
v1 = CASLTERM -> Map Id (Set Qid)
getVarsTerm CASLTERM
t1
           v2 :: Map Id (Set Qid)
v2 = CASLTERM -> Map Id (Set Qid)
getVarsTerm CASLTERM
t2
getVars (CAS.Membership t :: CASLTERM
t _ _) = CASLTERM -> Map Id (Set Qid)
getVarsTerm CASLTERM
t
getVars (CAS.Mixfix_formula t :: CASLTERM
t) = CASLTERM -> Map Id (Set Qid)
getVarsTerm CASLTERM
t
getVars _ = Map Id (Set Qid)
forall k a. Map k a
Map.empty

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

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

-- | transforms a maude identifier into a valid CASL identifier
maudeSymbol2validCASLSymbol :: Token -> [Token]
maudeSymbol2validCASLSymbol :: Qid -> [Qid]
maudeSymbol2validCASLSymbol t :: Qid
t = String -> String -> [Qid]
splitDoubleUnderscores String
str ""
    where str :: String
str = String -> String
ms2vcs (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ Qid -> String
forall a. Show a => a -> String
show Qid
t

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

-- | map of reserved words
stringMap :: Map.Map String String
stringMap :: Map String String
stringMap = [(String, String)] -> Map String String
forall k a. Ord k => [(k, a)] -> Map k a
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 :: String -> String -> [Qid]
splitDoubleUnderscores [] acc :: String
acc = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
acc
                                then []
                                else [String -> Qid
mkSimpleId String
acc]
splitDoubleUnderscores ('_' : '_' : cs :: String
cs) acc :: String
acc = if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
acc
                                              then Qid
dut Qid -> [Qid] -> [Qid]
forall a. a -> [a] -> [a]
: [Qid]
rest
                                              else Qid
acct Qid -> [Qid] -> [Qid]
forall a. a -> [a] -> [a]
: Qid
dut Qid -> [Qid] -> [Qid]
forall a. a -> [a] -> [a]
: [Qid]
rest
     where acct :: Qid
acct = String -> Qid
mkSimpleId String
acc
           dut :: Qid
dut = String -> Qid
mkSimpleId "__"
           rest :: [Qid]
rest = String -> String -> [Qid]
splitDoubleUnderscores String
cs []
splitDoubleUnderscores (c :: Char
c : cs :: String
cs) acc :: String
acc = String -> String -> [Qid]
splitDoubleUnderscores String
cs (String
acc String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Char
c])


-- | error Id
errorId :: String -> Id
errorId :: String -> Id
errorId s :: String
s = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ "ERROR: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

kindId :: Id -> Id
kindId :: Id -> Id
kindId i :: Id
i = Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ "kind_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
i

kindMapId :: MSign.KindRel -> IdMap
kindMapId :: KindRel -> IdMap
kindMapId kr :: KindRel
kr = [(Id, Id)] -> IdMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Id, Id)]
krl'
     where krl :: [(Symbol, Symbol)]
krl = KindRel -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList KindRel
kr
           krl' :: [(Id, Id)]
krl' = ((Symbol, Symbol) -> (Id, Id)) -> [(Symbol, Symbol)] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Symbol
x, y :: Symbol
y) -> (Symbol -> Id
mSym2caslId Symbol
x, Symbol -> Id
mSym2caslId Symbol
y)) [(Symbol, Symbol)]
krl

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

-- | checks the profile has at least one sort
atLeastOneSort :: MSign.OpMap -> MSign.OpMap
atLeastOneSort :: OpMap -> OpMap
atLeastOneSort om :: OpMap
om = [(Qid, OpDeclSet)] -> OpMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Qid, OpDeclSet)]
lom'
      where lom :: [(Qid, OpDeclSet)]
lom = OpMap -> [(Qid, OpDeclSet)]
forall k a. Map k a -> [(k, a)]
Map.toList OpMap
om
            lom' :: [(Qid, OpDeclSet)]
lom' = [(Qid, OpDeclSet)] -> [(Qid, OpDeclSet)]
filterAtLeastOneSort [(Qid, OpDeclSet)]
lom

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

atLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet
atLeastOneSortODS :: OpDeclSet -> OpDeclSet
atLeastOneSortODS ods :: OpDeclSet
ods = [OpDecl] -> OpDeclSet
forall a. Ord a => [a] -> Set a
Set.fromList [OpDecl]
lods'
     where lods :: [OpDecl]
lods = OpDeclSet -> [OpDecl]
forall a. Set a -> [a]
Set.toList OpDeclSet
ods
           lods' :: [OpDecl]
lods' = [OpDecl] -> [OpDecl]
atLeastOneSortLODS [OpDecl]
lods

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

atLeastOneSortSS :: Set.Set MSym.Symbol -> Set.Set MSym.Symbol
atLeastOneSortSS :: SortSet -> SortSet
atLeastOneSortSS = (Symbol -> Bool) -> SortSet -> SortSet
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Symbol -> Bool
hasOneSort

hasOneSort :: MSym.Symbol -> Bool
hasOneSort :: Symbol -> Bool
hasOneSort (MSym.Operator _ ar :: Symbols
ar co :: Symbol
co) = (Symbol -> Bool) -> Symbols -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Symbol -> Bool
isSymSort (Symbol
co Symbol -> Symbols -> Symbols
forall a. a -> [a] -> [a]
: Symbols
ar)
hasOneSort _ = Bool
False

isSymSort :: MSym.Symbol -> Bool
isSymSort :: Symbol -> Bool
isSymSort (MSym.Sort _) = Bool
True
isSymSort _ = Bool
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' :: IdMap -> OpMap -> (OpMap, OpMap, Set Component)
translateOps' im :: IdMap
im = (OpDeclSet
 -> (OpMap, OpMap, Set Component) -> (OpMap, OpMap, Set Component))
-> (OpMap, OpMap, Set Component)
-> OpMap
-> (OpMap, OpMap, Set Component)
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (IdMap
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDeclSet' IdMap
im)
  (OpMap
forall a b. MapSet a b
MapSet.empty, OpMap
forall a b. MapSet a b
MapSet.empty, Set Component
forall a. Set a
Set.empty)

-- | translates an operator declaration set into a tern as described above
translateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet' :: IdMap
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDeclSet' im :: IdMap
im ods :: OpDeclSet
ods tpl :: (OpMap, OpMap, Set Component)
tpl = (OpDecl
 -> (OpMap, OpMap, Set Component) -> (OpMap, OpMap, Set Component))
-> (OpMap, OpMap, Set Component)
-> OpDeclSet
-> (OpMap, OpMap, Set Component)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl' IdMap
im) (OpMap, OpMap, Set Component)
tpl OpDeclSet
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' :: IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl' im :: IdMap
im (syms :: SortSet
syms, ats :: [Attr]
ats) (ops :: OpMap
ops, assoc_ops :: OpMap
assoc_ops, cs :: Set Component
cs) =
        if SortSet -> Bool
forall a. Set a -> Bool
Set.null SortSet
syms'
        then (OpMap
ops', OpMap
assoc_ops', Set Component
cs')
        else IdMap
-> OpDecl
-> (OpMap, OpMap, Set Component)
-> (OpMap, OpMap, Set Component)
translateOpDecl' IdMap
im (SortSet
syms', [Attr]
ats) (OpMap
ops', OpMap
assoc_ops', Set Component
cs')
      where (sym :: Symbol
sym, syms' :: SortSet
syms') = SortSet -> (Symbol, SortSet)
forall a. Set a -> (a, Set a)
Set.deleteFindMin SortSet
syms
            Just (cop_id :: Id
cop_id, ot :: OpType
ot, _) = IdMap -> Symbol -> Maybe (Id, OpType, OpType)
maudeSym2CASLOp' IdMap
im Symbol
sym
            ops' :: OpMap
ops' = Id -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
cop_id OpType
ot OpMap
ops
            assoc_ops' :: OpMap
assoc_ops' = if (Attr -> Bool) -> [Attr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
MAS.assoc [Attr]
ats
                         then Id -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
cop_id OpType
ot OpMap
assoc_ops
                         else OpMap
assoc_ops
            cs' :: Set Component
cs' = if (Attr -> Bool) -> [Attr] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Attr -> Bool
MAS.ctor [Attr]
ats
                  then Component -> Set Component -> Set Component
forall a. Ord a => a -> Set a -> Set a
Set.insert (Id -> OpType -> Component
Component Id
cop_id OpType
ot) Set Component
cs
                  else Set Component
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' :: IdMap -> Symbol -> Maybe (Id, OpType, OpType)
maudeSym2CASLOp' im :: IdMap
im (MSym.Operator op :: Qid
op ar :: Symbols
ar co :: Symbol
co) = (Id, OpType, OpType) -> Maybe (Id, OpType, OpType)
forall a. a -> Maybe a
Just (Qid -> Id
token2id Qid
op, OpType
ot, OpType
ot')
      where f :: Symbol -> Id
f = Qid -> Id
token2id (Qid -> Id) -> (Symbol -> Qid) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName
            g :: Symbol -> Id
g = (Symbol -> IdMap -> Id
`maudeSymbol2caslSort'` IdMap
im)
            ot :: OpType
ot = OpKind -> [Id] -> Id -> OpType
CSign.OpType OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
g Symbols
ar) (Symbol -> Id
g Symbol
co)
            ot' :: OpType
ot' = OpKind -> [Id] -> Id -> OpType
CSign.OpType OpKind
CAS.Total ((Symbol -> Id) -> Symbols -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Id
f Symbols
ar) (Symbol -> Id
f Symbol
co)
maudeSym2CASLOp' _ _ = Maybe (Id, OpType, OpType)
forall a. Maybe a
Nothing

maudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT
maudeSymbol2caslSort' :: Symbol -> IdMap -> Id
maudeSymbol2caslSort' (MSym.Sort q :: Qid
q) _ =
    Qid -> Id
token2id (Qid -> Id) -> Qid -> Id
forall a b. (a -> b) -> a -> b
$ String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ "kind_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Qid -> String
forall a. Show a => a -> String
show Qid
q
maudeSymbol2caslSort' (MSym.Kind q :: Qid
q) im :: IdMap
im = Id -> Id -> IdMap -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
err Id
q' IdMap
im
      where q' :: Id
q' = Qid -> Id
token2id Qid
q
            err :: Id
err = String -> Id
errorId "error translate symbol"
maudeSymbol2caslSort' _ _ = String -> Id
errorId "error translate symbol"