{- |
Module      :  ./Fpl/Morphism.hs
Description :  morphism mapping for FPL
Copyright   :  (c) Christian Maeder, DFKI GmbH 2011
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable
-}

module Fpl.Morphism (FplMor, mapFplSen) where

import Fpl.As
import Fpl.Sign

import CASL.Sign
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.MapSentence

type FplMor = Morphism TermExt SignExt (DefMorExt SignExt)

mapFplSen :: FplMor -> FplForm -> FplForm
mapFplSen :: FplMor -> FplForm -> FplForm
mapFplSen = MapSen TermExt SignExt (DefMorExt SignExt)
-> FplMor -> FplForm -> FplForm
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen TermExt SignExt (DefMorExt SignExt)
mapTermExt

mapTermExt :: FplMor -> TermExt -> TermExt
mapTermExt :: MapSen TermExt SignExt (DefMorExt SignExt)
mapTermExt m :: FplMor
m te :: TermExt
te = let rec :: TERM TermExt -> TERM TermExt
rec = MapSen TermExt SignExt (DefMorExt SignExt)
-> FplMor -> TERM TermExt -> TERM TermExt
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen TermExt SignExt (DefMorExt SignExt)
mapTermExt FplMor
m in case TermExt
te of
    FixDef fd :: FunDef
fd -> FunDef -> TermExt
FixDef (FunDef -> TermExt) -> FunDef -> TermExt
forall a b. (a -> b) -> a -> b
$ FplMor -> FunDef -> FunDef
mapFunDef FplMor
m FunDef
fd
    Case o :: TERM TermExt
o l :: [(TERM TermExt, TERM TermExt)]
l r :: Range
r -> TERM TermExt -> [(TERM TermExt, TERM TermExt)] -> Range -> TermExt
Case (TERM TermExt -> TERM TermExt
rec TERM TermExt
o) (((TERM TermExt, TERM TermExt) -> (TERM TermExt, TERM TermExt))
-> [(TERM TermExt, TERM TermExt)] -> [(TERM TermExt, TERM TermExt)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (p :: TERM TermExt
p, t :: TERM TermExt
t) -> (TERM TermExt -> TERM TermExt
rec TERM TermExt
p, TERM TermExt -> TERM TermExt
rec TERM TermExt
t)) [(TERM TermExt, TERM TermExt)]
l) Range
r
    Let fd :: FunDef
fd t :: TERM TermExt
t r :: Range
r -> FunDef -> TERM TermExt -> Range -> TermExt
Let (FplMor -> FunDef -> FunDef
mapFunDef FplMor
m FunDef
fd) (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) Range
r
    IfThenElse f :: TERM TermExt
f t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> TERM TermExt -> Range -> TermExt
IfThenElse (TERM TermExt -> TERM TermExt
rec TERM TermExt
f) (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) (TERM TermExt -> TERM TermExt
rec TERM TermExt
e) Range
r
    EqTerm t :: TERM TermExt
t e :: TERM TermExt
e r :: Range
r -> TERM TermExt -> TERM TermExt -> Range -> TermExt
EqTerm (TERM TermExt -> TERM TermExt
rec TERM TermExt
t) (TERM TermExt -> TERM TermExt
rec TERM TermExt
e) Range
r
    BoolTerm t :: TERM TermExt
t -> TERM TermExt -> TermExt
BoolTerm (TERM TermExt -> TERM TermExt
rec TERM TermExt
t)

mapFunDef :: FplMor -> FunDef -> FunDef
mapFunDef :: FplMor -> FunDef -> FunDef
mapFunDef m :: FplMor
m (FunDef i :: OP_NAME
i h :: OP_HEAD
h@(Op_head k :: OpKind
k vs :: [VAR_DECL]
vs ms :: Maybe OP_NAME
ms q :: Range
q) at :: Annoted (TERM TermExt)
at r :: Range
r) =
   let nvs :: [VAR_DECL]
nvs = (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (FplMor -> VAR_DECL -> VAR_DECL
forall f e m. Morphism f e m -> VAR_DECL -> VAR_DECL
mapVars FplMor
m) [VAR_DECL]
vs
       nt :: Annoted (TERM TermExt)
nt = (TERM TermExt -> TERM TermExt)
-> Annoted (TERM TermExt) -> Annoted (TERM TermExt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MapSen TermExt SignExt (DefMorExt SignExt)
-> FplMor -> TERM TermExt -> TERM TermExt
forall f e m. MapSen f e m -> Morphism f e m -> TERM f -> TERM f
mapTerm MapSen TermExt SignExt (DefMorExt SignExt)
mapTermExt FplMor
m) Annoted (TERM TermExt)
at
   in FunDef -> (OP_TYPE -> FunDef) -> Maybe OP_TYPE -> FunDef
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (OP_NAME -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef OP_NAME
i (OpKind -> [VAR_DECL] -> Maybe OP_NAME -> Range -> OP_HEAD
Op_head OpKind
k [VAR_DECL]
nvs Maybe OP_NAME
ms Range
q) Annoted (TERM TermExt)
nt Range
r)
      (\ hty :: OP_TYPE
hty -> let
        (j :: OP_NAME
j, ty :: OpType
ty) = Sort_map -> Op_map -> (OP_NAME, OpType) -> (OP_NAME, OpType)
mapOpSym (FplMor -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map FplMor
m) (FplMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map FplMor
m) (OP_NAME
i, OP_TYPE -> OpType
toOpType OP_TYPE
hty)
        in OP_NAME -> OP_HEAD -> Annoted (TERM TermExt) -> Range -> FunDef
FunDef OP_NAME
j (OpKind -> [VAR_DECL] -> Maybe OP_NAME -> Range -> OP_HEAD
Op_head (OpType -> OpKind
opKind OpType
ty) [VAR_DECL]
nvs ((OP_NAME -> OP_NAME) -> Maybe OP_NAME -> Maybe OP_NAME
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FplMor -> OP_NAME -> OP_NAME
forall f e m. Morphism f e m -> OP_NAME -> OP_NAME
mapSrt FplMor
m) Maybe OP_NAME
ms) Range
q) Annoted (TERM TermExt)
nt Range
r)
      (Maybe OP_TYPE -> FunDef) -> Maybe OP_TYPE -> FunDef
forall a b. (a -> b) -> a -> b
$ OP_HEAD -> Maybe OP_TYPE
headToType OP_HEAD
h