-- unused but may be used
-- | \"alias\" for 'defaultHetcatsOpts' (for export)
-- | Cast Signature to CASLSignature if possible
getCASLSign :: G_sign -> Maybe CASLSign
getCASLSign (G_sign lid sign _) = do
ExtSign caslSign _ <- coerceSign lid CASL "getCASLSign" sign
-- | like a typed /fromMaybe/
getJustCASLSign :: Maybe CASLSign -> CASLSign
getJustCASLSign = maybe (error "getJustCASLSign") id
-- will fail if not possible
coerceMorphism (targetLogic cid) CASL "getCASLMorphLL" morph
-- | This datatype represents /something/ that has an origin.
data WithOrigin a b = WithOrigin { woItem::a, woOrigin::b }
-- | 'WithOrigin' specialized to '
Graph.Node' as type of origin.
-- | 'Eq' instance for 'WithOrigin'
-- Two 'WithOrigin'-objects are equal if their origins are equal and
-- their wrapped elements are equal.
instance (Eq a, Eq b)=>Eq (WithOrigin a b) where
wo1 == wo2 = woOrigin wo1 == woOrigin wo2 && woItem wo1 == woItem wo2
-- | 'Ord' instance for 'WithOrigin'
-- 'WithOrigin'-objects are ordered by their wrapped elements unless they are
-- equal. In that case they are ordered by their origin.
instance (Eq a, Ord b, Ord a)=>Ord (WithOrigin a b) where
icmp = compare (woItem wo1) (woItem wo2)
if icmp == EQ then compare (woOrigin wo1) (woOrigin wo2) else icmp
instance (Show a, Show b)=>Show (WithOrigin a b) where
show wo = (show (woItem wo)) ++ " Origin:(" ++ (show (woOrigin wo)) ++ ")"
-- | extract wrapped element from 'WithOrigin'
wonItem::WithOriginNode a->a
-- | extract origin from 'WithOrigin'
-- | create an element with origin where the origin is a '
Graph.Node'
-- | get CASL-formulas from a node
getNodeSentences::DGNodeLab->[
Ann.Named CASLFORMULA]
getNodeSentences node = if isDGRef node then [] else
maybe (error "getNodeSentences") id $ do
G_theory lid _ _ thsens _ <- return $ dgn_theory node
-- | create a mapping over all nodes of a DevGraph
-- where a checker function is provided to filter out
DGraph -- ^ DevGraph to use
->(a->Bool) -- ^ checker function, to determine of the
-- result of the mapping function is to be kept
getNodeDGNameMappingWO dg mapper dispose =
foldl (\mapping (n,node) ->
Map.insert (mkWON (dgn_name node) n) mapped mapping
-- added Integer to keep the order of imports (to OMDoc, from OMDoc)
type Imports =
Set.Set (Int, (String, HidingAndRequationList, Bool))
-- | node names with origin (node number)
type NodeNameWO = WithOriginNode NodeName
type SORTWO = WithOriginNode SORT
type IdWO = WithOriginNode Id
type SentenceWO = WithOriginNode (
Ann.Named CASLFORMULA)
-- | map of predicate ids with origin to
-- | map of operator ids with origin to
-- | map of 'Imports' (for theories)
type ImportsMap =
Map.Map String Imports
-- | map of node names with origin to their sorts with origin
type SortsMapDGWO =
Map.Map NodeNameWO SortsWO
-- | map of node names with origin to their predicates with origin
type PredsMapDGWO =
Map.Map NodeNameWO PredsWO
-- | map of node names with origin to their operators with origin
type OpsMapDGWO =
Map.Map NodeNameWO OpsWO
-- | Emptyness test for morphisms.
-- Tests for emptyness of sort- function- and predicate-map.
isEmptyMorphism:: Morphism a b c ->Bool
-- | return an empty 'CASLSign'
emptyCASLSign = emptySign ()
-- | abstract symbol requations (theory, name) -> (theory, name)
type RequationList = [ ( (String, String), (String, String) ) ]
-- | abstract symbol requations and a list of hidden symbols
type HidingAndRequationList = ([String], RequationList)
-- | test if there are no requations (but maybe hiding)
isEmptyHidAndReqL::HidingAndRequationList->Bool
isEmptyHidAndReqL (_, l) = null l
-- | test if there is no hiding (but maybe requations)
isNonHidingHidAndReqL::HidingAndRequationList->Bool
isNonHidingHidAndReqL (h, _) = null h
-- | Instance of 'Read' for 'Id'S
(tokens, rest) = spanEsc (not . (flip elem "[]")) s
tokenl = breakIfNonEsc "," tokens
token = map (\str -> Token (trimString $ unesc str) nullRange) tokenl
idl = breakIfNonEsc "," rest
ids = foldl (\ids' str ->
case ((readsPrec 0 (trimString str))::[(Id, String)]) of
[] -> error ("Unable to parse \"" ++ str ++ "\"")
((newid,_):_) -> ids' ++ [newid]
case (trimString rest) of
(']':_) -> [(Id token [] nullRange, "")]
_ -> [(Id token ids nullRange, "")]
-- | escapes special characters. used in 'idToString'.
escapeForId::String->String
escapeForId ('\\':r) = "\\\\" ++ escapeForId r
escapeForId ('[':r) = "\\[" ++ escapeForId r
escapeForId (']':r) = "\\]" ++ escapeForId r
escapeForId (',':r) = "\\," ++ escapeForId r
escapeForId (' ':r) = "\\ " ++ escapeForId r
escapeForId (c:r) = c:escapeForId r
-- | creates a parseable representation of an 'Id' (see Read-instance)
idToString (Id toks ids _) =
(implode "," (map (\t -> escapeForId $ tokStr t) toks)) ++
(implode "," (map idToString ids)) ++
-- | encapsulates a node_name in an id
nodeNameToId::NodeName->Id
nodeNameToId (NodeName s e n) =
mkId [s, mkSimpleId e, mkSimpleId (show n)]
-- | reads back an encapsulated node_name
idToNodeName::Id->NodeName
idToNodeName (Id toks _ _) = case toks of
t0 : t1 : t2 : _ -> NodeName t0 (show t1) $ read $ show t2
_ -> error "idToNodeName"
-- | This type is used for constructing unique names for
-- use in OMDoc-Documents.
-- Essential it provides a mapping for a single theory (node) but
-- these are constructed for a full library environment.
,
Set.Set ((Id, OpType, Maybe (Int, Id)), String)
instance Show IdNameMapping where
show (ln, nn, nsn, nnum, sorts, preds, ops, sens, cons) =
"(" ++ show ln ++ ", " ++ show nn ++ ", " ++ show nsn ++ ", "
++ show nnum ++ ", " ++ show sorts ++ ", " ++ show preds ++ ", "
++ show ops ++ ", " ++ show sens ++ ", " ++ show cons ++ ")"
-- | projection function for library name
inmGetLibName::IdNameMapping->LIB_NAME
inmGetLibName (ln, _, _, _, _, _, _, _, _) = ln
-- | projection function for node name
inmGetNodeName::IdNameMapping->NodeName
inmGetNodeName (_, nn, _, _, _, _, _, _, _) = nn
-- | projection function for XML node name (theory name)
inmGetNodeId::IdNameMapping->String
inmGetNodeId (_, _, id', _, _, _, _, _, _) = id'
-- | projection function for node (number)
inmGetNodeNum (_, _, _, nn, _, _, _, _, _) = nn
-- | projection function for the set of sorts
inmGetIdNameSortSet::IdNameMapping->
Set.Set (Id, String)
inmGetIdNameSortSet (_, _, _, _, s, _, _, _, _) = s
-- | projection function for the disambiguated set of predicates
inmGetIdNamePredSet::IdNameMapping->
Set.Set ((Id, PredType), String)
inmGetIdNamePredSet (_, _, _, _, _, s, _, _, _) = s
-- | projection function for the disambiguated set of operators
inmGetIdNameOpSet::IdNameMapping->
Set.Set ((Id, OpType), String)
inmGetIdNameOpSet (_, _, _, _, _, _, s, _, _) =
Set.map (\((i, t, _), u) -> ((i, t), u)) s
-- | projection function for the sentences (annotated by their appearance)
inmGetIdNameSensSet::IdNameMapping->
Set.Set ((Id, Int), String)
inmGetIdNameSensSet (_, _, _, _, _, _, _, s, _) = s
-- | projection function for the operators that represent constructors
inmGetIdNameConstructors::IdNameMapping->
Set.Set ((Id, OpType, Int, Id), String)
inmGetIdNameConstructors (_, _, _, _, _, _, s, _, _) =
(\((i, t, m), u) newset ->
inmGetIdNameGaPredSet::IdNameMapping->
Set.Set ((Id, PredType), String)
inmGetIdNameGaPredSet (_, _, _, _, _, _, _, _, s) = s
-- | get just a set with all known 'Id'S and their XML-names
-- ('Id'S can show up more than once because their XML-name differs).
-- This does not contain the 'Id's from 'inmGetIdNameGaPredSet'.
inmGetIdNameAllSet::IdNameMapping->
Set.Set (Id, String)
(inmGetIdNameSortSet inm)
(\( (id', _), s') -> (id', s'))
(inmGetIdNameSensSet inm)
(\( (id',_), s') -> (id', s'))
(inmGetIdNamePredSet inm)
(\( (id',_), s') -> (id', s'))
-- | projection function to get library name and node number
inmGetLNNN inm = (inmGetLibName inm, inmGetNodeNum inm)
-- | searches for mapping where library name and node number match
inmFindLNNN::(LIB_NAME,
Graph.Node)->[IdNameMapping]->Maybe IdNameMapping
inmFindLNNN lnnn = find (\inm -> inmGetLNNN inm == lnnn)
-- | filter a list of mappings to keep only mappings that contain a
getIdOrigins::[IdNameMapping]->Id->[IdNameMapping]
(\(sid', _) -> sid' == sid)
-- | like 'getIdOrigins' but search for an XML-name instead of an 'Id'
getNameOrigins::[IdNameMapping]->String->[IdNameMapping]
getNameOrigins (o:r) name =
(\(_, name') -> name' == name)
) ++ getNameOrigins r name
-- | check whether a list of mappings contains a mapping for a given
-- library and node number and if this mappings contains entries for
--Returns the empty list, if there is no such mapping. Otherwise a list with
--one element is returned.
getNameOrigin::[IdNameMapping]->LIB_NAME->
Graph.Node->String->[IdNameMapping]
getNameOrigin names ln node name =
case getLNGN names ln node of
(\(_, name') -> name' == name)
-- | search for a mapping where the library name and the node match the given
getLNGN::[IdNameMapping]->LIB_NAME->
Graph.Node->Maybe IdNameMapping
| (inmGetLibName h) == ln && (inmGetNodeNum h) == nn = Just h
| otherwise = getLNGN r ln nn
-- | go through a list of mappings, extract part of the mapping, process that
-- part and check if this processed part is what is searched for. If yes,
-- transform into a name ('String').
[IdNameMapping] -- ^ list to search in
->(IdNameMapping->a) -- ^ part extractor
->(a->c) -- ^ part processor
->(c->Bool) -- ^ part checker
->(c->String) -- ^ applied to processed part iff checker is 'True'
getNameFor [] _ _ _ _ = Nothing
getNameFor (h:r) translate process found extract =
processed = process $ translate h
getNameFor r translate process found extract
-- | search in a list of mappings for the XML-name of a given sort
getNameForSort::[IdNameMapping]->SORT->Maybe String
getNameForSort mapping s =
-- | search in a list of mappings for the XML-name of a given predicate
getNameForPred::[IdNameMapping]->(Id, PredType)->Maybe String
getNameForPred mapping (pid, pt) =
(inmGetIdNameGaPredSet nm)
(
Set.filter (\((pid', pt'), _) -> pid' == pid && pt' == pt))
-- | search in a list of mappings for the XML-name of a fiven operator
getNameForOp::[IdNameMapping]->(Id, OpType)->Maybe String
getNameForOp mapping (oid, ot) =
(
Set.filter (\((oid', ot'), _) -> oid' == oid && ot' == ot))
-- | search in a list of mappings for the XML-name of a given
-- sentence name (and apperance-tag)
getNameForSens::[IdNameMapping]->(Id, Int)->Maybe String
getNameForSens mapping (s,sn) =
(
Set.filter (\((sid, sn'), _) -> sid == s && sn' == sn))
-- | type conversion. Ommit 'Range'
cv_Op_typeToOpType::OP_TYPE->OpType
cv_Op_typeToOpType (Op_type fk args res _) = OpType fk args res
-- | type conversion. Set range to 'nullRange'.
cv_OpTypeToOp_type::OpType->OP_TYPE
cv_OpTypeToOp_type (OpType fk args res) = Op_type fk args res nullRange
-- | type conversion. Ommit 'Range'
cv_Pred_typeToPredType::PRED_TYPE->PredType
cv_Pred_typeToPredType (Pred_type args _) = PredType args
-- | type conversion. Set range to 'nullRange'.
cv_PredTypeToPred_type::PredType->PRED_TYPE
cv_PredTypeToPred_type (PredType args) = Pred_type args nullRange
-- | translate a named 'CASLFORMULA' into a set of operators
-- corresponding to the /Sort_gen_ax/-axiom.
-- Anything else than a /Sort_gen_ax/-axiom for input results in an
extractConstructorOps ansen =
(\ops (Constraint _ symbs _) ->
(\ops' (Qual_op_name name ot _) ->
-- | translate a node name to a string like 'showName' but
-- creates the strign \"/AnonNode/\" if the node name is empty
nodeNameToName::NodeName->String
if (length nodename) == 0
-- | wrapper around (CASL) symbols
| IdOpM Id OpType (Maybe (Int, Id)) Bool
-- | uniform types for 'Identifier'
data IdentifierType = IdTNodeName | IdTId | IdTOpM | IdTPred | IdTSens | IdTGaPred
-- | get type for an 'Identifier'
getIdType::Identifier->IdentifierType
getIdType (IdNodeName {}) = IdTNodeName
getIdType (IdId {}) = IdTId
getIdType (IdOpM {}) = IdTOpM
getIdType (IdPred {}) = IdTPred
getIdType (IdSens {}) = IdTSens
getIdType (IdGaPred {}) = IdTGaPred
-- | uniformly project the 'Id' an 'Identifier' refers to
getIdId (IdNodeName i) = i
getIdId (IdOpM i _ _ _) = i
getIdId (IdGaPred i _) = i
-- | equality for 'Identifier'S. Uses equality of wrapped data
-- (except for disambiguation 'Int'S)
instance Eq Identifier where
(IdNodeName x) == (IdNodeName y) = x == y
(IdId x) == (IdId y) = x == y
(IdOpM x xt _ _) == (IdOpM y yt _ _) = x == y && xt == yt
(IdPred x xt) == (IdPred y yt) = x == y && xt == yt
(IdSens x _) == (IdSens y _) = x == y
(IdGaPred x xt) == (IdGaPred y yt) = x == y && xt == yt
-- | ordering for 'Identifier'S. Orders by 'IdentifierType' unless equal.
-- Orders by string representation if equal.
instance Ord Identifier where
if (getIdType x) == (getIdType y)
(show x) `compare`(show y)
(getIdType x) `compare` (getIdType y)
-- | 'Identifier'S with origins
type IdentifierWON = WithOriginNode Identifier
-- | extract predicates from 'FORMULA'S.
-- Applied recursively to all internal 'FORMULA'S. Internal
-- 'TERM'S are processed by 'getRecursivePredicatesT'.
getRecursivePredicates::FORMULA f->[PRED_SYMB]
getRecursivePredicates (Quantification _ _ f _) =
getRecursivePredicates (Conjunction fs _) =
concatMap getRecursivePredicates fs
getRecursivePredicates (Disjunction fs _) =
concatMap getRecursivePredicates fs
getRecursivePredicates (Implication f1 f2 _ _) =
(getRecursivePredicates f1) ++ (getRecursivePredicates f2)
getRecursivePredicates (Equivalence f1 f2 _) =
(getRecursivePredicates f1) ++ (getRecursivePredicates f2)
getRecursivePredicates (Negation f _) =
getRecursivePredicates (Predication ps t _) =
[ps] ++ (concatMap getRecursivePredicatesT t)
getRecursivePredicates (Definedness t _) =
getRecursivePredicatesT t
getRecursivePredicates (Existl_equation t1 t2 _) =
(getRecursivePredicatesT t1) ++ (getRecursivePredicatesT t2)
getRecursivePredicates (Strong_equation t1 t2 _) =
(getRecursivePredicatesT t1) ++ (getRecursivePredicatesT t2)
getRecursivePredicates (Membership t _ _) =
getRecursivePredicatesT t
getRecursivePredicates _ =
-- | extract predicates from 'TERM'S.
-- Applied recursively to all internal 'TERM'S. Internal
-- 'FORMULA'S are processed by 'getRecursivePredicates'.
getRecursivePredicatesT::TERM f->[PRED_SYMB]
getRecursivePredicatesT (Application _ ts _) =
concatMap getRecursivePredicatesT ts
getRecursivePredicatesT (Sorted_term t _ _) =
getRecursivePredicatesT t
getRecursivePredicatesT (Cast t _ _) =
getRecursivePredicatesT t
getRecursivePredicatesT (Conditional t1 f t2 _) =
(getRecursivePredicatesT t1)
(getRecursivePredicates f)
(getRecursivePredicatesT t2)
getRecursivePredicatesT _ =
-- | Collect all used symbols from a library environment.
-- Inspects all signatures and sentences and collects generated predicates
-- by extracting them with 'getRecursivePredicates' from the corresponding
-- Uses 'createNODENAMEWOMap' and 'extractConstructorOps'.
dg = lookupDGraph ln lenv
-- extract sorts, predicates and operators
(sortswomap, predswomap, opswomap) =
dgnodes = filter (not . isDGRef . snd) $ labNodesDG dg
(\(nn, node) -> (nn, stringToId $ nodeNameToName $ dgn_name node))
-- collect and label sentences
(\(nn, node) -> map (\x -> (nn, x)) $ zip [1..] (getNodeSentences node))
-- get constructors from sentences
(\(nodenum, (sennum, s)) ->
(\(cid, ot) -> (nodenum, (sennum, cid, ot)))
(extractConstructorOps s)
-- find sort generating predicates
(Sort_gen_ax constraints _) ->
getRecursivePredicates (cf :: FORMULA ())
nnamewo = mkWON (dgn_name sennode) nn
(\(Constraint _ cops _ ) ->
(Qual_op_name copid coptype _) ->
&& cot == cv_Op_typeToOpType coptype
(cv_Op_typeToOpType coptype)
(cv_Op_typeToOpType coptype)
error "Unqualified OpName in Constraints!"
mkWON (IdGaPred pn (PredType [])) nn
(Qual_pred_name pn pt _) ->
(IdGaPred pn (cv_Pred_typeToPredType pt))
(
Set.map (\swo -> mkWON (IdId (woItem swo)) (woOrigin swo) ) sortsetwo)
(\(num, (_, cid, cot)) ->
(num == woOrigin oid) && (cid == woItem oid) && (cot == ot)
(
Set.singleton (mkWON (IdOpM (woItem oid) ot Nothing False) (woOrigin oid)))
(Just (sennum, opRes ot))
(\fm' (nodenum, (sennum, namedsen)) ->
-- this will override some of
-- the previous operators
-- but catches also sentence-related cons
(\fm' (nodenum, (sennum, cid, cot)) ->
sennode = labDG dg nodenum
nnamewo = mkWON (dgn_name sennode) nodenum
"Generating Constructor from Sentence: "
++ (show (nodenum, (cid, cot)))
(
Set.singleton (mkWON (IdOpM cid cot (Just (sennum, opRes cot)) True) nodenum))
(\(nn, nnid)-> mkWON (IdNodeName nnid) nn)
-- | find out, which used symbols are actually from
-- somewhere else (imported)
->
Map.Map (LIB_NAME, IdentifierWON) (LIB_NAME, IdentifierWON)
-- create a list of referenced (external) libraries
dg = lookupDGraph ln lenv
(\(_, node) -> isDGRef node)
rl ++ (map (\(rnn, rnode) -> (ln, rnn, dgn_libname rnode, dgn_node rnode)) refnodes)
-- cure some recursive evil...
(\im (refln, refnn, refedln, refednode) ->
-- identifiers for reference
-- identifiers there with origin in current library
refedids =
Set.filter (\ws -> woOrigin ws == refnn) reflnids
-- identifiers in the referenced library
-- for each referenced identifier
-- try to find at least one matching identifier in reference
Set.filter (\x -> woItem x == woItem rws) refedlnids
-- if none, something is wrong (should not happen)
("The impossible : " ++ (show $ woItem rws))
Map.insert (refln, rws) (refedln, mkWON (IdId $ stringToId "unknown") refednode) im'
-- use first matching element to construct reference information
-- this is correct for Hets (same name -> same thing)
-- but for OMDoc this equality needs to be constructed... (TODO)
sameConAsOp::Identifier->Identifier->Bool
sameConAsOp (IdCons cid cot _) (IdOp oid oot) = cid == oid && cot == oot
sameConAsOp (IdOp oid oot) (IdCons cid cot _) = cid == oid && cot == oot
sameConAsOp i1 i2 = i1 == i2
-- | find recursive identity matches and reduce targets to real identity.
-- Background: import from identifiers that where already imported from
-- somewhere else are not found at first.
Map.Map (LIB_NAME, IdentifierWON) (LIB_NAME, IdentifierWON)
->
Map.Map (LIB_NAME, IdentifierWON) (LIB_NAME, IdentifierWON)
case finalRecursiveTarget identMap key of
finalRecursiveTarget::(Eq a, Ord a)=>
Map.Map a a->a->Maybe a
finalRecursiveTarget m a =
case finalRecursiveTarget m a' of
findMultiOriginUnifications::
findMultiOriginUnifications
idents = identifyFlatNames lenv flatted
-- | use previously created reference mapping to remove referenced
-- identifiers from a mapping (leaving only identifiers where they are
removeReferencedIdentifiers::
->
Map.Map (LIB_NAME, IdentifierWON) (LIB_NAME, IdentifierWON)
removeReferencedIdentifiers
-- OMDoc does only enforce unique names inside a theory
-- | Calculate the number of use of a name (attach increasing numbers to
-- multiple occurences of the same name).
-- OMDoc allows same names only in different theories (and the names of all
-- theories inside a document must be unique).
(\newset currentOrigin ->
(\i -> (woOrigin i) == currentOrigin)
(getIdId $ woItem previousIWO)
makeUniqueGlobalCounts unnMap
-- NodeNames and Sentences (Axioms / Definitions) need
-- to be unique in the whole document
-- | fix global namespace issues
Create unique names from the use count.
Name collisions are handled by numbering names in order of
appereance and adding \"_\<number>\" to their name. From this
a second form of collisions arises when there is a \'natural\'
name in the form of \"name_1\". This algorithm uses the numbering
as a start and checks uniqueness per theory (and for node-names).
(\(iwon, c) (ni, nodeNames, inTheoryNames) ->
(IdNodeName {}) -> nodeNames
ext = case c' of 0 -> ""; _ -> "_" ++ (show c')
name = (show $ getIdId $ woItem iwon) ++ ext
_ -> "_" ++ (show finalCount)
finalName = (show $ getIdId $ woItem iwon) ++ finalExt
(newSet, newNameSet, inTheoryNames)
,
Map.insert (woOrigin iwon) newNameSet inTheoryNames
-- | uses a previously generated unique name mapping for identifiers
-- to generated a list of 'IdNameMapping'S for a library environment.
-- The mappings contain only the theory unique symbols. See 'makeFullNames'.
makeUniqueIdNameMapping::
dg = lookupDGraph ln lenv
(\(i, _) -> case woItem i of IdSens {} -> True; _ -> False)
(\(i, _) -> case woItem i of IdGaPred {} -> True; _ -> False)
(\(i, _) -> woOrigin i == nn)
nodeNameToName $ dgn_name node
++ show (nn, nodeNameToName $ dgn_name node)
mdg = lookupDGraph mln lenv
nodeNameToName $ dgn_name mnode
++ show (ln, nn, nodeNameToName $ dgn_name node)
++ show (mln, mnn, nodeNameToName $ dgn_name mnode)
(nodeNameToName $ dgn_name mnode)
(getIdId $ woItem i, uname)
(\(i, _) -> case woItem i of IdId {} -> True; _ -> False)
(\(i, _) -> case woItem i of
case woItem i of IdPred {} -> True; _ -> False) nodeids
nodesensunn =
Set.filter (\(i, _) -> woOrigin i == nn) sensfromunn
(IdSens sensid sennum) ->
((sensid, sennum), uname)
_ -> error "Non-sentence found in sentence processing...."
Set.filter (\(i, _) -> woOrigin i == nn) gapredsfromunn
(IdGaPred gapredid gapt) ->
((gapredid, gapt), uname)
_ -> error "Non-ga_pred found in ga_pred processing..."
-- | check if a type t1 is a subtype of a type t2
-- Returns 'True' iff the first sort is the same as the second sort
-- or the first sort is a subsort of the second sort.
-- Uses '
Rel.path' /first/ /second/ /rel/ to check subsort.
isTypeOrSubType sortrel givensort neededsort =
(givensort == neededsort)
|| (
Rel.path givensort neededsort sortrel)
-- | check for type compatibility
-- a type /t1/ is compatible to a type /t2/ if
-- a) /t1 == t2/ or b) /t1/ is a subtype of /t2/
-- Each sort in the given lists must be /compatible/ to the sort
-- at the same position in the other list. That is, the sorts in the
-- first lists must be of the same or of a sub-type of the sort in the
->[SORT] -- ^ types to compare (/given/)
->[SORT] -- ^ types to compare (/needed/)
compatibleTypes _ [] [] = True
compatibleTypes _ [] _ = False
compatibleTypes _ _ [] = False
compatibleTypes sortrel (s1:r1) (s2:r2) =
(isTypeOrSubType sortrel s1 s2) && (compatibleTypes sortrel r1 r2)
-- | check type compatibility for two predicates
compatiblePredicate::
Rel.Rel SORT->PredType->PredType->Bool
compatiblePredicate sortrel pt1 pt2 =
compatibleTypes sortrel (predArgs pt1) (predArgs pt2)
-- | check type compatibility for two operators
compatibleOperator::
Rel.Rel SORT->OpType->OpType->Bool
compatibleOperator sortrel ot1 ot2 =
-- (\x -> trace ("Comparing " ++ show ot1 ++ " to " ++ show ot2 ++ " -> " ++ show x) x)
(isTypeOrSubType sortrel (opRes ot1) (opRes ot2))
(compatibleTypes sortrel (opArgs ot1) (opArgs ot2))
->[(IdentifierWON, String)]
->[(IdentifierWON, String)]
getIdentifierAt collectionMap location
->[((IdentifierWON, PredType), String)]
(IdPred _ pt) -> l ++ [((i, pt), uName)]
(IdGaPred _ pt) -> l ++ [((i, pt), uName)]
getIdentifierAt collectionMap location
->[((IdentifierWON, OpType), String)]
(IdOpM _ ot _ _) -> l ++ [((i, ot), uName)]
getIdentifierAt collectionMap location
->[((IdentifierWON, Int), String)]
l ++ [((i, snum), uName)]
getIdentifierAt collectionMap location
->[(IdentifierWON, String)]
->[(IdentifierWON, String)]
getDefinedIdentifierAt collectionMap location
->[((IdentifierWON, PredType), String)]
(IdPred _ pt) -> l ++ [((i, pt), uName)]
(IdGaPred _ pt) -> l ++ [((i, pt), uName)]
getDefinedIdentifierAt collectionMap location
->[((IdentifierWON, OpType), String)]
(IdOpM _ ot _ _) -> l ++ [((i, ot), uName)]
getDefinedIdentifierAt collectionMap location
->[((IdentifierWON, Int), String)]
l ++ [((i, snum), uName)]
getDefinedIdentifierAt collectionMap location
->[(LIB_NAME, IdentifierWON)]
(stringproc uName) == idname
->[(LIB_NAME, IdentifierWON)]
allValid = findIdentifiersForName collectionMap location idname stringproc
->[(LIB_NAME, IdentifierWON)]
allValid = findIdentifiersForName collectionMap location idname stringproc
compatiblePredicate srel ipt ptype
compatiblePredicate srel ipt ptype
if null eqpr then comp else eqpr
->[(LIB_NAME, IdentifierWON)]
allValid = findIdentifiersForName collectionMap location idname stringproc
compatibleOperator srel iot otype
iot { opKind = opKind otype } == otype
if null eqop then comp else eqop
->[(LIB_NAME, (IdentifierWON, String))]
getIdId (woItem idwo) == id'
->[(LIB_NAME, (IdentifierWON, String))]
allValid = findIdentifiersForId collectionMap location id'
->[(LIB_NAME, (IdentifierWON, String))]
allValid = findIdentifiersForId collectionMap location id'
compatiblePredicate srel ipt ptype
compatiblePredicate srel ipt ptype
if null eqpr then comp else eqpr
->[(LIB_NAME, (IdentifierWON, String))]
allValid = findIdentifiersForId collectionMap location id'
compatibleOperator srel iot otype
iot { opKind = opKind otype } == otype
if null eqop then comp else eqop
-- | uses previously generated unique name and reference mappings
-- to generate a mapping for each node showing
-- which symbols are imported from where.
-- By this better statements about the origin of a symbol
-- can be written out (
e.g. cdbase)
-- See 'makeUniqueIdNameMapping'.
->
Map.Map (LIB_NAME, IdentifierWON) (LIB_NAME, IdentifierWON)
dg = lookupDGraph ln lenv
(sortswomap, predswomap, opswomap) =
(\(i, _) -> case woItem i of IdSens {} -> True; _ -> False)
(\(i, _) -> case woItem i of IdGaPred {} -> True; _ -> False)
(\(i, _) -> case woItem i of IdOpM _ _ _ True -> True; _ -> False)
(stringToId $ nodeNameToName $ dgn_name node)
++ show (nn, nodeNameToName $ dgn_name node)
mdg = lookupDGraph mln lenv
(stringToId $ nodeNameToName $ dgn_name mnode)
++ show (ln, nn, nodeNameToName $ dgn_name node)
++ show (mln, mnn, nodeNameToName $ dgn_name mnode)
(nodeNameToName $ dgn_name mnode)
(mkWON (dgn_name node) nn)
sasid = mkWON (IdId (woItem swo)) (woOrigin swo)
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Sort " ++ (show swo)
(\(s, _) -> case wonItem s of IdId {} -> True; _ -> False)
(\(s,_) -> (getIdId $ wonItem s) == (wonItem swo))
(\(s,_) -> (woOrigin s) == (woOrigin mid))
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Sort \"" ++ (show swo)
++ " referencing to it as \""
++ (show mid) ++ "\" in Library \""
++ "Matches by Name : " ++ (show refMatch) ++ " "
++ "Matches by Origin : " ++ (show refOrigin)
Set.filter (\(i, _) -> woOrigin i == nn) genopsfromunn
-- generated operators can not be referenced from
-- somewhere so they are not checked here.
opasid = mkWON (IdOpM (woItem idwo) ot Nothing False) (woOrigin idwo)
(\(i, _) -> (i == opasid) )
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Operator \"" ++ (show idwo)
(ln, (opasid, show idwo))
("Not an operator, but same name... " ++ (show x))
(\(s, _) -> case wonItem s of IdId {} -> True; _ -> False)
(\(s,_) -> (getIdId $ wonItem s) == (wonItem idwo))
(\(s,_) -> (woOrigin s) == (woOrigin mid))
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Operator \"" ++ (show idwo)
++ " referencing to it as \""
++ (show mid) ++ "\" in Library \""
++ "Matches by Name : " ++ (show refMatch) ++ " "
++ "Matches by Origin : " ++ (show refOrigin)
("Not an operator but same name " ++ (show x))
predasid = mkWON (IdPred (woItem idwo) pt) (woOrigin idwo)
(\(i, _) -> i == predasid)
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Predicate \"" ++ (show idwo)
(ln, (predasid, show idwo))
(\(s, _) -> case wonItem s of IdId {} -> True; _ -> False)
(\(s,_) -> (getIdId $ wonItem s) == (wonItem idwo))
(\(s,_) -> (woOrigin s) == (woOrigin mid))
"In Library " ++ (show ln) ++ ", Theory \""
++ nodename ++ "\" : Predicate \"" ++ (show idwo)
++ " referencing to it as \""
++ (show mid) ++ "\" in Library \""
++ "Matches by Name : " ++ (show refMatch) ++ " "
++ "Matches by Origin : " ++ (show refOrigin)
nodesensunn =
Set.filter (\(i, _) -> woOrigin i == nn) sensfromunn
Set.filter (\(i, _) -> woOrigin i == nn) gapredsfromunn
-- | check if a link is a definitional link (LocaDef, GlobalDef, HidingDef)
isDefLink :: DGLinkLab -> Bool
isDefLink = isDefEdge . dgl_type
-- | try to find the origin of an identifier in the DevGraph
DGraph -- ^ DevGraph to use
->Identifier -- ^ Identifier to search origin for
caslsign = getJustCASLSign $ getCASLSign $ dgn_sign node
sortset = sortSet caslsign
(\(_, tos) i -> tos == i)
nextTrace nonBlockingEdges
(IdPred predid predtype) ->
predmap = predMap caslsign
(\(_, topredid) i -> topredid == i)
nextTrace nonBlockingEdges
(IdOpM opid optype _ _) ->
(\(_, (toopid, _)) i -> toopid == i)
nextTrace nonBlockingEdges
_ -> error "not implemented!"
nextTrace::[
Graph.LEdge DGLinkLab]->Maybe IdentifierWON
map (\(from, _, _) -> from) nbe
(\n' -> traceIdentifierOrigin dg n' identifier)
caslmorph = getCASLMorphLL dgl
(\d -> checkPart d (getIdId identifier))
(getMorphParts caslmorph)
-- | try to find the origins of all identifiers in a node
traceAllIdentifierOrigins::
DGraph -- ^ DevGraph to use
->
Graph.Node -- ^ node to take identifiers from (to find their origins)
traceAllIdentifierOrigins
caslsign = getJustCASLSign $ getCASLSign $ dgn_sign node
(\pt -> IdPred predid pt)
(\ot -> IdOpM opid ot Nothing False)
Nothing -> error "should never happen!"
-- | create a mapping of 'Identifier'S with their origins for a DevGraph
(\dg' n' -> traceAllIdentifierOrigins dg' n')
-- | split a mapping of 'Identifier'S with origins into
-- three mapping. One for sorts, one for predicates and one for operators.
-- | search in a list of name mappings for every mapping that
-- matches a given library name and if it contains an element.
-- The /full names/ list is used after the /unique/ list has been searched
-- completely without result.
LIB_NAME -- ^ only mappings with that library name are searched
->[IdNameMapping] -- ^ mapping of unique names
->[IdNameMapping] -- ^ mapping of full names (used if nothing found in unique names)
->(IdNameMapping->Maybe a) -- ^ search for element
nextsearch = findOriginInCurrentLib ln uniqueNames fullNames check
if (inmGetLibName inm == ln)
traceRealIdentifierOrigins::
->Identifier -- ^ Identifier to search origin for
traceRealIdentifierOrigins
dg = lookupDGraph ln lenv
caslsign = getJustCASLSign $ getCASLSign $ dgn_sign node
sortset = sortSet caslsign
(\(_, tos) i -> tos == i)
(\(oldname, _) -> IdId oldname)
(\(_, tos) i -> tos == i)
nextTraces nonBlockingEdges morphismSearches
(IdPred predid predtype) ->
predmap = predMap caslsign
(\(_, tos) i -> tos == i)
(\((oldname, oldtype), _) -> IdPred oldname oldtype)
(\(_, topredid) i -> topredid == i)
nextTraces nonBlockingEdges morphismSearches
(IdOpM opid optype mc isGen) ->
(\(_, (tos, _)) i -> tos == i)
(\((oldname, oldtype), _) -> IdOpM oldname oldtype mc isGen)
(\(_, (toopid, _)) i -> toopid == i)
nextTraces nonBlockingEdges morphismSearches
_ -> error "not implemented!"
map (\(from, _, _) -> from) nbl
(\n' -> traceRealIdentifierOrigins lenv ln n' identifier)
traceRealIdentifierOrigins lenv ln' n' i'
(\mS (fromNodeNumber, _, dgl) ->
caslmorph = getCASLMorphLL dgl
fromNode = labDG dg fromNodeNumber
(dgn_libname fromNode, dgn_node fromNode)
(\p -> checkPart p (getIdId identifier))
(getMorphParts caslmorph)
map (\p -> (fromlib, fromNodeNum, makeNewId p)) mlist
caslmorph = getCASLMorphLL dgl
(\d -> checkPart d (getIdId identifier))
(getMorphParts caslmorph)
DGraph -- ^ DevGraph to use
->Identifier -- ^ Identifier to search origin for
caslsign = getJustCASLSign $ getCASLSign $ dgn_sign node
sortset = sortSet caslsign
caslmorph = getCASLMorphLL dgl
(\(_, tos) -> tos == sid)
nextTraces nonBlockingEdges
(IdPred predid predtype) ->
predmap = predMap caslsign
caslmorph = getCASLMorphLL dgl
(\(_, topredid) -> topredid == predid)
nextTraces nonBlockingEdges
(IdOpM opid optype _ _) ->
caslmorph = getCASLMorphLL dgl
(\(_, (toopid, _)) -> toopid == opid)
nextTraces nonBlockingEdges
_ -> error "not implemented!"
map (\(from, _, _) -> from) nbl
(\n' -> traceIdentifierOrigins dg n' identifier)
[] -> [mkWON identifier n]
-- | try to find all possible origins of all identifiers in a node
traceAllIdentifierOriginsMulti::
DGraph -- ^ DevGraph to use
->
Graph.Node -- ^ node to take identifiers from (to find their origins)
traceAllIdentifierOriginsMulti
caslsign = getJustCASLSign $ getCASLSign $ dgn_sign node
(\pt -> IdPred predid pt)
(\ot -> IdOpM opid ot Nothing False)
[] -> error "should never happen!"
dg = lookupDGraph ln lenv
dgnodes = filter (not . isDGRef . snd) $ labNodesDG dg
multi = traceAllIdentifierOriginsMulti dg nnum