Project.hs revision 2b33802ca26124644f4311db4319376ecffdc8d2
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : replace casts with explicit projection functions
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Christian Maeder, Uni Bremen 2005-2006
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : portable
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederReplace casts with explicit projection functions
c9a7e6af169a2adfb92f42331cd578065ed83a2bChristian MaederThis module replaces Cast(s) with explicit projection
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder functions. Don't do this after simplification since crucial sort
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder information may be missing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Membership test are replaced with Definedness formulas
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder projection names may be also made unique by appending the source
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich and target sort
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian MaederprojRecord :: OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian MaederprojRecord fk mf = (mapRecord mf)
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder { foldCast = \ _ st s ps -> projectUnique fk ps st s
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder , foldMembership = \ _ t s ps -> Definedness (projectUnique fk ps t s) ps }
e593b89bfd4952698dc37feced21cefe869d87a2Christian MaederprojTerm :: OpKind -> (f -> f) -> TERM f -> TERM f
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederprojTerm fk = foldTerm . projRecord fk
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian MaederprojFormula :: OpKind -> (f -> f) -> FORMULA f -> FORMULA f
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederprojFormula fk = foldFormula . projRecord fk
51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian MaederuniqueProjName :: OP_TYPE -> Id
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaederuniqueProjName t = case t of
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder Op_type _ [from] to _ -> mkUniqueProjName from to
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederbotTok :: Token
c3053d57f642ca507cdf79512e604437c4546cb9Christian MaederbotTok = genToken "bottom"
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederuniqueBotName :: OP_TYPE -> Id
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederuniqueBotName t = case t of
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Op_type _ [] to _ -> mkUniqueName botTok [to]
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaederprojectUnique :: OpKind -> Range -> TERM f -> SORT -> TERM f
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederprojectUnique = makeInjOrProj uniqueProjName