{- |

Module : ./CASL/Project.hs

Description : replace casts with explicit projection functions

Copyright : (c) Christian Maeder, Uni Bremen 2005-2006

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

Replace casts with explicit projection functions

This module replaces Cast(s) with explicit projection

functions. Don't do this after simplification since crucial sort

information may be missing

Membership test are replaced with Definedness formulas

projection names may be also made unique by appending the source

and target sort

-}

module CASL.Project where

import CASL.AS_Basic_CASL

import CASL.Fold

import CASL.Inject

import CASL.Sign

import Common.Id

projRecord :: TermExtension f => OpKind -> (f -> f)

-> Record f (FORMULA f) (TERM f)

projRecord fk mf = (mapRecord mf)

{ foldCast = \ _ st s ps -> projectUnique fk ps st s

, foldMembership = \ _ t s ps -> Definedness (projectUnique fk ps t s) ps }

projTerm :: TermExtension f => OpKind -> (f -> f) -> TERM f -> TERM f

projTerm fk = foldTerm . projRecord fk

projFormula :: TermExtension f => OpKind -> (f -> f) -> FORMULA f -> FORMULA f

projFormula fk = foldFormula . projRecord fk

uniqueProjName :: OP_TYPE -> Id

uniqueProjName t = case t of

Op_type _ [from] to _ -> mkUniqueProjName from to

_ -> error "CASL.Project.uniqueProjName"

botTok :: Token

botTok = genToken "bottom"

uniqueBotName :: OP_TYPE -> Id

uniqueBotName t = case t of

Op_type _ [] to _ -> mkUniqueName botTok [to]

_ -> error "CASL.Project.uniqueBotName"

projectUnique :: TermExtension f => OpKind -> Range -> TERM f -> SORT -> TERM f

projectUnique = makeInjOrProj uniqueProjName