{- |
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 :: OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
projRecord fk :: OpKind
fk mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
  { foldCast :: TERM f -> TERM f -> SORT -> Range -> TERM f
foldCast = \ _ st :: TERM f
st s :: SORT
s ps :: Range
ps -> OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
fk Range
ps TERM f
st SORT
s
  , foldMembership :: FORMULA f -> TERM f -> SORT -> Range -> FORMULA f
foldMembership = \ _ t :: TERM f
t s :: SORT
s ps :: Range
ps -> TERM f -> Range -> FORMULA f
forall f. TERM f -> Range -> FORMULA f
Definedness (OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique OpKind
fk Range
ps TERM f
t SORT
s) Range
ps }

projTerm :: TermExtension f => OpKind -> (f -> f) -> TERM f -> TERM f
projTerm :: OpKind -> (f -> f) -> TERM f -> TERM f
projTerm fk :: OpKind
fk = Record f (FORMULA f) (TERM f) -> TERM f -> TERM f
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f (FORMULA f) (TERM f) -> TERM f -> TERM f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> TERM f
-> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f.
TermExtension f =>
OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
projRecord OpKind
fk

projFormula :: TermExtension f => OpKind -> (f -> f) -> FORMULA f -> FORMULA f
projFormula :: OpKind -> (f -> f) -> FORMULA f -> FORMULA f
projFormula fk :: OpKind
fk = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> ((f -> f) -> Record f (FORMULA f) (TERM f))
-> (f -> f)
-> FORMULA f
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f.
TermExtension f =>
OpKind -> (f -> f) -> Record f (FORMULA f) (TERM f)
projRecord OpKind
fk

uniqueProjName :: OP_TYPE -> Id
uniqueProjName :: OP_TYPE -> SORT
uniqueProjName t :: OP_TYPE
t = case OP_TYPE
t of
    Op_type _ [from :: SORT
from] to :: SORT
to _ -> SORT -> SORT -> SORT
mkUniqueProjName SORT
from SORT
to
    _ -> [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "CASL.Project.uniqueProjName"

botTok :: Token
botTok :: Token
botTok = [Char] -> Token
genToken "bottom"

uniqueBotName :: OP_TYPE -> Id
uniqueBotName :: OP_TYPE -> SORT
uniqueBotName t :: OP_TYPE
t = case OP_TYPE
t of
    Op_type _ [] to :: SORT
to _ -> Token -> [SORT] -> SORT
mkUniqueName Token
botTok [SORT
to]
    _ -> [Char] -> SORT
forall a. HasCallStack => [Char] -> a
error "CASL.Project.uniqueBotName"

projectUnique :: TermExtension f => OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique :: OpKind -> Range -> TERM f -> SORT -> TERM f
projectUnique = (OP_TYPE -> SORT) -> OpKind -> Range -> TERM f -> SORT -> TERM f
forall f.
TermExtension f =>
(OP_TYPE -> SORT) -> OpKind -> Range -> TERM f -> SORT -> TERM f
makeInjOrProj OP_TYPE -> SORT
uniqueProjName