PreComorphism.hs revision 6e121321775373fe11161d23c541437456df19b4
2d0611ffc9f91c5fc2ddccb93f9a3d17791ae650takashiModule : $Header$
c79e39ad568d9af854765f64049534044ef6c034ndDescription : Maude Comorphisms
d3e250aab242db84d14060985b5db675a731d548ndCopyright : (c) Adrian Riesco, Facultad de Informatica UCM 2009
c79e39ad568d9af854765f64049534044ef6c034ndLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c79e39ad568d9af854765f64049534044ef6c034ndMaintainer : ariesco@fdi.ucm.es
c79e39ad568d9af854765f64049534044ef6c034ndStability : experimental
c79e39ad568d9af854765f64049534044ef6c034ndPortability : portable
4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluemComorphism 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 Comorphisms.GetPreludeLib (readLib)
import System.IO.Unsafe
import Static.GTheory
import Logic.Prover
import Logic.Coerce
type IdMap = Map.Map Id Id
src = MMorphism.source morph
tgt = MMorphism.target morph
mk = kindMapId $ MSign.kindRel src
mk' = kindMapId $ MSign.kindRel tgt
smap = MMorphism.sortMap morph
kmap = MMorphism.kindMap morph
omap = MMorphism.opMap morph
in return $ CMorphism.Morphism src' tgt' smap' omap' pmap ()
g = \ x -> Map.findWithDefault (errorId "translate op map entry") (f x) im
to' = (token2id to, CAS.Total)
copm' = Map.insert cop to' copm
translateOpMapEntry _ _ _ _ = Map.empty
where mk = kindMapId $ MSign.kindRel sg
kind = Map.findWithDefault (errorId "map symbol") sym_id mk
pred_data = CSign.PredType [kind]
where mk = kindMapId $ MSign.kindRel sg
mapSymbol _ _ = Set.empty
maudeSort2caslId :: IdMap -> MSym.Symbol -> Id
maudeSort2caslId im sym = Map.findWithDefault (errorId "sort to id") (token2id $ getName sym) im
createPredMap4sort im from to m = Map.insert key id_to m
kind = Map.findWithDefault (errorId "predicate for sort") id_from im
key = (id_from, CSign.PredType [kind])
applySortMap2CASLSorts sm im im' = Map.fromList sml'
where sml = Map.toList sm
f = \ x y -> Map.findWithDefault (errorId $ "err" ++ (show $ mSym2caslId x)) (mSym2caslId x) y
rename :: MMorphism.SortMap -> Token -> Token
where sym = MSym.Sort tok
sym' = if Map.member sym sm
then fromJust $ Map.lookup sym sm
where mk = kindMapId $ MSign.kindRel sg
MAS.Eq _ _ _ ats = eq
mapSentence sg sen@(MSentence.Membership mb) = return $ sentence form
where mk = kindMapId $ MSign.kindRel sg
MAS.Mb _ _ _ _ = mb
mapSentence sg sen@(MSentence.Rule rl) = return $ sentence form
where mk = kindMapId $ MSign.kindRel sg
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 = kindMapId $ MSign.kindRel msign
sbs = MSign.subsorts msign
cs = Set.union ss' $ kindsFromMap mk
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) = (sortSym2id sym, Set.map (kindId . sortSym2id) st)
subsorts2Ids (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
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
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
kindMapId :: MSign.KindRel -> IdMap
kindMapId kr = Map.fromList krl'
where krl = Map.toList kr
mSym2caslId :: MSym.Symbol -> Id
mSym2caslId (MSym.Sort q) = token2id q
mSym2caslId (MSym.Kind q) = kindId q'