{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

{- |

Module : $Header$

Description : Coding CSMOF into CASL

Copyright : (c) Daniel Calegari Universidad de la Republica, Uruguay 2013

License : GPLv2 or higher, see LICENSE.txt

Maintainer : dcalegar@fing.edu.uy

Stability : provisional

Portability : portable

-}

module Comorphisms.CSMOF2CASL

( CSMOF2CASL (..)

) where

import Logic.Logic

import Logic.Comorphism

import Common.DefaultMorphism

-- CSMOF

import CSMOF.Logic_CSMOF as CSMOF

import CSMOF.As as CSMOFAs

import CSMOF.Sign as CSMOF

-- CASL

import CASL.Logic_CASL

import CASL.AS_Basic_CASL as C

import CASL.Sublogic

import CASL.Sign as C

import CASL.Morphism as C

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.Id

import Common.ProofTree

import Common.Result

import qualified Common.Lib.Rel as Rel

import qualified Common.Lib.MapSet as MapSet

import qualified Data.Set as Set

import qualified Data.Map as Map

-- | lid of the morphism

data CSMOF2CASL = CSMOF2CASL deriving Show

instance Language CSMOF2CASL -- default is ok

instance Comorphism CSMOF2CASL

CSMOF.CSMOF

()

CSMOFAs.Metamodel

CSMOF.Sen

()

()

CSMOF.Sign

CSMOF.Morphism

()

()

()

CASL

CASL_Sublogics

CASLBasicSpec

CASLFORMULA

SYMB_ITEMS

SYMB_MAP_ITEMS

CASLSign

CASLMor

C.Symbol

C.RawSymbol

ProofTree

where

sourceLogic CSMOF2CASL = CSMOF

sourceSublogic CSMOF2CASL = ()

targetLogic CSMOF2CASL = CASL

mapSublogic CSMOF2CASL _ = Just $ caslTop

{ has_part = False

, sub_features = LocFilSub

, cons_features = SortGen True True }

map_theory CSMOF2CASL = mapTheory

map_sentence CSMOF2CASL s = return . mapSen (mapSign s)

map_morphism CSMOF2CASL = mapMor

-- map_symbol CSMOF2CASL _ = Set.singleton . mapSym

is_model_transportable CSMOF2CASL = True

has_model_expansion CSMOF2CASL = True

is_weakly_amalgamable CSMOF2CASL = True

isInclusionComorphism CSMOF2CASL = True

mapTheory :: (CSMOF.Sign, [Named CSMOF.Sen]) -> Result (CASLSign, [Named CASLFORMULA])

mapTheory (s, ns) = let cs = mapSign s in

return (cs, map (mapNamed $ mapSen cs) ns ++ sentences cs)

mapSign :: CSMOF.Sign -> CASLSign

mapSign s =

let

sorts = getSorts (types s) (typeRel s)

ops = getOperations (instances s)

predd = getPredicates (properties s)

sent = getSentencesRels (links s) (instances s)

sentDisEmb = getSortGen (typeRel s) (abstractClasses s) (types s) (instances s)

noConfBetOps = getNoConfusionBetweenSets (instances s) (typeRel s)

in

C.Sign

{ sortRel = sorts

, revSortRel = Just $ Rel.fromList (map revertOrder (Rel.toList sorts))

, emptySortSet = Set.empty

, opMap = ops

, assocOps = MapSet.empty

, predMap = fst predd

, varMap = Map.empty

, sentences = snd predd ++ sent ++ sentDisEmb ++ noConfBetOps

, declaredSymbols = Set.empty

, envDiags = []

, annoMap = MapSet.empty

, globAnnos = emptyGlobalAnnos

, extendedInfo = ()

}

getSorts :: Set.Set TypeClass -> Rel.Rel TypeClass -> Rel.Rel SORT

getSorts setC relC =

let relS = Set.fold (insertSort . name) Rel.empty setC

in foldr (insertPair) relS (Rel.toList relC)

insertSort :: String -> Rel.Rel SORT -> Rel.Rel SORT

insertSort s relS = Rel.insertPair (stringToId s) (stringToId s) relS

insertPair :: (TypeClass,TypeClass) -> Rel.Rel SORT -> Rel.Rel SORT

insertPair (t1,t2) relS = Rel.insertPair (stringToId $ name t1) (stringToId $ name t2) relS

revertOrder :: (SORT,SORT) -> (SORT,SORT)

revertOrder (a,b) = (b,a)

getPredicates :: Set.Set PropertyT -> (PredMap,[Named (FORMULA f)])

getPredicates props = Set.fold (insertPredicate) (MapSet.empty,[]) props

insertPredicate :: PropertyT -> (PredMap,[Named (FORMULA f)]) -> (PredMap,[Named (FORMULA f)])

insertPredicate prop (predM,form) =

let

sort1 = stringToId $ name $ sourceType prop

sort2 = stringToId $ name $ targetType prop

pname1 = stringToId $ targetRole prop

ptype1 = PredType $ sort1 : [sort2]

pname2 = stringToId $ sourceRole prop

ptype2 = PredType $ sort2 : [sort1]

nam = "equiv_" ++ targetRole prop ++ "_" ++ sourceRole prop

varsD = [Var_decl [(mkSimpleId "x")] sort2 nullRange, Var_decl [(mkSimpleId "y")] sort1 nullRange]

sentRel = C.Relation

(C.Predication (C.Qual_pred_name pname2 (Pred_type [sort2,sort1] nullRange) nullRange)

(C.Qual_var (mkSimpleId "x") sort2 nullRange : [C.Qual_var (mkSimpleId "y") sort1 nullRange])

nullRange)

C.Equivalence

(C.Predication (C.Qual_pred_name pname1 (Pred_type [sort1,sort2] nullRange) nullRange)

(C.Qual_var (mkSimpleId "y") sort1 nullRange : [C.Qual_var (mkSimpleId "x") sort2 nullRange])

nullRange)

nullRange

sent = Quantification Universal varsD sentRel nullRange

in

-- MapSet does not allows repeated elements, but predicate names can be repeated

-- (this must be corrected by creating a more complex ID)

if sourceRole prop == "_"

then (MapSet.insert pname1 ptype1 predM, form)

else if targetRole prop == "_"

then (MapSet.insert pname2 ptype2 predM, form)

else (MapSet.insert pname1 ptype1 $ MapSet.insert pname2 ptype2 predM, (makeNamed nam sent) : form)

getOperations :: Map.Map String TypeClass -> OpMap

getOperations ops = foldr (insertOperations) MapSet.empty (Map.toList ops)

insertOperations :: (String,TypeClass) -> OpMap -> OpMap

insertOperations (na,tc) opM =

let

opName = stringToId na

opType = OpType Total [] (stringToId $ name tc)

in

MapSet.insert opName opType opM

getSentencesRels :: Set.Set LinkT -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

getSentencesRels linkk ops = completenessOfRelations linkk ops

completenessOfRelations :: Set.Set LinkT -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

completenessOfRelations linkk ops =

let ordLinks = getLinksByProperty linkk

in foldr ((++) . (createComplFormula ops)) [] (Map.toList ordLinks)

createComplFormula :: Map.Map String TypeClass -> (String,[LinkT]) -> [Named (CASLFORMULA)]

createComplFormula ops (nam,linksL) =

let

varA = mkSimpleId "x"

varB = mkSimpleId "y"

in

case linksL of

[] -> []

(LinkT _ _ pr) : _ -> let

sorA = stringToId $ name $ sourceType pr

sorB = stringToId $ name $ targetType pr

varsD = [Var_decl [varA] sorA nullRange, Var_decl [varB] sorB nullRange]

sent = C.Relation

(C.Predication (C.Qual_pred_name (stringToId $ targetRole pr) (Pred_type [sorA,sorB] nullRange) nullRange)

(C.Qual_var varA sorA nullRange

: [C.Qual_var varB sorB nullRange])

nullRange)

C.Equivalence

(Junction Dis (foldr ((:) . (getPropHold ops varA sorA varB sorB)) [] linksL) nullRange)

nullRange

sentQuan = Quantification Universal varsD sent nullRange

in

[makeNamed ("compRel_" ++ nam) sentQuan]

getPropHold :: Map.Map String TypeClass -> VAR -> SORT -> VAR -> SORT -> LinkT -> CASLFORMULA

getPropHold ops varA sorA varB sorB lin =

let

souObj = Map.lookup (sourceVar lin) ops

tarObj = Map.lookup (targetVar lin) ops

typSou = case souObj of

Nothing -> sourceVar lin -- if happens then is an error

Just tSou -> name tSou

typTar = case tarObj of

Nothing -> targetVar lin -- if happens then is an error

Just tTar -> name tTar

eqA = Equation (Qual_var varA sorA nullRange)

Strong

(Application (Qual_op_name (stringToId (sourceVar lin))

(Op_type Total [] (stringToId typSou) nullRange)

nullRange) [] nullRange)

nullRange

eqB = Equation (Qual_var varB sorB nullRange)

Strong

(Application (Qual_op_name (stringToId (targetVar lin))

(Op_type Total [] (stringToId typTar) nullRange)

nullRange) [] nullRange)

nullRange

in

Junction Con (eqA : [eqB]) nullRange

getLinksByProperty :: Set.Set LinkT -> Map.Map String [LinkT]

getLinksByProperty linkk =

let elems = Set.elems linkk

in foldr (getByProperty) Map.empty elems

getByProperty :: LinkT -> Map.Map String [LinkT] -> Map.Map String [LinkT]

getByProperty lin mapL =

let

prope = CSMOF.property lin

nameLook = sourceRole prope ++ name (sourceType prope) ++ targetRole prope ++ name (targetType prope)

setProp = Map.lookup nameLook mapL

in

case setProp of

Nothing -> Map.insert nameLook [lin] (Map.delete nameLook mapL)

Just s -> Map.insert nameLook (lin : s) (Map.delete nameLook mapL)

getSortGen :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

getSortGen typpR absCl typCl inst = disjointEmbedding absCl typpR ++ sortGeneration inst ++

sortGenerationNonAbstractSuperClasses typpR typCl absCl inst

-- free type de superclases que no son abstract

sortGenerationNonAbstractSuperClasses :: Rel.Rel TypeClass -> Set.Set TypeClass -> Set.Set TypeClass -> Map.Map String TypeClass -> [Named (CASLFORMULA)]

sortGenerationNonAbstractSuperClasses typpR typCl absCl inst =

let

ordObj = foldr (orderByClass) Map.empty (Map.toList inst)

nonAbsClasses = getNonAbstractClasess absCl typCl

nonAbsClassesWChilds = filter (\x -> not (null (snd x))) (Set.fold ((:) . (getSubClasses typpR)) [] nonAbsClasses)

childObjects = foldr ((:) . (getClassSubObjects ordObj)) [] nonAbsClassesWChilds -- [(TypeClass,[String])]

in

foldr ((:) . (toSortConstraintNonAbsClass inst)) [] childObjects

-- Takes the objects, and a class with its child classes and returns the descendent objects of such class

getClassSubObjects :: Map.Map TypeClass [String] -> (TypeClass,[TypeClass]) -> (TypeClass,[String])

getClassSubObjects objs (tc, subCl) =

let objTC = findObjectInMap objs tc

in

(tc, objTC ++ (foldr ((++) . (findObjectInMap objs)) [] subCl))

findObjectInMap :: Map.Map TypeClass [String] -> TypeClass -> [String]

findObjectInMap objs tc =

case Map.lookup tc objs of

Nothing -> []

Just objsTC -> objsTC

getNonAbstractClasess :: Set.Set TypeClass -> Set.Set TypeClass -> Set.Set TypeClass

getNonAbstractClasess absCl classes = Set.difference classes absCl

getSubClasses :: Rel.Rel TypeClass -> TypeClass -> (TypeClass,[TypeClass])

getSubClasses typpR tc =

let subCla = map (fst) (filter (isParent tc) (Rel.toList typpR))

rec = foldr ((++) . snd . (getSubClasses typpR)) [] subCla

in (tc, subCla ++ rec)

isParent :: TypeClass -> (TypeClass,TypeClass) -> Bool

isParent tc (_,tc2) = tc == tc2

toSortConstraintNonAbsClass :: Map.Map String TypeClass -> (TypeClass, [String]) -> Named (CASLFORMULA)

toSortConstraintNonAbsClass inst (tc,lisObj) =

let

sor = stringToId $ name tc

varA = Var_decl [(mkSimpleId "x")] sor nullRange

sent = Junction Dis (foldr ((:) . (getEqualityVarObject sor inst)) [] lisObj) nullRange

constr = Quantification Universal [varA] sent nullRange

in

makeNamed ("sortGenCon_" ++ name tc) constr

getEqualityVarObject :: SORT -> Map.Map String TypeClass -> String -> CASLFORMULA

getEqualityVarObject sor inst obj =

let oTyp = case Map.lookup obj inst of

Nothing -> stringToId obj -- If happens, there is an error

Just ob -> stringToId $ name ob

in

Equation (Qual_var (mkSimpleId "x") sor nullRange)

Strong

(Application (Qual_op_name (stringToId obj)

(Op_type Total [] oTyp nullRange)

nullRange) [] nullRange)

nullRange

-- Sorts are generated as a free type of object functions

sortGeneration :: Map.Map String TypeClass -> [Named (CASLFORMULA)]

sortGeneration inst =

let

ordObj = foldr (orderByClass) Map.empty (Map.toList inst)

noJunk = foldr ((:) . toSortConstraint) [] (Map.toList ordObj)

in

noJunk

mapFilterJust :: [Maybe a] -> [a]

mapFilterJust list =

case list of

[] -> []

a : rest -> case a of

Nothing -> mapFilterJust rest

Just el -> el : mapFilterJust rest

orderByClass :: (String,TypeClass) -> Map.Map TypeClass [String] -> Map.Map TypeClass [String]

orderByClass (ob,tc) mapTC =

case Map.lookup tc mapTC of

Nothing -> Map.insert tc [ob] mapTC

Just listObj -> Map.insert tc (ob : listObj) (Map.delete tc mapTC)

getNoConfusionBetweenSets :: Map.Map String TypeClass -> Rel.Rel TypeClass -> [Named (CASLFORMULA)]

getNoConfusionBetweenSets inst relC =

let ordObj = Map.toList $ foldr (orderByClass) Map.empty (Map.toList inst)

in mapFilterJust $ foldr ((:) . getNoConfusionBSetsAxiom ordObj relC) [] ordObj

getNoConfusionBSetsAxiom :: [(TypeClass, [String])] -> Rel.Rel TypeClass -> (TypeClass, [String]) -> Maybe (Named (CASLFORMULA))

getNoConfusionBSetsAxiom ordObj relC (tc,lisObj) =

case lisObj of

[] -> Nothing

_ : _ -> let

filteredObj = removeUntilType tc ordObj

diffForm = foldr ((++) . (diffOfRestConstants (tc,lisObj) relC)) [] filteredObj

in

case diffForm of

[] -> Nothing

_ : _ -> let constr = Junction Con diffForm nullRange

in Just $ makeNamed ("noConfusion_" ++ name tc) constr

removeUntilType :: TypeClass -> [(TypeClass, [String])] -> [(TypeClass, [String])]

removeUntilType tc lis =

case lis of

[] -> []

(tc2,lisObj2) : rest -> if tc == tc2

then (tc2,lisObj2) : rest

else removeUntilType tc rest

diffOfRestConstants :: (TypeClass, [String]) -> Rel.Rel TypeClass -> (TypeClass, [String]) -> [CASLFORMULA]

diffOfRestConstants (tc1,lisObj1) relC (tc2,lisObj2) =

case tc1 == tc2 of

True -> foldr ((++) . (diffOfRestOps tc1 lisObj1)) [] lisObj1

False -> case haveCommonSort tc1 tc2 relC of

True -> concat $ map (diffOfRestOpsDiffSort (tc1,lisObj1) tc2) lisObj2

False -> []

haveCommonSort :: TypeClass -> TypeClass -> Rel.Rel TypeClass -> Bool

haveCommonSort t1 t2 relT =

let succT1 = superSorts relT t1

succT2 = superSorts relT t2

in not $ Set.null $ Set.intersection succT1 succT2

-- This is the non exported function reachable in Rel

superSorts :: Rel.Rel TypeClass -> TypeClass -> Set.Set TypeClass

superSorts relT tc = Set.fold reach Set.empty $ Rel.succs relT tc where

reach e s = if Set.member e s then s

else Set.fold reach (Set.insert e s) $ Rel.succs relT e

diffOfRestOpsDiffSort :: (TypeClass, [String]) -> TypeClass -> String -> [CASLFORMULA]

diffOfRestOpsDiffSort (tc1,lisObj1) tc2 objName = concat $ map (diffOpsDiffSorts tc2 objName tc1) lisObj1

diffOpsDiffSorts :: TypeClass -> String -> TypeClass -> String -> [CASLFORMULA]

diffOpsDiffSorts tc2 objName2 tc1 objName1 = [Negation (Equation

(Application (Qual_op_name (stringToId objName1)

(Op_type Total [] (stringToId $ name tc1) nullRange)

nullRange)

[] nullRange)

Strong

(Application (Qual_op_name (stringToId objName2)

(Op_type Total [] (stringToId $ name tc2) nullRange)

nullRange)

[] nullRange)

nullRange)

nullRange]

diffOfRestOps :: TypeClass -> [String] -> String -> [CASLFORMULA]

diffOfRestOps tc lisObj objName =

let lis = removeUntil lisObj objName

in concat $ map (diffOps tc objName) lis

removeUntil :: [String] -> String -> [String]

removeUntil lis str =

case lis of

[] -> []

a : rest -> if a == str

then rest

else removeUntil rest str

diffOps :: TypeClass -> String -> String -> [CASLFORMULA]

diffOps tc objName1 objName2 =

if not (objName1 == objName2)

then [Negation (Equation

(Application (Qual_op_name (stringToId objName1)

(Op_type Total [] (stringToId $ name tc) nullRange)

nullRange) [] nullRange)

Strong

(Application (Qual_op_name (stringToId objName2)

(Op_type Total [] (stringToId $ name tc) nullRange)

nullRange) [] nullRange)

nullRange)

nullRange]

else []

toSortConstraint :: (TypeClass, [String]) -> Named (CASLFORMULA)

toSortConstraint (tc,lisObj) =

let

sor = stringToId $ name tc

simplCon = Constraint sor (foldr ((:) . toConstraint sor) [] lisObj) sor

constr = Sort_gen_ax [simplCon] True

in

makeNamed ("sortGenCon_" ++ name tc) constr

toConstraint :: Id -> String -> (OP_SYMB, [Int])

toConstraint sor obName =

let obj = stringToId obName

in

(Qual_op_name obj (Op_type Total [] sor nullRange) nullRange,[])

-- Each abstract class is the disjoint embedding of it subsorts

disjointEmbedding :: Set.Set TypeClass -> Rel.Rel TypeClass -> [Named (CASLFORMULA)]

disjointEmbedding absCl rel =

let

injSyms = map (\ (s, t) -> (Qual_op_name (mkUniqueInjName (stringToId $ name s) (stringToId $ name t))

(Op_type Total [(stringToId $ name s)] (stringToId $ name t) nullRange) nullRange,[]))

$ Rel.toList

$ Rel.irreflex rel

resType _ ((Op_name _),_) = False

resType s ((Qual_op_name _ t _),_) = res_OP_TYPE t == s

collectOps s = Constraint (stringToId $ name s) (filter (resType (stringToId $ name s)) injSyms) (stringToId $ name s)

sortList = Set.toList absCl

constrs = map collectOps sortList

in

[makeNamed "disjEmbedd" (Sort_gen_ax constrs True)]

mapSen :: CASLSign -> CSMOF.Sen -> CASLFORMULA

mapSen sig (Sen con car cot) = -- trueForm

case cot of

EQUAL -> let

minC = minConstraint con car (predMap sig)

maxC = maxConstraint con car (predMap sig)

in

Junction Con (minC : [maxC]) nullRange

LEQ -> maxConstraint con car (predMap sig)

GEQ -> minConstraint con car (predMap sig)

minConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA

minConstraint con int predM =

let

predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType

souVars = generateVars "x" 1

tarVars = generateVars "y" int

correctPredType = Set.fold (getCorrectPredType con) [] predTypes

souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange

tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange

in

if int > 1

then Quantification Universal [souVarDec] (Quantification

Existential

[tarVarDec]

(Junction Con ((generateVarDiff tarVarDec) :

[(generateProp souVarDec tarVarDec (stringToId $ getRole con))]) nullRange)

nullRange)

nullRange

else Quantification Universal [souVarDec] (Quantification

Existential

[tarVarDec]

(generateProp souVarDec tarVarDec (stringToId $ getRole con))

nullRange

) nullRange

getCorrectPredType :: MultConstr -> PredType -> [PredType] -> [PredType]

getCorrectPredType con pt ptLis =

case (stringToId $ name (CSMOF.getType con)) == head (predArgs pt) of

True -> pt : ptLis

False -> ptLis

generateVars :: String -> Integer -> [VAR]

generateVars varRoot int =

case int of

1 -> [mkSimpleId (varRoot ++ "_" ++ show int)]

n -> mkSimpleId (varRoot ++ "_" ++ show int) : generateVars varRoot (n-1)

generateVarDiff :: VAR_DECL -> CASLFORMULA

generateVarDiff (Var_decl vars sor _) = Junction Con (foldr ((++) . diffOfRest sor vars) [] vars) nullRange

diffOfRest :: SORT -> [VAR] -> VAR -> [CASLFORMULA]

diffOfRest sor vars var = map (diffVar sor var) vars

diffVar :: SORT -> VAR -> VAR -> CASLFORMULA

diffVar sor var1 var2 =

if not (var1 == var2)

then Negation (Equation

(Qual_var var1 sor nullRange)

Strong

(Qual_var var2 sor nullRange)

nullRange)

nullRange

else trueForm

generateProp :: VAR_DECL -> VAR_DECL -> Id -> CASLFORMULA

generateProp (Var_decl varD sort _) (Var_decl varD2 sort2 _) rol =

Junction Con (map (createPropRel (head varD) sort rol sort2) varD2) nullRange

createPropRel :: VAR -> SORT -> Id -> SORT -> VAR -> CASLFORMULA

createPropRel souVar sor rol sor2 tarVar =

Predication (C.Qual_pred_name rol (Pred_type [sor,sor2] nullRange) nullRange)

((Qual_var souVar sor nullRange):[Qual_var tarVar sor2 nullRange]) nullRange

maxConstraint :: MultConstr -> Integer -> PredMap -> CASLFORMULA

maxConstraint con int predM =

let

predTypes = MapSet.lookup (stringToId $ getRole con) predM -- Set PredType

souVars = generateVars "x" 1

tarVars = generateVars "y" (int + 1)

correctPredType = Set.fold (getCorrectPredType con) [] predTypes

souVarDec = Var_decl souVars (head (predArgs (head correctPredType))) nullRange

tarVarDec = Var_decl tarVars (last (predArgs (head correctPredType))) nullRange

in

Quantification Universal (souVarDec : [tarVarDec])

(Relation

(Junction Con [generateProp souVarDec tarVarDec (stringToId $ getRole con)] nullRange)

Implication

(Junction Dis (generateExEqual tarVarDec) nullRange)

nullRange)

nullRange

generateExEqual :: VAR_DECL -> [CASLFORMULA]

generateExEqual (Var_decl varD sor _) = generateExEqualList varD sor

generateExEqualList :: [VAR] -> SORT -> [CASLFORMULA]

generateExEqualList vars sor =

case vars of

[] -> []

v : rest -> (generateExEqualVar rest sor v) ++ (generateExEqualList rest sor)

generateExEqualVar :: [VAR] -> SORT -> VAR -> [CASLFORMULA]

generateExEqualVar vars sor var =

foldr ((++) . (\el -> if el == var

then []

else [Equation (Qual_var var sor nullRange) Strong (Qual_var el sor nullRange) nullRange]))

[] vars

-- | Translation of morphisms

mapMor :: CSMOF.Morphism -> Result CASLMor

mapMor m = return C.Morphism

{ msource = mapSign $ domOfDefaultMorphism m

, mtarget = mapSign $ codOfDefaultMorphism m

, sort_map = Map.empty

, op_map = Map.empty

, pred_map = Map.empty

, extended_map = ()

}

-- mapSym :: CSMOF.Symbol -> C.Symbol