PreComorphism.hs revision ebdb7b09e2ad2bb780d84c127d72c30dfcfb87b2
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoModule : $Header$
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoDescription : Maude Comorphisms
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoMaintainer : ariesco@fdi.ucm.es
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoStability : experimental
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoPortability : portable
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescoComorphism from Maude to CASL.
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Data.List as List
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Data.Set as Set
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Data.Map as Map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Sign as MSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Sentence as MSentence
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Morphism as MMorphism
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.AS_Maude as MAS
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Maude.Symbol as MSym
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified CASL.Sign as CSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified CASL.Morphism as CMorphism
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified CASL.AS_Basic_CASL as CAS
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Common.Lib.Rel as Rel
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescotype IdMap = Map.Map Id Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescotype OpTransTuple = (CSign.OpMap, CSign.OpMap, Set.Set Component)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | generates a CASL morphism from a Maude morphism
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapMorphism :: MMorphism.Morphism -> Result (CMorphism.CASLMor)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapMorphism morph =
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco mk = arrangeKinds (MSign.sorts src) (MSign.subsorts src)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco cs = kindsFromMap mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco smap' = applySortMap2CASLSorts smap cs
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco omap' = maudeOpMap2CASLOpMap mk omap
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco pmap = createPredMap mk smap
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco (src', _) = maude2casl src []
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco (tgt', _) = maude2casl tgt []
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | translates the Maude morphism between operators into a CASL morpshim between
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomaudeOpMap2CASLOpMap :: IdMap -> MMorphism.OpMap -> CMorphism.Op_map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomaudeOpMap2CASLOpMap im = Map.foldWithKey (translateOpMapEntry im) Map.empty
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | translates the mapping between two symbols representing operators into
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- a CASL operators map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescotranslateOpMapEntry :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Op_map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescotranslateOpMapEntry im (MSym.Operator from ar co) (MSym.Operator to _ _) copm = copm'
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where f = token2id . getName
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco cop = (token2id from, ot)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco to' = (token2id to, CAS.Total)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco copm' = Map.insert cop to' copm
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescotranslateOpMapEntry _ _ _ _ = Map.empty
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | generates a set of CASL symbol from a Maude Symbol
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapSymbol :: MSign.Sign -> MSym.Symbol -> Set.Set CSign.Symbol
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapSymbol sg (MSym.Sort q) = Set.singleton csym
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco sym_id = token2id q
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco kind = Map.findWithDefault (errorId "map symbol") sym_id mk
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco pred_data = CSign.PredType [kind]
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco csym = CSign.Symbol sym_id $ CSign.PredAsItemType pred_data
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapSymbol sg (MSym.Operator q ar co) = Set.singleton csym
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where mk = arrangeKinds (MSign.sorts sg) (MSign.subsorts sg)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco q' = token2id q
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ar' = map (maudeSort2caslId mk) ar
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco co' = token2id $ getName co
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco csym = CSign.Symbol q' $ CSign.OpAsItemType op_data
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomapSymbol _ _ = Set.empty
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | returns the sort in CASL of the Maude sort symbol
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomaudeSort2caslId :: IdMap -> MSym.Symbol -> Id
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescomaudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | creates the predicate map for the CASL morphism from the Maude sort map and
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- the map between sorts and kinds
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescocreatePredMap :: IdMap -> MMorphism.SortMap -> CMorphism.Pred_map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescocreatePredMap im = Map.foldWithKey (createPredMap4sort im) Map.empty
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco-- | creates an entry of the predicate map for a single sort
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescocreatePredMap4sort :: IdMap -> MSym.Symbol -> MSym.Symbol -> CMorphism.Pred_map
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescocreatePredMap4sort im from to m = Map.insert key id_to m
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco where id_from = token2id $ getName from
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco id_to = token2id $ getName to
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco kind = Map.findWithDefault (errorId "predicate for sort") id_from im
key = (id_from, CSign.PredType [kind])
else Map.insert sort new_sort csm
rename :: MMorphism.SortMap -> Token -> Token
where sym = MSym.Sort tok
sym' = if Map.member sym sm
then fromJust $ Map.lookup sym sm
MAS.Eq _ _ _ ats = eq
mapSentence sg sen@(MSentence.Membership mb) = return $ sentence form
MAS.Mb _ _ _ _ = mb
mapSentence sg sen@(MSentence.Rule rl) = return $ sentence form
MAS.Rl _ _ _ _ = rl
maude2casl msign nsens = (csign { CSign.sortSet = cs,
CSign.sortRel = 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 = arrangeKinds ss (MSign.subsorts msign)
sbs = MSign.subsorts msign
ops = deleteUniversal $ MSign.ops msign
ctor_sen = [] -- [ctorSen False (cs, Rel.empty, comps)]
pred_forms = loadLibraries (MSign.sorts msign) ops
maudeSbs2caslSbs sbs im = Rel.fromDistinctMap m4
l2 = idList2Subsorts $ Map.toList im
m1 = Map.fromList l1
m2 = Map.fromList l2
m3 = Map.fromList l3
idList2Subsorts :: [(Id, Id)] -> [(Id, Set.Set Id)]
where t1 = (id1, Set.singleton id2)
maudeSb2caslSb (sym, st) = (kindId $ sortSym2id sym, Set.map (kindId . sortSym2id) st)
subsortsKinds (sym, st) = (sortSym2id sym, Set.map sortSym2id st)
sortSym2id :: MSym.Symbol -> Id
sortSym2id (MSym.Sort q) = token2id q
rewPredicatesCongSens = Map.foldWithKey rewPredCongSet []
where fs' = Set.fold (rewPredCong idn) [] ots
where args = CSign.opArgs ot
res = CSign.opRes ot
res_pred_type = CAS.Pred_type [res, res] nullRange
pn = CAS.Qual_pred_name rewID res_pred_type 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
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
loadNaturalNatSens :: [Named CAS.CASLFORMULA]
let lib = head $ unsafePerformIO $ readLib "Maude/MaudeNumbers.casl"
ctorCons :: Named CAS.CASLFORMULA -> Bool
CAS.Sort_gen_ax _ _ -> True
booleanImported :: MSign.OpMap -> Bool
booleanImported = Map.member (mkSimpleId "if_then_else_fi")
b2 = Map.member (mkSimpleId "s_") om
specialZeroSet :: MSign.OpDeclSet -> Bool
specialZeroSet = Set.fold specialZero False
specialZero :: MSign.OpDecl -> Bool -> Bool
isSpecial :: [MAS.Attr] -> Bool
isSpecial ((MAS.Special _) : _) = True
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
universalOps kinds om True = Set.fold universalOpKind om kinds
universalSens = Set.fold universalSensKind []
ifSens :: Id -> [Named CAS.CASLFORMULA]
true_id = CAS.Qual_op_name (str2id "true") true_type nullRange
true_term = CAS.Application true_id [] nullRange
if_id = CAS.Qual_op_name if_name if_type nullRange
if_term = CAS.Application if_id [bv, v1, v2] nullRange
prem = CAS.Strong_equation bv true_term nullRange
concl = CAS.Strong_equation if_term v1 nullRange
form = CAS.Implication prem concl True nullRange
neg_prem = CAS.Negation prem nullRange
neg_concl = CAS.Strong_equation if_term v2 nullRange
neg_form = CAS.Implication neg_prem neg_concl True nullRange
equalitySens :: Id -> [Named CAS.CASLFORMULA]
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.Strong_equation v1 v2 nullRange
double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
concl = CAS.Strong_equation double_eq_term true_term nullRange
form = CAS.Implication prem concl True nullRange
neg_prem = CAS.Negation prem nullRange
new_concl = CAS.Strong_equation double_eq_term false_term nullRange
comp_form = CAS.Implication neg_prem new_concl True nullRange
nonEqualitySens :: Id -> [Named CAS.CASLFORMULA]
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.Strong_equation v1 v2 nullRange
double_eq_id = CAS.Qual_op_name double_eq_name double_eq_type nullRange
double_eq_term = CAS.Application double_eq_id [v1, v2] nullRange
concl = CAS.Strong_equation double_eq_term false_term nullRange
form = CAS.Implication prem concl True nullRange
neg_prem = CAS.Negation prem nullRange
new_concl = CAS.Strong_equation double_eq_term true_term nullRange
comp_form = CAS.Implication neg_prem new_concl True nullRange
translateOps :: IdMap -> MSign.OpMap -> OpTransTuple
translateOpDeclSet :: IdMap -> MSign.OpDeclSet -> OpTransTuple -> OpTransTuple
translateOpDeclSet im ods tpl = Set.fold (translateOpDecl im) tpl ods
translateOpDecl :: IdMap -> MSign.OpDecl -> OpTransTuple -> OpTransTuple
where sym = head $ Set.toList syms
tl = tail $ Set.toList syms
syms' = Set.fromList tl
assoc_ops' = if any MAS.assoc ats
cs' = if any MAS.ctor ats
then Set.insert (Component cop_id ot) cs
maudeSym2CASLOp im (MSym.Operator op ar co) = Just (token2id op, ot, ot')
g = \ x -> maudeSymbol2caslSort x im -- \ x -> Map.findWithDefault (errorId "Maude_sym2CASL_sym") (f x) im
createConjForm [] = CAS.True_atom nullRange
createConjForm fs = CAS.Conjunction fs nullRange
createImpForm (CAS.True_atom _) form = form
createImpForm form1 form2 = CAS.Implication form1 form2 True nullRange
ops2predPremises im (MSym.Sort s : ss) i = (var : terms, form : forms)
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
form = CAS.Predication pred_name [var] nullRange
ops2predPremises im (MSym.Kind k : ss) i = (var : terms, forms)
kind = Map.findWithDefault (errorId "mb of op as predicate") k' im
splitOwiseEqs :: [Named MSentence.Sentence] ->
noOwiseSen2Formula :: IdMap -> Named MSentence.Sentence
-> Named CAS.CASLFORMULA
where MSentence.Equation eq = sentence s
owiseSen2Formula :: IdMap -> [Named CAS.CASLFORMULA]
where MSentence.Equation eq = sentence s
MSentence.Membership mb -> let
MSentence.Rule rl -> let
_ -> makeNamed "" $ CAS.False_atom nullRange
newVarIndex :: Int -> Id -> CAS.CASLTERM
newVarIndex i sort = CAS.Qual_var var sort nullRange
newVar :: Id -> CAS.CASLTERM
newVar sort = CAS.Qual_var var sort nullRange
noOwiseEq2Formula im (MAS.Eq t t' [] _) = quantifyUniversally form
form = CAS.Strong_equation ct ct' nullRange
noOwiseEq2Formula im (MAS.Eq t t' conds@(_:_) _) = quantifyUniversally form
concl_form = CAS.Strong_equation ct ct' nullRange
then CAS.Conjunction ex_forms nullRange
conj_form = CAS.Conjunction prems nullRange
neg_form = CAS.Negation ex_form nullRange
createEqs (t1 : ts1) (t2 : ts2) = CAS.Strong_equation t1 t2 nullRange : ls
getLeftApp (CAS.Strong_equation term _ _) = case getLeftAppTerm term of
getLeftApp (CAS.Implication prem concl _ _) = case getLeftApp concl of
getLeftAppTerm (CAS.Application op ts _) = Just (op, ts)
getPremisesImplication (CAS.Conjunction forms _) = forms
mb2formula im (MAS.Mb t s [] _) = quantifyUniversally form
form = CAS.Membership ct s' nullRange
mb2formula im (MAS.Mb t s conds@(_ : _) _) = quantifyUniversally form
concl_form = CAS.Membership ct s' nullRange
form = CAS.Implication conds_form concl_form True nullRange
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
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
concl_form = CAS.Predication pred_name [ct, ct'] nullRange
form = CAS.Implication conds_form concl_form True nullRange
conds2formula im conds = CAS.Conjunction forms nullRange
kind = Map.findWithDefault (errorId "mb cond to formula") s' im
pred_type = CAS.Pred_type [kind] nullRange
pred_name = CAS.Qual_pred_name s' pred_type nullRange
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
op = CAS.Qual_op_name name op_type nullRange
op = CAS.Qual_op_name name op_type nullRange
maudeSymbol2caslSort (MSym.Sort q) _ = token2id q
maudeType2caslSort (MAS.TypeSort q) _ = token2id $ getName q
getTypes :: [CAS.CASLTERM] -> [Id]
getType :: CAS.CASLTERM -> Maybe Id
getType (CAS.Qual_var _ kind _) = Just kind
getType (CAS.Application op _ _) = case op of
rewPredicatesSens = Set.fold rewPredicateSens []
reflSen :: Id -> Named CAS.CASLFORMULA
pred_type = CAS.Pred_type [kind, kind] nullRange
pn = CAS.Qual_pred_name rewID pred_type nullRange
form = CAS.Predication pn [v, v] nullRange
transSen :: Id -> Named CAS.CASLFORMULA
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.Conjunction [prem1, prem2] nullRange
form = CAS.Implication conj_form concl True nullRange
kindsFromMap :: IdMap -> Set.Set Id
arrangeKinds ss _ = Map.fromList l'
where l = Set.toList ss
arrangeSortKind :: MSym.Symbol -> (Id, Id)
where tops = List.sort $ getTop r s
tc = Rel.transClosure r
f = \ x y z -> Map.insert (sym2id y) (kindId $ sort2id x) z
sameKindList t r (t' : ts) = if MSym.sameKind r t t'
sortsTranslation ss r = sortsTranslationList (Set.toList ss) r
sortsTranslationList [] _ = Set.empty
sortsTranslationList (s : ss) r = Set.insert (sort2id tops) res
where tops@(top : _) = List.sort $ getTop r s
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
else Set.insert x y
sym2id :: MSym.Symbol -> Id
sort2id :: [MSym.Symbol] -> Id
where sym = head $ List.sort syms
listVarDecl = Map.foldWithKey f []
noQuantification (CAS.Quantification _ vars form _) = (form, vars)
kinds2syms = Set.map kind2sym
kind2sym :: Id -> CSign.Symbol
pred2sym pn spt acc = Set.fold (createSym4id pn) acc spt
createSym4id pn pt acc = Set.insert sym acc
op2sym on sot acc = Set.union set acc
createSymOp4id on ot acc = Set.insert sym acc
getVars (CAS.Quantification _ _ f _) = getVars f
getVars (CAS.Negation f _) = getVars f
getVars (CAS.Definedness t _) = getVarsTerm t
getVars (CAS.Membership t _ _) = getVarsTerm t
getVars (CAS.Mixfix_formula t) = getVarsTerm t
getVars _ = Map.empty
getVarsTerm (CAS.Sorted_term t _ _) = getVarsTerm t
getVarsTerm (CAS.Cast t _ _) = getVarsTerm t
getVarsTerm (CAS.Mixfix_parenthesized ts _) =
getVarsTerm (CAS.Mixfix_bracketed ts _) =
getVarsTerm (CAS.Mixfix_braced ts _) =
getVarsTerm _ = Map.empty
ctorSen :: Bool -> GenAx -> Named CAS.CASLFORMULA
let sortList = Set.toList sorts
opSyms = map ( \ c -> let ide = compId c in CAS.Qual_op_name ide
resType _ (CAS.Op_name _) = False
getIndex s = maybe (-1) id $ List.findIndex (== 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)
CAS.Constraint s (map addIndices $ filter (resType s) allSyms) s
f = CAS.Sort_gen_ax constrs isFree
ms2vcs s = case Map.member s stringMap of
True -> Map.findWithDefault "" s stringMap
False -> let f = \ x y -> if Map.member x charMap
stringMap :: Map.Map String String
stringMap = Map.fromList