{- |

Module : $Header$

Description : Maude Comorphisms

Copyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009

License : GPLv2 or higher, see LICENSE.txt

Maintainer : ariesco@fdi.ucm.es

Stability : experimental

Portability : portable

Comorphism from Maude to CASL.

-}

module Maude.PreComorphism where

import Data.Maybe

import qualified Data.List as List

import qualified Data.Set as Set

import qualified Data.Map as Map

import qualified Maude.Sign as MSign

import qualified Maude.Sentence as MSentence

import qualified Maude.Morphism as MMorphism

import qualified Maude.AS_Maude as MAS

import qualified Maude.Symbol as MSym

import Maude.Meta.HasName

import qualified CASL.Sign as CSign

import qualified CASL.Morphism as CMorphism

import qualified CASL.AS_Basic_CASL as CAS

import CASL.StaticAna

import CASL.Logic_CASL

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

import Comorphisms.GetPreludeLib (readLib)

import System.IO.Unsafe

import Static.GTheory

import Logic.Prover

import Logic.Coerce

type IdMap = Map.Map Id Id

type OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)

-- | generates a CASL morphism from a Maude morphism

mapMorphism :: MMorphism.Morphism -> Result CMorphism.CASLMor

mapMorphism morph =

let

src = MMorphism.source morph

tgt = MMorphism.target morph

mk = kindMapId $ MSign.kindRel src

mk' = kindMapId $ MSign.kindRel tgt

smap = MMorphism.sortMap morph

omap = MMorphism.opMap morph

smap' = applySortMap2CASLSorts smap mk mk'

omap' = maudeOpMap2CASLOpMap mk omap

pmap = createPredMap mk smap

(src', _) = maude2casl src []

(tgt', _) = maude2casl tgt []

in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()

{- | translates the Maude morphism between operators into a CASL morpshim

between operators -}

maudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map

maudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty

{- | translates the mapping between two symbols representing operators into

a CASL operators map -}

translateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map

-> CMorphism.Op_map

translateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm

= copm'

where f = token2id . getName

g x = Map.findWithDefault (errorId "translate op map entry")

(f x) im

ot = CSign.OpType CAS.Total (map g ar) (g co)

cop = (token2id from, ot)

to' = (token2id to, CAS.Total)

copm' = Map.insert cop to' copm

translateOpMapEntry _ _ _ _ = Map.empty

-- | generates a set of CASL symbol from a Maude Symbol

mapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol

mapSymbol sg (MSym.Sort q) = Set.singleton csym

where mk = kindMapId $ MSign.kindRel sg

sym_id = token2id q

kind = Map.findWithDefault (errorId "map symbol") sym_id mk

pred_data = CSign.PredType [kind]

csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data

mapSymbol sg (MSym.Operator q ar co) = Set.singleton csym

where mk = kindMapId $ MSign.kindRel sg

q' = token2id q

ar' = map (maudeSort2caslId mk) ar

co' = token2id $ getName co

op_data = CSign.OpType CAS.Total ar' co'

csym = CSign.Symbol q' $ CSign.OpAsItemType op_data

mapSymbol _ _ = Set.empty

-- | returns the sort in CASL of the Maude sort symbol

maudeSort2caslId :: IdMap -> MSym.Symbol -> Id

maudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id")

(token2id $ getName sym) im

{- | creates the predicate map for the CASL morphism from the Maude sort map and

the map between sorts and kinds -}

createPredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map

createPredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty

-- | creates an entry of the predicate map for a single sort

createPredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map

-> CMorphism.Pred_map

createPredMap4sort im from to = Map.insert key id_to

where id_from = token2id $ getName from

id_to = token2id $ getName to

kind = Map.findWithDefault (errorId "predicate for sort")

id_from im

key = (id_from, CSign.PredType [kind])

{- | computes the sort morphism of CASL from the sort morphism in Maude

and the set of kinds -}

applySortMap2CASLSorts :: MMorphism.SortMap -> IdMap -> IdMap

-> CMorphism.Sort_map

applySortMap2CASLSorts sm im im' = Map.fromList sml'

where sml = Map.toList sm

sml' = foldr (applySortMap2CASLSort im im') [] sml

-- | computes the morphism for a single sort pair

applySortMap2CASLSort :: IdMap -> IdMap -> (MSym.Symbol, MSym.Symbol)

-> [(Id, Id)] -> [(Id, Id)]

applySortMap2CASLSort im im' (s1, s2) l = l'

where p1 = (mSym2caslId s1, mSym2caslId s2)

f x = Map.findWithDefault

(errorId $ "err" ++ show (mSym2caslId x)) (mSym2caslId x)

p2 = (f s1 im, f s2 im')

l' = if s1 == s2

then p1 : l

else p1 : p2 : l

-- | renames the sorts in a given kind

rename :: MMorphism.SortMap -> Token -> Token

rename sm tok = new_tok

where sym = MSym.Sort tok

sym' = if Map.member sym sm

then fromJust $ Map.lookup sym sm

else sym

new_tok = getName sym'

-- | translates a Maude sentence into a CASL formula

mapSentence :: MSign.Sign -> MSentence.Sentence -> Result CAS.CASLFORMULA

mapSentence sg sen = let

mk = kindMapId $ MSign.kindRel sg

named = makeNamed "" sen

form = mb_rl2formula mk named

in return $ sentence $ case sen of

MSentence.Equation (MAS.Eq _ _ _ ats) -> if any MAS.owise ats then let

sg_sens = map (makeNamed "") $ Set.toList $ MSign.sentences sg

(no_owise_sens, _, _) = splitOwiseEqs sg_sens

no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

in owiseSen2Formula mk no_owise_forms named

else noOwiseSen2Formula mk named

MSentence.Membership (MAS.Mb {}) -> form

MSentence.Rule (MAS.Rl {}) -> form

{- | applies maude2casl to compute the CASL signature and sentences from

the Maude ones, and wraps them into a Result datatype -}

mapTheory :: (MSign.Sign, [Named MSentence.Sentence])

-> Result (CSign.CASLSign, [Named CAS.CASLFORMULA])

mapTheory (sg, nsens) = return $ maude2casl sg nsens

{- | computes new signature and sentences of CASL associated to the

given Maude signature and sentences -}

maude2casl :: MSign.Sign -> [Named MSentence.Sentence]

-> (CSign.CASLSign, [Named CAS.CASLFORMULA])

maude2casl msign nsens = (csign {

CSign.sortRel =

Rel.union (Rel.fromKeysSet cs) sbs',

CSign.opMap = cops',

CSign.assocOps = assoc_ops,

CSign.predMap = preds,

CSign.declaredSymbols = syms }, new_sens)

where csign = CSign.emptySign ()

ss = MSign.sorts msign

ss' = Set.map sym2id ss

mk = kindMapId $ MSign.kindRel msign

sbs = MSign.subsorts msign

sbs' = maudeSbs2caslSbs sbs mk

cs = Set.union ss' $ kindsFromMap mk

preds = rewPredicates cs

rs = rewPredicatesSens cs

ops = deleteUniversal $ MSign.ops msign

ksyms = kinds2syms cs

(cops, assoc_ops, _) = translateOps mk ops -- (cops, assoc_ops, comps)

axSens = axiomsSens mk ops

ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]

cops' = universalOps cs cops $ booleanImported ops

rs' = rewPredicatesCongSens cops'

pred_forms = loadLibraries (MSign.sorts msign) ops

ops_syms = ops2symbols cops'

(no_owise_sens, owise_sens, mbs_rls_sens) = splitOwiseEqs nsens

no_owise_forms = map (noOwiseSen2Formula mk) no_owise_sens

owise_forms = map (owiseSen2Formula mk no_owise_forms) owise_sens

mb_rl_forms = map (mb_rl2formula mk) mbs_rls_sens

preds_syms = preds2syms preds

syms = Set.union ksyms $ Set.union ops_syms preds_syms

new_sens = concat [rs, rs', no_owise_forms, owise_forms,

mb_rl_forms, ctor_sen, pred_forms, axSens]

{- | translates the Maude subsorts into CASL subsorts, and adds the subsorts

for the kinds -}

maudeSbs2caslSbs :: MSign.SubsortRel -> IdMap -> Rel.Rel CAS.SORT

maudeSbs2caslSbs sbs im = Rel.fromMap m4

where l = Map.toList $ Rel.toMap sbs

l1 = [] -- map maudeSb2caslSb l

l2 = idList2Subsorts $ Map.toList im

l3 = map subsorts2Ids l

m1 = Map.fromList l1

m2 = Map.fromList l2

m3 = Map.fromList l3

m4 = Map.unionWith Set.union m1 $ Map.unionWith Set.union m2 m3

idList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]

idList2Subsorts [] = []

idList2Subsorts ((id1, id2) : il) = t1 : idList2Subsorts il

where t1 = (id1, Set.singleton id2)

maudeSb2caslSb :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

maudeSb2caslSb (sym, st) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)

subsorts2Ids :: (MSym.Symbol, Set.Set MSym.Symbol) -> (Id, Set.Set Id)

subsorts2Ids (sym, st) = (sortSym2id sym, Set.map sortSym2id st)

sortSym2id :: MSym.Symbol -> Id

sortSym2id (MSym.Sort q) = token2id q

sortSym2id _ = token2id $ mkSimpleId "error_translation"

-- | generates the sentences to state that the rew predicates are a congruence

rewPredicatesCongSens :: CSign.OpMap -> [Named CAS.CASLFORMULA]

rewPredicatesCongSens = MapSet.foldWithKey rewPredCong []

{- | generates the sentences to state that the rew predicates are a congruence

for a single operator -}

rewPredCong :: Id -> CSign.OpType -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

rewPredCong op ot fs = case args of

[] -> fs

_ -> nq_form : fs

where args = CSign.opArgs ot

vars1 = rewPredCongPremise 0 args

vars2 = rewPredCongPremise (length args) args

res = CSign.opRes ot

res_pred_type = CAS.Pred_type [res, res] nullRange

pn = CAS.Qual_pred_name rewID res_pred_type nullRange

name = "rew_cong_" ++ show op

prems = rewPredsCong args vars1 vars2

prems_conj = createConjForm prems

os = CAS.Qual_op_name op (CSign.toOP_TYPE ot) nullRange

conc_term1 = CAS.Application os vars1 nullRange

conc_term2 = CAS.Application os vars2 nullRange

conc_form = CAS.Predication pn [conc_term1, conc_term2] nullRange

form = createImpForm prems_conj conc_form

nq_form = makeNamed name $ quantifyUniversally form

-- | generates a list of variables of the given sorts

rewPredCongPremise :: Int -> [CAS.SORT] -> [CAS.CASLTERM]

rewPredCongPremise n (s : ss) = newVarIndex n s : rewPredCongPremise (n + 1) ss

rewPredCongPremise _ [] = []

-- | generates a list of rew predicates with the given variables

rewPredsCong :: [CAS.SORT] -> [CAS.CASLTERM] -> [CAS.CASLTERM]

-> [CAS.CASLFORMULA]

rewPredsCong (s : ss) (t : ts) (t' : ts') = form : forms

where pred_type = CAS.Pred_type [s, s] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

form = CAS.Predication pn [t, t'] nullRange

forms = rewPredsCong ss ts ts'

rewPredsCong _ _ _ = []

-- | load the CASL libraries for the Maude built-in operators

loadLibraries :: MSign.SortSet -> MSign.OpMap -> [Named CAS.CASLFORMULA]

loadLibraries ss om = if natImported ss om then loadNaturalNatSens else []

-- | loads the sentences associated to the natural numbers

loadNaturalNatSens :: [Named CAS.CASLFORMULA]

loadNaturalNatSens =

case unsafePerformIO $ readLib "Maude/MaudeNumbers.casl" of

G_theory lid _ _ _ thSens _ : _ -> do

let sens = toNamedList thSens

sens' <- coerceSens lid CASL "" sens

filter (not . ctorCons) sens'

_ -> error "Maude.loadNaturalNatSens"

-- | checks if a sentence is an constructor sentence

ctorCons :: Named CAS.CASLFORMULA -> Bool

ctorCons f = case sentence f of

CAS.Sort_gen_ax _ _ -> True

_ -> False

-- | checks if the boolean values are imported

booleanImported :: MSign.OpMap -> Bool

booleanImported = Map.member (mkSimpleId "if_then_else_fi")

-- | checks if the natural numbers are imported

natImported :: MSign.SortSet -> MSign.OpMap -> Bool

natImported ss om = b1 && b2 && b3

where b1 = Set.member (MSym.Sort $ mkSimpleId "Nat") ss

b2 = Map.member (mkSimpleId "s_") om

b3 = if b2 then specialZeroSet $ om Map.! mkSimpleId "s_" else True

specialZeroSet :: MSign.OpDeclSet -> Bool

specialZeroSet = Set.fold specialZero False

specialZero :: MSign.OpDecl -> Bool -> Bool

specialZero (_, ats) b = b' || b

where b' = isSpecial ats

isSpecial :: [MAS.Attr] -> Bool

isSpecial [] = False

isSpecial (MAS.Special _ : _) = True

isSpecial (_ : ats) = isSpecial ats

{- | delete the universal operators from Maude specifications, that will be

substituted for one operator for each sort in the specification -}

deleteUniversal :: MSign.OpMap -> MSign.OpMap

deleteUniversal om = om5

where om1 = Map.delete (mkSimpleId "if_then_else_fi") om

om2 = Map.delete (mkSimpleId "_==_") om1

om3 = Map.delete (mkSimpleId "_=/=_") om2

om4 = Map.delete (mkSimpleId "upTerm") om3

om5 = Map.delete (mkSimpleId "downTerm") om4

-- | generates the universal operators for all the sorts in the module

universalOps :: Set.Set Id -> CSign.OpMap -> Bool -> CSign.OpMap

universalOps kinds om True = Set.fold universalOpKind om kinds

universalOps _ om False = om

-- | generates the universal operators for a concrete module

universalOpKind :: Id -> CSign.OpMap -> CSign.OpMap

universalOpKind kind = MapSet.union $ MapSet.fromList

[ (if_id, [if_opt]), (double_eq_id, [eq_opt]), (neg_double_eq_id, [eq_opt]) ]

where if_id = str2id "if_then_else_fi"

double_eq_id = str2id "_==_"

neg_double_eq_id = str2id "_=/=_"

bool_id = str2id "Bool"

if_opt = CSign.OpType CAS.Total [bool_id, kind, kind] kind

eq_opt = CSign.OpType CAS.Total [kind, kind] bool_id

-- | generates the formulas for the universal operators

universalSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

universalSens = Set.fold universalSensKind []

-- | generates the formulas for the universal operators for the given sort

universalSensKind :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

universalSensKind kind acc = concat [iss, eqs, neqs, acc]

where iss = ifSens kind

eqs = equalitySens kind

neqs = nonEqualitySens kind

-- | generates the formulas for the if statement

ifSens :: Id -> [Named CAS.CASLFORMULA]

ifSens kind = [form'', neg_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

bv = newVarIndex 2 bk

true_type = CAS.Op_type CAS.Total [] bk nullRange

true_id = CAS.Qual_op_name (str2id "true") true_type nullRange

true_term = CAS.Application true_id [] nullRange

if_type = CAS.Op_type CAS.Total [bk, kind, kind] kind nullRange

if_name = str2id "if_then_else_fi"

if_id = CAS.Qual_op_name if_name if_type nullRange

if_term = CAS.Application if_id [bv, v1, v2] nullRange

prem = CAS.mkStEq bv true_term

concl = CAS.mkStEq if_term v1

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

neg_concl = CAS.mkStEq if_term v2

neg_form = CAS.mkImpl neg_prem neg_concl

neg_form' = quantifyUniversally neg_form

name1 = show kind ++ "_if_true"

name2 = show kind ++ "_if_false"

form'' = makeNamed name1 form'

neg_form'' = makeNamed name2 neg_form'

-- | generates the formulas for the equality

equalitySens :: Id -> [Named CAS.CASLFORMULA]

equalitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

b_type = CAS.Op_type CAS.Total [] bk nullRange

true_id = CAS.Qual_op_name (str2id "true") b_type nullRange

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Qual_op_name (str2id "false") b_type nullRange

false_term = CAS.Application false_id [] nullRange

prem = CAS.mkStEq v1 v2

double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind

nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.mkQualOp double_eq_name double_eq_type

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.mkStEq double_eq_term true_term

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.mkStEq double_eq_term false_term

comp_form = CAS.mkImpl neg_prem new_concl

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_==_true"

name2 = show kind ++ "_==_false"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

-- | generates the formulas for the inequality

nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]

nonEqualitySens kind = [form'', comp_form'']

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

bk = str2id "Bool"

b_type = CAS.Op_type CAS.Total [] bk nullRange

true_id = CAS.Qual_op_name (str2id "true") b_type nullRange

true_term = CAS.Application true_id [] nullRange

false_id = CAS.Qual_op_name (str2id "false") b_type nullRange

false_term = CAS.Application false_id [] nullRange

prem = CAS.mkStEq v1 v2

double_eq_type = CAS.Op_type CAS.Total [kind, kind] kind

nullRange

double_eq_name = str2id "_==_"

double_eq_id = CAS.mkQualOp double_eq_name double_eq_type

double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange

concl = CAS.mkStEq double_eq_term false_term

form = CAS.mkImpl prem concl

form' = quantifyUniversally form

neg_prem = CAS.Negation prem nullRange

new_concl = CAS.mkStEq double_eq_term true_term

comp_form = CAS.mkImpl neg_prem new_concl

comp_form' = quantifyUniversally comp_form

name1 = show kind ++ "_=/=_false"

name2 = show kind ++ "_=/=_true"

form'' = makeNamed name1 form'

comp_form'' = makeNamed name2 comp_form'

-- | generates the sentences for the operator attributes

axiomsSens :: IdMap -> MSign.OpMap -> [Named CAS.CASLFORMULA]

axiomsSens im = Map.fold (axiomsSensODS im) []

axiomsSensODS :: IdMap -> MSign.OpDeclSet -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

axiomsSensODS im ods l = Set.fold (axiomsSensOD im) l ods

axiomsSensOD :: IdMap -> MSign.OpDecl -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

axiomsSensOD im (ss, ats) l = Set.fold (axiomsSensSS im ats) l ss

axiomsSensSS :: IdMap -> [MAS.Attr] -> MSym.Symbol -> [Named CAS.CASLFORMULA]

-> [Named CAS.CASLFORMULA]

axiomsSensSS im ats (MSym.Operator q ar co) l = l ++ l1

where l1 = if elem MAS.Comm ats

then commSen im q ar co

else []

axiomsSensSS _ _ _ l = l

commSen :: IdMap -> MAS.Qid -> MSym.Symbols -> MSym.Symbol

-> [Named CAS.CASLFORMULA]

commSen im q ar@[ar1, ar2] co = [form']

where q' = token2id q

f = (`maudeSymbol2caslSort` im)

ar1' = f ar1

ar2' = f ar2

ot = CAS.Op_type CAS.Total (map f ar) (f co) nullRange

os = CAS.Qual_op_name q' ot nullRange

v1 = newVarIndex 1 ar1'

v2 = newVarIndex 2 ar2'

t1 = CAS.Application os [v1, v2] nullRange

t2 = CAS.Application os [v2, v1] nullRange

form = CAS.mkStEq t1 t2

name = "comm_" ++ ms2vcs (show q') ++ "_" ++ show ar1'

form' = makeNamed name $ quantifyUniversally form

commSen _ _ _ _ = []

-- (newVarIndex 1 (hd ar))

-- maudeSymbol2caslSort x im

{- | translates the Maude operator map into a tuple of CASL operators, CASL

associative operators, membership induced from each Maude operator,

and the set of sorts with the ctor attribute -}

translateOps :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps im = Map.fold (translateOpDeclSet im)

(MapSet.empty, MapSet.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above

translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods

{- | given an operator declaration updates the accumulator with the translation

to CASL operator, checking if the operator has the assoc attribute to insert

it in the map of associative operators, generating the membership predicate

induced by the operator declaration, and checking if it has the ctor

attribute to introduce the operator in the generators sentence -}

translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl im (syms, ats) (ops, assoc_ops, cs) = case tl of

[] -> (ops', assoc_ops', cs')

_ -> translateOpDecl im (syms', ats) (ops', assoc_ops', cs')

where sym = head $ Set.toList syms

tl = tail $ Set.toList syms

syms' = Set.fromList tl

(cop_id, ot, _) = fromJust $ maudeSym2CASLOp im sym

ops' = MapSet.insert cop_id ot ops

assoc_ops' = if any MAS.assoc ats

then MapSet.insert cop_id ot assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

{- | translates a Maude operator symbol into a pair with the id of the operator

and its CASL type -}

maudeSym2CASLOp :: IdMap -> MSym.Symbol

-> Maybe (Id, CSign.OpType, CSign.OpType)

maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')

where f = token2id . getName

g = (`maudeSymbol2caslSort` im)

ot = CSign.OpType CAS.Total (map g ar) (g co)

ot' = CSign.OpType CAS.Total (map f ar) (f co)

maudeSym2CASLOp _ _ = Nothing

-- | creates a conjuctive formula distinguishing the size of the list

createConjForm :: [CAS.CASLFORMULA] -> CAS.CASLFORMULA

createConjForm = CAS.conjunct

-- | creates a implication formula distinguishing the size of the premises

createImpForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA -> CAS.CASLFORMULA

createImpForm (CAS.Atom True _) form = form

createImpForm form1 form2 = CAS.mkImpl form1 form2

{- | generates the predicates asserting the "true" sort of the operator if all

the arguments have the correct sort -}

ops2predPremises :: IdMap -> [MSym.Symbol] -> Int

-> ([CAS.CASLTERM], [CAS.CASLFORMULA])

ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)

where s' = token2id s

kind = Map.findWithDefault (errorId "mb of op as predicate")

s' im

pred_type = CAS.Pred_type [kind] nullRange

pred_name = CAS.Qual_pred_name s' pred_type nullRange

var = newVarIndex i kind

form = CAS.Predication pred_name [var] nullRange

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)

where k' = token2id k

kind = Map.findWithDefault (errorId "mb of op as predicate")

k' im

var = newVarIndex i kind

(terms, forms) = ops2predPremises im ss (i + 1)

ops2predPremises _ _ _ = ([], [])

{- | traverses the Maude sentences, returning a pair of list of sentences.

The first list in the pair are the equations without the attribute "owise",

while the second one are the equations with this attribute -}

splitOwiseEqs :: [Named MSentence.Sentence] -> ([Named MSentence.Sentence]

, [Named MSentence.Sentence], [Named MSentence.Sentence])

splitOwiseEqs [] = ([], [], [])

splitOwiseEqs (s : ss) = res

where (no_owise_sens, owise_sens, mbs_rls) = splitOwiseEqs ss

sen = sentence s

res = case sen of

MSentence.Equation (MAS.Eq _ _ _ ats) ->

if any MAS.owise ats

then (no_owise_sens, s : owise_sens, mbs_rls)

else (s : no_owise_sens, owise_sens, mbs_rls)

_ -> (no_owise_sens, owise_sens, s : mbs_rls)

{- | translates a Maude equation defined without the "owise" attribute into

a CASL formula -}

noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence

-> Named CAS.CASLFORMULA

noOwiseSen2Formula im s = s'

where MSentence.Equation eq = sentence s

sen' = noOwiseEq2Formula im eq

s' = s { sentence = sen' }

{- | translates a Maude equation defined with the "owise" attribute into

a CASL formula -}

owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]

-> Named MSentence.Sentence -> Named CAS.CASLFORMULA

owiseSen2Formula im owise_forms s = s'

where MSentence.Equation eq = sentence s

sen' = owiseEq2Formula im owise_forms eq

s' = s { sentence = sen' }

-- | translates a Maude membership or rule into a CASL formula

mb_rl2formula :: IdMap -> Named MSentence.Sentence -> Named CAS.CASLFORMULA

mb_rl2formula im s = case sen of

MSentence.Membership mb -> let

mb' = mb2formula im mb

in s { sentence = mb' }

MSentence.Rule rl -> let

rl' = rl2formula im rl

in s { sentence = rl' }

_ -> makeNamed "" CAS.falseForm

where sen = sentence s

-- | generates a new variable qualified with the given number

newVarIndex :: Int -> Id -> CAS.CASLTERM

newVarIndex i sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId $ 'V' : show i

-- | generates a new variable

newVar :: Id -> CAS.CASLTERM

newVar sort = CAS.Qual_var var sort nullRange

where var = mkSimpleId "V"

-- | Id for the rew predicate

rewID :: Id

rewID = token2id $ mkSimpleId "rew"

{- | translates a Maude equation without the "owise" attribute into a CASL

formula -}

noOwiseEq2Formula :: IdMap -> MAS.Equation -> CAS.CASLFORMULA

noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.mkStEq ct ct'

noOwiseEq2Formula im (MAS.Eq t t' conds@(_ : _) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.mkStEq ct ct'

form = createImpForm conds_form concl_form

{- | transforms a Maude equation defined with the otherwise attribute into

a CASL formula -}

owiseEq2Formula :: IdMap -> [Named CAS.CASLFORMULA] -> MAS.Equation

-> CAS.CASLFORMULA

owiseEq2Formula im no_owise_form eq = form

where (eq_form, vars) = noQuantification $ noOwiseEq2Formula im eq

(op, ts, _) = fromJust $ getLeftApp eq_form

ex_form = existencialNegationOtherEqs op ts no_owise_form

imp_form = createImpForm ex_form eq_form

form = CAS.mkForall vars imp_form

-- | generates a conjunction of negation of existencial quantifiers

existencialNegationOtherEqs :: CAS.OP_SYMB -> [CAS.CASLTERM] ->

[Named CAS.CASLFORMULA] -> CAS.CASLFORMULA

existencialNegationOtherEqs op ts forms = form

where ex_forms = foldr ((++) . existencialNegationOtherEq op ts) [] forms

form = CAS.conjunct ex_forms

{- | given a formula, if it refers to the same operator indicated by the

parameters the predicate creates a list with the negation of the existence of

variables that match the pattern described in the formula. In other case it

returns an empty list -}

existencialNegationOtherEq :: CAS.OP_SYMB -> [CAS.CASLTERM]

-> Named CAS.CASLFORMULA -> [CAS.CASLFORMULA]

existencialNegationOtherEq req_op terms form = if ok then let

(_, ts, conds) = fromJust tpl

ts' = qualifyExVarsTerms ts

conds' = qualifyExVarsForms conds

prems = createEqs ts' terms ++ conds'

conj_form = CAS.conjunct prems

ex_form = if null vars' then conj_form else

CAS.mkExist vars' conj_form

neg_form = CAS.mkNeg ex_form

in [neg_form]

else []

where (inner_form, vars) = noQuantification $ sentence form

vars' = qualifyExVars vars

tpl = getLeftApp inner_form

ok = case tpl of

Nothing -> False

Just _ -> let (op, ts, _) = fromJust tpl

in req_op == op && length terms == length ts

{- | qualifies the variables in a list of formulas with the suffix "_ex" to

distinguish them from the variables already bound -}

qualifyExVarsForms :: [CAS.CASLFORMULA] -> [CAS.CASLFORMULA]

qualifyExVarsForms = map qualifyExVarsForm

{- | qualifies the variables in a formula with the suffix "_ex" to distinguish

them from the variables already bound -}

qualifyExVarsForm :: CAS.CASLFORMULA -> CAS.CASLFORMULA

qualifyExVarsForm (CAS.Equation t CAS.Strong t' r) =

CAS.Equation qt CAS.Strong qt' r

where qt = qualifyExVarsTerm t

qt' = qualifyExVarsTerm t'

qualifyExVarsForm (CAS.Predication op ts r) = CAS.Predication op ts' r

where ts' = qualifyExVarsTerms ts

qualifyExVarsForm f = f

{- | qualifies the variables in a list of terms with the suffix "_ex" to

distinguish them from the variables already bound -}

qualifyExVarsTerms :: [CAS.CASLTERM] -> [CAS.CASLTERM]

qualifyExVarsTerms = map qualifyExVarsTerm

{- | qualifies the variables in a term with the suffix "_ex" to distinguish them

from the variables already bound -}

qualifyExVarsTerm :: CAS.CASLTERM -> CAS.CASLTERM

qualifyExVarsTerm (CAS.Qual_var var sort r) =

CAS.Qual_var (qualifyExVarAux var) sort r

qualifyExVarsTerm (CAS.Application op ts r) = CAS.Application op ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Sorted_term t s r) =

CAS.Sorted_term (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Cast t s r) = CAS.Cast (qualifyExVarsTerm t) s r

qualifyExVarsTerm (CAS.Conditional t1 f t2 r) = CAS.Conditional t1' f t2' r

where t1' = qualifyExVarsTerm t1

t2' = qualifyExVarsTerm t2

qualifyExVarsTerm (CAS.Mixfix_term ts) = CAS.Mixfix_term ts'

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_parenthesized ts r) =

CAS.Mixfix_parenthesized ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_bracketed ts r) = CAS.Mixfix_bracketed ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm (CAS.Mixfix_braced ts r) = CAS.Mixfix_braced ts' r

where ts' = map qualifyExVarsTerm ts

qualifyExVarsTerm t = t

{- | qualifies a list of variables with the suffix "_ex" to

distinguish them from the variables already bound -}

qualifyExVars :: [CAS.VAR_DECL] -> [CAS.VAR_DECL]

qualifyExVars = map qualifyExVar

{- | qualifies a variable with the suffix "_ex" to distinguish it from

the variables already bound -}

qualifyExVar :: CAS.VAR_DECL -> CAS.VAR_DECL

qualifyExVar (CAS.Var_decl vars s r) = CAS.Var_decl vars' s r

where vars' = map qualifyExVarAux vars

-- | qualifies a token with the suffix "_ex"

qualifyExVarAux :: Token -> Token

qualifyExVarAux var = mkSimpleId $ show var ++ "_ex"

-- | creates a list of strong equalities from two lists of terms

createEqs :: [CAS.CASLTERM] -> [CAS.CASLTERM] -> [CAS.CASLFORMULA]

createEqs (t1 : ts1) (t2 : ts2) = CAS.mkStEq t1 t2 : ls

where ls = createEqs ts1 ts2

createEqs _ _ = []

{- | extracts the operator at the top and the arguments of the lefthand side

in a strong equation -}

getLeftApp :: CAS.CASLFORMULA

-> Maybe (CAS.OP_SYMB, [CAS.CASLTERM], [CAS.CASLFORMULA])

getLeftApp (CAS.Equation term CAS.Strong _ _) = case getLeftAppTerm term of

Nothing -> Nothing

Just (op, ts) -> Just (op, ts, [])

getLeftApp (CAS.Relation prem c concl _) = case getLeftApp concl of

Just (op, ts, _) | c /= CAS.Equivalence -> Just (op, ts, conds)

where conds = getPremisesImplication prem

_ -> Nothing

getLeftApp _ = Nothing

{- | extracts the operator at the top and the arguments of the lefthand side

in an application term -}

getLeftAppTerm :: CAS.CASLTERM -> Maybe (CAS.OP_SYMB, [CAS.CASLTERM])

getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)

getLeftAppTerm _ = Nothing

{- | extracts the formulas of the given premise, distinguishing whether it is

a conjunction or not -}

getPremisesImplication :: CAS.CASLFORMULA -> [CAS.CASLFORMULA]

getPremisesImplication (CAS.Junction CAS.Con forms _) =

concatMap getPremisesImplication forms

getPremisesImplication form = [form]

-- | translate a Maude membership into a CASL formula

mb2formula :: IdMap -> MAS.Membership -> CAS.CASLFORMULA

mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

form = CAS.Membership ct s' nullRange

mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

conds_form = conds2formula im conds

concl_form = CAS.Membership ct s' nullRange

form = CAS.mkImpl conds_form concl_form

-- | translate a Maude rule into a CASL formula

rl2formula :: IdMap -> MAS.Rule -> CAS.CASLFORMULA

rl2formula im (MAS.Rl t t' [] _) = quantifyUniversally form

where ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rl to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

form = CAS.Predication pred_name [ct, ct'] nullRange

rl2formula im (MAS.Rl t t' conds@(_ : _) _) = quantifyUniversally form

where ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rl to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

conds_form = conds2formula im conds

concl_form = CAS.Predication pred_name [ct, ct'] nullRange

form = CAS.mkImpl conds_form concl_form

-- | translate a conjunction of Maude conditions to a CASL formula

conds2formula :: IdMap -> [MAS.Condition] -> CAS.CASLFORMULA

conds2formula im conds = CAS.conjunct forms

where forms = map (cond2formula im) conds

-- | translate a single Maude condition to a CASL formula

cond2formula :: IdMap -> MAS.Condition -> CAS.CASLFORMULA

cond2formula im (MAS.EqCond t t') = CAS.mkStEq ct ct'

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MatchCond t t') = CAS.mkStEq ct ct'

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

cond2formula im (MAS.MbCond t s) = CAS.Membership ct s' nullRange

where ct = maudeTerm2caslTerm im t

s' = token2id $ getName s

cond2formula im (MAS.RwCond t t') = CAS.mkPredication pred_name [ct, ct']

where ct = maudeTerm2caslTerm im t

ct' = maudeTerm2caslTerm im t'

ty = token2id $ getName $ MAS.getTermType t

kind = Map.findWithDefault (errorId "rw cond to formula") ty im

pred_type = CAS.Pred_type [kind, kind] nullRange

pred_name = CAS.Qual_pred_name rewID pred_type nullRange

-- | translates a Maude term into a CASL term

maudeTerm2caslTerm :: IdMap -> MAS.Term -> CAS.CASLTERM

maudeTerm2caslTerm im (MAS.Var q ty) = CAS.Qual_var q ty' nullRange

where ty' = maudeType2caslSort ty im

maudeTerm2caslTerm im (MAS.Const q ty) = CAS.Application op [] nullRange

where name = token2id q

ty' = maudeType2caslSort ty im

op_type = CAS.Op_type CAS.Total [] ty' nullRange

op = CAS.Qual_op_name name op_type nullRange

maudeTerm2caslTerm im (MAS.Apply q ts ty) = CAS.Application op tts nullRange

where name = token2id q

tts = map (maudeTerm2caslTerm im) ts

ty' = maudeType2caslSort ty im

types_tts = getTypes tts

op_type = CAS.Op_type CAS.Total types_tts ty' nullRange

op = CAS.Qual_op_name name op_type nullRange

maudeSymbol2caslSort :: MSym.Symbol -> IdMap -> CAS.SORT

maudeSymbol2caslSort (MSym.Sort q) _ = token2id q

maudeSymbol2caslSort (MSym.Kind q) im = Map.findWithDefault err q' im

where q' = token2id q

err = errorId "error translate symbol"

maudeSymbol2caslSort _ _ = errorId "error translate symbol"

maudeType2caslSort :: MAS.Type -> IdMap -> CAS.SORT

maudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q

maudeType2caslSort (MAS.TypeKind q) im = Map.findWithDefault err q' im

where q' = token2id $ getName q

err = errorId "error translate type"

-- | obtains the types of the given terms

getTypes :: [CAS.CASLTERM] -> [Id]

getTypes = mapMaybe getType

-- | extracts the type of the temr

getType :: CAS.CASLTERM -> Maybe Id

getType (CAS.Qual_var _ kind _) = Just kind

getType (CAS.Application op _ _) = case op of

CAS.Qual_op_name _ (CAS.Op_type _ _ kind _) _ -> Just kind

_ -> Nothing

getType _ = Nothing

-- | generates the formulas for the rewrite predicates

rewPredicatesSens :: Set.Set Id -> [Named CAS.CASLFORMULA]

rewPredicatesSens = Set.fold rewPredicateSens []

-- | generates the formulas for the rewrite predicate of the given sort

rewPredicateSens :: Id -> [Named CAS.CASLFORMULA] -> [Named CAS.CASLFORMULA]

rewPredicateSens kind acc = ref : trans : acc

where ref = reflSen kind

trans = transSen kind

-- | creates the reflexivity predicate for the given kind

reflSen :: Id -> Named CAS.CASLFORMULA

reflSen kind = makeNamed name $ quantifyUniversally form

where v = newVar kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

form = CAS.Predication pn [v, v] nullRange

name = "rew_refl_" ++ show kind

-- | creates the transitivity predicate for the given kind

transSen :: Id -> Named CAS.CASLFORMULA

transSen kind = makeNamed name $ quantifyUniversally form

where v1 = newVarIndex 1 kind

v2 = newVarIndex 2 kind

v3 = newVarIndex 3 kind

pred_type = CAS.Pred_type [kind, kind] nullRange

pn = CAS.Qual_pred_name rewID pred_type nullRange

prem1 = CAS.Predication pn [v1, v2] nullRange

prem2 = CAS.Predication pn [v2, v3] nullRange

concl = CAS.Predication pn [v1, v3] nullRange

conj_form = CAS.conjunct [prem1, prem2]

form = CAS.mkImpl conj_form concl

name = "rew_trans_" ++ show kind

-- | generate the predicates for the rewrites

rewPredicates :: Set.Set Id -> CSign.PredMap

rewPredicates = Set.fold rewPredicate MapSet.empty

-- | generate the predicates for the rewrites of the given sort

rewPredicate :: Id -> CSign.PredMap -> CSign.PredMap

rewPredicate kind = MapSet.insert rewID $ CSign.PredType [kind, kind]

-- | create the predicates that assign sorts to each term

kindPredicates :: IdMap -> Map.Map Id (Set.Set CSign.PredType)

kindPredicates = Map.foldWithKey kindPredicate Map.empty

{- | create the predicates that assign the current sort to the

corresponding terms -}

kindPredicate :: Id -> Id -> Map.Map Id (Set.Set CSign.PredType)

-> Map.Map Id (Set.Set CSign.PredType)

kindPredicate sort kind mis = if sort == str2id "Universal" then mis else

let ar = Set.singleton $ CSign.PredType [kind]

in Map.insertWith Set.union sort ar mis

-- | extract the kinds from the map of id's

kindsFromMap :: IdMap -> Set.Set Id

kindsFromMap = Map.fold Set.insert Set.empty

{- | transform the set of Maude sorts in a set of CASL sorts, including

only one sort for each kind. -}

sortsTranslation :: MSign.SortSet -> MSign.SubsortRel -> Set.Set Id

sortsTranslation = sortsTranslationList . Set.toList

{- | transform a list representing the Maude sorts in a set of CASL sorts,

including only one sort for each kind. -}

sortsTranslationList :: [MSym.Symbol] -> MSign.SubsortRel -> Set.Set Id

sortsTranslationList [] _ = Set.empty

sortsTranslationList (s : ss) r = Set.insert (sort2id tops) res

where tops@(top : _) = List.sort $ getTop r s

ss' = deleteRelated ss top r

res = sortsTranslation ss' r

-- | return the maximal elements from the sort relation

getTop :: MSign.SubsortRel -> MSym.Symbol -> [MSym.Symbol]

getTop r tok = case succs of

[] -> [tok]

toks@(_ : _) -> foldr ((++) . getTop r) [] toks

where succs = Set.toList $ Rel.succs r tok

-- | delete from the list of sorts those in the same kind that the parameter

deleteRelated :: [MSym.Symbol] -> MSym.Symbol -> MSign.SubsortRel

-> MSign.SortSet

deleteRelated ss sym r = foldr (f sym tc) Set.empty ss

where tc = Rel.transClosure r

f sort trC x y = if MSym.sameKind trC sort x

then y

else Set.insert x y

-- | build an Id from a token with the function mkId

token2id :: Token -> Id

token2id t = mkId ts

where ts = maudeSymbol2validCASLSymbol t

-- | build an Id from a Maude symbol

sym2id :: MSym.Symbol -> Id

sym2id = token2id . getName

-- | generates an Id from a string

str2id :: String -> Id

str2id = token2id . mkSimpleId

-- | build an Id from a list of sorts, taking the first from the ordered list

sort2id :: [MSym.Symbol] -> Id

sort2id syms = mkId sym''

where sym : _ = List.sort syms

sym' = getName sym

sym'' = maudeSymbol2validCASLSymbol sym'

-- | add universal quantification of all variables in the formula

quantifyUniversally :: CAS.CASLFORMULA -> CAS.CASLFORMULA

quantifyUniversally form = CAS.mkForall var_decl form

where vars = getVars form

var_decl = listVarDecl vars

{- | traverses a map with sorts as keys and sets of variables as value and

creates a list of variable declarations -}

listVarDecl :: Map.Map Id (Set.Set Token) -> [CAS.VAR_DECL]

listVarDecl = Map.foldWithKey f []

where f sort var_set =

(CAS.Var_decl (Set.toList var_set) sort nullRange :)

-- | removes a quantification from a formula

noQuantification :: CAS.CASLFORMULA -> (CAS.CASLFORMULA, [CAS.VAR_DECL])

noQuantification (CAS.Quantification _ vars form _) = (form, vars)

noQuantification form = (form, [])

-- | translate the CASL sorts to symbols

kinds2syms :: Set.Set Id -> Set.Set CSign.Symbol

kinds2syms = Set.map kind2sym

-- | translate a CASL sort to a CASL symbol

kind2sym :: Id -> CSign.Symbol

kind2sym k = CSign.Symbol k CSign.SortAsItemType

-- | translates the CASL predicates into CASL symbols

preds2syms :: CSign.PredMap -> Set.Set CSign.Symbol

preds2syms = MapSet.foldWithKey createSym4id Set.empty

-- | creates a CASL symbol for a predicate

createSym4id :: Id -> CSign.PredType -> Set.Set CSign.Symbol

-> Set.Set CSign.Symbol

createSym4id pn pt = Set.insert sym

where sym = CSign.Symbol pn $ CSign.PredAsItemType pt

-- | translates the CASL operators into CASL symbols

ops2symbols :: CSign.OpMap -> Set.Set CSign.Symbol

ops2symbols = MapSet.foldWithKey createSymOp4id Set.empty

-- | creates a CASL symbol for an operator

createSymOp4id :: Id -> CSign.OpType -> Set.Set CSign.Symbol

-> Set.Set CSign.Symbol

createSymOp4id on ot = Set.insert sym

where sym = CSign.Symbol on $ CSign.OpAsItemType ot

{- | extract the variables from a CASL formula and put them in a map

with keys the sort of the variables and value the set of variables

in this sort -}

getVars :: CAS.CASLFORMULA -> Map.Map Id (Set.Set Token)

getVars (CAS.Quantification _ _ f _) = getVars f

getVars (CAS.Junction _ fs _) =

foldr (Map.unionWith Set.union . getVars) Map.empty fs

getVars (CAS.Relation f1 _ f2 _) = Map.unionWith Set.union v1 v2

where v1 = getVars f1

v2 = getVars f2

getVars (CAS.Negation f _) = getVars f

getVars (CAS.Predication _ ts _) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVars (CAS.Definedness t _) = getVarsTerm t

getVars (CAS.Equation t1 _ t2 _) = Map.unionWith Set.union v1 v2

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

getVars (CAS.Membership t _ _) = getVarsTerm t

getVars (CAS.Mixfix_formula t) = getVarsTerm t

getVars _ = Map.empty

-- | extract the variables of a CASL term

getVarsTerm :: CAS.CASLTERM -> Map.Map Id (Set.Set Token)

getVarsTerm (CAS.Qual_var var sort _) =

Map.insert sort (Set.singleton var) Map.empty

getVarsTerm (CAS.Application _ ts _) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t

getVarsTerm (CAS.Cast t _ _) = getVarsTerm t

getVarsTerm (CAS.Conditional t1 f t2 _) = Map.unionWith Set.union v3 m

where v1 = getVarsTerm t1

v2 = getVarsTerm t2

v3 = getVars f

m = Map.unionWith Set.union v1 v2

getVarsTerm (CAS.Mixfix_term ts) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_parenthesized ts _) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_bracketed ts _) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVarsTerm (CAS.Mixfix_braced ts _) =

foldr (Map.unionWith Set.union . getVarsTerm) Map.empty ts

getVarsTerm _ = Map.empty

-- | generates the constructor constraint

ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA

ctorSen isFree (sorts, _, ops) =

let sortList = Set.toList sorts

opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide

(CSign.toOP_TYPE $ compType c) $ posOfId ide)

$ Set.toList ops

allSyms = opSyms

resType _ (CAS.Op_name _) = False

resType s (CAS.Qual_op_name _ t _) = CAS.res_OP_TYPE t == s

getIndex s = fromMaybe (-1) $ List.elemIndex s sortList

addIndices (CAS.Op_name _) =

error "CASL/StaticAna: Internal error in function addIndices"

addIndices os@(CAS.Qual_op_name _ t _) =

(os, map getIndex $ CAS.args_OP_TYPE t)

collectOps s =

CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s

constrs = map collectOps sortList

f = CAS.Sort_gen_ax constrs isFree

in makeNamed

("ga_generated_" ++ showSepList (showString "_") showId sortList "") f

-- | transforms a maude identifier into a valid CASL identifier

maudeSymbol2validCASLSymbol :: Token -> [Token]

maudeSymbol2validCASLSymbol t = splitDoubleUnderscores str ""

where str = ms2vcs $ show t

{- | transforms a string coding a Maude identifier into another string

representing a CASL identifier -}

ms2vcs :: String -> String

ms2vcs s@('k' : 'i' : 'n' : 'd' : '_' : _) = s

ms2vcs s = if Map.member s stringMap

then stringMap Map.! s

else let f x y

| Map.member x charMap = (charMap Map.! x) ++ "'" ++ y

| x == '_' = "__" ++ y

| otherwise = x : y

in foldr f [] s

-- | map of reserved words

stringMap :: Map.Map String String

stringMap = Map.fromList

[("true", "maudeTrue"),

("false", "maudeFalse"),

("not_", "neg__"),

("s_", "suc"),

("_+_", "__+__"),

("_*_", "__*__"),

("_<_", "__<__"),

("_<=_", "__<=__"),

("_>_", "__>__"),

("_>=_", "__>=__"),

("_and_", "__maudeAnd__")]

{- | splits the string into a list of tokens, separating the double

underscores from the rest of characters -}

splitDoubleUnderscores :: String -> String -> [Token]

splitDoubleUnderscores [] acc = if null acc

then []

else [mkSimpleId acc]

splitDoubleUnderscores ('_' : '_' : cs) acc = if null acc

then dut : rest

else acct : dut : rest

where acct = mkSimpleId acc

dut = mkSimpleId "__"

rest = splitDoubleUnderscores cs []

splitDoubleUnderscores (c : cs) acc = splitDoubleUnderscores cs (acc ++ [c])

-- | error Id

errorId :: String -> Id

errorId s = token2id $ mkSimpleId $ "ERROR: " ++ s

kindId :: Id -> Id

kindId i = token2id $ mkSimpleId $ "kind_" ++ show i

kindMapId :: MSign.KindRel -> IdMap

kindMapId kr = Map.fromList krl'

where krl = Map.toList kr

krl' = map (\ (x, y) -> (mSym2caslId x, mSym2caslId y)) krl

mSym2caslId :: MSym.Symbol -> Id

mSym2caslId (MSym.Sort q) = token2id q

mSym2caslId (MSym.Kind q) = kindId q'

where q' = token2id q

mSym2caslId _ = errorId "error translate symbol"

-- | checks the profile has at least one sort

atLeastOneSort :: MSign.OpMap -> MSign.OpMap

atLeastOneSort om = Map.fromList lom'

where lom = Map.toList om

lom' = filterAtLeastOneSort lom

filterAtLeastOneSort :: [(MAS.Qid, MSign.OpDeclSet)]

-> [(MAS.Qid, MSign.OpDeclSet)]

filterAtLeastOneSort [] = []

filterAtLeastOneSort ((q, ods) : ls) = hd ++ filterAtLeastOneSort ls

where ods' = atLeastOneSortODS ods

hd = if Set.null ods'

then []

else [(q, ods')]

atLeastOneSortODS :: MSign.OpDeclSet -> MSign.OpDeclSet

atLeastOneSortODS ods = Set.fromList lods'

where lods = Set.toList ods

lods' = atLeastOneSortLODS lods

atLeastOneSortLODS :: [MSign.OpDecl] -> [MSign.OpDecl]

atLeastOneSortLODS [] = []

atLeastOneSortLODS ((ss, ats) : ls) = res ++ atLeastOneSortLODS ls

where ss' = atLeastOneSortSS ss

res = if Set.null ss'

then []

else [(ss', ats)]

atLeastOneSortSS :: Set.Set MSym.Symbol -> Set.Set MSym.Symbol

atLeastOneSortSS = Set.filter hasOneSort

hasOneSort :: MSym.Symbol -> Bool

hasOneSort (MSym.Operator _ ar co) = any isSymSort (co : ar)

hasOneSort _ = False

isSymSort :: MSym.Symbol -> Bool

isSymSort (MSym.Sort _) = True

isSymSort _ = False

{- | translates the Maude operator map into a tuple of CASL operators, CASL

associative operators, membership induced from each Maude operator,

and the set of sorts with the ctor attribute -}

translateOps' :: IdMap -> MSign.OpMap -> OpTransTuple

translateOps' im = Map.fold (translateOpDeclSet' im)

(MapSet.empty, MapSet.empty, Set.empty)

-- | translates an operator declaration set into a tern as described above

translateOpDeclSet' :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple

translateOpDeclSet' im ods tpl = Set.fold (translateOpDecl' im) tpl ods

{- | given an operator declaration updates the accumulator with the translation

to CASL operator, checking if the operator has the assoc attribute to insert

it in the map of associative operators, generating the membership predicate

induced by the operator declaration, and checking if it has the ctor

attribute to introduce the operator in the generators sentence -}

translateOpDecl' :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple

translateOpDecl' im (syms, ats) (ops, assoc_ops, cs) = case tl of

[] -> (ops', assoc_ops', cs')

_ -> translateOpDecl' im (syms', ats) (ops', assoc_ops', cs')

where sym = head $ Set.toList syms

tl = tail $ Set.toList syms

syms' = Set.fromList tl

(cop_id, ot, _) = fromJust $ maudeSym2CASLOp' im sym

ops' = MapSet.insert cop_id ot ops

assoc_ops' = if any MAS.assoc ats

then MapSet.insert cop_id ot assoc_ops

else assoc_ops

cs' = if any MAS.ctor ats

then Set.insert (Component cop_id ot) cs

else cs

{- | translates a Maude operator symbol into a pair with the id of the operator

and its CASL type -}

maudeSym2CASLOp' :: IdMap -> MSym.Symbol

-> Maybe (Id, CSign.OpType, CSign.OpType)

maudeSym2CASLOp' im (MSym.Operator op ar co) = Just (token2id op, ot, ot')

where f = token2id . getName

g = (`maudeSymbol2caslSort'` im)

ot = CSign.OpType CAS.Total (map g ar) (g co)

ot' = CSign.OpType CAS.Total (map f ar) (f co)

maudeSym2CASLOp' _ _ = Nothing

maudeSymbol2caslSort' :: MSym.Symbol -> IdMap -> CAS.SORT

maudeSymbol2caslSort' (MSym.Sort q) _ =

token2id $ mkSimpleId $ "kind_" ++ show q

maudeSymbol2caslSort' (MSym.Kind q) im = Map.findWithDefault err q' im

where q' = token2id q

err = errorId "error translate symbol"

maudeSymbol2caslSort' _ _ = errorId "error translate symbol"