{- |
Module      :  ./QBF/Analysis.hs
Description :  Basic analysis for propositional logic extended with QBFs
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

Basic and static analysis for propositional logic

  Ref.
  <http://en.wikipedia.org/wiki/Propositional_logic>
  <http://www.voronkov.com/lics.cgi>
-}

module QBF.Analysis
    (
     basicPropositionalAnalysis
    , mkStatSymbItems
    , mkStatSymbMapItem
    , inducedFromMorphism
    , inducedFromToMorphism
    , signatureColimit
    )
    where

import Common.ExtSign
import Common.Lib.Graph
import Common.SetColimit
import Data.Graph.Inductive.Graph
import Propositional.Sign as Sign
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.GlobalAnnotations as GlobalAnnos
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Morphism as Morphism
import qualified QBF.Symbol as Symbol
import Control.Arrow

-- | Datatype for formulas with diagnosis data
data DIAGFORM = DiagForm
    {
      DIAGFORM -> Named FORMULA
formula :: AS_Anno.Named AS_BASIC.FORMULA,
      DIAGFORM -> Diagnosis
diagnosis :: Result.Diagnosis
    }

-- | Formula annotated with a number
data NUMFORM = NumForm
    {
      NUMFORM -> Annoted FORMULA
nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
    , NUMFORM -> Integer
nfnum :: Integer
    }

data TESTSIG = TestSig
    {
      TESTSIG -> Sign
msign :: Sign.Sign
    , TESTSIG -> Int
occurence :: Int
    , TESTSIG -> [Diagnosis]
tdiagnosis :: [Result.Diagnosis]
    }

-- | Retrieves the signature out of a basic spec
makeSig ::
    AS_BASIC.BASICSPEC                   -- Input SPEC
    -> Sign.Sign                         -- Input Signature
    -> TESTSIG                           -- Output Signature
makeSig :: BASICSPEC -> Sign -> TESTSIG
makeSig (AS_BASIC.BasicSpec spec :: [Annoted BASICITEMS]
spec) sig :: Sign
sig = (TESTSIG -> Annoted BASICITEMS -> TESTSIG)
-> TESTSIG -> [Annoted BASICITEMS] -> TESTSIG
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl TESTSIG -> Annoted BASICITEMS -> TESTSIG
retrieveBasicItem
                                         TestSig :: Sign -> Int -> [Diagnosis] -> TESTSIG
TestSig { msign :: Sign
msign = Sign
sig
                                                 , occurence :: Int
occurence = 0
                                                 , tdiagnosis :: [Diagnosis]
tdiagnosis = []
                                                 }
                                         [Annoted BASICITEMS]
spec

-- Helper for makeSig
retrieveBasicItem ::
    TESTSIG                                      -- Input Signature
    -> AS_Anno.Annoted AS_BASIC.BASICITEMS      -- Input Item
    -> TESTSIG                                   -- Output Signature
retrieveBasicItem :: TESTSIG -> Annoted BASICITEMS -> TESTSIG
retrieveBasicItem tsig :: TESTSIG
tsig x :: Annoted BASICITEMS
x =
    let
        occ :: Int
occ = TESTSIG -> Int
occurence TESTSIG
tsig
    in
    case Annoted BASICITEMS -> BASICITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASICITEMS
x of
      (AS_BASIC.PredDecl apred :: PREDITEM
apred) ->
          if Int
occ Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
          then
              (TESTSIG -> SIMPLE_ID -> TESTSIG)
-> TESTSIG -> [SIMPLE_ID] -> TESTSIG
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl
                      (\ asig :: TESTSIG
asig ax :: SIMPLE_ID
ax -> TestSig :: Sign -> Int -> [Diagnosis] -> TESTSIG
TestSig {
                                   msign :: Sign
msign = Sign -> Id -> Sign
Sign.addToSig (TESTSIG -> Sign
msign TESTSIG
asig)
                                            (Id -> Sign) -> Id -> Sign
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> Id
Id.simpleIdToId SIMPLE_ID
ax
                                 , occurence :: Int
occurence = Int
occ
                                 , tdiagnosis :: [Diagnosis]
tdiagnosis = TESTSIG -> [Diagnosis]
tdiagnosis TESTSIG
tsig [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
                                   [Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                                    {
                                      diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Hint
                                    , diagString :: String
Result.diagString = "All fine"
                                    , diagPos :: Range
Result.diagPos = Annoted BASICITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASICITEMS
x
                                    }]
                                 })
                      TESTSIG
tsig ([SIMPLE_ID] -> TESTSIG) -> [SIMPLE_ID] -> TESTSIG
forall a b. (a -> b) -> a -> b
$ (\ (AS_BASIC.PredItem xs :: [SIMPLE_ID]
xs _) -> [SIMPLE_ID]
xs) PREDITEM
apred
          else
              (TESTSIG -> SIMPLE_ID -> TESTSIG)
-> TESTSIG -> [SIMPLE_ID] -> TESTSIG
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl
                      (\ asig :: TESTSIG
asig ax :: SIMPLE_ID
ax -> TestSig :: Sign -> Int -> [Diagnosis] -> TESTSIG
TestSig {
                                   msign :: Sign
msign = Sign -> Id -> Sign
Sign.addToSig (TESTSIG -> Sign
msign TESTSIG
asig)
                                            (Id -> Sign) -> Id -> Sign
forall a b. (a -> b) -> a -> b
$ SIMPLE_ID -> Id
Id.simpleIdToId SIMPLE_ID
ax
                                 , occurence :: Int
occurence = Int
occ
                                 , tdiagnosis :: [Diagnosis]
tdiagnosis = TESTSIG -> [Diagnosis]
tdiagnosis TESTSIG
tsig [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
                                   [Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                                    {
                                      diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
                                    , diagString :: String
Result.diagString =
                                              "Definition of proposition " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                              Doc -> String
forall a. Show a => a -> String
show (SIMPLE_ID -> Doc
forall a. Pretty a => a -> Doc
pretty SIMPLE_ID
ax) String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                              " after first axiom"
                                    , diagPos :: Range
Result.diagPos = Annoted BASICITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASICITEMS
x
                                    }]
                                 })
                          TESTSIG
tsig ([SIMPLE_ID] -> TESTSIG) -> [SIMPLE_ID] -> TESTSIG
forall a b. (a -> b) -> a -> b
$ (\ (AS_BASIC.PredItem xs :: [SIMPLE_ID]
xs _) -> [SIMPLE_ID]
xs) PREDITEM
apred
      (AS_BASIC.AxiomItems _) -> TestSig :: Sign -> Int -> [Diagnosis] -> TESTSIG
TestSig { msign :: Sign
msign = TESTSIG -> Sign
msign TESTSIG
tsig
                                          , occurence :: Int
occurence = Int
occ Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
                                          , tdiagnosis :: [Diagnosis]
tdiagnosis = TESTSIG -> [Diagnosis]
tdiagnosis TESTSIG
tsig [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
                                              [Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                                               {
                                                 diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Hint
                                               , diagString :: String
Result.diagString =
                                                         "First axiom"
                                               , diagPos :: Range
Result.diagPos =
                                                         Annoted BASICITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASICITEMS
x
                                               }]
                                            }

-- | Retrieve the formulas out of a basic spec
makeFormulas ::
    AS_BASIC.BASICSPEC
    -> Sign.Sign
    -> [DIAGFORM]
makeFormulas :: BASICSPEC -> Sign -> [DIAGFORM]
makeFormulas (AS_BASIC.BasicSpec bspec :: [Annoted BASICITEMS]
bspec) sig :: Sign
sig =
    ([DIAGFORM] -> Annoted BASICITEMS -> [DIAGFORM])
-> [DIAGFORM] -> [Annoted BASICITEMS] -> [DIAGFORM]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl (\ xs :: [DIAGFORM]
xs bs :: Annoted BASICITEMS
bs -> [DIAGFORM] -> Annoted BASICITEMS -> Sign -> [DIAGFORM]
retrieveFormulaItem [DIAGFORM]
xs Annoted BASICITEMS
bs Sign
sig) [] [Annoted BASICITEMS]
bspec

-- Helper for makeFormulas
retrieveFormulaItem ::
    [DIAGFORM]
    -> AS_Anno.Annoted AS_BASIC.BASICITEMS
    -> Sign.Sign
    -> [DIAGFORM]
retrieveFormulaItem :: [DIAGFORM] -> Annoted BASICITEMS -> Sign -> [DIAGFORM]
retrieveFormulaItem axs :: [DIAGFORM]
axs x :: Annoted BASICITEMS
x sig :: Sign
sig =
    case Annoted BASICITEMS -> BASICITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASICITEMS
x of
      (AS_BASIC.PredDecl _) -> [DIAGFORM]
axs
      (AS_BASIC.AxiomItems ax :: [Annoted FORMULA]
ax) ->
          ([DIAGFORM] -> NUMFORM -> [DIAGFORM])
-> [DIAGFORM] -> [NUMFORM] -> [DIAGFORM]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl (\ xs :: [DIAGFORM]
xs bs :: NUMFORM
bs -> [DIAGFORM] -> NUMFORM -> Sign -> [DIAGFORM]
addFormula [DIAGFORM]
xs NUMFORM
bs Sign
sig) [DIAGFORM]
axs ([NUMFORM] -> [DIAGFORM]) -> [NUMFORM] -> [DIAGFORM]
forall a b. (a -> b) -> a -> b
$ [Annoted FORMULA] -> Integer -> [NUMFORM]
numberFormulae [Annoted FORMULA]
ax 0

-- Number formulae
numberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUMFORM]
numberFormulae :: [Annoted FORMULA] -> Integer -> [NUMFORM]
numberFormulae [] _ = []
numberFormulae (x :: Annoted FORMULA
x : xs :: [Annoted FORMULA]
xs) i :: Integer
i
    | String
label String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" =
       NumForm :: Annoted FORMULA -> Integer -> NUMFORM
NumForm {nfformula :: Annoted FORMULA
nfformula = Annoted FORMULA
x, nfnum :: Integer
nfnum = Integer
i} NUMFORM -> [NUMFORM] -> [NUMFORM]
forall a. a -> [a] -> [a]
: [Annoted FORMULA] -> Integer -> [NUMFORM]
numberFormulae [Annoted FORMULA]
xs (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
    | Bool
otherwise =
       NumForm :: Annoted FORMULA -> Integer -> NUMFORM
NumForm {nfformula :: Annoted FORMULA
nfformula = Annoted FORMULA
x, nfnum :: Integer
nfnum = 0} NUMFORM -> [NUMFORM] -> [NUMFORM]
forall a. a -> [a] -> [a]
: [Annoted FORMULA] -> Integer -> [NUMFORM]
numberFormulae [Annoted FORMULA]
xs Integer
i
    where
      label :: String
label = Annoted FORMULA -> String
forall a. Annoted a -> String
AS_Anno.getRLabel Annoted FORMULA
x

-- Add a formula to a named list of formulas
addFormula :: [DIAGFORM]
           -> NUMFORM
           -> Sign.Sign
           -> [DIAGFORM]
addFormula :: [DIAGFORM] -> NUMFORM -> Sign -> [DIAGFORM]
addFormula formulae :: [DIAGFORM]
formulae nf :: NUMFORM
nf sign :: Sign
sign
    | Bool
isLegal = [DIAGFORM]
formulae [DIAGFORM] -> [DIAGFORM] -> [DIAGFORM]
forall a. [a] -> [a] -> [a]
++
                        [DiagForm :: Named FORMULA -> Diagnosis -> DIAGFORM
DiagForm
                         {
                           formula :: Named FORMULA
formula = Annoted FORMULA -> Integer -> Named FORMULA
makeNamed Annoted FORMULA
f Integer
i
                         , diagnosis :: Diagnosis
diagnosis = Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                           {
                             diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Hint
                           , diagString :: String
Result.diagString = "All fine"
                           , diagPos :: Range
Result.diagPos = Range
lnum
                           }
                         }]
    | Bool
otherwise = [DIAGFORM]
formulae [DIAGFORM] -> [DIAGFORM] -> [DIAGFORM]
forall a. [a] -> [a] -> [a]
++
                        [DiagForm :: Named FORMULA -> Diagnosis -> DIAGFORM
DiagForm
                         {
                           formula :: Named FORMULA
formula = Annoted FORMULA -> Integer -> Named FORMULA
makeNamed Annoted FORMULA
f Integer
i
                         , diagnosis :: Diagnosis
diagnosis = Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                                       {
                                         diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
                                       , diagString :: String
Result.diagString =
                                                 "Unknown propositions "
                                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
difference)
                                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ " in formula "
                                         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty FORMULA
nakedFormula)
                                       , diagPos :: Range
Result.diagPos = Range
lnum
                                       }
                         }]
    where
      f :: Annoted FORMULA
f = NUMFORM -> Annoted FORMULA
nfformula NUMFORM
nf
      i :: Integer
i = NUMFORM -> Integer
nfnum NUMFORM
nf
      nakedFormula :: FORMULA
nakedFormula = Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item Annoted FORMULA
f
      varsOfFormula :: Sign
varsOfFormula = FORMULA -> Sign
propsOfFormula FORMULA
nakedFormula
      isLegal :: Bool
isLegal = Sign -> Sign -> Bool
Sign.isSubSigOf Sign
varsOfFormula Sign
sign
      difference :: Sign
difference = Sign -> Sign -> Sign
Sign.sigDiff Sign
varsOfFormula Sign
sign
      lnum :: Range
lnum = Annoted FORMULA -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted FORMULA
f

-- generates a named formula
makeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
              -> AS_Anno.Named AS_BASIC.FORMULA
makeNamed :: Annoted FORMULA -> Integer -> Named FORMULA
makeNamed f :: Annoted FORMULA
f i :: Integer
i = (String -> FORMULA -> Named FORMULA
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed (if String
label String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "" then "Ax_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i
                                       else String
label) (FORMULA -> Named FORMULA) -> FORMULA -> Named FORMULA
forall a b. (a -> b) -> a -> b
$ Annoted FORMULA -> FORMULA
forall a. Annoted a -> a
AS_Anno.item Annoted FORMULA
f)
                    { isAxiom :: Bool
AS_Anno.isAxiom = Bool -> Bool
not Bool
isTheorem }
    where
      label :: String
label = Annoted FORMULA -> String
forall a. Annoted a -> String
AS_Anno.getRLabel Annoted FORMULA
f
      annos :: [Annotation]
annos = Annoted FORMULA -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted FORMULA
f
      isImplies :: Bool
isImplies = (Bool -> Annotation -> Bool) -> Bool -> [Annotation] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ y :: Bool
y x :: Annotation
x -> Annotation -> Bool
AS_Anno.isImplies Annotation
x Bool -> Bool -> Bool
|| Bool
y) Bool
False [Annotation]
annos
      isImplied :: Bool
isImplied = (Bool -> Annotation -> Bool) -> Bool -> [Annotation] -> Bool
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ y :: Bool
y x :: Annotation
x -> Annotation -> Bool
AS_Anno.isImplied Annotation
x Bool -> Bool -> Bool
|| Bool
y) Bool
False [Annotation]
annos
      isTheorem :: Bool
isTheorem = Bool
isImplies Bool -> Bool -> Bool
|| Bool
isImplied

-- Retrives the signature of a formula
propsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
propsOfFormula :: FORMULA -> Sign
propsOfFormula (AS_BASIC.Negation form :: FORMULA
form _) = FORMULA -> Sign
propsOfFormula FORMULA
form
propsOfFormula (AS_BASIC.Implication form1 :: FORMULA
form1 form2 :: FORMULA
form2 _) = Sign -> Sign -> Sign
Sign.unite
                                           (FORMULA -> Sign
propsOfFormula FORMULA
form1)
                                           (FORMULA -> Sign
propsOfFormula FORMULA
form2)
propsOfFormula (AS_BASIC.Equivalence form1 :: FORMULA
form1 form2 :: FORMULA
form2 _) = Sign -> Sign -> Sign
Sign.unite
                                           (FORMULA -> Sign
propsOfFormula FORMULA
form1)
                                           (FORMULA -> Sign
propsOfFormula FORMULA
form2)
propsOfFormula (AS_BASIC.TrueAtom _) = Sign
Sign.emptySig
propsOfFormula (AS_BASIC.FalseAtom _) = Sign
Sign.emptySig
propsOfFormula (AS_BASIC.Predication x :: SIMPLE_ID
x) = Sign :: Set Id -> Sign
Sign.Sign
                         {items :: Set Id
Sign.items = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$
                                       SIMPLE_ID -> Id
Id.simpleIdToId SIMPLE_ID
x }
propsOfFormula (AS_BASIC.Conjunction xs :: [FORMULA]
xs _) = (Sign -> FORMULA -> Sign) -> Sign -> [FORMULA] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl
 (\ sig :: Sign
sig frm :: FORMULA
frm -> Sign -> Sign -> Sign
Sign.unite Sign
sig (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ FORMULA -> Sign
propsOfFormula FORMULA
frm)
 Sign
Sign.emptySig [FORMULA]
xs
propsOfFormula (AS_BASIC.Disjunction xs :: [FORMULA]
xs _) = (Sign -> FORMULA -> Sign) -> Sign -> [FORMULA] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl
 (\ sig :: Sign
sig frm :: FORMULA
frm -> Sign -> Sign -> Sign
Sign.unite Sign
sig (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ FORMULA -> Sign
propsOfFormula FORMULA
frm)
 Sign
Sign.emptySig [FORMULA]
xs
propsOfFormula (AS_BASIC.ForAll xs :: [SIMPLE_ID]
xs f :: FORMULA
f _) = Sign -> Sign -> Sign
sigDiff
                         (FORMULA -> Sign
propsOfFormula FORMULA
f)
                         (Set Id -> Sign
Sign.Sign ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ((SIMPLE_ID -> Id) -> [SIMPLE_ID] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> Id
Id.simpleIdToId [SIMPLE_ID]
xs)))
propsOfFormula (AS_BASIC.Exists xs :: [SIMPLE_ID]
xs f :: FORMULA
f _) = Sign -> Sign -> Sign
sigDiff
                         (FORMULA -> Sign
propsOfFormula FORMULA
f)
                         (Set Id -> Sign
Sign.Sign ([Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList ((SIMPLE_ID -> Id) -> [SIMPLE_ID] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> Id
Id.simpleIdToId [SIMPLE_ID]
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 :: (BASICSPEC, Sign, GlobalAnnos)
-> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
basicPropositionalAnalysis (bs :: BASICSPEC
bs, sig :: Sign
sig, _) =
   [Diagnosis]
-> Maybe (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diags (Maybe (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
 -> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a b. (a -> b) -> a -> b
$ if Bool
exErrs then Maybe (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. Maybe a
Nothing else
     (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Maybe (BASICSPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. a -> Maybe a
Just (BASICSPEC
bs, Sign -> Set Symbol -> ExtSign Sign Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign Sign
sigItems Set Symbol
declaredSyms, [Named FORMULA]
formulae)
    where
      bsSig :: TESTSIG
bsSig = BASICSPEC -> Sign -> TESTSIG
makeSig BASICSPEC
bs Sign
sig
      sigItems :: Sign
sigItems = TESTSIG -> Sign
msign TESTSIG
bsSig
      declaredSyms :: Set Symbol
declaredSyms = (Id -> Symbol) -> Set Id -> Set Symbol
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Symbol
Symbol.Symbol
        (Set Id -> Set Symbol) -> Set Id -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
items Sign
sigItems) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
sig
      bsForm :: [DIAGFORM]
bsForm = BASICSPEC -> Sign -> [DIAGFORM]
makeFormulas BASICSPEC
bs Sign
sigItems
      formulae :: [Named FORMULA]
formulae = (DIAGFORM -> Named FORMULA) -> [DIAGFORM] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map DIAGFORM -> Named FORMULA
formula [DIAGFORM]
bsForm
      diags :: [Diagnosis]
diags = (DIAGFORM -> Diagnosis) -> [DIAGFORM] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map DIAGFORM -> Diagnosis
diagnosis [DIAGFORM]
bsForm [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ TESTSIG -> [Diagnosis]
tdiagnosis TESTSIG
bsSig
      exErrs :: Bool
exErrs = [Diagnosis] -> Bool
Result.hasErrors [Diagnosis]
diags

-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
                  -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem :: [SYMBMAPITEMS] -> Result (Map Symbol Symbol)
mkStatSymbMapItem xs :: [SYMBMAPITEMS]
xs =
    Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result
    {
      diags :: [Diagnosis]
Result.diags = []
    , maybeResult :: Maybe (Map Symbol Symbol)
Result.maybeResult = Map Symbol Symbol -> Maybe (Map Symbol Symbol)
forall a. a -> Maybe a
Just (Map Symbol Symbol -> Maybe (Map Symbol Symbol))
-> Map Symbol Symbol -> Maybe (Map Symbol Symbol)
forall a b. (a -> b) -> a -> b
$
                           (Map Symbol Symbol -> SYMBMAPITEMS -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMBMAPITEMS] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                           (
                            \ smap :: Map Symbol Symbol
smap x :: SYMBMAPITEMS
x ->
                                case SYMBMAPITEMS
x of
                                  AS_BASIC.SymbMapItems sitem :: [SYMBORMAP]
sitem _ ->
                                       Map Symbol Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Symbol Symbol
smap (Map Symbol Symbol -> Map Symbol Symbol)
-> Map Symbol Symbol -> Map Symbol Symbol
forall a b. (a -> b) -> a -> b
$ [SYMBORMAP] -> Map Symbol Symbol
statSymbMapItem [SYMBORMAP]
sitem
                           )
                           Map Symbol Symbol
forall k a. Map k a
Map.empty
                           [SYMBMAPITEMS]
xs
    }

statSymbMapItem :: [AS_BASIC.SYMBORMAP]
                 -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem :: [SYMBORMAP] -> Map Symbol Symbol
statSymbMapItem =
    (Map Symbol Symbol -> SYMBORMAP -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMBORMAP] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
    (
     \ mmap :: Map Symbol Symbol
mmap x :: SYMBORMAP
x ->
         case SYMBORMAP
x of
           AS_BASIC.Symb sym :: SYMB
sym -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert
                                     (SYMB -> Symbol
symbToSymbol SYMB
sym)
                                     (SYMB -> Symbol
symbToSymbol SYMB
sym) Map Symbol Symbol
mmap
           AS_BASIC.SymbMap s1 :: SYMB
s1 s2 :: SYMB
s2 _
             -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SYMB -> Symbol
symbToSymbol SYMB
s1) (SYMB -> Symbol
symbToSymbol SYMB
s2) Map Symbol Symbol
mmap
    )
    Map Symbol Symbol
forall k a. Map k a
Map.empty

-- | Retrieve raw symbols
mkStatSymbItems :: [AS_BASIC.SYMBITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems :: [SYMBITEMS] -> Result [Symbol]
mkStatSymbItems a :: [SYMBITEMS]
a = Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result
                    {
                      diags :: [Diagnosis]
Result.diags = []
                    , maybeResult :: Maybe [Symbol]
Result.maybeResult = [Symbol] -> Maybe [Symbol]
forall a. a -> Maybe a
Just ([Symbol] -> Maybe [Symbol]) -> [Symbol] -> Maybe [Symbol]
forall a b. (a -> b) -> a -> b
$ [SYMBITEMS] -> [Symbol]
statSymbItems [SYMBITEMS]
a
                    }

statSymbItems :: [AS_BASIC.SYMBITEMS] -> [Symbol.Symbol]
statSymbItems :: [SYMBITEMS] -> [Symbol]
statSymbItems = (SYMBITEMS -> [Symbol]) -> [SYMBITEMS] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SYMBITEMS -> [Symbol]
symbItemsToSymbol

symbItemsToSymbol :: AS_BASIC.SYMBITEMS -> [Symbol.Symbol]
symbItemsToSymbol :: SYMBITEMS -> [Symbol]
symbItemsToSymbol (AS_BASIC.SymbItems syms :: [SYMB]
syms _) = (SYMB -> Symbol) -> [SYMB] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map SYMB -> Symbol
symbToSymbol [SYMB]
syms

symbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
symbToSymbol :: SYMB -> Symbol
symbToSymbol (AS_BASIC.SymbId tok :: SIMPLE_ID
tok) =
    Symbol :: Id -> Symbol
Symbol.Symbol {symName :: Id
Symbol.symName = SIMPLE_ID -> Id
Id.simpleIdToId SIMPLE_ID
tok}

pMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Set.Set Id.Id
         -> Map.Map Id.Id Id.Id
pMap :: Map Symbol Symbol -> Set Id -> Map Id Id
pMap imap :: Map Symbol Symbol
imap =
 (Id -> Map Id Id -> Map Id Id) -> Map Id Id -> Set Id -> Map Id Id
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (
  \ x :: Id
x ->
    let
        symOf :: Symbol
symOf = Symbol :: Id -> Symbol
Symbol.Symbol
                 { symName :: Id
Symbol.symName = Id
x }
        y :: Id
y = Symbol -> Id
Symbol.symName
             (Symbol -> Id) -> Symbol -> Id
forall a b. (a -> b) -> a -> b
$ Map Symbol Symbol -> Symbol -> Symbol
Symbol.applySymMap Map Symbol Symbol
imap Symbol
symOf
    in Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
x Id
y
 ) Map Id Id
forall k a. Map k a
Map.empty

-- | 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 :: Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism imap :: Map Symbol Symbol
imap sig :: Sign
sig =
    Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result
          {
            diags :: [Diagnosis]
Result.diags = []
          , maybeResult :: Maybe Morphism
Result.maybeResult =
              let
                  sigItems :: Set Id
sigItems = Sign -> Set Id
Sign.items Sign
sig
              in
              Morphism -> Maybe Morphism
forall a. a -> Maybe a
Just
              Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism
                          {
                            source :: Sign
Morphism.source = Sign
sig
                          , propMap :: Map Id Id
Morphism.propMap = Map Symbol Symbol -> Set Id -> Map Id Id
pMap Map Symbol Symbol
imap Set Id
sigItems
                          , target :: Sign
Morphism.target = Sign :: Set Id -> Sign
Sign.Sign
                                      {items :: Set Id
Sign.items =
                                             (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
Morphism.applyMap
                                              (Map Symbol Symbol -> Set Id -> Map Id Id
pMap Map Symbol Symbol
imap Set Id
sigItems))
                                                  (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.items Sign
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 :: Map Symbol Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism imap :: Map Symbol Symbol
imap (ExtSign sig :: Sign
sig _) (ExtSign tSig :: Sign
tSig _) =
              let
                  sigItems :: Set Id
sigItems = Sign -> Set Id
Sign.items Sign
sig
                  targetSig :: Sign
targetSig = Sign :: Set Id -> Sign
Sign.Sign
                                               {items :: Set Id
Sign.items =
                                                    (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map
                                                       (Map Id Id -> Id -> Id
Morphism.applyMap
                                                        (Map Symbol Symbol -> Set Id -> Map Id Id
pMap Map Symbol Symbol
imap Set Id
sigItems))
                                                       (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.items Sign
sig
                                               }
                  isSub :: Bool
isSub = Sign -> Set Id
Sign.items Sign
targetSig
                           Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf`
                          Sign -> Set Id
Sign.items Sign
tSig
              in
                if Bool
isSub then
                     Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result {
                         diags :: [Diagnosis]
Result.diags = []
                         , maybeResult :: Maybe Morphism
Result.maybeResult =
                             Morphism -> Maybe Morphism
forall a. a -> Maybe a
Just Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism
                                 {
                                     source :: Sign
Morphism.source = Sign
sig
                                     , propMap :: Map Id Id
Morphism.propMap = Map Symbol Symbol -> Set Id -> Map Id Id
pMap Map Symbol Symbol
imap Set Id
sigItems
                                     , target :: Sign
Morphism.target = Sign
tSig
                                 }
                     }
                else
                    Result :: forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result {
                        diags :: [Diagnosis]
Result.diags =
                            [
                                Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
                                    {
                                        diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
                                        , diagString :: String
Result.diagString =
                                                 "Incompatible mapping"
                                        , diagPos :: Range
Result.diagPos = Range
Id.nullRange
                                    }
                            ]
                        , maybeResult :: Maybe Morphism
Result.maybeResult = Maybe Morphism
forall a. Maybe a
Nothing
                    }

signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
                 -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signatureColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signatureColimit graph :: Gr Sign (Int, Morphism)
graph = do
 let graph1 :: Gr (Set Id) (Int, Map Id Id)
graph1 = (Sign -> Set Id)
-> Gr Sign (Int, Map Id Id) -> Gr (Set Id) (Int, Map Id Id)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign -> Set Id
Sign.items (Gr Sign (Int, Map Id Id) -> Gr (Set Id) (Int, Map Id Id))
-> Gr Sign (Int, Map Id Id) -> Gr (Set Id) (Int, Map Id Id)
forall a b. (a -> b) -> a -> b
$ ((Int, Morphism) -> (Int, Map Id Id))
-> Gr Sign (Int, Morphism) -> Gr Sign (Int, Map Id Id)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap ((Morphism -> Map Id Id) -> (Int, Morphism) -> (Int, Map Id Id)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
Control.Arrow.second Morphism -> Map Id Id
Morphism.propMap)
                                     Gr Sign (Int, Morphism)
graph
     (set :: Set Id
set, maps :: Map Int (Map Id Id)
maps) = (Set (Id, Int), Map Int (Map Id (Id, Int)))
-> (Set Id, Map Int (Map Id Id))
forall a.
SymbolName a =>
(Set (a, Int), Map Int (Map a (a, Int)))
-> (Set a, Map Int (Map a a))
addIntToSymbols ((Set (Id, Int), Map Int (Map Id (Id, Int)))
 -> (Set Id, Map Int (Map Id Id)))
-> (Set (Id, Int), Map Int (Map Id (Id, Int)))
-> (Set Id, Map Int (Map Id Id))
forall a b. (a -> b) -> a -> b
$ Gr (Set Id) (Int, Map Id Id)
-> (Set (Id, Int), Map Int (Map Id (Id, Int)))
forall a.
Ord a =>
Gr (Set a) (Int, Map a a)
-> (Set (a, Int), Map Int (Map a (a, Int)))
computeColimitSet Gr (Set Id) (Int, Map Id Id)
graph1
     cSig :: Sign
cSig = Sign :: Set Id -> Sign
Sign.Sign {items :: Set Id
Sign.items = Set Id
set}
 (Sign, Map Int Morphism) -> Result (Sign, Map Int Morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
cSig,
         [(Int, Morphism)] -> Map Int Morphism
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Morphism)] -> Map Int Morphism)
-> [(Int, Morphism)] -> Map Int Morphism
forall a b. (a -> b) -> a -> b
$ ((Int, Sign) -> (Int, Morphism))
-> [(Int, Sign)] -> [(Int, Morphism)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i, n :: Sign
n) ->
                              (Int
i, Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism {
                                    source :: Sign
Morphism.source = Sign
n,
                                    target :: Sign
Morphism.target = Sign
cSig,
                                    propMap :: Map Id Id
Morphism.propMap = Map Int (Map Id Id)
maps Map Int (Map Id Id) -> Int -> Map Id Id
forall k a. Ord k => Map k a -> k -> a
Map.! Int
i
                                  })) ([(Int, Sign)] -> [(Int, Morphism)])
-> [(Int, Sign)] -> [(Int, Morphism)]
forall a b. (a -> b) -> a -> b
$ Gr Sign (Int, Morphism) -> [(Int, Sign)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes Gr Sign (Int, Morphism)
graph)