content: {- |
  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
  