57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- |

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyModule : $Header$

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyDescription : embedding from CASL to VSE, plus wrapping procedures

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly with default implementations

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyCopyright : (c) M.Codescu, DFKI Bremen 2008

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyMaintainer : Mihai.Codescu@dfki.de

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyStability : provisional

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'ReillyPortability : non-portable (imports Logic.Logic)

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly

33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyThe embedding comorphism from CASL to VSE.

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly-}

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillymodule Comorphisms.CASL2VSEImport (CASL2VSEImport(..)) where

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maederimport Logic.Logic

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maederimport Logic.Comorphism

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly

56899f6457976a2ee20f6a23f088cb5655b15715Liam O'Reillyimport CASL.Logic_CASL

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CASL.Sublogic as SL

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport CASL.Sign

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyimport CASL.AS_Basic_CASL

648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport CASL.Morphism

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport VSE.Logic_VSE

648fe1220044aac847acbdfbc4155af5556063ebChristian Maederimport VSE.As

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maederimport VSE.Ana

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly

c0833539c8cf577dd3f2497792fbdd818442744cChristian Maederimport Common.AS_Annotation

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Common.Id

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Common.ProofTree

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederimport Common.Result

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly

fa373bc327620e08861294716b4454be8d25669fChristian Maederimport qualified Data.Set as Set

036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maederimport qualified Data.Map as Map

fa373bc327620e08861294716b4454be8d25669fChristian Maeder

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder-- | The identity of the comorphism

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillydata CASL2VSEImport = CASL2VSEImport deriving (Show)

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reillyinstance Language CASL2VSEImport -- default definition is okay

53bd0c89aa4743dc41a6394db5a90717c1ca4517Liam O'Reilly

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyinstance Comorphism CASL2VSEImport

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly CASL CASL_Sublogics

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CASLSign

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder CASLMor

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Symbol RawSymbol ProofTree

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder VSE ()

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder VSESign

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder VSEMor

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Symbol RawSymbol () where

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sourceLogic CASL2VSEImport = CASL

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sourceSublogic CASL2VSEImport = SL.cFol

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder targetLogic CASL2VSEImport = VSE

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder mapSublogic CASL2VSEImport _ = Just ()

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder map_theory CASL2VSEImport = mapCASLTheory

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder map_morphism CASL2VSEImport = return . mapMor

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly map_sentence CASL2VSEImport _ = return . toSen

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly map_symbol CASL2VSEImport = error "nyi"

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly -- check these 3, but should be fine

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder has_model_expansion CASL2VSEImport = True

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder is_weakly_amalgamable CASL2VSEImport = True

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder isInclusionComorphism CASL2VSEImport = True

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder

648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapCASLTheory :: (CASLSign, [Named CASLFORMULA]) ->

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Result (VSESign, [Named Sentence])

33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymapCASLTheory (sig, n_sens) = do

fa373bc327620e08861294716b4454be8d25669fChristian Maeder let (tsig, genAx) = mapSig sig

fa373bc327620e08861294716b4454be8d25669fChristian Maeder tsens = map mapNamedSen n_sens

fa373bc327620e08861294716b4454be8d25669fChristian Maeder case not $ null $ checkCases tsig (tsens ++ genAx) of

fa373bc327620e08861294716b4454be8d25669fChristian Maeder True -> fail "case error in signature"

fa373bc327620e08861294716b4454be8d25669fChristian Maeder _ -> return (tsig, tsens ++ genAx)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder

fa373bc327620e08861294716b4454be8d25669fChristian MaedermkIfProg :: FORMULA () -> Program

fa373bc327620e08861294716b4454be8d25669fChristian MaedermkIfProg f =

fa373bc327620e08861294716b4454be8d25669fChristian Maeder mkRanged $ If f (mkRanged $ Return aTrue) $ mkRanged $ Return aFalse

fa373bc327620e08861294716b4454be8d25669fChristian Maeder

fa373bc327620e08861294716b4454be8d25669fChristian MaedermapSig :: CASLSign -> (VSESign, [Named Sentence])

648fe1220044aac847acbdfbc4155af5556063ebChristian MaedermapSig sign =

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder let wrapSort (procsym, axs) s = let

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder restrName = genName $ "restr_" ++ show s

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder eqName = genName $ "eq_" ++ show s

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder sProcs = [(restrName, Profile [Procparam In s] Nothing),

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (eqName,

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly Profile [Procparam In s, Procparam In s]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Just uBoolean))]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder sSens = [makeNamed ("ga_restriction_" ++ show s) $ ExtFORMULA $

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder mkRanged

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Defprocs

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [Defproc Proc restrName [genToken "x"]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (mkRanged (Block [] (mkRanged Skip)))

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange])

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ,makeNamed ("ga_equality_" ++ show s) $ ExtFORMULA $

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder mkRanged

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Defprocs

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [Defproc Func eqName (map mkSimpleId ["x","y"])

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (mkRanged (Block [] (mkIfProg (Strong_equation

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Qual_var (mkSimpleId "x") s nullRange)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Qual_var (mkSimpleId "y") s nullRange)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange))))

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder nullRange])

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ]

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (sProcs ++ procsym, sSens ++ axs)

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (sortProcs, sortSens) = foldl wrapSort ([],[]) $

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Set.toList $ sortSet sign

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder wrapOp (procsym, axs) (i, opTypeSet) = let

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder funName = mkGenName i

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder opTypes = Set.toList opTypeSet

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder fProcs = map (\profile ->

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (funName,

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Profile

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (map (Procparam In) $ opArgs profile)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Just $ opRes profile))) opTypes

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder fSens = map (\ (OpType fKind w s) -> let

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder vars = map (\(t,n) -> (genToken ("x" ++ (show n)), t)) $

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder zip w [1::Int ..]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder makeNamed "" $ ExtFORMULA $ Ranged

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Defprocs

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder [Defproc

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Func funName (map fst vars)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ( Ranged (Block []

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (Ranged

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (Block

d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder [Var_decl [genToken "y"] s nullRange]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Ranged

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Seq

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Ranged

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Assign

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (genToken "y")

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Application

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (Qual_op_name i

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (Op_type fKind w s nullRange)

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder nullRange )

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (map (\(v,ss) ->

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder Qual_var v ss nullRange) vars)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange))

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder nullRange)

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (Ranged

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder (Return

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (Qual_var (genToken "y") s nullRange))

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange)

7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder )--end seq

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder )--end block

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange)-- end procedure body

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder ) nullRange)

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder nullRange]

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder )

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly nullRange

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly ) opTypes

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder in

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder (procsym ++ fProcs, axs ++ fSens)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (opProcs, opSens) = foldl wrapOp ([],[]) $

fa373bc327620e08861294716b4454be8d25669fChristian Maeder Map.toList $ opMap sign

fa373bc327620e08861294716b4454be8d25669fChristian Maeder wrapPred (procsym, axs) (i, predTypeSet) = let

fa373bc327620e08861294716b4454be8d25669fChristian Maeder predTypes = Set.toList predTypeSet

fa373bc327620e08861294716b4454be8d25669fChristian Maeder procName = mkGenName i

fa373bc327620e08861294716b4454be8d25669fChristian Maeder pProcs = map (\profile -> (procName,

fa373bc327620e08861294716b4454be8d25669fChristian Maeder Profile

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (map (Procparam In) $ predArgs profile)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Just $ uBoolean))) predTypes

fa373bc327620e08861294716b4454be8d25669fChristian Maeder pSens = map (\ (PredType w) -> let

fa373bc327620e08861294716b4454be8d25669fChristian Maeder vars = map (\(t,n) -> (genToken ("x" ++ (show n)), t)) $

fa373bc327620e08861294716b4454be8d25669fChristian Maeder zip w [1::Int ..]

fa373bc327620e08861294716b4454be8d25669fChristian Maeder in

fa373bc327620e08861294716b4454be8d25669fChristian Maeder makeNamed "" $ ExtFORMULA $ mkRanged

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Defprocs

fa373bc327620e08861294716b4454be8d25669fChristian Maeder [Defproc

fa373bc327620e08861294716b4454be8d25669fChristian Maeder Func procName (map fst vars)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (mkRanged (Block [] (mkIfProg

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Predication

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Qual_pred_name

fa373bc327620e08861294716b4454be8d25669fChristian Maeder i

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (Pred_type

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (map snd vars)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder nullRange)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder nullRange)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (map (\(v,ss) ->

fa373bc327620e08861294716b4454be8d25669fChristian Maeder Qual_var v ss nullRange) vars)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder nullRange))))

fa373bc327620e08861294716b4454be8d25669fChristian Maeder nullRange]

fa373bc327620e08861294716b4454be8d25669fChristian Maeder )

fa373bc327620e08861294716b4454be8d25669fChristian Maeder ) predTypes

fa373bc327620e08861294716b4454be8d25669fChristian Maeder in

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (procsym ++ pProcs, axs ++ pSens)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder (predProcs, predSens) = foldl wrapPred ([],[]) $

fa373bc327620e08861294716b4454be8d25669fChristian Maeder Map.toList $ predMap sign

fa373bc327620e08861294716b4454be8d25669fChristian Maeder procs = Procs $ Map.fromList (sortProcs ++ opProcs ++ predProcs)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder newPreds = procsToPredMap procs

fa373bc327620e08861294716b4454be8d25669fChristian Maeder newOps = procsToOpMap procs

fa373bc327620e08861294716b4454be8d25669fChristian Maeder in(sign { opMap = addOpMapSet (opMap sign) newOps,

fa373bc327620e08861294716b4454be8d25669fChristian Maeder predMap = addMapSet (predMap sign) newPreds,

fa373bc327620e08861294716b4454be8d25669fChristian Maeder extendedInfo = procs,

fa373bc327620e08861294716b4454be8d25669fChristian Maeder sentences = [] }, sortSens ++ opSens ++ predSens)

fa373bc327620e08861294716b4454be8d25669fChristian Maeder

fa373bc327620e08861294716b4454be8d25669fChristian MaedermapNamedSen :: Named CASLFORMULA -> Named Sentence

fa373bc327620e08861294716b4454be8d25669fChristian MaedermapNamedSen = mapNamed toSen

fa373bc327620e08861294716b4454be8d25669fChristian Maeder

fa373bc327620e08861294716b4454be8d25669fChristian MaedermapMor :: CASLMor -> VSEMor

56899f6457976a2ee20f6a23f088cb5655b15715Liam O'ReillymapMor m = let

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder renSorts = Map.keys $ sort_map m

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder eqOps = Map.fromList $ map

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (\s -> ((genName $ "eq_" ++ show s,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder OpType Partial [s,s] (uBoolean)) ,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (genName $ "eq_" ++

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (show $ (sort_map m) Map.!s ),

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Partial )

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ))

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder renSorts

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder restrPreds = Map.fromList $ concatMap

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (\s -> [(

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (genName $ "restr_" ++ show s,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder PredType [s,s]),

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder genName $ "restr_" ++

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder show ((sort_map m) Map.!s)),

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (genName $ "uniform_" ++ show s,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder PredType [s,s]),

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder genName $ "uniform_" ++

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder show ((sort_map m) Map.!s))

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ]

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder )

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly renSorts

ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder renOps = Map.keys $ fun_map m

ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder opsProcs = Map.fromList $

ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder map (\ (idN, oT@(OpType _ w s)) -> let

ace03c3051e5c5144e43ae78cae73f6a29dde6d5Christian Maeder (idN', _) = (fun_map m) Map.! (idN, oT)

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder in

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ((mkGenName idN,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder OpType Partial w s) ,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (mkGenName idN',

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder Partial)

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly )

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly )

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly renOps

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly renPreds = Map.keys $ pred_map m

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly predProcs = Map.fromList $

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder map (\ (idN, pT@(PredType w)) -> let

8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder idN' = (pred_map m) Map.! (idN, pT)

8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder in

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder ((mkGenName idN,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder PredType w) ,

7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder mkGenName idN'

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly )

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly )

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly renPreds

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly (sig1,_) = mapSig $ msource m

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (sig2,_) = mapSig $ mtarget m

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly in

57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder m

57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder { msource = sig1

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , mtarget = sig2

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , fun_map = Map.union (Map.union eqOps opsProcs) $ fun_map m

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , pred_map = Map.union (Map.union restrPreds predProcs) $ pred_map m

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , extended_map = emptyMorExt

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly }

648fe1220044aac847acbdfbc4155af5556063ebChristian Maeder