b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./QBF/Analysis.hs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDescription : Basic analysis for propositional logic extended with QBFs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederMaintainer : jonathan.von_schroeder@dfki.de
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederStability : experimental
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederPortability : portable
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederBasic and static analysis for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Ref.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder <http://en.wikipedia.org/wiki/Propositional_logic>
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder <http://www.voronkov.com/lics.cgi>
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroedermodule QBF.Analysis
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder basicPropositionalAnalysis
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , mkStatSymbItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , mkStatSymbMapItem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , inducedFromMorphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , inducedFromToMorphism
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , signatureColimit
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder )
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport Common.ExtSign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport Common.Lib.Graph
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport Common.SetColimit
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport Data.Graph.Inductive.Graph
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport Propositional.Sign as Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.AS_Annotation as AS_Anno
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.GlobalAnnotations as GlobalAnnos
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.Id as Id
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Common.Result as Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.List as List
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Map as Map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Set as Set
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.AS_BASIC_QBF as AS_BASIC
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.Morphism as Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.Symbol as Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederimport Control.Arrow
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Datatype for formulas with diagnosis data
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata DIAGFORM = DiagForm
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula :: AS_Anno.Named AS_BASIC.FORMULA,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder diagnosis :: Result.Diagnosis
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Formula annotated with a number
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata NUMFORM = NumForm
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , nfnum :: Integer
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroederdata TESTSIG = TestSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder msign :: Sign.Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence :: Int
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis :: [Result.Diagnosis]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieves the signature out of a basic spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermakeSig ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.BASICSPEC -- Input SPEC
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign -- Input Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> TESTSIG -- Output Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeSig (AS_BASIC.BasicSpec spec) sig = List.foldl retrieveBasicItem
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder TestSig { msign = sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , occurence = 0
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = []
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Helper for makeSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveBasicItem ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder TESTSIG -- Input Signature
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS -- Input Item
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> TESTSIG -- Output Signature
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveBasicItem tsig x =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder occ = occurence tsig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder in
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder case AS_Anno.item x of
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (AS_BASIC.PredDecl apred) ->
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder if occ == 0
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder then
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder List.foldl
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\ asig ax -> TestSig {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder msign = Sign.addToSig (msign asig)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder $ Id.simpleIdToId ax
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder [Result.Diag
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diagKind = Result.Hint
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.diagString = "All fine"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos = AS_Anno.opt_pos x
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder })
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder else
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder List.foldl
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (\ asig ax -> TestSig {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder msign = Sign.addToSig (msign asig)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder $ Id.simpleIdToId ax
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder [Result.Diag
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diagKind = Result.Error
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagString =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Definition of proposition " ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder show (pretty ax) ++
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder " after first axiom"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos = AS_Anno.opt_pos x
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder })
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (AS_BASIC.AxiomItems _) -> TestSig { msign = msign tsig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , occurence = occ + 1
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , tdiagnosis = tdiagnosis tsig ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder [Result.Diag
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diagKind = Result.Hint
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagString =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "First axiom"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_Anno.opt_pos x
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieve the formulas out of a basic spec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermakeFormulas ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.BASICSPEC
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> [DIAGFORM]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeFormulas (AS_BASIC.BasicSpec bspec) sig =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Helper for makeFormulas
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveFormulaItem ::
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder [DIAGFORM]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> AS_Anno.Annoted AS_BASIC.BASICITEMS
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> [DIAGFORM]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederretrieveFormulaItem axs x sig =
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder case AS_Anno.item x of
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (AS_BASIC.PredDecl _) -> axs
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (AS_BASIC.AxiomItems ax) ->
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Number formulae
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedernumberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUMFORM]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedernumberFormulae [] _ = []
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedernumberFormulae (x : xs) i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | label == "" =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | otherwise =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder label = AS_Anno.getRLabel x
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder-- Add a formula to a named list of formulas
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederaddFormula :: [DIAGFORM]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> NUMFORM
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> [DIAGFORM]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederaddFormula formulae nf sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | isLegal = formulae ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder [DiagForm
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula = makeNamed f i
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , diagnosis = Result.Diag
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.diagKind = Result.Hint
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.diagString = "All fine"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos = lnum
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder | otherwise = formulae ++
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder [DiagForm
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formula = makeNamed f i
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , diagnosis = Result.Diag
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.diagKind = Result.Error
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagString =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Unknown propositions "
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ++ show (pretty difference)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ " in formula "
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ++ show (pretty nakedFormula)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos = lnum
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder f = nfformula nf
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder i = nfnum nf
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder nakedFormula = AS_Anno.item f
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder varsOfFormula = propsOfFormula nakedFormula
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isLegal = Sign.isSubSigOf varsOfFormula sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder difference = Sign.sigDiff varsOfFormula sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder lnum = AS_Anno.opt_pos f
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- generates a named formula
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermakeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> AS_Anno.Named AS_BASIC.FORMULA
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermakeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder else label) $ AS_Anno.item f)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder { AS_Anno.isAxiom = not isTheorem }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder label = AS_Anno.getRLabel f
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder annos = AS_Anno.r_annos f
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder isTheorem = isImplies || isImplied
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Retrives the signature of a formula
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederpropsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederpropsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula form1)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (propsOfFormula form2)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula form1)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (propsOfFormula form2)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.TrueAtom _) = Sign.emptySig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.FalseAtom _) = Sign.emptySig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Predication x) = Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder {Sign.items = Set.singleton $
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Id.simpleIdToId x }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder Sign.emptySig xs
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder Sign.emptySig xs
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.ForAll xs f _) = sigDiff
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula f)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederpropsOfFormula (AS_BASIC.Exists xs f _) = sigDiff
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (propsOfFormula f)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- Basic analysis for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederbasicPropositionalAnalysis
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder :: (AS_BASIC.BASICSPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder -> Result.Result (AS_BASIC.BASICSPEC,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ExtSign Sign.Sign Symbol.Symbol,
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder [AS_Anno.Named AS_BASIC.FORMULA])
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederbasicPropositionalAnalysis (bs, sig, _) =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.Result diags $ if exErrs then Nothing else
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Just (bs, ExtSign sigItems declaredSyms, formulae)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder where
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder bsSig = makeSig bs sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder sigItems = msign bsSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder declaredSyms = Set.map Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder $ Set.difference (items sigItems) $ items sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder bsForm = makeFormulas bs sigItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder formulae = map formula bsForm
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder diags = map diagnosis bsForm ++ tdiagnosis bsSig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder exErrs = Result.hasErrors diags
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Static analysis for symbol maps
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermkStatSymbMapItem xs =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.diags = []
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.maybeResult = Just $
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder foldl
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \ smap x ->
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder case x of
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.SymbMapItems sitem _ ->
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Map.union smap $ statSymbMapItem sitem
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder )
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Map.empty
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder xs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbMapItem :: [AS_BASIC.SYMBORMAP]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Map.Map Symbol.Symbol Symbol.Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbMapItem =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder foldl
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder \ mmap x ->
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder case x of
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.Symb sym -> Map.insert
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (symbToSymbol sym)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (symbToSymbol sym) mmap
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.SymbMap s1 s2 _
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder )
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Map.empty
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Retrieve raw symbols
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedermkStatSymbItems :: [AS_BASIC.SYMBITEMS] -> Result.Result [Symbol.Symbol]
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermkStatSymbItems a = Result.Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.diags = []
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.maybeResult = Just $ statSymbItems a
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbItems :: [AS_BASIC.SYMBITEMS] -> [Symbol.Symbol]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroederstatSymbItems = concatMap symbItemsToSymbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbItemsToSymbol :: AS_BASIC.SYMBITEMS -> [Symbol.Symbol]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbItemsToSymbol (AS_BASIC.SymbItems syms _) = map symbToSymbol syms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersymbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von SchroedersymbToSymbol (AS_BASIC.SymbId tok) =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
ba06b25b69be05a4733db7197940efd73976f215Jonathan von SchroederpMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Set.Set Id.Id
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder -> Map.Map Id.Id Id.Id
ba06b25b69be05a4733db7197940efd73976f215Jonathan von SchroederpMap imap =
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder Set.fold (
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder \ x ->
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder let
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder symOf = Symbol.Symbol
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder { Symbol.symName = x }
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder y = Symbol.symName
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder $ Symbol.applySymMap imap symOf
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder in Map.insert x y
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder ) Map.empty
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Induce a signature morphism from a source signature and a raw symbol map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Sign.Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result Morphism.Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromMorphism imap sig =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.Result
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Result.diags = []
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , Result.maybeResult =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sigItems = Sign.items sig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder in
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Just
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism.Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Morphism.source = sig
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder , Morphism.propMap = pMap imap sigItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Morphism.target = Sign.Sign
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder {Sign.items =
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder Set.map (Morphism.applyMap
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (pMap imap sigItems))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder $ Sign.items sig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Induce a signature morphism from a source signature and a raw symbol map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> ExtSign Sign.Sign Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> ExtSign Sign.Sign Symbol.Symbol
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result Morphism.Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder sigItems = Sign.items sig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder targetSig = Sign.Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {Sign.items =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Set.map
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (Morphism.applyMap
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder (pMap imap sigItems))
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder $ Sign.items sig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder isSub = Sign.items targetSig
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder `Set.isSubsetOf`
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Sign.items tSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder in
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder if isSub then
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.Result {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diags = []
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.maybeResult =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Just Morphism.Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Morphism.source = sig
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder , Morphism.propMap = pMap imap sigItems
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Morphism.target = tSig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder else
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.Result {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diags =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder [
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.Diag
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder {
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Result.diagKind = Result.Error
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagString =
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder "Incompatible mapping"
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.diagPos = Id.nullRange
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder }
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder ]
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder , Result.maybeResult = Nothing
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersignatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedersignatureColimit graph = do
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder let graph1 = nmap Sign.items $ emap (Control.Arrow.second Morphism.propMap)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder graph
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (set, maps) = addIntToSymbols $ computeColimitSet graph1
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder cSig = Sign.Sign {Sign.items = set}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder return (cSig,
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder Map.fromList $ map (\ (i, n) ->
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (i, Morphism.Morphism {
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism.source = n,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism.target = cSig,
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Morphism.propMap = maps Map.! i
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder })) $ labNodes graph)