{- |

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 = mapSen mapTermExt

mapTermExt :: FplMor -> TermExt -> TermExt

mapTermExt m te = let rec = mapTerm mapTermExt m in case te of

FixDef fd -> FixDef $ mapFunDef m fd

Case o l r -> Case (rec o) (map (\ (p, t) -> (rec p, rec t)) l) r

Let fd t r -> Let (mapFunDef m fd) (rec t) r

IfThenElse f t e r -> IfThenElse (rec f) (rec t) (rec e) r

EqTerm t e r -> EqTerm (rec t) (rec e) r

BoolTerm t -> BoolTerm (rec t)

mapFunDef :: FplMor -> FunDef -> FunDef

mapFunDef m (FunDef i h@(Op_head k vs ms q) at r) =

let nvs = map (mapVars m) vs

nt = fmap (mapTerm mapTermExt m) at

in maybe (FunDef i (Op_head k nvs ms q) nt r)

(\ hty -> let

(j, ty) = mapOpSym (sort_map m) (op_map m) (i, toOpType hty)

in FunDef j (Op_head (opKind ty) nvs (fmap (mapSrt m) ms) q) nt r)

$ headToType h