{- |
Module      :  ./CASL/Inject.hs
Description :  Replace Sorted_term(s) with explicit injection functions.
Copyright   :  (c) Christian Maeder, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Replace Sorted_term(s) with explicit injection functions.  Don't do this after
   simplification since crucial sort information may be missing
 -}

module CASL.Inject where

import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Fold
import Common.Id

makeInjOrProj :: TermExtension f => (OP_TYPE -> Id) -> OpKind -> Range
  -> TERM f -> SORT -> TERM f
makeInjOrProj :: (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> Id -> TERM f
makeInjOrProj mkName :: OP_TYPE -> Id
mkName fk :: OpKind
fk pos :: Range
pos argument :: TERM f
argument to :: Id
to =
    let from :: Id
from = TERM f -> Id
forall f. TermExtension f => f -> Id
sortOfTerm TERM f
argument
        t :: OP_TYPE
t = OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
fk [Id
from] Id
to Range
pos
    in if Id
to Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
from then TERM f
argument else
    OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name (OP_TYPE -> Id
mkName OP_TYPE
t) OP_TYPE
t Range
pos) [TERM f
argument] Range
pos

injectUnique :: TermExtension f => Range -> TERM f -> SORT -> TERM f
injectUnique :: Range -> TERM f -> Id -> TERM f
injectUnique = (OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> Id -> TERM f
forall f.
TermExtension f =>
(OP_TYPE -> Id) -> OpKind -> Range -> TERM f -> Id -> TERM f
makeInjOrProj OP_TYPE -> Id
uniqueInjName OpKind
Total

uniqueInjName :: OP_TYPE -> Id
uniqueInjName :: OP_TYPE -> Id
uniqueInjName t :: OP_TYPE
t = case OP_TYPE
t of
    Op_type _ [from :: Id
from] to :: Id
to _ -> Id -> Id -> Id
mkUniqueInjName Id
from Id
to
    _ -> [Char] -> Id
forall a. HasCallStack => [Char] -> a
error "CASL.Inject.uniqueInjName"

injRecord :: TermExtension f => (f -> f) -> Record f (FORMULA f) (TERM f)
injRecord :: (f -> f) -> Record f (FORMULA f) (TERM f)
injRecord 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)
     { foldApplication :: TERM f -> OP_SYMB -> [TERM f] -> Range -> TERM f
foldApplication = \ _ o :: OP_SYMB
o ts :: [TERM f]
ts ps :: Range
ps -> case OP_SYMB
o of
         Qual_op_name _ ty :: OP_TYPE
ty _ -> OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application OP_SYMB
o
             ((TERM f -> Id -> TERM f) -> [TERM f] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Range -> TERM f -> Id -> TERM f
forall f. TermExtension f => Range -> TERM f -> Id -> TERM f
injectUnique Range
ps) [TERM f]
ts ([Id] -> [TERM f]) -> [Id] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> [Id]
args_OP_TYPE OP_TYPE
ty) Range
ps
         _ -> [Char] -> TERM f
forall a. HasCallStack => [Char] -> a
error "injApplication"
     , foldSorted_term :: TERM f -> TERM f -> Id -> Range -> TERM f
foldSorted_term = \ _ st :: TERM f
st s :: Id
s ps :: Range
ps -> Range -> TERM f -> Id -> TERM f
forall f. TermExtension f => Range -> TERM f -> Id -> TERM f
injectUnique Range
ps TERM f
st Id
s
     , foldPredication :: FORMULA f -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
foldPredication = \ _ p :: PRED_SYMB
p ts :: [TERM f]
ts ps :: Range
ps -> case PRED_SYMB
p of
         Qual_pred_name _ (Pred_type s :: [Id]
s _) _ -> PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
p
             ((TERM f -> Id -> TERM f) -> [TERM f] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Range -> TERM f -> Id -> TERM f
forall f. TermExtension f => Range -> TERM f -> Id -> TERM f
injectUnique Range
ps) [TERM f]
ts [Id]
s) Range
ps
         _ -> [Char] -> FORMULA f
forall a. HasCallStack => [Char] -> a
error "injPredication" }

injTerm :: TermExtension f => (f -> f) -> TERM f -> TERM f
injTerm :: (f -> f) -> TERM f -> TERM f
injTerm = 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
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f.
TermExtension f =>
(f -> f) -> Record f (FORMULA f) (TERM f)
injRecord

injFormula :: TermExtension f => (f -> f) -> FORMULA f -> FORMULA f
injFormula :: (f -> f) -> FORMULA f -> FORMULA f
injFormula = 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
. (f -> f) -> Record f (FORMULA f) (TERM f)
forall f.
TermExtension f =>
(f -> f) -> Record f (FORMULA f) (TERM f)
injRecord

{- | takes a list of OP_SYMB generated by
'CASL.AS_Basic_CASL.recover_Sort_gen_ax' and inserts these operations into
the signature; unqualified OP_SYMBs yield an error -}
insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e
insertInjOps :: Sign f e -> [OP_SYMB] -> Sign f e
insertInjOps = (Sign f e -> OP_SYMB -> Sign f e)
-> Sign f e -> [OP_SYMB] -> Sign f e
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Sign f e -> OP_SYMB -> Sign f e
forall f e. Sign f e -> OP_SYMB -> Sign f e
insOp
    where insOp :: Sign f e -> OP_SYMB -> Sign f e
insOp sign :: Sign f e
sign o :: OP_SYMB
o =
              case OP_SYMB
o of
              Qual_op_name i :: Id
i ot :: OP_TYPE
ot _
                  | Id -> Bool
isInjName Id
i ->
                       Sign f e
sign { opMap :: OpMap
opMap = Id -> OpType -> OpMap -> OpMap
addOpTo Id
i (OP_TYPE -> OpType
toOpType OP_TYPE
ot) (Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sign)}
                  | Bool
otherwise -> Sign f e
sign
              _ -> [Char] -> Sign f e
forall a. HasCallStack => [Char] -> a
error "CASL.Inject.insertInjOps: Wrong constructor."