{- |
Module      :  ./CommonLogic/Analysis.hs
Description :  Basic analysis for common logic
Copyright   :  (c) Eugen Kuksa, Karl Luc, Uni Bremen 2010
License     :  GPLv2 or higher, see LICENSE.txt

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

Basic and static analysis for common logic
-}

module CommonLogic.Analysis
    ( basicCommonLogicAnalysis
    , negForm
    , symsOfTextMeta
    , mkStatSymbItems
    , mkStatSymbMapItem
    , inducedFromMorphism
    , inducedFromToMorphism
    , signColimit
    )
    where

import Common.ExtSign
import Common.Result as Result
import Common.GlobalAnnotations
import qualified Common.AS_Annotation as AS_Anno
import Common.Id as Id
import Common.IRI (parseIRIReference)
import Common.DocUtils
import Common.Lib.Graph
import Common.SetColimit
import qualified Control.Monad.Fail as Fail

import CommonLogic.Symbol as Symbol
import qualified CommonLogic.AS_CommonLogic as AS
import CommonLogic.Morphism as Morphism
import CommonLogic.Sign as Sign
import CommonLogic.ExpandCurie

import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Common.Lib.MapSet as MapSet
import qualified Data.List as List
import Data.Graph.Inductive.Graph as Graph

data DIAG_FORM = DiagForm
    {
        DIAG_FORM -> Named TEXT_META
formula :: AS_Anno.Named AS.TEXT_META,
      DIAG_FORM -> Diagnosis
diagnosis :: Result.Diagnosis
    }

-- | retrieves the signature out of a basic spec
makeSig :: AS.BASIC_SPEC -> Sign.Sign -> Sign.Sign
makeSig :: BASIC_SPEC -> Sign -> Sign
makeSig (AS.Basic_spec spec :: [Annoted BASIC_ITEMS]
spec) sig :: Sign
sig = (Sign -> Annoted BASIC_ITEMS -> Sign)
-> Sign -> [Annoted BASIC_ITEMS] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl Sign -> Annoted BASIC_ITEMS -> Sign
retrieveBasicItem Sign
sig [Annoted BASIC_ITEMS]
spec

retrieveBasicItem :: Sign.Sign -> AS_Anno.Annoted AS.BASIC_ITEMS -> Sign.Sign
retrieveBasicItem :: Sign -> Annoted BASIC_ITEMS -> Sign
retrieveBasicItem sig :: Sign
sig x :: Annoted BASIC_ITEMS
x = case Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
AS_Anno.item Annoted BASIC_ITEMS
x of
                            AS.Axiom_items xs :: [Annoted TEXT_META]
xs -> (Sign -> Annoted TEXT_META -> Sign)
-> Sign -> [Annoted TEXT_META] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl Sign -> Annoted TEXT_META -> Sign
retrieveSign Sign
sig [Annoted TEXT_META]
xs

retrieveSign :: Sign.Sign -> AS_Anno.Annoted AS.TEXT_META -> Sign.Sign
retrieveSign :: Sign -> Annoted TEXT_META -> Sign
retrieveSign sig :: Sign
sig (AS_Anno.Annoted tm :: TEXT_META
tm _ _ _) =
  Sign -> Sign -> Sign
Sign.unite (Sign -> Sign -> Sign
Sign.unite Sign
sig (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Maybe (Set NAME) -> Sign
nondiscItems (Maybe (Set NAME) -> Sign) -> Maybe (Set NAME) -> Sign
forall a b. (a -> b) -> a -> b
$ TEXT_META -> Maybe (Set NAME)
AS.nondiscourseNames TEXT_META
tm)
             (TEXT -> Sign
propsOfFormula (TEXT -> Sign) -> TEXT -> Sign
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
AS.getText TEXT_META
tm)

nondiscItems :: Maybe (Set.Set AS.NAME) -> Sign.Sign
nondiscItems :: Maybe (Set NAME) -> Sign
nondiscItems s :: Maybe (Set NAME)
s = case Maybe (Set NAME)
s of
  Nothing -> Sign
Sign.emptySig
  Just ns :: Set NAME
ns -> Sign
Sign.emptySig {nondiscourseNames :: Set Id
Sign.nondiscourseNames = (NAME -> Id) -> Set NAME -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map NAME -> Id
Id.simpleIdToId Set NAME
ns}

-- | retrieve sentences
makeFormulas :: AS.BASIC_SPEC -> Sign.Sign -> [DIAG_FORM]
makeFormulas :: BASIC_SPEC -> Sign -> [DIAG_FORM]
makeFormulas (AS.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

retrieveFormulaItem :: [DIAG_FORM] -> AS_Anno.Annoted AS.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.Axiom_items ax :: [Annoted TEXT_META]
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 TEXT_META] -> Int -> [NUM_FORM]
numberFormulae [Annoted TEXT_META]
ax 0

data NUM_FORM = NumForm
    {
      NUM_FORM -> Annoted TEXT_META
nfformula :: AS_Anno.Annoted AS.TEXT_META
    , NUM_FORM -> Int
nfnum :: Int
    }

numberFormulae :: [AS_Anno.Annoted AS.TEXT_META] -> Int -> [NUM_FORM]
numberFormulae :: [Annoted TEXT_META] -> Int -> [NUM_FORM]
numberFormulae [] _ = []
numberFormulae (x :: Annoted TEXT_META
x : xs :: [Annoted TEXT_META]
xs) i :: Int
i =
  if [Char] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Char] -> Bool) -> [Char] -> Bool
forall a b. (a -> b) -> a -> b
$ Annoted TEXT_META -> [Char]
forall a. Annoted a -> [Char]
AS_Anno.getRLabel Annoted TEXT_META
x
  then NumForm :: Annoted TEXT_META -> Int -> NUM_FORM
NumForm {nfformula :: Annoted TEXT_META
nfformula = Annoted TEXT_META
x, nfnum :: Int
nfnum = Int
i} NUM_FORM -> [NUM_FORM] -> [NUM_FORM]
forall a. a -> [a] -> [a]
: [Annoted TEXT_META] -> Int -> [NUM_FORM]
numberFormulae [Annoted TEXT_META]
xs (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
  else NumForm :: Annoted TEXT_META -> Int -> NUM_FORM
NumForm {nfformula :: Annoted TEXT_META
nfformula = Annoted TEXT_META
x, nfnum :: Int
nfnum = 0} NUM_FORM -> [NUM_FORM] -> [NUM_FORM]
forall a. a -> [a] -> [a]
: [Annoted TEXT_META] -> Int -> [NUM_FORM]
numberFormulae [Annoted TEXT_META]
xs Int
i

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 _ = [DIAG_FORM]
formulae [DIAG_FORM] -> [DIAG_FORM] -> [DIAG_FORM]
forall a. [a] -> [a] -> [a]
++
                          [DiagForm :: Named TEXT_META -> Diagnosis -> DIAG_FORM
DiagForm {
                             formula :: Named TEXT_META
formula = Annoted TEXT_META -> Int -> Named TEXT_META
makeNamed (Annoted TEXT_META -> Annoted TEXT_META
setTextIRI Annoted TEXT_META
f) Int
i
                           , diagnosis :: Diagnosis
diagnosis = Diag :: DiagKind -> [Char] -> Range -> Diagnosis
Result.Diag
                           {
                             diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Hint
                           , diagString :: [Char]
Result.diagString = "All fine"
                           , diagPos :: Range
Result.diagPos = Range
lnum
                           }
                         }]
    where
      f :: Annoted TEXT_META
f = NUM_FORM -> Annoted TEXT_META
nfformula NUM_FORM
nf
      i :: Int
i = NUM_FORM -> Int
nfnum NUM_FORM
nf
      lnum :: Range
lnum = Annoted TEXT_META -> Range
forall a. Annoted a -> Range
AS_Anno.opt_pos Annoted TEXT_META
f

-- | extract comment from text, used as formula label
getComment :: AS.TEXT -> String
getComment :: TEXT -> [Char]
getComment (AS.Text ((AS.Comment_text (AS.Comment s :: [Char]
s _) _ _) :_) _)= [Char]
s
getComment (AS.Text (_:rest :: [PHRASE]
rest) pos :: Range
pos) = TEXT -> [Char]
getComment ([PHRASE] -> Range -> TEXT
AS.Text [PHRASE]
rest Range
pos)
getComment _ = ""

stripQuote :: String -> String
stripQuote :: [Char] -> [Char]
stripQuote ('"':rest :: [Char]
rest) = [Char]
rest
stripQuote s :: [Char]
s = [Char]
s

stripQuotes :: String -> String
stripQuotes :: [Char] -> [Char]
stripQuotes ('"':rest :: [Char]
rest) = [Char] -> [Char]
forall a. [a] -> [a]
reverse ([Char] -> [Char]
stripQuote ([Char] -> [Char]
forall a. [a] -> [a]
reverse [Char]
rest))
stripQuotes s :: [Char]
s = [Char]
s

-- | generates a named formula
makeNamed :: AS_Anno.Annoted AS.TEXT_META -> Int
             -> AS_Anno.Named AS.TEXT_META
makeNamed :: Annoted TEXT_META -> Int -> Named TEXT_META
makeNamed f :: Annoted TEXT_META
f i :: Int
i =
  ([Char] -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed (
      if [Char] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
label2
        then case TEXT
text of
                AS.Named_text n :: NAME
n _ _ -> NAME -> [Char]
Id.tokStr NAME
n
                _ -> "Ax_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i
        else [Char]
label2
    ) (TEXT_META -> Named TEXT_META) -> TEXT_META -> Named TEXT_META
forall a b. (a -> b) -> a -> b
$ Annoted TEXT_META -> TEXT_META
forall a. Annoted a -> a
AS_Anno.item Annoted TEXT_META
f)
  { isAxiom :: Bool
AS_Anno.isAxiom = Bool -> Bool
not Bool
isTheorem }
   where
      text :: TEXT
text = TEXT_META -> TEXT
AS.getText (TEXT_META -> TEXT) -> TEXT_META -> TEXT
forall a b. (a -> b) -> a -> b
$ Annoted TEXT_META -> TEXT_META
forall a. Annoted a -> a
AS_Anno.item Annoted TEXT_META
f
      label :: [Char]
label = Annoted TEXT_META -> [Char]
forall a. Annoted a -> [Char]
AS_Anno.getRLabel Annoted TEXT_META
f
      label2 :: [Char]
label2 = if [Char] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
label then [Char] -> [Char]
stripQuotes ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ TEXT -> [Char]
getComment TEXT
text
                else [Char]
label
      annos :: [Annotation]
annos = Annoted TEXT_META -> [Annotation]
forall a. Annoted a -> [Annotation]
AS_Anno.r_annos Annoted TEXT_META
f
      isImplies :: Bool
isImplies = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
AS_Anno.isImplies [Annotation]
annos
      isImplied :: Bool
isImplied = (Annotation -> Bool) -> [Annotation] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Annotation -> Bool
AS_Anno.isImplied [Annotation]
annos
      isTheorem :: Bool
isTheorem = Bool
isImplies Bool -> Bool -> Bool
|| Bool
isImplied

setTextIRI :: AS_Anno.Annoted AS.TEXT_META -> AS_Anno.Annoted AS.TEXT_META
setTextIRI :: Annoted TEXT_META -> Annoted TEXT_META
setTextIRI atm :: Annoted TEXT_META
atm@(AS_Anno.Annoted { item :: forall a. Annoted a -> a
AS_Anno.item = TEXT_META
tm }) =
  let mi :: Maybe IRI
mi = case TEXT_META -> TEXT
AS.getText TEXT_META
tm of
            AS.Named_text n :: NAME
n _ _ -> [Char] -> Maybe IRI
parseIRIReference ([Char] -> Maybe IRI) -> [Char] -> Maybe IRI
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. [a] -> [a]
init ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
forall a. [a] -> [a]
tail ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ NAME -> [Char]
Id.tokStr NAME
n
            _ -> Maybe IRI
forall a. Maybe a
Nothing
  in Annoted TEXT_META
atm { item :: TEXT_META
AS_Anno.item = TEXT_META
tm { textIri :: Maybe IRI
AS.textIri = Maybe IRI
mi } }

-- | Retrives the signature of a sentence
propsOfFormula :: AS.TEXT -> Sign.Sign
propsOfFormula :: TEXT -> Sign
propsOfFormula (AS.Named_text _ txt :: TEXT
txt _) = TEXT -> Sign
propsOfFormula TEXT
txt
propsOfFormula (AS.Text phrs :: [PHRASE]
phrs _) = [Sign] -> Sign
Sign.uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Sign) -> [PHRASE] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map PHRASE -> Sign
propsOfPhrase [PHRASE]
phrs

propsOfPhrase :: AS.PHRASE -> Sign.Sign
propsOfPhrase :: PHRASE -> Sign
propsOfPhrase (AS.Module m :: MODULE
m) = MODULE -> Sign
propsOfModule MODULE
m
propsOfPhrase (AS.Sentence s :: SENTENCE
s) = SENTENCE -> Sign
propsOfSentence SENTENCE
s
propsOfPhrase (AS.Comment_text _ txt :: TEXT
txt _) = TEXT -> Sign
propsOfFormula TEXT
txt
propsOfPhrase (AS.Importation _) = Sign
Sign.emptySig

propsOfModule :: AS.MODULE -> Sign.Sign
propsOfModule :: MODULE -> Sign
propsOfModule m :: MODULE
m = case MODULE
m of
  (AS.Mod n :: NAME
n txt :: TEXT
txt _) -> Sign -> Sign -> Sign
Sign.unite (TEXT -> Sign
propsOfFormula TEXT
txt) (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ NAME -> Sign
nameToSign NAME
n
  (AS.Mod_ex n :: NAME
n exs :: [NAME]
exs txt :: TEXT
txt _) -> Sign -> Sign -> Sign
Sign.unite (TEXT -> Sign
propsOfFormula TEXT
txt)
      (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ [Sign] -> Sign
Sign.uniteL ([Sign] -> Sign) -> [Sign] -> Sign
forall a b. (a -> b) -> a -> b
$ NAME -> Sign
nameToSign NAME
n Sign -> [Sign] -> [Sign]
forall a. a -> [a] -> [a]
: (NAME -> Sign) -> [NAME] -> [Sign]
forall a b. (a -> b) -> [a] -> [b]
map NAME -> Sign
nameToSign [NAME]
exs
  where nameToSign :: NAME -> Sign
nameToSign x :: NAME
x = Sign
Sign.emptySig {
            discourseNames :: Set Id
Sign.discourseNames = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
x
          }

propsOfSentence :: AS.SENTENCE -> Sign.Sign
propsOfSentence :: SENTENCE -> Sign
propsOfSentence (AS.Atom_sent form :: ATOM
form _) = case ATOM
form of
    AS.Equation term1 :: TERM
term1 term2 :: TERM
term2 -> Sign -> Sign -> Sign
Sign.unite (TERM -> Sign
propsOfTerm TERM
term1)
      (TERM -> Sign
propsOfTerm TERM
term2)
    AS.Atom term :: TERM
term ts :: [TERM_SEQ]
ts -> Sign -> Sign -> Sign
Sign.unite (TERM -> Sign
propsOfTerm TERM
term)
      ((TERM_SEQ -> Sign) -> [TERM_SEQ] -> Sign
forall a. (a -> Sign) -> [a] -> Sign
uniteMap TERM_SEQ -> Sign
propsOfTermSeq [TERM_SEQ]
ts)
propsOfSentence (AS.Quant_sent _ xs :: [NAME_OR_SEQMARK]
xs s :: SENTENCE
s _) =
    Sign -> Sign -> Sign
Sign.sigDiff (SENTENCE -> Sign
propsOfSentence SENTENCE
s) ((NAME_OR_SEQMARK -> Sign) -> [NAME_OR_SEQMARK] -> Sign
forall a. (a -> Sign) -> [a] -> Sign
uniteMap NAME_OR_SEQMARK -> Sign
propsOfNames [NAME_OR_SEQMARK]
xs)
propsOfSentence (AS.Bool_sent bs :: BOOL_SENT
bs _) = case BOOL_SENT
bs of
    AS.Junction _ xs :: [SENTENCE]
xs -> (SENTENCE -> Sign) -> [SENTENCE] -> Sign
forall a. (a -> Sign) -> [a] -> Sign
uniteMap SENTENCE -> Sign
propsOfSentence [SENTENCE]
xs
    AS.Negation x :: SENTENCE
x -> SENTENCE -> Sign
propsOfSentence SENTENCE
x
    AS.BinOp _ s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> Sign -> Sign -> Sign
Sign.unite (SENTENCE -> Sign
propsOfSentence SENTENCE
s1) (SENTENCE -> Sign
propsOfSentence SENTENCE
s2)
propsOfSentence (AS.Comment_sent _ s :: SENTENCE
s _) = SENTENCE -> Sign
propsOfSentence SENTENCE
s
propsOfSentence (AS.Irregular_sent s :: SENTENCE
s _) = SENTENCE -> Sign
propsOfSentence SENTENCE
s

propsOfTerm :: AS.TERM -> Sign.Sign
propsOfTerm :: TERM -> Sign
propsOfTerm term :: TERM
term = case TERM
term of
    AS.Name_term x :: NAME
x -> Sign
Sign.emptySig {
            discourseNames :: Set Id
Sign.discourseNames = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
x
          }
    AS.Funct_term t :: TERM
t ts :: [TERM_SEQ]
ts _ -> Sign -> Sign -> Sign
Sign.unite (TERM -> Sign
propsOfTerm TERM
t)
                                       ((TERM_SEQ -> Sign) -> [TERM_SEQ] -> Sign
forall a. (a -> Sign) -> [a] -> Sign
uniteMap TERM_SEQ -> Sign
propsOfTermSeq [TERM_SEQ]
ts)
    AS.Comment_term t :: TERM
t _ _ -> TERM -> Sign
propsOfTerm TERM
t -- fix
    AS.That_term s :: SENTENCE
s _ -> SENTENCE -> Sign
propsOfSentence SENTENCE
s

propsOfNames :: AS.NAME_OR_SEQMARK -> Sign.Sign
propsOfNames :: NAME_OR_SEQMARK -> Sign
propsOfNames (AS.Name x :: NAME
x) = Sign
Sign.emptySig {
            discourseNames :: Set Id
Sign.discourseNames = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
x
          }
propsOfNames (AS.SeqMark x :: NAME
x) = Sign
Sign.emptySig {
            sequenceMarkers :: Set Id
Sign.sequenceMarkers = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
x
          }

propsOfTermSeq :: AS.TERM_SEQ -> Sign.Sign
propsOfTermSeq :: TERM_SEQ -> Sign
propsOfTermSeq s :: TERM_SEQ
s = case TERM_SEQ
s of
    AS.Term_seq term :: TERM
term -> TERM -> Sign
propsOfTerm TERM
term
    AS.Seq_marks x :: NAME
x -> Sign
Sign.emptySig {
            sequenceMarkers :: Set Id
Sign.sequenceMarkers = Id -> Set Id
forall a. a -> Set a
Set.singleton (Id -> Set Id) -> Id -> Set Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
Id.simpleIdToId NAME
x
          }

uniteMap :: (a -> Sign.Sign) -> [a] -> Sign
uniteMap :: (a -> Sign) -> [a] -> Sign
uniteMap p :: a -> Sign
p = (Sign -> a -> Sign) -> Sign -> [a] -> Sign
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl (\ sig :: Sign
sig -> Sign -> Sign -> Sign
Sign.unite Sign
sig (Sign -> Sign) -> (a -> Sign) -> a -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Sign
p)
   Sign
Sign.emptySig

-- | Common Logic static analysis
basicCommonLogicAnalysis :: (AS.BASIC_SPEC, Sign.Sign, GlobalAnnos)
  -> Result (AS.BASIC_SPEC,
             ExtSign Sign.Sign Symbol.Symbol,
             [AS_Anno.Named AS.TEXT_META])
basicCommonLogicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos)
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
basicCommonLogicAnalysis (bs' :: BASIC_SPEC
bs', sig :: Sign
sig, ga :: GlobalAnnos
ga) =
   [Diagnosis]
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
 -> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META]))
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
-> Result (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
forall a b. (a -> b) -> a -> b
$ if Bool
exErrs then Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
forall a. Maybe a
Nothing else
     (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
-> Maybe (BASIC_SPEC, ExtSign Sign Symbol, [Named TEXT_META])
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
newSyms, [Named TEXT_META]
sentences)
    where
      bs :: BASIC_SPEC
bs = Map [Char] IRI -> BASIC_SPEC -> BASIC_SPEC
expandCurieBS (GlobalAnnos -> Map [Char] IRI
prefix_map GlobalAnnos
ga) BASIC_SPEC
bs'
      sigItems :: Sign
sigItems = BASIC_SPEC -> Sign -> Sign
makeSig BASIC_SPEC
bs Sign
sig
      newSyms :: Set Symbol
newSyms = (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
Sign.allItems Sign
sigItems) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sign.allItems Sign
sig
      bsform :: [DIAG_FORM]
bsform = BASIC_SPEC -> Sign -> [DIAG_FORM]
makeFormulas BASIC_SPEC
bs Sign
sigItems
  -- [DIAG_FORM] signature and list of sentences
      sentences :: [Named TEXT_META]
sentences = (DIAG_FORM -> Named TEXT_META) -> [DIAG_FORM] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map DIAG_FORM -> Named TEXT_META
formula [DIAG_FORM]
bsform
  -- Annoted Sentences (Ax_), numbering, DiagError
      exErrs :: Bool
exErrs = Bool
False

-- | creates a morphism from a symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> Sign.Sign
                    -> Result.Result Morphism.Morphism
inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism m :: Map Symbol Symbol
m s :: Sign
s = let
  p :: Map Id Id
p = (Symbol -> Id) -> Map Symbol Id -> Map Id Id
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Symbol -> Id
symName (Map Symbol Id -> Map Id Id) -> Map Symbol Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ (Symbol -> Id) -> Map Symbol Symbol -> Map Symbol Id
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Symbol -> Id
symName Map Symbol Symbol
m
  t :: Sign
t = Sign
Sign.emptySig { discourseNames :: Set Id
discourseNames = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
discourseNames Sign
s
                    , nondiscourseNames :: Set Id
nondiscourseNames = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
nondiscourseNames Sign
s
                    , sequenceMarkers :: Set Id
sequenceMarkers = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
sequenceMarkers Sign
s
                    }
  in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map Id Id -> Morphism
mkMorphism Sign
s Sign
t Map Id Id
p

splitFragment :: Id -> (String, String)
splitFragment :: Id -> ([Char], [Char])
splitFragment = (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= '#') ([Char] -> ([Char], [Char]))
-> (Id -> [Char]) -> Id -> ([Char], [Char])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> [Char]
forall a. Show a => a -> [Char]
show

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 m :: Map Symbol Symbol
m (ExtSign s :: Sign
s sys :: Set Symbol
sys) (ExtSign t :: Sign
t ty :: Set Symbol
ty) = let
  tsy :: MapSet [Char] [Char]
tsy = (Symbol -> MapSet [Char] [Char] -> MapSet [Char] [Char])
-> MapSet [Char] [Char] -> Set Symbol -> MapSet [Char] [Char]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ r :: Symbol
r -> let (q :: [Char]
q, f :: [Char]
f) = Id -> ([Char], [Char])
splitFragment (Id -> ([Char], [Char])) -> Id -> ([Char], [Char])
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
symName Symbol
r
          in [Char] -> [Char] -> MapSet [Char] [Char] -> MapSet [Char] [Char]
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert [Char]
f [Char]
q) MapSet [Char] [Char]
forall a b. MapSet a b
MapSet.empty Set Symbol
ty
  p :: Map Id Id
p = (Symbol -> Map Id Id -> Map Id Id)
-> Map Id Id -> Set Symbol -> Map Id Id
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ sy :: Symbol
sy -> let n :: Id
n = Symbol -> Id
symName Symbol
sy in case Symbol -> Map Symbol Symbol -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
sy Map Symbol Symbol
m of
         Just r :: Symbol
r -> Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
n (Id -> Map Id Id -> Map Id Id) -> Id -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ Symbol -> Id
symName Symbol
r
         Nothing -> if Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
sy Set Symbol
ty then Map Id Id -> Map Id Id
forall a. a -> a
id else
           let (_, f :: [Char]
f) = Id -> ([Char], [Char])
splitFragment Id
n
           in case Set [Char] -> [[Char]]
forall a. Set a -> [a]
Set.toList (Set [Char] -> [[Char]]) -> Set [Char] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ [Char] -> MapSet [Char] [Char] -> Set [Char]
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup [Char]
f MapSet [Char] [Char]
tsy of
                [q :: [Char]
q] -> Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
n (Id -> Map Id Id -> Map Id Id) -> Id -> Map Id Id -> Map Id Id
forall a b. (a -> b) -> a -> b
$ NAME -> Id
simpleIdToId
                    (NAME -> Id) -> NAME -> Id
forall a b. (a -> b) -> a -> b
$ [Char] -> NAME
mkSimpleId ([Char] -> NAME) -> [Char] -> NAME
forall a b. (a -> b) -> a -> b
$ [Char]
q [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
f
                _ -> Map Id Id -> Map Id Id
forall a. a -> a
id) Map Id Id
forall k a. Map k a
Map.empty Set Symbol
sys
  t2 :: Sign
t2 = Sign
Sign.emptySig
       { discourseNames :: Set Id
discourseNames = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
discourseNames Sign
s
       , nondiscourseNames :: Set Id
nondiscourseNames = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
nondiscourseNames Sign
s
       , sequenceMarkers :: Set Id
sequenceMarkers = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Map Id Id -> Id -> Id
applyMap Map Id Id
p) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
sequenceMarkers Sign
s
       }
  in if Sign -> Sign -> Bool
isSubSigOf Sign
t2 Sign
t then Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map Id Id -> Morphism
mkMorphism Sign
s Sign
t Map Id Id
p else
        [Char] -> Result Morphism
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
Fail.fail ([Char] -> Result Morphism) -> [Char] -> Result Morphism
forall a b. (a -> b) -> a -> b
$ "cannot map symbols from\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sign -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc (Sign -> Sign -> Sign
sigDiff Sign
t2 Sign
t) "\nto\n"
          [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Sign -> [Char] -> [Char]
forall a. Pretty a => a -> [Char] -> [Char]
showDoc Sign
t ""

-- | negate sentence (text) - propagates negation to sentences
negForm :: AS.TEXT_META -> AS.TEXT_META
negForm :: TEXT_META -> TEXT_META
negForm tm :: TEXT_META
tm = TEXT_META
tm { getText :: TEXT
AS.getText = TEXT -> TEXT
negForm_txt (TEXT -> TEXT) -> TEXT -> TEXT
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
AS.getText TEXT_META
tm }

negForm_txt :: AS.TEXT -> AS.TEXT
negForm_txt :: TEXT -> TEXT
negForm_txt t :: TEXT
t = case TEXT
t of
  AS.Text phrs :: [PHRASE]
phrs r :: Range
r -> [PHRASE] -> Range -> TEXT
AS.Text ((PHRASE -> PHRASE) -> [PHRASE] -> [PHRASE]
forall a b. (a -> b) -> [a] -> [b]
map PHRASE -> PHRASE
negForm_phr [PHRASE]
phrs) Range
r
  AS.Named_text n :: NAME
n txt :: TEXT
txt r :: Range
r -> NAME -> TEXT -> Range -> TEXT
AS.Named_text NAME
n (TEXT -> TEXT
negForm_txt TEXT
txt) Range
r

-- negate phrase - propagates negation to sentences
negForm_phr :: AS.PHRASE -> AS.PHRASE
negForm_phr :: PHRASE -> PHRASE
negForm_phr phr :: PHRASE
phr = case PHRASE
phr of
  AS.Module m :: MODULE
m -> MODULE -> PHRASE
AS.Module (MODULE -> PHRASE) -> MODULE -> PHRASE
forall a b. (a -> b) -> a -> b
$ MODULE -> MODULE
negForm_mod MODULE
m
  AS.Sentence s :: SENTENCE
s -> SENTENCE -> PHRASE
AS.Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
negForm_sen SENTENCE
s
  AS.Comment_text c :: COMMENT
c t :: TEXT
t r :: Range
r -> COMMENT -> TEXT -> Range -> PHRASE
AS.Comment_text COMMENT
c (TEXT -> TEXT
negForm_txt TEXT
t) Range
r
  x :: PHRASE
x -> PHRASE
x

-- negate module - propagates negation to sentences
negForm_mod :: AS.MODULE -> AS.MODULE
negForm_mod :: MODULE -> MODULE
negForm_mod m :: MODULE
m = case MODULE
m of
  AS.Mod n :: NAME
n t :: TEXT
t r :: Range
r -> NAME -> TEXT -> Range -> MODULE
AS.Mod NAME
n (TEXT -> TEXT
negForm_txt TEXT
t) Range
r
  AS.Mod_ex n :: NAME
n exs :: [NAME]
exs t :: TEXT
t r :: Range
r -> NAME -> [NAME] -> TEXT -> Range -> MODULE
AS.Mod_ex NAME
n [NAME]
exs (TEXT -> TEXT
negForm_txt TEXT
t) Range
r

-- negate sentence
negForm_sen :: AS.SENTENCE -> AS.SENTENCE
negForm_sen :: SENTENCE -> SENTENCE
negForm_sen f :: SENTENCE
f = case SENTENCE
f of
  AS.Quant_sent _ _ _ r :: Range
r -> BOOL_SENT -> Range -> SENTENCE
AS.Bool_sent (SENTENCE -> BOOL_SENT
AS.Negation SENTENCE
f) Range
r
  AS.Bool_sent bs :: BOOL_SENT
bs r :: Range
r -> case BOOL_SENT
bs of
    AS.Negation s :: SENTENCE
s -> SENTENCE
s
    _ -> BOOL_SENT -> Range -> SENTENCE
AS.Bool_sent (SENTENCE -> BOOL_SENT
AS.Negation SENTENCE
f) Range
r
  _ -> BOOL_SENT -> Range -> SENTENCE
AS.Bool_sent (SENTENCE -> BOOL_SENT
AS.Negation SENTENCE
f) Range
Id.nullRange

-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS.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.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.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.Symb sym :: NAME_OR_SEQMARK
sym -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (NAME_OR_SEQMARK -> Symbol
nosToSymbol NAME_OR_SEQMARK
sym) (NAME_OR_SEQMARK -> Symbol
nosToSymbol NAME_OR_SEQMARK
sym) Map Symbol Symbol
mmap
           AS.Symb_mapN s1 :: NAME
s1 s2 :: NAME
s2 _
             -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (NAME -> Symbol
symbToSymbol NAME
s1) (NAME -> Symbol
symbToSymbol NAME
s2) Map Symbol Symbol
mmap
           AS.Symb_mapS s1 :: NAME
s1 s2 :: NAME
s2 _
             -> Symbol -> Symbol -> Map Symbol Symbol -> Map Symbol Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (NAME -> Symbol
symbToSymbol NAME
s1) (NAME -> Symbol
symbToSymbol NAME
s2) Map Symbol Symbol
mmap
    )
    Map Symbol Symbol
forall k a. Map k a
Map.empty

-- | Retrieve raw symbols
mkStatSymbItems :: [AS.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.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.SYMB_ITEMS -> [Symbol.Symbol]
symbItemsToSymbol :: SYMB_ITEMS -> [Symbol]
symbItemsToSymbol (AS.Symb_items syms :: [NAME_OR_SEQMARK]
syms _) = (NAME_OR_SEQMARK -> Symbol) -> [NAME_OR_SEQMARK] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map NAME_OR_SEQMARK -> Symbol
nosToSymbol [NAME_OR_SEQMARK]
syms

nosToSymbol :: AS.NAME_OR_SEQMARK -> Symbol.Symbol
nosToSymbol :: NAME_OR_SEQMARK -> Symbol
nosToSymbol nos :: NAME_OR_SEQMARK
nos = case NAME_OR_SEQMARK
nos of
  AS.Name tok :: NAME
tok -> NAME -> Symbol
symbToSymbol NAME
tok
  AS.SeqMark tok :: NAME
tok -> NAME -> Symbol
symbToSymbol NAME
tok

symbToSymbol :: Id.Token -> Symbol.Symbol
symbToSymbol :: NAME -> Symbol
symbToSymbol tok :: NAME
tok = Symbol :: Id -> Symbol
Symbol.Symbol {symName :: Id
Symbol.symName = NAME -> Id
Id.simpleIdToId NAME
tok}

-- | retrieves all symbols from the text
symsOfTextMeta :: AS.TEXT_META -> [Symbol.Symbol]
symsOfTextMeta :: TEXT_META -> [Symbol]
symsOfTextMeta tm :: TEXT_META
tm =
  Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList (Set Symbol -> [Symbol]) -> Set Symbol -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
Symbol.symOf (Sign -> Set Symbol) -> Sign -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Annoted TEXT_META -> Sign
retrieveSign Sign
Sign.emptySig (Annoted TEXT_META -> Sign) -> Annoted TEXT_META -> Sign
forall a b. (a -> b) -> a -> b
$ TEXT_META -> Annoted TEXT_META
forall a. a -> Annoted a
AS_Anno.emptyAnno TEXT_META
tm

-- | compute colimit of CL signatures
signColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
                           -> Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
signColimit diag :: Gr Sign (Int, Morphism)
diag = do
 let mor2fun :: (a, Morphism) -> (a, Map Id Id)
mor2fun (x :: a
x,mor :: Morphism
mor) = (a
x, Morphism -> Map Id Id
Morphism.propMap Morphism
mor)
     dGraph :: Gr (Set Id) (Int, Map Id Id)
dGraph = ((Int, Morphism) -> (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (Int, Morphism) -> (Int, Map Id Id)
forall a. (a, Morphism) -> (a, Map Id Id)
mor2fun (Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall a b. (a -> b) -> a -> b
$ (Sign -> Set Id)
-> Gr Sign (Int, Morphism) -> Gr (Set Id) (Int, Morphism)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign -> Set Id
Sign.discourseNames Gr Sign (Int, Morphism)
diag
     (dCol :: Set Id
dCol, dmap :: Map Int (Map Id Id)
dmap) = (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)
dGraph
     ndGraph :: Gr (Set Id) (Int, Map Id Id)
ndGraph = ((Int, Morphism) -> (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (Int, Morphism) -> (Int, Map Id Id)
forall a. (a, Morphism) -> (a, Map Id Id)
mor2fun (Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall a b. (a -> b) -> a -> b
$ (Sign -> Set Id)
-> Gr Sign (Int, Morphism) -> Gr (Set Id) (Int, Morphism)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign -> Set Id
Sign.nondiscourseNames Gr Sign (Int, Morphism)
diag
     (ndCol :: Set Id
ndCol, ndmap :: Map Int (Map Id Id)
ndmap) = (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)
ndGraph
     sGraph :: Gr (Set Id) (Int, Map Id Id)
sGraph = ((Int, Morphism) -> (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall (gr :: * -> * -> *) b c a.
DynGraph gr =>
(b -> c) -> gr a b -> gr a c
emap (Int, Morphism) -> (Int, Map Id Id)
forall a. (a, Morphism) -> (a, Map Id Id)
mor2fun (Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id))
-> Gr (Set Id) (Int, Morphism) -> Gr (Set Id) (Int, Map Id Id)
forall a b. (a -> b) -> a -> b
$ (Sign -> Set Id)
-> Gr Sign (Int, Morphism) -> Gr (Set Id) (Int, Morphism)
forall (gr :: * -> * -> *) a c b.
DynGraph gr =>
(a -> c) -> gr a b -> gr c b
nmap Sign -> Set Id
Sign.sequenceMarkers Gr Sign (Int, Morphism)
diag
     (sCol :: Set Id
sCol, smap :: Map Int (Map Id Id)
smap) = (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)
sGraph
     sig :: Sign
sig = Sign :: Set Id -> Set Id -> Set Id -> Sign
Sign { discourseNames :: Set Id
Sign.discourseNames = Set Id
dCol
                 , nondiscourseNames :: Set Id
Sign.nondiscourseNames = Set Id
ndCol
                 , sequenceMarkers :: Set Id
Sign.sequenceMarkers = Set Id
sCol
                 }
     mors :: Map Int Morphism
mors = [Map Int Morphism] -> Map Int Morphism
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions ([Map Int Morphism] -> Map Int Morphism)
-> [Map Int Morphism] -> Map Int Morphism
forall a b. (a -> b) -> a -> b
$ ((Int, Sign) -> Map Int Morphism)
-> [(Int, Sign)] -> [Map Int Morphism]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: Int
x, nsig :: Sign
nsig) -> 
                   let m :: Morphism
m = Morphism :: Sign -> Sign -> Map Id Id -> Morphism
Morphism.Morphism {
                              source :: Sign
Morphism.source = Sign
nsig
                            , target :: Sign
Morphism.target = Sign
sig
                            , propMap :: Map Id Id
Morphism.propMap = [Map Id Id] -> Map Id Id
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions 
                                [ Map Id Id -> Int -> Map Int (Map Id Id) -> Map Id Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map Id Id
forall a. HasCallStack => [Char] -> a
error "dmap") Int
x Map Int (Map Id Id)
dmap, 
                                  Map Id Id -> Int -> Map Int (Map Id Id) -> Map Id Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map Id Id
forall a. HasCallStack => [Char] -> a
error "ndmap") Int
x Map Int (Map Id Id)
ndmap, 
                                  Map Id Id -> Int -> Map Int (Map Id Id) -> Map Id Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault ([Char] -> Map Id Id
forall a. HasCallStack => [Char] -> a
error "smap") Int
x Map Int (Map Id Id)
smap]
                           }
                            in Int -> Morphism -> Map Int Morphism -> Map Int Morphism
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
x Morphism
m Map Int Morphism
forall k a. Map k a
Map.empty) ([(Int, Sign)] -> [Map Int Morphism])
-> [(Int, Sign)] -> [Map 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)
diag
 (Sign, Map Int Morphism) -> Result (Sign, Map Int Morphism)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig, Map Int Morphism
mors)