Analysis.hs revision ece3b1a5353a9af3c966a1d5453594ed35334f7b
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke{- |
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeModule : $Header$
9eb6a481980d81a55898ba418fba72fc3c09d8c8Dominik LueckeDescription : Basic analysis for propositional logic extended with QBFs
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : jonathan.von_schroeder@dfki.de
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckeStability : experimental
b72a390042c19e630cf221494b60c9df2a60d187Dominik LueckePortability : portable
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke
f90884915ff10ae83f59e709c68824de834e64f5Dominik LueckeBasic and static analysis for propositional logic
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke Ref.
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke <http://en.wikipedia.org/wiki/Propositional_logic>
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke <http://www.voronkov.com/lics.cgi>
cf04ba46b9eb495d334466e24e082e391055ca7bDominik Luecke-}
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke
2af38fde95f93562f2124ec615fba0e509c8202eDominik Lueckemodule QBF.Analysis
926b3c5491f1c608f5b79e2d8014d7a1385558c3Dominik Luecke (
2af38fde95f93562f2124ec615fba0e509c8202eDominik Luecke basicPropositionalAnalysis
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke , mkStatSymbItems
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke , mkStatSymbMapItem
da955132262baab309a50fdffe228c9efe68251dCui Jian , inducedFromMorphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , inducedFromToMorphism
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder , signatureColimit
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder )
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder where
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport Common.ExtSign
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport Common.Lib.Graph
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport Common.SetColimit
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport Data.Graph.Inductive.Graph
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport Propositional.Sign as Sign
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maederimport qualified Common.AS_Annotation as AS_Anno
16e124196c6b204769042028c74f533509c9b5d3Christian Maederimport qualified Common.GlobalAnnotations as GlobalAnnos
f90884915ff10ae83f59e709c68824de834e64f5Dominik Lueckeimport qualified Common.Id as Id
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Common.Result as Result
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport qualified Data.List as List
f90884915ff10ae83f59e709c68824de834e64f5Dominik Lueckeimport qualified Data.Map as Map
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Lueckeimport qualified Data.Set as Set
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Lueckeimport qualified QBF.AS_BASIC_QBF as AS_BASIC
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Lueckeimport qualified QBF.Morphism as Morphism
08056875f5f633ef432598d5245ea41c112d2178Dominik Lueckeimport qualified QBF.Symbol as Symbol
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Lueckeimport Control.Arrow
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke-- | Datatype for formulas with diagnosis data
da955132262baab309a50fdffe228c9efe68251dCui Jiandata DIAGFORM = DiagForm
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder {
f90884915ff10ae83f59e709c68824de834e64f5Dominik Luecke formula :: AS_Anno.Named AS_BASIC.FORMULA,
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder diagnosis :: Result.Diagnosis
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder }
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder-- | Formula annotated with a number
b72a390042c19e630cf221494b60c9df2a60d187Dominik Lueckedata NUMFORM = NumForm
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke {
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke , nfnum :: Integer
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder }
b72a390042c19e630cf221494b60c9df2a60d187Dominik Luecke
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederdata TESTSIG = TestSig
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke {
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke msign :: Sign.Sign
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke , occurence :: Int
da955132262baab309a50fdffe228c9efe68251dCui Jian , tdiagnosis :: [Result.Diagnosis]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder }
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke-- | Retrieves the signature out of a basic spec
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckemakeSig ::
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder AS_BASIC.BASICSPEC -- Input SPEC
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> Sign.Sign -- Input Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke -> TESTSIG -- Output Signature
548f3850942936a8c6021185c8391dfcd3b03018Dominik LueckemakeSig (AS_BASIC.BasicSpec spec) sig = List.foldl retrieveBasicItem
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke TestSig { msign = sig
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke , occurence = 0
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke , tdiagnosis = []
5b2e9f4673599e1bc6e18a43ad615da28305b8e1Christian Maeder }
548f3850942936a8c6021185c8391dfcd3b03018Dominik Luecke spec
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke-- Helper for makeSig
08056875f5f633ef432598d5245ea41c112d2178Dominik LueckeretrieveBasicItem ::
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder TESTSIG -- Input Signature
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS -- Input Item
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke -> TESTSIG -- Output Signature
08056875f5f633ef432598d5245ea41c112d2178Dominik LueckeretrieveBasicItem tsig x =
08056875f5f633ef432598d5245ea41c112d2178Dominik Luecke let
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder occ = occurence tsig
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder in
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder case (AS_Anno.item x) of
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (AS_BASIC.PredDecl apred) ->
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder if occ == 0
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder then
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder List.foldl
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke (\ asig ax -> TestSig {
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke msign = Sign.addToSig (msign asig)
fcac596b16bb10f475066c323b9b1ca44db2b755Dominik Luecke $ Id.simpleIdToId ax
0859769b65851f4c06d6d32fac084b0f4db56c94Christian Maeder , occurence = occ
da955132262baab309a50fdffe228c9efe68251dCui Jian , tdiagnosis = tdiagnosis tsig ++
4df63f7187b1ba16cbe5c781db187a42f2f49579Dominik Luecke [Result.Diag
b694e4b3f771a2f32042c9c505dd698bde969558Dominik Luecke {
5b9f5c1b3592b99fc74d3438740ebcf9eb4c94beDominik Luecke Result.diagKind = Result.Hint
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , Result.diagString = "All fine"
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , Result.diagPos = AS_Anno.opt_pos x
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder }]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder })
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke else
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke List.foldl
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke (\ asig ax -> TestSig {
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke msign = Sign.addToSig (msign asig)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder $ Id.simpleIdToId ax
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , occurence = occ
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , tdiagnosis = tdiagnosis tsig ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder [Result.Diag
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder {
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke Result.diagKind = Result.Error
2ea0ce749d2525f96d5d2f285f519ab07b005b8dDominik Luecke , Result.diagString =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder "Definition of proposition " ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder show (pretty ax) ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder " after first axiom"
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , Result.diagPos = AS_Anno.opt_pos x
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder }]
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder })
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder (AS_BASIC.AxiomItems _) -> TestSig { msign = msign tsig
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , occurence = occ + 1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , tdiagnosis = tdiagnosis tsig ++
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder [Result.Diag
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder {
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Result.diagKind = Result.Hint
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , Result.diagString =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder "First axiom"
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder , Result.diagPos =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder AS_Anno.opt_pos x
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder }]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder }
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- | Retrieve the formulas out of a basic spec
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermakeFormulas ::
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder AS_BASIC.BASICSPEC
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> Sign.Sign
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> [DIAGFORM]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaedermakeFormulas (AS_BASIC.BasicSpec bspec) sig =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder-- Helper for makeFormulas
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaederretrieveFormulaItem ::
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder [DIAGFORM]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> Sign.Sign
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder -> [DIAGFORM]
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian MaederretrieveFormulaItem axs x sig =
202df46772cac2ee2e8627ba196a5faebb6f9a05Christian Maeder case (AS_Anno.item x) of
(AS_BASIC.PredDecl _) -> axs
(AS_BASIC.AxiomItems ax) ->
List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
-- Number formulae
numberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUMFORM]
numberFormulae [] _ = []
numberFormulae (x : xs) i
| label == "" =
NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
| otherwise =
NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
where
label = AS_Anno.getRLabel x
-- Add a formula to a named list of formulas
addFormula :: [DIAGFORM]
-> NUMFORM
-> Sign.Sign
-> [DIAGFORM]
addFormula formulae nf sign
| isLegal = formulae ++
[DiagForm
{
formula = makeNamed f i
, diagnosis = Result.Diag
{
Result.diagKind = Result.Hint
, Result.diagString = "All fine"
, Result.diagPos = lnum
}
}]
| otherwise = formulae ++
[DiagForm
{
formula = makeNamed f i
, diagnosis = Result.Diag
{
Result.diagKind = Result.Error
, Result.diagString =
"Unknown propositions "
++ show (pretty difference)
++ " in formula "
++ show (pretty nakedFormula)
, Result.diagPos = lnum
}
}]
where
f = nfformula nf
i = nfnum nf
nakedFormula = AS_Anno.item f
varsOfFormula = propsOfFormula nakedFormula
isLegal = Sign.isSubSigOf varsOfFormula sign
difference = Sign.sigDiff varsOfFormula sign
lnum = AS_Anno.opt_pos f
-- generates a named formula
makeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
-> AS_Anno.Named AS_BASIC.FORMULA
makeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
else label) $ AS_Anno.item f)
{ AS_Anno.isAxiom = not isTheorem }
where
label = AS_Anno.getRLabel f
annos = AS_Anno.r_annos f
isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
isTheorem = isImplies || isImplied
-- Retrives the signature of a formula
propsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
propsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
propsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite
(propsOfFormula form1)
(propsOfFormula form2)
propsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite
(propsOfFormula form1)
(propsOfFormula form2)
propsOfFormula (AS_BASIC.TrueAtom _) = Sign.emptySig
propsOfFormula (AS_BASIC.FalseAtom _) = Sign.emptySig
propsOfFormula (AS_BASIC.Predication x) = Sign.Sign
{Sign.items = Set.singleton $
Id.simpleIdToId x }
propsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl
(\ sig frm -> Sign.unite sig
$ propsOfFormula frm)
Sign.emptySig xs
propsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl
(\ sig frm -> Sign.unite sig
$ propsOfFormula frm)
Sign.emptySig xs
propsOfFormula (AS_BASIC.ForAll xs f _) = sigDiff
(propsOfFormula f)
(Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
propsOfFormula (AS_BASIC.Exists xs f _) = sigDiff
(propsOfFormula f)
(Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
-- Basic analysis for propositional logic
basicPropositionalAnalysis
:: (AS_BASIC.BASICSPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
-> Result.Result (AS_BASIC.BASICSPEC,
ExtSign Sign.Sign Symbol.Symbol,
[AS_Anno.Named AS_BASIC.FORMULA])
basicPropositionalAnalysis (bs, sig, _) =
Result.Result diags $ if exErrs then Nothing else
Just (bs, ExtSign sigItems declaredSyms, formulae)
where
bsSig = makeSig bs sig
sigItems = msign bsSig
declaredSyms = Set.map Symbol.Symbol
$ Set.difference (items sigItems) $ items sig
bsForm = makeFormulas bs sigItems
formulae = map formula bsForm
diags = map diagnosis bsForm ++ tdiagnosis bsSig
exErrs = Result.hasErrors diags
-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
-> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem xs =
Result.Result
{
Result.diags = []
, Result.maybeResult = Just $
foldl
(
\ smap x ->
case x of
AS_BASIC.SymbMapItems sitem _ ->
Map.union smap $ statSymbMapItem sitem
)
Map.empty
xs
}
statSymbMapItem :: [AS_BASIC.SYMBORMAP]
-> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem =
foldl
(
\ mmap x ->
case x of
AS_BASIC.Symb sym -> Map.insert
(symbToSymbol sym)
(symbToSymbol sym) mmap
AS_BASIC.SymbMap s1 s2 _
-> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
)
Map.empty
-- | Retrieve raw symbols
mkStatSymbItems :: [AS_BASIC.SYMBITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems a = Result.Result
{
Result.diags = []
, Result.maybeResult = Just $ statSymbItems a
}
statSymbItems :: [AS_BASIC.SYMBITEMS] -> [Symbol.Symbol]
statSymbItems = concatMap symbItemsToSymbol
symbItemsToSymbol :: AS_BASIC.SYMBITEMS -> [Symbol.Symbol]
symbItemsToSymbol (AS_BASIC.SymbItems syms _) = map symbToSymbol syms
symbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
symbToSymbol (AS_BASIC.SymbId tok) =
Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
-> Sign.Sign
-> Result.Result Morphism.Morphism
inducedFromMorphism imap sig =
Result.Result
{
Result.diags = []
, Result.maybeResult =
let
sigItems = Sign.items sig
pMap :: Map.Map Id.Id Id.Id
pMap =
Set.fold (
\ x ->
let
symOf = Symbol.Symbol
{ Symbol.symName = x }
y = Symbol.symName
$ Symbol.applySymMap imap symOf
in
Map.insert x y
)
Map.empty sigItems
in
Just
Morphism.Morphism
{
Morphism.source = sig
, Morphism.propMap = pMap
, Morphism.target = Sign.Sign
{Sign.items =
Set.map (Morphism.applyMap pMap)
$ Sign.items sig
}
}
}
-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
-> ExtSign Sign.Sign Symbol.Symbol
-> ExtSign Sign.Sign Symbol.Symbol
-> Result.Result Morphism.Morphism
inducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
let
sigItems = Sign.items sig
pMap :: Map.Map Id.Id Id.Id
pMap =
Set.fold (
\ x ->
let
symOf = Symbol.Symbol
{ Symbol.symName = x }
y = Symbol.symName
$ Symbol.applySymMap
imap
symOf
in
Map.insert x y
)
Map.empty sigItems
targetSig = Sign.Sign
{Sign.items =
Set.map
(Morphism.applyMap pMap)
$ Sign.items sig
}
isSub = Sign.items targetSig
`Set.isSubsetOf`
Sign.items tSig
in
if isSub then
Result.Result {
Result.diags = []
, Result.maybeResult =
Just Morphism.Morphism
{
Morphism.source = sig
, Morphism.propMap = pMap
, Morphism.target = tSig
}
}
else
Result.Result {
Result.diags =
[
Result.Diag
{
Result.diagKind = Result.Error
, Result.diagString =
"Incompatible mapping"
, Result.diagPos = Id.nullRange
}
]
, Result.maybeResult = Nothing
}
signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
-> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signatureColimit graph = do
let graph1 = nmap Sign.items $ emap (Control.Arrow.second Morphism.propMap)
graph
(set, maps) = addIntToSymbols $ computeColimitSet graph1
cSig = Sign.Sign {Sign.items = set}
return (cSig,
Map.fromList $ map (\ (i, n) ->
(i, Morphism.Morphism {
Morphism.source = n,
Morphism.target = cSig,
Morphism.propMap = maps Map.! i
})) $ labNodes graph)