CASL2PCFOL.inline.hs revision f2d72b2254513ef810b0951f0b13a62c2921cb4d
843e19887f64dde75055cf8842fc4db2171eff45johnlevModule : $Header$
843e19887f64dde75055cf8842fc4db2171eff45johnlevCopyright : (c) Zicheng Wang, Uni Bremen 2002-2004
843e19887f64dde75055cf8842fc4db2171eff45johnlevLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
843e19887f64dde75055cf8842fc4db2171eff45johnlevMaintainer : hets@tzi.de
843e19887f64dde75055cf8842fc4db2171eff45johnlevStability : provisional
843e19887f64dde75055cf8842fc4db2171eff45johnlevPortability : portable
843e19887f64dde75055cf8842fc4db2171eff45johnlev Coding out subsorting (SubPCFOL= -> PCFOL=),
843e19887f64dde75055cf8842fc4db2171eff45johnlev following Chap. III:3.1 of the CASL Reference Manual
843e19887f64dde75055cf8842fc4db2171eff45johnlev wenn es druch geht, dann in hets.hs einf�gen
843e19887f64dde75055cf8842fc4db2171eff45johnlev und dann einchecken, wenn es durch geht (make hets)
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab cvs commit
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab--import Test
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabimport qualified Common.Lib.Map as Map
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabimport qualified Common.Lib.Set as Set
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabimport qualified Common.Lib.Rel as Rel
843e19887f64dde75055cf8842fc4db2171eff45johnlevimport List (nub,delete)
843e19887f64dde75055cf8842fc4db2171eff45johnlev-- | The identity of the comorphism
843e19887f64dde75055cf8842fc4db2171eff45johnlevdata CASL2PCFOL = CASL2PCFOL deriving (Show)
843e19887f64dde75055cf8842fc4db2171eff45johnlevinstance Language CASL2PCFOL -- default definition is okay
843e19887f64dde75055cf8842fc4db2171eff45johnlevinstance Comorphism CASL2PCFOL
843e19887f64dde75055cf8842fc4db2171eff45johnlev CASL CASL_Sublogics
843e19887f64dde75055cf8842fc4db2171eff45johnlev CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
843e19887f64dde75055cf8842fc4db2171eff45johnlev Symbol RawSymbol ()
843e19887f64dde75055cf8842fc4db2171eff45johnlev CASL CASL_Sublogics
843e19887f64dde75055cf8842fc4db2171eff45johnlev CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
843e19887f64dde75055cf8842fc4db2171eff45johnlev Symbol RawSymbol () where
843e19887f64dde75055cf8842fc4db2171eff45johnlev sourceLogic CASL2PCFOL = CASL
843e19887f64dde75055cf8842fc4db2171eff45johnlev sourceSublogic CASL2PCFOL = CASL_SL
843e19887f64dde75055cf8842fc4db2171eff45johnlev { has_sub = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_part = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_cons = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_eq = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_pred = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev which_logic = FOL
843e19887f64dde75055cf8842fc4db2171eff45johnlev targetLogic CASL2PCFOL = CASL
843e19887f64dde75055cf8842fc4db2171eff45johnlev targetSublogic CASL2PCFOL = CASL_SL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab { has_sub = False, -- subsorting is coded out
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab has_part = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_cons = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_eq = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev has_pred = True,
843e19887f64dde75055cf8842fc4db2171eff45johnlev which_logic = FOL
843e19887f64dde75055cf8842fc4db2171eff45johnlev map_sign CASL2PCFOL sig = let e = encodeSig sig in Just (e, [])
843e19887f64dde75055cf8842fc4db2171eff45johnlev map_morphism CASL2PCFOL = Just . id
843e19887f64dde75055cf8842fc4db2171eff45johnlev map_sentence CASL2PCFOL sig = Just -- needs to be improved !
843e19887f64dde75055cf8842fc4db2171eff45johnlev map_symbol CASL2PCFOL = Set.single . id
843e19887f64dde75055cf8842fc4db2171eff45johnlev-- | Add injection, projection and membership symbols to a signature
843e19887f64dde75055cf8842fc4db2171eff45johnlevencodeSig :: Sign f e -> Sign f e
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabencodeSig sig = sig {sortRel=newsortRel,opMap=priopMap,predMap=newpredMap}
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab trivial=[(x,x)|x<-(fst(unzip(Rel.toList(sortRel sig))))++ snd(unzip(Rel.toList(sortRel sig)))]
5d2eda970e48f8985448151c73e699614ce9f357John Levon relList=Rel.toList(sortRel sig)++nub(trivial) --[(SORT,SORT)]
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab newsortRel=Rel.fromList(relList) --Rel SORT
843e19887f64dde75055cf8842fc4db2171eff45johnlev total (s, s') = OpType {opKind=Total,opArgs=[s],opRes=s'}
843e19887f64dde75055cf8842fc4db2171eff45johnlev partial (s, s') = OpType {opKind=Partial,opArgs=[s'],opRes=s}
5d2eda970e48f8985448151c73e699614ce9f357John Levon setinjOptype= Set.fromList(map total relList)
843e19887f64dde75055cf8842fc4db2171eff45johnlev setproOptype= Set.fromList (map partial relList)
843e19887f64dde75055cf8842fc4db2171eff45johnlev injopMap=Map.insert inj setinjOptype (opMap sig)
5d2eda970e48f8985448151c73e699614ce9f357John Levon priopMap=Map.insert pro setproOptype (injopMap)
843e19887f64dde75055cf8842fc4db2171eff45johnlev inj=mkId[mkSimpleId "_inj"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev pro=mkId[mkSimpleId "_proj"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev --(SORT,[SORT])->[(SORT,[SORT])]
843e19887f64dde75055cf8842fc4db2171eff45johnlev predList= nub(fst(unzip (relList)))
843e19887f64dde75055cf8842fc4db2171eff45johnlev udupredList=[(x,Set.toList(supersortsOf x sig))|x<-predList] --[(SORT,[SORT])]
843e19887f64dde75055cf8842fc4db2171eff45johnlev altpredMap=predMap sig
843e19887f64dde75055cf8842fc4db2171eff45johnlev newcomb (x,[])=[ ] --(SORT,[SORT])->[(SORT,[SORT])]
843e19887f64dde75055cf8842fc4db2171eff45johnlev newcomb (x,(y:ys))=(x,[y]):(newcomb (x,ys))
843e19887f64dde75055cf8842fc4db2171eff45johnlev pred x = PredType {predArgs=x} --[SORT]
843e19887f64dde75055cf8842fc4db2171eff45johnlev newpredMap = insertPred newLList altpredMap
843e19887f64dde75055cf8842fc4db2171eff45johnlev newLList=(concat(map newcomb udupredList)) --map (SORT,[SORT])->[(SORT,[SORT])] [(SORT,[SORT])] [[(SORT,[SORT])]]
843e19887f64dde75055cf8842fc4db2171eff45johnlev insertPred [ ] m = m
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab insertPred ((x,y):xs) m = insertPred (xs) (Map.insert (Id [mkSimpleId "_elem_"] [x] []) (Set.fromList[pred y]) m)
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabgenerateAxioms :: Sign f e -> [Named (FORMULA f)]
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rabgenerateAxioms sig =
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab ([inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sorts s < s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op inj : s->s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x,y:s . inj(x)=e=inj(y) => x=e=y %(ga_embedding_injectivity)% "++
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s< s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op pr : s'->?s ; inj:s->s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x:s . pr(inj(x))=e=x %(projection)% " ++
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s<s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op pr : s'->?s \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x,y:s'. pr(x)=e=pr(y)=>x=e=y %(projection_transitiv)% " ++
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op inj : s->s \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x:s . inj(x)=e=x %(indentity)%" ++
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s<s' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op pr : s' -> ?s \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x:s . x<=>def(pr(x)) %(mebership)%"
843e19887f64dde75055cf8842fc4db2171eff45johnlev | (s,s') <- rel2List])
843e19887f64dde75055cf8842fc4db2171eff45johnlev x = mkSimpleId "x"
843e19887f64dde75055cf8842fc4db2171eff45johnlev y = mkSimpleId "y"
843e19887f64dde75055cf8842fc4db2171eff45johnlev inj = mkId [mkSimpleId "_inj"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev pr=mkId [mkSimpleId "_pr"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev pr_trans=mkId [mkSimpleId "_pr_trans"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev indentity=mkId [mkSimpleId "_indentity"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev membership=mkId[mkSimpleId "_membership"]
843e19887f64dde75055cf8842fc4db2171eff45johnlev rel2Map=Rel.toMap(sortRel sig)
843e19887f64dde75055cf8842fc4db2171eff45johnlev --mapOp=Set.toList(opMap sig)
843e19887f64dde75055cf8842fc4db2171eff45johnlev rel2List=Rel.toList(sortRel sig)
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab [inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s<s';s'<s'' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op inj:s'->s'' ; inj: s->s' ; inj:s->s'' \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ forall x:s . inj(inj(x))=e=inj(x) %(transitive)% "
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab |(s,s')<-rel2List,s''<-Set.toList(supersortsOf s' sig)]++
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab [inlineAxioms CASL
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab " sort s'<s ; s''<s ; w'_i ; w''_i ; w_i; \
a576ab5b6e08c47732b3dedca9eaa8a8cbb85720rab \ op f:w'->s' ; f:w''->s'' ; inj: s' -> s ; inj: s''->s ; inj: s_i->s'_i ; inj:s_i -> s''_i \
843e19887f64dde75055cf8842fc4db2171eff45johnlev \ forall x_i : s_i . inj(f(inj(x_i)))=inj(f(inj(x_i))) \
843e19887f64dde75055cf8842fc4db2171eff45johnlev \ |(w,s,s',s'',w'_i,w''_i,f) | f<-mapOp,