{- |
Module      :  ./CASL_DL/StatAna.hs
Description :  static analysis of DL parts
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

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

static analysis of DL parts especially cardinalities, predefined datatypes
and additional annottations
-}

module CASL_DL.StatAna ( basicCASL_DLAnalysis
                       , minDLForm
                       , checkSymbolMapDL
                       , DLSign) where

import CASL_DL.AS_CASL_DL
import CASL_DL.Print_AS ()
import CASL_DL.Sign
import CASL_DL.PredefinedCASLAxioms

import CASL.Sign
import CASL.MixfixParser
import CASL.Morphism
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.Overload
import CASL.Quantification

import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.ConvertGlobalAnnos
import Common.DocUtils
import Common.Id
import Common.Result
import Common.ConvertLiteral
import Common.ExtSign
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set

instance TermExtension DL_FORMULA where
    freeVarsOfExt :: Sign DL_FORMULA e -> DL_FORMULA -> VarSet
freeVarsOfExt sign :: Sign DL_FORMULA e
sign (Cardinality _ _ t1 :: TERM DL_FORMULA
t1 t2 :: TERM DL_FORMULA
t2 mf :: Maybe (FORMULA DL_FORMULA)
mf _) =
        VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign DL_FORMULA e -> TERM DL_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign DL_FORMULA e
sign TERM DL_FORMULA
t1) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign DL_FORMULA e -> TERM DL_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars Sign DL_FORMULA e
sign TERM DL_FORMULA
t2)
           (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ case Maybe (FORMULA DL_FORMULA)
mf of
               Nothing -> VarSet
forall a. Set a
Set.empty
               Just f :: FORMULA DL_FORMULA
f -> Sign DL_FORMULA e -> FORMULA DL_FORMULA -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign DL_FORMULA e
sign FORMULA DL_FORMULA
f

basicCASL_DLAnalysis
    :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign, GlobalAnnos)
    -> Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
basicCASL_DLAnalysis :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign,
 GlobalAnnos)
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
basicCASL_DLAnalysis (bs :: BASIC_SPEC () () DL_FORMULA
bs, sig :: Sign DL_FORMULA CASL_DLSign
sig, ga :: GlobalAnnos
ga) =
    do GlobalAnnos
ga' <- GlobalAnnos -> GlobalAnnos -> Result GlobalAnnos
mergeGlobalAnnos GlobalAnnos
ga (GlobalAnnos -> Result GlobalAnnos)
-> GlobalAnnos -> Result GlobalAnnos
forall a b. (a -> b) -> a -> b
$ Sign () () -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign () ()
predefSign
       let sig' :: Sign DL_FORMULA CASL_DLSign
sig' = (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> Sign DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign Sign DL_FORMULA CASL_DLSign
sig (Sign DL_FORMULA CASL_DLSign -> Sign DL_FORMULA CASL_DLSign)
-> Sign DL_FORMULA CASL_DLSign -> Sign DL_FORMULA CASL_DLSign
forall a b. (a -> b) -> a -> b
$ CASL_DLSign -> Sign DL_FORMULA CASL_DLSign
forall e f. e -> Sign f e
predefinedSign CASL_DLSign
emptyCASL_DLSign
           bs' :: BASIC_SPEC () () DL_FORMULA
bs' = Bool -> BASIC_SPEC () () DL_FORMULA -> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations Bool
True BASIC_SPEC () () DL_FORMULA
bs
       case Min DL_FORMULA CASL_DLSign
-> Ana () () () DL_FORMULA CASL_DLSign
-> Ana () () () DL_FORMULA CASL_DLSign
-> Mix () () DL_FORMULA CASL_DLSign
-> (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign,
    GlobalAnnos)
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall f e b s.
(FormExtension f, TermExtension f) =>
Min f e
-> Ana b b s f e
-> Ana s b s f e
-> Mix b s f e
-> (BASIC_SPEC b s f, Sign f e, GlobalAnnos)
-> Result
     (BASIC_SPEC b s f, ExtSign (Sign f e) Symbol, [Named (FORMULA f)])
basicAnalysis Min DL_FORMULA CASL_DLSign
minDLForm ((() -> State (Sign DL_FORMULA CASL_DLSign) ())
-> Ana () () () DL_FORMULA CASL_DLSign
forall a b. a -> b -> a
const () -> State (Sign DL_FORMULA CASL_DLSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return)
             ((() -> State (Sign DL_FORMULA CASL_DLSign) ())
-> Ana () () () DL_FORMULA CASL_DLSign
forall a b. a -> b -> a
const () -> State (Sign DL_FORMULA CASL_DLSign) ()
forall (m :: * -> *) a. Monad m => a -> m a
return) Mix () () DL_FORMULA CASL_DLSign
ana_Mix (BASIC_SPEC () () DL_FORMULA
bs', Sign DL_FORMULA CASL_DLSign
sig', GlobalAnnos
ga') of
         r :: Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
r@(Result ds1 :: [Diagnosis]
ds1 mr :: Maybe
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
mr) ->
             Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
-> ((BASIC_SPEC () () DL_FORMULA,
     ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
     [Named (FORMULA DL_FORMULA)])
    -> Result
         (BASIC_SPEC () () DL_FORMULA,
          ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
          [Named (FORMULA DL_FORMULA)]))
-> Maybe
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
r (Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
cleanStatAnaResult (Result
   (BASIC_SPEC () () DL_FORMULA,
    ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
    [Named (FORMULA DL_FORMULA)])
 -> Result
      (BASIC_SPEC () () DL_FORMULA,
       ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
       [Named (FORMULA DL_FORMULA)]))
-> ((BASIC_SPEC () () DL_FORMULA,
     ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
     [Named (FORMULA DL_FORMULA)])
    -> Result
         (BASIC_SPEC () () DL_FORMULA,
          ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
          [Named (FORMULA DL_FORMULA)]))
-> (BASIC_SPEC () () DL_FORMULA,
    ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
    [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Diagnosis]
-> Sign DL_FORMULA CASL_DLSign
-> (BASIC_SPEC () () DL_FORMULA,
    ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
    [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
postAna [Diagnosis]
ds1 Sign DL_FORMULA CASL_DLSign
sig') Maybe
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
mr

{- |
  True -> extend all sort declarations without a supersort
          with supersort Thing
  False -> remove Thing from all sort declarations with supersort Thing
-}
generateSubsorting :: Sign f e -> Sign f e
generateSubsorting :: Sign f e -> Sign f e
generateSubsorting sig :: Sign f e
sig =
    let
        inS :: Set SORT
inS = Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign f e
sig
        inR :: Rel SORT
inR = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig
    in
      Sign f e
sig
      {
        sortRel :: Rel SORT
sortRel = (SORT -> Rel SORT -> Rel SORT) -> Rel SORT -> Set SORT -> Rel SORT
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ x :: SORT
x y :: Rel SORT
y -> SORT -> SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertDiffPair SORT
x SORT
thing Rel SORT
y) Rel SORT
inR Set SORT
inS
      }

transformSortDeclarations :: Bool
                          -> BASIC_SPEC () () DL_FORMULA
                          -> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations :: Bool -> BASIC_SPEC () () DL_FORMULA -> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations addThing :: Bool
addThing (Basic_spec aBIs :: [Annoted (BASIC_ITEMS () () DL_FORMULA)]
aBIs) =
    [Annoted (BASIC_ITEMS () () DL_FORMULA)]
-> BASIC_SPEC () () DL_FORMULA
forall b s f. [Annoted (BASIC_ITEMS b s f)] -> BASIC_SPEC b s f
Basic_spec ([Annoted (BASIC_ITEMS () () DL_FORMULA)]
-> [Annoted (BASIC_ITEMS () () DL_FORMULA)]
forall b s f.
[Annoted (BASIC_ITEMS b s f)] -> [Annoted (BASIC_ITEMS b s f)]
processBIs [Annoted (BASIC_ITEMS () () DL_FORMULA)]
aBIs)
    where processBIs :: [Annoted (BASIC_ITEMS b s f)] -> [Annoted (BASIC_ITEMS b s f)]
processBIs = (Annoted (BASIC_ITEMS b s f) -> Annoted (BASIC_ITEMS b s f))
-> [Annoted (BASIC_ITEMS b s f)] -> [Annoted (BASIC_ITEMS b s f)]
forall a b. (a -> b) -> [a] -> [b]
map ((BASIC_ITEMS b s f -> BASIC_ITEMS b s f)
-> Annoted (BASIC_ITEMS b s f) -> Annoted (BASIC_ITEMS b s f)
forall a b. (a -> b) -> Annoted a -> Annoted b
mapAn BASIC_ITEMS b s f -> BASIC_ITEMS b s f
forall b s f. BASIC_ITEMS b s f -> BASIC_ITEMS b s f
processBI)
          processBI :: BASIC_ITEMS b s f -> BASIC_ITEMS b s f
processBI bi :: BASIC_ITEMS b s f
bi = case BASIC_ITEMS b s f
bi of
                           Sig_items sig_i :: SIG_ITEMS s f
sig_i -> SIG_ITEMS s f -> BASIC_ITEMS b s f
forall b s f. SIG_ITEMS s f -> BASIC_ITEMS b s f
Sig_items (SIG_ITEMS s f -> SIG_ITEMS s f
forall s f. SIG_ITEMS s f -> SIG_ITEMS s f
processSig_i SIG_ITEMS s f
sig_i)
                           _ -> BASIC_ITEMS b s f
bi
          processSig_i :: SIG_ITEMS s f -> SIG_ITEMS s f
processSig_i sig_i :: SIG_ITEMS s f
sig_i =
              case SIG_ITEMS s f
sig_i of
                Sort_items sk :: SortsKind
sk aSor_is :: [Annoted (SORT_ITEM f)]
aSor_is r :: Range
r ->
                    SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
forall s f.
SortsKind -> [Annoted (SORT_ITEM f)] -> Range -> SIG_ITEMS s f
Sort_items SortsKind
sk ((Annoted (SORT_ITEM f) -> [Annoted (SORT_ITEM f)])
-> [Annoted (SORT_ITEM f)] -> [Annoted (SORT_ITEM f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Annoted (SORT_ITEM f) -> [Annoted (SORT_ITEM f)]
forall f. Annoted (SORT_ITEM f) -> [Annoted (SORT_ITEM f)]
processaSor_i [Annoted (SORT_ITEM f)]
aSor_is) Range
r
                _ -> SIG_ITEMS s f
sig_i
          processaSor_i :: Annoted (SORT_ITEM f) -> [Annoted (SORT_ITEM f)]
processaSor_i aSor_i :: Annoted (SORT_ITEM f)
aSor_i =
              case SORT_ITEM f -> [SORT_ITEM f]
forall f. SORT_ITEM f -> [SORT_ITEM f]
processSor_i (Annoted (SORT_ITEM f) -> SORT_ITEM f
forall a. Annoted a -> a
item Annoted (SORT_ITEM f)
aSor_i) of
                [] -> []
                x :: SORT_ITEM f
x : xs :: [SORT_ITEM f]
xs -> SORT_ITEM f -> Annoted (SORT_ITEM f) -> Annoted (SORT_ITEM f)
forall b a. b -> Annoted a -> Annoted b
replaceAnnoted SORT_ITEM f
x Annoted (SORT_ITEM f)
aSor_i Annoted (SORT_ITEM f)
-> [Annoted (SORT_ITEM f)] -> [Annoted (SORT_ITEM f)]
forall a. a -> [a] -> [a]
: (SORT_ITEM f -> Annoted (SORT_ITEM f))
-> [SORT_ITEM f] -> [Annoted (SORT_ITEM f)]
forall a b. (a -> b) -> [a] -> [b]
map SORT_ITEM f -> Annoted (SORT_ITEM f)
forall a. a -> Annoted a
emptyAnno [SORT_ITEM f]
xs
          processSor_i :: SORT_ITEM f -> [SORT_ITEM f]
processSor_i sor_i :: SORT_ITEM f
sor_i =
              if Bool
addThing
              then
                    case SORT_ITEM f
sor_i of
                      Sort_decl sorts :: [SORT]
sorts r :: Range
r ->
                          [[SORT] -> SORT -> Range -> SORT_ITEM f
forall f. [SORT] -> SORT -> Range -> SORT_ITEM f
Subsort_decl [SORT]
sorts SORT
thing Range
r]
                      Subsort_decl _ supSort :: SORT
supSort _
                          | SORT
supSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
thing -> [SORT_ITEM f
sor_i]
                          | Bool
otherwise ->
                              [ SORT_ITEM f
sor_i
                              , [SORT] -> SORT -> Range -> SORT_ITEM f
forall f. [SORT] -> SORT -> Range -> SORT_ITEM f
Subsort_decl [SORT
supSort] SORT
thing Range
statAnaMarker]
                      _ -> [SORT_ITEM f
sor_i]
              else
                    case SORT_ITEM f
sor_i of
                      Subsort_decl sorts :: [SORT]
sorts supSort :: SORT
supSort r :: Range
r
                          | SORT
supSort SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
thing -> if Range
r Range -> Range -> Bool
forall a. Eq a => a -> a -> Bool
== Range
statAnaMarker
                                                  then []
                                                  else [[SORT] -> Range -> SORT_ITEM f
forall f. [SORT] -> Range -> SORT_ITEM f
Sort_decl [SORT]
sorts Range
r]
                          | Bool
otherwise -> [SORT_ITEM f
sor_i]
                      _ -> [SORT_ITEM f
sor_i]

-- | marker for sig items added to a basic spec
statAnaMarker :: Range
statAnaMarker :: Range
statAnaMarker = [Pos] -> Range
Range [String -> Int -> Int -> Pos
SourcePos ">:>added for DL.StaticAna<:<" 0 0]

{- |
 * remove predefined symbols from a result of the static analysis

 * remove all explicit references of Thing from the BSIC_SPEC
-}
cleanStatAnaResult
    :: Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
    -> Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
cleanStatAnaResult :: Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
cleanStatAnaResult r :: Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
r@(Result ds1 :: [Diagnosis]
ds1 mr :: Maybe
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
mr) = Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
-> ((BASIC_SPEC () () DL_FORMULA,
     ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
     [Named (FORMULA DL_FORMULA)])
    -> Result
         (BASIC_SPEC () () DL_FORMULA,
          ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
          [Named (FORMULA DL_FORMULA)]))
-> Maybe
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Result
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
r (BASIC_SPEC () () DL_FORMULA,
 ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
 [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall f c.
(BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
 c)
-> Result
     (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
      c)
clean Maybe
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
mr
    where clean :: (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
 c)
-> Result
     (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
      c)
clean (bs :: BASIC_SPEC () () DL_FORMULA
bs, ExtSign sig :: Sign f CASL_DLSign
sig sys :: Set Symbol
sys, sen :: c
sen) =
              [Diagnosis]
-> Maybe
     (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
      c)
-> Result
     (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
      c)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds1 ((BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
 c)
-> Maybe
     (BASIC_SPEC () () DL_FORMULA, ExtSign (Sign f CASL_DLSign) Symbol,
      c)
forall a. a -> Maybe a
Just (Bool -> BASIC_SPEC () () DL_FORMULA -> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations Bool
False BASIC_SPEC () () DL_FORMULA
bs
                               , Sign f CASL_DLSign
-> Set Symbol -> ExtSign (Sign f CASL_DLSign) Symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign (Sign f CASL_DLSign -> Sign f CASL_DLSign
forall f e. Sign f e -> Sign f e
generateSubsorting (Sign f CASL_DLSign -> Sign f CASL_DLSign)
-> Sign f CASL_DLSign -> Sign f CASL_DLSign
forall a b. (a -> b) -> a -> b
$ Sign f CASL_DLSign -> Sign f CASL_DLSign
forall f. Sign f CASL_DLSign -> Sign f CASL_DLSign
cleanSign Sign f CASL_DLSign
sig) (Set Symbol -> ExtSign (Sign f CASL_DLSign) Symbol)
-> Set Symbol -> ExtSign (Sign f CASL_DLSign) Symbol
forall a b. (a -> b) -> a -> b
$
                                 Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.delete (SORT -> Symbol
idToSortSymbol SORT
thing) Set Symbol
sys
                               , c
sen))
          cleanSign :: Sign f CASL_DLSign -> Sign f CASL_DLSign
cleanSign sig :: Sign f CASL_DLSign
sig =
              (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> Sign f CASL_DLSign -> Sign f CASL_DLSign -> Sign f CASL_DLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig CASL_DLSign -> CASL_DLSign -> CASL_DLSign
diffCASL_DLSign Sign f CASL_DLSign
sig (Sign f CASL_DLSign -> Sign f CASL_DLSign)
-> Sign f CASL_DLSign -> Sign f CASL_DLSign
forall a b. (a -> b) -> a -> b
$ CASL_DLSign -> Sign f CASL_DLSign
forall e f. e -> Sign f e
predefinedSign CASL_DLSign
emptyCASL_DLSign

{- |
  postAna checks the Signature for

  * all new sorts must be a proper subsort of Thing and
    must not be related to DATA

  * no new subsort relations with DATA

  * all new predicates must have a subsort of Thing as subject (1st argument)

  * all new operations must have a subsort of Thing as 1st argument

-}
postAna :: [Diagnosis]
        -> Sign DL_FORMULA CASL_DLSign
        -> (BASIC_SPEC () () DL_FORMULA,
            ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
            [Named (FORMULA DL_FORMULA)])
        -> Result (BASIC_SPEC () () DL_FORMULA,
                   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
                   [Named (FORMULA DL_FORMULA)])
postAna :: [Diagnosis]
-> Sign DL_FORMULA CASL_DLSign
-> (BASIC_SPEC () () DL_FORMULA,
    ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
    [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
postAna ds1 :: [Diagnosis]
ds1 in_sig :: Sign DL_FORMULA CASL_DLSign
in_sig i :: (BASIC_SPEC () () DL_FORMULA,
 ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
 [Named (FORMULA DL_FORMULA)])
i@(_, ExtSign acc_sig :: Sign DL_FORMULA CASL_DLSign
acc_sig _, _) =
    [Diagnosis]
-> Maybe
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis]
ds1 [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
ds_sig) (Maybe
   (BASIC_SPEC () () DL_FORMULA,
    ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
    [Named (FORMULA DL_FORMULA)])
 -> Result
      (BASIC_SPEC () () DL_FORMULA,
       ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
       [Named (FORMULA DL_FORMULA)]))
-> Maybe
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
-> Result
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall a b. (a -> b) -> a -> b
$ if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds_sig then (BASIC_SPEC () () DL_FORMULA,
 ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
 [Named (FORMULA DL_FORMULA)])
-> Maybe
     (BASIC_SPEC () () DL_FORMULA,
      ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
      [Named (FORMULA DL_FORMULA)])
forall a. a -> Maybe a
Just (BASIC_SPEC () () DL_FORMULA,
 ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
 [Named (FORMULA DL_FORMULA)])
i else Maybe
  (BASIC_SPEC () () DL_FORMULA,
   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
   [Named (FORMULA DL_FORMULA)])
forall a. Maybe a
Nothing
    where ds_sig :: [Diagnosis]
ds_sig = [Diagnosis]
chkSorts [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
checkPreds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [Diagnosis]
checkOps
          diff_sig :: Sign DL_FORMULA CASL_DLSign
diff_sig = (CASL_DLSign -> CASL_DLSign -> CASL_DLSign)
-> Sign DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig CASL_DLSign -> CASL_DLSign -> CASL_DLSign
diffCASL_DLSign Sign DL_FORMULA CASL_DLSign
acc_sig Sign DL_FORMULA CASL_DLSign
in_sig
          chkSorts :: [Diagnosis]
chkSorts = (SORT -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> Set SORT -> [Diagnosis]
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold SORT -> [Diagnosis] -> [Diagnosis]
chSort [] (Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. Sign f e -> Set SORT
sortSet Sign DL_FORMULA CASL_DLSign
diff_sig) [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
             [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
                        ("\n     new subsort relations with data " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         "topsort are not allowed") Range
nullRange
             | SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
dataS (SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
thing Sign DL_FORMULA CASL_DLSign
acc_sig) Bool -> Bool -> Bool
||
                 SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
dataS (SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
thing Sign DL_FORMULA CASL_DLSign
acc_sig) Bool -> Bool -> Bool
||
                 SORT -> Sign () () -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
dataS Sign () ()
predefSign Set SORT -> Set SORT -> Bool
forall a. Eq a => a -> a -> Bool
/=
                  SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
dataS Sign DL_FORMULA CASL_DLSign
acc_sig Bool -> Bool -> Bool
||
                 Rel SORT -> Rel SORT
selectDATAKernel (Sign () () -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign () ()
predefSign)
                  Rel SORT -> Rel SORT -> Bool
forall a. Eq a => a -> a -> Bool
/= Rel SORT -> Rel SORT
selectDATAKernel (Sign DL_FORMULA CASL_DLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign DL_FORMULA CASL_DLSign
acc_sig)]
          chSort :: SORT -> [Diagnosis] -> [Diagnosis]
chSort s :: SORT
s ds :: [Diagnosis]
ds = [Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++
              [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                        ("\n     new sort is not a subsort of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
thing "':") SORT
s
              | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
thing (Set SORT -> Bool) -> Set SORT -> Bool
forall a b. (a -> b) -> a -> b
$ SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s Sign DL_FORMULA CASL_DLSign
acc_sig]
              [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [DiagKind -> String -> SORT -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                        ("\n     new sort must not be a supersort of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
thing "':") SORT
s
                 | SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
thing (SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
s Sign DL_FORMULA CASL_DLSign
acc_sig)]
          selectDATAKernel :: Rel SORT -> Rel SORT
selectDATAKernel rel :: Rel SORT
rel =
              Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.intransKernel (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Set SORT -> Rel SORT
forall a. Ord a => Rel a -> Set a -> Rel a
Rel.restrict Rel SORT
rel (Set SORT -> Rel SORT) -> Set SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$
                 SORT -> Set SORT -> Set SORT
forall a. Ord a => a -> Set a -> Set a
Set.insert SORT
dataS
                        (SORT -> Sign () () -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
subsortsOf SORT
dataS Sign () ()
predefSign)

          checkPreds :: [Diagnosis]
checkPreds = (SORT -> PredType -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> MapSet SORT PredType -> [Diagnosis]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey SORT -> PredType -> [Diagnosis] -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> PredType -> [Diagnosis] -> [Diagnosis]
chPred [] (Sign DL_FORMULA CASL_DLSign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign DL_FORMULA CASL_DLSign
diff_sig)
          chPred :: a -> PredType -> [Diagnosis] -> [Diagnosis]
chPred p :: a
p ty :: PredType
ty = (String -> a -> [SORT] -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
String -> a -> [SORT] -> [Diagnosis]
chArgs "pred" a
p (PredType -> [SORT]
predArgs PredType
ty) [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++)
          checkOps :: [Diagnosis]
checkOps = (SORT -> OpType -> [Diagnosis] -> [Diagnosis])
-> [Diagnosis] -> MapSet SORT OpType -> [Diagnosis]
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey SORT -> OpType -> [Diagnosis] -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
a -> OpType -> [Diagnosis] -> [Diagnosis]
chOp [] (Sign DL_FORMULA CASL_DLSign -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign DL_FORMULA CASL_DLSign
diff_sig)
          chOp :: a -> OpType -> [Diagnosis] -> [Diagnosis]
chOp o :: a
o ty :: OpType
ty = (String -> a -> [SORT] -> [Diagnosis]
forall a.
(GetRange a, Pretty a) =>
String -> a -> [SORT] -> [Diagnosis]
chArgs "op" a
o (OpType -> [SORT]
opArgs OpType
ty) [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++)
          chArgs :: String -> a -> [SORT] -> [Diagnosis]
chArgs kstr :: String
kstr sym :: a
sym args :: [SORT]
args =
              case [SORT]
args of
              [] -> if String
kstr String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "op"
                    then []
                    else [DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                        "\n     propositional symbols are not allowed" a
sym]
              (s :: SORT
s : _) ->
                  if SORT
s SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
thing Bool -> Bool -> Bool
||
                     SORT -> Set SORT -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member SORT
thing (SORT -> Sign DL_FORMULA CASL_DLSign -> Set SORT
forall f e. SORT -> Sign f e -> Set SORT
supersortsOf SORT
s Sign DL_FORMULA CASL_DLSign
acc_sig)
                  then []
                  else [DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                        ("\n     the first argument sort of this " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
kstr String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        " is not a subsort of '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
thing "':")
                        a
sym]


{- sketch of Annotation analysis:

    where callAna bsRes =
              case analyseAnnos ga acc_sig bs of
              Result ds2 mESig ->
                  maybe (Result (ds1++ds2) Nothing)
                        (integrateExt (ds1++ds2) baRes) mESig
          integrateExt ds (bs',dif_sig,acc_sig,sens) eSig =
              Result ds (bs',
                         dif_sig {extendedInfo = dif eSig (extendedInfo sig)},
                         acc_sig {extendedInfo = eSig},
                         sens)
-}

ana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ana_Mix = Mix () () Any CASL_DLSign
forall b s f e. Mix b s f e
emptyMix
    { putParen :: DL_FORMULA -> DL_FORMULA
putParen = DL_FORMULA -> DL_FORMULA
mapDL_FORMULA
    , mixResolve :: MixResolve DL_FORMULA
mixResolve = MixResolve DL_FORMULA
resolveDL_FORMULA
    }

type DLSign = Sign DL_FORMULA CASL_DLSign

mapDL_FORMULA :: DL_FORMULA -> DL_FORMULA
mapDL_FORMULA :: DL_FORMULA -> DL_FORMULA
mapDL_FORMULA (Cardinality ct :: CardType
ct pn :: PRED_SYMB
pn varTerm :: TERM DL_FORMULA
varTerm natTerm :: TERM DL_FORMULA
natTerm qualTerm :: Maybe (FORMULA DL_FORMULA)
qualTerm ps :: Range
ps) =
    CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
pn (TERM DL_FORMULA -> TERM DL_FORMULA
mapT TERM DL_FORMULA
varTerm) (TERM DL_FORMULA -> TERM DL_FORMULA
mapT TERM DL_FORMULA
natTerm) Maybe (FORMULA DL_FORMULA)
qualTerm Range
ps
    where mapT :: TERM DL_FORMULA -> TERM DL_FORMULA
mapT = (DL_FORMULA -> DL_FORMULA) -> TERM DL_FORMULA -> TERM DL_FORMULA
forall f. (f -> f) -> TERM f -> TERM f
mapTerm DL_FORMULA -> DL_FORMULA
mapDL_FORMULA

resolveDL_FORMULA :: MixResolve DL_FORMULA
resolveDL_FORMULA :: MixResolve DL_FORMULA
resolveDL_FORMULA ga :: GlobalAnnos
ga ids :: (TokRules, Rules)
ids (Cardinality ct :: CardType
ct ps :: PRED_SYMB
ps varTerm :: TERM DL_FORMULA
varTerm natTerm :: TERM DL_FORMULA
natTerm qualTerm :: Maybe (FORMULA DL_FORMULA)
qualTerm ran :: Range
ran) =
    do TERM DL_FORMULA
vt <- TERM DL_FORMULA -> Result (TERM DL_FORMULA)
resMixTerm TERM DL_FORMULA
varTerm
       TERM DL_FORMULA
nt <- TERM DL_FORMULA -> Result (TERM DL_FORMULA)
resMixTerm TERM DL_FORMULA
natTerm
       Maybe (FORMULA DL_FORMULA)
mf <- case Maybe (FORMULA DL_FORMULA)
qualTerm of
         Nothing -> Maybe (FORMULA DL_FORMULA) -> Result (Maybe (FORMULA DL_FORMULA))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (FORMULA DL_FORMULA)
forall a. Maybe a
Nothing
         Just f :: FORMULA DL_FORMULA
f -> (FORMULA DL_FORMULA -> Maybe (FORMULA DL_FORMULA))
-> Result (FORMULA DL_FORMULA)
-> Result (Maybe (FORMULA DL_FORMULA))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FORMULA DL_FORMULA -> Maybe (FORMULA DL_FORMULA)
forall a. a -> Maybe a
Just (Result (FORMULA DL_FORMULA)
 -> Result (Maybe (FORMULA DL_FORMULA)))
-> Result (FORMULA DL_FORMULA)
-> Result (Maybe (FORMULA DL_FORMULA))
forall a b. (a -> b) -> a -> b
$
                   (DL_FORMULA -> DL_FORMULA)
-> MixResolve DL_FORMULA -> MixResolve (FORMULA DL_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (FORMULA f)
resolveMixFrm DL_FORMULA -> DL_FORMULA
mapDL_FORMULA MixResolve DL_FORMULA
resolveDL_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids FORMULA DL_FORMULA
f
       DL_FORMULA -> Result DL_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (DL_FORMULA -> Result DL_FORMULA)
-> DL_FORMULA -> Result DL_FORMULA
forall a b. (a -> b) -> a -> b
$ CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
ps TERM DL_FORMULA
vt TERM DL_FORMULA
nt Maybe (FORMULA DL_FORMULA)
mf Range
ran
    where resMixTerm :: TERM DL_FORMULA -> Result (TERM DL_FORMULA)
resMixTerm = (DL_FORMULA -> DL_FORMULA)
-> MixResolve DL_FORMULA -> MixResolve (TERM DL_FORMULA)
forall f.
FormExtension f =>
(f -> f) -> MixResolve f -> MixResolve (TERM f)
resolveMixTrm DL_FORMULA -> DL_FORMULA
mapDL_FORMULA
                                     MixResolve DL_FORMULA
resolveDL_FORMULA GlobalAnnos
ga (TokRules, Rules)
ids

minDLForm :: Min DL_FORMULA CASL_DLSign
minDLForm :: Min DL_FORMULA CASL_DLSign
minDLForm sign :: Sign DL_FORMULA CASL_DLSign
sign form :: DL_FORMULA
form = case DL_FORMULA
form of
    Cardinality ct :: CardType
ct ps :: PRED_SYMB
ps varTerm :: TERM DL_FORMULA
varTerm natTerm :: TERM DL_FORMULA
natTerm qualTerm :: Maybe (FORMULA DL_FORMULA)
qualTerm ran :: Range
ran ->
       let pn :: SORT
pn = PRED_SYMB -> SORT
predSymbName PRED_SYMB
ps
           pn_RelTypes :: Set PredType
pn_RelTypes = (PredType -> Bool) -> Set PredType -> Set PredType
forall a. (a -> Bool) -> Set a -> Set a
Set.filter PredType -> Bool
isBinPredType
                 (Set PredType -> Set PredType) -> Set PredType -> Set PredType
forall a b. (a -> b) -> a -> b
$ SORT -> MapSet SORT PredType -> Set PredType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup SORT
pn (Sign DL_FORMULA CASL_DLSign -> MapSet SORT PredType
forall f e. Sign f e -> MapSet SORT PredType
predMap Sign DL_FORMULA CASL_DLSign
sign)
       in
      if Set PredType -> Bool
forall a. Set a -> Bool
Set.null Set PredType
pn_RelTypes then
                [Diagnosis] -> Maybe DL_FORMULA -> Result DL_FORMULA
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error ("Unknown binary predicate: \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                    SORT -> String
forall a. Show a => a -> String
show SORT
pn String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\"") (SORT -> Range
posOfId SORT
pn)]
                       Maybe DL_FORMULA
forall a. Maybe a
Nothing
      else do
                   TERM DL_FORMULA
v2 <- Min DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
-> TERM DL_FORMULA
-> Result (TERM DL_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min DL_FORMULA CASL_DLSign
minDLForm Sign DL_FORMULA CASL_DLSign
sign TERM DL_FORMULA
varTerm
                   let v_sort :: SORT
v_sort = TERM DL_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM DL_FORMULA
v2
                   TERM DL_FORMULA
n2 <- Min DL_FORMULA CASL_DLSign
-> Sign DL_FORMULA CASL_DLSign
-> TERM DL_FORMULA
-> Result (TERM DL_FORMULA)
forall f e.
(FormExtension f, TermExtension f) =>
Min f e -> Sign f e -> TERM f -> Result (TERM f)
oneExpTerm Min DL_FORMULA CASL_DLSign
minDLForm Sign DL_FORMULA CASL_DLSign
sign TERM DL_FORMULA
natTerm
                   let n_sort :: SORT
n_sort = TERM DL_FORMULA -> SORT
forall f. TermExtension f => f -> SORT
sortOfTerm TERM DL_FORMULA
n2
                   PRED_SYMB
ps' <- case SORT -> SORT -> Set PredType -> Result [PRED_TYPE]
forall a.
(GetRange a, Pretty a) =>
a -> SORT -> Set PredType -> Result [PRED_TYPE]
sub_sort_of_subj SORT
pn SORT
v_sort Set PredType
pn_RelTypes of
                          Result ds :: [Diagnosis]
ds mts :: Maybe [PRED_TYPE]
mts ->
                            let ds' :: [Diagnosis]
ds' =
                                 if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds
                                 then [DiagKind -> String -> TERM DL_FORMULA -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                                       ("Variable in cardinality constraint\n"
                                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ "    has wrong type")
                                       TERM DL_FORMULA
varTerm]
                                 else [Diagnosis]
ds
                                amigDs :: [a] -> [Diagnosis]
amigDs ts :: [a]
ts =
                                 [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
                                  ("Ambiguous types found for\n    pred '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   SORT -> String -> String
forall a. Pretty a => a -> String -> String
showDoc SORT
pn "' in cardinalty " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   "constraint: (showing only two of them)\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   "    '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ([a] -> a
forall a. [a] -> a
head [a]
ts) "', '" String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                   a -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ([a] -> a
forall a. [a] -> a
head ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
tail [a]
ts) "'") Range
ran]
                             in Result PRED_SYMB
-> ([PRED_TYPE] -> Result PRED_SYMB)
-> Maybe [PRED_TYPE]
-> Result PRED_SYMB
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> Maybe PRED_SYMB -> Result PRED_SYMB
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds' Maybe PRED_SYMB
forall a. Maybe a
Nothing)
                              (\ ts :: [PRED_TYPE]
ts -> case [PRED_TYPE]
ts of
                                [] -> String -> Result PRED_SYMB
forall a. HasCallStack => String -> a
error "CASL_DL.StatAna: Internal error"
                                [x :: PRED_TYPE
x] -> Result PRED_SYMB
-> (PRED_TYPE -> Result PRED_SYMB)
-> Maybe PRED_TYPE
-> Result PRED_SYMB
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
                                         (PRED_SYMB -> Result PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return (PRED_SYMB -> Result PRED_SYMB) -> PRED_SYMB -> Result PRED_SYMB
forall a b. (a -> b) -> a -> b
$
                                            SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
pn PRED_TYPE
x Range
nullRange)
                                         (\ pt :: PRED_TYPE
pt -> if PRED_TYPE
x PRED_TYPE -> PRED_TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_TYPE
pt
                                                  then PRED_SYMB -> Result PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return PRED_SYMB
ps
                                                  else PRED_SYMB -> Result PRED_SYMB
forall a a. (GetRange a, Pretty a) => a -> Result a
noPredTypeErr PRED_SYMB
ps)
                                         (PRED_SYMB -> Maybe PRED_TYPE
getType PRED_SYMB
ps)
                                _ -> Result PRED_SYMB
-> (PRED_TYPE -> Result PRED_SYMB)
-> Maybe PRED_TYPE
-> Result PRED_SYMB
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> Maybe PRED_SYMB -> Result PRED_SYMB
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([PRED_TYPE] -> [Diagnosis]
forall a. Pretty a => [a] -> [Diagnosis]
amigDs [PRED_TYPE]
ts) Maybe PRED_SYMB
forall a. Maybe a
Nothing)
                                           (\ pt :: PRED_TYPE
pt -> if PRED_TYPE
pt PRED_TYPE -> [PRED_TYPE] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PRED_TYPE]
ts
                                                    then PRED_SYMB -> Result PRED_SYMB
forall (m :: * -> *) a. Monad m => a -> m a
return PRED_SYMB
ps
                                                    else PRED_SYMB -> Result PRED_SYMB
forall a a. (GetRange a, Pretty a) => a -> Result a
noPredTypeErr PRED_SYMB
ps)
                                           (PRED_SYMB -> Maybe PRED_TYPE
getType PRED_SYMB
ps))
                              Maybe [PRED_TYPE]
mts
                   let isNatTerm :: [Diagnosis]
isNatTerm =
                           if GlobalAnnos -> TERM DL_FORMULA -> Bool
forall f. GlobalAnnos -> TERM f -> Bool
isNumberTerm (Sign DL_FORMULA CASL_DLSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos Sign DL_FORMULA CASL_DLSign
sign) TERM DL_FORMULA
n2 Bool -> Bool -> Bool
&&
                              SORT -> String
forall a. Show a => a -> String
show SORT
n_sort String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "nonNegativeInteger"
                           then []
                           else [DiagKind -> String -> TERM DL_FORMULA -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                                    ("The second argument of a\n    " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                     "cardinality constrain must be a " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                     "number literal\n    typeable as " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                     "nonNegativeInteger")
                                    TERM DL_FORMULA
natTerm]
                       ds :: [Diagnosis]
ds = [Diagnosis]
isNatTerm
                   [Diagnosis] -> Result ()
appendDiags [Diagnosis]
ds
                   if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
ds
                    then DL_FORMULA -> Result DL_FORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CardType
-> PRED_SYMB
-> TERM DL_FORMULA
-> TERM DL_FORMULA
-> Maybe (FORMULA DL_FORMULA)
-> Range
-> DL_FORMULA
Cardinality CardType
ct PRED_SYMB
ps' TERM DL_FORMULA
v2 TERM DL_FORMULA
n2 Maybe (FORMULA DL_FORMULA)
qualTerm Range
ran)
                    else [Diagnosis] -> Maybe DL_FORMULA -> Result DL_FORMULA
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe DL_FORMULA
forall a. Maybe a
Nothing
    where
          getType :: PRED_SYMB -> Maybe PRED_TYPE
getType ps :: PRED_SYMB
ps = case PRED_SYMB
ps of
                        Pred_name _ -> Maybe PRED_TYPE
forall a. Maybe a
Nothing
                        Qual_pred_name _ pType :: PRED_TYPE
pType _ -> PRED_TYPE -> Maybe PRED_TYPE
forall a. a -> Maybe a
Just PRED_TYPE
pType
          isNumberTerm :: GlobalAnnos -> TERM f -> Bool
isNumberTerm ga :: GlobalAnnos
ga t :: TERM f
t =
              Bool
-> ((SORT, [TERM f]) -> Bool) -> Maybe (SORT, [TERM f]) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((SORT -> [TERM f] -> Bool) -> (SORT, [TERM f]) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (GlobalAnnos -> SORT -> [TERM f] -> Bool
forall f. GlobalAnnos -> SORT -> [TERM f] -> Bool
isNumber GlobalAnnos
ga)) (TERM f -> Maybe (SORT, [TERM f])
forall f. TERM f -> Maybe (SORT, [TERM f])
splitApplM TERM f
t)

          noPredTypeErr :: a -> Result a
noPredTypeErr ps :: a
ps = [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result
              [DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "no predicate with \n    given type found" a
ps]
              Maybe a
forall a. Maybe a
Nothing

          sub_sort_of_subj :: a -> SORT -> Set PredType -> Result [PRED_TYPE]
sub_sort_of_subj pn :: a
pn v_sort :: SORT
v_sort typeSet :: Set PredType
typeSet =
              (Result [PRED_TYPE] -> PredType -> Result [PRED_TYPE])
-> Result [PRED_TYPE] -> [PredType] -> Result [PRED_TYPE]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (Result ds :: [Diagnosis]
ds mv :: Maybe [PRED_TYPE]
mv) pt :: PredType
pt ->
                         case PredType -> [SORT]
predArgs PredType
pt of
                         (s :: SORT
s : _)
                             | Sign DL_FORMULA CASL_DLSign -> SORT -> SORT -> Bool
forall f e. Sign f e -> SORT -> SORT -> Bool
leqSort Sign DL_FORMULA CASL_DLSign
sign SORT
v_sort SORT
s ->
                                 Result [PRED_TYPE]
-> ([PRED_TYPE] -> Result [PRED_TYPE])
-> Maybe [PRED_TYPE]
-> Result [PRED_TYPE]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Diagnosis] -> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds (Maybe [PRED_TYPE] -> Result [PRED_TYPE])
-> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a b. (a -> b) -> a -> b
$ [PRED_TYPE] -> Maybe [PRED_TYPE]
forall a. a -> Maybe a
Just [PredType -> PRED_TYPE
toPRED_TYPE PredType
pt])
                                       (\ l :: [PRED_TYPE]
l -> [Diagnosis] -> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds (Maybe [PRED_TYPE] -> Result [PRED_TYPE])
-> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a b. (a -> b) -> a -> b
$
                                                   [PRED_TYPE] -> Maybe [PRED_TYPE]
forall a. a -> Maybe a
Just ([PRED_TYPE] -> Maybe [PRED_TYPE])
-> [PRED_TYPE] -> Maybe [PRED_TYPE]
forall a b. (a -> b) -> a -> b
$ [PRED_TYPE]
l [PRED_TYPE] -> [PRED_TYPE] -> [PRED_TYPE]
forall a. [a] -> [a] -> [a]
++ [PredType -> PRED_TYPE
toPRED_TYPE PredType
pt])
                                       Maybe [PRED_TYPE]
mv
                             | Bool
otherwise ->
                                 [Diagnosis] -> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe [PRED_TYPE]
mv
                         _ -> [Diagnosis] -> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a. [Diagnosis] -> Maybe a -> Result a
Result ([Diagnosis]
ds [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ [DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                                                  ("no propositional " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                                   "symbols are allowed\n    "
                                                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ "within cardinality " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                                   "constraints")
                                                  a
pn]) Maybe [PRED_TYPE]
mv
                  ) ([Diagnosis] -> Maybe [PRED_TYPE] -> Result [PRED_TYPE]
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe [PRED_TYPE]
forall a. Maybe a
Nothing) ([PredType] -> Result [PRED_TYPE])
-> [PredType] -> Result [PRED_TYPE]
forall a b. (a -> b) -> a -> b
$ Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
typeSet

-- | symbol map analysis
checkSymbolMapDL :: RawSymbolMap -> Result RawSymbolMap
{- - implement a symbol mapping that forbids mapping of predefined symbols
       from emptySign
       use from Logic.Logic.Logic and from CASL:
          matches, symOf, statSymbMapItems
-}
checkSymbolMapDL :: RawSymbolMap -> Result RawSymbolMap
checkSymbolMapDL rsm :: RawSymbolMap
rsm =
    let checkSourceSymbol :: RawSymbol -> p -> [RawSymbol] -> [RawSymbol]
checkSourceSymbol sSym :: RawSymbol
sSym _ =
              if (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> RawSymbol -> Bool
`matches` RawSymbol
sSym) [Symbol]
symOfPredefinedSign then
                  (RawSymbol
sSym RawSymbol -> [RawSymbol] -> [RawSymbol]
forall a. a -> [a] -> [a]
:) else [RawSymbol] -> [RawSymbol]
forall a. a -> a
id
        syms :: [RawSymbol]
syms = (RawSymbol -> RawSymbol -> [RawSymbol] -> [RawSymbol])
-> [RawSymbol] -> RawSymbolMap -> [RawSymbol]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey RawSymbol -> RawSymbol -> [RawSymbol] -> [RawSymbol]
forall p. RawSymbol -> p -> [RawSymbol] -> [RawSymbol]
checkSourceSymbol [] RawSymbolMap
rsm
    in if [RawSymbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RawSymbol]
syms
       then RawSymbolMap -> Result RawSymbolMap
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbolMap
rsm
       else String -> [RawSymbol] -> Result RawSymbolMap
forall a b. (GetRange a, Pretty a) => String -> a -> Result b
mkError "Predefined CASL_DL symbols cannot be mapped" [RawSymbol]
syms

symOfPredefinedSign :: [Symbol]
symOfPredefinedSign :: [Symbol]
symOfPredefinedSign = Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList (Set Symbol -> [Symbol])
-> ([Set Symbol] -> Set Symbol) -> [Set Symbol] -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Symbol] -> [Symbol]) -> [Set Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign () () -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf Sign () ()
predefSign

isNumber :: GlobalAnnos -> Id -> [TERM f] -> Bool
isNumber :: GlobalAnnos -> SORT -> [TERM f] -> Bool
isNumber = SplitM (TERM f) -> GlobalAnnos -> SORT -> [TERM f] -> Bool
forall a. SplitM a -> GlobalAnnos -> SORT -> [a] -> Bool
isGenNum SplitM (TERM f)
forall f. TERM f -> Maybe (SORT, [TERM f])
splitApplM

splitApplM :: TERM f -> Maybe (Id, [TERM f])
splitApplM :: TERM f -> Maybe (SORT, [TERM f])
splitApplM t :: TERM f
t = case TERM f
t of
    Application {} -> (SORT, [TERM f]) -> Maybe (SORT, [TERM f])
forall a. a -> Maybe a
Just ((SORT, [TERM f]) -> Maybe (SORT, [TERM f]))
-> (SORT, [TERM f]) -> Maybe (SORT, [TERM f])
forall a b. (a -> b) -> a -> b
$ TERM f -> (SORT, [TERM f])
forall f. TERM f -> (SORT, [TERM f])
splitAppl TERM f
t
    _ -> Maybe (SORT, [TERM f])
forall a. Maybe a
Nothing

splitAppl :: TERM f -> (Id, [TERM f])
splitAppl :: TERM f -> (SORT, [TERM f])
splitAppl t :: TERM f
t = case TERM f
t of
              Application oi :: OP_SYMB
oi ts :: [TERM f]
ts _ -> (OP_SYMB -> SORT
op_id OP_SYMB
oi, [TERM f]
ts)
              _ -> String -> (SORT, [TERM f])
forall a. HasCallStack => String -> a
error "splitAppl: no Application found"

-- | extract the Id from any OP_SYMB
op_id :: OP_SYMB -> Id
op_id :: OP_SYMB -> SORT
op_id op :: OP_SYMB
op = case OP_SYMB
op of
           Qual_op_name x :: SORT
x _ _ -> SORT
x
           Op_name x :: SORT
x -> SORT
x