{- |
Module      :  ./Propositional/Analysis.hs
Description :  Basic analysis for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Basic and static analysis for propositional logic

  Ref.
  <http://en.wikipedia.org/wiki/Propositional_logic>
-}

module Propositional.Analysis
    ( basicPropositionalAnalysis
    , mkStatSymbItems
    , mkStatSymbMapItem
    , inducedFromMorphism
    , inducedFromToMorphism
    , signatureColimit
    , pROPsen_analysis
    )
    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 Control.Monad.Fail as Fail
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
import qualified Propositional.Morphism as Morphism
import qualified Propositional.Symbol as Symbol

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

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

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

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

-- Helper for makeSig
retrieveBasicItem ::
    TEST_SIG                                      -- Input Signature
    -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS       -- Input Item
    -> TEST_SIG                                   -- Output Signature
retrieveBasicItem :: TEST_SIG -> Annoted BASIC_ITEMS -> TEST_SIG
retrieveBasicItem tsig :: TEST_SIG
tsig x :: Annoted BASIC_ITEMS
x =
    let
        occ :: Int
occ = TEST_SIG -> Int
occurence TEST_SIG
tsig
        nocc :: Bool
nocc = Int
occ Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
    in
    case Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASIC_ITEMS
x of
      AS_BASIC.Pred_decl apred :: PRED_ITEM
apred -> (TEST_SIG -> SIMPLE_ID -> TEST_SIG)
-> TEST_SIG -> [SIMPLE_ID] -> TEST_SIG
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl (\ asig :: TEST_SIG
asig ax :: SIMPLE_ID
ax -> TestSig :: Sign -> Int -> [Diagnosis] -> TEST_SIG
TestSig
        { msign :: Sign
msign = Sign -> Id -> Sign
Sign.addToSig (TEST_SIG -> Sign
msign TEST_SIG
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 = TEST_SIG -> [Diagnosis]
tdiagnosis TEST_SIG
tsig [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
            [ Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
              { diagKind :: DiagKind
Result.diagKind = if Bool
nocc then DiagKind
Result.Hint else DiagKind
Result.Error
              , diagString :: String
Result.diagString = if Bool
nocc then "All fine" else
                 "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 BASIC_ITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASIC_ITEMS
x }]
        }) TEST_SIG
tsig ([SIMPLE_ID] -> TEST_SIG) -> [SIMPLE_ID] -> TEST_SIG
forall a b. (a -> b) -> a -> b
$ (\ (AS_BASIC.Pred_item xs :: [SIMPLE_ID]
xs _) -> [SIMPLE_ID]
xs) PRED_ITEM
apred
      AS_BASIC.Axiom_items _ -> TestSig :: Sign -> Int -> [Diagnosis] -> TEST_SIG
TestSig
        { msign :: Sign
msign = TEST_SIG -> Sign
msign TEST_SIG
tsig
        , occurence :: Int
occurence = Int
occ Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1
        , tdiagnosis :: [Diagnosis]
tdiagnosis = TEST_SIG -> [Diagnosis]
tdiagnosis TEST_SIG
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 BASIC_ITEMS -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted BASIC_ITEMS
x }]
        }

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

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

-- Number formulae
numberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUM_FORM]
numberFormulae :: [Annoted FORMULA] -> Integer -> [NUM_FORM]
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 -> NUM_FORM
NumForm {nfformula :: Annoted FORMULA
nfformula = Annoted FORMULA
x, nfnum :: Integer
nfnum = Integer
i}
                    NUM_FORM -> [NUM_FORM] -> [NUM_FORM]
forall a. a -> [a] -> [a]
: [Annoted FORMULA] -> Integer -> [NUM_FORM]
numberFormulae [Annoted FORMULA]
xs (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
    | Bool
otherwise = NumForm :: Annoted FORMULA -> Integer -> NUM_FORM
NumForm {nfformula :: Annoted FORMULA
nfformula = Annoted FORMULA
x, nfnum :: Integer
nfnum = 0} NUM_FORM -> [NUM_FORM] -> [NUM_FORM]
forall a. a -> [a] -> [a]
: [Annoted FORMULA] -> Integer -> [NUM_FORM]
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 :: [DIAG_FORM]
           -> NUM_FORM
           -> Sign.Sign
           -> [DIAG_FORM]
addFormula :: [DIAG_FORM] -> NUM_FORM -> Sign -> [DIAG_FORM]
addFormula formulae :: [DIAG_FORM]
formulae nf :: NUM_FORM
nf sign :: Sign
sign
    | Bool
isLegal = [DIAG_FORM]
formulae [DIAG_FORM] -> [DIAG_FORM] -> [DIAG_FORM]
forall a. [a] -> [a] -> [a]
++
                        [DiagForm :: Named FORMULA -> Diagnosis -> DIAG_FORM
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 = [DIAG_FORM]
formulae [DIAG_FORM] -> [DIAG_FORM] -> [DIAG_FORM]
forall a. [a] -> [a] -> [a]
++
                        [DiagForm :: Named FORMULA -> Diagnosis -> DIAG_FORM
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 = NUM_FORM -> Annoted FORMULA
nfformula NUM_FORM
nf
      i :: Integer
i = NUM_FORM -> Integer
nfnum NUM_FORM
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.True_atom _) = Sign
Sign.emptySig
propsOfFormula (AS_BASIC.False_atom _) = 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

-- Basic analysis for propositional logic
basicPropositionalAnalysis
  :: (AS_BASIC.BASIC_SPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
  -> Result.Result (AS_BASIC.BASIC_SPEC,
                    ExtSign Sign.Sign Symbol.Symbol,
                    [AS_Anno.Named AS_BASIC.FORMULA])
basicPropositionalAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
basicPropositionalAnalysis (bs :: BASIC_SPEC
bs, sig :: Sign
sig, _) =
   [Diagnosis]
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diags (Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA]))
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a b. (a -> b) -> a -> b
$ if Bool
exErrs then Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. Maybe a
Nothing else
     (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named FORMULA])
forall a. a -> Maybe a
Just (BASIC_SPEC
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 :: TEST_SIG
bsSig = BASIC_SPEC -> Sign -> TEST_SIG
makeSig BASIC_SPEC
bs Sign
sig
      sigItems :: Sign
sigItems = TEST_SIG -> Sign
msign TEST_SIG
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 :: [DIAG_FORM]
bsForm = BASIC_SPEC -> Sign -> [DIAG_FORM]
makeFormulas BASIC_SPEC
bs Sign
sigItems
      formulae :: [Named FORMULA]
formulae = (DIAG_FORM -> Named FORMULA) -> [DIAG_FORM] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map DIAG_FORM -> Named FORMULA
formula [DIAG_FORM]
bsForm
      diags :: [Diagnosis]
diags = (DIAG_FORM -> Diagnosis) -> [DIAG_FORM] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map DIAG_FORM -> Diagnosis
diagnosis [DIAG_FORM]
bsForm [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ TEST_SIG -> [Diagnosis]
tdiagnosis TEST_SIG
bsSig
      exErrs :: Bool
exErrs = [Diagnosis] -> Bool
Result.hasErrors [Diagnosis]
diags

-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS_BASIC.SYMB_MAP_ITEMS]
                  -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem :: [SYMB_MAP_ITEMS] -> Result (Map Symbol Symbol)
mkStatSymbMapItem xs :: [SYMB_MAP_ITEMS]
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 -> SYMB_MAP_ITEMS -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_MAP_ITEMS] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
                           (
                            \ smap :: Map Symbol Symbol
smap x :: SYMB_MAP_ITEMS
x ->
                                case SYMB_MAP_ITEMS
x of
                                  AS_BASIC.Symb_map_items sitem :: [SYMB_OR_MAP]
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
$ [SYMB_OR_MAP] -> Map Symbol Symbol
statSymbMapItem [SYMB_OR_MAP]
sitem
                           )
                           Map Symbol Symbol
forall k a. Map k a
Map.empty
                           [SYMB_MAP_ITEMS]
xs
    }

statSymbMapItem :: [AS_BASIC.SYMB_OR_MAP]
                 -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem :: [SYMB_OR_MAP] -> Map Symbol Symbol
statSymbMapItem =
    (Map Symbol Symbol -> SYMB_OR_MAP -> Map Symbol Symbol)
-> Map Symbol Symbol -> [SYMB_OR_MAP] -> Map Symbol Symbol
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
    (
     \ mmap :: Map Symbol Symbol
mmap x :: SYMB_OR_MAP
x ->
         case SYMB_OR_MAP
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.Symb_map 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.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems :: [SYMB_ITEMS] -> Result [Symbol]
mkStatSymbItems a :: [SYMB_ITEMS]
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
$ [SYMB_ITEMS] -> [Symbol]
statSymbItems [SYMB_ITEMS]
a
                    }

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

symbItemsToSymbol :: AS_BASIC.SYMB_ITEMS -> [Symbol.Symbol]
symbItemsToSymbol :: SYMB_ITEMS -> [Symbol]
symbItemsToSymbol (AS_BASIC.Symb_items 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.Symb_id tok :: SIMPLE_ID
tok) =
    Symbol :: Id -> Symbol
Symbol.Symbol {symName :: Id
Symbol.symName = SIMPLE_ID -> Id
Id.simpleIdToId SIMPLE_ID
tok}

makePMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Sign.Sign
  -> Map.Map Id.Id Id.Id
makePMap :: Map Symbol Symbol -> Sign -> Map Id Id
makePMap imap :: Map Symbol Symbol
imap sig :: Sign
sig = (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 (Set Id -> Map Id Id) -> Set Id -> Map Id 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
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 = let pMap :: Map Id Id
pMap = Map Symbol Symbol -> Sign -> Map Id Id
makePMap Map Symbol Symbol
imap Sign
sig in
              Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return
              Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism
                          { source :: Sign
Morphism.source = Sign
sig
                          , propMap :: Map Id Id
Morphism.propMap = Map Id Id
pMap
                          , 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 Id Id
pMap)
                              (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
                  pMap :: Map.Map Id.Id Id.Id
                  pMap :: Map Id Id
pMap = (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 Set Id
sigItems
                  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 Id Id
pMap)
                      (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 Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism
                     { source :: Sign
Morphism.source = Sign
sig
                     , propMap :: Map Id Id
Morphism.propMap = Map Symbol Symbol -> Sign -> Map Id Id
makePMap Map Symbol Symbol
imap Sign
sig
                     , target :: Sign
Morphism.target = Sign
tSig
                     }
                     else String -> Result Morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "Incompatible mapping"

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 (\ (x :: Int
x, y :: Morphism
y) -> (Int
x, Morphism -> Map Id Id
Morphism.propMap Morphism
y)) 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)


pROPsen_analysis :: (AS_BASIC.BASIC_SPEC, Sign.Sign, AS_BASIC.FORMULA)
  -> Result.Result AS_BASIC.FORMULA
pROPsen_analysis :: (BASIC_SPEC, Sign, FORMULA) -> Result FORMULA
pROPsen_analysis (_, s :: Sign
s, f :: FORMULA
f) =
        let x :: [DIAG_FORM]
x = [DIAG_FORM] -> NUM_FORM -> Sign -> [DIAG_FORM]
addFormula [] (Annoted FORMULA -> Integer -> NUM_FORM
NumForm Annoted FORMULA
annoF 0) Sign
s
            h :: [DIAG_FORM] -> [Diagnosis]
h = Diagnosis -> [Diagnosis]
forall (m :: * -> *) a. Monad m => a -> m a
return (Diagnosis -> [Diagnosis])
-> ([DIAG_FORM] -> Diagnosis) -> [DIAG_FORM] -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DIAG_FORM -> Diagnosis
diagnosis (DIAG_FORM -> Diagnosis)
-> ([DIAG_FORM] -> DIAG_FORM) -> [DIAG_FORM] -> Diagnosis
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DIAG_FORM] -> DIAG_FORM
forall a. [a] -> a
head
            g :: [DIAG_FORM] -> Maybe FORMULA
g = FORMULA -> Maybe FORMULA
forall a. a -> Maybe a
Just (FORMULA -> Maybe FORMULA)
-> ([DIAG_FORM] -> FORMULA) -> [DIAG_FORM] -> Maybe FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence (Named FORMULA -> FORMULA)
-> ([DIAG_FORM] -> Named FORMULA) -> [DIAG_FORM] -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DIAG_FORM -> Named FORMULA
formula (DIAG_FORM -> Named FORMULA)
-> ([DIAG_FORM] -> DIAG_FORM) -> [DIAG_FORM] -> Named FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [DIAG_FORM] -> DIAG_FORM
forall a. [a] -> a
head
            annoF :: Annoted FORMULA
annoF = FORMULA -> Range -> [Annotation] -> [Annotation] -> Annoted FORMULA
forall a. a -> Range -> [Annotation] -> [Annotation] -> Annoted a
AS_Anno.Annoted FORMULA
f Range
Id.nullRange [] []
        in [Diagnosis] -> Maybe FORMULA -> Result FORMULA
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result ([DIAG_FORM] -> [Diagnosis]
h [DIAG_FORM]
x) ([DIAG_FORM] -> Maybe FORMULA
g [DIAG_FORM]
x)